awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Affine.Ceva
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 (p 1) (t.points (HAdd.hAdd (α := Fin 3) 1 2)) ≠ 0

Tactic:
have := aux 1
-- Module: Mathlib.Analysis.Normed.Affine.Ceva
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 (p 2) (t.points (HAdd.hAdd (α := Fin 3) 2 2)) ≠ 0

Tactic:
have := aux 2
-- Module: Mathlib.Analysis.Normed.Affine.Ceva
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_2 : dist (p 1) (t.points (HAdd.hAdd (α := Fin 3) 1 2)) ≠ 0
this : dist (p 2) (t.points (HAdd.hAdd (α := Fin 3) 2 2)) ≠ 0
field_simp :
  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 (HAdd.hAdd (α := ℕ) 2 1)) 0 2)) *
        dist (p 1) (t.points (HAdd.hAdd (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 1 2)) *
      dist (p 2) (t.points (HAdd.hAdd (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 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

Tactic:
field_simp
-- Module: Mathlib.Analysis.Normed.Affine.Ceva
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_2 : dist (p 1) (t.points (HAdd.hAdd (α := Fin 3) 1 2)) ≠ 0
this : dist (p 2) (t.points (HAdd.hAdd (α := Fin 3) 2 2)) ≠ 0
⊢ 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 (HAdd.hAdd (α := ℕ) 2 1)) 0 2)) *
        dist (p 1) (t.points (HAdd.hAdd (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 1 2)) *
      dist (p 2) (t.points (HAdd.hAdd (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 2 2))

Tactic:
key
-- Module: Mathlib.Analysis.Normed.Affine.Ceva
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_2 : dist (p 1) (t.points (HAdd.hAdd (α := Fin 3) 1 2)) ≠ 0
this : dist (p 2) (t.points (HAdd.hAdd (α := Fin 3) 2 2)) ≠ 0
⊢ 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 (HAdd.hAdd (α := ℕ) 2 1)) 0 2)) *
        dist (p 1) (t.points (HAdd.hAdd (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 1 2)) *
      dist (p 2) (t.points (HAdd.hAdd (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 2 2))

Tactic:
exact key
-- Module: Mathlib.Analysis.Normed.Affine.ContinuousAffineMap
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
⊢ ‖f‖ = max (norm.{u_4} (E := W) ((f : (a : V) → W) 0 : W)) (norm (E := V →L[𝕜] W) f.contLinear)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Affine.ContinuousAffineMap
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
⊢ norm (E := V →L[𝕜] W) f.contLinear ≤ ‖f‖

Tactic:
le_max_right _ _

Premises used: le_max_right
-- Module: Mathlib.Analysis.Normed.Affine.ContinuousAffineMap
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
⊢ norm.{u_4} (E := W) ((f : (a : V) → W) 0 : W) ≤ ‖f‖

Tactic:
le_max_left _ _

Premises used: le_max_left
-- Module: Mathlib.Analysis.Normed.Affine.ContinuousAffineMap
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 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)
⊢ ‖f‖ = max (norm.{u_4} (E := W) ((f : (a : V) → W) 0 : W)) (norm (E := V →L[𝕜] W) f.contLinear)

Tactic:
rw [norm_def]

Premises used: ContinuousAffineMap.norm_def
-- Module: Mathlib.Analysis.Normed.Affine.ContinuousAffineMap
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)
rw₁ rw₂ : max 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)

Tactic:
rw [h, norm_zero]

Premises used: norm_zero
-- Module: Mathlib.Analysis.Normed.Affine.ContinuousAffineMap
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
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)
⊢ ‖f.comp g‖ ≤ ‖f‖ * ‖g‖ + norm.{u_4} (E := W) ((f : (a : V) → W) 0 : W)

Tactic:
rw [norm_def, max_le_iff]

Premises used: ContinuousAffineMap.norm_def, max_le_iff
-- Module: Mathlib.Analysis.Normed.Affine.ContinuousAffineMap
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)
right : norm (E := W₂ →L[𝕜] W) (f.comp g).contLinear ≤ ‖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)

Tactic:
constructor
-- Module: Mathlib.Analysis.Normed.Affine.ContinuousAffineMap
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) =
    norm.{u_4} (E := W) ((f : (a : V) → W) ((g : (a : W₂) → V) 0 : V) : W)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Affine.ContinuousAffineMap
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
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)‖
⊢ 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:
rw [f.decomp]

Premises used: ContinuousAffineMap.decomp
-- Module: Mathlib.Analysis.Normed.Affine.ContinuousAffineMap
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 (α := (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:
simp
-- Module: Mathlib.Analysis.Normed.Affine.ContinuousAffineMap
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)
grw₁ 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)
⊢ ‖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:
grw [norm_add_le, f.contLinear.le_opNorm]

Premises used: ContinuousAffineMap.contLinear, ContinuousLinearMap.le_opNorm, norm_add_le
-- Module: Mathlib.Analysis.Normed.Affine.ContinuousAffineMap
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)
grw₁ 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)
⊢ 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:
grw [f.norm_contLinear_le, g.norm_image_zero_le]

Premises used: ContinuousAffineMap.norm_contLinear_le, ContinuousAffineMap.norm_image_zero_le
-- Module: Mathlib.Analysis.Normed.Affine.ContinuousAffineMap
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)
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)
⊢ 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:
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]

Premises used: ContinuousAffineMap.contLinear, ContinuousAffineMap.comp, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Affine.ContinuousAffineMap
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 := W₂ →L[𝕜] W) (f.comp g).contLinear ≤
    norm (E := V →L[𝕜] W) f.contLinear * norm (E := W₂ →L[𝕜] V) g.contLinear

Tactic:
(g.comp_contLinear f).symm ▸ f.contLinear.opNorm_comp_le _

Premises used: ContinuousAffineMap.contLinear, ContinuousAffineMap.comp_contLinear, Eq.rec, ContinuousLinearMap.opNorm_comp_le, Eq.symm
-- Module: Mathlib.Analysis.Normed.Affine.ContinuousAffineMap
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‖
grw₁ grw₂ : ‖f‖ * ‖g‖ ≤ ‖f‖ * ‖g‖
⊢ norm (E := V →L[𝕜] W) f.contLinear * norm (E := W₂ →L[𝕜] V) g.contLinear ≤ ‖f‖ * ‖g‖

Tactic:
grw [f.norm_contLinear_le, g.norm_contLinear_le]

Premises used: ContinuousAffineMap.norm_contLinear_le
-- Module: Mathlib.Analysis.Normed.Affine.ContinuousAffineMap
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
rw : 0 ≤ norm.{u_4} (E := W) ((f : (a : V) → W) 0 : W)
⊢ ‖f‖ * ‖g‖ ≤ ‖f‖ * ‖g‖ + norm.{u_4} (E := W) ((f : (a : V) → W) 0 : W)

Tactic:
rw [le_add_iff_nonneg_right]

Premises used: le_add_iff_nonneg_right
-- Module: Mathlib.Analysis.Normed.Affine.ContinuousAffineMap
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
⊢ 0 ≤ norm.{u_4} (E := W) ((f : (a : V) → W) 0 : W)

Tactic:
apply norm_nonneg

Premises used: norm_nonneg
-- Module: Mathlib.Analysis.Normed.Affine.ContinuousAffineMap
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‖
_₁ : ‖f‖ * ‖g‖ ≤ ‖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:
calc
      ‖(f.comp g).contLinear‖ ≤ ‖f.contLinear‖ * ‖g.contLinear‖ :=
        (g.comp_contLinear f).symm ▸ f.contLinear.opNorm_comp_le _
      _ ≤ ‖f‖ * ‖g‖ := by grw [f.norm_contLinear_le, g.norm_contLinear_le]
      _ ≤ ‖f‖ * ‖g‖ + ‖f 0‖ := by rw [le_add_iff_nonneg_right]; apply norm_nonneg

Premises used: ContinuousAffineMap.contLinear, ContinuousAffineMap.comp, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Affine.ContinuousAffineMap
Goal:
𝕜 : Type u_1
R : Type u_2
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
inst_5 : Ring R
inst_6 : Module R W
inst_7 : ContinuousConstSMul R W
inst_8 : SMulCommClass 𝕜 R W
f : V →ᴬ[𝕜] W
⊢ Eq.{u_4 + 1} (α := W) (((decompLinearIsometryEquiv 𝕜 R V W : (a : V →ᴬ[𝕜] W) → W × (V →L[𝕜] W)) f).1 : W)
    ((f : (a : V) → W) 0 : W)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Affine.ContinuousAffineMap
Goal:
𝕜 : Type u_1
R : Type u_2
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
inst_5 : Ring R
inst_6 : Module R W
inst_7 : ContinuousConstSMul R W
inst_8 : SMulCommClass 𝕜 R W
f : V →ᴬ[𝕜] W
⊢ Eq (α := V →L[𝕜] W) ((decompLinearIsometryEquiv 𝕜 R V W : (a : V →ᴬ[𝕜] W) → W × (V →L[𝕜] W)) f).2 f.contLinear

Tactic:
rfl

Premises used: ContinuousAffineMap.contLinear, rfl
-- Module: Mathlib.Analysis.Normed.Affine.ContinuousAffineMap
Goal:
𝕜 : Type u_1
R : Type u_2
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
inst_5 : Ring R
inst_6 : Module R W
inst_7 : ContinuousConstSMul R W
inst_8 : SMulCommClass 𝕜 R W
p : W × (V →L[𝕜] W)
x : V
⊢ (((LinearIsometryEquiv.symm (decompLinearIsometryEquiv 𝕜 R V W) : (a : W × (V →L[𝕜] W)) → V →ᴬ[𝕜] W) p : V →ᴬ[𝕜] W) :
        (a : V) → W)
      x =
    HAdd.hAdd (α := W) ((p.2 : (a : V) → W) x : W) p.1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Affine.ContinuousAffineMap
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
⊢ Eq.{u_4 + 1} (α := W) (((toConstProdContinuousLinearMap 𝕜 V W : (a : V →ᴬ[𝕜] W) → W × (V →L[𝕜] W)) f).1 : W)
    ((f : (a : V) → W) 0 : W)

Tactic:
rfl

Premises used: rfl