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

Goal state before:
pp: α : Type u_1
K : Type u_4
inst✝² : CommGroupWithZero K
inst✝¹ : TopologicalSpace K
f g : α → K
inst✝ : SeparatelyContinuousMul K
c : K
hc : HasProd f c
s : Finset α
hs : ∀ a ∈ s, f a ≠ 0
hs' : ∀ a ∉ s, f a = g a
t : Finset α
ht : s ⊆ t
⊢ (((∏ i ∈ s, f i) * ∏ i ∈ t \ s, g i) * ∏ i ∈ s, g i) / ∏ i ∈ s, f i = (∏ i ∈ s, g i) * ∏ i ∈ t \ s, g i

Tactic:
← div_mul_eq_mul_div,

Goal state after:
α : Type u_1
K : Type u_4
inst✝² : CommGroupWithZero K
inst✝¹ : TopologicalSpace K
f g : α → K
inst✝ : SeparatelyContinuousMul K
c : K
hc : HasProd f c
s : Finset α
hs : ∀ a ∈ s, f a ≠ 0
hs' : ∀ a ∉ s, f a = g a
t : Finset α
ht : s ⊆ t
⊢ (((∏ i ∈ s, f i) * ∏ i ∈ t \ s, g i) / ∏ i ∈ s, f i) * ∏ i ∈ s, g i = (∏ i ∈ s, g i) * ∏ i ∈ t \ s, g i
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: α : Type u_1
K : Type u_4
inst✝² : CommGroupWithZero K
inst✝¹ : TopologicalSpace K
f g : α → K
inst✝ : SeparatelyContinuousMul K
c : K
hc : HasProd f c
s : Finset α
hs : ∀ a ∈ s, f a ≠ 0
hs' : ∀ a ∉ s, f a = g a
t : Finset α
ht : s ⊆ t
⊢ (((∏ i ∈ s, f i) * ∏ i ∈ t \ s, g i) / ∏ i ∈ s, f i) * ∏ i ∈ s, g i = (∏ i ∈ s, g i) * ∏ i ∈ t \ s, g i

Tactic:
← div_mul_eq_mul_div,

Goal state after:
α : Type u_1
K : Type u_4
inst✝² : CommGroupWithZero K
inst✝¹ : TopologicalSpace K
f g : α → K
inst✝ : SeparatelyContinuousMul K
c : K
hc : HasProd f c
s : Finset α
hs : ∀ a ∈ s, f a ≠ 0
hs' : ∀ a ∉ s, f a = g a
t : Finset α
ht : s ⊆ t
⊢ (((∏ i ∈ s, f i) / ∏ i ∈ s, f i) * ∏ i ∈ t \ s, g i) * ∏ i ∈ s, g i = (∏ i ∈ s, g i) * ∏ i ∈ t \ s, g i
Module: Mathlib.Topology.MetricSpace.Isometry

Goal state before:
pp: F : Type u_1
ι : Type u_2
α : Type u
β : Type v
γ : Type w
inst✝⁵ : PseudoEMetricSpace α
inst✝⁴ : PseudoEMetricSpace β
inst✝³ : PseudoEMetricSpace γ
ι' : Type u_3
inst✝² : Fintype ι
inst✝¹ : Fintype ι'
Y : ι → Type u_4
inst✝ : (j : ι) → PseudoEMetricSpace (Y j)
e : ι ≃ ι'
x1 x2 : (i : ι) → Y i
⊢ ⨆ b, edist ((Equiv.piCongrLeft' Y e).toFun x1 b) ((Equiv.piCongrLeft' Y e).toFun x2 b) = ⨆ b, edist (x1 b) (x2 b)

Tactic:
exact (Equiv.iSup_comp (g := fun b ↦ edist (x1 b) (x2 b)) e.symm)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
L : SummationFilter β
inst✝³ : AddCommMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : StarAddMonoid α
inst✝ : ContinuousStar α
f : β → α
hf : Summable (fun b ↦ Star.star (f b)) L
⊢ Summable f L

Tactic:
by
  simpa only [star_star] using hf.star

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

Goal state before:
pp: b : ℝ≥0
x✝ : ∞ ≠ ∞ ∨ ↑b ≠ ∞
⊢ ∀ (x : ℝ≥0), ∀ᶠ (a : ℝ≥0∞ × ℝ≥0∞) in 𝓝 (∞, ↑b), ↑x < a.1 - a.2

Tactic:
refine fun x => ((lt_mem_nhds <| @coe_lt_top (b + 1 + x)).prod_nhds
      (ge_mem_nhds <| coe_lt_coe.2 <| lt_add_one b)).mono fun y hy => ?_

Goal state after:
b : ℝ≥0
x✝ : ∞ ≠ ∞ ∨ ↑b ≠ ∞
x : ℝ≥0
y : ℝ≥0∞ × ℝ≥0∞
hy : ↑(b + 1 + x) < y.1 ∧ y.2 ≤ ↑(b + 1)
⊢ ↑x < y.1 - y.2
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: a : ℝ≥0
x✝ : ↑a ≠ ∞ ∨ ∞ ≠ ∞
⊢ Tendsto (fun p ↦ p.1 - p.2) (𝓝 (↑a, ∞)) (𝓝 (↑a - ∞))

Tactic:
rw [sub_top]

Goal state after:
a : ℝ≥0
x✝ : ↑a ≠ ∞ ∨ ∞ ≠ ∞
⊢ Tendsto (fun p ↦ p.1 - p.2) (𝓝 (↑a, ∞)) (𝓝 0)
Module: Mathlib.Topology.Metrizable.Uniformity

Goal state before:
pp: case refine_2
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 := fun x y ↦ if h : ∃ n, (x, y) ∉ U n then (1 / 2) ^ Nat.find h else 0
hd₀ : ∀ {x y : X}, d x y = 0 ↔ Inseparable x y
hd_symm : ∀ (x y : X), d x y = d y x
hr : ↑0 < ↑(1 / 2) ∧ ↑(1 / 2) < ↑1
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ ↑(d x y)
hle_d : ∀ {x y : X} {n : ℕ}, (1 / 2) ^ n ≤ d x y ↔ (x, y) ∉ U n
hd_le : ∀ (x y : X), ↑(d x y) ≤ 2 * dist x y
⊢ ∀ (i' : ℕ), True → ∃ i, True ∧ {p | dist p.1 p.2 < ↑(1 / 2) ^ i} ⊆ U i'

Tactic:
refine fun n _ => ⟨n + 1, trivial, fun x hx => ?_⟩
    rw [mem_ofPred_eq] at hx
    contrapose! hx
    refine le_trans ?_ ((div_le_iff₀' zero_lt_two).2 (hd_le x.1 x.2))
    rwa [← NNReal.coe_two, ← NNReal.coe_div, ← NNReal.coe_pow, NNReal.coe_le_coe, pow_succ,
      mul_one_div, div_le_iff₀ zero_lt_two, div_mul_cancel₀ _ two_ne_zero, hle_d]

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

Goal state before:
pp: α : Type u_2
inst✝ : NontriviallyNormedField α
x : α
⊢ (𝓝[≠] x).NeBot

Tactic:
← mem_closure_iff_nhdsWithin_neBot,

Goal state after:
α : Type u_2
inst✝ : NontriviallyNormedField α
x : α
⊢ x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {x}ᶜ
Module: Mathlib.Topology.MetricSpace.Dilation

Goal state before:
pp: α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x y : α
⊢ edist (f x) (f y) = ↑(if ∀ (x y : α), edist x y = 0 ∨ edist x y = ∞ then 1 else ⋯.choose) * edist x y

Tactic:
split_ifs with key

Goal state after:
case pos
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x y : α
key : ∀ (x y : α), edist x y = 0 ∨ edist x y = ∞
⊢ edist (f x) (f y) = ↑1 * edist x y

case neg
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x y : α
key : ¬∀ (x y : α), edist x y = 0 ∨ edist x y = ∞
⊢ edist (f x) (f y) = ↑⋯.choose * edist x y
Module: Mathlib.Analysis.Normed.MulAction

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : NonUnitalSeminormedRing α
x y₁ y₂ : α
⊢ dist (x • y₁) (x • y₂) ≤ dist x 0 * dist y₁ y₂

Tactic:
by simpa [mul_sub, dist_eq_norm] using norm_mul_le x (y₁ - y₂)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f g : α → β
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSingletonClass α
hf : Measurable f
h : {x | f x ≠ g x}.Countable
⊢ Measurable g

Tactic:
intro t ht
  have : g ⁻¹' t = g ⁻¹' t ∩ { x | f x = g x }ᶜ ∪ g ⁻¹' t ∩ { x | f x = g x } := by
    simp [← inter_union_distrib_left]
  rw [this]
  refine (h.mono inter_subset_right).measurableSet.union ?_
  have : g ⁻¹' t ∩ { x : α | f x = g x } = f ⁻¹' t ∩ { x : α | f x = g x } := by
    ext x
    simp +contextual
  rw [this]
  exact (hf ht).inter h.measurableSet.of_compl

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

Goal state before:
pp: case inl
𝕜 : Type u_1
𝕜' : Type u_2
E✝ : Type u_3
F : Type u_4
α : Type u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : SeminormedAddCommGroup E✝
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 E✝
inst✝² : NormedSpace 𝕜 F
E : Type u_6
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℚ E
this : IsAddTorsionFree E
⊢ DiscreteTopology ↥(AddSubgroup.zmultiples 0)

pp: case inr
𝕜 : Type u_1
𝕜' : Type u_2
E✝ : Type u_3
F : Type u_4
α : Type u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : SeminormedAddCommGroup E✝
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 E✝
inst✝² : NormedSpace 𝕜 F
E : Type u_6
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℚ E
e : E
this : IsAddTorsionFree E
he : e ≠ 0
⊢ DiscreteTopology ↥(AddSubgroup.zmultiples e)

Tactic:
· rw [AddSubgroup.zmultiples_zero_eq_bot]
    exact Subsingleton.discreteTopology (α := ↑(⊥ : Subspace ℚ E))

Goal state after:
case inr
𝕜 : Type u_1
𝕜' : Type u_2
E✝ : Type u_3
F : Type u_4
α : Type u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : SeminormedAddCommGroup E✝
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 E✝
inst✝² : NormedSpace 𝕜 F
E : Type u_6
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℚ E
e : E
this : IsAddTorsionFree E
he : e ≠ 0
⊢ DiscreteTopology ↥(AddSubgroup.zmultiples e)
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s t u : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hsu : MeasurableSet (Subtype.val ⁻¹' u)
htu : MeasurableSet (Subtype.val ⁻¹' u)
⊢ MeasurableSet u

Tactic:
by
  convert! (hs.subtype_image hsu).union (ht.subtype_image htu)
  simp [image_preimage_eq_inter_range, ← inter_union_distrib_left, univ_subset_iff.1 h]

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

Goal state before:
pp: α : Type u_1
m₁ m₂ : OuterMeasure α
s : Set α
this : ((bif true then m₁ else m₂) ⊔ bif false then m₁ else m₂) s = ⨆ i, (bif i then m₁ else m₂) s
⊢ (m₁ ⊔ m₂) s = max (m₁ s) (m₂ s)

Tactic:
iSup_bool_eq

Goal state after:
α : Type u_1
m₁ m₂ : OuterMeasure α
s : Set α
this :
  ((bif true then m₁ else m₂) ⊔ bif false then m₁ else m₂) s =
    max ((bif true then m₁ else m₂) s) ((bif false then m₁ else m₂) s)
⊢ (m₁ ⊔ m₂) s = max (m₁ s) (m₂ s)
Module: Mathlib.MeasureTheory.OuterMeasure.Operations

Goal state before:
pp: α : Type u_1
β : Type u_3
f : α → β
m : OuterMeasure β
s : Set β
⊢ f '' f ⁻¹' s = Subtype.val '' Subtype.val ⁻¹' s

Tactic:
simp only [image_preimage_eq_inter_range, Subtype.range_coe]

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

Goal state before:
pp: case hf
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ (fun i ↦ ↑(d i)) n
hd : Summable fun i ↦ ↑(d i)
⊢ ∀ (n : ℕ), edist (f n) (f n.succ) ≤ ↑(d n)

Tactic:
exact_mod_cast hf

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSingletonClass β
f : α → β
hf : Measurable f
a : β
⊢ Measurable fun x ↦ a = f x

Tactic:
conv => enter [1, x]; rw [eq_comm]
  exact .eq_const hf a

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
⊢ sign a = sign b ∨ sign a = -sign b

Tactic:
rcases trichotomy (sign a) with hsa | hsa | hsa <;>
    rcases trichotomy (sign b) with hsb | hsb | hsb

Goal state after:
case inl.inl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : sign a = -1
hsb : sign b = -1
⊢ sign a = sign b ∨ sign a = -sign b

case inl.inr.inl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : sign a = -1
hsb : sign b = 0
⊢ sign a = sign b ∨ sign a = -sign b

case inl.inr.inr
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : sign a = -1
hsb : sign b = 1
⊢ sign a = sign b ∨ sign a = -sign b

case inr.inl.inl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : sign a = 0
hsb : sign b = -1
⊢ sign a = sign b ∨ sign a = -sign b

case inr.inl.inr.inl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : sign a = 0
hsb : sign b = 0
⊢ sign a = sign b ∨ sign a = -sign b

case inr.inl.inr.inr
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : sign a = 0
hsb : sign b = 1
⊢ sign a = sign b ∨ sign a = -sign b

case inr.inr.inl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : sign a = 1
hsb : sign b = -1
⊢ sign a = sign b ∨ sign a = -sign b

case inr.inr.inr.inl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : sign a = 1
hsb : sign b = 0
⊢ sign a = sign b ∨ sign a = -sign b

case inr.inr.inr.inr
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : sign a = 1
hsb : sign b = 1
⊢ sign a = sign b ∨ sign a = -sign b
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_4
inst✝ : Infinite α
c : ℝ≥0∞
hc : c ≠ 0
⊢ ∑' (x : α), c = ∞

Tactic:
by
  have A : Tendsto (fun n : ℕ => (n : ℝ≥0∞) * c) atTop (𝓝 (∞ * c)) := by
    apply ENNReal.Tendsto.mul_const tendsto_nat_nhds_top
    simp only [true_or, top_ne_zero, Ne, not_false_iff]
  have B : ∀ n : ℕ, (n : ℝ≥0∞) * c ≤ ∑' _ : α, c := fun n => by
    rcases Infinite.exists_subset_card_eq α n with ⟨s, hs⟩
    simpa [hs] using @ENNReal.sum_le_tsum α (fun _ => c) s
  simpa [hc] using le_of_tendsto' A B

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

Goal state before:
pp: case pos
α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
hf : ∀ (i : α), f i = 0
⊢ ∑' (i : α), a * f i = a * ∑' (i : α), f i

pp: case neg
α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
hf : ¬∀ (i : α), f i = 0
⊢ ∑' (i : α), a * f i = a * ∑' (i : α), f i

Tactic:
· simp [hf]

Goal state after:
case neg
α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
hf : ¬∀ (i : α), f i = 0
⊢ ∑' (i : α), a * f i = a * ∑' (i : α), f i
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: x y : EReal
⊢ (x * y).abs = x.abs * y.abs

Tactic:
induction x, y using induction₂_symm_neg with
  | top_zero => simp only [mul_zero, abs_zero]
  | top_top => rfl
  | symm h => rwa [mul_comm, EReal.mul_comm]
  | coe_coe => simp only [← coe_mul, abs_def, _root_.abs_mul, ENNReal.ofReal_mul (abs_nonneg _)]
  | top_pos _ h =>
    rw [top_mul_coe_of_pos h, abs_top, ENNReal.top_mul]
    rw [Ne, abs_eq_zero_iff, coe_eq_zero]
    exact h.ne'
  | neg_left h => rwa [neg_mul, EReal.abs_neg, EReal.abs_neg]

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

Goal state before:
pp: α : Type u_1
ι : Type u_4
inst✝ : Fintype ι
f : α → ℝ≥0∞
t : ι → Set α
⊢ ∑' (x : ↑(⋃ i, t i)), f ↑x ≤ ∑ i, ∑' (x : ↑(t i)), f ↑x

Tactic:
by
  rw [← tsum_fintype (L := SummationFilter.unconditional _)]
  exact tsum_iUnion_le_tsum f t

Goal state after:
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a : EReal
h : a ≠ ⊥
h' : a ≠ ⊤
⊢ a⁻¹⁻¹ = a

Tactic:
by
  rw [← coe_toReal h' h, ← coe_inv a.toReal, ← coe_inv a.toReal⁻¹, _root_.inv_inv a.toReal]

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

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ ↑(d n)
ε : ℝ≥0
εpos : 0 < ε
hd : CauchySeq fun n ↦ ∑ x ∈ Finset.range n, d x
N : ℕ
hN : ∀ n ≥ N, dist (∑ x ∈ Finset.range n, d x) (∑ x ∈ Finset.range N, d x) < ↑ε
n : ℕ
hn : N ≤ n
⊢ edist (f n) (f N) < ↑ε

Tactic:
specialize hN n hn

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ ↑(d n)
ε : ℝ≥0
εpos : 0 < ε
hd : CauchySeq fun n ↦ ∑ x ∈ Finset.range n, d x
N n : ℕ
hN : dist (∑ x ∈ Finset.range n, d x) (∑ x ∈ Finset.range N, d x) < ↑ε
hn : N ≤ n
⊢ edist (f n) (f N) < ↑ε
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a b c : EReal
h : 0 < c
h' : c ≠ ⊤
⊢ b / c < c * a / c ↔ b < a * c

Tactic:
mul_comm a c

Goal state after:
a b c : EReal
h : 0 < c
h' : c ≠ ⊤
⊢ b / c < c * a / c ↔ b < c * a
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case neg
x✝ : EReal
h_top : ¬x✝ = ⊤
x : EReal
hx : x ∈ {⊤}ᶜ
h_bot : ¬x = ⊥
⊢ x ∉ {⊥, ⊤}

Tactic:
simp_all only [mem_compl_iff, mem_singleton_iff, mem_insert_iff, or_self, not_false_eq_true]

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

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
C : ℝ≥0∞
hC : C ≠ ∞
f : ℕ → α
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C / 2 ^ n
⊢ CauchySeq f

Tactic:
simp only [div_eq_mul_inv, ENNReal.inv_pow] at hu
  refine cauchySeq_of_edist_le_geometric 2⁻¹ C ?_ hC hu
  simp

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

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
⊢ (fun s ↦ ⨆ (_ : s.Nonempty), m s) = m

Tactic:
ext1 t

Goal state after:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s t : Set α
⊢ ⨆ (_ : t.Nonempty), m t = m t
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: ε : ℝ≥0
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∃ c, HasSum ε' c ∧ c < ε

Tactic:
cases nonempty_encodable ι

Goal state after:
case intro
ε : ℝ≥0
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
val✝ : Encodable ι
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∃ c, HasSum ε' c ∧ c < ε
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
ι : Type u_2
β : Type u_3
I : Set ι
hI : I.Nonempty
f : α → β
m : ι → OuterMeasure β
⊢ (map f) (⨅ i ∈ I, (comap f) (m i)) = ⨅ i ∈ I, (map f) ((comap f) (m i))

Tactic:
have := hI.to_subtype
  rw [← iInf_subtype'', ← iInf_subtype'']
  exact map_iInf_comap _

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_1
S : Set α
⊢ IsPiSystem {S}

Tactic:
by
  intro s h_s t h_t _
  rw [Set.mem_singleton_iff.1 h_s, Set.mem_singleton_iff.1 h_t, Set.inter_self,
    Set.mem_singleton_iff]

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

Goal state before:
pp: α : Type u
m : OuterMeasure α
s₁ s₂ : Set α
h₁ : m.IsCaratheodory s₁
h₂ : m.IsCaratheodory s₂
t : Set α
⊢ m (t ∩ s₁ ∩ s₂) + m ((t ∩ s₁) \ s₂) + (m (t \ s₁ ∩ s₂) + m ((t \ s₁) \ s₂)) =
    m (t ∩ (s₁ ∪ s₂) ∩ s₁) + m ((t ∩ (s₁ ∪ s₂)) \ s₁) + m (t \ (s₁ ∪ s₂))

Tactic:
inter_sdiff_assoc _ _ s₁,

Goal state after:
α : Type u
m : OuterMeasure α
s₁ s₂ : Set α
h₁ : m.IsCaratheodory s₁
h₂ : m.IsCaratheodory s₂
t : Set α
⊢ m (t ∩ s₁ ∩ s₂) + m ((t ∩ s₁) \ s₂) + (m (t \ s₁ ∩ s₂) + m ((t \ s₁) \ s₂)) =
    m (t ∩ (s₁ ∪ s₂) ∩ s₁) + m (t ∩ ((s₁ ∪ s₂) \ s₁)) + m (t \ (s₁ ∪ s₂))
Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory

Goal state before:
pp: α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
t : Set α
hp : m (t ∩ ⋃ i, s i) ≤ ⨆ n, m (t ∩ ⋃ i, ⋃ (_ : i < n), s i)
⊢ m (t ∩ ⋃ i, s i) + m (t \ ⋃ i, s i) ≤ m t

Tactic:
grw [hp, ENNReal.iSup_add]

Goal state after:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
t : Set α
hp : m (t ∩ ⋃ i, s i) ≤ ⨆ n, m (t ∩ ⋃ i, ⋃ (_ : i < n), s i)
⊢ ⨆ i, m (t ∩ ⋃ i_1, ⋃ (_ : i_1 < i), s i_1) + m (t \ ⋃ i, s i) ≤ m t
Module: Mathlib.MeasureTheory.OuterMeasure.AE

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
μ : F
inst✝ : Countable α
p : α → Prop
⊢ (∀ᵐ (x : α) ∂μ, p x) ↔ ∀ (x : α), μ {x} ≠ 0 → p x

Tactic:
rw [ae_iff, measure_null_iff_singleton]
  exacts [forall_congr' fun _ ↦ not_imp_comm, Set.to_countable _]

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

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i) μ
x : α
hx : x ∈ aeSeqSet hf p
⊢ p x fun n ↦ f n x

Tactic:
have h_eq : (fun n => f n x) = fun n => aeSeq hf p n x :=
    funext fun n => (aeSeq_eq_fun_of_mem_aeSeqSet hf hx n).symm
  rw [h_eq]
  exact prop_of_mem_aeSeqSet hf hx

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

Goal state before:
pp: α : Type u_1
s : Set α
⊢ generateFrom {s} = MeasurableSpace.comap (fun x ↦ x ∈ s) ⊤

Tactic:
(Tactic.tacticLet__
 "let"
 (Term.letConfig [])
 (Term.letDecl
  (Term.letIdDecl
   (Term.letId (hygieneInfo `[anonymous]))
   []
   [(Term.typeSpec ":" (Term.app `MeasurableSpace [`α]))]
   ":="
   (Term.app
    `generateFrom
    [(choice
      («term{_}» "{" [`s] "}")
      (Term.structInst
       "{"
       []
       (Term.structInstFields [(Term.structInstField (Term.structInstLVal `s []) [])])
       (Term.optEllipsis [])
       []
       "}"))]))))

Goal state after:
α : Type u_1
s : Set α
this : MeasurableSpace α := generateFrom {s}
⊢ generateFrom {s} = MeasurableSpace.comap (fun x ↦ x ∈ s) ⊤
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: α : Type u_1
s t : Set α
⊢ (∃ s', True ∧ (fun x ↦ x ∈ s) ⁻¹' s' = t) ↔ t = ∅ ∨ t = s ∨ t = sᶜ ∨ t = univ

Tactic:
true_and

Goal state after:
α : Type u_1
s t : Set α
⊢ (∃ s', (fun x ↦ x ∈ s) ⁻¹' s' = t) ↔ t = ∅ ∨ t = s ∨ t = sᶜ ∨ t = univ
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
⊢ MeasurableSet (limsup s atTop)

Tactic:
simpa only [← blimsup_true] using measurableSet_blimsup fun n _ => hs n

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

Goal state before:
pp: case neg.refine_1
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t
hs : ¬ms = ∞
this✝ : ∀ r > ms, ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t < r
t : ℕ → Set α
hsub : ∀ (n : ℕ), s ⊆ t n
hm : ∀ (n : ℕ), MeasurableSet (t n)
hm' : ∀ (n : ℕ), m (t n) < ms + (↑n)⁻¹
this : Tendsto (fun n ↦ ms + (↑n)⁻¹) atTop (𝓝 ms)
n : ℕ
⊢ m (⋂ n, t n) ≤ ms + (↑n)⁻¹

Tactic:
exact le_trans (measure_mono <| iInter_subset t n) (hm' n).le

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t s : Set α
ht : NullMeasurableSet t μ
⊢ μ (s ∩ t) + μ (s \ t) = μ s

Tactic:
refine le_antisymm ?_ (measure_le_inter_add_sdiff _ _ _)
  rcases exists_measurable_superset μ s with ⟨s', hsub, hs'm, hs'⟩
  replace hs'm : NullMeasurableSet s' μ := hs'm.nullMeasurableSet
  calc
    μ (s ∩ t) + μ (s \ t) ≤ μ (s' ∩ t) + μ (s' \ t) := by gcongr
    _ = μ (s' ∩ t ∪ s' \ t) :=
      (measure_union₀_aux (hs'm.inter ht) (hs'm.diff ht) <|
          (@disjoint_inf_sdiff _ s' t _).aedisjoint).symm
    _ = μ s' := congr_arg μ (inter_union_sdiff _ _)
    _ = μ s := hs'

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure α
s : Set β
t : Set β := f '' toMeasurable μ (f ⁻¹' s) ∪ (range f)ᶜ
htm : MeasurableSet t
hst : s ⊆ t
⊢ (map f μ) s ≤ μ (f ⁻¹' s)

Tactic:
have hft : f ⁻¹' t = toMeasurable μ (f ⁻¹' s) := by
    rw [preimage_union, preimage_compl, preimage_range, compl_univ, union_empty,
      hf.injective.preimage_image]

Goal state after:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure α
s : Set β
t : Set β := f '' toMeasurable μ (f ⁻¹' s) ∪ (range f)ᶜ
htm : MeasurableSet t
hst : s ⊆ t
hft : f ⁻¹' t = toMeasurable μ (f ⁻¹' s)
⊢ (map f μ) s ≤ μ (f ⁻¹' s)
Module: Mathlib.MeasureTheory.Measure.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
h : map f μ = map f ν
s : Set α
hs : MeasurableSet s
⊢ (map f μ) (f '' s) = ν (f ⁻¹' f '' s)

Tactic:
← hf.map_apply

Goal state after:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
h : map f μ = map f ν
s : Set α
hs : MeasurableSet s
⊢ (map f μ) (f '' s) = (map f ν) (f '' s)
Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving

Goal state before:
pp: case refine_2
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → α
h : QuasiMeasurePreserving f μ μ
hs' : f ⁻¹' s =ᵐ[μ] s
t : Set α
htm : MeasurableSet t
ht : s =ᵐ[μ] t
⊢ limsup (fun x ↦ f^[x] ⁻¹' t) atTop =ᵐ[μ] s

Tactic:
have : f ⁻¹' t =ᵐ[μ] t := (h.preimage_ae_eq ht.symm).trans (hs'.trans ht)
    exact limsup_ae_eq_of_forall_ae_eq _ fun n ↦ .trans (h.preimage_iterate_ae_eq _ this) ht.symm

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
⊢ s ∪ t =ᵐ[μ] t ↔ s ≤ᵐ[μ] t

Tactic:
by
  rw [union_comm, union_ae_eq_left_iff_ae_subset]

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

Goal state before:
pp: case inr
α : Type u_1
ι : Type u_3
m0 : MeasurableSpace α
inst✝¹ : Countable ι
m : ι → Measure α
inst✝ : ∀ (n : ι), IsFiniteMeasure (m n)
f : ι → ℕ
hf : Injective f
n : ℕ
hn : n ∉ range f
⊢ IsFiniteMeasure (Function.extend f m 0 n)

Tactic:
Function.extend_apply' _ _ _ hn,

Goal state after:
case inr
α : Type u_1
ι : Type u_3
m0 : MeasurableSpace α
inst✝¹ : Countable ι
m : ι → Measure α
inst✝ : ∀ (n : ι), IsFiniteMeasure (m n)
f : ι → ℕ
hf : Injective f
n : ℕ
hn : n ∉ range f
⊢ IsFiniteMeasure (0 n)