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

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
inst✝⁸ : PseudoMetricSpace α✝
inst✝⁷ : PseudoMetricSpace β✝
ι : Type u_3
inst✝⁶ : Fintype ι
α : Type u_4
β : ι → Type u_5
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : (i : ι) → PseudoMetricSpace (β i)
inst✝³ : Zero α
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → SMul α (β i)
inst✝ : ∀ (i : ι), IsBoundedSMul α (β i)
x₁ x₂ : α
y : (i : ι) → β i
⊢ 0 ≤ dist x₁ x₂ * dist y 0

Tactic:
by positivity

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

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
inst✝⁸ : PseudoMetricSpace α✝
inst✝⁷ : PseudoMetricSpace β✝
ι : Type u_3
inst✝⁶ : Fintype ι
α : ι → Type u_4
β : ι → Type u_5
inst✝⁵ : (i : ι) → PseudoMetricSpace (α i)
inst✝⁴ : (i : ι) → PseudoMetricSpace (β i)
inst✝³ : (i : ι) → Zero (α i)
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → SMul (α i) (β i)
inst✝ : ∀ (i : ι), IsBoundedSMul (α i) (β i)
x : (i : ι) → α i
y₁ y₂ : (i : ι) → β i
⊢ 0 ≤ dist x 0 * dist y₁ y₂

Tactic:
by positivity

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

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
inst✝⁸ : PseudoMetricSpace α✝
inst✝⁷ : PseudoMetricSpace β✝
ι : Type u_3
inst✝⁶ : Fintype ι
α : ι → Type u_4
β : ι → Type u_5
inst✝⁵ : (i : ι) → PseudoMetricSpace (α i)
inst✝⁴ : (i : ι) → PseudoMetricSpace (β i)
inst✝³ : (i : ι) → Zero (α i)
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → SMul (α i) (β i)
inst✝ : ∀ (i : ι), IsBoundedSMul (α i) (β i)
x₁ x₂ : (i : ι) → α i
y : (i : ι) → β i
⊢ 0 ≤ dist x₁ x₂ * dist y 0

Tactic:
by positivity

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

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedGroup E
a b : E
⊢ dist b (b * a) = ‖a‖

Tactic:
dist_self_mul_right

Goal state after:
E : Type u_2
inst✝ : SeminormedGroup E
a b : E
⊢ ‖a‖ = ‖a‖
Module: Mathlib.Analysis.Normed.Group.Uniform

Goal state before:
pp: 𝓕 : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : SeminormedGroup E
inst✝² : SeminormedGroup F
inst✝¹ : FunLike 𝓕 E F
inst✝ : MonoidHomClass 𝓕 E F
f : 𝓕
x✝ : ∃ K, AntilipschitzWith K ⇑f
K : ℝ≥0
hK : AntilipschitzWith K ⇑f
⊢ (↑K + 1)⁻¹ > 0

Tactic:
by positivity

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

Goal state before:
pp: 𝓕 : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : SeminormedGroup E
inst✝² : SeminormedGroup F
inst✝¹ : FunLike 𝓕 E F
inst✝ : MonoidHomClass 𝓕 E F
f : 𝓕
x✝ : ∃ c > 0, ∀ (x : E), c * ‖x‖ ≤ ‖f x‖
c : ℝ
hc0 : c > 0
hc : ∀ (x : E), c * ‖x‖ ≤ ‖f x‖
⊢ 0 ≤ c⁻¹

Tactic:
by positivity

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

Goal state before:
pp: case refine_1
𝓕 : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : SeminormedGroup E
inst✝² : SeminormedGroup F
inst✝¹ : FunLike 𝓕 E F
inst✝ : MonoidHomClass 𝓕 E F
f : 𝓕
x✝ : ∃ K, AntilipschitzWith K ⇑f
K : ℝ≥0
hK : AntilipschitzWith K ⇑f
x : E
⊢ (↑K + 1)⁻¹ * ↑K * ‖f x‖ ≤ ‖f x‖

Tactic:
exact mul_le_of_le_one_left (norm_nonneg' (f x)) (by simp [field])

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

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedGroup E
s : Set E
hs : IsBounded s
R₀ : ℝ
hR₀ : ∀ x ∈ s, ‖x‖ ≤ R₀
⊢ max R₀ 1 > 0

Tactic:
by positivity

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

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedGroup E
s : Set E
hs : IsBounded s
R : ℝ
hR₀ : R > 0
hR : ∀ x ∈ s, ‖x‖ ≤ R
⊢ R + 1 > 0

Tactic:
by positivity

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
hf : Isometry f
x y : α
h₁ : edist x y ≠ 0
h₂ : edist x y ≠ ∞
⊢ edist ((Isometry.toDilation f hf) x) ((Isometry.toDilation f hf) y) = ↑1 * edist x y

Tactic:
by simp [hf x y]

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

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝¹ : NormedAddGroup α
f : α → E
inst✝ : One E
hf : HasCompactMulSupport f
K : Set α
hK1 : IsCompact K
hK2 : ∀ x ∉ K, f x = 1
S : ℝ
hS : S > 0
hS' : ∀ x ∈ K, ‖x‖ ≤ S
⊢ 0 < S + 1

Tactic:
by positivity

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

Goal state before:
pp: ι : Type u_4
α : Type u_5
inst✝ : NormedCommRing α
f : ι → α
val✝ : Multiset ι
l : List ι
hl : Multiset.Nodup (Quot.mk (⇑(List.isSetoid ι)) l)
hs : { val := Quot.mk (⇑(List.isSetoid ι)) l, nodup := hl }.Nonempty
⊢ List.map f l ≠ []

Tactic:
simpa using! hs

Goal state after:
Module: Mathlib.Data.Finset.Update

Goal state before:
pp: ι : Type u_2
π : ι → Type u_3
inst✝ : DecidableEq ι
α : Type u_1
f : ((i : ι) → π i) → α
s : Set ι
hf : DependsOn f s
t : Finset ι
y : (i : ↥t) → π ↑i
x₁ x₂ : (i : ι) → π i
h : ∀ i ∈ s \ ↑t, x₁ i = x₂ i
i : ι
hi : i ∈ s
⊢ Function.updateFinset x₁ t y i = Function.updateFinset x₂ t y i

Tactic:
simp only [Function.updateFinset]

Goal state after:
ι : Type u_2
π : ι → Type u_3
inst✝ : DecidableEq ι
α : Type u_1
f : ((i : ι) → π i) → α
s : Set ι
hf : DependsOn f s
t : Finset ι
y : (i : ↥t) → π ↑i
x₁ x₂ : (i : ι) → π i
h : ∀ i ∈ s \ ↑t, x₁ i = x₂ i
i : ι
hi : i ∈ s
⊢ (if hi : i ∈ t then y ⟨i, hi⟩ else x₁ i) = if hi : i ∈ t then y ⟨i, hi⟩ else x₂ i
Module: Mathlib.Analysis.Normed.Field.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : NormedDivisionRing α
s : Set α
hs : sᶜ ∈ 𝓝 0
ε : ℝ
hε : ε > 0
r : ℝ
hr₀ : 0 < r
hr : s ⊆ {a | r ≤ ‖a‖}
hs₀ : ∀ x ∈ s, x ≠ 0
⊢ ε * r ^ 2 > 0

Tactic:
by positivity

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Defs

Goal state before:
pp: α : Type u_1
ι : Sort u_6
m : ι → MeasurableSpace α
⊢ ⨆ n, m n = generateFrom {s | ∃ n, MeasurableSet s}

Tactic:
by
  ext s
  rw [measurableSet_iSup]
  rfl

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

Goal state before:
pp: E : Type u_6
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
⊢ 0 ≤ 2

Tactic:
by positivity

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.Basic

Goal state before:
pp: case inr.refine_2
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ∞
n : ℕ
h' : Monotone s
x : α
this✝ : ∃ i, x ∈ s i
j : ℕ
hj : x ∈ s j
hlt : ∀ m < j, x ∉ s m
hnj : n < j
this : j - (n + 1) + n + 1 = j
⊢ j - (n + 1) + n < j

Tactic:
← Nat.succ_le_iff,

Goal state after:
case inr.refine_2
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ∞
n : ℕ
h' : Monotone s
x : α
this✝ : ∃ i, x ∈ s i
j : ℕ
hj : x ∈ s j
hlt : ∀ m < j, x ∉ s m
hnj : n < j
this : j - (n + 1) + n + 1 = j
⊢ (j - (n + 1) + n).succ ≤ j
Module: Mathlib.MeasureTheory.OuterMeasure.Operations

Goal state before:
pp: α : Type u_1
β : Type u_2
m✝ : OuterMeasure α
R : Type u_3
inst✝³ : SMul R ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
R' : Type u_4
inst✝¹ : SMul R' ℝ≥0∞
inst✝ : IsScalarTower R' ℝ≥0∞ ℝ≥0∞
c : R
m : OuterMeasure α
s t : Set α
h : s ⊆ t
⊢ c • 1 * m s ≤ c • 1 * m t

Tactic:
exact mul_right_mono (m.mono h)

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: δ : Type u_4
X : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (X a)
a : δ
inst✝ : DecidableEq δ
⊢ Measurable fun p ↦ update p.1 a p.2

Tactic:
rw [measurable_pi_iff]

Goal state after:
δ : Type u_4
X : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (X a)
a : δ
inst✝ : DecidableEq δ
⊢ ∀ (a_1 : δ), Measurable fun x ↦ update x.1 a x.2 a_1
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: δ : Type u_4
X : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (X a)
inst✝ : Unique δ
⊢ Measurable uniqueElim

Tactic:
simp_rw [measurable_pi_iff, Unique.forall_iff, uniqueElim_default]; exact measurable_id

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: δ : Type u_4
δ' : Type u_5
X : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (X a)
f : δ' ≃ δ
⊢ Measurable ⇑(Equiv.piCongrLeft X f)

Tactic:
rw [measurable_pi_iff]

Goal state after:
δ : Type u_4
δ' : Type u_5
X : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (X a)
f : δ' ≃ δ
⊢ ∀ (a : δ), Measurable fun x ↦ (Equiv.piCongrLeft X f) x a
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: α : Type u_2
β : Type u_3
F : Type u_4
inst✝⁵ : AddGroupWithOne α
inst✝⁴ : One β
inst✝³ : SubtractionMonoid β
inst✝² : FunLike F α β
inst✝¹ : AddMonoidHomClass F α β
inst✝ : OneHomClass F α β
f : F
s : SignType
⊢ f ↑s = ↑s

Tactic:
apply map_cast'

Goal state after:
case h₁
α : Type u_2
β : Type u_3
F : Type u_4
inst✝⁵ : AddGroupWithOne α
inst✝⁴ : One β
inst✝³ : SubtractionMonoid β
inst✝² : FunLike F α β
inst✝¹ : AddMonoidHomClass F α β
inst✝ : OneHomClass F α β
f : F
s : SignType
⊢ f 1 = 1

case h₂
α : Type u_2
β : Type u_3
F : Type u_4
inst✝⁵ : AddGroupWithOne α
inst✝⁴ : One β
inst✝³ : SubtractionMonoid β
inst✝² : FunLike F α β
inst✝¹ : AddMonoidHomClass F α β
inst✝ : OneHomClass F α β
f : F
s : SignType
⊢ f 0 = 0

case h₃
α : Type u_2
β : Type u_3
F : Type u_4
inst✝⁵ : AddGroupWithOne α
inst✝⁴ : One β
inst✝³ : SubtractionMonoid β
inst✝² : FunLike F α β
inst✝¹ : AddMonoidHomClass F α β
inst✝ : OneHomClass F α β
f : F
s : SignType
⊢ f (-1) = -1
Module: Mathlib.Topology.Algebra.Algebra

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
A : Type u_2
inst✝⁵ : Semiring A
inst✝⁴ : TopologicalSpace A
B : Type u_3
inst✝³ : Semiring B
inst✝² : TopologicalSpace B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f g : A →A[R] B
h : (fun f ↦ ⇑f.toAlgHom) f = (fun f ↦ ⇑f.toAlgHom) g
⊢ f = g

Tactic:
by
    cases f; cases g
    simp only [mk.injEq]
    exact AlgHom.ext (congrFun h)

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
⊢ (if 0 < a then 1 else if a < 0 then -1 else 0) ≤ if 0 < b then 1 else if b < 0 then -1 else 0

Tactic:
split_ifs with h₁ h₂ h₃ h₄ _ _ h₂ h₃ <;> try constructor

Goal state after:
case pos
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
h₁ : 0 < a
h₂ : ¬0 < b
h₃ : b < 0
⊢ 1 ≤ -1

case neg
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
h₁ : 0 < a
h₂ : ¬0 < b
h₃ : ¬b < 0
⊢ 1 ≤ 0

case pos
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
h₁ : ¬0 < a
h₄ : ¬a < 0
h₂ : ¬0 < b
h₃ : b < 0
⊢ 0 ≤ -1
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case coe.inr.inr
a : ℝ
a_pos : 0 < a
⊢ ↑1 * (↑(↑a).abs)⁻¹ = (↑a)⁻¹

Tactic:
SignType.coe_one,

Goal state after:
case coe.inr.inr
a : ℝ
a_pos : 0 < a
⊢ 1 * (↑(↑a).abs)⁻¹ = (↑a)⁻¹
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_1
f g : α → ℝ≥0∞
sf sg : ℝ≥0∞
i : α
h : ∀ (a : α), f a ≤ g a
hi : f i < g i
hsf : sf ≠ ∞
hf : HasSum f sf
hg : HasSum g sg
⊢ sf < sg

Tactic:
by_cases hsg : sg = ∞

Goal state after:
case pos
α : Type u_1
f g : α → ℝ≥0∞
sf sg : ℝ≥0∞
i : α
h : ∀ (a : α), f a ≤ g a
hi : f i < g i
hsf : sf ≠ ∞
hf : HasSum f sf
hg : HasSum g sg
hsg : sg = ∞
⊢ sf < sg

case neg
α : Type u_1
f g : α → ℝ≥0∞
sf sg : ℝ≥0∞
i : α
h : ∀ (a : α), f a ≤ g a
hi : f i < g i
hsf : sf ≠ ∞
hf : HasSum f sf
hg : HasSum g sg
hsg : ¬sg = ∞
⊢ sf < sg
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case coe.inr.inr
a : ℝ
a_pos : 0 < a
⊢ ↑1 * ↑(↑a).abs⁻¹ = (↑a)⁻¹

Tactic:
SignType.coe_one,

Goal state after:
case coe.inr.inr
a : ℝ
a_pos : 0 < a
⊢ 1 * ↑(↑a).abs⁻¹ = (↑a)⁻¹
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: case neg
α : Type u_1
f g : α → ℝ≥0∞
sf sg : ℝ≥0∞
i : α
h : ∀ (a : α), f a ≤ g a
hi : f i < g i
hsf : sf ≠ ∞
hf : HasSum f sf
hg : HasSum g sg
hsg : ¬sg = ∞
⊢ sf < sg

Tactic:
· have hg' : ∀ x, g x ≠ ∞ := ENNReal.ne_top_of_tsum_ne_top (hg.tsum_eq.symm ▸ hsg)
    lift f to α → ℝ≥0 using fun x =>
      ne_of_lt (lt_of_le_of_lt (h x) <| lt_of_le_of_ne le_top (hg' x))
    lift g to α → ℝ≥0 using hg'
    lift sf to ℝ≥0 using hsf
    lift sg to ℝ≥0 using hsg
    simp only [coe_le_coe, coe_lt_coe] at h hi ⊢
    exact NNReal.hasSum_lt h hi (ENNReal.hasSum_coe.1 hf) (ENNReal.hasSum_coe.1 hg)

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: 𝕜 : Type u_4
inst✝⁶ : Semifield 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsStrictOrderedRing 𝕜
inst✝³ : ExistsAddOfLE 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
h₁ : 0 ≤ r
h₂ : r < 1
hr : 0 = r
⊢ Tendsto (fun n ↦ r ^ (n + 1)) atTop (𝓝 0)

Tactic:
by
      simp [_root_.pow_succ, ← hr]

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: m : ℝ
f : ℕ → ℕ
hm : 1 < m
fi : ∀ (i : ℕ), i ≤ f i
a : ℕ
⊢ 0 ≤ 1 / m ^ f a

Tactic:
by positivity

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
ι : Sort u_2
inst✝ : Nonempty ι
m : ι → OuterMeasure α
s : Set α
⊢ ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ μ ∈ range m, μ (t n) =
    ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ i, (m i) (t n)

Tactic:
simp only [iInf_range]

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
ι : Sort u_2
m : ι → OuterMeasure α
s : Set α
hs : s.Nonempty
⊢ ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ μ ∈ range fun i ↦ m i, μ (t n) =
    ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ i, (m i) (t n)

Tactic:
simp only [iInf_range]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
⊢ μ s = μ.trim s

Tactic:
μ.trimmed,

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
⊢ μ s = μ.toOuterMeasure s
Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
⊢ s ⊆ toMeasurable μ s

Tactic:
by
  rw [toMeasurable_def]; split_ifs with hs h's
  exacts [hs.choose_spec.1, h's.choose_spec.1, (exists_measurable_superset μ s).choose_spec.1]

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: case mpr
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
h :
  ∀ (t : Set α),
    P t →
      (inducedOuterMeasure m P0 m0) (t ∩ s) + (inducedOuterMeasure m P0 m0) (t \ s) ≤ (inducedOuterMeasure m P0 m0) t
u t : Set α
ht : P t
⊢ u ⊆ t → (inducedOuterMeasure m P0 m0) (u ∩ s) + (inducedOuterMeasure m P0 m0) (u \ s) ≤ m t ht

Tactic:
intro h2t

Goal state after:
case mpr
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
h :
  ∀ (t : Set α),
    P t →
      (inducedOuterMeasure m P0 m0) (t ∩ s) + (inducedOuterMeasure m P0 m0) (t \ s) ≤ (inducedOuterMeasure m P0 m0) t
u t : Set α
ht : P t
h2t : u ⊆ t
⊢ (inducedOuterMeasure m P0 m0) (u ∩ s) + (inducedOuterMeasure m P0 m0) (u \ s) ≤ m t ht
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
hs : s₁ ⊆ s₂
h₂ : MeasurableSet s₂
⊢ extend m s₁ ≤ m s₂ h₂

Tactic:
have :=
    extend_union MeasurableSet.empty m0 MeasurableSet.iUnion mU disjoint_sdiff_self_right h₁
      (h₂.diff h₁)

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
hs : s₁ ⊆ s₂
h₂ : MeasurableSet s₂
this : extend m (s₁ ∪ s₂ \ s₁) = extend m s₁ + extend m (s₂ \ s₁)
⊢ extend m s₁ ≤ m s₂ h₂
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
π : δ' → Type u_6
π' : δ' → Type u_7
inst✝¹ : (x : δ') → MeasurableSpace (π x)
inst✝ : (x : δ') → MeasurableSpace (π' x)
f : δ ≃ δ'
⊢ Measurable ⇑(Equiv.piCongrLeft π f).symm

Tactic:
rw [measurable_pi_iff]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
π : δ' → Type u_6
π' : δ' → Type u_7
inst✝¹ : (x : δ') → MeasurableSpace (π x)
inst✝ : (x : δ') → MeasurableSpace (π' x)
f : δ ≃ δ'
⊢ ∀ (a : δ), Measurable fun x ↦ (Equiv.piCongrLeft π f).symm x a
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α✝
inst✝⁵ : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
π : δ' → Type u_6
π' : δ' → Type u_7
inst✝² : (x : δ') → MeasurableSpace (π x)
inst✝¹ : (x : δ') → MeasurableSpace (π' x)
α : δ ⊕ δ' → Type u_8
inst✝ : (i : δ ⊕ δ') → MeasurableSpace (α i)
⊢ Measurable ⇑(Equiv.sumPiEquivProdPi α).symm

Tactic:
rw [measurable_pi_iff]

Goal state after:
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α✝
inst✝⁵ : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
π : δ' → Type u_6
π' : δ' → Type u_7
inst✝² : (x : δ') → MeasurableSpace (π x)
inst✝¹ : (x : δ') → MeasurableSpace (π' x)
α : δ ⊕ δ' → Type u_8
inst✝ : (i : δ ⊕ δ') → MeasurableSpace (α i)
⊢ ∀ (a : δ ⊕ δ'), Measurable fun x ↦ (Equiv.sumPiEquivProdPi α).symm x a
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: case refine_1.succ
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n ↦ F^[n] univ
n : ℕ
ih : MeasurableSet (F^[n] univ)
⊢ MeasurableSet (F^[n + 1] univ)

Tactic:
rw [Function.iterate_succ', Function.comp_apply]
      exact (hg.measurableSet_image' (hf.measurableSet_image' ih).compl).compl

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
f : α → β
h : μ ≤ ν
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ (map f μ) s ≤ (map f ν) s

Tactic:
simp [hf.aemeasurable, hs, h _]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Comap

Goal state before:
pp: α : Type u_1
β : Type u_2
ma : MeasurableSpace α
mb : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure β
⊢ Measure.comap f (μ + ν) = Measure.comap f μ + Measure.comap f ν

Tactic:
by
  ext s hs
  simp only [← comapₗ_eq_comap _ hf.injective (fun _ ↦ hf.measurableSet_image.mpr) _ hs,
    map_add, add_apply]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
⊢ μ (s ∪ t) + μ (s ∩ t) = μ s + μ t

Tactic:
by
  rw [union_comm, inter_comm, measure_union_add_inter t hs, add_comm]

Goal state after:
Module: Mathlib.Topology.Order.AtTopBotIxx

Goal state before:
pp: case inr
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s : Set X
b : X
hsb : s ⊆ Iio b
hs : ∀ a' < b, ∃ a < b, Ioo a b ⊆ s
hb : IsSuccPrelimit b
a : X
ha : a ∈ Iio b
⊢ s ∈ 𝓝[<] b

Tactic:
exact (mem_nhdsLT_iff_exists_Ioo_subset' ha).2 (hs a ha)

Goal state after:
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst✝ : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), μ (t i) ≤ μ (s i)
⊢ μ (⋃ i, s i) = μ (⋃ i, t i)

Tactic:
refine le_antisymm (by gcongr; apply hsub) ?_
  by_cases! htop : ∃ i, μ (t i) = ∞
  · rcases htop with ⟨i, hi⟩
    calc
      μ (⋃ i, t i) ≤ ∞ := le_top
      _ ≤ μ (s i) := hi ▸ h_le i
      _ ≤ μ (⋃ i, s i) := measure_mono <| subset_iUnion _ _
  set M := toMeasurable μ
  have H : ∀ b, (M (t b) ∩ M (⋃ b, s b) : Set α) =ᵐ[μ] M (t b) := by
    refine fun b => ae_eq_of_subset_of_measure_ge inter_subset_left ?_ ?_ ?_
    · calc
        μ (M (t b)) = μ (t b) := measure_toMeasurable _
        _ ≤ μ (s b) := h_le b
        _ ≤ μ (M (t b) ∩ M (⋃ b, s b)) :=
          measure_mono <|
            subset_inter ((hsub b).trans <| subset_toMeasurable _ _)
              ((subset_iUnion _ _).trans <| subset_toMeasurable _ _)
    · measurability
    · rw [measure_toMeasurable]
      exact htop b
  calc
    μ (⋃ b, t b) ≤ μ (⋃ b, M (t b)) := measure_mono (iUnion_mono fun b => subset_toMeasurable _ _)
    _ = μ (⋃ b, M (t b) ∩ M (⋃ b, s b)) :=
      measure_congr (Filter.EventuallyEq.countable_iUnion H).symm
    _ ≤ μ (M (⋃ b, s b)) := measure_mono (iUnion_subset fun b => inter_subset_right)
    _ = μ (⋃ b, s b) := measure_toMeasurable _

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
μ ν : Measure α
s t : Set α
a : α
inst✝¹ : SFinite μ
inst✝ : SFinite ν
⊢ SFinite (μ + ν)

Tactic:
by
  have : ∀ b : Bool, SFinite (cond b μ ν) := by simp [*]
  simpa using (inferInstance : SFinite (.sum (cond · μ ν)))

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ ν : Measure α
s t : Set α
a : α
inst✝ : SigmaFinite μ
⊢ SFinite μ

Tactic:
have : ∀ n, Fact (μ (disjointed (spanningSets μ) n) < ∞) :=
    fun n ↦ ⟨(measure_mono (disjointed_subset _ _)).trans_lt (measure_spanningSets_lt_top μ n)⟩
  exact ⟨⟨fun n ↦ μ.restrict (disjointed (spanningSets μ) n), fun n ↦ by infer_instance,
    (sum_restrict_disjointed_spanningSets μ μ).symm⟩⟩

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
ι : Type u_4
x✝ : MeasurableSpace α
μ : Measure α
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) μ
As_disj : Pairwise (AEDisjoint μ on As)
Union_As_finite : μ (⋃ i, As i) ≠ ∞
⊢ {i | 0 < μ (As i)}.Countable

Tactic:
set posmeas := { i : ι | 0 < μ (As i) } with posmeas_def

Goal state after:
α : Type u_1
ι : Type u_4
x✝ : MeasurableSpace α
μ : Measure α
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) μ
As_disj : Pairwise (AEDisjoint μ on As)
Union_As_finite : μ (⋃ i, As i) ≠ ∞
posmeas : Set ι := {i | 0 < μ (As i)}
posmeas_def : posmeas = {i | 0 < μ (As i)}
⊢ posmeas.Countable
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
⊢ μ.restrict s = ν.restrict s ∧ μ.restrict t = ν.restrict t → μ.restrict (s ∪ t) = ν.restrict (s ∪ t)

Tactic:
rintro ⟨hs, ht⟩

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : μ.restrict s = ν.restrict s
ht : μ.restrict t = ν.restrict t
⊢ μ.restrict (s ∪ t) = ν.restrict (s ∪ t)
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
⊢ ∀ (a : α) (u : Set α), a ∈ u → IsOpen[inst✝¹] u → ∃ v ∈ {s | IsOpen[inst✝¹] s ∧ μ s < ∞}, a ∈ v ∧ v ⊆ u

Tactic:
intro x s xs hs

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
x : α
s : Set α
xs : x ∈ s
hs : IsOpen[inst✝¹] s
⊢ ∃ v ∈ {s | IsOpen[inst✝¹] s ∧ μ s < ∞}, x ∈ v ∧ v ⊆ s