internlm/Lean-Github huggingface dataset:
Theorem: lt_area_of_lt_base
Proof state before:
case neg.intro.intro.intro.intro.intro.intro.intro.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
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
this✝ : ¬online f O
g : point
N : line
gM : online g M
gN : online g N
fN : online f N
pON : para O N
efgd : paragram e f g d L N M O
this : length e f = length d g
dg : d ≠ g
P : line
bP : online b P
dP : online d P
⊢ area a b c > area d e f
Tactic:
have := not_online_of_triangle bP dP dM gM (offline_of_para bL pLM) dg
Proof state after:
case neg.intro.intro.intro.intro.intro.intro.intro.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
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
this✝¹ : ¬online f O
g : point
N : line
gM : online g M
gN : online g N
fN : online f N
pON : para O N
efgd : paragram e f g d L N M O
this✝ : length e f = length d g
dg : d ≠ g
P : line
bP : online b P
dP : online d P
this : ¬online g P
⊢ area a b c > area d e f
Theorem: lt_area_of_lt_base
Proof state before:
case neg.intro.intro.intro.intro.intro.intro.intro.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
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
this✝¹ : ¬online f O
g : point
N : line
gM : online g M
gN : online g N
fN : online f N
pON : para O N
efgd : paragram e f g d L N M O
this✝ : length e f = length d g
dg : d ≠ g
P : line
bP : online b P
dP : online d P
this : ¬online g P
⊢ area a b c > area d e f
Tactic:
obtain ⟨ h, R, hL, hR, gR, pPR ⟩ := parallel_projection gM (para_symm pLM) (not_para_of_online_online dP dM) this
Proof state after:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.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
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
this✝¹ : ¬online f O
g : point
N : line
gM : online g M
gN : online g N
fN : online f N
pON : para O N
efgd : paragram e f g d L N M O
this✝ : length e f = length d g
dg : d ≠ g
P : line
bP : online b P
dP : online d P
this : ¬online g P
h : point
R : line
hL : online h L
hR : online h R
gR : online g R
pPR : para P R
⊢ area a b c > area d e f
Theorem: lt_area_of_lt_base
Proof state before:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.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
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
this✝¹ : ¬online f O
g : point
N : line
gM : online g M
gN : online g N
fN : online f N
pON : para O N
efgd : paragram e f g d L N M O
this✝ : length e f = length d g
dg : d ≠ g
P : line
bP : online b P
dP : online d P
this : ¬online g P
h : point
R : line
hL : online h L
hR : online h R
gR : online g R
pPR : para P R
⊢ area a b c > area d e f
Tactic:
have bhgd : paragram b h g d L R M P := by splitAll <;> perma only [para]
Proof state after:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.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
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
this✝¹ : ¬online f O
g : point
N : line
gM : online g M
gN : online g N
fN : online f N
pON : para O N
efgd : paragram e f g d L N M O
this✝ : length e f = length d g
dg : d ≠ g
P : line
bP : online b P
dP : online d P
this : ¬online g P
h : point
R : line
hL : online h L
hR : online h R
gR : online g R
pPR : para P R
bhgd : paragram b h g d L R M P
⊢ area a b c > area d e f
Theorem: lt_area_of_lt_base
Proof state before:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.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
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
this✝¹ : ¬online f O
g : point
N : line
gM : online g M
gN : online g N
fN : online f N
pON : para O N
efgd : paragram e f g d L N M O
this✝ : length e f = length d g
dg : d ≠ g
P : line
bP : online b P
dP : online d P
this : ¬online g P
h : point
R : line
hL : online h L
hR : online h R
gR : online g R
pPR : para P R
bhgd : paragram b h g d L R M P
⊢ area a b c > area d e f
Tactic:
have ef_bh : length e f = length b h := by linperm [(len_ang_area_eq_of_parallelogram bhgd).1]
Proof state after:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.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
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
this✝¹ : ¬online f O
g : point
N : line
gM : online g M
gN : online g N
fN : online f N
pON : para O N
efgd : paragram e f g d L N M O
this✝ : length e f = length d g
dg : d ≠ g
P : line
bP : online b P
dP : online d P
this : ¬online g P
h : point
R : line
hL : online h L
hR : online h R
gR : online g R
pPR : para P R
bhgd : paragram b h g d L R M P
ef_bh : length e f = length b h
⊢ area a b c > area d e f
Theorem: lt_area_of_lt_base
Proof state before:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.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
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
this✝¹ : ¬online f O
g : point
N : line
gM : online g M
gN : online g N
fN : online f N
pON : para O N
efgd : paragram e f g d L N M O
this✝ : length e f = length d g
dg : d ≠ g
P : line
bP : online b P
dP : online d P
this : ¬online g P
h : point
R : line
hL : online h L
hR : online h R
gR : online g R
pPR : para P R
bhgd : paragram b h g d L R M P
ef_bh : length e f = length b h
⊢ area a b c > area d e f
Tactic:
have bh : b ≠ h := ne_of_ne_len ef ef_bh
Proof state after:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.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
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
this✝¹ : ¬online f O
g : point
N : line
gM : online g M
gN : online g N
fN : online f N
pON : para O N
efgd : paragram e f g d L N M O
this✝ : length e f = length d g
dg : d ≠ g
P : line
bP : online b P
dP : online d P
this : ¬online g P
h : point
R : line
hL : online h L
hR : online h R
gR : online g R
pPR : para P R
bhgd : paragram b h g d L R M P
ef_bh : length e f = length b h
bh : b ≠ h
⊢ area a b c > area d e f
Theorem: lt_area_of_lt_base
Proof state before:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.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
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
this✝¹ : ¬online f O
g : point
N : line
gM : online g M
gN : online g N
fN : online f N
pON : para O N
efgd : paragram e f g d L N M O
this✝ : length e f = length d g
dg : d ≠ g
P : line
bP : online b P
dP : online d P
this : ¬online g P
h : point
R : line
hL : online h L
hR : online h R
gR : online g R
pPR : para P R
bhgd : paragram b h g d L R M P
ef_bh : length e f = length b h
bh : b ≠ h
⊢ area a b c > area d e f
Tactic:
rw [eq_area_of_eq_base dM eL fL aM bL hL pLM ef_bh]
Proof state after:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.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
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
this✝¹ : ¬online f O
g : point
N : line
gM : online g M
gN : online g N
fN : online f N
pON : para O N
efgd : paragram e f g d L N M O
this✝ : length e f = length d g
dg : d ≠ g
P : line
bP : online b P
dP : online d P
this : ¬online g P
h : point
R : line
hL : online h L
hR : online h R
gR : online g R
pPR : para P R
bhgd : paragram b h g d L R M P
ef_bh : length e f = length b h
bh : b ≠ h
⊢ area a b c > area a b h
Theorem: lt_area_of_lt_base
Proof state before:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.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
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
this✝¹ : ¬online f O
g : point
N : line
gM : online g M
gN : online g N
fN : online f N
pON : para O N
efgd : paragram e f g d L N M O
this✝ : length e f = length d g
dg : d ≠ g
P : line
bP : online b P
dP : online d P
this : ¬online g P
h : point
R : line
hL : online h L
hR : online h R
gR : online g R
pPR : para P R
bhgd : paragram b h g d L R M P
ef_bh : length e f = length b h
bh : b ≠ h
⊢ area a b c > area a b h
Tactic:
have : length b c > length b h := by rw [← ef_bh]; exact hlen
Proof state after:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.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
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
this✝² : ¬online f O
g : point
N : line
gM : online g M
gN : online g N
fN : online f N
pON : para O N
efgd : paragram e f g d L N M O
this✝¹ : length e f = length d g
dg : d ≠ g
P : line
bP : online b P
dP : online d P
this✝ : ¬online g P
h : point
R : line
hL : online h L
hR : online h R
gR : online g R
pPR : para P R
bhgd : paragram b h g d L R M P
ef_bh : length e f = length b h
bh : b ≠ h
this : length b c > length b h
⊢ area a b c > area a b h
Theorem: lt_area_of_lt_base
Proof state before:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.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
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
this✝² : ¬online f O
g : point
N : line
gM : online g M
gN : online g N
fN : online f N
pON : para O N
efgd : paragram e f g d L N M O
this✝¹ : length e f = length d g
dg : d ≠ g
P : line
bP : online b P
dP : online d P
this✝ : ¬online g P
h : point
R : line
hL : online h L
hR : online h R
gR : online g R
pPR : para P R
bhgd : paragram b h g d L R M P
ef_bh : length e f = length b h
bh : b ≠ h
this : length b c > length b h
⊢ area a b c > area a b h
Tactic:
exact lt_area_of_lt_base_sameedge a bL cL hL bc bh aL this
Proof state after:
no goals
Theorem: lt_area_of_lt_base
Proof state before:
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
hlen : length b c > length e f
bc : b = c
⊢ False
Tactic:
rw [length_eq_zero_iff.mpr bc] at hlen
Proof state after:
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
hlen : 0 > length e f
bc : b = c
⊢ False
Theorem: lt_area_of_lt_base
Proof state before:
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
hlen : 0 > length e f
bc : b = c
⊢ False
Tactic:
exact (not_le_of_gt hlen) (length_nonneg e f)
Proof state after:
no goals
Theorem: lt_area_of_lt_base
Proof state before:
case pos
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
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : e = f
⊢ area a b c > area d e f
Tactic:
perm [(area_zero_iff_online bc bL cL).not.mpr aL]
Proof state after:
case pos
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
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : e = f
this : ¬area a b c = 0
⊢ area a b c > area d e f
Theorem: lt_area_of_lt_base
Proof state before:
case pos
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
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : e = f
this : ¬area a b c = 0
⊢ area a b c > area d e f
Tactic:
rw [area_of_eq d e f (by tauto)]
Proof state after:
case pos
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
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : e = f
this : ¬area a b c = 0
⊢ area a b c > 0
Theorem: lt_area_of_lt_base
Proof state before:
case pos
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
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : e = f
this : ¬area a b c = 0
⊢ area a b c > 0
Tactic:
exact (Ne.symm this).lt_of_le (area_nonneg a b c)
Proof state after:
no goals
Theorem: lt_area_of_lt_base
Proof state before:
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
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : e = f
this : ¬area a b c = 0
⊢ d = e ∨ d = f ∨ e = f
Tactic:
tauto
Proof state after:
no goals
Theorem: lt_area_of_lt_base
Proof state before:
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
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
this : ¬online f O
g : point
N : line
gM : online g M
gN : online g N
fN : online f N
pON : para O N
⊢ paragram e f g d L N M O
Tactic:
splitAll <;> perma only [para] at *
Proof state after:
no goals
Theorem: lt_area_of_lt_base
Proof state before:
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
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
this✝¹ : ¬online f O
g : point
N : line
gM : online g M
gN : online g N
fN : online f N
pON : para O N
efgd : paragram e f g d L N M O
this✝ : length e f = length d g
dg : d ≠ g
P : line
bP : online b P
dP : online d P
this : ¬online g P
h : point
R : line
hL : online h L
hR : online h R
gR : online g R
pPR : para P R
⊢ paragram b h g d L R M P
Tactic:
splitAll <;> perma only [para]
Proof state after:
no goals
Theorem: lt_area_of_lt_base
Proof state before:
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
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
this✝¹ : ¬online f O
g : point
N : line
gM : online g M
gN : online g N
fN : online f N
pON : para O N
efgd : paragram e f g d L N M O
this✝ : length e f = length d g
dg : d ≠ g
P : line
bP : online b P
dP : online d P
this : ¬online g P
h : point
R : line
hL : online h L
hR : online h R
gR : online g R
pPR : para P R
bhgd : paragram b h g d L R M P
⊢ length e f = length b h
Tactic:
linperm [(len_ang_area_eq_of_parallelogram bhgd).1]
Proof state after:
no goals
Theorem: lt_area_of_lt_base
Proof state before:
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
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
this✝¹ : ¬online f O
g : point
N : line
gM : online g M
gN : online g N
fN : online f N
pON : para O N
efgd : paragram e f g d L N M O
this✝ : length e f = length d g
dg : d ≠ g
P : line
bP : online b P
dP : online d P
this : ¬online g P
h : point
R : line
hL : online h L
hR : online h R
gR : online g R
pPR : para P R
bhgd : paragram b h g d L R M P
ef_bh : length e f = length b h
bh : b ≠ h
⊢ length b c > length b h
Tactic:
rw [← ef_bh]
Proof state after:
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
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
this✝¹ : ¬online f O
g : point
N : line
gM : online g M
gN : online g N
fN : online f N
pON : para O N
efgd : paragram e f g d L N M O
this✝ : length e f = length d g
dg : d ≠ g
P : line
bP : online b P
dP : online d P
this : ¬online g P
h : point
R : line
hL : online h L
hR : online h R
gR : online g R
pPR : para P R
bhgd : paragram b h g d L R M P
ef_bh : length e f = length b h
bh : b ≠ h
⊢ length b c > length e f
Theorem: lt_area_of_lt_base
Proof state before:
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
hlen : length b c > length e f
bc : b ≠ c
aL : ¬online a L
dL : ¬online d L
ef : ¬e = f
O : line
dO : online d O
eO : online e O
this✝¹ : ¬online f O
g : point
N : line
gM : online g M
gN : online g N
fN : online f N
pON : para O N
efgd : paragram e f g d L N M O
this✝ : length e f = length d g
dg : d ≠ g
P : line
bP : online b P
dP : online d P
this : ¬online g P
h : point
R : line
hL : online h L
hR : online h R
gR : online g R
pPR : para P R
bhgd : paragram b h g d L R M P
ef_bh : length e f = length b h
bh : b ≠ h
⊢ length b c > length e f
Tactic:
exact hlen
Proof state after:
no goals
Theorem: proportion_area_of_proportion_base
Proof state before:
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
⊢ proportion (length b c) (length e f) (area a b c) (area d e f)
Tactic:
refine' ⟨ length_nonneg b c, length_nonneg e f, area_nonneg a b c, area_nonneg d e f, _ ⟩
Proof state after:
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 : ℕ),
    (↑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)
Theorem: proportion_area_of_proportion_base
Proof state before:
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 : ℕ),
    (↑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:
intros n m
Proof state after:
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 : ℕ
⊢ (↑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)
Theorem: proportion_area_of_proportion_base
Proof state before:
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 : ℕ
⊢ (↑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:
obtain ⟨ h, Hh ⟩ := rescale_length n bL cL
Proof state after:
case 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)
⊢ (↑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)
Theorem: proportion_area_of_proportion_base
Proof state before:
case 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)
⊢ (↑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:
obtain ⟨ l, Hl ⟩ := rescale_length m eL fL
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)
⊢ (↑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)