mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Smooth.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type u_1
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FormallySmooth R A
I : Ideal B
hI : I ^ 2 = ⊥
f : A →ₐ[R] B ⧸ I
P : Generators R A A := Generators.self R A
hP : Function.Injective ⇑P.toExtension.cotangentComplex
l : P.toExtension.CotangentSpace →ₗ[A] P.toExtension.Cotangent
hl : l ∘ₗ P.toExtension.cotangentComplex = LinearMap.id
g : A →ₐ[R] P.Ring ⧸ RingHom.ker (IsScalarTower.toAlgHom R P.Ring A).toRingHom ^ 2
hg : (IsScalarTower.toAlgHom R P.Ring A).kerSquareLift.comp g = AlgHom.id R A
σ : B ⧸ I → B := Function.surjInv ⋯
x : P.Ring
⊢ (aeval (⇑(algebraMap B (B ⧸ I)) ∘ σ ∘ ⇑f)) x = f (↑(aeval P.val) x)

Tactic:
AlgHom.coe_toRingHom,

Goal state after:
R : Type u
A : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type u_1
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FormallySmooth R A
I : Ideal B
hI : I ^ 2 = ⊥
f : A →ₐ[R] B ⧸ I
P : Generators R A A := Generators.self R A
hP : Function.Injective ⇑P.toExtension.cotangentComplex
l : P.toExtension.CotangentSpace →ₗ[A] P.toExtension.Cotangent
hl : l ∘ₗ P.toExtension.cotangentComplex = LinearMap.id
g : A →ₐ[R] P.Ring ⧸ RingHom.ker (IsScalarTower.toAlgHom R P.Ring A).toRingHom ^ 2
hg : (IsScalarTower.toAlgHom R P.Ring A).kerSquareLift.comp g = AlgHom.id R A
σ : B ⧸ I → B := Function.surjInv ⋯
x : P.Ring
⊢ (aeval (⇑(algebraMap B (B ⧸ I)) ∘ σ ∘ ⇑f)) x = f ((aeval P.val) x)
Module: Mathlib.RingTheory.Smooth.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type u_1
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FormallySmooth R A
I : Ideal B
hI : I ^ 2 = ⊥
f : A →ₐ[R] B ⧸ I
P : Generators R A A := Generators.self R A
hP : Function.Injective ⇑P.toExtension.cotangentComplex
l✝ : P.toExtension.CotangentSpace →ₗ[A] P.toExtension.Cotangent
hl : l✝ ∘ₗ P.toExtension.cotangentComplex = LinearMap.id
g : A →ₐ[R] P.Ring ⧸ RingHom.ker (IsScalarTower.toAlgHom R P.Ring A).toRingHom ^ 2
hg : (IsScalarTower.toAlgHom R P.Ring A).kerSquareLift.comp g = AlgHom.id R A
σ : B ⧸ I → B := Function.surjInv ⋯
H : ∀ (x : P.Ring), (Ideal.Quotient.mk I) ((aeval (σ ∘ ⇑f)) x) = f ((algebraMap P.Ring A) x)
l : P.Ring ⧸ RingHom.ker (algebraMap P.Ring A) ^ 2 →ₐ[R] B :=
  Ideal.Quotient.liftₐ (RingHom.ker (algebraMap P.Ring A) ^ 2) (aeval (σ ∘ ⇑f)) ⋯
this : f.comp (IsScalarTower.toAlgHom R P.Ring A).kerSquareLift = (Ideal.Quotient.mkₐ R I).comp l
⊢ f.comp ((IsScalarTower.toAlgHom R P.Ring A).kerSquareLift.comp g) = f

Tactic:
hg,

Goal state after:
R : Type u
A : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type u_1
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FormallySmooth R A
I : Ideal B
hI : I ^ 2 = ⊥
f : A →ₐ[R] B ⧸ I
P : Generators R A A := Generators.self R A
hP : Function.Injective ⇑P.toExtension.cotangentComplex
l✝ : P.toExtension.CotangentSpace →ₗ[A] P.toExtension.Cotangent
hl : l✝ ∘ₗ P.toExtension.cotangentComplex = LinearMap.id
g : A →ₐ[R] P.Ring ⧸ RingHom.ker (IsScalarTower.toAlgHom R P.Ring A).toRingHom ^ 2
hg : (IsScalarTower.toAlgHom R P.Ring A).kerSquareLift.comp g = AlgHom.id R A
σ : B ⧸ I → B := Function.surjInv ⋯
H : ∀ (x : P.Ring), (Ideal.Quotient.mk I) ((aeval (σ ∘ ⇑f)) x) = f ((algebraMap P.Ring A) x)
l : P.Ring ⧸ RingHom.ker (algebraMap P.Ring A) ^ 2 →ₐ[R] B :=
  Ideal.Quotient.liftₐ (RingHom.ker (algebraMap P.Ring A) ^ 2) (aeval (σ ∘ ⇑f)) ⋯
this : f.comp (IsScalarTower.toAlgHom R P.Ring A).kerSquareLift = (Ideal.Quotient.mkₐ R I).comp l
⊢ f.comp (AlgHom.id R A) = f
Module: Mathlib.RingTheory.Etale.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
T : Type u_3
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hf : f.FormallyEtale
hg : g.FormallyEtale
algInst✝² : Algebra R S := f.toAlgebra
algInst✝¹ : Algebra S T := g.toAlgebra
algInst✝ : Algebra R T := (g.comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower R S T := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R T))
algebraizeInst✝¹ : Algebra.FormallyEtale R S
algebraizeInst✝ : Algebra.FormallyEtale S T
⊢ (g.comp f).FormallyEtale

Tactic:
exact Algebra.FormallyEtale.comp R S T

Goal state after:
Module: Mathlib.RingTheory.Smooth.Kaehler

Goal state before:
pp: R : Type u_1
P : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
g✝ : S →ₐ[R] P
f : P →ₐ[R] S
hf' : RingHom.ker f ^ 2 = ⊥
g : S →ₐ[R] P
hg : f.comp g = AlgHom.id R S
x y : P
⊢ ⟨x + y - g (f (x + y)), ⋯⟩ = ⟨x - g (f x), ⋯⟩ + ⟨y - g (f y), ⋯⟩

Tactic:
simp only [map_add, AddMemClass.mk_add_mk, Subtype.mk.injEq]; ring

Goal state after:
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: case hF
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 σ
i : σ
⊢ (D R T) ((algebraMap S T) (P.val i)) =
    (Q.comp P).toExtension.toKaehler
      ((Extension.CotangentSpace.map (Q.toComp P).toExtensionHom) (P.cotangentSpaceBasis i))

Tactic:
rw [cotangentSpaceBasis_apply]

Goal state after:
case hF
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 σ
i : σ
⊢ (D R T) ((algebraMap S T) (P.val i)) =
    (Q.comp P).toExtension.toKaehler
      ((Extension.CotangentSpace.map (Q.toComp P).toExtensionHom) (1 ⊗ₜ[P.Ring] (D R P.Ring) (X i)))
Module: Mathlib.RingTheory.Unramified.Field

Goal state before:
pp: K : Type u_1
L : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FormallyUnramified K L
inst✝¹ : EssFiniteType K L
inst✝ : IsPurelyInseparable K L
this✝¹ : Nontrivial (L ⊗[K] L)
x : L
a✝ : x ∈ ⊤
n : ℕ
hn : x ^ ringExpChar K ^ n ∈ (algebraMap K L).range
this✝ : ExpChar (L ⊗[K] L) (ringExpChar K)
this : (1 ⊗ₜ[K] x - x ⊗ₜ[K] 1) ^ ringExpChar K ^ n = 0
H : 1 ⊗ₜ[K] x = x ⊗ₜ[K] 1
a : K
e : a • 1 + 0 • x = 0
hab : a = 0 → ¬0 = 0
⊢ False

Tactic:
rw [zero_smul, ← algebraMap_eq_smul_one, add_zero,
        (injective_iff_map_eq_zero' _).mp (algebraMap K L).injective] at e

Goal state after:
K : Type u_1
L : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FormallyUnramified K L
inst✝¹ : EssFiniteType K L
inst✝ : IsPurelyInseparable K L
this✝¹ : Nontrivial (L ⊗[K] L)
x : L
a✝ : x ∈ ⊤
n : ℕ
hn : x ^ ringExpChar K ^ n ∈ (algebraMap K L).range
this✝ : ExpChar (L ⊗[K] L) (ringExpChar K)
this : (1 ⊗ₜ[K] x - x ⊗ₜ[K] 1) ^ ringExpChar K ^ n = 0
H : 1 ⊗ₜ[K] x = x ⊗ₜ[K] 1
a : K
e : a = 0
hab : a = 0 → ¬0 = 0
⊢ False
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
⊢ ↑s ⊆ ↑(RingHom.ker (algebraMap R (Away ↑(∏ i, m i))))

Tactic:
intro x hxs

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
x : R
hxs : x ∈ ↑s
⊢ x ∈ ↑(RingHom.ker (algebraMap R (Away ↑(∏ i, m i))))
Module: Mathlib.RingTheory.RamificationInertia.Ramification

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
q : Ideal S
r : Ideal T
inst✝¹ : r.LiesOver q
inst✝ : Module.Flat S T
⊢ r.ramificationIdx R = q.ramificationIdx R * r.ramificationIdx S

Tactic:
by_cases hr : r.IsPrime

Goal state after:
case pos
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
q : Ideal S
r : Ideal T
inst✝¹ : r.LiesOver q
inst✝ : Module.Flat S T
hr : r.IsPrime
⊢ r.ramificationIdx R = q.ramificationIdx R * r.ramificationIdx S

case neg
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
q : Ideal S
r : Ideal T
inst✝¹ : r.LiesOver q
inst✝ : Module.Flat S T
hr : ¬r.IsPrime
⊢ r.ramificationIdx R = q.ramificationIdx R * r.ramificationIdx S
Module: Mathlib.RingTheory.RamificationInertia.Ramification

Goal state before:
pp: case pos
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
q : Ideal S
G : Type u_4
inst✝² : Group G
inst✝¹ : MulSemiringAction G S
inst✝ : SMulCommClass G R S
g : G
hq : q.IsPrime
p : Ideal R := under R q
f₀ : S ≃ₐ[R] S := (MulSemiringAction.toAlgAut G R S) g
hg : g • q = map f₀ q
Sq : Type u_2 := Localization.AtPrime q
Sq' : Type u_2 := Localization.AtPrime (map f₀ q)
f : Sq ≃ₐ[R] Sq' := Localization.localAlgEquiv q (map f₀ q) f₀ ⋯
this✝ : Algebra Sq Sq' := f.toRingEquiv.toRingHom.toAlgebra
this : IsScalarTower R Sq Sq'
e : (Sq ⧸ map (algebraMap R Sq) p) ≃ₐ[Sq] Sq' ⧸ map (algebraMap R Sq') p :=
  (map (algebraMap R Sq) p).quotientEquivAlg (map (algebraMap R Sq') p) (AlgEquiv.ofBijective (Algebra.ofId Sq Sq') ⋯) ⋯
⊢ (g • q).ramificationIdx R = q.ramificationIdx R

Tactic:
hg,

Goal state after:
case pos
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
q : Ideal S
G : Type u_4
inst✝² : Group G
inst✝¹ : MulSemiringAction G S
inst✝ : SMulCommClass G R S
g : G
hq : q.IsPrime
p : Ideal R := under R q
f₀ : S ≃ₐ[R] S := (MulSemiringAction.toAlgAut G R S) g
hg : g • q = map f₀ q
Sq : Type u_2 := Localization.AtPrime q
Sq' : Type u_2 := Localization.AtPrime (map f₀ q)
f : Sq ≃ₐ[R] Sq' := Localization.localAlgEquiv q (map f₀ q) f₀ ⋯
this✝ : Algebra Sq Sq' := f.toRingEquiv.toRingHom.toAlgebra
this : IsScalarTower R Sq Sq'
e : (Sq ⧸ map (algebraMap R Sq) p) ≃ₐ[Sq] Sq' ⧸ map (algebraMap R Sq') p :=
  (map (algebraMap R Sq) p).quotientEquivAlg (map (algebraMap R Sq') p) (AlgEquiv.ofBijective (Algebra.ofId Sq Sq') ⋯) ⋯
⊢ (map f₀ q).ramificationIdx R = q.ramificationIdx R
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
hRS : (RingHom.ker (algebraMap R S)).FG
H : Function.Bijective ⇑(localRingHom p q (algebraMap R S) ⋯)
s : Finset S
hs : Algebra.adjoin R ↑s = ⊤
a b : S → R
hbp : ∀ (x : S), b x ∉ p
e : ∀ (x : S), (algebraMap R S) (a x) = x * (algebraMap R S) (b x)
r : R
hrp : r ∉ p
hr : ∀ (r' : R), r ∣ r' → Function.Injective ⇑(awayMap (algebraMap R S) r')
r' : R
hr' : r * ∏ i ∈ s, b i ∣ r'
⊢ ↑s ⊆
    ↑(Subalgebra.comap (IsScalarTower.toAlgHom R S (Away ((Algebra.ofId R S) r')))
        (awayMapₐ (Algebra.ofId R S) r').range)

Tactic:
intro x hxs

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
hRS : (RingHom.ker (algebraMap R S)).FG
H : Function.Bijective ⇑(localRingHom p q (algebraMap R S) ⋯)
s : Finset S
hs : Algebra.adjoin R ↑s = ⊤
a b : S → R
hbp : ∀ (x : S), b x ∉ p
e : ∀ (x : S), (algebraMap R S) (a x) = x * (algebraMap R S) (b x)
r : R
hrp : r ∉ p
hr : ∀ (r' : R), r ∣ r' → Function.Injective ⇑(awayMap (algebraMap R S) r')
r' : R
hr' : r * ∏ i ∈ s, b i ∣ r'
x : S
hxs : x ∈ ↑s
⊢ x ∈
    ↑(Subalgebra.comap (IsScalarTower.toAlgHom R S (Away ((Algebra.ofId R S) r')))
        (awayMapₐ (Algebra.ofId R S) r').range)
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r p : ℝ≥0
h : p ≠ 0
⊢ r < p⁻¹ ↔ r * p < 1

Tactic:
rw [← mul_lt_mul_iff_right₀ (pos_iff_ne_zero.2 h), mul_inv_cancel₀ h, mul_comm]

Goal state after:
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
⊢ False

Tactic:
refine (le_csSup ub ?_).not_gt ((lt_add_iff_pos_left _).2 (half_pos ε0))

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
⊢ ε / 2 + sSup s ∈ s
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: a : ℝ
ha : ∀ (k : ℕ), 0 < k → a ≤ 1 / ↑k + 1
q : ℚ
hq : 1 < ↑q.num / ↑q.den
⊢ 1 ≤ q * ↑q.den - ↑q.den

Tactic:
one_lt_div (by positivity)

Goal state after:
a : ℝ
ha : ∀ (k : ℕ), 0 < k → a ≤ 1 / ↑k + 1
q : ℚ
hq : ↑q.den < ↑q.num
⊢ 1 ≤ q * ↑q.den - ↑q.den
Module: Mathlib.Data.ENNReal.Real

Goal state before:
pp: case inr
a b : ℝ≥0∞
h : a ≤ b
ht : b = ∞ → a = ∞
ha : a ≠ ∞
⊢ a.toReal ≤ b.toReal

Tactic:
exact toReal_mono (mt ht ha) h

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

Goal state before:
pp: case pos
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : x = 0
⊢ (if x + y = 0 then 0 else 1) ≤ max (if x = 0 then 0 else 1) (if y = 0 then 0 else 1)

Tactic:
simp_rw [if_pos hx, hx, zero_add]

Goal state after:
case pos
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : x = 0
⊢ (if y = 0 then 0 else 1) ≤ max 0 (if y = 0 then 0 else 1)
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: r₂ : ℝ≥0∞
h₂ : r₂ ≠ ∞
r₁ : ℝ≥0
⊢ (↑r₁ + r₂).toNNReal = (↑r₁).toNNReal + r₂.toNNReal

Tactic:
lift r₂ to ℝ≥0 using h₂

Goal state after:
r₁ r₂ : ℝ≥0
⊢ (↑r₁ + ↑r₂).toNNReal = (↑r₁).toNNReal + (↑r₂).toNNReal
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: a b c : ℝ≥0∞
h : 0 < b → b < a → c ≠ ∞
⊢ (a - b) * c = a * c - b * c

Tactic:
by
  rcases le_or_gt a b with hab | hab; · simp [hab, mul_left_mono hab, tsub_eq_zero_of_le]
  rcases eq_zero_or_pos b with (rfl | hb); · simp
  exact (cancel_of_ne <| mul_ne_top hab.ne_top (h hb hab)).tsub_mul

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

Goal state before:
pp: m n : ℕ
⊢ ↑↑m ≤ ↑↑n ↔ m ≤ n

Tactic:
EReal.coe_le_coe_iff,

Goal state after:
m n : ℕ
⊢ ↑m ≤ ↑n ↔ m ≤ n
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x✝ : ↑{⊥, ⊤}ᶜ
x : EReal
hx : x ∈ {⊥, ⊤}ᶜ
⊢ (fun x ↦ ⟨↑x, ⋯⟩) ((fun x ↦ (↑x).toReal) ⟨x, hx⟩) = ⟨x, hx⟩

Tactic:
by
    lift x to ℝ
    · simpa [not_or, and_comm] using hx
    · simp

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

Goal state before:
pp: a b : ℝ≥0∞
htop : b ≠ ∞ ∨ a ≠ ∞
hzero : b ≠ 0 ∨ a ≠ 0
⊢ (a / b)⁻¹ = b / a

Tactic:
rw [← ENNReal.inv_ne_zero] at htop
  rw [← ENNReal.inv_ne_top] at hzero
  rw [ENNReal.div_eq_inv_mul, ENNReal.div_eq_inv_mul, ENNReal.mul_inv htop hzero, mul_comm, inv_inv]

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

Goal state before:
pp: case coe.inr
a x✝ : ℝ≥0
h : a < x✝
ha : a ≠ 0
⊢ (↑x✝)⁻¹ < (↑a)⁻¹

Tactic:
← coe_inv h.ne_bot,

Goal state after:
case coe.inr
a x✝ : ℝ≥0
h : a < x✝
ha : a ≠ 0
⊢ ↑x✝⁻¹ < (↑a)⁻¹
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a : ℝ≥0∞
h : a ≠ ∞
⊢ ∞ / a = ∞

Tactic:
by simp [top_div, h]

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
n : ℤ
⊢ count K v (↑v.asIdeal ^ n) = n

Tactic:
count_zpow,

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
v : HeightOneSpectrum R
n : ℤ
⊢ n * count K v ↑v.asIdeal = n
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b : ℝ≥0∞
ha : a ≠ ∞
hb₀ : b ≠ 0
hb : b ≠ ∞
⊢ a + 1 ≠ ∞

Tactic:
by finiteness

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

Goal state before:
pp: case hp₂
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
exps : HeightOneSpectrum R → ℤ
w : HeightOneSpectrum R
hw : w ∈ fun i ↦ i = v → False
⊢ count K v (↑w.asIdeal ^ exps w) = 0

Tactic:
count_zpow,

Goal state after:
case hp₂
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
exps : HeightOneSpectrum R → ℤ
w : HeightOneSpectrum R
hw : w ∈ fun i ↦ i = v → False
⊢ exps w * count K v ↑w.asIdeal = 0
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
p : α → Prop
a : { a // p a }
r : ℝ≥0∞
⊢ val '' val ⁻¹' eball (↑a) r = eball (↑a) r ∩ {a | p a}

Tactic:
image_preimage_eq_inter_range,

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
p : α → Prop
a : { a // p a }
r : ℝ≥0∞
⊢ eball (↑a) r ∩ range val = eball (↑a) r ∩ {a | p a}
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
p : α → Prop
a : { a // p a }
r : ℝ≥0∞
⊢ val '' val ⁻¹' closedEBall (↑a) r = closedEBall (↑a) r ∩ {a | p a}

Tactic:
image_preimage_eq_inter_range,

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
p : α → Prop
a : { a // p a }
r : ℝ≥0∞
⊢ closedEBall (↑a) r ∩ range val = closedEBall (↑a) r ∩ {a | p a}
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: ι : Sort u_1
κ : Sort u_2
f : ι → ℝ≥0∞
a : ℝ≥0∞
g : κ → ℝ≥0∞
hf : ∃ i, f i ≠ ∞
hg : ∃ j, g j ≠ ∞
ha : ∀ (i : ι) (j : κ), a ≤ f i * g j
⊢ a ≤ (⨅ i, f i) * ⨅ j, g j

Tactic:
← iInf_ne_top_subtype

Goal state after:
ι : Sort u_1
κ : Sort u_2
f : ι → ℝ≥0∞
a : ℝ≥0∞
g : κ → ℝ≥0∞
hf : ∃ i, f i ≠ ∞
hg : ∃ j, g j ≠ ∞
ha : ∀ (i : ι) (j : κ), a ≤ f i * g j
⊢ a ≤ (⨅ i, f ↑i) * ⨅ j, g j
Module: Mathlib.Data.Real.Pointwise

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

pp: case inr.inr
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : IsOrderedModule α ℝ
a : α
ha : 0 ≤ a
s : Set ℝ
hs : s.Nonempty
ha' : 0 < a
⊢ sSup (a • s) = a • sSup s

Tactic:
· rw [zero_smul_set hs, zero_smul]
    exact csSup_singleton 0

Goal state after:
case inr.inr
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : IsOrderedModule α ℝ
a : α
ha : 0 ≤ a
s : Set ℝ
hs : s.Nonempty
ha' : 0 < a
⊢ sSup (a • s) = a • sSup s
Module: Mathlib.Data.Real.Pointwise

Goal state before:
pp: case inr.inl
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Module α ℝ
inst✝ : IsOrderedModule α ℝ
s : Set ℝ
hs : s.Nonempty
ha : 0 ≤ 0
⊢ sSup (0 • s) = 0 • sInf s

pp: case inr.inr
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Module α ℝ
inst✝ : IsOrderedModule α ℝ
a : α
ha : a ≤ 0
s : Set ℝ
hs : s.Nonempty
ha' : a < 0
⊢ sSup (a • s) = a • sInf s

Tactic:
· rw [zero_smul_set hs, zero_smul]
    exact csSup_singleton 0

Goal state after:
case inr.inr
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Module α ℝ
inst✝ : IsOrderedModule α ℝ
a : α
ha : a ≤ 0
s : Set ℝ
hs : s.Nonempty
ha' : a < 0
⊢ sSup (a • s) = a • sInf s
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
a : α
⊢ (∀ (i : ℝ), 0 < i → ∃ y ∈ s, y ∈ ball a i) ↔ ∀ ε > 0, ∃ b ∈ s, dist a b < ε

Tactic:
simp only [mem_ball, dist_comm]

Goal state after:
Module: Mathlib.Topology.Bornology.Constructions

Goal state before:
pp: α : Type u_1
inst✝ : Bornology α
p : α → Prop
⊢ BoundedSpace (Subtype p) ↔ Bornology.IsBounded {x | p x}

Tactic:
by
  rw [boundedSpace_induced_iff, Subtype.range_coe_subtype]

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

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
p : α → Prop
a : { a // p a }
r : ℝ
⊢ val '' val ⁻¹' ball (↑a) r = ball (↑a) r ∩ {a | p a}

Tactic:
image_preimage_eq_inter_range,

Goal state after:
α : Type u_1
inst✝ : PseudoMetricSpace α
p : α → Prop
a : { a // p a }
r : ℝ
⊢ ball (↑a) r ∩ range val = ball (↑a) r ∩ {a | p a}
Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
p : α → Prop
a : { a // p a }
r : ℝ
⊢ val '' val ⁻¹' closedBall (↑a) r = closedBall (↑a) r ∩ {a | p a}

Tactic:
image_preimage_eq_inter_range,

Goal state after:
α : Type u_1
inst✝ : PseudoMetricSpace α
p : α → Prop
a : { a // p a }
r : ℝ
⊢ closedBall (↑a) r ∩ range val = closedBall (↑a) r ∩ {a | p a}
Module: Mathlib.Topology.Order.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
hab : a ≠ b
⊢ closure[inst✝³] (Ioc a b) = Icc a b

Tactic:
by
  apply Subset.antisymm
  · exact closure_minimal Ioc_subset_Icc_self isClosed_Icc
  · apply Subset.trans _ (closure_mono Ioo_subset_Ioc_self)
    rw [closure_Ioo hab]

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
a b c : FractionalIdeal R⁰ K
hac : a ≤ c
ha : a ≠ 0
hb : b ≠ 0
⊢ ∃ x, a + FractionalIdeal.spanSingleton R⁰ x * b = c

Tactic:
wlog hb' : b = 1

Goal state after:
case inr
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
a b c : FractionalIdeal R⁰ K
hac : a ≤ c
ha : a ≠ 0
hb : b ≠ 0
this :
  ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K]
    [inst_3 : IsFractionRing R K] [IsDedekindDomain R] {a b c : FractionalIdeal R⁰ K},
    a ≤ c → a ≠ 0 → b ≠ 0 → b = 1 → ∃ x, a + FractionalIdeal.spanSingleton R⁰ x * b = c
hb' : ¬b = 1
⊢ ∃ x, a + FractionalIdeal.spanSingleton R⁰ x * b = c

R✝ : Type u_1
inst✝⁸ : CommRing R✝
K✝ : Type u_2
inst✝⁷ : Field K✝
inst✝⁶ : Algebra R✝ K✝
inst✝⁵ : IsFractionRing R✝ K✝
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
a b c : FractionalIdeal R⁰ K
hac : a ≤ c
ha : a ≠ 0
hb : b ≠ 0
hb' : b = 1
⊢ ∃ x, a + FractionalIdeal.spanSingleton R⁰ x * b = c
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 y : X), d x y = d y x

Tactic:
simp [hd, edist_comm]

Goal state after:
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 : EMetricSpace X
d : X → X → ℝ≥0∞
hd : d = edist
⊢ ∀ (x y : X), d x y = d y x

Tactic:
simp [hd, edist_comm]

Goal state after: