Analysis I, Appendix A.3: The structure of proofs

Some examples of proofs

Proposition A.3.1

example {A B C D: Prop} (hAC: A → C) (hCD: C → D) (hDB: D → B): A → B := byA:PropB:PropC:PropD:ProphAC:A → ChCD:C → DhDB:D → B⊢ A → B
  intro hA:PropB:PropC:PropD:ProphAC:A → ChCD:C → DhDB:D → Bh:A⊢ B
  apply hAC at hA:PropB:PropC:PropD:ProphAC:A → ChCD:C → DhDB:D → Bh:C⊢ B
  apply hCD at hA:PropB:PropC:PropD:ProphAC:A → ChCD:C → DhDB:D → Bh:D⊢ B
  apply hDB at hA:PropB:PropC:PropD:ProphAC:A → ChCD:C → DhDB:D → Bh:B⊢ B
  exact hAll goals completed! 🐙

Proposition A.3.2

example {x:ℝ} : x = Real.pi → Real.sin (x/2) + 1 = 2 := byx:ℝ⊢ x = Real.pi → Real.sin (x / 2) + 1 = 2
  intro hx:ℝh:x = Real.pi⊢ Real.sin (x / 2) + 1 = 2
  -- congr() produces an equality (or similar relation) from one or more existing relations, such as `h`, by substituting that relation in every location marked with a `$` sign followed by that relation, for instance `h` would be substituted at every location of `$h`.
  replace h := congr($h/2)x:ℝh:?_mvar.316 := id (congrArg (fun x => x / 2) _fvar.312)⊢ Real.sin (x / 2) + 1 = 2
  replace h := congr(Real.sin $h)x:ℝh:?_mvar.500 := id (congrArg Real.sin _fvar.494)⊢ Real.sin (x / 2) + 1 = 2
  simp at hx:ℝh:Real.sin (x / 2) = 1⊢ Real.sin (x / 2) + 1 = 2
  replace h := congr($h + 1)x:ℝh:?_mvar.767 := id (congrArg (fun x => x + 1) _fvar.762)⊢ Real.sin (x / 2) + 1 = 2
  convert hh.e'_3x:ℝh:?_mvar.767 := id (congrArg (fun x => x + 1) _fvar.762)⊢ 2 = 1 + 1
  norm_numAll goals completed! 🐙

Proposition A.3.1, alternate proof

example {A B C D: Prop} (hAC: A → C) (hCD: C → D) (hDB: D → B): A → B := byA:PropB:PropC:PropD:ProphAC:A → ChCD:C → DhDB:D → B⊢ A → B
  intro hA:PropB:PropC:PropD:ProphAC:A → ChCD:C → DhDB:D → Bh:A⊢ B
  suffices hD : DA:PropB:PropC:PropD:ProphAC:A → ChCD:C → DhDB:D → Bh:AhD:D⊢ BhDA:PropB:PropC:PropD:ProphAC:A → ChCD:C → DhDB:D → Bh:A⊢ D
  .A:PropB:PropC:PropD:ProphAC:A → ChCD:C → DhDB:D → Bh:AhD:D⊢ B exact hDB hDAll goals completed! 🐙
  suffices hC : ChDA:PropB:PropC:PropD:ProphAC:A → ChCD:C → DhDB:D → Bh:AhC:C⊢ DhCA:PropB:PropC:PropD:ProphAC:A → ChCD:C → DhDB:D → Bh:A⊢ C
  .hDA:PropB:PropC:PropD:ProphAC:A → ChCD:C → DhDB:D → Bh:AhC:C⊢ D exact hCD hCAll goals completed! 🐙
  exact hAC hAll goals completed! 🐙

Proposition A.3.2, alternate proof

example {x:ℝ} : x = Real.pi → Real.sin (x/2) + 1 = 2 := byx:ℝ⊢ x = Real.pi → Real.sin (x / 2) + 1 = 2
  intro hx:ℝh:x = Real.pi⊢ Real.sin (x / 2) + 1 = 2
  suffices h1 : Real.sin (x/2) = 1x:ℝh:x = Real.pih1:Real.sin (x / 2) = 1⊢ Real.sin (x / 2) + 1 = 2h1x:ℝh:x = Real.pi⊢ Real.sin (x / 2) = 1
  .x:ℝh:x = Real.pih1:Real.sin (x / 2) = 1⊢ Real.sin (x / 2) + 1 = 2 simp [h1]x:ℝh:x = Real.pih1:Real.sin (x / 2) = 1⊢ 1 + 1 = 2
    norm_numAll goals completed! 🐙
  suffices h2 : x/2 = Real.pi/2h1x:ℝh:x = Real.pih2:x / 2 = Real.pi / 2⊢ Real.sin (x / 2) = 1h2x:ℝh:x = Real.pi⊢ x / 2 = Real.pi / 2
  .h1x:ℝh:x = Real.pih2:x / 2 = Real.pi / 2⊢ Real.sin (x / 2) = 1 simp [h2]All goals completed! 🐙
  simp [h]All goals completed! 🐙

Proposition A.3.3

example {r:ℝ} (h: 0 < r) (h': r < 1) : Summable (fun n:ℕ ↦ n * r^n) := byr:ℝh:0 < rh':r < 1⊢ Summable fun n => ↑n * r ^ n
  apply summable_of_ratio_test_tendsto_lt_one h' _ _r:ℝh:0 < rh':r < 1⊢ ∀ᶠ (n : ℕ) in Filter.atTop, ↑n * r ^ n ≠ 0r:ℝh:0 < rh':r < 1⊢ Filter.Tendsto (fun n => ‖↑(n + 1) * r ^ (n + 1)‖ / ‖↑n * r ^ n‖) Filter.atTop (nhds r)
  .r:ℝh:0 < rh':r < 1⊢ ∀ᶠ (n : ℕ) in Filter.atTop, ↑n * r ^ n ≠ 0 simp [Filter.eventually_atTop]r:ℝh:0 < rh':r < 1⊢ ∃ a, ∀ (b : ℕ), a ≤ b → ¬b = 0 ∧ (r = 0 → b = 0)
    use 1hr:ℝh:0 < rh':r < 1⊢ ∀ (b : ℕ), 1 ≤ b → ¬b = 0 ∧ (r = 0 → b = 0)
    intro b hbhr:ℝh:0 < rh':r < 1b:ℕhb:1 ≤ b⊢ ¬b = 0 ∧ (r = 0 → b = 0)
    simp [show b ≠ 0 by linarith, show r ≠ 0 by linarith]All goals completed! 🐙
  suffices hconv: Filter.atTop.Tendsto (fun n:ℕ ↦ r * ((n+1) / n)) (nhds r)r:ℝh:0 < rh':r < 1hconv:Filter.Tendsto (fun n => r * ((↑n + 1) / ↑n)) Filter.atTop (nhds r)⊢ Filter.Tendsto (fun n => ‖↑(n + 1) * r ^ (n + 1)‖ / ‖↑n * r ^ n‖) Filter.atTop (nhds r)hconvr:ℝh:0 < rh':r < 1⊢ Filter.Tendsto (fun n => r * ((↑n + 1) / ↑n)) Filter.atTop (nhds r)
  .r:ℝh:0 < rh':r < 1hconv:Filter.Tendsto (fun n => r * ((↑n + 1) / ↑n)) Filter.atTop (nhds r)⊢ Filter.Tendsto (fun n => ‖↑(n + 1) * r ^ (n + 1)‖ / ‖↑n * r ^ n‖) Filter.atTop (nhds r) apply hconv.congr'r:ℝh:0 < rh':r < 1hconv:Filter.Tendsto (fun n => r * ((↑n + 1) / ↑n)) Filter.atTop (nhds r)⊢ (fun n => r * ((↑n + 1) / ↑n)) =ᶠ[Filter.atTop] fun n => ‖↑(n + 1) * r ^ (n + 1)‖ / ‖↑n * r ^ n‖
    simp [Filter.EventuallyEq, Filter.eventually_atTop]r:ℝh:0 < rh':r < 1hconv:Filter.Tendsto (fun n => r * ((↑n + 1) / ↑n)) Filter.atTop (nhds r)⊢ ∃ a, ∀ (b : ℕ), a ≤ b → r * ((↑b + 1) / ↑b) = |↑b + 1| * |r| ^ (b + 1) / (↑b * |r| ^ b)
    use 1hr:ℝh:0 < rh':r < 1hconv:Filter.Tendsto (fun n => r * ((↑n + 1) / ↑n)) Filter.atTop (nhds r)⊢ ∀ (b : ℕ), 1 ≤ b → r * ((↑b + 1) / ↑b) = |↑b + 1| * |r| ^ (b + 1) / (↑b * |r| ^ b)
    intro b hbhr:ℝh:0 < rh':r < 1hconv:Filter.Tendsto (fun n => r * ((↑n + 1) / ↑n)) Filter.atTop (nhds r)b:ℕhb:1 ≤ b⊢ r * ((↑b + 1) / ↑b) = |↑b + 1| * |r| ^ (b + 1) / (↑b * |r| ^ b)
    have : b > 0 := byr:ℝh:0 < rh':r < 1⊢ Summable fun n => ↑n * r ^ n linarithAll goals completed! 🐙
    have hb1 : (b+1:ℝ) > 0 := byr:ℝh:0 < rh':r < 1⊢ Summable fun n => ↑n * r ^ n linarithAll goals completed! 🐙
    simp [abs_of_pos h, abs_of_pos hb1]hr:ℝh:0 < rh':r < 1hconv:Filter.Tendsto (fun n => r * ((↑n + 1) / ↑n)) Filter.atTop (nhds r)b:ℕhb:1 ≤ bthis:_fvar.25009 > 0 := ?_mvar.25050hb1:↑_fvar.25009 + 1 > 0 := ?_mvar.27080⊢ r * ((↑b + 1) / ↑b) = (↑b + 1) * r ^ (b + 1) / (↑b * r ^ b)
    field_simphr:ℝh:0 < rh':r < 1hconv:Filter.Tendsto (fun n => r * ((↑n + 1) / ↑n)) Filter.atTop (nhds r)b:ℕhb:1 ≤ bthis:_fvar.25009 > 0 := ?_mvar.25050hb1:↑_fvar.25009 + 1 > 0 := ?_mvar.27080⊢ r * (↑b + 1) * (↑b * r ^ b) = (↑b + 1) * r ^ (b + 1) * ↑b
    ring_nfAll goals completed! 🐙
  suffices hconv : Filter.atTop.Tendsto (fun n:ℕ ↦ ((n+1:ℝ) / n)) (nhds 1)hconvr:ℝh:0 < rh':r < 1hconv:Filter.Tendsto (fun n => (↑n + 1) / ↑n) Filter.atTop (nhds 1)⊢ Filter.Tendsto (fun n => r * ((↑n + 1) / ↑n)) Filter.atTop (nhds r)hconvr:ℝh:0 < rh':r < 1⊢ Filter.Tendsto (fun n => (↑n + 1) / ↑n) Filter.atTop (nhds 1)
  .hconvr:ℝh:0 < rh':r < 1hconv:Filter.Tendsto (fun n => (↑n + 1) / ↑n) Filter.atTop (nhds 1)⊢ Filter.Tendsto (fun n => r * ((↑n + 1) / ↑n)) Filter.atTop (nhds r) convert hconv.const_mul rh.e'_5.h.e'_3r:ℝh:0 < rh':r < 1hconv:Filter.Tendsto (fun n => (↑n + 1) / ↑n) Filter.atTop (nhds 1)⊢ r = r * 1
    simpAll goals completed! 🐙
  suffices hconv : Filter.atTop.Tendsto (fun n:ℕ ↦ 1 + 1/(n:ℝ)) (nhds 1)hconvr:ℝh:0 < rh':r < 1hconv:Filter.Tendsto (fun n => 1 + 1 / ↑n) Filter.atTop (nhds 1)⊢ Filter.Tendsto (fun n => (↑n + 1) / ↑n) Filter.atTop (nhds 1)hconvr:ℝh:0 < rh':r < 1⊢ Filter.Tendsto (fun n => 1 + 1 / ↑n) Filter.atTop (nhds 1)
  .hconvr:ℝh:0 < rh':r < 1hconv:Filter.Tendsto (fun n => 1 + 1 / ↑n) Filter.atTop (nhds 1)⊢ Filter.Tendsto (fun n => (↑n + 1) / ↑n) Filter.atTop (nhds 1) apply hconv.congr'hconvr:ℝh:0 < rh':r < 1hconv:Filter.Tendsto (fun n => 1 + 1 / ↑n) Filter.atTop (nhds 1)⊢ (fun n => 1 + 1 / ↑n) =ᶠ[Filter.atTop] fun n => (↑n + 1) / ↑n
    simp [Filter.EventuallyEq, Filter.eventually_atTop]hconvr:ℝh:0 < rh':r < 1hconv:Filter.Tendsto (fun n => 1 + 1 / ↑n) Filter.atTop (nhds 1)⊢ ∃ a, ∀ (b : ℕ), a ≤ b → 1 + (↑b)⁻¹ = (↑b + 1) / ↑b
    use 1hr:ℝh:0 < rh':r < 1hconv:Filter.Tendsto (fun n => 1 + 1 / ↑n) Filter.atTop (nhds 1)⊢ ∀ (b : ℕ), 1 ≤ b → 1 + (↑b)⁻¹ = (↑b + 1) / ↑b
    intro b hbhr:ℝh:0 < rh':r < 1hconv:Filter.Tendsto (fun n => 1 + 1 / ↑n) Filter.atTop (nhds 1)b:ℕhb:1 ≤ b⊢ 1 + (↑b)⁻¹ = (↑b + 1) / ↑b
    have : (b:ℝ) > 0 := byr:ℝh:0 < rh':r < 1⊢ Summable fun n => ↑n * r ^ n norm_castAll goals completed! 🐙
    field_simpAll goals completed! 🐙
  suffices hconv : Filter.atTop.Tendsto (fun n:ℕ ↦ 1/(n:ℝ)) (nhds 0)hconvr:ℝh:0 < rh':r < 1hconv:Filter.Tendsto (fun n => 1 / ↑n) Filter.atTop (nhds 0)⊢ Filter.Tendsto (fun n => 1 + 1 / ↑n) Filter.atTop (nhds 1)hconvr:ℝh:0 < rh':r < 1⊢ Filter.Tendsto (fun n => 1 / ↑n) Filter.atTop (nhds 0)
  .hconvr:ℝh:0 < rh':r < 1hconv:Filter.Tendsto (fun n => 1 / ↑n) Filter.atTop (nhds 0)⊢ Filter.Tendsto (fun n => 1 + 1 / ↑n) Filter.atTop (nhds 1) convert hconv.const_add 1h.e'_5.h.e'_3r:ℝh:0 < rh':r < 1hconv:Filter.Tendsto (fun n => 1 / ↑n) Filter.atTop (nhds 0)⊢ 1 = 1 + 0
    simpAll goals completed! 🐙
  exact tendsto_one_div_atTop_nhds_zero_natAll goals completed! 🐙

Proposition A.3.1, third proof

example {A B C D: Prop} (hAC: A → C) (hCD: C → D) (hDB: D → B): A → B := byA:PropB:PropC:PropD:ProphAC:A → ChCD:C → DhDB:D → B⊢ A → B
  intro hA:PropB:PropC:PropD:ProphAC:A → ChCD:C → DhDB:D → Bh:A⊢ B
  suffices hD : DA:PropB:PropC:PropD:ProphAC:A → ChCD:C → DhDB:D → Bh:AhD:D⊢ BhDA:PropB:PropC:PropD:ProphAC:A → ChCD:C → DhDB:D → Bh:A⊢ D
  .A:PropB:PropC:PropD:ProphAC:A → ChCD:C → DhDB:D → Bh:AhD:D⊢ B exact hDB hDAll goals completed! 🐙
  have hC : C := hAC hhDA:PropB:PropC:PropD:ProphAC:A → ChCD:C → DhDB:D → Bh:AhC:_fvar.53662 := @_fvar.53664 _fvar.53668⊢ D
  exact hCD hCAll goals completed! 🐙

Proposition A.3.4

example {A B C D E F G H I:Prop} (hAE: A → E) (hEB: E ∧ B → F) (hADG : A → G → D) (hHI: H ∨ I) (hFHC : F ∧ H → C) (hAHG : A ∧ H → G) (hIG: I → G) (hIGC: G → C) : A ∧ B → C ∧ D := byA:PropB:PropC:PropD:PropE:PropF:PropG:PropH:PropI:ProphAE:A → EhEB:E ∧ B → FhADG:A → G → DhHI:H ∨ IhFHC:F ∧ H → ChAHG:A ∧ H → GhIG:I → GhIGC:G → C⊢ A ∧ B → C ∧ D
  intro ⟨ hA, hB ⟩A:PropB:PropC:PropD:PropE:PropF:PropG:PropH:PropI:ProphAE:A → EhEB:E ∧ B → FhADG:A → G → DhHI:H ∨ IhFHC:F ∧ H → ChAHG:A ∧ H → GhIG:I → GhIGC:G → ChA:AhB:B⊢ C ∧ D
  have hE : E := hAE hAA:PropB:PropC:PropD:PropE:PropF:PropG:PropH:PropI:ProphAE:A → EhEB:E ∧ B → FhADG:A → G → DhHI:H ∨ IhFHC:F ∧ H → ChAHG:A ∧ H → GhIG:I → GhIGC:G → ChA:AhB:BhE:_fvar.53751 := @_fvar.53756 _fvar.53788⊢ C ∧ D
  have hF : F := hEB ⟨hE, hB⟩A:PropB:PropC:PropD:PropE:PropF:PropG:PropH:PropI:ProphAE:A → EhEB:E ∧ B → FhADG:A → G → DhHI:H ∨ IhFHC:F ∧ H → ChAHG:A ∧ H → GhIG:I → GhIGC:G → ChA:AhB:BhE:_fvar.53751 := @_fvar.53756 _fvar.53788hF:_fvar.53752 := @_fvar.53757 ⋯⊢ C ∧ D
  suffices hCG : C ∧ GA:PropB:PropC:PropD:PropE:PropF:PropG:PropH:PropI:ProphAE:A → EhEB:E ∧ B → FhADG:A → G → DhHI:H ∨ IhFHC:F ∧ H → ChAHG:A ∧ H → GhIG:I → GhIGC:G → ChA:AhB:BhE:_fvar.53751 := @_fvar.53756 _fvar.53788hF:_fvar.53752 := @_fvar.53757 ⋯hCG:C ∧ G⊢ C ∧ DhCGA:PropB:PropC:PropD:PropE:PropF:PropG:PropH:PropI:ProphAE:A → EhEB:E ∧ B → FhADG:A → G → DhHI:H ∨ IhFHC:F ∧ H → ChAHG:A ∧ H → GhIG:I → GhIGC:G → ChA:AhB:BhE:_fvar.53751 := @_fvar.53756 _fvar.53788hF:_fvar.53752 := @_fvar.53757 ⋯⊢ C ∧ G
  .A:PropB:PropC:PropD:PropE:PropF:PropG:PropH:PropI:ProphAE:A → EhEB:E ∧ B → FhADG:A → G → DhHI:H ∨ IhFHC:F ∧ H → ChAHG:A ∧ H → GhIG:I → GhIGC:G → ChA:AhB:BhE:_fvar.53751 := @_fvar.53756 _fvar.53788hF:_fvar.53752 := @_fvar.53757 ⋯hCG:C ∧ G⊢ C ∧ D obtain ⟨ hC, hG ⟩ := hCGintroA:PropB:PropC:PropD:PropE:PropF:PropG:PropH:PropI:ProphAE:A → EhEB:E ∧ B → FhADG:A → G → DhHI:H ∨ IhFHC:F ∧ H → ChAHG:A ∧ H → GhIG:I → GhIGC:G → ChA:AhB:BhE:_fvar.53751 := @_fvar.53756 _fvar.53788hF:_fvar.53752 := @_fvar.53757 ⋯hC:ChG:G⊢ C ∧ D
    have hD : D := hADG hA hGintroA:PropB:PropC:PropD:PropE:PropF:PropG:PropH:PropI:ProphAE:A → EhEB:E ∧ B → FhADG:A → G → DhHI:H ∨ IhFHC:F ∧ H → ChAHG:A ∧ H → GhIG:I → GhIGC:G → ChA:AhB:BhE:_fvar.53751 := @_fvar.53756 _fvar.53788hF:_fvar.53752 := @_fvar.53757 ⋯hC:ChG:GhD:_fvar.53750 := @_fvar.53758 _fvar.53788 _fvar.53894⊢ C ∧ D
    exact ⟨hC, hD⟩All goals completed! 🐙
  obtain hH | hI := hHIhCG.inlA:PropB:PropC:PropD:PropE:PropF:PropG:PropH:PropI:ProphAE:A → EhEB:E ∧ B → FhADG:A → G → DhFHC:F ∧ H → ChAHG:A ∧ H → GhIG:I → GhIGC:G → ChA:AhB:BhE:_fvar.53751 := @_fvar.53756 _fvar.53788hF:_fvar.53752 := @_fvar.53757 ⋯hH:H⊢ C ∧ GhCG.inrA:PropB:PropC:PropD:PropE:PropF:PropG:PropH:PropI:ProphAE:A → EhEB:E ∧ B → FhADG:A → G → DhFHC:F ∧ H → ChAHG:A ∧ H → GhIG:I → GhIGC:G → ChA:AhB:BhE:_fvar.53751 := @_fvar.53756 _fvar.53788hF:_fvar.53752 := @_fvar.53757 ⋯hI:I⊢ C ∧ G
  .hCG.inlA:PropB:PropC:PropD:PropE:PropF:PropG:PropH:PropI:ProphAE:A → EhEB:E ∧ B → FhADG:A → G → DhFHC:F ∧ H → ChAHG:A ∧ H → GhIG:I → GhIGC:G → ChA:AhB:BhE:_fvar.53751 := @_fvar.53756 _fvar.53788hF:_fvar.53752 := @_fvar.53757 ⋯hH:H⊢ C ∧ G have hC := hFHC ⟨ hF, hH⟩hCG.inlA:PropB:PropC:PropD:PropE:PropF:PropG:PropH:PropI:ProphAE:A → EhEB:E ∧ B → FhADG:A → G → DhFHC:F ∧ H → ChAHG:A ∧ H → GhIG:I → GhIGC:G → ChA:AhB:BhE:_fvar.53751 := @_fvar.53756 _fvar.53788hF:_fvar.53752 := @_fvar.53757 ⋯hH:HhC:?_mvar.53939 := @_fvar.53760 ⋯⊢ C ∧ G
    have hG := hAHG ⟨hA, hH⟩hCG.inlA:PropB:PropC:PropD:PropE:PropF:PropG:PropH:PropI:ProphAE:A → EhEB:E ∧ B → FhADG:A → G → DhFHC:F ∧ H → ChAHG:A ∧ H → GhIG:I → GhIGC:G → ChA:AhB:BhE:_fvar.53751 := @_fvar.53756 _fvar.53788hF:_fvar.53752 := @_fvar.53757 ⋯hH:HhC:?_mvar.53939 := @_fvar.53760 ⋯hG:?_mvar.53951 := @_fvar.53761 ⋯⊢ C ∧ G
    exact ⟨hC, hG⟩All goals completed! 🐙
  have hG := hIG hIhCG.inrA:PropB:PropC:PropD:PropE:PropF:PropG:PropH:PropI:ProphAE:A → EhEB:E ∧ B → FhADG:A → G → DhFHC:F ∧ H → ChAHG:A ∧ H → GhIG:I → GhIGC:G → ChA:AhB:BhE:_fvar.53751 := @_fvar.53756 _fvar.53788hF:_fvar.53752 := @_fvar.53757 ⋯hI:IhG:?_mvar.53969 := @_fvar.53762 _fvar.53935⊢ C ∧ G
  have hC := hIGC hGhCG.inrA:PropB:PropC:PropD:PropE:PropF:PropG:PropH:PropI:ProphAE:A → EhEB:E ∧ B → FhADG:A → G → DhFHC:F ∧ H → ChAHG:A ∧ H → GhIG:I → GhIGC:G → ChA:AhB:BhE:_fvar.53751 := @_fvar.53756 _fvar.53788hF:_fvar.53752 := @_fvar.53757 ⋯hI:IhG:?_mvar.53969 := @_fvar.53762 _fvar.53935hC:?_mvar.53975 := @_fvar.53763 _fvar.53970⊢ C ∧ G
  exact ⟨hC, hG⟩All goals completed! 🐙

Proposition A.3.5

example {A B C D:Prop} (hBC: B → C) (hAD: A → D) (hCD: D → ¬ C) : A → ¬ B := byA:PropB:PropC:PropD:ProphBC:B → ChAD:A → DhCD:D → ¬C⊢ A → ¬B
  intro hAA:PropB:PropC:PropD:ProphBC:B → ChAD:A → DhCD:D → ¬ChA:A⊢ ¬B
  by_contra hBA:PropB:PropC:PropD:ProphBC:B → ChAD:A → DhCD:D → ¬ChA:AhB:B⊢ False
  have hC : C := hBC hBA:PropB:PropC:PropD:ProphBC:B → ChAD:A → DhCD:D → ¬ChA:AhB:BhC:_fvar.54021 := @_fvar.54023 _fvar.54033⊢ False
  have hD : D := hAD hAA:PropB:PropC:PropD:ProphBC:B → ChAD:A → DhCD:D → ¬ChA:AhB:BhC:_fvar.54021 := @_fvar.54023 _fvar.54033hD:_fvar.54022 := @_fvar.54024 _fvar.54028⊢ False
  have hC' : ¬ C := hCD hDA:PropB:PropC:PropD:ProphBC:B → ChAD:A → DhCD:D → ¬ChA:AhB:BhC:_fvar.54021 := @_fvar.54023 _fvar.54033hD:_fvar.54022 := @_fvar.54024 _fvar.54028hC':¬_fvar.54021 := @_fvar.54025 _fvar.54042⊢ False
  contradictionAll goals completed! 🐙