mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: case mk.mk
α : 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_6
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
β : Type u_7
inst✝ : MeasurableSpace β
μb : Measure β
f✝ f : α → β
hf : MeasurePreserving f μ μb
val✝¹ : β →ₘ[μb] E
a✝¹ : { f // AEStronglyMeasurable f μb }
property✝¹ : Quot.mk (⇑(Measure.aeEqSetoid E μb)) a✝¹ ∈ Lp E p μb
val✝ : β →ₘ[μb] E
a✝ : { f // AEStronglyMeasurable f μb }
property✝ : Quot.mk (⇑(Measure.aeEqSetoid E μb)) a✝ ∈ Lp E p μb
⊢ ⟨(↑(⟨Quot.mk (⇑(Measure.aeEqSetoid E μb)) a✝¹, property✝¹⟩ +
              ⟨Quot.mk (⇑(Measure.aeEqSetoid E μb)) a✝, property✝⟩)).compMeasurePreserving
        f hf,
      ⋯⟩ =
    ⟨(↑⟨Quot.mk (⇑(Measure.aeEqSetoid E μb)) a✝¹, property✝¹⟩).compMeasurePreserving f hf, ⋯⟩ +
      ⟨(↑⟨Quot.mk (⇑(Measure.aeEqSetoid E μb)) a✝, property✝⟩).compMeasurePreserving f hf, ⋯⟩

Tactic:
;

Goal state after:
case mk.mk
α : 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_6
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
β : Type u_7
inst✝ : MeasurableSpace β
μb : Measure β
f✝ f : α → β
hf : MeasurePreserving f μ μb
val✝¹ : β →ₘ[μb] E
a✝¹ : { f // AEStronglyMeasurable f μb }
property✝¹ : Quot.mk (⇑(Measure.aeEqSetoid E μb)) a✝¹ ∈ Lp E p μb
val✝ : β →ₘ[μb] E
a✝ : { f // AEStronglyMeasurable f μb }
property✝ : Quot.mk (⇑(Measure.aeEqSetoid E μb)) a✝ ∈ Lp E p μb
⊢ ⟨(↑(⟨Quot.mk (⇑(Measure.aeEqSetoid E μb)) a✝¹, property✝¹⟩ +
              ⟨Quot.mk (⇑(Measure.aeEqSetoid E μb)) a✝, property✝⟩)).compMeasurePreserving
        f hf,
      ⋯⟩ =
    ⟨(↑⟨Quot.mk (⇑(Measure.aeEqSetoid E μb)) a✝¹, property✝¹⟩).compMeasurePreserving f hf, ⋯⟩ +
      ⟨(↑⟨Quot.mk (⇑(Measure.aeEqSetoid E μb)) a✝, property✝⟩).compMeasurePreserving f hf, ⋯⟩
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: case mk
α : 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_6
inst✝⁵ : TopologicalSpace ε
inst✝⁴ : ContinuousENorm ε
β : Type u_7
inst✝³ : MeasurableSpace β
μb : Measure β
f✝ : α → β
𝕜 : Type u_8
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
f : α → β
hf : MeasurePreserving f μ μb
c : 𝕜
val✝ : β →ₘ[μb] E
a✝ : { f // AEStronglyMeasurable f μb }
property✝ : Quot.mk (⇑(Measure.aeEqSetoid E μb)) a✝ ∈ Lp E p μb
⊢ (↑(compMeasurePreserving f hf)).toFun (c • ⟨Quot.mk (⇑(Measure.aeEqSetoid E μb)) a✝, property✝⟩) =
    (RingHom.id 𝕜) c • (↑(compMeasurePreserving f hf)).toFun ⟨Quot.mk (⇑(Measure.aeEqSetoid E μb)) a✝, property✝⟩

Tactic:
;

Goal state after:
case mk
α : 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_6
inst✝⁵ : TopologicalSpace ε
inst✝⁴ : ContinuousENorm ε
β : Type u_7
inst✝³ : MeasurableSpace β
μb : Measure β
f✝ : α → β
𝕜 : Type u_8
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
f : α → β
hf : MeasurePreserving f μ μb
c : 𝕜
val✝ : β →ₘ[μb] E
a✝ : { f // AEStronglyMeasurable f μb }
property✝ : Quot.mk (⇑(Measure.aeEqSetoid E μb)) a✝ ∈ Lp E p μb
⊢ (↑(compMeasurePreserving f hf)).toFun (c • ⟨Quot.mk (⇑(Measure.aeEqSetoid E μb)) a✝, property✝⟩) =
    (RingHom.id 𝕜) c • (↑(compMeasurePreserving f hf)).toFun ⟨Quot.mk (⇑(Measure.aeEqSetoid E μb)) a✝, property✝⟩
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
f : ↥(Lp E p μ)
⊢ (compLpL p μ (L + L')) f = (compLpL p μ L + compLpL p μ L') f

Tactic:
;

Goal state after:
α : 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
f : ↥(Lp E p μ)
⊢ (compLpL p μ (L + L')) f = (compLpL p μ L + compLpL p μ L') f
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)
𝕜'' : Type u_8
inst✝³ : NormedRing 𝕜''
inst✝² : Module 𝕜'' F
inst✝¹ : IsBoundedSMul 𝕜'' F
inst✝ : SMulCommClass 𝕜' 𝕜'' F
c : 𝕜''
L : E →SL[σ] F
f : ↥(Lp E p μ)
⊢ (compLpL p μ (c • L)) f = (c • compLpL p μ L) f

Tactic:
;

Goal state after:
α : 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)
𝕜'' : Type u_8
inst✝³ : NormedRing 𝕜''
inst✝² : Module 𝕜'' F
inst✝¹ : IsBoundedSMul 𝕜'' F
inst✝ : SMulCommClass 𝕜' 𝕜'' F
c : 𝕜''
L : E →SL[σ] F
f : ↥(Lp E p μ)
⊢ (compLpL p μ (c • L)) f = (c • compLpL p μ L) f
Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure

Goal state before:
pp: α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
f : ι → α → E
g : α → E
inst✝ : SeminormedAddCommGroup E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
l : Filter ι
ε : ℝ≥0∞
hε : 0 < ε
hε_top : ε ≠ ∞
hfg : ∀ ε_1 > 0, ∀ᶠ (x : ι) in l, 1 / ε ^ p.toReal * eLpNorm (f x - g) p μ ^ p.toReal ≤ ε_1
δ : ℝ≥0∞
hδ : δ > 0
n : ι
hn : 1 / ε ^ p.toReal * eLpNorm (f n - g) p μ ^ p.toReal ≤ δ
⊢ μ {x | ε ≤ edist (f n x) (g x)} ≤ (ε ^ p.toReal)⁻¹ * eLpNorm (f n - g) p μ ^ p.toReal

Tactic:
← ENNReal.inv_mul_le_iff,

Goal state after:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
f : ι → α → E
g : α → E
inst✝ : SeminormedAddCommGroup E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
l : Filter ι
ε : ℝ≥0∞
hε : 0 < ε
hε_top : ε ≠ ∞
hfg : ∀ ε_1 > 0, ∀ᶠ (x : ι) in l, 1 / ε ^ p.toReal * eLpNorm (f x - g) p μ ^ p.toReal ≤ ε_1
δ : ℝ≥0∞
hδ : δ > 0
n : ι
hn : 1 / ε ^ p.toReal * eLpNorm (f n - g) p μ ^ p.toReal ≤ δ
⊢ (ε ^ p.toReal)⁻¹⁻¹ * μ {x | ε ≤ edist (f n x) (g x)} ≤ eLpNorm (f n - g) p μ ^ p.toReal

case h1
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
f : ι → α → E
g : α → E
inst✝ : SeminormedAddCommGroup E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
l : Filter ι
ε : ℝ≥0∞
hε : 0 < ε
hε_top : ε ≠ ∞
hfg : ∀ ε_1 > 0, ∀ᶠ (x : ι) in l, 1 / ε ^ p.toReal * eLpNorm (f x - g) p μ ^ p.toReal ≤ ε_1
δ : ℝ≥0∞
hδ : δ > 0
n : ι
hn : 1 / ε ^ p.toReal * eLpNorm (f n - g) p μ ^ p.toReal ≤ δ
⊢ (ε ^ p.toReal)⁻¹ ≠ 0

case h2
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
f : ι → α → E
g : α → E
inst✝ : SeminormedAddCommGroup E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
l : Filter ι
ε : ℝ≥0∞
hε : 0 < ε
hε_top : ε ≠ ∞
hfg : ∀ ε_1 > 0, ∀ᶠ (x : ι) in l, 1 / ε ^ p.toReal * eLpNorm (f x - g) p μ ^ p.toReal ≤ ε_1
δ : ℝ≥0∞
hδ : δ > 0
n : ι
hn : 1 / ε ^ p.toReal * eLpNorm (f n - g) p μ ^ p.toReal ≤ δ
⊢ (ε ^ p.toReal)⁻¹ ≠ ∞
Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure

Goal state before:
pp: α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
f : ι → α → E
g : α → E
inst✝ : SeminormedAddCommGroup E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
l : Filter ι
hfg : Tendsto (fun n ↦ eLpNorm (f n - g) p μ) l (𝓝 0)
n : ι
⊢ eLpNorm (AEStronglyMeasurable.mk (f n) ⋯ - AEStronglyMeasurable.mk g hg) p μ = eLpNorm (f n - g) p μ

Tactic:
;

Goal state after:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
f : ι → α → E
g : α → E
inst✝ : SeminormedAddCommGroup E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
l : Filter ι
hfg : Tendsto (fun n ↦ eLpNorm (f n - g) p μ) l (𝓝 0)
n : ι
⊢ eLpNorm (AEStronglyMeasurable.mk (f n) ⋯ - AEStronglyMeasurable.mk g hg) p μ = eLpNorm (f n - g) p μ
Module: Mathlib.Topology.Algebra.Module.Multilinear.Basic

Goal state before:
pp: R : Type u
ι : Type v
M₁ : ι → Type w₁
M₂ : Type w₂
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁴ : AddCommMonoid M₂
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
inst✝¹ : (i : ι) → TopologicalSpace (M₁ i)
inst✝ : TopologicalSpace M₂
f : MultilinearMap R M₁ M₂
hf : Continuous f.toFun
hg : Continuous { toMultilinearMap := f, cont := hf }.toFun
⊢ { toMultilinearMap := f, cont := hf } =
    { toMultilinearMap := { toMultilinearMap := f, cont := hf }.toMultilinearMap, cont := hg }

Tactic:
;

Goal state after:
R : Type u
ι : Type v
M₁ : ι → Type w₁
M₂ : Type w₂
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁴ : AddCommMonoid M₂
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
inst✝¹ : (i : ι) → TopologicalSpace (M₁ i)
inst✝ : TopologicalSpace M₂
f : MultilinearMap R M₁ M₂
hf : Continuous f.toFun
hg : Continuous { toMultilinearMap := f, cont := hf }.toFun
⊢ { toMultilinearMap := f, cont := hf } =
    { toMultilinearMap := { toMultilinearMap := f, cont := hf }.toMultilinearMap, cont := hg }
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) fun x ↦ 1) = 0 fun x ↦ 1

Tactic:
;

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.Topology.Algebra.Module.Multilinear.Bounded

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
F : Type u_3
E : ι → Type u_4
inst✝⁷ : NormedField 𝕜
inst✝⁶ : (i : ι) → AddCommGroup (E i)
inst✝⁵ : (i : ι) → Module 𝕜 (E i)
inst✝⁴ : (i : ι) → TopologicalSpace (E i)
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : TopologicalSpace F
inst✝ : Nonempty ι
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
f : ContinuousMultilinearMap 𝕜 E F
V : Set F
hV : V ∈ 𝓝 0
h₁ : ¬∀ (c : 𝕜), ‖c‖ ≤ 1
x✝ : NontriviallyNormedField 𝕜 := { toNormedField := inst✝⁷, non_trivial := ⋯ }
I : Finset ι
t : (i : ι) → Set (E i)
ht₀ : ∀ (i : ι), t i ∈ 𝓝 0
hft : (↑I).pi t ⊆ ⇑f ⁻¹' V
c : ι → 𝕜
hc₀ : ∀ (i : ι), c i ≠ 0
hc : ∀ (i : ι) (c' : 𝕜), ‖c'‖ ≤ ‖c i‖ → ∀ x ∈ s, c' • x i ∈ t i
hc₀' : ∏ i ∈ I, c i ≠ 0
a : 𝕜
ha : a ∈ {y | ‖y‖ < ‖∏ i ∈ I, c i‖}
x : (i : ι) → E i
hx : x ∈ s
y : (i : ι) → E i := I.piecewise (fun i ↦ c i • x i) x
i : ι
hi : i ∈ ↑I
⊢ ‖a‖ / ‖∏ i ∈ I, c i‖ * ‖c i‖ ≤ ‖∏ i ∈ I, c i‖ / ‖∏ i ∈ I, c i‖ * ‖c i‖

Tactic:
;

Goal state after:
ι : Type u_1
𝕜 : Type u_2
F : Type u_3
E : ι → Type u_4
inst✝⁷ : NormedField 𝕜
inst✝⁶ : (i : ι) → AddCommGroup (E i)
inst✝⁵ : (i : ι) → Module 𝕜 (E i)
inst✝⁴ : (i : ι) → TopologicalSpace (E i)
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : TopologicalSpace F
inst✝ : Nonempty ι
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
f : ContinuousMultilinearMap 𝕜 E F
V : Set F
hV : V ∈ 𝓝 0
h₁ : ¬∀ (c : 𝕜), ‖c‖ ≤ 1
x✝ : NontriviallyNormedField 𝕜 := { toNormedField := inst✝⁷, non_trivial := ⋯ }
I : Finset ι
t : (i : ι) → Set (E i)
ht₀ : ∀ (i : ι), t i ∈ 𝓝 0
hft : (↑I).pi t ⊆ ⇑f ⁻¹' V
c : ι → 𝕜
hc₀ : ∀ (i : ι), c i ≠ 0
hc : ∀ (i : ι) (c' : 𝕜), ‖c'‖ ≤ ‖c i‖ → ∀ x ∈ s, c' • x i ∈ t i
hc₀' : ∏ i ∈ I, c i ≠ 0
a : 𝕜
ha : a ∈ {y | ‖y‖ < ‖∏ i ∈ I, c i‖}
x : (i : ι) → E i
hx : x ∈ s
y : (i : ι) → E i := I.piecewise (fun i ↦ c i • x i) x
i : ι
hi : i ∈ ↑I
⊢ ‖a‖ / ‖∏ i ∈ I, c i‖ * ‖c i‖ ≤ ‖∏ i ∈ I, c i‖ / ‖∏ i ∈ I, c i‖ * ‖c i‖
Module: Mathlib.Topology.Algebra.Module.Multilinear.Bounded

Goal state before:
pp: case hab
ι : Type u_1
𝕜 : Type u_2
F : Type u_3
E : ι → Type u_4
inst✝⁷ : NormedField 𝕜
inst✝⁶ : (i : ι) → AddCommGroup (E i)
inst✝⁵ : (i : ι) → Module 𝕜 (E i)
inst✝⁴ : (i : ι) → TopologicalSpace (E i)
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : TopologicalSpace F
inst✝ : Nonempty ι
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
f : ContinuousMultilinearMap 𝕜 E F
V : Set F
hV : V ∈ 𝓝 0
h₁ : ¬∀ (c : 𝕜), ‖c‖ ≤ 1
x✝ : NontriviallyNormedField 𝕜 := ⋯
I : Finset ι
t : (i : ι) → Set (E i)
ht₀ : ∀ (i : ι), t i ∈ 𝓝 0
hft : (↑I).pi t ⊆ ⇑f ⁻¹' V
c : ι → 𝕜
hc₀ : ∀ (i : ι), c i ≠ 0
hc : ∀ (i : ι) (c' : 𝕜), ‖c'‖ ≤ ‖c i‖ → ∀ x ∈ s, c' • x i ∈ t i
hc₀' : ∏ i ∈ I, c i ≠ 0
a : 𝕜
ha : a ∈ {y | ‖y‖ < ‖∏ i ∈ I, c i‖}
x : (i : ι) → E i
hx : x ∈ s
y : (i : ι) → E i := ⋯
i : ι
hi : i ∈ ↑I
⊢ ‖a‖ ≤ ‖∏ i ∈ I, c i‖

Tactic:
;

Goal state after:
case hab
ι : Type u_1
𝕜 : Type u_2
F : Type u_3
E : ι → Type u_4
inst✝⁷ : NormedField 𝕜
inst✝⁶ : (i : ι) → AddCommGroup (E i)
inst✝⁵ : (i : ι) → Module 𝕜 (E i)
inst✝⁴ : (i : ι) → TopologicalSpace (E i)
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : TopologicalSpace F
inst✝ : Nonempty ι
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
f : ContinuousMultilinearMap 𝕜 E F
V : Set F
hV : V ∈ 𝓝 0
h₁ : ¬∀ (c : 𝕜), ‖c‖ ≤ 1
x✝ : NontriviallyNormedField 𝕜 := ⋯
I : Finset ι
t : (i : ι) → Set (E i)
ht₀ : ∀ (i : ι), t i ∈ 𝓝 0
hft : (↑I).pi t ⊆ ⇑f ⁻¹' V
c : ι → 𝕜
hc₀ : ∀ (i : ι), c i ≠ 0
hc : ∀ (i : ι) (c' : 𝕜), ‖c'‖ ≤ ‖c i‖ → ∀ x ∈ s, c' • x i ∈ t i
hc₀' : ∏ i ∈ I, c i ≠ 0
a : 𝕜
ha : a ∈ {y | ‖y‖ < ‖∏ i ∈ I, c i‖}
x : (i : ι) → E i
hx : x ∈ s
y : (i : ι) → E i := ⋯
i : ι
hi : i ∈ ↑I
⊢ ‖a‖ ≤ ‖∏ i ∈ I, c i‖
Module: Mathlib.Topology.Algebra.Module.Multilinear.Bounded

Goal state before:
pp: case hbc
ι : Type u_1
𝕜 : Type u_2
F : Type u_3
E : ι → Type u_4
inst✝⁷ : NormedField 𝕜
inst✝⁶ : (i : ι) → AddCommGroup (E i)
inst✝⁵ : (i : ι) → Module 𝕜 (E i)
inst✝⁴ : (i : ι) → TopologicalSpace (E i)
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : TopologicalSpace F
inst✝ : Nonempty ι
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
f : ContinuousMultilinearMap 𝕜 E F
V : Set F
hV : V ∈ 𝓝 0
h₁ : ¬∀ (c : 𝕜), ‖c‖ ≤ 1
x✝ : NontriviallyNormedField 𝕜 := ⋯
I : Finset ι
t : (i : ι) → Set (E i)
ht₀ : ∀ (i : ι), t i ∈ 𝓝 0
hft : (↑I).pi t ⊆ ⇑f ⁻¹' V
c : ι → 𝕜
hc₀ : ∀ (i : ι), c i ≠ 0
hc : ∀ (i : ι) (c' : 𝕜), ‖c'‖ ≤ ‖c i‖ → ∀ x ∈ s, c' • x i ∈ t i
hc₀' : ∏ i ∈ I, c i ≠ 0
a : 𝕜
ha : a ∈ {y | ‖y‖ < ‖∏ i ∈ I, c i‖}
x : (i : ι) → E i
hx : x ∈ s
y : (i : ι) → E i := ⋯
i : ι
hi : i ∈ ↑I
⊢ ‖∏ i ∈ I, c i‖ / ‖∏ i ∈ I, c i‖ ≤ 1

Tactic:
;

Goal state after:
case hbc
ι : Type u_1
𝕜 : Type u_2
F : Type u_3
E : ι → Type u_4
inst✝⁷ : NormedField 𝕜
inst✝⁶ : (i : ι) → AddCommGroup (E i)
inst✝⁵ : (i : ι) → Module 𝕜 (E i)
inst✝⁴ : (i : ι) → TopologicalSpace (E i)
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : TopologicalSpace F
inst✝ : Nonempty ι
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
f : ContinuousMultilinearMap 𝕜 E F
V : Set F
hV : V ∈ 𝓝 0
h₁ : ¬∀ (c : 𝕜), ‖c‖ ≤ 1
x✝ : NontriviallyNormedField 𝕜 := ⋯
I : Finset ι
t : (i : ι) → Set (E i)
ht₀ : ∀ (i : ι), t i ∈ 𝓝 0
hft : (↑I).pi t ⊆ ⇑f ⁻¹' V
c : ι → 𝕜
hc₀ : ∀ (i : ι), c i ≠ 0
hc : ∀ (i : ι) (c' : 𝕜), ‖c'‖ ≤ ‖c i‖ → ∀ x ∈ s, c' • x i ∈ t i
hc₀' : ∏ i ∈ I, c i ≠ 0
a : 𝕜
ha : a ∈ {y | ‖y‖ < ‖∏ i ∈ I, c i‖}
x : (i : ι) → E i
hx : x ∈ s
y : (i : ι) → E i := ⋯
i : ι
hi : i ∈ ↑I
⊢ ‖∏ i ∈ I, c i‖ / ‖∏ i ∈ I, c i‖ ≤ 1
Module: Mathlib.Analysis.Normed.Ring.Units

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
n : ℕ
t : R
ht : ‖t‖ < 1
this : Summable fun n ↦ t ^ n
⊢ ∑ i ∈ range n, t ^ i + t ^ n * ∑' (i : ℕ), t ^ i = ∑ i ∈ range n, t ^ i + t ^ n * ↑(Units.oneSub t ht)⁻¹

Tactic:
;

Goal state after:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
n : ℕ
t : R
ht : ‖t‖ < 1
this : Summable fun n ↦ t ^ n
⊢ ∑ i ∈ range n, t ^ i + t ^ n * ∑' (i : ℕ), t ^ i = ∑ i ∈ range n, t ^ i + t ^ n * ↑(Units.oneSub t ht)⁻¹
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
x✝¹ x✝ : R
⊢ ((mul 𝕜 R).flip x✝¹) x✝ = ((mul 𝕜 R) x✝¹) x✝

Tactic:
;

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.Analysis.Normed.Operator.NormedSpace

Goal state before:
pp: case pos
𝕜 : Type u_1
𝕜₂ : Type u_3
E : Type u_5
F : Type u_6
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
ε C : ℝ
ε_pos : 0 < ε
c : 𝕜
hc : 1 < ‖c‖
hf : ∀ (x : E), ε / ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖f x‖ ≤ C * ‖x‖
x : E
hx : x = 0
⊢ ‖f x‖ ≤ C * ‖x‖

pp: case neg
𝕜 : Type u_1
𝕜₂ : Type u_3
E : Type u_5
F : Type u_6
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
ε C : ℝ
ε_pos : 0 < ε
c : 𝕜
hc : 1 < ‖c‖
hf : ∀ (x : E), ε / ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖f x‖ ≤ C * ‖x‖
x : E
hx : ¬x = 0
⊢ ‖f x‖ ≤ C * ‖x‖

Tactic:
;

Goal state after:
case pos
𝕜 : Type u_1
𝕜₂ : Type u_3
E : Type u_5
F : Type u_6
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
ε C : ℝ
ε_pos : 0 < ε
c : 𝕜
hc : 1 < ‖c‖
hf : ∀ (x : E), ε / ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖f x‖ ≤ C * ‖x‖
x : E
hx : x = 0
⊢ ‖f x‖ ≤ C * ‖x‖

case neg
𝕜 : Type u_1
𝕜₂ : Type u_3
E : Type u_5
F : Type u_6
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
ε C : ℝ
ε_pos : 0 < ε
c : 𝕜
hc : 1 < ‖c‖
hf : ∀ (x : E), ε / ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖f x‖ ≤ C * ‖x‖
x : E
hx : ¬x = 0
⊢ ‖f x‖ ≤ C * ‖x‖
Module: Mathlib.Analysis.Normed.Operator.NormedSpace

Goal state before:
pp: case hbc
𝕜 : Type u_1
𝕜₂ : Type u_3
E : Type u_5
F : Type u_6
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NontriviallyNormedField 𝕜₂
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : Filter.comap (⇑f) (𝓝 0) ≤ 𝓝 0
ε : ℝ≥0
ε0 : 0 < ↑ε
hε : ∀ (x : E), ‖f x‖ < ↑ε → ‖x‖ < 1
c : 𝕜
hc : 1 < ‖σ₁₂ c‖
x : E
hx : ¬f x = 0
hc₀ : c ≠ 0
n : ℤ
hlt : ‖f (c ^ n • x)‖ < ↑ε
hle : ‖c ^ n‖⁻¹ ≤ (↑ε)⁻¹ * ‖c‖ * ‖f x‖
⊢ ‖c ^ n • x‖ ≤ 1

Tactic:
;

Goal state after:
case hbc
𝕜 : Type u_1
𝕜₂ : Type u_3
E : Type u_5
F : Type u_6
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NontriviallyNormedField 𝕜₂
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : Filter.comap (⇑f) (𝓝 0) ≤ 𝓝 0
ε : ℝ≥0
ε0 : 0 < ↑ε
hε : ∀ (x : E), ‖f x‖ < ↑ε → ‖x‖ < 1
c : 𝕜
hc : 1 < ‖σ₁₂ c‖
x : E
hx : ¬f x = 0
hc₀ : c ≠ 0
n : ℤ
hlt : ‖f (c ^ n • x)‖ < ↑ε
hle : ‖c ^ n‖⁻¹ ≤ (↑ε)⁻¹ * ‖c‖ * ‖f x‖
⊢ ‖c ^ n • x‖ ≤ 1
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
hcont : Continuous[Pi.topologicalSpace, inst✝¹] ((toFun {s | IsVonNBounded 𝕜 s}) f)
hadd :
  ∀ (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)
hsmul :
  ∀ (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)
inst✝ : DecidableEq ι
⊢ ∀ (m : (i : ι) → E i) (i : ι) (x y : E i), f (update m i (x + y)) = f (update m i x) + f (update m i y)

Tactic:
;

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✝² : DecidableEq ι
inst✝¹ : TopologicalSpace F
f : ((i : ι) → E i) →ᵤ[{s | IsVonNBounded 𝕜 s}] F
hcont : Continuous[Pi.topologicalSpace, inst✝¹] ((toFun {s | IsVonNBounded 𝕜 s}) f)
hadd :
  ∀ (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)
hsmul :
  ∀ (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)
inst✝ : DecidableEq ι
⊢ ∀ (m : (i : ι) → E i) (i : ι) (x y : E i), f (update m i (x + y)) = f (update m i x) + f (update m i y)