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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : StandardEtalePresentation R S
x : S
⊢ ∃ p n, x * (aeval P.x) P.g ^ n = (aeval P.x) p

Tactic:
obtain ⟨x, rfl⟩ := (P.equivRing.trans P.P.equivAwayAdjoinRoot).symm.surjective x

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : StandardEtalePresentation R S
x : Localization.Away ((AdjoinRoot.mk P.f) P.g)
⊢ ∃ p n, (P.equivRing.trans P.equivAwayAdjoinRoot).symm x * (aeval P.x) P.g ^ n = (aeval P.x) p
Module: Mathlib.RingTheory.Etale.StandardEtale

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
P : StandardEtalePresentation R S
f₁ f₂ : S →ₐ[R] T
h : f₁ P.x = f₂ P.x
⊢ f₁ = f₂

Tactic:
by
  have : f₁.comp P.equivRing.symm.toAlgHom = f₂.comp P.equivRing.symm.toAlgHom :=
    P.P.hom_ext (by simpa)
  ext x
  obtain ⟨x, rfl⟩ := P.equivRing.symm.surjective x
  exact congr($this x)

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

Goal state before:
pp: R : Type u_1
S : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing B
inst✝ : Algebra R B
φ : S[X] →ₐ[R] B
hφ : Function.Surjective ⇑φ
f : S[X]
hf : f.Monic
hf' : ∀ (i : ℕ), IsIntegral R (f.coeff i)
hfx : RingHom.ker φ.toRingHom = Ideal.span {f}
h✝ : Nontrivial B
hfd : f.natDegree ≠ 0
algInst✝¹ : Algebra S B := (φ.comp C).toAlgebra
this : Nontrivial S
y : S[X]
hy : IsIntegral R (φ y)
S' : Type u_2
w✝⁴ : CommRing S'
w✝³ : Algebra S S'
w✝² : Module.Finite S S'
w✝¹ : Module.Free S S'
w✝ : Nontrivial S'
hS' : (Polynomial.map (algebraMap S S') f).Splits
m : Multiset S'
hm : Polynomial.map (algebraMap S S') f = (Multiset.map (fun x ↦ X - C x) m).prod
algInst✝ : Algebra R S' := ((algebraMap S S').comp (algebraMap R S)).toAlgebra
scalarTowerInst✝ : IsScalarTower R S S' := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R S'))
hm' : ∀ a ∈ m, IsIntegral R a
hmc : m.card = f.natDegree
g : S'[X]
hg :
  Polynomial.map (algebraMap S S') (derivative f * y) -
      (Multiset.map (fun x ↦ (Multiset.map (fun x ↦ X - C x) (m.erase x)).prod * C ((aeval x) y)) m).sum =
    Polynomial.map (algebraMap S S') f * g
⊢ (Multiset.map (fun x ↦ (Multiset.map (fun x ↦ X - C x) (m.erase x)).prod * C ((aeval x) y)) m).sum.natDegree <
    (Polynomial.map (algebraMap S S') f).natDegree

Tactic:
hf.natDegree_map,

Goal state after:
R : Type u_1
S : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing B
inst✝ : Algebra R B
φ : S[X] →ₐ[R] B
hφ : Function.Surjective ⇑φ
f : S[X]
hf : f.Monic
hf' : ∀ (i : ℕ), IsIntegral R (f.coeff i)
hfx : RingHom.ker φ.toRingHom = Ideal.span {f}
h✝ : Nontrivial B
hfd : f.natDegree ≠ 0
algInst✝¹ : Algebra S B := (φ.comp C).toAlgebra
this : Nontrivial S
y : S[X]
hy : IsIntegral R (φ y)
S' : Type u_2
w✝⁴ : CommRing S'
w✝³ : Algebra S S'
w✝² : Module.Finite S S'
w✝¹ : Module.Free S S'
w✝ : Nontrivial S'
hS' : (Polynomial.map (algebraMap S S') f).Splits
m : Multiset S'
hm : Polynomial.map (algebraMap S S') f = (Multiset.map (fun x ↦ X - C x) m).prod
algInst✝ : Algebra R S' := ((algebraMap S S').comp (algebraMap R S)).toAlgebra
scalarTowerInst✝ : IsScalarTower R S S' := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R S'))
hm' : ∀ a ∈ m, IsIntegral R a
hmc : m.card = f.natDegree
g : S'[X]
hg :
  Polynomial.map (algebraMap S S') (derivative f * y) -
      (Multiset.map (fun x ↦ (Multiset.map (fun x ↦ X - C x) (m.erase x)).prod * C ((aeval x) y)) m).sum =
    Polynomial.map (algebraMap S S') f * g
⊢ (Multiset.map (fun x ↦ (Multiset.map (fun x ↦ X - C x) (m.erase x)).prod * C ((aeval x) y)) m).sum.natDegree <
    f.natDegree
Module: Mathlib.RingTheory.Smooth.IntegralClosure

Goal state before:
pp: R : Type u_1
S : Type u_2
B : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : Algebra.IsStandardEtale R S
a : S ⊗[R] B
hx : IsIntegral S a
𝓟 : StandardEtalePresentation R S
e : S ≃ₐ[R] Localization.Away ((AdjoinRoot.mk 𝓟.f) 𝓟.g) := 𝓟.equivRing.trans 𝓟.equivAwayAdjoinRoot
algInst✝ : Algebra (AdjoinRoot 𝓟.f) S :=
  ((↑e.symm).comp (IsScalarTower.toAlgHom R (AdjoinRoot 𝓟.f) (Localization.Away ((AdjoinRoot.mk 𝓟.f) 𝓟.g)))).toAlgebra
this : IsLocalization (Submonoid.powers ((AdjoinRoot.mk 𝓟.f) 𝓟.g)) S
⊢ ∃ n, ∀ (m : ℕ), IsIntegral R ((aeval 𝓟.x) 𝓟.g ^ (n + m) • a)

Tactic:
obtain ⟨⟨_, m, rfl⟩, hm⟩ := IsIntegral.exists_multiple_integral_of_isLocalization
      (R := AdjoinRoot 𝓟.f) (.powers (.mk _ 𝓟.g)) _ hx

Goal state after:
R : Type u_1
S : Type u_2
B : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : Algebra.IsStandardEtale R S
a : S ⊗[R] B
hx : IsIntegral S a
𝓟 : StandardEtalePresentation R S
e : S ≃ₐ[R] Localization.Away ((AdjoinRoot.mk 𝓟.f) 𝓟.g) := 𝓟.equivRing.trans 𝓟.equivAwayAdjoinRoot
algInst✝ : Algebra (AdjoinRoot 𝓟.f) S :=
  ((↑e.symm).comp (IsScalarTower.toAlgHom R (AdjoinRoot 𝓟.f) (Localization.Away ((AdjoinRoot.mk 𝓟.f) 𝓟.g)))).toAlgebra
this : IsLocalization (Submonoid.powers ((AdjoinRoot.mk 𝓟.f) 𝓟.g)) S
m : ℕ
hm : IsIntegral (AdjoinRoot 𝓟.f) (⟨(fun x ↦ (AdjoinRoot.mk 𝓟.f) 𝓟.g ^ x) m, ⋯⟩ • a)
⊢ ∃ n, ∀ (m : ℕ), IsIntegral R ((aeval 𝓟.x) 𝓟.g ^ (n + m) • a)
Module: Mathlib.RingTheory.Polynomial.DegreeLT

Goal state before:
pp: case refine_1
m n : ℕ
R : Type u_2
inst✝ : Ring R
f : ↥R[X]_(m + n)
a✝ : Nontrivial R
⊢ ↑((addLinearEquiv R m n) f).1 + X ^ m * ↑((addLinearEquiv R m n) f).2 = ↑f

pp: case refine_2
m n : ℕ
R : Type u_2
inst✝ : Ring R
f : ↥R[X]_(m + n)
a✝ : Nontrivial R
⊢ (↑((addLinearEquiv R m n) f).1).degree < (X ^ m).degree

Tactic:
· rw [← addLinearEquiv_symm_apply', LinearEquiv.symm_apply_apply]

Goal state after:
case refine_2
m n : ℕ
R : Type u_2
inst✝ : Ring R
f : ↥R[X]_(m + n)
a✝ : Nontrivial R
⊢ (↑((addLinearEquiv R m n) f).1).degree < (X ^ m).degree
Module: Mathlib.RingTheory.Polynomial.DegreeLT

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
r : R
n : ℕ
⊢ Submodule.map (↑↑(taylorEquiv r)) R[X]_n = R[X]_n

Tactic:
← comap_taylorEquiv_degreeLT (r := r),

Goal state after:
R : Type u_1
inst✝ : CommRing R
r : R
n : ℕ
⊢ Submodule.map (↑↑(taylorEquiv r)) (Submodule.comap (↑↑(taylorEquiv r)) R[X]_n) = R[X]_n
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
X✝ Y✝ Z✝ : Y.Opensᵒᵖ
i : X✝ ⟶ Y✝
j : Y✝ ⟶ Z✝
⊢ CommRingCat.ofHom
      ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯ ≫ homOfLE ⋯).op)).restrict
        (integralClosure ↑Γ(Y, Opposite.unop X✝) ↑Γ(X, f ⁻¹ᵁ Opposite.unop X✝))
        (integralClosure ↑Γ(Y, Opposite.unop Z✝) ↑Γ(X, f ⁻¹ᵁ Opposite.unop Z✝)) ⋯) =
    CommRingCat.ofHom
      (((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)).restrict
            (integralClosure ↑Γ(Y, Opposite.unop Y✝) ↑Γ(X, f ⁻¹ᵁ Opposite.unop Y✝))
            (integralClosure ↑Γ(Y, Opposite.unop Z✝) ↑Γ(X, f ⁻¹ᵁ Opposite.unop Z✝)) ⋯).comp
        ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)).restrict
          (integralClosure ↑Γ(Y, Opposite.unop X✝) ↑Γ(X, f ⁻¹ᵁ Opposite.unop X✝))
          (integralClosure ↑Γ(Y, Opposite.unop Y✝) ↑Γ(X, f ⁻¹ᵁ Opposite.unop Y✝)) ⋯))

Tactic:
op_comp

Goal state after:
X Y : Scheme
f : X ⟶ Y
X✝ Y✝ Z✝ : Y.Opensᵒᵖ
i : X✝ ⟶ Y✝
j : Y✝ ⟶ Z✝
⊢ CommRingCat.ofHom
      ((CommRingCat.Hom.hom (X.presheaf.map ((homOfLE ⋯).op ≫ (homOfLE ⋯).op))).restrict
        (integralClosure ↑Γ(Y, Opposite.unop X✝) ↑Γ(X, f ⁻¹ᵁ Opposite.unop X✝))
        (integralClosure ↑Γ(Y, Opposite.unop Z✝) ↑Γ(X, f ⁻¹ᵁ Opposite.unop Z✝)) ⋯) =
    CommRingCat.ofHom
      (((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)).restrict
            (integralClosure ↑Γ(Y, Opposite.unop Y✝) ↑Γ(X, f ⁻¹ᵁ Opposite.unop Y✝))
            (integralClosure ↑Γ(Y, Opposite.unop Z✝) ↑Γ(X, f ⁻¹ᵁ Opposite.unop Z✝)) ⋯).comp
        ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)).restrict
          (integralClosure ↑Γ(Y, Opposite.unop X✝) ↑Γ(X, f ⁻¹ᵁ Opposite.unop X✝))
          (integralClosure ↑Γ(Y, Opposite.unop Y✝) ↑Γ(X, f ⁻¹ᵁ Opposite.unop Y✝)) ⋯))
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case succ.e_a.e_a
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
n : ℕ
⊢ g.coeff (m + 1 + n - m) = g.coeff (n + 1)

Tactic:
simp [add_assoc, add_comm 1]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
n : ℕ
b : Fin (m + 1 + (n + 1))
hb : b ≠ Fin.castAdd (n + 1) (Fin.last m)
⊢ f.sylvester g (m + 1) (n + 1) (Fin.last (m + 1 + n)) b = 0

Tactic:
induction b using Fin.addCases with
    | left b =>
      simp only [Nat.add_eq, Nat.succ_eq_add_one, ne_eq, Fin.ext_iff, Fin.val_castAdd,
        Fin.val_last] at hb
      simp only [sylvester, Set.mem_Icc, Matrix.of_apply, Fin.val_last, Fin.addCases_left,
        ite_eq_right_iff, and_imp]
      intros
      lia
    | right i => simpa [sylvester] using fun _ _ ↦ coeff_eq_zero_of_natDegree_lt (by lia)

Goal state after:
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)
x : S
hx : x ∈ ↑s
⊢ x ∈ ↑(R'.saturation (Submonoid.powers r) ⋯)

Tactic:
refine ⟨_, ⟨s.sup m, rfl⟩, Algebra.subset_adjoin ?_⟩

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)
x : S
hx : x ∈ ↑s
⊢ (fun x ↦ r ^ x) (s.sup m) * x ∈ ↑(Finset.image (⇑f ∘ MvPolynomial.X ∘ Fin.succ) Finset.univ ∪ r ^ s.sup m • s ∪ {r})
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case insert
R : Type u_1
inst✝ : CommRing R
ι : Type u_3
f : ι → R[X]
g : R[X]
n : ℕ
hn : g.natDegree ≤ n
a : ι
s : Finset ι
has : a ∉ s
IH :
  ∏ i ∈ s, (f i).leadingCoeff ≠ 0 →
    (∏ i ∈ s, f i).resultant g (∏ i ∈ s, f i).natDegree n = ∏ i ∈ s, (f i).resultant g (f i).natDegree n
hf : ∏ i ∈ insert a s, (f i).leadingCoeff ≠ 0
hf' : ∏ i ∈ s, (f i).leadingCoeff ≠ 0
⊢ (∏ i ∈ insert a s, f i).resultant g (∏ i ∈ insert a s, f i).natDegree n =
    ∏ i ∈ insert a s, (f i).resultant g (f i).natDegree n

Tactic:
Finset.prod_insert has,

Goal state after:
case insert
R : Type u_1
inst✝ : CommRing R
ι : Type u_3
f : ι → R[X]
g : R[X]
n : ℕ
hn : g.natDegree ≤ n
a : ι
s : Finset ι
has : a ∉ s
IH :
  ∏ i ∈ s, (f i).leadingCoeff ≠ 0 →
    (∏ i ∈ s, f i).resultant g (∏ i ∈ s, f i).natDegree n = ∏ i ∈ s, (f i).resultant g (f i).natDegree n
hf : ∏ i ∈ insert a s, (f i).leadingCoeff ≠ 0
hf' : ∏ i ∈ s, (f i).leadingCoeff ≠ 0
⊢ (f a * ∏ x ∈ s, f x).resultant g (f a * ∏ x ∈ s, f x).natDegree n =
    ∏ i ∈ insert a s, (f i).resultant g (f i).natDegree n
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: case tmul.refine_2
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)
x : MvPolynomial (Fin m) R
y : MvPolynomial (Fin k) R
⊢ (universalFactorizationMap R n m k hn).IsIntegralElem (1 ⊗ₜ[R] y)

Tactic:
induction y using MvPolynomial.induction_on with
      | C a => simpa [← algebraMap_eq, ← algebraMap_apply, Algebra.algebraMap_eq_smul_one] using!
          (universalFactorizationMap R n m k hn).isIntegralElem_map (x := .C a)
      | add p q _ _ => simp only [TensorProduct.tmul_add, RingHom.IsIntegralElem.add, *]
      | mul_X p i IH => simpa [← map_mul] using! IH.mul _ (H₂ i)

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

Goal state before:
pp: 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)
x : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R
⊢ (universalFactorizationMap R n m k hn).IsIntegralElem x

Tactic:
induction x with
  | zero => exact RingHom.isIntegralElem_zero _
  | add x y _ _ => exact RingHom.IsIntegralElem.add _ ‹_› ‹_›
  | tmul x y =>
    suffices (universalFactorizationMap R n m k hn).IsIntegralElem (x ⊗ₜ 1 * 1 ⊗ₜ y) by simpa
    refine RingHom.IsIntegralElem.mul _ ?_ ?_
    · induction x using MvPolynomial.induction_on with
      | C a => simpa using! (universalFactorizationMap R n m k hn).isIntegralElem_map (x := .C a)
      | add p q _ _ => simp only [TensorProduct.add_tmul, RingHom.IsIntegralElem.add, *]
      | mul_X p i IH => simpa [← map_mul] using! IH.mul _ (H₁ i)
    · induction y using MvPolynomial.induction_on with
      | C a => simpa [← algebraMap_eq, ← algebraMap_apply, Algebra.algebraMap_eq_smul_one] using!
          (universalFactorizationMap R n m k hn).isIntegralElem_map (x := .C a)
      | add p q _ _ => simp only [TensorProduct.tmul_add, RingHom.IsIntegralElem.add, *]
      | mul_X p i IH => simpa [← map_mul] using! IH.mul _ (H₂ i)

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

Goal state before:
pp: R : Type u_1
R' : Type u_2
S : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing R'
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R R'
inst✝³ : Algebra R S
p : Ideal R
q : Ideal R'
inst✝² : p.IsPrime
inst✝¹ : q.IsPrime
inst✝ : q.LiesOver p
H : Function.Bijective ⇑(ResidueField.mapₐ p q (Algebra.ofId R R') ⋯)
Q : ↑(q.primesOver (R' ⊗[R] S))
⊢ ↑((fiberIsoOfBijectiveResidueField H) Q) = comap Algebra.TensorProduct.includeRight ↑Q

Tactic:
by
  simpa using! (Ideal.comap_fiberIsoOfBijectiveResidueField_symm H
    (Ideal.fiberIsoOfBijectiveResidueField H Q)).symm

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
X : C
F : Cᵒᵖ ⥤ CommMonCat
α : (F ⋙ forget CommMonCat).RepresentableBy X
this✝ : MonObj X := MonObj.ofRepresentableBy X (F ⋙ forget₂ CommMonCat MonCat) α
this : μ = α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X))
⊢ autoParam
    (α.homEquiv' ((β_ X X).hom ≫ α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X))) =
      α.homEquiv' (α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X))))
    mul_comm._autoParam

Tactic:
α.homEquiv'_comp,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
X : C
F : Cᵒᵖ ⥤ CommMonCat
α : (F ⋙ forget CommMonCat).RepresentableBy X
this✝ : MonObj X := MonObj.ofRepresentableBy X (F ⋙ forget₂ CommMonCat MonCat) α
this : μ = α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X))
⊢ autoParam
    ((ConcreteCategory.hom (F.map (β_ X X).hom.op))
        (α.homEquiv' (α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X)))) =
      α.homEquiv' (α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X))))
    mul_comm._autoParam
Module: Mathlib.AlgebraicGeometry.Group.Abelian

Goal state before:
pp: K : Type u
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
G : Over (Spec (CommRingCat.of K))
inst✝² : IsProper G.hom
inst✝¹ : IsIntegral (G ⊗ G).left
inst✝ : GrpObj G
S : Scheme := Spec (CommRingCat.of K)
point : ↥S := IsLocalRing.closedPoint K
hpoint : IsClosed {point}
this✝⁹ : Nonempty ↥G.left
this✝⁸ : IsProper (G ⊗ G).hom
this✝⁷ : JacobsonSpace ↥(G ⊗ G).left
this✝⁶ : Surjective G.hom
this✝⁵ : IsProper (Over.Hom.left (fst G G))
this✝⁴ : Surjective (Over.Hom.left (fst G G))
this✝³ : IsProper (Over.Hom.left (GrpObj.commutator G) ≫ G.hom)
this✝² : IsClosedImmersion (Over.Hom.left (lift η η) ≫ Over.Hom.left (fst G G))
this✝¹ : IsClosedImmersion (Over.Hom.left (lift η η))
γ : G ⊗ G ⟶ G ⊗ G := lift (fst G G) (GrpObj.commutator G)
this✝ : IsProper (Over.Hom.left γ ≫ Over.Hom.left (fst G G))
this : IsProper (Over.Hom.left γ)
H✝ : ⇑(Over.Hom.left γ) '' ⇑(Over.Hom.left (fst G G)) ⁻¹' {(Over.Hom.left η) point} ⊆ {(Over.Hom.left (lift η η)) point}
U : G.left.Opens
hηU : (Over.Hom.left η) point ∈ U
H : IsFinite ((Scheme.Hom.imageι (Over.Hom.left γ) ≫ Over.Hom.left (fst G G)) ∣_ U)
x : ↥U
⊢ ⇑(pullback.fst G.hom G.hom) ⁻¹' {↑x} ∩ Set.range ⇑(Over.Hom.left γ) ⊆
    ⇑(((Scheme.Hom.imageι (Over.Hom.left γ) ≫ Over.Hom.left (fst G G)) ⁻¹ᵁ U).ι ≫
          Scheme.Hom.imageι (Over.Hom.left γ)) ''
      ⇑((Scheme.Hom.imageι (Over.Hom.left γ) ≫ Over.Hom.left (fst G G)) ∣_ U) ⁻¹' {x}

Tactic:
have : U.ι ⁻¹' {x.1} = {x} := by ext; simp

Goal state after:
K : Type u
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
G : Over (Spec (CommRingCat.of K))
inst✝² : IsProper G.hom
inst✝¹ : IsIntegral (G ⊗ G).left
inst✝ : GrpObj G
S : Scheme := Spec (CommRingCat.of K)
point : ↥S := IsLocalRing.closedPoint K
hpoint : IsClosed {point}
this✝¹⁰ : Nonempty ↥G.left
this✝⁹ : IsProper (G ⊗ G).hom
this✝⁸ : JacobsonSpace ↥(G ⊗ G).left
this✝⁷ : Surjective G.hom
this✝⁶ : IsProper (Over.Hom.left (fst G G))
this✝⁵ : Surjective (Over.Hom.left (fst G G))
this✝⁴ : IsProper (Over.Hom.left (GrpObj.commutator G) ≫ G.hom)
this✝³ : IsClosedImmersion (Over.Hom.left (lift η η) ≫ Over.Hom.left (fst G G))
this✝² : IsClosedImmersion (Over.Hom.left (lift η η))
γ : G ⊗ G ⟶ G ⊗ G := lift (fst G G) (GrpObj.commutator G)
this✝¹ : IsProper (Over.Hom.left γ ≫ Over.Hom.left (fst G G))
this✝ : IsProper (Over.Hom.left γ)
H✝ : ⇑(Over.Hom.left γ) '' ⇑(Over.Hom.left (fst G G)) ⁻¹' {(Over.Hom.left η) point} ⊆ {(Over.Hom.left (lift η η)) point}
U : G.left.Opens
hηU : (Over.Hom.left η) point ∈ U
H : IsFinite ((Scheme.Hom.imageι (Over.Hom.left γ) ≫ Over.Hom.left (fst G G)) ∣_ U)
x : ↥U
this : ⇑U.ι ⁻¹' {↑x} = {x}
⊢ ⇑(pullback.fst G.hom G.hom) ⁻¹' {↑x} ∩ Set.range ⇑(Over.Hom.left γ) ⊆
    ⇑(((Scheme.Hom.imageι (Over.Hom.left γ) ≫ Over.Hom.left (fst G G)) ⁻¹ᵁ U).ι ≫
          Scheme.Hom.imageι (Over.Hom.left γ)) ''
      ⇑((Scheme.Hom.imageι (Over.Hom.left γ) ≫ Over.Hom.left (fst G G)) ∣_ U) ⁻¹' {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
inst✝ : Module.Flat R T
t : T
x : P.Cotangent
⊢ (P.tensorCotangentOfFlat T) (t ⊗ₜ[R] x) = t • (Cotangent.map (toBaseChange T)) x

Tactic:
by
  obtain ⟨x, rfl⟩ := Cotangent.mk_surjective x
  simp only [tensorCotangentOfFlat, LinearEquiv.trans_apply, AlgebraTensorModule.congr_tmul,
    LinearEquiv.refl_apply, LinearEquiv.restrictScalars_apply, cotangentEquivCotangentKer_apply,
    Cotangent.val_mk, Ideal.tensorCotangentEquiv_tmul, map_smul, Cotangent.map_mk,
    Hom.toAlgHom_apply, Ideal.Cotangent.equivOfEq_toCotangent]
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
S : StrictPseudofunctorCore B C
a✝ b✝ c✝ : B
f✝ g✝ : a✝ ⟶ b✝
η : f✝ ⟶ g✝
f : b✝ ⟶ c✝
⊢ S.map₂ (η ▷ f) = (eqToIso ⋯).hom ≫ S.map₂ η ▷ S.map f ≫ (eqToIso ⋯).inv

Tactic:
simpa using S.map₂_whisker_right η f

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor

Goal state before:
pp: B : Type u₁
inst✝⁴ : Bicategory B
C : Type u₂
inst✝³ : Bicategory C
D : Type u₃
inst✝² : Bicategory D
inst✝¹ : Strict B
inst✝ : Strict C
S : StrictPseudofunctorPreCore B C
a✝ b✝ c✝ : B
f✝ g✝ : a✝ ⟶ b✝
η : f✝ ⟶ g✝
f : b✝ ⟶ c✝
⊢ S.map₂ (η ▷ f) = (eqToIso ⋯).hom ≫ S.map₂ η ▷ S.map f ≫ (eqToIso ⋯).inv

Tactic:
simpa using S.map₂_whisker_right η f

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
S : StrictlyUnitaryPseudofunctorCore B C
a✝ b✝ c✝ : B
f✝ g✝ : a✝ ⟶ b✝
η : f✝ ⟶ g✝
f : b✝ ⟶ c✝
⊢ S.map₂ (η ▷ f) = (S.mapComp f✝ f).hom ≫ S.map₂ η ▷ S.map f ≫ (S.mapComp g✝ f).inv

Tactic:
simpa using S.map₂_whisker_right η f

Goal state after: