internlm/Lean-Github huggingface dataset:
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
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
Tactic:
rw [this]
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 = 2 * area b c d
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
this : area b c d + area a b d = 2 * area b c d
⊢ area a b c + area a c d = 2 * area b c d
Tactic:
perm [(area_of_parallelogram bcda).2]
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
this : area a b c + area a c d = 2 * area b c d
⊢ area a b c + area a c d = 2 * area b c d
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
this✝ : area b c d + area a b d = 2 * area b c d
this : area a b c + area a c d = 2 * area b c d
⊢ area a b c + area a c d = 2 * area b c d
Tactic:
rw [this]
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
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
⊢ length c b = length f g
Tactic:
perma
Proof state after:
no goals
Theorem: eq_area_of_eq_base
Proof 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
Proof 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
Theorem: eq_area_of_eq_base
Proof 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
Proof 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
Theorem: eq_area_of_eq_base
Proof 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
Proof 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
Theorem: eq_area_of_eq_base
Proof 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
Proof 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
Theorem: eq_area_of_eq_base
Proof 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)
Proof 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
Theorem: eq_area_of_eq_base
Proof 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)
Proof 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
Theorem: eq_area_of_eq_base
Proof 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
Proof 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
Theorem: eq_area_of_eq_base
Proof 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)
Proof 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
Theorem: eq_area_of_eq_base
Proof 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
Proof 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
Theorem: eq_area_of_eq_base
Proof 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
Proof 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
Theorem: eq_area_of_eq_base
Proof 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]
Proof 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
Theorem: eq_area_of_eq_base
Proof 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]
Proof 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
Theorem: eq_area_of_eq_base
Proof 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]
Proof 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
Theorem: eq_area_of_eq_base
Proof 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]
Proof 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
Theorem: eq_area_of_eq_base
Proof 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]
Proof 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
Theorem: eq_area_of_eq_base
Proof 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
Proof state after:
no goals
Theorem: eq_area_of_eq_base
Proof 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
Proof 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