Theorem: proportion_area_of_proportion_base (Pythagoras/euclid_VI.lean)

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, _ ⟩
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)

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
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)

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
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)

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
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)

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]
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)

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]
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)

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 ⟩
State after:
no goals