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

Goal state before:
pp: α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
s : Set α
μ : Measure α
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
C : ℝ≥0∞
hC : ‖C‖ₑ ≠ ∞
hs : μ s ≠ ∞
hf : ∀ᵐ (x : α) ∂μ.restrict s, ‖f x‖ₑ ≤ C
⊢ (μ.restrict s) univ < ∞

Tactic:
rw [Measure.restrict_apply_univ]

Goal state after:
α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
s : Set α
μ : Measure α
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
C : ℝ≥0∞
hC : ‖C‖ₑ ≠ ∞
hs : μ s ≠ ∞
hf : ∀ᵐ (x : α) ∂μ.restrict s, ‖f x‖ₑ ≤ C
⊢ μ s < ∞
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g₁ g₂ : α → ℝ
hf : AEStronglyMeasurable f μ
h_le₁ : g₁ ≤ᵐ[μ] f
h_le₂ : f ≤ᵐ[μ] g₂
h_int₁ : Integrable g₁ μ
h_int₂ : Integrable g₂ μ
⊢ ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ max ‖g₁ x‖ ‖g₂ x‖

Tactic:
filter_upwards [h_le₁, h_le₂] with x hx1 hx2

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g₁ g₂ : α → ℝ
hf : AEStronglyMeasurable f μ
h_le₁ : g₁ ≤ᵐ[μ] f
h_le₂ : f ≤ᵐ[μ] g₂
h_int₁ : Integrable g₁ μ
h_int₂ : Integrable g₂ μ
x : α
hx1 : g₁ x ≤ f x
hx2 : f x ≤ g₂ x
⊢ ‖f x‖ ≤ max ‖g₁ x‖ ‖g₂ x‖
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 : MultilinearMap 𝕜 E G
hf : Continuous[Pi.topologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ⇑f
⊢ ∃ C, 0 < C ∧ ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i, ‖m i‖

Tactic:
by
  cases isEmpty_or_nonempty ι
  · refine ⟨‖f 0‖ + 1, add_pos_of_nonneg_of_pos (norm_nonneg _) zero_lt_one, fun m => ?_⟩
    obtain rfl : m = 0 := funext (IsEmpty.elim ‹_›)
    simp [univ_eq_empty, zero_le_one]
  obtain ⟨ε : ℝ, ε0 : 0 < ε, hε : ∀ m : ∀ i, E i, ‖m - 0‖ < ε → ‖f m - f 0‖ < 1⟩ :=
    NormedAddCommGroup.tendsto_nhds_nhds.1 (hf.tendsto 0) 1 zero_lt_one
  simp only [sub_zero, f.map_zero] at hε
  rcases NormedField.exists_one_lt_norm 𝕜 with ⟨c, hc⟩
  have : 0 < (‖c‖ / ε) ^ Fintype.card ι := pow_pos (div_pos (zero_lt_one.trans hc) ε0) _
  refine ⟨_, this, ?_⟩
  refine f.bound_of_shell_of_continuous hf (fun _ => ε0) (fun _ => hc) fun m hcm hm => ?_
  refine (hε m ((pi_norm_lt_iff ε0).2 hm)).le.trans ?_
  rw [← div_le_iff₀' this, one_div, ← inv_pow, inv_div, Fintype.card, ← prod_const]
  gcongr
  apply hcm

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 : α → β
hf : Integrable f μ
⊢ ‖toL1 f hf‖ = (∫⁻ (a : α), ‖f a‖ₑ ∂μ).toReal

Tactic:
by
  simp_rw [norm_toL1, edist_zero_right]

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

Goal state before:
pp: X : Type u_1
ε : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
f : X → ε
μ : Measure X
inst✝ : SecondCountableTopology X
hf : LocallyIntegrable f μ
u : ℕ → Set X
u_open : ∀ (n : ℕ), IsOpen[inst✝³] (u n)
u_union : univ ⊆ ⋃ n, u n
hu : ∀ (n : ℕ), IntegrableOn f (u n ∩ univ) μ
⊢ ∃ u, (∀ (n : ℕ), IsOpen[inst✝³] (u n)) ∧ ⋃ n, u n = univ ∧ ∀ (n : ℕ), IntegrableOn f (u n) μ

Tactic:
refine ⟨u, u_open, eq_univ_of_univ_subset u_union, fun n ↦ ?_⟩

Goal state after:
X : Type u_1
ε : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
f : X → ε
μ : Measure X
inst✝ : SecondCountableTopology X
hf : LocallyIntegrable f μ
u : ℕ → Set X
u_open : ∀ (n : ℕ), IsOpen[inst✝³] (u n)
u_union : univ ⊆ ⋃ n, u n
hu : ∀ (n : ℕ), IntegrableOn f (u n ∩ univ) μ
n : ℕ
⊢ IntegrableOn f (u n) μ
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: 𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
G : Type wG
G' : Type wG'
inst✝¹⁰ : Fintype ι'
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁷ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝⁴ : SeminormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
inst✝² : SeminormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
inst✝ : Fintype ι
g : ContinuousMultilinearMap 𝕜 E₁ G
⊢ ∀ [inst : DecidableEq ι] (m : (i : ι) → E i →L[𝕜] E₁ i) (i : ι) (c : 𝕜) (x : E i →L[𝕜] E₁ i),
    g.compContinuousLinearMap (update m i (c • x)) = c • g.compContinuousLinearMap (update m i x)

Tactic:
intro h f i a f₀
        ext x
        simp only [compContinuousLinearMap_apply, smul_apply]
        convert! g.map_update_smul (fun j ↦ f j (x j)) i a (f₀ (x i)) <;>
          exact apply_update (fun (i : ι) (f : E i →L[𝕜] E₁ i) ↦ f (x i)) f i _ _

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 ι
α : Type u_1
inst✝¹ : Fintype α
f : ContinuousMultilinearMap 𝕜 E₁ G
s : Set ι
e : α ≃ ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
x : (i : ι) → E₁ i
⊢ ‖f‖ * ∏ _i, ‖x‖ = ‖f‖ * ‖x‖ ^ Fintype.card { a // a ∉ s }

Tactic:
rw [prod_const, card_univ]

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
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
f' : β → E := AEStronglyMeasurable.mk f ⋯
hf' : MemLp f' p μ
f'meas : Measurable f'
this : SeparableSpace ↑(Set.range f' ∪ {0})
⊢ ∃ g, eLpNorm (f' - ⇑g) p μ < ε ∧ MemLp (⇑g) p μ

Tactic:
rcases ((tendsto_approxOn_range_Lp_eLpNorm hp_ne_top f'meas hf'.2).eventually <|
    gt_mem_nhds hε.bot_lt).exists with ⟨n, hn⟩

Goal state after:
β : 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
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
f' : β → E := AEStronglyMeasurable.mk f ⋯
hf' : MemLp f' p μ
f'meas : Measurable f'
this : SeparableSpace ↑(Set.range f' ∪ {0})
n : ℕ
hn : eLpNorm (⇑(approxOn f' f'meas (Set.range f' ∪ {0}) 0 ⋯ n) - f') p μ < ε
⊢ ∃ g, eLpNorm (f' - ⇑g) p μ < ε ∧ MemLp (⇑g) p μ
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: α : Type u_1
β : Type u_7
inst✝ : SeminormedAddCommGroup β
C : ℝ
m : MeasurableSpace α
μ : Measure α
hC : 0 ≤ C
⊢ DominatedFinMeasAdditive μ 0 C

Tactic:
refine ⟨FinMeasAdditive.zero, fun s _ _ => ?_⟩
  rw [Pi.zero_apply, norm_zero]
  exact mul_nonneg hC toReal_nonneg

Goal state after:
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 g : ↥(simpleFunc E p μ)
a✝ : α
⊢ (toSimpleFunc (f + g)) a✝ = ↑(↑↑f + ↑↑g) a✝ →
    (toSimpleFunc f) a✝ = ↑↑↑f a✝ →
      (toSimpleFunc g) a✝ = ↑↑↑g a✝ →
        ↑(↑↑f + ↑↑g) a✝ = ↑↑↑f a✝ + ↑↑↑g a✝ → (toSimpleFunc (f + g)) a✝ = (toSimpleFunc f) a✝ + (toSimpleFunc g) a✝

Tactic:
iterate 4 intro h; rw [h]

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

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
x : F
⊢ (weightedSMul μ ∅) x = 0 x

Tactic:
rw [weightedSMul_apply]

Goal state after:
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
x : F
⊢ μ.real ∅ • x = 0 x
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: α : Type u_1
G' : Type u_7
G'' : Type u_8
inst✝⁶ : NormedAddCommGroup G''
inst✝⁵ : PartialOrder G''
inst✝⁴ : IsOrderedAddMonoid G''
inst✝³ : NormedSpace ℝ G''
inst✝² : NormedAddCommGroup G'
inst✝¹ : PartialOrder G'
inst✝ : NormedSpace ℝ G'
m : MeasurableSpace α
T : Set α → G' →L[ℝ] G''
hT_nonneg : ∀ (s : Set α) (x : G'), 0 ≤ x → 0 ≤ (T s) x
f : α →ₛ G'
hf : 0 ≤ f
⊢ 0 ≤ setToSimpleFunc T f

Tactic:
refine sum_nonneg fun i hi => hT_nonneg _ i ?_
  rw [mem_range] at hi
  obtain ⟨y, hy⟩ := Set.mem_range.mp hi
  rw [← hy]
  refine le_trans ?_ (hf y)
  simp

Goal state after:
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v : α → β
l : Filter α
huv : u ~[l] v
x✝ : α
⊢ ((fun x ↦ -u x) - fun x ↦ -v x) x✝ = -(u - v) x✝

Tactic:
simp [neg_add_eq_sub]

Goal state after:
Module: Mathlib.Analysis.Normed.Group.AddTorsor

Goal state before:
pp: V : Type u_2
P : Type u_3
inst✝² : SeminormedAddCommGroup V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
v v' : V
p p' : P
⊢ nndist (v +ᵥ p) (v' +ᵥ p') ≤ nndist v v' + nndist p p'

Tactic:
apply dist_vadd_vadd_le

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

Goal state before:
pp: case inr.const.inr
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_ne_top : p ≠ ∞
P : (α → E) → Prop
h0P :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s → μ s < ∞ → ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ g, eLpNorm (g - s.indicator fun x ↦ c) p μ ≤ ε ∧ P g
h1P : ∀ (f g : α → E), P f → P g → P (f + g)
h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ
f : α → E
hf : MemLp f p μ
ε✝ : ℝ≥0∞
hε : ε✝ ≠ 0
hp_pos : p ≠ 0
c : E
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
εpos : ε ≠ 0
Hs : MemLp (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))) p μ
hc : c ≠ 0
this : μ s < ∞
g : α → E
hg : eLpNorm ((s.indicator fun x ↦ c) - g) p μ ≤ ε
Pg : P g
⊢ ∃ g, eLpNorm (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) - g) p μ ≤ ε ∧ P g

Tactic:
exact ⟨g, hg, Pg⟩

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

Goal state before:
pp: case mk
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
g : P →ᴬ[R] Q
toAffineMap✝ : P →ᵃ[R] Q
cont✝ : Continuous toAffineMap✝.toFun
h : ↑{ toAffineMap := toAffineMap✝, cont := cont✝ } = ↑g
⊢ { toAffineMap := toAffineMap✝, cont := cont✝ } = g

Tactic:
cases g

Goal state after:
case mk.mk
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
toAffineMap✝¹ : P →ᵃ[R] Q
cont✝¹ : Continuous toAffineMap✝¹.toFun
toAffineMap✝ : P →ᵃ[R] Q
cont✝ : Continuous toAffineMap✝.toFun
h : ↑{ toAffineMap := toAffineMap✝¹, cont := cont✝¹ } = ↑{ toAffineMap := toAffineMap✝, cont := cont✝ }
⊢ { toAffineMap := toAffineMap✝¹, cont := cont✝¹ } = { toAffineMap := toAffineMap✝, cont := cont✝ }
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (F x))
f' : ℕ → α → ℝ := fun n x ↦ f n x - f 0 x
hf'_nonneg : ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, 0 ≤ f' i a
hf'_meas : ∀ (n : ℕ), Integrable (f' n) μ
hF_ge : 0 ≤ᵐ[μ] fun x ↦ (F - f 0) x
h_cont : ContinuousAt ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal ((F - f 0) a) ∂μ)
x : α
hx : Tendsto (fun n ↦ f n x) atTop (𝓝 (F x))
⊢ Tendsto (fun n ↦ f' n x) atTop (𝓝 ((F - f 0) x))

Tactic:
simp only [Pi.sub_apply]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (F x))
f' : ℕ → α → ℝ := fun n x ↦ f n x - f 0 x
hf'_nonneg : ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, 0 ≤ f' i a
hf'_meas : ∀ (n : ℕ), Integrable (f' n) μ
hF_ge : 0 ≤ᵐ[μ] fun x ↦ (F - f 0) x
h_cont : ContinuousAt ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal ((F - f 0) a) ∂μ)
x : α
hx : Tendsto (fun n ↦ f n x) atTop (𝓝 (F x))
⊢ Tendsto (fun n ↦ f' n x) atTop (𝓝 (F x - f 0 x))
Module: Mathlib.Analysis.Normed.Affine.Isometry

Goal state before:
pp: case mk
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₁' : Type u_4
V₂ : Type u_5
V₃ : Type u_6
V₄ : Type u_7
P₁ : Type u_8
P₁' : Type u_9
P : Type u_10
P₂ : Type u_11
P₃ : Type u_12
P₄ : Type u_13
inst✝²⁴ : NormedField 𝕜
inst✝²³ : SeminormedAddCommGroup V
inst✝²² : NormedSpace 𝕜 V
inst✝²¹ : PseudoMetricSpace P
inst✝²⁰ : NormedAddTorsor V P
inst✝¹⁹ : SeminormedAddCommGroup V₁
inst✝¹⁸ : NormedSpace 𝕜 V₁
inst✝¹⁷ : PseudoMetricSpace P₁
inst✝¹⁶ : NormedAddTorsor V₁ P₁
inst✝¹⁵ : SeminormedAddCommGroup V₁'
inst✝¹⁴ : NormedSpace 𝕜 V₁'
inst✝¹³ : MetricSpace P₁'
inst✝¹² : NormedAddTorsor V₁' P₁'
inst✝¹¹ : SeminormedAddCommGroup V₂
inst✝¹⁰ : NormedSpace 𝕜 V₂
inst✝⁹ : PseudoMetricSpace P₂
inst✝⁸ : NormedAddTorsor V₂ P₂
inst✝⁷ : SeminormedAddCommGroup V₃
inst✝⁶ : NormedSpace 𝕜 V₃
inst✝⁵ : PseudoMetricSpace P₃
inst✝⁴ : NormedAddTorsor V₃ P₃
inst✝³ : SeminormedAddCommGroup V₄
inst✝² : NormedSpace 𝕜 V₄
inst✝¹ : PseudoMetricSpace P₄
inst✝ : NormedAddTorsor V₄ P₄
f g : P →ᵃⁱ[𝕜] P₂
toAffineMap✝ : P →ᵃ[𝕜] P₂
norm_map✝ : ∀ (x : V), ‖toAffineMap✝.linear x‖ = ‖x‖
⊢ (fun f ↦ f.toFun) { toAffineMap := toAffineMap✝, norm_map := norm_map✝ } = (fun f ↦ f.toFun) g →
    { toAffineMap := toAffineMap✝, norm_map := norm_map✝ } = g

Tactic:
cases g

Goal state after:
case mk.mk
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₁' : Type u_4
V₂ : Type u_5
V₃ : Type u_6
V₄ : Type u_7
P₁ : Type u_8
P₁' : Type u_9
P : Type u_10
P₂ : Type u_11
P₃ : Type u_12
P₄ : Type u_13
inst✝²⁴ : NormedField 𝕜
inst✝²³ : SeminormedAddCommGroup V
inst✝²² : NormedSpace 𝕜 V
inst✝²¹ : PseudoMetricSpace P
inst✝²⁰ : NormedAddTorsor V P
inst✝¹⁹ : SeminormedAddCommGroup V₁
inst✝¹⁸ : NormedSpace 𝕜 V₁
inst✝¹⁷ : PseudoMetricSpace P₁
inst✝¹⁶ : NormedAddTorsor V₁ P₁
inst✝¹⁵ : SeminormedAddCommGroup V₁'
inst✝¹⁴ : NormedSpace 𝕜 V₁'
inst✝¹³ : MetricSpace P₁'
inst✝¹² : NormedAddTorsor V₁' P₁'
inst✝¹¹ : SeminormedAddCommGroup V₂
inst✝¹⁰ : NormedSpace 𝕜 V₂
inst✝⁹ : PseudoMetricSpace P₂
inst✝⁸ : NormedAddTorsor V₂ P₂
inst✝⁷ : SeminormedAddCommGroup V₃
inst✝⁶ : NormedSpace 𝕜 V₃
inst✝⁵ : PseudoMetricSpace P₃
inst✝⁴ : NormedAddTorsor V₃ P₃
inst✝³ : SeminormedAddCommGroup V₄
inst✝² : NormedSpace 𝕜 V₄
inst✝¹ : PseudoMetricSpace P₄
inst✝ : NormedAddTorsor V₄ P₄
f : P →ᵃⁱ[𝕜] P₂
toAffineMap✝¹ : P →ᵃ[𝕜] P₂
norm_map✝¹ : ∀ (x : V), ‖toAffineMap✝¹.linear x‖ = ‖x‖
toAffineMap✝ : P →ᵃ[𝕜] P₂
norm_map✝ : ∀ (x : V), ‖toAffineMap✝.linear x‖ = ‖x‖
⊢ (fun f ↦ f.toFun) { toAffineMap := toAffineMap✝¹, norm_map := norm_map✝¹ } =
      (fun f ↦ f.toFun) { toAffineMap := toAffineMap✝, norm_map := norm_map✝ } →
    { toAffineMap := toAffineMap✝¹, norm_map := norm_map✝¹ } = { toAffineMap := toAffineMap✝, norm_map := norm_map✝ }
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 : Set α → E →L[ℝ] F
C : ℝ
inst✝ : CompleteSpace F
hT : DominatedFinMeasAdditive μ T C
f : ↥(Lp E 1 μ)
⊢ (setToL1 hT) (Integrable.toL1 ↑↑f ⋯) = (setToL1 hT) f

Tactic:
Integrable.toL1_coeFn

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 : Set α → E →L[ℝ] F
C : ℝ
inst✝ : CompleteSpace F
hT : DominatedFinMeasAdditive μ T C
f : ↥(Lp E 1 μ)
⊢ (setToL1 hT) f = (setToL1 hT) f
Module: Mathlib.Analysis.Normed.Affine.Isometry

Goal state before:
pp: case mk
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₁' : Type u_4
V₂ : Type u_5
V₃ : Type u_6
V₄ : Type u_7
P₁ : Type u_8
P₁' : Type u_9
P : Type u_10
P₂ : Type u_11
P₃ : Type u_12
P₄ : Type u_13
inst✝²⁴ : NormedField 𝕜
inst✝²³ : SeminormedAddCommGroup V
inst✝²² : NormedSpace 𝕜 V
inst✝²¹ : PseudoMetricSpace P
inst✝²⁰ : NormedAddTorsor V P
inst✝¹⁹ : SeminormedAddCommGroup V₁
inst✝¹⁸ : NormedSpace 𝕜 V₁
inst✝¹⁷ : PseudoMetricSpace P₁
inst✝¹⁶ : NormedAddTorsor V₁ P₁
inst✝¹⁵ : SeminormedAddCommGroup V₁'
inst✝¹⁴ : NormedSpace 𝕜 V₁'
inst✝¹³ : MetricSpace P₁'
inst✝¹² : NormedAddTorsor V₁' P₁'
inst✝¹¹ : SeminormedAddCommGroup V₂
inst✝¹⁰ : NormedSpace 𝕜 V₂
inst✝⁹ : PseudoMetricSpace P₂
inst✝⁸ : NormedAddTorsor V₂ P₂
inst✝⁷ : SeminormedAddCommGroup V₃
inst✝⁶ : NormedSpace 𝕜 V₃
inst✝⁵ : PseudoMetricSpace P₃
inst✝⁴ : NormedAddTorsor V₃ P₃
inst✝³ : SeminormedAddCommGroup V₄
inst✝² : NormedSpace 𝕜 V₄
inst✝¹ : PseudoMetricSpace P₄
inst✝ : NormedAddTorsor V₄ P₄
e g : P ≃ᵃⁱ[𝕜] P₂
toAffineEquiv✝ : P ≃ᵃ[𝕜] P₂
norm_map✝ : ∀ (x : V), ‖toAffineEquiv✝.linear x‖ = ‖x‖
h : { toAffineEquiv := toAffineEquiv✝, norm_map := norm_map✝ }.toFun = g.toFun
x✝ : { toAffineEquiv := toAffineEquiv✝, norm_map := norm_map✝ }.invFun = g.invFun
⊢ { toAffineEquiv := toAffineEquiv✝, norm_map := norm_map✝ } = g

Tactic:
cases g

Goal state after:
case mk.mk
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₁' : Type u_4
V₂ : Type u_5
V₃ : Type u_6
V₄ : Type u_7
P₁ : Type u_8
P₁' : Type u_9
P : Type u_10
P₂ : Type u_11
P₃ : Type u_12
P₄ : Type u_13
inst✝²⁴ : NormedField 𝕜
inst✝²³ : SeminormedAddCommGroup V
inst✝²² : NormedSpace 𝕜 V
inst✝²¹ : PseudoMetricSpace P
inst✝²⁰ : NormedAddTorsor V P
inst✝¹⁹ : SeminormedAddCommGroup V₁
inst✝¹⁸ : NormedSpace 𝕜 V₁
inst✝¹⁷ : PseudoMetricSpace P₁
inst✝¹⁶ : NormedAddTorsor V₁ P₁
inst✝¹⁵ : SeminormedAddCommGroup V₁'
inst✝¹⁴ : NormedSpace 𝕜 V₁'
inst✝¹³ : MetricSpace P₁'
inst✝¹² : NormedAddTorsor V₁' P₁'
inst✝¹¹ : SeminormedAddCommGroup V₂
inst✝¹⁰ : NormedSpace 𝕜 V₂
inst✝⁹ : PseudoMetricSpace P₂
inst✝⁸ : NormedAddTorsor V₂ P₂
inst✝⁷ : SeminormedAddCommGroup V₃
inst✝⁶ : NormedSpace 𝕜 V₃
inst✝⁵ : PseudoMetricSpace P₃
inst✝⁴ : NormedAddTorsor V₃ P₃
inst✝³ : SeminormedAddCommGroup V₄
inst✝² : NormedSpace 𝕜 V₄
inst✝¹ : PseudoMetricSpace P₄
inst✝ : NormedAddTorsor V₄ P₄
e : P ≃ᵃⁱ[𝕜] P₂
toAffineEquiv✝¹ : P ≃ᵃ[𝕜] P₂
norm_map✝¹ : ∀ (x : V), ‖toAffineEquiv✝¹.linear x‖ = ‖x‖
toAffineEquiv✝ : P ≃ᵃ[𝕜] P₂
norm_map✝ : ∀ (x : V), ‖toAffineEquiv✝.linear x‖ = ‖x‖
h :
  { toAffineEquiv := toAffineEquiv✝¹, norm_map := norm_map✝¹ }.toFun =
    { toAffineEquiv := toAffineEquiv✝, norm_map := norm_map✝ }.toFun
x✝ :
  { toAffineEquiv := toAffineEquiv✝¹, norm_map := norm_map✝¹ }.invFun =
    { toAffineEquiv := toAffineEquiv✝, norm_map := norm_map✝ }.invFun
⊢ { toAffineEquiv := toAffineEquiv✝¹, norm_map := norm_map✝¹ } =
    { toAffineEquiv := toAffineEquiv✝, norm_map := norm_map✝ }
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: case neg
α : 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 : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
hf : ¬Integrable f μ
hF : ¬CompleteSpace F
⊢ setToFun μ T hT f = 0

Tactic:
· simp [setToFun, hF]

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

Goal state before:
pp: case neg
α : 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' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
h : T = T'
f : α → E
hF : ¬CompleteSpace F
⊢ setToFun μ T hT f = setToFun μ T' hT' f

pp: case pos
α : 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' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
h : T = T'
f : α → E
hF : CompleteSpace F
⊢ setToFun μ T hT f = setToFun μ T' hT' f

Tactic:
· simp [setToFun, hF]

Goal state after:
case pos
α : 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' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
h : T = T'
f : α → E
hF : CompleteSpace F
⊢ setToFun μ T hT f = setToFun μ T' hT' f
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: case neg
α : 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' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
h : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T s = T' s
f : α → E
hF : ¬CompleteSpace F
⊢ setToFun μ T hT f = setToFun μ T' hT' f

pp: case pos
α : 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' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
h : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T s = T' s
f : α → E
hF : CompleteSpace F
⊢ setToFun μ T hT f = setToFun μ T' hT' f

Tactic:
· simp [setToFun, hF]

Goal state after:
case pos
α : 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' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
h : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T s = T' s
f : α → E
hF : CompleteSpace F
⊢ setToFun μ T hT f = setToFun μ T' hT' f
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: case neg
α : 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' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
f : α → E
hF : ¬CompleteSpace F
⊢ setToFun μ (T + T') ⋯ f = setToFun μ T hT f + setToFun μ T' hT' f

pp: case pos
α : 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' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
f : α → E
hF : CompleteSpace F
⊢ setToFun μ (T + T') ⋯ f = setToFun μ T hT f + setToFun μ T' hT' f

Tactic:
· simp [setToFun, hF]

Goal state after:
case pos
α : 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' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
f : α → E
hF : CompleteSpace F
⊢ setToFun μ (T + T') ⋯ f = setToFun μ T hT f + setToFun μ T' hT' f