internlm/Lean-Github huggingface dataset:
Theorem: proportion_inv
Proof state before:
r s t u : ℝ
h :
  0 ≤ r ∧
    0 ≤ s ∧
      0 ≤ t ∧
        0 ≤ u ∧
          ∀ (n m : ℕ),
            (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧
              (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
n m : ℕ
⊢ (↑n * s = ↑m * r → ↑n * u = ↑m * t) ∧ (↑n * s < ↑m * r → ↑n * u < ↑m * t) ∧ (↑m * r < ↑n * s → ↑m * t < ↑n * u)
Tactic:
have := h.2.2.2.2 m n
Proof state after:
r s t u : ℝ
h :
  0 ≤ r ∧
    0 ≤ s ∧
      0 ≤ t ∧
        0 ≤ u ∧
          ∀ (n m : ℕ),
            (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧
              (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
n m : ℕ
this : (↑m * r = ↑n * s → ↑m * t = ↑n * u) ∧ (↑m * r < ↑n * s → ↑m * t < ↑n * u) ∧ (↑n * s < ↑m * r → ↑n * u < ↑m * t)
⊢ (↑n * s = ↑m * r → ↑n * u = ↑m * t) ∧ (↑n * s < ↑m * r → ↑n * u < ↑m * t) ∧ (↑m * r < ↑n * s → ↑m * t < ↑n * u)
Theorem: proportion_inv
Proof state before:
r s t u : ℝ
h :
  0 ≤ r ∧
    0 ≤ s ∧
      0 ≤ t ∧
        0 ≤ u ∧
          ∀ (n m : ℕ),
            (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧
              (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
n m : ℕ
this : (↑m * r = ↑n * s → ↑m * t = ↑n * u) ∧ (↑m * r < ↑n * s → ↑m * t < ↑n * u) ∧ (↑n * s < ↑m * r → ↑n * u < ↑m * t)
⊢ (↑n * s = ↑m * r → ↑n * u = ↑m * t) ∧ (↑n * s < ↑m * r → ↑n * u < ↑m * t) ∧ (↑m * r < ↑n * s → ↑m * t < ↑n * u)
Tactic:
exact ⟨fun h => (this.1 h.symm).symm, ⟨fun h => (this.2.2 h), fun h => (this.2.1 h)⟩⟩
Proof state after:
no goals
Theorem: proportion_inv_iff
Proof state before:
r s t u : ℝ
⊢ proportion r s t u ↔ proportion s r u t
Tactic:
constructor
Proof state after:
case mp
r s t u : ℝ
⊢ proportion r s t u → proportion s r u t

case mpr
r s t u : ℝ
⊢ proportion s r u t → proportion r s t u
Theorem: proportion_inv_iff
Proof state before:
case mp
r s t u : ℝ
⊢ proportion r s t u → proportion s r u t

case mpr
r s t u : ℝ
⊢ proportion s r u t → proportion r s t u
Tactic:
all_goals exact fun h => proportion_inv h
Proof state after:
no goals
Theorem: proportion_inv_iff
Proof state before:
case mpr
r s t u : ℝ
⊢ proportion s r u t → proportion r s t u
Tactic:
exact fun h => proportion_inv h
Proof state after:
no goals
Theorem: zero_of_proportion_iff
Proof state before:
r s t u : ℝ
h : proportion r s t u
⊢ s = 0 ↔ u = 0
Tactic:
constructor
Proof state after:
case mp
r s t u : ℝ
h : proportion r s t u
⊢ s = 0 → u = 0

case mpr
r s t u : ℝ
h : proportion r s t u
⊢ u = 0 → s = 0
Theorem: zero_of_proportion_iff
Proof state before:
case mp
r s t u : ℝ
h : proportion r s t u
⊢ s = 0 → u = 0
Tactic:
intro s_ne
Proof state after:
case mp
r s t u : ℝ
h : proportion r s t u
s_ne : s = 0
⊢ u = 0
Theorem: zero_of_proportion_iff
Proof state before:
case mp
r s t u : ℝ
h : proportion r s t u
s_ne : s = 0
⊢ u = 0
Tactic:
have := (h.2.2.2.2 0 1).1
Proof state after:
case mp
r s t u : ℝ
h : proportion r s t u
s_ne : s = 0
this : ↑0 * r = ↑1 * s → ↑0 * t = ↑1 * u
⊢ u = 0
Theorem: zero_of_proportion_iff
Proof state before:
case mp
r s t u : ℝ
h : proportion r s t u
s_ne : s = 0
this : ↑0 * r = ↑1 * s → ↑0 * t = ↑1 * u
⊢ u = 0
Tactic:
simp at this
Proof state after:
case mp
r s t u : ℝ
h : proportion r s t u
s_ne : s = 0
this : 0 = s → 0 = u
⊢ u = 0
Theorem: zero_of_proportion_iff
Proof state before:
case mp
r s t u : ℝ
h : proportion r s t u
s_ne : s = 0
this : 0 = s → 0 = u
⊢ u = 0
Tactic:
exact (this s_ne.symm).symm
Proof state after:
no goals
Theorem: zero_of_proportion_iff
Proof state before:
case mpr
r s t u : ℝ
h : proportion r s t u
⊢ u = 0 → s = 0
Tactic:
intro u_ne
Proof state after:
case mpr
r s t u : ℝ
h : proportion r s t u
u_ne : u = 0
⊢ s = 0
Theorem: zero_of_proportion_iff
Proof state before:
case mpr
r s t u : ℝ
h : proportion r s t u
u_ne : u = 0
⊢ s = 0
Tactic:
have hh := (h.2.2.2.2 0 1).2.1
Proof state after:
case mpr
r s t u : ℝ
h : proportion r s t u
u_ne : u = 0
hh : ↑0 * r < ↑1 * s → ↑0 * t < ↑1 * u
⊢ s = 0
Theorem: zero_of_proportion_iff
Proof state before:
case mpr
r s t u : ℝ
h : proportion r s t u
u_ne : u = 0
hh : ↑0 * r < ↑1 * s → ↑0 * t < ↑1 * u
⊢ s = 0
Tactic:
simp at hh
Proof state after:
case mpr
r s t u : ℝ
h : proportion r s t u
u_ne : u = 0
hh : 0 < s → 0 < u
⊢ s = 0
Theorem: zero_of_proportion_iff
Proof state before:
case mpr
r s t u : ℝ
h : proportion r s t u
u_ne : u = 0
hh : 0 < s → 0 < u
⊢ s = 0
Tactic:
by_contra s_ne
Proof state after:
case mpr
r s t u : ℝ
h : proportion r s t u
u_ne : u = 0
hh : 0 < s → 0 < u
s_ne : ¬s = 0
⊢ False
Theorem: zero_of_proportion_iff
Proof state before:
case mpr
r s t u : ℝ
h : proportion r s t u
u_ne : u = 0
hh : 0 < s → 0 < u
s_ne : ¬s = 0
⊢ False
Tactic:
have : 0 < s := Ne.lt_of_le (fun ss => s_ne ss.symm) h.2.1
Proof state after:
case mpr
r s t u : ℝ
h : proportion r s t u
u_ne : u = 0
hh : 0 < s → 0 < u
s_ne : ¬s = 0
this : 0 < s
⊢ False
Theorem: zero_of_proportion_iff
Proof state before:
case mpr
r s t u : ℝ
h : proportion r s t u
u_ne : u = 0
hh : 0 < s → 0 < u
s_ne : ¬s = 0
this : 0 < s
⊢ False
Tactic:
have := hh this
Proof state after:
case mpr
r s t u : ℝ
h : proportion r s t u
u_ne : u = 0
hh : 0 < s → 0 < u
s_ne : ¬s = 0
this✝ : 0 < s
this : 0 < u
⊢ False
Theorem: zero_of_proportion_iff
Proof state before:
case mpr
r s t u : ℝ
h : proportion r s t u
u_ne : u = 0
hh : 0 < s → 0 < u
s_ne : ¬s = 0
this✝ : 0 < s
this : 0 < u
⊢ False
Tactic:
linarith
Proof state after:
no goals
Theorem: proportion_of_zero
Proof state before:
⊢ proportion 0 0 0 0
Tactic:
simp [proportion]
Proof state after:
no goals
Theorem: proportion_symm'
Proof state before:
r s t u : ℝ
h : proportion r s t u
⊢ proportion t u r s
Tactic:
by_cases s_ne : s = 0
Proof state after:
case pos
r s t u : ℝ
h : proportion r s t u
s_ne : s = 0
⊢ proportion t u r s

case neg
r s t u : ℝ
h : proportion r s t u
s_ne : ¬s = 0
⊢ proportion t u r s
Theorem: proportion_symm'
Proof state before:
case pos
r s t u : ℝ
h : proportion r s t u
s_ne : s = 0
⊢ proportion t u r s
Tactic:
have u_ne := (zero_of_proportion_iff h).mp s_ne
Proof state after:
case pos
r s t u : ℝ
h : proportion r s t u
s_ne : s = 0
u_ne : u = 0
⊢ proportion t u r s
Theorem: proportion_symm'
Proof state before:
case pos
r s t u : ℝ
h : proportion r s t u
s_ne : s = 0
u_ne : u = 0
⊢ proportion t u r s
Tactic:
have inv := proportion_inv h
Proof state after:
case pos
r s t u : ℝ
h : proportion r s t u
s_ne : s = 0
u_ne : u = 0
inv : proportion s r u t
⊢ proportion t u r s
Theorem: proportion_symm'
Proof state before:
case pos
r s t u : ℝ
h : proportion r s t u
s_ne : s = 0
u_ne : u = 0
inv : proportion s r u t
⊢ proportion t u r s
Tactic:
by_cases r_ne : r = 0
Proof state after:
case pos
r s t u : ℝ
h : proportion r s t u
s_ne : s = 0
u_ne : u = 0
inv : proportion s r u t
r_ne : r = 0
⊢ proportion t u r s

case neg
r s t u : ℝ
h : proportion r s t u
s_ne : s = 0
u_ne : u = 0
inv : proportion s r u t
r_ne : ¬r = 0
⊢ proportion t u r s
Theorem: proportion_symm'
Proof state before:
case pos
r s t u : ℝ
h : proportion r s t u
s_ne : s = 0
u_ne : u = 0
inv : proportion s r u t
r_ne : r = 0
⊢ proportion t u r s
Tactic:
have t_ne := (zero_of_proportion_iff inv).mp r_ne
Proof state after:
case pos
r s t u : ℝ
h : proportion r s t u
s_ne : s = 0
u_ne : u = 0
inv : proportion s r u t
r_ne : r = 0
t_ne : t = 0
⊢ proportion t u r s
Theorem: proportion_symm'
Proof state before:
case pos
r s t u : ℝ
h : proportion r s t u
s_ne : s = 0
u_ne : u = 0
inv : proportion s r u t
r_ne : r = 0
t_ne : t = 0
⊢ proportion t u r s
Tactic:
rw [s_ne, r_ne, t_ne, u_ne]
Proof state after:
case pos
r s t u : ℝ
h : proportion r s t u
s_ne : s = 0
u_ne : u = 0
inv : proportion s r u t
r_ne : r = 0
t_ne : t = 0
⊢ proportion 0 0 0 0
Theorem: proportion_symm'
Proof state before:
case pos
r s t u : ℝ
h : proportion r s t u
s_ne : s = 0
u_ne : u = 0
inv : proportion s r u t
r_ne : r = 0
t_ne : t = 0
⊢ proportion 0 0 0 0
Tactic:
exact proportion_of_zero
Proof state after:
no goals
Theorem: proportion_symm'
Proof state before:
case neg
r s t u : ℝ
h : proportion r s t u
s_ne : s = 0
u_ne : u = 0
inv : proportion s r u t
r_ne : ¬r = 0
⊢ proportion t u r s
Tactic:
have t_ne := (zero_of_proportion_iff inv).not.mp r_ne
Proof state after:
case neg
r s t u : ℝ
h : proportion r s t u
s_ne : s = 0
u_ne : u = 0
inv : proportion s r u t
r_ne : ¬r = 0
t_ne : ¬t = 0
⊢ proportion t u r s
Theorem: proportion_symm'
Proof state before:
case neg
r s t u : ℝ
h : proportion r s t u
s_ne : s = 0
u_ne : u = 0
inv : proportion s r u t
r_ne : ¬r = 0
t_ne : ¬t = 0
⊢ proportion t u r s
Tactic:
rw [proportion_inv_iff]
Proof state after:
case neg
r s t u : ℝ
h : proportion r s t u
s_ne : s = 0
u_ne : u = 0
inv : proportion s r u t
r_ne : ¬r = 0
t_ne : ¬t = 0
⊢ proportion u t s r
Theorem: proportion_symm'
Proof state before:
case neg
r s t u : ℝ
h : proportion r s t u
s_ne : s = 0
u_ne : u = 0
inv : proportion s r u t
r_ne : ¬r = 0
t_ne : ¬t = 0
⊢ proportion u t s r
Tactic:
exact proportion_symm r_ne t_ne inv
Proof state after:
no goals
Theorem: proportion_symm'
Proof state before:
case neg
r s t u : ℝ
h : proportion r s t u
s_ne : ¬s = 0
⊢ proportion t u r s
Tactic:
have u_ne := (zero_of_proportion_iff h).not.mp s_ne
Proof state after:
case neg
r s t u : ℝ
h : proportion r s t u
s_ne : ¬s = 0
u_ne : ¬u = 0
⊢ proportion t u r s
Theorem: proportion_symm'
Proof state before:
case neg
r s t u : ℝ
h : proportion r s t u
s_ne : ¬s = 0
u_ne : ¬u = 0
⊢ proportion t u r s
Tactic:
exact proportion_symm s_ne u_ne h
Proof state after:
no goals
Theorem: proportion_eq
Proof state before:
r s : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
r_ne : r ≠ 0
s_ne : s ≠ 0
⊢ proportion r r s s
Tactic:
rw [(proportion_iff hr hr hs hs r_ne s_ne).symm]
Proof state after:
r s : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
r_ne : r ≠ 0
s_ne : s ≠ 0
⊢ r / r = s / s
Theorem: proportion_eq
Proof state before:
r s : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
r_ne : r ≠ 0
s_ne : s ≠ 0
⊢ r / r = s / s
Tactic:
field_simp
Proof state after:
no goals
Theorem: aux
Proof state before:
i : incidence_geometry
a b c : point
Tabc : ¬colinear a b c
ang_a : rightangle ≤ angle b a c
⊢ ∃ d, B b d c ∧ angle b d a = rightangle ∧ angle c d a = rightangle
Tactic:
obtain ⟨_, bL, cL⟩ := line_of_pts b c
Proof state after:
case intro.intro
i : incidence_geometry
a b c : point
Tabc : ¬colinear a b c
ang_a : rightangle ≤ angle b a c
w✝ : line
bL : online b w✝
cL : online c w✝
⊢ ∃ d, B b d c ∧ angle b d a = rightangle ∧ angle c d a = rightangle
Theorem: aux
Proof state before:
case intro.intro
i : incidence_geometry
a b c : point
Tabc : ¬colinear a b c
ang_a : rightangle ≤ angle b a c
w✝ : line
bL : online b w✝
cL : online c w✝
⊢ ∃ d, B b d c ∧ angle b d a = rightangle ∧ angle c d a = rightangle
Tactic:
have aL := online_1_of_triangle bL cL Tabc
Proof state after:
case intro.intro
i : incidence_geometry
a b c : point
Tabc : ¬colinear a b c
ang_a : rightangle ≤ angle b a c
w✝ : line
bL : online b w✝
cL : online c w✝
aL : ¬online a w✝
⊢ ∃ d, B b d c ∧ angle b d a = rightangle ∧ angle c d a = rightangle
Theorem: aux
Proof state before:
case intro.intro
i : incidence_geometry
a b c : point
Tabc : ¬colinear a b c
ang_a : rightangle ≤ angle b a c
w✝ : line
bL : online b w✝
cL : online c w✝
aL : ¬online a w✝
⊢ ∃ d, B b d c ∧ angle b d a = rightangle ∧ angle c d a = rightangle
Tactic:
obtain ⟨d, adc, adb, Bcdb⟩ := pythlem (ne_23_of_tri Tabc).symm cL bL aL ang_a
Proof state after:
case intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
Tabc : ¬colinear a b c
ang_a : rightangle ≤ angle b a c
w✝ : line
bL : online b w✝
cL : online c w✝
aL : ¬online a w✝
d : point
adc : angle a d c = rightangle
adb : angle a d b = rightangle
Bcdb : B c d b
⊢ ∃ d, B b d c ∧ angle b d a = rightangle ∧ angle c d a = rightangle
Theorem: aux
Proof state before:
case intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
Tabc : ¬colinear a b c
ang_a : rightangle ≤ angle b a c
w✝ : line
bL : online b w✝
cL : online c w✝
aL : ¬online a w✝
d : point
adc : angle a d c = rightangle
adb : angle a d b = rightangle
Bcdb : B c d b
⊢ ∃ d, B b d c ∧ angle b d a = rightangle ∧ angle c d a = rightangle
Tactic:
exact ⟨d, B_symm Bcdb, (by perma), (by perma)⟩
Proof state after:
no goals
Theorem: aux
Proof state before:
i : incidence_geometry
a b c : point
Tabc : ¬colinear a b c
ang_a : rightangle ≤ angle b a c
w✝ : line
bL : online b w✝
cL : online c w✝
aL : ¬online a w✝
d : point
adc : angle a d c = rightangle
adb : angle a d b = rightangle
Bcdb : B c d b
⊢ angle b d a = rightangle
Tactic:
perma
Proof state after:
no goals
Theorem: aux
Proof state before:
i : incidence_geometry
a b c : point
Tabc : ¬colinear a b c
ang_a : rightangle ≤ angle b a c
w✝ : line
bL : online b w✝
cL : online c w✝
aL : ¬online a w✝
d : point
adc : angle a d c = rightangle
adb : angle a d b = rightangle
Bcdb : B c d b
⊢ angle c d a = rightangle
Tactic:
perma
Proof state after:
no goals
Theorem: aux2
Proof state before:
i : incidence_geometry
a b c : point
Tabc : triangle a b c
⊢ length b a ≠ 0 ∧ length c a ≠ 0 ∧ length b c ≠ 0 ∧ length c b ≠ 0
Tactic:
have ba := length_eq_zero_iff.not.mpr $ ne_21_of_tri Tabc
Proof state after:
i : incidence_geometry
a b c : point
Tabc : triangle a b c
ba : ¬length b a = 0
⊢ length b a ≠ 0 ∧ length c a ≠ 0 ∧ length b c ≠ 0 ∧ length c b ≠ 0
Theorem: aux2
Proof state before:
i : incidence_geometry
a b c : point
Tabc : triangle a b c
ba : ¬length b a = 0
⊢ length b a ≠ 0 ∧ length c a ≠ 0 ∧ length b c ≠ 0 ∧ length c b ≠ 0
Tactic:
have ca := length_eq_zero_iff.not.mpr $ ne_31_of_tri Tabc
Proof state after:
i : incidence_geometry
a b c : point
Tabc : triangle a b c
ba : ¬length b a = 0
ca : ¬length c a = 0
⊢ length b a ≠ 0 ∧ length c a ≠ 0 ∧ length b c ≠ 0 ∧ length c b ≠ 0
Theorem: aux2
Proof state before:
i : incidence_geometry
a b c : point
Tabc : triangle a b c
ba : ¬length b a = 0
ca : ¬length c a = 0
⊢ length b a ≠ 0 ∧ length c a ≠ 0 ∧ length b c ≠ 0 ∧ length c b ≠ 0
Tactic:
have bc := length_eq_zero_iff.not.mpr $ ne_23_of_tri Tabc
Proof state after:
i : incidence_geometry
a b c : point
Tabc : triangle a b c
ba : ¬length b a = 0
ca : ¬length c a = 0
bc : ¬length b c = 0
⊢ length b a ≠ 0 ∧ length c a ≠ 0 ∧ length b c ≠ 0 ∧ length c b ≠ 0
Theorem: aux2
Proof state before:
i : incidence_geometry
a b c : point
Tabc : triangle a b c
ba : ¬length b a = 0
ca : ¬length c a = 0
bc : ¬length b c = 0
⊢ length b a ≠ 0 ∧ length c a ≠ 0 ∧ length b c ≠ 0 ∧ length c b ≠ 0
Tactic:
have cb := fun h => bc ((length_symm b c).trans h)
Proof state after:
i : incidence_geometry
a b c : point
Tabc : triangle a b c
ba : ¬length b a = 0
ca : ¬length c a = 0
bc : ¬length b c = 0
cb : length c b = 0 → False
⊢ length b a ≠ 0 ∧ length c a ≠ 0 ∧ length b c ≠ 0 ∧ length c b ≠ 0
Theorem: aux2
Proof state before:
i : incidence_geometry
a b c : point
Tabc : triangle a b c
ba : ¬length b a = 0
ca : ¬length c a = 0
bc : ¬length b c = 0
cb : length c b = 0 → False
⊢ length b a ≠ 0 ∧ length c a ≠ 0 ∧ length b c ≠ 0 ∧ length c b ≠ 0
Tactic:
exact ⟨ ba, ca, bc, cb ⟩
Proof state after:
no goals
Theorem: pythagorean_proof_two
Proof state before:
i : incidence_geometry
a b c : point
Tabc : triangle a b c
ang_a : angle b a c = rightangle
⊢ length a b ^ 2 + length a c ^ 2 = length b c ^ 2
Tactic:
obtain ⟨ d, Bbdc, ang_bda, ang_cda ⟩ := aux Tabc ang_a.symm.le
Proof state after:
case intro.intro.intro
i : incidence_geometry
a b c : point
Tabc : triangle a b c
ang_a : angle b a c = rightangle
d : point
Bbdc : B b d c
ang_bda : angle b d a = rightangle
ang_cda : angle c d a = rightangle
⊢ length a b ^ 2 + length a c ^ 2 = length b c ^ 2
Theorem: pythagorean_proof_two
Proof state before:
case intro.intro.intro
i : incidence_geometry
a b c : point
Tabc : triangle a b c
ang_a : angle b a c = rightangle
d : point
Bbdc : B b d c
ang_bda : angle b d a = rightangle
ang_cda : angle c d a = rightangle
⊢ length a b ^ 2 + length a c ^ 2 = length b c ^ 2
Tactic:
obtain ⟨ ba, ca, bc, cb ⟩ := aux2 Tabc
Proof state after:
case intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
Tabc : triangle a b c
ang_a : angle b a c = rightangle
d : point
Bbdc : B b d c
ang_bda : angle b d a = rightangle
ang_cda : angle c d a = rightangle
ba : length b a ≠ 0
ca : length c a ≠ 0
bc : length b c ≠ 0
cb : length c b ≠ 0
⊢ length a b ^ 2 + length a c ^ 2 = length b c ^ 2
Theorem: pythagorean_proof_two
Proof state before:
case intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
Tabc : triangle a b c
ang_a : angle b a c = rightangle
d : point
Bbdc : B b d c
ang_bda : angle b d a = rightangle
ang_cda : angle c d a = rightangle
ba : length b a ≠ 0
ca : length c a ≠ 0
bc : length b c ≠ 0
cb : length c b ≠ 0
⊢ length a b ^ 2 + length a c ^ 2 = length b c ^ 2
Tactic:
obtain ⟨ Tdba, Tdca ⟩ := aux3 Tabc Bbdc
Proof state after:
case intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
Tabc : triangle a b c
ang_a : angle b a c = rightangle
d : point
Bbdc : B b d c
ang_bda : angle b d a = rightangle
ang_cda : angle c d a = rightangle
ba : length b a ≠ 0
ca : length c a ≠ 0
bc : length b c ≠ 0
cb : length c b ≠ 0
Tdba : triangle d b a
Tdca : triangle d c a
⊢ length a b ^ 2 + length a c ^ 2 = length b c ^ 2
Theorem: pythagorean_proof_two
Proof state before:
case intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
Tabc : triangle a b c
ang_a : angle b a c = rightangle
d : point
Bbdc : B b d c
ang_bda : angle b d a = rightangle
ang_cda : angle c d a = rightangle
ba : length b a ≠ 0
ca : length c a ≠ 0
bc : length b c ≠ 0
cb : length c b ≠ 0
Tdba : triangle d b a
Tdca : triangle d c a
⊢ length a b ^ 2 + length a c ^ 2 = length b c ^ 2
Tactic:
have abc_dba : angle a b c = angle d b a := by linperm [aux4 ba Bbdc]
Proof state after:
case intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
Tabc : triangle a b c
ang_a : angle b a c = rightangle
d : point
Bbdc : B b d c
ang_bda : angle b d a = rightangle
ang_cda : angle c d a = rightangle
ba : length b a ≠ 0
ca : length c a ≠ 0
bc : length b c ≠ 0
cb : length c b ≠ 0
Tdba : triangle d b a
Tdca : triangle d c a
abc_dba : angle a b c = angle d b a
⊢ length a b ^ 2 + length a c ^ 2 = length b c ^ 2
Theorem: pythagorean_proof_two
Proof state before:
case intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
Tabc : triangle a b c
ang_a : angle b a c = rightangle
d : point
Bbdc : B b d c
ang_bda : angle b d a = rightangle
ang_cda : angle c d a = rightangle
ba : length b a ≠ 0
ca : length c a ≠ 0
bc : length b c ≠ 0
cb : length c b ≠ 0
Tdba : triangle d b a
Tdca : triangle d c a
abc_dba : angle a b c = angle d b a
⊢ length a b ^ 2 + length a c ^ 2 = length b c ^ 2
Tactic:
have acb_dca : angle a c b = angle d c a := by linperm [aux4 ca $ B_symm Bbdc]
Proof state after:
case intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
Tabc : triangle a b c
ang_a : angle b a c = rightangle
d : point
Bbdc : B b d c
ang_bda : angle b d a = rightangle
ang_cda : angle c d a = rightangle
ba : length b a ≠ 0
ca : length c a ≠ 0
bc : length b c ≠ 0
cb : length c b ≠ 0
Tdba : triangle d b a
Tdca : triangle d c a
abc_dba : angle a b c = angle d b a
acb_dca : angle a c b = angle d c a
⊢ length a b ^ 2 + length a c ^ 2 = length b c ^ 2
Theorem: pythagorean_proof_two
Proof state before:
case intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
Tabc : triangle a b c
ang_a : angle b a c = rightangle
d : point
Bbdc : B b d c
ang_bda : angle b d a = rightangle
ang_cda : angle c d a = rightangle
ba : length b a ≠ 0
ca : length c a ≠ 0
bc : length b c ≠ 0
cb : length c b ≠ 0
Tdba : triangle d b a
Tdca : triangle d c a
abc_dba : angle a b c = angle d b a
acb_dca : angle a c b = angle d c a
⊢ length a b ^ 2 + length a c ^ 2 = length b c ^ 2
Tactic:
have prop1 := similar_of_AA (tri213 Tdba) (tri213 Tabc) abc_dba.symm (by linarith)
Proof state after:
case intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
Tabc : triangle a b c
ang_a : angle b a c = rightangle
d : point
Bbdc : B b d c
ang_bda : angle b d a = rightangle
ang_cda : angle c d a = rightangle
ba : length b a ≠ 0
ca : length c a ≠ 0
bc : length b c ≠ 0
cb : length c b ≠ 0
Tdba : triangle d b a
Tdca : triangle d c a
abc_dba : angle a b c = angle d b a
acb_dca : angle a c b = angle d c a
prop1 : proportion (length b d) (length b a) (length b a) (length b c)
⊢ length a b ^ 2 + length a c ^ 2 = length b c ^ 2
Theorem: pythagorean_proof_two
Proof state before:
case intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
Tabc : triangle a b c
ang_a : angle b a c = rightangle
d : point
Bbdc : B b d c
ang_bda : angle b d a = rightangle
ang_cda : angle c d a = rightangle
ba : length b a ≠ 0
ca : length c a ≠ 0
bc : length b c ≠ 0
cb : length c b ≠ 0
Tdba : triangle d b a
Tdca : triangle d c a
abc_dba : angle a b c = angle d b a
acb_dca : angle a c b = angle d c a
prop1 : proportion (length b d) (length b a) (length b a) (length b c)
⊢ length a b ^ 2 + length a c ^ 2 = length b c ^ 2
Tactic:
have rat1 := (proportion_len_iff _ _ _ _ _ _ _ _ ba bc).mpr prop1
Proof state after:
case intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
Tabc : triangle a b c
ang_a : angle b a c = rightangle
d : point
Bbdc : B b d c
ang_bda : angle b d a = rightangle
ang_cda : angle c d a = rightangle
ba : length b a ≠ 0
ca : length c a ≠ 0
bc : length b c ≠ 0
cb : length c b ≠ 0
Tdba : triangle d b a
Tdca : triangle d c a
abc_dba : angle a b c = angle d b a
acb_dca : angle a c b = angle d c a
prop1 : proportion (length b d) (length b a) (length b a) (length b c)
rat1 : length b d / length b a = length b a / length b c
⊢ length a b ^ 2 + length a c ^ 2 = length b c ^ 2
Theorem: pythagorean_proof_two
Proof state before:
case intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
Tabc : triangle a b c
ang_a : angle b a c = rightangle
d : point
Bbdc : B b d c
ang_bda : angle b d a = rightangle
ang_cda : angle c d a = rightangle
ba : length b a ≠ 0
ca : length c a ≠ 0
bc : length b c ≠ 0
cb : length c b ≠ 0
Tdba : triangle d b a
Tdca : triangle d c a
abc_dba : angle a b c = angle d b a
acb_dca : angle a c b = angle d c a
prop1 : proportion (length b d) (length b a) (length b a) (length b c)
rat1 : length b d / length b a = length b a / length b c
⊢ length a b ^ 2 + length a c ^ 2 = length b c ^ 2
Tactic:
field_simp at rat1
Proof state after:
case intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
Tabc : triangle a b c
ang_a : angle b a c = rightangle
d : point
Bbdc : B b d c
ang_bda : angle b d a = rightangle
ang_cda : angle c d a = rightangle
ba : length b a ≠ 0
ca : length c a ≠ 0
bc : length b c ≠ 0
cb : length c b ≠ 0
Tdba : triangle d b a
Tdca : triangle d c a
abc_dba : angle a b c = angle d b a
acb_dca : angle a c b = angle d c a
prop1 : proportion (length b d) (length b a) (length b a) (length b c)
rat1 : length b d * length b c = length b a * length b a
⊢ length a b ^ 2 + length a c ^ 2 = length b c ^ 2