Theorem: B_of_three_online_ne_short (Pythagoras/euclid_I_extras.lean)

State before:
i : incidence_geometry
a b c : point
L : line
hlen : length a b < length a c
ab : a ≠ b
ac : a ≠ c
bc : b ≠ c
aL : online a L
bL : online b L
cL : online c L
⊢ B a b c ∨ B b a c
Tactic:
have := B_of_three_online_ne ab ac bc aL bL cL
State after:
i : incidence_geometry
a b c : point
L : line
hlen : length a b < length a c
ab : a ≠ b
ac : a ≠ c
bc : b ≠ c
aL : online a L
bL : online b L
cL : online c L
this : B a b c ∨ B b a c ∨ B a c b
⊢ B a b c ∨ B b a c

State before:
i : incidence_geometry
a b c : point
L : line
hlen : length a b < length a c
ab : a ≠ b
ac : a ≠ c
bc : b ≠ c
aL : online a L
bL : online b L
cL : online c L
this : B a b c ∨ B b a c ∨ B a c b
⊢ B a b c ∨ B b a c
Tactic:
convert this
State after:
case h.e'_2.a
i : incidence_geometry
a b c : point
L : line
hlen : length a b < length a c
ab : a ≠ b
ac : a ≠ c
bc : b ≠ c
aL : online a L
bL : online b L
cL : online c L
this : B a b c ∨ B b a c ∨ B a c b
⊢ B b a c ↔ B b a c ∨ B a c b

State before:
case h.e'_2.a
i : incidence_geometry
a b c : point
L : line
hlen : length a b < length a c
ab : a ≠ b
ac : a ≠ c
bc : b ≠ c
aL : online a L
bL : online b L
cL : online c L
this : B a b c ∨ B b a c ∨ B a c b
⊢ B b a c ↔ B b a c ∨ B a c b
Tactic:
simp [not_B_of_short hlen]
State after:
no goals