mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Types.Multiequalizer

Goal state before:
pp: case id
J : MulticospanShape
I : MulticospanIndex J (Type u)
s : I.sections
j✝ : WalkingMulticospan J
⊢ (ConcreteCategory.hom (I.multicospan.map (WalkingMulticospan.Hom.id j✝)))
      ((fun i ↦
          match i with
          | WalkingMulticospan.left i => s.val i
          | WalkingMulticospan.right j => (ConcreteCategory.hom (I.fst j)) (s.val (J.fst j)))
        j✝) =
    (fun i ↦
        match i with
        | WalkingMulticospan.left i => s.val i
        | WalkingMulticospan.right j => (ConcreteCategory.hom (I.fst j)) (s.val (J.fst j)))
      j✝

pp: case fst
J : MulticospanShape
I : MulticospanIndex J (Type u)
s : I.sections
b✝ : J.R
⊢ (ConcreteCategory.hom (I.multicospan.map (WalkingMulticospan.Hom.fst b✝)))
      ((fun i ↦
          match i with
          | WalkingMulticospan.left i => s.val i
          | WalkingMulticospan.right j => (ConcreteCategory.hom (I.fst j)) (s.val (J.fst j)))
        (WalkingMulticospan.left (J.fst b✝))) =
    (fun i ↦
        match i with
        | WalkingMulticospan.left i => s.val i
        | WalkingMulticospan.right j => (ConcreteCategory.hom (I.fst j)) (s.val (J.fst j)))
      (WalkingMulticospan.right b✝)

pp: case snd
J : MulticospanShape
I : MulticospanIndex J (Type u)
s : I.sections
r : J.R
⊢ (ConcreteCategory.hom (I.multicospan.map (WalkingMulticospan.Hom.snd r)))
      ((fun i ↦
          match i with
          | WalkingMulticospan.left i => s.val i
          | WalkingMulticospan.right j => (ConcreteCategory.hom (I.fst j)) (s.val (J.fst j)))
        (WalkingMulticospan.left (J.snd r))) =
    (fun i ↦
        match i with
        | WalkingMulticospan.left i => s.val i
        | WalkingMulticospan.right j => (ConcreteCategory.hom (I.fst j)) (s.val (J.fst j)))
      (WalkingMulticospan.right r)

Tactic:
· rfl

Goal state after:
case fst
J : MulticospanShape
I : MulticospanIndex J (Type u)
s : I.sections
b✝ : J.R
⊢ (ConcreteCategory.hom (I.multicospan.map (WalkingMulticospan.Hom.fst b✝)))
      ((fun i ↦
          match i with
          | WalkingMulticospan.left i => s.val i
          | WalkingMulticospan.right j => (ConcreteCategory.hom (I.fst j)) (s.val (J.fst j)))
        (WalkingMulticospan.left (J.fst b✝))) =
    (fun i ↦
        match i with
        | WalkingMulticospan.left i => s.val i
        | WalkingMulticospan.right j => (ConcreteCategory.hom (I.fst j)) (s.val (J.fst j)))
      (WalkingMulticospan.right b✝)

case snd
J : MulticospanShape
I : MulticospanIndex J (Type u)
s : I.sections
r : J.R
⊢ (ConcreteCategory.hom (I.multicospan.map (WalkingMulticospan.Hom.snd r)))
      ((fun i ↦
          match i with
          | WalkingMulticospan.left i => s.val i
          | WalkingMulticospan.right j => (ConcreteCategory.hom (I.fst j)) (s.val (J.fst j)))
        (WalkingMulticospan.left (J.snd r))) =
    (fun i ↦
        match i with
        | WalkingMulticospan.left i => s.val i
        | WalkingMulticospan.right j => (ConcreteCategory.hom (I.fst j)) (s.val (J.fst j)))
      (WalkingMulticospan.right r)
Module: Mathlib.CategoryTheory.Limits.Types.Multiequalizer

Goal state before:
pp: case fst
J : MulticospanShape
I : MulticospanIndex J (Type u)
s : I.sections
b✝ : J.R
⊢ (ConcreteCategory.hom (I.multicospan.map (WalkingMulticospan.Hom.fst b✝)))
      ((fun i ↦
          match i with
          | WalkingMulticospan.left i => s.val i
          | WalkingMulticospan.right j => (ConcreteCategory.hom (I.fst j)) (s.val (J.fst j)))
        (WalkingMulticospan.left (J.fst b✝))) =
    (fun i ↦
        match i with
        | WalkingMulticospan.left i => s.val i
        | WalkingMulticospan.right j => (ConcreteCategory.hom (I.fst j)) (s.val (J.fst j)))
      (WalkingMulticospan.right b✝)

pp: case snd
J : MulticospanShape
I : MulticospanIndex J (Type u)
s : I.sections
r : J.R
⊢ (ConcreteCategory.hom (I.multicospan.map (WalkingMulticospan.Hom.snd r)))
      ((fun i ↦
          match i with
          | WalkingMulticospan.left i => s.val i
          | WalkingMulticospan.right j => (ConcreteCategory.hom (I.fst j)) (s.val (J.fst j)))
        (WalkingMulticospan.left (J.snd r))) =
    (fun i ↦
        match i with
        | WalkingMulticospan.left i => s.val i
        | WalkingMulticospan.right j => (ConcreteCategory.hom (I.fst j)) (s.val (J.fst j)))
      (WalkingMulticospan.right r)

Tactic:
· rfl

Goal state after:
case snd
J : MulticospanShape
I : MulticospanIndex J (Type u)
s : I.sections
r : J.R
⊢ (ConcreteCategory.hom (I.multicospan.map (WalkingMulticospan.Hom.snd r)))
      ((fun i ↦
          match i with
          | WalkingMulticospan.left i => s.val i
          | WalkingMulticospan.right j => (ConcreteCategory.hom (I.fst j)) (s.val (J.fst j)))
        (WalkingMulticospan.left (J.snd r))) =
    (fun i ↦
        match i with
        | WalkingMulticospan.left i => s.val i
        | WalkingMulticospan.right j => (ConcreteCategory.hom (I.fst j)) (s.val (J.fst j)))
      (WalkingMulticospan.right r)
Module: Mathlib.CategoryTheory.Limits.Types.Multiequalizer

Goal state before:
pp: case left
J : MulticospanShape
I : MulticospanIndex J (Type u)
s : ↑I.multicospan.sections
a✝ : J.L
⊢ ↑((fun s ↦
            ⟨fun i ↦
              match i with
              | WalkingMulticospan.left i => s.val i
              | WalkingMulticospan.right j => (ConcreteCategory.hom (I.fst j)) (s.val (J.fst j)),
              ⋯⟩)
          ((fun s ↦ { val := fun i ↦ ↑s (WalkingMulticospan.left i), property := ⋯ }) s))
      (WalkingMulticospan.left a✝) =
    ↑s (WalkingMulticospan.left a✝)

pp: case right
J : MulticospanShape
I : MulticospanIndex J (Type u)
s : ↑I.multicospan.sections
r : J.R
⊢ ↑((fun s ↦
            ⟨fun i ↦
              match i with
              | WalkingMulticospan.left i => s.val i
              | WalkingMulticospan.right j => (ConcreteCategory.hom (I.fst j)) (s.val (J.fst j)),
              ⋯⟩)
          ((fun s ↦ { val := fun i ↦ ↑s (WalkingMulticospan.left i), property := ⋯ }) s))
      (WalkingMulticospan.right r) =
    ↑s (WalkingMulticospan.right r)

Tactic:
· rfl

Goal state after:
case right
J : MulticospanShape
I : MulticospanIndex J (Type u)
s : ↑I.multicospan.sections
r : J.R
⊢ ↑((fun s ↦
            ⟨fun i ↦
              match i with
              | WalkingMulticospan.left i => s.val i
              | WalkingMulticospan.right j => (ConcreteCategory.hom (I.fst j)) (s.val (J.fst j)),
              ⋯⟩)
          ((fun s ↦ { val := fun i ↦ ↑s (WalkingMulticospan.left i), property := ⋯ }) s))
      (WalkingMulticospan.right r) =
    ↑s (WalkingMulticospan.right r)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
h : P ≈ Q
⊢ W'.Nonsingular P ↔ W'.Nonsingular Q

Tactic:
rcases h with ⟨u, rfl⟩
  exact nonsingular_smul Q u.isUnit

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

Goal state before:
pp: case neg
F : Type u
inst✝¹ : Field F
W : Projective F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z = 0
hQz : ¬Q z = 0
⊢ toAffine W ((P y ^ 2 * Q z) • Q) = toAffine W Q

Tactic:
toAffine_smul _ <| ((isUnit_Y_of_Z_eq_zero hP hPz).pow 2).mul <| Ne.isUnit hQz

Goal state after:
case neg
F : Type u
inst✝¹ : Field F
W : Projective F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z = 0
hQz : ¬Q z = 0
⊢ toAffine W Q = toAffine W Q
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✝ : FormallySmooth R ((i : I) → A i)
i : I
⊢ Pi.single i 1 - 1 ∈ RingHom.ker (Pi.evalAlgHom R A i).toRingHom

Tactic:
simp [RingHom.mem_ker]

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

Goal state before:
pp: 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
x y : L
h : x ∈ K⟮y⟯
e : K⟮x⟯ ≤ K⟮y⟯
⊢ (g y) ⟨x, h⟩ = ((g y).comp (IntermediateField.inclusion e)) (IntermediateField.AdjoinSimple.gen K x)

pp: 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
x y : L
h : x ∈ K⟮y⟯
e : K⟮x⟯ ≤ K⟮y⟯
⊢ (fun g ↦ (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮x⟯) L))
    ((g y).comp (IntermediateField.inclusion e))

Tactic:
· rfl

Goal state after:
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
x y : L
h : x ∈ K⟮y⟯
e : K⟮x⟯ ≤ K⟮y⟯
⊢ (fun g ↦ (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮x⟯) L))
    ((g y).comp (IntermediateField.inclusion e))
Module: Mathlib.RingTheory.Kaehler.TensorProduct

Goal state before:
pp: 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
⊢ B ⊗[A] Ω[A⁄R] ≃ₗ[B] Ω[B⁄S]

Tactic:
have : Algebra.IsPushout R A S B := .symm inferInstance
  let e₁ : B ⊗[A] Ω[A⁄R] ≃ₗ[A] Ω[A⁄R] ⊗[R] S :=
    AlgebraTensorModule.congr (Algebra.IsPushout.equiv R A S B).symm.toLinearEquiv (.refl _ _)
      ≪≫ₗ _root_.TensorProduct.comm _ _ _ ≪≫ₗ AlgebraTensorModule.cancelBaseChange ..
  let e₂ : B ⊗[A] Ω[A⁄R] ≃ₗ[R] Ω[B⁄S] :=
    e₁.restrictScalars R ≪≫ₗ _root_.TensorProduct.comm _ _ _ ≪≫ₗ
      (KaehlerDifferential.tensorKaehlerEquivBase R S A B).restrictScalars R
  refine { __ := e₂, map_smul' := ?_ }
  intro m x
  obtain ⟨m, rfl⟩ := (Algebra.IsPushout.equiv R A S B).surjective m
  dsimp
  induction m with
  | zero => simp
  | add x y _ _ => simp only [add_smul, map_add, *]
  | tmul a b =>
  induction x with
  | zero => simp
  | add x y _ _ => simp only [smul_add, map_add, *]
  | tmul x y =>
  obtain ⟨x, rfl⟩ := (Algebra.IsPushout.equiv R A S B).surjective x
  induction x with
  | zero => simp
  | add x y _ _ => simp only [smul_add, map_add, *, add_tmul]
  | tmul x z =>
  suffices b • z • a • x • KaehlerDifferential.map R S A B y =
      (algebraMap A B a * algebraMap S B b) • z • x • KaehlerDifferential.map R S A B y by
    simpa [e₂, e₁, smul_tmul', Algebra.IsPushout.equiv_tmul, ← mul_smul,
      Algebra.IsPushout.equiv_symm_algebraMap_left, Algebra.IsPushout.equiv_symm_algebraMap_right]
  simp only [← mul_smul, ← @algebraMap_smul S _ B, ← @algebraMap_smul A _ B]
  ring_nf

Goal state after:
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
P : Type u_4
inst✝³ : AddCommGroup P
inst✝² : Module R P
T : Type u_5
inst✝¹ : AddCommGroup T
inst✝ : Module (AdicCompletion I R) T
f : M ≃ₗ[R] N
⊢ map I ↑f ∘ₗ map I ↑f.symm = LinearMap.id

Tactic:
simp [map_comp]

Goal state after:
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
P : Type u_4
inst✝³ : AddCommGroup P
inst✝² : Module R P
T : Type u_5
inst✝¹ : AddCommGroup T
inst✝ : Module (AdicCompletion I R) T
f : M ≃ₗ[R] N
⊢ map I ↑f.symm ∘ₗ map I ↑f = LinearMap.id

Tactic:
simp [map_comp]

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Functoriality

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
ι : Type u_6
M : ι → Type u_7
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
j : ι
x : AdicCauchySequence I (M j)
i : ι
n : ℕ
h : j = i
⊢ Submodule.Quotient.mk (Eq.recOn h (↑x n)) = ↑(Eq.recOn h ((mk I (M j)) x)) n

Tactic:
subst h

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
ι : Type u_6
M : ι → Type u_7
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
j : ι
x : AdicCauchySequence I (M j)
n : ℕ
⊢ Submodule.Quotient.mk (Eq.recOn ⋯ (↑x n)) = ↑(Eq.recOn ⋯ ((mk I (M j)) x)) n
Module: Mathlib.RingTheory.AdicCompletion.Algebra

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
I : Ideal R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
b : AdicCompletion I M
n : ℕ
⊢ ↑(1 • b) n = ↑b n

Tactic:
simp only [smul_eval, val_one, one_smul]

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.AsTensorProduct

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
x y : AdicCompletion I R
⊢ ↑R ((LinearMap.lsmul (AdicCompletion I R) (AdicCompletion I M)) (x + y)) ∘ₗ of I M =
    ↑R ((LinearMap.lsmul (AdicCompletion I R) (AdicCompletion I M)) x) ∘ₗ of I M +
      ↑R ((LinearMap.lsmul (AdicCompletion I R) (AdicCompletion I M)) y) ∘ₗ of I M

Tactic:
by
        apply LinearMap.ext
        simp

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

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

Tactic:
obtain ⟨A₀, B₀, _, _, _, _, _, _, _, _, ⟨e⟩⟩ := exists_finiteType ℤ R A

Goal state after:
R : Type u_1
A : Type u_2
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Smooth R A
A₀ B₀ : Type u_1
w✝⁴ : CommRing A₀
w✝³ : CommRing B₀
w✝² : Algebra ℤ A₀
w✝¹ : Algebra A₀ R
w✝ : Algebra A₀ B₀
left✝² : Function.Injective ⇑(algebraMap A₀ R)
left✝¹ : FiniteType ℤ A₀
left✝ : Smooth A₀ B₀
e : A ≃ₐ[R] TensorProduct A₀ R B₀
⊢ Module.Flat R A
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))
h : x = 0
⊢ (Ideal.Quotient.mk (Ideal.span (Set.range (Subtype.val ∘ D.f ∘ ⇑b)))) 0 = x

Tactic:
subst h

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

Tactic:
subst h

Goal state after:
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
h✝ : ¬-1 = 0
⊢ (Ideal.Quotient.mk (Ideal.span (Set.range (Subtype.val ∘ D.f ∘ ⇑b)))) (-1) = -1
Module: Mathlib.RingTheory.Smooth.NoetherianDescent

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
A : Type u
B : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Smooth A B
P : Presentation A B (Fin (Presentation.ofFinitePresentationVars A B))
  (Fin (Presentation.ofFinitePresentationRels A B)) :=
  Presentation.ofFinitePresentation A B
f : P.Ring →ₐ[A] B := IsScalarTower.toAlgHom A P.Ring B
hkerf : RingHom.ker f = Ideal.span (Set.range P.relation)
σ : B →ₐ[A] MvPolynomial (Fin (Presentation.ofFinitePresentationVars A B)) A ⧸ RingHom.ker f ^ 2
hsig : f.kerSquareLift.comp σ = AlgHom.id A B
h : Fin (Presentation.ofFinitePresentationVars A B) → MvPolynomial (Fin (Presentation.ofFinitePresentationVars A B)) A
hh :
  ∀ (i : Fin (Presentation.ofFinitePresentationVars A B)), (Ideal.Quotient.mk (RingHom.ker f ^ 2)) (h i) = σ (P.val i)
⊢ ∀ (i : Fin (Presentation.ofFinitePresentationVars A B)),
    ((Ideal.Quotient.mkₐ A (RingHom.ker f ^ 2)).comp (aeval h)) (X i) = (σ.comp (aeval P.val)) (X i)

Tactic:
by simp [hh]

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

Goal state before:
pp: case h
n m : ℕ
X✝ Y : Scheme
f : X✝ ⟶ Y
X : Scheme
⊢ ∀ {Y : Scheme} (f : X ⟶ Y),
    SmoothOfRelativeDimension n f ↔
      ∀ (x : ↥X),
        ∃ U V,
          ∃ (_ : x ∈ ↑V) (e : ↑V ≤ f ⁻¹ᵁ ↑U),
            IsStandardSmoothOfRelativeDimension n (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))

Tactic:
Y

Goal state after:
case h
n m : ℕ
X✝ Y✝ : Scheme
f : X✝ ⟶ Y✝
X Y : Scheme
⊢ ∀ (f : X ⟶ Y),
    SmoothOfRelativeDimension n f ↔
      ∀ (x : ↥X),
        ∃ U V,
          ∃ (_ : x ∈ ↑V) (e : ↑V ≤ f ⁻¹ᵁ ↑U),
            IsStandardSmoothOfRelativeDimension n (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))
Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
x : ↥X
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
hx : x ∈ V
this : Algebra ↑Γ(Y, U) ↑Γ(X, V) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
p : Ideal ↑Γ(Y, U) := (hU.primeIdealOf ⟨f x, ⋯⟩).asIdeal
q : Ideal ↑Γ(X, V) := (hV.primeIdealOf ⟨x, hx⟩).asIdeal
⊢ (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallySmooth ↔
    hV.primeIdealOf ⟨x, hx⟩ ∈ Algebra.smoothLocus ↑Γ(Y, U) ↑Γ(X, V)

Tactic:
have : q.LiesOver p :=
    ⟨congr($(IsAffineOpen.comap_primeIdealOf_appLE U hU V hV hVU hx).1).symm⟩

Goal state after:
X Y : Scheme
f : X ⟶ Y
x : ↥X
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
hx : x ∈ V
this✝ : Algebra ↑Γ(Y, U) ↑Γ(X, V) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
p : Ideal ↑Γ(Y, U) := (hU.primeIdealOf ⟨f x, ⋯⟩).asIdeal
q : Ideal ↑Γ(X, V) := (hV.primeIdealOf ⟨x, hx⟩).asIdeal
this : q.LiesOver p
⊢ (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallySmooth ↔
    hV.primeIdealOf ⟨x, hx⟩ ∈ Algebra.smoothLocus ↑Γ(Y, U) ↑Γ(X, V)
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: case refine_1
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
σ : ι →₀ ℕ
hσ : σ ∈ F.support
i : ι
hσi : σ i ≠ 0
H✝ : (F.toPolynomialAdjoinImageCompl a i).coeff (σ i) = 0
F₀ : Polynomial (MvPolynomial { b // b ≠ i } k) :=
  (optionEquivLeft k { b // b ≠ i }) ((renameEquiv k (Equiv.optionSubtypeNe i).symm) F)
H : F₀.coeff (σ i) = 0
e : ι ≃ Option { b // b ≠ i } := (Equiv.optionSubtypeNe i).symm
this :
  coeff (Finsupp.mapDomain (⇑e) σ).some
      (((optionEquivLeft k { b // b ≠ i }) ((rename ⇑(Equiv.optionSubtypeNe i).symm) F)).coeff
        ((Finsupp.mapDomain (⇑e) σ) none)) =
    coeff (Finsupp.mapDomain (⇑e) σ) ((rename ⇑(Equiv.optionSubtypeNe i).symm) F)
⊢ False

Tactic:
coeff_rename_mapDomain _
      e.injective,

Goal state after:
case refine_1
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
σ : ι →₀ ℕ
hσ : σ ∈ F.support
i : ι
hσi : σ i ≠ 0
H✝ : (F.toPolynomialAdjoinImageCompl a i).coeff (σ i) = 0
F₀ : Polynomial (MvPolynomial { b // b ≠ i } k) :=
  (optionEquivLeft k { b // b ≠ i }) ((renameEquiv k (Equiv.optionSubtypeNe i).symm) F)
H : F₀.coeff (σ i) = 0
e : ι ≃ Option { b // b ≠ i } := (Equiv.optionSubtypeNe i).symm
this :
  coeff (Finsupp.mapDomain (⇑e) σ).some
      (((optionEquivLeft k { b // b ≠ i }) ((rename ⇑(Equiv.optionSubtypeNe i).symm) F)).coeff
        ((Finsupp.mapDomain (⇑e) σ) none)) =
    coeff σ F
⊢ False
Module: Mathlib.AlgebraicGeometry.Morphisms.Etale

Goal state before:
pp: X✝ Y : Scheme
f : X✝ ⟶ Y
X : Scheme
⊢ ∀ ⦃Y : Scheme⦄ (f : X ⟶ Y), (@LocallyOfFiniteType ⊓ @FormallyUnramified) f → diagonal (@Etale) f

Tactic:
Y

Goal state after:
X✝ Y✝ : Scheme
f : X✝ ⟶ Y✝
X Y : Scheme
⊢ ∀ (f : X ⟶ Y), (@LocallyOfFiniteType ⊓ @FormallyUnramified) f → diagonal (@Etale) f
Module: Mathlib.AlgebraicGeometry.Morphisms.Etale

Goal state before:
pp: X✝ Y : Scheme
f : X✝ ⟶ Y
X : Scheme
⊢ ∀ ⦃Y : Scheme⦄ (f : X ⟶ Y), Etale f → (@LocallyOfFiniteType ⊓ @FormallyUnramified) f

Tactic:
Y

Goal state after:
X✝ Y✝ : Scheme
f : X✝ ⟶ Y✝
X Y : Scheme
⊢ ∀ (f : X ⟶ Y), Etale f → (@LocallyOfFiniteType ⊓ @FormallyUnramified) f
Module: Mathlib.AlgebraicGeometry.Morphisms.LocalIso

Goal state before:
pp: P : MorphismProperty Scheme
inst✝¹ : P.ContainsIdentities
inst✝ : IsZariskiLocalAtSource P
X : Scheme
⊢ @IsLocalIso X ≤ P

Tactic:
Y

Goal state after:
P : MorphismProperty Scheme
inst✝¹ : P.ContainsIdentities
inst✝ : IsZariskiLocalAtSource P
X Y : Scheme
⊢ IsLocalIso ≤ P
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
H : ∀ (s : Finset K), LinearIndepOn k id ↑s → LinearIndepOn k (fun x ↦ x ^ p) ↑s
a : ι → K
n : ι
inst✝ : ExpChar k p
ha' : IsTranscendenceBasis k fun i ↦ a ↑i
S : Set (MvPolynomial ι k) := {F | F ≠ 0 ∧ (aeval a) F = 0}
F : MvPolynomial ι k
hFmin : ∀ (G : MvPolynomial ι k), G ≠ 0 → (aeval a) G = 0 → F.totalDegree ≤ G.totalDegree
hF₀ : F ≠ 0
hFa : (aeval a) F = 0
hFirr : Irreducible F
i : ι
σ : ι →₀ ℕ
hσ : σ ∈ F.support
hi : ¬p ∣ σ i
hσi : σ i ≠ 0
alg : IsAlgebraic (↥(Algebra.adjoin k (a '' {i}ᶜ))) (a i)
Hi : IsTranscendenceBasis k fun x ↦ a ↑x
k' : IntermediateField k K := adjoin k (a '' {i}ᶜ)
hF₁irr : Irreducible (F.toPolynomialAdjoinImageCompl a i)
this✝ : UniqueFactorizationMonoid ↥(Algebra.adjoin k (a '' {i}ᶜ))
hF₂irr :
  Irreducible (Polynomial.map (algebraMap ↥(Algebra.adjoin k (a '' {i}ᶜ)) ↥k') (F.toPolynomialAdjoinImageCompl a i))
Hsep : ¬IsSeparable (↥(adjoin k (a '' {i}ᶜ))) (a i)
this : CharP (↥k') p
g : Polynomial ↥k'
hg : Irreducible g
eq : ((Polynomial.expand (↥k') p) g).coeff (σ i) = (minpoly (↥k') (a i)).coeff (σ i)
⊢ (F.toPolynomialAdjoinImageCompl a i).coeff (σ i) = 0

Tactic:
rwa [← minpoly.eq_of_irreducible hF₂irr ((Polynomial.aeval_map_algebraMap ..).trans
    (aeval_toPolynomialAdjoinImageCompl_eq_zero hFa i)), Polynomial.coeff_mul_C,
    Polynomial.coeff_expand hp.pos, if_neg hi, eq_mul_inv_iff_mul_eq₀
    (by simpa using hF₂irr.ne_zero), zero_mul, eq_comm,
    Polynomial.coeff_map, map_eq_zero_iff _ (FaithfulSMul.algebraMap_injective ..)] at eq

Goal state after: