Аналіз I, Додаток A.3

Деякі приклади доказів

Твердження 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
  replace h := hAC hA:PropB:PropC:PropD:ProphAC:A → ChCD:C → DhDB:D → Bh:C⊢ B
  replace h := hCD hA:PropB:PropC:PropD:ProphAC:A → ChCD:C → DhDB:D → Bh:D⊢ B
  replace h := hDB hA:PropB:PropC:PropD:ProphAC:A → ChCD:C → DhDB:D → Bh:B⊢ B
  exact hAll goals completed! 🐙

Твердження 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
  apply_fun (fun x ↦ x/2) at hx:ℝh:x / 2 = Real.pi / 2⊢ Real.sin (x / 2) + 1 = 2
  apply_fun (fun x ↦ Real.sin x) at hx:ℝh:Real.sin (x / 2) = Real.sin (Real.pi / 2)⊢ Real.sin (x / 2) + 1 = 2
  simp at hx:ℝh:Real.sin (x / 2) = 1⊢ Real.sin (x / 2) + 1 = 2
  apply_fun (fun x ↦ x + 1) at hx:ℝh:Real.sin (x / 2) + 1 = 1 + 1⊢ Real.sin (x / 2) + 1 = 2
  convert hh.e'_3x:ℝh:Real.sin (x / 2) + 1 = 1 + 1⊢ 2 = 1 + 1
  norm_numAll goals completed! 🐙

Твердження 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
  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! 🐙

Твердження 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
  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! 🐙

Твердження 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.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)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 Filter.Tendsto.congr' _ hconvr:ℝ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 > 0hb1:↑b + 1 > 0⊢ 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 > 0hb1:↑b + 1 > 0⊢ r * (↑b + 1) * (↑b * r ^ b) = (↑b + 1) * r ^ (b + 1) * ↑b
    ring_nfAll goals completed! 🐙
  suffices hconv : 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)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 Filter.Tendsto.const_mul r hconvh.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.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)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 Filter.Tendsto.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]r:ℝ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.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)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 Filter.Tendsto.const_add 1 hconvh.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! 🐙

Твердження 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
  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⊢ D
  exact hCD hCAll goals completed! 🐙

Твердження 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
  rintro ⟨ hA, hB ⟩introA: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 hAintroA: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⊢ C ∧ D
  have hF : F := hEB ⟨hE, hB⟩introA: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:EhF:F⊢ C ∧ D
  suffices hCG : C ∧ GintroA: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:EhF:FhCG: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:EhF:F⊢ C ∧ G
  .introA: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:EhF:FhCG:C ∧ G⊢ C ∧ D obtain ⟨ hC, hG ⟩ := hCGintro.introA: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:EhF:FhC:ChG:G⊢ C ∧ D
    have hD : D := hADG hA hGintro.introA: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:EhF:FhC:ChG:GhD:D⊢ C ∧ D
    exact ⟨hC, hD⟩All goals completed! 🐙
  rcases hHI with hH | hIhCG.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:EhF:FhH: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:EhF:FhI: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:EhF:FhH: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:EhF:FhH:HhC:C⊢ 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:EhF:FhH:HhC:ChG:G⊢ 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:EhF:FhI:IhG:G⊢ 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:EhF:FhI:IhG:GhC:C⊢ C ∧ G
  exact ⟨hC, hG⟩All goals completed! 🐙

Твердження 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⊢ False
  have hD : D := hAD hAA:PropB:PropC:PropD:ProphBC:B → ChAD:A → DhCD:D → ¬ChA:AhB:BhC:ChD:D⊢ False
  have hC' : ¬ C := hCD hDA:PropB:PropC:PropD:ProphBC:B → ChAD:A → DhCD:D → ¬ChA:AhB:BhC:ChD:DhC':¬C⊢ False
  contradictionAll goals completed! 🐙