SCM.ID.Discrete ID
Discrete ID support: point-mass algebra, positivity conditions, and the executable checker for finite/discrete identification formulas.
Mass 5 core · 16 supporting This file provides the finite-measure primitives used by the discrete ID lane: singleton masses, marginal singleton masses, and conditional masses as ratios. ★ valuesOn_measure_eq_of_singletonMass_eq
Finite masses for discrete ID
This file provides the finite-measure primitives used by the discrete ID lane: singleton masses, marginal singleton masses, and conditional masses as ratios. The definitions are intentionally point-mass based, so later ID proofs can state positivity on the actual denominators used by a formula.
The main API includes:
* singletonMass, marginalMass, conditionalMass, and
conditionalDenominator for writing finite observational formulas.
* measure_eq_of_singletonMass_eq and valuesOn_measure_eq_of_singletonMass_eq,
which reduce equality of finite/countable measures to equality of all singleton
masses.
* singletonMass_map_eq_sum_fiber, singletonMass_comp_eq_sum, and the
point-mass specializations for constant or degenerate mixtures.
* conditionalMass_mul_denominator, the algebraic cancellation lemma that
recovers the joint point mass from a conditional-mass ratio once the actual
denominator is nonzero and finite.
For a measure on a measurable space and a point in that space, the singleton mass is the mass that the measure assigns to the set containing that point alone.
Definition (Lean source)
For a measure, a map to a second measurable space, proof that the map is measurable, and a value in that second space, the marginal mass is the singleton mass of that value under the pushforward of the measure by the map.
Definition (Lean source)
For a measure on a product of two measurable spaces, a value of the first coordinate, and a value of the second coordinate, the conditional mass is the joint singleton mass at the two values divided by the singleton mass of the second value under the second-coordinate marginal.
Definition (Lean source)
For a measure on a product of two measurable spaces and a value of the second coordinate, the conditional denominator is the singleton mass of that value under the measure's second-coordinate marginal.
Definition (Lean source)
For two measures on a finite-coordinate product over countable value spaces, if every value assignment carries the same singleton point mass under both measures, then the two measures are equal.
Formal statement
Proof (Lean source)
16 supporting declarations (lemmas, instances)
-
singletonMass_applytheoremhypothesesconclusionsingletonMass μ x = μ ({x} : Set α)Proof (Lean source)
@[simp] theorem singletonMass_apply {α : Type*} [MeasurableSpace α] (μ : Measure α) (x : α) : singletonMass μ x = μ ({x} : Set α) := rfl -
measure_eq_of_singletonMass_eqtheorem — Measures on a countable space are equal when all singleton masses agree.Proof (Lean source)
theorem measure_eq_of_singletonMass_eq {α : Type*} [MeasurableSpace α] [Countable α] {μ ν : Measure α} (h : ∀ x : α, singletonMass μ x = singletonMass ν x) : μ = ν := MeasureTheory.Measure.ext_of_singleton h -
eq_of_ae_eq_of_forall_singletonMass_ne_zerotheorem — An almost-everywhere equality is pointwise when every singleton has nonzero mass.Proof (Lean source)
theorem eq_of_ae_eq_of_forall_singletonMass_ne_zero {α β : Type*} [MeasurableSpace α] {μ : Measure α} {f g : α → β} (hμ : ∀ x : α, singletonMass μ x ≠ 0) (hfg : f =ᵐ[μ] g) : ∀ x : α, f x = g x := by intro x by_contra hx have hnull : μ {y | ¬ f y = g y} = 0 := MeasureTheory.ae_iff.mp hfg have hsubset : ({x} : Set α) ⊆ {y | ¬ f y = g y} := by intro y hy have hyx : y = x := by simpa using hy simpa [hyx] using hx have hxzero : singletonMass μ x = 0 := by rw [singletonMass_apply] exact MeasureTheory.measure_mono_null hsubset hnull exact hμ x hxzero -
singletonMass_maptheorem — The singleton mass of a mapped measure is the mass of the corresponding fibre.hypothesesconclusionsingletonMass (μ.map f) y = μ (f ⁻¹' ({y} : Set β))Proof (Lean source)
theorem singletonMass_map {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSingletonClass β] (μ : Measure α) {f : α → β} (hf : Measurable f) (y : β) : singletonMass (μ.map f) y = μ (f ⁻¹' ({y} : Set β)) := by rw [singletonMass_apply, MeasureTheory.Measure.map_apply hf (MeasurableSet.singleton y)] -
singletonMass_map_const_eq_univtheorem — If a measurable map is pointwise constant, the pushed-forward measure has all mass at that constant value.hypothesesconclusionsingletonMass (μ.map f) y0 = μ univProof (Lean source)
theorem singletonMass_map_const_eq_univ {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSingletonClass β] (μ : Measure α) {f : α → β} (hf : Measurable f) (y0 : β) (hconst : ∀ x : α, f x = y0) : singletonMass (μ.map f) y0 = μ univ := by rw [singletonMass_map μ hf y0] congr ext x simp [hconst x] -
singletonMass_map_const_eq_zero_of_netheorem — If a measurable map is pointwise constant at y0, the pushed-forward measure has zero singleton mass at every different value.hypothesesconclusionsingletonMass (μ.map f) y = 0Proof (Lean source)
theorem singletonMass_map_const_eq_zero_of_ne {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSingletonClass β] (μ : Measure α) {f : α → β} (hf : Measurable f) (y0 y : β) (hconst : ∀ x : α, f x = y0) (hy : y ≠ y0) : singletonMass (μ.map f) y = 0 := by rw [singletonMass_map μ hf y] have hpre : f ⁻¹' ({y} : Set β) = (∅ : Set α) := by ext x have hy' : y0 ≠ y := fun h => hy h.symm simp [hconst x, hy'] rw [hpre, MeasureTheory.measure_empty] -
singletonMass_map_const_eq_onetheorem — A pointwise constant measurable map from a probability measure gives unit singleton mass at the constant value.hypothesesconclusionsingletonMass (μ.map f) y0 = 1Proof (Lean source)
theorem singletonMass_map_const_eq_one {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSingletonClass β] (μ : Measure α) {f : α → β} (hf : Measurable f) (y0 : β) (hconst : ∀ x : α, f x = y0) (hμ : μ univ = 1) : singletonMass (μ.map f) y0 = 1 := by rw [singletonMass_map_const_eq_univ μ hf y0 hconst, hμ] -
singletonMass_map_eq_sum_fibertheorem — On a finite measurable-singleton space, the singleton mass of a pushed-forward measure is the finite sum of singleton masses over the fiber.hypothesesconclusionsingletonMass (μ.map f) y = ∑ x : α, if f x = y then singletonMass μ x else 0Proof (Lean source)
theorem singletonMass_map_eq_sum_fiber {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] [Fintype α] [MeasurableSingletonClass α] [MeasurableSingletonClass β] [DecidableEq β] (μ : Measure α) {f : α → β} (hf : Measurable f) (y : β) : singletonMass (μ.map f) y = ∑ x : α, if f x = y then singletonMass μ x else 0 := by classical let s : Finset α := Finset.univ.filter fun x => f x = y have hs : (s : Set α) = f ⁻¹' ({y} : Set β) := by ext x simp [s] calc singletonMass (μ.map f) y = μ (f ⁻¹' ({y} : Set β)) := by exact singletonMass_map μ hf y _ = μ (s : Set α) := by rw [← hs] _ = ∑ x ∈ s, μ ({x} : Set α) := by rw [← MeasureTheory.sum_measure_singleton (μ := μ) (s := s)] _ = ∑ x : α, if f x = y then singletonMass μ x else 0 := by have hsum : (∑ x : α, if f x = y then singletonMass μ x else 0) = ∑ x ∈ s, μ ({x} : Set α) := by simp [singletonMass, s, Finset.sum_filter] exact hsum.symm -
sum_singletonMass_eq_univtheorem — On a finite measurable-singleton space, the sum of all singleton masses is the total mass of the measure.Proof (Lean source)
theorem sum_singletonMass_eq_univ {α : Type*} [MeasurableSpace α] [Fintype α] [MeasurableSingletonClass α] (μ : Measure α) : (∑ x : α, singletonMass μ x) = μ univ := by classical calc (∑ x : α, singletonMass μ x) = ∑ x ∈ (Finset.univ : Finset α), μ ({x} : Set α) := by simp [singletonMass] _ = μ ((Finset.univ : Finset α) : Set α) := by rw [MeasureTheory.sum_measure_singleton] _ = μ univ := by simp -
sum_singletonMass_eq_onetheorem — On a finite measurable-singleton probability space, singleton masses sum to one.Proof (Lean source)
theorem sum_singletonMass_eq_one {α : Type*} [MeasurableSpace α] [Fintype α] [MeasurableSingletonClass α] (μ : Measure α) [IsProbabilityMeasure μ] : (∑ x : α, singletonMass μ x) = 1 := by rw [sum_singletonMass_eq_univ] exact MeasureTheory.measure_univ -
singletonMass_comp_eq_sumtheorem — On a finite source space, the singleton mass of a kernel mixture is the finite weighted sum of the singleton masses of the kernel slices.Proof (Lean source)
theorem singletonMass_comp_eq_sum {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] [Fintype α] [MeasurableSingletonClass α] [MeasurableSingletonClass β] (μ : Measure α) (κ : Kernel α β) (y : β) : singletonMass (κ ∘ₘ μ) y = ∑ x : α, singletonMass μ x * singletonMass (κ x) y := by rw [singletonMass_apply, MeasureTheory.Measure.bind_apply (MeasurableSet.singleton y) κ.aemeasurable] rw [MeasureTheory.lintegral_fintype] simp [singletonMass, mul_comm] -
singletonMass_comp_eq_of_consttheorem — A finite kernel mixture has the common singleton mass of its slices when the finite singleton masses of the mixing measure sum to one.hypothesesα β :μ :Measure ακ :Kernel α βy :βc :hμ :(∑ x : α, singletonMass μ x) = 1hconst :∀ x : α, singletonMass (κ x) y = cconclusionsingletonMass (κ ∘ₘ μ) y = cProof (Lean source)
theorem singletonMass_comp_eq_of_const {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] [Fintype α] [MeasurableSingletonClass α] [MeasurableSingletonClass β] (μ : Measure α) (κ : Kernel α β) (y : β) (c : ENNReal) (hμ : (∑ x : α, singletonMass μ x) = 1) (hconst : ∀ x : α, singletonMass (κ x) y = c) : singletonMass (κ ∘ₘ μ) y = c := by rw [singletonMass_comp_eq_sum] calc (∑ x : α, singletonMass μ x * singletonMass (κ x) y) = ∑ x : α, singletonMass μ x * c := by apply Finset.sum_congr rfl intro x _hx rw [hconst x] _ = (∑ x : α, singletonMass μ x) * c := by rw [Finset.sum_mul] _ = c := by rw [hμ, one_mul] -
singletonMass_comp_eq_of_pointMasstheorem — A finite kernel mixture has the singleton mass of one slice when the mixing measure is a point mass at that slice.hypothesesα β :μ :Measure ακ :Kernel α βx0 :αy :βhμ0 :singletonMass μ x0 = 1hμzero :∀ x : αifx ≠ x0thensingletonMass μ x = 0conclusionsingletonMass (κ ∘ₘ μ) y = singletonMass (κ x0) yProof (Lean source)
theorem singletonMass_comp_eq_of_pointMass {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] [Finite α] [MeasurableSingletonClass α] [MeasurableSingletonClass β] (μ : Measure α) (κ : Kernel α β) (x0 : α) (y : β) (hμ0 : singletonMass μ x0 = 1) (hμzero : ∀ x : α, x ≠ x0 → singletonMass μ x = 0) : singletonMass (κ ∘ₘ μ) y = singletonMass (κ x0) y := by classical letI : Fintype α := ofFinite α rw [singletonMass_comp_eq_sum] rw [Finset.sum_eq_single x0] · rw [hμ0, one_mul] · intro x _hx hx rw [hμzero x hx, zero_mul] · intro hx exact (hx (Finset.mem_univ x0)).elim -
valuesProjection_surjectivetheorem — Coordinate restriction is surjective when every omitted coordinate has at least one default value.hypothesesconclusionSurjective (valuesProjection (Ω := Ω') hJI)Proof (Lean source)
theorem valuesProjection_surjective {M : Type*} {I J : Finset M} {Ω' : M → Type*} [∀ m, MeasurableSpace (Ω' m)] [∀ m : {m // m ∈ I}, Nonempty (Ω' m.val)] (hJI : J ⊆ I) : Surjective (valuesProjection (Ω := Ω') hJI) := by classical intro y refine ⟨fun i => if h : i.val ∈ J then y ⟨i.val, h⟩ else choice (inferInstance : Nonempty (Ω' i.val)), ?_⟩ funext j simp [valuesProjection] -
conditionalDenominator_applytheoremhypothesesconclusionProof (Lean source)
@[simp] theorem conditionalDenominator_apply {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] (μ : Measure (α × β)) (b : β) : conditionalDenominator μ b = singletonMass (μ.map snd) b := rfl -
conditionalMass_mul_denominatortheorem — Multiplying a discrete conditional mass by its actual denominator recovers the joint point mass, provided that denominator is nonzero and finite.hypothesesα β :μ :Measure (α × β)a :αb :βh0 :conditionalDenominator μ b ≠ 0htop :conditionalDenominator μ b ≠ ∞conclusionconditionalMass μ a b * conditionalDenominator μ b = singletonMass μ (a, b)Proof (Lean source)
theorem conditionalMass_mul_denominator {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] (μ : Measure (α × β)) (a : α) (b : β) (h0 : conditionalDenominator μ b ≠ 0) (htop : conditionalDenominator μ b ≠ ∞) : conditionalMass μ a b * conditionalDenominator μ b = singletonMass μ (a, b) := by rw [conditionalMass, conditionalDenominator] exact ENNReal.div_mul_cancel h0 htop
Positive 4 core · 4 supporting The discrete ID lane uses ratio-based conditional masses. ★ map_valuesProjection
Positivity assumptions for discrete ID formulas
The discrete ID lane uses ratio-based conditional masses. This file records the nonzero point-mass assumptions needed to make those ratios meaningful. The default model-level predicate is full observational support on every observed assignment at every fixed slice; later formula-level soundness lemmas can weaken it to only the denominators actually used by a concrete formula.
Important declarations are PositiveMass, DiscretePositive, and
StandardDiscretePositive, together with transport lemmas showing that positive
point mass is preserved by measurable surjections and coordinate projections.
These lemmas turn full observational support into the denominator positivity
needed by conditionalMass.
For a measure on a measurable space, positive point mass means that every point of that space has nonzero singleton mass.
Definition (Lean source)
For a finite node-label set, measurable node-value spaces, and a structural causal model, discrete positivity means that, at every assignment of its fixed variables, the model's observational probability measure assigns nonzero mass to every assignment of its observed variables.
Definition (Lean source)
If a measure assigns nonzero point mass to every value assignment on the full index set, then restricting to the values on a subset of coordinates reached by projection preserves this: the pushed-forward measure still assigns nonzero point mass to every value assignment on that subset.
Formal statement
Proof (Lean source)
For a finite node-label set, measurable node-value spaces, and a structural causal model, standard discrete positivity means that the model is standard and has discrete positivity.
Definition (Lean source)
4 supporting declarations (lemmas, instances)
-
eq_of_ae_eqtheorem — Under positive point mass at every point, almost-everywhere equality is pointwise equality.hypothesesconclusionf x = g xProof (Lean source)
theorem PositiveMass.eq_of_ae_eq {α β : Type*} [MeasurableSpace α] {μ : Measure α} (hμ : PositiveMass μ) {f g : α → β} (hfg : f =ᵐ[μ] g) : ∀ x : α, f x = g x := eq_of_ae_eq_of_forall_singletonMass_ne_zero hμ hfg -
map_of_surjectivetheorem — Positive point mass is preserved by a measurable surjection.Proof (Lean source)
theorem PositiveMass.map_of_surjective {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSingletonClass β] {μ : Measure α} {f : α → β} (hf : Measurable f) (hμ : PositiveMass μ) (hsurj : Surjective f) : PositiveMass (μ.map f) := by intro y rcases hsurj y with ⟨x, hx⟩ rw [singletonMass_map μ hf y] intro hzero have hsubset : ({x} : Set α) ⊆ f ⁻¹' ({y} : Set β) := by intro z hz change f z = y rw [show z = x by simpa using hz, hx] have hle : μ ({x} : Set α) ≤ μ (f ⁻¹' ({y} : Set β)) := MeasureTheory.measure_mono hsubset have hxzero : singletonMass μ x = 0 := by rw [singletonMass_apply] exact le_antisymm (by simpa [hzero] using hle) zero_le exact hμ x hxzero -
of_map_injectivetheorem — Positive point mass can be pulled back across an injective measurable map when the pushed-forward measure is positive at every image value.Proof (Lean source)
theorem PositiveMass.of_map_injective {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSingletonClass β] {μ : Measure α} {f : α → β} (hf : Measurable f) (hinj : Injective f) (hmap : PositiveMass (μ.map f)) : PositiveMass μ := by intro x have hxmap : singletonMass (μ.map f) (f x) ≠ 0 := hmap (f x) rw [singletonMass_map μ hf (f x)] at hxmap have hpre : f ⁻¹' ({f x} : Set β) = ({x} : Set α) := by ext y constructor · intro hy have hfy : f y = f x := by simpa using hy exact hinj hfy · intro hy have hyx : y = x := by simpa using hy simp [hyx] rw [hpre] at hxmap exact hxmap -
conditionalDenominator_ne_zero_of_positive_marginaltheorem — A positive marginal point mass is exactly the nonzero denominator needed by the finite conditional-mass ratio.hypothesesconclusionconditionalDenominator μ b ≠ 0Proof (Lean source)
theorem conditionalDenominator_ne_zero_of_positive_marginal {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure (α × β)} (hμ : PositiveMass (μ.map snd)) (b : β) : conditionalDenominator μ b ≠ 0 := hμ b
Checker 3 core · 5 supporting id_sound_rec proves soundness for the *declarative* success certificate idSucceedsRec (an inductive predicate — an existence claim needing a hand-built derivation). ★ idAlgorithm_sound
The executable ID algorithm and its soundness
id_sound_rec proves soundness for the declarative success certificate
idSucceedsRec (an inductive predicate — an existence claim needing a hand-built
derivation). This file adds the executable checker: a computable
Bool-valued function idAlgorithm that runs Tian's IDENTIFY procedure with a
fuel bound, together with idAlgorithm_sound — when the checker reports true,
the interventional query is identified.
* cFactorReachableRecB — computable, choice-free fuel-bounded IDENTIFY
reachability (mirrors the inductive CFactorReachableRec, using
cComponentSet.any in place of the noncomputable containingCComponent).
* idAlgorithm — the runnable checker: valid intervention, observed query,
and every post-intervention ancestral district recursively reachable.
* idAlgorithm_sound — the public soundness theorem: idAlgorithm … = true implies
IdentifiableUnder … (interventionalQuery X Y) over the standard discrete
positive model class. Obtained from id_sound_rec_discrete through the
structural bridge idAlgorithm_success_toRec.
For a finite population of variables, a SWIG graph, a nonnegative fuel bound, a proposed containing node set, and a target node set, the computable reachability checker returns false at zero fuel, while at positive fuel it accepts exactly the stated one-step or recursively reachable cases.
Definition (Lean source)
For a finite population of variables, a fuel bound, a SWIG graph, an intervention set, and an outcome-node set, the executable ID checker returns true exactly when the intervention is valid, the outcomes are observed and disjoint from intervention random nodes, and every post-intervention ancestral c-component passes the fuel-bounded reachability check.
Definition (Lean source)
Soundness of the executable ID algorithm. When the runnable checker idAlgorithm returns true on the graph G, intervention set X, query Y, and the given fuel bound, the interventional query P(Y ∣ do(X)) is identified within the standard discrete positive model class.
Formal statement
Proof (Lean source)
5 supporting declarations (lemmas, instances)
-
containingCComponent_eq_of_mem_of_subsettheorem — The unique c-component containing a nonempty set S is containingCComponent. Bridges the checker's cComponentSet.any search to the reachability predicate's choice-based containingCComponent.hypothesesN :sharedType u_1G :hne :S.Nonemptyhmem :C' ∈ G.cComponentSethsub :S ⊆ C'conclusioncontainingCComponent G S = C'Proof (Lean source)
theorem containingCComponent_eq_of_mem_of_subset (G : SWIGGraph N) {S C' : Finset (SWIGNode N)} (hne : S.Nonempty) (hmem : C' ∈ G.cComponentSet) (hsub : S ⊆ C') : containingCComponent G S = C' := by classical have hchoose : hne.choose ∈ C' := hsub hne.choose_spec have hcomponent : G.cComponentOf hne.choose = C' := G.cComponentOf_eq_of_mem_cComponentSet hmem hchoose simpa [containingCComponent, hne] using hcomponent -
cComponentSet_nonemptytheorem — Every c-component in a graph's c-component set contains at least one node.hypothesesconclusionC.NonemptyProof (Lean source)
theorem cComponentSet_nonempty (G : SWIGGraph N) {C : Finset (SWIGNode N)} (hmem : C ∈ G.cComponentSet) : C.Nonempty := by classical rw [SWIGGraph.cComponentSet, mem_image] at hmem obtain ⟨v, hv, rfl⟩ := hmem exact ⟨v, G.mem_cComponentOf_self hv⟩ -
cFactorReachableRecB_soundtheorem — Soundness of the computable reachability check. If the fuel-bounded checker accepts, the inductive reachability certificate holds.hypothesesconclusionCFactorReachableRec G T CProof (Lean source)
theorem cFactorReachableRecB_sound (G : SWIGGraph N) : ∀ (fuel : ℕ) (T C : Finset (SWIGNode N)), cFactorReachableRecB G fuel T C = true → CFactorReachableRec G T C := by classical intro fuel induction fuel with | zero => intro T C h simp [cFactorReachableRecB] at h | succ fuel ih => intro T C h simp only [cFactorReachableRecB, Bool.and_eq_true, decide_eq_true_eq] at h rcases h with ⟨⟨hne, hCT⟩, hinner⟩ by_cases hAC : inducedAncestral G T C = C · exact CFactorReachableRec.base hne hCT hAC · by_cases hAT : inducedAncestral G T C = T · have hinner' : (if T = C then true else false) = true := by simpa only [hAT, ↓reduceIte] using hinner have hTC : T = C := by by_contra hTC simp only [hTC, ↓reduceIte] at hinner' exact Bool.false_ne_true hinner' exact elim (hAC (hAT.trans hTC)) · have hex : ∃ C' ∈ (G.induce (inducedAncestral G T C)).cComponentSet, C ⊆ C' ∧ cFactorReachableRecB G fuel C' C = true := by simpa only [hAC, hAT, ↓reduceIte, decide_eq_true_eq] using hinner rcases hex with ⟨C', hC', hCC', hrecB⟩ have hrec : CFactorReachableRec G C' C := ih C' C hrecB have hcontain : containingCComponent (G.induce (inducedAncestral G T C)) C = C' := containingCComponent_eq_of_mem_of_subset (G.induce (inducedAncestral G T C)) hne hC' hCC' exact CFactorReachableRec.step hne hCT hAC hAT (hcontain ▸ hrec) -
instDecidableInterventionValidinstance — For a finite collection of distinguishable node labels, an intervention-variable set, and a SWIG graph, decidability of intervention validity determines whether splitting the graph at that intervention set is valid. -
idAlgorithm_success_toRectheorem — A successful run yields the graphical certificate. idAlgorithm … = true implies the declarative recursive success certificate idSucceedsRec.hypothesesconclusionidSucceedsRec X Y GProof (Lean source)
theorem idAlgorithm_success_toRec (fuel : ℕ) (G : SWIGGraph N) (X : Finset N) (Y : Finset (SWIGNode N)) (h : idAlgorithm fuel G X Y = true) : idSucceedsRec X Y G := by classical unfold idAlgorithm at h by_cases hX : interventionValid X G · simp only [hX, dite_true, Bool.and_eq_true, decide_eq_true_eq] at h rcases h with ⟨⟨hYobs, hdisj⟩, hcert⟩ refine ⟨hX, hYobs, hdisj, ?_⟩ intro S hS rcases hcert S hS with ⟨C, hC, hSC, hrecB⟩ have hSne : S.Nonempty := cComponentSet_nonempty _ hS have hrec : CFactorReachableRec G C S := cFactorReachableRecB_sound G fuel C S hrecB have hcontain : containingCComponent G S = C := containingCComponent_eq_of_mem_of_subset G hSne hC hSC exact hcontain ▸ hrec · simp [hX] at h