mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.BilinearForm.DualLattice

Goal state before:
pp: R : Type u_1
S : Type u_3
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : Field S
inst✝⁴ : AddCommGroup M
inst✝³ : Algebra R S
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
B : BilinForm S M
N₁ N₂ : Submodule R M
⊢ N₁ ≤ B.flip.dualSubmodule N₂ ↔ N₂ ≤ B.dualSubmodule N₁

Tactic:
by
  change (∀ (x : M), x ∈ N₁ → _) ↔ ∀ (x : M), x ∈ N₂ → _
  simp only [mem_dualSubmodule, Submodule.mem_one, flip_apply]
  exact forall₂_comm

Goal state after:
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
f : R[X]
hf : f.Monic
g : K[X]
hg : g.Monic
hd : g ∣ map (algebraMap R K) f
this :
  ∀ (n : ℕ),
    (map (algebraMap K g.SplittingField) g).coeff n ∈
      ↑(algebraMap (↥(integralClosure R g.SplittingField)) g.SplittingField).range
⊢ g ∈ lifts (algebraMap (↥(integralClosure R K)) K)

Tactic:
Subalgebra.range_algebraMap

Goal state after:
case refine_2
R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
f : R[X]
hf : f.Monic
g : K[X]
hg : g.Monic
hd : g ∣ map (algebraMap R K) f
this : ∀ (n : ℕ), (map (algebraMap K g.SplittingField) g).coeff n ∈ ↑(integralClosure R g.SplittingField).toSubring
⊢ g ∈ lifts (algebraMap (↥(integralClosure R K)) K)
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
f : R[X]
hf : f.Monic
g : K[X]
hg : g.Monic
hd : g ∣ map (algebraMap R K) f
this : ∀ (n : ℕ), (map (algebraMap K g.SplittingField) g).coeff n ∈ ↑(integralClosure R g.SplittingField).toSubring
n : ℕ
⊢ g.coeff n ∈ ↑(algebraMap (↥(integralClosure R K)) K).range

Tactic:
Subalgebra.range_algebraMap

Goal state after:
case refine_2
R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
f : R[X]
hf : f.Monic
g : K[X]
hg : g.Monic
hd : g ∣ map (algebraMap R K) f
this : ∀ (n : ℕ), (map (algebraMap K g.SplittingField) g).coeff n ∈ ↑(integralClosure R g.SplittingField).toSubring
n : ℕ
⊢ g.coeff n ∈ ↑(integralClosure R K).toSubring
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
p q : R[X]
hp : p.Monic
hq : q.Monic
r : K[X]
hr : Polynomial.map (algebraMap R K) p = Polynomial.map (algebraMap R K) q * r
d' : R[X]
hr' : Polynomial.map (algebraMap R K) d' * C r.leadingCoeff = r
⊢ (Polynomial.map (algebraMap R K) q * r).Monic

Tactic:
by simpa [← hr] using hp.map _

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

Goal state before:
pp: F : Type u
E : Type v
inst✝⁸ : Field F
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
K : Type w
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
p : ℕ
inst✝ : ExpChar A p
x y : A
n : ℕ
hx : x ^ p ^ n ∈ (algebraMap R A).rangeS
m : ℕ
hy : y ^ p ^ m ∈ (algebraMap R A).rangeS
⊢ x * y ∈ {x | ∃ n, x ^ p ^ n ∈ (algebraMap R A).rangeS}

Tactic:
use n + m

Goal state after:
case h
F : Type u
E : Type v
inst✝⁸ : Field F
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
K : Type w
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
p : ℕ
inst✝ : ExpChar A p
x y : A
n : ℕ
hx : x ^ p ^ n ∈ (algebraMap R A).rangeS
m : ℕ
hy : y ^ p ^ m ∈ (algebraMap R A).rangeS
⊢ (x * y) ^ p ^ (n + m) ∈ (algebraMap R A).rangeS
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: F : Type u
E : Type v
inst✝⁸ : Field F
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
K : Type w
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
p : ℕ
inst✝ : ExpChar A p
x y : A
n : ℕ
hx : x ^ p ^ n ∈ (algebraMap R A).rangeS
m : ℕ
hy : y ^ p ^ m ∈ (algebraMap R A).rangeS
⊢ x + y ∈ {x | ∃ n, x ^ p ^ n ∈ (algebraMap R A).rangeS}

Tactic:
use n + m

Goal state after:
case h
F : Type u
E : Type v
inst✝⁸ : Field F
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
K : Type w
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
p : ℕ
inst✝ : ExpChar A p
x y : A
n : ℕ
hx : x ^ p ^ n ∈ (algebraMap R A).rangeS
m : ℕ
hy : y ^ p ^ m ∈ (algebraMap R A).rangeS
⊢ (x + y) ^ p ^ (n + m) ∈ (algebraMap R A).rangeS
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: case inl.zero
k : Type u_1
K : Type u_2
R : Type u_3
inst✝⁶ : Field k
inst✝⁵ : Field K
inst✝⁴ : Algebra k K
inst✝³ : CommRing R
inst✝² : Algebra k R
inst✝¹ : IsPurelyInseparable k K
q : ℕ
inst✝ : ExpChar k q
a✝ : Nontrivial (R ⊗[k] K)
hq : Nat.Prime q
⊢ ∃ n, 0 ^ q ^ n ∈ (algebraMap R (R ⊗[k] K)).range

Tactic:
exact ⟨0, 0, by simp⟩

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

Goal state before:
pp: G : Type u_1
B : Type u_3
inst✝⁴ : Group G
inst✝³ : Semiring B
inst✝² : MulSemiringAction G B
C : Type u_4
inst✝¹ : CommSemiring C
inst✝ : Algebra C B
N : Subgroup G
hN : N.Normal
hC : IsGaloisGroup (↥N) C B
g : G
x : C
n : ↥N
⊢ (g⁻¹ * ↑n * g) • (algebraMap C B) x = (algebraMap C B) x

Tactic:
exact Subgroup.smul_algebraMap B (hN.conj_mem' n n.prop g) x

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : NumberField K
M : Type u_3
inst✝ : AddZeroClass M
f : M →+ K
h : ∀ (x : M), IsIntegral ℤ (f x)
⊢ restrict (⇑f) h 0 = 0

Tactic:
by simp only [restrict, map_zero]; rfl

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

Goal state before:
pp: G : Type u_1
inst✝⁹ : Group G
H : Subgroup G
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁸ : CommSemiring A
inst✝⁷ : Semiring C
inst✝⁶ : Algebra A C
inst✝⁵ : MulSemiringAction G C
N : Subgroup G
inst✝⁴ : CommSemiring B
inst✝³ : Algebra B C
inst✝² : FaithfulSMul B C
inst✝¹ : IsGaloisGroup (↥N) B C
inst✝ : N.Normal
this : MulSemiringAction G B := mulSemiringActionOfNormal G B C N
q : G ⧸ N
x : B
g₁ g₂ : G
h : (QuotientGroup.leftRel N) g₁ g₂
⊢ g₁⁻¹ * g₂ ∈ ?m.186

Tactic:
rwa [← QuotientGroup.leftRel_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.Quotient.Pi

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
Ms : ι → Type u_3
inst✝⁵ : (i : ι) → AddCommGroup (Ms i)
inst✝⁴ : (i : ι) → Module R (Ms i)
N : Type u_4
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
q : Submodule R N
f : (i : ι) → Ms i →ₗ[R] N
hf : ∀ (i : ι), p i ≤ comap (f i) q
x : (i : ι) → Ms i
⊢ ((piQuotientLift p q f hf) fun i ↦ Quotient.mk (x i)) = Quotient.mk (((lsum R Ms R) f) x)

Tactic:
rw [piQuotientLift, lsum_apply, sum_apply, ← mkQ_apply, lsum_apply, sum_apply, _root_.map_sum]
  simp only [coe_proj, mapQ_apply, mkQ_apply, comp_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.Quotient.Pi

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁴ : CommRing R
Ms : ι → Type u_3
inst✝³ : (i : ι) → AddCommGroup (Ms i)
inst✝² : (i : ι) → Module R (Ms i)
p : (i : ι) → Submodule R (Ms i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
x : Ms i ⧸ p i
⊢ (quotientPiLift p (fun i ↦ (p i).mkQ) ⋯ ∘ₗ piQuotientLift p (pi Set.univ p) (single R Ms) ⋯) (Pi.single i x) =
    LinearMap.id (Pi.single i x)

Tactic:
induction x using Submodule.Quotient.induction_on with

Goal state after:
case H
ι : Type u_1
R : Type u_2
inst✝⁴ : CommRing R
Ms : ι → Type u_3
inst✝³ : (i : ι) → AddCommGroup (Ms i)
inst✝² : (i : ι) → Module R (Ms i)
p : (i : ι) → Submodule R (Ms i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
x' : Ms i
⊢ (quotientPiLift p (fun i ↦ (p i).mkQ) ⋯ ∘ₗ piQuotientLift p (pi Set.univ p) (single R Ms) ⋯)
      (Pi.single i (Quotient.mk x')) =
    LinearMap.id (Pi.single i (Quotient.mk x'))
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: F : Type u_3
inst✝² : Field F
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP F p
⊢ (X ^ p - X).roots = univ.val

Tactic:
let _ := Subfield.fintypeBot F p

Goal state after:
F : Type u_3
inst✝² : Field F
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP F p
x✝ : Fintype ↥⊥ := fintypeBot F p
⊢ (X ^ p - X).roots = univ.val
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: F : Type u_3
inst✝² : Field F
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP F p
⊢ (X ^ p - X).Splits

Tactic:
let _ := Subfield.fintypeBot F p

Goal state after:
F : Type u_3
inst✝² : Field F
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP F p
x✝ : Fintype ↥⊥ := fintypeBot F p
⊢ (X ^ p - X).Splits
Module: Mathlib.LinearAlgebra.FreeModule.Finite.Quotient

Goal state before:
pp: M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Free ℤ M
inst✝ : Module.Finite ℤ M
N : Submodule ℤ M
h : finrank ℤ ↥N = finrank ℤ M
⊢ Finite (M ⧸ N)

Tactic:
let b := Module.Free.chooseBasis ℤ M
  let a := smithNormalFormCoeffs b h
  let e := N.quotientEquivPiZMod b h
  have : ∀ i, NeZero (a i).natAbs := fun i ↦
    ⟨Int.natAbs_ne_zero.mpr (smithNormalFormCoeffs_ne_zero b h i)⟩
  exact Finite.of_equiv (Π i, ZMod (a i).natAbs) e.symm

Goal state after:
Module: Mathlib.RingTheory.Finiteness.NilpotentKer

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✝ : 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)

Tactic:
refine ?_ ∘ₗ (TensorProduct.quotTensorEquivQuotSMul _ I).toLinearMap
        refine Submodule.liftQ _ ((Submodule.mkQ _).comp (I ^ n).subtype) ?_
        rw [LinearMap.ker_comp, ← Submodule.map_le_map_iff_of_injective (I ^ n).subtype_injective,
          Submodule.map_smul'', Submodule.map_comap_eq]
        simpa [pow_succ'] using Ideal.mul_le_right (I := I) (J := I ^ n)

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

Goal state before:
pp: case succ.refine_2.h
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
a : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
f g : (c : S) → c ∈ P ^ i → S
hg : ∀ (c : S) (hc : c ∈ P ^ i), g c hc ∈ P ^ (i + 1)
hf : ∀ (c : S) (hc : c ∈ P ^ i), a * f c hc + g c hc = c
k : (c' : S ⧸ P ^ i.succ) → c' ∈ map (mkQ (P ^ i.succ)) (P ^ i) → S
hk_mem : ∀ (c' : S ⧸ P ^ i.succ) (hc' : c' ∈ map (mkQ (P ^ i.succ)) (P ^ i)), k c' hc' ∈ P ^ i
hk_eq : ∀ (c' : S ⧸ P ^ i.succ) (hc' : c' ∈ map (mkQ (P ^ i.succ)) (P ^ i)), (mkQ (P ^ i.succ)) (k c' hc') = c'
d : S
⊢ ∃ a, (fun c' ↦ Quotient.mk'' (f (k ↑c' ⋯) ⋯)) a = ⟦d⟧

Tactic:
have hd' := (mem_map (f := mkQ (P ^ i.succ))).mpr ⟨a * d, Ideal.mul_mem_right d _ a_mem, rfl⟩

Goal state after:
case succ.refine_2.h
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
a : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
f g : (c : S) → c ∈ P ^ i → S
hg : ∀ (c : S) (hc : c ∈ P ^ i), g c hc ∈ P ^ (i + 1)
hf : ∀ (c : S) (hc : c ∈ P ^ i), a * f c hc + g c hc = c
k : (c' : S ⧸ P ^ i.succ) → c' ∈ map (mkQ (P ^ i.succ)) (P ^ i) → S
hk_mem : ∀ (c' : S ⧸ P ^ i.succ) (hc' : c' ∈ map (mkQ (P ^ i.succ)) (P ^ i)), k c' hc' ∈ P ^ i
hk_eq : ∀ (c' : S ⧸ P ^ i.succ) (hc' : c' ∈ map (mkQ (P ^ i.succ)) (P ^ i)), (mkQ (P ^ i.succ)) (k c' hc') = c'
d : S
hd' : (mkQ (P ^ i.succ)) (a * d) ∈ map (mkQ (P ^ i.succ)) (P ^ i)
⊢ ∃ a, (fun c' ↦ Quotient.mk'' (f (k ↑c' ⋯) ⋯)) a = ⟦d⟧
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
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) ∨ p ∣ ↑(absNorm I)
⊢ ∃ P_1, P_1.IsMaximal ∧ under ℤ P_1 = span {p} ∧ P_1 ∣ P * I

Tactic:
cases hI with
    | inr h =>
      obtain ⟨Q, h₁, h₂, h₃⟩ := IH h
      exact ⟨Q, h₁, h₂, dvd_mul_of_dvd_right h₃ _⟩
    | inl hI =>
      have := (Ideal.isPrime_of_prime hP).isMaximal hP.ne_zero
      refine ⟨P, this, (hpMax.eq_of_le (by simpa using this.ne_top) ?_).symm, dvd_mul_right _ _⟩
      obtain ⟨q, n, hn, hqP, hq, H⟩ := Ideal.exists_prime_and_absNorm_eq_pow P
      rw [H, Nat.cast_pow, dvd_prime_pow (Nat.prime_iff_prime_int.mp hq)] at hI
      obtain ⟨m, hmn, hp⟩ := hI
      rw [Ideal.span_singleton_le_iff_mem]
      have : m ≠ 0 := fun h ↦ hpMax.ne_top (Ideal.span_singleton_eq_top.mpr (by simpa [h] using hp))
      exact Ideal.mem_of_dvd _ hp.symm.dvd (Ideal.pow_mem_of_mem _ (by simpa) _ this.bot_lt)

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

Goal state before:
pp: case refine_1
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDedekindDomain S
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
n : ℕ
inst✝ : CharZero S
this✝ : Finite { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n }
this : Finite { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n }
⊢ ∀ (x : Ideal S), absNorm x ≤ n ↔ x ∈ (Ideal S)⁰ ∧ absNorm x ≤ n ∨ x ∉ (Ideal S)⁰ ∧ absNorm x ≤ n

Tactic:
intro _
      simp_rw [← or_and_right, em, true_and]

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✝ : DecidablePred fun n ↦ ∀ (k : ℕ), map f p ≤ P ^ k → k ≤ n
h : ∃ n, ∀ (k : ℕ), map f p ≤ P ^ k → k ≤ n
⊢ p.ramificationIdx' P = Nat.find h

Tactic:
convert! Nat.sSup_def h

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
inst✝³ : IsDedekindDomain S
inst✝² : IsDedekindDomain R
inst✝¹ : FaithfulSMul R S
v : Ideal R
w : Ideal S
p : Ideal R
hv : Irreducible v
hp : Prime p
hw : Irreducible w
hw_bot : w ≠ ⊥
inst✝ : w.LiesOver v
hp_bot : map f p ≠ ⊥
⊢ emultiplicity w (map f p) = ↑(v.ramificationIdx' w) * emultiplicity v p

Tactic:
by_cases hvp : v = p

Goal state after:
case pos
R : Type u
inst✝⁶ : CommRing R
S : Type v
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDedekindDomain S
inst✝² : IsDedekindDomain R
inst✝¹ : FaithfulSMul R S
v : Ideal R
w : Ideal S
p : Ideal R
hv : Irreducible v
hp : Prime p
hw : Irreducible w
hw_bot : w ≠ ⊥
inst✝ : w.LiesOver v
hp_bot : map f p ≠ ⊥
hvp : v = p
⊢ emultiplicity w (map f p) = ↑(v.ramificationIdx' w) * emultiplicity v p

case neg
R : Type u
inst✝⁶ : CommRing R
S : Type v
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDedekindDomain S
inst✝² : IsDedekindDomain R
inst✝¹ : FaithfulSMul R S
v : Ideal R
w : Ideal S
p : Ideal R
hv : Irreducible v
hp : Prime p
hw : Irreducible w
hw_bot : w ≠ ⊥
inst✝ : w.LiesOver v
hp_bot : map f p ≠ ⊥
hvp : ¬v = p
⊢ emultiplicity w (map f p) = ↑(v.ramificationIdx' w) * emultiplicity v p
Module: Mathlib.RingTheory.QuasiFinite.Basic

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✝² : QuasiFinite R S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra R A
P : Ideal A
hP : P.IsPrime
p : Ideal R := Ideal.under R P
⊢ Module.Finite P.ResidueField (P.Fiber (A ⊗[R] S))

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

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✝² : QuasiFinite R S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra R A
P : Ideal A
hP : P.IsPrime
p : Ideal R := Ideal.under R P
this : Algebra (Localization.AtPrime p) (Localization.AtPrime P) := Localization.AtPrime.algebraOfLiesOver p P
⊢ Module.Finite P.ResidueField (P.Fiber (A ⊗[R] S))
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
inst✝ : FiniteType R S
⊢ (∀ (a : Ideal R) (b : a.IsPrime),
      (PrimeSpectrum.comap (algebraMap R S) ⁻¹' {(PrimeSpectrum.equivSubtype R).symm ⟨a, b⟩}).Finite) ↔
    ∀ (I : Ideal R), I.IsPrime → (I.primesOver S).Finite

Tactic:
refine forall₂_congr fun I hI ↦ ?_

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FiniteType R S
I : Ideal R
hI : I.IsPrime
⊢ (PrimeSpectrum.comap (algebraMap R S) ⁻¹' {(PrimeSpectrum.equivSubtype R).symm ⟨I, hI⟩}).Finite ↔
    (I.primesOver S).Finite
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
B : Type u_1
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
C : Type u_4
inst✝² : CommRing C
inst✝¹ : Algebra R C
inst✝ : FormallySmooth R A
f : A →ₐ[R] C
g : B →ₐ[R] C
hg : Function.Surjective ⇑g
hg' : IsNilpotent (RingHom.ker g)
x : A
⊢ (Ideal.quotientKerAlgEquivOfSurjective hg).symm (g ((liftOfSurjective f g hg hg') x)) =
    (Ideal.quotientKerAlgEquivOfSurjective hg).symm (f x)

Tactic:
conv_rhs => rw [← AlgEquiv.coe_toAlgHom, ← AlgHom.comp_apply,
    ← FormallySmooth.mk_lift (A := A) _ hg']

Goal state after:
R : Type u
A : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
B : Type u_1
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
C : Type u_4
inst✝² : CommRing C
inst✝¹ : Algebra R C
inst✝ : FormallySmooth R A
f : A →ₐ[R] C
g : B →ₐ[R] C
hg : Function.Surjective ⇑g
hg' : IsNilpotent (RingHom.ker g)
x : A
⊢ (Ideal.quotientKerAlgEquivOfSurjective hg).symm (g ((liftOfSurjective f g hg hg') x)) =
    (Ideal.Quotient.mk (RingHom.ker g))
      ((lift (RingHom.ker g) hg' ((↑(Ideal.quotientKerAlgEquivOfSurjective hg).symm).comp f)) x)
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
P : Extension R A
inst✝ : FormallySmooth R P.Ring
⊢ Function.Injective ⇑P.cotangentComplex ↔ Subsingleton (H1Cotangent R A)

Tactic:
← Algebra.Extension.subsingleton_h1Cotangent,

Goal state after:
R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
P : Extension R A
inst✝ : FormallySmooth R P.Ring
⊢ Subsingleton P.H1Cotangent ↔ Subsingleton (H1Cotangent R A)
Module: Mathlib.RingTheory.Smooth.Basic

Goal state before:
pp: case e'_1
R : Type u
A : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
P : Type u_2
inst✝⁴ : CommRing P
inst✝³ : Algebra R P
inst✝² : FormallySmooth R P
inst✝¹ : Algebra P A
inst✝ : IsScalarTower R P A
hf : Function.Surjective ⇑(algebraMap P A)
⊢ (∃ i, mapBaseChange R P A ∘ₗ i = LinearMap.id) ↔ ∃ l, ↑P (mapBaseChange R P A) ∘ₗ l = LinearMap.id

Tactic:
rw [← (LinearMap.extendScalarsOfSurjectiveEquiv hf).exists_congr_right]

Goal state after:
case e'_1
R : Type u
A : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
P : Type u_2
inst✝⁴ : CommRing P
inst✝³ : Algebra R P
inst✝² : FormallySmooth R P
inst✝¹ : Algebra P A
inst✝ : IsScalarTower R P A
hf : Function.Surjective ⇑(algebraMap P A)
⊢ (∃ a, mapBaseChange R P A ∘ₗ (LinearMap.extendScalarsOfSurjectiveEquiv hf).toAddEquiv.toEquiv a = LinearMap.id) ↔
    ∃ l, ↑P (mapBaseChange R P A) ∘ₗ l = LinearMap.id
Module: Mathlib.RingTheory.Smooth.Basic

Goal state before:
pp: case e'_2
R : Type u
A : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
P : Type u_2
inst✝⁴ : CommRing P
inst✝³ : Algebra R P
inst✝² : FormallySmooth R P
inst✝¹ : Algebra P A
inst✝ : IsScalarTower R P A
hf : Function.Surjective ⇑(algebraMap P A)
⊢ (∃ l, l ∘ₗ kerCotangentToTensor R P A = LinearMap.id) ↔
    Function.Surjective ⇑(↑P (mapBaseChange R P A)) ∧ ∃ l, l ∘ₗ kerCotangentToTensor R P A = LinearMap.id

Tactic:
and_iff_right (by exact mapBaseChange_surjective R P A hf)

Goal state after:
case e'_2
R : Type u
A : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
P : Type u_2
inst✝⁴ : CommRing P
inst✝³ : Algebra R P
inst✝² : FormallySmooth R P
inst✝¹ : Algebra P A
inst✝ : IsScalarTower R P A
hf : Function.Surjective ⇑(algebraMap P A)
⊢ (∃ l, l ∘ₗ kerCotangentToTensor R P A = LinearMap.id) ↔ ∃ l, l ∘ₗ kerCotangentToTensor R P A = LinearMap.id
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 σ
⊢ Function.Exact ⇑(LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom))
    ⇑(Extension.CotangentSpace.map (Q.ofComp P).toExtensionHom)

Tactic:
rw [← fst_compEquiv, ← compEquiv_symm_inr]

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 σ
⊢ Function.Exact
    ⇑(↑(compEquiv Q P).symm ∘ₗ LinearMap.inr T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace))
    ⇑(LinearMap.fst T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace) ∘ₗ ↑(compEquiv Q P))
Module: Mathlib.RingTheory.Smooth.Basic

Goal state before:
pp: R : Type u_4
A : Type u_5
Rₘ : Type u_6
Sₘ : Type u_7
inst✝¹³ : CommRing R
inst✝¹² : CommRing A
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : CommRing Sₘ
M : Submonoid R
inst✝⁹ : Algebra R A
inst✝⁸ : Algebra R Sₘ
inst✝⁷ : Algebra A Sₘ
inst✝⁶ : Algebra R Rₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsScalarTower R A Sₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : IsLocalization (Submonoid.map (algebraMap R A) M) Sₘ
inst✝ : FormallySmooth R A
this : FormallySmooth A Sₘ
⊢ FormallySmooth Rₘ Sₘ

Tactic:
have : FormallySmooth R Sₘ := FormallySmooth.comp R A Sₘ

Goal state after:
R : Type u_4
A : Type u_5
Rₘ : Type u_6
Sₘ : Type u_7
inst✝¹³ : CommRing R
inst✝¹² : CommRing A
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : CommRing Sₘ
M : Submonoid R
inst✝⁹ : Algebra R A
inst✝⁸ : Algebra R Sₘ
inst✝⁷ : Algebra A Sₘ
inst✝⁶ : Algebra R Rₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsScalarTower R A Sₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : IsLocalization (Submonoid.map (algebraMap R A) M) Sₘ
inst✝ : FormallySmooth R A
this✝ : FormallySmooth A Sₘ
this : FormallySmooth R Sₘ
⊢ FormallySmooth Rₘ Sₘ
Module: Mathlib.RingTheory.Unramified.Locus

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra R A
inst✝⁷ : Algebra A B
inst✝⁶ : Algebra R B
inst✝⁵ : IsScalarTower R A B
p : Ideal A
P : Ideal B
inst✝⁴ : P.LiesOver p
inst✝³ : p.IsPrime
inst✝² : P.IsPrime
inst✝¹ : IsUnramifiedAt R p
inst✝ : IsUnramifiedAt A P
⊢ IsUnramifiedAt R P

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

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra R A
inst✝⁷ : Algebra A B
inst✝⁶ : Algebra R B
inst✝⁵ : IsScalarTower R A B
p : Ideal A
P : Ideal B
inst✝⁴ : P.LiesOver p
inst✝³ : p.IsPrime
inst✝² : P.IsPrime
inst✝¹ : IsUnramifiedAt R p
inst✝ : IsUnramifiedAt A P
this : Algebra (Localization.AtPrime p) (Localization.AtPrime P) := Localization.AtPrime.algebraOfLiesOver p P
⊢ IsUnramifiedAt R P