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

Goal state before:
pp: case refine_1
α : 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
⊢ ENNReal.ofReal (∫ (x : α), (F - f 0) x ∂μ) ≠ ∞

Tactic:
]

Goal state after:
case refine_1
α : 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
⊢ ENNReal.ofReal (∫ (x : α), (F - f 0) x ∂μ) ≠ ∞
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: case e'_3
α : 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'
⊢ ⇑f + ⇑f' - (g + g') = ⇑f - g + (⇑f' - g')

Tactic:
]

Goal state after:
case e'_3
α : 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'
⊢ ⇑f + ⇑f' - (g + g') = ⇑f - g + (⇑f' - g')
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f : ↥(α →₁ₛ[μ] E)
⊢ MemLp (⇑(Lp.simpleFunc.toSimpleFunc f)) 1 μ

Tactic:
]

Goal state after:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f : ↥(α →₁ₛ[μ] E)
⊢ MemLp (⇑(Lp.simpleFunc.toSimpleFunc f)) 1 μ
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
⊢ (AffineMap.lineMap (↑f p₀) (↑f p₁)) c = (AffineMap.lineMap (↑f p₀) (↑f p₁)) c

Tactic:
]

Goal state after:
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 ↦ ENNReal.ofReal (f' n x)) atTop (𝓝 (ENNReal.ofReal ((F - f 0) x)))

Tactic:
refine (ENNReal.continuous_ofReal.tendsto _).comp ?_

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 - f 0) x))
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₂
inst✝⁵ : TopologicalSpace V
inst✝⁴ : IsTopologicalAddTorsor P
inst✝³ : TopologicalSpace W
inst✝² : IsTopologicalAddTorsor Q
inst✝¹ : TopologicalSpace W₂
inst✝ : IsTopologicalAddTorsor Q₂
f : P →ᴬ[R] Q
⊢ Continuous ⇑↑f

Tactic:
]

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₂
inst✝⁵ : TopologicalSpace V
inst✝⁴ : IsTopologicalAddTorsor P
inst✝³ : TopologicalSpace W
inst✝² : IsTopologicalAddTorsor Q
inst✝¹ : TopologicalSpace W₂
inst✝ : IsTopologicalAddTorsor Q₂
f : P →ᴬ[R] Q
⊢ Continuous ⇑↑f
Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv

Goal state before:
pp: k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
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₂
e : P₁ ≃ᴬ[k] P₂
s : Set P₂
⊢ ⇑e ⁻¹' s = ⇑e ⁻¹' s

Tactic:
]

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

Goal state before:
pp: case refine_1
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module R V
inst✝⁹ : TopologicalSpace P
inst✝⁸ : AddTorsor V P
inst✝⁷ : AddCommGroup W
inst✝⁶ : Module R W
inst✝⁵ : TopologicalSpace Q
inst✝⁴ : AddTorsor W Q
inst✝³ : TopologicalSpace V
inst✝² : IsTopologicalAddTorsor P
inst✝¹ : TopologicalSpace W
inst✝ : IsTopologicalAddTorsor Q
f : P →ᴬ[R] Q
h : f.contLinear = 0
x✝ : V
⊢ ↑0 x✝ = 0 x✝

Tactic:
]

Goal state after:
case refine_1
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module R V
inst✝⁹ : TopologicalSpace P
inst✝⁸ : AddTorsor V P
inst✝⁷ : AddCommGroup W
inst✝⁶ : Module R W
inst✝⁵ : TopologicalSpace Q
inst✝⁴ : AddTorsor W Q
inst✝³ : TopologicalSpace V
inst✝² : IsTopologicalAddTorsor P
inst✝¹ : TopologicalSpace W
inst✝ : IsTopologicalAddTorsor Q
f : P →ᴬ[R] Q
h : f.contLinear = 0
x✝ : V
⊢ ↑0 x✝ = 0 x✝
Module: Mathlib.Topology.Algebra.ContinuousAffineMap

Goal state before:
pp: case refine_2
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module R V
inst✝⁹ : TopologicalSpace P
inst✝⁸ : AddTorsor V P
inst✝⁷ : AddCommGroup W
inst✝⁶ : Module R W
inst✝⁵ : TopologicalSpace Q
inst✝⁴ : AddTorsor W Q
inst✝³ : TopologicalSpace V
inst✝² : IsTopologicalAddTorsor P
inst✝¹ : TopologicalSpace W
inst✝ : IsTopologicalAddTorsor Q
f : P →ᴬ[R] Q
h : (↑f).linear = 0
x✝ : V
⊢ 0 x✝ = 0 x✝

Tactic:
]

Goal state after:
case refine_2
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module R V
inst✝⁹ : TopologicalSpace P
inst✝⁸ : AddTorsor V P
inst✝⁷ : AddCommGroup W
inst✝⁶ : Module R W
inst✝⁵ : TopologicalSpace Q
inst✝⁴ : AddTorsor W Q
inst✝³ : TopologicalSpace V
inst✝² : IsTopologicalAddTorsor P
inst✝¹ : TopologicalSpace W
inst✝ : IsTopologicalAddTorsor Q
f : P →ᴬ[R] Q
h : (↑f).linear = 0
x✝ : V
⊢ 0 x✝ = 0 x✝
Module: Mathlib.Topology.Algebra.ContinuousAffineMap

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

Tactic:
have h₁ : f.contLinear = 0 ↔ (f : P →ᵃ[R] Q).linear = 0 := by
    refine ⟨fun h => ?_, fun h => ?_⟩ <;> ext
    · rw [← coe_contLinear_eq_linear, h]; rfl
    · rw [← coe_linear_eq_coe_contLinear, h]; rfl

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

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module R V
inst✝⁴ : TopologicalSpace P
inst✝³ : AddTorsor V P
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddTorsor P
s : AffineSubspace R P
inst✝ : Nonempty ↥s
⊢ Continuous (Subtype.val ∘ fun p ↦ p.1 +ᵥ p.2)

Tactic:
]

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module R V
inst✝⁴ : TopologicalSpace P
inst✝³ : AddTorsor V P
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddTorsor P
s : AffineSubspace R P
inst✝ : Nonempty ↥s
⊢ Continuous (Subtype.val ∘ fun p ↦ p.1 +ᵥ p.2)
Module: Mathlib.Topology.Algebra.AffineSubspace

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module R V
inst✝⁴ : TopologicalSpace P
inst✝³ : AddTorsor V P
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddTorsor P
s : AffineSubspace R P
inst✝ : Nonempty ↥s
⊢ Continuous (Subtype.val ∘ fun x ↦ x.1 -ᵥ x.2)

Tactic:
]

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module R V
inst✝⁴ : TopologicalSpace P
inst✝³ : AddTorsor V P
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddTorsor P
s : AffineSubspace R P
inst✝ : Nonempty ↥s
⊢ Continuous (Subtype.val ∘ fun x ↦ x.1 -ᵥ x.2)
Module: Mathlib.Topology.Algebra.ContinuousAffineMap

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

Tactic:
]

Goal state after:
case refine_1
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module R V
inst✝⁹ : TopologicalSpace P
inst✝⁸ : AddTorsor V P
inst✝⁷ : AddCommGroup W
inst✝⁶ : Module R W
inst✝⁵ : TopologicalSpace Q
inst✝⁴ : AddTorsor W Q
inst✝³ : TopologicalSpace V
inst✝² : IsTopologicalAddTorsor P
inst✝¹ : TopologicalSpace W
inst✝ : IsTopologicalAddTorsor Q
f : P →ᴬ[R] Q
h₁ : f.contLinear = 0 ↔ (↑f).linear = 0
q : Q
h : f = const R P q
p✝ : P
⊢ ↑(const R P q) p✝ = (AffineMap.const R P q) p✝
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case e'_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, Antitone fun n ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (F x))
this : Tendsto (fun n ↦ ∫ (x : α), -f n x ∂μ) atTop (𝓝 (∫ (x : α), -F x ∂μ))
x✝ : ℕ
⊢ -∫ (a : α), -f x✝ a ∂μ = -∫ (x : α), -f x✝ x ∂μ

Tactic:
]

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

Goal state before:
pp: case inr
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module R V
inst✝⁴ : TopologicalSpace P
inst✝³ : AddTorsor V P
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddTorsor P
inst✝ : T1Space V
s : AffineSubspace R P
x : P
hx : x ∈ ↑s
⊢ IsClosed ((fun x_1 ↦ x_1 -ᵥ x) '' ↑s) ↔ IsClosed (⇑(Homeomorph.vaddConst x).symm '' ↑s)

Tactic:
]

Goal state after:
case inr
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module R V
inst✝⁴ : TopologicalSpace P
inst✝³ : AddTorsor V P
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddTorsor P
inst✝ : T1Space V
s : AffineSubspace R P
x : P
hx : x ∈ ↑s
⊢ IsClosed ((fun x_1 ↦ x_1 -ᵥ x) '' ↑s) ↔ IsClosed (⇑(Homeomorph.vaddConst x).symm '' ↑s)
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case e'_5
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, Antitone fun n ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (F x))
this : Tendsto (fun n ↦ ∫ (x : α), -f n x ∂μ) atTop (𝓝 (∫ (x : α), -F x ∂μ))
⊢ -∫ (a : α), -F a ∂μ = -∫ (x : α), -F x ∂μ

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: R : Type u_1
V : Type u_2
W : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module R V
inst✝⁵ : TopologicalSpace V
inst✝⁴ : AddCommGroup W
inst✝³ : Module R W
inst✝² : TopologicalSpace W
inst✝¹ : IsTopologicalAddGroup V
inst✝ : IsTopologicalAddGroup W
f : V →ᵃ[R] W
h : Continuous f.toFun
⊢ (⇑f.linear + fun x ↦ f 0) = ⇑f.linear + fun x ↦ f 0

Tactic:
]

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

Goal state before:
pp: α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] G)
⊢ (∫⁻ (x : α), ‖(toSimpleFunc f) x‖ₑ ∂μ).toReal = ∑ x ∈ (toSimpleFunc f).range, μ.real (⇑(toSimpleFunc f) ⁻¹' {x}) * ‖x‖

Tactic:
]

Goal state after:
α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] G)
⊢ (∫⁻ (x : α), ‖(toSimpleFunc f) x‖ₑ ∂μ).toReal = ∑ x ∈ (toSimpleFunc f).range, μ.real (⇑(toSimpleFunc f) ⁻¹' {x}) * ‖x‖
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] G)
h_eq : ∀ (a : α), (SimpleFunc.map (fun x ↦ ‖x‖ₑ) (toSimpleFunc f)) a = ‖(toSimpleFunc f) a‖ₑ
⊢ ∑ a ∈ (toSimpleFunc f).range, (‖a‖ₑ * μ (⇑(toSimpleFunc f) ⁻¹' {a})).toReal =
    ∑ x ∈ (toSimpleFunc f).range, (μ (⇑(toSimpleFunc f) ⁻¹' {x})).toReal * ‖x‖

pp: α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] G)
h_eq : ∀ (a : α), (SimpleFunc.map (fun x ↦ ‖x‖ₑ) (toSimpleFunc f)) a = ‖(toSimpleFunc f) a‖ₑ
⊢ ∀ a ∈ (toSimpleFunc f).range, ‖a‖ₑ * μ (⇑(toSimpleFunc f) ⁻¹' {a}) ≠ ∞

Tactic:
]

Goal state after:
α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] G)
h_eq : ∀ (a : α), (SimpleFunc.map (fun x ↦ ‖x‖ₑ) (toSimpleFunc f)) a = ‖(toSimpleFunc f) a‖ₑ
⊢ ∑ a ∈ (toSimpleFunc f).range, (‖a‖ₑ * μ (⇑(toSimpleFunc f) ⁻¹' {a})).toReal =
    ∑ x ∈ (toSimpleFunc f).range, (μ (⇑(toSimpleFunc f) ⁻¹' {x})).toReal * ‖x‖

α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] G)
h_eq : ∀ (a : α), (SimpleFunc.map (fun x ↦ ‖x‖ₑ) (toSimpleFunc f)) a = ‖(toSimpleFunc f) a‖ₑ
⊢ ∀ a ∈ (toSimpleFunc f).range, ‖a‖ₑ * μ (⇑(toSimpleFunc f) ⁻¹' {a}) ≠ ∞
Module: Mathlib.Topology.Algebra.ContinuousAffineMap

Goal state before:
pp: R : Type u_1
S : Type u_2
V : Type u_3
W : Type u_4
Q : Type u_5
inst✝¹⁵ : Ring S
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✝⁶ : Module S W
inst✝⁵ : SMulCommClass R S W
inst✝⁴ : ContinuousConstSMul S W
inst✝³ : AddTorsor W Q
inst✝² : TopologicalSpace Q
inst✝¹ : IsTopologicalAddGroup W
inst✝ : IsTopologicalAddTorsor Q
p : Q × (V →L[R] W)
⊢ p.2 = p.2

Tactic:
]

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

Goal state before:
pp: case e_f
α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] G)
h_eq : ∀ (a : α), (SimpleFunc.map (fun x ↦ ‖x‖ₑ) (toSimpleFunc f)) a = ‖(toSimpleFunc f) a‖ₑ
x : G
⊢ (μ (⇑(toSimpleFunc f) ⁻¹' {x})).toReal * ‖x‖ = (μ (⇑(toSimpleFunc f) ⁻¹' {x})).toReal * ‖x‖

Tactic:
]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf_int : ∀ (n : ℕ), Integrable (f n) μ
hF_int : Integrable F μ
hf_tendsto : Tendsto (fun i ↦ ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
f' : ℕ → α → ℝ≥0∞ := fun n a ↦ ENNReal.ofReal (f n a - f 0 a)
F' : α → ℝ≥0∞ := fun a ↦ ENNReal.ofReal (F a - f 0 a)
i : ℕ
⊢ ENNReal.ofReal (∫ (a : α), f i a ∂μ - ∫ (a : α), f 0 a ∂μ) =
    ENNReal.ofReal (∫ (a : α), f i a ∂μ - ∫ (a : α), f 0 a ∂μ)

pp: case hfi
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf_int : ∀ (n : ℕ), Integrable (f n) μ
hF_int : Integrable F μ
hf_tendsto : Tendsto (fun i ↦ ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
f' : ℕ → α → ℝ≥0∞ := fun n a ↦ ENNReal.ofReal (f n a - f 0 a)
F' : α → ℝ≥0∞ := fun a ↦ ENNReal.ofReal (F a - f 0 a)
i : ℕ
⊢ Integrable (fun a ↦ f i a - f 0 a) μ

pp: case f_nn
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf_int : ∀ (n : ℕ), Integrable (f n) μ
hF_int : Integrable F μ
hf_tendsto : Tendsto (fun i ↦ ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
f' : ℕ → α → ℝ≥0∞ := fun n a ↦ ENNReal.ofReal (f n a - f 0 a)
F' : α → ℝ≥0∞ := fun a ↦ ENNReal.ofReal (F a - f 0 a)
i : ℕ
⊢ 0 ≤ᵐ[μ] fun a ↦ f i a - f 0 a

Tactic:
]

Goal state after:
case hfi
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf_int : ∀ (n : ℕ), Integrable (f n) μ
hF_int : Integrable F μ
hf_tendsto : Tendsto (fun i ↦ ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
f' : ℕ → α → ℝ≥0∞ := fun n a ↦ ENNReal.ofReal (f n a - f 0 a)
F' : α → ℝ≥0∞ := fun a ↦ ENNReal.ofReal (F a - f 0 a)
i : ℕ
⊢ Integrable (fun a ↦ f i a - f 0 a) μ

case f_nn
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf_int : ∀ (n : ℕ), Integrable (f n) μ
hF_int : Integrable F μ
hf_tendsto : Tendsto (fun i ↦ ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
f' : ℕ → α → ℝ≥0∞ := fun n a ↦ ENNReal.ofReal (f n a - f 0 a)
F' : α → ℝ≥0∞ := fun a ↦ ENNReal.ofReal (F a - f 0 a)
i : ℕ
⊢ 0 ≤ᵐ[μ] fun a ↦ f i a - f 0 a
Module: Mathlib.Analysis.Normed.Module.RCLike.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_nonneg : 0 ≤ r
x : E
hx : x ≠ 0
this : ‖x‖ ≠ 0
⊢ ‖(↑r * (↑‖x‖)⁻¹) • x‖ = r

Tactic:
simp [field, norm_smul, r_nonneg, rclike_simps]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.RCLike.Basic

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ z ∈ sphere 0 r, ‖f z‖ ≤ c
z : E
z_zero : z = 0
⊢ ‖f 0‖ ≤ c / r * ‖0‖

Tactic:
]

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ z ∈ sphere 0 r, ‖f z‖ ≤ c
z : E
z_zero : z = 0
⊢ ‖f 0‖ ≤ c / r * ‖0‖
Module: Mathlib.Analysis.Normed.Module.RCLike.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ z ∈ sphere 0 r, ‖f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
⊢ ‖z₁‖ = r

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ z ∈ sphere 0 r, ‖f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
⊢ ‖z₁‖ = r
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: case pos
α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] G)
h_eq : ∀ (a : α), (SimpleFunc.map (fun x ↦ ‖x‖ₑ) (toSimpleFunc f)) a = ‖(toSimpleFunc f) a‖ₑ
x : G
a✝ : x ∈ (toSimpleFunc f).range
hx0 : x = 0
⊢ ‖0‖ₑ * μ (⇑(toSimpleFunc f) ⁻¹' {0}) ≠ ∞

Tactic:
]

Goal state after:
case pos
α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] G)
h_eq : ∀ (a : α), (SimpleFunc.map (fun x ↦ ‖x‖ₑ) (toSimpleFunc f)) a = ‖(toSimpleFunc f) a‖ₑ
x : G
a✝ : x ∈ (toSimpleFunc f).range
hx0 : x = 0
⊢ ‖0‖ₑ * μ (⇑(toSimpleFunc f) ⁻¹' {0}) ≠ ∞