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_geometry :=
(
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 )

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₁: ∀ [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 := by
Goals 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 by
Goals accomplished! 🐙
    by_contra 
h: length a b = 0
h
i: 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
False
length_eq_zero_iff: ∀ [self : incidence_geometry] {a b : point}, length a b = 0 ↔ a = b
length_eq_zero_iff
i: 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
h
i: 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
b
i: incidence_geometry
a, b: point
ab: a ≠ b
h₁: length a b ≠ 0
h₂: 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
symm
Goals accomplished! 🐙

-- #find |- ?a ≠ ?b

lemma len_pos_of_neq₂ (ab : a ≠ b) : 0 < length a b := by
Goals 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
ab
i: incidence_geometry
a, b: point
ab: a ≠ b
h1: 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
b
i: incidence_geometry
a, b: point
ab: a ≠ b
h1: length a b ≠ 0
h2: 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
symm
Goals 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 := by
Goals 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
ab
i: incidence_geometry
a, b: point
ab: a ≠ b
h1: 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
b
i: incidence_geometry
a, b: point
ab: a ≠ b
h1: length a b ≠ 0
h2: 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
symm
Goals 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 := by
Goals 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
ab
i: incidence_geometry
a, b: point
ab: a ≠ b
h1: 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
b
i: incidence_geometry
a, b: point
ab: a ≠ b
h1: length a b ≠ 0
h2: 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
symm
Goals 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 := by
Goals 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
Babc
i: incidence_geometry
a, b, c: point
Babc: B a b c
ab: 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
ab
i: incidence_geometry
a, b, c: point
Babc: B a b c
ab: a ≠ b
ab_pos: 0 < length a b
0 < length a b ∧ 0 < length b a
    constructor
i: incidence_geometry
a, b, c: point
Babc: B a b c
ab: a ≠ b
ab_pos: 0 < length a b
left
0 < length a b
i: incidence_geometry
a, b, c: point
Babc: B a b c
ab: a ≠ b
ab_pos: 0 < length a b
right
0 < length b a
    .
i: incidence_geometry
a, b, c: point
Babc: B a b c
ab: a ≠ b
ab_pos: 0 < length a b
left
0 < length a b exact 
ab_pos: 0 < length a b
ab_pos
Goals accomplished! 🐙
    .
i: incidence_geometry
a, b, c: point
Babc: B a b c
ab: a ≠ b
ab_pos: 0 < length a b
right
0 < length b a rw [
i: incidence_geometry
a, b, c: point
Babc: B a b c
ab: a ≠ b
ab_pos: 0 < length a b
right
0 < length b a
length_symm: ∀ [self : incidence_geometry] (a b : point), length a b = length b a
length_symm
i: incidence_geometry
a, b, c: point
Babc: B a b c
ab: a ≠ b
ab_pos: 0 < length b a
right
0 < length b a]
i: incidence_geometry
a, b, c: point
Babc: B a b c
ab: a ≠ b
ab_pos: 0 < length b a
right
0 < length b a at 
ab_pos: 0 < length a b
ab_pos
i: incidence_geometry
a, b, c: point
Babc: B a b c
ab: a ≠ b
ab_pos: 0 < length b a
right
0 < length b a
      exact 
ab_pos: 0 < length b a
ab_pos
Goals 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 := by
Goals accomplished! 🐙
      constructor
i: incidence_geometry
a, b, c: point
Babc: B a b c
left
0 < length a b
i: incidence_geometry
a, b, c: point
Babc: B a b c
right
0 < length b a
      .
i: incidence_geometry
a, b, c: point
Babc: B a b c
left
0 < 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_neq
Goals accomplished! 🐙
      .
i: incidence_geometry
a, b, c: point
Babc: B a b c
right
0 < 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₃: ∀ {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 := by
Goals accomplished! 🐙
   simp only [
ne_eq: ∀ {α : Sort ?u.2314} (a b : α), (a ≠ b) = ¬a = b
ne_eq, 
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_neq, 
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! 🐙