Theorem: lt_area_of_lt_base (Pythagoras/euclid_VI.lean)

State before:
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
⊢ length b c > length e f → area a b c > area d e f
Tactic:
intro hlen
State after:
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
⊢ area a b c > area d e f

State before:
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
⊢ area a b c > area d e f
Tactic:
have bc : b ≠ c := fun bc => by
  rw [length_eq_zero_iff.mpr bc] at hlen
  exact (not_le_of_gt hlen) (length_nonneg e f)
State after:
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
⊢ area a b c > area d e f

State before:
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
⊢ area a b c > area d e f
Tactic:
have aL := offline_of_para aM (para_symm pLM)
State after:
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
⊢ area a b c > area d e f

State before:
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
⊢ area a b c > area d e f
Tactic:
have dL := offline_of_para dM (para_symm pLM)
State after:
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
⊢ area a b c > area d e f

State before:
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
⊢ area a b c > area d e f
Tactic:
by_cases ef: e = f
State after:
case pos
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : e = f
⊢ area a b c > area d e f

case neg
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
⊢ area a b c > area d e f

State before:
case neg
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
⊢ area a b c > area d e f
Tactic:
obtain ⟨ O, dO, eO ⟩ := line_of_pts d e
State after:
case neg.intro.intro
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
⊢ area a b c > area d e f

State before:
case neg.intro.intro
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
⊢ area a b c > area d e f
Tactic:
have := not_online_of_triangle dO eO eL fL dL ef
State after:
case neg.intro.intro
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
this : ¬online f O
⊢ area a b c > area d e f

State before:
case neg.intro.intro
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
this : ¬online f O
⊢ area a b c > area d e f
Tactic:
obtain ⟨ g, N, gM, gN, fN, pON ⟩ := parallel_projection fL pLM (not_para_of_online_online eO eL) this
State after:
case neg.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
this : ¬online f O
g : point
N : line
gM : online g M
gN : online g N
fN : online f N
pON : para O N
⊢ area a b c > area d e f

State before:
case neg.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
this : ¬online f O
g : point
N : line
gM : online g M
gN : online g N
fN : online f N
pON : para O N
⊢ area a b c > area d e f
Tactic:
have efgd : paragram e f g d L N M O := by splitAll <;> perma only [para] at *
State after:
case neg.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
this : ¬online f O
g : point
N : line
gM : online g M
gN : online g N
fN : online f N
pON : para O N
efgd : paragram e f g d L N M O
⊢ area a b c > area d e f

State before:
case neg.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
this : ¬online f O
g : point
N : line
gM : online g M
gN : online g N
fN : online f N
pON : para O N
efgd : paragram e f g d L N M O
⊢ area a b c > area d e f
Tactic:
perm [(len_ang_area_eq_of_parallelogram efgd).1]
State after:
case neg.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
this✝ : ¬online f O
g : point
N : line
gM : online g M
gN : online g N
fN : online f N
pON : para O N
efgd : paragram e f g d L N M O
this : length e f = length d g
⊢ area a b c > area d e f

State before:
case neg.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
this✝ : ¬online f O
g : point
N : line
gM : online g M
gN : online g N
fN : online f N
pON : para O N
efgd : paragram e f g d L N M O
this : length e f = length d g
⊢ area a b c > area d e f
Tactic:
have dg : d ≠ g := ne_of_ne_len ef this
State after:
case neg.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
this✝ : ¬online f O
g : point
N : line
gM : online g M
gN : online g N
fN : online f N
pON : para O N
efgd : paragram e f g d L N M O
this : length e f = length d g
dg : d ≠ g
⊢ area a b c > area d e f

State before:
case neg.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
this✝ : ¬online f O
g : point
N : line
gM : online g M
gN : online g N
fN : online f N
pON : para O N
efgd : paragram e f g d L N M O
this : length e f = length d g
dg : d ≠ g
⊢ area a b c > area d e f
Tactic:
obtain ⟨ P, bP, dP ⟩ := line_of_pts b d
State after:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
this✝ : ¬online f O
g : point
N : line
gM : online g M
gN : online g N
fN : online f N
pON : para O N
efgd : paragram e f g d L N M O
this : length e f = length d g
dg : d ≠ g
P : line
bP : online b P
dP : online d P
⊢ area a b c > area d e f

State before:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
this✝ : ¬online f O
g : point
N : line
gM : online g M
gN : online g N
fN : online f N
pON : para O N
efgd : paragram e f g d L N M O
this : length e f = length d g
dg : d ≠ g
P : line
bP : online b P
dP : online d P
⊢ area a b c > area d e f
Tactic:
have := not_online_of_triangle bP dP dM gM (offline_of_para bL pLM) dg
State after:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
this✝¹ : ¬online f O
g : point
N : line
gM : online g M
gN : online g N
fN : online f N
pON : para O N
efgd : paragram e f g d L N M O
this✝ : length e f = length d g
dg : d ≠ g
P : line
bP : online b P
dP : online d P
this : ¬online g P
⊢ area a b c > area d e f

State before:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
this✝¹ : ¬online f O
g : point
N : line
gM : online g M
gN : online g N
fN : online f N
pON : para O N
efgd : paragram e f g d L N M O
this✝ : length e f = length d g
dg : d ≠ g
P : line
bP : online b P
dP : online d P
this : ¬online g P
⊢ area a b c > area d e f
Tactic:
obtain ⟨ h, R, hL, hR, gR, pPR ⟩ := parallel_projection gM (para_symm pLM) (not_para_of_online_online dP dM) this
State after:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
this✝¹ : ¬online f O
g : point
N : line
gM : online g M
gN : online g N
fN : online f N
pON : para O N
efgd : paragram e f g d L N M O
this✝ : length e f = length d g
dg : d ≠ g
P : line
bP : online b P
dP : online d P
this : ¬online g P
h : point
R : line
hL : online h L
hR : online h R
gR : online g R
pPR : para P R
⊢ area a b c > area d e f

State before:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
this✝¹ : ¬online f O
g : point
N : line
gM : online g M
gN : online g N
fN : online f N
pON : para O N
efgd : paragram e f g d L N M O
this✝ : length e f = length d g
dg : d ≠ g
P : line
bP : online b P
dP : online d P
this : ¬online g P
h : point
R : line
hL : online h L
hR : online h R
gR : online g R
pPR : para P R
⊢ area a b c > area d e f
Tactic:
have bhgd : paragram b h g d L R M P := by splitAll <;> perma only [para]
State after:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
this✝¹ : ¬online f O
g : point
N : line
gM : online g M
gN : online g N
fN : online f N
pON : para O N
efgd : paragram e f g d L N M O
this✝ : length e f = length d g
dg : d ≠ g
P : line
bP : online b P
dP : online d P
this : ¬online g P
h : point
R : line
hL : online h L
hR : online h R
gR : online g R
pPR : para P R
bhgd : paragram b h g d L R M P
⊢ area a b c > area d e f

State before:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
this✝¹ : ¬online f O
g : point
N : line
gM : online g M
gN : online g N
fN : online f N
pON : para O N
efgd : paragram e f g d L N M O
this✝ : length e f = length d g
dg : d ≠ g
P : line
bP : online b P
dP : online d P
this : ¬online g P
h : point
R : line
hL : online h L
hR : online h R
gR : online g R
pPR : para P R
bhgd : paragram b h g d L R M P
⊢ area a b c > area d e f
Tactic:
have ef_bh : length e f = length b h := by linperm [(len_ang_area_eq_of_parallelogram bhgd).1]
State after:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
this✝¹ : ¬online f O
g : point
N : line
gM : online g M
gN : online g N
fN : online f N
pON : para O N
efgd : paragram e f g d L N M O
this✝ : length e f = length d g
dg : d ≠ g
P : line
bP : online b P
dP : online d P
this : ¬online g P
h : point
R : line
hL : online h L
hR : online h R
gR : online g R
pPR : para P R
bhgd : paragram b h g d L R M P
ef_bh : length e f = length b h
⊢ area a b c > area d e f

State before:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
this✝¹ : ¬online f O
g : point
N : line
gM : online g M
gN : online g N
fN : online f N
pON : para O N
efgd : paragram e f g d L N M O
this✝ : length e f = length d g
dg : d ≠ g
P : line
bP : online b P
dP : online d P
this : ¬online g P
h : point
R : line
hL : online h L
hR : online h R
gR : online g R
pPR : para P R
bhgd : paragram b h g d L R M P
ef_bh : length e f = length b h
⊢ area a b c > area d e f
Tactic:
have bh : b ≠ h := ne_of_ne_len ef ef_bh
State after:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
this✝¹ : ¬online f O
g : point
N : line
gM : online g M
gN : online g N
fN : online f N
pON : para O N
efgd : paragram e f g d L N M O
this✝ : length e f = length d g
dg : d ≠ g
P : line
bP : online b P
dP : online d P
this : ¬online g P
h : point
R : line
hL : online h L
hR : online h R
gR : online g R
pPR : para P R
bhgd : paragram b h g d L R M P
ef_bh : length e f = length b h
bh : b ≠ h
⊢ area a b c > area d e f

State before:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
this✝¹ : ¬online f O
g : point
N : line
gM : online g M
gN : online g N
fN : online f N
pON : para O N
efgd : paragram e f g d L N M O
this✝ : length e f = length d g
dg : d ≠ g
P : line
bP : online b P
dP : online d P
this : ¬online g P
h : point
R : line
hL : online h L
hR : online h R
gR : online g R
pPR : para P R
bhgd : paragram b h g d L R M P
ef_bh : length e f = length b h
bh : b ≠ h
⊢ area a b c > area d e f
Tactic:
rw [eq_area_of_eq_base dM eL fL aM bL hL pLM ef_bh]
State after:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
this✝¹ : ¬online f O
g : point
N : line
gM : online g M
gN : online g N
fN : online f N
pON : para O N
efgd : paragram e f g d L N M O
this✝ : length e f = length d g
dg : d ≠ g
P : line
bP : online b P
dP : online d P
this : ¬online g P
h : point
R : line
hL : online h L
hR : online h R
gR : online g R
pPR : para P R
bhgd : paragram b h g d L R M P
ef_bh : length e f = length b h
bh : b ≠ h
⊢ area a b c > area a b h

State before:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
this✝¹ : ¬online f O
g : point
N : line
gM : online g M
gN : online g N
fN : online f N
pON : para O N
efgd : paragram e f g d L N M O
this✝ : length e f = length d g
dg : d ≠ g
P : line
bP : online b P
dP : online d P
this : ¬online g P
h : point
R : line
hL : online h L
hR : online h R
gR : online g R
pPR : para P R
bhgd : paragram b h g d L R M P
ef_bh : length e f = length b h
bh : b ≠ h
⊢ area a b c > area a b h
Tactic:
have : length b c > length b h := by rw [← ef_bh]; exact hlen
State after:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
this✝² : ¬online f O
g : point
N : line
gM : online g M
gN : online g N
fN : online f N
pON : para O N
efgd : paragram e f g d L N M O
this✝¹ : length e f = length d g
dg : d ≠ g
P : line
bP : online b P
dP : online d P
this✝ : ¬online g P
h : point
R : line
hL : online h L
hR : online h R
gR : online g R
pPR : para P R
bhgd : paragram b h g d L R M P
ef_bh : length e f = length b h
bh : b ≠ h
this : length b c > length b h
⊢ area a b c > area a b h

State before:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
this✝² : ¬online f O
g : point
N : line
gM : online g M
gN : online g N
fN : online f N
pON : para O N
efgd : paragram e f g d L N M O
this✝¹ : length e f = length d g
dg : d ≠ g
P : line
bP : online b P
dP : online d P
this✝ : ¬online g P
h : point
R : line
hL : online h L
hR : online h R
gR : online g R
pPR : para P R
bhgd : paragram b h g d L R M P
ef_bh : length e f = length b h
bh : b ≠ h
this : length b c > length b h
⊢ area a b c > area a b h
Tactic:
exact lt_area_of_lt_base_sameedge a bL cL hL bc bh aL this
State after:
no goals

State before:
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b = c
⊢ False
Tactic:
rw [length_eq_zero_iff.mpr bc] at hlen
State after:
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : 0 > length e f
bc : b = c
⊢ False

State before:
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : 0 > length e f
bc : b = c
⊢ False
Tactic:
exact (not_le_of_gt hlen) (length_nonneg e f)
State after:
no goals

State before:
case pos
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : e = f
⊢ area a b c > area d e f
Tactic:
perm [(area_zero_iff_online bc bL cL).not.mpr aL]
State after:
case pos
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : e = f
this : ¬area a b c = 0
⊢ area a b c > area d e f

State before:
case pos
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : e = f
this : ¬area a b c = 0
⊢ area a b c > area d e f
Tactic:
rw [area_of_eq d e f (by tauto)]
State after:
case pos
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : e = f
this : ¬area a b c = 0
⊢ area a b c > 0

State before:
case pos
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : e = f
this : ¬area a b c = 0
⊢ area a b c > 0
Tactic:
exact (Ne.symm this).lt_of_le (area_nonneg a b c)
State after:
no goals

State before:
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : e = f
this : ¬area a b c = 0
⊢ d = e ∨ d = f ∨ e = f
Tactic:
tauto
State after:
no goals

State before:
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
this : ¬online f O
g : point
N : line
gM : online g M
gN : online g N
fN : online f N
pON : para O N
⊢ paragram e f g d L N M O
Tactic:
splitAll <;> perma only [para] at *
State after:
no goals

State before:
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
this✝¹ : ¬online f O
g : point
N : line
gM : online g M
gN : online g N
fN : online f N
pON : para O N
efgd : paragram e f g d L N M O
this✝ : length e f = length d g
dg : d ≠ g
P : line
bP : online b P
dP : online d P
this : ¬online g P
h : point
R : line
hL : online h L
hR : online h R
gR : online g R
pPR : para P R
⊢ paragram b h g d L R M P
Tactic:
splitAll <;> perma only [para]
State after:
no goals

State before:
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
this✝¹ : ¬online f O
g : point
N : line
gM : online g M
gN : online g N
fN : online f N
pON : para O N
efgd : paragram e f g d L N M O
this✝ : length e f = length d g
dg : d ≠ g
P : line
bP : online b P
dP : online d P
this : ¬online g P
h : point
R : line
hL : online h L
hR : online h R
gR : online g R
pPR : para P R
bhgd : paragram b h g d L R M P
⊢ length e f = length b h
Tactic:
linperm [(len_ang_area_eq_of_parallelogram bhgd).1]
State after:
no goals

State before:
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
this✝¹ : ¬online f O
g : point
N : line
gM : online g M
gN : online g N
fN : online f N
pON : para O N
efgd : paragram e f g d L N M O
this✝ : length e f = length d g
dg : d ≠ g
P : line
bP : online b P
dP : online d P
this : ¬online g P
h : point
R : line
hL : online h L
hR : online h R
gR : online g R
pPR : para P R
bhgd : paragram b h g d L R M P
ef_bh : length e f = length b h
bh : b ≠ h
⊢ length b c > length b h
Tactic:
rw [← ef_bh]
State after:
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
this✝¹ : ¬online f O
g : point
N : line
gM : online g M
gN : online g N
fN : online f N
pON : para O N
efgd : paragram e f g d L N M O
this✝ : length e f = length d g
dg : d ≠ g
P : line
bP : online b P
dP : online d P
this : ¬online g P
h : point
R : line
hL : online h L
hR : online h R
gR : online g R
pPR : para P R
bhgd : paragram b h g d L R M P
ef_bh : length e f = length b h
bh : b ≠ h
⊢ length b c > length e f

State before:
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
this✝¹ : ¬online f O
g : point
N : line
gM : online g M
gN : online g N
fN : online f N
pON : para O N
efgd : paragram e f g d L N M O
this✝ : length e f = length d g
dg : d ≠ g
P : line
bP : online b P
dP : online d P
this : ¬online g P
h : point
R : line
hL : online h L
hR : online h R
gR : online g R
pPR : para P R
bhgd : paragram b h g d L R M P
ef_bh : length e f = length b h
bh : b ≠ h
⊢ length b c > length e f
Tactic:
exact hlen
State after:
no goals