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

Goal state before:
pp: case hs
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
⊢ b - g (f b) ∈ RingHom.ker f

Tactic:
simpa using

Goal state after:
case hs
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
⊢ f b = f (g (f b))
Module: Mathlib.RingTheory.Smooth.Kaehler

Goal state before:
pp: case e_a
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
this : Algebra S P := g.toAlgebra
p : P
s : S
m : ↥(RingHom.ker (algebraMap P S))
⊢ g ((algebraMap P S) p) - p ∈ RingHom.ker (algebraMap P S)

Tactic:
simpa using

Goal state after:
case e_a
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
this : Algebra S P := g.toAlgebra
p : P
s : S
m : ↥(RingHom.ker (algebraMap P S))
⊢ (algebraMap P S) (g ((algebraMap P S) p)) = (algebraMap P S) p
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✝² : Algebra.IsSeparable K L
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra K B
I : Ideal B
hI : I ^ 2 = ⊥
f₁ f₂ : L →ₐ[K] B
e : (Ideal.Quotient.mkₐ K I).comp f₁ = (Ideal.Quotient.mkₐ K I).comp f₂
x : L
⊢ f₁ x - f₂ x ∈ I

Tactic:
simpa using

Goal state after:
K : Type u_1
L : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Algebra.IsSeparable K L
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra K B
I : Ideal B
hI : I ^ 2 = ⊥
f₁ f₂ : L →ₐ[K] B
e : (Ideal.Quotient.mkₐ K I).comp f₁ = (Ideal.Quotient.mkₐ K I).comp f₂
x : L
⊢ f₁ x - f₂ x ∈ I
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 = ⊥
a b : S
⊢ σ (a + b) - ↑(l (1 ⊗ₜ[P] (D R P) (σ (a + b)))) =
    σ a - ↑(l (1 ⊗ₜ[P] (D R P) (σ a))) + (σ b - ↑(l (1 ⊗ₜ[P] (D R P) (σ b))))

Tactic:
by
    simp only [sectionOfRetractionKerToTensorAux_prop l hl (σ (a + b)) (σ a + σ b) (by simp [hσ]),
      map_add, tmul_add, Submodule.coe_add, add_sub_add_comm]

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
inst✝³ : FormallyUnramified K A
inst✝² : EssFiniteType K A
inst✝¹ : IsAlgClosed K
inst✝ : IsLocalRing A
⊢ Function.Bijective ⇑(algebraMap K A)

Tactic:
have := finite_of_free (R := K) (S := A)
  have : IsArtinianRing A := isArtinian_of_tower K inferInstance
  have hA : IsNilpotent (IsLocalRing.maximalIdeal A) := by
    rw [← IsLocalRing.jacobson_eq_maximalIdeal ⊥]
    · exact IsArtinianRing.isNilpotent_jacobson_bot
    · exact bot_ne_top
  let e : K ≃ₐ[K] A ⧸ IsLocalRing.maximalIdeal A := {
    __ := Algebra.ofId K (A ⧸ IsLocalRing.maximalIdeal A)
    __ := Equiv.ofBijective _ IsAlgClosed.algebraMap_bijective_of_isIntegral }
  let e' : A ⊗[K] (A ⧸ IsLocalRing.maximalIdeal A) ≃ₐ[A] A :=
    (Algebra.TensorProduct.congr AlgEquiv.refl e.symm).trans (Algebra.TensorProduct.rid K A A)
  let f : A ⧸ IsLocalRing.maximalIdeal A →ₗ[A] A := e'.toLinearMap.comp (sec K A _)
  have hf : (Algebra.ofId _ _).toLinearMap ∘ₗ f = LinearMap.id := by
    dsimp [f]
    rw [← LinearMap.comp_assoc, ← comp_sec K A]
    congr 1
    apply LinearMap.restrictScalars_injective K
    apply _root_.TensorProduct.ext'
    intro r s
    obtain ⟨s, rfl⟩ := e.surjective s
    suffices s • (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A)) r = r • e s by
      simpa [ofId, e']
    simp [Algebra.smul_def, e, ofId, mul_comm]
  have hf₁ : f 1 • (1 : A ⧸ IsLocalRing.maximalIdeal A) = 1 := by
    rw [← algebraMap_eq_smul_one]
    exact LinearMap.congr_fun hf 1
  have hf₂ : 1 - f 1 ∈ IsLocalRing.maximalIdeal A := by
    rw [← Ideal.Quotient.eq_zero_iff_mem, map_sub, map_one, ← Ideal.Quotient.algebraMap_eq,
     algebraMap_eq_smul_one, hf₁, sub_self]
  have hf₃ : IsIdempotentElem (1 - f 1) := by
    apply IsIdempotentElem.one_sub
    rw [IsIdempotentElem, ← smul_eq_mul, ← map_smul, hf₁]
  have hf₄ : f 1 = 1 := by
    obtain ⟨n, hn⟩ := hA
    have : (1 - f 1) ^ n = 0 := by
      rw [← Ideal.mem_bot, ← Ideal.zero_eq_bot, ← hn]
      exact Ideal.pow_mem_pow hf₂ n
    rw [eq_comm, ← sub_eq_zero, ← hf₃.pow_succ_eq n, pow_succ, this, zero_mul]
  refine Equiv.bijective ⟨algebraMap K A, ⇑e.symm ∘ ⇑(algebraMap A _), fun x ↦ by simp, fun x ↦ ?_⟩
  have : ⇑(algebraMap K A) = ⇑f ∘ ⇑e := by
    ext k
    conv_rhs => rw [← mul_one k, ← smul_eq_mul, Function.comp_apply, map_smul,
      LinearMap.map_smul_of_tower, map_one, hf₄, ← algebraMap_eq_smul_one]
  rw [this]
  simp only [Function.comp_apply, AlgEquiv.apply_symm_apply, algebraMap_eq_smul_one,
    map_smul, hf₄, smul_eq_mul, mul_one]

Goal state after:
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
inst✝ : Algebra.FormallyEtale S T
⊢ ⇑(lift (↑S ((Algebra.linearMap T (Module.End T (Ω[S⁄R] →ₗ[S] Ω[T⁄R]))).flip (map R R S T)))) =
    ⇑(tensorKaehlerEquivOfFormallyEtale R S T)

Tactic:
change _ = ((tensorKaehlerEquivOfFormallyEtale
    R S T).toLinearMap.restrictScalars S : T ⊗[S] Ω[S⁄R] → _)

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
inst✝ : Algebra.FormallyEtale S T
⊢ ⇑(lift (↑S ((Algebra.linearMap T (Module.End T (Ω[S⁄R] →ₗ[S] Ω[T⁄R]))).flip (map R R S T)))) =
    ⇑(↑S ↑(tensorKaehlerEquivOfFormallyEtale R S T))
Module: Mathlib.RingTheory.Smooth.Kaehler

Goal state before:
pp: R : Type u_1
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x : ↥P.ker
hx : P.toInfinitesimal.toRingHom ↑x ∈ ⊥
⊢ ↑x ∈ P.ker ^ 2

Tactic:
simpa using

Goal state after:
R : Type u_1
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x : ↥P.ker
hx : P.toInfinitesimal.toRingHom ↑x ∈ ⊥
⊢ ↑x ∈ P.ker ^ 2
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
inst✝⁴ : IsLocalRing R
inst✝³ : IsLocalRing S
inst✝² : IsLocalHom (algebraMap R S)
inst✝¹ : EssFiniteType R S
inst✝ : Algebra.IsSeparable (ResidueField R) (ResidueField S)
H : Ideal.map (algebraMap R S) (maximalIdeal R) = maximalIdeal S
this✝ : FormallyUnramified (ResidueField R) (ResidueField S)
this : FormallyUnramified R (ResidueField S)
x : S
hx : x ∈ RingHom.ker (algebraMap S (ResidueField S))
⊢ x ∈ Ideal.map (algebraMap R S) (maximalIdeal R)

Tactic:
simpa using

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing R
inst✝³ : IsLocalRing S
inst✝² : IsLocalHom (algebraMap R S)
inst✝¹ : EssFiniteType R S
inst✝ : Algebra.IsSeparable (ResidueField R) (ResidueField S)
H : Ideal.map (algebraMap R S) (maximalIdeal R) = maximalIdeal S
this✝ : FormallyUnramified (ResidueField R) (ResidueField S)
this : FormallyUnramified R (ResidueField S)
x : S
hx : x ∈ RingHom.ker (algebraMap S (ResidueField S))
⊢ ¬IsUnit x
Module: Mathlib.RingTheory.Smooth.Kaehler

Goal state before:
pp: case right
R : Type u_1
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x : P.Cotangent
hx : (Cotangent.map P.toInfinitesimal) x ∈ P.infinitesimal.cotangentComplex.ker
⊢ x ∈ P.cotangentComplex.ker

Tactic:
simpa using

Goal state after:
case right
R : Type u_1
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x : P.Cotangent
hx : (Cotangent.map P.toInfinitesimal) x ∈ P.infinitesimal.cotangentComplex.ker
⊢ P.cotangentComplex x = 0
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: case add
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 y : T ⊗[S] P.toExtension.H1Cotangent
hx :
  (LinearMap.liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom))
      ((LinearMap.lTensor T Extension.h1Cotangentι) x) ∈
    (Q.comp P).toExtension.cotangentComplex.ker
hy :
  (LinearMap.liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom))
      ((LinearMap.lTensor T Extension.h1Cotangentι) y) ∈
    (Q.comp P).toExtension.cotangentComplex.ker
⊢ (LinearMap.liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom))
      ((LinearMap.lTensor T Extension.h1Cotangentι) (x + y)) ∈
    (Q.comp P).toExtension.cotangentComplex.ker

Tactic:
simpa using

Goal state after:
case add
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 y : T ⊗[S] P.toExtension.H1Cotangent
hx :
  (LinearMap.liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom))
      ((LinearMap.lTensor T Extension.h1Cotangentι) x) ∈
    (Q.comp P).toExtension.cotangentComplex.ker
hy :
  (LinearMap.liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom))
      ((LinearMap.lTensor T Extension.h1Cotangentι) y) ∈
    (Q.comp P).toExtension.cotangentComplex.ker
⊢ (Q.comp P).toExtension.cotangentComplex
        ((LinearMap.liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom))
          ((LinearMap.lTensor T Extension.h1Cotangentι) x)) +
      (Q.comp P).toExtension.cotangentComplex
        ((LinearMap.liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom))
          ((LinearMap.lTensor T Extension.h1Cotangentι) y)) =
    0
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 σ
inst✝ : Flat S T
x : (Q.comp P).toExtension.Cotangent
x_in : x ∈ (Q.comp P).toExtension.cotangentComplex.ker
hx : ⟨x, x_in⟩ ∈ (Extension.H1Cotangent.map (Q.ofComp P).toExtensionHom).ker
⊢ (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) x = 0

Tactic:
simpa using

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 σ
inst✝ : Flat S T
x : (Q.comp P).toExtension.Cotangent
x_in : x ∈ (Q.comp P).toExtension.cotangentComplex.ker
hx : ⟨x, x_in⟩ ∈ (Extension.H1Cotangent.map (Q.ofComp P).toExtensionHom).ker
⊢ (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) x = 0
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✝¹ : Algebra.IsIntegral R S
inst✝ : FaithfulSMul R S
x : R
s : ↥p.primeCompl
hx : (localRingHom p q (algebraMap R S) ⋯) (IsLocalization.mk' (Localization.AtPrime p) x s) = 0
⊢ ∃ a ∉ q, a * (algebraMap R S) x = 0

Tactic:
simpa using

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✝¹ : Algebra.IsIntegral R S
inst✝ : FaithfulSMul R S
x : R
s : ↥p.primeCompl
hx : (localRingHom p q (algebraMap R S) ⋯) (IsLocalization.mk' (Localization.AtPrime p) x s) = 0
⊢ ∃ a ∉ q, a * (algebraMap R S) x = 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
M : Submonoid S
inst✝ : IsLocalization M T
P : Extension R S := (Generators.self R S).toExtension
M' : Submonoid P.Ring := Submonoid.comap (algebraMap P.Ring S) M
x✝ : ↥M'
y : P.Ring
hy : y ∈ M'
⊢ IsUnit (((IsScalarTower.toAlgHom R S T).comp (IsScalarTower.toAlgHom R P.Ring S)) ↑⟨y, hy⟩)

Tactic:
simpa using

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
M : Submonoid S
inst✝ : IsLocalization M T
P : Extension R S := (Generators.self R S).toExtension
M' : Submonoid P.Ring := Submonoid.comap (algebraMap P.Ring S) M
x✝ : ↥M'
y : P.Ring
hy : y ∈ M'
⊢ IsUnit ((algebraMap S T) ((algebraMap P.Ring S) y))
Module: Mathlib.RingTheory.RamificationInertia.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
p : Ideal R
inst✝⁴ : p.IsPrime
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.QuasiFinite R S
inst✝ : Fintype ↑(p.primesOver S)
this✝¹ : Fintype (PrimeSpectrum (p.Fiber S)) := Fintype.ofFinite (PrimeSpectrum (p.Fiber S))
q : PrimeSpectrum (p.Fiber S)
a✝ : q ∈ Finset.univ
r : Ideal S := comap Algebra.TensorProduct.includeRight q.asIdeal
this✝ : Algebra (Localization.AtPrime p) (Localization.AtPrime r) := Localization.AtPrime.algebraOfLiesOver p r
Rp : Type u_1 := Localization.AtPrime p
Sq : Type (max u_1 u_2) := Localization.AtPrime q.asIdeal
Sr : Type u_2 := Localization.AtPrime r
κp : Type u_1 := p.ResidueField
κr : Type u_2 := r.ResidueField
A : Type u_2 := Sr ⧸ map (algebraMap R Sr) p
this : length Sr A * ↑(finrank κp κr) = ↑(finrank κp Sq)
⊢ (length (Localization.AtPrime r) (Localization.AtPrime r ⧸ map (algebraMap R (Localization.AtPrime r)) p)).toNat *
      finrank p.ResidueField r.ResidueField =
    finrank p.ResidueField (Localization.AtPrime q.asIdeal)

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
p : Ideal R
inst✝⁴ : p.IsPrime
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.QuasiFinite R S
inst✝ : Fintype ↑(p.primesOver S)
this✝¹ : Fintype (PrimeSpectrum (p.Fiber S)) := Fintype.ofFinite (PrimeSpectrum (p.Fiber S))
q : PrimeSpectrum (p.Fiber S)
a✝ : q ∈ Finset.univ
r : Ideal S := comap Algebra.TensorProduct.includeRight q.asIdeal
this✝ : Algebra (Localization.AtPrime p) (Localization.AtPrime r) := Localization.AtPrime.algebraOfLiesOver p r
Rp : Type u_1 := Localization.AtPrime p
Sq : Type (max u_1 u_2) := Localization.AtPrime q.asIdeal
Sr : Type u_2 := Localization.AtPrime r
κp : Type u_1 := p.ResidueField
κr : Type u_2 := r.ResidueField
A : Type u_2 := Sr ⧸ map (algebraMap R Sr) p
this : length Sr A * ↑(finrank κp κr) = ↑(finrank κp Sq)
⊢ (length (Localization.AtPrime r) (Localization.AtPrime r ⧸ map (algebraMap R (Localization.AtPrime r)) p)).toNat *
      finrank p.ResidueField r.ResidueField =
    finrank p.ResidueField (Localization.AtPrime q.asIdeal)
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
M : Submonoid S
inst✝ : IsLocalization M T
x : H1Cotangent R S
P : Extension R S := (Generators.self R S).toExtension
M' : Submonoid P.Ring := Submonoid.comap (algebraMap P.Ring S) M
x✝ : ↥M'
y : P.Ring
hy : y ∈ M'
⊢ IsUnit (((IsScalarTower.toAlgHom R S T).comp (IsScalarTower.toAlgHom R P.Ring S)) ↑⟨y, hy⟩)

Tactic:
simpa using

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
M : Submonoid S
inst✝ : IsLocalization M T
x : H1Cotangent R S
P : Extension R S := (Generators.self R S).toExtension
M' : Submonoid P.Ring := Submonoid.comap (algebraMap P.Ring S) M
x✝ : ↥M'
y : P.Ring
hy : y ∈ M'
⊢ IsUnit ((algebraMap S T) ((algebraMap P.Ring S) y))
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✝⁴ : FaithfulSMul R S
inst✝³ : q.LiesOver p
inst✝² : Algebra.IsUnramifiedAt R q
inst✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝ : AtPrime.IsLiesOverAlgebra p q
H : Function.Surjective ⇑(algebraMap p.ResidueField q.ResidueField)
⊢ (RingHom.ker (algebraMap R S)).FG

Tactic:
by simpa using! Submodule.fg_bot

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

Goal state before:
pp: case mp
A : Type u_1
M : Type u_2
inst✝² : CommRing A
I : Ideal A
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
x : M
a : ∃ i, x ∈ torsionBySet A M ↑(I ^ i)
⊢ ∃ n, ∀ a ∈ I ^ n, a • x = 0

Tactic:
simpa using

Goal state after:
case mp
A : Type u_1
M : Type u_2
inst✝² : CommRing A
I : Ideal A
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
x : M
a : ∃ i, x ∈ torsionBySet A M ↑(I ^ i)
⊢ ∃ n, ∀ a ∈ I ^ n, a • x = 0
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: A : Type u_1
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
inst✝⁶ : CommRing A
I : Ideal A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : Module A M
inst✝¹ : Module A M₁
inst✝ : Module A M₂
φ : M₁ →ₗ[A] M₂
c : ↥(primaryComponent M₁ I)
⊢ (φ.domRestrict (primaryComponent M₁ I)) c ∈ primaryComponent M₂ I

Tactic:
simpa using

Goal state after:
A : Type u_1
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
inst✝⁶ : CommRing A
I : Ideal A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : Module A M
inst✝¹ : Module A M₁
inst✝ : Module A M₂
φ : M₁ →ₗ[A] M₂
c : ↥(primaryComponent M₁ I)
⊢ φ ↑c ∈ primaryComponent M₂ I
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: A : Type u_1
M : Type u_2
inst✝³ : CommRing A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : IsDedekindDomain A
h : IsTorsion A M
x : M
a : A
ha : a ∈ A⁰
hmem : x ∈ torsionBySet A M ↑(span {a})
⊢ span {a} ≠ ⊥

Tactic:
simpa using

Goal state after:
A : Type u_1
M : Type u_2
inst✝³ : CommRing A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : IsDedekindDomain A
h : IsTorsion A M
x : M
a : A
ha : a ∈ A⁰
hmem : x ∈ torsionBySet A M ↑(span {a})
⊢ ¬a = 0
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : DecidableEq α
s : Finset ι
S : ι → Finset α
⊢ ↑(#(s.biUnion S)) = ∑ t, (-1) ^ (#↑t + 1) * ↑(#((↑t).inf' ⋯ S))

Tactic:
simpa using

Goal state after:
ι : Type u_1
α : Type u_2
inst✝ : DecidableEq α
s : Finset ι
S : ι → Finset α
⊢ ↑(#(s.biUnion S)) = ∑ t ∈ {x ∈ s.powerset | x.Nonempty}.attach, (-1) ^ (#↑t + 1) * ↑(#((↑t).inf' ⋯ S))
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset ι
S : ι → Finset α
⊢ ↑(#(s.inf fun i ↦ (S i)ᶜ)) = ∑ t ∈ s.powerset, (-1) ^ #t * ↑(#(t.inf S))

Tactic:
simpa using

Goal state after:
ι : Type u_1
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset ι
S : ι → Finset α
⊢ ↑(#(s.inf fun i ↦ (S i)ᶜ)) = ∑ t ∈ s.powerset, (-1) ^ #t * ↑(#(t.inf S))
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this : ∀ (d : ℕ), BddAbove {m | ∃ y ∈ s, ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d} ∧ ∀ z ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d}, z ≤ f d
n : ℕ
n0 : n > 0
y : ℝ
yS : y ∈ s
hy : ↑(f n) ≤ y * ↑n
⊢ ↑(↑(f n) / ↑n) ≤ y

Tactic:
simpa using

Goal state after:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this : ∀ (d : ℕ), BddAbove {m | ∃ y ∈ s, ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d} ∧ ∀ z ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d}, z ≤ f d
n : ℕ
n0 : n > 0
y : ℝ
yS : y ∈ s
hy : ↑(f n) ≤ y * ↑n
⊢ ↑(f n) / ↑n ≤ y
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

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

Tactic:
simpa using

Goal state after:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this : ∀ (d : ℕ), BddAbove {m | ∃ y ∈ s, ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d} ∧ ∀ z ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d}, z ≤ f d
hf₁ : ∀ n > 0, ∃ y ∈ s, ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ n > 0, ∀ y ∈ s, y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
ε : ℚ
ε0 : ε > 0
j k : ℕ
ij : ε⁻¹ ≤ ↑j
ik : ε⁻¹ ≤ ↑k
j0 : 0 < j
k0 : 0 < k
y : ℝ
yS : y ∈ s
hy : ↑(↑(f j) / ↑j) ≤ y
⊢ ↑(f j) / ↑j - ↑(f k) / ↑k < (↑k)⁻¹
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:
simpa using

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 w : { x // x.asIdeal ∣ I }
hvw : (fun v ↦ ⟨(↑v).asIdeal, ⋯⟩) v = (fun v ↦ ⟨(↑v).asIdeal, ⋯⟩) w
⊢ (↑v).asIdeal = (↑w).asIdeal
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r : ℝ
⊢ r.toNNReal = 0 ↔ r ≤ 0

Tactic:
simpa using

Goal state after:
r : ℝ
⊢ r.toNNReal = 0 ↔ r ≤ 0
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r : ℝ
⊢ r.toNNReal ≤ 1 ↔ r ≤ 1

Tactic:
simpa using

Goal state after:
r : ℝ
⊢ r.toNNReal ≤ 1 ↔ r ≤ 1
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r : ℝ
⊢ 1 < r.toNNReal ↔ 1 < r

Tactic:
simpa using

Goal state after:
r : ℝ
⊢ 1 < r.toNNReal ↔ 1 < r
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r : ℝ
n : ℕ
⊢ r.toNNReal ≤ ↑n ↔ r ≤ ↑n

Tactic:
simpa using

Goal state after:
r : ℝ
n : ℕ
⊢ r.toNNReal ≤ ↑n ↔ r ≤ ↑n
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r : ℝ
n : ℕ
⊢ ↑n < r.toNNReal ↔ ↑n < r

Tactic:
simpa using

Goal state after:
r : ℝ
n : ℕ
⊢ ↑n < r.toNNReal ↔ ↑n < r
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r : ℝ
⊢ 1 ≤ r.toNNReal ↔ 1 ≤ r

Tactic:
simpa using

Goal state after:
r : ℝ
⊢ 1 ≤ r.toNNReal ↔ 1 ≤ r
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: n : ℕ
r : ℝ
⊢ ↑n ≤ r.toNNReal ↔ ↑n ≤ r ∨ n = 0

Tactic:
simpa using

Goal state after:
n : ℕ
r : ℝ
⊢ ↑n ≤ r.toNNReal ↔ ↑n ≤ r ∨ n = 0