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

Goal state before:
pp: case refine_5
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
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hf : Surjective ⇑(algebraMap P S)
P' : Type u_2 := ⋯
h₁ : Surjective ⇑(algebraMap P' S)
h₂ : RingHom.ker (algebraMap P' S) ^ 2 = ⊥
e₁ : (RingHom.ker (algebraMap P S)).Cotangent ≃ₗ[P] ↥(RingHom.ker (algebraMap P' S)) := ⋯
e₂ : S ⊗[P'] Ω[P'⁄R] ≃ₗ[P] S ⊗[P] Ω[P⁄R] := ⋯
H : kerCotangentToTensor R P S = ↑e₂ ∘ₗ ↑P (kerToTensor R P' S) ∘ₗ ↑e₁
f : { l // l ∘ₗ kerToTensor R P' S = LinearMap.id }
x : S
a✝ : P'
⊢ ↑((((AlgebraTensorModule.curry
                ↑((fun x ↦
                      match x with
                      | ⟨l, hl⟩ => ⟨{ toAddHom := ↑(↑e₁ ∘ₗ l ∘ₗ ↑e₂), map_smul' := ⋯ }, ⋯⟩)
                    ((fun x ↦
                        match x with
                        | ⟨l, hl⟩ => ⟨↑e₁.symm ∘ₗ ↑P l ∘ₗ ↑e₂.symm, ⋯⟩)
                      f)))
              x).compDer
          (D R P'))
        a✝) =
    ↑((((AlgebraTensorModule.curry ↑f) x).compDer (D R P')) a✝)

Tactic:
simp only [AlgebraTensorModule.curry_apply, Derivation.coe_comp, LinearMap.coe_comp,
      LinearMap.coe_restrictScalars, Derivation.coeFn_coe, Function.comp_apply, curry_apply,
      LinearMap.coe_mk, AddHom.coe_coe, LinearEquiv.coe_coe,
      LinearEquiv.symm_apply_apply, LinearEquiv.apply_symm_apply]

Goal state after:
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)
this : (algebraMap A (Localization.AtPrime Q)) ((aeval x) q) = 0
m : K[X]
hm : (aeval x) m ∈ Q.primeCompl
hm' : p ∣ m * q
H : q * q ∣ p
⊢ False

Tactic:
have := (mul_dvd_mul_iff_right (minpoly.ne_zero (Algebra.IsIntegral.isIntegral _))).mp
    (H.trans hm')

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)
this✝ : (algebraMap A (Localization.AtPrime Q)) ((aeval x) q) = 0
m : K[X]
hm : (aeval x) m ∈ Q.primeCompl
hm' : p ∣ m * q
H : q * q ∣ p
this : q ∣ m
⊢ False
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)
this✝ : (algebraMap A (Localization.AtPrime Q)) ((aeval x) q) = 0
m : K[X]
hm : (aeval x) m ∈ Q.primeCompl
hm' : p ∣ m * q
H : q * q ∣ p
this : q ∣ m
⊢ False

Tactic:
rw [minpoly.dvd_iff, aeval_algebraMap_apply, Q.algebraMap_residueField_eq_zero] at this

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)
this✝ : (algebraMap A (Localization.AtPrime Q)) ((aeval x) q) = 0
m : K[X]
hm : (aeval x) m ∈ Q.primeCompl
hm' : p ∣ m * q
H : q * q ∣ p
this : (aeval x) m ∈ Q
⊢ False
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: 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 : P.Ring
x_in✝ : x ∈ P.toExtension.ker
x_in : x ∈ RingHom.ker (aeval P.val)
property✝ : Extension.Cotangent.mk ⟨x, x_in✝⟩ ∈ P.toExtension.cotangentComplex.ker
⊢ C (↑(aeval P.val) x) ∈ Q.toExtension.ker ^ 2

Tactic:
RingHom.coe_coe,

Goal state after:
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 : P.Ring
x_in✝ : x ∈ P.toExtension.ker
x_in : x ∈ RingHom.ker (aeval P.val)
property✝ : Extension.Cotangent.mk ⟨x, x_in✝⟩ ∈ P.toExtension.cotangentComplex.ker
⊢ C ((aeval P.val) x) ∈ Q.toExtension.ker ^ 2
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: 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 : P.Ring
x_in✝ : x ∈ P.toExtension.ker
x_in : x ∈ RingHom.ker (aeval P.val)
property✝ : Extension.Cotangent.mk ⟨x, x_in✝⟩ ∈ P.toExtension.cotangentComplex.ker
⊢ (Q.ofComp P).toAlgHom ((Q.toComp P).toAlgHom x) ∈ Q.toExtension.ker ^ 2

Tactic:
rw [toComp_toAlgHom, toAlgHom_ofComp_rename, Generators.algebraMap_eq, RingHom.coe_coe,
    x_in, RingHom.map_zero]

Goal state after:
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 : P.Ring
x_in✝ : x ∈ P.toExtension.ker
x_in : x ∈ RingHom.ker (aeval P.val)
property✝ : Extension.Cotangent.mk ⟨x, x_in✝⟩ ∈ P.toExtension.cotangentComplex.ker
⊢ 0 ∈ Q.toExtension.ker ^ 2
Module: Mathlib.RingTheory.Etale.Kaehler

Goal state before:
pp: case left
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
inst✝ : Module.Flat S T
H₁ : f.toRingHom.FormallyEtale
H₂ : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
⊢ Function.Injective ⇑(LinearMap.liftBaseChange T (H1Cotangent.map f))

pp: case right
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
inst✝ : Module.Flat S T
H₁ : f.toRingHom.FormallyEtale
H₂ : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
⊢ Function.Surjective ⇑(LinearMap.liftBaseChange T (H1Cotangent.map f))

Tactic:
· rw [injective_iff_map_eq_zero]
    intro x hx
    apply Module.Flat.lTensor_preserves_injective_linearMap _ h1Cotangentι_injective
    apply (Extension.tensorCotangent f halg H₂).injective
    simp only [map_zero]
    rw [← h1Cotangentι.map_zero, ← hx]
    change ((Cotangent.map f).liftBaseChange T ∘ₗ h1Cotangentι.baseChange T) x =
      (h1Cotangentι ∘ₗ _) x
    congr 1
    ext x
    simp

Goal state after:
case right
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
inst✝ : Module.Flat S T
H₁ : f.toRingHom.FormallyEtale
H₂ : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
⊢ Function.Surjective ⇑(LinearMap.liftBaseChange T (H1Cotangent.map f))
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 }
v w : { x // x.asIdeal ∣ I }
hvw : (fun v ↦ ⟨(↑v).asIdeal, ⋯⟩) v = (fun v ↦ ⟨(↑v).asIdeal, ⋯⟩) w
⊢ ((fun a ↦ ↑a) v).asIdeal = ((fun a ↦ ↑a) w).asIdeal

Tactic:
by simpa using hvw

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: 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 ⇑φ
⊢ Surjective ⇑(map P.asIdeal φ)

Tactic:
rintro ⟨y, hy⟩
  obtain ⟨b, rfl⟩ : ∃ a, φ a = y := hf y
  obtain ⟨f, hf⟩ : ∃ f : Π₀ i : HeightOneSpectrum A, primaryComponent M₁ i.asIdeal,
      (DFinsupp.lsum ℕ fun i : HeightOneSpectrum A ↦
      (primaryComponent M₁ i.asIdeal).subtype) f = b := by
    simp only [← mem_iSup_iff_exists_dfinsupp, iSup_primaryComponent_eq_top hM₁, mem_top]
  refine ⟨f P, Subtype.ext ?_⟩
  simp only [map_apply_coe]
  rw [eq_comm, ← sub_eq_zero]
  refine (Submodule.disjoint_def.mp (iSupIndep_primaryComponent A M₂ P)) _ ?_ ?_
  · exact Submodule.sub_mem _ hy (primaryComponent_map_mem _ _ _)
  · have hdiff : φ b - φ ↑(f P) = ∑ Q ∈ f.support \ {P}, φ ↑(f Q) := by
      rw [sub_eq_iff_eq_add',
        ← Finset.sum_eq_add_sum_sdiff_singleton P (fun P ↦ φ (f P)) (by aesop)]
      simpa [DFinsupp.sumAddHom_apply, DFinsupp.sum] using congr(φ $hf).symm
    rw [hdiff]
    exact Submodule.sum_mem _ fun Q hQ ↦ Submodule.mem_iSup_of_mem Q <|
        Submodule.mem_iSup_of_mem (by grind) (primaryComponent_map_mem _ _ _)

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

Goal state before:
pp: a : ℝ≥0∞
⊢ (∞ * a).toReal = 0

Tactic:
by
  rw [mul_comm]
  exact toReal_mul_top _

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

Goal state before:
pp: p q : ℝ≥0∞
hpq : p ≤ q
⊢ p = 0 ∧ q = 0 ∨
    p = 0 ∧ q = ∞ ∨
      p = 0 ∧ 0 < q.toReal ∨ p = ∞ ∧ q = ∞ ∨ 0 < p.toReal ∧ q = ∞ ∨ 0 < p.toReal ∧ 0 < q.toReal ∧ p.toReal ≤ q.toReal

Tactic:
rcases eq_or_lt_of_le (bot_le : 0 ≤ p) with ((rfl : 0 = p) | (hp : 0 < p))

Goal state after:
case inl
q : ℝ≥0∞
hpq : 0 ≤ q
⊢ 0 = 0 ∧ q = 0 ∨
    0 = 0 ∧ q = ∞ ∨
      0 = 0 ∧ 0 < q.toReal ∨
        0 = ∞ ∧ q = ∞ ∨ 0 < ENNReal.toReal 0 ∧ q = ∞ ∨ 0 < ENNReal.toReal 0 ∧ 0 < q.toReal ∧ ENNReal.toReal 0 ≤ q.toReal

case inr
p q : ℝ≥0∞
hpq : p ≤ q
hp : 0 < p
⊢ p = 0 ∧ q = 0 ∨
    p = 0 ∧ q = ∞ ∨
      p = 0 ∧ 0 < q.toReal ∨ p = ∞ ∧ q = ∞ ∨ 0 < p.toReal ∧ q = ∞ ∨ 0 < p.toReal ∧ 0 < q.toReal ∧ p.toReal ≤ q.toReal
Module: Mathlib.Data.EReal.Basic

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

Tactic:
by
    induction x
    · simp at hx
    · simp
    · simp at hx

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

Goal state before:
pp: case zero
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
⊢ count K v 1 = ↑0 * count K v I

Tactic:
ofNat_zero,

Goal state after:
case zero
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
⊢ count K v 1 = 0 * 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 0

Tactic:
count_zero,

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) * 0
Module: Mathlib.Data.ENNReal.Inv

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

Tactic:
· simp [← mul_assoc, ENNReal.mul_inv_cancel, *]

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
hv : ↑v.asIdeal ≠ 0
h_self : ↑v.asIdeal = spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑v.asIdeal
hv_irred : Irreducible (Associates.mk v.asIdeal)
⊢ ↑1 - ↑0 = 1

Tactic:
ofNat_zero,

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)
⊢ ↑1 - 0 = 1
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b c : ℝ≥0∞
⊢ a / b * c = a * (c / b)

Tactic:
simp only [div_eq_mul_inv, mul_left_comm, mul_comm]

Goal state after:
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 0 = -count K v 0

Tactic:
count_zero,

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
⊢ 0 = -0
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case coe.coe
x✝¹ x✝ : ℝ≥0
ha : ↑x✝ ≠ 0 ∨ ↑x✝¹ ≠ ∞
hb : ↑x✝ ≠ ∞ ∨ ↑x✝¹ ≠ 0
⊢ (↑x✝ * ↑x✝¹)⁻¹ = (↑x✝)⁻¹ * (↑x✝¹)⁻¹

Tactic:
grind [_=_ coe_mul, coe_zero, inv_zero, = mul_inv, coe_ne_top, ENNReal.inv_eq_zero,
    =_ coe_inv, zero_mul, = mul_eq_zero, mul_top, mul_zero, top_mul]

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 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)
⊢ ↑((Associates.mk v.asIdeal).count (Associates.mk w.asIdeal).factors) - ↑0 = 0

Tactic:
ofNat_zero,

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)
⊢ ↑((Associates.mk v.asIdeal).count (Associates.mk w.asIdeal).factors) - 0 = 0
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a : ℝ≥0∞
ha : a ≠ 0
h'a : a ≠ ∞
n : ℤ
⊢ 0 < a ^ n

Tactic:
cases n

Goal state after:
case ofNat
a : ℝ≥0∞
ha : a ≠ 0
h'a : a ≠ ∞
a✝ : ℕ
⊢ 0 < a ^ Int.ofNat a✝

case negSucc
a : ℝ≥0∞
ha : a ≠ 0
h'a : a ≠ ∞
a✝ : ℕ
⊢ 0 < a ^ Int.negSucc a✝
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a : ℝ≥0∞
ha : a ≠ 0
h'a : a ≠ ∞
n : ℤ
⊢ a ^ n < ∞

Tactic:
cases n

Goal state after:
case ofNat
a : ℝ≥0∞
ha : a ≠ 0
h'a : a ≠ ∞
a✝ : ℕ
⊢ a ^ Int.ofNat a✝ < ∞

case negSucc
a : ℝ≥0∞
ha : a ≠ 0
h'a : a ≠ ∞
a✝ : ℕ
⊢ a ^ Int.negSucc a✝ < ∞
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
⊢ (𝓤 α).HasBasis p fun x ↦ {p | edist p.1 p.2 ≤ f x}

Tactic:
by
  refine ⟨fun s => uniformity_basis_edist.mem_iff.trans ?_⟩
  constructor
  · rintro ⟨ε, ε₀, hε⟩
    rcases exists_between ε₀ with ⟨ε', hε'⟩
    rcases hf ε' hε'.1 with ⟨i, hi, H⟩
    exact ⟨i, hi, fun x hx => hε <| lt_of_le_of_lt (le_trans hx.out H) hε'.2⟩
  · exact fun ⟨i, hi, H⟩ => ⟨f i, hf₀ i hi, fun x hx => H (le_of_lt hx.out)⟩

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

Goal state before:
pp: x : ℝ≥0∞
n : ℤ
⊢ x⁻¹ ^ n = (x ^ n)⁻¹

Tactic:
cases n

Goal state after:
case ofNat
x : ℝ≥0∞
a✝ : ℕ
⊢ x⁻¹ ^ Int.ofNat a✝ = (x ^ Int.ofNat a✝)⁻¹

case negSucc
x : ℝ≥0∞
a✝ : ℕ
⊢ x⁻¹ ^ Int.negSucc a✝ = (x ^ Int.negSucc a✝)⁻¹
Module: Mathlib.Analysis.Normed.Group.Defs

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
inst✝ : Group E
f : GroupSeminorm E
x : E
⊢ f (x⁻¹ * x) = 0

Tactic:
simp only [inv_mul_cancel, map_one_eq_zero]

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

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

Tactic:
by
  refine le_antisymm (le_iInf fun i ↦ mul_le_mul' (iInf_le ..) (iInf_le ..))
    (le_iInf_mul_iInf hf hg fun i j ↦ ?_)
  obtain ⟨k, hk⟩ := h i j
  exact iInf_le_of_le k hk

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x y : α
⊢ Function.swap dist x y = dist x y

Tactic:
exact dist_comm _ _

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
s : Finset (HeightOneSpectrum R) := ⋯.toFinset
this : ∀ p ∈ s, J * ∏ q ∈ s, q.asIdeal < J * ∏ q ∈ s \ {p}, q.asIdeal
a : HeightOneSpectrum R → R
ha : ∀ p ∈ s, a p ∈ J * ∏ q ∈ s \ {p}, q.asIdeal
ha' : ∀ p ∈ s, a p ∉ J * ∏ q ∈ s, q.asIdeal
K : Ideal R
hK : Ideal.span {∑ p ∈ s, a p} = J * K
⊢ I + K = ⊤

Tactic:
by_contra H

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
s : Finset (HeightOneSpectrum R) := ⋯.toFinset
this : ∀ p ∈ s, J * ∏ q ∈ s, q.asIdeal < J * ∏ q ∈ s \ {p}, q.asIdeal
a : HeightOneSpectrum R → R
ha : ∀ p ∈ s, a p ∈ J * ∏ q ∈ s \ {p}, q.asIdeal
ha' : ∀ p ∈ s, a p ∉ J * ∏ q ∈ s, q.asIdeal
K : Ideal R
hK : Ideal.span {∑ p ∈ s, a p} = J * K
H : ¬I + K = ⊤
⊢ False
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝¹ : PseudoMetricSpace α
β : Type u_3
p : β → Prop
f : β → ℝ
l : Filter β
inst✝ : l.NeBot
hf₀ : ∀ (i : β), p i → 0 < f i
hf₁ : ∀ᶠ (i : β) in l, p i
hf : ∀ (i : ℝ), 0 < i → ∀ᶠ (x : β) in l, f x ∈ closedBall 0 i
ε : ℝ
hε : 0 < ε
i : β
hp : p i
hi : f i ∈ closedBall 0 ε
⊢ p i ∧ f i ≤ ε

Tactic:
exact ⟨hp, by
    simpa [Metric.mem_closedBall, Real.dist_eq, abs_of_nonneg (hf₀ i hp).le] using hi⟩

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

Goal state before:
pp: case refine_1
β : Type u_2
inst✝³ : Fintype β
Y : Type u_4
inst✝² : PseudoMetricSpace Y
inst✝¹ : Zero Y
inst✝ : DecidableEq β
i j : β
a b : Y
h : i ≠ j
k : β
⊢ nndist (if k = i then a else 0) (if k = j then b else 0) ≤ max (nndist a 0) (nndist b 0)

Tactic:
by_cases hki : k = i <;> by_cases hkj : k = j

Goal state after:
case pos
β : Type u_2
inst✝³ : Fintype β
Y : Type u_4
inst✝² : PseudoMetricSpace Y
inst✝¹ : Zero Y
inst✝ : DecidableEq β
i j : β
a b : Y
h : i ≠ j
k : β
hki : k = i
hkj : k = j
⊢ nndist (if k = i then a else 0) (if k = j then b else 0) ≤ max (nndist a 0) (nndist b 0)

case neg
β : Type u_2
inst✝³ : Fintype β
Y : Type u_4
inst✝² : PseudoMetricSpace Y
inst✝¹ : Zero Y
inst✝ : DecidableEq β
i j : β
a b : Y
h : i ≠ j
k : β
hki : k = i
hkj : ¬k = j
⊢ nndist (if k = i then a else 0) (if k = j then b else 0) ≤ max (nndist a 0) (nndist b 0)

case pos
β : Type u_2
inst✝³ : Fintype β
Y : Type u_4
inst✝² : PseudoMetricSpace Y
inst✝¹ : Zero Y
inst✝ : DecidableEq β
i j : β
a b : Y
h : i ≠ j
k : β
hki : ¬k = i
hkj : k = j
⊢ nndist (if k = i then a else 0) (if k = j then b else 0) ≤ max (nndist a 0) (nndist b 0)

case neg
β : Type u_2
inst✝³ : Fintype β
Y : Type u_4
inst✝² : PseudoMetricSpace Y
inst✝¹ : Zero Y
inst✝ : DecidableEq β
i j : β
a b : Y
h : i ≠ j
k : β
hki : ¬k = i
hkj : ¬k = j
⊢ nndist (if k = i then a else 0) (if k = j then b else 0) ≤ max (nndist a 0) (nndist b 0)
Module: Mathlib.Topology.Order.Monotone

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
x y : α
h_nonempty : (Ioo y x).Nonempty
Mf : MonotoneOn f (Ioo y x)
h_bdd : BddAbove (f '' Ioo y x)
l : β
hl : l < sSup (f '' Ioo y x)
⊢ ∃ a ∈ Ioo y x, l < f a

Tactic:
simpa only [mem_image, exists_prop, exists_exists_and_eq_and] using
        exists_lt_of_lt_csSup (h_nonempty.image _) hl

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

Goal state before:
pp: α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : ClosedIicTopology α
s : Set α
hs : IsCompact s
ne_s : s.Nonempty
this : Nonempty ↑s
⊢ (s ∩ ⋂ x, Iic ↑x).Nonempty

Tactic:
by_contra H

Goal state after:
α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : ClosedIicTopology α
s : Set α
hs : IsCompact s
ne_s : s.Nonempty
this : Nonempty ↑s
H : ¬(s ∩ ⋂ x, Iic ↑x).Nonempty
⊢ False
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case refine_3
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 J I' J' : FractionalIdeal R⁰ K
H : I * J' = I' * J
h : J ≤ I
h' : J' ≤ I'
hJ' : J' ≠ 0
hI : I ≠ 0
this : J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I = spanSingleton R⁰ (I'.divMod I J') * J
⊢ Injective
    ⇑((Submodule.comap (↑I).subtype ↑J).mapQ (Submodule.comap (↑I').subtype ↑J')
        (LinearMap.restrict ((Algebra.lsmul R R K) (I'.divMod I J')) ⋯) ⋯)

Tactic:
← LinearMap.ker_eq_bot,

Goal state after:
case refine_3
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 J I' J' : FractionalIdeal R⁰ K
H : I * J' = I' * J
h : J ≤ I
h' : J' ≤ I'
hJ' : J' ≠ 0
hI : I ≠ 0
this : J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I = spanSingleton R⁰ (I'.divMod I J') * J
⊢ ((Submodule.comap (↑I).subtype ↑J).mapQ (Submodule.comap (↑I').subtype ↑J')
        (LinearMap.restrict ((Algebra.lsmul R R K) (I'.divMod I J')) ⋯) ⋯).ker =
    ⊥
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a : E
⊢ dist 1 a = ‖a‖

Tactic:
by rw [dist_comm, dist_one_right]

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a : E
n : ℤ
hn : IsUnit n
⊢ ‖a ^ n.natAbs‖ = ‖a‖

Tactic:
Int.isUnit_iff_natAbs_eq.mp hn,

Goal state after:
E : Type u_5
inst✝ : SeminormedGroup E
a : E
n : ℤ
hn : IsUnit n
⊢ ‖a ^ 1‖ = ‖a‖