mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.DedekindDomain.IntegralClosure

Goal state before:
pp: A : Type u_1
K : Type u_2
inst✝¹⁷ : CommRing A
inst✝¹⁶ : Field K
inst✝¹⁵ : Algebra A K
inst✝¹⁴ : IsFractionRing A K
L : Type u_3
inst✝¹³ : Field L
C : Type u_4
inst✝¹² : CommRing C
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : Algebra C L
inst✝⁷ : IsIntegralClosure C A L
inst✝⁶ : Algebra A C
inst✝⁵ : IsScalarTower A C L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsDomain A
inst✝² : Algebra.IsSeparable K L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsNoetherianRing A
this✝ : DecidableEq L
s : Finset L
b : Basis (↥s) K L
hb_int : ∀ (x : ↥s), IsIntegral A (b x)
b' : Basis (↥s) K L := (traceForm K L).dualBasis ⋯ b
this : IsNoetherian A ↥(Submodule.span A (Set.range ⇑b')) := isNoetherian_span_of_finite A (Set.finite_range ⇑b')
⊢ IsNoetherian A C

Tactic:
let f : C →ₗ[A] Submodule.span A (Set.range b') :=
    (Submodule.inclusion (IsIntegralClosure.range_le_span_dualBasis C b hb_int)).comp
      ((Algebra.linearMap C L).restrictScalars A).rangeRestrict

Goal state after:
A : Type u_1
K : Type u_2
inst✝¹⁷ : CommRing A
inst✝¹⁶ : Field K
inst✝¹⁵ : Algebra A K
inst✝¹⁴ : IsFractionRing A K
L : Type u_3
inst✝¹³ : Field L
C : Type u_4
inst✝¹² : CommRing C
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : Algebra C L
inst✝⁷ : IsIntegralClosure C A L
inst✝⁶ : Algebra A C
inst✝⁵ : IsScalarTower A C L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsDomain A
inst✝² : Algebra.IsSeparable K L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsNoetherianRing A
this✝ : DecidableEq L
s : Finset L
b : Basis (↥s) K L
hb_int : ∀ (x : ↥s), IsIntegral A (b x)
b' : Basis (↥s) K L := (traceForm K L).dualBasis ⋯ b
this : IsNoetherian A ↥(Submodule.span A (Set.range ⇑b')) := isNoetherian_span_of_finite A (Set.finite_range ⇑b')
f : C →ₗ[A] ↥(Submodule.span A (Set.range ⇑b')) := Submodule.inclusion ⋯ ∘ₗ (↑A (Algebra.linearMap C L)).rangeRestrict
⊢ IsNoetherian A C
Module: Mathlib.RingTheory.IsGaloisGroup.Basic

Goal state before:
pp: case refine_1
G : Type u_1
A : Type u_2
B : Type u_3
K : Type u_4
L : Type u_5
inst✝¹⁸ : Group G
inst✝¹⁷ : CommRing A
inst✝¹⁶ : CommRing B
inst✝¹⁵ : MulSemiringAction G B
inst✝¹⁴ : Algebra A B
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A K
inst✝⁹ : Algebra B L
inst✝⁸ : Algebra A L
inst✝⁷ : IsFractionRing A K
inst✝⁶ : IsFractionRing B L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : IsScalarTower A B L
inst✝³ : MulSemiringAction G L
inst✝² : SMulDistribClass G B L
hGKL : IsGaloisGroup G K L
inst✝¹ : IsIntegrallyClosed A
inst✝ : Algebra.IsIntegral A B
hc : ∀ (a : A), (algebraMap K L) ((algebraMap A K) a) = (algebraMap B L) ((algebraMap A B) a)
m₁✝ m₂✝ : G
h : ∀ (a : B), m₁✝ • a = m₂✝ • a
⊢ m₁✝ = m₂✝

Tactic:
have := hGKL.faithful
    refine eq_of_smul_eq_smul fun (y : L) ↦ ?_
    obtain ⟨a, b, hb, rfl⟩ := IsFractionRing.div_surjective B y
    simp only [smul_div₀', ← algebraMap.coe_smul', h]

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

Goal state before:
pp: G : Type u_1
inst✝⁹ : Group G
B : Type u_3
C : Type u_4
inst✝⁸ : Semiring C
inst✝⁷ : MulSemiringAction G C
N : Subgroup G
inst✝⁶ : CommSemiring B
inst✝⁵ : Algebra B C
inst✝⁴ : FaithfulSMul B C
inst✝³ : MulSemiringAction G B
inst✝² : SMulDistribClass G B C
inst✝¹ : IsGaloisGroup (↥N) B C
inst✝ : N.Normal
g : G
b : B
⊢ ↑g • b = g • b

Tactic:
by
  let := mulSemiringActionOfNormal G B C N
  refine (Quotient.liftOn'_mk'' (· • b) _ g).trans (FaithfulSMul.algebraMap_injective B C ?_)
  rw [algebraMap.smul', algebraMap.smul']

Goal state after:
Module: Mathlib.Data.Nat.Prime.Int

Goal state before:
pp: p : ℕ
hp : Prime p
a b : ℤ
h : ↑p ∣ ↑(a * b).natAbs
⊢ ↑p ∣ a ∨ ↑p ∣ b

Tactic:
Int.natCast_dvd_natCast,

Goal state after:
p : ℕ
hp : Prime p
a b : ℤ
h : p ∣ (a * b).natAbs
⊢ ↑p ∣ a ∨ ↑p ∣ b
Module: Mathlib.Data.Nat.Prime.Int

Goal state before:
pp: p : ℕ
hp : Prime p
a b : ℤ
h : p ∣ a.natAbs ∨ p ∣ b.natAbs
⊢ ↑p ∣ ↑a.natAbs ∨ ↑p ∣ b

Tactic:
Int.natCast_dvd_natCast,

Goal state after:
p : ℕ
hp : Prime p
a b : ℤ
h : p ∣ a.natAbs ∨ p ∣ b.natAbs
⊢ p ∣ a.natAbs ∨ ↑p ∣ b
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case pos
k n : ℕ
h✝¹ : k = n + 1
x : ZMod (namedPattern k (n + 1) h✝¹)
h✝ : x.val ≤ namedPattern k (n + 1) h✝¹ / 2
⊢ ↑↑x.val = x

Tactic:
rw [Int.cast_natCast, natCast_zmod_val]

Goal state after:
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case h2
n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
⊢ |x.valMinAbs - y| * |2| < ↑n * 2

Tactic:
rw [← abs_mul, sub_mul, abs_lt]

Goal state after:
case h2
n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
⊢ -(↑n * 2) < x.valMinAbs * 2 - y * 2 ∧ x.valMinAbs * 2 - y * 2 < ↑n * 2
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ ↑a.valMinAbs.natAbs = if a.val ≤ n / 2 then a else -a

Tactic:
have : (a.val : ℤ) - n ≤ 0 := by
    rw [sub_nonpos, Int.ofNat_le]
    exact a.val_le

Goal state after:
n : ℕ
inst✝ : NeZero n
a : ZMod n
this : ↑a.val - ↑n ≤ 0
⊢ ↑a.valMinAbs.natAbs = if a.val ≤ n / 2 then a else -a
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: case neg.succ.hnc
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : ¬Algebra.IsSeparable K L
p : ℕ
hp : ExpChar K p
this : p ≠ 0
x : L
h₀ : FiniteDimensional K L
hx : ¬IsSeparable K x
g : K[X]
hg₁ : g.Separable
n : ℕ
hg₂ : (expand K (p ^ (n + 1))) g = minpoly K x
⊢ ¬(minpoly K x).natDegree = 0

Tactic:
exact (minpoly.natDegree_pos (IsIntegral.isIntegral x)).ne'

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

Goal state before:
pp: case refine_2
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
this : FiniteDimensional K L
e : Fin pb.dim ≃ (L →ₐ[K] AlgebraicClosure L) := (Fintype.equivFinOfCardEq ?refine_1).symm
⊢ (vandermonde fun i ↦ (e i) pb.gen).det * (vandermonde fun i ↦ (e i) pb.gen)ᵀᵀ.det ≠ 0

Tactic:
refine mt mul_self_eq_zero.mp ?_

Goal state after:
case refine_2
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
this : FiniteDimensional K L
e : Fin pb.dim ≃ (L →ₐ[K] AlgebraicClosure L) := (Fintype.equivFinOfCardEq ?refine_1).symm
⊢ ¬(vandermonde fun i ↦ (e i) pb.gen).det = 0
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
h : i < q - 1
hi : i = 0
⊢ ∑ x, x ^ i = 0

Tactic:
simp only [hi, nsmul_one, sum_const, pow_zero, card_univ, cast_card_eq_zero]

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

Goal state before:
pp: case e'_4
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
aux : X ^ q - X ≠ 0
this : (X ^ q - X).roots.toFinset = univ
⊢ C 0 * X ^ (q - 1) - 1 = -1

Tactic:
C_0,

Goal state after:
case e'_4
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
aux : X ^ q - X ≠ 0
this : (X ^ q - X).roots.toFinset = univ
⊢ 0 * X ^ (q - 1) - 1 = -1
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case pos
p x y : ℕ
hp : Nat.Prime p
h : (p - 1) * ((x - y) / (p - 1)) = x - y
hxy : y ≤ x
hy : 0 < y
n : ℤ
hn : n ≡ 0 [ZMOD ↑p]
⊢ n ^ x ≡ n ^ y [ZMOD ↑p]

pp: case neg
p x y : ℕ
hp : Nat.Prime p
h : (p - 1) * ((x - y) / (p - 1)) = x - y
hxy : y ≤ x
hy : 0 < y
n : ℤ
hn : ¬n ≡ 0 [ZMOD ↑p]
⊢ n ^ x ≡ n ^ y [ZMOD ↑p]

Tactic:
· grw [hn, zero_pow (hy.trans_le hxy).ne', zero_pow hy.ne']

Goal state after:
case neg
p x y : ℕ
hp : Nat.Prime p
h : (p - 1) * ((x - y) / (p - 1)) = x - y
hxy : y ≤ x
hy : 0 < y
n : ℤ
hn : ¬n ≡ 0 [ZMOD ↑p]
⊢ n ^ x ≡ n ^ y [ZMOD ↑p]
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
⊢ Units.mk0 a ha ^ (Fintype.card F / 2) = 1 ↔ a ^ (Fintype.card F / 2) = 1

Tactic:
by simp [Units.ext_iff]

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient

Goal state before:
pp: E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Module ℚ E
L₁ L₂ : AddSubgroup E
H : L₁ ≤ L₂
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b₁ b₂ : Basis ι ℚ E
h₁ : L₁ = closure (Set.range ⇑b₁)
h₂ : L₂ = closure (Set.range ⇑b₂)
⊢ ↑((Basis.addSubgroupOfClosure L₂ b₂ h₂).det fun i ↦ ⟨↑((Basis.addSubgroupOfClosure L₁ b₁ h₁) i), ⋯⟩).natAbs =
    |b₂.det ⇑b₁|

Tactic:
Nat.cast_natAbs,

Goal state after:
E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Module ℚ E
L₁ L₂ : AddSubgroup E
H : L₁ ≤ L₂
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b₁ b₂ : Basis ι ℚ E
h₁ : L₁ = closure (Set.range ⇑b₁)
h₂ : L₂ = closure (Set.range ⇑b₂)
⊢ ↑|(Basis.addSubgroupOfClosure L₂ b₂ h₂).det fun i ↦ ⟨↑((Basis.addSubgroupOfClosure L₁ b₁ h₁) i), ⋯⟩| = |b₂.det ⇑b₁|
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
P : Ideal S
T : Type u_2
inst✝⁷ : CommRing T
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra S T
inst✝⁴ : IsScalarTower R S T
inst✝³ : Module.Finite R T
Q : Ideal T
inst✝² : P.LiesOver p
inst✝¹ : Q.LiesOver P
inst✝ : p.IsPrime
this : Q.LiesOver p
⊢ finrank (S ⧸ P) (T ⧸ Q) ≤ finrank (R ⧸ p) (T ⧸ Q)

Tactic:
have : IsScalarTower (R ⧸ p) (S ⧸ P) (T ⧸ Q) := IsScalarTower.of_algebraMap_eq <| by
    rintro ⟨x⟩
    simp [Submodule.Quotient.quot_mk_eq_mk, IsScalarTower.algebraMap_apply R (S ⧸ P) (T ⧸ Q)]

Goal state after:
R : Type u
inst✝¹⁰ : CommRing R
S : Type v
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
p : Ideal R
P : Ideal S
T : Type u_2
inst✝⁷ : CommRing T
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra S T
inst✝⁴ : IsScalarTower R S T
inst✝³ : Module.Finite R T
Q : Ideal T
inst✝² : P.LiesOver p
inst✝¹ : Q.LiesOver P
inst✝ : p.IsPrime
this✝ : Q.LiesOver p
this : IsScalarTower (R ⧸ p) (S ⧸ P) (T ⧸ Q)
⊢ finrank (S ⧸ P) (T ⧸ Q) ≤ finrank (R ⧸ p) (T ⧸ Q)
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝¹ : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst✝ : IsDedekindDomain S
hP : P ≠ ⊥
i : ℕ
ih : cardQuot (P ^ i) = cardQuot P ^ i
this : P ^ (i + 1) < P ^ i
hquot : ↥(map (mkQ (P ^ i.succ)) (P ^ i)) ≃ S ⧸ P
⊢ cardQuot (P ^ (i + 1)) = cardQuot P ^ (i + 1)

Tactic:
by
    rw [pow_succ' (cardQuot P), ← ih, cardQuot_apply (P ^ i.succ), ←
      card_quotient_mul_card_quotient (P ^ i) (P ^ i.succ) this.le, cardQuot_apply (P ^ i),
      cardQuot_apply P, Nat.card_congr hquot]

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
I : Ideal S
⊢ ↑(cardQuot I) ∈ I

Tactic:
cardQuot,

Goal state after:
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDedekindDomain S
inst✝ : Free ℤ S
I : Ideal S
⊢ ↑(toAddSubgroup I).index ∈ I
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: case h₃.inl
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
I P : Ideal S
hI' : I ≠ 0
hP : Prime P
IH : p ∣ ↑(absNorm I) → ∃ P, P.IsMaximal ∧ under ℤ P = span {p} ∧ P ∣ I
this : P.IsMaximal
q n : ℕ
hn : 0 < n
hqP : ↑q ∈ P
hq : Nat.Prime q
H : absNorm P = q ^ n
m : ℕ
hmn : m ≤ n
hp : Associated p (↑q ^ m)
⊢ span {p} ≤ under ℤ P

Tactic:
rw [Ideal.span_singleton_le_iff_mem]

Goal state after:
case h₃.inl
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
I P : Ideal S
hI' : I ≠ 0
hP : Prime P
IH : p ∣ ↑(absNorm I) → ∃ P, P.IsMaximal ∧ under ℤ P = span {p} ∧ P ∣ I
this : P.IsMaximal
q n : ℕ
hn : 0 < n
hqP : ↑q ∈ P
hq : Nat.Prime q
H : absNorm P = q ^ n
m : ℕ
hmn : m ≤ n
hp : Associated p (↑q ^ m)
⊢ p ∈ under ℤ P
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: X : Type u_2
Y : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : JacobsonSpace Y
hf : IsOpenEmbedding f
⊢ ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ closedPoints X).Nonempty

Tactic:
← hf.preimage_closedPoints

Goal state after:
X : Type u_2
Y : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : JacobsonSpace Y
hf : IsOpenEmbedding f
⊢ ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ f ⁻¹' closedPoints Y).Nonempty
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: X : Type u_2
Y : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : JacobsonSpace Y
hf : IsClosedEmbedding f
⊢ ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ closedPoints X).Nonempty

Tactic:
← hf.preimage_closedPoints

Goal state after:
X : Type u_2
Y : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : JacobsonSpace Y
hf : IsClosedEmbedding f
⊢ ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ f ⁻¹' closedPoints Y).Nonempty
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: X : Type u_2
Y : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : JacobsonSpace Y
hf : IsClosedEmbedding f
⊢ JacobsonSpace X

Tactic:
rw [jacobsonSpace_iff_locallyClosed, ← hf.preimage_closedPoints]
  intro Z hZ hZ'
  obtain ⟨_, ⟨x, hx, rfl⟩, hx'⟩ := nonempty_inter_closedPoints
    (hZ.image f) (hZ'.image hf.isInducing hf.isClosed_range.isLocallyClosed)
  exact ⟨_, hx, hx'⟩

Goal state after:
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_1
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), JacobsonSpace ↥(U i)
Z : Set X
hZ' : IsLocallyClosed Z
i : ι
x : X
hx : x ∈ Z
hx' : x ∈ ↑(U i)
y : ↥(U i)
hy : y ∈ Subtype.val ⁻¹' Z
hy' : y ∈ closedPoints ↥(U i)
j : ι
h : ↑y ∈ U j
⊢ Subtype.val ⁻¹' {↑y} = {⟨↑y, h⟩}

Tactic:
ext; simp [← Subtype.coe_inj]

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

Goal state before:
pp: R : Type v
inst✝⁶ : CommRing R
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
inst✝³ : Small.{w, u} A
H :
  ∀ ⦃B : Type w⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp
B : Type u
inst✝² : CommRing B
inst✝¹ : Small.{w, u} B
inst✝ : Algebra R B
I : Ideal B
hI : I ^ 2 = ⊥
f : A →ₐ[R] B
⊢ ∀ ⦃a₂ : A →ₐ[R] B⦄, (Ideal.Quotient.mkₐ R I).comp f = (Ideal.Quotient.mkₐ R I).comp a₂ → f = a₂

Tactic:
g

Goal state after:
R : Type v
inst✝⁶ : CommRing R
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
inst✝³ : Small.{w, u} A
H :
  ∀ ⦃B : Type w⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp
B : Type u
inst✝² : CommRing B
inst✝¹ : Small.{w, u} B
inst✝ : Algebra R B
I : Ideal B
hI : I ^ 2 = ⊥
f g : A →ₐ[R] B
⊢ (Ideal.Quotient.mkₐ R I).comp f = (Ideal.Quotient.mkₐ R I).comp g → f = g
Module: Mathlib.RingTheory.QuasiFinite.Basic

Goal state before:
pp: case h
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
inst✝ : QuasiFinite R S
P : Ideal S
hP : P.IsPrime
p : P.ResidueField
s : S
t : ↥M
⊢ (fun x ↦ x * TensorProduct.includeRight ((algebraMap S T) ↑t))
      ((↑S (Algebra.linearMap P.ResidueField (P.Fiber T))) (s • p / (algebraMap S P.ResidueField) ↑t)) =
    (fun x ↦ x * TensorProduct.includeRight ((algebraMap S T) ↑t)) (p ⊗ₜ[S] IsLocalization.mk' T s t)

Tactic:
by_cases ht : algebraMap _ P.ResidueField t.1 = 0

Goal state after:
case pos
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
inst✝ : QuasiFinite R S
P : Ideal S
hP : P.IsPrime
p : P.ResidueField
s : S
t : ↥M
ht : (algebraMap S P.ResidueField) ↑t = 0
⊢ (fun x ↦ x * TensorProduct.includeRight ((algebraMap S T) ↑t))
      ((↑S (Algebra.linearMap P.ResidueField (P.Fiber T))) (s • p / (algebraMap S P.ResidueField) ↑t)) =
    (fun x ↦ x * TensorProduct.includeRight ((algebraMap S T) ↑t)) (p ⊗ₜ[S] IsLocalization.mk' T s t)

case neg
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
inst✝ : QuasiFinite R S
P : Ideal S
hP : P.IsPrime
p : P.ResidueField
s : S
t : ↥M
ht : ¬(algebraMap S P.ResidueField) ↑t = 0
⊢ (fun x ↦ x * TensorProduct.includeRight ((algebraMap S T) ↑t))
      ((↑S (Algebra.linearMap P.ResidueField (P.Fiber T))) (s • p / (algebraMap S P.ResidueField) ↑t)) =
    (fun x ↦ x * TensorProduct.includeRight ((algebraMap S T) ↑t)) (p ⊗ₜ[S] IsLocalization.mk' T s t)
Module: Mathlib.RingTheory.Unramified.Finite

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FormallyUnramified R S
inst✝¹ : EssFiniteType R S
inst✝ : Free R S
I : Type u_2 := ⋯
b : Basis I R S := ⋯
f : I →₀ S
hf : elem R S = f.sum fun i x ↦ x ⊗ₜ[R] b i
x : S
a : I → I →₀ R := ⋯
F : I →₀ I →₀ R := ⋯
hG : ∀ j ∉ f.support.biUnion fun i ↦ (a i).support, b.repr (f.sum fun i y ↦ (a i) j • y) = 0
G : I →₀ I →₀ R := ⋯
this : ∀ (i : I), ((b.repr (x * f i)).sum fun j k ↦ k • b j ⊗ₜ[R] b i) = (x * f i) ⊗ₜ[R] b i
⊢ x ⊗ₜ[R] 1 * elem R S =
    ∑ a_1 ∈ f.support.biUnion fun i ↦ (a i).support,
      (b.repr (f.sum fun i y ↦ (a i) a_1 • y)).sum fun b' c ↦ c • b b' ⊗ₜ[R] b a_1

Tactic:
rw [← one_tmul_mul_elem, hf, finite_of_free_aux]
        rfl

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

Goal state before:
pp: case h₂
R : Type u
A : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
B✝ : Type u_1
inst✝³ : CommRing B✝
inst✝² : FormallySmooth R A
I✝ : Ideal B✝
hI : IsNilpotent I✝
B : Type u_1
inst✝¹ : CommRing B
I J : Ideal B
hIJ : I ≤ J
h₁ : ∀ [inst : Algebra R B], Function.Surjective (Ideal.Quotient.mkₐ R I).comp
h₂ : ∀ [inst : Algebra R (B ⧸ I)], Function.Surjective (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)).comp
inst✝ : Algebra R B
⊢ Function.Surjective (Ideal.Quotient.mkₐ R J).comp

Tactic:
g

Goal state after:
case h₂
R : Type u
A : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
B✝ : Type u_1
inst✝³ : CommRing B✝
inst✝² : FormallySmooth R A
I✝ : Ideal B✝
hI : IsNilpotent I✝
B : Type u_1
inst✝¹ : CommRing B
I J : Ideal B
hIJ : I ≤ J
h₁ : ∀ [inst : Algebra R B], Function.Surjective (Ideal.Quotient.mkₐ R I).comp
h₂ : ∀ [inst : Algebra R (B ⧸ I)], Function.Surjective (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)).comp
inst✝ : Algebra R B
g : A →ₐ[R] B ⧸ J
⊢ ∃ a, (Ideal.Quotient.mkₐ R J).comp a = g
Module: Mathlib.RingTheory.Smooth.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
H :
  ∀ ⦃B : Type (max u v)⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Surjective (Ideal.Quotient.mkₐ R I).comp
P : Generators R A A := Generators.self R A
f : P.Ring →ₐ[R] A := IsScalarTower.toAlgHom R P.Ring A
⊢ FormallySmooth R A

Tactic:
iff_split_surjection f P.algebraMap_surjective

Goal state after:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
H :
  ∀ ⦃B : Type (max u v)⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Surjective (Ideal.Quotient.mkₐ R I).comp
P : Generators R A A := Generators.self R A
f : P.Ring →ₐ[R] A := IsScalarTower.toAlgHom R P.Ring A
⊢ ∃ g, f.kerSquareLift.comp g = AlgHom.id R A
Module: Mathlib.RingTheory.Smooth.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
H :
  ∀ ⦃B : Type (max u v)⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Surjective (Ideal.Quotient.mkₐ R I).comp
P : Generators R A A := Generators.self R A
f : P.Ring →ₐ[R] A := IsScalarTower.toAlgHom R P.Ring A
surj : Function.Surjective ⇑f.kerSquareLift
sqz : RingHom.ker f.kerSquareLift ^ 2 = ⊥
g : A →ₐ[R] P.Ring ⧸ RingHom.ker f ^ 2
hg : (Ideal.Quotient.mkₐ R (RingHom.ker f.kerSquareLift)).comp g = ↑(Ideal.quotientKerAlgEquivOfSurjective surj).symm
x : A
⊢ f.kerSquareLift.kerLift (↑(Ideal.quotientKerAlgEquivOfSurjective surj).symm x) = (AlgHom.id R A) x

Tactic:
obtain ⟨x, rfl⟩ := (Ideal.quotientKerAlgEquivOfSurjective surj).surjective x

Goal state after:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
H :
  ∀ ⦃B : Type (max u v)⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Surjective (Ideal.Quotient.mkₐ R I).comp
P : Generators R A A := Generators.self R A
f : P.Ring →ₐ[R] A := IsScalarTower.toAlgHom R P.Ring A
surj : Function.Surjective ⇑f.kerSquareLift
sqz : RingHom.ker f.kerSquareLift ^ 2 = ⊥
g : A →ₐ[R] P.Ring ⧸ RingHom.ker f ^ 2
hg : (Ideal.Quotient.mkₐ R (RingHom.ker f.kerSquareLift)).comp g = ↑(Ideal.quotientKerAlgEquivOfSurjective surj).symm
x : (P.Ring ⧸ RingHom.ker f.toRingHom ^ 2) ⧸ RingHom.ker f.kerSquareLift
⊢ f.kerSquareLift.kerLift
      (↑(Ideal.quotientKerAlgEquivOfSurjective surj).symm ((Ideal.quotientKerAlgEquivOfSurjective surj) x)) =
    (AlgHom.id R A) ((Ideal.quotientKerAlgEquivOfSurjective surj) x)
Module: Mathlib.RingTheory.Smooth.Basic

Goal state before:
pp: case mp
R : Type u_4
inst✝² : CommRing R
A : Type u_6
inst✝¹ : CommRing A
inst✝ : Algebra R A
h : Function.Surjective ⇑(algebraMap R A)
g : A →ₐ[R] R ⧸ RingHom.ker (ofId R A).toRingHom ^ 2
hg : (ofId R A).kerSquareLift.comp g = AlgHom.id R A
e : A ≃ₐ[R] R ⧸ RingHom.ker (algebraMap R A) ^ 2 := AlgEquiv.ofAlgHom g (ofId R A).kerSquareLift ⋯ hg
⊢ RingHom.ker (algebraMap R A) ^ 2 = RingHom.ker (algebraMap R A)

Tactic:
← Ideal.mk_ker (I := _ ^ 2),

Goal state after:
case mp
R : Type u_4
inst✝² : CommRing R
A : Type u_6
inst✝¹ : CommRing A
inst✝ : Algebra R A
h : Function.Surjective ⇑(algebraMap R A)
g : A →ₐ[R] R ⧸ RingHom.ker (ofId R A).toRingHom ^ 2
hg : (ofId R A).kerSquareLift.comp g = AlgHom.id R A
e : A ≃ₐ[R] R ⧸ RingHom.ker (algebraMap R A) ^ 2 := AlgEquiv.ofAlgHom g (ofId R A).kerSquareLift ⋯ hg
⊢ RingHom.ker (Ideal.Quotient.mk (RingHom.ker (algebraMap R A) ^ 2)) = RingHom.ker (algebraMap R A)
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
this✝ : Module.Finite K A
this : IsArtinianRing A
hA : IsNilpotent (IsLocalRing.maximalIdeal A)
e : K ≃ₐ[K] A ⧸ IsLocalRing.maximalIdeal A :=
  let __spread.0 := ofId K (A ⧸ IsLocalRing.maximalIdeal A);
  let __spread.1 := Equiv.ofBijective ⇑(algebraMap K (A ⧸ IsLocalRing.maximalIdeal A)) ⋯;
  { toFun := (↑↑__spread.0.toRingHom).toFun, invFun := __spread.1.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯,
    map_add' := ⋯, commutes' := ⋯ }
e' : A ⊗[K] (A ⧸ IsLocalRing.maximalIdeal A) ≃ₐ[A] A :=
  (TensorProduct.congr AlgEquiv.refl e.symm).trans (TensorProduct.rid K A A)
f : A ⧸ IsLocalRing.maximalIdeal A →ₗ[A] A := e'.toLinearMap ∘ₗ sec K A (A ⧸ IsLocalRing.maximalIdeal A)
hf : (ofId A (A ⧸ IsLocalRing.maximalIdeal A)).toLinearMap ∘ₗ f = LinearMap.id
hf₁ : f 1 • 1 = 1
hf₂ : 1 - f 1 ∈ IsLocalRing.maximalIdeal A
⊢ IsIdempotentElem (1 - f 1)

Tactic:
apply IsIdempotentElem.one_sub

Goal state after:
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
this✝ : Module.Finite K A
this : IsArtinianRing A
hA : IsNilpotent (IsLocalRing.maximalIdeal A)
e : K ≃ₐ[K] A ⧸ IsLocalRing.maximalIdeal A := ⋯
e' : A ⊗[K] (A ⧸ IsLocalRing.maximalIdeal A) ≃ₐ[A] A := ⋯
f : A ⧸ IsLocalRing.maximalIdeal A →ₗ[A] A := ⋯
hf : (ofId A (A ⧸ IsLocalRing.maximalIdeal A)).toLinearMap ∘ₗ f = LinearMap.id
hf₁ : f 1 • 1 = 1
hf₂ : 1 - f 1 ∈ IsLocalRing.maximalIdeal A
⊢ IsIdempotentElem (f 1)