mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.MeasurableSpace.Pi

Goal state before:
pp: case intro.a
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
i : ι
⊢ generateFrom ((preimage fun b ↦ b i) '' C i) ≤ generateFrom (univ.pi '' univ.pi C)

Tactic:
apply generateFrom_le

Goal state after:
case intro.a
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
i : ι
⊢ ∀ t ∈ (preimage fun b ↦ b i) '' C i, MeasurableSet t
Module: Mathlib.Topology.ContinuousMap.Algebra

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : TopologicalSpace α
𝕜 : Type u_5
inst✝² : TopologicalSpace 𝕜
inst✝¹ : Field 𝕜
inst✝ : IsTopologicalRing 𝕜
s : Subalgebra 𝕜 C(α, 𝕜)
h : s.SeparatesPoints
v : α → 𝕜
x y : α
n : x = y
⊢ ∃ f ∈ ↑s, f x = v x ∧ f y = v y

pp: case neg
α : Type u_1
inst✝³ : TopologicalSpace α
𝕜 : Type u_5
inst✝² : TopologicalSpace 𝕜
inst✝¹ : Field 𝕜
inst✝ : IsTopologicalRing 𝕜
s : Subalgebra 𝕜 C(α, 𝕜)
h : s.SeparatesPoints
v : α → 𝕜
x y : α
n : ¬x = y
⊢ ∃ f ∈ ↑s, f x = v x ∧ f y = v y

Tactic:
· subst n
    exact ⟨_, (v x • (1 : s) : s).prop, mul_one _, mul_one _⟩

Goal state after:
case neg
α : Type u_1
inst✝³ : TopologicalSpace α
𝕜 : Type u_5
inst✝² : TopologicalSpace 𝕜
inst✝¹ : Field 𝕜
inst✝ : IsTopologicalRing 𝕜
s : Subalgebra 𝕜 C(α, 𝕜)
h : s.SeparatesPoints
v : α → 𝕜
x y : α
n : ¬x = y
⊢ ∃ f ∈ ↑s, f x = v x ∧ f y = v y
Module: Mathlib.MeasureTheory.MeasurableSpace.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set (α i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), ⋃ n, t i n = univ
x✝ : (i : ι) → α i
⊢ ∀ (a : ι), x✝ a ∈ update (fun i' ↦ iUnion (t i')) i (⋃ x, s) a ↔ x✝ a ∈ ⋃ j, update (fun i' ↦ t i' j) i s a

Tactic:
intro i'

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set (α i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), ⋃ n, t i n = univ
x✝ : (i : ι) → α i
i' : ι
⊢ x✝ i' ∈ update (fun i' ↦ iUnion (t i')) i (⋃ x, s) i' ↔ x✝ i' ∈ ⋃ j, update (fun i' ↦ t i' j) i s i'
Module: Mathlib.Topology.ContinuousMap.Algebra

Goal state before:
pp: α : Type u_1
inst✝⁸ : TopologicalSpace α
R : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : TopologicalSpace R
M : Type u_3
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : ContinuousSMul R M
inst✝¹ : IsTopologicalSemiring R
inst✝ : ContinuousAdd M
r : C(α, R)
⊢ r • 0 = 0

Tactic:
ext x; exact smul_zero _

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Pi

Goal state before:
pp: case a
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
⊢ generateFrom (univ.pi '' univ.pi C) ≤ MeasurableSpace.pi

Tactic:
apply generateFrom_le

Goal state after:
case a
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
⊢ ∀ t ∈ univ.pi '' univ.pi C, MeasurableSet t
Module: Mathlib.Probability.UniformOn

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s u t : Set Ω
hs : s.Finite
| (uniformOn s) t

Tactic:
rw [(by simp : s = s ∩ u ∪ s ∩ uᶜ),
      ← uniformOn_disjoint_union (hs.inter_of_left _) (hs.inter_of_left _)
      (disjoint_compl_right.mono inf_le_right inf_le_right)]

Goal state after:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s u t : Set Ω
hs : s.Finite
| (uniformOn (s ∩ u)) t * (uniformOn (s ∩ u ∪ s ∩ uᶜ)) (s ∩ u) +
    (uniformOn (s ∩ uᶜ)) t * (uniformOn (s ∩ u ∪ s ∩ uᶜ)) (s ∩ uᶜ)
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
γ : Type u_3
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace γ
inst✝¹ : CommMonoid γ
inst✝ : ContinuousMul γ
ι : Type u_5
s : Finset ι
f : ι → α →ₘ[μ] γ
⊢ ↑(∏ i ∈ s, f i) =ᵐ[μ] fun x ↦ ∏ i ∈ s, ↑(f i) x

Tactic:
by
  grw [coeFn_finsetProd]
  filter_upwards with x using by simp

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
β : Type u_5
inst✝⁴ : TopologicalSpace β
inst✝³ : Lattice β
inst✝² : TopologicalLattice β
inst✝¹ : AddGroup β
inst✝ : IsTopologicalAddGroup β
f : α →ₘ[μ] β
x : α
hx_sup : ↑(f ⊔ -f) x = ↑f x ⊔ ↑(-f) x
⊢ ↑(-f) x = (-↑f) x → ↑(f ⊔ -f) x = ↑f x ⊔ -↑f x

Tactic:
hx_neg

Goal state after:
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
β : Type u_5
inst✝⁴ : TopologicalSpace β
inst✝³ : Lattice β
inst✝² : TopologicalLattice β
inst✝¹ : AddGroup β
inst✝ : IsTopologicalAddGroup β
f : α →ₘ[μ] β
x : α
hx_sup : ↑(f ⊔ -f) x = ↑f x ⊔ ↑(-f) x
hx_neg : ↑(-f) x = (-↑f) x
⊢ ↑(f ⊔ -f) x = ↑f x ⊔ -↑f x
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
i : ι
s : Set (α i)
hs : MeasurableSet s
h2s : (μ i) s = 0
⊢ (map (eval i) (Measure.pi μ)) s = 0

Tactic:
rw [map_apply (by fun_prop) hs, pi_eval_preimage_null μ h2s]

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
i : ι
⊢ QuasiMeasurePreserving (eval i) (Measure.pi μ) (μ i)

Tactic:
refine ⟨by fun_prop, AbsolutelyContinuous.mk fun s hs h2s => ?_⟩
  rw [map_apply (by fun_prop) hs, pi_eval_preimage_null μ h2s]

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝⁴ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝³ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝² : ∀ (i : ι), SigmaFinite (μ i)
inst✝¹ : (i : ι) → TopologicalSpace (α i)
inst✝ : ∀ (i : ι), IsFiniteMeasureOnCompacts (μ i)
K : Set ((i : ι) → α i)
hK : IsCompact K
⊢ (Measure.pi μ) K < ∞

Tactic:
suffices Measure.pi μ (Set.univ.pi fun j => Function.eval j '' K) < ⊤ by
    exact lt_of_le_of_lt (measure_mono (univ.subset_pi_eval_image K)) this

Goal state after:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝⁴ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝³ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝² : ∀ (i : ι), SigmaFinite (μ i)
inst✝¹ : (i : ι) → TopologicalSpace (α i)
inst✝ : ∀ (i : ι), IsFiniteMeasureOnCompacts (μ i)
K : Set ((i : ι) → α i)
hK : IsCompact K
⊢ (Measure.pi μ) (univ.pi fun j ↦ eval j '' K) < ∞
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst✝³ : TopologicalSpace ε'
inst✝² : ContinuousENorm ε'
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ≥0∞
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
⊢ eLpNorm f p μ ≤ c * eLpNorm g p μ

Tactic:
by_cases h₀ : p = 0
  · simp [h₀]
  simp only [eLpNorm, h₀, ↓reduceIte, mul_ite]
  by_cases hp' : p = ⊤
  · simpa [hp'] using eLpNormEssSup_le_nnreal_smul_eLpNormEssSup_of_ae_le_mul' h
  · simpa [hp'] using eLpNorm'_le_mul_eLpNorm'_of_ae_le_mul hg h (ENNReal.toReal_pos h₀ hp')

Goal state after:
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: p q r : ℝ≥0∞
hp : 0 < p.toNNReal
hq : 0 < q.toNNReal
⊢ p.toNNReal.HolderTriple q.toNNReal r.toNNReal ↔ p.HolderTriple q r

Tactic:
simp_rw [← NNReal.holderTriple_coe_iff, coe_toNNReal_eq_toReal]
  apply toReal_iff r ?_ ?_
  all_goals simpa [← coe_toNNReal_eq_toReal]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
μ ν : Measure α
p : ℝ≥0∞
⊢ eLpNorm f p μ ≤ eLpNorm f p (μ + ν)

Tactic:
← Measure.le_add_right le_rfl

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
μ ν : Measure α
p : ℝ≥0∞
⊢ eLpNorm f p μ ≤ eLpNorm f p μ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: E : Type u_4
inst✝³ : NormedAddCommGroup E
X : Type u_7
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
f : X → E
hf : Continuous[inst✝², PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h'f : HasCompactSupport f
μ : Measure X
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
⊢ MemLp f ∞ μ

Tactic:
rcases hf.bounded_above_of_compact_support h'f with ⟨C, hC⟩

Goal state after:
E : Type u_4
inst✝³ : NormedAddCommGroup E
X : Type u_7
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
f : X → E
hf : Continuous[inst✝², PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h'f : HasCompactSupport f
μ : Measure X
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
C : ℝ
hC : ∀ (x : X), ‖f x‖ ≤ C
⊢ MemLp f ∞ μ
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case e'_3.inl
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ i ∈ s, w i = 1
hz✝ : ∀ i ∈ s, 0 ≤ z i
A : ∀ i ∈ s, z i = 0 → w i = 0
this : ∏ x ∈ s, rexp (log (z x) * w x) ≤ ∑ x ∈ s, w x * rexp (log (z x))
i : ι
hi : i ∈ s
hz : 0 = z i
⊢ z i ^ w i = rexp (log (z i) * w i)

Tactic:
simp [A i hi hz.symm]

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case e'_4.inl
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ i ∈ s, w i = 1
hz✝ : ∀ i ∈ s, 0 ≤ z i
A : ∀ i ∈ s, z i = 0 → w i = 0
this : ∏ x ∈ s, rexp (log (z x) * w x) ≤ ∑ x ∈ s, w x * rexp (log (z x))
i : ι
hi : i ∈ s
hz : 0 = z i
⊢ w i * z i = w i * rexp (log (z i))

Tactic:
simp [A i hi hz.symm]

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

Goal state before:
pp: case pos
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
p q : ℝ
hp0_lt : 0 < p
hpq : p ≤ q
hf : AEStronglyMeasurable f μ
hq0_lt : 0 < q
hpq_eq : p = q
⊢ eLpNorm' f p μ ≤ eLpNorm' f q μ * μ Set.univ ^ (1 / p - 1 / q)

Tactic:
rw [hpq_eq, sub_self, ENNReal.rpow_zero, mul_one]

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 : ℝ≥0∞
inst✝ : IsFiniteMeasure μ
hfq : MemLp f q μ
hpq : p ≤ q
⊢ MemLp f p μ

Tactic:
by
  obtain ⟨hfq_m, hfq_lt_top⟩ := hfq
  by_cases hp0 : p = 0
  · rwa [hp0, memLp_zero_iff_aestronglyMeasurable]
  rw [← Ne] at hp0
  refine ⟨hfq_m, ?_⟩
  by_cases hp_top : p = ∞
  · have hq_top : q = ∞ := by rwa [hp_top, top_le_iff] at hpq
    rw [hp_top]
    rwa [hq_top] at hfq_lt_top
  have hp_pos : 0 < p.toReal := ENNReal.toReal_pos hp0 hp_top
  by_cases hq_top : q = ∞
  · rw [eLpNorm_eq_eLpNorm' hp0 hp_top]
    rw [hq_top, eLpNorm_exponent_top] at hfq_lt_top
    refine lt_of_le_of_lt (eLpNorm'_le_eLpNormEssSup_mul_rpow_measure_univ hp_pos) ?_
    refine ENNReal.mul_lt_top hfq_lt_top ?_
    exact ENNReal.rpow_lt_top_of_nonneg (by simp [hp_pos.le]) (by finiteness)
  have hq0 : q ≠ 0 := by
    by_contra hq_eq_zero
    obtain rfl : p = 0 := le_antisymm (by rwa [hq_eq_zero] at hpq) zero_le
    rw [ENNReal.toReal_zero] at hp_pos
    exact (lt_irrefl _) hp_pos
  have hpq_real : p.toReal ≤ q.toReal := ENNReal.toReal_mono hq_top hpq
  rw [eLpNorm_eq_eLpNorm' hp0 hp_top]
  rw [eLpNorm_eq_eLpNorm' hq0 hq_top] at hfq_lt_top
  exact eLpNorm'_lt_top_of_eLpNorm'_lt_top_of_exponent_le hfq_m hfq_lt_top hp_pos.le hpq_real

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

Goal state before:
pp: α : 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
hf : AEStronglyMeasurable f μ
g : α → F
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
⊢ ∀ᵐ (x : α) ∂μ, ‖flip b (g x) (f x)‖₊ ≤ c * ‖g x‖₊ * ‖f x‖₊

Tactic:
by
        convert! h using 3 with x
        simp only [mul_assoc, mul_comm ‖f x‖₊]

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
h_add_zero : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ 0
h_add_top : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ ∞
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≠ 0

Tactic:
simp [h_add_zero, h_add_top, -Pi.add_apply]

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

Goal state before:
pp: case neg
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), Measurable fun a ↦ edist (f n a) (g a)
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : 0 < ε
δ : ℝ≥0∞
hδ : δ > 0
hδi : ¬δ = ∞
⊢ ∃ N, ∀ n ≥ N, μ {x | ε ≤ edist (f n x) (g x)} ≤ δ

Tactic:
lift δ to ℝ≥0 using hδi

Goal state after:
case neg
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), Measurable fun a ↦ edist (f n a) (g a)
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : 0 < ε
δ : ℝ≥0
hδ : ↑δ > 0
⊢ ∃ N, ∀ n ≥ N, μ {x | ε ≤ edist (f n x) (g x)} ≤ ↑δ
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
⊢ ∑' (a : ℕ), 2⁻¹ ^ a ≠ ∞

Tactic:
simpa only [ENNReal.tsum_geometric, ENNReal.one_sub_inv_two, inv_inv] using ENNReal.ofNat_ne_top

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : { f // Disjoint (Set.range ⇑f.1) (Set.range ⇑f.2) }
f : α ↪ γ
g : β ↪ γ
disj : Disjoint (Set.range ⇑(f, g).1) (Set.range ⇑(f, g).2)
⊢ Function.Injective fun x ↦
    match x with
    | Sum.inl a => f a
    | Sum.inr b => g b

Tactic:
rintro (a₁ | b₁) (a₂ | b₂) f_eq <;>
        simp only at f_eq

Goal state after:
case inl.inl
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : { f // Disjoint (Set.range ⇑f.1) (Set.range ⇑f.2) }
f : α ↪ γ
g : β ↪ γ
disj : Disjoint (Set.range ⇑(f, g).1) (Set.range ⇑(f, g).2)
a₁ a₂ : α
f_eq : f a₁ = f a₂
⊢ Sum.inl a₁ = Sum.inl a₂

case inl.inr
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : { f // Disjoint (Set.range ⇑f.1) (Set.range ⇑f.2) }
f : α ↪ γ
g : β ↪ γ
disj : Disjoint (Set.range ⇑(f, g).1) (Set.range ⇑(f, g).2)
a₁ : α
b₂ : β
f_eq : f a₁ = g b₂
⊢ Sum.inl a₁ = Sum.inr b₂

case inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : { f // Disjoint (Set.range ⇑f.1) (Set.range ⇑f.2) }
f : α ↪ γ
g : β ↪ γ
disj : Disjoint (Set.range ⇑(f, g).1) (Set.range ⇑(f, g).2)
b₁ : β
a₂ : α
f_eq : g b₁ = f a₂
⊢ Sum.inr b₁ = Sum.inl a₂

case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : { f // Disjoint (Set.range ⇑f.1) (Set.range ⇑f.2) }
f : α ↪ γ
g : β ↪ γ
disj : Disjoint (Set.range ⇑(f, g).1) (Set.range ⇑(f, g).2)
b₁ b₂ : β
f_eq : g b₁ = g b₂
⊢ Sum.inr b₁ = Sum.inr b₂
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✝ : ContinuousSMul 𝕜 F
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
f : ContinuousMultilinearMap 𝕜 E F
⊢ IsVonNBounded 𝕜 (⇑f '' s)

Tactic:
by
  cases isEmpty_or_nonempty ι with
  | inl h =>
    exact (isBounded_iff_isVonNBounded _).1 <|
      @Set.Finite.isBounded _ (vonNBornology 𝕜 F) _ (s.toFinite.image _)
  | inr h => exact hs.image_multilinear' f

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ˣ
n : ℕ
⊢ (fun x_1 ↦ (-↑x⁻¹ * x_1) ^ n) =O[𝓝 0] fun t ↦ ‖t‖ ^ n

Tactic:
exact ((isBigO_refl _ _).norm_right.const_mul_left _).pow _

Goal state after:
Module: Mathlib.Order.Filter.IndicatorFunction

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : One β
l : Filter α
f : α → β
hf : ∀ᶠ (x : α) in l, f x ≠ 1
s✝ t : Set α
h : s✝.mulIndicator f =ᶠ[l] t.mulIndicator f
s : Set α
⊢ Function.mulSupport (s.mulIndicator f) =ᶠ[l] s

Tactic:
rw [mulSupport_mulIndicator]
    exact (hf.mono fun x hx ↦ and_iff_left hx).set_eq

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
c : E
⊢ c = 0 ∨ μ s ≠ ∞

Tactic:
exact .inr hμs

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
⊢ AEMeasurable f (μ.restrict s)

Tactic:
classical
  nontriviality α; inhabit α
  have : (Set.piecewise s f fun _ => f default) =ᵐ[μ.restrict s] f := piecewise_ae_eq_restrict hs
  refine ⟨Set.piecewise s f fun _ => f default, ?_, this.symm⟩
  apply measurable_of_isOpen
  intro t ht
  obtain ⟨u, u_open, hu⟩ : ∃ u : Set α, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s :=
    _root_.continuousOn_iff'.1 hf t ht
  rw [piecewise_preimage, Set.ite, hu]
  exact (u_open.measurableSet.inter hs).union ((measurable_const ht.measurableSet).diff hs)

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

Goal state before:
pp: X : Type u_1
E : Type u_6
F : Type u_7
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure X
s : Set X
f : X → E
hf : LocallyIntegrableOn f s μ
g : X → F
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : X) ∂μ, ‖g x‖ ≤ ‖f x‖
⊢ LocallyIntegrableOn g s μ

Tactic:
intro x hx
  rcases hf x hx with ⟨t, t_mem, ht⟩
  exact ⟨t, t_mem, Integrable.mono ht hg.restrict (ae_restrict_of_ae h)⟩

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

Goal state before:
pp: X : Type u_1
E : Type u_6
inst✝⁹ : MeasurableSpace X
inst✝⁸ : TopologicalSpace X
inst✝⁷ : NormedAddCommGroup E
μ : Measure X
inst✝⁶ : BorelSpace X
inst✝⁵ : ConditionallyCompleteLinearOrder X
inst✝⁴ : ConditionallyCompleteLinearOrder E
inst✝³ : OrderTopology X
inst✝² : OrderTopology E
inst✝¹ : SecondCountableTopology E
f : X → E
inst✝ : IsLocallyFiniteMeasure μ
hmono : Monotone f
x : X
U : Set X
hU : U ∈ 𝓝 x
h'U : μ U < ∞
a b : X
xab : x ∈ Icc a b
hab : Icc a b ∈ 𝓝 x
abU : Icc a b ⊆ U
ab : a ≤ b
⊢ IntegrableOn f (Icc a b) μ

Tactic:
exact
    (hmono.monotoneOn _).integrableOn_of_measure_ne_top (isLeast_Icc ab) (isGreatest_Icc ab)
      ((measure_mono abU).trans_lt h'U).ne measurableSet_Icc

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
T : Set α → β
inst✝ : AddMonoid β
c : ℝ≥0∞
hc_ne_zero : c ≠ 0
hT : FinMeasAdditive μ T
s : Set α
x✝ : MeasurableSet s
hμs : μ s = ∞
⊢ c ≠ 0 ∧ μ s = ∞ ∨ c = ∞ ∧ μ s ≠ 0

Tactic:
simp only [hc_ne_zero, true_and, Ne, not_false_iff]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
T : Set α → β
inst✝ : AddMonoid β
c : ℝ≥0∞
hc_ne_zero : c ≠ 0
hT : FinMeasAdditive μ T
s : Set α
x✝ : MeasurableSet s
hμs : μ s = ∞
⊢ μ s = ∞ ∨ c = ∞ ∧ ¬μ s = 0
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α →ₛ E
hfi : MemLp (⇑f) p μ
⊢ ⇑(toSimpleFunc (f.toLp hfi)) =ᵐ[μ] ⇑f

Tactic:
by
  rw [← AEEqFun.mk_eq_mk]; exact Classical.choose_spec (toLp f hfi).2

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

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst✝¹ : NormedAddCommGroup G
inst✝ : PartialOrder G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
g : { g // 0 ≤ g }
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
⊢ ∃ x, (∀ (n : ℕ), x n ∈ Set.range (coeSimpleFuncNonnegToLpNonneg p μ G)) ∧ Tendsto x atTop (𝓝 g)

Tactic:
have hg_memLp : MemLp (g : α → G) p μ := Lp.memLp (g : Lp G p μ)

Goal state after:
α : Type u_1
inst✝² : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst✝¹ : NormedAddCommGroup G
inst✝ : PartialOrder G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
g : { g // 0 ≤ g }
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
hg_memLp : MemLp (↑↑↑g) p μ
⊢ ∃ x, (∀ (n : ℕ), x n ∈ Set.range (coeSimpleFuncNonnegToLpNonneg p μ G)) ∧ Tendsto x atTop (𝓝 g)
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedSpace ℝ E
f : α →ₛ E
hf : Integrable (⇑f) μ
⊢ ‖integral μ f‖ ≤ integral μ (map norm f)

Tactic:
refine (norm_setToSimpleFunc_le_integral_norm _ (fun s _ _ => ?_) hf).trans (one_mul _).le
  exact (norm_weightedSMul_le s).trans (one_mul _).symm.le

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

Goal state before:
pp: α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m : MeasurableSpace α
T : Set α → F' →L[ℝ] F
f : α →ₛ F'
⊢ ∑ x ∈ f.range, ‖(T (⇑f ⁻¹' {x})) x‖ ≤ ∑ x ∈ f.range, ‖T (⇑f ⁻¹' {x})‖ * ‖x‖

Tactic:
by
      gcongr with b; apply ContinuousLinearMap.le_opNorm

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 α
X : Type u_6
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
F : X → α → G
x₀ : X
bound : α → ℝ
hF_meas : ∀ᶠ (x : X) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
h_bound : ∀ᶠ (x : X) in 𝓝 x₀, ∀ᵐ (a : α) ∂μ, ‖F x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousAt (fun x ↦ F x a) x₀
⊢ ContinuousAt (fun x ↦ setToFun μ (weightedSMul μ) ⋯ (F x)) x₀

Tactic:
exact continuousAt_setToFun_of_dominated (dominatedFinMeasAdditive_weightedSMul μ)
    hF_meas h_bound bound_integrable h_cont

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

Goal state before:
pp: case neg
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : s.Nonempty
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ 0 ∉ {x}

Tactic:
rw [Set.mem_singleton_iff]

Goal state after:
case neg
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : s.Nonempty
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ ¬0 = x