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

Goal state before:
pp: case refine_3
α : Type u_2
ι : Type u_3
inst✝ : MeasurableSpace α
μ : Measure α
s : Finset ι
g : α → ℝ≥0∞
f : ι → α → ℝ≥0∞
hg : AEMeasurable g μ
hf : ∀ i ∈ s, AEMeasurable (f i) μ
q : ℝ
p : ι → ℝ
hpq : q + ∑ i ∈ s, p i = 1
hq : 0 ≤ q
hp : ∀ i ∈ s, 0 ≤ p i
⊢ ∀ i ∈ insertNone s, 0 ≤ i.elim q p

Tactic:
rintro (_ | i) hi
    · exact hq
    · refine hp i ?_
      simpa using hi

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp

Goal state before:
pp: α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
p q : ℝ
inst✝ : IsFiniteMeasure μ
hf : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm' f q μ < ∞
hp_nonneg : 0 ≤ p
hpq : p ≤ q
hp_pos : 0 < p
hq_pos : 0 < q
⊢ eLpNorm' f q μ * μ Set.univ ^ (1 / p - 1 / q) < ∞

Tactic:
rw [ENNReal.mul_lt_top_iff]

Goal state after:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
p q : ℝ
inst✝ : IsFiniteMeasure μ
hf : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm' f q μ < ∞
hp_nonneg : 0 ≤ p
hpq : p ≤ q
hp_pos : 0 < p
hq_pos : 0 < q
⊢ eLpNorm' f q μ < ∞ ∧ μ Set.univ ^ (1 / p - 1 / q) < ∞ ∨ eLpNorm' f q μ = 0 ∨ μ Set.univ ^ (1 / p - 1 / q) = 0
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: a b : ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
⊢ a * b ≤ a ^ p / p.toNNReal + b ^ q / q.toNNReal

Tactic:
by
  simpa [hpq.nonneg, hpq.symm.nonneg] using young_inequality a b hpq.toNNReal

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp

Goal state before:
pp: case h₂.inr.inr
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
μ : Measure α
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hp : 0 < p.toReal
hp₁ : 0 < p
hp₂ : p < ∞
⊢ ∫⁻ (x : α), (‖f x‖ₑ * ‖g x‖ₑ) ^ p.toReal ∂μ ≤
    (essSup (fun x ↦ ‖f x‖ₑ) μ * (∫⁻ (x : α), ‖g x‖ₑ ^ p.toReal ∂μ) ^ p.toReal⁻¹) ^ p.toReal

Tactic:
ENNReal.mul_rpow_of_nonneg (hz := hp.le),

Goal state after:
case h₂.inr.inr
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
μ : Measure α
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hp : 0 < p.toReal
hp₁ : 0 < p
hp₂ : p < ∞
⊢ ∫⁻ (x : α), (‖f x‖ₑ * ‖g x‖ₑ) ^ p.toReal ∂μ ≤
    essSup (fun x ↦ ‖f x‖ₑ) μ ^ p.toReal * ((∫⁻ (x : α), ‖g x‖ₑ ^ p.toReal ∂μ) ^ p.toReal⁻¹) ^ p.toReal
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
f g : ι → ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : Summable fun i ↦ f i ^ p
hg : Summable fun i ↦ g i ^ p
pos : 0 < p
⊢ (Summable fun i ↦ (f i + g i) ^ p) ∧
    (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)

Tactic:
have H₁ : ∀ s : Finset ι,
      (∑ i ∈ s, (f i + g i) ^ p) ≤
        ((∑' i, f i ^ p) ^ (1 / p) + (∑' i, g i ^ p) ^ (1 / p)) ^ p := by
    intro s
    rw [one_div, ← NNReal.rpow_inv_le_iff pos, ← one_div]
    refine le_trans (Lp_add_le s f g hp) ?_
    gcongr <;>
      refine Summable.sum_le_tsum _ (fun _ _ ↦ zero_le) ?_
    exacts [hf, hg]

Goal state after:
ι : Type u
f g : ι → ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : Summable fun i ↦ f i ^ p
hg : Summable fun i ↦ g i ^ p
pos : 0 < p
H₁ :
  ∀ (s : Finset ι), ∑ i ∈ s, (f i + g i) ^ p ≤ ((∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)) ^ p
⊢ (Summable fun i ↦ (f i + g i) ^ p) ∧
    (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)
Module: Mathlib.MeasureTheory.Function.LpSpace.Complete

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : SeminormedAddGroup E
f : ℕ → α → E
p : ℝ
hp_pos : 0 < p
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (f_lim x))
⊢ eLpNorm' f_lim p μ ≤ liminf (fun n ↦ eLpNorm' (f n) p μ) atTop

Tactic:
eLpNorm'_lim_eq_lintegral_liminf h_lim

Goal state after:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : SeminormedAddGroup E
f : ℕ → α → E
p : ℝ
hp_pos : 0 < p
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (f_lim x))
⊢ (∫⁻ (a : α), liminf (fun x ↦ ‖f x a‖ₑ ^ p) atTop ∂μ) ^ (1 / p) ≤ liminf (fun n ↦ eLpNorm' (f n) p μ) atTop
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 : α → E
hf : MemLp f p μ
⊢ (eLpNorm (↑↑(MemLp.toLp f hf)) p μ).toReal = (eLpNorm f p μ).toReal

Tactic:
eLpNorm_congr_ae (MemLp.coeFn_toLp hf)

Goal state after:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
⊢ (eLpNorm f p μ).toReal = (eLpNorm f p μ).toReal
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 : ↥(Lp E p μ)
hp : 0 < p
⊢ ‖f‖₊ = 0 ↔ f = 0

Tactic:
refine ⟨fun hf => ?_, fun hf => by simp [hf]⟩
  simp_rw [nnnorm_def, ENNReal.toNNReal_eq_zero_iff, eLpNorm_ne_top, or_false] at hf
  simp_rw [eq_zero_iff_ae_eq_zero, ← eLpNorm_eq_zero_iff (Lp.aestronglyMeasurable f) hp.ne.symm, hf]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hn : eLpNorm' (fun x ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖) p μ ≤ ∑' (i : ℕ), B i
hp_pos : 0 < p
⊢ ∫⁻ (a : α), (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ ≤ (∑' (i : ℕ), B i) ^ p

Tactic:
rw [← inv_inv p, @ENNReal.le_rpow_inv_iff _ _ p⁻¹ (by simp [hp_pos]), inv_inv p]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hn : eLpNorm' (fun x ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖) p μ ≤ ∑' (i : ℕ), B i
hp_pos : 0 < p
⊢ (∫⁻ (a : α), (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
hf : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
⊢ MemLp (fun x ↦ ‖f x‖ₑ ^ p.toReal) 1 μ

Tactic:
convert! hf.enorm_rpow_div p
  rw [div_eq_mul_inv, ENNReal.mul_inv_cancel hp_ne_zero hp_ne_top]

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
𝕜 : Type u_6
𝕜' : Type u_7
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜'
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜' F✝
σ : 𝕜 →+* 𝕜'
inst✝⁴ : RingHomIsometric σ
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
B : G →L[𝕜] E →L[𝕜] F
c : 𝕜
g : G
⊢ compLpₗ p μ (B (c • g)) = (RingHom.id 𝕜) c • compLpₗ p μ (B g)

Tactic:
ext f
    filter_upwards [(c • B g).coeFn_compLp f, (B g).coeFn_compLp f,
      Lp.coeFn_smul c ((B g).compLp f)] with x hx hg hsmul
    simp [hx, hsmul, hg]

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p : ℝ
hp : 1 ≤ p
⊢ (∑ 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
  by_cases H' : (∑ i ∈ s, f i ^ p) ^ (1 / p) = ⊤ ∨ (∑ i ∈ s, g i ^ p) ^ (1 / p) = ⊤
  · rcases H' with H' | H' <;> simp [H', -one_div]
  have pos : 0 < p := lt_of_lt_of_le zero_lt_one hp
  replace H' : (∀ i ∈ s, f i ≠ ⊤) ∧ ∀ i ∈ s, g i ≠ ⊤ := by
    simpa [ENNReal.rpow_eq_top_iff, asymm pos, pos, ENNReal.sum_eq_top, not_or] using H'
  have :=
    ENNReal.coe_le_coe.2
      (@NNReal.Lp_add_le _ s (fun i => ENNReal.toNNReal (f i)) (fun i => ENNReal.toNNReal (g i)) _
        hp)
  push_cast [ENNReal.coe_rpow_of_nonneg, le_of_lt pos, le_of_lt (one_div_pos.2 pos)] at this
  simp_all

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpOrder

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝⁴ : NormedAddCommGroup E
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : Fact (1 ≤ p)
inst✝ : ClosedIciTopology E
f : ℕ → ↥(Lp E p μ)
f₀ : ↥(Lp E p μ)
hf : ∀ (n : ℕ), 0 ≤ f n
h_tendsto : Filter.Tendsto f Filter.atTop (nhds f₀)
⊢ f₀ ∈ {x | 0 ≤ x}

Tactic:
simp only [← coeFn_nonneg] at hf ⊢
    obtain ⟨φ, -, hφ⟩ := tendstoInMeasure_of_tendsto_Lp h_tendsto |>.exists_seq_tendsto_ae
    filter_upwards [countable_iInter_mem.mpr hf, hφ] with x hx hφx
    exact ge_of_tendsto' hφx fun _ ↦ Set.mem_iInter.mp hx _

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.Units

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
t : R
h : ‖t‖ < ‖↑x⁻¹‖⁻¹
a✝ : Nontrivial R
hpos : 0 < ‖↑x⁻¹‖
⊢ ‖↑x⁻¹‖ * ‖t‖ < ‖↑x⁻¹‖ * ‖↑x⁻¹‖⁻¹

Tactic:
nlinarith only [h, hpos]

Goal state after:
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
i₀ : ι
y : (i : ι) → E i := I.piecewise (fun i ↦ c i • x i) x
⊢ ((fun x ↦ a • x) ∘ ⇑f) x ∈ V

Tactic:
calc
      f (update y i₀ ((a / ∏ i ∈ I, c i) • y i₀)) ∈ V := hft fun i hi => by
        rcases eq_or_ne i i₀ with rfl | hne
        · simp_rw [update_self, y, I.piecewise_eq_of_mem _ _ hi, smul_smul]
          refine hc _ _ ?_ _ hx
          calc
            ‖(a / ∏ i ∈ I, c i) * c i‖ ≤ (‖∏ i ∈ I, c i‖ / ‖∏ i ∈ I, c i‖) * ‖c i‖ := by
              rw [norm_mul, norm_div]; gcongr; exact ha.out.le
            _ ≤ 1 * ‖c i‖ := by gcongr; apply div_self_le_one
            _ = ‖c i‖ := one_mul _
        · simp_rw [update_of_ne hne, y, I.piecewise_eq_of_mem _ _ hi]
          exact hc _ _ le_rfl _ hx
      _ = a • f x := by
        rw [f.map_update_smul, update_eq_self, f.map_piecewise_smul, div_eq_mul_inv, mul_smul,
          inv_smul_smul₀ hc₀']

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

Goal state before:
pp: case inr
𝕜 : 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✝⁴ : UniformSpace F
inst✝³ : IsUniformAddGroup F
inst✝² : ∀ (i : ι), ContinuousSMul 𝕜 (E i)
inst✝¹ : ContinuousConstSMul 𝕜 F
inst✝ : CompleteSpace F
h : IsCoherentWith {s | IsVonNBounded 𝕜 s}
this :
  ∀ {F : Type u_4} [inst : AddCommGroup F] [inst_1 : Module 𝕜 F] [inst_2 : UniformSpace F]
    [inst_3 : IsUniformAddGroup F] [ContinuousConstSMul 𝕜 F] [CompleteSpace F],
    T2Space F → CompleteSpace (ContinuousMultilinearMap 𝕜 E F)
hF : ¬T2Space F
⊢ Surjective (SeparationQuotient.mkCLM 𝕜 F).compContinuousMultilinearMap

Tactic:
intro f

Goal state after:
case inr
𝕜 : 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✝⁴ : UniformSpace F
inst✝³ : IsUniformAddGroup F
inst✝² : ∀ (i : ι), ContinuousSMul 𝕜 (E i)
inst✝¹ : ContinuousConstSMul 𝕜 F
inst✝ : CompleteSpace F
h : IsCoherentWith {s | IsVonNBounded 𝕜 s}
this :
  ∀ {F : Type u_4} [inst : AddCommGroup F] [inst_1 : Module 𝕜 F] [inst_2 : UniformSpace F]
    [inst_3 : IsUniformAddGroup F] [ContinuousConstSMul 𝕜 F] [CompleteSpace F],
    T2Space F → CompleteSpace (ContinuousMultilinearMap 𝕜 E F)
hF : ¬T2Space F
f : ContinuousMultilinearMap 𝕜 E (SeparationQuotient F)
⊢ ∃ a, (SeparationQuotient.mkCLM 𝕜 F).compContinuousMultilinearMap a = f
Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology

Goal state before:
pp: case inr
𝕜 : 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✝⁴ : UniformSpace F
inst✝³ : IsUniformAddGroup F
inst✝² : ∀ (i : ι), ContinuousSMul 𝕜 (E i)
inst✝¹ : ContinuousConstSMul 𝕜 F
inst✝ : CompleteSpace F
h : IsCoherentWith {s | IsVonNBounded 𝕜 s}
this :
  ∀ {F : Type u_4} [inst : AddCommGroup F] [inst_1 : Module 𝕜 F] [inst_2 : UniformSpace F]
    [inst_3 : IsUniformAddGroup F] [ContinuousConstSMul 𝕜 F] [CompleteSpace F],
    T2Space F → CompleteSpace (ContinuousMultilinearMap 𝕜 E F)
hF : ¬T2Space F
f : ContinuousMultilinearMap 𝕜 E (SeparationQuotient F)
⊢ ∃ a, (SeparationQuotient.mkCLM 𝕜 F).compContinuousMultilinearMap a = f

Tactic:
use (SeparationQuotient.outCLM _ _).compContinuousMultilinearMap f

Goal state after:
case h
𝕜 : 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✝⁴ : UniformSpace F
inst✝³ : IsUniformAddGroup F
inst✝² : ∀ (i : ι), ContinuousSMul 𝕜 (E i)
inst✝¹ : ContinuousConstSMul 𝕜 F
inst✝ : CompleteSpace F
h : IsCoherentWith {s | IsVonNBounded 𝕜 s}
this :
  ∀ {F : Type u_4} [inst : AddCommGroup F] [inst_1 : Module 𝕜 F] [inst_2 : UniformSpace F]
    [inst_3 : IsUniformAddGroup F] [ContinuousConstSMul 𝕜 F] [CompleteSpace F],
    T2Space F → CompleteSpace (ContinuousMultilinearMap 𝕜 E F)
hF : ¬T2Space F
f : ContinuousMultilinearMap 𝕜 E (SeparationQuotient F)
⊢ (SeparationQuotient.mkCLM 𝕜 F).compContinuousMultilinearMap
      ((SeparationQuotient.outCLM 𝕜 F).compContinuousMultilinearMap f) =
    f
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
inst✝ : ContinuousConstSMul 𝕜 F
S : Set (ContinuousMultilinearMap 𝕜 E F)
hS : IsVonNBounded 𝕜 S
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
U : Set F
hU : U ∈ 𝓝 0
c : 𝕜
hc : S ⊆ c • {x | MapsTo (⇑x) s U}
⊢ ∀ x ∈ S, ∀ y ∈ s, x y ∈ c • U

Tactic:
intro f

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
inst✝ : ContinuousConstSMul 𝕜 F
S : Set (ContinuousMultilinearMap 𝕜 E F)
hS : IsVonNBounded 𝕜 S
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
U : Set F
hU : U ∈ 𝓝 0
c : 𝕜
hc : S ⊆ c • {x | MapsTo (⇑x) s U}
f : ContinuousMultilinearMap 𝕜 E F
⊢ f ∈ S → ∀ y ∈ s, f y ∈ c • U
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s : Set α
h : μ s ≠ ∞
⊢ μ.real s ≠ 0 ↔ μ s ≠ 0

Tactic:
by
  simp [measureReal_eq_zero_iff, h]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
ht : NullMeasurableSet t μ
h₁ : μ s ≠ ∞
h₂ : μ t ≠ ∞
this : μ (s ∪ t) ≠ ∞
⊢ μ.real t + μ.real (s \ t) + μ.real (s ∩ t) = μ.real (s ∩ t) + μ.real (s \ t) + μ.real t

Tactic:
ac_rfl

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

Goal state before:
pp: 𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
inst✝⁷ : CompleteSpace 𝕜
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [T2Space E] {ι : Type v} [inst_6 : Finite ι]
    (ξ : Basis ι 𝕜 E) (this : Fintype ι),
    let this_1 := IsTopologicalAddGroup.rightUniformSpace E;
    let this_2 := ⋯;
    Fintype.card ι = n → Continuous[_, Pi.topologicalSpace] ⇑ξ.equivFun
E : Type v
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : T2Space E
ι : Type v
inst✝ : Finite ι
ξ : Basis ι 𝕜 E
this✝² : Fintype ι
this✝¹ : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this✝ : IsUniformAddGroup E := isUniformAddGroup_of_addCommGroup
hn : Fintype.card ι = n + 1
this : FiniteDimensional 𝕜 E
H₁ : ∀ (s : Submodule 𝕜 E), finrank 𝕜 ↥s = n → IsClosed[inst✝⁴] ↑s
⊢ ∀ (f : E →ₗ[𝕜] 𝕜), Continuous[inst✝⁴, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ⇑f

Tactic:
intro f

Goal state after:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
inst✝⁷ : CompleteSpace 𝕜
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [T2Space E] {ι : Type v} [inst_6 : Finite ι]
    (ξ : Basis ι 𝕜 E) (this : Fintype ι),
    let this_1 := IsTopologicalAddGroup.rightUniformSpace E;
    let this_2 := ⋯;
    Fintype.card ι = n → Continuous[_, Pi.topologicalSpace] ⇑ξ.equivFun
E : Type v
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : T2Space E
ι : Type v
inst✝ : Finite ι
ξ : Basis ι 𝕜 E
this✝² : Fintype ι
this✝¹ : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this✝ : IsUniformAddGroup E := isUniformAddGroup_of_addCommGroup
hn : Fintype.card ι = n + 1
this : FiniteDimensional 𝕜 E
H₁ : ∀ (s : Submodule 𝕜 E), finrank 𝕜 ↥s = n → IsClosed[inst✝⁴] ↑s
f : E →ₗ[𝕜] 𝕜
⊢ Continuous[inst✝⁴, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ⇑f
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
l : Filter α
f : α → E
h' : ∀ s ∈ l, μ s = ∞
a : E
hf : Tendsto f l (𝓝 a)
H : ¬a = 0
ε : ℝ
εpos : 0 < ε
hε : ε < ‖a‖
u : Set α
ul : u ∈ l
hu : IntegrableOn f u μ
v : Set α := u ∩ {b | ε < ‖f b‖}
hv : IntegrableOn f v μ
vl : v ∈ l
this✝ : (μ.restrict v) v < ∞
this : μ v ≠ ∞
⊢ False

Tactic:
exact this (h' v vl)

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: 𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E G
⊢ ‖-f‖ = ‖f‖

Tactic:
by simp [norm_def]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: case h
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
A : ∀ (f : ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
c : 𝕜
hc : 1 < ‖c‖
hc₀ : 0 < ‖c‖
⊢ ∀ (f : ContinuousMultilinearMap 𝕜 E G), (∀ (x : (i : ι) → E i), ‖x‖ ≤ ‖c‖ → ‖f x‖ ≤ 1) → ‖f‖ ≤ 1

Tactic:
intro f

Goal state after:
case h
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
A : ∀ (f : ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
c : 𝕜
hc : 1 < ‖c‖
hc₀ : 0 < ‖c‖
f : ContinuousMultilinearMap 𝕜 E G
⊢ (∀ (x : (i : ι) → E i), ‖x‖ ≤ ‖c‖ → ‖f x‖ ≤ 1) → ‖f‖ ≤ 1
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
n : ℕ
A : Type u_1
inst✝¹ : SeminormedRing A
inst✝ : NormedAlgebra 𝕜 A
hn : 0 < n
⊢ ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n A‖ ≤ 1

Tactic:
by
  obtain ⟨n, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hn.ne'
  exact norm_mkPiAlgebraFin_succ_le

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst✝⁵ : PartialOrder α
inst✝⁴ : MeasurableSingletonClass α
inst✝³ : TopologicalSpace ε'
inst✝² : ESeminormedAddMonoid ε'
inst✝¹ : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
a b : α
inst✝ : NullSingletonClass μ
ha : ‖f a‖ₑ ≠ ∞
hb : ‖f b‖ₑ ≠ ∞
⊢ IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ioo a b) μ

Tactic:
by
  rw [integrableOn_Icc_iff_integrableOn_Ioc ha, integrableOn_Ioc_iff_integrableOn_Ioo hb]

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable

Goal state before:
pp: case inr
ι : Type u_1
X : Type u_2
E : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace E
inst✝² : Countable ι
l : Filter ι
inst✝¹ : l.IsCountablyGenerated
f : ι → X → E
inst✝ : IsCompletelyPseudoMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
hl : l.NeBot
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : UpgradedIsCompletelyPseudoMetrizableSpace E := upgradeIsCompletelyPseudoMetrizable E
⊢ MeasurableSet {x | ∃ c, Tendsto (fun x_1 ↦ f x_1 x) l (𝓝 c)}

Tactic:
let s := closure (⋃ i, range (f i))

Goal state after:
case inr
ι : Type u_1
X : Type u_2
E : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace E
inst✝² : Countable ι
l : Filter ι
inst✝¹ : l.IsCountablyGenerated
f : ι → X → E
inst✝ : IsCompletelyPseudoMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
hl : l.NeBot
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : UpgradedIsCompletelyPseudoMetrizableSpace E := upgradeIsCompletelyPseudoMetrizable E
s : Set E := closure[inst✝³] (⋃ i, range (f i))
⊢ MeasurableSet {x | ∃ c, Tendsto (fun x_1 ↦ f x_1 x) l (𝓝 c)}