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:x / 2 = Real.pi / 2 := id (congrArg (fun x => x / 2) _fvar.317)⊢ Real.sin (x / 2) + 1 = 2
  replace h := congr(Real.sin $h)x:ℝh:Real.sin (x / 2) = Real.sin (Real.pi / 2) := id (congrArg Real.sin _fvar.484)⊢ 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:Real.sin (x / 2) + 1 = 1 + 1 := id (congrArg (fun x => x + 1) _fvar.714)⊢ Real.sin (x / 2) + 1 = 2
  convert hh.e'_3x:ℝh:Real.sin (x / 2) + 1 = 1 + 1 := id (congrArg (fun x => x + 1) _fvar.714)⊢ 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:b > 0 := 
  lt_of_not_ge fun a =>
    Mathlib.Tactic.Linarith.lt_irrefl
      (Eq.mp
        (congrArg (fun _a => _a < 0)
          (Mathlib.Tactic.Ring.of_eq
            (Mathlib.Tactic.Ring.add_congr
              (Mathlib.Tactic.Ring.add_congr
                (Mathlib.Tactic.Ring.neg_congr
                  (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                  (Mathlib.Tactic.Ring.neg_add
                    (Mathlib.Tactic.Ring.neg_one_mul
                      (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                        (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                          (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                          (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                          (Eq.refl (Int.negOfNat 1)))))
                    Mathlib.Tactic.Ring.neg_zero))
                (Mathlib.Tactic.Ring.sub_congr
                  (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                  (Mathlib.Tactic.Ring.atom_pf ↑b)
                  (Mathlib.Tactic.Ring.sub_pf
                    (Mathlib.Tactic.Ring.neg_add
                      (Mathlib.Tactic.Ring.neg_mul (↑b) (Nat.rawCast 1)
                        (Mathlib.Tactic.Ring.neg_one_mul
                          (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                            (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                              (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                              (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                              (Eq.refl (Int.negOfNat 1))))))
                      Mathlib.Tactic.Ring.neg_zero)
                    (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 1)
                      (Mathlib.Tactic.Ring.add_pf_zero_add (↑b ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))))
                (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                  (Mathlib.Meta.NormNum.IsInt.to_isNat
                    (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                      (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                      (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                      (Eq.refl (Int.ofNat 0))))
                  (Mathlib.Tactic.Ring.add_pf_zero_add (↑b ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))
              (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf ↑b)
                (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)))
                (Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero
                  (Mathlib.Tactic.Ring.add_pf_add_zero (↑b ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
              (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                (Mathlib.Tactic.Ring.add_overlap_pf_zero (↑b) (Nat.rawCast 1)
                  (Mathlib.Meta.NormNum.IsInt.to_isNat
                    (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                      (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                      (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                      (Eq.refl (Int.ofNat 0)))))
                (Mathlib.Tactic.Ring.add_pf_zero_add 0)))
            (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)))))
        (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le
          (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one)
            (Mathlib.Tactic.Linarith.sub_nonpos_of_le
              (id
                (Eq.mp
                  (Eq.trans (Mathlib.Tactic.Zify.natCast_le._simp_1 1 b) (congrFun' (congrArg LE.le Nat.cast_one) ↑b))
                  hb))))
          (Mathlib.Tactic.Linarith.sub_nonpos_of_le
            (id (Eq.mp (Eq.trans (Mathlib.Tactic.Zify.natCast_le._simp_1 b 0) (congrArg (LE.le ↑b) Nat.cast_zero)) a)))))hb1:↑b + 1 > 0 := 
  lt_of_not_ge fun a =>
    Mathlib.Tactic.Linarith.lt_irrefl
      (Eq.mp
        (congrArg (fun _a => _a < 0)
          (Mathlib.Tactic.Ring.of_eq
            (Mathlib.Tactic.Ring.add_congr
              (Mathlib.Tactic.Ring.add_congr
                (Mathlib.Tactic.Ring.add_congr
                  (Mathlib.Tactic.Ring.sub_congr
                    (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))
                    (Mathlib.Tactic.Ring.atom_pf ↑b)
                    (Mathlib.Tactic.Ring.sub_pf
                      (Mathlib.Tactic.Ring.neg_add
                        (Mathlib.Tactic.Ring.neg_mul (↑b) (Nat.rawCast 1)
                          (Mathlib.Tactic.Ring.neg_one_mul
                            (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                              (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                                (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
                                (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
                                (Eq.refl (Int.negOfNat 1))))))
                        Mathlib.Tactic.Ring.neg_zero)
                      (Mathlib.Tactic.Ring.add_pf_zero_add (↑b ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))
                  (Mathlib.Tactic.Ring.sub_congr
                    (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))
                    (Mathlib.Tactic.Ring.atom_pf r)
                    (Mathlib.Tactic.Ring.sub_pf
                      (Mathlib.Tactic.Ring.neg_add
                        (Mathlib.Tactic.Ring.neg_mul r (Nat.rawCast 1)
                          (Mathlib.Tactic.Ring.neg_one_mul
                            (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                              (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                                (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
                                (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
                                (Eq.refl (Int.negOfNat 1))))))
                        Mathlib.Tactic.Ring.neg_zero)
                      (Mathlib.Tactic.Ring.add_pf_zero_add (r ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))
                  (Mathlib.Tactic.Ring.add_pf_add_lt (↑b ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast)
                    (Mathlib.Tactic.Ring.add_pf_zero_add (r ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))
                (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf r)
                  (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                  (Mathlib.Tactic.Ring.sub_pf
                    (Mathlib.Tactic.Ring.neg_add
                      (Mathlib.Tactic.Ring.neg_one_mul
                        (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                          (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                            (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
                            (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
                            (Eq.refl (Int.negOfNat 1)))))
                      Mathlib.Tactic.Ring.neg_zero)
                    (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast
                      (Mathlib.Tactic.Ring.add_pf_add_zero (r ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
                (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast
                  (Mathlib.Tactic.Ring.add_pf_add_lt (↑b ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast)
                    (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                      (Mathlib.Tactic.Ring.add_overlap_pf_zero r (Nat.rawCast 1)
                        (Mathlib.Meta.NormNum.IsInt.to_isNat
                          (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                            (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
                            (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
                            (Eq.refl (Int.ofNat 0)))))
                      (Mathlib.Tactic.Ring.add_pf_zero_add 0)))))
              (Mathlib.Tactic.Ring.sub_congr
                (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf ↑b)
                  (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                  (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 1)
                    (Mathlib.Tactic.Ring.add_pf_add_zero (↑b ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
                (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))
                (Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero
                  (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + (↑b ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
              (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                (Mathlib.Meta.NormNum.IsInt.to_isNat
                  (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                    (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
                    (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
                    (Eq.refl (Int.ofNat 0))))
                (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                  (Mathlib.Tactic.Ring.add_overlap_pf_zero (↑b) (Nat.rawCast 1)
                    (Mathlib.Meta.NormNum.IsInt.to_isNat
                      (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                        (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
                        (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
                        (Eq.refl (Int.ofNat 0)))))
                  (Mathlib.Tactic.Ring.add_pf_zero_add 0))))
            (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))))
        (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le
          (Mathlib.Tactic.Linarith.add_neg
            (Mathlib.Tactic.Linarith.add_lt_of_le_of_neg
              (Mathlib.Tactic.Linarith.sub_nonpos_of_le (Mathlib.Tactic.Linarith.natCast_nonneg ℝ b))
              (Mathlib.Tactic.Linarith.sub_neg_of_lt h))
            (Mathlib.Tactic.Linarith.sub_neg_of_lt h'))
          (Mathlib.Tactic.Linarith.sub_nonpos_of_le a)))⊢ 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:b > 0 := 
  lt_of_not_ge fun a =>
    Mathlib.Tactic.Linarith.lt_irrefl
      (Eq.mp
        (congrArg (fun _a => _a < 0)
          (Mathlib.Tactic.Ring.of_eq
            (Mathlib.Tactic.Ring.add_congr
              (Mathlib.Tactic.Ring.add_congr
                (Mathlib.Tactic.Ring.neg_congr
                  (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                  (Mathlib.Tactic.Ring.neg_add
                    (Mathlib.Tactic.Ring.neg_one_mul
                      (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                        (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                          (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                          (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                          (Eq.refl (Int.negOfNat 1)))))
                    Mathlib.Tactic.Ring.neg_zero))
                (Mathlib.Tactic.Ring.sub_congr
                  (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                  (Mathlib.Tactic.Ring.atom_pf ↑b)
                  (Mathlib.Tactic.Ring.sub_pf
                    (Mathlib.Tactic.Ring.neg_add
                      (Mathlib.Tactic.Ring.neg_mul (↑b) (Nat.rawCast 1)
                        (Mathlib.Tactic.Ring.neg_one_mul
                          (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                            (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                              (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                              (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                              (Eq.refl (Int.negOfNat 1))))))
                      Mathlib.Tactic.Ring.neg_zero)
                    (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 1)
                      (Mathlib.Tactic.Ring.add_pf_zero_add (↑b ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))))
                (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                  (Mathlib.Meta.NormNum.IsInt.to_isNat
                    (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                      (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                      (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                      (Eq.refl (Int.ofNat 0))))
                  (Mathlib.Tactic.Ring.add_pf_zero_add (↑b ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))
              (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf ↑b)
                (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)))
                (Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero
                  (Mathlib.Tactic.Ring.add_pf_add_zero (↑b ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
              (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                (Mathlib.Tactic.Ring.add_overlap_pf_zero (↑b) (Nat.rawCast 1)
                  (Mathlib.Meta.NormNum.IsInt.to_isNat
                    (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                      (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                      (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                      (Eq.refl (Int.ofNat 0)))))
                (Mathlib.Tactic.Ring.add_pf_zero_add 0)))
            (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)))))
        (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le
          (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one)
            (Mathlib.Tactic.Linarith.sub_nonpos_of_le
              (id
                (Eq.mp
                  (Eq.trans (Mathlib.Tactic.Zify.natCast_le._simp_1 1 b) (congrFun' (congrArg LE.le Nat.cast_one) ↑b))
                  hb))))
          (Mathlib.Tactic.Linarith.sub_nonpos_of_le
            (id (Eq.mp (Eq.trans (Mathlib.Tactic.Zify.natCast_le._simp_1 b 0) (congrArg (LE.le ↑b) Nat.cast_zero)) a)))))hb1:↑b + 1 > 0 := 
  lt_of_not_ge fun a =>
    Mathlib.Tactic.Linarith.lt_irrefl
      (Eq.mp
        (congrArg (fun _a => _a < 0)
          (Mathlib.Tactic.Ring.of_eq
            (Mathlib.Tactic.Ring.add_congr
              (Mathlib.Tactic.Ring.add_congr
                (Mathlib.Tactic.Ring.add_congr
                  (Mathlib.Tactic.Ring.sub_congr
                    (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))
                    (Mathlib.Tactic.Ring.atom_pf ↑b)
                    (Mathlib.Tactic.Ring.sub_pf
                      (Mathlib.Tactic.Ring.neg_add
                        (Mathlib.Tactic.Ring.neg_mul (↑b) (Nat.rawCast 1)
                          (Mathlib.Tactic.Ring.neg_one_mul
                            (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                              (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                                (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
                                (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
                                (Eq.refl (Int.negOfNat 1))))))
                        Mathlib.Tactic.Ring.neg_zero)
                      (Mathlib.Tactic.Ring.add_pf_zero_add (↑b ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))
                  (Mathlib.Tactic.Ring.sub_congr
                    (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))
                    (Mathlib.Tactic.Ring.atom_pf r)
                    (Mathlib.Tactic.Ring.sub_pf
                      (Mathlib.Tactic.Ring.neg_add
                        (Mathlib.Tactic.Ring.neg_mul r (Nat.rawCast 1)
                          (Mathlib.Tactic.Ring.neg_one_mul
                            (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                              (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                                (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
                                (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
                                (Eq.refl (Int.negOfNat 1))))))
                        Mathlib.Tactic.Ring.neg_zero)
                      (Mathlib.Tactic.Ring.add_pf_zero_add (r ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))
                  (Mathlib.Tactic.Ring.add_pf_add_lt (↑b ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast)
                    (Mathlib.Tactic.Ring.add_pf_zero_add (r ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))
                (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf r)
                  (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                  (Mathlib.Tactic.Ring.sub_pf
                    (Mathlib.Tactic.Ring.neg_add
                      (Mathlib.Tactic.Ring.neg_one_mul
                        (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                          (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                            (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
                            (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
                            (Eq.refl (Int.negOfNat 1)))))
                      Mathlib.Tactic.Ring.neg_zero)
                    (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast
                      (Mathlib.Tactic.Ring.add_pf_add_zero (r ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
                (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast
                  (Mathlib.Tactic.Ring.add_pf_add_lt (↑b ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast)
                    (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                      (Mathlib.Tactic.Ring.add_overlap_pf_zero r (Nat.rawCast 1)
                        (Mathlib.Meta.NormNum.IsInt.to_isNat
                          (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                            (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
                            (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
                            (Eq.refl (Int.ofNat 0)))))
                      (Mathlib.Tactic.Ring.add_pf_zero_add 0)))))
              (Mathlib.Tactic.Ring.sub_congr
                (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf ↑b)
                  (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                  (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 1)
                    (Mathlib.Tactic.Ring.add_pf_add_zero (↑b ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
                (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))
                (Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero
                  (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + (↑b ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
              (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                (Mathlib.Meta.NormNum.IsInt.to_isNat
                  (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                    (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
                    (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
                    (Eq.refl (Int.ofNat 0))))
                (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                  (Mathlib.Tactic.Ring.add_overlap_pf_zero (↑b) (Nat.rawCast 1)
                    (Mathlib.Meta.NormNum.IsInt.to_isNat
                      (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                        (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
                        (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
                        (Eq.refl (Int.ofNat 0)))))
                  (Mathlib.Tactic.Ring.add_pf_zero_add 0))))
            (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))))
        (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le
          (Mathlib.Tactic.Linarith.add_neg
            (Mathlib.Tactic.Linarith.add_lt_of_le_of_neg
              (Mathlib.Tactic.Linarith.sub_nonpos_of_le (Mathlib.Tactic.Linarith.natCast_nonneg ℝ b))
              (Mathlib.Tactic.Linarith.sub_neg_of_lt h))
            (Mathlib.Tactic.Linarith.sub_neg_of_lt h'))
          (Mathlib.Tactic.Linarith.sub_nonpos_of_le a)))⊢ r * r ^ b = r ^ (b + 1)
    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:C := hAC h⊢ 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:E := hAE hA⊢ 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:E := hAE hAhF:F := hEB ⟨hE, hB⟩⊢ 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:E := hAE hAhF:F := hEB ⟨hE, hB⟩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:E := hAE hAhF:F := hEB ⟨hE, hB⟩⊢ 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:E := hAE hAhF:F := hEB ⟨hE, hB⟩hCG:C ∧ G⊢ C ∧ D obtain ⟨ hC, hG ⟩ := hCGA: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:E := hAE hAhF:F := hEB ⟨hE, hB⟩hC:ChG:G⊢ C ∧ D
    have hD : D := hADG hA hGA: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:E := hAE hAhF:F := hEB ⟨hE, hB⟩hC:ChG:GhD:D := hADG hA hG⊢ 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:E := hAE hAhF:F := hEB ⟨hE, hB⟩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:E := hAE hAhF:F := hEB ⟨hE, hB⟩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:E := hAE hAhF:F := hEB ⟨hE, hB⟩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:E := hAE hAhF:F := hEB ⟨hE, hB⟩hH:HhC:C := hFHC ⟨hF, hH⟩⊢ 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:E := hAE hAhF:F := hEB ⟨hE, hB⟩hH:HhC:C := hFHC ⟨hF, hH⟩hG:G := hAHG ⟨hA, hH⟩⊢ 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:E := hAE hAhF:F := hEB ⟨hE, hB⟩hI:IhG:G := hIG hI⊢ 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:E := hAE hAhF:F := hEB ⟨hE, hB⟩hI:IhG:G := hIG hIhC:C := hIGC hG⊢ 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:C := hBC hB⊢ False
  have hD : D := hAD hAA:PropB:PropC:PropD:ProphBC:B → ChAD:A → DhCD:D → ¬ChA:AhB:BhC:C := hBC hBhD:D := hAD hA⊢ False
  have hC' : ¬ C := hCD hDA:PropB:PropC:PropD:ProphBC:B → ChAD:A → DhCD:D → ¬ChA:AhB:BhC:C := hBC hBhD:D := hAD hAhC':¬C := hCD hD⊢ False
  contradictionAll goals completed! 🐙