internlm/Lean-Github huggingface dataset:
Theorem: para_trans
Proof state before:
case pos
i : incidence_geometry
L M N : line
pLM : para L M
pLN : para L N
MN : ¬M = N
npMN : ¬M = N ∧ ¬para M N
c : point
cM : online c M
cN : online c N
cL : ¬online c L
d : point
dL : online d L
O : line
cO : online c O
dO : online d O
cd : c ≠ d
LO : L ≠ O
α : circle
Hα : center_circle c α ∧ on_circle d α
cα : in_circle c α
αM : line_circle_inter M α
αN : line_circle_inter N α
a a' : point
aa' : a ≠ a'
aM : online a M
a'M : online a' M
aα : on_circle a α ∧ on_circle a' α
b b' : point
bb' : b ≠ b'
bN : online b N
b'N : online b' N
bα : on_circle b α ∧ on_circle b' α
Baca' : B a c a'
Bbcb' : B b c b'
ac : a ≠ c
bc : b ≠ c
b'c : b' ≠ c
aO : ¬online a O
bO : ¬online b O
b'O : ¬online b' O
aN : ¬online a N
bM : ¬online b M
b'M : ¬online b' M
NO : N ≠ O
MO : M ≠ O
ssbaO : sameside b a O
ssabO : sameside a b O
ss1 : ¬sameside d a N → sameside d b M
ss2 : sameside d a N → ¬sameside d b M
ss : sameside d a N ∨ sameside d b M
e0 : point
e0d : e0 ≠ d
β : circle
hβ : center_circle d β ∧ on_circle e0 β
dβ : in_circle d β
βL : line_circle_inter L β
e e' : point
ee' : e ≠ e'
eL : online e L
e'L : online e' L
eβ : on_circle e β ∧ on_circle e' β
Bede' : B e d e'
ed : e ≠ d
e'd : e' ≠ d
hneO : ¬online e O
hne'O : ¬online e' O
nsaeO : sameside a e' O
nse'eO : ¬sameside e' e O
dsaeO : diffside a e O
dsbeO : diffside b e O
acd : angle a c d = angle c d e
⊢ False
Tactic:
have bcd := alternate_eq_of_para bN cN cO dO dL eL dsbeO (para_symm pLN)
Proof state after:
case pos
i : incidence_geometry
L M N : line
pLM : para L M
pLN : para L N
MN : ¬M = N
npMN : ¬M = N ∧ ¬para M N
c : point
cM : online c M
cN : online c N
cL : ¬online c L
d : point
dL : online d L
O : line
cO : online c O
dO : online d O
cd : c ≠ d
LO : L ≠ O
α : circle
Hα : center_circle c α ∧ on_circle d α
cα : in_circle c α
αM : line_circle_inter M α
αN : line_circle_inter N α
a a' : point
aa' : a ≠ a'
aM : online a M
a'M : online a' M
aα : on_circle a α ∧ on_circle a' α
b b' : point
bb' : b ≠ b'
bN : online b N
b'N : online b' N
bα : on_circle b α ∧ on_circle b' α
Baca' : B a c a'
Bbcb' : B b c b'
ac : a ≠ c
bc : b ≠ c
b'c : b' ≠ c
aO : ¬online a O
bO : ¬online b O
b'O : ¬online b' O
aN : ¬online a N
bM : ¬online b M
b'M : ¬online b' M
NO : N ≠ O
MO : M ≠ O
ssbaO : sameside b a O
ssabO : sameside a b O
ss1 : ¬sameside d a N → sameside d b M
ss2 : sameside d a N → ¬sameside d b M
ss : sameside d a N ∨ sameside d b M
e0 : point
e0d : e0 ≠ d
β : circle
hβ : center_circle d β ∧ on_circle e0 β
dβ : in_circle d β
βL : line_circle_inter L β
e e' : point
ee' : e ≠ e'
eL : online e L
e'L : online e' L
eβ : on_circle e β ∧ on_circle e' β
Bede' : B e d e'
ed : e ≠ d
e'd : e' ≠ d
hneO : ¬online e O
hne'O : ¬online e' O
nsaeO : sameside a e' O
nse'eO : ¬sameside e' e O
dsaeO : diffside a e O
dsbeO : diffside b e O
acd : angle a c d = angle c d e
bcd : angle b c d = angle c d e
⊢ False
Theorem: para_trans
Proof state before:
case pos
i : incidence_geometry
L M N : line
pLM : para L M
pLN : para L N
MN : ¬M = N
npMN : ¬M = N ∧ ¬para M N
c : point
cM : online c M
cN : online c N
cL : ¬online c L
d : point
dL : online d L
O : line
cO : online c O
dO : online d O
cd : c ≠ d
LO : L ≠ O
α : circle
Hα : center_circle c α ∧ on_circle d α
cα : in_circle c α
αM : line_circle_inter M α
αN : line_circle_inter N α
a a' : point
aa' : a ≠ a'
aM : online a M
a'M : online a' M
aα : on_circle a α ∧ on_circle a' α
b b' : point
bb' : b ≠ b'
bN : online b N
b'N : online b' N
bα : on_circle b α ∧ on_circle b' α
Baca' : B a c a'
Bbcb' : B b c b'
ac : a ≠ c
bc : b ≠ c
b'c : b' ≠ c
aO : ¬online a O
bO : ¬online b O
b'O : ¬online b' O
aN : ¬online a N
bM : ¬online b M
b'M : ¬online b' M
NO : N ≠ O
MO : M ≠ O
ssbaO : sameside b a O
ssabO : sameside a b O
ss1 : ¬sameside d a N → sameside d b M
ss2 : sameside d a N → ¬sameside d b M
ss : sameside d a N ∨ sameside d b M
e0 : point
e0d : e0 ≠ d
β : circle
hβ : center_circle d β ∧ on_circle e0 β
dβ : in_circle d β
βL : line_circle_inter L β
e e' : point
ee' : e ≠ e'
eL : online e L
e'L : online e' L
eβ : on_circle e β ∧ on_circle e' β
Bede' : B e d e'
ed : e ≠ d
e'd : e' ≠ d
hneO : ¬online e O
hne'O : ¬online e' O
nsaeO : sameside a e' O
nse'eO : ¬sameside e' e O
dsaeO : diffside a e O
dsbeO : diffside b e O
acd : angle a c d = angle c d e
bcd : angle b c d = angle c d e
⊢ False
Tactic:
cases ss with
| inl ssdaN =>
  have sum := (angle_add_iff_sameside bc.symm cd cN bN cO dO aO aN NO).2 ⟨sameside_symm ssabO, ssdaN⟩
  rw [acd, bcd, self_eq_add_left] at sum
  exact aN ((angle_zero_iff_online bc.symm ac.symm cN bN).2 sum).1
| inr ssdbM =>
  have sum := (angle_add_iff_sameside ac.symm cd cM aM cO dO bO bM MO).2 ⟨ssabO, ssdbM⟩
  rw [acd, bcd, self_eq_add_left] at sum;
  exact bM ((angle_zero_iff_online ac.symm bc.symm cM aM).2 sum).1
Proof state after:
no goals
Theorem: para_trans
Proof state before:
case pos.inl
i : incidence_geometry
L M N : line
pLM : para L M
pLN : para L N
MN : ¬M = N
npMN : ¬M = N ∧ ¬para M N
c : point
cM : online c M
cN : online c N
cL : ¬online c L
d : point
dL : online d L
O : line
cO : online c O
dO : online d O
cd : c ≠ d
LO : L ≠ O
α : circle
Hα : center_circle c α ∧ on_circle d α
cα : in_circle c α
αM : line_circle_inter M α
αN : line_circle_inter N α
a a' : point
aa' : a ≠ a'
aM : online a M
a'M : online a' M
aα : on_circle a α ∧ on_circle a' α
b b' : point
bb' : b ≠ b'
bN : online b N
b'N : online b' N
bα : on_circle b α ∧ on_circle b' α
Baca' : B a c a'
Bbcb' : B b c b'
ac : a ≠ c
bc : b ≠ c
b'c : b' ≠ c
aO : ¬online a O
bO : ¬online b O
b'O : ¬online b' O
aN : ¬online a N
bM : ¬online b M
b'M : ¬online b' M
NO : N ≠ O
MO : M ≠ O
ssbaO : sameside b a O
ssabO : sameside a b O
ss1 : ¬sameside d a N → sameside d b M
ss2 : sameside d a N → ¬sameside d b M
e0 : point
e0d : e0 ≠ d
β : circle
hβ : center_circle d β ∧ on_circle e0 β
dβ : in_circle d β
βL : line_circle_inter L β
e e' : point
ee' : e ≠ e'
eL : online e L
e'L : online e' L
eβ : on_circle e β ∧ on_circle e' β
Bede' : B e d e'
ed : e ≠ d
e'd : e' ≠ d
hneO : ¬online e O
hne'O : ¬online e' O
nsaeO : sameside a e' O
nse'eO : ¬sameside e' e O
dsaeO : diffside a e O
dsbeO : diffside b e O
acd : angle a c d = angle c d e
bcd : angle b c d = angle c d e
ssdaN : sameside d a N
⊢ False
Tactic:
have sum := (angle_add_iff_sameside bc.symm cd cN bN cO dO aO aN NO).2 ⟨sameside_symm ssabO, ssdaN⟩
Proof state after:
case pos.inl
i : incidence_geometry
L M N : line
pLM : para L M
pLN : para L N
MN : ¬M = N
npMN : ¬M = N ∧ ¬para M N
c : point
cM : online c M
cN : online c N
cL : ¬online c L
d : point
dL : online d L
O : line
cO : online c O
dO : online d O
cd : c ≠ d
LO : L ≠ O
α : circle
Hα : center_circle c α ∧ on_circle d α
cα : in_circle c α
αM : line_circle_inter M α
αN : line_circle_inter N α
a a' : point
aa' : a ≠ a'
aM : online a M
a'M : online a' M
aα : on_circle a α ∧ on_circle a' α
b b' : point
bb' : b ≠ b'
bN : online b N
b'N : online b' N
bα : on_circle b α ∧ on_circle b' α
Baca' : B a c a'
Bbcb' : B b c b'
ac : a ≠ c
bc : b ≠ c
b'c : b' ≠ c
aO : ¬online a O
bO : ¬online b O
b'O : ¬online b' O
aN : ¬online a N
bM : ¬online b M
b'M : ¬online b' M
NO : N ≠ O
MO : M ≠ O
ssbaO : sameside b a O
ssabO : sameside a b O
ss1 : ¬sameside d a N → sameside d b M
ss2 : sameside d a N → ¬sameside d b M
e0 : point
e0d : e0 ≠ d
β : circle
hβ : center_circle d β ∧ on_circle e0 β
dβ : in_circle d β
βL : line_circle_inter L β
e e' : point
ee' : e ≠ e'
eL : online e L
e'L : online e' L
eβ : on_circle e β ∧ on_circle e' β
Bede' : B e d e'
ed : e ≠ d
e'd : e' ≠ d
hneO : ¬online e O
hne'O : ¬online e' O
nsaeO : sameside a e' O
nse'eO : ¬sameside e' e O
dsaeO : diffside a e O
dsbeO : diffside b e O
acd : angle a c d = angle c d e
bcd : angle b c d = angle c d e
ssdaN : sameside d a N
sum : angle b c d = angle b c a + angle a c d
⊢ False
Theorem: para_trans
Proof state before:
case pos.inl
i : incidence_geometry
L M N : line
pLM : para L M
pLN : para L N
MN : ¬M = N
npMN : ¬M = N ∧ ¬para M N
c : point
cM : online c M
cN : online c N
cL : ¬online c L
d : point
dL : online d L
O : line
cO : online c O
dO : online d O
cd : c ≠ d
LO : L ≠ O
α : circle
Hα : center_circle c α ∧ on_circle d α
cα : in_circle c α
αM : line_circle_inter M α
αN : line_circle_inter N α
a a' : point
aa' : a ≠ a'
aM : online a M
a'M : online a' M
aα : on_circle a α ∧ on_circle a' α
b b' : point
bb' : b ≠ b'
bN : online b N
b'N : online b' N
bα : on_circle b α ∧ on_circle b' α
Baca' : B a c a'
Bbcb' : B b c b'
ac : a ≠ c
bc : b ≠ c
b'c : b' ≠ c
aO : ¬online a O
bO : ¬online b O
b'O : ¬online b' O
aN : ¬online a N
bM : ¬online b M
b'M : ¬online b' M
NO : N ≠ O
MO : M ≠ O
ssbaO : sameside b a O
ssabO : sameside a b O
ss1 : ¬sameside d a N → sameside d b M
ss2 : sameside d a N → ¬sameside d b M
e0 : point
e0d : e0 ≠ d
β : circle
hβ : center_circle d β ∧ on_circle e0 β
dβ : in_circle d β
βL : line_circle_inter L β
e e' : point
ee' : e ≠ e'
eL : online e L
e'L : online e' L
eβ : on_circle e β ∧ on_circle e' β
Bede' : B e d e'
ed : e ≠ d
e'd : e' ≠ d
hneO : ¬online e O
hne'O : ¬online e' O
nsaeO : sameside a e' O
nse'eO : ¬sameside e' e O
dsaeO : diffside a e O
dsbeO : diffside b e O
acd : angle a c d = angle c d e
bcd : angle b c d = angle c d e
ssdaN : sameside d a N
sum : angle b c d = angle b c a + angle a c d
⊢ False
Tactic:
rw [acd, bcd, self_eq_add_left] at sum
Proof state after:
case pos.inl
i : incidence_geometry
L M N : line
pLM : para L M
pLN : para L N
MN : ¬M = N
npMN : ¬M = N ∧ ¬para M N
c : point
cM : online c M
cN : online c N
cL : ¬online c L
d : point
dL : online d L
O : line
cO : online c O
dO : online d O
cd : c ≠ d
LO : L ≠ O
α : circle
Hα : center_circle c α ∧ on_circle d α
cα : in_circle c α
αM : line_circle_inter M α
αN : line_circle_inter N α
a a' : point
aa' : a ≠ a'
aM : online a M
a'M : online a' M
aα : on_circle a α ∧ on_circle a' α
b b' : point
bb' : b ≠ b'
bN : online b N
b'N : online b' N
bα : on_circle b α ∧ on_circle b' α
Baca' : B a c a'
Bbcb' : B b c b'
ac : a ≠ c
bc : b ≠ c
b'c : b' ≠ c
aO : ¬online a O
bO : ¬online b O
b'O : ¬online b' O
aN : ¬online a N
bM : ¬online b M
b'M : ¬online b' M
NO : N ≠ O
MO : M ≠ O
ssbaO : sameside b a O
ssabO : sameside a b O
ss1 : ¬sameside d a N → sameside d b M
ss2 : sameside d a N → ¬sameside d b M
e0 : point
e0d : e0 ≠ d
β : circle
hβ : center_circle d β ∧ on_circle e0 β
dβ : in_circle d β
βL : line_circle_inter L β
e e' : point
ee' : e ≠ e'
eL : online e L
e'L : online e' L
eβ : on_circle e β ∧ on_circle e' β
Bede' : B e d e'
ed : e ≠ d
e'd : e' ≠ d
hneO : ¬online e O
hne'O : ¬online e' O
nsaeO : sameside a e' O
nse'eO : ¬sameside e' e O
dsaeO : diffside a e O
dsbeO : diffside b e O
acd : angle a c d = angle c d e
bcd : angle b c d = angle c d e
ssdaN : sameside d a N
sum : angle b c a = 0
⊢ False
Theorem: para_trans
Proof state before:
case pos.inl
i : incidence_geometry
L M N : line
pLM : para L M
pLN : para L N
MN : ¬M = N
npMN : ¬M = N ∧ ¬para M N
c : point
cM : online c M
cN : online c N
cL : ¬online c L
d : point
dL : online d L
O : line
cO : online c O
dO : online d O
cd : c ≠ d
LO : L ≠ O
α : circle
Hα : center_circle c α ∧ on_circle d α
cα : in_circle c α
αM : line_circle_inter M α
αN : line_circle_inter N α
a a' : point
aa' : a ≠ a'
aM : online a M
a'M : online a' M
aα : on_circle a α ∧ on_circle a' α
b b' : point
bb' : b ≠ b'
bN : online b N
b'N : online b' N
bα : on_circle b α ∧ on_circle b' α
Baca' : B a c a'
Bbcb' : B b c b'
ac : a ≠ c
bc : b ≠ c
b'c : b' ≠ c
aO : ¬online a O
bO : ¬online b O
b'O : ¬online b' O
aN : ¬online a N
bM : ¬online b M
b'M : ¬online b' M
NO : N ≠ O
MO : M ≠ O
ssbaO : sameside b a O
ssabO : sameside a b O
ss1 : ¬sameside d a N → sameside d b M
ss2 : sameside d a N → ¬sameside d b M
e0 : point
e0d : e0 ≠ d
β : circle
hβ : center_circle d β ∧ on_circle e0 β
dβ : in_circle d β
βL : line_circle_inter L β
e e' : point
ee' : e ≠ e'
eL : online e L
e'L : online e' L
eβ : on_circle e β ∧ on_circle e' β
Bede' : B e d e'
ed : e ≠ d
e'd : e' ≠ d
hneO : ¬online e O
hne'O : ¬online e' O
nsaeO : sameside a e' O
nse'eO : ¬sameside e' e O
dsaeO : diffside a e O
dsbeO : diffside b e O
acd : angle a c d = angle c d e
bcd : angle b c d = angle c d e
ssdaN : sameside d a N
sum : angle b c a = 0
⊢ False
Tactic:
exact aN ((angle_zero_iff_online bc.symm ac.symm cN bN).2 sum).1
Proof state after:
no goals
Theorem: para_trans
Proof state before:
case pos.inr
i : incidence_geometry
L M N : line
pLM : para L M
pLN : para L N
MN : ¬M = N
npMN : ¬M = N ∧ ¬para M N
c : point
cM : online c M
cN : online c N
cL : ¬online c L
d : point
dL : online d L
O : line
cO : online c O
dO : online d O
cd : c ≠ d
LO : L ≠ O
α : circle
Hα : center_circle c α ∧ on_circle d α
cα : in_circle c α
αM : line_circle_inter M α
αN : line_circle_inter N α
a a' : point
aa' : a ≠ a'
aM : online a M
a'M : online a' M
aα : on_circle a α ∧ on_circle a' α
b b' : point
bb' : b ≠ b'
bN : online b N
b'N : online b' N
bα : on_circle b α ∧ on_circle b' α
Baca' : B a c a'
Bbcb' : B b c b'
ac : a ≠ c
bc : b ≠ c
b'c : b' ≠ c
aO : ¬online a O
bO : ¬online b O
b'O : ¬online b' O
aN : ¬online a N
bM : ¬online b M
b'M : ¬online b' M
NO : N ≠ O
MO : M ≠ O
ssbaO : sameside b a O
ssabO : sameside a b O
ss1 : ¬sameside d a N → sameside d b M
ss2 : sameside d a N → ¬sameside d b M
e0 : point
e0d : e0 ≠ d
β : circle
hβ : center_circle d β ∧ on_circle e0 β
dβ : in_circle d β
βL : line_circle_inter L β
e e' : point
ee' : e ≠ e'
eL : online e L
e'L : online e' L
eβ : on_circle e β ∧ on_circle e' β
Bede' : B e d e'
ed : e ≠ d
e'd : e' ≠ d
hneO : ¬online e O
hne'O : ¬online e' O
nsaeO : sameside a e' O
nse'eO : ¬sameside e' e O
dsaeO : diffside a e O
dsbeO : diffside b e O
acd : angle a c d = angle c d e
bcd : angle b c d = angle c d e
ssdbM : sameside d b M
⊢ False
Tactic:
have sum := (angle_add_iff_sameside ac.symm cd cM aM cO dO bO bM MO).2 ⟨ssabO, ssdbM⟩
Proof state after:
case pos.inr
i : incidence_geometry
L M N : line
pLM : para L M
pLN : para L N
MN : ¬M = N
npMN : ¬M = N ∧ ¬para M N
c : point
cM : online c M
cN : online c N
cL : ¬online c L
d : point
dL : online d L
O : line
cO : online c O
dO : online d O
cd : c ≠ d
LO : L ≠ O
α : circle
Hα : center_circle c α ∧ on_circle d α
cα : in_circle c α
αM : line_circle_inter M α
αN : line_circle_inter N α
a a' : point
aa' : a ≠ a'
aM : online a M
a'M : online a' M
aα : on_circle a α ∧ on_circle a' α
b b' : point
bb' : b ≠ b'
bN : online b N
b'N : online b' N
bα : on_circle b α ∧ on_circle b' α
Baca' : B a c a'
Bbcb' : B b c b'
ac : a ≠ c
bc : b ≠ c
b'c : b' ≠ c
aO : ¬online a O
bO : ¬online b O
b'O : ¬online b' O
aN : ¬online a N
bM : ¬online b M
b'M : ¬online b' M
NO : N ≠ O
MO : M ≠ O
ssbaO : sameside b a O
ssabO : sameside a b O
ss1 : ¬sameside d a N → sameside d b M
ss2 : sameside d a N → ¬sameside d b M
e0 : point
e0d : e0 ≠ d
β : circle
hβ : center_circle d β ∧ on_circle e0 β
dβ : in_circle d β
βL : line_circle_inter L β
e e' : point
ee' : e ≠ e'
eL : online e L
e'L : online e' L
eβ : on_circle e β ∧ on_circle e' β
Bede' : B e d e'
ed : e ≠ d
e'd : e' ≠ d
hneO : ¬online e O
hne'O : ¬online e' O
nsaeO : sameside a e' O
nse'eO : ¬sameside e' e O
dsaeO : diffside a e O
dsbeO : diffside b e O
acd : angle a c d = angle c d e
bcd : angle b c d = angle c d e
ssdbM : sameside d b M
sum : angle a c d = angle a c b + angle b c d
⊢ False
Theorem: para_trans
Proof state before:
case pos.inr
i : incidence_geometry
L M N : line
pLM : para L M
pLN : para L N
MN : ¬M = N
npMN : ¬M = N ∧ ¬para M N
c : point
cM : online c M
cN : online c N
cL : ¬online c L
d : point
dL : online d L
O : line
cO : online c O
dO : online d O
cd : c ≠ d
LO : L ≠ O
α : circle
Hα : center_circle c α ∧ on_circle d α
cα : in_circle c α
αM : line_circle_inter M α
αN : line_circle_inter N α
a a' : point
aa' : a ≠ a'
aM : online a M
a'M : online a' M
aα : on_circle a α ∧ on_circle a' α
b b' : point
bb' : b ≠ b'
bN : online b N
b'N : online b' N
bα : on_circle b α ∧ on_circle b' α
Baca' : B a c a'
Bbcb' : B b c b'
ac : a ≠ c
bc : b ≠ c
b'c : b' ≠ c
aO : ¬online a O
bO : ¬online b O
b'O : ¬online b' O
aN : ¬online a N
bM : ¬online b M
b'M : ¬online b' M
NO : N ≠ O
MO : M ≠ O
ssbaO : sameside b a O
ssabO : sameside a b O
ss1 : ¬sameside d a N → sameside d b M
ss2 : sameside d a N → ¬sameside d b M
e0 : point
e0d : e0 ≠ d
β : circle
hβ : center_circle d β ∧ on_circle e0 β
dβ : in_circle d β
βL : line_circle_inter L β
e e' : point
ee' : e ≠ e'
eL : online e L
e'L : online e' L
eβ : on_circle e β ∧ on_circle e' β
Bede' : B e d e'
ed : e ≠ d
e'd : e' ≠ d
hneO : ¬online e O
hne'O : ¬online e' O
nsaeO : sameside a e' O
nse'eO : ¬sameside e' e O
dsaeO : diffside a e O
dsbeO : diffside b e O
acd : angle a c d = angle c d e
bcd : angle b c d = angle c d e
ssdbM : sameside d b M
sum : angle a c d = angle a c b + angle b c d
⊢ False
Tactic:
rw [acd, bcd, self_eq_add_left] at sum
Proof state after:
case pos.inr
i : incidence_geometry
L M N : line
pLM : para L M
pLN : para L N
MN : ¬M = N
npMN : ¬M = N ∧ ¬para M N
c : point
cM : online c M
cN : online c N
cL : ¬online c L
d : point
dL : online d L
O : line
cO : online c O
dO : online d O
cd : c ≠ d
LO : L ≠ O
α : circle
Hα : center_circle c α ∧ on_circle d α
cα : in_circle c α
αM : line_circle_inter M α
αN : line_circle_inter N α
a a' : point
aa' : a ≠ a'
aM : online a M
a'M : online a' M
aα : on_circle a α ∧ on_circle a' α
b b' : point
bb' : b ≠ b'
bN : online b N
b'N : online b' N
bα : on_circle b α ∧ on_circle b' α
Baca' : B a c a'
Bbcb' : B b c b'
ac : a ≠ c
bc : b ≠ c
b'c : b' ≠ c
aO : ¬online a O
bO : ¬online b O
b'O : ¬online b' O
aN : ¬online a N
bM : ¬online b M
b'M : ¬online b' M
NO : N ≠ O
MO : M ≠ O
ssbaO : sameside b a O
ssabO : sameside a b O
ss1 : ¬sameside d a N → sameside d b M
ss2 : sameside d a N → ¬sameside d b M
e0 : point
e0d : e0 ≠ d
β : circle
hβ : center_circle d β ∧ on_circle e0 β
dβ : in_circle d β
βL : line_circle_inter L β
e e' : point
ee' : e ≠ e'
eL : online e L
e'L : online e' L
eβ : on_circle e β ∧ on_circle e' β
Bede' : B e d e'
ed : e ≠ d
e'd : e' ≠ d
hneO : ¬online e O
hne'O : ¬online e' O
nsaeO : sameside a e' O
nse'eO : ¬sameside e' e O
dsaeO : diffside a e O
dsbeO : diffside b e O
acd : angle a c d = angle c d e
bcd : angle b c d = angle c d e
ssdbM : sameside d b M
sum : angle a c b = 0
⊢ False
Theorem: para_trans
Proof state before:
case pos.inr
i : incidence_geometry
L M N : line
pLM : para L M
pLN : para L N
MN : ¬M = N
npMN : ¬M = N ∧ ¬para M N
c : point
cM : online c M
cN : online c N
cL : ¬online c L
d : point
dL : online d L
O : line
cO : online c O
dO : online d O
cd : c ≠ d
LO : L ≠ O
α : circle
Hα : center_circle c α ∧ on_circle d α
cα : in_circle c α
αM : line_circle_inter M α
αN : line_circle_inter N α
a a' : point
aa' : a ≠ a'
aM : online a M
a'M : online a' M
aα : on_circle a α ∧ on_circle a' α
b b' : point
bb' : b ≠ b'
bN : online b N
b'N : online b' N
bα : on_circle b α ∧ on_circle b' α
Baca' : B a c a'
Bbcb' : B b c b'
ac : a ≠ c
bc : b ≠ c
b'c : b' ≠ c
aO : ¬online a O
bO : ¬online b O
b'O : ¬online b' O
aN : ¬online a N
bM : ¬online b M
b'M : ¬online b' M
NO : N ≠ O
MO : M ≠ O
ssbaO : sameside b a O
ssabO : sameside a b O
ss1 : ¬sameside d a N → sameside d b M
ss2 : sameside d a N → ¬sameside d b M
e0 : point
e0d : e0 ≠ d
β : circle
hβ : center_circle d β ∧ on_circle e0 β
dβ : in_circle d β
βL : line_circle_inter L β
e e' : point
ee' : e ≠ e'
eL : online e L
e'L : online e' L
eβ : on_circle e β ∧ on_circle e' β
Bede' : B e d e'
ed : e ≠ d
e'd : e' ≠ d
hneO : ¬online e O
hne'O : ¬online e' O
nsaeO : sameside a e' O
nse'eO : ¬sameside e' e O
dsaeO : diffside a e O
dsbeO : diffside b e O
acd : angle a c d = angle c d e
bcd : angle b c d = angle c d e
ssdbM : sameside d b M
sum : angle a c b = 0
⊢ False
Tactic:
exact bM ((angle_zero_iff_online ac.symm bc.symm cM aM).2 sum).1
Proof state after:
no goals
Theorem: area_of_eq
Proof state before:
i : incidence_geometry
a b c : point
h : a = b ∨ a = c ∨ b = c
⊢ area a b c = 0
Tactic:
cases h with
| inl ab => rw [ab]; exact degenerate_area b c
| inr h => cases h with
  | inl ac => rw [ac, ar132]; exact degenerate_area c b
  | inr bc => rw [bc, ar321]; exact degenerate_area c a
Proof state after:
no goals
Theorem: area_of_eq
Proof state before:
case inl
i : incidence_geometry
a b c : point
ab : a = b
⊢ area a b c = 0
Tactic:
rw [ab]
Proof state after:
case inl
i : incidence_geometry
a b c : point
ab : a = b
⊢ area b b c = 0
Theorem: area_of_eq
Proof state before:
case inl
i : incidence_geometry
a b c : point
ab : a = b
⊢ area b b c = 0
Tactic:
exact degenerate_area b c
Proof state after:
no goals
Theorem: area_of_eq
Proof state before:
case inr
i : incidence_geometry
a b c : point
h : a = c ∨ b = c
⊢ area a b c = 0
Tactic:
cases h with
| inl ac => rw [ac, ar132]; exact degenerate_area c b
| inr bc => rw [bc, ar321]; exact degenerate_area c a
Proof state after:
no goals
Theorem: area_of_eq
Proof state before:
case inr.inl
i : incidence_geometry
a b c : point
ac : a = c
⊢ area a b c = 0
Tactic:
rw [ac, ar132]
Proof state after:
case inr.inl
i : incidence_geometry
a b c : point
ac : a = c
⊢ area c c b = 0
Theorem: area_of_eq
Proof state before:
case inr.inl
i : incidence_geometry
a b c : point
ac : a = c
⊢ area c c b = 0
Tactic:
exact degenerate_area c b
Proof state after:
no goals
Theorem: area_of_eq
Proof state before:
case inr.inr
i : incidence_geometry
a b c : point
bc : b = c
⊢ area a b c = 0
Tactic:
rw [bc, ar321]
Proof state after:
case inr.inr
i : incidence_geometry
a b c : point
bc : b = c
⊢ area c c a = 0
Theorem: area_of_eq
Proof state before:
case inr.inr
i : incidence_geometry
a b c : point
bc : b = c
⊢ area c c a = 0
Tactic:
exact degenerate_area c a
Proof state after:
no goals
Theorem: area_of_parallelogram
Proof state before:
i : incidence_geometry
a b c d : point
L M N O : line
abcd : paragram a b c d L M N O
⊢ area a b c + area a d c = 2 * area a b c ∧ area b a d + area b c d = 2 * area a b c
Tactic:
obtain ⟨ aL, bL, bM, cM, cN, dN, dO, aO, pLN, pMO⟩ := id abcd
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c d : point
L M N O : line
abcd : paragram a b c d L M N O
aL : online a L
bL : online b L
bM : online b M
cM : online c M
cN : online c N
dN : online d N
dO : online d O
aO : online a O
pLN : para L N
pMO : para M O
⊢ area a b c + area a d c = 2 * area a b c ∧ area b a d + area b c d = 2 * area a b c
Theorem: area_of_parallelogram
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c d : point
L M N O : line
abcd : paragram a b c d L M N O
aL : online a L
bL : online b L
bM : online b M
cM : online c M
cN : online c N
dN : online d N
dO : online d O
aO : online a O
pLN : para L N
pMO : para M O
⊢ area a b c + area a d c = 2 * area a b c ∧ area b a d + area b c d = 2 * area a b c
Tactic:
have bcda : paragram b c d a M N O L := by splitAll <;> perma only [para]
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c d : point
L M N O : line
abcd : paragram a b c d L M N O
aL : online a L
bL : online b L
bM : online b M
cM : online c M
cN : online c N
dN : online d N
dO : online d O
aO : online a O
pLN : para L N
pMO : para M O
bcda : paragram b c d a M N O L
⊢ area a b c + area a d c = 2 * area a b c ∧ area b a d + area b c d = 2 * area a b c