internlm/Lean-Github huggingface dataset:
Theorem: eq_of_parallelogram_of_eq_basis
Proof 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
⊢ area a b c + area a d c = area e f g + area e h g
Tactic:
have bcda: paragram b c d a M N L K := by splitAll <;> perma only [para]
Proof state after:
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
bcda : paragram b c d a M N L K
⊢ area a b c + area a d c = area e f g + area e h g
Theorem: eq_of_parallelogram_of_eq_basis
Proof 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
bcda : paragram b c d a M N L K
⊢ area a b c + area a d c = area e f g + area e h g
Tactic:
have fghe: paragram f g h e M P L O := by splitAll <;> perma only [para]
Proof state after:
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
bcda : paragram b c d a M N L K
fghe : paragram f g h e M P L O
⊢ area a b c + area a d c = area e f g + area e h g
Theorem: eq_of_parallelogram_of_eq_basis
Proof 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
bcda : paragram b c d a M N L K
fghe : paragram f g h e M P L O
⊢ area a b c + area a d c = area e f g + area e h g
Tactic:
have fg_he := (len_ang_area_eq_of_parallelogram fghe).1
Proof state after:
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
bcda : paragram b c d a M N L K
fghe : paragram f g h e M P L O
fg_he : length f g = length h e
⊢ area a b c + area a d c = area e f g + area e h g
Theorem: eq_of_parallelogram_of_eq_basis
Proof 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
bcda : paragram b c d a M N L K
fghe : paragram f g h e M P L O
fg_he : length f g = length h e
⊢ area a b c + area a d c = area e f g + area e h g
Tactic:
by_cases bc: b = c
Proof state after:
case pos
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
bcda : paragram b c d a M N L K
fghe : paragram f g h e M P L O
fg_he : length f g = length h e
bc : b = c
⊢ area a b c + area a d c = area e f g + area e h g

case neg
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
bcda : paragram b c d a M N L K
fghe : paragram f g h e M P L O
fg_he : length f g = length h e
bc : ¬b = c
⊢ area a b c + area a d c = area e f g + area e h g
Theorem: eq_of_parallelogram_of_eq_basis
Proof 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
⊢ paragram b c d a M N L K
Tactic:
splitAll <;> perma only [para]
Proof state after:
no goals
Theorem: eq_of_parallelogram_of_eq_basis
Proof 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
bcda : paragram b c d a M N L K
⊢ paragram f g h e M P L O
Tactic:
splitAll <;> perma only [para]
Proof state after:
no goals
Theorem: eq_of_parallelogram_of_eq_basis
Proof state before:
case pos
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
bcda : paragram b c d a M N L K
fghe : paragram f g h e M P L O
fg_he : length f g = length h e
bc : b = c
⊢ area a b c + area a d c = area e f g + area e h g
Tactic:
have hg := (same_len_pts_coincide_iff hlen).mp bc
Proof state after:
case pos
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
bcda : paragram b c d a M N L K
fghe : paragram f g h e M P L O
fg_he : length f g = length h e
bc : b = c
hg : f = g
⊢ area a b c + area a d c = area e f g + area e h g
Theorem: eq_of_parallelogram_of_eq_basis
Proof state before:
case pos
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
bcda : paragram b c d a M N L K
fghe : paragram f g h e M P L O
fg_he : length f g = length h e
bc : b = c
hg : f = g
⊢ area a b c + area a d c = area e f g + area e h g
Tactic:
have he := (same_len_pts_coincide_iff fg_he).mp hg
Proof state after:
case pos
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
bcda : paragram b c d a M N L K
fghe : paragram f g h e M P L O
fg_he : length f g = length h e
bc : b = c
hg : f = g
he : h = e
⊢ area a b c + area a d c = area e f g + area e h g
Theorem: eq_of_parallelogram_of_eq_basis
Proof state before:
case pos
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
bcda : paragram b c d a M N L K
fghe : paragram f g h e M P L O
fg_he : length f g = length h e
bc : b = c
hg : f = g
he : h = e
⊢ area a b c + area a d c = area e f g + area e h g
Tactic:
have da := (same_len_pts_coincide_iff (len_ang_area_eq_of_parallelogram bcda).1).mp bc
Proof state after:
case pos
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
bcda : paragram b c d a M N L K
fghe : paragram f g h e M P L O
fg_he : length f g = length h e
bc : b = c
hg : f = g
he : h = e
da : d = a
⊢ area a b c + area a d c = area e f g + area e h g
Theorem: eq_of_parallelogram_of_eq_basis
Proof state before:
case pos
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
bcda : paragram b c d a M N L K
fghe : paragram f g h e M P L O
fg_he : length f g = length h e
bc : b = c
hg : f = g
he : h = e
da : d = a
⊢ area a b c + area a d c = area e f g + area e h g
Tactic:
conv in (occs := *) area _ _ _ => all_goals rw [area_of_eq _ _ _ (by tauto)]
Proof state after:
no goals
Theorem: eq_of_parallelogram_of_eq_basis
Proof 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
bcda : paragram b c d a M N L K
fghe : paragram f g h e M P L O
fg_he : length f g = length h e
bc : b = c
hg : f = g
he : h = e
da : d = a
⊢ e = h ∨ e = g ∨ h = g
Tactic:
tauto
Proof state after:
no goals
Theorem: eq_of_parallelogram_of_eq_basis
Proof state before:
case neg
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
bcda : paragram b c d a M N L K
fghe : paragram f g h e M P L O
fg_he : length f g = length h e
bc : ¬b = c
⊢ area a b c + area a d c = area e f g + area e h g
Tactic:
rw [(Ne.def b c).symm] at bc
Proof state after:
case neg
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
bcda : paragram b c d a M N L K
fghe : paragram f g h e M P L O
fg_he : length f g = length h e
bc : b ≠ c
⊢ area a b c + area a d c = area e f g + area e h g
Theorem: eq_of_parallelogram_of_eq_basis
Proof state before:
case neg
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
bcda : paragram b c d a M N L K
fghe : paragram f g h e M P L O
fg_he : length f g = length h e
bc : b ≠ c
⊢ area a b c + area a d c = area e f g + area e h g
Tactic:
have he : h ≠ e := ne_of_ne_len bc (hlen.trans fg_he)
Proof state after:
case neg
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
bcda : paragram b c d a M N L K
fghe : paragram f g h e M P L O
fg_he : length f g = length h e
bc : b ≠ c
he : h ≠ e
⊢ area a b c + area a d c = area e f g + area e h g
Theorem: eq_of_parallelogram_of_eq_basis
Proof state before:
case neg
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
bcda : paragram b c d a M N L K
fghe : paragram f g h e M P L O
fg_he : length f g = length h e
bc : b ≠ c
he : h ≠ e
⊢ area a b c + area a d c = area e f g + area e h g
Tactic:
obtain ⟨ S, cS, eS ⟩ := line_of_pts c e
Proof state after:
case neg.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
bcda : paragram b c d a M N L K
fghe : paragram f g h e M P L O
fg_he : length f g = length h e
bc : b ≠ c
he : h ≠ e
S : line
cS : online c S
eS : online e S
⊢ area a b c + area a d c = area e f g + area e h g
Theorem: eq_of_parallelogram_of_eq_basis
Proof state before:
case neg.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
bcda : paragram b c d a M N L K
fghe : paragram f g h e M P L O
fg_he : length f g = length h e
bc : b ≠ c
he : h ≠ e
S : line
cS : online c S
eS : online e S
⊢ 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
Proof state after:
case neg.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
bcda : paragram b c d a M N L K
fghe : paragram f g h e M P L O
fg_he : length f g = length h e
bc : b ≠ c
he : h ≠ e
S : line
cS : online c S
eS : online e S
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
Theorem: eq_of_parallelogram_of_eq_basis
Proof state before:
case neg.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
bcda : paragram b c d a M N L K
fghe : paragram f g h e M P L O
fg_he : length f g = length h e
bc : b ≠ c
he : h ≠ e
S : line
cS : online c S
eS : online e S
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:
have aPd := diffside_of_trapezoid hL eL eQ bQ bM cM eS cS pLM ⟨ he, bc ⟩
Proof state after:
case neg.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
bcda : paragram b c d a M N L K
fghe : paragram f g h e M P L O
fg_he : length f g = length h e
bc : b ≠ c
he : h ≠ e
S : line
cS : online c S
eS : online e S
Q : line
bQ : online b Q
eQ : online e Q
aPd : diffside h b S ∨ diffside h c Q
⊢ area a b c + area a d c = area e f g + area e h g
Theorem: eq_of_parallelogram_of_eq_basis
Proof state before:
case neg.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
bcda : paragram b c d a M N L K
fghe : paragram f g h e M P L O
fg_he : length f g = length h e
bc : b ≠ c
he : h ≠ e
S : line
cS : online c S
eS : online e S
Q : line
bQ : online b Q
eQ : online e Q
aPd : diffside h b S ∨ diffside h c Q
⊢ area a b c + area a d c = area e f g + area e h g
Tactic:
cases aPd with
| inl aPd =>
  exact eq_of_parallelogram_of_eq_basis_of_diffside aL dL eL hL bM cM fM gM aK bK dN cN eO fO hP gP pLM pKN pOP hlen cS eS (diffside_symm aPd) bc
| inr aPd =>
  rw [← eq_of_parallelogram_of_eq_basis_of_diffside dL aL eL hL cM bM fM gM dN cN aK bK eO fO hP gP pLM (para_symm pKN) pOP (by perma) bQ eQ (diffside_symm aPd) bc.symm]
  perm [(area_of_parallelogram bcda).1]; rw [this]
  perm [(area_of_parallelogram bcda).2]; rw [this]
Proof state after:
no goals
Theorem: eq_of_parallelogram_of_eq_basis
Proof state before:
case neg.intro.intro.intro.intro.inl
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
bcda : paragram b c d a M N L K
fghe : paragram f g h e M P L O
fg_he : length f g = length h e
bc : b ≠ c
he : h ≠ e
S : line
cS : online c S
eS : online e S
Q : line
bQ : online b Q
eQ : online e Q
aPd : diffside h b S
⊢ area a b c + area a d c = area e f g + area e h g
Tactic:
exact eq_of_parallelogram_of_eq_basis_of_diffside aL dL eL hL bM cM fM gM aK bK dN cN eO fO hP gP pLM pKN pOP hlen cS eS (diffside_symm aPd) bc
Proof state after:
no goals
Theorem: eq_of_parallelogram_of_eq_basis
Proof state before:
case neg.intro.intro.intro.intro.inr
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
bcda : paragram b c d a M N L K
fghe : paragram f g h e M P L O
fg_he : length f g = length h e
bc : b ≠ c
he : h ≠ e
S : line
cS : online c S
eS : online e S
Q : line
bQ : online b Q
eQ : online e Q
aPd : diffside h c Q
⊢ area a b c + area a d c = area e f g + area e h g
Tactic:
rw [← eq_of_parallelogram_of_eq_basis_of_diffside dL aL eL hL cM bM fM gM dN cN aK bK eO fO hP gP pLM (para_symm pKN) pOP (by perma) bQ eQ (diffside_symm aPd) bc.symm]
Proof state after:
case neg.intro.intro.intro.intro.inr
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
bcda : paragram b c d a M N L K
fghe : paragram f g h e M P L O
fg_he : length f g = length h e
bc : b ≠ c
he : h ≠ e
S : line
cS : online c S
eS : online e S
Q : line
bQ : online b Q
eQ : online e Q
aPd : diffside h c Q
⊢ area a b c + area a d c = area d c b + area d a b
Theorem: eq_of_parallelogram_of_eq_basis
Proof state before:
case neg.intro.intro.intro.intro.inr
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
bcda : paragram b c d a M N L K
fghe : paragram f g h e M P L O
fg_he : length f g = length h e
bc : b ≠ c
he : h ≠ e
S : line
cS : online c S
eS : online e S
Q : line
bQ : online b Q
eQ : online e Q
aPd : diffside h c Q
⊢ area a b c + area a d c = area d c b + area d a b
Tactic:
perm [(area_of_parallelogram bcda).1]
Proof state after:
case neg.intro.intro.intro.intro.inr
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
bcda : paragram b c d a M N L K
fghe : paragram f g h e M P L O
fg_he : length f g = length h e
bc : b ≠ c
he : h ≠ e
S : line
cS : online c S
eS : online e S
Q : line
bQ : online b Q
eQ : online e Q
aPd : diffside h c Q
this : area b c d + area a b d = 2 * area b c d
⊢ area a b c + area a c d = area b c d + area a b d