Theorem: eq_of_parallelogram_of_eq_basis_of_diffside (Pythagoras/euclid_I_extras.lean)

State before:
i : incidence_geometry
a b c d e f g h : point
L M K N O P : line
aL : online a L
dL : online d L
eL : online e L
hL : online h L
bM : online b M
cM : online c M
fM : online f M
gM : online g M
aK : online a K
bK : online b K
dN : online d N
cN : online c N
eO : online e O
fO : online f O
hP : online h P
gP : online g P
pLM : para L M
pKN : para K N
pOP : para O P
hlen : length b c = length f g
S : line
cS : online c S
eS : online e S
aPd : diffside b h S
bc : b ≠ c
⊢ area a b c + area a d c = area e f g + area e h g
Tactic:
obtain ⟨ Q, bQ, eQ ⟩ := line_of_pts b e
State after:
case intro.intro
i : incidence_geometry
a b c d e f g h : point
L M K N O P : line
aL : online a L
dL : online d L
eL : online e L
hL : online h L
bM : online b M
cM : online c M
fM : online f M
gM : online g M
aK : online a K
bK : online b K
dN : online d N
cN : online c N
eO : online e O
fO : online f O
hP : online h P
gP : online g P
pLM : para L M
pKN : para K N
pOP : para O P
hlen : length b c = length f g
S : line
cS : online c S
eS : online e S
aPd : diffside b h S
bc : b ≠ c
Q : line
bQ : online b Q
eQ : online e Q
⊢ area a b c + area a d c = area e f g + area e h g

State before:
case intro.intro
i : incidence_geometry
a b c d e f g h : point
L M K N O P : line
aL : online a L
dL : online d L
eL : online e L
hL : online h L
bM : online b M
cM : online c M
fM : online f M
gM : online g M
aK : online a K
bK : online b K
dN : online d N
cN : online c N
eO : online e O
fO : online f O
hP : online h P
gP : online g P
pLM : para L M
pKN : para K N
pOP : para O P
hlen : length b c = length f g
S : line
cS : online c S
eS : online e S
aPd : diffside b h S
bc : b ≠ c
Q : line
bQ : online b Q
eQ : online e Q
⊢ area a b c + area a d c = area e f g + area e h g
Tactic:
obtain ⟨ R, cR, hR ⟩ := line_of_pts c h
State after:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e f g h : point
L M K N O P : line
aL : online a L
dL : online d L
eL : online e L
hL : online h L
bM : online b M
cM : online c M
fM : online f M
gM : online g M
aK : online a K
bK : online b K
dN : online d N
cN : online c N
eO : online e O
fO : online f O
hP : online h P
gP : online g P
pLM : para L M
pKN : para K N
pOP : para O P
hlen : length b c = length f g
S : line
cS : online c S
eS : online e S
aPd : diffside b h S
bc : b ≠ c
Q : line
bQ : online b Q
eQ : online e Q
R : line
cR : online c R
hR : online h R
⊢ area a b c + area a d c = area e f g + area e h g

State before:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e f g h : point
L M K N O P : line
aL : online a L
dL : online d L
eL : online e L
hL : online h L
bM : online b M
cM : online c M
fM : online f M
gM : online g M
aK : online a K
bK : online b K
dN : online d N
cN : online c N
eO : online e O
fO : online f O
hP : online h P
gP : online g P
pLM : para L M
pKN : para K N
pOP : para O P
hlen : length b c = length f g
S : line
cS : online c S
eS : online e S
aPd : diffside b h S
bc : b ≠ c
Q : line
bQ : online b Q
eQ : online e Q
R : line
cR : online c R
hR : online h R
⊢ area a b c + area a d c = area e f g + area e h g
Tactic:
have ec : e ≠ c := neq_of_para eL cM pLM
State after:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e f g h : point
L M K N O P : line
aL : online a L
dL : online d L
eL : online e L
hL : online h L
bM : online b M
cM : online c M
fM : online f M
gM : online g M
aK : online a K
bK : online b K
dN : online d N
cN : online c N
eO : online e O
fO : online f O
hP : online h P
gP : online g P
pLM : para L M
pKN : para K N
pOP : para O P
hlen : length b c = length f g
S : line
cS : online c S
eS : online e S
aPd : diffside b h S
bc : b ≠ c
Q : line
bQ : online b Q
eQ : online e Q
R : line
cR : online c R
hR : online h R
ec : e ≠ c
⊢ area a b c + area a d c = area e f g + area e h g

State before:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e f g h : point
L M K N O P : line
aL : online a L
dL : online d L
eL : online e L
hL : online h L
bM : online b M
cM : online c M
fM : online f M
gM : online g M
aK : online a K
bK : online b K
dN : online d N
cN : online c N
eO : online e O
fO : online f O
hP : online h P
gP : online g P
pLM : para L M
pKN : para K N
pOP : para O P
hlen : length b c = length f g
S : line
cS : online c S
eS : online e S
aPd : diffside b h S
bc : b ≠ c
Q : line
bQ : online b Q
eQ : online e Q
R : line
cR : online c R
hR : online h R
ec : e ≠ c
⊢ area a b c + area a d c = area e f g + area e h g
Tactic:
have ehgf : paragram e h g f L P M O := by splitAll <;> perma only [para]
State after:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e f g h : point
L M K N O P : line
aL : online a L
dL : online d L
eL : online e L
hL : online h L
bM : online b M
cM : online c M
fM : online f M
gM : online g M
aK : online a K
bK : online b K
dN : online d N
cN : online c N
eO : online e O
fO : online f O
hP : online h P
gP : online g P
pLM : para L M
pKN : para K N
pOP : para O P
hlen : length b c = length f g
S : line
cS : online c S
eS : online e S
aPd : diffside b h S
bc : b ≠ c
Q : line
bQ : online b Q
eQ : online e Q
R : line
cR : online c R
hR : online h R
ec : e ≠ c
ehgf : paragram e h g f L P M O
⊢ area a b c + area a d c = area e f g + area e h g

State before:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e f g h : point
L M K N O P : line
aL : online a L
dL : online d L
eL : online e L
hL : online h L
bM : online b M
cM : online c M
fM : online f M
gM : online g M
aK : online a K
bK : online b K
dN : online d N
cN : online c N
eO : online e O
fO : online f O
hP : online h P
gP : online g P
pLM : para L M
pKN : para K N
pOP : para O P
hlen : length b c = length f g
S : line
cS : online c S
eS : online e S
aPd : diffside b h S
bc : b ≠ c
Q : line
bQ : online b Q
eQ : online e Q
R : line
cR : online c R
hR : online h R
ec : e ≠ c
ehgf : paragram e h g f L P M O
⊢ area a b c + area a d c = area e f g + area e h g
Tactic:
have : length b c = length e h := by linperm [(len_ang_area_eq_of_parallelogram ehgf).1]
State after:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e f g h : point
L M K N O P : line
aL : online a L
dL : online d L
eL : online e L
hL : online h L
bM : online b M
cM : online c M
fM : online f M
gM : online g M
aK : online a K
bK : online b K
dN : online d N
cN : online c N
eO : online e O
fO : online f O
hP : online h P
gP : online g P
pLM : para L M
pKN : para K N
pOP : para O P
hlen : length b c = length f g
S : line
cS : online c S
eS : online e S
aPd : diffside b h S
bc : b ≠ c
Q : line
bQ : online b Q
eQ : online e Q
R : line
cR : online c R
hR : online h R
ec : e ≠ c
ehgf : paragram e h g f L P M O
this : length b c = length e h
⊢ area a b c + area a d c = area e f g + area e h g

State before:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e f g h : point
L M K N O P : line
aL : online a L
dL : online d L
eL : online e L
hL : online h L
bM : online b M
cM : online c M
fM : online f M
gM : online g M
aK : online a K
bK : online b K
dN : online d N
cN : online c N
eO : online e O
fO : online f O
hP : online h P
gP : online g P
pLM : para L M
pKN : para K N
pOP : para O P
hlen : length b c = length f g
S : line
cS : online c S
eS : online e S
aPd : diffside b h S
bc : b ≠ c
Q : line
bQ : online b Q
eQ : online e Q
R : line
cR : online c R
hR : online h R
ec : e ≠ c
ehgf : paragram e h g f L P M O
this : length b c = length e h
⊢ area a b c + area a d c = area e f g + area e h g
Tactic:
have' pQR := para_len_parallelogram bM cM eL hL bQ eQ cR hR cS eS ec aPd (para_symm pLM) this
State after:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e f g h : point
L M K N O P : line
aL : online a L
dL : online d L
eL : online e L
hL : online h L
bM : online b M
cM : online c M
fM : online f M
gM : online g M
aK : online a K
bK : online b K
dN : online d N
cN : online c N
eO : online e O
fO : online f O
hP : online h P
gP : online g P
pLM : para L M
pKN : para K N
pOP : para O P
hlen : length b c = length f g
S : line
cS : online c S
eS : online e S
aPd : diffside b h S
bc : b ≠ c
Q : line
bQ : online b Q
eQ : online e Q
R : line
cR : online c R
hR : online h R
ec : e ≠ c
ehgf : paragram e h g f L P M O
this : length b c = length e h
pQR : para Q R
⊢ area a b c + area a d c = area e f g + area e h g

State before:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e f g h : point
L M K N O P : line
aL : online a L
dL : online d L
eL : online e L
hL : online h L
bM : online b M
cM : online c M
fM : online f M
gM : online g M
aK : online a K
bK : online b K
dN : online d N
cN : online c N
eO : online e O
fO : online f O
hP : online h P
gP : online g P
pLM : para L M
pKN : para K N
pOP : para O P
hlen : length b c = length f g
S : line
cS : online c S
eS : online e S
aPd : diffside b h S
bc : b ≠ c
Q : line
bQ : online b Q
eQ : online e Q
R : line
cR : online c R
hR : online h R
ec : e ≠ c
ehgf : paragram e h g f L P M O
this : length b c = length e h
pQR : para Q R
⊢ area a b c + area a d c = area e f g + area e h g
Tactic:
have eq1 := parallelarea aL dL bM cM eL hL aK bK dN cN bQ eQ cR hR pLM pKN pQR
State after:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e f g h : point
L M K N O P : line
aL : online a L
dL : online d L
eL : online e L
hL : online h L
bM : online b M
cM : online c M
fM : online f M
gM : online g M
aK : online a K
bK : online b K
dN : online d N
cN : online c N
eO : online e O
fO : online f O
hP : online h P
gP : online g P
pLM : para L M
pKN : para K N
pOP : para O P
hlen : length b c = length f g
S : line
cS : online c S
eS : online e S
aPd : diffside b h S
bc : b ≠ c
Q : line
bQ : online b Q
eQ : online e Q
R : line
cR : online c R
hR : online h R
ec : e ≠ c
ehgf : paragram e h g f L P M O
this : length b c = length e h
pQR : para Q R
eq1 : area b a d + area d b c = area c h e + area e c b
⊢ area a b c + area a d c = area e f g + area e h g

State before:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e f g h : point
L M K N O P : line
aL : online a L
dL : online d L
eL : online e L
hL : online h L
bM : online b M
cM : online c M
fM : online f M
gM : online g M
aK : online a K
bK : online b K
dN : online d N
cN : online c N
eO : online e O
fO : online f O
hP : online h P
gP : online g P
pLM : para L M
pKN : para K N
pOP : para O P
hlen : length b c = length f g
S : line
cS : online c S
eS : online e S
aPd : diffside b h S
bc : b ≠ c
Q : line
bQ : online b Q
eQ : online e Q
R : line
cR : online c R
hR : online h R
ec : e ≠ c
ehgf : paragram e h g f L P M O
this : length b c = length e h
pQR : para Q R
eq1 : area b a d + area d b c = area c h e + area e c b
⊢ area a b c + area a d c = area e f g + area e h g
Tactic:
have eq2 := parallelarea bM cM eL hL fM gM bQ eQ cR hR eO fO hP gP (para_symm pLM) pQR pOP
State after:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e f g h : point
L M K N O P : line
aL : online a L
dL : online d L
eL : online e L
hL : online h L
bM : online b M
cM : online c M
fM : online f M
gM : online g M
aK : online a K
bK : online b K
dN : online d N
cN : online c N
eO : online e O
fO : online f O
hP : online h P
gP : online g P
pLM : para L M
pKN : para K N
pOP : para O P
hlen : length b c = length f g
S : line
cS : online c S
eS : online e S
aPd : diffside b h S
bc : b ≠ c
Q : line
bQ : online b Q
eQ : online e Q
R : line
cR : online c R
hR : online h R
ec : e ≠ c
ehgf : paragram e h g f L P M O
this : length b c = length e h
pQR : para Q R
eq1 : area b a d + area d b c = area c h e + area e c b
eq2 : area e b c + area c e h = area h g f + area f h e
⊢ area a b c + area a d c = area e f g + area e h g

State before:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e f g h : point
L M K N O P : line
aL : online a L
dL : online d L
eL : online e L
hL : online h L
bM : online b M
cM : online c M
fM : online f M
gM : online g M
aK : online a K
bK : online b K
dN : online d N
cN : online c N
eO : online e O
fO : online f O
hP : online h P
gP : online g P
pLM : para L M
pKN : para K N
pOP : para O P
hlen : length b c = length f g
S : line
cS : online c S
eS : online e S
aPd : diffside b h S
bc : b ≠ c
Q : line
bQ : online b Q
eQ : online e Q
R : line
cR : online c R
hR : online h R
ec : e ≠ c
ehgf : paragram e h g f L P M O
this : length b c = length e h
pQR : para Q R
eq1 : area b a d + area d b c = area c h e + area e c b
eq2 : area e b c + area c e h = area h g f + area f h e
⊢ area a b c + area a d c = area e f g + area e h g
Tactic:
have abcd : paragram a b c d K M N L := by splitAll <;> perma only [para]
State after:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e f g h : point
L M K N O P : line
aL : online a L
dL : online d L
eL : online e L
hL : online h L
bM : online b M
cM : online c M
fM : online f M
gM : online g M
aK : online a K
bK : online b K
dN : online d N
cN : online c N
eO : online e O
fO : online f O
hP : online h P
gP : online g P
pLM : para L M
pKN : para K N
pOP : para O P
hlen : length b c = length f g
S : line
cS : online c S
eS : online e S
aPd : diffside b h S
bc : b ≠ c
Q : line
bQ : online b Q
eQ : online e Q
R : line
cR : online c R
hR : online h R
ec : e ≠ c
ehgf : paragram e h g f L P M O
this : length b c = length e h
pQR : para Q R
eq1 : area b a d + area d b c = area c h e + area e c b
eq2 : area e b c + area c e h = area h g f + area f h e
abcd : paragram a b c d K M N L
⊢ area a b c + area a d c = area e f g + area e h g

State before:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e f g h : point
L M K N O P : line
aL : online a L
dL : online d L
eL : online e L
hL : online h L
bM : online b M
cM : online c M
fM : online f M
gM : online g M
aK : online a K
bK : online b K
dN : online d N
cN : online c N
eO : online e O
fO : online f O
hP : online h P
gP : online g P
pLM : para L M
pKN : para K N
pOP : para O P
hlen : length b c = length f g
S : line
cS : online c S
eS : online e S
aPd : diffside b h S
bc : b ≠ c
Q : line
bQ : online b Q
eQ : online e Q
R : line
cR : online c R
hR : online h R
ec : e ≠ c
ehgf : paragram e h g f L P M O
this : length b c = length e h
pQR : para Q R
eq1 : area b a d + area d b c = area c h e + area e c b
eq2 : area e b c + area c e h = area h g f + area f h e
abcd : paragram a b c d K M N L
⊢ area a b c + area a d c = area e f g + area e h g
Tactic:
have hgfe : paragram h g f e P M O L := by splitAll <;> perma only [para]
State after:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e f g h : point
L M K N O P : line
aL : online a L
dL : online d L
eL : online e L
hL : online h L
bM : online b M
cM : online c M
fM : online f M
gM : online g M
aK : online a K
bK : online b K
dN : online d N
cN : online c N
eO : online e O
fO : online f O
hP : online h P
gP : online g P
pLM : para L M
pKN : para K N
pOP : para O P
hlen : length b c = length f g
S : line
cS : online c S
eS : online e S
aPd : diffside b h S
bc : b ≠ c
Q : line
bQ : online b Q
eQ : online e Q
R : line
cR : online c R
hR : online h R
ec : e ≠ c
ehgf : paragram e h g f L P M O
this : length b c = length e h
pQR : para Q R
eq1 : area b a d + area d b c = area c h e + area e c b
eq2 : area e b c + area c e h = area h g f + area f h e
abcd : paragram a b c d K M N L
hgfe : paragram h g f e P M O L
⊢ area a b c + area a d c = area e f g + area e h g

State before:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e f g h : point
L M K N O P : line
aL : online a L
dL : online d L
eL : online e L
hL : online h L
bM : online b M
cM : online c M
fM : online f M
gM : online g M
aK : online a K
bK : online b K
dN : online d N
cN : online c N
eO : online e O
fO : online f O
hP : online h P
gP : online g P
pLM : para L M
pKN : para K N
pOP : para O P
hlen : length b c = length f g
S : line
cS : online c S
eS : online e S
aPd : diffside b h S
bc : b ≠ c
Q : line
bQ : online b Q
eQ : online e Q
R : line
cR : online c R
hR : online h R
ec : e ≠ c
ehgf : paragram e h g f L P M O
this : length b c = length e h
pQR : para Q R
eq1 : area b a d + area d b c = area c h e + area e c b
eq2 : area e b c + area c e h = area h g f + area f h e
abcd : paragram a b c d K M N L
hgfe : paragram h g f e P M O L
⊢ area a b c + area a d c = area e f g + area e h g
Tactic:
have: area a b c = area a c d := by linperm [(area_of_parallelogram abcd).1]
State after:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e f g h : point
L M K N O P : line
aL : online a L
dL : online d L
eL : online e L
hL : online h L
bM : online b M
cM : online c M
fM : online f M
gM : online g M
aK : online a K
bK : online b K
dN : online d N
cN : online c N
eO : online e O
fO : online f O
hP : online h P
gP : online g P
pLM : para L M
pKN : para K N
pOP : para O P
hlen : length b c = length f g
S : line
cS : online c S
eS : online e S
aPd : diffside b h S
bc : b ≠ c
Q : line
bQ : online b Q
eQ : online e Q
R : line
cR : online c R
hR : online h R
ec : e ≠ c
ehgf : paragram e h g f L P M O
this✝ : length b c = length e h
pQR : para Q R
eq1 : area b a d + area d b c = area c h e + area e c b
eq2 : area e b c + area c e h = area h g f + area f h e
abcd : paragram a b c d K M N L
hgfe : paragram h g f e P M O L
this : area a b c = area a c d
⊢ area a b c + area a d c = area e f g + area e h g

State before:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e f g h : point
L M K N O P : line
aL : online a L
dL : online d L
eL : online e L
hL : online h L
bM : online b M
cM : online c M
fM : online f M
gM : online g M
aK : online a K
bK : online b K
dN : online d N
cN : online c N
eO : online e O
fO : online f O
hP : online h P
gP : online g P
pLM : para L M
pKN : para K N
pOP : para O P
hlen : length b c = length f g
S : line
cS : online c S
eS : online e S
aPd : diffside b h S
bc : b ≠ c
Q : line
bQ : online b Q
eQ : online e Q
R : line
cR : online c R
hR : online h R
ec : e ≠ c
ehgf : paragram e h g f L P M O
this✝ : length b c = length e h
pQR : para Q R
eq1 : area b a d + area d b c = area c h e + area e c b
eq2 : area e b c + area c e h = area h g f + area f h e
abcd : paragram a b c d K M N L
hgfe : paragram h g f e P M O L
this : area a b c = area a c d
⊢ area a b c + area a d c = area e f g + area e h g
Tactic:
have: area f g h = area e f h := by linperm [(area_of_parallelogram hgfe).1]
State after:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e f g h : point
L M K N O P : line
aL : online a L
dL : online d L
eL : online e L
hL : online h L
bM : online b M
cM : online c M
fM : online f M
gM : online g M
aK : online a K
bK : online b K
dN : online d N
cN : online c N
eO : online e O
fO : online f O
hP : online h P
gP : online g P
pLM : para L M
pKN : para K N
pOP : para O P
hlen : length b c = length f g
S : line
cS : online c S
eS : online e S
aPd : diffside b h S
bc : b ≠ c
Q : line
bQ : online b Q
eQ : online e Q
R : line
cR : online c R
hR : online h R
ec : e ≠ c
ehgf : paragram e h g f L P M O
this✝¹ : length b c = length e h
pQR : para Q R
eq1 : area b a d + area d b c = area c h e + area e c b
eq2 : area e b c + area c e h = area h g f + area f h e
abcd : paragram a b c d K M N L
hgfe : paragram h g f e P M O L
this✝ : area a b c = area a c d
this : area f g h = area e f h
⊢ area a b c + area a d c = area e f g + area e h g

State before:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e f g h : point
L M K N O P : line
aL : online a L
dL : online d L
eL : online e L
hL : online h L
bM : online b M
cM : online c M
fM : online f M
gM : online g M
aK : online a K
bK : online b K
dN : online d N
cN : online c N
eO : online e O
fO : online f O
hP : online h P
gP : online g P
pLM : para L M
pKN : para K N
pOP : para O P
hlen : length b c = length f g
S : line
cS : online c S
eS : online e S
aPd : diffside b h S
bc : b ≠ c
Q : line
bQ : online b Q
eQ : online e Q
R : line
cR : online c R
hR : online h R
ec : e ≠ c
ehgf : paragram e h g f L P M O
this✝¹ : length b c = length e h
pQR : para Q R
eq1 : area b a d + area d b c = area c h e + area e c b
eq2 : area e b c + area c e h = area h g f + area f h e
abcd : paragram a b c d K M N L
hgfe : paragram h g f e P M O L
this✝ : area a b c = area a c d
this : area f g h = area e f h
⊢ area a b c + area a d c = area e f g + area e h g
Tactic:
have: 2 * area a b c = area f g h + area e f h := by linperm [(area_of_parallelogram abcd).2]
State after:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e f g h : point
L M K N O P : line
aL : online a L
dL : online d L
eL : online e L
hL : online h L
bM : online b M
cM : online c M
fM : online f M
gM : online g M
aK : online a K
bK : online b K
dN : online d N
cN : online c N
eO : online e O
fO : online f O
hP : online h P
gP : online g P
pLM : para L M
pKN : para K N
pOP : para O P
hlen : length b c = length f g
S : line
cS : online c S
eS : online e S
aPd : diffside b h S
bc : b ≠ c
Q : line
bQ : online b Q
eQ : online e Q
R : line
cR : online c R
hR : online h R
ec : e ≠ c
ehgf : paragram e h g f L P M O
this✝² : length b c = length e h
pQR : para Q R
eq1 : area b a d + area d b c = area c h e + area e c b
eq2 : area e b c + area c e h = area h g f + area f h e
abcd : paragram a b c d K M N L
hgfe : paragram h g f e P M O L
this✝¹ : area a b c = area a c d
this✝ : area f g h = area e f h
this : 2 * area a b c = area f g h + area e f h
⊢ area a b c + area a d c = area e f g + area e h g

State before:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e f g h : point
L M K N O P : line
aL : online a L
dL : online d L
eL : online e L
hL : online h L
bM : online b M
cM : online c M
fM : online f M
gM : online g M
aK : online a K
bK : online b K
dN : online d N
cN : online c N
eO : online e O
fO : online f O
hP : online h P
gP : online g P
pLM : para L M
pKN : para K N
pOP : para O P
hlen : length b c = length f g
S : line
cS : online c S
eS : online e S
aPd : diffside b h S
bc : b ≠ c
Q : line
bQ : online b Q
eQ : online e Q
R : line
cR : online c R
hR : online h R
ec : e ≠ c
ehgf : paragram e h g f L P M O
this✝² : length b c = length e h
pQR : para Q R
eq1 : area b a d + area d b c = area c h e + area e c b
eq2 : area e b c + area c e h = area h g f + area f h e
abcd : paragram a b c d K M N L
hgfe : paragram h g f e P M O L
this✝¹ : area a b c = area a c d
this✝ : area f g h = area e f h
this : 2 * area a b c = area f g h + area e f h
⊢ area a b c + area a d c = area e f g + area e h g
Tactic:
linperm [(area_of_parallelogram hgfe).2]
State after:
no goals

State before:
i : incidence_geometry
a b c d e f g h : point
L M K N O P : line
aL : online a L
dL : online d L
eL : online e L
hL : online h L
bM : online b M
cM : online c M
fM : online f M
gM : online g M
aK : online a K
bK : online b K
dN : online d N
cN : online c N
eO : online e O
fO : online f O
hP : online h P
gP : online g P
pLM : para L M
pKN : para K N
pOP : para O P
hlen : length b c = length f g
S : line
cS : online c S
eS : online e S
aPd : diffside b h S
bc : b ≠ c
Q : line
bQ : online b Q
eQ : online e Q
R : line
cR : online c R
hR : online h R
ec : e ≠ c
⊢ paragram e h g f L P M O
Tactic:
splitAll <;> perma only [para]
State after:
no goals

State before:
i : incidence_geometry
a b c d e f g h : point
L M K N O P : line
aL : online a L
dL : online d L
eL : online e L
hL : online h L
bM : online b M
cM : online c M
fM : online f M
gM : online g M
aK : online a K
bK : online b K
dN : online d N
cN : online c N
eO : online e O
fO : online f O
hP : online h P
gP : online g P
pLM : para L M
pKN : para K N
pOP : para O P
hlen : length b c = length f g
S : line
cS : online c S
eS : online e S
aPd : diffside b h S
bc : b ≠ c
Q : line
bQ : online b Q
eQ : online e Q
R : line
cR : online c R
hR : online h R
ec : e ≠ c
ehgf : paragram e h g f L P M O
⊢ length b c = length e h
Tactic:
linperm [(len_ang_area_eq_of_parallelogram ehgf).1]
State after:
no goals

State before:
i : incidence_geometry
a b c d e f g h : point
L M K N O P : line
aL : online a L
dL : online d L
eL : online e L
hL : online h L
bM : online b M
cM : online c M
fM : online f M
gM : online g M
aK : online a K
bK : online b K
dN : online d N
cN : online c N
eO : online e O
fO : online f O
hP : online h P
gP : online g P
pLM : para L M
pKN : para K N
pOP : para O P
hlen : length b c = length f g
S : line
cS : online c S
eS : online e S
aPd : diffside b h S
bc : b ≠ c
Q : line
bQ : online b Q
eQ : online e Q
R : line
cR : online c R
hR : online h R
ec : e ≠ c
ehgf : paragram e h g f L P M O
this : length b c = length e h
pQR : para Q R
eq1 : area b a d + area d b c = area c h e + area e c b
eq2 : area e b c + area c e h = area h g f + area f h e
⊢ paragram a b c d K M N L
Tactic:
splitAll <;> perma only [para]
State after:
no goals

State before:
i : incidence_geometry
a b c d e f g h : point
L M K N O P : line
aL : online a L
dL : online d L
eL : online e L
hL : online h L
bM : online b M
cM : online c M
fM : online f M
gM : online g M
aK : online a K
bK : online b K
dN : online d N
cN : online c N
eO : online e O
fO : online f O
hP : online h P
gP : online g P
pLM : para L M
pKN : para K N
pOP : para O P
hlen : length b c = length f g
S : line
cS : online c S
eS : online e S
aPd : diffside b h S
bc : b ≠ c
Q : line
bQ : online b Q
eQ : online e Q
R : line
cR : online c R
hR : online h R
ec : e ≠ c
ehgf : paragram e h g f L P M O
this : length b c = length e h
pQR : para Q R
eq1 : area b a d + area d b c = area c h e + area e c b
eq2 : area e b c + area c e h = area h g f + area f h e
abcd : paragram a b c d K M N L
⊢ paragram h g f e P M O L
Tactic:
splitAll <;> perma only [para]
State after:
no goals

State before:
i : incidence_geometry
a b c d e f g h : point
L M K N O P : line
aL : online a L
dL : online d L
eL : online e L
hL : online h L
bM : online b M
cM : online c M
fM : online f M
gM : online g M
aK : online a K
bK : online b K
dN : online d N
cN : online c N
eO : online e O
fO : online f O
hP : online h P
gP : online g P
pLM : para L M
pKN : para K N
pOP : para O P
hlen : length b c = length f g
S : line
cS : online c S
eS : online e S
aPd : diffside b h S
bc : b ≠ c
Q : line
bQ : online b Q
eQ : online e Q
R : line
cR : online c R
hR : online h R
ec : e ≠ c
ehgf : paragram e h g f L P M O
this : length b c = length e h
pQR : para Q R
eq1 : area b a d + area d b c = area c h e + area e c b
eq2 : area e b c + area c e h = area h g f + area f h e
abcd : paragram a b c d K M N L
hgfe : paragram h g f e P M O L
⊢ area a b c = area a c d
Tactic:
linperm [(area_of_parallelogram abcd).1]
State after:
no goals

State before:
i : incidence_geometry
a b c d e f g h : point
L M K N O P : line
aL : online a L
dL : online d L
eL : online e L
hL : online h L
bM : online b M
cM : online c M
fM : online f M
gM : online g M
aK : online a K
bK : online b K
dN : online d N
cN : online c N
eO : online e O
fO : online f O
hP : online h P
gP : online g P
pLM : para L M
pKN : para K N
pOP : para O P
hlen : length b c = length f g
S : line
cS : online c S
eS : online e S
aPd : diffside b h S
bc : b ≠ c
Q : line
bQ : online b Q
eQ : online e Q
R : line
cR : online c R
hR : online h R
ec : e ≠ c
ehgf : paragram e h g f L P M O
this✝ : length b c = length e h
pQR : para Q R
eq1 : area b a d + area d b c = area c h e + area e c b
eq2 : area e b c + area c e h = area h g f + area f h e
abcd : paragram a b c d K M N L
hgfe : paragram h g f e P M O L
this : area a b c = area a c d
⊢ area f g h = area e f h
Tactic:
linperm [(area_of_parallelogram hgfe).1]
State after:
no goals

State before:
i : incidence_geometry
a b c d e f g h : point
L M K N O P : line
aL : online a L
dL : online d L
eL : online e L
hL : online h L
bM : online b M
cM : online c M
fM : online f M
gM : online g M
aK : online a K
bK : online b K
dN : online d N
cN : online c N
eO : online e O
fO : online f O
hP : online h P
gP : online g P
pLM : para L M
pKN : para K N
pOP : para O P
hlen : length b c = length f g
S : line
cS : online c S
eS : online e S
aPd : diffside b h S
bc : b ≠ c
Q : line
bQ : online b Q
eQ : online e Q
R : line
cR : online c R
hR : online h R
ec : e ≠ c
ehgf : paragram e h g f L P M O
this✝¹ : length b c = length e h
pQR : para Q R
eq1 : area b a d + area d b c = area c h e + area e c b
eq2 : area e b c + area c e h = area h g f + area f h e
abcd : paragram a b c d K M N L
hgfe : paragram h g f e P M O L
this✝ : area a b c = area a c d
this : area f g h = area e f h
⊢ 2 * area a b c = area f g h + area e f h
Tactic:
linperm [(area_of_parallelogram abcd).2]
State after:
no goals