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

Goal state before:
pp: β : Type u_2
inst✝² : PseudoEMetricSpace β
K : ℝ≥0
α : Type u_4
inst✝¹ : EMetricSpace α
inst✝ : Nontrivial α
f : α → β
hf : AntilipschitzWith K f
h₀ : K ≤ 0
⊢ K = 0

Tactic:
rwa [le_zero_iff] at h₀

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

Goal state before:
pp: ι : Type u_5
inst✝² : Fintype ι
α : ι → Type u_3
β : ι → Type u_4
inst✝¹ : (i : ι) → PseudoEMetricSpace (α i)
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
f : (i : ι) → α i → β i
hf : ∀ (i : ι), Isometry (f i)
x y : (i : ι) → α i
⊢ edist (Pi.map f x) (Pi.map f y) = edist x y

Tactic:
simp only [edist_pi_def, (hf _).edist_eq, Pi.map_apply]

Goal state after:
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case inr.refine_1.refine_2
x : ℝ≥0∞
xt : x ≠ ∞
x0 : 0 < x
a b : ℝ≥0∞
ha : (a, b).1 < x
hb : x < (a, b).2
ε : ℝ≥0∞
ε0 : 0 < ε
hε : ε < x - (a, b).1
δ : ℝ≥0
δ0 : 0 < δ
hδ : x + ↑δ < (a, b).2
⊢ x + ↑δ < (a, b).2

Tactic:
exact hδ

Goal state after:
Module: Mathlib.Topology.UniformSpace.AbstractCompletion

Goal state before:
pp: α : Type uα
inst✝³ : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝² : UniformSpace β
pkg' : AbstractCompletion.{vβ, uβ} β
γ : Type uγ
inst✝¹ : UniformSpace γ
f : α → β → γ
inst✝ : CompleteSpace γ
⊢ UniformContinuous (uncurry (Function.curry ((pkg.prod pkg').extend (uncurry f))))

Tactic:
uncurry_curry

Goal state after:
α : Type uα
inst✝³ : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝² : UniformSpace β
pkg' : AbstractCompletion.{vβ, uβ} β
γ : Type uγ
inst✝¹ : UniformSpace γ
f : α → β → γ
inst✝ : CompleteSpace γ
⊢ UniformContinuous ((pkg.prod pkg').extend (uncurry f))
Module: Mathlib.Topology.Algebra.UniformMulAction

Goal state before:
pp: R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst✝⁶ : UniformSpace X
inst✝⁵ : UniformSpace Y
inst✝⁴ : SMul M X
inst✝³ : SMul N X
inst✝² : SMulCommClass M N X
inst✝¹ : UniformContinuousConstSMul M X
inst✝ : UniformContinuousConstSMul N X
m : M
n : N
x : Completion X
hmn : m • n • x = (Completion.map (SMul.smul m) ∘ Completion.map (SMul.smul n)) x
⊢ m • n • x = n • m • x

Tactic:
have hnm : n • m • x = (Completion.map (SMul.smul n) ∘ Completion.map (SMul.smul m)) x := rfl

Goal state after:
R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst✝⁶ : UniformSpace X
inst✝⁵ : UniformSpace Y
inst✝⁴ : SMul M X
inst✝³ : SMul N X
inst✝² : SMulCommClass M N X
inst✝¹ : UniformContinuousConstSMul M X
inst✝ : UniformContinuousConstSMul N X
m : M
n : N
x : Completion X
hmn : m • n • x = (Completion.map (SMul.smul m) ∘ Completion.map (SMul.smul n)) x
hnm : n • m • x = (Completion.map (SMul.smul n) ∘ Completion.map (SMul.smul m)) x
⊢ m • n • x = n • m • x
Module: Mathlib.Topology.MetricSpace.Lipschitz

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
f g : α → ℝ
Kf Kg : ℝ≥0
hf : LipschitzWith Kf f
hg : LipschitzWith Kg g
⊢ LipschitzWith (max Kf Kg) fun x ↦ min (f x) (g x)

Tactic:
by
  simpa only [(· ∘ ·), one_mul] using! lipschitzWith_min.comp (hf.prodMk hg)

Goal state after:
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: ι : Type u_4
u : Filter ι
g : ι → ℝ≥0∞
hg : Tendsto g u (𝓝 0)
f : ι → ℝ≥0∞
b : ℝ≥0∞
hb : ∀ᶠ (n : ι) in u, b ≤ (f + g) n
⊢ b ≤ liminf f u

Tactic:
Filter.le_liminf_iff'

Goal state after:
ι : Type u_4
u : Filter ι
g : ι → ℝ≥0∞
hg : Tendsto g u (𝓝 0)
f : ι → ℝ≥0∞
b : ℝ≥0∞
hb : ∀ᶠ (n : ι) in u, b ≤ (f + g) n
⊢ ∀ y < b, ∀ᶠ (a : ι) in u, y ≤ f a
Module: Mathlib.Topology.MetricSpace.Algebra

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : IsBoundedSMul α β
s : Set (α × β)
hs : IsBounded s
C : ℝ
hC₀ : 0 < C
hC : s ⊆ Metric.ball 0 C
ε : ℝ
hε : ε > 0
x✝¹ x✝ : α × β
a : α
b : β
hab : (a, b) ∈ Metric.ball 0 C
x : α
y : β
hxy : (x, y) ∈ Metric.ball 0 C
h : dist (a, b) (x, y) ≤ ε / (2 * C)
⊢ dist (Function.uncurry (fun x1 x2 ↦ x1 • x2) (a, b)) (Function.uncurry (fun x1 x2 ↦ x1 • x2) (x, y)) ≤ ε

Tactic:
Metric.mem_ball,

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : IsBoundedSMul α β
s : Set (α × β)
hs : IsBounded s
C : ℝ
hC₀ : 0 < C
hC : s ⊆ Metric.ball 0 C
ε : ℝ
hε : ε > 0
x✝¹ x✝ : α × β
a : α
b : β
hab : dist (a, b) 0 < C
x : α
y : β
hxy : dist (x, y) 0 < C
h : dist (a, b) (x, y) ≤ ε / (2 * C)
⊢ dist (Function.uncurry (fun x1 x2 ↦ x1 • x2) (a, b)) (Function.uncurry (fun x1 x2 ↦ x1 • x2) (x, y)) ≤ ε
Module: Mathlib.Analysis.Normed.Order.Lattice

Goal state before:
pp: α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
z x y : α
⊢ ‖x ⊔ z - y ⊔ z‖ ≤ dist x y

Tactic:
dist_eq_norm

Goal state after:
α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
z x y : α
⊢ ‖x ⊔ z - y ⊔ z‖ ≤ ‖x - y‖
Module: Mathlib.Analysis.Normed.Order.Lattice

Goal state before:
pp: α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
⊢ LipschitzWith 1 negPart

Tactic:
simpa [Function.comp] using! lipschitzWith_posPart.comp LipschitzWith.id.neg

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

Goal state before:
pp: α : Type u_4
E : Type u_5
inst✝¹ : SeminormedCommGroup E
inst✝ : PseudoEMetricSpace α
K : ℝ≥0
f : α → E
s : Set α
⊢ LipschitzOnWith K f⁻¹ s ↔ LipschitzOnWith K f s

Tactic:
by
  simp [LipschitzOnWith]

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

Goal state before:
pp: α : Type u_5
β : Type u_6
F : Type u_7
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x y : α
r : ℝ≥0
hxy : nndist x y ≠ 0
hr : nndist (f x) (f y) = r * nndist x y
⊢ ↑(nndist x y) ≠ 0

Tactic:
ENNReal.coe_ne_zero

Goal state after:
α : Type u_5
β : Type u_6
F : Type u_7
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x y : α
r : ℝ≥0
hxy : nndist x y ≠ 0
hr : nndist (f x) (f y) = r * nndist x y
⊢ nndist x y ≠ 0
Module: Mathlib.Data.Prod.TProd

Goal state before:
pp: ι : Type u
α : ι → Type v
i : ι
l : List ι
t : (i : ι) → Set (α i)
f : (i : ι) → α i
h : TProd.mk l f ∈ Set.tprod l t ↔ ∀ (i : ι), i ∈ l → f i ∈ t i
⊢ (f i, TProd.mk l f) ∈ t i ×ˢ Set.tprod l t ↔ ∀ (i_1 : ι), i_1 ∈ {i_2 | i_2 ∈ i :: l} → f i_1 ∈ t i_1

Tactic:
prodMk_mem_set_prod_eq

Goal state after:
ι : Type u
α : ι → Type v
i : ι
l : List ι
t : (i : ι) → Set (α i)
f : (i : ι) → α i
h : TProd.mk l f ∈ Set.tprod l t ↔ ∀ (i : ι), i ∈ l → f i ∈ t i
⊢ f i ∈ t i ∧ TProd.mk l f ∈ Set.tprod l t ↔ ∀ (i_1 : ι), i_1 ∈ {i_2 | i_2 ∈ i :: l} → f i_1 ∈ t i_1
Module: Mathlib.Analysis.Normed.Field.Lemmas

Goal state before:
pp: K : Type u_4
val✝ : NontriviallyNormedField K
h : IsComplete (closedBall 0 1)
u : ℕ → K
hu : CauchySeq u
k : ℝ
hk : k ∈ upperBounds (Set.range fun n ↦ ‖u n‖)
kpos : 0 ≤ k
x : K
hx : k < ‖x‖
hu' : CauchySeq ((fun x_1 ↦ x_1 / x) ∘ u)
n✝ : ℕ
⊢ ‖u n✝‖ / ‖x‖ ≤ 1

Tactic:
rw [div_le_one (kpos.trans_lt hx)]

Goal state after:
K : Type u_4
val✝ : NontriviallyNormedField K
h : IsComplete (closedBall 0 1)
u : ℕ → K
hu : CauchySeq u
k : ℝ
hk : k ∈ upperBounds (Set.range fun n ↦ ‖u n‖)
kpos : 0 ≤ k
x : K
hx : k < ‖x‖
hu' : CauchySeq ((fun x_1 ↦ x_1 / x) ∘ u)
n✝ : ℕ
⊢ ‖u n✝‖ ≤ ‖x‖
Module: Mathlib.MeasureTheory.MeasurableSpace.Basic

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
s : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝² : Zero β
inst✝¹ : MeasurableSingletonClass β
b : β
inst✝ : NeZero b
h : Measurable (s.indicator fun x ↦ b)
⊢ MeasurableSet s

Tactic:
convert! h (MeasurableSet.singleton (0 : β)).compl

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝² : Zero β
inst✝¹ : MeasurableSingletonClass β
b : β
inst✝ : NeZero b
h : Measurable (s.indicator fun x ↦ b)
⊢ s = (s.indicator fun x ↦ b) ⁻¹' {0}ᶜ
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
⊢ diam (sphere x r) = 2 * r

Tactic:
apply le_antisymm
    (diam_mono sphere_subset_closedBall isBounded_closedBall |>.trans <| diam_closedBall hr)

Goal state after:
E : Type u_6
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
⊢ 2 * r ≤ diam (sphere x r)
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedRing 𝕜'
inst✝¹ : NormedAlgebra 𝕜 𝕜'
inst✝ : NormOneClass 𝕜'
x y : 𝕜
⊢ dist ((algebraMap 𝕜 𝕜') x) ((algebraMap 𝕜 𝕜') y) = dist x y

Tactic:
rw [dist_eq_norm, dist_eq_norm, ← map_sub, norm_algebraMap']

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

Goal state before:
pp: case neg
δ : Type u_4
X : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (X a)
p : δ → Prop
inst✝ : DecidablePred p
j : δ
hj : ¬p j
⊢ Measurable fun x ↦ (Equiv.piEquivPiSubtypeProd p X).symm x j

Tactic:
simp only [hj, Equiv.piEquivPiSubtypeProd_symm_apply, dif_neg, not_false_iff]

Goal state after:
case neg
δ : Type u_4
X : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (X a)
p : δ → Prop
inst✝ : DecidablePred p
j : δ
hj : ¬p j
⊢ Measurable fun x ↦ x.2 ⟨j, ⋯⟩
Module: Mathlib.Topology.Algebra.InfiniteSum.Real

Goal state before:
pp: f : ℕ → ℝ
c : ℝ
hf : ∀ (n : ℕ), 0 ≤ f n
h : ∀ (n : ℕ), ∑ i ∈ range n, f i ≤ c
H : Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop atTop
⊢ False

Tactic:
rcases exists_lt_of_tendsto_atTop H 0 c with ⟨n, -, hn⟩

Goal state after:
f : ℕ → ℝ
c : ℝ
hf : ∀ (n : ℕ), 0 ≤ f n
h : ∀ (n : ℕ), ∑ i ∈ range n, f i ≤ c
H : Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop atTop
n : ℕ
hn : c < ∑ i ∈ range n, f i
⊢ False
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
inst✝ : Algebra R A
f : A →A[R] A
⊢ ↑f = AlgHom.id R A ↔ f = ContinuousAlgHom.id R A

Tactic:
← coe_id,

Goal state after:
R : Type u_1
inst✝³ : CommSemiring R
A : Type u_2
inst✝² : Semiring A
inst✝¹ : TopologicalSpace A
inst✝ : Algebra R A
f : A →A[R] A
⊢ ↑f = ↑(ContinuousAlgHom.id R A) ↔ f = ContinuousAlgHom.id R A
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: x y : EReal
⊢ x ≤ y ↔
    sign x < sign y ∨
      sign x = neg ∧ sign y = neg ∧ y.abs ≤ x.abs ∨
        sign x = zero ∧ sign y = zero ∨ sign x = pos ∧ sign y = pos ∧ x.abs ≤ y.abs

Tactic:
constructor
  · intro h
    refine (sign.monotone h).lt_or_eq.imp_right (fun hs => ?_)
    rw [← x.sign_mul_abs, ← y.sign_mul_abs] at h
    cases hy : sign y <;> rw [hs, hy] at h ⊢
    · simp
    · left; simpa using h
    · right; right; simpa using h
  · rintro (h | h | h | h)
    · exact (sign.monotone.reflect_lt h).le
    all_goals rw [← x.sign_mul_abs, ← y.sign_mul_abs]; simp [h]

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: f : ℕ → ℝ≥0
c : ℝ≥0
h : ∀ (n : ℕ), ∑ i ∈ Finset.range n, f i ≤ c
H : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, f i) atTop atTop
⊢ False

Tactic:
rcases exists_lt_of_tendsto_atTop H 0 c with ⟨n, -, hn⟩

Goal state after:
f : ℕ → ℝ≥0
c : ℝ≥0
h : ∀ (n : ℕ), ∑ i ∈ Finset.range n, f i ≤ c
H : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, f i) atTop atTop
n : ℕ
hn : c < ∑ i ∈ Finset.range n, f i
⊢ False
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: 𝕜 : Type u_4
inst✝⁵ : Semifield 𝕜
inst✝⁴ : CharZero 𝕜
inst✝³ : TopologicalSpace 𝕜
inst✝² : ContinuousSMul ℚ≥0 𝕜
inst✝¹ : IsTopologicalSemiring 𝕜
inst✝ : ContinuousInv₀ 𝕜
a b c d : 𝕜
hd : d ≠ 0
⊢ ℕ → 𝕜

Tactic:
exact fun k ↦ (a * (↑k)⁻¹ + c) / (b * (↑k)⁻¹ + d)

Goal state after:
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case inr
α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
h✝ : f.NeBot
u_0 : 0 ≤ limsup u f
h₁ : 0 < limsup u f ∨ limsup v f ≠ ⊤
h₂ : limsup u f ≠ ⊤ ∨ 0 < limsup v f
a : EReal
a_u : a > limsup u f
b : EReal
b_v : b > limsup v f
c : EReal
c_ab : c > a * b
x : α
x_a : u x < a
x_b : v x < b
v_0 : 0 x ≤ v x
hux : 0 ≤ u x
⊢ (u * v) x ≤ a * b

Tactic:
· exact mul_le_mul x_a.le x_b.le v_0 (hux.trans x_a.le)

Goal state after:
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case pos
α : Type u_1
inst✝⁵ : TopologicalSpace α
s : Set α
x : α
γ : Type u_5
inst✝⁴ : AddCommMonoid γ
inst✝³ : LinearOrder γ
inst✝² : IsOrderedAddMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p ↦ p.1 + p.2) (f x, g x)
y : γ
hy : (fun z ↦ f z + g z) x > y
u v : Set γ
u_open : IsOpen[inst✝¹] u
xu : f x ∈ u
v_open : IsOpen[inst✝¹] v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.1 + p.2}
hx₁ : ∃ l, l < f x
z₁ : γ
z₁lt : z₁ < f x
h₁ : Ioc z₁ (f x) ⊆ u
hx₂ : ∃ l, l < g x
z₂ : γ
z₂lt : z₂ < g x
h₂ : Ioc z₂ (g x) ⊆ v
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun x1 x2 ↦ (fun z ↦ f z + g z) x1 > x2) x' y

Tactic:
filter_upwards [hf z₁ z₁lt, hg z₂ z₂lt] with z h₁z h₂z

Goal state after:
α : Type u_1
inst✝⁵ : TopologicalSpace α
s : Set α
x : α
γ : Type u_5
inst✝⁴ : AddCommMonoid γ
inst✝³ : LinearOrder γ
inst✝² : IsOrderedAddMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p ↦ p.1 + p.2) (f x, g x)
y : γ
hy : (fun z ↦ f z + g z) x > y
u v : Set γ
u_open : IsOpen[inst✝¹] u
xu : f x ∈ u
v_open : IsOpen[inst✝¹] v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.1 + p.2}
hx₁ : ∃ l, l < f x
z₁ : γ
z₁lt : z₁ < f x
h₁ : Ioc z₁ (f x) ⊆ u
hx₂ : ∃ l, l < g x
z₂ : γ
z₂lt : z₂ < g x
h₂ : Ioc z₂ (g x) ⊆ v
z : α
h₁z : f z > z₁
h₂z : g z > z₂
⊢ f z + g z > y
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: r : ℝ≥0∞
h : Tendsto (fun n ↦ r ^ n) atTop (𝓝 0)
⊢ r < 1

Tactic:
lift r to NNReal

Goal state after:
r : ℝ≥0∞
h : Tendsto (fun n ↦ r ^ n) atTop (𝓝 0)
⊢ r ≠ ∞

r : ℝ≥0
h : Tendsto (fun n ↦ ↑r ^ n) atTop (𝓝 0)
⊢ ↑r < 1
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: case refine_1
α : Type u_1
m : Set (OuterMeasure α)
s : Set α
μ : OuterMeasure α
hμ : μ ∈ m
⊢ (sInf m) s ≤ μ s

Tactic:
apply sInf_le hμ

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
m : MeasurableSpace α
C : (s : Set α) → MeasurableSet s → Prop
s : Set (Set α)
h_eq : m = generateFrom s
h_inter : IsPiSystem s
empty : C ∅ ⋯
basic : ∀ (t : Set α) (ht : t ∈ s), C t ⋯
compl : ∀ (t : Set α) (htm : MeasurableSet t), C t htm → C tᶜ ⋯
iUnion :
  ∀ (f : ℕ → Set α),
    Pairwise (Disjoint on f) → ∀ (hfm : ∀ (i : ℕ), MeasurableSet (f i)), (∀ (i : ℕ), C (f i) ⋯) → C (⋃ i, f i) ⋯
⊢ MeasurableSet = DynkinSystem.GenerateHas s

Tactic:
rw [h_eq, DynkinSystem.generateFrom_eq h_inter]

Goal state after:
α : Type u_3
m : MeasurableSpace α
C : (s : Set α) → MeasurableSet s → Prop
s : Set (Set α)
h_eq : m = generateFrom s
h_inter : IsPiSystem s
empty : C ∅ ⋯
basic : ∀ (t : Set α) (ht : t ∈ s), C t ⋯
compl : ∀ (t : Set α) (htm : MeasurableSet t), C t htm → C tᶜ ⋯
iUnion :
  ∀ (f : ℕ → Set α),
    Pairwise (Disjoint on f) → ∀ (hfm : ∀ (i : ℕ), MeasurableSet (f i)), (∀ (i : ℕ), C (f i) ⋯) → C (⋃ i, f i) ⋯
⊢ MeasurableSet = DynkinSystem.GenerateHas s
Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous

Goal state before:
pp: α : Type u_1
ι : Type u_4
mα : MeasurableSpace α
ν : Measure α
μs : ι → Measure α
i : ι
hνμ : ν ≪ μs i
s : Set α
hs : MeasurableSet s
hs0 : (sum μs) s = 0
⊢ ν s = 0

Tactic:
simp only [sum_apply _ hs, ENNReal.tsum_eq_zero] at hs0

Goal state after:
α : Type u_1
ι : Type u_4
mα : MeasurableSpace α
ν : Measure α
μs : ι → Measure α
i : ι
hνμ : ν ≪ μs i
s : Set α
hs : MeasurableSet s
hs0 : ∀ (i : ι), (μs i) s = 0
⊢ ν s = 0
Module: Mathlib.MeasureTheory.Measure.Comap

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s t : Set α
hst : s =ᵐ[comap f μ] t
⊢ f '' s =ᵐ[μ] f '' t

Tactic:
EventuallyEq,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s t : Set α
hst : ∀ᵐ (x : α) ∂comap f μ, s x = t x
⊢ ∀ᵐ (x : β) ∂μ, (f '' s) x = (f '' t) x
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : Disjoint s t
hs : MeasurableSet s
⊢ μ.restrict (s ∪ t) = μ.restrict s + μ.restrict t

Tactic:
by
  rw [union_comm, restrict_union h.symm hs, add_comm]

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S : Set (Set α)
hc : S.Countable
hs : ⋃₀ S = univ
⊢ ⋃ i ∈ S, i = univ

Tactic:
by rwa [← sUnion_eq_biUnion]

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

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
hm : m ≤ m0
⊢ μ.trim hm ≪ ν.trim hm

Tactic:
refine Measure.AbsolutelyContinuous.mk (fun s hs hsν ↦ ?_)
  rw [trim_measurableSet_eq hm hs] at hsν ⊢
  exact hμν hsν

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

Goal state before:
pp: α : Type u_2
δ : Type u_4
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
f g : α → δ
⊢ f =ᵐ[μ.restrict (⋃ i, s i)] g ↔ ∀ (i : ι), f =ᵐ[μ.restrict (s i)] g

Tactic:
EventuallyEq,

Goal state after:
α : Type u_2
δ : Type u_4
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
f g : α → δ
⊢ (∀ᵐ (x : α) ∂μ.restrict (⋃ i, s i), f x = g x) ↔ ∀ (i : ι), ∀ᵐ (x : α) ∂μ.restrict (s i), f x = g x
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
δ : Type u_4
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
s : ι → Set α
t : Set ι
ht : t.Countable
f g : α → δ
⊢ f =ᶠ[⨆ i ∈ t, ae (μ.restrict (s i))] g ↔ ∀ i ∈ t, f =ᵐ[μ.restrict (s i)] g

Tactic:
EventuallyEq,

Goal state after:
α : Type u_2
δ : Type u_4
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
s : ι → Set α
t : Set ι
ht : t.Countable
f g : α → δ
⊢ (∀ᶠ (x : α) in ⨆ i ∈ t, ae (μ.restrict (s i)), f x = g x) ↔ ∀ i ∈ t, ∀ᵐ (x : α) ∂μ.restrict (s i), f x = g x
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : f =ᵐ[μ.restrict sᶜ] fun x ↦ b
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
⊢ μ (f ⁻¹' t) = μ (f ⁻¹' t ∩ s)

Tactic:
EventuallyEq,

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : ∀ᵐ (x : α) ∂μ.restrict sᶜ, f x = b
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
⊢ μ (f ⁻¹' t) = μ (f ⁻¹' t ∩ s)
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
⊢ ∃ b, b.Countable ∧ inst✝¹ = generateFrom b

Tactic:
refine ⟨⋃ y, {measurableAtom y}, countable_iUnion (fun i ↦ countable_singleton _), ?_⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
⊢ inst✝¹ = generateFrom (⋃ y, {measurableAtom y})
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case inl
β : Type u_2
α : Type u_3
γ : Type u_4
inst✝ : MeasurableSpace γ
h : Countable (α × β)
⊢ CountableOrCountablyGenerated (β × α) γ

pp: case inr
β : Type u_2
α : Type u_3
γ : Type u_4
inst✝ : MeasurableSpace γ
h : CountablyGenerated γ
⊢ CountableOrCountablyGenerated (β × α) γ

Tactic:
· refine ⟨Or.inl countable_prod_swap⟩

Goal state after:
case inr
β : Type u_2
α : Type u_3
γ : Type u_4
inst✝ : MeasurableSpace γ
h : CountablyGenerated γ
⊢ CountableOrCountablyGenerated (β × α) γ
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: case mpr
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
μ : Measure α
inst✝ : Zero β
s : Set α
hs : MeasurableSet s
h : AEMeasurable f (μ.restrict s)
⊢ AEMeasurable (s.indicator f) μ

Tactic:
refine ⟨indicator s (h.mk f), h.measurable_mk.indicator hs, ?_⟩

Goal state after:
case mpr
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
μ : Measure α
inst✝ : Zero β
s : Set α
hs : MeasurableSet s
h : AEMeasurable f (μ.restrict s)
⊢ s.indicator f =ᵐ[μ] s.indicator (AEMeasurable.mk f h)
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
ι : Type u_8
ι' : Type u_9
f : ι → ι'
hf : Injective f
m : ι → Measure α
⊢ sum (Function.extend f m 0) = sum m

Tactic:
by
  ext s hs
  simp [*, Function.apply_extend (fun μ : Measure α ↦ μ s)]

Goal state after:
Module: Mathlib.Topology.Separation.GDelta

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : T1Space X
hs : s.Countable
⊢ IsGδ sᶜ

Tactic:
← biUnion_of_singleton s,

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : T1Space X
hs : s.Countable
⊢ IsGδ (⋃ x ∈ s, {x})ᶜ
Module: Mathlib.Topology.Separation.GDelta

Goal state before:
pp: case inr
X : Type u_1
inst✝¹ : TopologicalSpace X
s t : Set X
inst✝ : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed[inst✝¹] t
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen[inst✝¹] t
T_count : T.Countable
T_int : t = ⋂₀ T
T_nonempty : T.Nonempty
g : ℕ → ↑T
g_surj : Surjective g
g' : ℕ → Set X
g'_open : ∀ (n : ℕ), IsOpen[inst✝¹] (g' n)
clt_sub_g' : ∀ (n : ℕ), t ⊆ g' n
clg'_sub_g : ∀ (n : ℕ), closure[inst✝¹] (g' n) ⊆ ↑(g n)
clg'_int : t = ⋂ i, closure[inst✝¹] (g' i)
⊢ HasSeparatingCover s t

Tactic:
use fun n ↦ (closure (g' n))ᶜ

Goal state after:
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
s t : Set X
inst✝ : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed[inst✝¹] t
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen[inst✝¹] t
T_count : T.Countable
T_int : t = ⋂₀ T
T_nonempty : T.Nonempty
g : ℕ → ↑T
g_surj : Surjective g
g' : ℕ → Set X
g'_open : ∀ (n : ℕ), IsOpen[inst✝¹] (g' n)
clt_sub_g' : ∀ (n : ℕ), t ⊆ g' n
clg'_sub_g : ∀ (n : ℕ), closure[inst✝¹] (g' n) ⊆ ↑(g n)
clg'_int : t = ⋂ i, closure[inst✝¹] (g' i)
⊢ s ⊆ ⋃ n, (fun n ↦ (closure[inst✝¹] (g' n))ᶜ) n ∧
    ∀ (n : ℕ),
      IsOpen[inst✝¹] ((fun n ↦ (closure[inst✝¹] (g' n))ᶜ) n) ∧
        Disjoint (closure[inst✝¹] ((fun n ↦ (closure[inst✝¹] (g' n))ᶜ) n)) t
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: α : Type u_1
s : Set α
inst✝³ : TopologicalSpace α
mα : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
h : s.OrdConnected
u : Set α := ⋃ x ∈ s, ⋃ y ∈ s, Ioo x y
huopen : IsOpen[inst✝³] u
humeas : MeasurableSet u
hfinite : (s \ u).Finite
⊢ MeasurableSet s

Tactic:
have : u ⊆ s := iUnion₂_subset fun x hx => iUnion₂_subset fun y hy =>
    Ioo_subset_Icc_self.trans (h.out hx hy)

Goal state after:
α : Type u_1
s : Set α
inst✝³ : TopologicalSpace α
mα : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
h : s.OrdConnected
u : Set α := ⋃ x ∈ s, ⋃ y ∈ s, Ioo x y
huopen : IsOpen[inst✝³] u
humeas : MeasurableSet u
hfinite : (s \ u).Finite
this : u ⊆ s
⊢ MeasurableSet s