mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm

Goal state before:
pp: R : Type u_1
inst✝² : SeminormedCommRing R
S : Type u_2
inst✝¹ : Ring S
inst✝ : Algebra R S
f : AlgebraNorm R S
hf1 : f 1 = 1
a : R
⊢ f (a • 1) = ‖a‖

Tactic:
rw [← mul_one ‖a‖, ← hf1]

Goal state after:
R : Type u_1
inst✝² : SeminormedCommRing R
S : Type u_2
inst✝¹ : Ring S
inst✝ : Algebra R S
f : AlgebraNorm R S
hf1 : f 1 = 1
a : R
⊢ f (a • 1) = ‖a‖ * f 1
Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm

Goal state before:
pp: case mk.mk
R : Type u_1
inst✝ : NonUnitalRing R
toRingSeminorm✝¹ : RingSeminorm R
eq_zero_of_map_eq_zero'✝¹ : ∀ (x : R), toRingSeminorm✝¹.toFun x = 0 → x = 0
toRingSeminorm✝ : RingSeminorm R
eq_zero_of_map_eq_zero'✝ : ∀ (x : R), toRingSeminorm✝.toFun x = 0 → x = 0
h :
  (fun f ↦ f.toFun) { toRingSeminorm := toRingSeminorm✝¹, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝¹ } =
    (fun f ↦ f.toFun) { toRingSeminorm := toRingSeminorm✝, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝ }
⊢ toRingSeminorm✝¹ = toRingSeminorm✝

Tactic:
ext x

Goal state after:
case mk.mk
R : Type u_1
inst✝ : NonUnitalRing R
toRingSeminorm✝¹ : RingSeminorm R
eq_zero_of_map_eq_zero'✝¹ : ∀ (x : R), toRingSeminorm✝¹.toFun x = 0 → x = 0
toRingSeminorm✝ : RingSeminorm R
eq_zero_of_map_eq_zero'✝ : ∀ (x : R), toRingSeminorm✝.toFun x = 0 → x = 0
h :
  (fun f ↦ f.toFun) { toRingSeminorm := toRingSeminorm✝¹, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝¹ } =
    (fun f ↦ f.toFun) { toRingSeminorm := toRingSeminorm✝, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝ }
x : R
⊢ toRingSeminorm✝¹ x = toRingSeminorm✝ x
Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm

Goal state before:
pp: case mk.mk
R : Type u_1
inst✝ : NonAssocRing R
toAddGroupSeminorm✝¹ : AddGroupSeminorm R
map_one'✝¹ : toAddGroupSeminorm✝¹.toFun 1 = 1
map_mul'✝¹ :
  ∀ (x y : R), toAddGroupSeminorm✝¹.toFun (x * y) = toAddGroupSeminorm✝¹.toFun x * toAddGroupSeminorm✝¹.toFun y
toAddGroupSeminorm✝ : AddGroupSeminorm R
map_one'✝ : toAddGroupSeminorm✝.toFun 1 = 1
map_mul'✝ : ∀ (x y : R), toAddGroupSeminorm✝.toFun (x * y) = toAddGroupSeminorm✝.toFun x * toAddGroupSeminorm✝.toFun y
h :
  (fun f ↦ f.toFun) { toAddGroupSeminorm := toAddGroupSeminorm✝¹, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ } =
    (fun f ↦ f.toFun) { toAddGroupSeminorm := toAddGroupSeminorm✝, map_one' := map_one'✝, map_mul' := map_mul'✝ }
⊢ toAddGroupSeminorm✝¹ = toAddGroupSeminorm✝

Tactic:
ext x

Goal state after:
case mk.mk
R : Type u_1
inst✝ : NonAssocRing R
toAddGroupSeminorm✝¹ : AddGroupSeminorm R
map_one'✝¹ : toAddGroupSeminorm✝¹.toFun 1 = 1
map_mul'✝¹ :
  ∀ (x y : R), toAddGroupSeminorm✝¹.toFun (x * y) = toAddGroupSeminorm✝¹.toFun x * toAddGroupSeminorm✝¹.toFun y
toAddGroupSeminorm✝ : AddGroupSeminorm R
map_one'✝ : toAddGroupSeminorm✝.toFun 1 = 1
map_mul'✝ : ∀ (x y : R), toAddGroupSeminorm✝.toFun (x * y) = toAddGroupSeminorm✝.toFun x * toAddGroupSeminorm✝.toFun y
h :
  (fun f ↦ f.toFun) { toAddGroupSeminorm := toAddGroupSeminorm✝¹, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ } =
    (fun f ↦ f.toFun) { toAddGroupSeminorm := toAddGroupSeminorm✝, map_one' := map_one'✝, map_mul' := map_mul'✝ }
x : R
⊢ toAddGroupSeminorm✝¹ x = toAddGroupSeminorm✝ x
Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm

Goal state before:
pp: case mk.mk
R : Type u_1
inst✝ : NonAssocRing R
toMulRingSeminorm✝¹ : MulRingSeminorm R
eq_zero_of_map_eq_zero'✝¹ : ∀ (x : R), toMulRingSeminorm✝¹.toFun x = 0 → x = 0
toMulRingSeminorm✝ : MulRingSeminorm R
eq_zero_of_map_eq_zero'✝ : ∀ (x : R), toMulRingSeminorm✝.toFun x = 0 → x = 0
h :
  (fun f ↦ f.toFun) { toMulRingSeminorm := toMulRingSeminorm✝¹, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝¹ } =
    (fun f ↦ f.toFun) { toMulRingSeminorm := toMulRingSeminorm✝, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝ }
⊢ toMulRingSeminorm✝¹ = toMulRingSeminorm✝

Tactic:
ext x

Goal state after:
case mk.mk
R : Type u_1
inst✝ : NonAssocRing R
toMulRingSeminorm✝¹ : MulRingSeminorm R
eq_zero_of_map_eq_zero'✝¹ : ∀ (x : R), toMulRingSeminorm✝¹.toFun x = 0 → x = 0
toMulRingSeminorm✝ : MulRingSeminorm R
eq_zero_of_map_eq_zero'✝ : ∀ (x : R), toMulRingSeminorm✝.toFun x = 0 → x = 0
h :
  (fun f ↦ f.toFun) { toMulRingSeminorm := toMulRingSeminorm✝¹, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝¹ } =
    (fun f ↦ f.toFun) { toMulRingSeminorm := toMulRingSeminorm✝, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝ }
x : R
⊢ toMulRingSeminorm✝¹ x = toMulRingSeminorm✝ x
Module: Mathlib.Topology.Algebra.Order.LiminfLimsup

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommGroup α
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : DenselyOrdered α
inst✝¹ : AddLeftMono α
f : Filter ι
inst✝ : f.NeBot
u v : ι → α
h₁ : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₃ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
h₄ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
h : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (u + v)
h' : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (u + v)
a : α
a_u : a > limsup u f
b : α
b_v : b > limsup v f
⊢ limsup (u + v) f ≤ a + b

Tactic:
limsup_le_iff h h'

Goal state after:
ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommGroup α
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : DenselyOrdered α
inst✝¹ : AddLeftMono α
f : Filter ι
inst✝ : f.NeBot
u v : ι → α
h₁ : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₃ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
h₄ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
h : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (u + v)
h' : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (u + v)
a : α
a_u : a > limsup u f
b : α
b_v : b > limsup v f
⊢ ∀ y > a + b, ∀ᶠ (a : ι) in f, (u + v) a < y
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded

Goal state before:
pp: case h
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x y : R
⊢ (fun y ↦ f (x * y) / f y) y ≤ c * f x

Tactic:
rcases (f_nonneg y).eq_or_lt' with hy0 | hy0

Goal state after:
case h.inl
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x y : R
hy0 : f y = 0 y
⊢ (fun y ↦ f (x * y) / f y) y ≤ c * f x

case h.inr
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x y : R
hy0 : 0 y < f y
⊢ (fun y ↦ f (x * y) / f y) y ≤ c * f x
Module: Mathlib.Analysis.Normed.Field.Approximation

Goal state before:
pp: K : Type u_1
inst✝ : NormedField K
f g : K[X]
ε : ℝ
hε : 0 < ε
a : K
ha : eval a f = 0
hfm : f.Monic
hgm : g.Monic
hdeg : g.natDegree = f.natDegree
hcoeff : ∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε
hg : g.Splits
⊢ ∃ b ∈ g.roots, ‖a - b‖ < ((↑f.natDegree + 1) * ε) ^ (↑f.natDegree)⁻¹ * max ‖a‖ 1

Tactic:
suffices this : (g.roots.map fun x => ‖a - x‖).prod <
      ((f.natDegree + 1) * ε) * (max ‖a‖ 1) ^ (f.natDegree : ℝ) by
    by_contra! h
    have := Multiset.prod_map_le_prod_map₀ (fun b ↦ ((f.natDegree + 1) * ε) ^ (f.natDegree : ℝ)⁻¹ *
        (‖a‖ ⊔ 1)) (fun b ↦ ‖a - b‖) (by intros; positivity) h
    simp only [Multiset.map_const', hg.natDegree_eq_card_roots.symm ▸ hdeg, Multiset.prod_replicate,
      mul_pow, ← Real.rpow_natCast,
      ← Real.rpow_mul (by positivity : ((f.natDegree + 1) * ε) > 0).le] at this
    rw [inv_mul_cancel₀, Real.rpow_one] at this
    · linarith
    · simp only [ne_eq, Nat.cast_eq_zero, hfm, Monic.natDegree_eq_zero]
      intro h
      simp [h] at ha

Goal state after:
K : Type u_1
inst✝ : NormedField K
f g : K[X]
ε : ℝ
hε : 0 < ε
a : K
ha : eval a f = 0
hfm : f.Monic
hgm : g.Monic
hdeg : g.natDegree = f.natDegree
hcoeff : ∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε
hg : g.Splits
⊢ (Multiset.map (fun x ↦ ‖a - x‖) g.roots).prod < (↑f.natDegree + 1) * ε * max ‖a‖ 1 ^ ↑f.natDegree
Module: Mathlib.Topology.Algebra.Order.LiminfLimsup

Goal state before:
pp: ι : Type u_1
f : Filter ι
u v : ι → ℝ
h₁ : ∃ᶠ (x : ι) in f, 0 ≤ u x
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
h : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun x ↦ u x * v x
h' : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (u * v)
u0 : 0 ≤ limsup u f
uv : 0 ≤ limsup (u * v) f
⊢ limsup u f * liminf v f ≤ limsup (u * v) f

Tactic:
refine mul_le_of_forall_lt_of_nonneg u0 uv fun a a0 au b b0 bv ↦ ?_

Goal state after:
ι : Type u_1
f : Filter ι
u v : ι → ℝ
h₁ : ∃ᶠ (x : ι) in f, 0 ≤ u x
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
h : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun x ↦ u x * v x
h' : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (u * v)
u0 : 0 ≤ limsup u f
uv : 0 ≤ limsup (u * v) f
a : ℝ
a0 : a ≥ 0
au : a < limsup u f
b : ℝ
b0 : b ≥ 0
bv : b < liminf v f
⊢ a * b ≤ limsup (u * v) f
Module: Mathlib.Analysis.Normed.Unbundled.FiniteExtension

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁴ : NormedField K
inst✝³ : Ring L
inst✝² : Algebra K L
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
B : Basis ι K L
i : ι
hBi : B i = 1
x : K
⊢ B.norm ((algebraMap K L) x) = ‖x‖

Tactic:
by
  classical
  simp only [norm, repr_algebraMap hBi, Finsupp.single_apply]
  apply le_antisymm
  · aesop
  · exact le_sup'_of_le _ (mem_univ i) (by simp)

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
⊢ seminormFromBounded' f ⁻¹' {0} = f ⁻¹' {0}

Tactic:
ext x

Goal state after:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
⊢ x ∈ seminormFromBounded' f ⁻¹' {0} ↔ x ∈ f ⁻¹' {0}
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_zero : f 0 = 0
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
f_add : ∀ (a b : R), f (a + b) ≤ f a + f b
f_neg : ∀ (x : R), f (-x) = f x
h0 : ∀ (x : R), (seminormFromBounded f_zero f_nonneg f_mul f_add f_neg).toFun x = 0 → x = 0
⊢ seminormFromBounded' f ⁻¹' {0} = {0}

Tactic:
ext x

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_zero : f 0 = 0
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
f_add : ∀ (a b : R), f (a + b) ≤ f a + f b
f_neg : ∀ (x : R), f (-x) = f x
h0 : ∀ (x : R), (seminormFromBounded f_zero f_nonneg f_mul f_add f_neg).toFun x = 0 → x = 0
x : R
⊢ x ∈ seminormFromBounded' f ⁻¹' {0} ↔ x ∈ {0}
Module: Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful

Goal state before:
pp: F : Type u_1
α : Type u_2
inst✝² : Ring α
inst✝¹ : FunLike F α ℝ
inst✝ : RingSeminormClass F α ℝ
f g : F
hfpm : IsPowMul ⇑f
hgpm : IsPowMul ⇑g
r : ℝ
hr0 : 0 < r
hr : ∀ (a : α), f a ≤ r * g a
s : ℝ
hs0 : 0 < s
hs : ∀ (a : α), g a ≤ s * f a
hle : RingHom.IsBoundedWrt (⇑f) (⇑g) (RingHom.id α)
hge : RingHom.IsBoundedWrt (⇑g) (⇑f) (RingHom.id α)
⊢ ⇑f = ⇑g

Tactic:
ext x

Goal state after:
F : Type u_1
α : Type u_2
inst✝² : Ring α
inst✝¹ : FunLike F α ℝ
inst✝ : RingSeminormClass F α ℝ
f g : F
hfpm : IsPowMul ⇑f
hgpm : IsPowMul ⇑g
r : ℝ
hr0 : 0 < r
hr : ∀ (a : α), f a ≤ r * g a
s : ℝ
hs0 : 0 < s
hs : ∀ (a : α), g a ≤ s * f a
hle : RingHom.IsBoundedWrt (⇑f) (⇑g) (RingHom.id α)
hge : RingHom.IsBoundedWrt (⇑g) (⇑f) (RingHom.id α)
x : α
⊢ f x = g x
Module: Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : NormedCommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f₁ : AlgebraNorm R S
hf₁_pm : IsPowMul ⇑f₁
f₂ : AlgebraNorm R S
hf₂_pm : IsPowMul ⇑f₂
h_eq : ∀ (y : S), ∃ C₁ C₂, ∃ (_ : 0 < C₁) (_ : 0 < C₂), ∀ (x : ↥R[y]), f₁ ↑x ≤ C₁ * f₂ ↑x ∧ f₂ ↑x ≤ C₂ * f₁ ↑x
⊢ f₁ = f₂

Tactic:
ext x

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : NormedCommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f₁ : AlgebraNorm R S
hf₁_pm : IsPowMul ⇑f₁
f₂ : AlgebraNorm R S
hf₂_pm : IsPowMul ⇑f₂
h_eq : ∀ (y : S), ∃ C₁ C₂, ∃ (_ : 0 < C₁) (_ : 0 < C₂), ∀ (x : ↥R[y]), f₁ ↑x ≤ C₁ * f₂ ↑x ∧ f₂ ↑x ≤ C₂ * f₁ ↑x
x : S
⊢ f₁ x = f₂ x
Module: Mathlib.FieldTheory.Minpoly.IsConjRoot

Goal state before:
pp: K : Type u_2
S : Type u_4
inst✝² : CommRing S
inst✝¹ : Field K
inst✝ : Algebra K S
x y : S
r : K
h : IsConjRoot K x y
⊢ minpoly K (x + (algebraMap K S) r) = minpoly K (y + (algebraMap K S) r)

Tactic:
minpoly.add_algebraMap x r,

Goal state after:
K : Type u_2
S : Type u_4
inst✝² : CommRing S
inst✝¹ : Field K
inst✝ : Algebra K S
x y : S
r : K
h : IsConjRoot K x y
⊢ (minpoly K x).comp (X - C r) = minpoly K (y + (algebraMap K S) r)
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: R : Type u_1
inst✝ : SeminormedRing R
p : R[X]
⊢ Set.range (spectralValueTerms p) ⊆ {0} ∪ (fun n ↦ ‖p.coeff n‖ ^ (1 / (↑p.natDegree - ↑n))) '' Set.Iio p.natDegree

Tactic:
aesop (add simp [Set.range_subset_iff, spectralValueTerms])

Goal state after:
Module: Mathlib.Analysis.Normed.Group.HomCompletion

Goal state before:
pp: G : Type u_1
inst✝ : SeminormedAddCommGroup G
⊢ (id G).completion = id (Completion G)

Tactic:
ext x

Goal state after:
G : Type u_1
inst✝ : SeminormedAddCommGroup G
x : Completion G
⊢ (id G).completion x = (id (Completion G)) x
Module: Mathlib.Analysis.Normed.Group.HomCompletion

Goal state before:
pp: G : Type u_1
inst✝² : SeminormedAddCommGroup G
H : Type u_2
inst✝¹ : SeminormedAddCommGroup H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
f : NormedAddGroupHom G H
g : NormedAddGroupHom H K
⊢ g.completion.comp f.completion = (g.comp f).completion

Tactic:
ext x

Goal state after:
G : Type u_1
inst✝² : SeminormedAddCommGroup G
H : Type u_2
inst✝¹ : SeminormedAddCommGroup H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
f : NormedAddGroupHom G H
g : NormedAddGroupHom H K
x : Completion G
⊢ (g.completion.comp f.completion) x = (g.comp f).completion x
Module: Mathlib.Analysis.Normed.Group.HomCompletion

Goal state before:
pp: G : Type u_1
inst✝¹ : SeminormedAddCommGroup G
H : Type u_2
inst✝ : SeminormedAddCommGroup H
f : NormedAddGroupHom G H
⊢ f.completion.comp toCompl = toCompl.comp f

Tactic:
ext x

Goal state after:
G : Type u_1
inst✝¹ : SeminormedAddCommGroup G
H : Type u_2
inst✝ : SeminormedAddCommGroup H
f : NormedAddGroupHom G H
x : G
⊢ (f.completion.comp toCompl) x = (toCompl.comp f) x
Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp

Goal state before:
pp: case refine_1
V : SemiNormedGrp
inst✝ : Subsingleton V.carrier
X : SemiNormedGrp
f : V ⟶ X
⊢ f = default

Tactic:
ext x

Goal state after:
case refine_1
V : SemiNormedGrp
inst✝ : Subsingleton V.carrier
X : SemiNormedGrp
f : V ⟶ X
x : V.carrier
⊢ (Hom.hom f) x = (Hom.hom default) x
Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp

Goal state before:
pp: case refine_1
V : SemiNormedGrp₁
inst✝ : Subsingleton V.carrier
X : SemiNormedGrp₁
f : V ⟶ X
⊢ f = default

Tactic:
ext x

Goal state after:
case refine_1
V : SemiNormedGrp₁
inst✝ : Subsingleton V.carrier
X : SemiNormedGrp₁
f : V ⟶ X
x : V.carrier
⊢ ↑(Hom.hom f) x = ↑(Hom.hom default) x
Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels

Goal state before:
pp: X Y : SemiNormedGrp₁
f : X ⟶ Y
⊢ f ≫ mkHom (↑(Hom.hom f)).range.normedMk ⋯ = 0 ≫ mkHom (↑(Hom.hom f)).range.normedMk ⋯

Tactic:
ext x

Goal state after:
X Y : SemiNormedGrp₁
f : X ⟶ Y
x : X.carrier
⊢ ↑(Hom.hom (f ≫ mkHom (↑(Hom.hom f)).range.normedMk ⋯)) x = ↑(Hom.hom (0 ≫ mkHom (↑(Hom.hom f)).range.normedMk ⋯)) x
Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels

Goal state before:
pp: V W : SemiNormedGrp
f g✝ : V ⟶ W
this : ∀ (c : Fork f g✝), (NormedAddGroupHom.compHom (Hom.hom (f - g✝))) (Hom.hom c.ι) = 0
c : Fork f g✝
g : c.pt ⟶ (fork f g✝).pt
h : g ≫ (fork f g✝).ι = c.ι
⊢ g = ofHom (NormedAddGroupHom.ker.lift (Hom.hom c.ι) (Hom.hom (f - g✝)) ⋯)

Tactic:
ext x

Goal state after:
V W : SemiNormedGrp
f g✝ : V ⟶ W
this : ∀ (c : Fork f g✝), (NormedAddGroupHom.compHom (Hom.hom (f - g✝))) (Hom.hom c.ι) = 0
c : Fork f g✝
g : c.pt ⟶ (fork f g✝).pt
h : g ≫ (fork f g✝).ι = c.ι
x : c.pt.carrier
⊢ (Hom.hom g) x = (Hom.hom (ofHom (NormedAddGroupHom.ker.lift (Hom.hom c.ι) (Hom.hom (f - g✝)) ⋯))) x
Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels

Goal state before:
pp: X Y : SemiNormedGrp
f : X ⟶ Y
Z : SemiNormedGrp
g h : explicitCokernel f ⟶ Z
H : explicitCokernelπ f ≫ g = explicitCokernelπ f ≫ h
⊢ g = h

Tactic:
ext x

Goal state after:
X Y : SemiNormedGrp
f : X ⟶ Y
Z : SemiNormedGrp
g h : explicitCokernel f ⟶ Z
H : explicitCokernelπ f ≫ g = explicitCokernelπ f ≫ h
x : Y.carrier
⊢ (Hom.hom (explicitCokernelπ f ≫ g)) x = (Hom.hom (explicitCokernelπ f ≫ h)) x
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: K : Type u_2
inst✝² : NormedField K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
h_fin : FiniteDimensional K L
hn : Normal K L
hu : IsUltrametricDist K
⊢ spectralNorm K L = ⇑(invariantExtension K L)

Tactic:
ext x

Goal state after:
K : Type u_2
inst✝² : NormedField K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
h_fin : FiniteDimensional K L
hn : Normal K L
hu : IsUltrametricDist K
x : L
⊢ spectralNorm K L x = (invariantExtension K L) x
Module: Mathlib.Analysis.Normed.Group.SeparationQuotient

Goal state before:
pp: M : Type u_1
N✝ : Type u_2
inst✝² : SeminormedAddCommGroup M
inst✝¹ : SeminormedAddCommGroup N✝
N : Type u_3
inst✝ : SeminormedAddCommGroup N
x✝ : NormedAddGroupHom (SeparationQuotient M) N
⊢ (fun f ↦ liftNormedAddGroupHom ↑f ⋯) ((fun g ↦ ⟨g.comp normedMk, ⋯⟩) x✝) = x✝

Tactic:
ext x

Goal state after:
M : Type u_1
N✝ : Type u_2
inst✝² : SeminormedAddCommGroup M
inst✝¹ : SeminormedAddCommGroup N✝
N : Type u_3
inst✝ : SeminormedAddCommGroup N
x✝ : NormedAddGroupHom (SeparationQuotient M) N
x : SeparationQuotient M
⊢ ((fun f ↦ liftNormedAddGroupHom ↑f ⋯) ((fun g ↦ ⟨g.comp normedMk, ⋯⟩) x✝)) x = x✝ x
Module: Mathlib.Analysis.Normed.Group.SeparationQuotient

Goal state before:
pp: case mpr
M : Type u_1
inst✝ : SeminormedAddCommGroup M
h : ∀ (x : M), ‖x‖ = 0
⊢ normedMk = 0

Tactic:
ext x

Goal state after:
case mpr
M : Type u_1
inst✝ : SeminormedAddCommGroup M
h : ∀ (x : M), ‖x‖ = 0
x : M
⊢ normedMk x = 0 x
Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm

Goal state before:
pp: case add
ι : Type uι
inst✝⁵ : Fintype ι
𝕜 : Type u𝕜
inst✝⁴ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
F : Type u_1
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : ContinuousMultilinearMap 𝕜 E F
G : Type (max (max uE u𝕜) uι) := (⨂[𝕜] (i : ι), E i) ⧸ (lift f.toMultilinearMap).ker
G' : Submodule 𝕜 F := (lift f.toMultilinearMap).range
e : ((⨂[𝕜] (i : ι), E i) ⧸ (lift f.toMultilinearMap).ker) ≃ₗ[𝕜] ↥(lift f.toMultilinearMap).range :=
  (lift f.toMultilinearMap).quotKerEquivRange
this✝ : SeminormedAddCommGroup G := SeminormedAddCommGroup.induced G (↥G') e
this : NormedSpace 𝕜 G := NormedSpace.induced 𝕜 G (↥G') e
f'₀ : MultilinearMap 𝕜 E ((⨂[𝕜] (i : ι), E i) ⧸ (lift f.toMultilinearMap).ker) :=
  lift.symm (↑e.symm ∘ₗ (lift f.toMultilinearMap).rangeRestrict)
hf'₀ : ∀ (x : (i : ι) → E i), ‖f'₀ x‖ ≤ ‖f‖ * ∏ i, ‖x i‖
f' : ContinuousMultilinearMap 𝕜 E ((⨂[𝕜] (i : ι), E i) ⧸ (lift f.toMultilinearMap).ker) := f'₀.mkContinuous ‖f‖ hf'₀
hnorm : ‖f'‖ ≤ ‖f‖
x✝ y✝ : ⨂[𝕜] (i : ι), E i
hx : ↑(e ((lift f'.toMultilinearMap) x✝)) = (lift f.toMultilinearMap) x✝
hy : ↑(e ((lift f'.toMultilinearMap) y✝)) = (lift f.toMultilinearMap) y✝
⊢ ↑(e ((lift f'.toMultilinearMap) (x✝ + y✝))) = (lift f.toMultilinearMap) (x✝ + y✝)

Tactic:
simp only [map_add, Submodule.coe_add, hx, hy]

Goal state after:
Module: Mathlib.Topology.Maps.Strict.Group

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : Group G
inst✝² : Group H
f : G →* H
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalSpace H
⊢ IsStrictMap ⇑f ↔ IsStrictMap ⇑(kerLift f) ∧ True

Tactic:
and_true,

Goal state after:
G : Type u_1
H : Type u_2
inst✝³ : Group G
inst✝² : Group H
f : G →* H
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalSpace H
⊢ IsStrictMap ⇑f ↔ IsStrictMap ⇑(kerLift f)
Module: Mathlib.Topology.Maps.Strict.Group

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : Group G
inst✝² : Group H
f : G →* H
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalSpace H
⊢ IsStrictMap ⇑f ↔ IsStrictMap ⇑(quotientKerEquivRange f) ∧ True

Tactic:
and_true,

Goal state after:
G : Type u_1
H : Type u_2
inst✝³ : Group G
inst✝² : Group H
f : G →* H
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalSpace H
⊢ IsStrictMap ⇑f ↔ IsStrictMap ⇑(quotientKerEquivRange f)
Module: Mathlib.Topology.Maps.Strict.Module

Goal state before:
pp: R : Type u_1
M : Type u_3
Nₗ : Type u_5
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup Nₗ
inst✝³ : Module R M
inst✝² : Module R Nₗ
fₗ : M →ₗ[R] Nₗ
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalSpace Nₗ
⊢ IsStrictMap ⇑fₗ ↔ IsStrictMap ⇑fₗ.quotKerEquivRange ∧ True

Tactic:
and_true,

Goal state after:
R : Type u_1
M : Type u_3
Nₗ : Type u_5
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup Nₗ
inst✝³ : Module R M
inst✝² : Module R Nₗ
fₗ : M →ₗ[R] Nₗ
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalSpace Nₗ
⊢ IsStrictMap ⇑fₗ ↔ IsStrictMap ⇑fₗ.quotKerEquivRange
Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm

Goal state before:
pp: case refine_1
ι : Type uι
inst✝³ : Fintype ι
𝕜 : Type u𝕜
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
⊢ 0 =
    (normSeminorm 𝕜
          (ContinuousMultilinearMap 𝕜 E PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)} →L[𝕜]
            PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)})).comp
      (toDualContinuousMultilinearMap PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)})

Tactic:
ext x

Goal state after:
case refine_1
ι : Type uι
inst✝³ : Fintype ι
𝕜 : Type u𝕜
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
x : ⨂[𝕜] (i : ι), E i
⊢ 0 x =
    ((normSeminorm 𝕜
            (ContinuousMultilinearMap 𝕜 E PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)} →L[𝕜]
              PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)})).comp
        (toDualContinuousMultilinearMap PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)}))
      x