internlm/Lean-Github huggingface dataset:
Theorem: pythagoras_converse
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
tri_abc : triangle a b c
sq_sum : length a b ^ 2 + length a c ^ 2 = length b c ^ 2
L : line
aL : online a L
cL : online c L
N : line
aN : online a N
bN : online b N
e : point
Bbae : B b a e
ba_ae : length b a = length a e
d' : point
d'eL : diffside d' e L
cad'_ra : angle c a d' = rightangle
d : point
Bd'ad : B d' a d
ba_ad : length b a = length a d
M : line
aM : online a M
d'M : online d' M
cM : ¬online c M
ang_split : angle c a d' + angle c a d = 2 * rightangle
⊢ angle b a c = rightangle
Tactic:
have pyth_2 := pythagorean_proof_two (triangle_of_ne_online (ne_23_of_B Bd'ad) aM
  (online_3_of_B Bd'ad d'M aM) cM) (by linperm)
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
tri_abc : triangle a b c
sq_sum : length a b ^ 2 + length a c ^ 2 = length b c ^ 2
L : line
aL : online a L
cL : online c L
N : line
aN : online a N
bN : online b N
e : point
Bbae : B b a e
ba_ae : length b a = length a e
d' : point
d'eL : diffside d' e L
cad'_ra : angle c a d' = rightangle
d : point
Bd'ad : B d' a d
ba_ad : length b a = length a d
M : line
aM : online a M
d'M : online d' M
cM : ¬online c M
ang_split : angle c a d' + angle c a d = 2 * rightangle
pyth_2 : length a d ^ 2 + length a c ^ 2 = length d c ^ 2
⊢ angle b a c = rightangle
Theorem: pythagoras_converse
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
tri_abc : triangle a b c
sq_sum : length a b ^ 2 + length a c ^ 2 = length b c ^ 2
L : line
aL : online a L
cL : online c L
N : line
aN : online a N
bN : online b N
e : point
Bbae : B b a e
ba_ae : length b a = length a e
d' : point
d'eL : diffside d' e L
cad'_ra : angle c a d' = rightangle
d : point
Bd'ad : B d' a d
ba_ad : length b a = length a d
M : line
aM : online a M
d'M : online d' M
cM : ¬online c M
ang_split : angle c a d' + angle c a d = 2 * rightangle
pyth_2 : length a d ^ 2 + length a c ^ 2 = length d c ^ 2
⊢ angle b a c = rightangle
Tactic:
rw[←ba_ad] at pyth_2
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
tri_abc : triangle a b c
sq_sum : length a b ^ 2 + length a c ^ 2 = length b c ^ 2
L : line
aL : online a L
cL : online c L
N : line
aN : online a N
bN : online b N
e : point
Bbae : B b a e
ba_ae : length b a = length a e
d' : point
d'eL : diffside d' e L
cad'_ra : angle c a d' = rightangle
d : point
Bd'ad : B d' a d
ba_ad : length b a = length a d
M : line
aM : online a M
d'M : online d' M
cM : ¬online c M
ang_split : angle c a d' + angle c a d = 2 * rightangle
pyth_2 : length b a ^ 2 + length a c ^ 2 = length d c ^ 2
⊢ angle b a c = rightangle
Theorem: pythagoras_converse
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
tri_abc : triangle a b c
sq_sum : length a b ^ 2 + length a c ^ 2 = length b c ^ 2
L : line
aL : online a L
cL : online c L
N : line
aN : online a N
bN : online b N
e : point
Bbae : B b a e
ba_ae : length b a = length a e
d' : point
d'eL : diffside d' e L
cad'_ra : angle c a d' = rightangle
d : point
Bd'ad : B d' a d
ba_ad : length b a = length a d
M : line
aM : online a M
d'M : online d' M
cM : ¬online c M
ang_split : angle c a d' + angle c a d = 2 * rightangle
pyth_2 : length b a ^ 2 + length a c ^ 2 = length d c ^ 2
⊢ angle b a c = rightangle
Tactic:
have sq_eq : (length c d)^2 = (length b c)^2 := by linperm
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
tri_abc : triangle a b c
sq_sum : length a b ^ 2 + length a c ^ 2 = length b c ^ 2
L : line
aL : online a L
cL : online c L
N : line
aN : online a N
bN : online b N
e : point
Bbae : B b a e
ba_ae : length b a = length a e
d' : point
d'eL : diffside d' e L
cad'_ra : angle c a d' = rightangle
d : point
Bd'ad : B d' a d
ba_ad : length b a = length a d
M : line
aM : online a M
d'M : online d' M
cM : ¬online c M
ang_split : angle c a d' + angle c a d = 2 * rightangle
pyth_2 : length b a ^ 2 + length a c ^ 2 = length d c ^ 2
sq_eq : length c d ^ 2 = length b c ^ 2
⊢ angle b a c = rightangle
Theorem: pythagoras_converse
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
tri_abc : triangle a b c
sq_sum : length a b ^ 2 + length a c ^ 2 = length b c ^ 2
L : line
aL : online a L
cL : online c L
N : line
aN : online a N
bN : online b N
e : point
Bbae : B b a e
ba_ae : length b a = length a e
d' : point
d'eL : diffside d' e L
cad'_ra : angle c a d' = rightangle
d : point
Bd'ad : B d' a d
ba_ad : length b a = length a d
M : line
aM : online a M
d'M : online d' M
cM : ¬online c M
ang_split : angle c a d' + angle c a d = 2 * rightangle
pyth_2 : length b a ^ 2 + length a c ^ 2 = length d c ^ 2
sq_eq : length c d ^ 2 = length b c ^ 2
⊢ angle b a c = rightangle
Tactic:
rw[sq_eq_sq_iff_abs_eq_abs] at sq_eq
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
tri_abc : triangle a b c
sq_sum : length a b ^ 2 + length a c ^ 2 = length b c ^ 2
L : line
aL : online a L
cL : online c L
N : line
aN : online a N
bN : online b N
e : point
Bbae : B b a e
ba_ae : length b a = length a e
d' : point
d'eL : diffside d' e L
cad'_ra : angle c a d' = rightangle
d : point
Bd'ad : B d' a d
ba_ad : length b a = length a d
M : line
aM : online a M
d'M : online d' M
cM : ¬online c M
ang_split : angle c a d' + angle c a d = 2 * rightangle
pyth_2 : length b a ^ 2 + length a c ^ 2 = length d c ^ 2
sq_eq : abs (length c d) = abs (length b c)
⊢ angle b a c = rightangle
Theorem: pythagoras_converse
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
tri_abc : triangle a b c
sq_sum : length a b ^ 2 + length a c ^ 2 = length b c ^ 2
L : line
aL : online a L
cL : online c L
N : line
aN : online a N
bN : online b N
e : point
Bbae : B b a e
ba_ae : length b a = length a e
d' : point
d'eL : diffside d' e L
cad'_ra : angle c a d' = rightangle
d : point
Bd'ad : B d' a d
ba_ad : length b a = length a d
M : line
aM : online a M
d'M : online d' M
cM : ¬online c M
ang_split : angle c a d' + angle c a d = 2 * rightangle
pyth_2 : length b a ^ 2 + length a c ^ 2 = length d c ^ 2
sq_eq : abs (length c d) = abs (length b c)
⊢ angle b a c = rightangle
Tactic:
have sq_eq' : (length c d) = (length b c) :=
by linperm[abs_of_nonneg (length_nonneg b c), abs_of_nonneg (length_nonneg c d)]
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
tri_abc : triangle a b c
sq_sum : length a b ^ 2 + length a c ^ 2 = length b c ^ 2
L : line
aL : online a L
cL : online c L
N : line
aN : online a N
bN : online b N
e : point
Bbae : B b a e
ba_ae : length b a = length a e
d' : point
d'eL : diffside d' e L
cad'_ra : angle c a d' = rightangle
d : point
Bd'ad : B d' a d
ba_ad : length b a = length a d
M : line
aM : online a M
d'M : online d' M
cM : ¬online c M
ang_split : angle c a d' + angle c a d = 2 * rightangle
pyth_2 : length b a ^ 2 + length a c ^ 2 = length d c ^ 2
sq_eq : abs (length c d) = abs (length b c)
sq_eq' : length c d = length b c
⊢ angle b a c = rightangle
Theorem: pythagoras_converse
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
tri_abc : triangle a b c
sq_sum : length a b ^ 2 + length a c ^ 2 = length b c ^ 2
L : line
aL : online a L
cL : online c L
N : line
aN : online a N
bN : online b N
e : point
Bbae : B b a e
ba_ae : length b a = length a e
d' : point
d'eL : diffside d' e L
cad'_ra : angle c a d' = rightangle
d : point
Bd'ad : B d' a d
ba_ad : length b a = length a d
M : line
aM : online a M
d'M : online d' M
cM : ¬online c M
ang_split : angle c a d' + angle c a d = 2 * rightangle
pyth_2 : length b a ^ 2 + length a c ^ 2 = length d c ^ 2
sq_eq : abs (length c d) = abs (length b c)
sq_eq' : length c d = length b c
⊢ angle b a c = rightangle
Tactic:
linperm[(sss (by linperm : length a d = length a b) (by linperm : length d c = length b c) rfl).2.1]
Proof state after:
no goals
Theorem: pythagoras_converse
Proof state before:
i : incidence_geometry
a b c : point
tri_abc : triangle a b c
sq_sum : length a b ^ 2 + length a c ^ 2 = length b c ^ 2
L : line
aL : online a L
cL : online c L
N : line
aN : online a N
bN : online b N
e : point
Bbae : B b a e
ba_ae : length b a = length a e
d' : point
d'eL : diffside d' e L
cad'_ra : angle c a d' = rightangle
d : point
Bd'ad : B d' a d
ba_ad : length b a = length a d
M : line
aM : online a M
d'M : online d' M
cM : ¬online c M
ang_split : angle c a d' + angle c a d = 2 * rightangle
⊢ angle d a c = rightangle
Tactic:
linperm
Proof state after:
no goals
Theorem: pythagoras_converse
Proof state before:
i : incidence_geometry
a b c : point
tri_abc : triangle a b c
sq_sum : length a b ^ 2 + length a c ^ 2 = length b c ^ 2
L : line
aL : online a L
cL : online c L
N : line
aN : online a N
bN : online b N
e : point
Bbae : B b a e
ba_ae : length b a = length a e
d' : point
d'eL : diffside d' e L
cad'_ra : angle c a d' = rightangle
d : point
Bd'ad : B d' a d
ba_ad : length b a = length a d
M : line
aM : online a M
d'M : online d' M
cM : ¬online c M
ang_split : angle c a d' + angle c a d = 2 * rightangle
pyth_2 : length b a ^ 2 + length a c ^ 2 = length d c ^ 2
⊢ length c d ^ 2 = length b c ^ 2
Tactic:
linperm
Proof state after:
no goals
Theorem: pythagoras_converse
Proof state before:
i : incidence_geometry
a b c : point
tri_abc : triangle a b c
sq_sum : length a b ^ 2 + length a c ^ 2 = length b c ^ 2
L : line
aL : online a L
cL : online c L
N : line
aN : online a N
bN : online b N
e : point
Bbae : B b a e
ba_ae : length b a = length a e
d' : point
d'eL : diffside d' e L
cad'_ra : angle c a d' = rightangle
d : point
Bd'ad : B d' a d
ba_ad : length b a = length a d
M : line
aM : online a M
d'M : online d' M
cM : ¬online c M
ang_split : angle c a d' + angle c a d = 2 * rightangle
pyth_2 : length b a ^ 2 + length a c ^ 2 = length d c ^ 2
sq_eq : abs (length c d) = abs (length b c)
⊢ length c d = length b c
Tactic:
linperm[abs_of_nonneg (length_nonneg b c), abs_of_nonneg (length_nonneg c d)]
Proof state after:
no goals
Theorem: pythagoras_converse
Proof state before:
i : incidence_geometry
a b c : point
tri_abc : triangle a b c
sq_sum : length a b ^ 2 + length a c ^ 2 = length b c ^ 2
L : line
aL : online a L
cL : online c L
N : line
aN : online a N
bN : online b N
e : point
Bbae : B b a e
ba_ae : length b a = length a e
d' : point
d'eL : diffside d' e L
cad'_ra : angle c a d' = rightangle
d : point
Bd'ad : B d' a d
ba_ad : length b a = length a d
M : line
aM : online a M
d'M : online d' M
cM : ¬online c M
ang_split : angle c a d' + angle c a d = 2 * rightangle
pyth_2 : length b a ^ 2 + length a c ^ 2 = length d c ^ 2
sq_eq : abs (length c d) = abs (length b c)
sq_eq' : length c d = length b c
⊢ length a d = length a b
Tactic:
linperm
Proof state after:
no goals
Theorem: pythagoras_converse
Proof state before:
i : incidence_geometry
a b c : point
tri_abc : triangle a b c
sq_sum : length a b ^ 2 + length a c ^ 2 = length b c ^ 2
L : line
aL : online a L
cL : online c L
N : line
aN : online a N
bN : online b N
e : point
Bbae : B b a e
ba_ae : length b a = length a e
d' : point
d'eL : diffside d' e L
cad'_ra : angle c a d' = rightangle
d : point
Bd'ad : B d' a d
ba_ad : length b a = length a d
M : line
aM : online a M
d'M : online d' M
cM : ¬online c M
ang_split : angle c a d' + angle c a d = 2 * rightangle
pyth_2 : length b a ^ 2 + length a c ^ 2 = length d c ^ 2
sq_eq : abs (length c d) = abs (length b c)
sq_eq' : length c d = length b c
⊢ length d c = length b c
Tactic:
linperm
Proof state after:
no goals
Theorem: same_len_pts_coincide_iff
Proof state before:
i : incidence_geometry
a b c d : point
hlen : length a b = length c d
⊢ a = b ↔ c = d
Tactic:
rw [← @length_eq_zero_iff i a b, ← @length_eq_zero_iff i c d, hlen]
Proof state after:
no goals
Theorem: pt_of_line_ne_pt
Proof state before:
i : incidence_geometry
a : point
L : line
⊢ ∃ b, b ≠ a ∧ online b L
Tactic:
obtain ⟨ b, c, Hbc ⟩ := online_ne_of_line L
Proof state after:
case intro.intro
i : incidence_geometry
a : point
L : line
b c : point
Hbc : b ≠ c ∧ online b L ∧ online c L
⊢ ∃ b, b ≠ a ∧ online b L
Theorem: pt_of_line_ne_pt
Proof state before:
case intro.intro
i : incidence_geometry
a : point
L : line
b c : point
Hbc : b ≠ c ∧ online b L ∧ online c L
⊢ ∃ b, b ≠ a ∧ online b L
Tactic:
by_cases b = a
Proof state after:
case pos
i : incidence_geometry
a : point
L : line
b c : point
Hbc : b ≠ c ∧ online b L ∧ online c L
h : b = a
⊢ ∃ b, b ≠ a ∧ online b L

case neg
i : incidence_geometry
a : point
L : line
b c : point
Hbc : b ≠ c ∧ online b L ∧ online c L
h : ¬b = a
⊢ ∃ b, b ≠ a ∧ online b L
Theorem: pt_of_line_ne_pt
Proof state before:
case pos
i : incidence_geometry
a : point
L : line
b c : point
Hbc : b ≠ c ∧ online b L ∧ online c L
h : b = a
⊢ ∃ b, b ≠ a ∧ online b L
Tactic:
simp_rw [h] at Hbc
Proof state after:
case pos
i : incidence_geometry
a : point
L : line
b c : point
h : b = a
Hbc : a ≠ c ∧ online a L ∧ online c L
⊢ ∃ b, b ≠ a ∧ online b L
Theorem: pt_of_line_ne_pt
Proof state before:
case pos
i : incidence_geometry
a : point
L : line
b c : point
h : b = a
Hbc : a ≠ c ∧ online a L ∧ online c L
⊢ ∃ b, b ≠ a ∧ online b L
Tactic:
exact ⟨c, Hbc.1.symm, Hbc.2.2 ⟩
Proof state after:
no goals
Theorem: pt_of_line_ne_pt
Proof state before:
case neg
i : incidence_geometry
a : point
L : line
b c : point
Hbc : b ≠ c ∧ online b L ∧ online c L
h : ¬b = a
⊢ ∃ b, b ≠ a ∧ online b L
Tactic:
exact ⟨ b, h, Hbc.2.1 ⟩
Proof state after:
no goals
Theorem: pt_of_line_line
Proof state before:
i : incidence_geometry
L M : line
hp : ¬para L M
⊢ ∃ a, online a L ∧ online a M
Tactic:
simp_rw [para, not_forall, not_or, not_not] at hp
Proof state after:
i : incidence_geometry
L M : line
hp : ∃ x, online x L ∧ online x M
⊢ ∃ a, online a L ∧ online a M
Theorem: pt_of_line_line
Proof state before:
i : incidence_geometry
L M : line
hp : ∃ x, online x L ∧ online x M
⊢ ∃ a, online a L ∧ online a M
Tactic:
exact hp
Proof state after:
no goals
Theorem: neq_of_para
Proof state before:
i : incidence_geometry
a b : point
L M : line
aL : online a L
bM : online b M
pLM : para L M
ab : a = b
⊢ False
Tactic:
have := offline_of_para aL pLM
Proof state after:
i : incidence_geometry
a b : point
L M : line
aL : online a L
bM : online b M
pLM : para L M
ab : a = b
this : ¬online a M
⊢ False
Theorem: neq_of_para
Proof state before:
i : incidence_geometry
a b : point
L M : line
aL : online a L
bM : online b M
pLM : para L M
ab : a = b
this : ¬online a M
⊢ False
Tactic:
rw [ab] at this
Proof state after:
i : incidence_geometry
a b : point
L M : line
aL : online a L
bM : online b M
pLM : para L M
ab : a = b
this : ¬online b M
⊢ False
Theorem: neq_of_para
Proof state before:
i : incidence_geometry
a b : point
L M : line
aL : online a L
bM : online b M
pLM : para L M
ab : a = b
this : ¬online b M
⊢ False
Tactic:
exact this bM
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
⊢ M = N ∨ para M N
Tactic:
by_cases MN : M = N
Proof state after:
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

case neg
i : incidence_geometry
L M N : line
pLM : para L M
pLN : para L N
MN : ¬M = N
⊢ M = N ∨ para M N
Theorem: para_trans
Proof state before:
case neg
i : incidence_geometry
L M N : line
pLM : para L M
pLN : para L N
MN : ¬M = N
⊢ M = N ∨ para M N
Tactic:
by_contra npMN
Proof state after:
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)
⊢ False
Theorem: para_trans
Proof state before:
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)
⊢ False
Tactic:
simp [not_or] at npMN
Proof state after:
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
⊢ False
Theorem: para_trans
Proof state before:
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
⊢ False
Tactic:
rcases pt_of_line_line npMN.2 with ⟨c, cM, cN⟩
Proof state after:
case neg.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
⊢ False
Theorem: para_trans
Proof state before:
case neg.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
⊢ False
Tactic:
have cL := offline_of_para cN (para_symm pLN)
Proof state after:
case neg.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
⊢ False
Theorem: para_trans
Proof state before:
case neg.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
⊢ False
Tactic:
rcases perpendicular_of_not_online cL with ⟨-, -, d, -, -, -, dL, -, -⟩
Proof state after:
case neg.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
⊢ False
Theorem: para_trans
Proof state before:
case neg.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
⊢ False
Tactic:
obtain ⟨O, cO, dO⟩ := line_of_pts c d
Proof state after:
case neg.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
⊢ False
Theorem: para_trans
Proof state before:
case neg.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
⊢ False
Tactic:
have cd : c ≠ d := neq_of_para cM dL (para_symm pLM)
Proof state after:
case neg.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
⊢ False
Theorem: para_trans
Proof state before:
case neg.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
⊢ False
Tactic:
have LO : L ≠ O := fun LO => cL (by rwa [← LO] at cO)
Proof state after:
case neg.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
⊢ False
Theorem: para_trans
Proof state before:
case neg.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
⊢ False
Tactic:
obtain ⟨α, Hα⟩ := circle_of_ne cd
Proof state after:
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 α
⊢ False
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 α
⊢ False
Tactic:
have cα := inside_circle_of_center Hα.1
Proof state after:
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 α
⊢ False
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 α
⊢ False
Tactic:
have αM := line_circle_inter_of_inside_online cM cα
Proof state after:
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 α
⊢ False
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 α
⊢ False
Tactic:
have αN := line_circle_inter_of_inside_online cN cα
Proof state after:
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