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

Goal state before:
pp: K : Type u
inst✝ : Field K
x y : K⟮X⟯
⊢ x + y =
    (algebraMap K[X] K⟮X⟯) (x.num * y.denom + x.denom * y.num) /
      ((algebraMap K[X] K⟮X⟯) x.denom * (algebraMap K[X] K⟮X⟯) y.denom)

Tactic:
map_add,

Goal state after:
K : Type u
inst✝ : Field K
x y : K⟮X⟯
⊢ x + y =
    ((algebraMap K[X] K⟮X⟯) (x.num * y.denom) + (algebraMap K[X] K⟮X⟯) (x.denom * y.num)) /
      ((algebraMap K[X] K⟮X⟯) x.denom * (algebraMap K[X] K⟮X⟯) y.denom)
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝ : Field K
x : K⟮X⟯
hx : x ≠ 0
⊢ x⁻¹.denom ∣ x.num

Tactic:
denom_dvd (num_ne_zero hx)

Goal state after:
K : Type u
inst✝ : Field K
x : K⟮X⟯
hx : x ≠ 0
⊢ ∃ p, x⁻¹ = (algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) x.num
Module: Mathlib.RingTheory.Unramified.LocalStructure

Goal state before:
pp: R : Type u_1
S : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
Q : Ideal S
inst✝⁴ : Q.IsPrime
inst✝³ : Module.Finite R S
inst✝² : IsUnramifiedAt R Q
inst✝¹ : Algebra (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra (Ideal.under R Q) Q
p : Ideal R := Ideal.under R Q
this✝³ : p.IsPrime
this✝² : Module p.ResidueField (p.Fiber S) := leftModule
this✝¹ : SMul p.ResidueField (p.Fiber S) := this✝².toSMul
this✝ : IsScalarTower p.ResidueField (p.Fiber S) (p.Fiber S) := IsScalarTower.right
this : Module.Finite p.ResidueField (p.Fiber S) := Module.Finite.base_change R p.ResidueField S
⊢ ∃ t ∉ Q,
    (∀ Q' ∈ (Ideal.under R Q).primesOver S, Q' ≠ Q → t ∈ Q') ∧
      (Ideal.under R Q).ResidueField[(algebraMap S Q.ResidueField) t] = ⊤

Tactic:
have : IsArtinianRing (p.Fiber S) := .of_finite p.ResidueField _

Goal state after:
R : Type u_1
S : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
Q : Ideal S
inst✝⁴ : Q.IsPrime
inst✝³ : Module.Finite R S
inst✝² : IsUnramifiedAt R Q
inst✝¹ : Algebra (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra (Ideal.under R Q) Q
p : Ideal R := Ideal.under R Q
this✝⁴ : p.IsPrime
this✝³ : Module p.ResidueField (p.Fiber S) := leftModule
this✝² : SMul p.ResidueField (p.Fiber S) := this✝³.toSMul
this✝¹ : IsScalarTower p.ResidueField (p.Fiber S) (p.Fiber S) := IsScalarTower.right
this✝ : Module.Finite p.ResidueField (p.Fiber S) := Module.Finite.base_change R p.ResidueField S
this : IsArtinianRing (p.Fiber S)
⊢ ∃ t ∉ Q,
    (∀ Q' ∈ (Ideal.under R Q).primesOver S, Q' ≠ Q → t ∈ Q') ∧
      (Ideal.under R Q).ResidueField[(algebraMap S Q.ResidueField) t] = ⊤
Module: Mathlib.RingTheory.Unramified.LocalStructure

Goal state before:
pp: R : Type u_1
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : Ideal S
inst✝² : p.IsPrime
inst✝¹ : FinitePresentation R S
inst✝ : IsSmoothAt R p
f : S
hfp : f ∉ p
H✝ : IsStandardSmooth R (Localization.Away f)
n : ℕ
φ : MvPolynomial (Fin n) R →+* Localization.Away f
hgC : φ.comp MvPolynomial.C = algebraMap R (Localization.Away f)
hg✝ : φ.Etale
algInst✝ : Algebra (MvPolynomial (Fin n) R) (Localization.Away f) := φ.toAlgebra
algebraizeInst✝ : Etale (MvPolynomial (Fin n) R) (Localization.Away f)
this✝¹ : IsScalarTower R (MvPolynomial (Fin n) R) (Localization.Away f)
this✝ : (Ideal.map (algebraMap S (Localization.Away f)) p).IsPrime
g₀ : Localization.Away f
H : IsStandardEtale (MvPolynomial (Fin n) R) (Localization.Away g₀)
g : S
m : ℕ
hg₀ : IsLocalization.mk' (Localization.Away f) g ⟨(fun x ↦ f ^ x) m, ⋯⟩ = g₀
hg : g ∉ p
this : IsLocalization.Away (f * g) (Localization.Away g₀)
e : Localization.Away g₀ ≃ₐ[S] Localization.Away (f * g) :=
  IsLocalization.algEquiv (Submonoid.powers (f * g)) (Localization.Away g₀) (Localization.Away (f * g))
⊢ ∃ f ∉ p,
    ∃ n x,
      IsScalarTower R (MvPolynomial (Fin n) R) (Localization.Away f) ∧
        IsStandardEtale (MvPolynomial (Fin n) R) (Localization.Away f)

Tactic:
let : Algebra (MvPolynomial (Fin n) R) (Localization.Away (f * g)) :=
    (e.toRingHom.comp (algebraMap (MvPolynomial (Fin n) R) _)).toAlgebra

Goal state after:
R : Type u_1
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : Ideal S
inst✝² : p.IsPrime
inst✝¹ : FinitePresentation R S
inst✝ : IsSmoothAt R p
f : S
hfp : f ∉ p
H✝ : IsStandardSmooth R (Localization.Away f)
n : ℕ
φ : MvPolynomial (Fin n) R →+* Localization.Away f
hgC : φ.comp MvPolynomial.C = algebraMap R (Localization.Away f)
hg✝ : φ.Etale
algInst✝ : Algebra (MvPolynomial (Fin n) R) (Localization.Away f) := φ.toAlgebra
algebraizeInst✝ : Etale (MvPolynomial (Fin n) R) (Localization.Away f)
this✝² : IsScalarTower R (MvPolynomial (Fin n) R) (Localization.Away f)
this✝¹ : (Ideal.map (algebraMap S (Localization.Away f)) p).IsPrime
g₀ : Localization.Away f
H : IsStandardEtale (MvPolynomial (Fin n) R) (Localization.Away g₀)
g : S
m : ℕ
hg₀ : IsLocalization.mk' (Localization.Away f) g ⟨(fun x ↦ f ^ x) m, ⋯⟩ = g₀
hg : g ∉ p
this✝ : IsLocalization.Away (f * g) (Localization.Away g₀)
e : Localization.Away g₀ ≃ₐ[S] Localization.Away (f * g) :=
  IsLocalization.algEquiv (Submonoid.powers (f * g)) (Localization.Away g₀) (Localization.Away (f * g))
this : Algebra (MvPolynomial (Fin n) R) (Localization.Away (f * g)) :=
  (e.toRingEquiv.toRingHom.comp (algebraMap (MvPolynomial (Fin n) R) (Localization.Away g₀))).toAlgebra
⊢ ∃ f ∉ p,
    ∃ n x,
      IsScalarTower R (MvPolynomial (Fin n) R) (Localization.Away f) ∧
        IsStandardEtale (MvPolynomial (Fin n) R) (Localization.Away f)
Module: Mathlib.RingTheory.Polynomial.DegreeLT

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
m n : ℕ
PQ : ↥R[X]_m × ↥R[X]_n
⊢ ↑((addLinearEquiv R m n).symm ((LinearMap.inl R (↥R[X]_m) ↥R[X]_n) PQ.1 + (LinearMap.inr R (↥R[X]_m) ↥R[X]_n) PQ.2)) =
    ↑PQ.1 + ↑PQ.2 * X ^ m

Tactic:
map_add,

Goal state after:
R : Type u_1
inst✝ : Semiring R
m n : ℕ
PQ : ↥R[X]_m × ↥R[X]_n
⊢ ↑((addLinearEquiv R m n).symm ((LinearMap.inl R (↥R[X]_m) ↥R[X]_n) PQ.1) +
        (addLinearEquiv R m n).symm ((LinearMap.inr R (↥R[X]_m) ↥R[X]_n) PQ.2)) =
    ↑PQ.1 + ↑PQ.2 * X ^ m
Module: Mathlib.RingTheory.Polynomial.DegreeLT

Goal state before:
pp: case h
R : Type u_1
inst✝ : CommRing R
r : R
n : ℕ
a✝ : Nontrivial R
i : Fin n
⊢ (X ^ ↑i).leadingCoeff = 1

Tactic:
leadingCoeff_X_pow

Goal state after:
case h
R : Type u_1
inst✝ : CommRing R
r : R
n : ℕ
a✝ : Nontrivial R
i : Fin n
⊢ 1 = 1
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g p : R[X]
m n : ℕ
hp : p.natDegree + m ≤ n
hf : f.natDegree ≤ m
k : ℕ
H : k ≤ n - m + 1
⊢ f.resultant (g + f * ∑ n ∈ Finset.range k, (monomial n) (p.coeff n)) m n = f.resultant g m n

Tactic:
induction k generalizing g with
  | zero =>
    simp only [Finset.range_zero, Finset.sum_empty]
    rw [mul_zero, add_zero]
  | succ k IH =>
    rw [Finset.sum_range_succ, mul_add, ← add_assoc, resultant_add_mul_monomial_right, IH] <;> lia

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g p : R[X]
m n : ℕ
hk : p.natDegree + n ≤ m
hg : g.natDegree ≤ n
⊢ (-1) ^ (m * n) * ((-1) ^ (n * m) * f.resultant g m n) = f.resultant g m n

Tactic:
← mul_assoc,

Goal state after:
R : Type u_1
inst✝ : CommRing R
f g p : R[X]
m n : ℕ
hk : p.natDegree + n ≤ m
hg : g.natDegree ≤ n
⊢ (-1) ^ (m * n) * (-1) ^ (n * m) * f.resultant g m n = f.resultant g m n
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
⊢ IsIntegralHom (fromNormalization f)

Tactic:
rw [IsZariskiLocalAtTarget.iff_of_iSup_eq_top (P := @IsIntegralHom) _
    (iSup_affineOpens_eq_top _)]
  intro U
  let e := IsOpenImmersion.isoOfRangeEq (f.fromNormalization ⁻¹ᵁ U).ι (f.normalizationOpenCover.f U)
      (by simpa using congr($(f.fromNormalization_preimage U).1))
  rw [← MorphismProperty.cancel_left_of_respectsIso @IsIntegralHom e.inv,
    ← MorphismProperty.cancel_right_of_respectsIso @IsIntegralHom _ U.2.isoSpec.hom]
  have : (f.normalizationDiagramMap.app (.op U)).hom.IsIntegral := by
    let := (f.app U).hom.toAlgebra
    change (algebraMap Γ(Y, U) (integralClosure Γ(Y, U) Γ(X, f ⁻¹ᵁ U))).IsIntegral
    exact algebraMap_isIntegral_iff.mpr inferInstance
  convert! IsIntegralHom.SpecMap_iff.mpr this
  rw [← cancel_mono U.2.fromSpec]
  simp [IsAffineOpen.isoSpec_hom, e, ι_fromNormalization]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : Y.Opens
hU : IsAffineOpen U
this✝ : Algebra ↑Γ(Y, U) ↑Γ(X, f ⁻¹ᵁ U) := (CommRingCat.Hom.hom (app f U)).toAlgebra
this : IsIso (app ((normalizationOpenCover f).f ⟨U, hU⟩) (fromNormalization f ⁻¹ᵁ U))
H : ⊤ = ((normalizationOpenCover f).f ⟨U, hU⟩ ≫ fromNormalization f) ⁻¹ᵁ U
⊢ (ΓSpecIso Γ(Y, U)).inv ≫ appLE (Spec.map ((normalizationDiagramMap f).app (Opposite.op U))) ⊤ ⊤ ⋯ =
    CommRingCat.ofHom (algebraMap ↑(Y.presheaf.1 (Opposite.op U)) ↥(integralClosure ↑Γ(Y, U) ↑Γ(X, f ⁻¹ᵁ U))) ≫
      (ΓSpecIso ((normalizationDiagram f).obj (Opposite.op ((toOpensFunctor Y).obj ⟨U, hU⟩)))).inv ≫
        (appIso ((normalizationOpenCover f).f ⟨U, hU⟩) ⊤).inv ≫
          appLE ((normalizationOpenCover f).f ⟨U, hU⟩) ((normalizationOpenCover f).f ⟨U, hU⟩ ''ᵁ ⊤) ⊤ ⋯

Tactic:
simp [Scheme.Hom.appLE, ← ΓSpecIso_inv_naturality]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : Y.Opens
hU : IsAffineOpen U
this✝ : Algebra ↑Γ(Y, U) ↑Γ(X, f ⁻¹ᵁ U) := (CommRingCat.Hom.hom (app f U)).toAlgebra
this : IsIso (app ((normalizationOpenCover f).f ⟨U, hU⟩) (fromNormalization f ⁻¹ᵁ U))
H : ⊤ = ((normalizationOpenCover f).f ⟨U, hU⟩ ≫ fromNormalization f) ⁻¹ᵁ U
⊢ (normalizationDiagramMap f).app (Opposite.op U) ≫ (ΓSpecIso ((normalizationDiagram f).obj (Opposite.op U))).inv =
    CommRingCat.ofHom (algebraMap ↑(Y.presheaf.1 (Opposite.op U)) ↥(integralClosure ↑Γ(Y, U) ↑Γ(X, f ⁻¹ᵁ U))) ≫
      (ΓSpecIso ((normalizationDiagram f).obj (Opposite.op ((toOpensFunctor Y).obj ⟨U, hU⟩)))).inv ≫
        ((normalizationOpenCover f).X ⟨U, hU⟩).presheaf.map (eqToHom ⋯) ≫
          ((normalizationOpenCover f).X ⟨U, hU⟩).presheaf.map (homOfLE ⋯).op
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case inr.inr.inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
hf : f ≠ 0
b : R[X]
r : R
hr : IsUnit r
H : IsCoprime f (C r)
hg : C r ≠ 0
e : 0 * f + b * C r = 1
⊢ ∃ n, f.resultant (C r) ∣ f.leadingCoeff ^ n

Tactic:
simp [hr.pow]

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

Goal state before:
pp: case inr.inr.inr.inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
g : R[X]
hg : g ≠ 0
a : R[X]
ha : a ≠ 0
r : R
hr : IsUnit r
H : IsCoprime (C r) g
hf : C r ≠ 0
e : a * C r + 0 * g = 1
⊢ ∃ n, (C r).resultant g ∣ (C r).leadingCoeff ^ n

Tactic:
simp [hr.pow]

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

Goal state before:
pp: case neg
R✝ : Type u_1
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
hR : IsDomain R
hg0 : ¬g = 0
⊢ (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g

Tactic:
apply mul_right_injective₀ (a := g.leadingCoeff ^ f.natDegree) (by simp [hg0])

Goal state after:
case neg
R✝ : Type u_1
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
hR : IsDomain R
hg0 : ¬g = 0
⊢ (fun x ↦ g.leadingCoeff ^ f.natDegree * x)
      ((f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree) =
    (fun x ↦ g.leadingCoeff ^ f.natDegree * x) (g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case neg
R✝ : Type u_1
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
hR : IsDomain R
hg0 : ¬g = 0
this :
  g.leadingCoeff ^ f.natDegree *
      (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * g.natDegree) * f.resultant g
⊢ g.leadingCoeff ^ (f.natDegree * g.natDegree) * f.resultant g =
    g.leadingCoeff ^ f.natDegree * (g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g)

Tactic:
← mul_assoc,

Goal state after:
case neg
R✝ : Type u_1
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
hR : IsDomain R
hg0 : ¬g = 0
this :
  g.leadingCoeff ^ f.natDegree *
      (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * g.natDegree) * f.resultant g
⊢ g.leadingCoeff ^ (f.natDegree * g.natDegree) * f.resultant g =
    g.leadingCoeff ^ f.natDegree * g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case Splits.mem.inr
R✝ : Type u_1
inst✝² : CommRing R✝
R : Type u_1
inst✝¹ : Field R
f : R[X]
g : R[X]
r s : R
inst✝ : Nontrivial R
⊢ ((taylor r) (X + C s)).resultant ((taylor r) g) = (X + C s).resultant g

Tactic:
map_add,

Goal state after:
case Splits.mem.inr
R✝ : Type u_1
inst✝² : CommRing R✝
R : Type u_1
inst✝¹ : Field R
f : R[X]
g : R[X]
r s : R
inst✝ : Nontrivial R
⊢ ((taylor r) X + (taylor r) (C s)).resultant ((taylor r) g) = (X + C s).resultant g
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case inl
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
⊢ (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:
suffices (if j.1 ≤ i then g.coeff (i - j) else 0) =
      if j ≤ i.1 ∧ ↑i ≤ j + n then g.coeff (i - j) else 0 by
        simpa [LinearMap.toMatrix_apply, sylvester, coeff_mul_X_pow']
    rw [ite_and]
    split_ifs with h₁ h₂ <;> try rfl
    exact coeff_eq_zero_of_natDegree_lt (by lia)

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.degree = 1
⊢ f.discr = 1

Tactic:
by
  rw [← Nat.cast_one, degree_eq_iff_natDegree_eq_of_pos one_pos] at hf
  let e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 1 := finCongr (by lia)
  have : f.sylvesterDeriv.reindex e e = !![1] := by
    have : NeZero (f.natDegree - 1 + f.natDegree) := ⟨by lia⟩
    ext ⟨i, hi⟩ ⟨j, hj⟩
    obtain ⟨rfl⟩ : i = 0 := by lia
    obtain ⟨rfl⟩ : j = 0 := by lia
    simp [e, sylvesterDeriv, mul_comm, hf]
  simp [discr, ← Matrix.det_reindex_self e, this, hf]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
i : ℕ
hi : i < 5
j : ℕ
hj : j < 5
⊢ (if i = 4 then if j = 1 then 1 else if j = 4 then 3 else 0
    else
      if j < 2 then if j ≤ i ∧ i ≤ j + 3 then f.coeff (i - j) else 0
      else if j ≤ i + 2 ∧ i ≤ j - 2 + 2 then f.coeff (i - (j - 2) + 1) * (↑(i - (j - 2)) + 1) else 0) =
    Matrix.vecCons (![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨j, hj⟩)
      (fun i ↦
        Matrix.vecCons (![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨j, hj⟩)
          (fun i ↦
            Matrix.vecCons (![f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, f.coeff 1] ⟨j, hj⟩)
              (fun i ↦
                Matrix.vecCons (![f.coeff 3, f.coeff 2, 0, 3 * f.coeff 3, 2 * f.coeff 2] ⟨j, hj⟩)
                  (fun i ↦ ![0, 1, 0, 0, 3] ⟨j, hj⟩) i)
              i)
          i)
      ⟨i, hi⟩

Tactic:
have hi' : i ∈ Finset.range 5 := Finset.mem_range.mpr hi

Goal state after:
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
i : ℕ
hi : i < 5
j : ℕ
hj : j < 5
hi' : i ∈ Finset.range 5
⊢ (if i = 4 then if j = 1 then 1 else if j = 4 then 3 else 0
    else
      if j < 2 then if j ≤ i ∧ i ≤ j + 3 then f.coeff (i - j) else 0
      else if j ≤ i + 2 ∧ i ≤ j - 2 + 2 then f.coeff (i - (j - 2) + 1) * (↑(i - (j - 2)) + 1) else 0) =
    Matrix.vecCons (![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨j, hj⟩)
      (fun i ↦
        Matrix.vecCons (![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨j, hj⟩)
          (fun i ↦
            Matrix.vecCons (![f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, f.coeff 1] ⟨j, hj⟩)
              (fun i ↦
                Matrix.vecCons (![f.coeff 3, f.coeff 2, 0, 3 * f.coeff 3, 2 * f.coeff 2] ⟨j, hj⟩)
                  (fun i ↦ ![0, 1, 0, 0, 3] ⟨j, hj⟩) i)
              i)
          i)
      ⟨i, hi⟩
Module: Mathlib.RingTheory.Ideal.CotangentBaseChange

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
I : Ideal S
a : S →+* T ⊗[R] S := Algebra.TensorProduct.includeRight.toRingHom
⊢ (tensorCotangentHom R T I) 0 =
    (map Algebra.TensorProduct.includeRight.toRingHom I).toCotangent
      ⟨(LinearMap.lTensor T (Submodule.restrictScalars R I).subtype) 0, ⋯⟩

Tactic:
simp only [map_zero]

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
I : Ideal S
a : S →+* T ⊗[R] S := Algebra.TensorProduct.includeRight.toRingHom
⊢ 0 = (map Algebra.TensorProduct.includeRight.toRingHom I).toCotangent ⟨0, ⋯⟩
Module: Mathlib.RingTheory.Ideal.CotangentBaseChange

Goal state before:
pp: case h
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 := ⋯
t : T
x : ↥(Submodule.restrictScalars R I)
⊢ (tensorCotangentHom R T I) (t ⊗ₜ[R] I.toCotangent x) =
    (map Algebra.TensorProduct.includeRight.toRingHom I).toCotangent
      ⟨(LinearMap.lTensor T (Submodule.restrictScalars R I).subtype) (t ⊗ₜ[R] x), ⋯⟩

Tactic:
apply Ideal.cotangentToQuotientSquare_injective

Goal state after:
case h
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 := ⋯
t : T
x : ↥(Submodule.restrictScalars R I)
⊢ (map Algebra.TensorProduct.includeRight.toRingHom I).cotangentToQuotientSquare
      ((tensorCotangentHom R T I) (t ⊗ₜ[R] I.toCotangent x)) =
    (map Algebra.TensorProduct.includeRight.toRingHom I).cotangentToQuotientSquare
      ((map Algebra.TensorProduct.includeRight.toRingHom I).toCotangent
        ⟨(LinearMap.lTensor T (Submodule.restrictScalars R I).subtype) (t ⊗ₜ[R] x), ⋯⟩)
Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange

Goal state before:
pp: 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✝
P : Extension R S
T : Type u_4
inst✝¹ : CommRing T
inst✝ : Algebra R T
this✝¹ : Algebra P.Ring P.baseChange.Ring := P.algebraBaseChange T
this✝ : Algebra S (T ⊗[R] S) := TensorProduct.rightAlgebra
this : Algebra P.Ring (T ⊗[R] S) := compHom (T ⊗[R] S) (algebraMap P.Ring S)
x : R
⊢ (algebraMap R (T ⊗[R] S)) x = (algebraMap P.Ring (T ⊗[R] S)) ((algebraMap R P.Ring) x)

Tactic:
TensorProduct.algebraMap_apply,

Goal state after:
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✝
P : Extension R S
T : Type u_4
inst✝¹ : CommRing T
inst✝ : Algebra R T
this✝¹ : Algebra P.Ring P.baseChange.Ring := P.algebraBaseChange T
this✝ : Algebra S (T ⊗[R] S) := TensorProduct.rightAlgebra
this : Algebra P.Ring (T ⊗[R] S) := compHom (T ⊗[R] S) (algebraMap P.Ring S)
x : R
⊢ (algebraMap R T) x ⊗ₜ[R] 1 = (algebraMap P.Ring (T ⊗[R] S)) ((algebraMap R P.Ring) x)
Module: Mathlib.Tactic.CategoryTheory.Bicategory.Datatypes

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b : B
f g : a ⟶ b
η : f ≅ g
⊢ η.symm.hom = η.inv

Tactic:
by
  simp only [Iso.symm_hom]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Cat

Goal state before:
pp: C D E F : Cat
G : C ⟶ E
H : D ⟶ F
L₁ : C ⟶ D
R₁ : D ⟶ C
L₂ : E ⟶ F
R₂ : F ⟶ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
f : G ≫ L₂ ⟶ L₁ ≫ H
⊢ ((mateEquiv adj₁ adj₂) f).toNatTrans =
    (CategoryTheory.mateEquiv (Adjunction.ofCat adj₁) (Adjunction.ofCat adj₂)) f.toNatTrans

Tactic:
ext X
  simp [mateEquiv, Adjunction.homEquiv₁, Adjunction.homEquiv₂]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
c d e f : B
g : c ⟶ e
h : d ⟶ f
l₁ : c ⟶ d
r₁ : d ⟶ c
l₂ : e ⟶ f
r₂ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
α : g ≫ l₂ ⟶ l₁ ≫ h
β : r₁ ≫ g ⟶ h ≫ r₂
| (mateEquiv adj₁ adj₂) α = β

Tactic:
rw [eq_comm, ← adj₁.homEquiv₁.symm.injective.eq_iff']

Goal state after:
B : Type u
inst✝ : Bicategory B
c d e f : B
g : c ⟶ e
h : d ⟶ f
l₁ : c ⟶ d
r₁ : d ⟶ c
l₂ : e ⟶ f
r₂ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
α : g ≫ l₂ ⟶ l₁ ≫ h
β : r₁ ≫ g ⟶ h ≫ r₂
| adj₁.homEquiv₁.symm β = ?m.127

B : Type u
inst✝ : Bicategory B
c d e f : B
g : c ⟶ e
h : d ⟶ f
l₁ : c ⟶ d
r₁ : d ⟶ c
l₂ : e ⟶ f
r₂ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
α : g ≫ l₂ ⟶ l₁ ≫ h
β : r₁ ≫ g ⟶ h ≫ r₂
⊢ adj₁.homEquiv₁.symm ((mateEquiv adj₁ adj₂) α) = ?m.127

B : Type u
inst✝ : Bicategory B
c d e f : B
g : c ⟶ e
h : d ⟶ f
l₁ : c ⟶ d
r₁ : d ⟶ c
l₂ : e ⟶ f
r₂ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
α : g ≫ l₂ ⟶ l₁ ≫ h
β : r₁ ≫ g ⟶ h ≫ r₂
⊢ g ⟶ l₁ ≫ h ≫ r₂
Module: Mathlib.RingTheory.Flat.Rank

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (algebraMap R S).finrank = Module.rankAtStalk S

Tactic:
by
  ext
  rw [RingHom.finrank, toAlgebra_algebraMap]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
h : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField (Spec.map φ) y)
inst✝¹ : (CommRingCat.Hom.hom φ).FinitePresentation
inst✝ : (CommRingCat.Hom.hom φ).Flat
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst✝¹ : Algebra.FinitePresentation ↑R ↑S
algebraizeInst✝ : Module.Flat ↑R ↑S
p : Ideal ↑R
hp : p.IsPrime
⊢ (CommRingCat.Hom.hom (CommRingCat.ofHom (algebraMap p.ResidueField (p.Fiber ↑S)))).Smooth

Tactic:
← HasRingHomProperty.Spec_iff (P := @Smooth),

Goal state after:
X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
h : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField (Spec.map φ) y)
inst✝¹ : (CommRingCat.Hom.hom φ).FinitePresentation
inst✝ : (CommRingCat.Hom.hom φ).Flat
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst✝¹ : Algebra.FinitePresentation ↑R ↑S
algebraizeInst✝ : Module.Flat ↑R ↑S
p : Ideal ↑R
hp : p.IsPrime
⊢ Smooth (Spec.map (CommRingCat.ofHom (algebraMap p.ResidueField (p.Fiber ↑S))))
Module: Mathlib.AlgebraicGeometry.Modules.Sheaf

Goal state before:
pp: case refine_2
X Y Z T : Scheme
M N K : X.Modules
φ : M ⟶ N
U✝ V✝ : X.Opens
f✝ : X ⟶ Y
g✝ : Y ⟶ Z
inst✝² : IsOpenImmersion f✝
inst✝¹ : IsOpenImmersion g✝
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U V : (TopologicalSpace.Opens ↥X)ᵒᵖ
g : U ⟶ V
this :
  Y.presheaf.map (homOfLE ⋯).op ≫ (Hom.appIso f (Opposite.unop V)).hom =
    (Hom.appIso f (Opposite.unop U)).hom ≫ X.presheaf.map g
x : ↑(((SheafOfModules.forget X.ringCatSheaf).obj (restrict (unit Y.ringCatSheaf) f)).obj U)
⊢ (ModuleCat.Hom.hom
        (((SheafOfModules.forget X.ringCatSheaf).obj (restrict (unit Y.ringCatSheaf) f)).map g ≫
          (ModuleCat.restrictScalars (RingCat.Hom.hom (X.ringCatSheaf.obj.map g))).map
            (ModuleCat.isoMk
                ((forget₂ CommRingCat RingCat ⋙ forget₂ RingCat Ab).mapIso (Hom.appIso f (Opposite.unop V))) ⋯).hom))
      x =
    (ModuleCat.Hom.hom
        ((ModuleCat.isoMk ((forget₂ CommRingCat RingCat ⋙ forget₂ RingCat Ab).mapIso (Hom.appIso f (Opposite.unop U)))
              ⋯).hom ≫
          ((SheafOfModules.forget X.ringCatSheaf).obj (unit X.ringCatSheaf)).map g))
      x

Tactic:
exact congr($(this) x)

Goal state after: