internlm/Lean-Github huggingface dataset:
Theorem: eq_area_of_same_base_implies_para
Proof state before:
case pos
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : ¬para N O
e : point
eN : online d N
eO : online e O
ar2 : area d b c = area e b c
be : b ≠ e
de : d = e
⊢ para L M
Tactic:
rwa [line_unique_of_pts ad aM dM aN eN]
Proof state after:
no goals
Theorem: eq_area_of_same_base_implies_para
Proof state before:
case neg
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : ¬para N O
e : point
eN : online e N
eO : online e O
ar2 : area d b c = area e b c
be : b ≠ e
de : ¬d = e
⊢ para L M
Tactic:
rw [← Ne.def d e] at de
Proof state after:
case neg
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : ¬para N O
e : point
eN : online e N
eO : online e O
ar2 : area d b c = area e b c
be : b ≠ e
de : d ≠ e
⊢ para L M
Theorem: eq_area_of_same_base_implies_para
Proof state before:
case neg
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : ¬para N O
e : point
eN : online e N
eO : online e O
ar2 : area d b c = area e b c
be : b ≠ e
de : d ≠ e
⊢ para L M
Tactic:
exfalso
Proof state after:
case neg.h
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : ¬para N O
e : point
eN : online e N
eO : online e O
ar2 : area d b c = area e b c
be : b ≠ e
de : d ≠ e
⊢ False
Theorem: eq_area_of_same_base_implies_para
Proof state before:
case neg.h
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : ¬para N O
e : point
eN : online e N
eO : online e O
ar2 : area d b c = area e b c
be : b ≠ e
de : d ≠ e
⊢ False
Tactic:
cases B_of_three_online_ne be bd de.symm bO eO dO with
| inl Bbed =>
  exact tri_sum_contra bO dO eO cO bd de be.symm Bbed (by perma at ar2)
| inr HB =>
  cases HB with
  | inl Bebd =>
    have ssaeL := sameside_of_para_online aN eN (para_symm pNL)
    have ssedL := sameside_symm (sameside_trans ssadL ssaeL)
    have dsedL:= not_sameside13_of_B123_online2 Bebd bL
    exact dsedL ssedL
  | inr Bbde =>
    exact tri_sum_contra bO eO dO cO be de.symm bd.symm Bbde (by perma at ar2)
Proof state after:
no goals
Theorem: eq_area_of_same_base_implies_para
Proof state before:
case neg.h.inl
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : ¬para N O
e : point
eN : online e N
eO : online e O
ar2 : area d b c = area e b c
be : b ≠ e
de : d ≠ e
Bbed : B b e d
⊢ False
Tactic:
exact tri_sum_contra bO dO eO cO bd de be.symm Bbed (by perma at ar2)
Proof state after:
no goals
Theorem: eq_area_of_same_base_implies_para
Proof state before:
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : ¬para N O
e : point
eN : online e N
eO : online e O
ar2 : area d b c = area e b c
be : b ≠ e
de : d ≠ e
Bbed : B b e d
⊢ area b c d = area b c e
Tactic:
perma at ar2
Proof state after:
no goals
Theorem: eq_area_of_same_base_implies_para
Proof state before:
case neg.h.inr
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : ¬para N O
e : point
eN : online e N
eO : online e O
ar2 : area d b c = area e b c
be : b ≠ e
de : d ≠ e
HB : B e b d ∨ B b d e
⊢ False
Tactic:
cases HB with
| inl Bebd =>
  have ssaeL := sameside_of_para_online aN eN (para_symm pNL)
  have ssedL := sameside_symm (sameside_trans ssadL ssaeL)
  have dsedL:= not_sameside13_of_B123_online2 Bebd bL
  exact dsedL ssedL
| inr Bbde =>
  exact tri_sum_contra bO eO dO cO be de.symm bd.symm Bbde (by perma at ar2)
Proof state after:
no goals
Theorem: eq_area_of_same_base_implies_para
Proof state before:
case neg.h.inr.inl
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : ¬para N O
e : point
eN : online e N
eO : online e O
ar2 : area d b c = area e b c
be : b ≠ e
de : d ≠ e
Bebd : B e b d
⊢ False
Tactic:
have ssaeL := sameside_of_para_online aN eN (para_symm pNL)
Proof state after:
case neg.h.inr.inl
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : ¬para N O
e : point
eN : online e N
eO : online e O
ar2 : area d b c = area e b c
be : b ≠ e
de : d ≠ e
Bebd : B e b d
ssaeL : sameside a e L
⊢ False
Theorem: eq_area_of_same_base_implies_para
Proof state before:
case neg.h.inr.inl
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : ¬para N O
e : point
eN : online e N
eO : online e O
ar2 : area d b c = area e b c
be : b ≠ e
de : d ≠ e
Bebd : B e b d
ssaeL : sameside a e L
⊢ False
Tactic:
have ssedL := sameside_symm (sameside_trans ssadL ssaeL)
Proof state after:
case neg.h.inr.inl
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : ¬para N O
e : point
eN : online e N
eO : online e O
ar2 : area d b c = area e b c
be : b ≠ e
de : d ≠ e
Bebd : B e b d
ssaeL : sameside a e L
ssedL : sameside e d L
⊢ False
Theorem: eq_area_of_same_base_implies_para
Proof state before:
case neg.h.inr.inl
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : ¬para N O
e : point
eN : online e N
eO : online e O
ar2 : area d b c = area e b c
be : b ≠ e
de : d ≠ e
Bebd : B e b d
ssaeL : sameside a e L
ssedL : sameside e d L
⊢ False
Tactic:
have dsedL:= not_sameside13_of_B123_online2 Bebd bL
Proof state after:
case neg.h.inr.inl
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : ¬para N O
e : point
eN : online e N
eO : online e O
ar2 : area d b c = area e b c
be : b ≠ e
de : d ≠ e
Bebd : B e b d
ssaeL : sameside a e L
ssedL : sameside e d L
dsedL : ¬sameside e d L
⊢ False
Theorem: eq_area_of_same_base_implies_para
Proof state before:
case neg.h.inr.inl
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : ¬para N O
e : point
eN : online e N
eO : online e O
ar2 : area d b c = area e b c
be : b ≠ e
de : d ≠ e
Bebd : B e b d
ssaeL : sameside a e L
ssedL : sameside e d L
dsedL : ¬sameside e d L
⊢ False
Tactic:
exact dsedL ssedL
Proof state after:
no goals
Theorem: eq_area_of_same_base_implies_para
Proof state before:
case neg.h.inr.inr
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : ¬para N O
e : point
eN : online e N
eO : online e O
ar2 : area d b c = area e b c
be : b ≠ e
de : d ≠ e
Bbde : B b d e
⊢ False
Tactic:
exact tri_sum_contra bO eO dO cO be de.symm bd.symm Bbde (by perma at ar2)
Proof state after:
no goals
Theorem: eq_area_of_same_base_implies_para
Proof state before:
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : ¬para N O
e : point
eN : online e N
eO : online e O
ar2 : area d b c = area e b c
be : b ≠ e
de : d ≠ e
Bbde : B b d e
⊢ area b c e = area b c d
Tactic:
perma at ar2
Proof state after:
no goals
Theorem: rescale_length
Proof state before:
i : incidence_geometry
a b : point
L : line
n : ℕ
aL : online a L
bL : online b L
⊢ ∃ c, online c L ∧ length a c = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b c)
Tactic:
by_cases ab: a = b
Proof state after:
case pos
i : incidence_geometry
a b : point
L : line
n : ℕ
aL : online a L
bL : online b L
ab : a = b
⊢ ∃ c, online c L ∧ length a c = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b c)

case neg
i : incidence_geometry
a b : point
L : line
n : ℕ
aL : online a L
bL : online b L
ab : ¬a = b
⊢ ∃ c, online c L ∧ length a c = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b c)
Theorem: rescale_length
Proof state before:
case pos
i : incidence_geometry
a b : point
L : line
n : ℕ
aL : online a L
bL : online b L
ab : a = b
⊢ ∃ c, online c L ∧ length a c = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b c)
Tactic:
use a
Proof state after:
case pos
i : incidence_geometry
a b : point
L : line
n : ℕ
aL : online a L
bL : online b L
ab : a = b
⊢ online a L ∧ length a a = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b a)
Theorem: rescale_length
Proof state before:
case pos
i : incidence_geometry
a b : point
L : line
n : ℕ
aL : online a L
bL : online b L
ab : a = b
⊢ online a L ∧ length a a = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b a)
Tactic:
rw [← ab, length_eq_zero_iff.mpr rfl]
Proof state after:
case pos
i : incidence_geometry
a b : point
L : line
n : ℕ
aL : online a L
bL : online b L
ab : a = b
⊢ online a L ∧ 0 = ↑n * 0 ∧ (n ≥ 2 ∧ a ≠ a → B a a a)
Theorem: rescale_length
Proof state before:
case pos
i : incidence_geometry
a b : point
L : line
n : ℕ
aL : online a L
bL : online b L
ab : a = b
⊢ online a L ∧ 0 = ↑n * 0 ∧ (n ≥ 2 ∧ a ≠ a → B a a a)
Tactic:
simp
Proof state after:
case pos
i : incidence_geometry
a b : point
L : line
n : ℕ
aL : online a L
bL : online b L
ab : a = b
⊢ online a L
Theorem: rescale_length
Proof state before:
case pos
i : incidence_geometry
a b : point
L : line
n : ℕ
aL : online a L
bL : online b L
ab : a = b
⊢ online a L
Tactic:
exact aL
Proof state after:
no goals
Theorem: rescale_length
Proof state before:
case neg.zero
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
⊢ ∃ c, online c L ∧ length a c = ↑Nat.zero * length a b ∧ (Nat.zero ≥ 2 ∧ a ≠ b → B a b c)
Tactic:
use a
Proof state after:
case neg.zero
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
⊢ online a L ∧ length a a = ↑Nat.zero * length a b ∧ (Nat.zero ≥ 2 ∧ a ≠ b → B a b a)
Theorem: rescale_length
Proof state before:
case neg.zero
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
⊢ online a L ∧ length a a = ↑Nat.zero * length a b ∧ (Nat.zero ≥ 2 ∧ a ≠ b → B a b a)
Tactic:
rw [length_eq_zero_iff.mpr rfl]
Proof state after:
case neg.zero
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
⊢ online a L ∧ 0 = ↑Nat.zero * length a b ∧ (Nat.zero ≥ 2 ∧ a ≠ b → B a b a)
Theorem: rescale_length
Proof state before:
case neg.zero
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
⊢ online a L ∧ 0 = ↑Nat.zero * length a b ∧ (Nat.zero ≥ 2 ∧ a ≠ b → B a b a)
Tactic:
simp
Proof state after:
case neg.zero
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
⊢ online a L
Theorem: rescale_length
Proof state before:
case neg.zero
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
⊢ online a L
Tactic:
exact aL
Proof state after:
no goals
Theorem: rescale_length
Proof state before:
case neg.succ
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
hn : ∃ c, online c L ∧ length a c = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b c)
⊢ ∃ c, online c L ∧ length a c = ↑(Nat.succ n) * length a b ∧ (Nat.succ n ≥ 2 ∧ a ≠ b → B a b c)
Tactic:
by_cases n0: n = 0
Proof state after:
case pos
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
hn : ∃ c, online c L ∧ length a c = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b c)
n0 : n = 0
⊢ ∃ c, online c L ∧ length a c = ↑(Nat.succ n) * length a b ∧ (Nat.succ n ≥ 2 ∧ a ≠ b → B a b c)

case neg
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
hn : ∃ c, online c L ∧ length a c = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b c)
n0 : ¬n = 0
⊢ ∃ c, online c L ∧ length a c = ↑(Nat.succ n) * length a b ∧ (Nat.succ n ≥ 2 ∧ a ≠ b → B a b c)
Theorem: rescale_length
Proof state before:
case neg
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
hn : ∃ c, online c L ∧ length a c = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b c)
n0 : ¬n = 0
⊢ ∃ c, online c L ∧ length a c = ↑(Nat.succ n) * length a b ∧ (Nat.succ n ≥ 2 ∧ a ≠ b → B a b c)
Tactic:
by_cases n1 : n = 1
Proof state after:
case pos
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
hn : ∃ c, online c L ∧ length a c = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b c)
n0 : ¬n = 0
n1 : n = 1
⊢ ∃ c, online c L ∧ length a c = ↑(Nat.succ n) * length a b ∧ (Nat.succ n ≥ 2 ∧ a ≠ b → B a b c)

case neg
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
hn : ∃ c, online c L ∧ length a c = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b c)
n0 : ¬n = 0
n1 : ¬n = 1
⊢ ∃ c, online c L ∧ length a c = ↑(Nat.succ n) * length a b ∧ (Nat.succ n ≥ 2 ∧ a ≠ b → B a b c)
Theorem: rescale_length
Proof state before:
case neg
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
hn : ∃ c, online c L ∧ length a c = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b c)
n0 : ¬n = 0
n1 : ¬n = 1
⊢ ∃ c, online c L ∧ length a c = ↑(Nat.succ n) * length a b ∧ (Nat.succ n ≥ 2 ∧ a ≠ b → B a b c)
Tactic:
obtain ⟨ d, Hd ⟩ := hn
Proof state after:
case neg.intro
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
n0 : ¬n = 0
n1 : ¬n = 1
d : point
Hd : online d L ∧ length a d = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b d)
⊢ ∃ c, online c L ∧ length a c = ↑(Nat.succ n) * length a b ∧ (Nat.succ n ≥ 2 ∧ a ≠ b → B a b c)
Theorem: rescale_length
Proof state before:
case neg.intro
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
n0 : ¬n = 0
n1 : ¬n = 1
d : point
Hd : online d L ∧ length a d = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b d)
⊢ ∃ c, online c L ∧ length a c = ↑(Nat.succ n) * length a b ∧ (Nat.succ n ≥ 2 ∧ a ≠ b → B a b c)
Tactic:
have ad : a ≠ d := by
  apply nq_of_len_pos
  rw [Hd.2.1]; simp [Nat.pos_of_ne_zero n0, zero_lt_mul_left, Nat.cast_pos]
  exact len_pos_of_nq ab
Proof state after:
case neg.intro
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
n0 : ¬n = 0
n1 : ¬n = 1
d : point
Hd : online d L ∧ length a d = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b d)
ad : a ≠ d
⊢ ∃ c, online c L ∧ length a c = ↑(Nat.succ n) * length a b ∧ (Nat.succ n ≥ 2 ∧ a ≠ b → B a b c)
Theorem: rescale_length
Proof state before:
case neg.intro
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
n0 : ¬n = 0
n1 : ¬n = 1
d : point
Hd : online d L ∧ length a d = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b d)
ad : a ≠ d
⊢ ∃ c, online c L ∧ length a c = ↑(Nat.succ n) * length a b ∧ (Nat.succ n ≥ 2 ∧ a ≠ b → B a b c)
Tactic:
obtain ⟨ e, He ⟩ := length_eq_B_of_ne_four ad ab
Proof state after:
case neg.intro.intro
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
n0 : ¬n = 0
n1 : ¬n = 1
d : point
Hd : online d L ∧ length a d = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b d)
ad : a ≠ d
e : point
He : B a d e ∧ length a b = length d e
⊢ ∃ c, online c L ∧ length a c = ↑(Nat.succ n) * length a b ∧ (Nat.succ n ≥ 2 ∧ a ≠ b → B a b c)
Theorem: rescale_length
Proof state before:
case neg.intro.intro
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
n0 : ¬n = 0
n1 : ¬n = 1
d : point
Hd : online d L ∧ length a d = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b d)
ad : a ≠ d
e : point
He : B a d e ∧ length a b = length d e
⊢ ∃ c, online c L ∧ length a c = ↑(Nat.succ n) * length a b ∧ (Nat.succ n ≥ 2 ∧ a ≠ b → B a b c)
Tactic:
use e
Proof state after:
case neg.intro.intro
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
n0 : ¬n = 0
n1 : ¬n = 1
d : point
Hd : online d L ∧ length a d = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b d)
ad : a ≠ d
e : point
He : B a d e ∧ length a b = length d e
⊢ online e L ∧ length a e = ↑(Nat.succ n) * length a b ∧ (Nat.succ n ≥ 2 ∧ a ≠ b → B a b e)
Theorem: rescale_length
Proof state before:
case neg.intro.intro
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
n0 : ¬n = 0
n1 : ¬n = 1
d : point
Hd : online d L ∧ length a d = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b d)
ad : a ≠ d
e : point
He : B a d e ∧ length a b = length d e
⊢ online e L ∧ length a e = ↑(Nat.succ n) * length a b ∧ (Nat.succ n ≥ 2 ∧ a ≠ b → B a b e)
Tactic:
rw [← length_sum_of_B He.1, Hd.2.1, He.2]
Proof state after:
case neg.intro.intro
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
n0 : ¬n = 0
n1 : ¬n = 1
d : point
Hd : online d L ∧ length a d = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b d)
ad : a ≠ d
e : point
He : B a d e ∧ length a b = length d e
⊢ online e L ∧ ↑n * length d e + length d e = ↑(Nat.succ n) * length d e ∧ (Nat.succ n ≥ 2 ∧ a ≠ b → B a b e)
Theorem: rescale_length
Proof state before:
case neg.intro.intro
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
n0 : ¬n = 0
n1 : ¬n = 1
d : point
Hd : online d L ∧ length a d = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b d)
ad : a ≠ d
e : point
He : B a d e ∧ length a b = length d e
⊢ online e L ∧ ↑n * length d e + length d e = ↑(Nat.succ n) * length d e ∧ (Nat.succ n ≥ 2 ∧ a ≠ b → B a b e)
Tactic:
simp
Proof state after:
case neg.intro.intro
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
n0 : ¬n = 0
n1 : ¬n = 1
d : point
Hd : online d L ∧ length a d = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b d)
ad : a ≠ d
e : point
He : B a d e ∧ length a b = length d e
⊢ online e L ∧ ↑n * length d e + length d e = (↑n + 1) * length d e ∧ (2 ≤ Nat.succ n → ¬a = b → B a b e)
Theorem: rescale_length
Proof state before:
case neg.intro.intro
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
n0 : ¬n = 0
n1 : ¬n = 1
d : point
Hd : online d L ∧ length a d = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b d)
ad : a ≠ d
e : point
He : B a d e ∧ length a b = length d e
⊢ online e L ∧ ↑n * length d e + length d e = (↑n + 1) * length d e ∧ (2 ≤ Nat.succ n → ¬a = b → B a b e)
Tactic:
ring_nf
Proof state after:
case neg.intro.intro
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
n0 : ¬n = 0
n1 : ¬n = 1
d : point
Hd : online d L ∧ length a d = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b d)
ad : a ≠ d
e : point
He : B a d e ∧ length a b = length d e
⊢ online e L ∧ True ∧ (2 ≤ Nat.succ n → ¬a = b → B a b e)
Theorem: rescale_length
Proof state before:
case neg.intro.intro
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
n0 : ¬n = 0
n1 : ¬n = 1
d : point
Hd : online d L ∧ length a d = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b d)
ad : a ≠ d
e : point
He : B a d e ∧ length a b = length d e
⊢ online e L ∧ True ∧ (2 ≤ Nat.succ n → ¬a = b → B a b e)
Tactic:
have := Hd.2.2 ⟨ ge2_of_n1_n0 n0 n1, ab ⟩
Proof state after:
case neg.intro.intro
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
n0 : ¬n = 0
n1 : ¬n = 1
d : point
Hd : online d L ∧ length a d = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b d)
ad : a ≠ d
e : point
He : B a d e ∧ length a b = length d e
this : B a b d
⊢ online e L ∧ True ∧ (2 ≤ Nat.succ n → ¬a = b → B a b e)
Theorem: rescale_length
Proof state before:
case neg.intro.intro
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
n0 : ¬n = 0
n1 : ¬n = 1
d : point
Hd : online d L ∧ length a d = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b d)
ad : a ≠ d
e : point
He : B a d e ∧ length a b = length d e
this : B a b d
⊢ online e L ∧ True ∧ (2 ≤ Nat.succ n → ¬a = b → B a b e)
Tactic:
exact ⟨ online_3_of_B He.1 aL Hd.1, (by tauto), fun _ _ => B124_of_B134_B123 He.1 this⟩
Proof state after:
no goals
Theorem: rescale_length
Proof state before:
case pos
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
hn : ∃ c, online c L ∧ length a c = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b c)
n0 : n = 0
⊢ ∃ c, online c L ∧ length a c = ↑(Nat.succ n) * length a b ∧ (Nat.succ n ≥ 2 ∧ a ≠ b → B a b c)
Tactic:
exact ⟨ b, bL, (by rw [n0]; simp) ⟩
Proof state after:
no goals
Theorem: rescale_length
Proof state before:
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
hn : ∃ c, online c L ∧ length a c = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b c)
n0 : n = 0
⊢ length a b = ↑(Nat.succ n) * length a b ∧ (Nat.succ n ≥ 2 ∧ a ≠ b → B a b b)
Tactic:
rw [n0]
Proof state after:
i : incidence_geometry
a b : point
L : line
aL : online a L
bL : online b L
ab : ¬a = b
n : ℕ
hn : ∃ c, online c L ∧ length a c = ↑n * length a b ∧ (n ≥ 2 ∧ a ≠ b → B a b c)
n0 : n = 0
⊢ length a b = ↑(Nat.succ 0) * length a b ∧ (Nat.succ 0 ≥ 2 ∧ a ≠ b → B a b b)