mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Module.Complement

Goal state before:
pp: R : Type u_1
inst✝⁸ : Ring R
E : Type u_2
F : Type u_3
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module R E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : TopologicalSpace F
inst✝² : AddCommGroup F
inst✝¹ : Module R F
inst✝ : ContinuousAdd F
p q : Submodule R E
h : IsTopCompl p q
φ : ↥p →L[R] F
ψ : ↥q →L[R] F
⊢ ofIsTopCompl h φ ψ = φ ∘SL p.projectionOntoL q h + ψ ∘SL q.projectionOntoL p ⋯

Tactic:
by
  ext; simp [ofIsTopCompl]

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator

Goal state before:
pp: case refine_2
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
hfg : MemLp (f + g) p μ
⊢ MemLp g p μ

Tactic:
rw [← Set.indicator_add_eq_right h]

Goal state after:
case refine_2
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
hfg : MemLp (f + g) p μ
⊢ MemLp ((support g).indicator (f + g)) p μ
Module: Mathlib.Topology.Algebra.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
t : TopologicalSpace 𝕜
h₁ : IsTopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
⊢ t = PseudoMetricSpace.toUniformSpace.toTopologicalSpace

Tactic:
refine IsTopologicalAddGroup.ext h₁ inferInstance (le_antisymm ?_ ?_)

Goal state after:
case refine_1
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
t : TopologicalSpace 𝕜
h₁ : IsTopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
⊢ 𝓝 0 ≤ 𝓝 0

case refine_2
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
t : TopologicalSpace 𝕜
h₁ : IsTopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
⊢ 𝓝 0 ≤ 𝓝 0
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:
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.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
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i, ‖m i‖
m₁ m₂ : (i : ι) → E i
i : ι
⊢ ∏ j, update (fun x ↦ max ‖m₁‖ ‖m₂‖) i ‖m₁ - m₂‖ j = ‖m₁ - m₂‖ * max ‖m₁‖ ‖m₂‖ ^ (Fintype.card ι - 1)

Tactic:
rw [prod_update_of_mem (Finset.mem_univ _)]
        simp [card_univ_sdiff]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹³ : NontriviallyNormedField 𝕜
inst✝¹² : CompleteSpace 𝕜
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : IsTopologicalAddGroup E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : ContinuousSMul 𝕜 E
inst✝⁶ : AddCommGroup F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : Module 𝕜 F
inst✝² : ContinuousSMul 𝕜 F
inst✝¹ : T2Space F
inst✝ : FiniteDimensional 𝕜 F
f : E →L[𝕜] F
⊢ IsStrictMap ⇑f

Tactic:
rw [isStrictMap_iff_isQuotientMap_rangeFactorization]

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹³ : NontriviallyNormedField 𝕜
inst✝¹² : CompleteSpace 𝕜
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : IsTopologicalAddGroup E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : ContinuousSMul 𝕜 E
inst✝⁶ : AddCommGroup F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : Module 𝕜 F
inst✝² : ContinuousSMul 𝕜 F
inst✝¹ : T2Space F
inst✝ : FiniteDimensional 𝕜 F
f : E →L[𝕜] F
⊢ IsQuotientMap (rangeFactorization ⇑f)
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: 𝕜 : Type u
ι : Type v
G : Type wG
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
z : G
⊢ ‖ContinuousMultilinearMap.mkPiRing 𝕜 ι z‖ = ‖z‖

Tactic:
by
  rw [ContinuousMultilinearMap.mkPiRing, norm_smulRight, norm_mkPiAlgebra, one_mul]

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

Goal state before:
pp: case neg
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hp_ne_top : p ≠ ∞
μ : Measure β
hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hi : eLpNorm (fun x ↦ f x - y₀) p μ < ∞
hp_zero : ¬p = 0
⊢ Tendsto (fun n ↦ eLpNorm (⇑(approxOn f hf s y₀ h₀ n) - f) p μ) atTop (𝓝 0)

Tactic:
have hp : 0 < p.toReal := toReal_pos hp_zero hp_ne_top

Goal state after:
case neg
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hp_ne_top : p ≠ ∞
μ : Measure β
hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hi : eLpNorm (fun x ↦ f x - y₀) p μ < ∞
hp_zero : ¬p = 0
hp : 0 < p.toReal
⊢ Tendsto (fun n ↦ eLpNorm (⇑(approxOn f hf s y₀ h₀ n) - f) p μ) atTop (𝓝 0)
Module: Mathlib.MeasureTheory.Function.LocallyIntegrable

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

Tactic:
have ab : a ≤ b := xab.1.trans xab.2

Goal state after:
X : Type u_1
E : Type u_6
inst✝⁹ : MeasurableSpace X
inst✝⁸ : TopologicalSpace X
inst✝⁷ : NormedAddCommGroup E
μ : Measure X
inst✝⁶ : BorelSpace X
inst✝⁵ : ConditionallyCompleteLinearOrder X
inst✝⁴ : ConditionallyCompleteLinearOrder E
inst✝³ : OrderTopology X
inst✝² : OrderTopology E
inst✝¹ : SecondCountableTopology E
f : X → E
inst✝ : IsLocallyFiniteMeasure μ
hmono : Monotone f
x : X
U : Set X
hU : U ∈ 𝓝 x
h'U : μ U < ∞
a b : X
xab : x ∈ Icc a b
hab : Icc a b ∈ 𝓝 x
abU : Icc a b ⊆ U
ab : a ≤ b
⊢ IntegrableAtFilter f (𝓝 x) μ
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:
intro h; rw [h]

Goal state after:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f g : ↥(simpleFunc E p μ)
a✝ : α
h : (toSimpleFunc (f + g)) a✝ = ↑(↑↑f + ↑↑g) a✝
⊢ (toSimpleFunc f) a✝ = ↑↑↑f a✝ →
    (toSimpleFunc g) a✝ = ↑↑↑g a✝ →
      ↑(↑↑f + ↑↑g) a✝ = ↑↑↑f a✝ + ↑↑↑g a✝ → ↑(↑↑f + ↑↑g) a✝ = (toSimpleFunc f) a✝ + (toSimpleFunc g) a✝
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✝ : α
h : (toSimpleFunc (f + g)) a✝ = ↑(↑↑f + ↑↑g) a✝
⊢ (toSimpleFunc f) a✝ = ↑↑↑f a✝ →
    (toSimpleFunc g) a✝ = ↑↑↑g a✝ →
      ↑(↑↑f + ↑↑g) a✝ = ↑↑↑f a✝ + ↑↑↑g a✝ → ↑(↑↑f + ↑↑g) a✝ = (toSimpleFunc f) a✝ + (toSimpleFunc g) a✝

Tactic:
intro h; rw [h]

Goal state after:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f g : ↥(simpleFunc E p μ)
a✝ : α
h✝ : (toSimpleFunc (f + g)) a✝ = ↑(↑↑f + ↑↑g) a✝
h : (toSimpleFunc f) a✝ = ↑↑↑f a✝
⊢ (toSimpleFunc g) a✝ = ↑↑↑g a✝ → ↑(↑↑f + ↑↑g) a✝ = ↑↑↑f a✝ + ↑↑↑g a✝ → ↑(↑↑f + ↑↑g) a✝ = ↑↑↑f a✝ + (toSimpleFunc g) a✝
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✝ : α
h✝ : (toSimpleFunc (f + g)) a✝ = ↑(↑↑f + ↑↑g) a✝
h : (toSimpleFunc f) a✝ = ↑↑↑f a✝
⊢ (toSimpleFunc g) a✝ = ↑↑↑g a✝ → ↑(↑↑f + ↑↑g) a✝ = ↑↑↑f a✝ + ↑↑↑g a✝ → ↑(↑↑f + ↑↑g) a✝ = ↑↑↑f a✝ + (toSimpleFunc g) a✝

Tactic:
intro h; rw [h]

Goal state after:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f g : ↥(simpleFunc E p μ)
a✝ : α
h✝¹ : (toSimpleFunc (f + g)) a✝ = ↑(↑↑f + ↑↑g) a✝
h✝ : (toSimpleFunc f) a✝ = ↑↑↑f a✝
h : (toSimpleFunc g) a✝ = ↑↑↑g a✝
⊢ ↑(↑↑f + ↑↑g) a✝ = ↑↑↑f a✝ + ↑↑↑g a✝ → ↑(↑↑f + ↑↑g) a✝ = ↑↑↑f a✝ + ↑↑↑g a✝
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✝ : α
h✝¹ : (toSimpleFunc (f + g)) a✝ = ↑(↑↑f + ↑↑g) a✝
h✝ : (toSimpleFunc f) a✝ = ↑↑↑f a✝
h : (toSimpleFunc g) a✝ = ↑↑↑g a✝
⊢ ↑(↑↑f + ↑↑g) a✝ = ↑↑↑f a✝ + ↑↑↑g a✝ → ↑(↑↑f + ↑↑g) a✝ = ↑↑↑f a✝ + ↑↑↑g a✝

Tactic:
intro h; rw [h]

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

Tactic:
intro h; rw [h]

Goal state after:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : ↥(simpleFunc E p μ)
a✝ : α
h : (toSimpleFunc (-f)) a✝ = ↑(-↑↑f) a✝
⊢ (toSimpleFunc f) a✝ = ↑↑↑f a✝ → ↑(-↑↑f) a✝ = -↑↑↑f a✝ → ↑(-↑↑f) a✝ = -(toSimpleFunc f) a✝
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 : ↥(simpleFunc E p μ)
a✝ : α
h : (toSimpleFunc (-f)) a✝ = ↑(-↑↑f) a✝
⊢ (toSimpleFunc f) a✝ = ↑↑↑f a✝ → ↑(-↑↑f) a✝ = -↑↑↑f a✝ → ↑(-↑↑f) a✝ = -(toSimpleFunc f) a✝

Tactic:
intro h; rw [h]

Goal state after:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : ↥(simpleFunc E p μ)
a✝ : α
h✝ : (toSimpleFunc (-f)) a✝ = ↑(-↑↑f) a✝
h : (toSimpleFunc f) a✝ = ↑↑↑f a✝
⊢ ↑(-↑↑f) a✝ = -↑↑↑f a✝ → ↑(-↑↑f) a✝ = -↑↑↑f a✝
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 : ↥(simpleFunc E p μ)
a✝ : α
h✝ : (toSimpleFunc (-f)) a✝ = ↑(-↑↑f) a✝
h : (toSimpleFunc f) a✝ = ↑↑↑f a✝
⊢ ↑(-↑↑f) a✝ = -↑↑↑f a✝ → ↑(-↑↑f) a✝ = -↑↑↑f a✝

Tactic:
intro h; rw [h]

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

Goal state before:

Tactic:
intro h; rw [h]

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:
intro h; rw [h]

Goal state after:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f g : ↥(simpleFunc E p μ)
a✝ : α
h : (toSimpleFunc (f - g)) a✝ = ↑(↑↑f - ↑↑g) a✝
⊢ (toSimpleFunc f) a✝ = ↑↑↑f a✝ →
    (toSimpleFunc g) a✝ = ↑↑↑g a✝ →
      ↑(↑↑f - ↑↑g) a✝ = ↑↑↑f a✝ - ↑↑↑g a✝ → ↑(↑↑f - ↑↑g) a✝ = (toSimpleFunc f) a✝ - (toSimpleFunc g) a✝
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✝ : α
h : (toSimpleFunc (f - g)) a✝ = ↑(↑↑f - ↑↑g) a✝
⊢ (toSimpleFunc f) a✝ = ↑↑↑f a✝ →
    (toSimpleFunc g) a✝ = ↑↑↑g a✝ →
      ↑(↑↑f - ↑↑g) a✝ = ↑↑↑f a✝ - ↑↑↑g a✝ → ↑(↑↑f - ↑↑g) a✝ = (toSimpleFunc f) a✝ - (toSimpleFunc g) a✝

Tactic:
intro h; rw [h]

Goal state after:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f g : ↥(simpleFunc E p μ)
a✝ : α
h✝ : (toSimpleFunc (f - g)) a✝ = ↑(↑↑f - ↑↑g) a✝
h : (toSimpleFunc f) a✝ = ↑↑↑f a✝
⊢ (toSimpleFunc g) a✝ = ↑↑↑g a✝ → ↑(↑↑f - ↑↑g) a✝ = ↑↑↑f a✝ - ↑↑↑g a✝ → ↑(↑↑f - ↑↑g) a✝ = ↑↑↑f a✝ - (toSimpleFunc g) a✝
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✝ : α
h✝ : (toSimpleFunc (f - g)) a✝ = ↑(↑↑f - ↑↑g) a✝
h : (toSimpleFunc f) a✝ = ↑↑↑f a✝
⊢ (toSimpleFunc g) a✝ = ↑↑↑g a✝ → ↑(↑↑f - ↑↑g) a✝ = ↑↑↑f a✝ - ↑↑↑g a✝ → ↑(↑↑f - ↑↑g) a✝ = ↑↑↑f a✝ - (toSimpleFunc g) a✝

Tactic:
intro h; rw [h]

Goal state after:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f g : ↥(simpleFunc E p μ)
a✝ : α
h✝¹ : (toSimpleFunc (f - g)) a✝ = ↑(↑↑f - ↑↑g) a✝
h✝ : (toSimpleFunc f) a✝ = ↑↑↑f a✝
h : (toSimpleFunc g) a✝ = ↑↑↑g a✝
⊢ ↑(↑↑f - ↑↑g) a✝ = ↑↑↑f a✝ - ↑↑↑g a✝ → ↑(↑↑f - ↑↑g) a✝ = ↑↑↑f a✝ - ↑↑↑g a✝
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✝ : α
h✝¹ : (toSimpleFunc (f - g)) a✝ = ↑(↑↑f - ↑↑g) a✝
h✝ : (toSimpleFunc f) a✝ = ↑↑↑f a✝
h : (toSimpleFunc g) a✝ = ↑↑↑g a✝
⊢ ↑(↑↑f - ↑↑g) a✝ = ↑↑↑f a✝ - ↑↑↑g a✝ → ↑(↑↑f - ↑↑g) a✝ = ↑↑↑f a✝ - ↑↑↑g a✝

Tactic:
intro h; rw [h]

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

Goal state before:
pp: α : Type u_1
E : Type u_4
𝕜 : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
k : 𝕜
f : ↥(simpleFunc E p μ)
a✝ : α
⊢ (toSimpleFunc (k • f)) a✝ = ↑↑(k • ↑f) a✝ →
    (toSimpleFunc f) a✝ = ↑↑↑f a✝ → ↑↑(k • ↑f) a✝ = k • ↑↑↑f a✝ → (toSimpleFunc (k • f)) a✝ = k • (toSimpleFunc f) a✝

Tactic:
intro h; rw [h]

Goal state after:
α : Type u_1
E : Type u_4
𝕜 : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
k : 𝕜
f : ↥(simpleFunc E p μ)
a✝ : α
h : (toSimpleFunc (k • f)) a✝ = ↑↑(k • ↑f) a✝
⊢ (toSimpleFunc f) a✝ = ↑↑↑f a✝ → ↑↑(k • ↑f) a✝ = k • ↑↑↑f a✝ → ↑↑(k • ↑f) a✝ = k • (toSimpleFunc f) a✝
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: α : Type u_1
E : Type u_4
𝕜 : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
k : 𝕜
f : ↥(simpleFunc E p μ)
a✝ : α
h : (toSimpleFunc (k • f)) a✝ = ↑↑(k • ↑f) a✝
⊢ (toSimpleFunc f) a✝ = ↑↑↑f a✝ → ↑↑(k • ↑f) a✝ = k • ↑↑↑f a✝ → ↑↑(k • ↑f) a✝ = k • (toSimpleFunc f) a✝

Tactic:
intro h; rw [h]

Goal state after:
α : Type u_1
E : Type u_4
𝕜 : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
k : 𝕜
f : ↥(simpleFunc E p μ)
a✝ : α
h✝ : (toSimpleFunc (k • f)) a✝ = ↑↑(k • ↑f) a✝
h : (toSimpleFunc f) a✝ = ↑↑↑f a✝
⊢ ↑↑(k • ↑f) a✝ = k • ↑↑↑f a✝ → ↑↑(k • ↑f) a✝ = k • ↑↑↑f a✝
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: α : Type u_1
E : Type u_4
𝕜 : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
k : 𝕜
f : ↥(simpleFunc E p μ)
a✝ : α
h✝ : (toSimpleFunc (k • f)) a✝ = ↑↑(k • ↑f) a✝
h : (toSimpleFunc f) a✝ = ↑↑↑f a✝
⊢ ↑↑(k • ↑f) a✝ = k • ↑↑↑f a✝ → ↑↑(k • ↑f) a✝ = k • ↑↑↑f a✝

Tactic:
intro h; rw [h]

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

Goal state before:
pp: case neg
α : Type u_1
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝² : PartialOrder F
inst✝¹ : IsOrderedAddMonoid F
inst✝ : IsOrderedModule ℝ F
f : α →ₛ F
hf : 0 ≤ᵐ[μ] ⇑f
y : α
hy : ¬0 ≤ f y
⊢ μ (⇑f ⁻¹' {f y}) = 0

Tactic:
← nonpos_iff_eq_zero

Goal state after:
case neg
α : Type u_1
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝² : PartialOrder F
inst✝¹ : IsOrderedAddMonoid F
inst✝ : IsOrderedModule ℝ F
f : α →ₛ F
hf : 0 ≤ᵐ[μ] ⇑f
y : α
hy : ¬0 ≤ f y
⊢ μ (⇑f ⁻¹' {f y}) ≤ 0
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_6
f : β → α → G
s : Set β
b : β
⊢ ∫ (y : α), s.indicator (fun x ↦ f x y) b ∂μ = s.indicator (fun x ↦ ∫ (y : α), f x y ∂μ) b

Tactic:
by_cases hb : b ∈ s <;> simp [hb]

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

Goal state before:
pp: α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
⊢ ‖∫ (a : α), f a ∂μ‖ₑ ≤ ∫⁻ (a : α), ‖f a‖ₑ ∂μ

Tactic:
by
  simp only [integral_eq_setToFun]
  exact (enorm_setToFun_le _ (by simp)).trans (by simp)

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

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u : α → β
l : Filter α
c : β
h✝ : c ≠ 0
h : Tendsto u l (𝓝 c)
⊢ Tendsto (u - fun x ↦ c) l (𝓝 0)

Tactic:
have := h.sub (tendsto_const_nhds (x := c))
    rwa [sub_self] at this

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : NormedField β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
u v : α → β
l : Filter α
inst✝ : OrderTopology β
huv : u ~[l] v
hu : Tendsto u l atBot
⊢ Tendsto v l atBot

Tactic:
by
  convert! tendsto_neg_atTop_atBot.comp (huv.neg.tendsto_atTop <| tendsto_neg_atBot_atTop.comp hu)
  ext
  simp

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 : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), 0 ≤ f' n x
hf'_meas : ∀ (n : ℕ), Integrable (f' n) μ
⊢ Tendsto (fun n ↦ ∫ (x : α), f n x ∂μ) atTop (𝓝 (∫ (x : α), F x ∂μ))

Tactic:
suffices Tendsto (fun n ↦ ∫ x, f' n x ∂μ) atTop (𝓝 (∫ x, (F - f 0) x ∂μ)) by
    simp_rw [f', integral_sub (hf _) (hf _), integral_sub' hF (hf 0),
      tendsto_sub_const_iff] at this
    exact this

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 : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), 0 ≤ f' n x
hf'_meas : ∀ (n : ℕ), Integrable (f' n) μ
⊢ Tendsto (fun n ↦ ∫ (x : α), f' n x ∂μ) atTop (𝓝 (∫ (x : α), (F - f 0) x ∂μ))
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
h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
hμ : μ ≪ μ'
f : ↥(α →₁ₛ[μ] E)
f' : ↥(α →₁ₛ[μ'] E)
h : ↑↑↑f =ᵐ[μ] ↑↑↑f'
⊢ setToL1S T f = setToL1S T f'

Tactic:
refine SimpleFunc.setToSimpleFunc_congr T h_zero h_add (SimpleFunc.integrable f) ?_

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
h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
hμ : μ ≪ μ'
f : ↥(α →₁ₛ[μ] E)
f' : ↥(α →₁ₛ[μ'] E)
h : ↑↑↑f =ᵐ[μ] ↑↑↑f'
⊢ ⇑(toSimpleFunc f) =ᵐ[μ] ⇑(toSimpleFunc f')
Module: Mathlib.Analysis.Normed.Module.RieszLemma

Goal state before:
pp: 𝕜 : Type u_4
inst✝² : RCLike 𝕜
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑F
hF : ∃ x, x ∉ F
r : ℝ
hr : r < 1
⊢ ∃ x₀ ∉ F, ‖x₀‖ = 1 ∧ ∀ y ∈ F, r ≤ ‖x₀ - y‖

Tactic:
by
  obtain ⟨x₀, hx₀, h⟩ := riesz_lemma hFc hF hr
  have hx₀' : x₀ ≠ 0 := by rintro rfl; simp at hx₀
  refine ⟨(‖x₀‖⁻¹ : 𝕜) • x₀, ?_, norm_smul_inv_norm hx₀', ?_⟩
  · rwa [Submodule.smul_mem_iff]
    simpa
  intro y hy
  have h₂ : ‖(‖x₀‖ : 𝕜)⁻¹ • (x₀ - (‖x₀‖ : 𝕜) • y)‖ = ‖x₀‖⁻¹ * ‖x₀ - (‖x₀‖ : 𝕜) • y‖ := by
    rw [norm_smul, norm_inv, norm_algebraMap', norm_norm]
  have h₁ := h ((‖x₀‖ : 𝕜) • y) (F.smul_mem _ hy)
  rwa [← le_inv_mul_iff₀' (by simpa), ← h₂, smul_sub, inv_smul_smul₀] at h₁
  simpa using hx₀'

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.Isometry

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
P : Type u_10
P₂ : Type u_11
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₂
⊢ Injective toAffineMap

Tactic:
rintro ⟨f, _⟩ ⟨g, _⟩ rfl

Goal state after:
𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
P : Type u_10
P₂ : Type u_11
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₂
f : P →ᵃ[𝕜] P₂
norm_map✝¹ : ∀ (x : V), ‖f.linear x‖ = ‖x‖
norm_map✝ : ∀ (x : V), ‖{ toAffineMap := f, norm_map := norm_map✝¹ }.linear x‖ = ‖x‖
⊢ { toAffineMap := f, norm_map := norm_map✝¹ } =
    { toAffineMap := { toAffineMap := f, norm_map := norm_map✝¹ }.toAffineMap, norm_map := norm_map✝ }