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

Goal state before:
pp: R : Type u_1
inst✝⁹ : CommRing R
A : Type u_2
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R A
B : Type u_3
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : IsScalarTower R A B
inst✝² : FormallyUnramified R B
Q : Type u_3
inst✝¹ : CommRing Q
inst✝ : Algebra A Q
I : Ideal Q
e : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[A] Q
e' : (Ideal.Quotient.mkₐ A I).comp f₁ = (Ideal.Quotient.mkₐ A I).comp f₂
this : Algebra R Q := ((algebraMap A Q).comp (algebraMap R A)).toAlgebra
⊢ f₁ = f₂

Tactic:
let : IsScalarTower R A Q := IsScalarTower.of_algebraMap_eq' rfl

Goal state after:
R : Type u_1
inst✝⁹ : CommRing R
A : Type u_2
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R A
B : Type u_3
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : IsScalarTower R A B
inst✝² : FormallyUnramified R B
Q : Type u_3
inst✝¹ : CommRing Q
inst✝ : Algebra A Q
I : Ideal Q
e : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[A] Q
e' : (Ideal.Quotient.mkₐ A I).comp f₁ = (Ideal.Quotient.mkₐ A I).comp f₂
this✝ : Algebra R Q := ((algebraMap A Q).comp (algebraMap R A)).toAlgebra
this : IsScalarTower R A Q := IsScalarTower.of_algebraMap_eq' rfl
⊢ f₁ = f₂
Module: Mathlib.RingTheory.Unramified.Finite

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FormallyUnramified R S
inst✝¹ : EssFiniteType R S
inst✝ : Free R S
I : Type u_2 := Free.ChooseBasisIndex R S
b : Basis I R S := Free.chooseBasis R S
f : I →₀ S
hf : elem R S = f.sum fun i x ↦ x ⊗ₜ[R] b i
x : S
a : I → I →₀ R := fun i ↦ b.repr (b i * x)
j : I
hj : j ∉ f.support
⊢ b.repr (x * f j) = 0

Tactic:
by simp [Finsupp.notMem_support_iff.mp hj]

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

Goal state before:
pp: case mpr
R : Type u_4
inst✝² : CommRing R
A : Type u_6
inst✝¹ : CommRing A
inst✝ : Algebra R A
h : Function.Surjective ⇑(algebraMap R A)
⊢ IsIdempotentElem (RingHom.ker (algebraMap R A)) → ∃ g, (ofId R A).kerSquareLift.comp g = AlgHom.id R A

Tactic:
intro H

Goal state after:
case mpr
R : Type u_4
inst✝² : CommRing R
A : Type u_6
inst✝¹ : CommRing A
inst✝ : Algebra R A
h : Function.Surjective ⇑(algebraMap R A)
H : IsIdempotentElem (RingHom.ker (algebraMap R A))
⊢ ∃ g, (ofId R A).kerSquareLift.comp g = AlgHom.id R A
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
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hg : (IsScalarTower.toAlgHom R P S).comp g = AlgHom.id R S
⊢ retractionOfSectionOfKerSqZero g hf' hg ∘ₗ kerToTensor R P S = LinearMap.id

Tactic:
by
  ext x; simp [RingHom.mem_ker.mp x.2]

Goal state after:
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)
⊢ ⊤ ≤ (algebraMap K L).range

Tactic:
intro x _

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 ∈ ⊤
⊢ x ∈ (algebraMap K L).range
Module: Mathlib.RingTheory.Unramified.Field

Goal state before:
pp: case neg
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 b : K
e : a • 1 + b • x = 0
hab : a = 0 → ¬b = 0
this : IsUnit b
⊢ x ∈ (algebraMap K L).range

Tactic:
use (-this.unit⁻¹ * a)

Goal state after:
case h
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 b : K
e : a • 1 + b • x = 0
hab : a = 0 → ¬b = 0
this : IsUnit b
⊢ (algebraMap K L) (-↑this.unit⁻¹ * a) = x
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
h_fin : Fintype { x // x ∣ I }
⊢ Injective fun v ↦ ⟨(↑v).asIdeal, ⋯⟩

Tactic:
intro v

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
h_fin : Fintype { x // x ∣ I }
v : { x // x.asIdeal ∣ I }
⊢ ∀ ⦃a₂ : { x // x.asIdeal ∣ I }⦄, (fun v ↦ ⟨(↑v).asIdeal, ⋯⟩) v = (fun v ↦ ⟨(↑v).asIdeal, ⋯⟩) a₂ → v = a₂
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
⊢ {v | v.maxPowDividing I ≠ 1} ⊆ {v | ↑((Associates.mk v.asIdeal).count (Associates.mk I).factors) ≠ 0}

Tactic:
intro v

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
v : HeightOneSpectrum R
⊢ v ∈ {v | v.maxPowDividing I ≠ 1} → v ∈ {v | ↑((Associates.mk v.asIdeal).count (Associates.mk I).factors) ≠ 0}
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case mp
s : Set ℝ
a : ℝ
h : BddBelow s
h' : s.Nonempty
⊢ (∀ (ε : ℝ), 0 < ε → sInf s < a + ε) → ∀ (ε : ℝ), 0 < ε → ∃ x ∈ s, x < a + ε

Tactic:
intro H

Goal state after:
case mp
s : Set ℝ
a : ℝ
h : BddBelow s
h' : s.Nonempty
H : ∀ (ε : ℝ), 0 < ε → sInf s < a + ε
⊢ ∀ (ε : ℝ), 0 < ε → ∃ x ∈ s, x < a + ε
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case mpr
s : Set ℝ
a : ℝ
h : BddBelow s
h' : s.Nonempty
⊢ (∀ (ε : ℝ), 0 < ε → ∃ x ∈ s, x < a + ε) → ∀ (ε : ℝ), 0 < ε → sInf s < a + ε

Tactic:
intro H

Goal state after:
case mpr
s : Set ℝ
a : ℝ
h : BddBelow s
h' : s.Nonempty
H : ∀ (ε : ℝ), 0 < ε → ∃ x ∈ s, x < a + ε
⊢ ∀ (ε : ℝ), 0 < ε → sInf s < a + ε
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
h✝ : HasFiniteMulSupport fun v ↦ v.maxPowDividing I
⊢ ∀ a ∈ Finite.toFinset h✝, a.maxPowDividing I ≠ 0

Tactic:
intro v

Goal state after:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
h✝ : HasFiniteMulSupport fun v ↦ v.maxPowDividing I
v : HeightOneSpectrum R
⊢ v ∈ Finite.toFinset h✝ → v.maxPowDividing I ≠ 0
Module: Mathlib.Data.NNReal.Defs

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

Tactic:
by_cases r = 0

Goal state after:
case pos
r p : ℝ≥0
h : 1 ≤ r * p
h✝ : r = 0
⊢ r⁻¹ ≤ p

case neg
r p : ℝ≥0
h : 1 ≤ r * p
h✝ : ¬r = 0
⊢ 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 j - (ε / 2 + sSup s)

Tactic:
add_comm,

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 - (sSup s + ε / 2)
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: case inr
ι : Sort u_1
f : ι → ℝ≥0
hf : BddAbove (range f)
h✝ : Nonempty ι
⊢ ⨆ i, f i = 0 ↔ ∀ (i : ι), f i = 0

Tactic:
· simp [← bot_eq_zero', ← le_bot_iff, ciSup_le_iff hf]

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

Goal state before:
pp: case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
⊢ ∀ (p : Associates (Ideal R)),
    Irreducible p →
      p.count (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I)).factors =
        p.count (Associates.mk I).factors

Tactic:
intro v

Goal state after:
case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
v : Associates (Ideal R)
⊢ Irreducible v →
    v.count (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I)).factors =
      v.count (Associates.mk I).factors
Module: Mathlib.Data.ENNReal.Basic

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
f : ℝ≥0∞ → α
⊢ ⨅ x, f ↑x = ⨅ x, f ↑x

Tactic:
cinfi_ne_top

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
f : ℝ≥0∞ → α
⊢ ⨅ x, f ↑x = ⨅ x, f ↑x
Module: Mathlib.Data.ENNReal.Basic

Goal state before:
pp: x : ℝ≥0∞
⊢ (∃ i, x ∈ Iio ↑i) ↔ x ∈ {∞}ᶜ

Tactic:
exact ⟨fun ⟨n, hn⟩ => ne_top_of_lt hn, ENNReal.exists_nat_gt⟩

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
a : R
J : Ideal R
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
hJ_ne_zero : J ≠ 0
hJ : ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) = ↑J
ha_ne_zero : span {a} ≠ 0
ha :
  ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk (span {a})).factors) =
    ↑(span {a})
⊢ ∀ (x : HeightOneSpectrum R),
    ↑x.asIdeal ^
        (↑((Associates.mk x.asIdeal).count (Associates.mk J).factors) -
          ↑((Associates.mk x.asIdeal).count (Associates.mk (span {a})).factors)) =
      ↑x.asIdeal ^ ↑((Associates.mk x.asIdeal).count (Associates.mk J).factors) *
        ↑x.asIdeal ^ (-↑((Associates.mk x.asIdeal).count (Associates.mk (span {a})).factors))

Tactic:
intro v

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
a : R
J : Ideal R
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
hJ_ne_zero : J ≠ 0
hJ : ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) = ↑J
ha_ne_zero : span {a} ≠ 0
ha :
  ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk (span {a})).factors) =
    ↑(span {a})
v : HeightOneSpectrum R
⊢ ↑v.asIdeal ^
      (↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
        ↑((Associates.mk v.asIdeal).count (Associates.mk (span {a})).factors)) =
    ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) *
      ↑v.asIdeal ^ (-↑((Associates.mk v.asIdeal).count (Associates.mk (span {a})).factors))
Module: Mathlib.Data.ENNReal.Real

Goal state before:
pp: a : ℝ
b : ℝ≥0
ha : 0 ≤ a
⊢ a < (↑b).toReal ↔ a < ↑b

Tactic:
rw [coe_toReal]

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
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
h_aJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
a₁ : R := choose ⋯
J₁ : Ideal R := choose ⋯
h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁
h_a₁_ne_zero : a₁ ≠ 0
h_J₁_ne_zero : J₁ ≠ 0
h_a_ne_zero : Ideal.span {a} ≠ 0
h_J_ne_zero : J ≠ 0
⊢ ¬(algebraMap R K) a₁ = (algebraMap R K) 0

Tactic:
Injective.eq_iff (IsLocalization.injective K (le_refl R⁰))

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
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
h_aJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
a₁ : R := choose ⋯
J₁ : Ideal R := choose ⋯
h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁
h_a₁_ne_zero : a₁ ≠ 0
h_J₁_ne_zero : J₁ ≠ 0
h_a_ne_zero : Ideal.span {a} ≠ 0
h_J_ne_zero : J ≠ 0
⊢ ¬a₁ = 0
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
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
h_aJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
a₁ : R := choose ⋯
J₁ : Ideal R := choose ⋯
h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁
h_a₁_ne_zero : a₁ ≠ 0
h_J₁_ne_zero : J₁ ≠ 0
h_a_ne_zero : Ideal.span {a} ≠ 0
h_J_ne_zero : J ≠ 0
h_a₁' : spanSingleton R⁰ ((algebraMap R K) a₁) ≠ 0
⊢ ¬(algebraMap R K) a = (algebraMap R K) 0

Tactic:
Injective.eq_iff (IsLocalization.injective K (le_refl R⁰))

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
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
h_aJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
a₁ : R := choose ⋯
J₁ : Ideal R := choose ⋯
h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁
h_a₁_ne_zero : a₁ ≠ 0
h_J₁_ne_zero : J₁ ≠ 0
h_a_ne_zero : Ideal.span {a} ≠ 0
h_J_ne_zero : J ≠ 0
h_a₁' : spanSingleton R⁰ ((algebraMap R K) a₁) ≠ 0
⊢ ¬a = 0
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case inr
p q : ℝ
hq : 0 ≤ q
h : q ≤ p
⊢ ENNReal.ofReal (p - q + q) = ENNReal.ofReal p

Tactic:
sub_add_cancel

Goal state after:
case inr
p q : ℝ
hq : 0 ≤ q
h : q ≤ p
⊢ ENNReal.ofReal p = ENNReal.ofReal p
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: ι : Sort u_1
f : ι → ℝ≥0∞
a c : ℝ≥0∞
⊢ a ≤ c + ⨅ i, f i ↔ ⨆ i, a - f i ≤ c

Tactic:
add_comm,

Goal state after:
ι : Sort u_1
f : ι → ℝ≥0∞
a c : ℝ≥0∞
⊢ a ≤ (⨅ i, f i) + c ↔ ⨆ i, a - f i ≤ c
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
⊢ a + iInf f = ⨅ b, a + f b

Tactic:
add_comm,

Goal state after:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
⊢ iInf f + a = ⨅ b, a + f b
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case neg
x : EReal
h : x ≠ ⊥
h' : ¬x = ⊤
⊢ ↑x.toReal ≤ x

Tactic:
· simp only [le_refl, coe_toReal h' h]

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

Goal state before:
pp: r : ℝ≥0
b : ℝ≥0∞
hb : 1 ≤ ↑r * b
⊢ ∀ (p : ℝ≥0), b = ↑p → r⁻¹ ≤ p

Tactic:
by
      rintro b rfl
      apply NNReal.inv_le_of_le_mul
      rwa [← coe_mul, ← coe_one, coe_le_coe] at hb

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

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

pp: case top
y : EReal
h : ⊤ ≤ y
⊢ ⊤.toENNReal ≤ y.toENNReal

Tactic:
· by_cases hy_top : y = ⊤
    · simp [hy_top]
    simp only [toENNReal, coe_ne_top, ↓reduceIte, toReal_coe, hy_top]
    exact ENNReal.ofReal_le_ofReal <| EReal.toReal_le_toReal h (coe_ne_bot _) hy_top

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

Goal state before:
pp: case inl
b : ℝ≥0∞
h₀ : 0 = 0 → b = 0
h₁ : 0 = ∞ → b = 0
⊢ 0 / (0 / b) = b

pp: case inr
a b : ℝ≥0∞
h₀ : a = 0 → b = 0
h₁ : a = ∞ → b = 0
ha : a ≠ 0
⊢ a / (a / b) = b

Tactic:
· simp [h₀]

Goal state after:
case inr
a b : ℝ≥0∞
h₀ : a = 0 → b = 0
h₁ : a = ∞ → b = 0
ha : a ≠ 0
⊢ a / (a / b) = b
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 w : HeightOneSpectrum R
hw : w ≠ v
hw_fact : ↑w.asIdeal = spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑w.asIdeal
hw_ne_zero : ↑w.asIdeal ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
⊢ count K v ↑w.asIdeal = 0

Tactic:
have hw' : Irreducible (Associates.mk w.asIdeal) := by apply w.associates_irreducible

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 w : HeightOneSpectrum R
hw : w ≠ v
hw_fact : ↑w.asIdeal = spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑w.asIdeal
hw_ne_zero : ↑w.asIdeal ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
hw' : Irreducible (Associates.mk w.asIdeal)
⊢ count K v ↑w.asIdeal = 0
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b c d : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ∞
hb : b ≠ 0
hb' : b ≠ ∞
| a * c = b * d

Tactic:
eq_comm

Goal state after:
a b c d : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ∞
hb : b ≠ 0
hb' : b ≠ ∞
| b * d = a * c
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b c d : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ∞
hb : b ≠ 0
hb' : b ≠ ∞
⊢ a * (c / b) = d ↔ d = a * (c / b)

Tactic:
eq_comm

Goal state after:
a b c d : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ∞
hb : b ≠ 0
hb' : b ≠ ∞
⊢ d = a * (c / b) ↔ d = a * (c / b)
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case e'_2.h
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 → ℤ
h_exps : ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, exps v = 0
⊢ (mulSupport fun v ↦ ↑v.asIdeal ^ exps v) ⊆ {x | (fun v ↦ exps v = 0) x}ᶜ

Tactic:
intro v

Goal state after:
case e'_2.h
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 → ℤ
h_exps : ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, exps v = 0
v : HeightOneSpectrum R
⊢ (v ∈ mulSupport fun v ↦ ↑v.asIdeal ^ exps v) → v ∈ {x | (fun v ↦ exps v = 0) x}ᶜ
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
a : R
J : Ideal R
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
ha_ne_zero : Ideal.span {a} ≠ 0
hJ_ne_zero : J ≠ 0
⊢ {v |
      ¬↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
            ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors) =
          0} ⊆
    {v | v.asIdeal ∣ J} ∪ {v | v.asIdeal ∣ Ideal.span {a}}

Tactic:
intro v

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
a : R
J : Ideal R
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
ha_ne_zero : Ideal.span {a} ≠ 0
hJ_ne_zero : J ≠ 0
v : HeightOneSpectrum R
⊢ v ∈
      {v |
        ¬↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
              ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors) =
            0} →
    v ∈ {v | v.asIdeal ∣ J} ∪ {v | v.asIdeal ∣ Ideal.span {a}}
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x y : α
δ ε : ℝ
h : δ + ε ≤ dist x y
⊢ ε + δ ≤ dist y x

Tactic:
add_comm,

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
δ ε : ℝ
h : δ + ε ≤ dist x y
⊢ δ + ε ≤ dist y x
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x y : α
ε₁ ε₂ : ℝ
h : (closedBall y ε₂ ∩ ball x ε₁).Nonempty
⊢ dist x y < ε₁ + ε₂

Tactic:
add_comm,

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
ε₁ ε₂ : ℝ
h : (closedBall y ε₂ ∩ ball x ε₁).Nonempty
⊢ dist x y < ε₂ + ε₁
Module: Mathlib.Data.NNReal.Basic

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
a : α
b : ℝ≥0
c : α
⊢ ↑(Pi.single a b c) = Pi.single a (↑b) c

Tactic:
by
  simpa using coe_indicator {a} (fun _ ↦ b) c

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

Goal state before:
pp: x y : ℝ
⊢ Ioo x y = Ioo ((x + y - (y - x)) / 2) ((x + y) / 2 + (y - x) / 2)

Tactic:
add_comm,

Goal state after:
x y : ℝ
⊢ Ioo x y = Ioo ((y + x - (y - x)) / 2) ((y + x) / 2 + (y - x) / 2)
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: x y : ℝ
⊢ Icc x y = Icc ((x + y - (y - x)) / 2) ((x + y) / 2 + (y - x) / 2)

Tactic:
add_comm,

Goal state after:
x y : ℝ
⊢ Icc x y = Icc ((y + x - (y - x)) / 2) ((y + x) / 2 + (y - x) / 2)
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✝¹] (Subtype.val '' range (inclusion ⋯))

Tactic:
by rw [← Set.range_comp, Set.val_comp_inclusion, Subtype.range_coe]

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

Goal state before:
pp: c : ℝ
⊢ ball 0 c = Ico 0 c.toNNReal

Tactic:
by_cases! c_pos : 0 < c

Goal state after:
case pos
c : ℝ
c_pos : 0 < c
⊢ ball 0 c = Ico 0 c.toNNReal

case neg
c : ℝ
c_pos : c ≤ 0
⊢ ball 0 c = Ico 0 c.toNNReal
Module: Mathlib.Topology.MetricSpace.Pseudo.Pi

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : PseudoMetricSpace α
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
⊢ PseudoMetricSpace ((b : β) → X b)

Tactic:
by
  /- we construct the instance from the pseudoemetric space instance to avoid checking again that
    the uniformity is the same as the product uniformity, but we register nevertheless a nice
    formula for the distance -/
  let i := PseudoEMetricSpace.toPseudoMetricSpaceOfDist
    (fun f g : ∀ b, X b => ((sup univ fun b => nndist (f b) (g b) : ℝ≥0) : ℝ))
    (fun f g => NNReal.zero_le_coe)
    (fun f g => by simp [edist_pi_def])
  refine i.replaceBornology fun s => ?_
  simp only [isBounded_iff_eventually, ← forall_isBounded_image_eval_iff,
    forall_mem_image, ← Filter.eventually_all, @dist_nndist (X _)]
  refine eventually_congr ((eventually_ge_atTop 0).mono fun C hC ↦ ?_)
  lift C to ℝ≥0 using hC
  refine ⟨fun H x hx y hy ↦ NNReal.coe_le_coe.2 <| Finset.sup_le fun b _ ↦ H b hx hy,
    fun H b x hx y hy ↦ NNReal.coe_le_coe.2 ?_⟩
  exact Finset.sup_le_iff.1 (NNReal.coe_le_coe.1 <| H hx hy) b (Finset.mem_univ b)

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

Goal state before:
pp: β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
x : (b : β) → X b
r : ℝ
hr : 0 ≤ r
⊢ closedBall x r = Set.univ.pi fun b ↦ closedBall (x b) r

Tactic:
by
  ext p
  simp [dist_pi_le_iff hr]

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

Goal state before:
pp: 𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
r _r _y : ℝ
⊢ |_y - _r| = ‖-_r + _y‖

Tactic:
add_comm,

Goal state after:
𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
r _r _y : ℝ
⊢ |_y - _r| = ‖_y + -_r‖
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 J : FractionalIdeal R⁰ K
⊢ divMod 0 I J = 0

Tactic:
simp [divMod, ← and_assoc]

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

Goal state before:
pp: case inr
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : ClosedIicTopology α
inst✝ : Nonempty α
s : Set α
hs : IsCompact s
hne : s.Nonempty
⊢ BddBelow s

Tactic:
obtain ⟨a, -, has⟩ := hs.exists_isLeast hne
    exact ⟨a, has⟩

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
u v : E
⊢ ‖u‖ ≤ ‖v‖ + ‖u⁻¹ * v‖

Tactic:
add_comm,

Goal state after:
E : Type u_5
inst✝ : SeminormedGroup E
u v : E
⊢ ‖u‖ ≤ ‖u⁻¹ * v‖ + ‖v‖