mathlib-initiative/mathlib-tactics huggingface dataset:
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, eLpNorm (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) - g) p μ ≤ ε ∧ P g

Tactic:
rcases h0P c hs this εpos with ⟨g, hg, Pg⟩

Goal state after:
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 (g - s.indicator fun x ↦ c) p μ ≤ ε
Pg : P g
⊢ ∃ g, eLpNorm (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) - g) p μ ≤ ε ∧ P g
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hfi : Integrable f μ
f_nn : 0 ≤ᵐ[μ] f
⊢ ENNReal.ofReal (∫ (x : α), f x ∂μ) = ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ

Tactic:
have : f =ᵐ[μ] (‖f ·‖) := f_nn.mono fun _x hx ↦ (abs_of_nonneg hx).symm

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hfi : Integrable f μ
f_nn : 0 ≤ᵐ[μ] f
this : f =ᵐ[μ] fun x ↦ ‖f x‖
⊢ ENNReal.ofReal (∫ (x : α), f x ∂μ) = ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: case inr.add
α : 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
f f' : α →ₛ E
hff' : Disjoint (support ⇑f) (support ⇑f')
hf : ∀ (δ : ℝ≥0∞), δ ≠ 0 → MemLp (⇑f) p μ → ∃ g, eLpNorm (⇑f - g) p μ ≤ δ ∧ P g
hf' : ∀ (δ : ℝ≥0∞), δ ≠ 0 → MemLp (⇑f') p μ → ∃ g, eLpNorm (⇑f' - g) p μ ≤ δ ∧ P g
δ : ℝ≥0∞
δpos : δ ≠ 0
int_ff' : MemLp (⇑f) p μ ∧ MemLp (⇑f') p μ
η : ℝ≥0∞
ηpos : 0 < η
hη :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < δ
g : α → E
hg : eLpNorm (⇑f - g) p μ ≤ η
Pg : P g
⊢ ∃ g, eLpNorm (⇑(f + f') - g) p μ ≤ δ ∧ P g

Tactic:
rcases hf' η ηpos.ne' int_ff'.2 with ⟨g', hg', Pg'⟩

Goal state after:
case inr.add
α : 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
f f' : α →ₛ E
hff' : Disjoint (support ⇑f) (support ⇑f')
hf : ∀ (δ : ℝ≥0∞), δ ≠ 0 → MemLp (⇑f) p μ → ∃ g, eLpNorm (⇑f - g) p μ ≤ δ ∧ P g
hf' : ∀ (δ : ℝ≥0∞), δ ≠ 0 → MemLp (⇑f') p μ → ∃ g, eLpNorm (⇑f' - g) p μ ≤ δ ∧ P g
δ : ℝ≥0∞
δpos : δ ≠ 0
int_ff' : MemLp (⇑f) p μ ∧ MemLp (⇑f') p μ
η : ℝ≥0∞
ηpos : 0 < η
hη :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < δ
g : α → E
hg : eLpNorm (⇑f - g) p μ ≤ η
Pg : P g
g' : α → E
hg' : eLpNorm (⇑f' - g') p μ ≤ η
Pg' : P g'
⊢ ∃ g, eLpNorm (⇑(f + f') - g) p μ ≤ δ ∧ P g
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:
eta_expand

Goal state after:
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 fun a ↦ ((↑e₁).prodCongr ↑e₂).toFun a
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:
eta_expand

Goal state after:
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 fun a ↦ ((↑e₁).prodCongr ↑e₂).invFun a
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:
eta_expand

Goal state after:
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 fun a ↦ (AffineEquiv.prodAssoc k P₁ P₂ P₃).toFun a
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:
eta_expand

Goal state after:
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 fun a ↦ (AffineEquiv.prodAssoc k P₁ P₂ P₃).invFun a
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:
eta_expand

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
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 fun a ↦ ((↑f).prod ↑g).toFun a
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).prodMap ↑g).toFun

Tactic:
eta_expand

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
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 fun a ↦ ((↑f).prodMap ↑g).toFun a
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_6
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedRing 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : IsBoundedSMul 𝕜 E
inst✝ : DistribSMul 𝕜 F
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x
c : 𝕜
f : ↥(α →₁ₛ[μ] E)
⊢ SimpleFunc.setToSimpleFunc T (toSimpleFunc (c • f)) = c • SimpleFunc.setToSimpleFunc T (toSimpleFunc f)

Tactic:
← SimpleFunc.setToSimpleFunc_smul T h_add h_smul c (SimpleFunc.integrable f)

Goal state after:
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_6
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedRing 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : IsBoundedSMul 𝕜 E
inst✝ : DistribSMul 𝕜 F
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x
c : 𝕜
f : ↥(α →₁ₛ[μ] E)
⊢ SimpleFunc.setToSimpleFunc T (toSimpleFunc (c • f)) = SimpleFunc.setToSimpleFunc T (c • toSimpleFunc f)
Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure

Goal state before:
pp: X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSingletonClass X
μ : Measure X
f : X → E
s : Set X
hs : s.Countable
hf : Integrable (f ∘ Subtype.val) (Measure.comap Subtype.val μ)
hi : Countable { x // x ∈ s }
⊢ Integrable (fun x ↦ f ↑x) (Measure.comap Subtype.val μ)

pp: case hg
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSingletonClass X
μ : Measure X
f : X → E
s : Set X
hs : s.Countable
hf : Integrable f (Measure.map Subtype.val (Measure.comap Subtype.val μ))
hi : Countable { x // x ∈ s }
⊢ AEStronglyMeasurable f (Measure.map Subtype.val (Measure.comap Subtype.val μ))

pp: case hf
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSingletonClass X
μ : Measure X
f : X → E
s : Set X
hs : s.Countable
hf : Integrable f (Measure.map Subtype.val (Measure.comap Subtype.val μ))
hi : Countable { x // x ∈ s }
⊢ AEMeasurable Subtype.val (Measure.comap Subtype.val μ)

pp: case hs
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSingletonClass X
μ : Measure X
f : X → E
s : Set X
hs : s.Countable
hf : Integrable f (μ.restrict s)
hi : Countable { x // x ∈ s }
⊢ MeasurableSet s

Tactic:
· apply hf

Goal state after:
case hg
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSingletonClass X
μ : Measure X
f : X → E
s : Set X
hs : s.Countable
hf : Integrable f (Measure.map Subtype.val (Measure.comap Subtype.val μ))
hi : Countable { x // x ∈ s }
⊢ AEStronglyMeasurable f (Measure.map Subtype.val (Measure.comap Subtype.val μ))

case hf
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSingletonClass X
μ : Measure X
f : X → E
s : Set X
hs : s.Countable
hf : Integrable f (Measure.map Subtype.val (Measure.comap Subtype.val μ))
hi : Countable { x // x ∈ s }
⊢ AEMeasurable Subtype.val (Measure.comap Subtype.val μ)

case hs
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSingletonClass X
μ : Measure X
f : X → E
s : Set X
hs : s.Countable
hf : Integrable f (μ.restrict s)
hi : Countable { x // x ∈ s }
⊢ MeasurableSet s
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: case pos
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_6
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
inst✝⁴ : NormedDivisionRing 𝕜
inst✝³ : Module 𝕜 E
inst✝² : NormSMulClass 𝕜 E
inst✝¹ : Module 𝕜 F
inst✝ : NormSMulClass 𝕜 F
hT : DominatedFinMeasAdditive μ T C
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x
c : 𝕜
f : α → E
hF : CompleteSpace F
hf : Integrable f μ
⊢ setToFun μ T hT (c • f) = c • (L1.setToL1 hT) (Integrable.toL1 f hf)

Tactic:
setToFun_eq hT (hf.smul c),

Goal state after:
case pos
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_6
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
inst✝⁴ : NormedDivisionRing 𝕜
inst✝³ : Module 𝕜 E
inst✝² : NormSMulClass 𝕜 E
inst✝¹ : Module 𝕜 F
inst✝ : NormSMulClass 𝕜 F
hT : DominatedFinMeasAdditive μ T C
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x
c : 𝕜
f : α → E
hF : CompleteSpace F
hf : Integrable f μ
⊢ (L1.setToL1 hT) (Integrable.toL1 (c • f) ⋯) = c • (L1.setToL1 hT) (Integrable.toL1 f hf)
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: case inl
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
h : IsEmpty ι
⊢ IsOpen[Pi.topologicalSpace] {p | AffineIndependent 𝕜 p}

pp: case inr
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
i₀ : ι
⊢ IsOpen[Pi.topologicalSpace] {p | AffineIndependent 𝕜 p}

Tactic:
· exact isOpen_discrete _

Goal state after:
case inr
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
i₀ : ι
⊢ IsOpen[Pi.topologicalSpace] {p | AffineIndependent 𝕜 p}
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : CompleteSpace 𝕜
V : Type u_1
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace V
inst✝⁵ : IsTopologicalAddGroup V
inst✝⁴ : T2Space V
inst✝³ : Nontrivial V
inst✝² : LocallyCompactSpace V
inst✝¹ : Module 𝕜 V
inst✝ : ContinuousSMul 𝕜 V
⊢ LocallyCompactSpace 𝕜

Tactic:
obtain ⟨v, hv⟩ : ∃ v : V, v ≠ 0 := exists_ne 0

Goal state after:
𝕜 : Type u
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : CompleteSpace 𝕜
V : Type u_1
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace V
inst✝⁵ : IsTopologicalAddGroup V
inst✝⁴ : T2Space V
inst✝³ : Nontrivial V
inst✝² : LocallyCompactSpace V
inst✝¹ : Module 𝕜 V
inst✝ : ContinuousSMul 𝕜 V
v : V
hv : v ≠ 0
⊢ LocallyCompactSpace 𝕜
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : CompleteSpace 𝕜
V : Type u_1
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace V
inst✝⁵ : IsTopologicalAddGroup V
inst✝⁴ : T2Space V
inst✝³ : Nontrivial V
inst✝² : LocallyCompactSpace V
inst✝¹ : Module 𝕜 V
inst✝ : ContinuousSMul 𝕜 V
v : V
hv : v ≠ 0
L : 𝕜 → V := fun t ↦ t • v
⊢ LocallyCompactSpace 𝕜

Tactic:
have : IsClosedEmbedding L := isClosedEmbedding_smul_left hv

Goal state after:
𝕜 : Type u
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : CompleteSpace 𝕜
V : Type u_1
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace V
inst✝⁵ : IsTopologicalAddGroup V
inst✝⁴ : T2Space V
inst✝³ : Nontrivial V
inst✝² : LocallyCompactSpace V
inst✝¹ : Module 𝕜 V
inst✝ : ContinuousSMul 𝕜 V
v : V
hv : v ≠ 0
L : 𝕜 → V := fun t ↦ t • v
this : IsClosedEmbedding L
⊢ LocallyCompactSpace 𝕜
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β → G
hf : AEStronglyMeasurable f (μ.trim hm)
⊢ ∫ (x : β), f x ∂μ = ∫ (x : β), f x ∂μ.trim hm

Tactic:
rw [integral_congr_ae (ae_eq_of_ae_eq_trim hf.ae_eq_mk), integral_congr_ae hf.ae_eq_mk]
  exact integral_trim hm hf.stronglyMeasurable_mk

Goal state after:
Module: Mathlib.Topology.MetricSpace.ThickenedIndicator

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_pos : ∀ (n : ℕ), 0 < δseq n
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
key :
  ∀ (x : α),
    Tendsto (fun i ↦ thickenedIndicatorAux (δseq i) E x) atTop
      (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).indicator (fun x ↦ 1) x))
x : α
⊢ Tendsto (fun i ↦ (thickenedIndicator ⋯ E) x) atTop
    (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).indicator (fun x ↦ 1) x))

Tactic:
rw [show indicator (closure E) (fun _ => (1 : ℝ≥0)) x =
        (indicator (closure E) (fun _ => (1 : ℝ≥0∞)) x).toNNReal
      by refine (congr_fun (comp_indicator_const 1 ENNReal.toNNReal toNNReal_zero) x).symm]

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_pos : ∀ (n : ℕ), 0 < δseq n
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
key :
  ∀ (x : α),
    Tendsto (fun i ↦ thickenedIndicatorAux (δseq i) E x) atTop
      (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).indicator (fun x ↦ 1) x))
x : α
⊢ Tendsto (fun i ↦ (thickenedIndicator ⋯ E) x) atTop
    (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).indicator (fun x ↦ 1) x).toNNReal)