internlm/Lean-Github huggingface dataset:
Theorem: proportion_area_of_proportion_base
Proof state before:
case intro.intro
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
n m : ℕ
h : point
Hh : online h L ∧ length b h = ↑n * length b c ∧ (n ≥ 2 ∧ b ≠ c → B b c h)
l : point
Hl : online l L ∧ length e l = ↑m * length e f ∧ (m ≥ 2 ∧ e ≠ f → B e f l)
⊢ (↑n * length b c = ↑m * length e f → ↑n * area a b c = ↑m * area d e f) ∧
    (↑n * length b c < ↑m * length e f → ↑n * area a b c < ↑m * area d e f) ∧
      (↑m * length e f < ↑n * length b c → ↑m * area d e f < ↑n * area a b c)
Tactic:
rw [(rescale_triangle_of_base a bL cL Hh.1 Hh.2.1).symm, Hh.2.1.symm]
Proof state after:
case intro.intro
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
n m : ℕ
h : point
Hh : online h L ∧ length b h = ↑n * length b c ∧ (n ≥ 2 ∧ b ≠ c → B b c h)
l : point
Hl : online l L ∧ length e l = ↑m * length e f ∧ (m ≥ 2 ∧ e ≠ f → B e f l)
⊢ (length b h = ↑m * length e f → area a b h = ↑m * area d e f) ∧
    (length b h < ↑m * length e f → area a b h < ↑m * area d e f) ∧
      (↑m * length e f < length b h → ↑m * area d e f < area a b h)
Theorem: proportion_area_of_proportion_base
Proof state before:
case intro.intro
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
n m : ℕ
h : point
Hh : online h L ∧ length b h = ↑n * length b c ∧ (n ≥ 2 ∧ b ≠ c → B b c h)
l : point
Hl : online l L ∧ length e l = ↑m * length e f ∧ (m ≥ 2 ∧ e ≠ f → B e f l)
⊢ (length b h = ↑m * length e f → area a b h = ↑m * area d e f) ∧
    (length b h < ↑m * length e f → area a b h < ↑m * area d e f) ∧
      (↑m * length e f < length b h → ↑m * area d e f < area a b h)
Tactic:
rw [(rescale_triangle_of_base d eL fL Hl.1 Hl.2.1).symm, Hl.2.1.symm]
Proof state after:
case intro.intro
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
n m : ℕ
h : point
Hh : online h L ∧ length b h = ↑n * length b c ∧ (n ≥ 2 ∧ b ≠ c → B b c h)
l : point
Hl : online l L ∧ length e l = ↑m * length e f ∧ (m ≥ 2 ∧ e ≠ f → B e f l)
⊢ (length b h = length e l → area a b h = area d e l) ∧
    (length b h < length e l → area a b h < area d e l) ∧ (length e l < length b h → area d e l < area a b h)
Theorem: proportion_area_of_proportion_base
Proof state before:
case intro.intro
i : incidence_geometry
a b c d e f : point
L M : line
aM : online a M
bL : online b L
cL : online c L
dM : online d M
eL : online e L
fL : online f L
pLM : para L M
n m : ℕ
h : point
Hh : online h L ∧ length b h = ↑n * length b c ∧ (n ≥ 2 ∧ b ≠ c → B b c h)
l : point
Hl : online l L ∧ length e l = ↑m * length e f ∧ (m ≥ 2 ∧ e ≠ f → B e f l)
⊢ (length b h = length e l → area a b h = area d e l) ∧
    (length b h < length e l → area a b h < area d e l) ∧ (length e l < length b h → area d e l < area a b h)
Tactic:
exact ⟨ eq_area_of_eq_base aM bL Hh.1 dM eL Hl.1 pLM,
        lt_area_of_lt_base dM eL Hl.1 aM bL Hh.1 pLM,
        lt_area_of_lt_base aM bL Hh.1 dM eL Hl.1 pLM ⟩
Proof state after:
no goals
Theorem: proportion_area_of_proportion_base_samevertex
Proof state before:
i : incidence_geometry
a b c e f : point
L : line
bL : online b L
cL : online c L
eL : online e L
fL : online f L
aL : ¬online a L
⊢ proportion (length b c) (length e f) (area a b c) (area a e f)
Tactic:
obtain ⟨ M, aM, pLM ⟩ := parallel_of_line_pt aL
Proof state after:
case intro.intro
i : incidence_geometry
a b c e f : point
L : line
bL : online b L
cL : online c L
eL : online e L
fL : online f L
aL : ¬online a L
M : line
aM : online a M
pLM : para L M
⊢ proportion (length b c) (length e f) (area a b c) (area a e f)
Theorem: proportion_area_of_proportion_base_samevertex
Proof state before:
case intro.intro
i : incidence_geometry
a b c e f : point
L : line
bL : online b L
cL : online c L
eL : online e L
fL : online f L
aL : ¬online a L
M : line
aM : online a M
pLM : para L M
⊢ proportion (length b c) (length e f) (area a b c) (area a e f)
Tactic:
exact proportion_area_of_proportion_base aM bL cL aM eL fL pLM
Proof state after:
no goals
Theorem: proportional_iff_para
Proof state before:
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
Tactic:
have bN := online_3_of_B Badb aN dN
Proof state after:
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
Theorem: proportional_iff_para
Proof state before:
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
Tactic:
obtain ⟨O, aO, eO⟩ := line_of_pts a e
Proof state after:
case intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
Theorem: proportional_iff_para
Proof state before:
case intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
Tactic:
have cO := online_3_of_B Baec aO eO
Proof state after:
case intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
Theorem: proportional_iff_para
Proof state before:
case intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
Tactic:
obtain ⟨P, cP, dP⟩ := line_of_pts c d
Proof state after:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
Theorem: proportional_iff_para
Proof state before:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
Tactic:
have ab : a ≠ b := ne_13_of_B Badb
Proof state after:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
Theorem: proportional_iff_para
Proof state before:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
Tactic:
have ae : a ≠ e := ne_12_of_B Baec
Proof state after:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
Theorem: proportional_iff_para
Proof state before:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
Tactic:
have ad : a ≠ d := ne_12_of_B Badb
Proof state after:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
Theorem: proportional_iff_para
Proof state before:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
Tactic:
have bd : b ≠ d := ne_12_of_B (B_symm Badb)
Proof state after:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
Theorem: proportional_iff_para
Proof state before:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
Tactic:
have ce : c ≠ e := ne_12_of_B (B_symm Baec)
Proof state after:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
Theorem: proportional_iff_para
Proof state before:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
Tactic:
have NO : N ≠ O := fun NO => eN (by rwa [← NO] at eO)
Proof state after:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
Theorem: proportional_iff_para
Proof state before:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
Tactic:
have PO : P ≠ O := fun PO => NO (line_unique_of_pts ad aO (by rwa [PO] at dP) aN dN).symm
Proof state after:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
Theorem: proportional_iff_para
Proof state before:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
Tactic:
have dO := fun dO => NO (line_unique_of_pts ad aN dN aO dO)
Proof state after:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
Theorem: proportional_iff_para
Proof state before:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
Tactic:
have eP := fun eP => PO (line_unique_of_pts ce cP eP cO eO)
Proof state after:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
Theorem: proportional_iff_para
Proof state before:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
Tactic:
have aL := fun aL => eN (by rwa [line_unique_of_pts ad aL dL aN dN] at eL)
Proof state after:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
Theorem: proportional_iff_para
Proof state before:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
Tactic:
have bL := fun bL => eN (by rwa [line_unique_of_pts bd bL dL bN dN] at eL)
Proof state after:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
Theorem: proportional_iff_para
Proof state before:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
Tactic:
have cL := fun cL => (by rwa [← line_unique_of_pts ce cO eO cL eL] at aL : ¬ online a O) aO
Proof state after:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
Theorem: proportional_iff_para
Proof state before:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
Tactic:
have bc : b ≠ c := fun bc => NO (line_unique_of_pts ab aN bN aO (by rwa [← bc] at cO))
Proof state after:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
Theorem: proportional_iff_para
Proof state before:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
Tactic:
have cd : c ≠ d := fun cd => by rw [← cd] at dO; exact dO cO
Proof state after:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
cd : c ≠ d
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M