mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case inl
K : Type u_1
inst✝³ : Ring K
inst✝² : NoZeroDivisors K
inst✝¹ : Nontrivial K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
n : ℕ := Fintype.card ↥G
nzero : ↑(Fintype.card ↥G) = 0
p : ℕ
char_p : CharP K p
hd : p ∣ n
pprime : Nat.Prime p
fact_pprime : Fact (Nat.Prime p)
x : ↥G
hx : orderOf x = p
u : K := ↑↑x
hu : orderOf u = p
h : u = 1
⊢ False

Tactic:
apply pprime.one_lt.ne

Goal state after:
case inl
K : Type u_1
inst✝³ : Ring K
inst✝² : NoZeroDivisors K
inst✝¹ : Nontrivial K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
n : ℕ := ⋯
nzero : ↑(Fintype.card ↥G) = 0
p : ℕ
char_p : CharP K p
hd : p ∣ n
pprime : Nat.Prime p
fact_pprime : Fact (Nat.Prime p)
x : ↥G
hx : orderOf x = p
u : K := ⋯
hu : orderOf u = p
h : u = 1
⊢ 1 = p
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: K : Type u_4
L : Type u_5
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
ι : Type w
inst✝² : Algebra.IsSeparable K L
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι K L
this : FiniteDimensional K L
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
⊢ ((pb.basis.toMatrix ⇑b)ᵀ * (LinearMap.BilinForm.toMatrix pb.basis) (traceForm K L) * pb.basis.toMatrix ⇑b).det ≠ 0

Tactic:
←
    det_comm' (pb.basis.toMatrix_mul_toMatrix_flip b) _,

Goal state after:
K : Type u_4
L : Type u_5
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
ι : Type w
inst✝² : Algebra.IsSeparable K L
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι K L
this : FiniteDimensional K L
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
⊢ (pb.basis.toMatrix ⇑b * ((pb.basis.toMatrix ⇑b)ᵀ * (LinearMap.BilinForm.toMatrix pb.basis) (traceForm K L))).det ≠ 0

K : Type u_4
L : Type u_5
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
ι : Type w
inst✝² : Algebra.IsSeparable K L
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι K L
this : FiniteDimensional K L
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
⊢ b.toMatrix ⇑pb.basis * pb.basis.toMatrix ⇑b = 1
Module: Mathlib.RingTheory.Int.Basic

Goal state before:
pp: a b : ℤ
⊢ IsCoprime a b ↔ a.natAbs.Coprime b.natAbs

Tactic:
rw [isCoprime_iff_gcd_eq_one, Nat.coprime_iff_gcd_eq_one, gcd_eq_natAbs]

Goal state after:
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
h : i < q - 1
hi : ¬i = 0
hiq : ¬q - 1 ∣ i
φ : Kˣ ↪ K := { toFun := fun x ↦ ↑x, inj' := ⋯ }
⊢ ∑ x, x ^ i = 0

Tactic:
have : univ.map φ = univ \ {0} := by
      ext x
      simpa only [mem_map, mem_univ, Function.Embedding.coeFn_mk, true_and, mem_sdiff,
        mem_singleton, φ] using! isUnit_iff_ne_zero

Goal state after:
case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
h : i < q - 1
hi : ¬i = 0
hiq : ¬q - 1 ∣ i
φ : Kˣ ↪ K := { toFun := fun x ↦ ↑x, inj' := ⋯ }
this : map φ univ = univ \ {0}
⊢ ∑ x, x ^ i = 0
Module: Mathlib.NumberTheory.RamificationInertia.Inertia

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal R
S₁ : Type u_1
inst✝¹ : CommRing S₁
inst✝ : Algebra R S₁
e : S ≃ₐ[R] S₁
P : Ideal S₁
he : comap f (comap e P) = p ↔ comap (algebraMap R S₁) P = p
⊢ p.inertiaDeg' (comap e P) = p.inertiaDeg' P

Tactic:
by_cases h : P.LiesOver p

Goal state after:
case pos
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal R
S₁ : Type u_1
inst✝¹ : CommRing S₁
inst✝ : Algebra R S₁
e : S ≃ₐ[R] S₁
P : Ideal S₁
he : comap f (comap e P) = p ↔ comap (algebraMap R S₁) P = p
h : P.LiesOver p
⊢ p.inertiaDeg' (comap e P) = p.inertiaDeg' P

case neg
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal R
S₁ : Type u_1
inst✝¹ : CommRing S₁
inst✝ : Algebra R S₁
e : S ≃ₐ[R] S₁
P : Ideal S₁
he : comap f (comap e P) = p ↔ comap (algebraMap R S₁) P = p
h : ¬P.LiesOver p
⊢ p.inertiaDeg' (comap e P) = p.inertiaDeg' P
Module: Mathlib.RingTheory.Artinian.Ring

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommSemiring L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r₁ : R
s : ↥S
⊢ ∃ r, IsLocalization.mk' L 1 s = (algebraMap R L) r

Tactic:
obtain ⟨n, r, hr⟩ := IsArtinian.exists_pow_succ_smul_dvd (s : R) (1 : R)

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommSemiring L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r₁ : R
s : ↥S
n : ℕ
r : R
hr : ↑s ^ n.succ • r = ↑s ^ n • 1
⊢ ∃ r, IsLocalization.mk' L 1 s = (algebraMap R L) r
Module: Mathlib.RingTheory.Spectrum.Prime.Noetherian

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
p : Ideal R
inst✝ : p.IsPrime
r : R
hr : (toPiLocalization R) r = Pi.single { asIdeal := p, isPrime := ⋯ } 1
this : (algebraMap R (Localization p.primeCompl)) r = 1
⊢ r ∉ p

pp: case refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
p : Ideal R
inst✝ : p.IsPrime
r : R
hr : (toPiLocalization R) r = Pi.single { asIdeal := p, isPrime := ⋯ } 1
this : (algebraMap R (Localization p.primeCompl)) r = 1
⊢ IsIdempotentElem r

pp: case refine_3
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
p : Ideal R
inst✝ : p.IsPrime
r : R
hr : (toPiLocalization R) r = Pi.single { asIdeal := p, isPrime := ⋯ } 1
this : (algebraMap R (Localization p.primeCompl)) r = 1
⊢ ∀ (q : Ideal R), q.IsPrime → q ≠ p → r ∈ q

Tactic:
· rw [← IsLocalization.AtPrime.to_map_mem_maximal_iff (Localization.AtPrime p) p, this]
    simp

Goal state after:
case refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
p : Ideal R
inst✝ : p.IsPrime
r : R
hr : (toPiLocalization R) r = Pi.single { asIdeal := p, isPrime := ⋯ } 1
this : (algebraMap R (Localization p.primeCompl)) r = 1
⊢ IsIdempotentElem r

case refine_3
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
p : Ideal R
inst✝ : p.IsPrime
r : R
hr : (toPiLocalization R) r = Pi.single { asIdeal := p, isPrime := ⋯ } 1
this : (algebraMap R (Localization p.primeCompl)) r = 1
⊢ ∀ (q : Ideal R), q.IsPrime → q ≠ p → r ∈ q
Module: Mathlib.RingTheory.Spectrum.Prime.Noetherian

Goal state before:
pp: case refine_3
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
p : Ideal R
inst✝ : p.IsPrime
r : R
hr : (toPiLocalization R) r = Pi.single { asIdeal := p, isPrime := ⋯ } 1
this : (algebraMap R (Localization p.primeCompl)) r = 1
⊢ ∀ (q : Ideal R), q.IsPrime → q ≠ p → r ∈ q

Tactic:
· intro q hq e
    have : PrimeSpectrum.mk q inferInstance ≠ ⟨p, inferInstance⟩ := ne_of_apply_ne (·.1) e
    have : (algebraMap R (Localization.AtPrime q)) r = 0 := by
      simpa [PrimeSpectrum.toPiLocalization, this,
        -FaithfulSMul.algebraMap_eq_zero_iff] using funext_iff.mp hr ⟨q, inferInstance⟩
    rw [← IsLocalization.AtPrime.to_map_mem_maximal_iff (Localization.AtPrime q) q, this]
    simp

Goal state after:
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDedekindDomain S
inst✝ : Free ℤ S
a b : Ideal S
hI : Irreducible (absNorm (a * b))
⊢ IsUnit a ∨ IsUnit b

Tactic:
simpa only [Ideal.isUnit_iff, Nat.isUnit_iff, absNorm_eq_one_iff] using
        hI.isUnit_or_isUnit (map_mul absNorm a b)

Goal state after:
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: case h₂
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
p : ℤ
hp : Prime p
this✝ : IsAddTorsionFree S
this : CharZero S
hpMax : (span {p}).IsMaximal
hI' : IsUnit ⊤
hI : p ∣ ↑(absNorm ⊤)
⊢ ∃ P, P.IsMaximal ∧ under ℤ P = span {p} ∧ P ∣ ⊤

Tactic:
cases hp.not_dvd_one (by simpa using hI)

Goal state after:
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: case inr
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : JacobsonSpace X
S : Set X
hS : IsLocallyClosed S
hf₁ : Continuous[inst✝², inst✝¹] f
hf₂ : IsClosedMap f
hfS : (f '' S).Finite
hS'' : S.Nonempty
hS' : IsIrreducible S
H₁ : IsIrreducible (S ∩ closedPoints X)
H₂ : f '' (S ∩ closedPoints X) ⊆ closedPoints Y
H₃ : (f '' (S ∩ closedPoints X)).Subsingleton
x : Y
hx : x ∈ f '' (S ∩ closedPoints X)
⊢ IsClosed[inst✝¹] (f '' (S ∩ closedPoints X))

Tactic:
rw [H₃.eq_singleton_of_mem hx]; exact H₂ hx

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

Goal state before:
pp: S : Type u_1
inst✝³ : CommRing S
q : Ideal S
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Algebra R S
hq : q.IsPrime
inst✝ : Module.Finite R S
⊢ 0 < q.inertiaDeg R

Tactic:
by
  let := Localization.AtPrime.algebraOfLiesOver (q.under R) q
  rw [inertiaDeg_def]
  apply Module.finrank_pos

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

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✝¹⁶ : q.LiesOver p
inst✝¹⁵ : p.IsPrime
inst✝¹⁴ : q.IsPrime
K : Type u_4
L : Type u_5
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : Algebra (R ⧸ p) K
inst✝¹⁰ : IsFractionRing (R ⧸ p) K
inst✝⁹ : Algebra (S ⧸ q) L
inst✝⁸ : IsFractionRing (S ⧸ q) L
inst✝⁷ : Algebra R K
inst✝⁶ : IsScalarTower R (R ⧸ p) K
inst✝⁵ : Algebra S L
inst✝⁴ : IsScalarTower S (S ⧸ q) L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R S L
inst✝¹ : Algebra K L
inst✝ : IsScalarTower R K L
⊢ q.inertiaDeg R = Module.finrank K L

Tactic:
let := Localization.AtPrime.algebraOfLiesOver p q

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✝¹⁶ : q.LiesOver p
inst✝¹⁵ : p.IsPrime
inst✝¹⁴ : q.IsPrime
K : Type u_4
L : Type u_5
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : Algebra (R ⧸ p) K
inst✝¹⁰ : IsFractionRing (R ⧸ p) K
inst✝⁹ : Algebra (S ⧸ q) L
inst✝⁸ : IsFractionRing (S ⧸ q) L
inst✝⁷ : Algebra R K
inst✝⁶ : IsScalarTower R (R ⧸ p) K
inst✝⁵ : Algebra S L
inst✝⁴ : IsScalarTower S (S ⧸ q) L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R S L
inst✝¹ : Algebra K L
inst✝ : IsScalarTower R K L
this : Algebra (Localization.AtPrime p) (Localization.AtPrime q) := Localization.AtPrime.algebraOfLiesOver p q
⊢ q.inertiaDeg R = Module.finrank K L
Module: Mathlib.RingTheory.RamificationInertia.Inertia

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
⊢ (g • q).inertiaDeg R = q.inertiaDeg R

Tactic:
let := Localization.AtPrime.algebraOfLiesOver p q

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
this : Algebra (Localization.AtPrime p) (Localization.AtPrime q) := Localization.AtPrime.algebraOfLiesOver p q
⊢ (g • q).inertiaDeg R = q.inertiaDeg R
Module: Mathlib.RingTheory.RamificationInertia.Inertia

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
this✝ : Algebra (Localization.AtPrime p) (Localization.AtPrime q) := Localization.AtPrime.algebraOfLiesOver p q
this : Algebra (Localization.AtPrime p) (Localization.AtPrime (g • q)) :=
  Localization.AtPrime.algebraOfLiesOver p (g • q)
⊢ Module.finrank p.ResidueField (g • q).ResidueField = Module.finrank p.ResidueField q.ResidueField

Tactic:
let e₂ := Ideal.residueFieldAlgEquiv' p (g • q) q f₀.symm (comap_symm f₀.toRingEquiv).symm

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
this✝ : Algebra (Localization.AtPrime p) (Localization.AtPrime q) := Localization.AtPrime.algebraOfLiesOver p q
this : Algebra (Localization.AtPrime p) (Localization.AtPrime (g • q)) :=
  Localization.AtPrime.algebraOfLiesOver p (g • q)
e₂ : (g • q).ResidueField ≃ₐ[p.ResidueField] q.ResidueField := p.residueFieldAlgEquiv' (g • q) q f₀.symm ⋯
⊢ Module.finrank p.ResidueField (g • q).ResidueField = Module.finrank p.ResidueField q.ResidueField
Module: Mathlib.NumberTheory.RamificationInertia.Ramification

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
inst✝¹ : IsDedekindDomain S
inst✝ : IsDedekindDomain T
p : Ideal R
P : Ideal S
Q : Ideal T
hpm : P.IsPrime
hqm : Q.IsPrime
hg0 : map (algebraMap S T) P ≠ ⊥
hfg : map (algebraMap R T) p ≠ ⊥
hg : map (algebraMap S T) P ≤ Q
hf0 : map f p ≠ ⊥
hp0 : P ≠ ⊥
hq0 : Q ≠ ⊥
this : P.IsMaximal := Ring.DimensionLEOne.maximalOfPrime hp0 hpm
I : Ideal S
hcp✝ : P ⊔ I = ⊤
heq : map f p = P ^ Multiset.count P (normalizedFactors (map f p)) * I
hntq : ¬⊤ ≤ Q
h : map (algebraMap S T) I = 0
hcp : ⊤ = map (algebraMap S T) P
⊢ False

Tactic:
exact hntq (hcp.trans_le hg)

Goal state after:
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 A
inst✝² : FormallyUnramified A B
C : Type u_3
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[R] C
e : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂
⊢ ((Ideal.Quotient.mkₐ R I).comp f₁).comp (IsScalarTower.toAlgHom R A B) =
    (Ideal.Quotient.mkₐ R I).comp (f₂.comp (IsScalarTower.toAlgHom R A B))

Tactic:
e,

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 A
inst✝² : FormallyUnramified A B
C : Type u_3
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[R] C
e : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂
⊢ ((Ideal.Quotient.mkₐ R I).comp f₂).comp (IsScalarTower.toAlgHom R A B) =
    (Ideal.Quotient.mkₐ R I).comp (f₂.comp (IsScalarTower.toAlgHom R A B))
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : EssFiniteType R S
inst✝ : FormallyUnramified R S
⊢ ∃ T x x_1, Nonempty (S ⊗[R] S ≃ₐ[S] S × T)

Tactic:
obtain ⟨e, he, hsp⟩ : ∃ e, IsIdempotentElem e ∧ KaehlerDifferential.ideal R S = S ⊗[R] S ∙ e :=
    (Ideal.isIdempotentElem_iff_of_fg _ (KaehlerDifferential.ideal_fg R S)).mp <|
      (Ideal.cotangent_subsingleton_iff _).mp <| inferInstanceAs <| Subsingleton Ω[S⁄R]
  let e₁ := AlgEquiv.prodQuotientOfIsIdempotentElem (R := S) he he.one_sub (by simp) (by simp [he])
  let e₂ : (S ⊗[R] S ⧸ Ideal.span {e}) ≃ₐ[S] S :=
    ((Ideal.span {e}).quotientEquivAlgOfEq S hsp.symm).trans <|
      Ideal.quotientKerAlgEquivOfSurjective <|
        (⟨· ⊗ₜ 1, by simp [Algebra.TensorProduct.lmul'']⟩)
  exact ⟨(S ⊗[R] S) ⧸ Ideal.span {1 - e}, inferInstance, inferInstance,
    ⟨e₁.trans (.prodCongr e₂ .refl)⟩⟩

Goal state after:
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✝ : EssFiniteType R S
this : ∀ (t : S ⊗[R] S), (TensorProduct.lmul' R) t = 1 ↔ 1 - t ∈ KaehlerDifferential.ideal R S
t e : S ⊗[R] S
ht₁ : ∀ (s : S), (1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) * (1 - e) = 0
ht₂ : e ∈ Ideal.span (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)
⊢ Ideal.span (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) ≤ (S ⊗[R] S ∙ (1 - e)).annihilator

Tactic:
simpa only [Ideal.span_le, Set.range_subset_iff,
        Submodule.mem_annihilator_span_singleton, SetLike.mem_coe]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
p : Ideal S
inst✝⁴ : p.IsPrime
inst✝³ : QuasiFiniteAt R p
A : Type u_4
inst✝² : CommRing A
inst✝¹ : Algebra R A
q : Ideal (A ⊗[R] S)
inst✝ : q.IsPrime
hq : p = Ideal.comap TensorProduct.includeRight.toRingHom q
f : A ⊗[R] Localization.AtPrime p →ₐ[A] Localization.AtPrime q :=
  TensorProduct.lift (ofId A (Localization.AtPrime q))
    { toRingHom := Localization.localRingHom p q TensorProduct.includeRight.toRingHom hq, commutes' := ⋯ } ⋯
g : A ⊗[R] S →ₐ[A] A ⊗[R] Localization.AtPrime p :=
  TensorProduct.map (AlgHom.id A A) (IsScalarTower.toAlgHom R S (Localization.AtPrime p))
this : ∀ (x : A ⊗[R] S), f (g x) = (algebraMap (A ⊗[R] S) (Localization.AtPrime q)) x
x s : A ⊗[R] S
hs : s ∈ q.primeCompl
⊢ IsLocalization.mk' (Localization.AtPrime q) x ⟨s, hs⟩ * (algebraMap (A ⊗[R] S) (Localization.AtPrime q)) s ∈ f.range

Tactic:
IsLocalization.mk'_spec_mk

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
p : Ideal S
inst✝⁴ : p.IsPrime
inst✝³ : QuasiFiniteAt R p
A : Type u_4
inst✝² : CommRing A
inst✝¹ : Algebra R A
q : Ideal (A ⊗[R] S)
inst✝ : q.IsPrime
hq : p = Ideal.comap TensorProduct.includeRight.toRingHom q
f : A ⊗[R] Localization.AtPrime p →ₐ[A] Localization.AtPrime q :=
  TensorProduct.lift (ofId A (Localization.AtPrime q))
    { toRingHom := Localization.localRingHom p q TensorProduct.includeRight.toRingHom hq, commutes' := ⋯ } ⋯
g : A ⊗[R] S →ₐ[A] A ⊗[R] Localization.AtPrime p :=
  TensorProduct.map (AlgHom.id A A) (IsScalarTower.toAlgHom R S (Localization.AtPrime p))
this : ∀ (x : A ⊗[R] S), f (g x) = (algebraMap (A ⊗[R] S) (Localization.AtPrime q)) x
x s : A ⊗[R] S
hs : s ∈ q.primeCompl
⊢ (algebraMap (A ⊗[R] S) (Localization.AtPrime q)) x ∈ f.range
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: case monomial
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₁
Q : Generators S T ι
y : Q.Ring
n : ι →₀ ℕ
r : S
⊢ (δAux R Q) ((monomial n) r * y) = (monomial n) r • (δAux R Q) y + y • (δAux R Q) ((monomial n) r)

Tactic:
| monomial n r =>

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)
x : L
a✝ : x ∈ ⊤
n : ℕ
hn : x ^ ringExpChar K ^ n ∈ (algebraMap K L).range
this✝ : ExpChar (L ⊗[K] L) (ringExpChar K)
this : (1 ⊗ₜ[K] x - x ⊗ₜ[K] 1) ^ ringExpChar K ^ n = 0
H : 1 ⊗ₜ[K] x = x ⊗ₜ[K] 1
a : K
e : (algebraMap K L) a + 0 = 0
hab : a = 0 → ¬0 = 0
⊢ False

Tactic:
add_zero,

Goal state after:
K : Type u_1
L : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FormallyUnramified K L
inst✝¹ : EssFiniteType K L
inst✝ : IsPurelyInseparable K L
this✝¹ : Nontrivial (L ⊗[K] L)
x : L
a✝ : x ∈ ⊤
n : ℕ
hn : x ^ ringExpChar K ^ n ∈ (algebraMap K L).range
this✝ : ExpChar (L ⊗[K] L) (ringExpChar K)
this : (1 ⊗ₜ[K] x - x ⊗ₜ[K] 1) ^ ringExpChar K ^ n = 0
H : 1 ⊗ₜ[K] x = x ⊗ₜ[K] 1
a : K
e : (algebraMap K L) a = 0
hab : a = 0 → ¬0 = 0
⊢ False
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))
this✝¹ : Algebra P.Ring T := ((algebraMap S T).comp (algebraMap P.Ring S)).toAlgebra
this✝ : IsScalarTower P.Ring S T
this : IsScalarTower P.Ring Q.Ring T
e : Q.Ring ⊗[P.Ring] ↥P.ker ≃ₗ[Q.Ring] ↥Q.ker :=
  LinearEquiv.ofBijective (LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) H
f' : ↥Q.ker →ₗ[Q.Ring] T ⊗[S] P.Cotangent :=
  LinearMap.liftBaseChange Q.Ring (↑P.Ring ((TensorProduct.mk S T P.Cotangent) 1) ∘ₗ Cotangent.mk) ∘ₗ ↑e.symm
x : Q.Ring ⊗[P.Ring] ↥P.ker
ha : ↑(e x) ∈ Q.ker
hx : e x = ⟨↑(e x), ha⟩
y : Q.Ring ⊗[P.Ring] ↥P.ker
⊢ ↑(e x) • e y ∈ (↑f').ker

Tactic:
simp only [AddMonoidHom.mem_ker, AddMonoidHom.coe_coe, map_smul,
      LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
      LinearEquiv.symm_apply_apply, f']

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))
this✝¹ : Algebra P.Ring T := ((algebraMap S T).comp (algebraMap P.Ring S)).toAlgebra
this✝ : IsScalarTower P.Ring S T
this : IsScalarTower P.Ring Q.Ring T
e : Q.Ring ⊗[P.Ring] ↥P.ker ≃ₗ[Q.Ring] ↥Q.ker :=
  LinearEquiv.ofBijective (LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) H
f' : ↥Q.ker →ₗ[Q.Ring] T ⊗[S] P.Cotangent :=
  LinearMap.liftBaseChange Q.Ring (↑P.Ring ((TensorProduct.mk S T P.Cotangent) 1) ∘ₗ Cotangent.mk) ∘ₗ ↑e.symm
x : Q.Ring ⊗[P.Ring] ↥P.ker
ha : ↑(e x) ∈ Q.ker
hx : e x = ⟨↑(e x), ha⟩
y : Q.Ring ⊗[P.Ring] ↥P.ker
⊢ ↑(e x) • (LinearMap.liftBaseChange Q.Ring (↑P.Ring ((TensorProduct.mk S T P.Cotangent) 1) ∘ₗ Cotangent.mk)) y = 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
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
y : ↥P.ker
this✝¹ : Algebra P.Ring T := ⋯
this✝ : IsScalarTower P.Ring S T
this : IsScalarTower P.Ring Q.Ring T
e : Q.Ring ⊗[P.Ring] ↥P.ker ≃ₗ[Q.Ring] ↥Q.ker := ⋯
⊢ (tensorCotangentInvFun f halg H) (x • Cotangent.mk ⟨f.toRingHom ↑y, ⋯⟩) =
    (tensorCotangentInvFun f halg H) (Cotangent.mk ((LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) (x ⊗ₜ[P.Ring] y)))

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
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
y : ↥P.ker
this✝¹ : Algebra P.Ring T := ⋯
this✝ : IsScalarTower P.Ring S T
this : IsScalarTower P.Ring Q.Ring T
e : Q.Ring ⊗[P.Ring] ↥P.ker ≃ₗ[Q.Ring] ↥Q.ker := ⋯
⊢ (tensorCotangentInvFun f halg H) (Cotangent.mk ((LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) (x ⊗ₜ[P.Ring] y))) =
    x • 1 ⊗ₜ[S] Cotangent.mk y

Tactic:
· simp; rfl

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
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
y : ↥P.ker
this✝¹ : Algebra P.Ring T := ⋯
this✝ : IsScalarTower P.Ring S T
this : IsScalarTower P.Ring Q.Ring T
e : Q.Ring ⊗[P.Ring] ↥P.ker ≃ₗ[Q.Ring] ↥Q.ker := ⋯
⊢ (tensorCotangentInvFun f halg H) (Cotangent.mk ((LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) (x ⊗ₜ[P.Ring] y))) =
    x • 1 ⊗ₜ[S] Cotangent.mk y