Theorem: Imo1974P5.T_continuous (Compfiles/Imo1974P5.lean)

State before:
⊢ ContinuousOn T (Set.Icc 0 1)
Tactic:
unfold T S
State after:
⊢ ContinuousOn
    (fun t =>
      1 / (1 + (1 - t) + t * (1 - t)) + (1 - t) / (1 + (1 - t) + t) + t / (1 - t + t + t * (1 - t)) +
        t * (1 - t) / (1 + t + t * (1 - t)))
    (Set.Icc 0 1)

State before:
⊢ ContinuousOn
    (fun t =>
      1 / (1 + (1 - t) + t * (1 - t)) + (1 - t) / (1 + (1 - t) + t) + t / (1 - t + t + t * (1 - t)) +
        t * (1 - t) / (1 + t + t * (1 - t)))
    (Set.Icc 0 1)
Tactic:
fun_prop (disch := (rintro x ⟨a,b⟩; nlinarith))
State after:
no goals

State before:
case funProp.discharger

⊢ ∀ x ∈ Set.Icc 0 1, 1 + x + x * (1 - x) ≠ 0
Tactic:
(rintro x ⟨a,b⟩; nlinarith)
State after:
no goals

State before:
case funProp.discharger

⊢ ∀ x ∈ Set.Icc 0 1, 1 + x + x * (1 - x) ≠ 0
Tactic:
rintro x ⟨a,b⟩
State after:
case funProp.discharger.intro
x : ℝ
a : 0 ≤ x
b : x ≤ 1
⊢ 1 + x + x * (1 - x) ≠ 0

State before:
case funProp.discharger.intro
x : ℝ
a : 0 ≤ x
b : x ≤ 1
⊢ 1 + x + x * (1 - x) ≠ 0
Tactic:
nlinarith
State after:
no goals