mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case refine_2
ι : Type u_1
s : Finset ι
hs : s.Nonempty
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : 0 < ∑ i ∈ s, w i
hz : ∀ i ∈ s, 0 < z i
⊢ ∑ i ∈ s, w i / ∑ i ∈ s, w i = 1

Tactic:
· simp_rw [div_eq_mul_inv (w _) (∑ i ∈ s, w i), ← Finset.sum_mul _ _ (∑ i ∈ s, w i)⁻¹]
    exact mul_inv_cancel₀ hw'.ne'

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: a b : ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
h : a ≠ ∞ ∧ b ≠ ∞
⊢ p.toNNReal ≠ 0

Tactic:
by simp [hpq.pos]

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: a b : ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
h0 : a ≠ 0 ∧ b ≠ 0
h : a ≠ ∞ ∧ b ≠ ∞
⊢ p.toNNReal ≠ 0

Tactic:
by simp [hpq.pos]

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
⊢ IsGreatest ((fun g ↦ ∑ i ∈ s, f i * g i) '' {g | ∑ i ∈ s, g i ^ q ≤ 1}) ((∑ i ∈ s, f i ^ p) ^ (1 / p))

Tactic:
constructor

Goal state after:
case left
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
⊢ (∑ i ∈ s, f i ^ p) ^ (1 / p) ∈ (fun g ↦ ∑ i ∈ s, f i * g i) '' {g | ∑ i ∈ s, g i ^ q ≤ 1}

case right
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
⊢ (∑ i ∈ s, f i ^ p) ^ (1 / p) ∈ upperBounds ((fun g ↦ ∑ i ∈ s, f i * g i) '' {g | ∑ i ∈ s, g i ^ q ≤ 1})
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:
pp: case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ∞
hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ∞
h1 : p = 1
⊢ ∫⁻ (a : α), (f + g) a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ

Tactic:
exact lintegral_add_left' hf _

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hpq : p.HolderConjugate q
⊢ ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, |f i| ^ p) ^ (1 / p) * (∑ i ∈ s, |g i| ^ q) ^ (1 / q)

Tactic:
refine le_trans (sum_le_sum fun i _ ↦ ?_) (by simpa using Lr_rpow_le_Lp_mul_Lq s f g hpq)

Goal state after:
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hpq : p.HolderConjugate q
i : ι
x✝ : i ∈ s
⊢ f i * g i ≤ |f i| * |g i|
Module: Mathlib.MeasureTheory.Function.LpSpace.Complete

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : SeminormedAddGroup E
ι : Type u_3
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
f : ι → α → E
g : α → E
C : ℝ≥0∞
bound : ∀ᶠ (n : ι) in u, eLpNorm (f n) p μ ≤ C
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun x_1 ↦ f x_1 x) u (𝓝 (g x))
v : ℕ → ι
hv : Tendsto v atTop u
this : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f (v n) x) atTop (𝓝 (g x))
⊢ liminf (fun n ↦ eLpNorm (f (v n)) p μ) atTop ≤ C

Tactic:
refine liminf_le_of_le (by isBoundedDefault) (fun b hb => ?_)
    obtain ⟨n, hn⟩ := (hb.and (hv.eventually bound)).exists
    exact hn.1.trans hn.2

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: α✝ : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
E✝ : Type u_4
F : Type u_5
m✝ : MeasurableSpace α✝
p✝ : ℝ≥0∞
μ✝ : Measure α✝
inst✝² : NormedAddCommGroup E✝
inst✝¹ : NormedAddCommGroup F
α : Type ?u.18
E : Type u_6
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f g : α →ₘ[μ] E
hf : f ∈ {f | eLpNorm (↑f) p μ < ∞}
hg : g ∈ {f | eLpNorm (↑f) p μ < ∞}
⊢ f + g ∈ {f | eLpNorm (↑f) p μ < ∞}

Tactic:
simp [eLpNorm_congr_ae (AEEqFun.coeFn_add f g),
      eLpNorm_add_lt_top ⟨f.aestronglyMeasurable, hf⟩ ⟨g.aestronglyMeasurable, hg⟩]

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : α → E
hf : MemLp f p μ
hg : MemLp g p μ
⊢ toLp f hf = toLp g hg ↔ f =ᵐ[μ] g

Tactic:
simp [toLp]

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : ↥(Lp E p μ)
h : ↑↑f =ᵐ[μ] ↑↑g
⊢ f = g

Tactic:
ext

Goal state after:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : ↥(Lp E p μ)
h : ↑↑f =ᵐ[μ] ↑↑g
⊢ ↑↑f =ᵐ[μ] ↑↑g
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
⊢ (∑ i ∈ s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) + (∑ i ∈ s, g i ^ p) ^ (1 / p)

Tactic:
by
  convert! Lp_add_le s f g hp using 2 <;> [skip; congr 1; congr 1] <;> apply sum_congr rfl <;>
      intro i hi <;>
    simp only [abs_of_nonneg, hf i hi, hg i hi, add_nonneg]

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
β : Type u_7
inst✝ : MeasurableSpace β
μb : Measure β
g : β →ₘ[μb] E
hg : g ∈ Lp E p μb
f : α → β
hf : MeasurePreserving f μ μb
⊢ g.compMeasurePreserving f hf ∈ Lp E p μ

Tactic:
rw [Lp.mem_Lp_iff_eLpNorm_lt_top] at hg ⊢

Goal state after:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
β : Type u_7
inst✝ : MeasurableSpace β
μb : Measure β
g : β →ₘ[μb] E
hg : eLpNorm (↑g) p μb < ∞
f : α → β
hf : MeasurePreserving f μ μb
⊢ eLpNorm (↑(g.compMeasurePreserving f hf)) p μ < ∞
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: E : Type u_4
p : ℝ≥0∞
inst✝¹ : NormedAddCommGroup E
β : Type u_7
inst✝ : MeasurableSpace β
μb : Measure β
⊢ compMeasurePreserving id ⋯ = AddMonoidHom.id ↥(Lp E p μb)

Tactic:
ext

Goal state after:
E : Type u_4
p : ℝ≥0∞
inst✝¹ : NormedAddCommGroup E
β : Type u_7
inst✝ : MeasurableSpace β
μb : Measure β
x✝ : ↥(Lp E p μb)
⊢ ↑↑((compMeasurePreserving id ⋯) x✝) =ᵐ[μb] ↑↑((AddMonoidHom.id ↥(Lp E p μb)) x✝)
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: p : ℝ≥0∞
α : Type u_6
E : Type u_7
F : Type u_8
K' : ℝ≥0
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
f : α → E
g : E → F
hL : MemLp (g ∘ f) p μ
hg : UniformContinuous g
hg' : AntilipschitzWith K' g
g0 : g 0 = 0
x : α
⊢ ‖f x‖ ≤ ↑K' * ‖g (f x)‖

Tactic:
rw [← dist_zero_right, ← dist_zero_right, ← g0]

Goal state after:
p : ℝ≥0∞
α : Type u_6
E : Type u_7
F : Type u_8
K' : ℝ≥0
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
f : α → E
g : E → F
hL : MemLp (g ∘ f) p μ
hg : UniformContinuous g
hg' : AntilipschitzWith K' g
g0 : g 0 = 0
x : α
⊢ dist (f x) 0 ≤ ↑K' * dist (g (f x)) (g 0)
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
g : E → F
c : ℝ≥0
hg : LipschitzWith c g
g0 : g 0 = 0
⊢ hg.compLp g0 0 = 0

Tactic:
rw [Lp.eq_zero_iff_ae_eq_zero]
  apply (coeFn_compLp _ _ _).trans
  filter_upwards [Lp.coeFn_zero E p μ] with _ ha
  simp only [ha, g0, Function.comp_apply, Pi.zero_apply]

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
𝕜 : Type u_6
𝕜' : Type u_7
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜'
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜' F
σ : 𝕜 →+* 𝕜'
inst✝¹ : RingHomIsometric σ
inst✝ : Fact (1 ≤ p)
L L' : E →SL[σ] F
⊢ compLpL p μ (L + L') = compLpL p μ L + compLpL p μ L'

Tactic:
ext1 f; exact add_compLp L L' f

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
𝕜 : Type u_6
𝕜' : Type u_7
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜'
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜' F
σ : 𝕜 →+* 𝕜'
inst✝¹ : RingHomIsometric σ
inst✝ : Fact (1 ≤ p)
L L' : E →SL[σ] F
⊢ compLpL p μ (L + L') = compLpL p μ L + compLpL p μ L'

Tactic:
by ext1 f; exact add_compLp L L' f

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
g✝ : E → F
c✝ : ℝ≥0
inst✝ : NormedSpace ℝ E
ν : Measure α
c : ℝ≥0∞
hc : c ≠ ∞
h : μ ≤ c • ν
f g : ↥(Lp E p ν)
⊢ MemLp.toLp ↑↑(f + g) ⋯ = MemLp.toLp ↑↑f ⋯ + MemLp.toLp ↑↑g ⋯

Tactic:
ext

Goal state after:
α : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
g✝ : E → F
c✝ : ℝ≥0
inst✝ : NormedSpace ℝ E
ν : Measure α
c : ℝ≥0∞
hc : c ≠ ∞
h : μ ≤ c • ν
f g : ↥(Lp E p ν)
⊢ ↑↑(MemLp.toLp ↑↑(f + g) ⋯) =ᵐ[μ] ↑↑(MemLp.toLp ↑↑f ⋯ + MemLp.toLp ↑↑g ⋯)
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
g : E → F
c✝¹ : ℝ≥0
inst✝ : NormedSpace ℝ E
ν : Measure α
c✝ : ℝ≥0∞
hc : c✝ ≠ ∞
h : μ ≤ c✝ • ν
c : ℝ
f : ↥(Lp E p ν)
⊢ MemLp.toLp ↑↑(c • f) ⋯ = (RingHom.id ℝ) c • MemLp.toLp ↑↑f ⋯

Tactic:
ext

Goal state after:
α : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
g : E → F
c✝¹ : ℝ≥0
inst✝ : NormedSpace ℝ E
ν : Measure α
c✝ : ℝ≥0∞
hc : c✝ ≠ ∞
h : μ ≤ c✝ • ν
c : ℝ
f : ↥(Lp E p ν)
⊢ ↑↑(MemLp.toLp ↑↑(c • f) ⋯) =ᵐ[μ] ↑↑((RingHom.id ℝ) c • MemLp.toLp ↑↑f ⋯)
Module: Mathlib.Logic.Equiv.Embedding

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ⊕ β ↪ γ
val✝ : α
⊢ {
        toFun := fun x ↦
          match x with
          | Sum.inl a => (inl.trans f) a
          | Sum.inr b => (inr.trans f) b,
        inj' := ⋯ }
      (Sum.inl val✝) =
    f (Sum.inl val✝)

Tactic:
simp!

Goal state after:
Module: Mathlib.Logic.Equiv.Embedding

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ⊕ β ↪ γ
val✝ : β
⊢ {
        toFun := fun x ↦
          match x with
          | Sum.inl a => (inl.trans f) a
          | Sum.inr b => (inr.trans f) b,
        inj' := ⋯ }
      (Sum.inr val✝) =
    f (Sum.inr val✝)

Tactic:
simp!

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSpace.Complete

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst✝ : NormedAddCommGroup E
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), MemLp (f n) p μ
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n - f_lim) p μ ≤ ε
N : ℕ
h_tendsto_1 : eLpNorm (f N - f_lim) p μ ≤ 1
h_add : f_lim = f_lim - f N + f N
⊢ eLpNorm (f_lim - f N) p μ < ∞ ∧ eLpNorm (f N) p μ < ∞

Tactic:
constructor

Goal state after:
case left
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst✝ : NormedAddCommGroup E
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), MemLp (f n) p μ
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n - f_lim) p μ ≤ ε
N : ℕ
h_tendsto_1 : eLpNorm (f N - f_lim) p μ ≤ 1
h_add : f_lim = f_lim - f N + f N
⊢ eLpNorm (f_lim - f N) p μ < ∞

case right
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst✝ : NormedAddCommGroup E
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), MemLp (f n) p μ
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n - f_lim) p μ ≤ ε
N : ℕ
h_tendsto_1 : eLpNorm (f N - f_lim) p μ ≤ 1
h_add : f_lim = f_lim - f N + f N
⊢ eLpNorm (f N) p μ < ∞
Module: Mathlib.Topology.Algebra.Module.Multilinear.Basic

Goal state before:
pp: R : Type u
A : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : Algebra R A
inst✝¹ : TopologicalSpace A
inst✝ : ContinuousMul A
n : ℕ
⊢ ContinuousMultilinearMap.mkPiAlgebra R (Fin n) A = ContinuousMultilinearMap.mkPiAlgebraFin R n A

Tactic:
ext

Goal state after:
R : Type u
A : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : Algebra R A
inst✝¹ : TopologicalSpace A
inst✝ : ContinuousMul A
n : ℕ
x✝ : Fin n → A
⊢ (ContinuousMultilinearMap.mkPiAlgebra R (Fin n) A) x✝ = (ContinuousMultilinearMap.mkPiAlgebraFin R n A) x✝
Module: Mathlib.Topology.Algebra.Module.Multilinear.Basic

Goal state before:
pp: R : Type u
ι : Type v
M : Type u_1
inst✝⁷ : Fintype ι
inst✝⁶ : CommRing R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : TopologicalSpace R
inst✝² : TopologicalSpace M
inst✝¹ : ContinuousMul R
inst✝ : ContinuousSMul R M
⊢ ContinuousMultilinearMap.mkPiRing R ι 0 = 0

Tactic:
ext

Goal state after:
R : Type u
ι : Type v
M : Type u_1
inst✝⁷ : Fintype ι
inst✝⁶ : CommRing R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : TopologicalSpace R
inst✝² : TopologicalSpace M
inst✝¹ : ContinuousMul R
inst✝ : ContinuousSMul R M
⊢ ((ContinuousMultilinearMap.mkPiRing R ι 0) fun x ↦ 1) = 0 fun x ↦ 1
Module: Mathlib.Analysis.Normed.Operator.Mul

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
R : Type u_3
inst✝³ : NonUnitalSeminormedCommRing R
inst✝² : NormedSpace 𝕜 R
inst✝¹ : IsScalarTower 𝕜 R R
inst✝ : SMulCommClass 𝕜 R R
⊢ (mul 𝕜 R).flip = mul 𝕜 R

Tactic:
ext

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
R : Type u_3
inst✝³ : NonUnitalSeminormedCommRing R
inst✝² : NormedSpace 𝕜 R
inst✝¹ : IsScalarTower 𝕜 R R
inst✝ : SMulCommClass 𝕜 R R
x✝¹ x✝ : R
⊢ ((mul 𝕜 R).flip x✝¹) x✝ = ((mul 𝕜 R) x✝¹) x✝
Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst✝⁷ : NormedField 𝕜
inst✝⁶ : (i : ι) → TopologicalSpace (E i)
inst✝⁵ : (i : ι) → AddCommGroup (E i)
inst✝⁴ : (i : ι) → Module 𝕜 (E i)
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : DecidableEq ι
inst✝ : TopologicalSpace F
f : ((i : ι) → E i) →ᵤ[{s | IsVonNBounded 𝕜 s}] F
⊢ f ∈ range toUniformOnFun ↔
    f ∈
      {f |
        Continuous[Pi.topologicalSpace, inst✝] ((toFun {s | IsVonNBounded 𝕜 s}) f) ∧
          (∀ (m : (i : ι) → E i) (i : ι) (x y : E i),
              (toFun {s | IsVonNBounded 𝕜 s}) f (update m i (x + y)) =
                (toFun {s | IsVonNBounded 𝕜 s}) f (update m i x) + (toFun {s | IsVonNBounded 𝕜 s}) f (update m i y)) ∧
            ∀ (m : (i : ι) → E i) (i : ι) (c : 𝕜) (x : E i),
              (toFun {s | IsVonNBounded 𝕜 s}) f (update m i (c • x)) =
                c • (toFun {s | IsVonNBounded 𝕜 s}) f (update m i x)}

Tactic:
constructor

Goal state after:
case mp
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst✝⁷ : NormedField 𝕜
inst✝⁶ : (i : ι) → TopologicalSpace (E i)
inst✝⁵ : (i : ι) → AddCommGroup (E i)
inst✝⁴ : (i : ι) → Module 𝕜 (E i)
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : DecidableEq ι
inst✝ : TopologicalSpace F
f : ((i : ι) → E i) →ᵤ[{s | IsVonNBounded 𝕜 s}] F
⊢ f ∈ range toUniformOnFun →
    f ∈
      {f |
        Continuous[Pi.topologicalSpace, inst✝] ((toFun {s | IsVonNBounded 𝕜 s}) f) ∧
          (∀ (m : (i : ι) → E i) (i : ι) (x y : E i),
              (toFun {s | IsVonNBounded 𝕜 s}) f (update m i (x + y)) =
                (toFun {s | IsVonNBounded 𝕜 s}) f (update m i x) + (toFun {s | IsVonNBounded 𝕜 s}) f (update m i y)) ∧
            ∀ (m : (i : ι) → E i) (i : ι) (c : 𝕜) (x : E i),
              (toFun {s | IsVonNBounded 𝕜 s}) f (update m i (c • x)) =
                c • (toFun {s | IsVonNBounded 𝕜 s}) f (update m i x)}

case mpr
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst✝⁷ : NormedField 𝕜
inst✝⁶ : (i : ι) → TopologicalSpace (E i)
inst✝⁵ : (i : ι) → AddCommGroup (E i)
inst✝⁴ : (i : ι) → Module 𝕜 (E i)
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : DecidableEq ι
inst✝ : TopologicalSpace F
f : ((i : ι) → E i) →ᵤ[{s | IsVonNBounded 𝕜 s}] F
⊢ f ∈
      {f |
        Continuous[Pi.topologicalSpace, inst✝] ((toFun {s | IsVonNBounded 𝕜 s}) f) ∧
          (∀ (m : (i : ι) → E i) (i : ι) (x y : E i),
              (toFun {s | IsVonNBounded 𝕜 s}) f (update m i (x + y)) =
                (toFun {s | IsVonNBounded 𝕜 s}) f (update m i x) + (toFun {s | IsVonNBounded 𝕜 s}) f (update m i y)) ∧
            ∀ (m : (i : ι) → E i) (i : ι) (c : 𝕜) (x : E i),
              (toFun {s | IsVonNBounded 𝕜 s}) f (update m i (c • x)) =
                c • (toFun {s | IsVonNBounded 𝕜 s}) f (update m i x)} →
    f ∈ range toUniformOnFun
Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst✝⁷ : NormedField 𝕜
inst✝⁶ : (i : ι) → TopologicalSpace (E i)
inst✝⁵ : (i : ι) → AddCommGroup (E i)
inst✝⁴ : (i : ι) → Module 𝕜 (E i)
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : DecidableEq ι
inst✝ : TopologicalSpace F
⊢ range toUniformOnFun =
    {f |
      Continuous[Pi.topologicalSpace, inst✝] ((toFun {s | IsVonNBounded 𝕜 s}) f) ∧
        (∀ (m : (i : ι) → E i) (i : ι) (x y : E i),
            (toFun {s | IsVonNBounded 𝕜 s}) f (update m i (x + y)) =
              (toFun {s | IsVonNBounded 𝕜 s}) f (update m i x) + (toFun {s | IsVonNBounded 𝕜 s}) f (update m i y)) ∧
          ∀ (m : (i : ι) → E i) (i : ι) (c : 𝕜) (x : E i),
            (toFun {s | IsVonNBounded 𝕜 s}) f (update m i (c • x)) =
              c • (toFun {s | IsVonNBounded 𝕜 s}) f (update m i x)}

Tactic:
ext f
  constructor
  · rintro ⟨f, rfl⟩
    exact ⟨f.cont, f.map_update_add, f.map_update_smul⟩
  · rintro ⟨hcont, hadd, hsmul⟩
    exact ⟨⟨⟨f, by intro; convert! hadd, by intro; convert! hsmul⟩, hcont⟩, rfl⟩

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Determinant

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : CommRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : ContinuousMul 𝕜
v : 𝕜
⊢ ((ContinuousLinearMap.id 𝕜 𝕜).smulRight v).det = v

Tactic:
det_smulRight

Goal state after:
𝕜 : Type u_1
inst✝² : CommRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : ContinuousMul 𝕜
v : 𝕜
⊢ (ContinuousLinearMap.id 𝕜 𝕜) 1 * v = v
Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace E
e : E ≃L[𝕜] F
O : (E →L[𝕜] F) → E →L[𝕜] E := fun f ↦ ↑e.symm ∘SL f
h_O : Continuous O
f' : E →L[𝕜] F
⊢ f' ∈ range toContinuousLinearMap ↔ f' ∈ O ⁻¹' {x | IsUnit x}

Tactic:
constructor

Goal state after:
case mp
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace E
e : E ≃L[𝕜] F
O : (E →L[𝕜] F) → E →L[𝕜] E := ⋯
h_O : Continuous O
f' : E →L[𝕜] F
⊢ f' ∈ range toContinuousLinearMap → f' ∈ O ⁻¹' {x | IsUnit x}

case mpr
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace E
e : E ≃L[𝕜] F
O : (E →L[𝕜] F) → E →L[𝕜] E := ⋯
h_O : Continuous O
f' : E →L[𝕜] F
⊢ f' ∈ O ⁻¹' {x | IsUnit x} → f' ∈ range toContinuousLinearMap
Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst✝¹¹ : NormedField 𝕜
inst✝¹⁰ : (i : ι) → TopologicalSpace (E i)
inst✝⁹ : (i : ι) → AddCommGroup (E i)
inst✝⁸ : (i : ι) → Module 𝕜 (E i)
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜 F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
E₁ : ι → Type u_5
inst✝³ : (i : ι) → TopologicalSpace (E₁ i)
inst✝² : ContinuousConstSMul 𝕜 F
inst✝¹ : (i : ι) → AddCommGroup (E₁ i)
inst✝ : (i : ι) → Module 𝕜 (E₁ i)
f : (i : ι) → E i →L[𝕜] E₁ i
x✝¹ x✝ : ContinuousMultilinearMap 𝕜 E₁ F
⊢ (x✝¹ + x✝).compContinuousLinearMap f = x✝¹.compContinuousLinearMap f + x✝.compContinuousLinearMap f

Tactic:
ext

Goal state after:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst✝¹¹ : NormedField 𝕜
inst✝¹⁰ : (i : ι) → TopologicalSpace (E i)
inst✝⁹ : (i : ι) → AddCommGroup (E i)
inst✝⁸ : (i : ι) → Module 𝕜 (E i)
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜 F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
E₁ : ι → Type u_5
inst✝³ : (i : ι) → TopologicalSpace (E₁ i)
inst✝² : ContinuousConstSMul 𝕜 F
inst✝¹ : (i : ι) → AddCommGroup (E₁ i)
inst✝ : (i : ι) → Module 𝕜 (E₁ i)
f : (i : ι) → E i →L[𝕜] E₁ i
x✝² x✝¹ : ContinuousMultilinearMap 𝕜 E₁ F
x✝ : (i : ι) → E i
⊢ ((x✝² + x✝¹).compContinuousLinearMap f) x✝ = (x✝².compContinuousLinearMap f + x✝¹.compContinuousLinearMap f) x✝
Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst✝¹¹ : NormedField 𝕜
inst✝¹⁰ : (i : ι) → TopologicalSpace (E i)
inst✝⁹ : (i : ι) → AddCommGroup (E i)
inst✝⁸ : (i : ι) → Module 𝕜 (E i)
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜 F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
E₁ : ι → Type u_5
inst✝³ : (i : ι) → TopologicalSpace (E₁ i)
inst✝² : ContinuousConstSMul 𝕜 F
inst✝¹ : (i : ι) → AddCommGroup (E₁ i)
inst✝ : (i : ι) → Module 𝕜 (E₁ i)
f : (i : ι) → E i →L[𝕜] E₁ i
x✝¹ : 𝕜
x✝ : ContinuousMultilinearMap 𝕜 E₁ F
⊢ (x✝¹ • x✝).compContinuousLinearMap f = (RingHom.id 𝕜) x✝¹ • x✝.compContinuousLinearMap f

Tactic:
ext

Goal state after:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst✝¹¹ : NormedField 𝕜
inst✝¹⁰ : (i : ι) → TopologicalSpace (E i)
inst✝⁹ : (i : ι) → AddCommGroup (E i)
inst✝⁸ : (i : ι) → Module 𝕜 (E i)
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜 F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
E₁ : ι → Type u_5
inst✝³ : (i : ι) → TopologicalSpace (E₁ i)
inst✝² : ContinuousConstSMul 𝕜 F
inst✝¹ : (i : ι) → AddCommGroup (E₁ i)
inst✝ : (i : ι) → Module 𝕜 (E₁ i)
f : (i : ι) → E i →L[𝕜] E₁ i
x✝² : 𝕜
x✝¹ : ContinuousMultilinearMap 𝕜 E₁ F
x✝ : (i : ι) → E i
⊢ ((x✝² • x✝¹).compContinuousLinearMap f) x✝ = ((RingHom.id 𝕜) x✝² • x✝¹.compContinuousLinearMap f) x✝
Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
G : Type u_5
inst✝¹³ : NormedField 𝕜
inst✝¹² : (i : ι) → TopologicalSpace (E i)
inst✝¹¹ : (i : ι) → AddCommGroup (E i)
inst✝¹⁰ : (i : ι) → Module 𝕜 (E i)
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : IsTopologicalAddGroup F
inst✝⁵ : ContinuousConstSMul 𝕜 F
inst✝⁴ : AddCommGroup G
inst✝³ : Module 𝕜 G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜 G
g : F →L[𝕜] G
x✝¹ x✝ : ContinuousMultilinearMap 𝕜 E F
⊢ g.compContinuousMultilinearMap (x✝¹ + x✝) = g.compContinuousMultilinearMap x✝¹ + g.compContinuousMultilinearMap x✝

Tactic:
ext

Goal state after:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
G : Type u_5
inst✝¹³ : NormedField 𝕜
inst✝¹² : (i : ι) → TopologicalSpace (E i)
inst✝¹¹ : (i : ι) → AddCommGroup (E i)
inst✝¹⁰ : (i : ι) → Module 𝕜 (E i)
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : IsTopologicalAddGroup F
inst✝⁵ : ContinuousConstSMul 𝕜 F
inst✝⁴ : AddCommGroup G
inst✝³ : Module 𝕜 G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜 G
g : F →L[𝕜] G
x✝² x✝¹ : ContinuousMultilinearMap 𝕜 E F
x✝ : (i : ι) → E i
⊢ (g.compContinuousMultilinearMap (x✝² + x✝¹)) x✝ =
    (g.compContinuousMultilinearMap x✝² + g.compContinuousMultilinearMap x✝¹) x✝