Theorem: rescale_length (Pythagoras/euclid_VI.lean)

State before:
i : incidence_geometry
a b : point
L : line
n : ℕ
aL : online a L
bL : online b L
⊢ ∃ c, online c L ∧ length a c = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b c)
Tactic:
by_cases ab: a = b
State after:
case pos
i : incidence_geometry
a b : point
L : line
n : ℕ
aL : online a L
bL : online b L
ab : a = b
⊢ ∃ c, online c L ∧ length a c = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b c)

case neg
i : incidence_geometry
a b : point
L : line
n : ℕ
aL : online a L
bL : online b L
ab : ¬a = b
⊢ ∃ c, online c L ∧ length a c = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b c)

State before:
case pos
i : incidence_geometry
a b : point
L : line
n : ℕ
aL : online a L
bL : online b L
ab : a = b
⊢ ∃ c, online c L ∧ length a c = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b c)
Tactic:
use a
State after:
case pos
i : incidence_geometry
a b : point
L : line
n : ℕ
aL : online a L
bL : online b L
ab : a = b
⊢ online a L ∧ length a a = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b a)

State before:
case pos
i : incidence_geometry
a b : point
L : line
n : ℕ
aL : online a L
bL : online b L
ab : a = b
⊢ online a L ∧ length a a = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b a)
Tactic:
rw [← ab, length_eq_zero_iff.mpr rfl]
State after:
case pos
i : incidence_geometry
a b : point
L : line
n : ℕ
aL : online a L
bL : online b L
ab : a = b
⊢ online a L ∧ 0 = ↑n * 0 ∧ (n ≥ 2 ∧ a ≠ a → B a a a)

State before:
case pos
i : incidence_geometry
a b : point
L : line
n : ℕ
aL : online a L
bL : online b L
ab : a = b
⊢ online a L ∧ 0 = ↑n * 0 ∧ (n ≥ 2 ∧ a ≠ a → B a a a)
Tactic:
simp
State after:
case pos
i : incidence_geometry
a b : point
L : line
n : ℕ
aL : online a L
bL : online b L
ab : a = b
⊢ online a L

State before:
case pos
i : incidence_geometry
a b : point
L : line
n : ℕ
aL : online a L
bL : online b L
ab : a = b
⊢ online a L
Tactic:
exact aL
State after:
no goals

State before:
case neg.zero
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
⊢ ∃ c, online c L ∧ length a c = ↑Nat.zero * length a b ∧ (Nat.zero ≥ 2 ∧ a ≠ b → B a b c)
Tactic:
use a
State after:
case neg.zero
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
⊢ online a L ∧ length a a = ↑Nat.zero * length a b ∧ (Nat.zero ≥ 2 ∧ a ≠ b → B a b a)

State before:
case neg.zero
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
⊢ online a L ∧ length a a = ↑Nat.zero * length a b ∧ (Nat.zero ≥ 2 ∧ a ≠ b → B a b a)
Tactic:
rw [length_eq_zero_iff.mpr rfl]
State after:
case neg.zero
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
⊢ online a L ∧ 0 = ↑Nat.zero * length a b ∧ (Nat.zero ≥ 2 ∧ a ≠ b → B a b a)

State before:
case neg.zero
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
⊢ online a L ∧ 0 = ↑Nat.zero * length a b ∧ (Nat.zero ≥ 2 ∧ a ≠ b → B a b a)
Tactic:
simp
State after:
case neg.zero
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
⊢ online a L

State before:
case neg.zero
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
⊢ online a L
Tactic:
exact aL
State after:
no goals

State before:
case neg.succ
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
hn : ∃ c, online c L ∧ length a c = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b c)
⊢ ∃ c, online c L ∧ length a c = ↑(Nat.succ n) * length a b ∧ (Nat.succ n ≥ 2 ∧ a ≠ b → B a b c)
Tactic:
by_cases n0: n = 0
State after:
case pos
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
hn : ∃ c, online c L ∧ length a c = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b c)
n0 : n = 0
⊢ ∃ c, online c L ∧ length a c = ↑(Nat.succ n) * length a b ∧ (Nat.succ n ≥ 2 ∧ a ≠ b → B a b c)

case neg
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
hn : ∃ c, online c L ∧ length a c = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b c)
n0 : ¬n = 0
⊢ ∃ c, online c L ∧ length a c = ↑(Nat.succ n) * length a b ∧ (Nat.succ n ≥ 2 ∧ a ≠ b → B a b c)

State before:
case neg
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
hn : ∃ c, online c L ∧ length a c = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b c)
n0 : ¬n = 0
⊢ ∃ c, online c L ∧ length a c = ↑(Nat.succ n) * length a b ∧ (Nat.succ n ≥ 2 ∧ a ≠ b → B a b c)
Tactic:
by_cases n1 : n = 1
State after:
case pos
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
hn : ∃ c, online c L ∧ length a c = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b c)
n0 : ¬n = 0
n1 : n = 1
⊢ ∃ c, online c L ∧ length a c = ↑(Nat.succ n) * length a b ∧ (Nat.succ n ≥ 2 ∧ a ≠ b → B a b c)

case neg
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
hn : ∃ c, online c L ∧ length a c = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b c)
n0 : ¬n = 0
n1 : ¬n = 1
⊢ ∃ c, online c L ∧ length a c = ↑(Nat.succ n) * length a b ∧ (Nat.succ n ≥ 2 ∧ a ≠ b → B a b c)

State before:
case neg
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
hn : ∃ c, online c L ∧ length a c = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b c)
n0 : ¬n = 0
n1 : ¬n = 1
⊢ ∃ c, online c L ∧ length a c = ↑(Nat.succ n) * length a b ∧ (Nat.succ n ≥ 2 ∧ a ≠ b → B a b c)
Tactic:
obtain ⟨ d, Hd ⟩ := hn
State after:
case neg.intro
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
n0 : ¬n = 0
n1 : ¬n = 1
d : point
Hd : online d L ∧ length a d = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b d)
⊢ ∃ c, online c L ∧ length a c = ↑(Nat.succ n) * length a b ∧ (Nat.succ n ≥ 2 ∧ a ≠ b → B a b c)

State before:
case neg.intro
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
n0 : ¬n = 0
n1 : ¬n = 1
d : point
Hd : online d L ∧ length a d = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b d)
⊢ ∃ c, online c L ∧ length a c = ↑(Nat.succ n) * length a b ∧ (Nat.succ n ≥ 2 ∧ a ≠ b → B a b c)
Tactic:
have ad : a ≠ d := by
  apply nq_of_len_pos
  rw [Hd.2.1]; simp [Nat.pos_of_ne_zero n0, zero_lt_mul_left, Nat.cast_pos]
  exact len_pos_of_nq ab
State after:
case neg.intro
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
n0 : ¬n = 0
n1 : ¬n = 1
d : point
Hd : online d L ∧ length a d = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b d)
ad : a ≠ d
⊢ ∃ c, online c L ∧ length a c = ↑(Nat.succ n) * length a b ∧ (Nat.succ n ≥ 2 ∧ a ≠ b → B a b c)

State before:
case neg.intro
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
n0 : ¬n = 0
n1 : ¬n = 1
d : point
Hd : online d L ∧ length a d = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b d)
ad : a ≠ d
⊢ ∃ c, online c L ∧ length a c = ↑(Nat.succ n) * length a b ∧ (Nat.succ n ≥ 2 ∧ a ≠ b → B a b c)
Tactic:
obtain ⟨ e, He ⟩ := length_eq_B_of_ne_four ad ab
State after:
case neg.intro.intro
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
n0 : ¬n = 0
n1 : ¬n = 1
d : point
Hd : online d L ∧ length a d = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b d)
ad : a ≠ d
e : point
He : B a d e ∧ length a b = length d e
⊢ ∃ c, online c L ∧ length a c = ↑(Nat.succ n) * length a b ∧ (Nat.succ n ≥ 2 ∧ a ≠ b → B a b c)

State before:
case neg.intro.intro
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
n0 : ¬n = 0
n1 : ¬n = 1
d : point
Hd : online d L ∧ length a d = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b d)
ad : a ≠ d
e : point
He : B a d e ∧ length a b = length d e
⊢ ∃ c, online c L ∧ length a c = ↑(Nat.succ n) * length a b ∧ (Nat.succ n ≥ 2 ∧ a ≠ b → B a b c)
Tactic:
use e
State after:
case neg.intro.intro
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
n0 : ¬n = 0
n1 : ¬n = 1
d : point
Hd : online d L ∧ length a d = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b d)
ad : a ≠ d
e : point
He : B a d e ∧ length a b = length d e
⊢ online e L ∧ length a e = ↑(Nat.succ n) * length a b ∧ (Nat.succ n ≥ 2 ∧ a ≠ b → B a b e)

State before:
case neg.intro.intro
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
n0 : ¬n = 0
n1 : ¬n = 1
d : point
Hd : online d L ∧ length a d = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b d)
ad : a ≠ d
e : point
He : B a d e ∧ length a b = length d e
⊢ online e L ∧ length a e = ↑(Nat.succ n) * length a b ∧ (Nat.succ n ≥ 2 ∧ a ≠ b → B a b e)
Tactic:
rw [← length_sum_of_B He.1, Hd.2.1, He.2]
State after:
case neg.intro.intro
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
n0 : ¬n = 0
n1 : ¬n = 1
d : point
Hd : online d L ∧ length a d = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b d)
ad : a ≠ d
e : point
He : B a d e ∧ length a b = length d e
⊢ online e L ∧ ↑n * length d e + length d e = ↑(Nat.succ n) * length d e ∧ (Nat.succ n ≥ 2 ∧ a ≠ b → B a b e)

State before:
case neg.intro.intro
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
n0 : ¬n = 0
n1 : ¬n = 1
d : point
Hd : online d L ∧ length a d = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b d)
ad : a ≠ d
e : point
He : B a d e ∧ length a b = length d e
⊢ online e L ∧ ↑n * length d e + length d e = ↑(Nat.succ n) * length d e ∧ (Nat.succ n ≥ 2 ∧ a ≠ b → B a b e)
Tactic:
simp
State after:
case neg.intro.intro
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
n0 : ¬n = 0
n1 : ¬n = 1
d : point
Hd : online d L ∧ length a d = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b d)
ad : a ≠ d
e : point
He : B a d e ∧ length a b = length d e
⊢ online e L ∧ ↑n * length d e + length d e = (↑n + 1) * length d e ∧ (2 ≤ Nat.succ n → ¬a = b → B a b e)

State before:
case neg.intro.intro
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
n0 : ¬n = 0
n1 : ¬n = 1
d : point
Hd : online d L ∧ length a d = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b d)
ad : a ≠ d
e : point
He : B a d e ∧ length a b = length d e
⊢ online e L ∧ ↑n * length d e + length d e = (↑n + 1) * length d e ∧ (2 ≤ Nat.succ n → ¬a = b → B a b e)
Tactic:
ring_nf
State after:
case neg.intro.intro
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
n0 : ¬n = 0
n1 : ¬n = 1
d : point
Hd : online d L ∧ length a d = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b d)
ad : a ≠ d
e : point
He : B a d e ∧ length a b = length d e
⊢ online e L ∧ True ∧ (2 ≤ Nat.succ n → ¬a = b → B a b e)

State before:
case neg.intro.intro
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
n0 : ¬n = 0
n1 : ¬n = 1
d : point
Hd : online d L ∧ length a d = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b d)
ad : a ≠ d
e : point
He : B a d e ∧ length a b = length d e
⊢ online e L ∧ True ∧ (2 ≤ Nat.succ n → ¬a = b → B a b e)
Tactic:
have := Hd.2.2 ⟨ ge2_of_n1_n0 n0 n1, ab ⟩
State after:
case neg.intro.intro
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
n0 : ¬n = 0
n1 : ¬n = 1
d : point
Hd : online d L ∧ length a d = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b d)
ad : a ≠ d
e : point
He : B a d e ∧ length a b = length d e
this : B a b d
⊢ online e L ∧ True ∧ (2 ≤ Nat.succ n → ¬a = b → B a b e)

State before:
case neg.intro.intro
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
n0 : ¬n = 0
n1 : ¬n = 1
d : point
Hd : online d L ∧ length a d = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b d)
ad : a ≠ d
e : point
He : B a d e ∧ length a b = length d e
this : B a b d
⊢ online e L ∧ True ∧ (2 ≤ Nat.succ n → ¬a = b → B a b e)
Tactic:
exact ⟨ online_3_of_B He.1 aL Hd.1, (by tauto), fun _ _ => B124_of_B134_B123 He.1 this⟩
State after:
no goals

State before:
case pos
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
hn : ∃ c, online c L ∧ length a c = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b c)
n0 : n = 0
⊢ ∃ c, online c L ∧ length a c = ↑(Nat.succ n) * length a b ∧ (Nat.succ n ≥ 2 ∧ a ≠ b → B a b c)
Tactic:
exact ⟨ b, bL, (by rw [n0]; simp) ⟩
State after:
no goals

State before:
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
hn : ∃ c, online c L ∧ length a c = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b c)
n0 : n = 0
⊢ length a b = ↑(Nat.succ n) * length a b ∧ (Nat.succ n ≥ 2 ∧ a ≠ b → B a b b)
Tactic:
rw [n0]
State after:
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
hn : ∃ c, online c L ∧ length a c = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b c)
n0 : n = 0
⊢ length a b = ↑(Nat.succ 0) * length a b ∧ (Nat.succ 0 ≥ 2 ∧ a ≠ b → B a b b)

State before:
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
hn : ∃ c, online c L ∧ length a c = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b c)
n0 : n = 0
⊢ length a b = ↑(Nat.succ 0) * length a b ∧ (Nat.succ 0 ≥ 2 ∧ a ≠ b → B a b b)
Tactic:
simp
State after:
no goals

State before:
case pos
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
hn : ∃ c, online c L ∧ length a c = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b c)
n0 : ¬n = 0
n1 : n = 1
⊢ ∃ c, online c L ∧ length a c = ↑(Nat.succ n) * length a b ∧ (Nat.succ n ≥ 2 ∧ a ≠ b → B a b c)
Tactic:
obtain ⟨ e, He ⟩ := length_eq_B_of_ne_four ab ab
State after:
case pos.intro
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
hn : ∃ c, online c L ∧ length a c = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b c)
n0 : ¬n = 0
n1 : n = 1
e : point
He : B a b e ∧ length a b = length b e
⊢ ∃ c, online c L ∧ length a c = ↑(Nat.succ n) * length a b ∧ (Nat.succ n ≥ 2 ∧ a ≠ b → B a b c)

State before:
case pos.intro
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
hn : ∃ c, online c L ∧ length a c = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b c)
n0 : ¬n = 0
n1 : n = 1
e : point
He : B a b e ∧ length a b = length b e
⊢ ∃ c, online c L ∧ length a c = ↑(Nat.succ n) * length a b ∧ (Nat.succ n ≥ 2 ∧ a ≠ b → B a b c)
Tactic:
use e
State after:
case pos.intro
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
hn : ∃ c, online c L ∧ length a c = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b c)
n0 : ¬n = 0
n1 : n = 1
e : point
He : B a b e ∧ length a b = length b e
⊢ online e L ∧ length a e = ↑(Nat.succ n) * length a b ∧ (Nat.succ n ≥ 2 ∧ a ≠ b → B a b e)

State before:
case pos.intro
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
hn : ∃ c, online c L ∧ length a c = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b c)
n0 : ¬n = 0
n1 : n = 1
e : point
He : B a b e ∧ length a b = length b e
⊢ online e L ∧ length a e = ↑(Nat.succ n) * length a b ∧ (Nat.succ n ≥ 2 ∧ a ≠ b → B a b e)
Tactic:
simp_rw [(length_sum_of_B He.1).symm, He.2, n1]
State after:
case pos.intro
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
hn : ∃ c, online c L ∧ length a c = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b c)
n0 : ¬n = 0
n1 : n = 1
e : point
He : B a b e ∧ length a b = length b e
⊢ online e L ∧ length b e + length b e = ↑(Nat.succ 1) * length b e ∧ (True ∧ a ≠ b → B a b e)

State before:
case pos.intro
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
hn : ∃ c, online c L ∧ length a c = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b c)
n0 : ¬n = 0
n1 : n = 1
e : point
He : B a b e ∧ length a b = length b e
⊢ online e L ∧ length b e + length b e = ↑(Nat.succ 1) * length b e ∧ (True ∧ a ≠ b → B a b e)
Tactic:
simp
State after:
case pos.intro
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
hn : ∃ c, online c L ∧ length a c = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b c)
n0 : ¬n = 0
n1 : n = 1
e : point
He : B a b e ∧ length a b = length b e
⊢ online e L ∧ length b e + length b e = (1 + 1) * length b e ∧ (¬a = b → B a b e)

State before:
case pos.intro
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
hn : ∃ c, online c L ∧ length a c = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b c)
n0 : ¬n = 0
n1 : n = 1
e : point
He : B a b e ∧ length a b = length b e
⊢ online e L ∧ length b e + length b e = (1 + 1) * length b e ∧ (¬a = b → B a b e)
Tactic:
ring_nf
State after:
case pos.intro
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
hn : ∃ c, online c L ∧ length a c = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b c)
n0 : ¬n = 0
n1 : n = 1
e : point
He : B a b e ∧ length a b = length b e
⊢ online e L ∧ True ∧ (¬a = b → B a b e)

State before:
case pos.intro
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
hn : ∃ c, online c L ∧ length a c = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b c)
n0 : ¬n = 0
n1 : n = 1
e : point
He : B a b e ∧ length a b = length b e
⊢ online e L ∧ True ∧ (¬a = b → B a b e)
Tactic:
refine' ⟨ online_3_of_B He.1 aL bL, (by tauto), fun _ => He.1 ⟩
State after:
no goals

State before:
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
hn : ∃ c, online c L ∧ length a c = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b c)
n0 : ¬n = 0
n1 : n = 1
e : point
He : B a b e ∧ length a b = length b e
⊢ True
Tactic:
tauto
State after:
no goals

State before:
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
n0 : ¬n = 0
n1 : ¬n = 1
d : point
Hd : online d L ∧ length a d = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b d)
⊢ a ≠ d
Tactic:
apply nq_of_len_pos
State after:
case length
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
n0 : ¬n = 0
n1 : ¬n = 1
d : point
Hd : online d L ∧ length a d = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b d)
⊢ 0 < length a d

State before:
case length
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
n0 : ¬n = 0
n1 : ¬n = 1
d : point
Hd : online d L ∧ length a d = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b d)
⊢ 0 < length a d
Tactic:
rw [Hd.2.1]
State after:
case length
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
n0 : ¬n = 0
n1 : ¬n = 1
d : point
Hd : online d L ∧ length a d = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b d)
⊢ 0 < ↑n * length a b

State before:
case length
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
n0 : ¬n = 0
n1 : ¬n = 1
d : point
Hd : online d L ∧ length a d = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b d)
⊢ 0 < ↑n * length a b
Tactic:
simp [Nat.pos_of_ne_zero n0, zero_lt_mul_left, Nat.cast_pos]
State after:
case length
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
n0 : ¬n = 0
n1 : ¬n = 1
d : point
Hd : online d L ∧ length a d = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b d)
⊢ 0 < length a b

State before:
case length
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
n0 : ¬n = 0
n1 : ¬n = 1
d : point
Hd : online d L ∧ length a d = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b d)
⊢ 0 < length a b
Tactic:
exact len_pos_of_nq ab
State after:
no goals

State before:
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
n0 : ¬n = 0
n1 : ¬n = 1
d : point
Hd : online d L ∧ length a d = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b d)
ad : a ≠ d
e : point
He : B a d e ∧ length a b = length d e
this : B a b d
⊢ True
Tactic:
tauto
State after:
no goals