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
x y : X
⊢ d x y = 0 ↔ ∀ (i : ℕ), True → (x, y) ∈ U i

Tactic:
simp only [d, true_imp_iff]

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
x y : X
⊢ (if h : ∃ n, (x, y) ∉ U n then (1 / 2) ^ Nat.find h else 0) = 0 ↔ ∀ (i : ℕ), (x, y) ∈ U i
Module: Mathlib.Topology.MetricSpace.Lipschitz

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
K : ℝ≥0
f : α → α
hf : LipschitzWith K f
x : α
n : ℕ
⊢ dist (f^[n] x) ((f^[n] ∘ f) x) ≤ ↑K ^ n * dist x (f x)

Tactic:
simpa only [NNReal.coe_pow] using! (hf.iterate n).dist_le_mul x (f x)

Goal state after:
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‖ ≤ ‖b‖

Tactic:
apply solid

Goal state after:
α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
a b : α
h : b ⊓ -b ≤ a ⊓ -a
⊢ |a| ≤ |b|
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|

Tactic:
rw [← neg_inf]

Goal state after:
α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
a b : α
h : b ⊓ -b ≤ a ⊓ -a
⊢ -(-a ⊓ a) ≤ |b|
Module: Mathlib.Analysis.Normed.Ring.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝⁵ : SeminormedAddCommGroup α
inst✝⁴ : One α
inst✝³ : NormOneClass α
inst✝² : SeminormedAddCommGroup β
inst✝¹ : One β
inst✝ : NormOneClass β
⊢ ‖1‖ = 1

Tactic:
by simp [Prod.norm_def]

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

Goal state before:
pp: α : Type u_2
inst✝ : SeminormedRing α
a b : αˣ
⊢ (‖(↑a - 1) * (↑b - 1)‖ + ‖(↑b - 1) * (↑a - 1)‖) * ‖↑a⁻¹‖ * ‖↑b⁻¹‖ ≤
    (‖↑a - 1‖ * ‖↑b - 1‖ + ‖↑b - 1‖ * ‖↑a - 1‖) * ‖↑a⁻¹‖ * ‖↑b⁻¹‖

Tactic:
by
      gcongr <;> exact norm_mul_le ..

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

Goal state before:
pp: α : Type u_5
inst✝¹ : Fintype α
ι : α → Type u
inst✝ : ∀ (a : α), Finite (ι a)
f : (a : α) → ι a → ℝ
hf₀ : ∀ (a : α) (i : ι a), 0 ≤ f a i
⊢ ⨆ i, ∏ a, f a (i a) = ∏ a, ⨆ i, f a i

Tactic:
by
  rcases isEmpty_or_nonempty ((a : α) → ι a) with h | h
  · rw [iSup_of_isEmpty, eq_comm, Finset.prod_eq_zero_iff]
    obtain ⟨a, ha⟩ := isEmpty_pi.mp h
    exact ⟨a, by simp⟩
  refine le_antisymm ?_ ?_
  · exact ciSup_le fun i ↦ Finset.prod_le_prod (by simp [hf₀])
      fun a ha ↦ Finite.le_ciSup_of_le _ le_rfl
  · rw [Classical.nonempty_pi] at h
    have H a : ∃ i : ι a, f a i = ⨆ i, f a i := exists_eq_ciSup_of_finite
    choose i hi using H
    simp only [← hi]
    exact Finite.le_ciSup_of_le i le_rfl

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

Goal state before:
pp: α : Type u_1
inst✝¹ : NormedDivisionRing α
X : Type u_4
ι : Type u_5
inst✝ : TopologicalSpace X
F : ι → X → α
f : X → α
l : Filter ι
hF : TendstoLocallyUniformlyOn F f l Set.univ
hf : ∀ (x : X), Disjoint (map f (𝓝 x)) (𝓝 0)
⊢ TendstoLocallyUniformlyOn F⁻¹ f⁻¹ l Set.univ

Tactic:
apply hF.inv₀_of_disjoint

Goal state after:
α : Type u_1
inst✝¹ : NormedDivisionRing α
X : Type u_4
ι : Type u_5
inst✝ : TopologicalSpace X
F : ι → X → α
f : X → α
l : Filter ι
hF : TendstoLocallyUniformlyOn F f l Set.univ
hf : ∀ (x : X), Disjoint (map f (𝓝 x)) (𝓝 0)
⊢ ∀ x ∈ Set.univ, Disjoint (map f (𝓝[Set.univ] x)) (𝓝 0)
Module: Mathlib.MeasureTheory.MeasurableSpace.Defs

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s t : Set α
hs : MeasurableSet s
h : s = t
⊢ MeasurableSet t

Tactic:
← h

Goal state after:
α : Type u_1
m : MeasurableSpace α
s t : Set α
hs : MeasurableSet s
h : s = t
⊢ MeasurableSet s
Module: Mathlib.GroupTheory.GroupAction.IterateAct

Goal state before:
pp: α : Type u_1
f : α → α
x✝ : IterateMulAct f
⊢ 1 * x✝ = x✝

Tactic:
ext; apply Nat.zero_add

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f g : α → β
m : MeasurableSpace α
mβ : MeasurableSpace β
x✝ : DecidablePred fun x ↦ x ∈ s
hs : MeasurableSet s
hf : Measurable f
hg : Measurable g
t : Set β
ht : MeasurableSet t
⊢ MeasurableSet (s.piecewise f g ⁻¹' t)

Tactic:
by simpa [piecewise_preimage] using hs.ite (hf ht) (hg ht)

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

Goal state before:
pp: α : Type u_1
ι : Sort u_7
m : ι → MeasurableSpace α
s : Set α
⊢ (∀ m_1 ∈ range m, MeasurableSet s) ↔ ∀ (i : ι), MeasurableSet s

Tactic:
forall_mem_range

Goal state after:
α : Type u_1
ι : Sort u_7
m : ι → MeasurableSpace α
s : Set α
⊢ (∀ (i : ι), MeasurableSet s) ↔ ∀ (i : ι), MeasurableSet s
Module: Mathlib.MeasureTheory.MeasurableSpace.Defs

Goal state before:
pp: α : Type u_1
ι : Sort u_7
m : ι → MeasurableSpace α
s : Set α
⊢ MeasurableSet s ↔ GenerateMeasurable {s | ∃ i, MeasurableSet s} s

Tactic:
unfold iSup

Goal state after:
α : Type u_1
ι : Sort u_7
m : ι → MeasurableSpace α
s : Set α
⊢ MeasurableSet s ↔ GenerateMeasurable {s | ∃ i, MeasurableSet s} s
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedRing 𝕜'
inst✝¹ : NormedAlgebra 𝕜 𝕜'
inst✝ : NormOneClass 𝕜'
⊢ Isometry ⇑(algebraMap 𝕜 𝕜')

Tactic:
refine Isometry.of_dist_eq fun x y => ?_

Goal state after:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedRing 𝕜'
inst✝¹ : NormedAlgebra 𝕜 𝕜'
inst✝ : NormOneClass 𝕜'
x y : 𝕜
⊢ dist ((algebraMap 𝕜 𝕜') x) ((algebraMap 𝕜 𝕜') y) = dist x y
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: case pos
α : Type u_1
mα : MeasurableSpace α
f : α → Prop
h : MeasurableSet (f ⁻¹' {True})
x : Prop
hx : x
⊢ MeasurableSet (f ⁻¹' {x})

Tactic:
simpa [hx] using h

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

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
μ : F
ι : Sort u_4
inst✝ : Countable ι
s : ι → Set α
⊢ (∀ s_1 ∈ range s, μ s_1 = 0) ↔ ∀ (i : ι), μ (s i) = 0

Tactic:
forall_mem_range

Goal state after:
α : Type u_1
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
μ : F
ι : Sort u_4
inst✝ : Countable ι
s : ι → Set α
⊢ (∀ (i : ι), μ (s i) = 0) ↔ ∀ (i : ι), μ (s i) = 0
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 : ℝ
hC : ⇑f '' ball 0 δ ⊆ ball 0 C
ε : ℝ
hε : 0 < ε
⊢ ∃ δ > 0, ∀ ⦃x : G⦄, ‖x‖ < δ → ‖f x‖ < ε

Tactic:
simp only [subset_def, mem_image, mem_ball, dist_zero_right, forall_exists_index, and_imp,
    forall_apply_eq_imp_iff₂] at hC

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
⊢ ∃ δ > 0, ∀ ⦃x : G⦄, ‖x‖ < δ → ‖f 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

Tactic:
intro z

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
z : β
⊢ z ∈ measurableAtom x → z ∈ ⋂ y ∈ (measurableAtom x)ᶜ, s y
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)ᶜ

Tactic:
intro z

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
z : β
⊢ z ∈ (measurableAtom x)ᶜ → z ∈ (⋂ y ∈ (measurableAtom x)ᶜ, s y)ᶜ
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: β : Type u_2
inst✝ : MeasurableSpace β
x y : β
hx : x ∈ measurableAtom y
⊢ measurableAtom x ⊆ measurableAtom y

Tactic:
intro z

Goal state after:
β : Type u_2
inst✝ : MeasurableSpace β
x y : β
hx : x ∈ measurableAtom y
z : β
⊢ z ∈ measurableAtom x → z ∈ measurableAtom y
Module: Mathlib.Topology.Algebra.Algebra

Goal state before:
pp: R : Type u_1
A : Type u
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : TopologicalSpace R
inst✝¹ : TopologicalSpace A
inst✝ : ContinuousSMul R A
⊢ Continuous[inst✝², inst✝¹] ⇑(algebraMap R A)

Tactic:
rw [algebraMap_eq_smul_one']

Goal state after:
R : Type u_1
A : Type u
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : TopologicalSpace R
inst✝¹ : TopologicalSpace A
inst✝ : ContinuousSMul R A
⊢ Continuous[inst✝², inst✝¹] fun r ↦ r • 1
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
⊢ sign a = 0 ↔ a = 0

Tactic:
refine ⟨fun h => ?_, fun h => h.symm ▸ sign_zero⟩
  rw [sign_apply] at h
  split_ifs at h with h_1 h_2
  cases h
  exact (le_of_not_gt h_1).eq_of_not_lt h_2

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
x : α
⊢ LowerHemicontinuousAt f x ↔ ∀ (t : Set β), IsClosed[inst✝] t → (∃ᶠ (x' : α) in 𝓝 x, f x' ⊆ t) → f x ⊆ t

Tactic:
rw [← lowerHemicontinuousWithinAt_univ_iff, lowerHemicontinuousWithinAt_iff_frequently]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
x : α
⊢ (∀ (t : Set β), IsClosed[inst✝] t → (∃ᶠ (x' : α) in 𝓝[univ] x, f x' ⊆ t) → f x ⊆ t) ↔
    ∀ (t : Set β), IsClosed[inst✝] t → (∃ᶠ (x' : α) in 𝓝 x, f x' ⊆ t) → f x ⊆ t
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case coe
x : ℝ
⊢ (↑x)⁻¹ < ⊤

Tactic:
exact (coe_inv x).symm ▸ coe_lt_top (x⁻¹)

Goal state after:
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)
ℱ : Filter α := ⨅ a, φ (f ↑a)
this : ℱ.NeBot
⊢ ∃ a ∈ s, ∀ x ∈ s, f a ≤ f x

Tactic:
have hℱs : ℱ ≤ 𝓟 s :=
    iInf_le_of_le (Classical.choice inferInstance) (principal_mono.mpr <| inter_subset_left)

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)
this : ℱ.NeBot
hℱs : ℱ ≤ 𝓟 s
⊢ ∃ a ∈ s, ∀ x ∈ s, f a ≤ f x
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
⊢ ∀ x_1 ∈ s, (fun x1 x2 ↦ f (M x) x1 > x2) x_1 b → (fun x1 x2 ↦ (fun x ↦ f (M x) x) x1 > x2) x_1 b

Tactic:
intro z

Goal state after:
α : 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 : α
⊢ z ∈ s → (fun x1 x2 ↦ f (M x) x1 > x2) z b → (fun x1 x2 ↦ (fun x ↦ f (M x) x) x1 > x2) z b
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: ⊢ 𝓝[≠] ⊥ = map Real.toEReal atBot

Tactic:
apply (nhdsWithin_hasBasis nhds_bot_basis_Iic _).ext (atBot_basis.map Real.toEReal)
  · simp only [EReal.image_coe_Iic,
      true_and]
    intro x hx
    by_cases hx_top : x = ⊤
    · simp [hx_top]
    lift x to ℝ using ⟨hx_top, hx.ne_bot⟩
    refine ⟨x, fun x ⟨h1, h2⟩ ↦ ?_⟩
    simp [h2, h1.ne_bot]
  · simp only [EReal.image_coe_Iic, true_implies]
    refine fun x ↦ ⟨x, ⟨EReal.bot_lt_coe x, fun x ⟨(h1 : x ≤ _), h2⟩ ↦ ?_⟩⟩
    simp [h1, Ne.bot_lt' fun a ↦ h2 a.symm]

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

Goal state before:
pp: a b c : EReal
h : 0 ≤ c
⊢ (a + b) / c = a / c + b / c

Tactic:
by
  apply right_distrib_of_nonneg_of_ne_top (inv_nonneg_of_nonneg h) (inv_lt_top c).ne

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

Goal state before:
pp: case inr
α : Type u_3
f : Filter α
u v : α → EReal
a b : EReal
ha : limsup u f < a
hb : limsup v f ≤ b
h : b < ⊤
⊢ limsup (u + v) f ≤ a + b

Tactic:
exact (limsup_add_le (.inr (hb.trans_lt h).ne) (.inl ha.ne_top)).trans (add_le_add ha.le hb)

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)
⊢ edist (f 0) a ≤ C / (1 - r)

Tactic:
by
  simpa only [_root_.pow_zero, mul_one] using edist_le_of_edist_le_geometric_of_tendsto r C hu ha 0

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

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Nonempty
⊢ ⊤ s ≤ ⊤ s

Tactic:
rw [top_apply hs]

Goal state after:
α : Type u_1
s : Set α
hs : s.Nonempty
⊢ ∞ ≤ ⊤ s
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case neg
α : 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₁ : ∀ (x_1 : γ), f x ≤ x_1
hx₂ : ∀ (x_1 : γ), g x ≤ x_1
⊢ ∀ (x : α), (fun x1 x2 ↦ (fun z ↦ f z + g z) x1 > x2) x y

Tactic:
intro z

Goal state after:
case neg
α : 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₁ : ∀ (x_1 : γ), f x ≤ x_1
hx₂ : ∀ (x_1 : γ), g x ≤ x_1
z : α
⊢ (fun x1 x2 ↦ (fun z ↦ f z + g z) x1 > x2) z y
Module: Mathlib.Analysis.SpecificLimits.Basic

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

Tactic:
refine (one_div_le_one_div ?_ ?_).mpr (pow_right_mono₀ hm.le (fi a))

Goal state after:
case refine_1
m : ℝ
f : ℕ → ℕ
hm : 1 < m
fi : ∀ (i : ℕ), i ≤ f i
a : ℕ
⊢ 0 < m ^ f a

case refine_2
m : ℝ
f : ℕ → ℕ
hm : 1 < m
fi : ∀ (i : ℕ), i ≤ f i
a : ℕ
⊢ 0 < m ^ a
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: R : Type u_1
α : Type u_2
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
inst✝⁴ : Semiring R
inst✝³ : IsDomain R
inst✝² : Module R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : Module.IsTorsionFree R ℝ≥0∞
c : R
hc : c ≠ 0
⊢ c • extend m = extend fun s h ↦ c • m s h

Tactic:
by
  classical
  ext s; by_cases h : P s <;> simp [extend, ENNReal.smul_top, *]

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

Goal state before:
pp: case neg
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥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) ⋯
s : ℕ → Set α
h : ∃ i, ¬P (s i)
⊢ extend m (⋃ i, s i) ≤ ∑' (i : ℕ), extend m (s i)

Tactic:
obtain ⟨i, hi⟩ := h

Goal state after:
case neg
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥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) ⋯
s : ℕ → Set α
i : ℕ
hi : ¬P (s i)
⊢ extend m (⋃ i, s i) ≤ ∑' (i : ℕ), extend m (s i)
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case refine_2.inl
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ π i
⊢ s ∈ {s | ∃ t, ↑t ⊆ {i} ∧ ∃ f, (∀ x ∈ t, f x ∈ π x) ∧ s = ⋂ x ∈ t, f x}

Tactic:
refine ⟨{i}, ?_, fun _ => s, ⟨fun x hx => ?_, ?_⟩⟩

Goal state after:
case refine_2.inl.refine_1
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ π i
⊢ ↑{i} ⊆ {i}

case refine_2.inl.refine_2
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ π i
x : ι
hx : x ∈ {i}
⊢ (fun x ↦ s) x ∈ π x

case refine_2.inl.refine_3
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ π i
⊢ s = ⋂ x ∈ {i}, (fun x ↦ s) x
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

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

Tactic:
simpa only [← bliminf_true] using measurableSet_bliminf fun n _ => hs n

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

Goal state before:
pp: α : Type u_1
α₁ : Type u_6
α₂ : Type u_7
α₃ : Type u_8
mα : MeasurableSpace α
mα₁ : MeasurableSpace α₁
mα₂ : MeasurableSpace α₂
mα₃ : MeasurableSpace α₃
i₁ : α₁ → α
i₂ : α₂ → α
i₃ : α₃ → α
s : Set α
hi₁ : MeasurableEmbedding i₁
hi₂ : MeasurableEmbedding i₂
hi₃ : MeasurableEmbedding i₃
h : univ ⊆ range i₁ ∪ range i₂ ∪ range i₃
hs₁ : MeasurableSet (i₁ ⁻¹' s)
hs₂ : MeasurableSet (i₂ ⁻¹' s)
hs₃ : MeasurableSet (i₃ ⁻¹' s)
⊢ MeasurableSet s

Tactic:
convert!
    (hi₁.measurableSet_image' hs₁).union (hi₂.measurableSet_image' hs₂) |>.union
      (hi₃.measurableSet_image' hs₃)
  simp [image_preimage_eq_range_inter, ← union_inter_distrib_right, univ_subset_iff.1 h]

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

Goal state before:
pp: α : Type u_2
m : MeasurableSpace α
μ : Measure α
t : Set α
ι : Sort u_3
inst✝ : Countable ι
s : ι → Set α
⊢ AEDisjoint μ (⋃ i, s i) t ↔ ∀ (i : ι), AEDisjoint μ (s i) t

Tactic:
simp only [AEDisjoint, iUnion_inter, measure_iUnion_null_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α ≃ᵐ β
μ : Measure α
s : Set β
⊢ s ∈ Filter.map (⇑f) (ae μ) ↔ s ∈ ae (map (⇑f) μ)

Tactic:
mem_map,

Goal state after:
α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α ≃ᵐ β
μ : Measure α
s : Set β
⊢ ⇑f ⁻¹' s ∈ ae μ ↔ s ∈ ae (map (⇑f) μ)
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
hμst : μ (s ∆ t) ≠ ∞
u v : Set α
hμuv : μ (u ∆ v) ≠ ∞
hμu : μ u = ∞
hμv : μ v ≠ ∞
⊢ ∞ = μ u - μ v

Tactic:
by rw [ENNReal.sub_eq_top_iff.2 ⟨hμu, hμv⟩]

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

Goal state before:
pp: case inr
X : Type u_1
inst✝⁶ : LinearOrder X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : OrderTopology X
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : NoMaxOrder X
inst✝ : NoMinOrder X
f g : α → X
hl : Tendsto f atTop atTop
hu : Tendsto g atBot atBot
x : X
h✝ : Nonempty α
x_L : X
hx_L : x_L < x
x_R : X
hx_R : x < x_R
a_L : α
ha_L : ∀ a ≤ a_L, g a ≤ x_L
a_R : α
ha_R : ∀ a ≥ a_R, x_R ≤ f a
⊢ {i | ((fun n ↦ Icc (f n) (g n)) i ∩ Ioo x_L x_R).Nonempty} ⊆ Icc a_L a_R

Tactic:
rintro n ⟨y, ⟨hf, hg⟩, ⟨hxL, hxR⟩⟩

Goal state after:
case inr
X : Type u_1
inst✝⁶ : LinearOrder X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : OrderTopology X
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : NoMaxOrder X
inst✝ : NoMinOrder X
f g : α → X
hl : Tendsto f atTop atTop
hu : Tendsto g atBot atBot
x : X
h✝ : Nonempty α
x_L : X
hx_L : x_L < x
x_R : X
hx_R : x < x_R
a_L : α
ha_L : ∀ a ≤ a_L, g a ≤ x_L
a_R : α
ha_R : ∀ a ≥ a_R, x_R ≤ f a
n : α
y : X
hf : f n ≤ y
hg : y ≤ g n
hxL : x_L < y
hxR : y < x_R
⊢ n ∈ Icc a_L a_R
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
c : ℕ → ℝ≥0
hc₀ : ∀ (i : ℕ), 0 < c i
hc : ∑' (i : ℕ), (sfiniteSeq μ i) univ * ↑(c i) < ∞
s : Set α
⊢ (sum fun n ↦ c n • sfiniteSeq μ n) s = 0 ↔ μ s = 0

Tactic:
conv_rhs => rw [← sum_sfiniteSeq μ, sum_apply_of_countable]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
c : ℕ → ℝ≥0
hc₀ : ∀ (i : ℕ), 0 < c i
hc : ∑' (i : ℕ), (sfiniteSeq μ i) univ * ↑(c i) < ∞
s : Set α
⊢ (sum fun n ↦ c n • sfiniteSeq μ n) s = 0 ↔ ∑' (i : ℕ), (sfiniteSeq μ i) s = 0
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: R : Type u_1
α : Type u_2
β : Type u_3
δ : Type u_4
γ : Type u_5
ι : Type u_6
m0✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s'✝ t✝ : Set α
m0 : MeasurableSpace α
s : Set α
μ : Measure α
s' : Set α
hs' : MeasurableSet s'
t : Set α
⊢ μ (s ∩ t) = μ (s ∩ t ∩ s') + μ ((s ∩ t) \ s')

Tactic:
exact le_toOuterMeasure_caratheodory _ _ hs' _

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
m : ℝ≥0∞ := ⨆ D ∈ {D | D ⊆ C ∧ D.Countable}, μ (⋃₀ D)
⊢ ∃ D ∈ {D | D ⊆ C ∧ D.Countable}, μ (⋃₀ D) = m

Tactic:
rcases eq_bot_or_bot_lt m with hm | hm
    · exact ⟨∅, by simp, by simp [hm]⟩
    obtain ⟨u, -, u_mem, u_lim⟩ :
        ∃ u : ℕ → ℝ≥0∞, StrictMono u ∧ (∀ n, u n ∈ Ioo 0 m) ∧ Tendsto u atTop (𝓝 m) :=
      exists_seq_strictMono_tendsto' hm
    have A n : ∃ D ∈ {D : Set (Set α) | D ⊆ C ∧ D.Countable}, u n < μ (⋃₀ D) :=
      lt_biSup_iff.1 (u_mem n).2
    choose! D D_mem huD using A
    have hD : ⋃ n, D n ∈ {D | D ⊆ C ∧ D.Countable} := by simp; grind
    refine ⟨⋃ n, D n, hD, ?_⟩
    apply le_antisymm (le_biSup (f := fun D ↦ μ (⋃₀ D)) hD)
    apply le_of_tendsto' u_lim (fun n ↦ (huD n).le.trans ?_)
    exact measure_mono (fun x hx ↦ by simp at hx ⊢; grind)

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

Goal state before:
pp: case compl
α : Type u_5
m₀ : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hμν : ∀ s ∈ C, μ s = ν s
m : MeasurableSpace α
h : m ≤ m₀
hA : m = generateFrom C
hC : IsPiSystem C
h_univ : μ univ = ν univ
s : Set α
this : IsFiniteMeasure ν
t : Set α
htm : MeasurableSet t
iht : μ t = ν t
⊢ μ tᶜ = ν tᶜ

Tactic:
| compl t htm iht =>

Goal state after: