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

Goal state before:
pp: R : Type u_1
I : Type u_2
inst✝⁵ : Finite I
f : I → Type u_3
inst✝⁴ : CommRing R
inst✝³ : (i : I) → CommRing (f i)
inst✝² : (i : I) → Algebra R (f i)
val✝ : Fintype I
H✝ : ∀ (i : I), FormallyUnramified R (f i)
B : Type (max u_2 u_3)
inst✝¹ : CommRing B
inst✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
f₁ f₂ : ((i : I) → f i) →ₐ[R] B
e✝ : (Ideal.Quotient.mkₐ R J).comp f₁ = (Ideal.Quotient.mkₐ R J).comp f₂
g : (i : I) → f i
x : I
hf : ∀ (x : (i : I) → f i), f₁ x - f₂ x ∈ J
e : (i : I) → f i := Pi.single x 1
he : IsIdempotentElem e
h₁ : f₁ e * (1 - f₂ e) = 0
h₂ : f₂ e * (1 - f₁ e) = 0
H : f₁ e = f₂ e
J' : Ideal B := Ideal.span {1 - f₁ e}
f₁' : f x →ₐ[R] B ⧸ J' :=
  AlgHom.ofLinearMap (((Ideal.Quotient.mkₐ R J').comp f₁).toLinearMap ∘ₗ LinearMap.single R f x) ⋯ ⋯
f₂' : f x →ₐ[R] B ⧸ J' :=
  AlgHom.ofLinearMap (((Ideal.Quotient.mkₐ R J').comp f₂).toLinearMap ∘ₗ LinearMap.single R f x) ⋯ ⋯
this : f₁' = f₂'
⊢ f₁ (Pi.single x (g x)) = f₂ (Pi.single x (g x))

Tactic:
have := AlgHom.congr_fun this (g x)

Goal state after:
R : Type u_1
I : Type u_2
inst✝⁵ : Finite I
f : I → Type u_3
inst✝⁴ : CommRing R
inst✝³ : (i : I) → CommRing (f i)
inst✝² : (i : I) → Algebra R (f i)
val✝ : Fintype I
H✝ : ∀ (i : I), FormallyUnramified R (f i)
B : Type (max u_2 u_3)
inst✝¹ : CommRing B
inst✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
f₁ f₂ : ((i : I) → f i) →ₐ[R] B
e✝ : (Ideal.Quotient.mkₐ R J).comp f₁ = (Ideal.Quotient.mkₐ R J).comp f₂
g : (i : I) → f i
x : I
hf : ∀ (x : (i : I) → f i), f₁ x - f₂ x ∈ J
e : (i : I) → f i := Pi.single x 1
he : IsIdempotentElem e
h₁ : f₁ e * (1 - f₂ e) = 0
h₂ : f₂ e * (1 - f₁ e) = 0
H : f₁ e = f₂ e
J' : Ideal B := Ideal.span {1 - f₁ e}
f₁' : f x →ₐ[R] B ⧸ J' :=
  AlgHom.ofLinearMap (((Ideal.Quotient.mkₐ R J').comp f₁).toLinearMap ∘ₗ LinearMap.single R f x) ⋯ ⋯
f₂' : f x →ₐ[R] B ⧸ J' :=
  AlgHom.ofLinearMap (((Ideal.Quotient.mkₐ R J').comp f₂).toLinearMap ∘ₗ LinearMap.single R f x) ⋯ ⋯
this✝ : f₁' = f₂'
this : f₁' (g x) = f₂' (g x)
⊢ f₁ (Pi.single x (g x)) = f₂ (Pi.single x (g x))
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W'.negY Q * P z
⊢ P z * (P y - W'.negY P) ^ 3 = 0

Tactic:
Y_eq_negY_of_Y_eq hQz hx hy hy',

Goal state after:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W'.negY Q * P z
⊢ P z * (W'.negY P - W'.negY P) ^ 3 = 0
Module: Mathlib.RingTheory.Etale.Field

Goal state before:
pp: case refine_2
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsSeparable K L
B : Type (max u_1 u_2)
x✝¹ : CommRing B
x✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
g : (k : L) → ↥K⟮k⟯ →ₐ[K] B
hg₁ : ∀ (k : L), (fun g ↦ (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) (g k)
hg₂ :
  ∀ (k : L) (y : ↥K⟮k⟯ →ₐ[K] B),
    (fun g ↦ (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) y → y = g k
hg₃ : ∀ (x y : L) (h : x ∈ K⟮y⟯), (g y) ⟨x, h⟩ = (g x) (IntermediateField.AdjoinSimple.gen K x)
H : ∀ (x y : L), ∃ α, x ∈ K⟮α⟯ ∧ y ∈ K⟮α⟯
⊢ ∀ (x y : L),
    { toFun := fun x ↦ (g x) (IntermediateField.AdjoinSimple.gen K x), map_one' := ⋯ }.toFun (x * y) =
      { toFun := fun x ↦ (g x) (IntermediateField.AdjoinSimple.gen K x), map_one' := ⋯ }.toFun x *
        { toFun := fun x ↦ (g x) (IntermediateField.AdjoinSimple.gen K x), map_one' := ⋯ }.toFun y

Tactic:
intro x y
    obtain ⟨α, hx, hy⟩ := H x y
    simp only [← hg₃ _ _ hx, ← hg₃ _ _ hy, ← map_mul, ← hg₃ _ _ (mul_mem hx hy)]
    rfl

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

Goal state before:
pp: R : Type u_1
I : Type u_2
A : I → Type u_3
inst✝³ : CommRing R
inst✝² : (i : I) → CommRing (A i)
inst✝¹ : (i : I) → Algebra R (A i)
inst✝ : Finite I
val✝ : Fintype I
H : ∀ (i : I), FormallySmooth R (A i)
B : Type (max u_1 u_2 u_3)
x✝² : CommRing B
x✝¹ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
g : ((i : I) → A i) →ₐ[R] B ⧸ J
hJ' : ∀ x ∈ RingHom.ker (Ideal.Quotient.mk J), IsNilpotent x
e : I → B
he : CompleteOrthogonalIdempotents e
he' : ∀ (i : I), (Ideal.Quotient.mk J) (e i) = g (Pi.single i 1)
iso : B ≃ₐ[R] (i : I) → B ⧸ Ideal.span {1 - e i} :=
  let __spread.0 := AlgHom.pi fun i ↦ Ideal.Quotient.mkₐ R (Ideal.span {1 - e i});
  let __spread.1 := Equiv.ofBijective ⇑(RingHom.pi fun i ↦ Ideal.Quotient.mk (Ideal.span {1 - e i})) ⋯;
  { toFun := (↑↑__spread.0.toRingHom).toFun, invFun := __spread.1.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯,
    map_add' := ⋯, commutes' := ⋯ }
J' : (i : I) → Ideal (B ⧸ Ideal.span {1 - e i}) := fun i ↦ Ideal.map (Ideal.Quotient.mk (Ideal.span {1 - e i})) J
ι : (i : I) → B ⧸ J →ₐ[R] (B ⧸ Ideal.span {1 - e i}) ⧸ J' i :=
  fun i ↦ Ideal.quotientMapₐ (J' i) (IsScalarTower.toAlgHom R B (B ⧸ Ideal.span {1 - e i})) ⋯
hι : ∀ (i : I) (x : B ⧸ J), (ι i) x = 0 → (Ideal.Quotient.mk J) (e i) * x = 0
a : (i : I) → A i →ₐ[R] B ⧸ Ideal.span {1 - e i}
ha : ∀ (i : I) (x : A i), (Ideal.Quotient.mk (J' i)) ((a i) x) = (ι i) (g (Pi.single i x))
x✝ : (i : I) → A i
i : I
x : A i
y : B
hy : (Ideal.Quotient.mk (Ideal.span {1 - e i})) y = (a i) x
hy' : (Ideal.Quotient.mk (Ideal.span {1 - e i})) (y * e i) = (a i) x
this : (Ideal.Quotient.mk J) (e i) * ((Ideal.Quotient.mk J) (y * e i) - g (Pi.single i x)) = 0
⊢ (Ideal.Quotient.mk J) (y * e i) = g (Pi.single i x)

Tactic:
rwa [mul_sub, ← map_mul, mul_comm, mul_assoc, (he.idem i).eq, he', ← map_mul, ← Pi.single_mul,
        one_mul, sub_eq_zero] at this

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

Goal state before:
pp: R : Type u_1
S : Type u_2
P : Type u_3
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Module.Flat R S
inst✝⁹ : CommRing P
inst✝⁸ : Algebra R P
inst✝⁷ : Algebra P S
inst✝⁶ : IsScalarTower R P S
inst✝⁵ : IsLocalRing R
inst✝⁴ : IsLocalRing S
inst✝³ : IsLocalHom (algebraMap R S)
inst✝² : FormallySmooth 𝓀[R] (𝓀[R] ⊗[R] S)
M : Submonoid P
inst✝¹ : IsLocalization M S
inst✝ : FinitePresentation R P
n : ℕ
f₀ : MvPolynomial (Fin n) R →ₐ[R] P
hf₀ : Function.Surjective ⇑f₀
M' : Submonoid (MvPolynomial (Fin n) R) := Submonoid.comap f₀ M
P' : Type u_1 := Localization M'
fP : P' →ₐ[R] S := IsLocalization.liftAlgHom ⋯
hf₁ : Function.Surjective ⇑fP
hfP : (RingHom.ker fP).FG
algInst✝ : Algebra P' S := fP.toAlgebra
this✝ : FormallyEtale (MvPolynomial (Fin n) R) P'
this : FormallySmooth R P'
⊢ FormallySmooth R S

Tactic:
have : Module.Free P' Ω[P'⁄R] :=
    .of_equiv (KaehlerDifferential.tensorKaehlerEquivOfFormallyEtale R (MvPolynomial (Fin n) R) P')

Goal state after:
R : Type u_1
S : Type u_2
P : Type u_3
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Module.Flat R S
inst✝⁹ : CommRing P
inst✝⁸ : Algebra R P
inst✝⁷ : Algebra P S
inst✝⁶ : IsScalarTower R P S
inst✝⁵ : IsLocalRing R
inst✝⁴ : IsLocalRing S
inst✝³ : IsLocalHom (algebraMap R S)
inst✝² : FormallySmooth 𝓀[R] (𝓀[R] ⊗[R] S)
M : Submonoid P
inst✝¹ : IsLocalization M S
inst✝ : FinitePresentation R P
n : ℕ
f₀ : MvPolynomial (Fin n) R →ₐ[R] P
hf₀ : Function.Surjective ⇑f₀
M' : Submonoid (MvPolynomial (Fin n) R) := Submonoid.comap f₀ M
P' : Type u_1 := Localization M'
fP : P' →ₐ[R] S := IsLocalization.liftAlgHom ⋯
hf₁ : Function.Surjective ⇑fP
hfP : (RingHom.ker fP).FG
algInst✝ : Algebra P' S := fP.toAlgebra
this✝¹ : FormallyEtale (MvPolynomial (Fin n) R) P'
this✝ : FormallySmooth R P'
this : Module.Free P' Ω[P'⁄R]
⊢ FormallySmooth R S
Module: Mathlib.RingTheory.AdicCompletion.Functoriality

Goal state before:
pp: case smul
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
h : Function.Surjective ⇑((I • ⊤).mkQ ∘ₗ f)
y✝ : N
n : ℕ
r : R
hr : r ∈ I ^ n
y : N
hn✝ : y ∈ ⊤
⊢ ∃ x ∈ I ^ n • ⊤, f x ≡ r • y [SMOD I ^ (n + 1) • ⊤]

Tactic:
obtain ⟨x, hx⟩ := h (mkQ _ y)

Goal state after:
case smul
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
h : Function.Surjective ⇑((I • ⊤).mkQ ∘ₗ f)
y✝ : N
n : ℕ
r : R
hr : r ∈ I ^ n
y : N
hn✝ : y ∈ ⊤
x : M
hx : ((I • ⊤).mkQ ∘ₗ f) x = (I • ⊤).mkQ y
⊢ ∃ x ∈ I ^ n • ⊤, f x ≡ r • y [SMOD I ^ (n + 1) • ⊤]
Module: Mathlib.RingTheory.AdicCompletion.Functoriality

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
h : Function.Surjective ⇑((I • ⊤).mkQ ∘ₗ f)
x : M
y : N
n : ℕ
hxy : f x ≡ y [SMOD I ^ n • ⊤]
⊢ ∃ x', x ≡ x' [SMOD I ^ n • ⊤] ∧ f x' ≡ y [SMOD I ^ (n + 1) • ⊤]

Tactic:
by
  obtain ⟨z, hz, hz'⟩ :=
    exists_smodEq_pow_add_one_smul h (y := y - f x) (SModEq.sub_mem.mp hxy.symm)
  use x + z
  constructor
  · simpa [SModEq.sub_mem]
  · simpa [SModEq.sub_mem, sub_sub_eq_add_sub, add_comm] using hz'

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

Goal state before:
pp: case inr
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
s : M →ₗ[R] K
hs : s ∘ₗ f = LinearMap.id
hfg : Function.Exact ⇑f ⇑g
κ : Type u_6
σ : Type u_7
v : κ ⊕ σ → M
hg : Function.Surjective ⇑g
hslzero : ∀ (i : κ), s (v (Sum.inl i)) = 0
hli : LinearIndependent R (⇑s ∘ v ∘ Sum.inr)
hsp : ⊤ ≤ Submodule.span R (Set.range v)
m : M
this :
  ∀ {R : Type u_1} {M : Type u_2} {K : Type u_3} {P : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M]
    [inst_2 : AddCommGroup K] [inst_3 : AddCommGroup P] [inst_4 : Module R M] [inst_5 : Module R K]
    [inst_6 : Module R P] {f : K →ₗ[R] M} {g : M →ₗ[R] P} {s : M →ₗ[R] K},
    s ∘ₗ f = LinearMap.id →
      Function.Exact ⇑f ⇑g →
        ∀ {κ : Type u_6} {σ : Type u_7} (v : κ ⊕ σ → M),
          Function.Surjective ⇑g →
            (∀ (i : κ), s (v (Sum.inl i)) = 0) →
              LinearIndependent R (⇑s ∘ v ∘ Sum.inr) →
                ⊤ ≤ Submodule.span R (Set.range v) → ∀ m ∈ s.ker, g m ∈ Submodule.span R (Set.range (⇑g ∘ v ∘ Sum.inl))
h : m ∉ s.ker
x : M := f (s m)
⊢ g m ∈ Submodule.span R (Set.range (⇑g ∘ v ∘ Sum.inl))

Tactic:
show g m = g (m - f (s m)) by simp [hfg.apply_apply_eq_zero]

Goal state after:
case inr
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
s : M →ₗ[R] K
hs : s ∘ₗ f = LinearMap.id
hfg : Function.Exact ⇑f ⇑g
κ : Type u_6
σ : Type u_7
v : κ ⊕ σ → M
hg : Function.Surjective ⇑g
hslzero : ∀ (i : κ), s (v (Sum.inl i)) = 0
hli : LinearIndependent R (⇑s ∘ v ∘ Sum.inr)
hsp : ⊤ ≤ Submodule.span R (Set.range v)
m : M
this :
  ∀ {R : Type u_1} {M : Type u_2} {K : Type u_3} {P : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M]
    [inst_2 : AddCommGroup K] [inst_3 : AddCommGroup P] [inst_4 : Module R M] [inst_5 : Module R K]
    [inst_6 : Module R P] {f : K →ₗ[R] M} {g : M →ₗ[R] P} {s : M →ₗ[R] K},
    s ∘ₗ f = LinearMap.id →
      Function.Exact ⇑f ⇑g →
        ∀ {κ : Type u_6} {σ : Type u_7} (v : κ ⊕ σ → M),
          Function.Surjective ⇑g →
            (∀ (i : κ), s (v (Sum.inl i)) = 0) →
              LinearIndependent R (⇑s ∘ v ∘ Sum.inr) →
                ⊤ ≤ Submodule.span R (Set.range v) → ∀ m ∈ s.ker, g m ∈ Submodule.span R (Set.range (⇑g ∘ v ∘ Sum.inl))
h : m ∉ s.ker
x : M := f (s m)
⊢ g (m - f (s m)) ∈ Submodule.span R (Set.range (⇑g ∘ v ∘ Sum.inl))
Module: Mathlib.RingTheory.Extension.Presentation.Submersive

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
Q : PreSubmersivePresentation S T ι' σ'
P : PreSubmersivePresentation R S ι σ
inst✝¹ : Finite σ
inst✝ : Finite σ'
⊢ (Q.comp P).jacobian = P.jacobian • Q.jacobian

Tactic:
classical
  cases nonempty_fintype σ'
  cases nonempty_fintype σ
  rw [jacobian_eq_jacobiMatrix_det, ← Matrix.fromBlocks_toBlocks ((Q.comp P).jacobiMatrix),
    jacobiMatrix_comp_₁₂]
  convert_to
    (aeval (Q.comp P).val) (Q.comp P).jacobiMatrix.toBlocks₁₁.det *
    (aeval (Q.comp P).val) (Q.comp P).jacobiMatrix.toBlocks₂₂.det = P.jacobian • Q.jacobian
  · simp only [Generators.algebraMap_apply, ← map_mul]
    congr
    convert!
      Matrix.det_fromBlocks_zero₁₂ (Q.comp P).jacobiMatrix.toBlocks₁₁
        (Q.comp P).jacobiMatrix.toBlocks₂₁ (Q.comp P).jacobiMatrix.toBlocks₂₂
  · rw [jacobiMatrix_comp_₁₁_det, jacobiMatrix_comp_₂₂_det, mul_comm, Algebra.smul_def]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Finite σ
P : SubmersivePresentation R S ι σ
x : ↥P.ker
hx : ∀ (i : σ), (aeval P.val) ((pderiv (P.map i)) ↑x) = 0
this✝ : ↑x ∈ Ideal.span (Set.range P.relation)
c : σ →₀ P.Ring
hc : (c.sum fun i a ↦ a * P.relation i) = ↑x
heq : ∀ (i : σ), ∑ x ∈ c.support, (aeval P.val) (c x) * (aeval P.val) ((pderiv (P.map i)) (P.relation x)) = 0
heq2 : (∑ i ∈ c.support, (aeval P.val) (c i) • fun j ↦ (aeval P.val) ((pderiv (P.map j)) (P.relation i))) = 0
this : ∀ (i : σ), (aeval P.val) (c i) = 0
i : σ
hi : i ∈ c.support
⊢ (fun i a ↦ a * P.relation i) i (c i) ∈ P.ker ^ 2

Tactic:
pow_two

Goal state after:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Finite σ
P : SubmersivePresentation R S ι σ
x : ↥P.ker
hx : ∀ (i : σ), (aeval P.val) ((pderiv (P.map i)) ↑x) = 0
this✝ : ↑x ∈ Ideal.span (Set.range P.relation)
c : σ →₀ P.Ring
hc : (c.sum fun i a ↦ a * P.relation i) = ↑x
heq : ∀ (i : σ), ∑ x ∈ c.support, (aeval P.val) (c x) * (aeval P.val) ((pderiv (P.map i)) (P.relation x)) = 0
heq2 : (∑ i ∈ c.support, (aeval P.val) (c i) • fun j ↦ (aeval P.val) ((pderiv (P.map j)) (P.relation i))) = 0
this : ∀ (i : σ), (aeval P.val) (c i) = 0
i : σ
hi : i ∈ c.support
⊢ (fun i a ↦ a * P.relation i) i (c i) ∈ P.ker * P.ker
Module: Mathlib.RingTheory.Smooth.StandardSmoothOfFree

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FinitePresentation R S
inst✝ : Subsingleton (H1Cotangent R S)
I : Type u_3
b : Module.Basis I S Ω[S⁄R]
a✝ : Nontrivial S
n : ℕ
P✝ : Generators R S (Fin n)
f' : ⦃a : Ω[S⁄R]⦄ → a ∈ Set.range ⇑b → S
hf' : ∀ ⦃a : Ω[S⁄R]⦄ (a_1 : a ∈ Set.range ⇑b), (D R S) (f' a_1) = a
P : Generators R S (Fin n ⊕ I) := P✝.extend fun i ↦ f' ⋯
hb : ∀ (i : I), b i = (D R S) (P.val (Sum.inr i))
this✝ : Function.Bijective ⇑(P.cotangentRestrict ⋯)
bcot' : Module.Basis (Fin n) S P.toExtension.Cotangent :=
  { repr := LinearEquiv.ofBijective (P.cotangentRestrict ⋯) this✝ }
this : Finite I
Q : Presentation R S (Unit ⊕ Fin n ⊕ I) (Unit ⊕ Fin n)
bcot : Module.Basis (Unit ⊕ Fin n) S Q.toExtension.Cotangent
hcomp : Q.val ∘ Sum.inr = P.val
hbcot : ∀ (r : Unit ⊕ Fin n), bcot r = Extension.Cotangent.mk ⟨Q.relation r, ⋯⟩
P' : PreSubmersivePresentation R S (Unit ⊕ Fin n ⊕ I) (Unit ⊕ Fin n) :=
  let __spread.0 := Q;
  { toPresentation := __spread.0, map := Sum.map _root_.id Sum.inl, map_inj := ⋯ }
⊢ IsCompl (Set.range (Sum.inr ∘ Sum.inr)) (Set.range P'.map)

Tactic:
simp [P', ← eq_compl_iff_isCompl, Set.ext_iff, Set.mem_compl_iff]

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

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Bijective ⇑f
⊢ f.FormallyUnramified ∧ f.Smooth

Tactic:
exact ⟨.of_surjective hf.2, .of_bijective hf⟩

Goal state after:
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_3
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
x : MvPolynomial ι R ⧸ Ideal.span (Set.range (Subtype.val ∘ D.f ∘ ⇑b))
⊢ (Ideal.Quotient.mk (Ideal.span (Set.range (Subtype.val ∘ D.f ∘ ⇑b))))
      (if x = 0 then 0 else if x = -1 then -1 else Function.surjInv ⋯ x) =
    x

Tactic:
split_ifs

Goal state after:
case pos
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
x : MvPolynomial ι R ⧸ Ideal.span (Set.range (Subtype.val ∘ D.f ∘ ⇑b))
h✝ : x = 0
⊢ (Ideal.Quotient.mk (Ideal.span (Set.range (Subtype.val ∘ D.f ∘ ⇑b)))) 0 = x

case pos
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
x : MvPolynomial ι R ⧸ Ideal.span (Set.range (Subtype.val ∘ D.f ∘ ⇑b))
h✝¹ : ¬x = 0
h✝ : x = -1
⊢ (Ideal.Quotient.mk (Ideal.span (Set.range (Subtype.val ∘ D.f ∘ ⇑b)))) (-1) = x

case neg
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
x : MvPolynomial ι R ⧸ Ideal.span (Set.range (Subtype.val ∘ D.f ∘ ⇑b))
h✝¹ : ¬x = 0
h✝ : ¬x = -1
⊢ (Ideal.Quotient.mk (Ideal.span (Set.range (Subtype.val ∘ D.f ∘ ⇑b)))) (Function.surjInv ⋯ x) = x
Module: Mathlib.RingTheory.Smooth.Field

Goal state before:
pp: K : Type u_1
L : Type u_2
ι : Type u_3
inst✝⁴ : Field L
inst✝³ : Field K
inst✝² : Algebra K L
inst✝¹ : PerfectField K
inst✝ : EssFiniteType K L
s : Finset L
hs : IsTranscendenceBasis K Subtype.val
H : Algebra.IsSeparable (↥(IntermediateField.adjoin K ↑s)) L
this : Algebra.IsSeparable (↥(IntermediateField.adjoin K (Set.range Subtype.val))) L
⊢ FormallySmooth K L

Tactic:
exact .of_algebraicIndependent_of_isSeparable hs.1

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

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

Tactic:
by
  rw [negAddY]
  ring1

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')
hF'' : coeff 0 F'' = 0
hpm : p * F''.totalDegree ≤ F.totalDegree
hF''0 : F''.totalDegree = 0
⊢ F'' = 0

Tactic:
rw [totalDegree_eq_zero_iff_eq_C.mp hF''0, hF'', map_zero]

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ IsZariskiLocalAtSource @IsLocalIso

Tactic:
rw [eq_sourceLocalClosure_isOpenImmersion]
  infer_instance

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ IsMultiplicative @IsLocalIso

Tactic:
rw [eq_sourceLocalClosure_isOpenImmersion]
  infer_instance

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ IsStableUnderBaseChange @IsLocalIso

Tactic:
rw [eq_sourceLocalClosure_isOpenImmersion]
  infer_instance

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

Goal state before:
pp: case inr
P P' : MorphismProperty Scheme
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝³ : P'.IsStableUnderBaseChange
inst✝² : P'.IsStableUnderComposition
inst✝¹ : P.IsStableUnderBaseChange
H₁ : @IsLocalIso ⊓ @Surjective ≤ P'
H₂ : ∀ {R S : CommRingCat} {f : R ⟶ S}, P' (Spec.map f) → Q' (CommRingCat.Hom.hom f)
inst✝ : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Q
hQQ' : RingHom.CodescendsAlong (fun {R S} [CommRing R] [CommRing S] ↦ Q) fun {R S} [CommRing R] [CommRing S] ↦ Q'
R S : CommRingCat
Y : Scheme
φ : R ⟶ S
g : Y ⟶ Spec R
h : P' (Spec.map φ)
hf : P (pullback.fst (Spec.map φ) g)
this : ∀ {Y : Scheme} (g : Y ⟶ Spec R), P (pullback.fst (Spec.map φ) g) → (∃ S, Y = Spec S) → P g
hY : ¬∃ S, Y = Spec S
⊢ P g

Tactic:
IsZariskiLocalAtSource.iff_of_openCover (P := P) Y.affineCover

Goal state after:
case inr
P P' : MorphismProperty Scheme
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝³ : P'.IsStableUnderBaseChange
inst✝² : P'.IsStableUnderComposition
inst✝¹ : P.IsStableUnderBaseChange
H₁ : @IsLocalIso ⊓ @Surjective ≤ P'
H₂ : ∀ {R S : CommRingCat} {f : R ⟶ S}, P' (Spec.map f) → Q' (CommRingCat.Hom.hom f)
inst✝ : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Q
hQQ' : RingHom.CodescendsAlong (fun {R S} [CommRing R] [CommRing S] ↦ Q) fun {R S} [CommRing R] [CommRing S] ↦ Q'
R S : CommRingCat
Y : Scheme
φ : R ⟶ S
g : Y ⟶ Spec R
h : P' (Spec.map φ)
hf : P (pullback.fst (Spec.map φ) g)
this : ∀ {Y : Scheme} (g : Y ⟶ Spec R), P (pullback.fst (Spec.map φ) g) → (∃ S, Y = Spec S) → P g
hY : ¬∃ S, Y = Spec S
⊢ ∀ (i : Y.affineCover.I₀), P (Y.affineCover.f i ≫ g)
Module: Mathlib.RingTheory.IntegralClosure.GoingDown

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsDomain S
inst✝⁴ : FaithfulSMul R S
inst✝³ : Algebra.IsIntegral R S
inst✝² : IsIntegrallyClosed R
this : IsDomain R
p : Ideal R
inst✝¹ : p.IsPrime
Q : Ideal S
inst✝ : Q.IsPrime
hpQ : p < Ideal.under R Q
SQ : Type u_2 := Localization.AtPrime Q
x : R
hx : x ∈ Ideal.comap (algebraMap R SQ) (Ideal.map (algebraMap R SQ) p)
a : S
ha : x • a ∈ Ideal.map (algebraMap R S) p
haQ : a ∉ Q
f : R[X]
hfm : f.Monic
hfa : (aeval (x • a)) f = 0
hf : ∀ (i : ℕ), i ≠ f.natDegree → f.coeff i ∈ p
⊢ x ∈ p

Tactic:
obtain ⟨i, hi, hip⟩ : ∃ i ≠ (minpoly R a).natDegree, (minpoly R a).coeff i ∉ p := by
    set g := minpoly R a
    by_contra! H
    have : g.map (Ideal.Quotient.mk p) = X ^ g.natDegree := by
      ext i
      obtain hi | rfl | hi := lt_trichotomy i g.natDegree
      · simpa [hi.ne, Ideal.Quotient.eq_zero_iff_mem] using H _ hi.ne
      · simp [g, minpoly.monic (Algebra.IsIntegral.isIntegral _)]
      · simp [coeff_eq_zero_of_natDegree_lt hi, hi.ne']
    have : Ideal.Quotient.mk (Ideal.map (algebraMap R S) p) (a ^ (minpoly R a).natDegree) = 0 := by
      simpa [← Ideal.Quotient.algebraMap_eq, aeval_algebraMap_apply, g] using
        congr(aeval (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p) a) $this).symm
    exact haQ (‹Q.IsPrime›.mem_of_pow_mem _
      (Ideal.map_le_iff_le_comap.mpr hpQ.le (Ideal.Quotient.eq_zero_iff_mem.mp this)))

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsDomain S
inst✝⁴ : FaithfulSMul R S
inst✝³ : Algebra.IsIntegral R S
inst✝² : IsIntegrallyClosed R
this : IsDomain R
p : Ideal R
inst✝¹ : p.IsPrime
Q : Ideal S
inst✝ : Q.IsPrime
hpQ : p < Ideal.under R Q
SQ : Type u_2 := Localization.AtPrime Q
x : R
hx : x ∈ Ideal.comap (algebraMap R SQ) (Ideal.map (algebraMap R SQ) p)
a : S
ha : x • a ∈ Ideal.map (algebraMap R S) p
haQ : a ∉ Q
f : R[X]
hfm : f.Monic
hfa : (aeval (x • a)) f = 0
hf : ∀ (i : ℕ), i ≠ f.natDegree → f.coeff i ∈ p
i : ℕ
hi : i ≠ (minpoly R a).natDegree
hip : (minpoly R a).coeff i ∉ p
⊢ x ∈ p