internlm/Lean-Github huggingface dataset:
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
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)]
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
bc : b = c
ef : e = f
⊢ a = b ∨ a = c ∨ b = c
Tactic:
tauto
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
bc : b = c
ef : e = f
⊢ d = e ∨ d = f ∨ e = f
Tactic:
tauto
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
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
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
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
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
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]
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
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]
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
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]
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
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]
Proof state after:
no goals
Theorem: eq_area_of_eq_base_samevertex
Proof state before:
i : incidence_geometry
a b c e f : point
L : line
bL : online b L
cL : online c L
eL : online e L
fL : online f L
hlen : length b c = length e f
⊢ area a b c = area a e f
Tactic:
by_cases bc : b = c
Proof state after:
case pos
i : incidence_geometry
a b c e f : point
L : line
bL : online b L
cL : online c L
eL : online e L
fL : online f L
hlen : length b c = length e f
bc : b = c
⊢ area a b c = area a e f

case neg
i : incidence_geometry
a b c e f : point
L : line
bL : online b L
cL : online c L
eL : online e L
fL : online f L
hlen : length b c = length e f
bc : ¬b = c
⊢ area a b c = area a e f
Theorem: eq_area_of_eq_base_samevertex
Proof state before:
case neg
i : incidence_geometry
a b c e f : point
L : line
bL : online b L
cL : online c L
eL : online e L
fL : online f L
hlen : length b c = length e f
bc : ¬b = c
⊢ area a b c = area a e f
Tactic:
have ef : e ≠ f := ne_of_ne_len bc hlen
Proof state after:
case neg
i : incidence_geometry
a b c e f : point
L : line
bL : online b L
cL : online c L
eL : online e L
fL : online f L
hlen : length b c = length e f
bc : ¬b = c
ef : e ≠ f
⊢ area a b c = area a e f
Theorem: eq_area_of_eq_base_samevertex
Proof state before:
case neg
i : incidence_geometry
a b c e f : point
L : line
bL : online b L
cL : online c L
eL : online e L
fL : online f L
hlen : length b c = length e f
bc : ¬b = c
ef : e ≠ f
⊢ area a b c = area a e f
Tactic:
by_cases aL : online a L
Proof state after:
case pos
i : incidence_geometry
a b c e f : point
L : line
bL : online b L
cL : online c L
eL : online e L
fL : online f L
hlen : length b c = length e f
bc : ¬b = c
ef : e ≠ f
aL : online a L
⊢ area a b c = area a e f

case neg
i : incidence_geometry
a b c e f : point
L : line
bL : online b L
cL : online c L
eL : online e L
fL : online f L
hlen : length b c = length e f
bc : ¬b = c
ef : e ≠ f
aL : ¬online a L
⊢ area a b c = area a e f
Theorem: eq_area_of_eq_base_samevertex
Proof state before:
case neg
i : incidence_geometry
a b c e f : point
L : line
bL : online b L
cL : online c L
eL : online e L
fL : online f L
hlen : length b c = length e f
bc : ¬b = c
ef : e ≠ f
aL : ¬online a L
⊢ area a b c = area a e f
Tactic:
obtain ⟨ _, hM ⟩ := parallel_of_line_pt aL
Proof state after:
case neg.intro
i : incidence_geometry
a b c e f : point
L : line
bL : online b L
cL : online c L
eL : online e L
fL : online f L
hlen : length b c = length e f
bc : ¬b = c
ef : e ≠ f
aL : ¬online a L
w✝ : line
hM : online a w✝ ∧ para L w✝
⊢ area a b c = area a e f
Theorem: eq_area_of_eq_base_samevertex
Proof state before:
case neg.intro
i : incidence_geometry
a b c e f : point
L : line
bL : online b L
cL : online c L
eL : online e L
fL : online f L
hlen : length b c = length e f
bc : ¬b = c
ef : e ≠ f
aL : ¬online a L
w✝ : line
hM : online a w✝ ∧ para L w✝
⊢ area a b c = area a e f
Tactic:
exact eq_area_of_eq_base hM.1 bL cL hM.1 eL fL hM.2 hlen
Proof state after:
no goals
Theorem: eq_area_of_eq_base_samevertex
Proof state before:
case pos
i : incidence_geometry
a b c e f : point
L : line
bL : online b L
cL : online c L
eL : online e L
fL : online f L
hlen : length b c = length e f
bc : b = c
⊢ area a b c = area a 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 e f : point
L : line
bL : online b L
cL : online c L
eL : online e L
fL : online f L
hlen : length b c = length e f
bc : b = c
ef : e = f
⊢ area a b c = area a e f
Theorem: eq_area_of_eq_base_samevertex
Proof state before:
case pos
i : incidence_geometry
a b c e f : point
L : line
bL : online b L
cL : online c L
eL : online e L
fL : online f L
hlen : length b c = length e f
bc : b = c
ef : e = f
⊢ area a b c = area a e f
Tactic:
rw [area_of_eq a b c (by tauto), area_of_eq a e f (by tauto)]
Proof state after:
no goals
Theorem: eq_area_of_eq_base_samevertex
Proof state before:
i : incidence_geometry
a b c e f : point
L : line
bL : online b L
cL : online c L
eL : online e L
fL : online f L
hlen : length b c = length e f
bc : b = c
ef : e = f
⊢ a = b ∨ a = c ∨ b = c
Tactic:
tauto
Proof state after:
no goals
Theorem: eq_area_of_eq_base_samevertex
Proof state before:
i : incidence_geometry
a b c e f : point
L : line
bL : online b L
cL : online c L
eL : online e L
fL : online f L
hlen : length b c = length e f
bc : b = c
ef : e = f
⊢ a = e ∨ a = f ∨ e = f
Tactic:
tauto
Proof state after:
no goals
Theorem: eq_area_of_eq_base_samevertex
Proof state before:
case pos
i : incidence_geometry
a b c e f : point
L : line
bL : online b L
cL : online c L
eL : online e L
fL : online f L
hlen : length b c = length e f
bc : ¬b = c
ef : e ≠ f
aL : online a L
⊢ area a b c = area a e f
Tactic:
perm [(area_zero_iff_online bc bL cL).mpr aL]
Proof state after:
case pos
i : incidence_geometry
a b c e f : point
L : line
bL : online b L
cL : online c L
eL : online e L
fL : online f L
hlen : length b c = length e f
bc : ¬b = c
ef : e ≠ f
aL : online a L
this : area a b c = 0
⊢ area a b c = area a e f
Theorem: eq_area_of_eq_base_samevertex
Proof state before:
case pos
i : incidence_geometry
a b c e f : point
L : line
bL : online b L
cL : online c L
eL : online e L
fL : online f L
hlen : length b c = length e f
bc : ¬b = c
ef : e ≠ f
aL : online a L
this : area a b c = 0
⊢ area a b c = area a e f
Tactic:
rw [this]
Proof state after:
case pos
i : incidence_geometry
a b c e f : point
L : line
bL : online b L
cL : online c L
eL : online e L
fL : online f L
hlen : length b c = length e f
bc : ¬b = c
ef : e ≠ f
aL : online a L
this : area a b c = 0
⊢ 0 = area a e f
Theorem: eq_area_of_eq_base_samevertex
Proof state before:
case pos
i : incidence_geometry
a b c e f : point
L : line
bL : online b L
cL : online c L
eL : online e L
fL : online f L
hlen : length b c = length e f
bc : ¬b = c
ef : e ≠ f
aL : online a L
this : area a b c = 0
⊢ 0 = area a e f
Tactic:
linperm [(area_zero_iff_online ef eL fL).mpr aL]
Proof state after:
no goals
Theorem: para_implies_eq_area_of_same_base
Proof state before:
i : incidence_geometry
a b c d : point
L M : line
aM : online a M
dM : online d M
bL : online b L
cL : online c L
pLM : para L M
⊢ area a b c = area d b c
Tactic:
exact eq_area_of_eq_base aM bL cL dM bL cL pLM rfl
Proof state after:
no goals
Theorem: tri_sum_contra
Proof state before:
i : incidence_geometry
b c d e : point
O : line
bO : online b O
dO : online d O
eO : online e O
cO : ¬online c O
bd : b ≠ d
de : d ≠ e
eb : e ≠ b
Bbed : B b e d
ar : area b c d = area b c e
⊢ False
Tactic:
apply cO
Proof state after:
i : incidence_geometry
b c d e : point
O : line
bO : online b O
dO : online d O
eO : online e O
cO : ¬online c O
bd : b ≠ d
de : d ≠ e
eb : e ≠ b
Bbed : B b e d
ar : area b c d = area b c e
⊢ online c O
Theorem: tri_sum_contra
Proof state before:
i : incidence_geometry
b c d e : point
O : line
bO : online b O
dO : online d O
eO : online e O
cO : ¬online c O
bd : b ≠ d
de : d ≠ e
eb : e ≠ b
Bbed : B b e d
ar : area b c d = area b c e
⊢ online c O
Tactic:
apply (area_zero_iff_online de dO eO).mp
Proof state after:
i : incidence_geometry
b c d e : point
O : line
bO : online b O
dO : online d O
eO : online e O
cO : ¬online c O
bd : b ≠ d
de : d ≠ e
eb : e ≠ b
Bbed : B b e d
ar : area b c d = area b c e
⊢ area d e c = 0
Theorem: tri_sum_contra
Proof state before:
i : incidence_geometry
b c d e : point
O : line
bO : online b O
dO : online d O
eO : online e O
cO : ¬online c O
bd : b ≠ d
de : d ≠ e
eb : e ≠ b
Bbed : B b e d
ar : area b c d = area b c e
⊢ area d e c = 0
Tactic:
linperm [(area_add_iff_B eb.symm de.symm bd.symm bO eO dO cO).mp Bbed]
Proof state after:
no goals
Theorem: eq_area_of_same_base_implies_para
Proof state before:
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
⊢ para L M
Tactic:
obtain ⟨N, aN, pNL⟩ := para_of_offline aL
Proof state after:
case intro.intro
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
⊢ para L M
Theorem: eq_area_of_same_base_implies_para
Proof state before:
case intro.intro
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
⊢ para L M
Tactic:
have pNO: ¬ para N O := fun pNO => by
  have LO_or_pLO := para_trans (para_symm pNL) pNO
  cases LO_or_pLO with
  | inl LO => rw [← LO] at cO; exact cO cL
  | inr pLO => exact neq_of_para bL bO pLO rfl
Proof state after:
case intro.intro
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : ¬para N O
⊢ para L M
Theorem: eq_area_of_same_base_implies_para
Proof state before:
case intro.intro
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : ¬para N O
⊢ para L M
Tactic:
rcases pt_of_line_line pNO with ⟨e, eN, eO⟩
Proof state after:
case intro.intro.intro.intro
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : ¬para N O
e : point
eN : online e N
eO : online e O
⊢ para L M
Theorem: eq_area_of_same_base_implies_para
Proof state before:
case intro.intro.intro.intro
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : ¬para N O
e : point
eN : online e N
eO : online e O
⊢ para L M
Tactic:
have ar2 := eq_area_of_eq_base aN bL cL eN bL cL pNL rfl
Proof state after:
case intro.intro.intro.intro
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : ¬para N O
e : point
eN : online e N
eO : online e O
ar2 : area a b c = area e b c
⊢ para L M
Theorem: eq_area_of_same_base_implies_para
Proof state before:
case intro.intro.intro.intro
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : ¬para N O
e : point
eN : online e N
eO : online e O
ar2 : area a b c = area e b c
⊢ para L M
Tactic:
rw [ar] at ar2
Proof state after:
case intro.intro.intro.intro
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : ¬para N O
e : point
eN : online e N
eO : online e O
ar2 : area d b c = area e b c
⊢ para L M
Theorem: eq_area_of_same_base_implies_para
Proof state before:
case intro.intro.intro.intro
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : ¬para N O
e : point
eN : online e N
eO : online e O
ar2 : area d b c = area e b c
⊢ para L M
Tactic:
have be := neq_of_para bL eN pNL
Proof state after:
case intro.intro.intro.intro
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : ¬para N O
e : point
eN : online e N
eO : online e O
ar2 : area d b c = area e b c
be : b ≠ e
⊢ para L M
Theorem: eq_area_of_same_base_implies_para
Proof state before:
case intro.intro.intro.intro
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : ¬para N O
e : point
eN : online e N
eO : online e O
ar2 : area d b c = area e b c
be : b ≠ e
⊢ para L M
Tactic:
by_cases de: d = e
Proof state after:
case pos
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : ¬para N O
e : point
eN : online e N
eO : online e O
ar2 : area d b c = area e b c
be : b ≠ e
de : d = e
⊢ para L M

case neg
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : ¬para N O
e : point
eN : online e N
eO : online e O
ar2 : area d b c = area e b c
be : b ≠ e
de : ¬d = e
⊢ para L M
Theorem: eq_area_of_same_base_implies_para
Proof state before:
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : para N O
⊢ False
Tactic:
have LO_or_pLO := para_trans (para_symm pNL) pNO
Proof state after:
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : para N O
LO_or_pLO : L = O ∨ para L O
⊢ False
Theorem: eq_area_of_same_base_implies_para
Proof state before:
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : para N O
LO_or_pLO : L = O ∨ para L O
⊢ False
Tactic:
cases LO_or_pLO with
| inl LO => rw [← LO] at cO; exact cO cL
| inr pLO => exact neq_of_para bL bO pLO rfl
Proof state after:
no goals
Theorem: eq_area_of_same_base_implies_para
Proof state before:
case inl
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : para N O
LO : L = O
⊢ False
Tactic:
rw [← LO] at cO
Proof state after:
case inl
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c L
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : para N O
LO : L = O
⊢ False
Theorem: eq_area_of_same_base_implies_para
Proof state before:
case inl
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c L
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : para N O
LO : L = O
⊢ False
Tactic:
exact cO cL
Proof state after:
no goals
Theorem: eq_area_of_same_base_implies_para
Proof state before:
case inr
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : para N O
pLO : para L O
⊢ False
Tactic:
exact neq_of_para bL bO pLO rfl
Proof state after:
no goals
Theorem: eq_area_of_same_base_implies_para
Proof state before:
case pos
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : ¬para N O
e : point
eN : online e N
eO : online e O
ar2 : area d b c = area e b c
be : b ≠ e
de : d = e
⊢ para L M
Tactic:
rw [← de] at eN
Proof state after:
case pos
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : ¬para N O
e : point
eN : online d N
eO : online e O
ar2 : area d b c = area e b c
be : b ≠ e
de : d = e
⊢ para L M