Theorem: proportion_inv (Pythagoras/proportion.lean)

State before:
r s t u : ℝ
h : proportion r s t u
⊢ proportion s r u t
Tactic:
dsimp [proportion] at *
State after:
r s t u : ℝ
h :
  0 ≤ r ∧
    0 ≤ s ∧
      0 ≤ t ∧
        0 ≤ u ∧
          ∀ (n m : ℕ),
            (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧
              (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
⊢ 0 ≤ s ∧
    0 ≤ r ∧
      0 ≤ u ∧
        0 ≤ t ∧
          ∀ (n m : ℕ),
            (↑n * s = ↑m * r → ↑n * u = ↑m * t) ∧
              (↑n * s < ↑m * r → ↑n * u < ↑m * t) ∧ (↑m * r < ↑n * s → ↑m * t < ↑n * u)

State before:
r s t u : ℝ
h :
  0 ≤ r ∧
    0 ≤ s ∧
      0 ≤ t ∧
        0 ≤ u ∧
          ∀ (n m : ℕ),
            (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧
              (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
⊢ 0 ≤ s ∧
    0 ≤ r ∧
      0 ≤ u ∧
        0 ≤ t ∧
          ∀ (n m : ℕ),
            (↑n * s = ↑m * r → ↑n * u = ↑m * t) ∧
              (↑n * s < ↑m * r → ↑n * u < ↑m * t) ∧ (↑m * r < ↑n * s → ↑m * t < ↑n * u)
Tactic:
refine ⟨h.2.1, h.1, h.2.2.2.1, h.2.2.1, ?_⟩
State after:
r s t u : ℝ
h :
  0 ≤ r ∧
    0 ≤ s ∧
      0 ≤ t ∧
        0 ≤ u ∧
          ∀ (n m : ℕ),
            (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧
              (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
⊢ ∀ (n m : ℕ),
    (↑n * s = ↑m * r → ↑n * u = ↑m * t) ∧ (↑n * s < ↑m * r → ↑n * u < ↑m * t) ∧ (↑m * r < ↑n * s → ↑m * t < ↑n * u)

State before:
r s t u : ℝ
h :
  0 ≤ r ∧
    0 ≤ s ∧
      0 ≤ t ∧
        0 ≤ u ∧
          ∀ (n m : ℕ),
            (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧
              (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
⊢ ∀ (n m : ℕ),
    (↑n * s = ↑m * r → ↑n * u = ↑m * t) ∧ (↑n * s < ↑m * r → ↑n * u < ↑m * t) ∧ (↑m * r < ↑n * s → ↑m * t < ↑n * u)
Tactic:
intro n m
State after:
r s t u : ℝ
h :
  0 ≤ r ∧
    0 ≤ s ∧
      0 ≤ t ∧
        0 ≤ u ∧
          ∀ (n m : ℕ),
            (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧
              (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
n m : ℕ
⊢ (↑n * s = ↑m * r → ↑n * u = ↑m * t) ∧ (↑n * s < ↑m * r → ↑n * u < ↑m * t) ∧ (↑m * r < ↑n * s → ↑m * t < ↑n * u)

State before:
r s t u : ℝ
h :
  0 ≤ r ∧
    0 ≤ s ∧
      0 ≤ t ∧
        0 ≤ u ∧
          ∀ (n m : ℕ),
            (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧
              (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
n m : ℕ
⊢ (↑n * s = ↑m * r → ↑n * u = ↑m * t) ∧ (↑n * s < ↑m * r → ↑n * u < ↑m * t) ∧ (↑m * r < ↑n * s → ↑m * t < ↑n * u)
Tactic:
have := h.2.2.2.2 m n
State after:
r s t u : ℝ
h :
  0 ≤ r ∧
    0 ≤ s ∧
      0 ≤ t ∧
        0 ≤ u ∧
          ∀ (n m : ℕ),
            (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧
              (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
n m : ℕ
this : (↑m * r = ↑n * s → ↑m * t = ↑n * u) ∧ (↑m * r < ↑n * s → ↑m * t < ↑n * u) ∧ (↑n * s < ↑m * r → ↑n * u < ↑m * t)
⊢ (↑n * s = ↑m * r → ↑n * u = ↑m * t) ∧ (↑n * s < ↑m * r → ↑n * u < ↑m * t) ∧ (↑m * r < ↑n * s → ↑m * t < ↑n * u)

State before:
r s t u : ℝ
h :
  0 ≤ r ∧
    0 ≤ s ∧
      0 ≤ t ∧
        0 ≤ u ∧
          ∀ (n m : ℕ),
            (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧
              (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
n m : ℕ
this : (↑m * r = ↑n * s → ↑m * t = ↑n * u) ∧ (↑m * r < ↑n * s → ↑m * t < ↑n * u) ∧ (↑n * s < ↑m * r → ↑n * u < ↑m * t)
⊢ (↑n * s = ↑m * r → ↑n * u = ↑m * t) ∧ (↑n * s < ↑m * r → ↑n * u < ↑m * t) ∧ (↑m * r < ↑n * s → ↑m * t < ↑n * u)
Tactic:
exact ⟨fun h => (this.1 h.symm).symm, ⟨fun h => (this.2.2 h), fun h => (this.2.1 h)⟩⟩
State after:
no goals