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

Goal state before:
pp: case inl
β : Type u_2
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : CommGroup G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
a : G
hβ : Finite β
⊢ ∏' (x : β), a = a ^ Nat.card β

Tactic:
let : Fintype β := Fintype.ofFinite β

Goal state after:
case inl
β : Type u_2
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : CommGroup G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
a : G
hβ : Finite β
this : Fintype β := Fintype.ofFinite β
⊢ ∏' (x : β), a = a ^ Nat.card β
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
| ((∏ x ∈ s, f x) * ∏ x ∈ t \ s, f x) * ((∏ i ∈ s, g i) / ∏ i ∈ s, f i)

Tactic:
prod_congr rfl fun i hi ↦ hs' i (mem_sdiff.mp hi).2

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
| (∏ x ∈ s, f x) * (t \ s).prod g * ((∏ i ∈ s, g i) / ∏ i ∈ s, f i)
Module: Mathlib.Topology.Sequences

Goal state before:
pp: case neg
X : Type u_1
inst✝¹ : TopologicalSpace X
x : ℕ → X
inst✝ : SequentialSpace X
hx : ∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 l)
y : ℕ → X
l : X
hy : ∀ (n : ℕ), y n ∈ ⋃ i, closure[inst✝¹] {x i}
hy' : Tendsto y atTop (𝓝 l)
hm : ∀ (m : ℕ), ∀ᶠ (x_1 : ℕ) in atTop, y x_1 ∉ closure[inst✝¹] {x m}
this : ∀ (j : ℕ), ∃ᶠ (k : ℕ) in atTop, ∃ n ≥ j, y n ∈ closure[inst✝¹] {x k}
⊢ l ∈ ⋃ i, closure[inst✝¹] {x i}

Tactic:
obtain ⟨φ, hφ⟩ := extraction_forall_of_frequently this

Goal state after:
case neg
X : Type u_1
inst✝¹ : TopologicalSpace X
x : ℕ → X
inst✝ : SequentialSpace X
hx : ∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 l)
y : ℕ → X
l : X
hy : ∀ (n : ℕ), y n ∈ ⋃ i, closure[inst✝¹] {x i}
hy' : Tendsto y atTop (𝓝 l)
hm : ∀ (m : ℕ), ∀ᶠ (x_1 : ℕ) in atTop, y x_1 ∉ closure[inst✝¹] {x m}
this : ∀ (j : ℕ), ∃ᶠ (k : ℕ) in atTop, ∃ n ≥ j, y n ∈ closure[inst✝¹] {x k}
φ : ℕ → ℕ
hφ : StrictMono φ ∧ ∀ (n : ℕ), ∃ n_1 ≥ n, y n_1 ∈ closure[inst✝¹] {x (φ n)}
⊢ l ∈ ⋃ i, closure[inst✝¹] {x i}
Module: Mathlib.Analysis.Normed.Group.Continuity

Goal state before:
pp: E : Type u_7
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousENorm E
X : Type u_8
inst✝ : TopologicalSpace X
f : X → E
s : Set X
a : X
h : ContinuousWithinAt f s a
x✝¹ : X
x✝ : x✝¹ ∈ s
⊢ f x✝¹ ∈ Set.univ

Tactic:
by trivial

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

Goal state before:
pp: case inr
x : ℝ≥0∞
xt : x ≠ ∞
x0 : 0 < x
⊢ (𝓝 x).HasBasis (fun x ↦ x ≠ 0) fun ε ↦ Icc (x - ε) (x + ε)

Tactic:
· refine (nhds_basis_Ioo' ⟨_, x0⟩ ⟨_, xt.lt_top⟩).to_hasBasis ?_ fun ε ε0 => ?_
    · rintro ⟨a, b⟩ ⟨ha, hb⟩
      rcases exists_between (tsub_pos_of_lt ha) with ⟨ε, ε0, hε⟩
      rcases lt_iff_exists_add_pos_lt.1 hb with ⟨δ, δ0, hδ⟩
      refine ⟨min ε δ, (lt_min ε0 (coe_pos.2 δ0)).ne', Icc_subset_Ioo ?_ ?_⟩
      · exact lt_tsub_comm.2 ((min_le_left _ _).trans_lt hε)
      · grw [min_le_right]
        exact hδ
    · exact ⟨(x - ε, x + ε), ⟨ENNReal.sub_lt_self xt x0.ne' ε0,
        lt_add_right xt ε0⟩, Ioo_subset_Icc_self⟩

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

Goal state before:
pp: case mp
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
n : β
hn : f n ≤ min 1 (ε / 2)
⊢ ∃ n, f n < ε

Tactic:
refine ⟨n, hn.trans_lt ?_⟩
      by_cases hε_top : ε = ∞
      · simp [hε_top]
      refine (min_le_right _ _).trans_lt ?_
      rw [ENNReal.div_lt_iff (Or.inr hε.ne') (Or.inr hε_top)]
      conv_lhs => rw [← mul_one ε]
      gcongr; simp

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 ((pkg.prod pkg').extend (uncurry f))

Tactic:
apply uniformContinuous_extend

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
inst✝² : PseudoEMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
s : β → α
⊢ (∀ ε > 0, ∃ N, ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (s m) (s n) < ε) →
    ∃ b, (∀ (n m N : β), N ≤ n → N ≤ m → edist (s n) (s m) ≤ b N) ∧ Tendsto b atTop (𝓝 0)

Tactic:
intro hs

Goal state after:
case mp
α : Type u_1
β : Type u_2
inst✝² : PseudoEMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
s : β → α
hs : ∀ ε > 0, ∃ N, ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (s m) (s n) < ε
⊢ ∃ b, (∀ (n m N : β), N ≤ n → N ≤ m → edist (s n) (s m) ≤ b N) ∧ Tendsto b atTop (𝓝 0)
Module: Mathlib.Topology.Metrizable.Uniformity

Goal state before:
pp: case pos
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 : 1 / 2 ∈ Ioo 0 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
x₁ x₂ x₃ x₄ : X
H : ∃ n, (x₁, x₄) ∉ U n
⊢ (1 / 2) ^ Nat.find H ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))

Tactic:
← div_le_iff₀' zero_lt_two,

Goal state after:
case pos
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 : 1 / 2 ∈ Ioo 0 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
x₁ x₂ x₃ x₄ : X
H : ∃ n, (x₁, x₄) ∉ U n
⊢ (1 / 2) ^ Nat.find H / 2 ≤ max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
Module: Mathlib.Analysis.Normed.Order.Lattice

Goal state before:
pp: α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
a b : α
h : b ⊓ -b ≤ a ⊓ -a
⊢ -(-a ⊓ a) ≤ b ⊔ -b

Tactic:
nth_rw 1 [← neg_neg b]

Goal state after:
α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
a b : α
h : b ⊓ -b ≤ a ⊓ -a
⊢ -(-a ⊓ a) ≤ - -b ⊔ -b
Module: Mathlib.Topology.MetricSpace.IsometricSMul

Goal state before:
pp: G : Type v
inst✝² : Group G
inst✝¹ : PseudoEMetricSpace G
inst✝ : IsIsometricSMul Gᵐᵒᵖ G
a b : G
r : ℝ≥0∞
⊢ (fun x ↦ x * a) ⁻¹' closedEBall b r = closedEBall (b / a) r

Tactic:
rw [div_eq_mul_inv]
  exact preimage_smul_closedEBall (MulOpposite.op a) b r

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

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedCommGroup E
u v : ℕ → E
N : ℕ
huv : ∀ n ≥ N, u n = v n
hv : CauchySeq fun n ↦ ∏ k ∈ range (n + 1), v k
d : ℕ → E := fun n ↦ ∏ k ∈ range (n + 1), u k / v k
n : ℕ
hn : n ≥ N
⊢ ∏ k ∈ range (n + 1), u k / v k = ∏ k ∈ range (N + 1), u k / v k

Tactic:
eventually_constant_prod (N := N + 1) _ (by gcongr)

Goal state after:
E : Type u_2
inst✝ : SeminormedCommGroup E
u v : ℕ → E
N : ℕ
huv : ∀ n ≥ N, u n = v n
hv : CauchySeq fun n ↦ ∏ k ∈ range (n + 1), v k
d : ℕ → E := fun n ↦ ∏ k ∈ range (n + 1), u k / v k
n : ℕ
hn : n ≥ N
⊢ ∏ k ∈ range (N + 1), u k / v k = ∏ k ∈ range (N + 1), u k / v k

E : Type u_2
inst✝ : SeminormedCommGroup E
u v : ℕ → E
N : ℕ
huv : ∀ n ≥ N, u n = v n
hv : CauchySeq fun n ↦ ∏ k ∈ range (n + 1), v k
d : ℕ → E := fun n ↦ ∏ k ∈ range (n + 1), u k / v k
n : ℕ
hn : n ≥ N
⊢ ∀ n ≥ N + 1, u n / v n = 1
Module: Mathlib.Analysis.Normed.Ring.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝¹ : NonUnitalSeminormedRing α
a a₁ a₂ b c : α
inst✝ : NonUnitalSeminormedRing β
x y : α × β
⊢ max (‖x.1‖ * ‖y.1‖) (‖y.2‖ * ‖x.2‖) ≤ max ‖x.1‖ ‖x.2‖ * max ‖y.2‖ ‖y.1‖

Tactic:
apply max_mul_mul_le_max_mul_max

Goal state after:
case ha
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝¹ : NonUnitalSeminormedRing α
a a₁ a₂ b c : α
inst✝ : NonUnitalSeminormedRing β
x y : α × β
⊢ 0 ≤ ‖x.1‖

case hd
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝¹ : NonUnitalSeminormedRing α
a a₁ a₂ b c : α
inst✝ : NonUnitalSeminormedRing β
x y : α × β
⊢ 0 ≤ ‖y.2‖
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
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 [discreteTopology_iff_isOpen_singleton_zero, isOpen_induced_iff]

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
⊢ ∃ t, IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ Subtype.val ⁻¹' t = {0}
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:
by
  simp only [dist_eq_norm, ← map_sub, norm_algebraMap']

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

Goal state before:
pp: G : Type u_6
H : Type u_7
inst✝² : SeminormedAddCommGroup G
inst✝¹ : SeminormedAddCommGroup H
inst✝ : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : s ∈ 𝓝 0
hbounded : Bornology.IsBounded (⇑f '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
C ε : ℝ
hε : 0 < ε
hC : ∀ (a : G), ‖a‖ < δ → ‖f a‖ < C
⊢ ∃ δ > 0, ∀ ⦃x : G⦄, ‖x‖ < δ → ‖f x‖ < ε

Tactic:
have hC₀ : 0 < C := (norm_nonneg _).trans_lt <| hC 0 (by simpa)

Goal state after:
G : Type u_6
H : Type u_7
inst✝² : SeminormedAddCommGroup G
inst✝¹ : SeminormedAddCommGroup H
inst✝ : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : s ∈ 𝓝 0
hbounded : Bornology.IsBounded (⇑f '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
C ε : ℝ
hε : 0 < ε
hC : ∀ (a : G), ‖a‖ < δ → ‖f a‖ < C
hC₀ : 0 < C
⊢ ∃ δ > 0, ∀ ⦃x : G⦄, ‖x‖ < δ → ‖f x‖ < ε
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:
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.MeasurableSpace.Constructions

Goal state before:
pp: β : Type u_2
δ : Type u_4
X✝ : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (X✝ a)
X : (a : δ) → β → X✝ a
⊢ MeasurableSpace.comap (fun b a ↦ X a b) inferInstance = ⨆ a, MeasurableSpace.comap (X a) inferInstance

Tactic:
simp_rw [MeasurableSpace.pi, MeasurableSpace.comap_iSup, MeasurableSpace.comap_comp]
  rfl

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

Goal state before:
pp: α : Type u_4
β : α → Type u_3
f : (x : α) × β x → ℝ
hf : ∀ (x : (x : α) × β x), 0 ≤ f x
⊢ Summable f ↔ (∀ (x : α), Summable fun y ↦ f ⟨x, y⟩) ∧ Summable fun x ↦ ∑' (y : β x), f ⟨x, y⟩

Tactic:
by
  lift f to (Σ x, β x) → ℝ≥0 using hf
  simpa using mod_cast NNReal.summable_sigma

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

Goal state before:
pp: α : Type u_3
β : Type u_4
f : β → ℝ
hf : 0 ≤ f
s : α → Set β
hs : ∀ (i : β), ∃! j, i ∈ s j
⊢ Summable f ↔ (∀ (j : α), Summable fun i ↦ f ↑i) ∧ Summable fun j ↦ ∑' (i : ↑(s j)), f ↑i

Tactic:
by
  simpa only [← (Set.sigmaEquiv s hs).summable_iff] using! summable_sigma_of_nonneg (fun _ ↦ hf _)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Countable α
⊢ MeasurableSet (range Function.diag)

Tactic:
Set.range_eq_iUnion

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Countable α
⊢ MeasurableSet (⋃ i, {Function.diag i})
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case neg_left
x✝ y✝ : EReal
h : sign (x✝ * y✝) = sign x✝ * sign y✝
⊢ sign (-(x✝ * y✝)) = sign (-x✝) * sign y✝

Tactic:
sign_neg,

Goal state after:
case neg_left
x✝ y✝ : EReal
h : sign (x✝ * y✝) = sign x✝ * sign y✝
⊢ -sign (x✝ * y✝) = sign (-x✝) * sign y✝
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case neg_left
x✝ y✝ : EReal
h : sign (x✝ * y✝) = sign x✝ * sign y✝
⊢ -sign (x✝ * y✝) = sign (-x✝) * sign y✝

Tactic:
sign_neg,

Goal state after:
case neg_left
x✝ y✝ : EReal
h : sign (x✝ * y✝) = sign x✝ * sign y✝
⊢ -sign (x✝ * y✝) = -sign x✝ * sign y✝
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: ι : Type u_4
a : ι → ℝ≥0∞
tsum_ne_top : ∑' (i : ι), a i ≠ ∞
ε : ℝ≥0∞
ε_ne_zero : ε ≠ 0
h : ¬{i | ε ≤ a i}.Finite
this : Infinite ↑{i | ε ≤ a i}
⊢ False

Tactic:
refine tsum_ne_top (top_unique ?_)

Goal state after:
ι : Type u_4
a : ι → ℝ≥0∞
tsum_ne_top : ∑' (i : ι), a i ≠ ∞
ε : ℝ≥0∞
ε_ne_zero : ε ≠ 0
h : ¬{i | ε ≤ a i}.Finite
this : Infinite ↑{i | ε ≤ a i}
⊢ ∞ ≤ ∑' (i : ι), a i
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a : EReal
h₁ : a ≠ ⊥
h₂ : a ≠ ⊤
h₃ : ↑a.toReal ≠ 0
⊢ ↑(a.toReal / a.toReal) = 1

Tactic:
_root_.div_self (coe_ne_zero.1 h₃),

Goal state after:
a : EReal
h₁ : a ≠ ⊥
h₂ : a ≠ ⊤
h₃ : ↑a.toReal ≠ 0
⊢ ↑1 = 1
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : Set α → ℝ≥0∞ := fun s ↦ ⨅ f, ⨅ (_ : s ⊆ ⋃ i, f i), ∑' (i : ℕ), m (f i)
s : ℕ → Set α
x✝ : Pairwise (Disjoint on s)
ε : ℝ≥0
hε : 0 < ε
hb : ∑' (i : ℕ), μ (s i) < ∞
ε' : ℕ → ℝ≥0
hε' : ∀ (i : ℕ), 0 < ε' i
hl : ∑' (i : ℕ), ↑(ε' i) < ↑ε
f : ℕ → ℕ → Set α
hf : ∀ (i : ℕ), s i ⊆ ⋃ i_1, f i i_1 ∧ ∑' (i_1 : ℕ), m (f i i_1) < μ (s i) + ↑(ε' i)
⊢ μ (⋃ i, s i) ≤ ∑' (c : ℕ), m (f (Nat.pairEquiv.symm c).1 (Nat.pairEquiv.symm c).2)

Tactic:
refine iInf_le_of_le _ (iInf_le _ ?_)

Goal state after:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : Set α → ℝ≥0∞ := fun s ↦ ⨅ f, ⨅ (_ : s ⊆ ⋃ i, f i), ∑' (i : ℕ), m (f i)
s : ℕ → Set α
x✝ : Pairwise (Disjoint on s)
ε : ℝ≥0
hε : 0 < ε
hb : ∑' (i : ℕ), μ (s i) < ∞
ε' : ℕ → ℝ≥0
hε' : ∀ (i : ℕ), 0 < ε' i
hl : ∑' (i : ℕ), ↑(ε' i) < ↑ε
f : ℕ → ℕ → Set α
hf : ∀ (i : ℕ), s i ⊆ ⋃ i_1, f i i_1 ∧ ∑' (i_1 : ℕ), m (f i i_1) < μ (s i) + ↑(ε' i)
⊢ ⋃ i, s i ⊆ ⋃ i, f (Nat.pairEquiv.symm i).1 (Nat.pairEquiv.symm i).2
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case inr
α : Type u_4
β : Type u_5
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder β
f g : α → β
s : Set α
a : α
hf : LowerSemicontinuousWithinAt f s a
hg : LowerSemicontinuousWithinAt g s a
b : β
hb : b < g a
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, b < f x' ∨ b < g x'

Tactic:
· filter_upwards [hg b hb] with x using Or.intro_right _

Goal state after:
Module: Mathlib.Order.SetDissipate

Goal state before:
pp: α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : LE α
x : α
⊢ ⋂ i, s i ⊆ dissipate s x

Tactic:
simp only [dissipate, subset_iInter_iff]

Goal state after:
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : LE α
x : α
⊢ ∀ i ≤ x, ⋂ i, s i ⊆ s i
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s₁ s₂ : Set α
h₁ : P s₁
hs : s₁ ⊆ s₂
h₂ : P s₂
⊢ extend m s₁ ≤ m s₂ h₂

Tactic:
extend_eq m h₁

Goal state after:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s₁ s₂ : Set α
h₁ : P s₁
hs : s₁ ⊆ s₂
h₂ : P s₂
⊢ m s₁ h₁ ≤ m s₂ h₂
Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
⊢ MeasurableSet s

Tactic:
apply ofFunction_caratheodory

Goal state after:
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
⊢ ∀ (t : Set α), (⨆ (_ : (t ∩ s).Nonempty), m (t ∩ s)) + ⨆ (_ : (t \ s).Nonempty), m (t \ s) ≤ ⨆ (_ : t.Nonempty), m t
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: α : 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₂
f : α ≃ α
Pm : ∀ (s : Set α), P (⇑f ⁻¹' s) ↔ P s
mm : ∀ (s : Set α) (hs : P s), m (⇑f ⁻¹' s) ⋯ = m s hs
A s : Set α
⊢ ∀ (x : P s), ⨅ (_ : ⇑f ⁻¹' A ⊆ ⇑f ⁻¹' s), m (⇑f ⁻¹' s) ⋯ = ⨅ (_ : A ⊆ s), m s x

Tactic:
intro hs

Goal state after:
α : 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₂
f : α ≃ α
Pm : ∀ (s : Set α), P (⇑f ⁻¹' s) ↔ P s
mm : ∀ (s : Set α) (hs : P s), m (⇑f ⁻¹' s) ⋯ = m s hs
A s : Set α
hs : P s
⊢ ⨅ (_ : ⇑f ⁻¹' A ⊆ ⇑f ⁻¹' s), m (⇑f ⁻¹' s) ⋯ = ⨅ (_ : A ⊆ s), m s hs
Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef

Goal state before:
pp: α : Type u_6
β : Type u_7
inst✝ : MeasurableSpace β
μ : Measure β
C : β → Set α → Prop
s : Set (Set α)
m : MeasurableSpace α
h_eq : m = generateFrom s
h_inter : IsPiSystem s
h_empty : ∀ᵐ (x : β) ∂μ, C x ∅
h_basic : ∀ᵐ (x : β) ∂μ, ∀ t ∈ s, C x t
h_compl : ∀ᵐ (x : β) ∂μ, ∀ (t : Set α), MeasurableSet t → C x t → C x tᶜ
h_union :
  ∀ᵐ (x : β) ∂μ,
    ∀ (f : ℕ → Set α),
      Pairwise (Disjoint on f) → (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), C x (f i)) → C x (⋃ i, f i)
x : β
hx_empty : C x ∅
hx_basic : ∀ t ∈ s, C x t
⊢ (∀ (t : Set α), MeasurableSet t → C x t → C x tᶜ) →
    (∀ (f : ℕ → Set α),
        Pairwise (Disjoint on f) → (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), C x (f i)) → C x (⋃ i, f i)) →
      ∀ ⦃t : Set α⦄, MeasurableSet t → C x t

Tactic:
hx_compl

Goal state after:
α : Type u_6
β : Type u_7
inst✝ : MeasurableSpace β
μ : Measure β
C : β → Set α → Prop
s : Set (Set α)
m : MeasurableSpace α
h_eq : m = generateFrom s
h_inter : IsPiSystem s
h_empty : ∀ᵐ (x : β) ∂μ, C x ∅
h_basic : ∀ᵐ (x : β) ∂μ, ∀ t ∈ s, C x t
h_compl : ∀ᵐ (x : β) ∂μ, ∀ (t : Set α), MeasurableSet t → C x t → C x tᶜ
h_union :
  ∀ᵐ (x : β) ∂μ,
    ∀ (f : ℕ → Set α),
      Pairwise (Disjoint on f) → (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), C x (f i)) → C x (⋃ i, f i)
x : β
hx_empty : C x ∅
hx_basic : ∀ t ∈ s, C x t
hx_compl : ∀ (t : Set α), MeasurableSet t → C x t → C x tᶜ
⊢ (∀ (f : ℕ → Set α),
      Pairwise (Disjoint on f) → (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), C x (f i)) → C x (⋃ i, f i)) →
    ∀ ⦃t : Set α⦄, MeasurableSet t → C x t
Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef

Goal state before:
pp: α : Type u_6
β : Type u_7
inst✝ : MeasurableSpace β
μ : Measure β
C : β → Set α → Prop
s : Set (Set α)
m : MeasurableSpace α
h_eq : m = generateFrom s
h_inter : IsPiSystem s
h_empty : ∀ᵐ (x : β) ∂μ, C x ∅
h_basic : ∀ᵐ (x : β) ∂μ, ∀ t ∈ s, C x t
h_compl : ∀ᵐ (x : β) ∂μ, ∀ (t : Set α), MeasurableSet t → C x t → C x tᶜ
h_union :
  ∀ᵐ (x : β) ∂μ,
    ∀ (f : ℕ → Set α),
      Pairwise (Disjoint on f) → (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), C x (f i)) → C x (⋃ i, f i)
⊢ ∀ᵐ (x : β) ∂μ, ∀ ⦃t : Set α⦄, MeasurableSet t → C x t

Tactic:
filter_upwards [h_empty, h_basic, h_compl, h_union] with x hx_empty hx_basic hx_compl hx_union
    using MeasurableSpace.induction_on_inter (C := fun t _ ↦ C x t)
      h_eq h_inter hx_empty hx_basic hx_compl hx_union

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:
by
  let : MeasurableSpace α := generateFrom {s}
  refine le_antisymm (generateFrom_le fun t ht => ⟨{True}, trivial, by simp [ht.symm]⟩) ?_
  rintro _ ⟨u, -, rfl⟩
  exact (show MeasurableSet s from GenerateMeasurable.basic _ <| mem_singleton s).mem trivial

Goal state after:
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
β₁ : Type u_9
α₂ : Type u_10
β₂ : Type u_11
inst✝¹ : MeasurableSpace β₁
inst✝ : MeasurableSpace β₂
hα : α₁ ≃ α₂
hβ : β₁ ≃ᵐ β₂
x✝ : Set (α₁ → β₁)
h : MeasurableSet x✝
⊢ MeasurableSet (⇑(hα.arrowCongr' ↑hβ).symm ⁻¹' x✝)

Tactic:
by
    exact MeasurableSet.preimage h <|
      measurable_pi_iff.mpr fun _ ↦ hβ.symm.measurable.comp (measurable_pi_apply _)

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

Goal state before:
pp: α : Type u_1
R : Type u_5
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
h : μ ≪ ν
c : R
s : Set α
hνs : c • ν s = 0
⊢ c • μ s = 0

Tactic:
← smul_one_smul ℝ≥0∞,

Goal state after:
α : Type u_1
R : Type u_5
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
h : μ ≪ ν
c : R
s : Set α
hνs : (c • 1) • ν s = 0
⊢ (c • 1) • μ s = 0
Module: Mathlib.MeasureTheory.Measure.Comap

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

Tactic:
rw [comap, dif_pos (And.intro hfi hf)] at hs ⊢

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
hs : NullMeasurableSet s (((OuterMeasure.comap f) μ.toOuterMeasure).toMeasure ⋯)
⊢ (((OuterMeasure.comap f) μ.toOuterMeasure).toMeasure ⋯) s = μ (f '' s)
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 : Set α
⊢ μ (f '' s) ≤ (comap f μ) s

Tactic:
rw [comap, dif_pos (And.intro hfi hf)]

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 : Set α
⊢ μ (f '' s) ≤ (((OuterMeasure.comap f) μ.toOuterMeasure).toMeasure ⋯) s