Theorem: eq_area_of_eq_base (Pythagoras/euclid_I_extras.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
hlen : length b c = length e f
⊢ area a b c = area d e f
Tactic:
by_cases bc: b = c
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
⊢ 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
⊢ 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
⊢ area a b c = area d e f
Tactic:
have ef : e ≠ f := ne_of_ne_len bc hlen
State after:
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
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
ef : e ≠ f
⊢ area a b c = area d e f
Tactic:
obtain ⟨ K, aK, cK ⟩ := line_of_pts a c
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
ef : e ≠ f
K : line
aK : online a K
cK : online c K
⊢ 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
ef : e ≠ f
K : line
aK : online a K
cK : online c K
⊢ area a b c = area d e f
Tactic:
obtain ⟨ N, dN, eN ⟩ := line_of_pts d e
State after:
case neg.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
ef : e ≠ f
K : line
aK : online a K
cK : online c K
N : line
dN : online d N
eN : online e N
⊢ area a b c = area d e f

State before:
case neg.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
ef : e ≠ f
K : line
aK : online a K
cK : online c K
N : line
dN : online d N
eN : online e N
⊢ area a b c = area d e f
Tactic:
have aL := offline_of_para aM (para_symm pLM)
State after:
case neg.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
ef : e ≠ f
K : line
aK : online a K
cK : online c K
N : line
dN : online d N
eN : online e N
aL : ¬online a L
⊢ area a b c = area d e f

State before:
case neg.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
ef : e ≠ f
K : line
aK : online a K
cK : online c K
N : line
dN : online d N
eN : online e N
aL : ¬online a L
⊢ area a b c = area d e f
Tactic:
have := not_online_of_triangle aK cK cL bL aL (fun cb => bc cb.symm)
State after:
case neg.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
ef : e ≠ f
K : line
aK : online a K
cK : online c K
N : line
dN : online d N
eN : online e N
aL : ¬online a L
this : ¬online b K
⊢ area a b c = area d e f

State before:
case neg.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
ef : e ≠ f
K : line
aK : online a K
cK : online c K
N : line
dN : online d N
eN : online e N
aL : ¬online a L
this : ¬online b K
⊢ area a b c = area d e f
Tactic:
obtain ⟨ g, O, gM, hgO, bO, pKO ⟩ := parallel_projection bL pLM (not_para_of_online_online cK cL) this
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
ef : e ≠ f
K : line
aK : online a K
cK : online c K
N : line
dN : online d N
eN : online e N
aL : ¬online a L
this : ¬online b K
g : point
O : line
gM : online g M
hgO : online g O
bO : online b O
pKO : para K O
⊢ 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
ef : e ≠ f
K : line
aK : online a K
cK : online c K
N : line
dN : online d N
eN : online e N
aL : ¬online a L
this : ¬online b K
g : point
O : line
gM : online g M
hgO : online g O
bO : online b O
pKO : para K O
⊢ area a b c = area d e f
Tactic:
have dL := offline_of_para dM (para_symm pLM)
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
ef : e ≠ f
K : line
aK : online a K
cK : online c K
N : line
dN : online d N
eN : online e N
aL : ¬online a L
this : ¬online b K
g : point
O : line
gM : online g M
hgO : online g O
bO : online b O
pKO : para K O
dL : ¬online d L
⊢ 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
ef : e ≠ f
K : line
aK : online a K
cK : online c K
N : line
dN : online d N
eN : online e N
aL : ¬online a L
this : ¬online b K
g : point
O : line
gM : online g M
hgO : online g O
bO : online b O
pKO : para K O
dL : ¬online d L
⊢ area a b c = area d e f
Tactic:
have := not_online_of_triangle dN eN eL fL dL ef
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
ef : e ≠ f
K : line
aK : online a K
cK : online c K
N : line
dN : online d N
eN : online e N
aL : ¬online a L
this✝ : ¬online b K
g : point
O : line
gM : online g M
hgO : online g O
bO : online b O
pKO : para K O
dL : ¬online d L
this : ¬online f N
⊢ 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
ef : e ≠ f
K : line
aK : online a K
cK : online c K
N : line
dN : online d N
eN : online e N
aL : ¬online a L
this✝ : ¬online b K
g : point
O : line
gM : online g M
hgO : online g O
bO : online b O
pKO : para K O
dL : ¬online d L
this : ¬online f N
⊢ area a b c = area d e f
Tactic:
obtain ⟨ h, P, hhM, hP, hfP, pNP ⟩ := parallel_projection fL pLM (not_para_of_online_online eN eL) 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
ef : e ≠ f
K : line
aK : online a K
cK : online c K
N : line
dN : online d N
eN : online e N
aL : ¬online a L
this✝ : ¬online b K
g : point
O : line
gM : online g M
hgO : online g O
bO : online b O
pKO : para K O
dL : ¬online d L
this : ¬online f N
h : point
P : line
hhM : online h M
hP : online h P
hfP : online f P
pNP : para N 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
ef : e ≠ f
K : line
aK : online a K
cK : online c K
N : line
dN : online d N
eN : online e N
aL : ¬online a L
this✝ : ¬online b K
g : point
O : line
gM : online g M
hgO : online g O
bO : online b O
pKO : para K O
dL : ¬online d L
this : ¬online f N
h : point
P : line
hhM : online h M
hP : online h P
hfP : online f P
pNP : para N P
⊢ area a b c = area d e f
Tactic:
perm [eq_of_parallelogram_of_eq_basis gM aM dM hhM bL cL eL fL hgO bO aK cK dN eN hP hfP (by perma) (by perma) pNP 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
ef : e ≠ f
K : line
aK : online a K
cK : online c K
N : line
dN : online d N
eN : online e N
aL : ¬online a L
this✝¹ : ¬online b K
g : point
O : line
gM : online g M
hgO : online g O
bO : online b O
pKO : para K O
dL : ¬online d L
this✝ : ¬online f N
h : point
P : line
hhM : online h M
hP : online h P
hfP : online f P
pNP : para N P
this : area b c g + area a c g = area d e f + area d f 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
ef : e ≠ f
K : line
aK : online a K
cK : online c K
N : line
dN : online d N
eN : online e N
aL : ¬online a L
this✝¹ : ¬online b K
g : point
O : line
gM : online g M
hgO : online g O
bO : online b O
pKO : para K O
dL : ¬online d L
this✝ : ¬online f N
h : point
P : line
hhM : online h M
hP : online h P
hfP : online f P
pNP : para N P
this : area b c g + area a c g = area d e f + area d f h
⊢ area a b c = area d e f
Tactic:
have bcag: paragram b c a g L K M O:= 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
ef : e ≠ f
K : line
aK : online a K
cK : online c K
N : line
dN : online d N
eN : online e N
aL : ¬online a L
this✝¹ : ¬online b K
g : point
O : line
gM : online g M
hgO : online g O
bO : online b O
pKO : para K O
dL : ¬online d L
this✝ : ¬online f N
h : point
P : line
hhM : online h M
hP : online h P
hfP : online f P
pNP : para N P
this : area b c g + area a c g = area d e f + area d f h
bcag : paragram b c a g L K M O
⊢ 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
ef : e ≠ f
K : line
aK : online a K
cK : online c K
N : line
dN : online d N
eN : online e N
aL : ¬online a L
this✝¹ : ¬online b K
g : point
O : line
gM : online g M
hgO : online g O
bO : online b O
pKO : para K O
dL : ¬online d L
this✝ : ¬online f N
h : point
P : line
hhM : online h M
hP : online h P
hfP : online f P
pNP : para N P
this : area b c g + area a c g = area d e f + area d f h
bcag : paragram b c a g L K M O
⊢ area a b c = area d e f
Tactic:
have fedh: paragram f e d h L N 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
ef : e ≠ f
K : line
aK : online a K
cK : online c K
N : line
dN : online d N
eN : online e N
aL : ¬online a L
this✝¹ : ¬online b K
g : point
O : line
gM : online g M
hgO : online g O
bO : online b O
pKO : para K O
dL : ¬online d L
this✝ : ¬online f N
h : point
P : line
hhM : online h M
hP : online h P
hfP : online f P
pNP : para N P
this : area b c g + area a c g = area d e f + area d f h
bcag : paragram b c a g L K M O
fedh : paragram f e d h L N 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
ef : e ≠ f
K : line
aK : online a K
cK : online c K
N : line
dN : online d N
eN : online e N
aL : ¬online a L
this✝¹ : ¬online b K
g : point
O : line
gM : online g M
hgO : online g O
bO : online b O
pKO : para K O
dL : ¬online d L
this✝ : ¬online f N
h : point
P : line
hhM : online h M
hP : online h P
hfP : online f P
pNP : para N P
this : area b c g + area a c g = area d e f + area d f h
bcag : paragram b c a g L K M O
fedh : paragram f e d h L N M P
⊢ area a b c = area d e f
Tactic:
have: area b c g + area a c g = 2 * area a b c := by perma [(area_of_parallelogram bcag).2]
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
ef : e ≠ f
K : line
aK : online a K
cK : online c K
N : line
dN : online d N
eN : online e N
aL : ¬online a L
this✝² : ¬online b K
g : point
O : line
gM : online g M
hgO : online g O
bO : online b O
pKO : para K O
dL : ¬online d L
this✝¹ : ¬online f N
h : point
P : line
hhM : online h M
hP : online h P
hfP : online f P
pNP : para N P
this✝ : area b c g + area a c g = area d e f + area d f h
bcag : paragram b c a g L K M O
fedh : paragram f e d h L N M P
this : area b c g + area a c g = 2 * area a b c
⊢ 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
ef : e ≠ f
K : line
aK : online a K
cK : online c K
N : line
dN : online d N
eN : online e N
aL : ¬online a L
this✝² : ¬online b K
g : point
O : line
gM : online g M
hgO : online g O
bO : online b O
pKO : para K O
dL : ¬online d L
this✝¹ : ¬online f N
h : point
P : line
hhM : online h M
hP : online h P
hfP : online f P
pNP : para N P
this✝ : area b c g + area a c g = area d e f + area d f h
bcag : paragram b c a g L K M O
fedh : paragram f e d h L N M P
this : area b c g + area a c g = 2 * area a b c
⊢ area a b c = area d e f
Tactic:
have: area d e f = area d f h := by linperm [(area_of_parallelogram fedh).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
ef : e ≠ f
K : line
aK : online a K
cK : online c K
N : line
dN : online d N
eN : online e N
aL : ¬online a L
this✝³ : ¬online b K
g : point
O : line
gM : online g M
hgO : online g O
bO : online b O
pKO : para K O
dL : ¬online d L
this✝² : ¬online f N
h : point
P : line
hhM : online h M
hP : online h P
hfP : online f P
pNP : para N P
this✝¹ : area b c g + area a c g = area d e f + area d f h
bcag : paragram b c a g L K M O
fedh : paragram f e d h L N M P
this✝ : area b c g + area a c g = 2 * area a b c
this : area d e f = area d f 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
ef : e ≠ f
K : line
aK : online a K
cK : online c K
N : line
dN : online d N
eN : online e N
aL : ¬online a L
this✝³ : ¬online b K
g : point
O : line
gM : online g M
hgO : online g O
bO : online b O
pKO : para K O
dL : ¬online d L
this✝² : ¬online f N
h : point
P : line
hhM : online h M
hP : online h P
hfP : online f P
pNP : para N P
this✝¹ : area b c g + area a c g = area d e f + area d f h
bcag : paragram b c a g L K M O
fedh : paragram f e d h L N M P
this✝ : area b c g + area a c g = 2 * area a b c
this : area d e f = area d f h
⊢ area a b c = area d e f
Tactic:
linarith
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
⊢ area a b c = area d e f
Tactic:
have ef: e = f := (same_len_pts_coincide_iff hlen).mp bc
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
ef : e = f
⊢ 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
ef : e = f
⊢ area a b c = area d e f
Tactic:
rw [area_of_eq a b c (by tauto), area_of_eq d e f (by 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
ef : e = f
⊢ a = b ∨ a = c ∨ b = c
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
ef : e = f
⊢ 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
ef : e ≠ f
K : line
aK : online a K
cK : online c K
N : line
dN : online d N
eN : online e N
aL : ¬online a L
this✝ : ¬online b K
g : point
O : line
gM : online g M
hgO : online g O
bO : online b O
pKO : para K O
dL : ¬online d L
this : ¬online f N
h : point
P : line
hhM : online h M
hP : online h P
hfP : online f P
pNP : para N P
⊢ para M L
Tactic:
perma
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
ef : e ≠ f
K : line
aK : online a K
cK : online c K
N : line
dN : online d N
eN : online e N
aL : ¬online a L
this✝ : ¬online b K
g : point
O : line
gM : online g M
hgO : online g O
bO : online b O
pKO : para K O
dL : ¬online d L
this : ¬online f N
h : point
P : line
hhM : online h M
hP : online h P
hfP : online f P
pNP : para N P
⊢ para O K
Tactic:
perma
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
ef : e ≠ f
K : line
aK : online a K
cK : online c K
N : line
dN : online d N
eN : online e N
aL : ¬online a L
this✝¹ : ¬online b K
g : point
O : line
gM : online g M
hgO : online g O
bO : online b O
pKO : para K O
dL : ¬online d L
this✝ : ¬online f N
h : point
P : line
hhM : online h M
hP : online h P
hfP : online f P
pNP : para N P
this : area b c g + area a c g = area d e f + area d f h
⊢ paragram b c a g L K M O
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
ef : e ≠ f
K : line
aK : online a K
cK : online c K
N : line
dN : online d N
eN : online e N
aL : ¬online a L
this✝¹ : ¬online b K
g : point
O : line
gM : online g M
hgO : online g O
bO : online b O
pKO : para K O
dL : ¬online d L
this✝ : ¬online f N
h : point
P : line
hhM : online h M
hP : online h P
hfP : online f P
pNP : para N P
this : area b c g + area a c g = area d e f + area d f h
bcag : paragram b c a g L K M O
⊢ paragram f e d h L N 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
ef : e ≠ f
K : line
aK : online a K
cK : online c K
N : line
dN : online d N
eN : online e N
aL : ¬online a L
this✝¹ : ¬online b K
g : point
O : line
gM : online g M
hgO : online g O
bO : online b O
pKO : para K O
dL : ¬online d L
this✝ : ¬online f N
h : point
P : line
hhM : online h M
hP : online h P
hfP : online f P
pNP : para N P
this : area b c g + area a c g = area d e f + area d f h
bcag : paragram b c a g L K M O
fedh : paragram f e d h L N M P
⊢ area b c g + area a c g = 2 * area a b c
Tactic:
perma [(area_of_parallelogram bcag).2]
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
ef : e ≠ f
K : line
aK : online a K
cK : online c K
N : line
dN : online d N
eN : online e N
aL : ¬online a L
this✝² : ¬online b K
g : point
O : line
gM : online g M
hgO : online g O
bO : online b O
pKO : para K O
dL : ¬online d L
this✝¹ : ¬online f N
h : point
P : line
hhM : online h M
hP : online h P
hfP : online f P
pNP : para N P
this✝ : area b c g + area a c g = area d e f + area d f h
bcag : paragram b c a g L K M O
fedh : paragram f e d h L N M P
this : area b c g + area a c g = 2 * area a b c
⊢ area d e f = area d f h
Tactic:
linperm [(area_of_parallelogram fedh).1]
State after:
no goals