internlm/Lean-Github huggingface dataset:
Theorem: para_trans
Proof state before:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
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
⊢ False
Tactic:
have MO : M ≠ O := fun MO => aO (by rwa [MO] at aM)
Proof state after:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
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
⊢ False
Theorem: para_trans
Proof state before:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
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
⊢ False
Tactic:
by_cases ssbaO: sameside b a O
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
⊢ False

case neg
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
⊢ 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
⊢ M = N ∨ para M N
Tactic:
tauto
Proof state after:
no goals
Theorem: para_trans
Proof state before:
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
⊢ online c L
Tactic:
rwa [← LO] at cO
Proof state after:
no goals
Theorem: para_trans
Proof state before:
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
⊢ para L O
Tactic:
rwa [← line_unique_of_pts ac aO cO aM cM] at pLM
Proof state after:
no goals
Theorem: para_trans
Proof state before:
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
⊢ para L O
Tactic:
rwa [← line_unique_of_pts bc bO cO bN cN] at pLN
Proof state after:
no goals
Theorem: para_trans
Proof state before:
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
hb'O : online b' O
⊢ para L O
Tactic:
rwa [← line_unique_of_pts b'c hb'O cO b'N cN] at pLN
Proof state after:
no goals
Theorem: para_trans
Proof state before:
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
⊢ online b O
Tactic:
rwa [NO] at bN
Proof state after:
no goals
Theorem: para_trans
Proof state before:
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
⊢ online a O
Tactic:
rwa [MO] at aM
Proof state after:
no goals
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
⊢ False
Tactic:
have ss1 := sameside_of_sameside_not_sameside cd cO cN cM dO bN aM aN (sameside_symm ssabO)
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
⊢ 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
⊢ False
Tactic:
have ss2 := not_sameside_of_sameside_sameside cO cM cN dO aM bN ssabO
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
⊢ 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
⊢ False
Tactic:
have ss: sameside d a N ∨ sameside d b M := by tauto
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
⊢ 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
⊢ False
Tactic:
obtain ⟨e0, e0d, -⟩ := pt_of_line_ne_pt d L
Proof state after:
case pos.intro.intro
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
⊢ False
Theorem: para_trans
Proof state before:
case pos.intro.intro
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
⊢ False
Tactic:
obtain ⟨β, hβ⟩ := circle_of_ne e0d.symm
Proof state after:
case pos.intro.intro.intro
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 β
⊢ False
Theorem: para_trans
Proof state before:
case pos.intro.intro.intro
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 β
⊢ False
Tactic:
have dβ := inside_circle_of_center hβ.1
Proof state after:
case pos.intro.intro.intro
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 β
⊢ False
Theorem: para_trans
Proof state before:
case pos.intro.intro.intro
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 β
⊢ False
Tactic:
have βL := line_circle_inter_of_inside_online dL dβ
Proof state after:
case pos.intro.intro.intro
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 β
⊢ False