import Mathlib.Tactic
import Mathlib.Data.Real.Basic
import Mathlib.Tactic

universe u1 u2 u3

-- See Help.lean for a full list of tactics

/-

  The following follows Lean series on writing tactics

  https://www.vladasedlacek.cz/en/posts/lean-02-demo

-/

class incidence_geometry: Type (max (max (u1 + 1) (u2 + 1)) (u3 + 1))
incidence_geometryWarning: `incidence_geometry`: universes `u1`, `u2`, `u3` only occur together. This usually means there is a `max` expression in the type where none of these universes appear on their own.

Note: This linter can be disabled with `set_option linter.checkUnivs false` :=Warning: `incidence_geometry`: universes `u1`, `u2`, `u3` only occur together. This usually means there is a `max` expression in the type where none of these universes appear on their own.

Note: This linter can be disabled with `set_option linter.checkUnivs false`
Warning: `class ... :=` has been deprecated in favor of `class ... where`.

Note: This linter can be disabled with `set_option linter.deprecated false`
(point: [self : incidence_geometry] → Type u1
point : Type u1: Type (u1 + 1)
Type u1)
(line: [self : incidence_geometry] → Type u2
line : Type u2: Type (u2 + 1)
Type u2)
(circle: [self : incidence_geometry] → Type u3
circle : Type u3: Type (u3 + 1)
Type u3)

(length: [self : incidence_geometry] → incidence_geometry.point → incidence_geometry.point → ℝ
length : point: Type u1
point → point: Type u1
point → ℝ: Type
ℝ)
(B: [self : incidence_geometry] → incidence_geometry.point → incidence_geometry.point → incidence_geometry.point → Prop
B : point: Type u1
point → point: Type u1
point → point: Type u1
point → Prop: Type
Prop) -- Betweenness

(length_nonneg: ∀ [self : incidence_geometry] (a b : incidence_geometry.point), 0 ≤ incidence_geometry.length a b
length_nonneg : ∀ (a: point
a b: point
b : point: Type u1
point), 0: ℝ
0 ≤ length: point → point → ℝ
length a: point
a b: point
b)
(length_symm: ∀ [self : incidence_geometry] (a b : incidence_geometry.point),
  incidence_geometry.length a b = incidence_geometry.length b a
length_symm : ∀ (a: point
a b: point
b : point: Type u1
point), length: point → point → ℝ
length a: point
a b: point
b = length: point → point → ℝ
length b: point
b a: point
a)
(length_eq_zero_iff: ∀ [self : incidence_geometry] {a b : incidence_geometry.point}, incidence_geometry.length a b = 0 ↔ a = b
length_eq_zero_iff : ∀ {a: point
a b: point
b : point: Type u1
point}, length: point → point → ℝ
length a: point
a b: point
b = 0: ℝ
0 ↔ a: point
a = b: point
b)
(length_sum_of_B: ∀ [self : incidence_geometry] {a b c : incidence_geometry.point},
  incidence_geometry.B a b c →
    incidence_geometry.length a b + incidence_geometry.length b c = incidence_geometry.length a c
length_sum_of_B : ∀ {a: point
a b: point
b c: point
c : point: Type u1
point},
   B: point → point → point → Prop
B a: point
a b: point
b c: point
c → length: point → point → ℝ
length a: point
a b: point
b + length: point → point → ℝ
length b: point
b c: point
c = length: point → point → ℝ
length a: point
a c: point
c)
(ne_12_of_B: ∀ [self : incidence_geometry] {a b c : incidence_geometry.point}, incidence_geometry.B a b c → a ≠ b
ne_12_of_B : ∀ {a: point
a b: point
b c: point
c : point: Type u1
point}, B: point → point → point → Prop
B a: point
a b: point
b c: point
c → a: point
a ≠ b: point
b )
(ne_13_of_B: ∀ [self : incidence_geometry] {a b c : incidence_geometry.point}, incidence_geometry.B a b c → a ≠ c
ne_13_of_B : ∀ {a: point
a b: point
b c: point
c : point: Type u1
point}, B: point → point → point → Prop
B a: point
a b: point
b c: point
c → a: point
a ≠ c: point
c )
(ne_23_of_B: ∀ [self : incidence_geometry] {a b c : incidence_geometry.point}, incidence_geometry.B a b c → b ≠ c
ne_23_of_B : ∀ {a: point
a b: point
b c: point
c : point: Type u1
point}, B: point → point → point → Prop
B a: point
a b: point
b c: point
c → b: point
b ≠ c: point
c )Warning: `incidence_geometry`: universes `u1`, `u2`, `u3` only occur together. This usually means there is a `max` expression in the type where none of these universes appear on their own.

Note: This linter can be disabled with `set_option linter.checkUnivs false`

variable [i: incidence_geometry
i : incidence_geometry: Type (max (max (u_1 + 1) (u_2 + 1)) (u_3 + 1))
incidence_geometry]
open incidence_geometry

lemma len_pos_of_neq₁: ∀ {a b : point}, a ≠ b → 0 < length a b
len_pos_of_neq₁ (ab: a ≠ b
ab : a: point
a ≠ b: point
b) : 0: ℝ
0 < length: [self : incidence_geometry] → point → point → ℝ
length a: point
a b: point
b := byGoals accomplished! 🐙
  have h₁: length a b ≠ 0
h₁ : length: [self : incidence_geometry] → point → point → ℝ
length a: point
a b: point
b ≠ 0: ℝ
0 :=i: incidence_geometry
a, b: point
ab: a ≠ b
0 < length a b byGoals accomplished! 🐙
    by_contra h: length a b = 0
hi: incidence_geometry
a, b: point
ab: a ≠ b
h: length a b = 0
False
    rw [i: incidence_geometry
a, b: point
ab: a ≠ b
h: length a b = 0
Falselength_eq_zero_iff: ∀ [self : incidence_geometry] {a b : point}, length a b = 0 ↔ a = b
length_eq_zero_iffi: incidence_geometry
a, b: point
ab: a ≠ b
h: a = b
False]i: incidence_geometry
a, b: point
ab: a ≠ b
h: a = b
False at h: length a b = 0
hi: incidence_geometry
a, b: point
ab: a ≠ b
h: a = b
False
    exact (absurd: ∀ {a b : Prop}, a → ¬a → b
absurd h: a = b
h ab: a ≠ b
ab)Goals accomplished! 🐙
  have h₂: 0 ≤ length a b
h₂ : 0: ℝ
0 ≤ length: [self : incidence_geometry] → point → point → ℝ
length a: point
a b: point
b := length_nonneg: ∀ [self : incidence_geometry] (a b : point), 0 ≤ length a b
length_nonneg a: point
a b: point
bi: incidence_geometry
a, b: point
ab: a ≠ b
h₁:= id fun h => absurd (Eq.mp (congrArg (fun _a => _a) (propext length_eq_zero_iff)) h) ab: length a b ≠ 0
h₂:= length_nonneg a b: 0 ≤ length a b
0 < length a b
  exact lt_of_le_of_ne: ∀ {α : Type} [inst : PartialOrder α] {a b : α}, a ≤ b → a ≠ b → a < b
lt_of_le_of_ne h₂: 0 ≤ length a b
h₂ h₁: length a b ≠ 0
h₁.symm: ∀ {α : Type} {a b : α}, a ≠ b → b ≠ a
symmGoals accomplished! 🐙

-- #find |- ?a ≠ ?b

lemma len_pos_of_neq₂ (ab : a ≠ b) : 0 < length a b := byGoals accomplished! 🐙
  have h1: length a b ≠ 0
h1 : length: [self : incidence_geometry] → point → point → ℝ
length a: point
a b: point
b ≠ 0: ℝ
0 := length_eq_zero_iff: ∀ [self : incidence_geometry] {a b : point}, length a b = 0 ↔ a = b
length_eq_zero_iff.not: ∀ {a b : Prop}, (a ↔ b) → (¬a ↔ ¬b)
not.mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr ab: a ≠ b
abi: incidence_geometry
a, b: point
ab: a ≠ b
h1:= (Iff.not length_eq_zero_iff).mpr ab: length a b ≠ 0
0 < length a b
  have h2: 0 ≤ length a b
h2 := length_nonneg: ∀ [self : incidence_geometry] (a b : point), 0 ≤ length a b
length_nonneg a: point
a b: point
bi: incidence_geometry
a, b: point
ab: a ≠ b
h1:= (Iff.not length_eq_zero_iff).mpr ab: length a b ≠ 0
h2:= length_nonneg a b: 0 ≤ length a b
0 < length a b
  exact lt_of_le_of_ne: ∀ {α : Type} [inst : PartialOrder α] {a b : α}, a ≤ b → a ≠ b → a < b
lt_of_le_of_ne h2: 0 ≤ length a b
h2 h1: length a b ≠ 0
h1.symm: ∀ {α : Type} {a b : α}, a ≠ b → b ≠ a
symmGoals accomplished! 🐙

lemma len_pos_of_neq₃: ∀ {a b : point}, a ≠ b → 0 < length a b
len_pos_of_neq₃ (ab: a ≠ b
ab : a: point
a ≠ b: point
b) : 0: ℝ
0 < length: [self : incidence_geometry] → point → point → ℝ
length a: point
a b: point
b := byGoals accomplished! 🐙
  have h1: length a b ≠ 0
h1 : length: [self : incidence_geometry] → point → point → ℝ
length a: point
a b: point
b ≠ 0: ℝ
0 := length_eq_zero_iff: ∀ [self : incidence_geometry] {a b : point}, length a b = 0 ↔ a = b
length_eq_zero_iff.not: ∀ {a b : Prop}, (a ↔ b) → (¬a ↔ ¬b)
not.mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr ab: a ≠ b
abi: incidence_geometry
a, b: point
ab: a ≠ b
h1:= (Iff.not length_eq_zero_iff).mpr ab: length a b ≠ 0
0 < length a b
  have h2: 0 ≤ length a b
h2 := length_nonneg: ∀ [self : incidence_geometry] (a b : point), 0 ≤ length a b
length_nonneg a: point
a b: point
bi: incidence_geometry
a, b: point
ab: a ≠ b
h1:= (Iff.not length_eq_zero_iff).mpr ab: length a b ≠ 0
h2:= length_nonneg a b: 0 ≤ length a b
0 < length a b
  exact lt_of_le_of_ne: ∀ {α : Type} [inst : PartialOrder α] {a b : α}, a ≤ b → a ≠ b → a < b
lt_of_le_of_ne h2: 0 ≤ length a b
h2 h1: length a b ≠ 0
h1.symm: ∀ {α : Type} {a b : α}, a ≠ b → b ≠ a
symmGoals accomplished! 🐙

lemma len_pos_of_neq₄: ∀ {a b : point}, a ≠ b → 0 < length a b
len_pos_of_neq₄ (ab: a ≠ b
ab : a: point
a ≠ b: point
b) : 0: ℝ
0 < length: [self : incidence_geometry] → point → point → ℝ
length a: point
a b: point
b := byGoals accomplished! 🐙
  have h1: length a b ≠ 0
h1 : length: [self : incidence_geometry] → point → point → ℝ
length a: point
a b: point
b ≠ 0: ℝ
0 := length_eq_zero_iff: ∀ [self : incidence_geometry] {a b : point}, length a b = 0 ↔ a = b
length_eq_zero_iff.not: ∀ {a b : Prop}, (a ↔ b) → (¬a ↔ ¬b)
not.mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr ab: a ≠ b
abi: incidence_geometry
a, b: point
ab: a ≠ b
h1:= (Iff.not length_eq_zero_iff).mpr ab: length a b ≠ 0
0 < length a b
  have h2: 0 ≤ length a b
h2 := length_nonneg: ∀ [self : incidence_geometry] (a b : point), 0 ≤ length a b
length_nonneg a: point
a b: point
bi: incidence_geometry
a, b: point
ab: a ≠ b
h1:= (Iff.not length_eq_zero_iff).mpr ab: length a b ≠ 0
h2:= length_nonneg a b: 0 ≤ length a b
0 < length a b
  exact lt_of_le_of_ne: ∀ {α : Type} [inst : PartialOrder α] {a b : α}, a ≤ b → a ≠ b → a < b
lt_of_le_of_ne h2: 0 ≤ length a b
h2 h1: length a b ≠ 0
h1.symm: ∀ {α : Type} {a b : α}, a ≠ b → b ≠ a
symmGoals accomplished! 🐙

lemma len_pos_of_neq: ∀ [i : incidence_geometry] {a b : point}, a ≠ b → 0 < length a b
len_pos_of_neq (ab: a ≠ b
ab : a: point
a ≠ b: point
b) : 0: ℝ
0 < length: [self : incidence_geometry] → point → point → ℝ
length a: point
a b: point
b := len_pos_of_neq₂: ∀ [i : incidence_geometry] {a b : point}, a ≠ b → 0 < length a b
len_pos_of_neq₂ ab: a ≠ b
ab

theorem length_sum_perm_of_B₁: ∀ {a b c : point}, B a b c → 0 < length a b ∧ 0 < length b a
length_sum_perm_of_B₁ (Babc: B a b c
Babc : B: [self : incidence_geometry] → point → point → point → Prop
B a: point
a b: point
b c: point
c) :
      0: ℝ
0 < length: [self : incidence_geometry] → point → point → ℝ
length a: point
a b: point
b ∧ 0: ℝ
0 < length: [self : incidence_geometry] → point → point → ℝ
length b: point
b a: point
a := byGoals accomplished! 🐙
    have ab: a ≠ b
ab : a: point
a ≠ b: point
b := ne_12_of_B: ∀ [self : incidence_geometry] {a b c : point}, B a b c → a ≠ b
ne_12_of_B Babc: B a b c
Babci: incidence_geometry
a, b, c: point
Babc: B a b c
ab:= ne_12_of_B Babc: a ≠ b
0 < length a b ∧ 0 < length b a
    have ab_pos: 0 < length a b
ab_pos : 0: ℝ
0 < length: [self : incidence_geometry] → point → point → ℝ
length a: point
a b: point
b := len_pos_of_neq: ∀ [i : incidence_geometry] {a b : point}, a ≠ b → 0 < length a b
len_pos_of_neq ab: a ≠ b
abi: incidence_geometry
a, b, c: point
Babc: B a b c
ab:= ne_12_of_B Babc: a ≠ b
ab_pos:= len_pos_of_neq ab: 0 < length a b
0 < length a b ∧ 0 < length b a
    constructori: incidence_geometry
a, b, c: point
Babc: B a b c
ab:= ne_12_of_B Babc: a ≠ b
ab_pos:= len_pos_of_neq ab: 0 < length a b
left0 < length a b
i: incidence_geometry
a, b, c: point
Babc: B a b c
ab:= ne_12_of_B Babc: a ≠ b
ab_pos:= len_pos_of_neq ab: 0 < length a b
right0 < length b a
    .i: incidence_geometry
a, b, c: point
Babc: B a b c
ab:= ne_12_of_B Babc: a ≠ b
ab_pos:= len_pos_of_neq ab: 0 < length a b
left0 < length a b exact ab_pos: 0 < length a b
ab_posGoals accomplished! 🐙
    .i: incidence_geometry
a, b, c: point
Babc: B a b c
ab:= ne_12_of_B Babc: a ≠ b
ab_pos:= len_pos_of_neq ab: 0 < length a b
right0 < length b a rw [i: incidence_geometry
a, b, c: point
Babc: B a b c
ab:= ne_12_of_B Babc: a ≠ b
ab_pos:= len_pos_of_neq ab: 0 < length a b
right0 < length b alength_symm: ∀ [self : incidence_geometry] (a b : point), length a b = length b a
length_symmi: incidence_geometry
a, b, c: point
Babc: B a b c
ab:= ne_12_of_B Babc: a ≠ b
ab_pos: 0 < length b a
right0 < length b a]i: incidence_geometry
a, b, c: point
Babc: B a b c
ab:= ne_12_of_B Babc: a ≠ b
ab_pos: 0 < length b a
right0 < length b a at ab_pos: 0 < length a b
ab_posi: incidence_geometry
a, b, c: point
Babc: B a b c
ab:= ne_12_of_B Babc: a ≠ b
ab_pos: 0 < length b a
right0 < length b a
      exact ab_pos: 0 < length b a
ab_posGoals accomplished! 🐙

theorem length_sum_perm_of_B₂: ∀ {a b c : point}, B a b c → 0 < length a b ∧ 0 < length b a
length_sum_perm_of_B₂ (Babc: B a b c
Babc : B: [self : incidence_geometry] → point → point → point → Prop
B a: point
a b: point
b c: point
c) :
      0: ℝ
0 < length: [self : incidence_geometry] → point → point → ℝ
length a: point
a b: point
b ∧ 0: ℝ
0 < length: [self : incidence_geometry] → point → point → ℝ
length b: point
b a: point
a := byGoals accomplished! 🐙
      constructori: incidence_geometry
a, b, c: point
Babc: B a b c
left0 < length a b
i: incidence_geometry
a, b, c: point
Babc: B a b c
right0 < length b a
      .i: incidence_geometry
a, b, c: point
Babc: B a b c
left0 < length a b exact ne_12_of_B: ∀ [self : incidence_geometry] {a b c : point}, B a b c → a ≠ b
ne_12_of_B Babc: B a b c
Babc |> len_pos_of_neq: ∀ [i : incidence_geometry] {a b : point}, a ≠ b → 0 < length a b
len_pos_of_neqGoals accomplished! 🐙
      .i: incidence_geometry
a, b, c: point
Babc: B a b c
right0 < length b a exact ne_12_of_B: ∀ [self : incidence_geometry] {a b c : point}, B a b c → a ≠ b
ne_12_of_B Babc: B a b c
Babc |> (length_symm: ∀ [self : incidence_geometry] (a b : point), length a b = length b a
length_symm a: point
a b: point
b ▸ len_pos_of_neq: ∀ [i : incidence_geometry] {a b : point}, a ≠ b → 0 < length a b
len_pos_of_neq)Goals accomplished! 🐙

theorem length_sum_perm_of_B₃: ∀ [i : incidence_geometry] {a b c : point}, B a b c → 0 < length a b ∧ 0 < length b a
length_sum_perm_of_B₃ (Babc: B a b c
Babc : B: [self : incidence_geometry] → point → point → point → Prop
B a: point
a b: point
b c: point
c) : 0: ℝ
0 < length: [self : incidence_geometry] → point → point → ℝ
length a: point
a b: point
b ∧ 0: ℝ
0 < length: [self : incidence_geometry] → point → point → ℝ
length b: point
b a: point
a := byGoals accomplished! 🐙
   simp only [i: incidence_geometry
a, b, c: point
Babc: B a b c
0 < length a b ∧ 0 < length b ane_eq: ∀ {α : Sort ?u.25} (a b : α), (a ≠ b) = ¬a = b
ne_eqWarning: This simp argument is unused:
  ne_eq

Hint: Omit it from the simp argument list.
  simp only [ne_e̵q̵,̵ ̵n̵e̵_̵12_of_B Babc, len_pos_of_neq, length_symm, and_self]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
i: incidence_geometry
a, b, c: point
Babc: B a b c
0 < length a b ∧ 0 < length b a,i: incidence_geometry
a, b, c: point
Babc: B a b c
0 < length a b ∧ 0 < length b a ne_12_of_B: ∀ [self : incidence_geometry] {a b c : point}, B a b c → a ≠ b
ne_12_of_B Babc: B a b c
BabcWarning: This simp argument is unused:
  ne_12_of_B Babc

Hint: Omit it from the simp argument list.
  simp only [ne_eq, n̵e̵_̵1̵2̵_̵o̵f̵_̵B̵ ̵B̵a̵b̵c̵,̵ ̵len_pos_of_neq, length_symm, and_self]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
i: incidence_geometry
a, b, c: point
Babc: B a b c
0 < length a b ∧ 0 < length b a,i: incidence_geometry
a, b, c: point
Babc: B a b c
0 < length a b ∧ 0 < length b a len_pos_of_neq: ∀ [i : incidence_geometry] {a b : point}, a ≠ b → 0 < length a b
len_pos_of_neqWarning: This simp argument is unused:
  len_pos_of_neq

Hint: Omit it from the simp argument list.
  simp only [ne_eq, ne_12_of_B Babc, len_̵p̵o̵s̵_̵o̵f̵_̵n̵e̵q̵,̵ ̵l̵e̵n̵gth_symm, and_self]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
i: incidence_geometry
a, b, c: point
Babc: B a b c
0 < length a b ∧ 0 < length b a, length_symm: ∀ [self : incidence_geometry] (a b : point), length a b = length b a
length_symm, and_self: ∀ (p : Prop), (p ∧ p) = p
and_self]i: incidence_geometry
a, b, c: point
Babc: B a b c
0 < length a b
   exact len_pos_of_neq: ∀ [i : incidence_geometry] {a b : point}, a ≠ b → 0 < length a b
len_pos_of_neq (ne_12_of_B: ∀ [self : incidence_geometry] {a b c : point}, B a b c → a ≠ b
ne_12_of_B Babc: B a b c
Babc)Goals accomplished! 🐙