Theorem: same_length_B_of_ne_ge (Pythagoras/euclid_I_extras.lean)

State before:
i : incidence_geometry
a b c d : point
ab : a ≠ b
big : length a b < length c d
⊢ ∃ p, B a b p ∧ length a p = length c d
Tactic:
have cd : c ≠ d := fun cd => by
  rw [cd, length_eq_zero_iff.mpr rfl] at big;
  exact not_lt_of_ge (length_nonneg a b) big
State after:
i : incidence_geometry
a b c d : point
ab : a ≠ b
big : length a b < length c d
cd : c ≠ d
⊢ ∃ p, B a b p ∧ length a p = length c d

State before:
i : incidence_geometry
a b c d : point
ab : a ≠ b
big : length a b < length c d
cd : c ≠ d
⊢ ∃ p, B a b p ∧ length a p = length c d
Tactic:
obtain ⟨q, Hq⟩ := length_eq_B_of_ne_four ab.symm cd
State after:
case intro
i : incidence_geometry
a b c d : point
ab : a ≠ b
big : length a b < length c d
cd : c ≠ d
q : point
Hq : B b a q ∧ length c d = length a q
⊢ ∃ p, B a b p ∧ length a p = length c d

State before:
case intro
i : incidence_geometry
a b c d : point
ab : a ≠ b
big : length a b < length c d
cd : c ≠ d
q : point
Hq : B b a q ∧ length c d = length a q
⊢ ∃ p, B a b p ∧ length a p = length c d
Tactic:
have aq : a ≠ q := fun aq => by
  rw [aq, length_eq_zero_iff.mpr rfl] at Hq; rw [Hq.2] at big
  exact not_lt_of_ge (length_nonneg a b) big
State after:
case intro
i : incidence_geometry
a b c d : point
ab : a ≠ b
big : length a b < length c d
cd : c ≠ d
q : point
Hq : B b a q ∧ length c d = length a q
aq : a ≠ q
⊢ ∃ p, B a b p ∧ length a p = length c d

State before:
case intro
i : incidence_geometry
a b c d : point
ab : a ≠ b
big : length a b < length c d
cd : c ≠ d
q : point
Hq : B b a q ∧ length c d = length a q
aq : a ≠ q
⊢ ∃ p, B a b p ∧ length a p = length c d
Tactic:
obtain ⟨C, hC⟩ := circle_of_ne aq
State after:
case intro.intro
i : incidence_geometry
a b c d : point
ab : a ≠ b
big : length a b < length c d
cd : c ≠ d
q : point
Hq : B b a q ∧ length c d = length a q
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
⊢ ∃ p, B a b p ∧ length a p = length c d

State before:
case intro.intro
i : incidence_geometry
a b c d : point
ab : a ≠ b
big : length a b < length c d
cd : c ≠ d
q : point
Hq : B b a q ∧ length c d = length a q
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
⊢ ∃ p, B a b p ∧ length a p = length c d
Tactic:
obtain ⟨p, Hp⟩ := pt_oncircle_of_inside_ne aq.symm (inside_circle_of_center hC.1)
State after:
case intro.intro.intro
i : incidence_geometry
a b c d : point
ab : a ≠ b
big : length a b < length c d
cd : c ≠ d
q : point
Hq : B b a q ∧ length c d = length a q
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
p : point
Hp : B q a p ∧ on_circle p C
⊢ ∃ p, B a b p ∧ length a p = length c d

State before:
case intro.intro.intro
i : incidence_geometry
a b c d : point
ab : a ≠ b
big : length a b < length c d
cd : c ≠ d
q : point
Hq : B b a q ∧ length c d = length a q
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
p : point
Hp : B q a p ∧ on_circle p C
⊢ ∃ p, B a b p ∧ length a p = length c d
Tactic:
obtain ⟨AB, aAB, bAB⟩ := line_of_pts a b
State after:
case intro.intro.intro.intro.intro
i : incidence_geometry
a b c d : point
ab : a ≠ b
big : length a b < length c d
cd : c ≠ d
q : point
Hq : B b a q ∧ length c d = length a q
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
p : point
Hp : B q a p ∧ on_circle p C
AB : line
aAB : online a AB
bAB : online b AB
⊢ ∃ p, B a b p ∧ length a p = length c d

State before:
case intro.intro.intro.intro.intro
i : incidence_geometry
a b c d : point
ab : a ≠ b
big : length a b < length c d
cd : c ≠ d
q : point
Hq : B b a q ∧ length c d = length a q
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
p : point
Hp : B q a p ∧ on_circle p C
AB : line
aAB : online a AB
bAB : online b AB
⊢ ∃ p, B a b p ∧ length a p = length c d
Tactic:
have qAB := online_3_of_B Hq.1 bAB aAB
State after:
case intro.intro.intro.intro.intro
i : incidence_geometry
a b c d : point
ab : a ≠ b
big : length a b < length c d
cd : c ≠ d
q : point
Hq : B b a q ∧ length c d = length a q
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
p : point
Hp : B q a p ∧ on_circle p C
AB : line
aAB : online a AB
bAB : online b AB
qAB : online q AB
⊢ ∃ p, B a b p ∧ length a p = length c d

State before:
case intro.intro.intro.intro.intro
i : incidence_geometry
a b c d : point
ab : a ≠ b
big : length a b < length c d
cd : c ≠ d
q : point
Hq : B b a q ∧ length c d = length a q
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
p : point
Hp : B q a p ∧ on_circle p C
AB : line
aAB : online a AB
bAB : online b AB
qAB : online q AB
⊢ ∃ p, B a b p ∧ length a p = length c d
Tactic:
have pAB := online_3_of_B Hp.1 qAB aAB
State after:
case intro.intro.intro.intro.intro
i : incidence_geometry
a b c d : point
ab : a ≠ b
big : length a b < length c d
cd : c ≠ d
q : point
Hq : B b a q ∧ length c d = length a q
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
p : point
Hp : B q a p ∧ on_circle p C
AB : line
aAB : online a AB
bAB : online b AB
qAB : online q AB
pAB : online p AB
⊢ ∃ p, B a b p ∧ length a p = length c d

State before:
case intro.intro.intro.intro.intro
i : incidence_geometry
a b c d : point
ab : a ≠ b
big : length a b < length c d
cd : c ≠ d
q : point
Hq : B b a q ∧ length c d = length a q
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
p : point
Hp : B q a p ∧ on_circle p C
AB : line
aAB : online a AB
bAB : online b AB
qAB : online q AB
pAB : online p AB
⊢ ∃ p, B a b p ∧ length a p = length c d
Tactic:
have := (on_circle_iff_length_eq hC.1 Hp.2).mpr hC.2
State after:
case intro.intro.intro.intro.intro
i : incidence_geometry
a b c d : point
ab : a ≠ b
big : length a b < length c d
cd : c ≠ d
q : point
Hq : B b a q ∧ length c d = length a q
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
p : point
Hp : B q a p ∧ on_circle p C
AB : line
aAB : online a AB
bAB : online b AB
qAB : online q AB
pAB : online p AB
this : length a p = length a q
⊢ ∃ p, B a b p ∧ length a p = length c d

State before:
case intro.intro.intro.intro.intro
i : incidence_geometry
a b c d : point
ab : a ≠ b
big : length a b < length c d
cd : c ≠ d
q : point
Hq : B b a q ∧ length c d = length a q
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
p : point
Hp : B q a p ∧ on_circle p C
AB : line
aAB : online a AB
bAB : online b AB
qAB : online q AB
pAB : online p AB
this : length a p = length a q
⊢ ∃ p, B a b p ∧ length a p = length c d
Tactic:
rw [← this] at Hq
State after:
case intro.intro.intro.intro.intro
i : incidence_geometry
a b c d : point
ab : a ≠ b
big : length a b < length c d
cd : c ≠ d
q : point
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
p : point
Hq : B b a q ∧ length c d = length a p
Hp : B q a p ∧ on_circle p C
AB : line
aAB : online a AB
bAB : online b AB
qAB : online q AB
pAB : online p AB
this : length a p = length a q
⊢ ∃ p, B a b p ∧ length a p = length c d

State before:
case intro.intro.intro.intro.intro
i : incidence_geometry
a b c d : point
ab : a ≠ b
big : length a b < length c d
cd : c ≠ d
q : point
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
p : point
Hq : B b a q ∧ length c d = length a p
Hp : B q a p ∧ on_circle p C
AB : line
aAB : online a AB
bAB : online b AB
qAB : online q AB
pAB : online p AB
this : length a p = length a q
⊢ ∃ p, B a b p ∧ length a p = length c d
Tactic:
rw [Hq.2] at big
State after:
case intro.intro.intro.intro.intro
i : incidence_geometry
a b c d : point
ab : a ≠ b
cd : c ≠ d
q : point
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
p : point
big : length a b < length a p
Hq : B b a q ∧ length c d = length a p
Hp : B q a p ∧ on_circle p C
AB : line
aAB : online a AB
bAB : online b AB
qAB : online q AB
pAB : online p AB
this : length a p = length a q
⊢ ∃ p, B a b p ∧ length a p = length c d

State before:
case intro.intro.intro.intro.intro
i : incidence_geometry
a b c d : point
ab : a ≠ b
cd : c ≠ d
q : point
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
p : point
big : length a b < length a p
Hq : B b a q ∧ length c d = length a p
Hp : B q a p ∧ on_circle p C
AB : line
aAB : online a AB
bAB : online b AB
qAB : online q AB
pAB : online p AB
this : length a p = length a q
⊢ ∃ p, B a b p ∧ length a p = length c d
Tactic:
have bp : b ≠ p := fun bp => by
  rw [←bp, bp] at Hq; rw [bp] at big
  simp [lt_self_iff_false] at big
State after:
case intro.intro.intro.intro.intro
i : incidence_geometry
a b c d : point
ab : a ≠ b
cd : c ≠ d
q : point
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
p : point
big : length a b < length a p
Hq : B b a q ∧ length c d = length a p
Hp : B q a p ∧ on_circle p C
AB : line
aAB : online a AB
bAB : online b AB
qAB : online q AB
pAB : online p AB
this : length a p = length a q
bp : b ≠ p
⊢ ∃ p, B a b p ∧ length a p = length c d

State before:
case intro.intro.intro.intro.intro
i : incidence_geometry
a b c d : point
ab : a ≠ b
cd : c ≠ d
q : point
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
p : point
big : length a b < length a p
Hq : B b a q ∧ length c d = length a p
Hp : B q a p ∧ on_circle p C
AB : line
aAB : online a AB
bAB : online b AB
qAB : online q AB
pAB : online p AB
this : length a p = length a q
bp : b ≠ p
⊢ ∃ p, B a b p ∧ length a p = length c d
Tactic:
have ap := (ne_12_of_B (B_symm Hp.1)).symm
State after:
case intro.intro.intro.intro.intro
i : incidence_geometry
a b c d : point
ab : a ≠ b
cd : c ≠ d
q : point
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
p : point
big : length a b < length a p
Hq : B b a q ∧ length c d = length a p
Hp : B q a p ∧ on_circle p C
AB : line
aAB : online a AB
bAB : online b AB
qAB : online q AB
pAB : online p AB
this : length a p = length a q
bp : b ≠ p
ap : a ≠ p
⊢ ∃ p, B a b p ∧ length a p = length c d

State before:
case intro.intro.intro.intro.intro
i : incidence_geometry
a b c d : point
ab : a ≠ b
cd : c ≠ d
q : point
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
p : point
big : length a b < length a p
Hq : B b a q ∧ length c d = length a p
Hp : B q a p ∧ on_circle p C
AB : line
aAB : online a AB
bAB : online b AB
qAB : online q AB
pAB : online p AB
this : length a p = length a q
bp : b ≠ p
ap : a ≠ p
⊢ ∃ p, B a b p ∧ length a p = length c d
Tactic:
refine' ⟨p, _, Hq.2.symm⟩
State after:
case intro.intro.intro.intro.intro
i : incidence_geometry
a b c d : point
ab : a ≠ b
cd : c ≠ d
q : point
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
p : point
big : length a b < length a p
Hq : B b a q ∧ length c d = length a p
Hp : B q a p ∧ on_circle p C
AB : line
aAB : online a AB
bAB : online b AB
qAB : online q AB
pAB : online p AB
this : length a p = length a q
bp : b ≠ p
ap : a ≠ p
⊢ B a b p

State before:
case intro.intro.intro.intro.intro
i : incidence_geometry
a b c d : point
ab : a ≠ b
cd : c ≠ d
q : point
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
p : point
big : length a b < length a p
Hq : B b a q ∧ length c d = length a p
Hp : B q a p ∧ on_circle p C
AB : line
aAB : online a AB
bAB : online b AB
qAB : online q AB
pAB : online p AB
this : length a p = length a q
bp : b ≠ p
ap : a ≠ p
⊢ B a b p
Tactic:
have B3 := B_of_three_online_ne_short big ab ap bp aAB bAB pAB
State after:
case intro.intro.intro.intro.intro
i : incidence_geometry
a b c d : point
ab : a ≠ b
cd : c ≠ d
q : point
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
p : point
big : length a b < length a p
Hq : B b a q ∧ length c d = length a p
Hp : B q a p ∧ on_circle p C
AB : line
aAB : online a AB
bAB : online b AB
qAB : online q AB
pAB : online p AB
this : length a p = length a q
bp : b ≠ p
ap : a ≠ p
B3 : B a b p ∨ B b a p
⊢ B a b p

State before:
case intro.intro.intro.intro.intro
i : incidence_geometry
a b c d : point
ab : a ≠ b
cd : c ≠ d
q : point
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
p : point
big : length a b < length a p
Hq : B b a q ∧ length c d = length a p
Hp : B q a p ∧ on_circle p C
AB : line
aAB : online a AB
bAB : online b AB
qAB : online q AB
pAB : online p AB
this : length a p = length a q
bp : b ≠ p
ap : a ≠ p
B3 : B a b p ∨ B b a p
⊢ B a b p
Tactic:
cases B3 with
| inl B3 => exact B3
| inr B3 => exfalso; exact (not_B324_of_B123_B124 (B_symm Hq.1) Hp.1) B3
State after:
no goals

State before:
i : incidence_geometry
a b c d : point
ab : a ≠ b
big : length a b < length c d
cd : c = d
⊢ False
Tactic:
rw [cd, length_eq_zero_iff.mpr rfl] at big
State after:
i : incidence_geometry
a b c d : point
ab : a ≠ b
big : length a b < 0
cd : c = d
⊢ False

State before:
i : incidence_geometry
a b c d : point
ab : a ≠ b
big : length a b < 0
cd : c = d
⊢ False
Tactic:
exact not_lt_of_ge (length_nonneg a b) big
State after:
no goals

State before:
i : incidence_geometry
a b c d : point
ab : a ≠ b
big : length a b < length c d
cd : c ≠ d
q : point
Hq : B b a q ∧ length c d = length a q
aq : a = q
⊢ False
Tactic:
rw [aq, length_eq_zero_iff.mpr rfl] at Hq
State after:
i : incidence_geometry
a b c d : point
ab : a ≠ b
big : length a b < length c d
cd : c ≠ d
q : point
Hq : B b q q ∧ length c d = 0
aq : a = q
⊢ False

State before:
i : incidence_geometry
a b c d : point
ab : a ≠ b
big : length a b < length c d
cd : c ≠ d
q : point
Hq : B b q q ∧ length c d = 0
aq : a = q
⊢ False
Tactic:
rw [Hq.2] at big
State after:
i : incidence_geometry
a b c d : point
ab : a ≠ b
big : length a b < 0
cd : c ≠ d
q : point
Hq : B b q q ∧ length c d = 0
aq : a = q
⊢ False

State before:
i : incidence_geometry
a b c d : point
ab : a ≠ b
big : length a b < 0
cd : c ≠ d
q : point
Hq : B b q q ∧ length c d = 0
aq : a = q
⊢ False
Tactic:
exact not_lt_of_ge (length_nonneg a b) big
State after:
no goals

State before:
i : incidence_geometry
a b c d : point
ab : a ≠ b
cd : c ≠ d
q : point
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
p : point
big : length a b < length a p
Hq : B b a q ∧ length c d = length a p
Hp : B q a p ∧ on_circle p C
AB : line
aAB : online a AB
bAB : online b AB
qAB : online q AB
pAB : online p AB
this : length a p = length a q
bp : b = p
⊢ False
Tactic:
rw [←bp, bp] at Hq
State after:
i : incidence_geometry
a b c d : point
ab : a ≠ b
cd : c ≠ d
q : point
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
p : point
big : length a b < length a p
Hq : B p a q ∧ length c d = length a p
Hp : B q a p ∧ on_circle p C
AB : line
aAB : online a AB
bAB : online b AB
qAB : online q AB
pAB : online p AB
this : length a p = length a q
bp : b = p
⊢ False

State before:
i : incidence_geometry
a b c d : point
ab : a ≠ b
cd : c ≠ d
q : point
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
p : point
big : length a b < length a p
Hq : B p a q ∧ length c d = length a p
Hp : B q a p ∧ on_circle p C
AB : line
aAB : online a AB
bAB : online b AB
qAB : online q AB
pAB : online p AB
this : length a p = length a q
bp : b = p
⊢ False
Tactic:
rw [bp] at big
State after:
i : incidence_geometry
a b c d : point
ab : a ≠ b
cd : c ≠ d
q : point
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
p : point
big : length a p < length a p
Hq : B p a q ∧ length c d = length a p
Hp : B q a p ∧ on_circle p C
AB : line
aAB : online a AB
bAB : online b AB
qAB : online q AB
pAB : online p AB
this : length a p = length a q
bp : b = p
⊢ False

State before:
i : incidence_geometry
a b c d : point
ab : a ≠ b
cd : c ≠ d
q : point
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
p : point
big : length a p < length a p
Hq : B p a q ∧ length c d = length a p
Hp : B q a p ∧ on_circle p C
AB : line
aAB : online a AB
bAB : online b AB
qAB : online q AB
pAB : online p AB
this : length a p = length a q
bp : b = p
⊢ False
Tactic:
simp [lt_self_iff_false] at big
State after:
no goals

State before:
case intro.intro.intro.intro.intro.inl
i : incidence_geometry
a b c d : point
ab : a ≠ b
cd : c ≠ d
q : point
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
p : point
big : length a b < length a p
Hq : B b a q ∧ length c d = length a p
Hp : B q a p ∧ on_circle p C
AB : line
aAB : online a AB
bAB : online b AB
qAB : online q AB
pAB : online p AB
this : length a p = length a q
bp : b ≠ p
ap : a ≠ p
B3 : B a b p
⊢ B a b p
Tactic:
exact B3
State after:
no goals

State before:
case intro.intro.intro.intro.intro.inr
i : incidence_geometry
a b c d : point
ab : a ≠ b
cd : c ≠ d
q : point
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
p : point
big : length a b < length a p
Hq : B b a q ∧ length c d = length a p
Hp : B q a p ∧ on_circle p C
AB : line
aAB : online a AB
bAB : online b AB
qAB : online q AB
pAB : online p AB
this : length a p = length a q
bp : b ≠ p
ap : a ≠ p
B3 : B b a p
⊢ B a b p
Tactic:
exfalso
State after:
case intro.intro.intro.intro.intro.inr.h
i : incidence_geometry
a b c d : point
ab : a ≠ b
cd : c ≠ d
q : point
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
p : point
big : length a b < length a p
Hq : B b a q ∧ length c d = length a p
Hp : B q a p ∧ on_circle p C
AB : line
aAB : online a AB
bAB : online b AB
qAB : online q AB
pAB : online p AB
this : length a p = length a q
bp : b ≠ p
ap : a ≠ p
B3 : B b a p
⊢ False

State before:
case intro.intro.intro.intro.intro.inr.h
i : incidence_geometry
a b c d : point
ab : a ≠ b
cd : c ≠ d
q : point
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
p : point
big : length a b < length a p
Hq : B b a q ∧ length c d = length a p
Hp : B q a p ∧ on_circle p C
AB : line
aAB : online a AB
bAB : online b AB
qAB : online q AB
pAB : online p AB
this : length a p = length a q
bp : b ≠ p
ap : a ≠ p
B3 : B b a p
⊢ False
Tactic:
exact (not_B324_of_B123_B124 (B_symm Hq.1) Hp.1) B3
State after:
no goals