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

Goal state before:
pp: K : Type u_1
A : Type u
inst✝⁹ : Field K
inst✝⁸ : CommRing A
inst✝⁷ : Algebra K A
B : Type u_3
inst✝⁶ : CommRing B
inst✝⁵ : EssFiniteType K A
inst✝⁴ : FormallyEtale K A
inst✝³ : Algebra K B
inst✝² : EssFiniteType K B
inst✝¹ : FormallyEtale K B
inst✝ : IsSepClosed K
f : A →ₐ[K] B
x : A
p : PrimeSpectrum B
heq : ofId K (B ⧸ p.asIdeal) = (Ideal.quotientMapₐ p.asIdeal f ⋯).comp (ofId K (A ⧸ Ideal.comap f p.asIdeal))
h :
  (Ideal.quotientMapₐ p.asIdeal f ⋯) ((Ideal.Quotient.mk (Ideal.comap f p.asIdeal)) x) =
    (Ideal.Quotient.mk p.asIdeal) (f x)
⊢ (ofId K (B ⧸ p.asIdeal))
      ((AlgEquiv.ofBijective (ofId K (A ⧸ Ideal.comap (↑f) p.asIdeal)) ⋯).symm
        ((Ideal.Quotient.mk (Ideal.comap (↑f) p.asIdeal)) x)) =
    (ofId K (B ⧸ p.asIdeal))
      ((AlgEquiv.ofBijective (ofId K (B ⧸ p.asIdeal)) ⋯).symm ((Ideal.Quotient.mk p.asIdeal) (f x)))

Tactic:
heq

Goal state after:
K : Type u_1
A : Type u
inst✝⁹ : Field K
inst✝⁸ : CommRing A
inst✝⁷ : Algebra K A
B : Type u_3
inst✝⁶ : CommRing B
inst✝⁵ : EssFiniteType K A
inst✝⁴ : FormallyEtale K A
inst✝³ : Algebra K B
inst✝² : EssFiniteType K B
inst✝¹ : FormallyEtale K B
inst✝ : IsSepClosed K
f : A →ₐ[K] B
x : A
p : PrimeSpectrum B
heq : ofId K (B ⧸ p.asIdeal) = (Ideal.quotientMapₐ p.asIdeal f ⋯).comp (ofId K (A ⧸ Ideal.comap f p.asIdeal))
h :
  (Ideal.quotientMapₐ p.asIdeal f ⋯) ((Ideal.Quotient.mk (Ideal.comap f p.asIdeal)) x) =
    (Ideal.Quotient.mk p.asIdeal) (f x)
⊢ ((Ideal.quotientMapₐ p.asIdeal f ⋯).comp (ofId K (A ⧸ Ideal.comap f p.asIdeal)))
      ((AlgEquiv.ofBijective (ofId K (A ⧸ Ideal.comap (↑f) p.asIdeal)) ⋯).symm
        ((Ideal.Quotient.mk (Ideal.comap (↑f) p.asIdeal)) x)) =
    (ofId K (B ⧸ p.asIdeal))
      ((AlgEquiv.ofBijective (ofId K (B ⧸ p.asIdeal)) ⋯).symm ((Ideal.Quotient.mk p.asIdeal) (f x)))
Module: Mathlib.RingTheory.Kaehler.TensorProduct

Goal state before:
pp: case tmul.smul
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : Algebra S B
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R S B
h : Algebra.IsPushout R S A B
z : A
s✝ : S
n✝ : B
e :
  (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) ((algebraMap A B) z * n✝) =
    (algebraMap A B) z • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) n✝ +
      n✝ • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) ((algebraMap A B) z)
⊢ s✝ • (algebraMap A B) z • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) n✝ +
      s✝ • n✝ • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) ((algebraMap A B) z) =
    (algebraMap A B) z • s✝ • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) n✝ +
      (s✝ • n✝) • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) ((algebraMap A B) z)

Tactic:
smul_comm,

Goal state after:
case tmul.smul
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : Algebra S B
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R S B
h : Algebra.IsPushout R S A B
z : A
s✝ : S
n✝ : B
e :
  (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) ((algebraMap A B) z * n✝) =
    (algebraMap A B) z • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) n✝ +
      n✝ • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) ((algebraMap A B) z)
⊢ (algebraMap A B) z • s✝ • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) n✝ +
      s✝ • n✝ • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) ((algebraMap A B) z) =
    (algebraMap A B) z • s✝ • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) n✝ +
      (s✝ • n✝) • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) ((algebraMap A B) z)
Module: Mathlib.RingTheory.Kaehler.TensorProduct

Goal state before:
pp: case tmul
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : Algebra S B
inst✝² : IsScalarTower R A B
inst✝¹ : IsScalarTower R S B
inst✝ : Algebra.IsPushout R S A B
x : S
x✝ y✝ : A
⊢ x • x✝ • 1 ⊗ₜ[R] (D R A) y✝ = x ⊗ₜ[R] (x✝ • (D R A) y✝)

Tactic:
smul_comm,

Goal state after:
case tmul
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : Algebra S B
inst✝² : IsScalarTower R A B
inst✝¹ : IsScalarTower R S B
inst✝ : Algebra.IsPushout R S A B
x : S
x✝ y✝ : A
⊢ x✝ • x • 1 ⊗ₜ[R] (D R A) y✝ = x ⊗ₜ[R] (x✝ • (D R A) y✝)
Module: Mathlib.RingTheory.AdicCompletion.Algebra

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
m n : ℕ
hmn : m ≤ n
r : AdicCauchySequence I R
h : I ^ m = I ^ m • ⊤
⊢ Submodule.Quotient.mk (↑r n) = Submodule.Quotient.mk (↑r m)

Tactic:
h

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
m n : ℕ
hmn : m ≤ n
r : AdicCauchySequence I R
h : I ^ m = I ^ m • ⊤
⊢ Submodule.Quotient.mk (↑r n) = Submodule.Quotient.mk (↑r m)
Module: Mathlib.RingTheory.AdicCompletion.Algebra

Goal state before:
pp: S : Type u_5
inst✝¹ : CommRing S
I : Ideal S
inst✝ : IsAdicComplete I S
n : ℕ
x : AdicCompletion I S
⊢ (Ideal.Quotient.mk (I ^ n)) ((ofAlgEquiv I).symm x) = ↑(Ideal.quotientEquivAlgOfEq S ⋯) ((eval I S n) x)

Tactic:
rw [← mk_smul_top_ofAlgEquiv_symm I n x]

Goal state after:
S : Type u_5
inst✝¹ : CommRing S
I : Ideal S
inst✝ : IsAdicComplete I S
n : ℕ
x : AdicCompletion I S
⊢ (Ideal.Quotient.mk (I ^ n)) ((ofAlgEquiv I).symm x) =
    ↑(Ideal.quotientEquivAlgOfEq S ⋯) ((Ideal.Quotient.mk (I ^ n • ⊤)) ((ofAlgEquiv I).symm x))
Module: Mathlib.RingTheory.Smooth.AdicCompletion

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
I : Ideal S
f : A →ₐ[R] S ⧸ I
inst✝ : FormallySmooth R A
m n : ℕ
hn : m ≤ n
⊢ (Ideal.Quotient.factorₐ R ⋯).comp (liftAdicCompletionAux I f n) = liftAdicCompletionAux I f m

Tactic:
induction n, hn using Nat.le_induction with

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Exact

Goal state before:
pp: R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup K
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R K
inst✝² : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
hfg : Function.Exact ⇑f ⇑g
hf : Function.Injective ⇑f
q : Submodule R M
E : Type u_8
inst✝¹ : AddCommGroup E
inst✝ : Module R E
i : E →ₗ[R] M
hi : Function.Injective ⇑i
h : IsCompl i.range q
hker : Disjoint g.ker q
hmap : Submodule.map g q = ⊤
⊢ Function.Bijective (⇑↑(LinearEquiv.ofInjective i hi).symm ∘ ⇑(i.range.projectionOnto q h ∘ₗ f))

Tactic:
Function.Bijective.of_comp_iff

Goal state after:
R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup K
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R K
inst✝² : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
hfg : Function.Exact ⇑f ⇑g
hf : Function.Injective ⇑f
q : Submodule R M
E : Type u_8
inst✝¹ : AddCommGroup E
inst✝ : Module R E
i : E →ₗ[R] M
hi : Function.Injective ⇑i
h : IsCompl i.range q
hker : Disjoint g.ker q
hmap : Submodule.map g q = ⊤
⊢ Function.Bijective ⇑↑(LinearEquiv.ofInjective i hi).symm

case hg
R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup K
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R K
inst✝² : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
hfg : Function.Exact ⇑f ⇑g
hf : Function.Injective ⇑f
q : Submodule R M
E : Type u_8
inst✝¹ : AddCommGroup E
inst✝ : Module R E
i : E →ₗ[R] M
hi : Function.Injective ⇑i
h : IsCompl i.range q
hker : Disjoint g.ker q
hmap : Submodule.map g q = ⊤
⊢ Function.Bijective ⇑(i.range.projectionOnto q h ∘ₗ f)
Module: Mathlib.RingTheory.Smooth.StandardSmooth

Goal state before:
pp: n m : ℕ
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : Finite σ
T : Type u_1
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : IsStandardSmooth R S
⊢ ∃ ι σ, ∃ (x : Finite σ), Finite ι ∧ Nonempty (SubmersivePresentation T (T ⊗[R] S) ι σ)

Tactic:
obtain ⟨ι, σ, _, _, ⟨P⟩⟩ := ‹IsStandardSmooth R S›
    exact ⟨ι, σ, _, inferInstance, ⟨P.baseChange T⟩⟩

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

Goal state before:
pp: case hli
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
ι : Type u_3
σ : Type u_4
P : PreSubmersivePresentation R S ι σ
inst✝ : Finite σ
b : Module.Basis σ S P.toExtension.Cotangent
hb : ∀ (r : σ), b r = Extension.Cotangent.mk ⟨P.relation r, ⋯⟩
h : Function.Bijective ⇑(P.cotangentRestrict ⋯)
heq :
  (fun j i ↦ (aeval P.val) ((pderiv (P.map i)) (P.relation j))) =
    ⇑(Finsupp.linearEquivFunOnFinite S S σ) ∘ ⇑(P.cotangentRestrict ⋯) ∘ ⇑b
⊢ LinearIndependent S fun j i ↦ (aeval P.val) ((pderiv (P.map i)) (P.relation j))

Tactic:
heq

Goal state after:
case hli
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
ι : Type u_3
σ : Type u_4
P : PreSubmersivePresentation R S ι σ
inst✝ : Finite σ
b : Module.Basis σ S P.toExtension.Cotangent
hb : ∀ (r : σ), b r = Extension.Cotangent.mk ⟨P.relation r, ⋯⟩
h : Function.Bijective ⇑(P.cotangentRestrict ⋯)
heq :
  (fun j i ↦ (aeval P.val) ((pderiv (P.map i)) (P.relation j))) =
    ⇑(Finsupp.linearEquivFunOnFinite S S σ) ∘ ⇑(P.cotangentRestrict ⋯) ∘ ⇑b
⊢ LinearIndependent S (⇑(Finsupp.linearEquivFunOnFinite S S σ) ∘ ⇑(P.cotangentRestrict ⋯) ∘ ⇑b)
Module: Mathlib.RingTheory.Extension.Cotangent.LocalizationAway

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
Q : Generators S T Unit := localizationAway T g
algInst✝ : Algebra P.Ring ((localizationAway T g).comp P).Ring := ((localizationAway T g).toComp P).toAlgHom.toAlgebra
f : P.Ring ⧸ P.ker ^ 2 := (Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)
⊢ Function.Injective ⇑(LinearMap.liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom))

Tactic:
let π := compLocalizationAwayAlgHom T g P

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
Q : Generators S T Unit := localizationAway T g
algInst✝ : Algebra P.Ring ((localizationAway T g).comp P).Ring := ((localizationAway T g).toComp P).toAlgHom.toAlgebra
f : P.Ring ⧸ P.ker ^ 2 := (Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)
π : ((localizationAway T g).comp P).Ring →ₐ[R] Localization.Away ((Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)) :=
  compLocalizationAwayAlgHom T g P
⊢ Function.Injective ⇑(LinearMap.liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom))
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Projective F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ≠ Q x * P z
⊢ ¬?a = ?b

pp: case a
F : Type u
inst✝¹ : Field F
W : Projective F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ≠ Q x * P z
⊢ ?m.167

pp: case b
F : Type u
inst✝¹ : Field F
W : Projective F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ≠ Q x * P z
⊢ ?m.167

pp: F : Type u
inst✝¹ : Field F
W : Projective F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ≠ Q x * P z
⊢ Type ?u.152

Tactic:
← X_eq_iff hPz hQz

Goal state after:
F : Type u
inst✝¹ : Field F
W : Projective F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ≠ Q x * P z
⊢ ¬P x * Q z = Q x * P z
Module: Mathlib.RingTheory.Smooth.Flat

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : IsNoetherianRing R
inst✝ : Smooth R A
⊢ Module.Flat R A

Tactic:
by
  obtain ⟨k, f, hf⟩ := (FiniteType.iff_quotient_mvPolynomial'' (R := R) (S := A)).mp inferInstance
  exact FormallySmooth.flat_of_algHom_of_isNoetherianRing f hf

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

Goal state before:
pp: case refine_3
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ✝ : Type u_3
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
⊢ IsUnit ((algebraMap P.Ring S) D.g)

Tactic:
suffices h : (algebraMap P.Ring S) D.g = 1 by simp [h]

Goal state after:
case refine_3
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ✝ : Type u_3
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
⊢ (algebraMap P.Ring S) D.g = 1
Module: Mathlib.RingTheory.Extension.Cotangent.Basis

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
⊢ D.presLeft.ker ≤ P.ker

Tactic:
by
  intro x hx
  simpa only [toExtension_commRing, toExtension_Ring, RingHom.mem_ker,
    toExtension_algebra₂, algebraMap_apply, Ideal.Quotient.algebraMap_eq,
    map_zero] using! (algebraMap D.T S).congr_arg hx

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

Goal state before:
pp: case e_6
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
inst✝ : Nontrivial S
this : Nontrivial (MvPolynomial ι R ⧸ Ideal.span (Set.range (Subtype.val ∘ D.f ∘ ⇑b)))
⊢ ((localizationAway S D.gbar).ofComp D.presLeft.toGenerators).toAlgHom (D.pres.relation (Sum.inl ())) =
    C D.gbar * X () - 1

Tactic:
pres,

Goal state after:
case e_6
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
inst✝ : Nontrivial S
this : Nontrivial (MvPolynomial ι R ⧸ Ideal.span (Set.range (Subtype.val ∘ D.f ∘ ⇑b)))
⊢ ((localizationAway S D.gbar).ofComp D.presLeft.toGenerators).toAlgHom
      ((D.presRight.comp D.presLeft).relation (Sum.inl ())) =
    C D.gbar * X () - 1
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ W'.addX P P = 0

Tactic:
by
  rw [addX]
  ring1

Goal state after:
Module: Mathlib.RingTheory.RingHom.LocallyStandardSmooth

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.IsStandardSmooth
algInst✝ : Algebra R S := f.toAlgebra
algebraizeInst✝ : Algebra.IsStandardSmooth R S
⊢ f.Smooth

Tactic:
RingHom.Smooth

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.IsStandardSmooth
algInst✝ : Algebra R S := f.toAlgebra
algebraizeInst✝ : Algebra.IsStandardSmooth R S
⊢ Algebra.Smooth R S
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : (aeval a) F = 0
⊢ Irreducible F

Tactic:
by
  refine ⟨fun h' ↦ (h'.map (aeval a)).ne_zero hFa, fun q₁ q₂ e ↦ ?_⟩
  wlog h₁ : aeval a q₁ = 0 generalizing q₁ q₂
  · exact .symm (this q₂ q₁ (e.trans (mul_comm ..)) <| by
      simpa [h₁, hFa] using Eq.symm <| congr(aeval a $e))
  have ne := mul_ne_zero_iff.mp (e ▸ hF0)
  have := HF q₁ ne.1 h₁
  rw [e, totalDegree_mul_of_isDomain ne.1 ne.2, add_le_iff_nonpos_right, nonpos_iff_eq_zero] at this
  refine .inr (isUnit_iff_totalDegree_of_isReduced.mpr ⟨?_, this⟩)
  rw [totalDegree_eq_zero_iff_eq_C.mp this] at ne
  simpa using ne.2

Goal state after:
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
p : ℕ
hp : Nat.Prime p
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : (aeval a) F = 0
this : ∀ (i : ι), ∀ σ ∈ F.support, p ∣ σ i
σ' : (ι →₀ ℕ) → ι →₀ ℕ
hσ' : ∀ σ ∈ F.support, σ = p • σ' σ
hσ'' : ∀ (σ : ↥F.support), ↑σ = p • σ' ↑σ
H : ∀ (ι : Type u_3) (x : Fintype ι) (v : ι → K), LinearIndependent k v → LinearIndependent k fun x ↦ v x ^ p
F' : ↥F.support →₀ k
hF' : (Finsupp.linearCombination k fun s ↦ (aeval a) ((monomial (σ' ↑s)) 1)) F' = 0
hF'0 : ¬F' = 0
F'' : MvPolynomial ι k := AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain (fun s ↦ σ' ↑s) F')
s t : ↥F.support
h : σ' ↑s = σ' ↑t
i : ι
⊢ (p • σ' ↑s) i = (p • σ' ↑t) i

Tactic:
h

Goal state after:
k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
p : ℕ
hp : Nat.Prime p
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : (aeval a) F = 0
this : ∀ (i : ι), ∀ σ ∈ F.support, p ∣ σ i
σ' : (ι →₀ ℕ) → ι →₀ ℕ
hσ' : ∀ σ ∈ F.support, σ = p • σ' σ
hσ'' : ∀ (σ : ↥F.support), ↑σ = p • σ' ↑σ
H : ∀ (ι : Type u_3) (x : Fintype ι) (v : ι → K), LinearIndependent k v → LinearIndependent k fun x ↦ v x ^ p
F' : ↥F.support →₀ k
hF' : (Finsupp.linearCombination k fun s ↦ (aeval a) ((monomial (σ' ↑s)) 1)) F' = 0
hF'0 : ¬F' = 0
F'' : MvPolynomial ι k := AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain (fun s ↦ σ' ↑s) F')
s t : ↥F.support
h : σ' ↑s = σ' ↑t
i : ι
⊢ (p • σ' ↑t) i = (p • σ' ↑t) i
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
p : ℕ
hp : Nat.Prime p
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : (aeval a) F = 0
this : ∀ (i : ι), ∀ σ ∈ F.support, p ∣ σ i
σ' : (ι →₀ ℕ) → ι →₀ ℕ
hσ' : ∀ σ ∈ F.support, σ = p • σ' σ
hσ'' : ∀ (σ : ↥F.support), ↑σ = p • σ' ↑σ
H : ∀ (ι : Type u_3) (x : Fintype ι) (v : ι → K), LinearIndependent k v → LinearIndependent k fun x ↦ v x ^ p
F' : ↥F.support →₀ k
hF' : (Finsupp.linearCombination k fun s ↦ (aeval a) ((monomial (σ' ↑s)) 1)) F' = 0
hF'0 : ¬F' = 0
F'' : MvPolynomial ι k := AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain (fun s ↦ σ' ↑s) F')
hF''0 : F'' ≠ 0
hF'' : (aeval a) F'' = 0
σ : ι →₀ ℕ
hσ : σ ∈ F''.support
⊢ (p * σ.sum fun x e ↦ e) ≤ F.totalDegree

Tactic:
obtain ⟨σ, hσ₂, rfl⟩ := Finset.mem_image.mp (Finsupp.mapDomain_support hσ)

Goal state after:
k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
p : ℕ
hp : Nat.Prime p
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : (aeval a) F = 0
this : ∀ (i : ι), ∀ σ ∈ F.support, p ∣ σ i
σ' : (ι →₀ ℕ) → ι →₀ ℕ
hσ' : ∀ σ ∈ F.support, σ = p • σ' σ
hσ'' : ∀ (σ : ↥F.support), ↑σ = p • σ' ↑σ
H : ∀ (ι : Type u_3) (x : Fintype ι) (v : ι → K), LinearIndependent k v → LinearIndependent k fun x ↦ v x ^ p
F' : ↥F.support →₀ k
hF' : (Finsupp.linearCombination k fun s ↦ (aeval a) ((monomial (σ' ↑s)) 1)) F' = 0
hF'0 : ¬F' = 0
F'' : MvPolynomial ι k := AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain (fun s ↦ σ' ↑s) F')
hF''0 : F'' ≠ 0
hF'' : (aeval a) F'' = 0
σ : ↥F.support
hσ₂ : σ ∈ F'.support
hσ : σ' ↑σ ∈ F''.support
⊢ (p * (σ' ↑σ).sum fun x e ↦ e) ≤ F.totalDegree
Module: Mathlib.CategoryTheory.MorphismProperty.Descent

Goal state before:
pp: case hfst
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
P✝ Q✝ W : MorphismProperty C
A X✝ Y✝ Z✝ : C
fst : A ⟶ X✝
snd : A ⟶ Y✝
f✝ : X✝ ⟶ Z✝
g✝ : Y✝ ⟶ Z✝
inst✝⁴ : HasPullbacks C
P Q : MorphismProperty C
inst✝³ : P.DescendsAlong Q
inst✝² : P.RespectsIso
inst✝¹ : Q.IsStableUnderBaseChange
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
hf : Q f
hfst : P.diagonal (pullback.fst f g)
heq :
  pullback.fst (pullback.fst (pullback.snd g g ≫ g) f) (pullback.diagonal g) =
    (pullbackSymmetry (pullback.fst (pullback.snd g g ≫ g) f) (pullback.diagonal g)).hom ≫
      (pullbackRightPullbackFstIso (pullback.snd g g ≫ g) f (pullback.diagonal g)).hom ≫
        (pullback.congrHom ⋯ ⋯).hom ≫
          (pullbackSymmetry g f).hom ≫ pullback.diagonal (pullback.fst f g) ≫ (diagonalObjPullbackFstIso f g).hom
⊢ P (pullback.fst (pullback.fst (pullback.snd g g ≫ g) f) (pullback.diagonal g))

Tactic:
heq

Goal state after:
case hfst
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
P✝ Q✝ W : MorphismProperty C
A X✝ Y✝ Z✝ : C
fst : A ⟶ X✝
snd : A ⟶ Y✝
f✝ : X✝ ⟶ Z✝
g✝ : Y✝ ⟶ Z✝
inst✝⁴ : HasPullbacks C
P Q : MorphismProperty C
inst✝³ : P.DescendsAlong Q
inst✝² : P.RespectsIso
inst✝¹ : Q.IsStableUnderBaseChange
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
hf : Q f
hfst : P.diagonal (pullback.fst f g)
heq :
  pullback.fst (pullback.fst (pullback.snd g g ≫ g) f) (pullback.diagonal g) =
    (pullbackSymmetry (pullback.fst (pullback.snd g g ≫ g) f) (pullback.diagonal g)).hom ≫
      (pullbackRightPullbackFstIso (pullback.snd g g ≫ g) f (pullback.diagonal g)).hom ≫
        (pullback.congrHom ⋯ ⋯).hom ≫
          (pullbackSymmetry g f).hom ≫ pullback.diagonal (pullback.fst f g) ≫ (diagonalObjPullbackFstIso f g).hom
⊢ P
    ((pullbackSymmetry (pullback.fst (pullback.snd g g ≫ g) f) (pullback.diagonal g)).hom ≫
      (pullbackRightPullbackFstIso (pullback.snd g g ≫ g) f (pullback.diagonal g)).hom ≫
        (pullback.congrHom ⋯ ⋯).hom ≫
          (pullbackSymmetry g f).hom ≫ pullback.diagonal (pullback.fst f g) ≫ (diagonalObjPullbackFstIso f g).hom)
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent

Goal state before:
pp: case H
R S : CommRingCat
Y : Scheme
φ : R ⟶ S
g : Y ⟶ Spec R
⊢ (@Surjective ⊓ @Flat) (Spec.map φ) → isomorphisms Scheme (pullback.fst (Spec.map φ) g) → isomorphisms Scheme g

Tactic:
h

Goal state after:
case H
R S : CommRingCat
Y : Scheme
φ : R ⟶ S
g : Y ⟶ Spec R
h : (@Surjective ⊓ @Flat) (Spec.map φ)
⊢ isomorphisms Scheme (pullback.fst (Spec.map φ) g) → isomorphisms Scheme g
Module: Mathlib.AlgebraicGeometry.Morphisms.Descent

Goal state before:
pp: P P' : MorphismProperty Scheme
inst✝³ : P'.IsStableUnderBaseChange
inst✝² : P'.IsStableUnderComposition
inst✝¹ : P.IsStableUnderBaseChange
H₁ : @IsLocalIso ⊓ @Surjective ≤ P'
inst✝ : IsZariskiLocalAtTarget P
H :
  ∀ {R S : CommRingCat} {Y : Scheme} (φ : R ⟶ S) (g : Y ⟶ Spec R),
    P' (Spec.map φ) → P (pullback.fst (Spec.map φ) g) → P g
R : CommRingCat
X Y : Scheme
f : X ⟶ Spec R
g : Y ⟶ Spec R
hf : (P' ⊓ @QuasiCompact) f
⊢ P (pullback.fst f g) → P g

Tactic:
h

Goal state after:
P P' : MorphismProperty Scheme
inst✝³ : P'.IsStableUnderBaseChange
inst✝² : P'.IsStableUnderComposition
inst✝¹ : P.IsStableUnderBaseChange
H₁ : @IsLocalIso ⊓ @Surjective ≤ P'
inst✝ : IsZariskiLocalAtTarget P
H :
  ∀ {R S : CommRingCat} {Y : Scheme} (φ : R ⟶ S) (g : Y ⟶ Spec R),
    P' (Spec.map φ) → P (pullback.fst (Spec.map φ) g) → P g
R : CommRingCat
X Y : Scheme
f : X ⟶ Spec R
g : Y ⟶ Spec R
hf : (P' ⊓ @QuasiCompact) f
h : P (pullback.fst f g)
⊢ P g
Module: Mathlib.RingTheory.RingHom.OpenImmersion

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
h : Function.Bijective ⇑(algebraMap R S)
⊢ IsStandardOpenImmersion R S

Tactic:
rw [Algebra.isStandardOpenImmersion_iff]

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
h : Function.Bijective ⇑(algebraMap R S)
⊢ ∃ r, Away r S