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
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 α
⊢ False
Tactic:
obtain ⟨a, a', aa', aM, a'M, aα⟩ := pts_of_line_circle_inter αM
Proof state after:
case neg.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' α
⊢ 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
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' α
⊢ False
Tactic:
obtain ⟨b, b', bb', bN, b'N, bα⟩ := pts_of_line_circle_inter αN
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' α
⊢ 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' α
⊢ False
Tactic:
have Baca' := B_of_line_circle_inter aa' cM aM a'M aα.1 aα.2 cα
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'
⊢ 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'
⊢ False
Tactic:
have Bbcb' := B_of_line_circle_inter bb' cN bN b'N bα.1 bα.2 cα
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'
⊢ 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'
⊢ False
Tactic:
have ac := ne_12_of_B Baca'
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
⊢ 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
⊢ False
Tactic:
have bc := ne_12_of_B Bbcb'
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
⊢ 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
⊢ False
Tactic:
have b'c := (ne_23_of_B Bbcb').symm
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
⊢ 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
⊢ False
Tactic:
have aO: ¬ online a O := fun aO => neq_of_para dL dO (by rwa [← line_unique_of_pts ac aO cO aM cM] at pLM) rfl
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
⊢ 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
⊢ False
Tactic:
have bO : ¬ online b O := fun bO => neq_of_para dL dO (by rwa [← line_unique_of_pts bc bO cO bN cN] at pLN) rfl
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
⊢ 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
⊢ False
Tactic:
have b'O : ¬ online b' O := fun hb'O => neq_of_para dL dO (by rwa [← line_unique_of_pts b'c hb'O cO b'N cN] at pLN) rfl
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
⊢ 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
⊢ False
Tactic:
have aN: ¬ online a N := fun aN => MN (line_unique_of_pts ac aM cM aN cN)
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
⊢ 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
⊢ False
Tactic:
have bM: ¬ online b M := fun bM => MN (line_unique_of_pts bc bM cM bN cN)
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
⊢ 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
⊢ False
Tactic:
have b'M: ¬ online b' M := fun hb'M => MN (line_unique_of_pts b'c hb'M cM b'N cN)
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
⊢ 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
⊢ False
Tactic:
have NO : N ≠ O := fun NO => bO (by rwa [NO] at bN)
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
⊢ False