Theorem: pythagoras_converse (Pythagoras/pythagoras_2.lean)

State before:
i : incidence_geometry
a b c : point
tri_abc : triangle a b c
sq_sum : length a b ^ 2 + length a c ^ 2 = length b c ^ 2
⊢ angle b a c = rightangle
Tactic:
rcases line_of_pts a c with ⟨L, aL, cL⟩
State after:
case intro.intro
i : incidence_geometry
a b c : point
tri_abc : triangle a b c
sq_sum : length a b ^ 2 + length a c ^ 2 = length b c ^ 2
L : line
aL : online a L
cL : online c L
⊢ angle b a c = rightangle

State before:
case intro.intro
i : incidence_geometry
a b c : point
tri_abc : triangle a b c
sq_sum : length a b ^ 2 + length a c ^ 2 = length b c ^ 2
L : line
aL : online a L
cL : online c L
⊢ angle b a c = rightangle
Tactic:
rcases line_of_pts a b with ⟨N, aN, bN⟩
State after:
case intro.intro.intro.intro
i : incidence_geometry
a b c : point
tri_abc : triangle a b c
sq_sum : length a b ^ 2 + length a c ^ 2 = length b c ^ 2
L : line
aL : online a L
cL : online c L
N : line
aN : online a N
bN : online b N
⊢ angle b a c = rightangle

State before:
case intro.intro.intro.intro
i : incidence_geometry
a b c : point
tri_abc : triangle a b c
sq_sum : length a b ^ 2 + length a c ^ 2 = length b c ^ 2
L : line
aL : online a L
cL : online c L
N : line
aN : online a N
bN : online b N
⊢ angle b a c = rightangle
Tactic:
rcases length_eq_B_of_ne_four (ne_21_of_tri tri_abc) (ne_21_of_tri tri_abc) with ⟨e, Bbae, ba_ae⟩
State after:
case intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
tri_abc : triangle a b c
sq_sum : length a b ^ 2 + length a c ^ 2 = length b c ^ 2
L : line
aL : online a L
cL : online c L
N : line
aN : online a N
bN : online b N
e : point
Bbae : B b a e
ba_ae : length b a = length a e
⊢ angle b a c = rightangle

State before:
case intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
tri_abc : triangle a b c
sq_sum : length a b ^ 2 + length a c ^ 2 = length b c ^ 2
L : line
aL : online a L
cL : online c L
N : line
aN : online a N
bN : online b N
e : point
Bbae : B b a e
ba_ae : length b a = length a e
⊢ angle b a c = rightangle
Tactic:
rcases perpendicular_of_online'' (ne_31_of_tri tri_abc) cL aL (offline_of_B_offline (B_symm Bbae)
  (online_3_of_B Bbae bN aN) aN aL cL (online_3_of_triangle aN bN tri_abc)) with ⟨d', d'eL, cad'_ra⟩
State after:
case intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
tri_abc : triangle a b c
sq_sum : length a b ^ 2 + length a c ^ 2 = length b c ^ 2
L : line
aL : online a L
cL : online c L
N : line
aN : online a N
bN : online b N
e : point
Bbae : B b a e
ba_ae : length b a = length a e
d' : point
d'eL : diffside d' e L
cad'_ra : angle c a d' = rightangle
⊢ angle b a c = rightangle

State before:
case intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
tri_abc : triangle a b c
sq_sum : length a b ^ 2 + length a c ^ 2 = length b c ^ 2
L : line
aL : online a L
cL : online c L
N : line
aN : online a N
bN : online b N
e : point
Bbae : B b a e
ba_ae : length b a = length a e
d' : point
d'eL : diffside d' e L
cad'_ra : angle c a d' = rightangle
⊢ angle b a c = rightangle
Tactic:
rcases length_eq_B_of_ne_four (ne_of_online aL d'eL.1).symm (ne_21_of_tri tri_abc)
  with ⟨d, Bd'ad, ba_ad⟩
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
tri_abc : triangle a b c
sq_sum : length a b ^ 2 + length a c ^ 2 = length b c ^ 2
L : line
aL : online a L
cL : online c L
N : line
aN : online a N
bN : online b N
e : point
Bbae : B b a e
ba_ae : length b a = length a e
d' : point
d'eL : diffside d' e L
cad'_ra : angle c a d' = rightangle
d : point
Bd'ad : B d' a d
ba_ad : length b a = length a d
⊢ angle b a c = rightangle

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
tri_abc : triangle a b c
sq_sum : length a b ^ 2 + length a c ^ 2 = length b c ^ 2
L : line
aL : online a L
cL : online c L
N : line
aN : online a N
bN : online b N
e : point
Bbae : B b a e
ba_ae : length b a = length a e
d' : point
d'eL : diffside d' e L
cad'_ra : angle c a d' = rightangle
d : point
Bd'ad : B d' a d
ba_ad : length b a = length a d
⊢ angle b a c = rightangle
Tactic:
rcases line_of_pts a d' with ⟨M, aM, d'M⟩
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
tri_abc : triangle a b c
sq_sum : length a b ^ 2 + length a c ^ 2 = length b c ^ 2
L : line
aL : online a L
cL : online c L
N : line
aN : online a N
bN : online b N
e : point
Bbae : B b a e
ba_ae : length b a = length a e
d' : point
d'eL : diffside d' e L
cad'_ra : angle c a d' = rightangle
d : point
Bd'ad : B d' a d
ba_ad : length b a = length a d
M : line
aM : online a M
d'M : online d' M
⊢ angle b a c = rightangle

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
tri_abc : triangle a b c
sq_sum : length a b ^ 2 + length a c ^ 2 = length b c ^ 2
L : line
aL : online a L
cL : online c L
N : line
aN : online a N
bN : online b N
e : point
Bbae : B b a e
ba_ae : length b a = length a e
d' : point
d'eL : diffside d' e L
cad'_ra : angle c a d' = rightangle
d : point
Bd'ad : B d' a d
ba_ad : length b a = length a d
M : line
aM : online a M
d'M : online d' M
⊢ angle b a c = rightangle
Tactic:
have cM := online_2_of_triangle aM d'M $ triangle_of_ne_online (ne_13_of_tri tri_abc) aL cL d'eL.1
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
tri_abc : triangle a b c
sq_sum : length a b ^ 2 + length a c ^ 2 = length b c ^ 2
L : line
aL : online a L
cL : online c L
N : line
aN : online a N
bN : online b N
e : point
Bbae : B b a e
ba_ae : length b a = length a e
d' : point
d'eL : diffside d' e L
cad'_ra : angle c a d' = rightangle
d : point
Bd'ad : B d' a d
ba_ad : length b a = length a d
M : line
aM : online a M
d'M : online d' M
cM : ¬online c M
⊢ angle b a c = rightangle

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
tri_abc : triangle a b c
sq_sum : length a b ^ 2 + length a c ^ 2 = length b c ^ 2
L : line
aL : online a L
cL : online c L
N : line
aN : online a N
bN : online b N
e : point
Bbae : B b a e
ba_ae : length b a = length a e
d' : point
d'eL : diffside d' e L
cad'_ra : angle c a d' = rightangle
d : point
Bd'ad : B d' a d
ba_ad : length b a = length a d
M : line
aM : online a M
d'M : online d' M
cM : ¬online c M
⊢ angle b a c = rightangle
Tactic:
have ang_split := two_right_of_flat_angle Bd'ad d'M aM cM
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
tri_abc : triangle a b c
sq_sum : length a b ^ 2 + length a c ^ 2 = length b c ^ 2
L : line
aL : online a L
cL : online c L
N : line
aN : online a N
bN : online b N
e : point
Bbae : B b a e
ba_ae : length b a = length a e
d' : point
d'eL : diffside d' e L
cad'_ra : angle c a d' = rightangle
d : point
Bd'ad : B d' a d
ba_ad : length b a = length a d
M : line
aM : online a M
d'M : online d' M
cM : ¬online c M
ang_split : angle c a d' + angle c a d = 2 * rightangle
⊢ angle b a c = rightangle

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
tri_abc : triangle a b c
sq_sum : length a b ^ 2 + length a c ^ 2 = length b c ^ 2
L : line
aL : online a L
cL : online c L
N : line
aN : online a N
bN : online b N
e : point
Bbae : B b a e
ba_ae : length b a = length a e
d' : point
d'eL : diffside d' e L
cad'_ra : angle c a d' = rightangle
d : point
Bd'ad : B d' a d
ba_ad : length b a = length a d
M : line
aM : online a M
d'M : online d' M
cM : ¬online c M
ang_split : angle c a d' + angle c a d = 2 * rightangle
⊢ angle b a c = rightangle
Tactic:
have pyth_2 := pythagorean_proof_two (triangle_of_ne_online (ne_23_of_B Bd'ad) aM
  (online_3_of_B Bd'ad d'M aM) cM) (by linperm)
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
tri_abc : triangle a b c
sq_sum : length a b ^ 2 + length a c ^ 2 = length b c ^ 2
L : line
aL : online a L
cL : online c L
N : line
aN : online a N
bN : online b N
e : point
Bbae : B b a e
ba_ae : length b a = length a e
d' : point
d'eL : diffside d' e L
cad'_ra : angle c a d' = rightangle
d : point
Bd'ad : B d' a d
ba_ad : length b a = length a d
M : line
aM : online a M
d'M : online d' M
cM : ¬online c M
ang_split : angle c a d' + angle c a d = 2 * rightangle
pyth_2 : length a d ^ 2 + length a c ^ 2 = length d c ^ 2
⊢ angle b a c = rightangle

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
tri_abc : triangle a b c
sq_sum : length a b ^ 2 + length a c ^ 2 = length b c ^ 2
L : line
aL : online a L
cL : online c L
N : line
aN : online a N
bN : online b N
e : point
Bbae : B b a e
ba_ae : length b a = length a e
d' : point
d'eL : diffside d' e L
cad'_ra : angle c a d' = rightangle
d : point
Bd'ad : B d' a d
ba_ad : length b a = length a d
M : line
aM : online a M
d'M : online d' M
cM : ¬online c M
ang_split : angle c a d' + angle c a d = 2 * rightangle
pyth_2 : length a d ^ 2 + length a c ^ 2 = length d c ^ 2
⊢ angle b a c = rightangle
Tactic:
rw[←ba_ad] at pyth_2
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
tri_abc : triangle a b c
sq_sum : length a b ^ 2 + length a c ^ 2 = length b c ^ 2
L : line
aL : online a L
cL : online c L
N : line
aN : online a N
bN : online b N
e : point
Bbae : B b a e
ba_ae : length b a = length a e
d' : point
d'eL : diffside d' e L
cad'_ra : angle c a d' = rightangle
d : point
Bd'ad : B d' a d
ba_ad : length b a = length a d
M : line
aM : online a M
d'M : online d' M
cM : ¬online c M
ang_split : angle c a d' + angle c a d = 2 * rightangle
pyth_2 : length b a ^ 2 + length a c ^ 2 = length d c ^ 2
⊢ angle b a c = rightangle

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
tri_abc : triangle a b c
sq_sum : length a b ^ 2 + length a c ^ 2 = length b c ^ 2
L : line
aL : online a L
cL : online c L
N : line
aN : online a N
bN : online b N
e : point
Bbae : B b a e
ba_ae : length b a = length a e
d' : point
d'eL : diffside d' e L
cad'_ra : angle c a d' = rightangle
d : point
Bd'ad : B d' a d
ba_ad : length b a = length a d
M : line
aM : online a M
d'M : online d' M
cM : ¬online c M
ang_split : angle c a d' + angle c a d = 2 * rightangle
pyth_2 : length b a ^ 2 + length a c ^ 2 = length d c ^ 2
⊢ angle b a c = rightangle
Tactic:
have sq_eq : (length c d)^2 = (length b c)^2 := by linperm
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
tri_abc : triangle a b c
sq_sum : length a b ^ 2 + length a c ^ 2 = length b c ^ 2
L : line
aL : online a L
cL : online c L
N : line
aN : online a N
bN : online b N
e : point
Bbae : B b a e
ba_ae : length b a = length a e
d' : point
d'eL : diffside d' e L
cad'_ra : angle c a d' = rightangle
d : point
Bd'ad : B d' a d
ba_ad : length b a = length a d
M : line
aM : online a M
d'M : online d' M
cM : ¬online c M
ang_split : angle c a d' + angle c a d = 2 * rightangle
pyth_2 : length b a ^ 2 + length a c ^ 2 = length d c ^ 2
sq_eq : length c d ^ 2 = length b c ^ 2
⊢ angle b a c = rightangle

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
tri_abc : triangle a b c
sq_sum : length a b ^ 2 + length a c ^ 2 = length b c ^ 2
L : line
aL : online a L
cL : online c L
N : line
aN : online a N
bN : online b N
e : point
Bbae : B b a e
ba_ae : length b a = length a e
d' : point
d'eL : diffside d' e L
cad'_ra : angle c a d' = rightangle
d : point
Bd'ad : B d' a d
ba_ad : length b a = length a d
M : line
aM : online a M
d'M : online d' M
cM : ¬online c M
ang_split : angle c a d' + angle c a d = 2 * rightangle
pyth_2 : length b a ^ 2 + length a c ^ 2 = length d c ^ 2
sq_eq : length c d ^ 2 = length b c ^ 2
⊢ angle b a c = rightangle
Tactic:
rw[sq_eq_sq_iff_abs_eq_abs] at sq_eq
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
tri_abc : triangle a b c
sq_sum : length a b ^ 2 + length a c ^ 2 = length b c ^ 2
L : line
aL : online a L
cL : online c L
N : line
aN : online a N
bN : online b N
e : point
Bbae : B b a e
ba_ae : length b a = length a e
d' : point
d'eL : diffside d' e L
cad'_ra : angle c a d' = rightangle
d : point
Bd'ad : B d' a d
ba_ad : length b a = length a d
M : line
aM : online a M
d'M : online d' M
cM : ¬online c M
ang_split : angle c a d' + angle c a d = 2 * rightangle
pyth_2 : length b a ^ 2 + length a c ^ 2 = length d c ^ 2
sq_eq : abs (length c d) = abs (length b c)
⊢ angle b a c = rightangle

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
tri_abc : triangle a b c
sq_sum : length a b ^ 2 + length a c ^ 2 = length b c ^ 2
L : line
aL : online a L
cL : online c L
N : line
aN : online a N
bN : online b N
e : point
Bbae : B b a e
ba_ae : length b a = length a e
d' : point
d'eL : diffside d' e L
cad'_ra : angle c a d' = rightangle
d : point
Bd'ad : B d' a d
ba_ad : length b a = length a d
M : line
aM : online a M
d'M : online d' M
cM : ¬online c M
ang_split : angle c a d' + angle c a d = 2 * rightangle
pyth_2 : length b a ^ 2 + length a c ^ 2 = length d c ^ 2
sq_eq : abs (length c d) = abs (length b c)
⊢ angle b a c = rightangle
Tactic:
have sq_eq' : (length c d) = (length b c) :=
by linperm[abs_of_nonneg (length_nonneg b c), abs_of_nonneg (length_nonneg c d)]
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
tri_abc : triangle a b c
sq_sum : length a b ^ 2 + length a c ^ 2 = length b c ^ 2
L : line
aL : online a L
cL : online c L
N : line
aN : online a N
bN : online b N
e : point
Bbae : B b a e
ba_ae : length b a = length a e
d' : point
d'eL : diffside d' e L
cad'_ra : angle c a d' = rightangle
d : point
Bd'ad : B d' a d
ba_ad : length b a = length a d
M : line
aM : online a M
d'M : online d' M
cM : ¬online c M
ang_split : angle c a d' + angle c a d = 2 * rightangle
pyth_2 : length b a ^ 2 + length a c ^ 2 = length d c ^ 2
sq_eq : abs (length c d) = abs (length b c)
sq_eq' : length c d = length b c
⊢ angle b a c = rightangle

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
tri_abc : triangle a b c
sq_sum : length a b ^ 2 + length a c ^ 2 = length b c ^ 2
L : line
aL : online a L
cL : online c L
N : line
aN : online a N
bN : online b N
e : point
Bbae : B b a e
ba_ae : length b a = length a e
d' : point
d'eL : diffside d' e L
cad'_ra : angle c a d' = rightangle
d : point
Bd'ad : B d' a d
ba_ad : length b a = length a d
M : line
aM : online a M
d'M : online d' M
cM : ¬online c M
ang_split : angle c a d' + angle c a d = 2 * rightangle
pyth_2 : length b a ^ 2 + length a c ^ 2 = length d c ^ 2
sq_eq : abs (length c d) = abs (length b c)
sq_eq' : length c d = length b c
⊢ angle b a c = rightangle
Tactic:
linperm[(sss (by linperm : length a d = length a b) (by linperm : length d c = length b c) rfl).2.1]
State after:
no goals

State before:
i : incidence_geometry
a b c : point
tri_abc : triangle a b c
sq_sum : length a b ^ 2 + length a c ^ 2 = length b c ^ 2
L : line
aL : online a L
cL : online c L
N : line
aN : online a N
bN : online b N
e : point
Bbae : B b a e
ba_ae : length b a = length a e
d' : point
d'eL : diffside d' e L
cad'_ra : angle c a d' = rightangle
d : point
Bd'ad : B d' a d
ba_ad : length b a = length a d
M : line
aM : online a M
d'M : online d' M
cM : ¬online c M
ang_split : angle c a d' + angle c a d = 2 * rightangle
⊢ angle d a c = rightangle
Tactic:
linperm
State after:
no goals

State before:
i : incidence_geometry
a b c : point
tri_abc : triangle a b c
sq_sum : length a b ^ 2 + length a c ^ 2 = length b c ^ 2
L : line
aL : online a L
cL : online c L
N : line
aN : online a N
bN : online b N
e : point
Bbae : B b a e
ba_ae : length b a = length a e
d' : point
d'eL : diffside d' e L
cad'_ra : angle c a d' = rightangle
d : point
Bd'ad : B d' a d
ba_ad : length b a = length a d
M : line
aM : online a M
d'M : online d' M
cM : ¬online c M
ang_split : angle c a d' + angle c a d = 2 * rightangle
pyth_2 : length b a ^ 2 + length a c ^ 2 = length d c ^ 2
⊢ length c d ^ 2 = length b c ^ 2
Tactic:
linperm
State after:
no goals

State before:
i : incidence_geometry
a b c : point
tri_abc : triangle a b c
sq_sum : length a b ^ 2 + length a c ^ 2 = length b c ^ 2
L : line
aL : online a L
cL : online c L
N : line
aN : online a N
bN : online b N
e : point
Bbae : B b a e
ba_ae : length b a = length a e
d' : point
d'eL : diffside d' e L
cad'_ra : angle c a d' = rightangle
d : point
Bd'ad : B d' a d
ba_ad : length b a = length a d
M : line
aM : online a M
d'M : online d' M
cM : ¬online c M
ang_split : angle c a d' + angle c a d = 2 * rightangle
pyth_2 : length b a ^ 2 + length a c ^ 2 = length d c ^ 2
sq_eq : abs (length c d) = abs (length b c)
⊢ length c d = length b c
Tactic:
linperm[abs_of_nonneg (length_nonneg b c), abs_of_nonneg (length_nonneg c d)]
State after:
no goals

State before:
i : incidence_geometry
a b c : point
tri_abc : triangle a b c
sq_sum : length a b ^ 2 + length a c ^ 2 = length b c ^ 2
L : line
aL : online a L
cL : online c L
N : line
aN : online a N
bN : online b N
e : point
Bbae : B b a e
ba_ae : length b a = length a e
d' : point
d'eL : diffside d' e L
cad'_ra : angle c a d' = rightangle
d : point
Bd'ad : B d' a d
ba_ad : length b a = length a d
M : line
aM : online a M
d'M : online d' M
cM : ¬online c M
ang_split : angle c a d' + angle c a d = 2 * rightangle
pyth_2 : length b a ^ 2 + length a c ^ 2 = length d c ^ 2
sq_eq : abs (length c d) = abs (length b c)
sq_eq' : length c d = length b c
⊢ length a d = length a b
Tactic:
linperm
State after:
no goals

State before:
i : incidence_geometry
a b c : point
tri_abc : triangle a b c
sq_sum : length a b ^ 2 + length a c ^ 2 = length b c ^ 2
L : line
aL : online a L
cL : online c L
N : line
aN : online a N
bN : online b N
e : point
Bbae : B b a e
ba_ae : length b a = length a e
d' : point
d'eL : diffside d' e L
cad'_ra : angle c a d' = rightangle
d : point
Bd'ad : B d' a d
ba_ad : length b a = length a d
M : line
aM : online a M
d'M : online d' M
cM : ¬online c M
ang_split : angle c a d' + angle c a d = 2 * rightangle
pyth_2 : length b a ^ 2 + length a c ^ 2 = length d c ^ 2
sq_eq : abs (length c d) = abs (length b c)
sq_eq' : length c d = length b c
⊢ length d c = length b c
Tactic:
linperm
State after:
no goals