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

Goal state before:
pp: case mp
R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
P : Extension R A
inst✝ : FormallySmooth R P.Ring
e : P.ker.Cotangent ≃ₗ[P.Ring] P.Cotangent :=
  let __spread.0 := AddEquiv.refl P.ker.Cotangent;
  { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
    right_inv := ⋯ }
l : A ⊗[P.Ring] Ω[P.Ring⁄R] →ₗ[P.Ring] (RingHom.ker (algebraMap P.Ring A)).Cotangent
hl : l ∘ₗ kerCotangentToTensor R P.Ring A = LinearMap.id
⊢ ∃ l, l ∘ₗ P.cotangentComplex = LinearMap.id

Tactic:
exact ⟨(e.comp l).extendScalarsOfSurjective P.algebraMap_surjective,
      LinearMap.ext (DFunLike.congr_fun hl : _)⟩

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

Goal state before:
pp: case h2
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 σ
x : (Q.comp P).Ring
hx' : x ∈ (Q.comp P).toExtension.ker
y : (Q.comp P).Ring
hy : y ∈ (Q.comp P).ker * (Q.comp P).ker
e : x - y ∈ Ideal.map (Q.toComp P).toAlgHom P.ker
z : ↥(Q.comp P).ker := ⟨x - y, ⋯⟩
hz : ↑z ∈ Ideal.map (Q.toComp P).toAlgHom.toRingHom P.ker
this : Extension.Cotangent.mk ⟨x, hx'⟩ = Extension.Cotangent.mk z
⊢ P.ker ≤
    Ideal.comap (Q.toComp P).toAlgHom.toRingHom
      (Submodule.map (Submodule.subtype (Q.comp P).toExtension.ker)
        (Submodule.comap Extension.Cotangent.mk
          (Submodule.restrictScalars (Q.comp P).Ring
            (Submodule.span T ↑(Extension.Cotangent.map (Q.toComp P).toExtensionHom).range))))

Tactic:
rintro w hw

Goal state after:
case h2
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 σ
x : (Q.comp P).Ring
hx' : x ∈ (Q.comp P).toExtension.ker
y : (Q.comp P).Ring
hy : y ∈ (Q.comp P).ker * (Q.comp P).ker
e : x - y ∈ Ideal.map (Q.toComp P).toAlgHom P.ker
z : ↥(Q.comp P).ker := ⟨x - y, ⋯⟩
hz : ↑z ∈ Ideal.map (Q.toComp P).toAlgHom.toRingHom P.ker
this : Extension.Cotangent.mk ⟨x, hx'⟩ = Extension.Cotangent.mk z
w : P.Ring
hw : w ∈ P.ker
⊢ w ∈
    Ideal.comap (Q.toComp P).toAlgHom.toRingHom
      (Submodule.map (Submodule.subtype (Q.comp P).toExtension.ker)
        (Submodule.comap Extension.Cotangent.mk
          (Submodule.restrictScalars (Q.comp P).Ring
            (Submodule.span T ↑(Extension.Cotangent.map (Q.toComp P).toExtensionHom).range))))
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
a b : P
this : (a - g (f a)) * (b - g (f b)) = 0
| -0

Tactic:
← this

Goal state after:
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
a b : P
this : (a - g (f a)) * (b - g (f b)) = 0
| -((a - g (f a)) * (b - g (f b)))
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
l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))
hl : l ∘ₗ kerToTensor R P S = LinearMap.id
σ : S → P
hσ : ∀ (x : S), (algebraMap P S) (σ x) = x
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
r : R
⊢ (algebraMap P S) (σ ((algebraMap R S) r)) = (algebraMap P S) ((algebraMap R P) r)

Tactic:
simp [hσ, ← IsScalarTower.algebraMap_apply]

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

Tactic:
have : IsUnit b := by
      rw [isUnit_iff_ne_zero]
      rintro rfl
      rw [zero_smul, ← algebraMap_eq_smul_one, add_zero,
        (injective_iff_map_eq_zero' _).mp (algebraMap K L).injective] at e
      cases hab e rfl

Goal state after:
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
Module: Mathlib.RingTheory.Unramified.Field

Goal state before:
pp: K : Type u_1
A : Type u_2
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : Algebra K A
Q : Ideal A
inst✝¹ : Q.IsPrime
inst✝ : IsUnramifiedAt K Q
x : A
p : K[X]
hp₁ : Ideal.span {p} = RingHom.ker (aeval x).toRingHom
hp₂ : Function.Surjective ⇑(aeval x)
this✝² : FiniteType K A
this✝¹ : Module.Finite K (Localization.AtPrime Q)
this✝ : IsField (Localization.AtPrime Q)
this : Field (Localization.AtPrime Q) := this✝.toField
q : K[X] := minpoly K ((algebraMap A Q.ResidueField) x)
⊢ (algebraMap A Q.ResidueField) ((aeval x) q) = (algebraMap (Localization.AtPrime Q) Q.ResidueField) 0

Tactic:
← aeval_algebraMap_apply,

Goal state after:
K : Type u_1
A : Type u_2
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : Algebra K A
Q : Ideal A
inst✝¹ : Q.IsPrime
inst✝ : IsUnramifiedAt K Q
x : A
p : K[X]
hp₁ : Ideal.span {p} = RingHom.ker (aeval x).toRingHom
hp₂ : Function.Surjective ⇑(aeval x)
this✝² : FiniteType K A
this✝¹ : Module.Finite K (Localization.AtPrime Q)
this✝ : IsField (Localization.AtPrime Q)
this : Field (Localization.AtPrime Q) := this✝.toField
q : K[X] := minpoly K ((algebraMap A Q.ResidueField) x)
⊢ (aeval ((algebraMap A Q.ResidueField) x)) q = (algebraMap (Localization.AtPrime Q) Q.ResidueField) 0
Module: Mathlib.RingTheory.Etale.Kaehler

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
P : Extension R S
Q : Extension R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
H : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
x : T ⊗[S] P.Cotangent
⊢ (tensorCotangentInvFun f halg H) ((LinearMap.liftBaseChange T (Cotangent.map f)).toFun x) = x

Tactic:
simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom]

Goal state after:
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
P : Extension R S
Q : Extension R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
H : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
x : T ⊗[S] P.Cotangent
⊢ (tensorCotangentInvFun f halg H) ((LinearMap.liftBaseChange T (Cotangent.map f)) x) = x
Module: Mathlib.RingTheory.Etale.Kaehler

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
P : Extension R S
Q : Extension R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
H : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
x : Q.Ring ⊗[P.Ring] ↥P.ker
⊢ (LinearMap.liftBaseChange T (Cotangent.map f)).toFun
      ((tensorCotangentInvFun f halg H) (Cotangent.mk ((LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) x))) =
    Cotangent.mk ((LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) x)

Tactic:
simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom]

Goal state after:
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
P : Extension R S
Q : Extension R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
H : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
x : Q.Ring ⊗[P.Ring] ↥P.ker
⊢ (LinearMap.liftBaseChange T (Cotangent.map f))
      ((tensorCotangentInvFun f halg H) (Cotangent.mk ((LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) x))) =
    Cotangent.mk ((LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) x)
Module: Mathlib.RingTheory.RamificationInertia.Ramification

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
q : Ideal S
inst✝¹ : IsDedekindDomain S
inst✝ : q.LiesOver p
hq : q.IsPrime
hpS : map (algebraMap R S) p ≠ ⊥
hq' : q ≠ ⊥
this : q.IsMaximal
I : Ideal S
hqI : q ⊔ I = ⊤
h :
  map (algebraMap R S) p =
    q ^ Multiset.count q (UniqueFactorizationMonoid.normalizedFactors (map (algebraMap R S) p)) * I
⊢ ¬I ≤ q

Tactic:
contrapose! hqI

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal R
q : Ideal S
inst✝¹ : IsDedekindDomain S
inst✝ : q.LiesOver p
hq : q.IsPrime
hpS : map (algebraMap R S) p ≠ ⊥
hq' : q ≠ ⊥
this : q.IsMaximal
I : Ideal S
h :
  map (algebraMap R S) p =
    q ^ Multiset.count q (UniqueFactorizationMonoid.normalizedFactors (map (algebraMap R S) p)) * I
hqI : I ≤ q
⊢ q ⊔ I ≠ ⊤
Module: Mathlib.RingTheory.RamificationInertia.Ramification

Goal state before:
pp: case neg.hq
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
⊢ ¬q.IsPrime

Tactic:
simpa

Goal state after:
Module: Mathlib.RingTheory.RamificationInertia.Ramification

Goal state before:
pp: case neg.hq
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
⊢ ¬(g • q).IsPrime

Tactic:
simpa

Goal state after:
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') ⋯) ⋯
⊢ (map f₀ q).ramificationIdx R =
    (Module.length (Localization.AtPrime q)
        (Localization.AtPrime q ⧸ map (algebraMap R (Localization.AtPrime q)) p)).toNat

Tactic:
ramificationIdx_eq p (q.map f₀),

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') ⋯) ⋯
⊢ (Module.length (Localization.AtPrime (map f₀ q))
        (Localization.AtPrime (map f₀ q) ⧸ map (algebraMap R (Localization.AtPrime (map f₀ q))) p)).toNat =
    (Module.length (Localization.AtPrime q)
        (Localization.AtPrime q ⧸ map (algebraMap R (Localization.AtPrime q)) p)).toNat
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: A : Type u_1
M : Type u_2
inst✝² : CommRing A
I : Ideal A
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
J : Ideal A
hD : IsCoprime I J
this : ∀ (n : ℕ), Disjoint (torsionBySet A M ↑(I ^ n)) (torsionBySet A M ↑J)
x : M
⊢ ((∃ n, ∀ a ∈ I ^ n, a • x = 0) ∧ ∀ a ∈ J, a • x = 0) ↔ x = 0

Tactic:
refine ⟨fun ⟨⟨n, _⟩, _⟩ ↦ ?_, by simp_all⟩

Goal state after:
A : Type u_1
M : Type u_2
inst✝² : CommRing A
I : Ideal A
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
J : Ideal A
hD : IsCoprime I J
this : ∀ (n : ℕ), Disjoint (torsionBySet A M ↑(I ^ n)) (torsionBySet A M ↑J)
x : M
x✝ : (∃ n, ∀ a ∈ I ^ n, a • x = 0) ∧ ∀ a ∈ J, a • x = 0
n : ℕ
h✝ : ∀ a ∈ I ^ n, a • x = 0
right✝ : ∀ a ∈ J, a • x = 0
⊢ x = 0
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: f : ℕ → ℚ
H : IsCauSeq abs fun i ↦ ↑(f i)
ε : ℚ
ε0 : ε > 0
i : ℕ
hi : ∀ j ≥ i, |(fun i ↦ ↑(f i)) j - (fun i ↦ ↑(f i)) i| < ↑ε
j : ℕ
ij : j ≥ i
⊢ |f j - f i| < ε

Tactic:
by dsimp at hi; exact mod_cast hi _ ij

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r✝ r₁ r₂ : ℝ≥0
x✝ y : ℝ
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra ℝ A
r : ℝ≥0
x : A
⊢ ((algebraMap ℝ A).comp toRealHom) r * x = x * ((algebraMap ℝ A).comp toRealHom) r

Tactic:
simp [Algebra.commutes]

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r : ℝ≥0
⊢ 1 ≤ ↑r ↔ 1 ≤ r

Tactic:
rw [← coe_le_coe, coe_one]

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r : ℝ≥0
⊢ ↑r ≤ 1 ↔ r ≤ 1

Tactic:
rw [← coe_le_coe, coe_one]

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

Goal state before:
pp: case h
a : ℝ
ha : 1 < a
k : ℕ
posk : 0 < k
hk : 1 / ↑k + 1 < a
⊢ ↑(2 * k ^ 2) + 1 < a ^ (2 * k ^ 2)

Tactic:
calc
    ((2 * k ^ 2 : ℕ) + 1 : ℝ) ≤ 2 ^ (2 * k) := mod_cast Nat.two_mul_sq_add_one_le_two_pow_two_mul _
    _ = (1 / k * k + 1 : ℝ) ^ (2 * k) := by simp [posk.ne']; norm_num
    _ ≤ ((1 / k + 1) ^ k : ℝ) ^ (2 * k) := by gcongr; exact mul_add_one_le_add_one_pow (by simp) _
    _ = (1 / k + 1 : ℝ) ^ (2 * k ^ 2) := by rw [← pow_mul, mul_left_comm, sq]
    _ < a ^ (2 * k ^ 2) := by gcongr

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

Goal state before:
pp: n : ℕ
⊢ ↑n = NNReal.mk ↑n ⋯

Tactic:
mk_natCast

Goal state after:
n : ℕ
⊢ ↑n = ↑n
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: case refine_1
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
M₁ : Type u_5
M₂ : Type u_6
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module A M₁
inst✝ : Module A M₂
hM₁ : IsTorsion A M₁
P : HeightOneSpectrum A
φ : M₁ →ₗ[A] M₂
hf✝ : Surjective ⇑φ
b : M₁
hy : φ b ∈ primaryComponent M₂ P.asIdeal
f : Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal)
hf : ((DFinsupp.lsum ℕ) fun i ↦ (primaryComponent M₁ i.asIdeal).subtype) f = b
⊢ φ b - φ ↑(f P) ∈ (fun P ↦ primaryComponent M₂ P.asIdeal) P

Tactic:
exact Submodule.sub_mem _ hy (primaryComponent_map_mem _ _ _)

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

Goal state before:
pp: n : ℕ
p : ℝ
hn : n ≠ 0
⊢ ↑n ≤ ENNReal.ofReal p ↔ ↑n ≤ p

Tactic:
simp only [← not_lt, ofReal_lt_natCast hn]

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

Goal state before:
pp: R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝ : AddGroup E
p q : NonarchAddGroupSeminorm E
s : Set (NonarchAddGroupSeminorm E)
h : BddAbove s
x y : E
⊢ ⨆ p, ↑p (x + y) ≤ max (⨆ p, ↑p x) (⨆ p, ↑p y)

Tactic:
by
          obtain (rfl | hs) := eq_empty_or_nonempty s
          · simp
          · have : Nonempty s := hs.to_subtype
            refine ciSup_le fun p ↦ (map_add_le_max p.1 x y).trans ?_
            gcongr
            all_goals
              apply le_ciSup (f := (DFunLike.coe · _) ∘ Subtype.val) ?_ p
              simpa [Set.range_comp] using Monotone.map_bddAbove (fun _ _ h' ↦ by exact h' _) h

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

Goal state before:
pp: c : ℝ
a : ℝ≥0∞
h : 0 ≤ c
⊢ (ENNReal.ofReal c * a).toReal = c * a.toReal

Tactic:
ENNReal.toReal_mul,

Goal state after:
c : ℝ
a : ℝ≥0∞
h : 0 ≤ c
⊢ (ENNReal.ofReal c).toReal * a.toReal = c * a.toReal
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: a b : ℝ≥0∞
⊢ a + b ≠ ∞ ↔ a ≠ ∞ ∧ b ≠ ∞

Tactic:
simpa only [lt_top_iff_ne_top] using add_lt_top

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

Goal state before:
pp: case inr.inr
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ
h : ∀ (i : ι), 0 ≤ f i
a : ℝ≥0∞
ha : a ≠ ∞
⊢ a ≤ ENNReal.ofReal (⨅ i, f i) ↔ ∀ (i : ι), a ≤ ENNReal.ofReal (f i)

Tactic:
le_ofReal_iff_toReal_le ha,

Goal state after:
case inr.inr
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ
h : ∀ (i : ι), 0 ≤ f i
a : ℝ≥0∞
ha : a ≠ ∞
⊢ a.toReal ≤ ⨅ i, f i ↔ ∀ (i : ι), a ≤ ENNReal.ofReal (f i)

case inr.inr
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ
h : ∀ (i : ι), 0 ≤ f i
a : ℝ≥0∞
ha : a ≠ ∞
⊢ 0 ≤ ⨅ i, f i
Module: Mathlib.Data.EReal.Basic

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

Tactic:
EReal.zero_mul

Goal state after:
x : EReal
⊢ 0 = 0
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case pos
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
n : ℕ
h : count K v (I ^ n) = ↑n * count K v I
hI : I = 0
⊢ (if I ^ n ≠ 0 ∧ I ≠ 0 then count K v (I ^ n) + count K v I else 0) = ↑(n + 1) * count K v I

Tactic:
have h_neg : ¬(I ^ n ≠ 0 ∧ I ≠ 0) := by order

Goal state after:
case pos
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
n : ℕ
h : count K v (I ^ n) = ↑n * count K v I
hI : I = 0
h_neg : ¬(I ^ n ≠ 0 ∧ I ≠ 0)
⊢ (if I ^ n ≠ 0 ∧ I ≠ 0 then count K v (I ^ n) + count K v I else 0) = ↑(n + 1) * count K v I
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case pos
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
n : ℕ
h : count K v (I ^ n) = ↑n * count K v I
hI : I = 0
h_neg : ¬(I ^ n ≠ 0 ∧ I ≠ 0)
⊢ 0 = ↑(n + 1) * count K v I

Tactic:
hI,

Goal state after:
case pos
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
n : ℕ
h : count K v (I ^ n) = ↑n * count K v I
hI : I = 0
h_neg : ¬(I ^ n ≠ 0 ∧ I ≠ 0)
⊢ 0 = ↑(n + 1) * count K v 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
hv : ↑v.asIdeal ≠ 0
h_self : ↑v.asIdeal = spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑v.asIdeal
⊢ count K v ↑v.asIdeal = 1

Tactic:
have hv_irred : Irreducible (Associates.mk v.asIdeal) := by apply v.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 : HeightOneSpectrum R
hv : ↑v.asIdeal ≠ 0
h_self : ↑v.asIdeal = spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑v.asIdeal
hv_irred : Irreducible (Associates.mk v.asIdeal)
⊢ count K v ↑v.asIdeal = 1
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case neg
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 : ℤ
I : FractionalIdeal R⁰ K
hI : I = 0
hn : ¬n = 0
⊢ count K v (I ^ (-n)) = -count K v (I ^ n)

Tactic:
hI,

Goal state after:
case neg
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 : ℤ
I : FractionalIdeal R⁰ K
hI : I = 0
hn : ¬n = 0
⊢ count K v (0 ^ (-n)) = -count K v (0 ^ n)
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case refine_1
a b c : ℝ≥0∞
hb0 : b ≠ 0 ∨ c ≠ ∞
hbt : b ≠ ∞ ∨ c ≠ 0
⊢ b⁻¹ ≠ 0 ∨ c ≠ 0

Tactic:
simpa

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

Goal state before:
pp: case refine_2
a b c : ℝ≥0∞
hb0 : b ≠ 0 ∨ c ≠ ∞
hbt : b ≠ ∞ ∨ c ≠ 0
⊢ b⁻¹ ≠ ∞ ∨ c ≠ ∞

Tactic:
simpa

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

Goal state before:
pp: a b c : ℝ≥0∞
hc₀ : c ≠ 0
hc : c ≠ ∞
⊢ c⁻¹ ≠ 0

Tactic:
simpa

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

Goal state before:
pp: a b c : ℝ≥0∞
hc₀ : c ≠ 0
hc : c ≠ ∞
⊢ c⁻¹ ≠ ∞

Tactic:
simpa

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

Goal state before:
pp: case inr
a b : ℝ≥0∞
ha : a ≠ ∞
hb₀ : b ≠ 0
hb : b ≠ ∞
⊢ ∃ c, 0 < c ∧ c * a < b

Tactic:
refine ⟨b / (a + 1), ENNReal.div_pos hb₀ (by finiteness), ENNReal.mul_lt_of_lt_div ?_⟩

Goal state after:
case inr
a b : ℝ≥0∞
ha : a ≠ ∞
hb₀ : b ≠ 0
hb : b ≠ ∞
⊢ b / (a + 1) < b / a
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case ha
b c a : ℝ≥0∞
h0 : b ≠ 0 ∨ c ≠ 0
htop : b ≠ ∞ ∨ c ≠ ∞
⊢ b ≠ 0 ∨ c⁻¹ ≠ ∞

Tactic:
simpa

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

Goal state before:
pp: case hb
b c a : ℝ≥0∞
h0 : b ≠ 0 ∨ c ≠ 0
htop : b ≠ ∞ ∨ c ≠ ∞
⊢ b ≠ ∞ ∨ c⁻¹ ≠ 0

Tactic:
simpa

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

Goal state before:
pp: case pos
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 → ℤ
I I' : FractionalIdeal R⁰ K
hI : count K v I = 0
hI' : count K v I' = 0
h : I ≠ 0 ∧ I' ≠ 0
⊢ count K v I + count K v I' = 0

Tactic:
hI,

Goal state after:
case pos
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 → ℤ
I I' : FractionalIdeal R⁰ K
hI : count K v I = 0
hI' : count K v I' = 0
h : I ≠ 0 ∧ I' ≠ 0
⊢ 0 + count K v I' = 0
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a : ℝ≥0∞
hz : a ≠ 0
ht : a ≠ ∞
⊢ a / 2 < a

Tactic:
lift a to ℝ≥0 using ht
  rw [coe_ne_zero] at hz
  rw [← coe_two, ← coe_div, coe_lt_coe]
  exacts [NNReal.half_lt_self hz, two_ne_zero' _]

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

Goal state before:
pp: case negSucc.ofNat
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.negSucc a ≤ Int.ofNat b
⊢ x ^ Int.negSucc a ≤ x ^ Int.ofNat b

Tactic:
simp only [zpow_negSucc, Int.ofNat_eq_natCast, zpow_natCast]
    refine (ENNReal.inv_le_one.2 ?_).trans ?_ <;> exact one_le_pow_of_one_le' hx _

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

Goal state before:
pp: u : ℝ≥0∞ˣ
hu : ↑u = ∞
this : ↑u * ↑u⁻¹ = ∞ * ↑u⁻¹
⊢ False

Tactic:
simp at this

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

Goal state before:
pp: ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
hinfty : a = 0 → ⨅ i, f i = 0 → ∃ i, f i = 0
h₀ : a = ∞ → Nonempty ι
⊢ a⁻¹ = ∞ → ⨅ i, f i = 0 → ∃ i, f i = 0

Tactic:
simpa

Goal state after: