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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : α → β
hf : Integrable f μ
hg : Integrable g μ
⊢ Integrable (fun a ↦ f a - g a) μ

Tactic:
simpa only [sub_eq_add_neg] using! hf.add hg.neg

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

Goal state before:
pp: case zero
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
inst✝⁷ : CompleteSpace 𝕜
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 : IsEmpty ι
⊢ Continuous[inst✝⁴, Pi.topologicalSpace] ⇑ξ.equivFun

Tactic:
exact continuous_of_const fun x y => funext hn.elim

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
l : Filter α
inst✝ : MeasurableSpace β
e : α → β
he : MeasurableEmbedding e
f : β → ε
⊢ (∃ s ∈ map e l, IntegrableOn (f ∘ e) (e ⁻¹' s) μ) ↔ ∃ s ∈ l, IntegrableOn (f ∘ e) s μ

Tactic:
constructor <;> rintro ⟨s, hs⟩

Goal state after:
case mp
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
l : Filter α
inst✝ : MeasurableSpace β
e : α → β
he : MeasurableEmbedding e
f : β → ε
s : Set β
hs : s ∈ map e l ∧ IntegrableOn (f ∘ e) (e ⁻¹' s) μ
⊢ ∃ s ∈ l, IntegrableOn (f ∘ e) s μ

case mpr
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
l : Filter α
inst✝ : MeasurableSpace β
e : α → β
he : MeasurableEmbedding e
f : β → ε
s : Set α
hs : s ∈ l ∧ IntegrableOn (f ∘ e) s μ
⊢ ∃ s ∈ map e l, IntegrableOn (f ∘ e) (e ⁻¹' s) μ
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
l : Filter α
inst✝ : MeasurableSpace β
e : α → β
he : MeasurableEmbedding e
f : β → ε
μ : Measure β
⊢ (∃ s ∈ map e l, IntegrableOn f s μ) → ∃ s ∈ map e l, IntegrableOn f s (μ.restrict (range e))

Tactic:
rintro ⟨s, hs, int⟩

Goal state after:
case mp
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
l : Filter α
inst✝ : MeasurableSpace β
e : α → β
he : MeasurableEmbedding e
f : β → ε
μ : Measure β
s : Set β
hs : s ∈ map e l
int : IntegrableOn f s μ
⊢ ∃ s ∈ map e l, IntegrableOn f s (μ.restrict (range e))
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
l : Filter α
inst✝ : MeasurableSpace β
e : α → β
he : MeasurableEmbedding e
f : β → ε
μ : Measure β
⊢ (∃ s ∈ map e l, IntegrableOn f s (μ.restrict (range e))) → ∃ s ∈ map e l, IntegrableOn f s μ

Tactic:
rintro ⟨s, hs, int⟩

Goal state after:
case mpr
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
l : Filter α
inst✝ : MeasurableSpace β
e : α → β
he : MeasurableEmbedding e
f : β → ε
μ : Measure β
s : Set β
hs : s ∈ map e l
int : IntegrableOn f s (μ.restrict (range e))
⊢ ∃ s ∈ map e l, IntegrableOn f s μ
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
hf : IntegrableAtFilter f l μ
⊢ IntegrableAtFilter (-f) l μ

Tactic:
rcases hf with ⟨s, sl, hs⟩
  exact ⟨s, sl, hs.neg⟩

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 →ₗ[𝕜] 𝕜
H : ¬finrank 𝕜 ↥f.range = 0
Z : finrank 𝕜 ↥f.range + finrank 𝕜 ↥f.ker = n + 1
⊢ finrank 𝕜 ↥f.ker = n

Tactic:
have : finrank 𝕜 (LinearMap.range f) = 1 :=
            le_antisymm (finrank_self 𝕜 ▸ (LinearMap.range f).finrank_le) (zero_lt_iff.mpr H)

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 →ₗ[𝕜] 𝕜
H : ¬finrank 𝕜 ↥f.range = 0
Z : finrank 𝕜 ↥f.range + finrank 𝕜 ↥f.ker = n + 1
this : finrank 𝕜 ↥f.range = 1
⊢ finrank 𝕜 ↥f.ker = n
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 ι
⊢ 𝓤 (ContinuousMultilinearMap 𝕜 E G) = ⨅ r, ⨅ (_ : r > 0), 𝓟 {f | ‖-f.1 + f.2‖ < r}

Tactic:
by
  have A (f : ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G) :
      ‖-f.1 + f.2‖ = ‖f.1 - f.2‖ := by rw [← opNorm_neg, neg_add, neg_neg, sub_eq_add_neg]
  simp only [A]
  refine (ContinuousMultilinearMap.seminorm 𝕜 E G).uniformity_eq_of_hasBasis
    (ContinuousMultilinearMap.hasBasis_nhds_zero_of_basis Metric.nhds_basis_closedBall)
    ?_ fun (s, r) ⟨hs, hr⟩ ↦ ?_
  · rcases NormedField.exists_lt_norm 𝕜 1 with ⟨c, hc⟩
    have hc₀ : 0 < ‖c‖ := one_pos.trans hc
    simp only [hasBasis_nhds_zero.mem_iff, Prod.exists]
    use 1, closedBall 0 ‖c‖, closedBall 0 1
    suffices ∀ f : ContinuousMultilinearMap 𝕜 E G, (∀ x, ‖x‖ ≤ ‖c‖ → ‖f x‖ ≤ 1) → ‖f‖ ≤ 1 by
      simpa [NormedSpace.isVonNBounded_closedBall, closedBall_mem_nhds, Set.subset_def, Set.MapsTo]
    intro f hf
    refine opNorm_le_bound (by positivity) <|
      f.1.bound_of_shell_of_continuous f.2 (fun _ ↦ hc₀) (fun _ ↦ hc) fun x hcx hx ↦ ?_
    calc
      ‖f x‖ ≤ 1 := hf _ <| (pi_norm_le_iff_of_nonneg (norm_nonneg c)).2 fun i ↦ (hx i).le
      _ = ∏ i : ι, 1 := by simp
      _ ≤ ∏ i, ‖x i‖ := by gcongr with i; simpa only [div_self hc₀.ne'] using hcx i
      _ = 1 * ∏ i, ‖x i‖ := (one_mul _).symm
  · rcases (NormedSpace.isVonNBounded_iff' _).1 hs with ⟨ε, hε⟩
    rcases exists_pos_mul_lt hr (ε ^ Fintype.card ι) with ⟨δ, hδ₀, hδ⟩
    refine ⟨δ, hδ₀, fun f hf x hx ↦ ?_⟩
    simp only [Seminorm.mem_ball_zero, mem_closedBall_zero_iff] at hf ⊢
    replace hf : ‖f‖ ≤ δ := hf.le
    replace hx : ‖x‖ ≤ ε := hε x hx
    calc
      ‖f x‖ ≤ ‖f‖ * ε ^ Fintype.card ι := le_opNorm_mul_pow_card_of_le f hx
      _ ≤ δ * ε ^ Fintype.card ι := by have := (norm_nonneg x).trans hx; gcongr
      _ ≤ r := (mul_comm _ _).trans_le hδ.le

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : CompleteSpace 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : UniformSpace E
inst✝⁴ : T2Space E
inst✝³ : IsUniformAddGroup E
inst✝² : Module 𝕜 E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
⊢ CompleteSpace E

Tactic:
set e := ContinuousLinearEquiv.ofFinrankEq (@finrank_fin_fun 𝕜 _ _ (finrank 𝕜 E)).symm

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : CompleteSpace 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : UniformSpace E
inst✝⁴ : T2Space E
inst✝³ : IsUniformAddGroup E
inst✝² : Module 𝕜 E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
e : E ≃L[𝕜] Fin (finrank 𝕜 E) → 𝕜 := ContinuousLinearEquiv.ofFinrankEq ⋯
⊢ CompleteSpace E
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: case refine_2.inl
𝕜 : 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 𝕜
z : G
hz : ‖z‖₊ = 0
⊢ ‖f‖₊ * ‖z‖₊ ≤ ‖f.smulRight z‖₊

Tactic:
simp [hz]

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
k : ℕ
x : (i : ι) → E₁ i
⊢ ‖f.iteratedFDeriv k x‖ ≤ ↑((Fintype.card ι).descFactorial k) * ‖f‖ * ‖x‖ ^ (Fintype.card ι - k)

Tactic:
by
  classical
  calc ‖f.iteratedFDeriv k x‖
  _ ≤ ∑ e : Fin k ↪ ι, ‖iteratedFDerivComponent f e.toEquivRange (fun i ↦ x i)‖ := norm_sum_le _ _
  _ ≤ ∑ _ : Fin k ↪ ι, ‖f‖ * ‖x‖ ^ (Fintype.card ι - k) := by
    gcongr with e _
    simpa using norm_iteratedFDerivComponent_le f e.toEquivRange x
  _ = Nat.descFactorial (Fintype.card ι) k * ‖f‖ * ‖x‖ ^ (Fintype.card ι - k) := by
    simp [card_univ, mul_assoc]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ = ∞
a : α
h : 0 a ≤ f a
⊢ (fun a ↦ ENNReal.ofReal (f a)) a = (fun a ↦ ENNReal.ofReal ‖f a‖) a

Tactic:
dsimp only

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ = ∞
a : α
h : 0 a ≤ f a
⊢ ENNReal.ofReal (f a) = ENNReal.ofReal ‖f a‖
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: α : Type u_1
β : Type u_3
inst✝ : NormedField β
t u : α → β
l : Filter α
h : t ~[l] u
n : ℕ
⊢ t ^ n ~[l] u ^ n

Tactic:
induction n with
  | zero => simpa using IsEquivalent.refl
  | succ _ ih => simpa [pow_succ] using ih.mul h

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᵐ[μ] g
⊢ ∫ (a : α), f a ∂μ = ∫ (a : α), g a ∂μ ↔ f =ᵐ[μ] g

Tactic:
refine ⟨fun h_le ↦ EventuallyEq.symm ?_, fun h ↦ integral_congr_ae h⟩
  rw [← sub_ae_eq_zero,
    ← integral_eq_zero_iff_of_nonneg_ae ((sub_nonneg_ae _ _).mpr hfg) (hg.sub hf)]
  simpa [Pi.sub_apply, integral_sub hg hf, sub_eq_zero, eq_comm]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfi : Integrable f μ
⊢ 0 ≠ ∫ (x : α), f x ∂μ ↔ 0 < μ (Function.support f)

Tactic:
pos_iff_ne_zero,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfi : Integrable f μ
⊢ 0 ≠ ∫ (x : α), f x ∂μ ↔ μ (Function.support f) ≠ 0
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
f : P →ᴬ[R] Q
p₀ p₁ : P
c : R
⊢ f ((AffineMap.lineMap p₀ p₁) c) = (AffineMap.lineMap (f p₀) (f p₁)) c

Tactic:
by
  rw [← ContinuousAffineMap.coe_toAffineMap, AffineMap.apply_lineMap]

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

Goal state before:
pp: R : Type u_1
V : Type u_3
W : Type u_4
Q : Type u_5
inst✝¹⁰ : Ring R
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module R V
inst✝⁷ : TopologicalSpace V
inst✝⁶ : IsTopologicalAddGroup V
inst✝⁵ : AddCommGroup W
inst✝⁴ : Module R W
inst✝³ : TopologicalSpace W
inst✝² : AddTorsor W Q
inst✝¹ : TopologicalSpace Q
inst✝ : IsTopologicalAddTorsor Q
p : Q × (V →L[R] W)
⊢ ((decompEquiv R V Q).symm p).contLinear = p.2

Tactic:
by
  have := IsTopologicalAddTorsor.to_isTopologicalAddGroup W Q
  ext; simp [decompEquiv]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.RieszLemma

Goal state before:
pp: case inl
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
s : Set F
hx : x ∈ s
h₀ : infDist x sᶜ = 0
⊢ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {x} ⊆
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s

Tactic:
exact closure_mono (singleton_subset_iff.2 hx)

Goal state after:
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
E : Type v
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace 𝕜
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun f ↦ f.det

Tactic:
change Continuous fun f : E →L[𝕜] E => LinearMap.det (f : E →ₗ[𝕜] E)

Goal state after:
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
E : Type v
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace 𝕜
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun f ↦ LinearMap.det ↑f
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f : α →ᵇ β
n : ℕ
⊢ ⇑(-(n.succ • f)) = Int.negSucc n • ⇑f

Tactic:
negSucc_zsmul,

Goal state after:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f : α →ᵇ β
n : ℕ
⊢ ⇑(-(n.succ • f)) = -((n + 1) • ⇑f)
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : LocallyCompactSpace 𝕜
inst✝ : FiniteDimensional 𝕜 E
this : ProperSpace 𝕜
⊢ ProperSpace E

Tactic:
set e := ContinuousLinearEquiv.ofFinrankEq (@finrank_fin_fun 𝕜 _ _ (finrank 𝕜 E)).symm

Goal state after:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : LocallyCompactSpace 𝕜
inst✝ : FiniteDimensional 𝕜 E
this : ProperSpace 𝕜
e : E ≃L[𝕜] Fin (finrank 𝕜 E) → 𝕜 := ContinuousLinearEquiv.ofFinrankEq ⋯
⊢ ProperSpace E
Module: Mathlib.Topology.MetricSpace.ThickenedIndicator

Goal state before:
pp: case pos
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
a : α
h : a ∈ E
⊢ E.indicator (fun x ↦ 1) a ≤ (thickenedIndicator δ_pos E) a

pp: case neg
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
a : α
h : a ∉ E
⊢ E.indicator (fun x ↦ 1) a ≤ (thickenedIndicator δ_pos E) a

Tactic:
· simp only [h, indicator_of_mem, thickenedIndicator_one δ_pos E h, le_refl]

Goal state after:
case neg
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
a : α
h : a ∉ E
⊢ E.indicator (fun x ↦ 1) a ≤ (thickenedIndicator δ_pos E) a
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: case pos.h_ae
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C C' : ℝ
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f μ
hF : CompleteSpace F
h_int : ∀ (g : α → E), Integrable g μ → Integrable g μ'
⊢ ∀ ⦃f g : α → E⦄,
    f =ᵐ[μ] g → Integrable f μ → setToFun μ T hT f = setToFun μ' T hT' f → setToFun μ T hT g = setToFun μ' T hT' g

Tactic:
intro f₂ g₂ hfg _ hf_eq

Goal state after:
case pos.h_ae
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C C' : ℝ
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f μ
hF : CompleteSpace F
h_int : ∀ (g : α → E), Integrable g μ → Integrable g μ'
f₂ g₂ : α → E
hfg : f₂ =ᵐ[μ] g₂
a✝ : Integrable f₂ μ
hf_eq : setToFun μ T hT f₂ = setToFun μ' T hT' f₂
⊢ setToFun μ T hT g₂ = setToFun μ' T hT' g₂
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ μ' μ'' : Measure α
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T' C'
hT'' : DominatedFinMeasAdditive μ'' T'' C''
h : ∀ (s : Set α), MeasurableSet s → (μ + μ') s < ∞ → T'' s = T s + T' s
hf : Integrable f μ
hf' : Integrable f μ'
hμ : μ'' ≤ μ + μ'
hC : 0 ≤ C
hC' : 0 ≤ C'
hC'' : 0 ≤ C''
I : DominatedFinMeasAdditive (μ + μ') T C
A : setToFun (μ + μ') T I f = setToFun μ T hT f
I' : DominatedFinMeasAdditive (μ + μ') T' C'
A' : setToFun (μ + μ') T' I' f = setToFun μ' T' hT' f
I'' : DominatedFinMeasAdditive (μ + μ') T'' C''
⊢ setToFun μ'' T'' hT'' f = setToFun μ T hT f + setToFun μ' T' hT' f

Tactic:
have A'' : setToFun (μ + μ') T'' I'' f = setToFun μ'' T'' hT'' f := by
    apply setToFun_congr_measure_of_integrable (c' := 1) (by simp) (by simpa using hμ)
    apply hf.add_measure hf'

Goal state after:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ μ' μ'' : Measure α
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T' C'
hT'' : DominatedFinMeasAdditive μ'' T'' C''
h : ∀ (s : Set α), MeasurableSet s → (μ + μ') s < ∞ → T'' s = T s + T' s
hf : Integrable f μ
hf' : Integrable f μ'
hμ : μ'' ≤ μ + μ'
hC : 0 ≤ C
hC' : 0 ≤ C'
hC'' : 0 ≤ C''
I : DominatedFinMeasAdditive (μ + μ') T C
A : setToFun (μ + μ') T I f = setToFun μ T hT f
I' : DominatedFinMeasAdditive (μ + μ') T' C'
A' : setToFun (μ + μ') T' I' f = setToFun μ' T' hT' f
I'' : DominatedFinMeasAdditive (μ + μ') T'' C''
A'' : setToFun (μ + μ') T'' I'' f = setToFun μ'' T'' hT'' f
⊢ setToFun μ'' T'' hT'' f = setToFun μ T hT f + setToFun μ' T' hT' f
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ μ' μ'' : Measure α
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T' C'
hT'' : DominatedFinMeasAdditive μ'' T'' C''
h : ∀ (s : Set α), MeasurableSet s → (μ + μ') s < ∞ → T'' s = T s + T' s
hf : Integrable f μ
hf' : Integrable f μ'
hμ : μ'' ≤ μ + μ'
hC : 0 ≤ C
hC' : 0 ≤ C'
hC'' : 0 ≤ C''
⊢ setToFun μ'' T'' hT'' f = setToFun μ T hT f + setToFun μ' T' hT' f

Tactic:
by
  have I : DominatedFinMeasAdditive (μ + μ') T C := .add_measure_right _ _ hT hC
  have A : setToFun (μ + μ') T I f = setToFun μ T hT f :=
    setToFun_congr_measure_of_add_right _ _ _ (hf.add_measure hf')
  have I' : DominatedFinMeasAdditive (μ + μ') T' C' := .add_measure_left _ _ hT' hC'
  have A' : setToFun (μ + μ') T' I' f = setToFun μ' T' hT' f :=
    setToFun_congr_measure_of_add_left _ _ _ (hf.add_measure hf')
  have I'' : DominatedFinMeasAdditive (μ + μ') T'' C'' := .of_measure_le hμ hT'' hC''
  have A'' : setToFun (μ + μ') T'' I'' f = setToFun μ'' T'' hT'' f := by
    apply setToFun_congr_measure_of_integrable (c' := 1) (by simp) (by simpa using hμ)
    apply hf.add_measure hf'
  rw [← A, ← A', ← A'']
  apply setToFun_add_left' _ _ _ h

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

Goal state before:
pp: case insert
δ : Type u_1
δ' : Type u_2
X : δ → Type u_3
inst✝³ : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝² : DecidableEq δ
inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)
inst✝ : DecidableEq δ'
e : δ' → δ
he : Injective e
f : ((i : δ') → X (e i)) → ℝ≥0∞
hf : Measurable f
h : Measurable fun x ↦ (fun {x_1} ↦ x) ∘' e
a✝ : δ'
s✝ : Finset δ'
hi : a✝ ∉ s✝
ih :
  ∀ (x : (i : δ) → X i),
    (∫⋯∫⁻_Finset.image e s✝, f ∘ fun x ↦ (fun {x_1} ↦ x) ∘' e ∂μ) x =
      (∫⋯∫⁻_s✝, f ∂(fun {x} ↦ μ) ∘' e) ((fun {x_1} ↦ x) ∘' e)
x : (i : δ) → X i
⊢ (∫⋯∫⁻_insert (e a✝) (Finset.image e s✝), f ∘ fun x ↦ (fun {x_1} ↦ x) ∘' e ∂μ) x =
    (∫⋯∫⁻_insert a✝ s✝, f ∂(fun {x} ↦ μ) ∘' e) ((fun {x_1} ↦ x) ∘' e)

Tactic:
lmarginal_insert _ (hf.comp h) (he.mem_finset_image.not.mpr hi),

Goal state after:
case insert
δ : Type u_1
δ' : Type u_2
X : δ → Type u_3
inst✝³ : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝² : DecidableEq δ
inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)
inst✝ : DecidableEq δ'
e : δ' → δ
he : Injective e
f : ((i : δ') → X (e i)) → ℝ≥0∞
hf : Measurable f
h : Measurable fun x ↦ (fun {x_1} ↦ x) ∘' e
a✝ : δ'
s✝ : Finset δ'
hi : a✝ ∉ s✝
ih :
  ∀ (x : (i : δ) → X i),
    (∫⋯∫⁻_Finset.image e s✝, f ∘ fun x ↦ (fun {x_1} ↦ x) ∘' e ∂μ) x =
      (∫⋯∫⁻_s✝, f ∂(fun {x} ↦ μ) ∘' e) ((fun {x_1} ↦ x) ∘' e)
x : (i : δ) → X i
⊢ ∫⁻ (xᵢ : X (e a✝)), (∫⋯∫⁻_Finset.image e s✝, f ∘ fun x ↦ (fun {x_1} ↦ x) ∘' e ∂μ) (update x (e a✝) xᵢ) ∂μ (e a✝) =
    (∫⋯∫⁻_insert a✝ s✝, f ∂(fun {x} ↦ μ) ∘' e) ((fun {x_1} ↦ x) ∘' e)