awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Ceva (hypothesis)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : SeminormedAddCommGroup V
inst_1 : NormedField 𝕜
inst_2 : NormedSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
t : Triangle 𝕜 P
p : Fin 3 → P
p' : P
hp0 : ∀ (i : Fin 3), p i ≠ t.points (i + 2)
hp : ∀ (i : Fin 3), Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 {t.points (i + 1), t.points (i + 2)}) (p i)
hp' : ∀ (i : Fin 3), Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 {t.points i, p i}) p'
aux : ∀ (i : Fin 3), dist (p i) (t.points (i + 2)) ≠ 0
key :
  dist (t.points (HAdd.hAdd (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 0 1)) (p 0) *
        dist (t.points (HAdd.hAdd (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 1 1)) (p 1) *
      dist (t.points (HAdd.hAdd (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 2 1)) (p 2) =
    ∏ i : Fin 3, dist (p i) (t.points (i + 2))
⊢ dist (t.points (HAdd.hAdd (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 0 1)) (p 0) /
          dist (p 0) (t.points (HAdd.hAdd (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 0 2)) *
        (dist (t.points (HAdd.hAdd (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 1 1)) (p 1) /
          dist (p 1) (t.points (HAdd.hAdd (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 1 2))) *
      (dist (t.points (HAdd.hAdd (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 2 1)) (p 2) /
        dist (p 2) (t.points (HAdd.hAdd (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 2 2))) =
    1
have key₁ : dist (t.points (HAdd.hAdd (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 0 1)) (p 0) *
      dist (t.points (HAdd.hAdd (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 1 1)) (p 1) *
    dist (t.points (HAdd.hAdd (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 2 1)) (p 2) =
  dist (p 0) (t.points (HAdd.hAdd (α := Fin 3) 0 2)) * dist (p 1) (t.points (HAdd.hAdd (α := Fin 3) 1 2)) *
    dist (p 2) (t.points (HAdd.hAdd (α := Fin 3) 2 2))
Tactic: rw [Fin.prod_univ_three] at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Ceva (hypothesis)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : SeminormedAddCommGroup V
inst_1 : NormedField 𝕜
inst_2 : NormedSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
t : Triangle 𝕜 P
p : Fin 3 → P
p' : P
hp0 : ∀ (i : Fin 3), p i ≠ t.points (i + 2)
hp : ∀ (i : Fin 3), Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 {t.points (i + 1), t.points (i + 2)}) (p i)
hp' : ∀ (i : Fin 3), Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 {t.points i, p i}) p'
aux : ∀ (i : Fin 3), dist (p i) (t.points (i + 2)) ≠ 0
key :
  dist (t.points (HAdd.hAdd (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 0 1)) (p 0) *
        dist (t.points (HAdd.hAdd (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 1 1)) (p 1) *
      dist (t.points (HAdd.hAdd (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 2 1)) (p 2) =
    dist (p 0) (t.points (HAdd.hAdd (α := Fin 3) 0 2)) * dist (p 1) (t.points (HAdd.hAdd (α := Fin 3) 1 2)) *
      dist (p 2) (t.points (HAdd.hAdd (α := Fin 3) 2 2))
⊢ dist (t.points (HAdd.hAdd (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 0 1)) (p 0) /
          dist (p 0) (t.points (HAdd.hAdd (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 0 2)) *
        (dist (t.points (HAdd.hAdd (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 1 1)) (p 1) /
          dist (p 1) (t.points (HAdd.hAdd (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 1 2))) *
      (dist (t.points (HAdd.hAdd (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 2 1)) (p 2) /
        dist (p 2) (t.points (HAdd.hAdd (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 2 2))) =
    1
have this : dist (p 0) (t.points (HAdd.hAdd (α := Fin 3) 0 2)) ≠ 0
Tactic: have := aux 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Ceva (hypothesis)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : SeminormedAddCommGroup V
inst_1 : NormedField 𝕜
inst_2 : NormedSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
t : Triangle 𝕜 P
p : Fin 3 → P
p' : P
hp0 : ∀ (i : Fin 3), p i ≠ t.points (i + 2)
hp : ∀ (i : Fin 3), Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 {t.points (i + 1), t.points (i + 2)}) (p i)
hp' : ∀ (i : Fin 3), Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 {t.points i, p i}) p'
aux : ∀ (i : Fin 3), dist (p i) (t.points (i + 2)) ≠ 0
key :
  dist (t.points (HAdd.hAdd (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 0 1)) (p 0) *
        dist (t.points (HAdd.hAdd (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 1 1)) (p 1) *
      dist (t.points (HAdd.hAdd (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 2 1)) (p 2) =
    dist (p 0) (t.points (HAdd.hAdd (α := Fin 3) 0 2)) * dist (p 1) (t.points (HAdd.hAdd (α := Fin 3) 1 2)) *
      dist (p 2) (t.points (HAdd.hAdd (α := Fin 3) 2 2))
this : dist (p 0) (t.points (HAdd.hAdd (α := Fin 3) 0 2)) ≠ 0
⊢ dist (t.points (HAdd.hAdd (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 0 1)) (p 0) /
          dist (p 0) (t.points (HAdd.hAdd (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 0 2)) *
        (dist (t.points (HAdd.hAdd (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 1 1)) (p 1) /
          dist (p 1) (t.points (HAdd.hAdd (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 1 2))) *
      (dist (t.points (HAdd.hAdd (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 2 1)) (p 2) /
        dist (p 2) (t.points (HAdd.hAdd (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 2 2))) =
    1
have this₁ : dist (p 1) (t.points (HAdd.hAdd (α := Fin 3) 1 2)) ≠ 0
Tactic: have := aux 1
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Ceva (hypothesis)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : SeminormedAddCommGroup V
inst_1 : NormedField 𝕜
inst_2 : NormedSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
t : Triangle 𝕜 P
p : Fin 3 → P
p' : P
hp0 : ∀ (i : Fin 3), p i ≠ t.points (i + 2)
hp : ∀ (i : Fin 3), Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 {t.points (i + 1), t.points (i + 2)}) (p i)
hp' : ∀ (i : Fin 3), Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 {t.points i, p i}) p'
aux : ∀ (i : Fin 3), dist (p i) (t.points (i + 2)) ≠ 0
key :
  dist (t.points (HAdd.hAdd (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 0 1)) (p 0) *
        dist (t.points (HAdd.hAdd (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 1 1)) (p 1) *
      dist (t.points (HAdd.hAdd (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 2 1)) (p 2) =
    dist (p 0) (t.points (HAdd.hAdd (α := Fin 3) 0 2)) * dist (p 1) (t.points (HAdd.hAdd (α := Fin 3) 1 2)) *
      dist (p 2) (t.points (HAdd.hAdd (α := Fin 3) 2 2))
this_1 : dist (p 0) (t.points (HAdd.hAdd (α := Fin 3) 0 2)) ≠ 0
this : dist (p 1) (t.points (HAdd.hAdd (α := Fin 3) 1 2)) ≠ 0
⊢ dist (t.points (HAdd.hAdd (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 0 1)) (p 0) /
          dist (p 0) (t.points (HAdd.hAdd (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 0 2)) *
        (dist (t.points (HAdd.hAdd (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 1 1)) (p 1) /
          dist (p 1) (t.points (HAdd.hAdd (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 1 2))) *
      (dist (t.points (HAdd.hAdd (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 2 1)) (p 2) /
        dist (p 2) (t.points (HAdd.hAdd (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 2 2))) =
    1
have this₁ : dist (p 2) (t.points (HAdd.hAdd (α := Fin 3) 2 2)) ≠ 0
Tactic: have := aux 2
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.ContinuousAffineMap (goal)
Goal:
𝕜 : Type u_1
V : Type u_3
W : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedSpace 𝕜 V
inst_4 : NormedSpace 𝕜 W
f : V →ᴬ[𝕜] W
h : Eq.{u_4 + 1} (α := W) ((f : (a : V) → W) 0 : W) (0 : W)
⊢ ‖f‖ = max (norm.{u_4} (E := W) ((f : (a : V) → W) 0 : W)) (norm (E := V →L[𝕜] W) f.contLinear)
have rw : max (norm.{u_4} (E := W) ((f : (a : V) → W) 0 : W)) (norm (E := V →L[𝕜] W) f.contLinear) =
  max (norm.{u_4} (E := W) ((f : (a : V) → W) 0 : W)) (norm (E := V →L[𝕜] W) f.contLinear)
Tactic: rw [norm_def]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.ContinuousAffineMap (goal)
Goal:
𝕜 : Type u_1
V : Type u_3
W : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedSpace 𝕜 V
inst_4 : NormedSpace 𝕜 W
f : V →ᴬ[𝕜] W
h : Eq.{u_4 + 1} (α := W) ((f : (a : V) → W) 0 : W) (0 : W)
⊢ max (norm.{u_4} (E := W) ((f : (a : V) → W) 0 : W)) (norm (E := V →L[𝕜] W) f.contLinear) =
    max 0 (norm (E := V →L[𝕜] W) f.contLinear)
have rw : max (norm.{u_4} (E := W) 0) (norm (E := V →L[𝕜] W) f.contLinear) = max 0 (norm (E := V →L[𝕜] W) f.contLinear)
Tactic: rw [h, norm_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.ContinuousAffineMap (goal)
Goal:
𝕜 : Type u_1
V : Type u_3
W : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedSpace 𝕜 V
inst_4 : NormedSpace 𝕜 W
f : V →ᴬ[𝕜] W
h : Eq.{u_4 + 1} (α := W) ((f : (a : V) → W) 0 : W) (0 : W)
rw : max (norm.{u_4} (E := W) 0) (norm (E := V →L[𝕜] W) f.contLinear) = max 0 (norm (E := V →L[𝕜] W) f.contLinear)
⊢ max (norm.{u_4} (E := W) ((f : (a : V) → W) 0 : W)) (norm (E := V →L[𝕜] W) f.contLinear) =
    max 0 (norm (E := V →L[𝕜] W) f.contLinear)
have rw₁ : max 0 (norm (E := V →L[𝕜] W) f.contLinear) = max 0 (norm (E := V →L[𝕜] W) f.contLinear)
Tactic: rw [h, norm_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.ContinuousAffineMap (goal)
Goal:
𝕜 : Type u_1
V : Type u_3
W : Type u_4
W₂ : Type u_5
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
inst_2 : SeminormedAddCommGroup W₂
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 V
inst_5 : NormedSpace 𝕜 W
inst_6 : NormedSpace 𝕜 W₂
f : V →ᴬ[𝕜] W
g : W₂ →ᴬ[𝕜] V
⊢ ‖f.comp g‖ ≤ ‖f‖ * ‖g‖ + norm.{u_4} (E := W) ((f : (a : V) → W) 0 : W)
have rw : norm.{u_4} (E := W) ((f.comp g : (a : W₂) → W) 0 : W) ≤ ‖f‖ * ‖g‖ + norm.{u_4} (E := W) ((f : (a : V) → W) 0 : W) ∧
  norm (E := W₂ →L[𝕜] W) (f.comp g).contLinear ≤ ‖f‖ * ‖g‖ + norm.{u_4} (E := W) ((f : (a : V) → W) 0 : W)
Tactic: rw [norm_def, max_le_iff]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.ContinuousAffineMap (goal)
Goal:
𝕜 : Type u_1
V : Type u_3
W : Type u_4
W₂ : Type u_5
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
inst_2 : SeminormedAddCommGroup W₂
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 V
inst_5 : NormedSpace 𝕜 W
inst_6 : NormedSpace 𝕜 W₂
f : V →ᴬ[𝕜] W
g : W₂ →ᴬ[𝕜] V
⊢ norm.{u_4} (E := W) ((f.comp g : (a : W₂) → W) 0 : W) ≤ ‖f‖ * ‖g‖ + norm.{u_4} (E := W) ((f : (a : V) → W) 0 : W) ∧
    norm (E := W₂ →L[𝕜] W) (f.comp g).contLinear ≤ ‖f‖ * ‖g‖ + norm.{u_4} (E := W) ((f : (a : V) → W) 0 : W)
have left : norm.{u_4} (E := W) ((f.comp g : (a : W₂) → W) 0 : W) ≤ ‖f‖ * ‖g‖ + norm.{u_4} (E := W) ((f : (a : V) → W) 0 : W)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.ContinuousAffineMap (goal)
Goal:
𝕜 : Type u_1
V : Type u_3
W : Type u_4
W₂ : Type u_5
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
inst_2 : SeminormedAddCommGroup W₂
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 V
inst_5 : NormedSpace 𝕜 W
inst_6 : NormedSpace 𝕜 W₂
f : V →ᴬ[𝕜] W
g : W₂ →ᴬ[𝕜] V
left : norm.{u_4} (E := W) ((f.comp g : (a : W₂) → W) 0 : W) ≤ ‖f‖ * ‖g‖ + norm.{u_4} (E := W) ((f : (a : V) → W) 0 : W)
⊢ norm.{u_4} (E := W) ((f.comp g : (a : W₂) → W) 0 : W) ≤ ‖f‖ * ‖g‖ + norm.{u_4} (E := W) ((f : (a : V) → W) 0 : W) ∧
    norm (E := W₂ →L[𝕜] W) (f.comp g).contLinear ≤ ‖f‖ * ‖g‖ + norm.{u_4} (E := W) ((f : (a : V) → W) 0 : W)
have right : norm (E := W₂ →L[𝕜] W) (f.comp g).contLinear ≤ ‖f‖ * ‖g‖ + norm.{u_4} (E := W) ((f : (a : V) → W) 0 : W)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.ContinuousAffineMap (goal)
Goal:
𝕜 : Type u_1
V : Type u_3
W : Type u_4
W₂ : Type u_5
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
inst_2 : SeminormedAddCommGroup W₂
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 V
inst_5 : NormedSpace 𝕜 W
inst_6 : NormedSpace 𝕜 W₂
f : V →ᴬ[𝕜] W
g : W₂ →ᴬ[𝕜] V
⊢ norm.{u_4} (E := W) ((f : (a : V) → W) ((g : (a : W₂) → V) 0 : V) : W) =
    ‖HAdd.hAdd (α := W) (β := W) ((f.contLinear : (a : V) → W) ((g : (a : W₂) → V) 0 : V) : W)
        ((f : (a : V) → W) 0 : W)‖
have rw : ‖HAdd.hAdd (α := (a : V) → W) (β := V → W) (⇑f.contLinear : (a : V) → W)
      (Function.const V ((f : (a : V) → W) 0) : V → W) ((g : (a : W₂) → V) 0)‖ =
  ‖HAdd.hAdd (α := W) ((f.contLinear : (a : V) → W) ((g : (a : W₂) → V) 0 : V) : W)
      (HAdd.hAdd (α := (a : V) → W) (β := V → W) (⇑f.contLinear : (a : V) → W)
        (Function.const V ((f : (a : V) → W) 0) : V → W) 0)‖
Tactic: rw [f.decomp]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.ContinuousAffineMap (goal)
Goal:
𝕜 : Type u_1
V : Type u_3
W : Type u_4
W₂ : Type u_5
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
inst_2 : SeminormedAddCommGroup W₂
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 V
inst_5 : NormedSpace 𝕜 W
inst_6 : NormedSpace 𝕜 W₂
f : V →ᴬ[𝕜] W
g : W₂ →ᴬ[𝕜] V
⊢ ‖HAdd.hAdd (α := W) (β := W) ((f.contLinear : (a : V) → W) ((g : (a : W₂) → V) 0 : V) : W)
        ((f : (a : V) → W) 0 : W)‖ ≤
    norm (E := V →L[𝕜] W) f.contLinear * norm.{u_3} (E := V) ((g : (a : W₂) → V) 0 : V) +
      norm.{u_4} (E := W) ((f : (a : V) → W) 0 : W)
have grw : norm.{u_4} (E := W) ((f.contLinear : (a : V) → W) ((g : (a : W₂) → V) 0 : V) : W) +
    norm.{u_4} (E := W) ((f : (a : V) → W) 0 : W) ≤
  norm (E := V →L[𝕜] W) f.contLinear * norm.{u_3} (E := V) ((g : (a : W₂) → V) 0 : V) +
    norm.{u_4} (E := W) ((f : (a : V) → W) 0 : W)
Tactic: grw [norm_add_le, f.contLinear.le_opNorm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.ContinuousAffineMap (goal)
Goal:
𝕜 : Type u_1
V : Type u_3
W : Type u_4
W₂ : Type u_5
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
inst_2 : SeminormedAddCommGroup W₂
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 V
inst_5 : NormedSpace 𝕜 W
inst_6 : NormedSpace 𝕜 W₂
f : V →ᴬ[𝕜] W
g : W₂ →ᴬ[𝕜] V
grw :
  norm.{u_4} (E := W) ((f.contLinear : (a : V) → W) ((g : (a : W₂) → V) 0 : V) : W) +
      norm.{u_4} (E := W) ((f : (a : V) → W) 0 : W) ≤
    norm (E := V →L[𝕜] W) f.contLinear * norm.{u_3} (E := V) ((g : (a : W₂) → V) 0 : V) +
      norm.{u_4} (E := W) ((f : (a : V) → W) 0 : W)
⊢ ‖HAdd.hAdd (α := W) (β := W) ((f.contLinear : (a : V) → W) ((g : (a : W₂) → V) 0 : V) : W)
        ((f : (a : V) → W) 0 : W)‖ ≤
    norm (E := V →L[𝕜] W) f.contLinear * norm.{u_3} (E := V) ((g : (a : W₂) → V) 0 : V) +
      norm.{u_4} (E := W) ((f : (a : V) → W) 0 : W)
have grw₁ : norm (E := V →L[𝕜] W) f.contLinear * norm.{u_3} (E := V) ((g : (a : W₂) → V) 0 : V) +
    norm.{u_4} (E := W) ((f : (a : V) → W) 0 : W) ≤
  norm (E := V →L[𝕜] W) f.contLinear * norm.{u_3} (E := V) ((g : (a : W₂) → V) 0 : V) +
    norm.{u_4} (E := W) ((f : (a : V) → W) 0 : W)
Tactic: grw [norm_add_le, f.contLinear.le_opNorm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.ContinuousAffineMap (goal)
Goal:
𝕜 : Type u_1
V : Type u_3
W : Type u_4
W₂ : Type u_5
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
inst_2 : SeminormedAddCommGroup W₂
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 V
inst_5 : NormedSpace 𝕜 W
inst_6 : NormedSpace 𝕜 W₂
f : V →ᴬ[𝕜] W
g : W₂ →ᴬ[𝕜] V
⊢ norm (E := V →L[𝕜] W) f.contLinear * norm.{u_3} (E := V) ((g : (a : W₂) → V) 0 : V) +
      norm.{u_4} (E := W) ((f : (a : V) → W) 0 : W) ≤
    ‖f‖ * ‖g‖ + norm.{u_4} (E := W) ((f : (a : V) → W) 0 : W)
have h₁ : 0 ≤ norm.{u_3} (E := V) ((g : (a : W₂) → V) 0 : V)
Tactic: grw [f.norm_contLinear_le, g.norm_image_zero_le]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.ContinuousAffineMap (goal)
Goal:
𝕜 : Type u_1
V : Type u_3
W : Type u_4
W₂ : Type u_5
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
inst_2 : SeminormedAddCommGroup W₂
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 V
inst_5 : NormedSpace 𝕜 W
inst_6 : NormedSpace 𝕜 W₂
f : V →ᴬ[𝕜] W
g : W₂ →ᴬ[𝕜] V
h₁ : 0 ≤ norm.{u_3} (E := V) ((g : (a : W₂) → V) 0 : V)
⊢ norm (E := V →L[𝕜] W) f.contLinear * norm.{u_3} (E := V) ((g : (a : W₂) → V) 0 : V) +
      norm.{u_4} (E := W) ((f : (a : V) → W) 0 : W) ≤
    ‖f‖ * ‖g‖ + norm.{u_4} (E := W) ((f : (a : V) → W) 0 : W)
have grw : ‖f‖ * norm.{u_3} (E := V) ((g : (a : W₂) → V) 0 : V) + norm.{u_4} (E := W) ((f : (a : V) → W) 0 : W) ≤
  ‖f‖ * ‖g‖ + norm.{u_4} (E := W) ((f : (a : V) → W) 0 : W)
Tactic: grw [f.norm_contLinear_le, g.norm_image_zero_le]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.ContinuousAffineMap (goal)
Goal:
𝕜 : Type u_1
V : Type u_3
W : Type u_4
W₂ : Type u_5
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
inst_2 : SeminormedAddCommGroup W₂
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 V
inst_5 : NormedSpace 𝕜 W
inst_6 : NormedSpace 𝕜 W₂
f : V →ᴬ[𝕜] W
g : W₂ →ᴬ[𝕜] V
h₁ : 0 ≤ norm.{u_3} (E := V) ((g : (a : W₂) → V) 0 : V)
grw :
  ‖f‖ * norm.{u_3} (E := V) ((g : (a : W₂) → V) 0 : V) + norm.{u_4} (E := W) ((f : (a : V) → W) 0 : W) ≤
    ‖f‖ * ‖g‖ + norm.{u_4} (E := W) ((f : (a : V) → W) 0 : W)
⊢ norm (E := V →L[𝕜] W) f.contLinear * norm.{u_3} (E := V) ((g : (a : W₂) → V) 0 : V) +
      norm.{u_4} (E := W) ((f : (a : V) → W) 0 : W) ≤
    ‖f‖ * ‖g‖ + norm.{u_4} (E := W) ((f : (a : V) → W) 0 : W)
have grw₁ : ‖f‖ * ‖g‖ + norm.{u_4} (E := W) ((f : (a : V) → W) 0 : W) ≤ ‖f‖ * ‖g‖ + norm.{u_4} (E := W) ((f : (a : V) → W) 0 : W)
Tactic: grw [f.norm_contLinear_le, g.norm_image_zero_le]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.ContinuousAffineMap (goal)
Goal:
𝕜 : Type u_1
V : Type u_3
W : Type u_4
W₂ : Type u_5
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
inst_2 : SeminormedAddCommGroup W₂
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 V
inst_5 : NormedSpace 𝕜 W
inst_6 : NormedSpace 𝕜 W₂
f : V →ᴬ[𝕜] W
g : W₂ →ᴬ[𝕜] V
⊢ norm.{u_4} (E := W) ((f.comp g : (a : W₂) → W) 0 : W) ≤ ‖f‖ * ‖g‖ + norm.{u_4} (E := W) ((f : (a : V) → W) 0 : W)
have g₁ : norm.{u_4} (E := W) ((f.comp g : (a : W₂) → W) 0 : W) =
  norm.{u_4} (E := W) ((f : (a : V) → W) ((g : (a : W₂) → V) 0 : V) : W)
Tactic: calc
      ‖f.comp g 0‖ = ‖f (g 0)‖ := by simp
      _ = ‖f.contLinear (g 0) + f 0‖ := by rw [f.decomp]; simp
      _ ≤ ‖f.contLinear‖ * ‖g 0‖ + ‖f 0‖ := by grw [norm_add_le, f.contLinear.le_opNorm]
      _ ≤ ‖f‖ * ‖g‖ + ‖f 0‖ := by grw [f.norm_contLinear_le, g.norm_image_zero_le]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.ContinuousAffineMap (goal)
Goal:
𝕜 : Type u_1
V : Type u_3
W : Type u_4
W₂ : Type u_5
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
inst_2 : SeminormedAddCommGroup W₂
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 V
inst_5 : NormedSpace 𝕜 W
inst_6 : NormedSpace 𝕜 W₂
f : V →ᴬ[𝕜] W
g : W₂ →ᴬ[𝕜] V
g₁ :
  norm.{u_4} (E := W) ((f.comp g : (a : W₂) → W) 0 : W) =
    norm.{u_4} (E := W) ((f : (a : V) → W) ((g : (a : W₂) → V) 0 : V) : W)
⊢ norm.{u_4} (E := W) ((f.comp g : (a : W₂) → W) 0 : W) ≤ ‖f‖ * ‖g‖ + norm.{u_4} (E := W) ((f : (a : V) → W) 0 : W)
have g₂ : norm.{u_4} (E := W) ((f : (a : V) → W) ((g : (a : W₂) → V) 0 : V) : W) =
  ‖HAdd.hAdd (α := W) (β := W) ((f.contLinear : (a : V) → W) ((g : (a : W₂) → V) 0 : V) : W) ((f : (a : V) → W) 0 : W)‖
Tactic: calc
      ‖f.comp g 0‖ = ‖f (g 0)‖ := by simp
      _ = ‖f.contLinear (g 0) + f 0‖ := by rw [f.decomp]; simp
      _ ≤ ‖f.contLinear‖ * ‖g 0‖ + ‖f 0‖ := by grw [norm_add_le, f.contLinear.le_opNorm]
      _ ≤ ‖f‖ * ‖g‖ + ‖f 0‖ := by grw [f.norm_contLinear_le, g.norm_image_zero_le]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.ContinuousAffineMap (goal)
Goal:
𝕜 : Type u_1
V : Type u_3
W : Type u_4
W₂ : Type u_5
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
inst_2 : SeminormedAddCommGroup W₂
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 V
inst_5 : NormedSpace 𝕜 W
inst_6 : NormedSpace 𝕜 W₂
f : V →ᴬ[𝕜] W
g : W₂ →ᴬ[𝕜] V
g₁ :
  norm.{u_4} (E := W) ((f.comp g : (a : W₂) → W) 0 : W) =
    norm.{u_4} (E := W) ((f : (a : V) → W) ((g : (a : W₂) → V) 0 : V) : W)
g₂ :
  norm.{u_4} (E := W) ((f : (a : V) → W) ((g : (a : W₂) → V) 0 : V) : W) =
    ‖HAdd.hAdd (α := W) (β := W) ((f.contLinear : (a : V) → W) ((g : (a : W₂) → V) 0 : V) : W)
        ((f : (a : V) → W) 0 : W)‖
⊢ norm.{u_4} (E := W) ((f.comp g : (a : W₂) → W) 0 : W) ≤ ‖f‖ * ‖g‖ + norm.{u_4} (E := W) ((f : (a : V) → W) 0 : W)
have g₃ : ‖HAdd.hAdd (α := W) (β := W) ((f.contLinear : (a : V) → W) ((g : (a : W₂) → V) 0 : V) : W) ((f : (a : V) → W) 0 : W)‖ ≤
  norm (E := V →L[𝕜] W) f.contLinear * norm.{u_3} (E := V) ((g : (a : W₂) → V) 0 : V) +
    norm.{u_4} (E := W) ((f : (a : V) → W) 0 : W)
Tactic: calc
      ‖f.comp g 0‖ = ‖f (g 0)‖ := by simp
      _ = ‖f.contLinear (g 0) + f 0‖ := by rw [f.decomp]; simp
      _ ≤ ‖f.contLinear‖ * ‖g 0‖ + ‖f 0‖ := by grw [norm_add_le, f.contLinear.le_opNorm]
      _ ≤ ‖f‖ * ‖g‖ + ‖f 0‖ := by grw [f.norm_contLinear_le, g.norm_image_zero_le]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.ContinuousAffineMap (goal)
Goal:
𝕜 : Type u_1
V : Type u_3
W : Type u_4
W₂ : Type u_5
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
inst_2 : SeminormedAddCommGroup W₂
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 V
inst_5 : NormedSpace 𝕜 W
inst_6 : NormedSpace 𝕜 W₂
f : V →ᴬ[𝕜] W
g : W₂ →ᴬ[𝕜] V
g₁ :
  norm.{u_4} (E := W) ((f.comp g : (a : W₂) → W) 0 : W) =
    norm.{u_4} (E := W) ((f : (a : V) → W) ((g : (a : W₂) → V) 0 : V) : W)
g₂ :
  norm.{u_4} (E := W) ((f : (a : V) → W) ((g : (a : W₂) → V) 0 : V) : W) =
    ‖HAdd.hAdd (α := W) (β := W) ((f.contLinear : (a : V) → W) ((g : (a : W₂) → V) 0 : V) : W)
        ((f : (a : V) → W) 0 : W)‖
g₃ :
  ‖HAdd.hAdd (α := W) (β := W) ((f.contLinear : (a : V) → W) ((g : (a : W₂) → V) 0 : V) : W)
        ((f : (a : V) → W) 0 : W)‖ ≤
    norm (E := V →L[𝕜] W) f.contLinear * norm.{u_3} (E := V) ((g : (a : W₂) → V) 0 : V) +
      norm.{u_4} (E := W) ((f : (a : V) → W) 0 : W)
⊢ norm.{u_4} (E := W) ((f.comp g : (a : W₂) → W) 0 : W) ≤ ‖f‖ * ‖g‖ + norm.{u_4} (E := W) ((f : (a : V) → W) 0 : W)
have g₄ : norm (E := V →L[𝕜] W) f.contLinear * norm.{u_3} (E := V) ((g : (a : W₂) → V) 0 : V) +
    norm.{u_4} (E := W) ((f : (a : V) → W) 0 : W) ≤
  ‖f‖ * ‖g‖ + norm.{u_4} (E := W) ((f : (a : V) → W) 0 : W)
Tactic: calc
      ‖f.comp g 0‖ = ‖f (g 0)‖ := by simp
      _ = ‖f.contLinear (g 0) + f 0‖ := by rw [f.decomp]; simp
      _ ≤ ‖f.contLinear‖ * ‖g 0‖ + ‖f 0‖ := by grw [norm_add_le, f.contLinear.le_opNorm]
      _ ≤ ‖f‖ * ‖g‖ + ‖f 0‖ := by grw [f.norm_contLinear_le, g.norm_image_zero_le]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.ContinuousAffineMap (goal)
Goal:
𝕜 : Type u_1
V : Type u_3
W : Type u_4
W₂ : Type u_5
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
inst_2 : SeminormedAddCommGroup W₂
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 V
inst_5 : NormedSpace 𝕜 W
inst_6 : NormedSpace 𝕜 W₂
f : V →ᴬ[𝕜] W
g : W₂ →ᴬ[𝕜] V
⊢ norm (E := V →L[𝕜] W) f.contLinear * norm (E := W₂ →L[𝕜] V) g.contLinear ≤ ‖f‖ * ‖g‖
have h₁ : 0 ≤ norm (E := W₂ →L[𝕜] V) g.contLinear
Tactic: grw [f.norm_contLinear_le, g.norm_contLinear_le]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.ContinuousAffineMap (goal)
Goal:
𝕜 : Type u_1
V : Type u_3
W : Type u_4
W₂ : Type u_5
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
inst_2 : SeminormedAddCommGroup W₂
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 V
inst_5 : NormedSpace 𝕜 W
inst_6 : NormedSpace 𝕜 W₂
f : V →ᴬ[𝕜] W
g : W₂ →ᴬ[𝕜] V
h₁ : 0 ≤ norm (E := W₂ →L[𝕜] V) g.contLinear
⊢ norm (E := V →L[𝕜] W) f.contLinear * norm (E := W₂ →L[𝕜] V) g.contLinear ≤ ‖f‖ * ‖g‖
have grw : ‖f‖ * norm (E := W₂ →L[𝕜] V) g.contLinear ≤ ‖f‖ * ‖g‖
Tactic: grw [f.norm_contLinear_le, g.norm_contLinear_le]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.ContinuousAffineMap (goal)
Goal:
𝕜 : Type u_1
V : Type u_3
W : Type u_4
W₂ : Type u_5
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
inst_2 : SeminormedAddCommGroup W₂
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 V
inst_5 : NormedSpace 𝕜 W
inst_6 : NormedSpace 𝕜 W₂
f : V →ᴬ[𝕜] W
g : W₂ →ᴬ[𝕜] V
h₁ : 0 ≤ norm (E := W₂ →L[𝕜] V) g.contLinear
grw : ‖f‖ * norm (E := W₂ →L[𝕜] V) g.contLinear ≤ ‖f‖ * ‖g‖
⊢ norm (E := V →L[𝕜] W) f.contLinear * norm (E := W₂ →L[𝕜] V) g.contLinear ≤ ‖f‖ * ‖g‖
have grw₁ : ‖f‖ * ‖g‖ ≤ ‖f‖ * ‖g‖
Tactic: grw [f.norm_contLinear_le, g.norm_contLinear_le]