mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.Galois.IsGaloisGroup

Goal state before:
pp: G : Type u_1
K : Type u_3
L : Type u_4
inst✝⁸ : Group G
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
inst✝⁴ : MulSemiringAction G L
H : Subgroup G
F : IntermediateField K L
N : Subgroup G
inst✝³ : N.Normal
inst✝² : IsGaloisGroup (↥N) (↥F) L
E : IntermediateField K L
hE : IsGaloisGroup (↥H) (↥E) L
inst✝¹ : Finite G
inst✝ : IsGaloisGroup G K L
h : E ≤ F
this✝³ : Algebra ↥E ↥F := (IntermediateField.inclusion h).toAlgebra
this✝² : SMul G ↥F := smulOfNormal G (↥F) L N
this✝¹ : SMulDistribClass G (↥F) L
this✝ : MulSemiringAction G ↥F := mulSemiringActionOfSmulDistribClass (↥F) L G
this : IsScalarTower (↥E) (↥F) L
g : G
hg : g ∈ ↑H
x : ↥E
y : ↥F
⊢ ⟨(QuotientGroup.mk' N) g, ⋯⟩ • x • y = x • ⟨(QuotientGroup.mk' N) g, ⋯⟩ • y

Tactic:
apply FaithfulSMul.algebraMap_injective F L

Goal state after:
G : Type u_1
K : Type u_3
L : Type u_4
inst✝⁸ : Group G
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
inst✝⁴ : MulSemiringAction G L
H : Subgroup G
F : IntermediateField K L
N : Subgroup G
inst✝³ : N.Normal
inst✝² : IsGaloisGroup (↥N) (↥F) L
E : IntermediateField K L
hE : IsGaloisGroup (↥H) (↥E) L
inst✝¹ : Finite G
inst✝ : IsGaloisGroup G K L
h : E ≤ F
this✝³ : Algebra ↥E ↥F := ⋯
this✝² : SMul G ↥F := ⋯
this✝¹ : SMulDistribClass G (↥F) L
this✝ : MulSemiringAction G ↥F := ⋯
this : IsScalarTower (↥E) (↥F) L
g : G
hg : g ∈ ↑H
x : ↥E
y : ↥F
⊢ (algebraMap (↥F) L) (⟨(QuotientGroup.mk' N) g, ⋯⟩ • x • y) =
    (algebraMap (↥F) L) (x • ⟨(QuotientGroup.mk' N) g, ⋯⟩ • y)
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
⊢ a ^ (p - 1) = if a ≠ 0 then 1 else 0

Tactic:
by
  split_ifs with ha
  · exact pow_card_sub_one_eq_one ha
  · simp [of_not_not ha, (Fact.out : p.Prime).one_lt, tsub_eq_zero_iff_le]

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

Goal state before:
pp: p : ℕ
hp : Nat.Prime p
n : ℤ
⊢ n ^ p ≡ n [ZMOD ↑p]

Tactic:
have : Fact p.Prime := ⟨hp⟩
  simp [← ZMod.intCast_eq_intCast_iff]

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

Goal state before:
pp: case succ
p a m : ℕ
hm : (1 + p * a) ^ p ^ m ≡ 1 [MOD p ^ m]
⊢ (1 + p * a) ^ p ^ (m + 1) ≡ 1 [MOD p ^ (m + 1)]

Tactic:
rw [Nat.ModEq.comm, add_comm, Nat.modEq_iff_dvd' (Nat.one_le_pow' _ _)] at hm

Goal state after:
case succ
p a m : ℕ
hm : p ^ m ∣ (p * a + 1) ^ p ^ m - 1
⊢ (1 + p * a) ^ p ^ (m + 1) ≡ 1 [MOD p ^ (m + 1)]
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
n : ℕ+
hp : Nat.Prime (ringChar F)
h : Fintype.card F = ringChar F ^ ↑n
⊢ ringChar F = 2 ↔ Even (ringChar F) ∧ ↑n ≠ 0

Tactic:
hp.even_iff

Goal state after:
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
n : ℕ+
hp : Nat.Prime (ringChar F)
h : Fintype.card F = ringChar F ^ ↑n
⊢ ringChar F = 2 ↔ ringChar F = 2 ∧ ↑n ≠ 0
Module: Mathlib.RingTheory.Norm.Basic

Goal state before:
pp: case pos
K : Type u_4
L : Type u_5
F : Type u_6
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
inst✝¹ : Algebra K L
inst✝ : Algebra K F
x : L
hf : (Polynomial.map (algebraMap K F) (minpoly K x)).Splits
injKxL : Function.Injective ⇑(algebraMap (↥K⟮x⟯) L)
hx : IsIntegral K x
⊢ ((minpoly K (adjoin.powerBasis hx).gen).aroots F).prod = ((minpoly K x).aroots F).prod

Tactic:
rw [adjoin.powerBasis_gen hx, ← minpoly.algebraMap_eq injKxL]

Goal state after:
case pos
K : Type u_4
L : Type u_5
F : Type u_6
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
inst✝¹ : Algebra K L
inst✝ : Algebra K F
x : L
hf : (Polynomial.map (algebraMap K F) (minpoly K x)).Splits
injKxL : Function.Injective ⇑(algebraMap (↥K⟮x⟯) L)
hx : IsIntegral K x
⊢ ((minpoly K ((algebraMap (↥K⟮x⟯) L) (AdjoinSimple.gen K x))).aroots F).prod = ((minpoly K x).aroots F).prod
Module: Mathlib.RingTheory.Norm.Basic

Goal state before:
pp: case pos.hf
K : Type u_4
L : Type u_5
F : Type u_6
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
inst✝¹ : Algebra K L
inst✝ : Algebra K F
x : L
hf : (Polynomial.map (algebraMap K F) (minpoly K x)).Splits
injKxL : Function.Injective ⇑(algebraMap (↥K⟮x⟯) L)
hx : IsIntegral K x
⊢ (Polynomial.map (algebraMap K F) (minpoly K (adjoin.powerBasis hx).gen)).Splits

Tactic:
rw [adjoin.powerBasis_gen hx, ← minpoly.algebraMap_eq injKxL]

Goal state after:
case pos.hf
K : Type u_4
L : Type u_5
F : Type u_6
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
inst✝¹ : Algebra K L
inst✝ : Algebra K F
x : L
hf : (Polynomial.map (algebraMap K F) (minpoly K x)).Splits
injKxL : Function.Injective ⇑(algebraMap (↥K⟮x⟯) L)
hx : IsIntegral K x
⊢ (Polynomial.map (algebraMap K F) (minpoly K ((algebraMap (↥K⟮x⟯) L) (AdjoinSimple.gen K x)))).Splits
Module: Mathlib.RingTheory.FiniteStability

Goal state before:
pp: R : Type w₁
inst✝⁴ : CommRing R
A : Type w₂
inst✝³ : CommRing A
inst✝² : Algebra R A
B : Type w₃
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Function.Surjective ⇑f
g : B ⊗[R] MvPolynomial (Fin n) R →ₐ[B] B ⊗[R] A := TensorProduct.map (AlgHom.id B B) f
this : Function.Surjective ⇑g
⊢ ∃ n f, Function.Surjective ⇑f

Tactic:
use n, AlgHom.comp g (MvPolynomial.algebraTensorAlgEquiv R B).symm.toAlgHom

Goal state after:
case h
R : Type w₁
inst✝⁴ : CommRing R
A : Type w₂
inst✝³ : CommRing A
inst✝² : Algebra R A
B : Type w₃
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Function.Surjective ⇑f
g : B ⊗[R] MvPolynomial (Fin n) R →ₐ[B] B ⊗[R] A := ⋯
this : Function.Surjective ⇑g
⊢ Function.Surjective ⇑(g.comp ↑(MvPolynomial.algebraTensorAlgEquiv R B).symm)
Module: Mathlib.RingTheory.Finiteness.NilpotentKer

Goal state before:
pp: case e'_6
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✝ : Module.Finite R T
f : S →ₐ[R] T
hf₁ : Function.Surjective ⇑f
I : Ideal S
hI : RingHom.ker f = I
hf₂ : I ≤ nilradical S
hf₃ : I.FG
this✝ : Module.Finite R (S ⧸ I)
n : ℕ
IH : Module.Finite R (S ⧸ I ^ n)
φ : S ⧸ I ^ (n + 1) →ₐ[S] S ⧸ I ^ n := ⋯
hφ : Function.Surjective ⇑φ
hφ' : φ.toLinearMap ∘ₗ Submodule.mkQ (I ^ (n + 1)) = Submodule.mkQ (I ^ n)
this : Module.Finite R ((S ⧸ I) ⊗[S] ↥(I ^ n))
ψ : (S ⧸ I) ⊗[S] ↥(I ^ n) →ₗ[S] S ⧸ I ^ (n + 1) := ⋯
e_3✝ : inst✝⁵.toSemiring = CommRing.toCommSemiring.toSemiring
e_4✝ : (Submodule.Quotient.addCommGroup (I ^ (n + 1))).toAddCommMonoid = Submodule.Quotient.addCommMonoid (I ^ (n + 1))
e_5✝ : Submodule.Quotient.module' (I ^ (n + 1)) ≍ Submodule.Quotient.module' (I ^ (n + 1))
⊢ ⊤ ⊓ (↑R φ.toLinearMap).ker = Submodule.map (↑R ψ) ⊤

Tactic:
suffices LinearMap.ker φ.toLinearMap = Submodule.map (I ^ (n + 1)).mkQ (I ^ n) by
        simpa [LinearMap.range_restrictScalars, ψ, LinearMap.range_comp, Submodule.range_liftQ]

Goal state after:
case e'_6
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✝ : Module.Finite R T
f : S →ₐ[R] T
hf₁ : Function.Surjective ⇑f
I : Ideal S
hI : RingHom.ker f = I
hf₂ : I ≤ nilradical S
hf₃ : I.FG
this✝ : Module.Finite R (S ⧸ I)
n : ℕ
IH : Module.Finite R (S ⧸ I ^ n)
φ : S ⧸ I ^ (n + 1) →ₐ[S] S ⧸ I ^ n := Ideal.Quotient.factorₐ S ⋯
hφ : Function.Surjective ⇑φ
hφ' : φ.toLinearMap ∘ₗ Submodule.mkQ (I ^ (n + 1)) = Submodule.mkQ (I ^ n)
this : Module.Finite R ((S ⧸ I) ⊗[S] ↥(I ^ n))
ψ : (S ⧸ I) ⊗[S] ↥(I ^ n) →ₗ[S] S ⧸ I ^ (n + 1) :=
  (I • ⊤).liftQ (Submodule.mkQ (I ^ (n + 1)) ∘ₗ Submodule.subtype (I ^ n)) ⋯ ∘ₗ ↑(quotTensorEquivQuotSMul (↥(I ^ n)) I)
e_3✝ : inst✝⁵.toSemiring = CommRing.toCommSemiring.toSemiring
e_4✝ : (Submodule.Quotient.addCommGroup (I ^ (n + 1))).toAddCommMonoid = Submodule.Quotient.addCommMonoid (I ^ (n + 1))
e_5✝ : Submodule.Quotient.module' (I ^ (n + 1)) ≍ Submodule.Quotient.module' (I ^ (n + 1))
⊢ φ.toLinearMap.ker = Submodule.map (Submodule.mkQ (I ^ (n + 1))) (I ^ n)
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: case mp
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
I : Ideal S
hI : absNorm I = 0
x : S
hx : x ∈ I
⊢ x ∈ ⊥

Tactic:
mem_bot,

Goal state after:
case mp
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
I : Ideal S
hI : absNorm I = 0
x : S
hx : x ∈ I
⊢ x = 0
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
I : Ideal S
⊢ 0 < absNorm I ↔ I ∈ (Ideal S)⁰

Tactic:
rw [← absNorm_ne_zero_iff_mem_nonZeroDivisors, Nat.pos_iff_ne_zero]

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
inst✝ : Module.Finite ℤ S
p : ℤ
hp : Prime p
this✝ : IsAddTorsionFree S
this : CharZero S
hpMax : (span {p}).IsMaximal
I : Ideal S
hI' : IsUnit I
hI : p ∣ ↑(absNorm I)
⊢ I = ⊤

Tactic:
simpa using hI'

Goal state after:
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
hI : p ∣ ↑(absNorm P)
this : P.IsMaximal
q n : ℕ
hn : 0 < n
hqP : ↑q ∈ P
hq : Nat.Prime q
H : absNorm P = q ^ n
⊢ span {p} ≤ under ℤ P

Tactic:
H,

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 : ℕ
hI : p ∣ ↑(q ^ n)
hn : 0 < n
hqP : ↑q ∈ P
hq : Nat.Prime q
H : absNorm P = q ^ n
⊢ span {p} ≤ under ℤ P
Module: Mathlib.RingTheory.HopkinsLevitzki

Goal state before:
pp: R₀ : Type u_1
R : Type u_2
M : Type u
inst✝⁷ : Ring R₀
inst✝⁶ : Ring R
inst✝⁵ : Module R₀ R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R₀ M
inst✝² : Module R M
inst✝¹ : IsScalarTower R₀ R M
inst✝ : IsSemiprimaryRing R
P : (M : Type u) → [inst : AddCommGroup M] → [Module R₀ M] → [Module R M] → Prop
h0 :
  ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [IsScalarTower R₀ R M]
    [IsSemisimpleModule R M], Module.IsTorsionBySet R M ↑(Ring.jacobson R) → P M
h1 :
  ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [inst_3 : IsScalarTower R₀ R M],
    let N := Ring.jacobson R • ⊤;
    P ↥N → P (M ⧸ N) → P M
⊢ P M

Tactic:
by
  have ⟨ss, n, hn⟩ := (isSemiprimaryRing_iff R).mp ‹_›
  set Jac := Ring.jacobson R
  replace hn : Jac ^ n ≤ Module.annihilator R M := hn ▸ bot_le
  have {M} [AddCommGroup M] [Module R₀ M] [Module R M] [IsScalarTower R₀ R M] :
      Jac ≤ Module.annihilator R M → P M := by
    rw [← SetLike.coe_subset_coe, ← Module.isTorsionBySet_iff_subset_annihilator]
    intro h
    let _ := h.module
    have := (h.semilinearMap.isSemisimpleModule_iff_of_bijective Function.bijective_id).2
      inferInstance
    exact h0 _ h
  induction n generalizing M with
  | zero => rw [Jac.pow_zero, Ideal.one_eq_top] at hn; exact this (le_top.trans hn)
  | succ n ih => ?_
  obtain _ | n := n
  · rw [Jac.pow_one] at hn; exact this hn
  refine h1 _ (ih _ ?_) (ih _ ?_)
  · rwa [← Submodule.annihilator_top, Submodule.le_annihilator_iff, Jac.pow_succ,
      Submodule.mul_smul, ← Submodule.le_annihilator_iff] at hn
  · rw [← SetLike.coe_subset_coe, ← Module.isTorsionBySet_iff_subset_annihilator,
      Module.isTorsionBySet_quotient_iff]
    exact fun m i hi ↦ Submodule.smul_mem_smul (Ideal.pow_le_self n.succ_ne_zero hi) trivial

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

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
inst✝¹ : P.IsPrime
inst✝ : IsNoetherianRing S
hpP : map f p ≤ P
hp : P ≠ ⊥
hp' : P.primeCompl ≤ nonZeroDivisors S
H : map (algebraMap R (Localization.AtPrime P)) p = maximalIdeal (Localization.AtPrime P)
h₂ : map (algebraMap R (Localization.AtPrime P)) p ≤ maximalIdeal (Localization P.primeCompl) ^ 2
⊢ False

Tactic:
H,

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
inst✝¹ : P.IsPrime
inst✝ : IsNoetherianRing S
hpP : map f p ≤ P
hp : P ≠ ⊥
hp' : P.primeCompl ≤ nonZeroDivisors S
H : map (algebraMap R (Localization.AtPrime P)) p = maximalIdeal (Localization.AtPrime P)
h₂ : maximalIdeal (Localization.AtPrime P) ≤ maximalIdeal (Localization P.primeCompl) ^ 2
⊢ False
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: case h₂
R : Type v
inst✝⁶ : CommRing R
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
B✝ : Type w
inst✝³ : CommRing B✝
inst✝² : FormallyUnramified R A
I✝ : Ideal B✝
hI : IsNilpotent I✝
B : Type w
inst✝¹ : CommRing B
I J : Ideal B
hIJ : I ≤ J
h₁ : ∀ [inst : Algebra R B], Function.Injective (Ideal.Quotient.mkₐ R I).comp
h₂ : ∀ [inst : Algebra R (B ⧸ I)], Function.Injective (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)).comp
inst✝ : Algebra R B
g₁ g₂ : A →ₐ[R] B
x : A
e : (Ideal.Quotient.mk J) (g₁ x) = (Ideal.Quotient.mk J) (g₂ x)
⊢ g₁ x - g₂ x ∈ J

Tactic:
← Ideal.Quotient.eq

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

Goal state before:
pp: case neg
R : Type v
inst✝⁵ : CommRing R
A : Type u
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type w
inst✝² : CommRing B
inst✝¹ : Algebra R B
I : Ideal B
inst✝ : FormallyUnramified R A
hI : ⨅ i, I ^ i = ⊥
g₁ g₂ : A →ₐ[R] B
H : ∀ (x : A), (Ideal.Quotient.mk I) (g₁ x) = (Ideal.Quotient.mk I) (g₂ x)
i : ℕ
hi : ¬i = 0
x : A
⊢ g₁ x - g₂ x ∈ I

pp: case neg
R : Type v
inst✝⁵ : CommRing R
A : Type u
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type w
inst✝² : CommRing B
inst✝¹ : Algebra R B
I : Ideal B
inst✝ : FormallyUnramified R A
hI : ⨅ i, I ^ i = ⊥
g₁ g₂ : A →ₐ[R] B
H : ∀ (x : A), (Ideal.Quotient.mk I) (g₁ x) = (Ideal.Quotient.mk I) (g₂ x)
i : ℕ
hi : ¬i = 0
x : A
⊢ RingHom.ker (Ideal.Quotient.mk (I ^ i)) ≤ I

pp: case neg.hf
R : Type v
inst✝⁵ : CommRing R
A : Type u
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type w
inst✝² : CommRing B
inst✝¹ : Algebra R B
I : Ideal B
inst✝ : FormallyUnramified R A
hI : ⨅ i, I ^ i = ⊥
g₁ g₂ : A →ₐ[R] B
H : ∀ (x : A), (Ideal.Quotient.mk I) (g₁ x) = (Ideal.Quotient.mk I) (g₂ x)
i : ℕ
hi : ¬i = 0
x : A
⊢ Function.Surjective ⇑(Ideal.Quotient.mk (I ^ i))

Tactic:
← Ideal.Quotient.eq

Goal state after:
case neg
R : Type v
inst✝⁵ : CommRing R
A : Type u
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type w
inst✝² : CommRing B
inst✝¹ : Algebra R B
I : Ideal B
inst✝ : FormallyUnramified R A
hI : ⨅ i, I ^ i = ⊥
g₁ g₂ : A →ₐ[R] B
H : ∀ (x : A), (Ideal.Quotient.mk I) (g₁ x) = (Ideal.Quotient.mk I) (g₂ x)
i : ℕ
hi : ¬i = 0
x : A
⊢ (Ideal.Quotient.mk I) (g₁ x) = (Ideal.Quotient.mk I) (g₂ x)

case neg
R : Type v
inst✝⁵ : CommRing R
A : Type u
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type w
inst✝² : CommRing B
inst✝¹ : Algebra R B
I : Ideal B
inst✝ : FormallyUnramified R A
hI : ⨅ i, I ^ i = ⊥
g₁ g₂ : A →ₐ[R] B
H : ∀ (x : A), (Ideal.Quotient.mk I) (g₁ x) = (Ideal.Quotient.mk I) (g₂ x)
i : ℕ
hi : ¬i = 0
x : A
⊢ RingHom.ker (Ideal.Quotient.mk (I ^ i)) ≤ I

case neg.hf
R : Type v
inst✝⁵ : CommRing R
A : Type u
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type w
inst✝² : CommRing B
inst✝¹ : Algebra R B
I : Ideal B
inst✝ : FormallyUnramified R A
hI : ⨅ i, I ^ i = ⊥
g₁ g₂ : A →ₐ[R] B
H : ∀ (x : A), (Ideal.Quotient.mk I) (g₁ x) = (Ideal.Quotient.mk I) (g₂ x)
i : ℕ
hi : ¬i = 0
x : A
⊢ Function.Surjective ⇑(Ideal.Quotient.mk (I ^ i))
Module: Mathlib.RingTheory.QuasiFinite.Basic

Goal state before:
pp: case neg
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : QuasiFinite R S
I : Ideal R
h : ¬I.IsPrime
⊢ (I.primesOver S).Finite

Tactic:
convert! Set.finite_empty

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : QuasiFinite R S
I : Ideal R
h : ¬I.IsPrime
⊢ I.primesOver S = ∅
Module: Mathlib.RingTheory.Smooth.Kaehler

Goal state before:
pp: R : Type u_1
P : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
g✝ : S →ₐ[R] P
f : P →ₐ[R] S
hf' : RingHom.ker f ^ 2 = ⊥
g : S →ₐ[R] P
hg : f.comp g = AlgHom.id R S
x : R
y : P
⊢ ⟨x • y - g (f (x • y)), ⋯⟩ = (RingHom.id R) x • ⟨y - g (f y), ⋯⟩

Tactic:
ext
    simp only [Algebra.smul_def, map_mul, AlgHom.commutes,
      RingHom.id_apply, Submodule.coe_smul_of_tower]
    ring

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
P : Ideal R
inst✝⁴ : P.IsPrime
Q' : Ideal (P.Fiber A)
inst✝³ : Q'.IsPrime
inst✝² : (Ideal.comap TensorProduct.includeRight.toRingHom Q').IsPrime
inst✝¹ : (Ideal.comap TensorProduct.includeRight.toRingHom Q').LiesOver P
inst✝ : IsUnramifiedAt R (Ideal.comap TensorProduct.includeRight.toRingHom Q')
f₀ : Localization.AtPrime (Ideal.comap TensorProduct.includeRight.toRingHom Q') →ₐ[R] Localization.AtPrime Q' :=
  Localization.localAlgHom (Ideal.comap TensorProduct.includeRight.toRingHom Q') Q' TensorProduct.includeRight ⋯
⊢ Function.Surjective ⇑f₀

Tactic:
exact P.surjectiveOnStalks_residueField.baseChange' _ _

Goal state after:
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:
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.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
⊢ (Q.ker • ⊤).toAddSubgroup ≤ (↑f').ker

Tactic:
by
    intro x hx
    refine Submodule.smul_induction_on hx ?_ fun _ _ ↦ add_mem
    clear x hx
    rintro a ha b -
    obtain ⟨x, hx⟩ := e.surjective ⟨a, ha⟩
    obtain rfl : (e x).1 = a := congr_arg Subtype.val hx
    obtain ⟨y, rfl⟩ := e.surjective b
    simp only [AddMonoidHom.mem_ker, AddMonoidHom.coe_coe, map_smul,
      LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
      LinearEquiv.symm_apply_apply, f']
    clear hx ha
    induction x with
    | zero => simp only [map_zero, ZeroMemClass.coe_zero, zero_smul]
    | add x y _ _ =>
      simp only [map_add, Submodule.coe_add, add_smul, zero_add, *]
    | tmul a b =>
      induction y with
      | zero => simp only [map_zero, smul_zero]
      | add x y hx hy => simp only [LinearMap.map_add, smul_add, hx, hy, zero_add]
      | tmul c d =>
        simp only [LinearMap.liftBaseChange_tmul, LinearMap.coe_comp, SetLike.val_smul,
          LinearMap.coe_restrictScalars, Function.comp_apply, mk_apply, smul_eq_mul, e,
          LinearMap.liftBaseChange_tmul, LinearEquiv.ofBijective_apply]
        have h₂ : b.1 • Cotangent.mk d = 0 := by ext; simp [Cotangent.smul_eq_zero_of_mem _ b.2]
        rw [TensorProduct.smul_tmul', mul_smul, f.mapKer_apply_coe, ← halg,
          algebraMap_smul, ← TensorProduct.tmul_smul, h₂, tmul_zero, smul_zero]

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

Goal state before:
pp: case e'_4
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₂
τ : Type w₅
Q : Generators S T ι
P : Generators R S σ
W : Generators R T τ
inst✝ : Flat S T
f : W.Hom Q
g : P.Hom W
⊢ ↑(equiv W (Q.comp P)) ∘ₗ LinearMap.liftBaseChange T (Extension.H1Cotangent.map g.toExtensionHom) =
    LinearMap.liftBaseChange T (Extension.H1Cotangent.map (Q.toComp P).toExtensionHom)

Tactic:
change Extension.H1Cotangent.map (W.defaultHom (Q.comp P)).toExtensionHom ∘ₗ _ = _

Goal state after:
case e'_4
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₂
τ : Type w₅
Q : Generators S T ι
P : Generators R S σ
W : Generators R T τ
inst✝ : Flat S T
f : W.Hom Q
g : P.Hom W
⊢ Extension.H1Cotangent.map (W.defaultHom (Q.comp P)).toExtensionHom ∘ₗ
      LinearMap.liftBaseChange T (Extension.H1Cotangent.map g.toExtensionHom) =
    LinearMap.liftBaseChange T (Extension.H1Cotangent.map (Q.toComp P).toExtensionHom)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Finsupp

Goal state before:
pp: α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : NormalizationMonoid α
inst✝ : DecidableEq α
a b : α
ha : a ≠ 0
hb : b ≠ 0
h : normalizedFactors a = normalizedFactors b
⊢ a ~ᵤ b

Tactic:
associated_iff_normalizedFactors_eq_normalizedFactors ha hb

Goal state after:
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : NormalizationMonoid α
inst✝ : DecidableEq α
a b : α
ha : a ≠ 0
hb : b ≠ 0
h : normalizedFactors a = normalizedFactors b
⊢ normalizedFactors a = normalizedFactors b
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: A : Type u_1
M : Type u_2
inst✝² : CommRing A
I : Ideal A
inst✝¹ : AddCommGroup M
inst✝ : Module A M
N₁ N₂ : Submodule A M
hD : Disjoint N₁ N₂
w : ℕ
y : M
hy : y ∈ N₁
z : M
hz : z ∈ N₂
h : ∀ a ∈ I ^ w, a • (y + z) = 0
⊢ y ∈ N₁

Tactic:
by simp [hy]

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

Goal state before:
pp: case mpr.right
A : Type u_1
M : Type u_2
inst✝² : CommRing A
I : Ideal A
inst✝¹ : AddCommGroup M
inst✝ : Module A M
N₁ N₂ : Submodule A M
hD : Disjoint N₁ N₂
y : M
hymem : y ∈ N₁
n₁ : ℕ
hy : ∀ a ∈ I ^ n₁, a • y = 0
z : M
hzmem : z ∈ N₂
n₂ : ℕ
hz : ∀ a ∈ I ^ n₂, a • z = 0
⊢ ∃ y_1 ∈ N₁, ∃ z_1 ∈ N₂, y_1 + z_1 = y + z

Tactic:
use y, hymem, z, hzmem

Goal state after: