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

Goal state before:
pp: α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg
S : ℕ → Set α := fun k ↦ {x | 2⁻¹ ^ k ≤ edist (f (ns k) x) (g x)}
hμS_le : ∀ (k : ℕ), μ (S k) ≤ 2⁻¹ ^ k
s : Set α := limsup S atTop
hs : s = limsup S atTop
hμs : μ s = 0
x : α
ε : ℝ≥0∞
hε : ε > 0
N k : ℕ
hk_lt_ε : 2 * 2⁻¹ ^ k < ε
n : ℕ
hNx : edist (f (ns n) x) (g x) < 2⁻¹ ^ n
hn_ge : n ≥ max N (k - 1)
⊢ (2 ^ n)⁻¹ ≤ (2 ^ k)⁻¹ * 2 ^ 1

Tactic:
ENNReal.inv_le_iff_le_mul,

Goal state after:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg
S : ℕ → Set α := fun k ↦ {x | 2⁻¹ ^ k ≤ edist (f (ns k) x) (g x)}
hμS_le : ∀ (k : ℕ), μ (S k) ≤ 2⁻¹ ^ k
s : Set α := limsup S atTop
hs : s = limsup S atTop
hμs : μ s = 0
x : α
ε : ℝ≥0∞
hε : ε > 0
N k : ℕ
hk_lt_ε : 2 * 2⁻¹ ^ k < ε
n : ℕ
hNx : edist (f (ns n) x) (g x) < 2⁻¹ ^ n
hn_ge : n ≥ max N (k - 1)
⊢ 1 ≤ 2 ^ n * ((2 ^ k)⁻¹ * 2 ^ 1)

case h₁
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg
S : ℕ → Set α := fun k ↦ {x | 2⁻¹ ^ k ≤ edist (f (ns k) x) (g x)}
hμS_le : ∀ (k : ℕ), μ (S k) ≤ 2⁻¹ ^ k
s : Set α := limsup S atTop
hs : s = limsup S atTop
hμs : μ s = 0
x : α
ε : ℝ≥0∞
hε : ε > 0
N k : ℕ
hk_lt_ε : 2 * 2⁻¹ ^ k < ε
n : ℕ
hNx : edist (f (ns n) x) (g x) < 2⁻¹ ^ n
hn_ge : n ≥ max N (k - 1)
⊢ (2 ^ k)⁻¹ * 2 ^ 1 = ∞ → 2 ^ n ≠ 0

case h₂
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg
S : ℕ → Set α := fun k ↦ {x | 2⁻¹ ^ k ≤ edist (f (ns k) x) (g x)}
hμS_le : ∀ (k : ℕ), μ (S k) ≤ 2⁻¹ ^ k
s : Set α := limsup S atTop
hs : s = limsup S atTop
hμs : μ s = 0
x : α
ε : ℝ≥0∞
hε : ε > 0
N k : ℕ
hk_lt_ε : 2 * 2⁻¹ ^ k < ε
n : ℕ
hNx : edist (f (ns n) x) (g x) < 2⁻¹ ^ n
hn_ge : n ≥ max N (k - 1)
⊢ 2 ^ n = ∞ → (2 ^ k)⁻¹ * 2 ^ 1 ≠ 0
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
hg : LipschitzWith c g
g0 : g 0 = 0
f : ↥(Lp E p μ)
⊢ AEEqFun.comp g ⋯ ↑f ∈ Lp F p μ

Tactic:
Lp.mem_Lp_iff_memLp

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
hg : LipschitzWith c g
g0 : g 0 = 0
f : ↥(Lp E p μ)
⊢ MemLp (↑(AEEqFun.comp g ⋯ ↑f)) p μ
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
f : ↥(Lp ℝ p μ)
a✝ : α
h₁ : ↑↑(posPart (-f)) a✝ = max (↑↑(-f) a✝) 0
h₂ : ↑↑(-f) a✝ = (-↑↑f) a✝
⊢ ↑↑(posPart (-f)) a✝ = max (-↑↑f a✝) 0

Tactic:
h₁,

Goal state after:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
f : ↥(Lp ℝ p μ)
a✝ : α
h₁ : ↑↑(posPart (-f)) a✝ = max (↑↑(-f) a✝) 0
h₂ : ↑↑(-f) a✝ = (-↑↑f) a✝
⊢ max (↑↑(-f) a✝) 0 = max (-↑↑f a✝) 0
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
g : MultilinearMap R M₁ M₂
hg : Continuous g.toFun
h : { toMultilinearMap := f, cont := hf }.toMultilinearMap = { toMultilinearMap := g, cont := hg }.toMultilinearMap
⊢ { toMultilinearMap := f, cont := hf } = { toMultilinearMap := g, cont := hg }

Tactic:
subst h; rfl

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ˣ
a✝ : Nontrivial R
t : R
ht : dist t 0 < ‖↑x⁻¹‖⁻¹
⊢ (↑x + t)⁻¹ʳ = (1 + ↑x⁻¹ * t)⁻¹ʳ * ↑x⁻¹

Tactic:
rw [dist_zero_right] at ht

Goal state after:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
a✝ : Nontrivial R
t : R
ht : ‖t‖ < ‖↑x⁻¹‖⁻¹
⊢ (↑x + t)⁻¹ʳ = (1 + ↑x⁻¹ * t)⁻¹ʳ * ↑x⁻¹
Module: Mathlib.Analysis.Normed.Ring.Units

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
⊢ ∀ᶠ (t : R) in 𝓝 0, (↑x + t)⁻¹ʳ = (1 + ↑x⁻¹ * t)⁻¹ʳ * ↑x⁻¹

Tactic:
nontriviality R
  rw [Metric.eventually_nhds_iff]
  refine ⟨‖(↑x⁻¹ : R)‖⁻¹, by cancel_denoms, fun t ht ↦ ?_⟩
  rw [dist_zero_right] at ht
  rw [← x.val_add t ht, inverse_unit, Units.add, Units.copy_eq, mul_inv_rev, Units.val_mul,
    ← inverse_unit, Units.val_oneSub, sub_neg_eq_add]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
t : R
ht : dist t 0 < 2⁻¹
⊢ ‖(1 - t)⁻¹ʳ‖ ≤ (‖1‖ + 1) * ‖1‖

Tactic:
rw [dist_zero_right] at ht

Goal state after:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
t : R
ht : ‖t‖ < 2⁻¹
⊢ ‖(1 - t)⁻¹ʳ‖ ≤ (‖1‖ + 1) * ‖1‖
Module: Mathlib.Analysis.Normed.Ring.Units

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
t : R
ht : ‖t‖ < 2⁻¹
ht' : ‖t‖ < 1
⊢ ‖(1 - t)⁻¹ʳ‖ ≤ (‖1‖ + 1) * ‖1‖

Tactic:
simp only [inverse_one_sub t ht', norm_one, mul_one]

Goal state after:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
t : R
ht : ‖t‖ < 2⁻¹
ht' : ‖t‖ < 1
⊢ ‖↑(Units.oneSub t ht')⁻¹‖ ≤ ‖1‖ + 1
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:
· simp [hx]

Goal state after:
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.Topology.Algebra.Module.Multilinear.Topology

Goal state before:
pp: 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)}

Tactic:
rintro ⟨f, rfl⟩
    exact ⟨f.cont, f.map_update_add, f.map_update_smul⟩

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

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
h : μ s₂ ≠ ∞
⊢ μ.real s₁ ≤ μ.real s₂ + μ.real (s₁ \ s₂)

Tactic:
calc
    μ.real s₁ ≤ μ.real (s₂ ∪ s₁) := measureReal_le_measureReal_union_right h
    _ = μ.real (s₂ ∪ s₁ \ s₂) := congr_arg μ.real union_sdiff_self.symm
    _ ≤ μ.real s₂ + μ.real (s₁ \ s₂) := measureReal_union_le _ _

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
c : E
t : Set α
ht : MeasurableSet t
hμt : μ t ≠ ∞
⊢ edist (indicatorConstLp p hs hμs c) (indicatorConstLp p ht hμt c) = ‖indicatorConstLp p ⋯ ⋯ c‖ₑ

Tactic:
unfold indicatorConstLp
  rw [Lp.edist_toLp_toLp, eLpNorm_indicator_sub_indicator, Lp.enorm_toLp]

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 ι
inst✝ : DecidableEq ι
f : MultilinearMap 𝕜 E G
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i, ‖m i‖
m₁ m₂ : (i : ι) → E i
i : ι
s : Finset ι
his : i ∉ s
Hrec : ‖f m₁ - f (s.piecewise m₂ m₁)‖ ≤ C * ∑ i ∈ s, ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
A : (insert i s).piecewise m₂ m₁ = update (s.piecewise m₂ m₁) i (m₂ i)
⊢ ‖f (s.piecewise m₂ m₁) - f ((insert i s).piecewise m₂ m₁)‖ ≤
    C * ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖

Tactic:
have B : s.piecewise m₂ m₁ = Function.update (s.piecewise m₂ m₁) i (m₁ i) := by
          simp [his]

Goal state after:
𝕜 : 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 ι
inst✝ : DecidableEq ι
f : MultilinearMap 𝕜 E G
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i, ‖m i‖
m₁ m₂ : (i : ι) → E i
i : ι
s : Finset ι
his : i ∉ s
Hrec : ‖f m₁ - f (s.piecewise m₂ m₁)‖ ≤ C * ∑ i ∈ s, ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
A : (insert i s).piecewise m₂ m₁ = update (s.piecewise m₂ m₁) i (m₂ i)
B : s.piecewise m₂ m₁ = update (s.piecewise m₂ m₁) i (m₁ i)
⊢ ‖f (s.piecewise m₂ m₁) - f ((insert i s).piecewise m₂ m₁)‖ ≤
    C * ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup β
inst✝ : MeasurableSingletonClass α
f : α → β
hs : Summable fun x ↦ ‖f x‖
hs' : (Function.support f).Countable
this✝ : MeasurableSpace β := borel β
this : BorelSpace β
⊢ IsSeparable (f '' univ)

Tactic:
suffices f '' univ ⊆ (f '' f.support) ∪ {0} from
      (((hs'.image f).union (countable_singleton 0)).mono this).isSeparable

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup β
inst✝ : MeasurableSingletonClass α
f : α → β
hs : Summable fun x ↦ ‖f x‖
hs' : (Function.support f).Countable
this✝ : MeasurableSpace β := borel β
this : BorelSpace β
⊢ f '' univ ⊆ f '' Function.support f ∪ {0}
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: 𝕜 : Type u
G : Type wG
G' : Type wG'
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : SeminormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
k n : ℕ
f : MultilinearMap 𝕜 (fun x ↦ G) G'
s : Finset (Fin n)
hk : #s = k
z : G
C : ℝ
H : ∀ (m : Fin n → G), ‖f m‖ ≤ C * ∏ i, ‖m i‖
v : Fin k → G
⊢ ‖(f.restr s hk z) v‖ ≤ C * ‖z‖ ^ (n - k) * ∏ i, ‖v i‖

Tactic:
mul_right_comm,

Goal state after:
𝕜 : Type u
G : Type wG
G' : Type wG'
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : SeminormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
k n : ℕ
f : MultilinearMap 𝕜 (fun x ↦ G) G'
s : Finset (Fin n)
hk : #s = k
z : G
C : ℝ
H : ∀ (m : Fin n → G), ‖f m‖ ≤ C * ∏ i, ‖m i‖
v : Fin k → G
⊢ ‖(f.restr s hk z) v‖ ≤ (C * ∏ i, ‖v i‖) * ‖z‖ ^ (n - k)
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
⊢ ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n.succ A‖ ≤ 1

Tactic:
by
  refine opNorm_le_bound zero_le_one fun m => ?_
  simp only [ContinuousMultilinearMap.mkPiAlgebraFin_apply, one_mul, List.ofFn_eq_map,
    Fin.prod_univ_def]
  refine (List.norm_prod_le' ?_).trans_eq ?_
  · rw [Ne, List.map_eq_nil_iff, List.finRange_eq_nil_iff]
    exact Nat.succ_ne_zero _
  rw [List.map_map, Function.comp_def]

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 : α
ha : μ {a} ≠ ∞
ha' : ‖f a‖ₑ ≠ ∞
hb : μ {b} ≠ ∞
hb' : ‖f b‖ₑ ≠ ∞
⊢ IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ioo a b) μ

Tactic:
by
  rw [integrableOn_Icc_iff_integrableOn_Ioc' ha ha', integrableOn_Ioc_iff_integrableOn_Ioo' hb hb']

Goal state after:
Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α →ₘ[μ] β
⊢ MemLp (↑f) 1 μ ↔ f ∈ Lp β 1 μ

Tactic:
Lp.mem_Lp_iff_memLp

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α →ₘ[μ] β
⊢ MemLp (↑f) 1 μ ↔ MemLp (↑f) 1 μ
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: 𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E' : ι' → Type wE'
G : Type wG
inst✝⁸ : Fintype ι'
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁴ : SeminormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
inst✝² : Fintype ι
inst✝¹ : (i : ι') → SeminormedAddCommGroup (E' i)
inst✝ : (i : ι') → NormedSpace 𝕜 (E' i)
f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G)
C : ℝ
H : ∀ (m₁ : (i : ι) → E i) (m₂ : (i : ι') → E' i), ‖(f m₁) m₂‖ ≤ (C * ∏ i, ‖m₁ i‖) * ∏ i, ‖m₂ i‖
⊢ ‖f.mkContinuousMultilinear C H‖ ≤ max C 0

Tactic:
dsimp only [mkContinuousMultilinear]
  exact mkContinuous_norm_le _ (le_max_right _ _) _

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

Goal state before:
pp: β : Type u_2
inst✝¹ : MeasurableSpace β
p : ℝ≥0∞
E : Type u_7
inst✝ : NormedAddCommGroup E
f : β → E
μ : Measure β
hf : MemLp f p μ
hp_ne_top : p ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ g, eLpNorm (f - ⇑g) p μ < ε ∧ MemLp (⇑g) p μ

Tactic:
borelize E
  let f' := hf.1.mk f
  rsuffices ⟨g, hg, g_mem⟩ : ∃ g : β →ₛ E, eLpNorm (f' - ⇑g) p μ < ε ∧ MemLp g p μ
  · refine ⟨g, ?_, g_mem⟩
    suffices eLpNorm (f - ⇑g) p μ = eLpNorm (f' - ⇑g) p μ by rwa [this]
    apply eLpNorm_congr_ae
    filter_upwards [hf.1.ae_eq_mk] with x hx
    simpa only [Pi.sub_apply, sub_left_inj] using hx
  have hf' : MemLp f' p μ := hf.ae_eq hf.1.ae_eq_mk
  have f'meas : Measurable f' := hf.1.measurable_mk
  have : SeparableSpace (range f' ∪ {0} : Set E) :=
    StronglyMeasurable.separableSpace_range_union_singleton hf.1.stronglyMeasurable_mk
  rcases ((tendsto_approxOn_range_Lp_eLpNorm hp_ne_top f'meas hf'.2).eventually <|
    gt_mem_nhds hε.bot_lt).exists with ⟨n, hn⟩
  rw [← eLpNorm_neg, neg_sub] at hn
  exact ⟨_, hn, memLp_approxOn_range f'meas hf' _⟩

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_6
x✝ : MeasurableSpace β
ν : Measure β
f g : α → β → G
h : ∀ᵐ (a : α) ∂μ, f a =ᵐ[ν] g a
⊢ ∫ (a : α), ∫ (b : β), f a b ∂ν ∂μ = ∫ (a : α), ∫ (b : β), g a b ∂ν ∂μ

Tactic:
by
  apply integral_congr_ae
  filter_upwards [h] with _ ha
  apply integral_congr_ae
  filter_upwards [ha] with _ hb using hb

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
a✝ : α
h₁ : ↑↑(Lp.posPart f₁) a✝ = max (↑↑f₁ a✝) 0
h₂ : ↑↑(Integrable.toL1 f hf) a✝ = f a✝
⊢ ENNReal.ofReal (f a✝) = ‖↑↑(Lp.posPart f₁) a✝‖ₑ

Tactic:
h₁,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
a✝ : α
h₁ : ↑↑(Lp.posPart f₁) a✝ = max (↑↑f₁ a✝) 0
h₂ : ↑↑(Integrable.toL1 f hf) a✝ = f a✝
⊢ ENNReal.ofReal (f a✝) = ‖max (↑↑f₁ a✝) 0‖ₑ
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
eq₁ : (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal = ‖Lp.posPart f₁‖
a✝ : α
h₁ : ↑↑(Lp.negPart f₁) a✝ = -min (↑↑f₁ a✝) 0
h₂ : ↑↑(Integrable.toL1 f hf) a✝ = f a✝
⊢ ENNReal.ofReal (-f a✝) = ‖↑↑(Lp.negPart f₁) a✝‖ₑ

Tactic:
h₁,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
eq₁ : (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal = ‖Lp.posPart f₁‖
a✝ : α
h₁ : ↑↑(Lp.negPart f₁) a✝ = -min (↑↑f₁ a✝) 0
h₂ : ↑↑(Integrable.toL1 f hf) a✝ = f a✝
⊢ ENNReal.ofReal (-f a✝) = ‖-min (↑↑f₁ a✝) 0‖ₑ
Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv

Goal state before:
pp: k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst✝¹⁶ : Ring k
inst✝¹⁵ : AddCommGroup V₁
inst✝¹⁴ : Module k V₁
inst✝¹³ : AddTorsor V₁ P₁
inst✝¹² : TopologicalSpace P₁
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : Module k V₂
inst✝⁹ : AddTorsor V₂ P₂
inst✝⁸ : TopologicalSpace P₂
inst✝⁷ : AddCommGroup V₃
inst✝⁶ : Module k V₃
inst✝⁵ : AddTorsor V₃ P₃
inst✝⁴ : TopologicalSpace P₃
inst✝³ : AddCommGroup V₄
inst✝² : Module k V₄
inst✝¹ : AddTorsor V₄ P₄
inst✝ : TopologicalSpace P₄
e₁ : P₁ ≃ᴬ[k] P₂
e₂ : P₃ ≃ᴬ[k] P₄
⊢ Continuous ((↑e₁).prodCongr ↑e₂).toFun

Tactic:
by eta_expand; dsimp; fun_prop

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

Goal state before:
pp: k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst✝¹⁶ : Ring k
inst✝¹⁵ : AddCommGroup V₁
inst✝¹⁴ : Module k V₁
inst✝¹³ : AddTorsor V₁ P₁
inst✝¹² : TopologicalSpace P₁
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : Module k V₂
inst✝⁹ : AddTorsor V₂ P₂
inst✝⁸ : TopologicalSpace P₂
inst✝⁷ : AddCommGroup V₃
inst✝⁶ : Module k V₃
inst✝⁵ : AddTorsor V₃ P₃
inst✝⁴ : TopologicalSpace P₃
inst✝³ : AddCommGroup V₄
inst✝² : Module k V₄
inst✝¹ : AddTorsor V₄ P₄
inst✝ : TopologicalSpace P₄
e₁ : P₁ ≃ᴬ[k] P₂
e₂ : P₃ ≃ᴬ[k] P₄
⊢ Continuous ((↑e₁).prodCongr ↑e₂).invFun

Tactic:
by eta_expand; dsimp; fun_prop

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

Goal state before:
pp: k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst✝¹⁶ : Ring k
inst✝¹⁵ : AddCommGroup V₁
inst✝¹⁴ : Module k V₁
inst✝¹³ : AddTorsor V₁ P₁
inst✝¹² : TopologicalSpace P₁
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : Module k V₂
inst✝⁹ : AddTorsor V₂ P₂
inst✝⁸ : TopologicalSpace P₂
inst✝⁷ : AddCommGroup V₃
inst✝⁶ : Module k V₃
inst✝⁵ : AddTorsor V₃ P₃
inst✝⁴ : TopologicalSpace P₃
inst✝³ : AddCommGroup V₄
inst✝² : Module k V₄
inst✝¹ : AddTorsor V₄ P₄
inst✝ : TopologicalSpace P₄
⊢ Continuous (AffineEquiv.prodAssoc k P₁ P₂ P₃).toFun

Tactic:
by eta_expand; dsimp; fun_prop

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

Goal state before:
pp: k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst✝¹⁶ : Ring k
inst✝¹⁵ : AddCommGroup V₁
inst✝¹⁴ : Module k V₁
inst✝¹³ : AddTorsor V₁ P₁
inst✝¹² : TopologicalSpace P₁
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : Module k V₂
inst✝⁹ : AddTorsor V₂ P₂
inst✝⁸ : TopologicalSpace P₂
inst✝⁷ : AddCommGroup V₃
inst✝⁶ : Module k V₃
inst✝⁵ : AddTorsor V₃ P₃
inst✝⁴ : TopologicalSpace P₃
inst✝³ : AddCommGroup V₄
inst✝² : Module k V₄
inst✝¹ : AddTorsor V₄ P₄
inst✝ : TopologicalSpace P₄
⊢ Continuous (AffineEquiv.prodAssoc k P₁ P₂ P₃).invFun

Tactic:
by eta_expand; dsimp; fun_prop

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

Goal state before:
pp: R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module R V
inst✝⁹ : TopologicalSpace P
inst✝⁸ : AddTorsor V P
inst✝⁷ : AddCommGroup W
inst✝⁶ : Module R W
inst✝⁵ : TopologicalSpace Q
inst✝⁴ : AddTorsor W Q
inst✝³ : TopologicalSpace V
inst✝² : IsTopologicalAddTorsor P
inst✝¹ : TopologicalSpace W
inst✝ : IsTopologicalAddTorsor Q
f : P →ᴬ[R] Q
h₁ : f.contLinear = 0 ↔ (↑f).linear = 0
h₂ : ∀ (q : Q), f = const R P q ↔ ↑f = AffineMap.const R P q
⊢ f.contLinear = 0 ↔ ∃ q, f = const R P q

Tactic:
h₁,

Goal state after:
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module R V
inst✝⁹ : TopologicalSpace P
inst✝⁸ : AddTorsor V P
inst✝⁷ : AddCommGroup W
inst✝⁶ : Module R W
inst✝⁵ : TopologicalSpace Q
inst✝⁴ : AddTorsor W Q
inst✝³ : TopologicalSpace V
inst✝² : IsTopologicalAddTorsor P
inst✝¹ : TopologicalSpace W
inst✝ : IsTopologicalAddTorsor Q
f : P →ᴬ[R] Q
h₁ : f.contLinear = 0 ↔ (↑f).linear = 0
h₂ : ∀ (q : Q), f = const R P q ↔ ↑f = AffineMap.const R P q
⊢ (↑f).linear = 0 ↔ ∃ q, f = const R P q
Module: Mathlib.Topology.Algebra.ContinuousAffineMap

Goal state before:
pp: R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝²⁹ : Ring R
inst✝²⁸ : AddCommGroup V
inst✝²⁷ : Module R V
inst✝²⁶ : TopologicalSpace P
inst✝²⁵ : AddTorsor V P
inst✝²⁴ : AddCommGroup W
inst✝²³ : Module R W
inst✝²² : TopologicalSpace Q
inst✝²¹ : AddTorsor W Q
W₂ : Type u_6
Q₂ : Type u_7
W₃ : Type u_8
Q₃ : Type u_9
inst✝²⁰ : AddCommGroup W₂
inst✝¹⁹ : Module R W₂
inst✝¹⁸ : TopologicalSpace Q₂
inst✝¹⁷ : AddTorsor W₂ Q₂
k : Type u_10
P₁ : Type u_11
P₂ : Type u_12
P₃ : Type u_13
P₄ : Type u_14
V₁ : Type u_15
V₂ : Type u_16
V₃ : Type u_17
V₄ : Type u_18
inst✝¹⁶ : Ring k
inst✝¹⁵ : AddCommGroup V₁
inst✝¹⁴ : Module k V₁
inst✝¹³ : AddTorsor V₁ P₁
inst✝¹² : TopologicalSpace P₁
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : Module k V₂
inst✝⁹ : AddTorsor V₂ P₂
inst✝⁸ : TopologicalSpace P₂
inst✝⁷ : AddCommGroup V₃
inst✝⁶ : Module k V₃
inst✝⁵ : AddTorsor V₃ P₃
inst✝⁴ : TopologicalSpace P₃
inst✝³ : AddCommGroup V₄
inst✝² : Module k V₄
inst✝¹ : AddTorsor V₄ P₄
inst✝ : TopologicalSpace P₄
f : P₁ →ᴬ[k] P₂
g : P₁ →ᴬ[k] P₃
⊢ Continuous ((↑f).prod ↑g).toFun

Tactic:
by eta_expand; dsimp; fun_prop

Goal state after: