mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Metrizable.Uniformity

Goal state before:
pp: 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)
⊢ ∃ I, PseudoMetricSpace.toUniformSpace = inst✝¹

Tactic:
have hle_d : ∀ {x y : X} {n : ℕ}, (1 / 2) ^ n ≤ d x y ↔ (x, y) ∉ U n := by
    intro x y n
    dsimp only [d]
    split_ifs with h
    · rw [(pow_right_strictAnti₀ hr.1 hr.2).le_iff_ge, Nat.find_le_iff]
      exact ⟨fun ⟨m, hmn, hm⟩ hn => hm (hB.antitone hmn hn), fun h => ⟨n, le_rfl, h⟩⟩
    · push Not at h
      simp only [h, not_true, (pow_pos hr.1 _).not_ge]

Goal state after:
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
⊢ ∃ I, PseudoMetricSpace.toUniformSpace = inst✝¹
Module: Mathlib.Analysis.Normed.Field.Basic

Goal state before:
pp: case mpr.inr
𝕜 : Type u_5
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : DiscreteTopology 𝕜
x : 𝕜
hx : x ≠ 0
ε : ℝ
εpos : ε > 0
h' : ∀ (y : 𝕜), ‖y‖ < ε → y = 0
H :
  ∀ {𝕜 : Type u_5} [inst : NormedDivisionRing 𝕜] [DiscreteTopology 𝕜] {x : 𝕜},
    x ≠ 0 → (∀ (y : 𝕜), ‖y‖ < ε → y = 0) → ‖x‖ < 1 → ‖x‖ = 1
h : 1 ≤ ‖x‖
⊢ ‖x‖ = 1

Tactic:
rcases h.eq_or_lt with h | h
      · rw [h]
      replace h := norm_inv x ▸ inv_lt_one_of_one_lt₀ h
      rw [← inv_inj, inv_one, ← norm_inv]
      exact H (by simpa) h' h

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

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
f : α → E
g : α → F
l : Filter α
hf : ∀ ε > 0, ∀ᶠ (x : α) in l, ‖f x‖ < ε
op : E → F → G
A : ℝ
h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖
C : ℝ
hC : ∀ᶠ (a : α) in l, (fun x1 x2 ↦ x1 ≤ x2) ((Norm.norm ∘ g) a) C
ε : ℝ
ε₀ : ε > 0
⊢ ∀ᶠ (x : α) in l, ‖op (f x) (g x)‖ < ε

Tactic:
rcases exists_pos_mul_lt ε₀ (A * C) with ⟨δ, δ₀, hδ⟩

Goal state after:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
f : α → E
g : α → F
l : Filter α
hf : ∀ ε > 0, ∀ᶠ (x : α) in l, ‖f x‖ < ε
op : E → F → G
A : ℝ
h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖
C : ℝ
hC : ∀ᶠ (a : α) in l, (fun x1 x2 ↦ x1 ≤ x2) ((Norm.norm ∘ g) a) C
ε : ℝ
ε₀ : ε > 0
δ : ℝ
δ₀ : 0 < δ
hδ : A * C * δ < ε
⊢ ∀ᶠ (x : α) in l, ‖op (f x) (g x)‖ < ε
Module: Mathlib.Data.Prod.TProd

Goal state before:
pp: ι : Type u
α : ι → Type v
j : ι
l : List ι
inst✝ : DecidableEq ι
hj : j ∈ l
hl : (j :: l).Nodup
v : TProd α (j :: l)
⊢ False

Tactic:
exact hl.notMem hj

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

Goal state before:
pp: case h
𝕜 : Type u_1
E : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
c : ℝ
x : E
hx : x ≠ 0
r : 𝕜
hr : c / ‖x‖ < ‖r‖
⊢ c < ‖r‖ * ‖x‖

Tactic:
← div_lt_iff₀

Goal state after:
case h
𝕜 : Type u_1
E : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
c : ℝ
x : E
hx : x ≠ 0
r : 𝕜
hr : c / ‖x‖ < ‖r‖
⊢ c / ‖x‖ < ‖r‖

case h
𝕜 : Type u_1
E : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
c : ℝ
x : E
hx : x ≠ 0
r : 𝕜
hr : c / ‖x‖ < ‖r‖
⊢ 0 < ‖x‖
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: case h₁
β : Type u_2
inst✝¹ : MeasurableSpace β
inst✝ : Countable β
x : β
s : β → Set β
hs : ∀ y ∉ measurableAtom x, x ∈ s y ∧ MeasurableSet (s y) ∧ y ∉ s y
⊢ measurableAtom x ⊆ ⋂ y ∈ (measurableAtom x)ᶜ, s y

pp: case h₂
β : Type u_2
inst✝¹ : MeasurableSpace β
inst✝ : Countable β
x : β
s : β → Set β
hs : ∀ y ∉ measurableAtom x, x ∈ s y ∧ MeasurableSet (s y) ∧ y ∉ s y
⊢ ⋂ y ∈ (measurableAtom x)ᶜ, s y ⊆ measurableAtom x

Tactic:
· intro z hz
      simp only [mem_iInter, mem_compl_iff]
      intro i hi
      exact mem_of_mem_measurableAtom hz (hs i hi).2.1 (hs i hi).1

Goal state after:
case h₂
β : Type u_2
inst✝¹ : MeasurableSpace β
inst✝ : Countable β
x : β
s : β → Set β
hs : ∀ y ∉ measurableAtom x, x ∈ s y ∧ MeasurableSet (s y) ∧ y ∉ s y
⊢ ⋂ y ∈ (measurableAtom x)ᶜ, s y ⊆ measurableAtom x
Module: Mathlib.MeasureTheory.OuterMeasure.Operations

Goal state before:
pp: α : Type u_1
β : Type u_3
f : α → β
m m' : OuterMeasure α
s : Set β
⊢ ((map f) (m ⊔ m')) s = ((map f) m ⊔ (map f) m') s

Tactic:
by simp only [map_apply, sup_apply]

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

Goal state before:
pp: s : SignType
z : ℤ
hz : Odd z
⊢ s ^ z = s

Tactic:
obtain rfl | hs := eq_or_ne s 0

Goal state after:
case inl
z : ℤ
hz : Odd z
⊢ 0 ^ z = 0

case inr
s : SignType
z : ℤ
hz : Odd z
hs : s ≠ 0
⊢ s ^ z = s
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: α : Type u
inst✝¹ : Nonempty α
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
n : ℕ
h : ∑ i ∈ s, (f i).natAbs ≤ n
β : Type u
w✝ : Fintype β
sgn : β → SignType
g : β → α
hg : ∀ (b : β), g b ∈ s
hβ : Fintype.card β = ∑ a ∈ s, (f a).natAbs
hf : ∀ a ∈ s, (∑ b, if g b = a then ↑(sgn b) else 0) = f a
a : α
ha : a ∈ s
⊢ (∑ i,
      if Sum.elim g (Classical.arbitrary (Fin (n - ∑ i ∈ s, (f i).natAbs) → α)) i = a then ↑(Sum.elim sgn 0 i) else 0) =
    f a

Tactic:
by simp [hf _ ha]

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

Goal state before:
pp: x : ℝ
⊢ ↑(ENNReal.ofReal ↑(Real.nnabs x)) = ↑↑(Real.nnabs x)

Tactic:
ENNReal.ofReal_coe_nnreal

Goal state after:
x : ℝ
⊢ ↑↑(Real.nnabs x) = ↑↑(Real.nnabs x)
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f : α → β
inst✝ : LinearOrder β
s : Set α
ne_s : s.Nonempty
hs : IsCompact s
hf : LowerSemicontinuousOn f s
x✝¹ : Nonempty α
x✝ : Nonempty ↑s
φ : β → Filter α := fun b ↦ 𝓟 (s ∩ f ⁻¹' Iic b)
⊢ ∃ a ∈ s, ∀ x ∈ s, f a ≤ f x

Tactic:
let ℱ : Filter α := ⨅ a : s, φ (f a)

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f : α → β
inst✝ : LinearOrder β
s : Set α
ne_s : s.Nonempty
hs : IsCompact s
hf : LowerSemicontinuousOn f s
x✝¹ : Nonempty α
x✝ : Nonempty ↑s
φ : β → Filter α := fun b ↦ 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ a, φ (f ↑a)
⊢ ∃ a ∈ s, ∀ x ∈ s, f a ≤ f x
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: b : EReal
h : 0 < b
h' : b ≠ ⊤
a a' : EReal
a_lt_a' : a < a'
hyp : a / b = a' / b
⊢ a = a'

Tactic:
← @EReal.mul_div_cancel a b (ne_bot_of_gt h) h' h.ne',

Goal state after:
b : EReal
h : 0 < b
h' : b ≠ ⊤
a a' : EReal
a_lt_a' : a < a'
hyp : a / b = a' / b
⊢ b * (a / b) = a'
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
s : Set α
ι : Type u_4
f : ι → α → β
inst✝ : Preorder β
I : Set ι
hfy : ∀ i ∈ I, LowerSemicontinuousOn (f i) s
M : α → ι
M_mem : ∀ x ∈ s, M x ∈ I
M_max : ∀ x ∈ s, IsMaxOn (fun y ↦ f y x) I (M x)
x : α
hx : x ∈ s
b : β
hb : (fun x ↦ f (M x) x) x > b
z : α
hz : z ∈ s
h : f (M x) z > b
⊢ (fun x ↦ f (M x) x) z > b

Tactic:
exact lt_of_lt_of_le h (M_max z hz (M_mem x hx))

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

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIciTopology γ
f : α → γ
s : Set α
hs : IsClosed[inst✝³] s
⊢ (∀ x ∈ s, ∀ y < f x, ∀ᶠ (x' : α) in 𝓝[s] x, y < f x') ↔ IsClosed[instTopologicalSpaceProd] {p | p.1 ∈ s ∧ f p.1 ≤ p.2}

Tactic:
eventually_nhdsWithin_iff,

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIciTopology γ
f : α → γ
s : Set α
hs : IsClosed[inst✝³] s
⊢ (∀ x ∈ s, ∀ y < f x, ∀ᶠ (x : α) in 𝓝 x, x ∈ s → y < f x) ↔
    IsClosed[instTopologicalSpaceProd] {p | p.1 ∈ s ∧ f p.1 ≤ p.2}
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case convert_2
𝕜 : Type u_4
inst✝⁵ : DivisionSemiring 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : ContinuousSMul ℚ≥0 𝕜
inst✝¹ : IsTopologicalSemiring 𝕜
inst✝ : ContinuousInv₀ 𝕜
x : 𝕜
⊢ ℕ → 𝕜

pp: case convert_5
𝕜 : Type u_4
inst✝⁵ : DivisionSemiring 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : ContinuousSMul ℚ≥0 𝕜
inst✝¹ : IsTopologicalSemiring 𝕜
inst✝ : ContinuousInv₀ 𝕜
x : 𝕜
n : ℕ
hn : n ≠ 0
⊢ ?convert_2 n = ↑n / (↑n + x)

pp: case convert_6
𝕜 : Type u_4
inst✝⁵ : DivisionSemiring 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : ContinuousSMul ℚ≥0 𝕜
inst✝¹ : IsTopologicalSemiring 𝕜
inst✝ : ContinuousInv₀ 𝕜
x : 𝕜
⊢ Tendsto ?convert_2 atTop (𝓝 1)

Tactic:
· exact fun n : ℕ ↦ 1 / (1 + x / n)

Goal state after:
case convert_5
𝕜 : Type u_4
inst✝⁵ : DivisionSemiring 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : ContinuousSMul ℚ≥0 𝕜
inst✝¹ : IsTopologicalSemiring 𝕜
inst✝ : ContinuousInv₀ 𝕜
x : 𝕜
n : ℕ
hn : n ≠ 0
⊢ 1 / (1 + x / ↑n) = ↑n / (↑n + x)

case convert_6
𝕜 : Type u_4
inst✝⁵ : DivisionSemiring 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : ContinuousSMul ℚ≥0 𝕜
inst✝¹ : IsTopologicalSemiring 𝕜
inst✝ : ContinuousInv₀ 𝕜
x : 𝕜
⊢ Tendsto (fun n ↦ 1 / (1 + x / ↑n)) atTop (𝓝 1)
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
h₁ : limsup u f ≠ 0 ∨ limsup v f ≠ ⊤
h₂ : limsup u f ≠ ⊤ ∨ limsup v f ≠ 0
⊢ limsup (u * v) f ≤ limsup u f * limsup v f

Tactic:
by
  rcases f.eq_or_neBot with rfl | _
  · rw [limsup_bot]; exact bot_le
  have u_0 : 0 ≤ limsup u f := le_limsup_of_frequently_le hu
  replace h₁ : 0 < limsup u f ∨ limsup v f ≠ ⊤ := h₁.imp_left fun h ↦ lt_of_le_of_ne u_0 h.symm
  replace h₂ : limsup u f ≠ ⊤ ∨ 0 < limsup v f :=
    h₂.imp_right fun h ↦ lt_of_le_of_ne (le_limsup_of_frequently_le hv.frequently) h.symm
  refine le_mul_of_forall_lt h₁ h₂ fun a a_u b b_v ↦ (limsup_le_iff).2 fun c c_ab ↦ ?_
  filter_upwards [eventually_lt_of_limsup_lt a_u, eventually_lt_of_limsup_lt b_v, hv]
    with x x_a x_b v_0
  apply lt_of_le_of_lt _ c_ab
  rcases lt_or_ge (u x) 0 with hux | hux
  · apply (mul_nonpos_iff.2 (.inr ⟨hux.le, v_0⟩)).trans
    exact mul_nonneg (u_0.trans a_u.le) (v_0.trans x_b.le)
  · exact mul_le_mul x_a.le x_b.le v_0 (hux.trans x_a.le)

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

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
r C : ℝ≥0∞
f : ℕ → α
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * r ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
⊢ edist (f n) a ≤ C * r ^ n / (1 - r)

Tactic:
by
  convert! edist_le_tsum_of_edist_le_of_tendsto _ hu ha _
  simp only [pow_add, ENNReal.tsum_mul_left, ENNReal.tsum_geometric, div_eq_mul_inv, mul_assoc]

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

Goal state before:
pp: case h.refine_1
x : ℝ
⊢ ∀ y ∈ Ioi (max (↑x) 0) ×ˢ Ioi 1, ↑x < y.1 * y.2

Tactic:
intro p p_in_prod
    simp only [Set.mem_prod, Set.mem_Ioi, max_lt_iff] at p_in_prod
    rcases p_in_prod with ⟨⟨p1_gt_x, p1_pos⟩, p2_gt_1⟩
    have := mul_le_mul_of_nonneg_left (le_of_lt p2_gt_1) (le_of_lt p1_pos)
    rw [mul_one p.1] at this
    exact lt_of_lt_of_le p1_gt_x this

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι✝ : Type u_3
ε : ℝ
hε : 0 < ε
ι : Type ?u.11
inst✝ : Encodable ι
f : ℕ → ℝ := fun n ↦ ε / 2 / 2 ^ n
hf : HasSum f ε
⊢ { ε' // (∀ (i : ι), 0 < ε' i) ∧ ∃ c, HasSum ε' c ∧ c ≤ ε }

Tactic:
have f0 : ∀ n, 0 < f n := fun n ↦ div_pos (half_pos hε) (pow_pos zero_lt_two _)

Goal state after:
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ε : ℝ
hε : 0 < ε
ι : Type ?u.11
inst✝ : Encodable ι
f : ℕ → ℝ := fun n ↦ ε / 2 / 2 ^ n
hf : HasSum f ε
f0 : ∀ (n : ℕ), 0 < f n
⊢ { ε' // (∀ (i : ι), 0 < ε' i) ∧ ∃ c, HasSum ε' c ∧ c ≤ ε }
Module: Mathlib.Order.SetDissipate

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Preorder α
s : α → Set β
x : α
⊢ ⋂ y, ⋂ (_ : y ≤ x), dissipate s y = dissipate s x

Tactic:
apply Subset.antisymm
  · apply iInter_mono fun z y hy ↦ ?_
    simp only [mem_iInter, mem_dissipate] at *
    exact fun h ↦ hy h z le_rfl
  · simp only [subset_iInter_iff]
    exact fun i j ↦ dissipate_subset_dissipate j

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

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
⊢ v ∈ 𝓝 (f x) → v ∈ map f (𝓝[s] x)

Tactic:
hv

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
⊢ v ∈ map f (𝓝[s] x)
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case bot.top
h₁ : (⊥, ⊤).1 ≠ 0 ∨ (⊥, ⊤).2 ≠ ⊥
h₂ : (⊥, ⊤).1 ≠ 0 ∨ (⊥, ⊤).2 ≠ ⊤
h₃ : (⊥, ⊤).1 ≠ ⊥ ∨ (⊥, ⊤).2 ≠ 0
h₄ : (⊥, ⊤).1 ≠ ⊤ ∨ (⊥, ⊤).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊥, ⊤)

Tactic:
exact EReal.neg_top ▸ continuousAt_mul_symm1 continuousAt_mul_top_top

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

Goal state before:
pp: case top.coe
a✝ : ℝ
h₁ : (⊤, ↑a✝).1 ≠ 0 ∨ (⊤, ↑a✝).2 ≠ ⊥
h₂ : (⊤, ↑a✝).1 ≠ 0 ∨ (⊤, ↑a✝).2 ≠ ⊤
h₃ : (⊤, ↑a✝).1 ≠ ⊥ ∨ (⊤, ↑a✝).2 ≠ 0
h₄ : (⊤, ↑a✝).1 ≠ ⊤ ∨ (⊤, ↑a✝).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊤, ↑a✝)

Tactic:
simp only [ne_eq, not_true_eq_false, EReal.coe_eq_zero, false_or] at h₄

Goal state after:
case top.coe
a✝ : ℝ
h₁ : (⊤, ↑a✝).1 ≠ 0 ∨ (⊤, ↑a✝).2 ≠ ⊥
h₂ : (⊤, ↑a✝).1 ≠ 0 ∨ (⊤, ↑a✝).2 ≠ ⊤
h₃ : (⊤, ↑a✝).1 ≠ ⊥ ∨ (⊤, ↑a✝).2 ≠ 0
h₄ : ¬a✝ = 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊤, ↑a✝)
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: α : Type u_2
f : Filter α
m : α → EReal
a b : EReal
hm : Tendsto m f (𝓝 b)
h₁ : a ≠ ⊥ ∨ b ≠ 0
h₂ : a ≠ ⊤ ∨ b ≠ 0
this : a = 0
⊢ Tendsto (fun b ↦ a * m b) f (𝓝 (a * b))

Tactic:
simp [this, tendsto_const_nhds]

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) ⋯
eq : MeasurableSet = DynkinSystem.GenerateHas s
⊢ ∀ (t : Set α) (ht : MeasurableSet t), C t ht

Tactic:
suffices ∀ t (ht : DynkinSystem.GenerateHas s t), C t (eq ▸ ht) from
    fun t ht ↦ this t (eq ▸ ht)

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) ⋯
eq : MeasurableSet = DynkinSystem.GenerateHas s
⊢ ∀ (t : Set α) (ht : DynkinSystem.GenerateHas s t), C t ⋯
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hsm : Antitone s
hs : ∃ᶠ (i : ι) in atTop, MeasurableSet (s i)
⊢ MeasurableSet (⋂ i, s i)

Tactic:
← compl_iff,

Goal state after:
α : Type u_1
inst✝² : MeasurableSpace α
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hsm : Antitone s
hs : ∃ᶠ (i : ι) in atTop, MeasurableSet (s i)
⊢ MeasurableSet (⋂ i, s i)ᶜ
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: α : Type u_1
inst✝³ : MeasurableSpace α
ι : Type u_5
inst✝² : Preorder ι
inst✝¹ : IsDirectedOrder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hsm : Antitone s
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ MeasurableSet (⋂ i, s i)

Tactic:
← compl_iff,

Goal state after:
α : Type u_1
inst✝³ : MeasurableSpace α
ι : Type u_5
inst✝² : Preorder ι
inst✝¹ : IsDirectedOrder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hsm : Antitone s
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ MeasurableSet (⋂ i, s i)ᶜ
Module: Mathlib.MeasureTheory.Measure.AEDisjoint

Goal state before:
pp: α : Type u_2
m : MeasurableSpace α
μ : Measure α
s t : Set α
h : Disjoint s t
⊢ μ ∅ = 0

Tactic:
measure_empty

Goal state after:
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s t : Set α
h : Disjoint s t
⊢ 0 = 0
Module: Mathlib.MeasureTheory.Measure.NullMeasurable

Goal state before:
pp: case refine_2
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
htm : MeasurableSet t
hst : s =ᵐ[μ] t
this : toMeasurable μ (s \ t) =ᵐ[μ] ∅
⊢ t ∪ toMeasurable μ (s \ t) =ᵐ[μ] s

Tactic:
simpa only [union_empty] using hst.symm.union this

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSingletonClass (NullMeasurableSpace α μ)
s : Finset α
⊢ NullMeasurableSet (↑s) μ

Tactic:
apply Finset.measurableSet

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

Goal state before:
pp: α : Type u_2
β : Type u_3
m : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
g : α → β
hf : NullMeasurable f μ
hg : f =ᵐ[μ] g
⊢ NullMeasurable g μ

Tactic:
by
  rw [nullMeasurable_iff_eventuallyMeasurable]
  exact EventuallyMeasurable.congr hf hg.symm

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

Goal state before:
pp: case pos.mpr
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s : Set X
b : X
hsne : s.Nonempty
this : Nonempty ↑s
hsub : s ⊆ Iio b
⊢ (∀ a < b, (s ∩ Ioo a b).Nonempty) → comap Subtype.val (𝓝[<] b) = atTop

Tactic:
· intro h
      refine (nhdsLT_basis_of_exists_lt (hsne.mono hsub)).comap _ |>.ext atTop_basis ?_ ?_
      · intro a hab
        rcases h a hab with ⟨c, hcs, hc⟩
        use ⟨c, hcs⟩
        simp_all [subset_def, hc.1.trans_le]
      · rintro ⟨a, has⟩ -
        use a, hsub has
        simp_all [subset_def, le_of_lt]

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

Goal state before:
pp: X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s : Set X
a : X
hsa : s ⊆ Ioi a
hs : s.Nonempty → ∃ b > a, Ioo a b ⊆ s
ha : IsPredPrelimit a
⊢ comap Subtype.val (𝓝[>] a) = atBot

Tactic:
refine comap_coe_nhdsLT_of_Ioo_subset (show ofDual ⁻¹' s ⊆ Iio (toDual a) from hsa) ?_ ha.dual

Goal state after:
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s : Set X
a : X
hsa : s ⊆ Ioi a
hs : s.Nonempty → ∃ b > a, Ioo a b ⊆ s
ha : IsPredPrelimit a
⊢ (⇑ofDual ⁻¹' s).Nonempty → ∃ a_2 < toDual a, Ioo a_2 (toDual a) ⊆ ⇑ofDual ⁻¹' s
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
n : ℕ
⊢ spanningSetsIndex μ ⁻¹' {n} = disjointed (spanningSets μ) n

Tactic:
classical
  exact preimage_find_eq_disjointed _ _ _

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S T : Set (Set α)
h_gen : m0 = generateFrom S
h_inter : IsPiSystem S
h_sub : T ⊆ S
hc : T.Countable
hU : ⋃₀ T = univ
htop : ∀ s ∈ T, μ s ≠ ∞
h_eq : ∀ s ∈ S, μ s = ν s
t : Set α
ht : t ∈ T
s : Set α
hs : s ∈ S
⊢ μ (s ∩ t) = ν (s ∩ t)

Tactic:
rcases (s ∩ t).eq_empty_or_nonempty with H | H

Goal state after:
case inl
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S T : Set (Set α)
h_gen : m0 = generateFrom S
h_inter : IsPiSystem S
h_sub : T ⊆ S
hc : T.Countable
hU : ⋃₀ T = univ
htop : ∀ s ∈ T, μ s ≠ ∞
h_eq : ∀ s ∈ S, μ s = ν s
t : Set α
ht : t ∈ T
s : Set α
hs : s ∈ S
H : s ∩ t = ∅
⊢ μ (s ∩ t) = ν (s ∩ t)

case inr
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S T : Set (Set α)
h_gen : m0 = generateFrom S
h_inter : IsPiSystem S
h_sub : T ⊆ S
hc : T.Countable
hU : ⋃₀ T = univ
htop : ∀ s ∈ T, μ s ≠ ∞
h_eq : ∀ s ∈ S, μ s = ν s
t : Set α
ht : t ∈ T
s : Set α
hs : s ∈ S
H : (s ∩ t).Nonempty
⊢ μ (s ∩ t) = ν (s ∩ t)
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
inst✝ : IsEmpty α
x✝ : MeasurableSpace α
μ : Measure α
s : Set α
⊢ μ ∅ = 0

Tactic:
measure_empty

Goal state after:
α : Type u_1
inst✝ : IsEmpty α
x✝ : MeasurableSpace α
μ : Measure α
s : Set α
⊢ 0 = 0
Module: Mathlib.Data.Set.MemPartition

Goal state before:
pp: case zero
α : Type u_1
f : ℕ → Set α
u v : Set α
hu : u ∈ memPartition f 0
⊢ v ∈ memPartition f 0 → u ≠ v → Disjoint u v

Tactic:
hv

Goal state after:
case zero
α : Type u_1
f : ℕ → Set α
u v : Set α
hu : u ∈ memPartition f 0
hv : v ∈ memPartition f 0
⊢ u ≠ v → Disjoint u v
Module: Mathlib.Data.Set.MemPartition

Goal state before:
pp: case zero
α : Type u_1
f : ℕ → Set α
u v : Set α
huv : univ ≠ v
hu : u = univ
hv : v = univ
⊢ Disjoint u v

Tactic:
hv

Goal state after:
case zero
α : Type u_1
f : ℕ → Set α
u v : Set α
huv : univ ≠ univ
hu : u = univ
hv : v = univ
⊢ Disjoint u v
Module: Mathlib.Data.Set.MemPartition

Goal state before:
pp: case succ
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α}, u ∈ memPartition f n → v ∈ memPartition f n → u ≠ v → Disjoint u v
u v : Set α
hu : u ∈ memPartition f (n + 1)
⊢ v ∈ memPartition f (n + 1) → u ≠ v → Disjoint u v

Tactic:
hv

Goal state after:
case succ
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α}, u ∈ memPartition f n → v ∈ memPartition f n → u ≠ v → Disjoint u v
u v : Set α
hu : u ∈ memPartition f (n + 1)
hv : v ∈ memPartition f (n + 1)
⊢ u ≠ v → Disjoint u v
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 : μ ({a | ¬f a = b} ∩ sᶜ) = 0
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
⊢ μ (f ⁻¹' t) ≤ μ (f ⁻¹' t ∩ s)

Tactic:
apply (measure_mono (Eq.symm (inter_union_compl (f ⁻¹' t) s)).le).trans

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 : μ ({a | ¬f a = b} ∩ sᶜ) = 0
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
⊢ μ (f ⁻¹' t ∩ s ∪ f ⁻¹' t ∩ sᶜ) ≤ μ (f ⁻¹' t ∩ s)
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : SigmaFinite μ
r : ℝ≥0∞
hs : MeasurableSet s
h's : r < μ s
⊢ ∃ t, MeasurableSet t ∧ t ⊆ s ∧ r < μ t ∧ μ t < ∞

Tactic:
← iSup_restrict_spanningSets,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : SigmaFinite μ
r : ℝ≥0∞
hs : MeasurableSet s
h's : r < ⨆ i, (μ.restrict (spanningSets μ i)) s
⊢ ∃ t, MeasurableSet t ∧ t ⊆ s ∧ r < μ t ∧ μ t < ∞
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable α
hμ : ∀ (a : α), μ {a} < ∞
h✝ : Nonempty α
f : ℕ → α
hf : Surjective f
⊢ ⋃ i, {f i} = univ

Tactic:
by simp [hf.range_eq]

Goal state after: