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

Goal state before:
pp: case succ
n : ℕ
IH :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal S) [inst_3 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (f : MvPolynomial (Fin n) R →ₐ[R] S), f.Finite → ZariskisMainProperty R p
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : WeaklyQuasiFiniteAt R p
f : MvPolynomial (Fin (n + 1)) R →ₐ[R] S
hf : f.Finite
f' : (MvPolynomial (Fin n) R)[X] →ₐ[R] S := f.comp ↑(MvPolynomial.finSuccEquiv R n).symm
this✝⁴ : Algebra (MvPolynomial (Fin n) R) S := (f'.comp C).toAlgebra
this✝³ : IsScalarTower R (MvPolynomial (Fin n) R) S
f'' : (MvPolynomial (Fin n) R)[X] →ₐ[MvPolynomial (Fin n) R] S := { toRingHom := f'.toRingHom, commutes' := ⋯ }
this✝² : WeaklyQuasiFiniteAt (MvPolynomial (Fin n) R) p
this✝¹ : ZariskisMainProperty (MvPolynomial (Fin n) R) p
r : S
hrp : r ∉ p
hr : IsIntegral (MvPolynomial (Fin n) R) r
m : S → ℕ
hm : ∀ (x : S), IsIntegral (MvPolynomial (Fin n) R) (r ^ m x * x)
s : Finset S
hs : adjoin R ↑s = ⊤
R' : Subalgebra R S := adjoin R ↑(Finset.image (⇑f ∘ MvPolynomial.X ∘ Fin.succ) Finset.univ ∪ r ^ s.sup m • s ∪ {r})
hrR' : r ∈ R'
this✝ : WeaklyQuasiFiniteAt R (Ideal.under (↥R') p)
φ : MvPolynomial (Fin n) R →ₐ[R] ↥R' := MvPolynomial.aeval fun i ↦ ⟨f (MvPolynomial.X i.succ), ⋯⟩
this : ZariskisMainProperty R (Ideal.under (↥R') p)
⊢ ⊤ ≤ R'.saturation (Submonoid.powers r) ⋯

Tactic:
← hs,

Goal state after:
case succ
n : ℕ
IH :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal S) [inst_3 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (f : MvPolynomial (Fin n) R →ₐ[R] S), f.Finite → ZariskisMainProperty R p
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : WeaklyQuasiFiniteAt R p
f : MvPolynomial (Fin (n + 1)) R →ₐ[R] S
hf : f.Finite
f' : (MvPolynomial (Fin n) R)[X] →ₐ[R] S := f.comp ↑(MvPolynomial.finSuccEquiv R n).symm
this✝⁴ : Algebra (MvPolynomial (Fin n) R) S := (f'.comp C).toAlgebra
this✝³ : IsScalarTower R (MvPolynomial (Fin n) R) S
f'' : (MvPolynomial (Fin n) R)[X] →ₐ[MvPolynomial (Fin n) R] S := { toRingHom := f'.toRingHom, commutes' := ⋯ }
this✝² : WeaklyQuasiFiniteAt (MvPolynomial (Fin n) R) p
this✝¹ : ZariskisMainProperty (MvPolynomial (Fin n) R) p
r : S
hrp : r ∉ p
hr : IsIntegral (MvPolynomial (Fin n) R) r
m : S → ℕ
hm : ∀ (x : S), IsIntegral (MvPolynomial (Fin n) R) (r ^ m x * x)
s : Finset S
hs : adjoin R ↑s = ⊤
R' : Subalgebra R S := adjoin R ↑(Finset.image (⇑f ∘ MvPolynomial.X ∘ Fin.succ) Finset.univ ∪ r ^ s.sup m • s ∪ {r})
hrR' : r ∈ R'
this✝ : WeaklyQuasiFiniteAt R (Ideal.under (↥R') p)
φ : MvPolynomial (Fin n) R →ₐ[R] ↥R' := MvPolynomial.aeval fun i ↦ ⟨f (MvPolynomial.X i.succ), ⋯⟩
this : ZariskisMainProperty R (Ideal.under (↥R') p)
⊢ adjoin R ↑s ≤ R'.saturation (Submonoid.powers r) ⋯
Module: Mathlib.RingTheory.ZariskisMainTheorem

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
p : Ideal S
H : ZariskisMainProperty R p
s : Finset S
hs : adjoin R ↑s = ⊤
r : S
hrp : r ∉ p
hr : IsIntegral R r
m : S → ℕ
hm : ∀ (x : S), IsIntegral R (r ^ m x * x)
t : Set S := insert r {x | ∃ x_1 ∈ s, r ^ m x_1 * x_1 = x}
r' : ↥(adjoin R t) := ⟨r, ⋯⟩
⊢ Subalgebra.map (IsScalarTower.toAlgHom R S (Localization.Away ((adjoin R t).val r'))) ⊤ ≤
    (Localization.awayMapₐ (adjoin R t).val r').range

Tactic:
← hs,

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
p : Ideal S
H : ZariskisMainProperty R p
s : Finset S
hs : adjoin R ↑s = ⊤
r : S
hrp : r ∉ p
hr : IsIntegral R r
m : S → ℕ
hm : ∀ (x : S), IsIntegral R (r ^ m x * x)
t : Set S := insert r {x | ∃ x_1 ∈ s, r ^ m x_1 * x_1 = x}
r' : ↥(adjoin R t) := ⟨r, ⋯⟩
⊢ Subalgebra.map (IsScalarTower.toAlgHom R S (Localization.Away ((adjoin R t).val r'))) (adjoin R ↑s) ≤
    (Localization.awayMapₐ (adjoin R t).val r').range
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: case inl
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
i : Fin m
j : Fin n
h : ↑j < ↑i
⊢ ∀ (a b : ℕ),
    a + b = ↑j →
      (if h : b < k then if a < m ∧ a = ↑i then X (Sum.inr ⟨b, ⋯⟩) else 0
        else if b = k ∧ a < m ∧ a = ↑i then 1 else 0) =
        0

Tactic:
intro a

Goal state after:
case inl
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
i : Fin m
j : Fin n
h : ↑j < ↑i
a : ℕ
⊢ ∀ (b : ℕ),
    a + b = ↑j →
      (if h : b < k then if a < m ∧ a = ↑i then X (Sum.inr ⟨b, ⋯⟩) else 0
        else if b = k ∧ a < m ∧ a = ↑i then 1 else 0) =
        0
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: case inr.h₀
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
i : Fin m
j : Fin n
h : ↑i ≤ ↑j
⊢ ∀ (a b : ℕ),
    a + b = ↑j →
      (a = ↑i → ¬b = ↑j - ↑i) →
        (if h : b < k then if a < m ∧ a = ↑i then X (Sum.inr ⟨b, ⋯⟩) else 0
          else if b = k ∧ a < m ∧ a = ↑i then 1 else 0) =
          0

Tactic:
intro a

Goal state after:
case inr.h₀
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
i : Fin m
j : Fin n
h : ↑i ≤ ↑j
a : ℕ
⊢ ∀ (b : ℕ),
    a + b = ↑j →
      (a = ↑i → ¬b = ↑j - ↑i) →
        (if h : b < k then if a < m ∧ a = ↑i then X (Sum.inr ⟨b, ⋯⟩) else 0
          else if b = k ∧ a < m ∧ a = ↑i then 1 else 0) =
          0
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: case inr.h₀
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
i : Fin k
j : Fin n
h : ↑i ≤ ↑j
⊢ ∀ (a b : ℕ),
    a + b = ↑j →
      ¬(a = ↑j - ↑i ∧ b = ↑i) →
        b < k → (if h : a < m then if b = ↑i then X (Sum.inl ⟨a, ⋯⟩) else 0 else if a = m ∧ b = ↑i then 1 else 0) = 0

Tactic:
intro a

Goal state after:
case inr.h₀
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
i : Fin k
j : Fin n
h : ↑i ≤ ↑j
a : ℕ
⊢ ∀ (b : ℕ),
    a + b = ↑j →
      ¬(a = ↑j - ↑i ∧ b = ↑i) →
        b < k → (if h : a < m then if b = ↑i then X (Sum.inl ⟨a, ⋯⟩) else 0 else if a = m ∧ b = ↑i then 1 else 0) = 0
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
P : {R : Type u} → [inst : CommRing R] → R[X] → Prop
Splits : ∀ (R : Type u) [inst : Field R] (p : R[X]), p.Splits → P p
injective :
  ∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S] (φ : R →+* S),
    Function.Injective ⇑φ → ∀ (p : R[X]), P (map φ p) → P p
surjective :
  ∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S] (φ : R →+* S),
    Function.Surjective ⇑φ → ∀ (p : S[X]), (∀ (q : R[X]), P q) → P p
⊢ P p

Tactic:
by
  wlog hR : IsDomain R generalizing R
  · exact surjective _ _ (MvPolynomial.eval₂Hom (algebraMap ℤ R) id)
      (fun x ↦ ⟨.X x, by simp [MvPolynomial.eval₂Hom]⟩) p
      (fun _ ↦ this _ inferInstance)
  wlog hR : IsField R generalizing R
  · exact injective _ _ _ (FaithfulSMul.algebraMap_injective R (FractionRing R)) _
      (this _ inferInstance (Field.toIsField _))
  wlog hp : p.Splits generalizing R
  · let inst := hR.toField
    exact injective _ _ _ (algebraMap R p.SplittingField).injective _
      (this _ inferInstance (Field.toIsField _) (SplittingField.splits _))
  let inst := hR.toField
  exact Splits _ _ hp

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
r : R
g : R[X]
m n : ℕ
hn : g.natDegree ≤ n
a✝ : Nontrivial R
⊢ ((X - C r) ^ m).resultant g m n = eval r g ^ m

Tactic:
convert! resultant_pow_left _ _ _ _ _ _ <;> simp [natDegree_pow', hn]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case neg.inr
R✝ : Type u_1
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : Field R
f : R[X]
hf' : f.Splits
g : R[X]
r : R
hf : f ≠ 0
hg : g ≠ 0
hf0 : ¬f.natDegree = 0
hg0 : ¬g.natDegree = 0
hr : r ≠ 0
⊢ (f.scaleRoots r).resultant (g.scaleRoots r) (f.scaleRoots r).natDegree =
    r ^ (f.natDegree * g.natDegree) * f.resultant g

Tactic:
resultant_eq_prod_eval _ _ _ le_rfl hf',

Goal state after:
case neg.inr
R✝ : Type u_1
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : Field R
f : R[X]
hf' : f.Splits
g : R[X]
r : R
hf : f ≠ 0
hg : g ≠ 0
hf0 : ¬f.natDegree = 0
hg0 : ¬g.natDegree = 0
hr : r ≠ 0
⊢ (f.scaleRoots r).resultant (g.scaleRoots r) (f.scaleRoots r).natDegree =
    r ^ (f.natDegree * g.natDegree) * (f.leadingCoeff ^ g.natDegree * (Multiset.map (fun x ↦ eval x g) f.roots).prod)
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
this✝¹ : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R n m k hn).toAlgebra
this✝ : IsDomain (MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ)
this : Algebra (MvPolynomial (Fin n) ℤ) (MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ) :=
  (universalFactorizationMap ℤ n m k hn).toAlgebra
F : MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ →ₐ[ℤ] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R :=
  Algebra.TensorProduct.lift (Algebra.TensorProduct.includeLeft.comp (mapAlgHom (Algebra.ofId ℤ R)))
    ((AlgHom.restrictScalars ℤ Algebra.TensorProduct.includeRight).comp (mapAlgHom (Algebra.ofId ℤ R))) ⋯
H₁ : ∀ (i : Fin m), (universalFactorizationMap R n m k hn).IsIntegralElem (X i ⊗ₜ[R] 1)
H₂ : ∀ (i : Fin k), (universalFactorizationMap R n m k hn).IsIntegralElem (1 ⊗ₜ[R] X i)
⊢ (universalFactorizationMap R n m k hn).IsIntegralElem 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
i : Fin (m + n)
j : Fin m
this : (if ↑j ≤ ↑i then g.coeff (↑i - ↑j) else 0) = if ↑j ≤ ↑i ∧ ↑i ≤ ↑j + n then g.coeff (↑i - ↑j) else 0
⊢ (LinearMap.toMatrix ((degreeLT.basis R m).prod (degreeLT.basis R n)) (degreeLT.basis R (m + n)))
      (f.sylvesterMap g hf hg) i (Sum.inl j) =
    (Matrix.reindex (Equiv.refl (Fin (m + n))) finSumFinEquiv.symm) (f.sylvester g m n) i (Sum.inl j)

Tactic:
by
        simpa [LinearMap.toMatrix_apply, sylvester, coeff_mul_X_pow']

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
i : Fin (m + n)
j : Fin n
this : (if ↑j ≤ ↑i then f.coeff (↑i - ↑j) else 0) = if ↑j ≤ ↑i ∧ ↑i ≤ ↑j + m then f.coeff (↑i - ↑j) else 0
⊢ (LinearMap.toMatrix ((degreeLT.basis R m).prod (degreeLT.basis R n)) (degreeLT.basis R (m + n)))
      (f.sylvesterMap g hf hg) i (Sum.inr j) =
    (Matrix.reindex (Equiv.refl (Fin (m + n))) finSumFinEquiv.symm) (f.sylvester g m n) i (Sum.inr j)

Tactic:
by
        simpa [LinearMap.toMatrix_apply, sylvester, coeff_mul_X_pow']

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

Goal state before:
pp: R : Type u
S : Type v
T : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra.FiniteType R T
inst✝¹ : Algebra.IsIntegral R S
f : S →ₐ[R] T
g : S
hg : Function.Surjective ⇑(awayMapₐ f g)
p : Ideal R
inst✝ : p.IsPrime
hgp : IsUnit (1 ⊗ₜ[R] g)
this✝¹ : IsClosed (PrimeSpectrum.comap (algebraMap R S) '' PrimeSpectrum.zeroLocus {g})
r : R
hpr : { asIdeal := p, isPrime := inst✝ } ∈ ↑(PrimeSpectrum.basicOpen r)
hrg : ↑(PrimeSpectrum.basicOpen r) ⊆ (PrimeSpectrum.comap (algebraMap R S) '' PrimeSpectrum.zeroLocus {g})ᶜ
this✝ : IsLocalization.Away (f.toRingHom ((algebraMap R S) r)) (Away ((algebraMap R T) r))
h₁ : (awayMap (algebraMap R S) r).IsIntegral
x : T
n m' : ℕ
s : S
hs : (algebraMap R S) r ^ m' = g * s
b : S
m : ℕ
e : f b = f g ^ m * x
this : f (s ^ m * b) = f (g * s) ^ m * x
⊢ ∃ a k l, (algebraMap R T) r ^ (l + n) * f a = (algebraMap R T) r ^ (l + k) * x

Tactic:
← hs,

Goal state after:
R : Type u
S : Type v
T : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra.FiniteType R T
inst✝¹ : Algebra.IsIntegral R S
f : S →ₐ[R] T
g : S
hg : Function.Surjective ⇑(awayMapₐ f g)
p : Ideal R
inst✝ : p.IsPrime
hgp : IsUnit (1 ⊗ₜ[R] g)
this✝¹ : IsClosed (PrimeSpectrum.comap (algebraMap R S) '' PrimeSpectrum.zeroLocus {g})
r : R
hpr : { asIdeal := p, isPrime := inst✝ } ∈ ↑(PrimeSpectrum.basicOpen r)
hrg : ↑(PrimeSpectrum.basicOpen r) ⊆ (PrimeSpectrum.comap (algebraMap R S) '' PrimeSpectrum.zeroLocus {g})ᶜ
this✝ : IsLocalization.Away (f.toRingHom ((algebraMap R S) r)) (Away ((algebraMap R T) r))
h₁ : (awayMap (algebraMap R S) r).IsIntegral
x : T
n m' : ℕ
s : S
hs : (algebraMap R S) r ^ m' = g * s
b : S
m : ℕ
e : f b = f g ^ m * x
this : f (s ^ m * b) = f ((algebraMap R S) r ^ m') ^ m * x
⊢ ∃ a k l, (algebraMap R T) r ^ (l + n) * f a = (algebraMap R T) r ^ (l + k) * x
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case neg.refine_2.inr
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.Monic
hf0 : ¬f.natDegree = 0
a b : R[X]
e : a * f + b * g = 1
this : f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
hb0 : a ≠ 0
⊢ 1 = f.resultant b * f.resultant g

Tactic:
rw [← resultant_add_mul_right _ _ a _ _ _ le_rfl, add_comm, mul_comm, e, ← C.map_one] at this
      · simpa [hf.leadingCoeff] using this
      · by_contra! H
        replace H := natDegree_mul_le.trans_lt H
        rw [add_comm, ← hf.natDegree_mul' hb0, mul_comm f] at H
        have := natDegree_add_eq_left_of_natDegree_lt H
        simp only [e, natDegree_one] at this
        lia

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp

Goal state before:
pp: case zero
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : BraidedCategory C
G H : Grp C
inst✝ : IsCommMonObj H.X
f : G ⟶ H
⊢ (f ^ 0).hom = f.hom ^ 0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u_2
S : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
inst✝⁸ : FiniteType R S
inst✝⁷ : CommRing R'
inst✝⁶ : Algebra R R'
inst✝⁵ : CommRing R''
inst✝⁴ : Algebra R R''
inst✝³ : Algebra R'' S
inst✝² : Algebra.IsIntegral R R''
inst✝¹ : IsScalarTower R R'' S
q : Ideal S
P : Ideal R'
inst✝ : P.IsPrime
e : R' ⊗[R] S
e₀ : R' ⊗[R] R''
he₀ : IsIdempotentElem e₀
he₀e : (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)) e₀ = e
P' : Ideal (R' ⊗[R] S)
hP'q : Ideal.comap TensorProduct.includeRight.toRingHom P' = q
H :
  ∀ (P'' : Ideal (R' ⊗[R] R'')),
    P''.IsPrime →
      P''.LiesOver P →
        e₀ ∉ P'' → P'' = Ideal.comap (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)).toRingHom P'
g : R''
hgq : (algebraMap R'' S) g ∉ q
hg : Function.Surjective ⇑(Localization.awayMap (algebraMap R'' S) g)
this : Algebra.IsIntegral R' (Localization.Away e₀)
⊢ ∃ b m,
    (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)).toRingHom b =
      (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)).toRingHom (e₀ * 1 ⊗ₜ[R] g) ^ m * 0

Tactic:
| zero =>

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
T : Type u_3
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : FaithfullyFlat R T
inst✝ : Module.Finite T (T ⊗[R] M)
n : ℕ
s : Fin n → T ⊗[R] M
hs : Submodule.span T (Set.range s) = ⊤
k : Fin n → ℕ
t : (i : Fin n) → Fin (k i) → T
m : (i : Fin n) → Fin (k i) → M
h : ∀ (i : Fin n), s i = ∑ j, t i j ⊗ₜ[R] m i j
f₀ : ((i : Fin n) × Fin (k i) → R) →ₗ[R] M :=
  ((Pi.basisFun R ((i : Fin n) × Fin (k i))).constr R) fun x ↦
    match x with
    | ⟨i, j⟩ => m i j
⊢ ⊤ ≤ ((AlgebraTensorModule.lTensor T T) f₀).range

Tactic:
← hs,

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
T : Type u_3
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : FaithfullyFlat R T
inst✝ : Module.Finite T (T ⊗[R] M)
n : ℕ
s : Fin n → T ⊗[R] M
hs : Submodule.span T (Set.range s) = ⊤
k : Fin n → ℕ
t : (i : Fin n) → Fin (k i) → T
m : (i : Fin n) → Fin (k i) → M
h : ∀ (i : Fin n), s i = ∑ j, t i j ⊗ₜ[R] m i j
f₀ : ((i : Fin n) × Fin (k i) → R) →ₗ[R] M :=
  ((Pi.basisFun R ((i : Fin n) × Fin (k i))).constr R) fun x ↦
    match x with
    | ⟨i, j⟩ => m i j
⊢ Submodule.span T (Set.range s) ≤ ((AlgebraTensorModule.lTensor T T) f₀).range
Module: Mathlib.RingTheory.Finiteness.Descent

Goal state before:
pp: case refine_2.zero
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.FaithfullyFlat R S
I : Ideal R
hI : (Ideal.map (algebraMap R S) I).FG
f : S ⊗[R] ↥I →ₗ[S] S := ↑(AlgebraTensorModule.rid R S S) ∘ₗ (AlgebraTensorModule.lTensor S S) (Submodule.subtype I)
hf : Function.Injective ⇑f
⊢ f 0 ∈ Ideal.map (algebraMap R S) I

Tactic:
| zero =>

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.FaithfullyFlat R S
I : Ideal R
hI : (Ideal.map (algebraMap R S) I).FG
f : S ⊗[R] ↥I →ₗ[S] S := ↑(AlgebraTensorModule.rid R S S) ∘ₗ (AlgebraTensorModule.lTensor S S) (Submodule.subtype I)
hf : Function.Injective ⇑f
this : Ideal.map (algebraMap R S) I = f.range
e : S ⊗[R] ↥I ≃ₗ[S] ↥(Ideal.map (algebraMap R S) I) :=
  LinearEquiv.ofInjective f hf ≪≫ₗ LinearEquiv.ofEq f.range (Ideal.map (algebraMap R S) I) ⋯
⊢ Module.Finite S (S ⊗[R] ↥I)

Tactic:
rwa [Module.Finite.equiv_iff e, Module.Finite.iff_fg]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_3
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Module.FaithfullyFlat R T
inst✝ : FiniteType T (T ⊗[R] S)
s : Finset (T ⊗[R] S)
hs : adjoin T ↑s = ⊤
k : ↥s → ℕ
t : (x : ↥s) → Fin (k x) → T
m : (x : ↥s) → Fin (k x) → S
h : ∀ (x : ↥s), ↑x = ∑ j, t x j ⊗ₜ[R] m x j
f : MvPolynomial ((x : ↥s) × Fin (k x)) R →ₐ[R] S :=
  MvPolynomial.aeval fun x ↦
    match x with
    | ⟨x, i⟩ => m x i
⊢ ⊤ ≤ (TensorProduct.map (AlgHom.id T T) f).range

Tactic:
← hs,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_3
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Module.FaithfullyFlat R T
inst✝ : FiniteType T (T ⊗[R] S)
s : Finset (T ⊗[R] S)
hs : adjoin T ↑s = ⊤
k : ↥s → ℕ
t : (x : ↥s) → Fin (k x) → T
m : (x : ↥s) → Fin (k x) → S
h : ∀ (x : ↥s), ↑x = ∑ j, t x j ⊗ₜ[R] m x j
f : MvPolynomial ((x : ↥s) × Fin (k x)) R →ₐ[R] S :=
  MvPolynomial.aeval fun x ↦
    match x with
    | ⟨x, i⟩ => m x i
⊢ adjoin T ↑s ≤ (TensorProduct.map (AlgHom.id T T) f).range
Module: Mathlib.RingTheory.Ideal.CotangentBaseChange

Goal state before:
pp: case zero
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra R T
I : Ideal S
a : S →+* T ⊗[R] S := Algebra.TensorProduct.includeRight.toRingHom
⊢ ∃ a,
    (tensorCotangentHom R T I) a =
      (map Algebra.TensorProduct.includeRight.toRingHom I).toCotangent
        ⟨(LinearMap.lTensor T (Submodule.restrictScalars R I).subtype) 0, ⋯⟩

Tactic:
| zero =>

Goal state after:
Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange

Goal state before:
pp: case zero
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Extension R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra R T
t : T
s : S
x : Ω[P.Ring⁄R]
⊢ t ⊗ₜ[R] s ⊗ₜ[P.baseChange.Ring]
      (KaehlerDifferential.tensorKaehlerEquiv R T P.Ring P.baseChange.Ring) (1 ⊗ₜ[P.Ring] 0) =
    t ⊗ₜ[R] s ⊗ₜ[P.baseChange.Ring] (KaehlerDifferential.map R T P.Ring P.baseChange.Ring) 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.RingTheory.Etale.Descent

Goal state before:
pp: case left
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_3
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Module.FaithfullyFlat R T
inst✝ : Smooth T (T ⊗[R] S)
this✝¹ : FinitePresentation R S
x✝ : Algebra T (S ⊗[R] T) := TensorProduct.rightAlgebra
e : S ⊗[R] T ≃ₐ[T] T ⊗[R] S := AlgEquiv.ofRingEquiv ⋯
this✝ : FormallySmooth T (S ⊗[R] T)
e' : S ⊗[R] T ⊗[S] Ω[S⁄R] ≃ₗ[S ⊗[R] T] Ω[S ⊗[R] T⁄T] := KaehlerDifferential.tensorKaehlerEquiv R T S (S ⊗[R] T)
this : Module.Flat (S ⊗[R] T) (S ⊗[R] T ⊗[S] Ω[S⁄R])
⊢ Module.Projective S Ω[S⁄R]

Tactic:
have : Module.Flat S Ω[S⁄R] := Module.Flat.of_flat_tensorProduct _ _ (S ⊗[R] T)

Goal state after:
case left
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_3
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Module.FaithfullyFlat R T
inst✝ : Smooth T (T ⊗[R] S)
this✝² : FinitePresentation R S
x✝ : Algebra T (S ⊗[R] T) := TensorProduct.rightAlgebra
e : S ⊗[R] T ≃ₐ[T] T ⊗[R] S := AlgEquiv.ofRingEquiv ⋯
this✝¹ : FormallySmooth T (S ⊗[R] T)
e' : S ⊗[R] T ⊗[S] Ω[S⁄R] ≃ₗ[S ⊗[R] T] Ω[S ⊗[R] T⁄T] := KaehlerDifferential.tensorKaehlerEquiv R T S (S ⊗[R] T)
this✝ : Module.Flat (S ⊗[R] T) (S ⊗[R] T ⊗[S] Ω[S⁄R])
this : Module.Flat S Ω[S⁄R]
⊢ Module.Projective S Ω[S⁄R]
Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange

Goal state before:
pp: case zero
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Extension R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra R T
t : T
⊢ (P.tensorCotangentSpace T) (t ⊗ₜ[R] 0) = t • (CotangentSpace.map (toBaseChange T)) 0

Tactic:
| zero =>

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

Goal state before:
pp: case h.zero
R : Type u
S : Type (max u v)
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Module.Finite R S
p : Ideal R
inst✝ : p.IsPrime
this : IsArtinianRing (p.ResidueField ⊗[R] S)
hpSfin : (p.primesOver S).Finite
IH :
  ∀ m < 0,
    ∀ {R : Type u} {S : Type (max u v)} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
      [Module.Finite R S] (p : Ideal R) [inst_4 : p.IsPrime],
      (p.primesOver S).ncard = m →
        ∃ R' x x_1,
          ∃ (_ : Etale R R'),
            ∃ P,
              ∃ (x_3 : P.IsPrime) (x_4 : P.LiesOver p),
                ∃ n e,
                  ∃ (_ : CompleteOrthogonalIdempotents e),
                    ∃ P',
                      ∃ (_ : ∀ (i : Fin n), (P' i).IsPrime) (_ : ∀ (i : Fin n), (P' i).LiesOver P),
                        Function.Bijective ⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯) ∧
                          (∀ (i : Fin n), e i.castSucc ∉ P' i) ∧
                            ∀ (P'' : Ideal (R' ⊗[R] S)),
                              P''.IsPrime →
                                P''.LiesOver P → e (Fin.last n) ∈ P'' ∧ ∀ (i : Fin n), e i.castSucc ∉ P'' → P'' = P' i
h : (p.primesOver S).ncard = 0
⊢ ∃ R' x x_1,
    ∃ (_ : Etale R R'),
      ∃ P,
        ∃ (x_3 : P.IsPrime) (x_4 : P.LiesOver p),
          ∃ n e,
            ∃ (_ : CompleteOrthogonalIdempotents e),
              ∃ P',
                ∃ (_ : ∀ (i : Fin n), (P' i).IsPrime) (_ : ∀ (i : Fin n), (P' i).LiesOver P),
                  Function.Bijective ⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯) ∧
                    (∀ (i : Fin n), e i.castSucc ∉ P' i) ∧
                      ∀ (P'' : Ideal (R' ⊗[R] S)),
                        P''.IsPrime →
                          P''.LiesOver P → e (Fin.last n) ∈ P'' ∧ ∀ (i : Fin n), e i.castSucc ∉ P'' → P'' = P' i

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommRing R
x : R
hx : x ∈ nonZeroDivisors R
⊢ ord R (x ^ 0) = 0 • ord R x

Tactic:
| zero =>

Goal state after:
Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
⊢ ord R x = ord R y ↔ Associated x y

Tactic:
simp [addVal_eq_iff_associated]

Goal state after: