mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Unramified.LocalRing

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
p : Ideal R
inst✝⁶ : p.IsPrime
q : Ideal S
inst✝⁵ : q.IsPrime
hq : p.primesOver S = {q}
inst✝⁴ : Module.Finite R S
inst✝³ : q.LiesOver p
inst✝² : Algebra.IsUnramifiedAt R q
inst✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝ : AtPrime.IsLiesOverAlgebra p q
H : Function.Surjective ⇑(algebraMap p.ResidueField q.ResidueField)
this : Module.Finite (Localization.AtPrime p) (Localization.AtPrime q)
x : Localization.AtPrime q
a : Localization.AtPrime p
ha :
  (algebraMap p.ResidueField q.ResidueField)
      ((algebraMap (Localization.AtPrime p) (ResidueField (Localization.AtPrime p))) a) =
    (algebraMap (Localization.AtPrime q) q.ResidueField) x
⊢ x ∈
    (Algebra.linearMap (Localization.AtPrime p) (Localization.AtPrime q)).range ⊔
      Submodule.restrictScalars (Localization.AtPrime p) (maximalIdeal (Localization.AtPrime q))

Tactic:
← IsScalarTower.algebraMap_apply,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
p : Ideal R
inst✝⁶ : p.IsPrime
q : Ideal S
inst✝⁵ : q.IsPrime
hq : p.primesOver S = {q}
inst✝⁴ : Module.Finite R S
inst✝³ : q.LiesOver p
inst✝² : Algebra.IsUnramifiedAt R q
inst✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝ : AtPrime.IsLiesOverAlgebra p q
H : Function.Surjective ⇑(algebraMap p.ResidueField q.ResidueField)
this : Module.Finite (Localization.AtPrime p) (Localization.AtPrime q)
x : Localization.AtPrime q
a : Localization.AtPrime p
ha : (algebraMap (Localization.AtPrime p) q.ResidueField) a = (algebraMap (Localization.AtPrime q) q.ResidueField) x
⊢ x ∈
    (Algebra.linearMap (Localization.AtPrime p) (Localization.AtPrime q)).range ⊔
      Submodule.restrictScalars (Localization.AtPrime p) (maximalIdeal (Localization.AtPrime q))
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: case h
R : Type u₁
S : Type u₂
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
T : Type u₃
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
inst✝ : Flat S T
x : T ⊗[S] P.toExtension.H1Cotangent
x_in :
  (liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom)) ((lTensor T Extension.h1Cotangentι) x) ∈
    (Q.comp P).toExtension.cotangentComplex.ker
⊢ (liftBaseChange T (Extension.H1Cotangent.map (Q.toComp P).toExtensionHom)) x =
    ⟨(liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom)) ((lTensor T Extension.h1Cotangentι) x),
      x_in⟩

Tactic:
induction x with
  | zero => ext; simp
  | tmul x y => ext; simp
  | add x y hx hy => ext; simp [hx (auxMemKer Q P x), hy (auxMemKer Q P y)]

Goal state after:
Module: Mathlib.RingTheory.Unramified.LocalRing

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : Ideal R
inst✝² : p.IsPrime
q : Ideal S
inst✝¹ : q.IsPrime
inst✝ : q.LiesOver p
H✝ : Function.Injective ⇑(localRingHom p q (algebraMap R S) ⋯)
s✝ : Finset R
hs : Ideal.span ↑s✝ = RingHom.ker (algebraMap R S)
this : ∀ (x : ↥s✝), (algebraMap R (Localization.AtPrime p)) ↑x = 0
m : ↥s✝ → ↥p.primeCompl
hm : ∀ (x : ↥s✝), ↑(m x) * ↑x = 0
H : RingHom.ker (algebraMap R S) ≤ RingHom.ker (algebraMap R (Away ↑(∏ i, m i)))
r' s : R
e : r' = ↑(∏ i, m i) * s
x : R
w✝ : ↥(Submonoid.powers r')
n : ℕ
hn : (algebraMap R S) (r' ^ n * x) = 0
k : ℕ
hk : ↑(∏ i, m i) ^ k * (r' ^ n * x) = 0
⊢ ↑(∏ i, m i) ^ k * s ^ k * ((↑(∏ i, m i) * s) ^ n * x) = 0

Tactic:
← e,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : Ideal R
inst✝² : p.IsPrime
q : Ideal S
inst✝¹ : q.IsPrime
inst✝ : q.LiesOver p
H✝ : Function.Injective ⇑(localRingHom p q (algebraMap R S) ⋯)
s✝ : Finset R
hs : Ideal.span ↑s✝ = RingHom.ker (algebraMap R S)
this : ∀ (x : ↥s✝), (algebraMap R (Localization.AtPrime p)) ↑x = 0
m : ↥s✝ → ↥p.primeCompl
hm : ∀ (x : ↥s✝), ↑(m x) * ↑x = 0
H : RingHom.ker (algebraMap R S) ≤ RingHom.ker (algebraMap R (Away ↑(∏ i, m i)))
r' s : R
e : r' = ↑(∏ i, m i) * s
x : R
w✝ : ↥(Submonoid.powers r')
n : ℕ
hn : (algebraMap R S) (r' ^ n * x) = 0
k : ℕ
hk : ↑(∏ i, m i) ^ k * (r' ^ n * x) = 0
⊢ ↑(∏ i, m i) ^ k * s ^ k * (r' ^ n * x) = 0
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: ι : Type u_1
α : Type u_2
G : Type u_3
inst✝¹ : AddCommGroup G
inst✝ : DecidableEq α
s : Finset ι
S : ι → Finset α
f : α → G
⊢ ∑ a ∈ s.biUnion S, f a - ∑ t, (-1) ^ (#↑t + 1) • ∑ a ∈ (↑t).inf' ⋯ S, f a =
    ∑ t, (-1) ^ #↑t • ∑ a ∈ (↑t).inf' ⋯ S, f a + ∑ t ∈ s.powerset with ¬t.Nonempty, (-1) ^ #t • ∑ a ∈ s.biUnion S, f a

Tactic:
simp [sub_eq_neg_add, ← sum_neg_distrib, filter_eq', pow_succ]

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this : ∀ (d : ℕ), BddAbove {m | ∃ y ∈ s, ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d} ∧ ∀ z ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d}, z ≤ f d
hf₁ : ∀ n > 0, ∃ y ∈ s, ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ n > 0, ∀ y ∈ s, y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
ε : ℚ
ε0 : ε > 0
j : ℕ
ij : j ≥ ⌈ε⁻¹⌉₊
k : ℕ
⊢ k ≥ ⌈ε⁻¹⌉₊ → ↑(f j) / ↑j - ↑(f k) / ↑k < ε

Tactic:
ik

Goal state after:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this : ∀ (d : ℕ), BddAbove {m | ∃ y ∈ s, ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d} ∧ ∀ z ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d}, z ≤ f d
hf₁ : ∀ n > 0, ∃ y ∈ s, ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ n > 0, ∀ y ∈ s, y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
ε : ℚ
ε0 : ε > 0
j : ℕ
ij : j ≥ ⌈ε⁻¹⌉₊
k : ℕ
ik : k ≥ ⌈ε⁻¹⌉₊
⊢ ↑(f j) / ↑j - ↑(f k) / ↑k < ε
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: case neg
s : Set ℝ≥0
hs : s.Nonempty
H : ¬BddAbove s
⊢ ↑(sSup s) = sSup (toReal '' s)

Tactic:
simp only [csSup_of_not_bddAbove H, csSup_empty, bot_eq_zero', NNReal.coe_zero]

Goal state after:
case neg
s : Set ℝ≥0
hs : s.Nonempty
H : ¬BddAbove s
⊢ 0 = sSup (toReal '' s)
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case refine_1
f : CauSeq ℝ abs
s : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ s
ub' : ∀ (x : ℝ), f < const abs x → ∀ y ∈ s, y ≤ x
ub : ∃ x, ∀ y ∈ s, y ≤ x
ε : ℝ
ε0 : ε > 0
i : ℕ
ih : ∀ j ≥ i, ε ≤ ↑(const abs (sSup s) - f) j
j : ℕ
ij : j ≥ i
⊢ ε / 2 ≤ ↑(const abs (sSup s - ε / 2) - f) j

Tactic:
sub_apply,

Goal state after:
case refine_1
f : CauSeq ℝ abs
s : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ s
ub' : ∀ (x : ℝ), f < const abs x → ∀ y ∈ s, y ≤ x
ub : ∃ x, ∀ y ∈ s, y ≤ x
ε : ℝ
ε0 : ε > 0
i : ℕ
ih : ∀ j ≥ i, ε ≤ ↑(const abs (sSup s) - f) j
j : ℕ
ij : j ≥ i
⊢ ε / 2 ≤ ↑(const abs (sSup s - ε / 2)) j - ↑f j
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r : ℝ≥0
p : ℝ
hp : 0 ≤ p
⊢ ↑r ≤ ↑p.toNNReal ↔ ↑r ≤ p

Tactic:
Real.coe_toNNReal p hp

Goal state after:
r : ℝ≥0
p : ℝ
hp : 0 ≤ p
⊢ ↑r ≤ p ↔ ↑r ≤ p
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case refine_2
f : CauSeq ℝ abs
s : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ s
ub' : ∀ (x : ℝ), f < const abs x → ∀ y ∈ s, y ≤ x
ub : ∃ x, ∀ y ∈ s, y ≤ x
ε : ℝ
ε0 : ε > 0
i : ℕ
ih : ∀ j ≥ i, ε ≤ ↑(f - const abs (sSup s)) j
j : ℕ
ij : j ≥ i
⊢ ε / 2 ≤ ↑(f - const abs (ε / 2 + sSup s)) j

Tactic:
sub_apply,

Goal state after:
case refine_2
f : CauSeq ℝ abs
s : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ s
ub' : ∀ (x : ℝ), f < const abs x → ∀ y ∈ s, y ≤ x
ub : ∃ x, ∀ y ∈ s, y ≤ x
ε : ℝ
ε0 : ε > 0
i : ℕ
ih : ∀ j ≥ i, ε ≤ ↑(f - const abs (sSup s)) j
j : ℕ
ij : j ≥ i
⊢ ε / 2 ≤ ↑f j - ↑(const abs (ε / 2 + sSup s)) j
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: E : Type u_3
inst✝ : Group E
s : Set (GroupSeminorm E)
hs : BddAbove s
x : E
⊢ (sSup s) x = sSup ((fun x_1 ↦ x_1 x) '' s)

Tactic:
by
  rw [coe_sSup_apply hs, ← sSup_range]
  congr
  ext
  simp

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
k : K
hk : I = spanSingleton R⁰ k
n : R := choose ⋯
d : ↥R⁰ := choose ⋯
hnd : mk' K n d = k
h : n = 0
⊢ False

Tactic:
← hnd,

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
k : K
n : R := choose ⋯
d : ↥R⁰ := choose ⋯
hk : I = spanSingleton R⁰ (mk' K n d)
hnd : mk' K n d = k
h : n = 0
⊢ False
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: E : Type u_3
inst✝ : AddGroup E
s : Set (NonarchAddGroupSeminorm E)
hs : BddAbove s
x : E
⊢ (sSup s) x = sSup ((fun x_1 ↦ x_1 x) '' s)

Tactic:
by
  rw [coe_sSup_apply hs, ← sSup_range]
  congr
  ext
  simp

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

Goal state before:
pp: X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
s t : Set X
hd✝ : Disjoint s (closure[inst✝¹] t)
ha : a ∈ s
hmem : tᶜ ∈ 𝓝[≥] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[≥] a
hsub : Icc a b ⊆ tᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hcb : c ≤ b
hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
hd : Disjoint s (s.ordSeparatingSet t).ordConnectedSection
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ (s.ordSeparatingSet t).ordConnectedSection
⊢ False

Tactic:
refine hx.2.ne (eq_of_mem_ordConnectedSection_of_uIcc_subset hx' hc ?_)

Goal state after:
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
s t : Set X
hd✝ : Disjoint s (closure[inst✝¹] t)
ha : a ∈ s
hmem : tᶜ ∈ 𝓝[≥] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[≥] a
hsub : Icc a b ⊆ tᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hcb : c ≤ b
hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
hd : Disjoint s (s.ordSeparatingSet t).ordConnectedSection
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ (s.ordSeparatingSet t).ordConnectedSection
⊢ [[x, c]] ⊆ s.ordSeparatingSet t
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: a b c : ℝ≥0∞
h : a ≠ ∞ ∨ b ≠ ∞
⊢ a - b < c → a < b + c

Tactic:
obtain rfl | hb := eq_or_ne b ∞
  · rw [top_add, lt_top_iff_ne_top]
    exact fun _ => h.resolve_right (Classical.not_not.2 rfl)
  · exact (cancel_of_ne hb).lt_add_of_tsub_lt_left

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

Goal state before:
pp: X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
s t : Set X
hd : Disjoint s (closure[inst✝¹] t)
ha : a ∈ s
⊢ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≥] a

Tactic:
by
  have hmem : tᶜ ∈ 𝓝[≥] a := by
    refine mem_nhdsWithin_of_mem_nhds ?_
    rw [← mem_interior_iff_mem_nhds, interior_compl]
    exact disjoint_left.1 hd ha
  rcases exists_Icc_mem_subset_of_mem_nhdsGE hmem with ⟨b, hab, hmem', hsub⟩
  by_cases H : Disjoint (Icc a b) (ordConnectedSection <| ordSeparatingSet s t)
  · exact mem_of_superset hmem' (disjoint_left.1 H)
  · simp only [Set.disjoint_left, not_forall, Classical.not_not] at H
    rcases H with ⟨c, ⟨hac, hcb⟩, hc⟩
    have hsub' : Icc a b ⊆ ordConnectedComponent tᶜ a :=
      subset_ordConnectedComponent (left_mem_Icc.2 hab) hsub
    have hd : Disjoint s (ordConnectedSection (ordSeparatingSet s t)) :=
      disjoint_left_ordSeparatingSet.mono_right ordConnectedSection_subset
    replace hac : a < c := hac.lt_of_ne <| Ne.symm <| ne_of_mem_of_not_mem hc <|
      disjoint_left.1 hd ha
    filter_upwards [Ico_mem_nhdsGE hac] with x hx hx'
    refine hx.2.ne (eq_of_mem_ordConnectedSection_of_uIcc_subset hx' hc ?_)
    refine subset_inter (subset_iUnion₂_of_subset a ha ?_) ?_
    · exact OrdConnected.uIcc_subset inferInstance (hsub' ⟨hx.1, hx.2.le.trans hcb⟩)
        (hsub' ⟨hac.le, hcb⟩)
    · rcases mem_iUnion₂.1 (ordConnectedSection_subset hx').2 with ⟨y, hyt, hxy⟩
      refine subset_iUnion₂_of_subset y hyt (OrdConnected.uIcc_subset inferInstance hxy ?_)
      refine subset_ordConnectedComponent left_mem_uIcc hxy ?_
      suffices c < y by
        rw [uIcc_of_ge (hx.2.trans this).le]
        exact ⟨hx.2.le, this.le⟩
      refine lt_of_not_ge fun hyc => ?_
      have hya : y < a := not_le.1 fun hay => hsub ⟨hay, hyc.trans hcb⟩ hyt
      exact hxy (Icc_subset_uIcc ⟨hya.le, hx.1⟩) ha

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

Goal state before:
pp: x y : EReal
⊢ x * y = y * x

Tactic:
induction x

Goal state after:
case bot
y : EReal
⊢ ⊥ * y = y * ⊥

case coe
y : EReal
a✝ : ℝ
⊢ ↑a✝ * y = y * ↑a✝

case top
y : EReal
⊢ ⊤ * y = y * ⊤
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : EReal
hx : x ≠ ⊤ ∧ x ≠ ⊥
⊢ ∃ y, ↑y = x

Tactic:
induction x

Goal state after:
case bot
hx : ⊥ ≠ ⊤ ∧ ⊥ ≠ ⊥
⊢ ∃ y, ↑y = ⊥

case coe
a✝ : ℝ
hx : ↑a✝ ≠ ⊤ ∧ ↑a✝ ≠ ⊥
⊢ ∃ y, ↑y = ↑a✝

case top
hx : ⊤ ≠ ⊤ ∧ ⊤ ≠ ⊥
⊢ ∃ y, ↑y = ⊤
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : EReal
⊢ x ∈ range Real.toEReal ↔ x ∈ {⊥, ⊤}ᶜ

Tactic:
induction x

Goal state after:
case bot
⊢ ⊥ ∈ range Real.toEReal ↔ ⊥ ∈ {⊥, ⊤}ᶜ

case coe
a✝ : ℝ
⊢ ↑a✝ ∈ range Real.toEReal ↔ ↑a✝ ∈ {⊥, ⊤}ᶜ

case top
⊢ ⊤ ∈ range Real.toEReal ↔ ⊤ ∈ {⊥, ⊤}ᶜ
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : EReal
⊢ x ∈ range Real.toEReal ↔ x ∈ Ioo ⊥ ⊤

Tactic:
induction x

Goal state after:
case bot
⊢ ⊥ ∈ range Real.toEReal ↔ ⊥ ∈ Ioo ⊥ ⊤

case coe
a✝ : ℝ
⊢ ↑a✝ ∈ range Real.toEReal ↔ ↑a✝ ∈ Ioo ⊥ ⊤

case top
⊢ ⊤ ∈ range Real.toEReal ↔ ⊤ ∈ Ioo ⊥ ⊤
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: y : ℝ
⊢ WithTop.some ⁻¹' WithBot.some ⁻¹' Iio ↑↑y = Iio y

Tactic:
simp only [WithBot.preimage_coe_Iio, WithTop.preimage_coe_Iio]

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

Goal state before:
pp: y : ℝ
⊢ Real.toEReal ⁻¹' Iio ↑y = Iio y

Tactic:
by
  change (WithBot.some ∘ WithTop.some) ⁻¹' (Iio (WithBot.some (WithTop.some y))) = _
  refine preimage_comp.trans ?_
  simp only [WithBot.preimage_coe_Iio, WithTop.preimage_coe_Iio]

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

Goal state before:
pp: x : EReal
⊢ x.toENNReal = 0 ↔ x ≤ 0

Tactic:
induction x

Goal state after:
case bot
⊢ ⊥.toENNReal = 0 ↔ ⊥ ≤ 0

case coe
a✝ : ℝ
⊢ (↑a✝).toENNReal = 0 ↔ ↑a✝ ≤ 0

case top
⊢ ⊤.toENNReal = 0 ↔ ⊤ ≤ 0
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case inr
a b : ℝ≥0∞
ha₀✝ : a = 0 → b = 0
ha : a = ∞ → b = 0
ha₀ : a ≠ 0
⊢ a⁻¹ * (a * b) = b

Tactic:
obtain rfl | ha := eq_or_ne a ⊤

Goal state after:
case inr.inl
b : ℝ≥0∞
ha₀✝ : ∞ = 0 → b = 0
ha : ∞ = ∞ → b = 0
ha₀ : ∞ ≠ 0
⊢ ∞⁻¹ * (∞ * b) = b

case inr.inr
a b : ℝ≥0∞
ha₀✝ : a = 0 → b = 0
ha✝ : a = ∞ → b = 0
ha₀ : a ≠ 0
ha : a ≠ ∞
⊢ a⁻¹ * (a * b) = b
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case inr
a b : ℝ≥0∞
ha₀✝ : a = 0 → b = 0
ha : a = ∞ → b = 0
ha₀ : a ≠ 0
⊢ a * (a⁻¹ * b) = b

Tactic:
obtain rfl | ha := eq_or_ne a ⊤

Goal state after:
case inr.inl
b : ℝ≥0∞
ha₀✝ : ∞ = 0 → b = 0
ha : ∞ = ∞ → b = 0
ha₀ : ∞ ≠ 0
⊢ ∞ * (∞⁻¹ * b) = b

case inr.inr
a b : ℝ≥0∞
ha₀✝ : a = 0 → b = 0
ha✝ : a = ∞ → b = 0
ha₀ : a ≠ 0
ha : a ≠ ∞
⊢ a * (a⁻¹ * b) = b
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x y : EReal
hx : 0 ≤ x
hy : 0 ≤ y
⊢ x.toENNReal = y.toENNReal ↔ x = y

Tactic:
induction x

Goal state after:
case bot
y : EReal
hy : 0 ≤ y
hx : 0 ≤ ⊥
⊢ ⊥.toENNReal = y.toENNReal ↔ ⊥ = y

case coe
y : EReal
hy : 0 ≤ y
a✝ : ℝ
hx : 0 ≤ ↑a✝
⊢ (↑a✝).toENNReal = y.toENNReal ↔ ↑a✝ = y

case top
y : EReal
hy : 0 ≤ y
hx : 0 ≤ ⊤
⊢ ⊤.toENNReal = y.toENNReal ↔ ⊤ = y
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x y : EReal
h : x ≤ y
⊢ x.toENNReal ≤ y.toENNReal

Tactic:
induction x

Goal state after:
case bot
y : EReal
h : ⊥ ≤ y
⊢ ⊥.toENNReal ≤ y.toENNReal

case coe
y : EReal
a✝ : ℝ
h : ↑a✝ ≤ y
⊢ (↑a✝).toENNReal ≤ y.toENNReal

case top
y : EReal
h : ⊤ ≤ y
⊢ ⊤.toENNReal ≤ y.toENNReal
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b : ℝ≥0∞
⊢ a⁻¹ < b ↔ b⁻¹ < a

Tactic:
by
  simpa only [inv_inv] using @ENNReal.inv_lt_inv a b⁻¹

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
J : Ideal R
hJ : J ≠ 0
⊢ count K v ↑J = ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors)

Tactic:
rw [count_well_defined K (J := J) (a := 1), Ideal.span_singleton_one, sub_eq_self,
    Nat.cast_eq_zero, ← Ideal.one_eq_top, Associates.mk_one, Associates.factors_one,
    Associates.count_zero v.associates_irreducible]
  · simpa only [ne_eq, coeIdeal_eq_zero]
  · simp only [map_one, inv_one, spanSingleton_one, one_mul]

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

Goal state before:
pp: α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
x✝² x✝¹ x✝ : Empty
⊢ 0 ≤ 0 + 0

Tactic:
rw [add_zero]

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

Goal state before:
pp: α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
x✝² x✝¹ x✝ : PUnit.{u + 1}
⊢ 0 ≤ 0 + 0

Tactic:
rw [add_zero]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
y : α
⊢ dist y x ≤ ε ↔ y ∈ ⋂ δ, ⋂ (_ : δ > ε), ball x δ

Tactic:
← forall_gt_iff_le,

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
y : α
⊢ (∀ ⦃c : ℝ⦄, ε < c → dist y x < c) ↔ y ∈ ⋂ δ, ⋂ (_ : δ > ε), ball x δ
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
⊢ (𝓤 α).HasBasis (fun ε ↦ 0 < ε) fun ε ↦ {p | dist p.1 p.2 < ε}

Tactic:
rw [toUniformSpace_eq]
  exact UniformSpace.hasBasis_ofFun (exists_gt _) _ _ _ _ _

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
a : R
K : Ideal R
e : J * K = Ideal.span {a}
e' : I + K = ⊤
⊢ J * I ⊔ Ideal.span {a} = J

Tactic:
← e,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
a : R
K : Ideal R
e : J * K = Ideal.span {a}
e' : I + K = ⊤
⊢ J * I ⊔ J * K = J
Module: Mathlib.Data.Real.Pointwise

Goal state before:
pp: α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : IsOrderedModule α ℝ
a : α
ha : 0 ≤ a
s : Set ℝ
⊢ sSup (a • s) = a • sSup s

Tactic:
by
  obtain rfl | hs := s.eq_empty_or_nonempty
  · rw [smul_set_empty, Real.sSup_empty, smul_zero]
  obtain rfl | ha' := ha.eq_or_lt
  · rw [zero_smul_set hs, zero_smul]
    exact csSup_singleton 0
  by_cases h : BddAbove s
  · exact ((OrderIso.smulRight ha').map_csSup' hs h).symm
  · rw [Real.sSup_of_not_bddAbove (mt (bddAbove_smul_iff_of_pos ha').1 h),
        Real.sSup_of_not_bddAbove h, smul_zero]

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

Goal state before:
pp: X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : PseudoMetrizableSpace X
s : Set X
hs✝ : IsSeparable s
u : Set X
hu : u.Countable
hs : s ⊆ closure[inst✝¹] u
this : Countable ↑u
⊢ closure[inst✝¹] u ⊆ closure[inst✝¹] (range Subtype.val)

Tactic:
Subtype.range_coe

Goal state after:
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : PseudoMetrizableSpace X
s : Set X
hs✝ : IsSeparable s
u : Set X
hu : u.Countable
hs : s ⊆ closure[inst✝¹] u
this : Countable ↑u
⊢ closure[inst✝¹] u ⊆ closure[inst✝¹] u
Module: Mathlib.Topology.EMetricSpace.Basic

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
hs : ∀ ε > 0, ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, closedEBall x ε
U : Set (α × α)
hU : U ∈ 𝓤 α
ε : ℝ≥0∞
hε : 0 < ε
hεU : {p | edist p.1 p.2 ≤ ε} ⊆ U
t : Set α
tC : t.Countable
ht : s ⊆ ⋃ x ∈ t, closedEBall x ε
x : α
hx : x ∈ t
y : α
hy : y ∈ closedEBall x ε
⊢ y ∈ UniformSpace.ball x {p | edist p.1 p.2 ≤ ε}

Tactic:
rwa [mem_closedEBall, edist_comm] at hy

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : DiscreteTopology α
⊢ Subsingleton α

Tactic:
suffices ∀ a b : α, b ≤ a from ⟨fun a b ↦ le_antisymm (this b a) (this a b)⟩
  intro a b
  by_contra! contra
  have : Ioo a b = Icc a b := by rw [← closure_discrete (Ioo a b), closure_Ioo contra.ne]
  grind => have : b ∈ Ioo a b; finish

Goal state after:
Module: Mathlib.Topology.MetricSpace.Pseudo.Pi

Goal state before:
pp: case inr.inl
β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
x : (b : β) → X b
h : 0 < 0 ∨ Nonempty β
⊢ sphere x 0 = (⋃ i, Function.eval i ⁻¹' sphere (x i) 0) ∩ closedBall x 0

Tactic:
closedBall_eq_sphere_of_nonpos le_rfl,

Goal state after:
case inr.inl
β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
x : (b : β) → X b
h : 0 < 0 ∨ Nonempty β
⊢ sphere x 0 = (⋃ i, Function.eval i ⁻¹' sphere (x i) 0) ∩ sphere x 0
Module: Mathlib.Topology.MetricSpace.Basic

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
X : Type u_2
m : PseudoEMetricSpace X
d : X → X → ℝ≥0∞
hd : d = edist
⊢ 𝓤 X = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | d p.1 p.2 < ε}

Tactic:
simp [hd, uniformity_edist]

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

Goal state before:
pp: E : Type u_5
F : Type u_6
inst✝¹ : SeminormedGroup E
inst✝ : SeminormedGroup F
x : E
y : F
h : ENNReal.ofReal ‖x‖ ≤ ENNReal.ofReal ‖y‖
⊢ ‖x‖ ≤ ‖y‖

Tactic:
ENNReal.ofReal_le_ofReal_iff (norm_nonneg' _)

Goal state after:
E : Type u_5
F : Type u_6
inst✝¹ : SeminormedGroup E
inst✝ : SeminormedGroup F
x : E
y : F
h : ‖x‖ ≤ ‖y‖
⊢ ‖x‖ ≤ ‖y‖
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: case inr
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
s : Set α
hs : IsClosed[inst✝³] (s ∩ Icc a b)
ha : a ∈ s
h✝ : ∀ t ∈ Ico a b, Icc a t ⊆ s → s ∈ 𝓝[>] t
hab : a ≤ b
A : Set α := {t | t ∈ Icc a b ∧ Icc a t ⊆ s}
a_mem : a ∈ A
bdd_A : BddAbove A
t₁ : α := sSup A
t₁_mem : t₁ ∈ Icc a b
t : α
ht : t ∈ Icc a t₁
h : t < t₁
⊢ t ∈ s

Tactic:
obtain ⟨c, cA, tc⟩ : ∃ c ∈ A, t < c := (lt_csSup_iff bdd_A ⟨a, a_mem⟩).1 h
      apply cA.2
      exact ⟨ht.1, tc.le⟩

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

Goal state before:
pp: α : Type u
inst✝² : PseudoMetricSpace α
inst✝¹ : Preorder α
inst✝ : CompactIccSpace α
x : α
bddBelow_ball : ∀ (r : ℝ), BddBelow (closedBall x r)
bddAbove_ball : ∀ (r : ℝ), BddAbove (closedBall x r)
s : Set α
⊢ Bornology.IsBounded s ↔ BddBelow s ∧ BddAbove s

Tactic:
refine ⟨?_, fun hs ↦ Metric.isBounded_of_bddAbove_of_bddBelow hs.2 hs.1⟩
    rw [Metric.isBounded_iff_subset_closedBall x]
    rintro ⟨r, hr⟩
    exact ⟨(bddBelow_ball _).mono hr, (bddAbove_ball _).mono hr⟩

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

Goal state before:
pp: ⊢ (range ofNNReal).OrdConnected

Tactic:
rw [range_coe']; exact ordConnected_Iio

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

Goal state before:
pp: r₁ r₂ : ℚ
⊢ dist r₁ r₂ = ‖↑(-r₁ + r₂)‖

Tactic:
by
    simp only [dist_eq, norm, cast_add, cast_neg]
    rw [← abs_neg, neg_sub]
    abel_nf

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

Goal state before:
pp: x : EReal
h : x ≠ ⊥
⊢ ⊤ + x = ⊤

Tactic:
induction x

Goal state after:
case bot
h : ⊥ ≠ ⊥
⊢ ⊤ + ⊥ = ⊤

case coe
a✝ : ℝ
h : ↑a✝ ≠ ⊥
⊢ ⊤ + ↑a✝ = ⊤

case top
h : ⊤ ≠ ⊥
⊢ ⊤ + ⊤ = ⊤
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: x y : EReal
hx : 0 ≤ x
hy : 0 ≤ y
⊢ (x + y).toENNReal = x.toENNReal + y.toENNReal

Tactic:
induction x

Goal state after:
case bot
y : EReal
hy : 0 ≤ y
hx : 0 ≤ ⊥
⊢ (⊥ + y).toENNReal = ⊥.toENNReal + y.toENNReal

case coe
y : EReal
hy : 0 ≤ y
a✝ : ℝ
hx : 0 ≤ ↑a✝
⊢ (↑a✝ + y).toENNReal = (↑a✝).toENNReal + y.toENNReal

case top
y : EReal
hy : 0 ≤ y
hx : 0 ≤ ⊤
⊢ (⊤ + y).toENNReal = ⊤.toENNReal + y.toENNReal