Theorem: area_of_eq (Pythagoras/euclid_I_extras.lean)

State before:
i : incidence_geometry
a b c : point
h : a = b ∨ a = c ∨ b = c
⊢ area a b c = 0
Tactic:
cases h with
| inl ab => rw [ab]; exact degenerate_area b c
| inr h => cases h with
  | inl ac => rw [ac, ar132]; exact degenerate_area c b
  | inr bc => rw [bc, ar321]; exact degenerate_area c a
State after:
no goals

State before:
case inl
i : incidence_geometry
a b c : point
ab : a = b
⊢ area a b c = 0
Tactic:
rw [ab]
State after:
case inl
i : incidence_geometry
a b c : point
ab : a = b
⊢ area b b c = 0

State before:
case inl
i : incidence_geometry
a b c : point
ab : a = b
⊢ area b b c = 0
Tactic:
exact degenerate_area b c
State after:
no goals

State before:
case inr
i : incidence_geometry
a b c : point
h : a = c ∨ b = c
⊢ area a b c = 0
Tactic:
cases h with
| inl ac => rw [ac, ar132]; exact degenerate_area c b
| inr bc => rw [bc, ar321]; exact degenerate_area c a
State after:
no goals

State before:
case inr.inl
i : incidence_geometry
a b c : point
ac : a = c
⊢ area a b c = 0
Tactic:
rw [ac, ar132]
State after:
case inr.inl
i : incidence_geometry
a b c : point
ac : a = c
⊢ area c c b = 0

State before:
case inr.inl
i : incidence_geometry
a b c : point
ac : a = c
⊢ area c c b = 0
Tactic:
exact degenerate_area c b
State after:
no goals

State before:
case inr.inr
i : incidence_geometry
a b c : point
bc : b = c
⊢ area a b c = 0
Tactic:
rw [bc, ar321]
State after:
case inr.inr
i : incidence_geometry
a b c : point
bc : b = c
⊢ area c c a = 0

State before:
case inr.inr
i : incidence_geometry
a b c : point
bc : b = c
⊢ area c c a = 0
Tactic:
exact degenerate_area c a
State after:
no goals