awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Smooth.Quotient
Goal:
R : Type u_1
inst : CommRing R
J I : Ideal R
sq : I * I = ⊥
f : J.Cotangent →ₗ[R] J.Cotangent
le : f.range ≤ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J))
x y : R
hy : y ∈ I
z : R
hz : z ∈ J
w : ↥J
hw : w ∈ Submodule.comap (Submodule.subtype J) (I * J)
eqz :
  Eq (α := J.Cotangent) ((J.toCotangent : (a : ↥J) → J.Cotangent) w : J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) z hz)) :
      J.Cotangent)
mem_bot : HMul.hMul (β := R) y ((Submodule.subtype J : (a : ↥J) → R) w : R) = 0
eq0 : y • w = 0
⊢ Subtype.mk (p := fun (x : R) ↦ x ∈ J) (y * z) ⋯ = y • Subtype.mk (p := fun (x : R) ↦ x ∈ J) z hz

Tactic:
have : ⟨y * z, Ideal.mul_le_left (Submodule.mul_mem_mul hy hz)⟩ = y • (⟨z, hz⟩ : J) := rfl
-- Module: Mathlib.RingTheory.Smooth.Quotient
Goal:
R : Type u_1
inst : CommRing R
J I : Ideal R
sq : I * I = ⊥
f : J.Cotangent →ₗ[R] J.Cotangent
le : f.range ≤ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J))
x y : R
hy : y ∈ I
z : R
hz : z ∈ J
w : ↥J
hw : w ∈ Submodule.comap (Submodule.subtype J) (I * J)
eqz :
  Eq (α := J.Cotangent) ((J.toCotangent : (a : ↥J) → J.Cotangent) w : J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) z hz)) :
      J.Cotangent)
mem_bot : HMul.hMul (β := R) y ((Submodule.subtype J : (a : ↥J) → R) w : R) = 0
eq0 : y • w = 0
this : Subtype.mk (p := fun (x : R) ↦ x ∈ J) (y * z) ⋯ = y • Subtype.mk (p := fun (x : R) ↦ x ∈ J) z hz
mem_mul_mem :
  Eq (α := J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        ((J.toCotangent : (a : ↥J) → J.Cotangent) (y • Subtype.mk (p := fun (x : R) ↦ x ∈ J) z hz)) :
      J.Cotangent)
    (0 : J.Cotangent)
mem_mul_mem₁ :
  Eq (α := J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        (HSMul.hSMul (β := J.Cotangent) y
          ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) z hz) : J.Cotangent)) :
      J.Cotangent)
    (0 : J.Cotangent)
mem_mul_mem₂ :
  HSMul.hSMul (β := J.Cotangent) y
      ((f : (a : J.Cotangent) → J.Cotangent)
          ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) z hz)) :
        J.Cotangent) =
    0
mem_mul_mem₃ : HSMul.hSMul (β := J.Cotangent) y ((J.toCotangent : (a : ↥J) → J.Cotangent) w : J.Cotangent) = 0
mem_mul_mem₄ : Eq (α := J.Cotangent) ((J.toCotangent : (a : ↥J) → J.Cotangent) (y • w) : J.Cotangent) (0 : J.Cotangent)
mem_mul_mem₅ : Eq (α := J.Cotangent) ((J.toCotangent : (a : ↥J) → J.Cotangent) 0) 0
mem_mul_mem₆ mem_mul_mem₇ : Eq.{u_1 + 1} (α := J.Cotangent) 0 0
⊢ Eq (α := J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) (y * z) ⋯)) :
      J.Cotangent)
    (0 : J.Cotangent)

Tactic:
rw [this, map_smul, map_smul, ← eqz, ← map_smul, eq0, map_zero]

Premises used: map_zero, map_smul
-- Module: Mathlib.RingTheory.Smooth.Quotient
Goal:
R : Type u_1
inst : CommRing R
J I : Ideal R
sq : I * I = ⊥
f : J.Cotangent →ₗ[R] J.Cotangent
le : f.range ≤ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J))
x y : R
ymem : y ∈ I * J
z : R
zmem : z ∈ I * J
hy :
  Eq (α := J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) y ⋯)) :
      J.Cotangent)
    (0 : J.Cotangent)
hz :
  Eq (α := J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) z ⋯)) :
      J.Cotangent)
    (0 : J.Cotangent)
⊢ Subtype.mk (p := fun (x : R) ↦ x ∈ J) (y + z) ⋯ =
    Subtype.mk (p := fun (x : R) ↦ x ∈ J) y ⋯ + Subtype.mk (p := fun (x : R) ↦ x ∈ J) z ⋯

Tactic:
have : (⟨y + z, Ideal.mul_le_left (add_mem ymem zmem)⟩ : J) =
        ⟨y, Ideal.mul_le_left ymem⟩ + ⟨z, Ideal.mul_le_left zmem⟩ := rfl
-- Module: Mathlib.RingTheory.Smooth.Quotient
Goal:
R : Type u_1
inst : CommRing R
J I : Ideal R
sq : I * I = ⊥
f : J.Cotangent →ₗ[R] J.Cotangent
le : f.range ≤ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J))
x y : R
ymem : y ∈ I * J
z : R
zmem : z ∈ I * J
hy :
  Eq (α := J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) y ⋯)) :
      J.Cotangent)
    (0 : J.Cotangent)
hz :
  Eq (α := J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) z ⋯)) :
      J.Cotangent)
    (0 : J.Cotangent)
this :
  Subtype.mk (p := fun (x : R) ↦ x ∈ J) (y + z) ⋯ =
    Subtype.mk (p := fun (x : R) ↦ x ∈ J) y ⋯ + Subtype.mk (p := fun (x : R) ↦ x ∈ J) z ⋯
add :
  Eq (α := J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        ((J.toCotangent : (a : ↥J) → J.Cotangent)
          (Subtype.mk (p := fun (x : R) ↦ x ∈ J) y ⋯ + Subtype.mk (p := fun (x : R) ↦ x ∈ J) z ⋯)) :
      J.Cotangent)
    (0 : J.Cotangent)
add₁ :
  Eq (α := J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        (HAdd.hAdd (α := J.Cotangent) (β := J.Cotangent)
          ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) y ⋯) : J.Cotangent)
          ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) z ⋯) : J.Cotangent)) :
      J.Cotangent)
    (0 : J.Cotangent)
add₂ :
  HAdd.hAdd (α := J.Cotangent) (β := J.Cotangent)
      ((f : (a : J.Cotangent) → J.Cotangent)
          ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) y ⋯)) :
        J.Cotangent)
      ((f : (a : J.Cotangent) → J.Cotangent)
          ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) z ⋯)) :
        J.Cotangent) =
    0
add₃ :
  HAdd.hAdd (α := J.Cotangent) (β := J.Cotangent) (0 : J.Cotangent)
      ((f : (a : J.Cotangent) → J.Cotangent)
          ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) z ⋯)) :
        J.Cotangent) =
    0
add₄ : HAdd.hAdd (α := J.Cotangent) 0 0 = 0
add₅ add₆ : Eq.{u_1 + 1} (α := J.Cotangent) 0 0
⊢ Eq (α := J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) (y + z) ⋯)) :
      J.Cotangent)
    (0 : J.Cotangent)

Tactic:
rw [this, map_add, map_add, hy, hz, add_zero]

Premises used: map_add, add_zero
-- Module: Mathlib.RingTheory.Smooth.Quotient
Goal:
R : Type u_1
inst : CommRing R
J I : Ideal R
sq : I * I = ⊥
f : J.Cotangent →ₗ[R] J.Cotangent
le : f.range ≤ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J))
x : R
h : x ∈ I * J
mem_mul_mem :
  ∀ (y : R) (hy : y ∈ I) (z : R) (hz : z ∈ J),
    Eq (α := J.Cotangent)
      ((f : (a : J.Cotangent) → J.Cotangent)
          ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) (y * z) ⋯)) :
        J.Cotangent)
      (0 : J.Cotangent)
add :
  ∀ (y : R) (ymem : y ∈ I * J) (z : R) (zmem : z ∈ I * J)
    (hy :
      Eq (α := J.Cotangent)
        ((f : (a : J.Cotangent) → J.Cotangent)
            ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) y ⋯)) :
          J.Cotangent)
        (0 : J.Cotangent))
    (hz :
      Eq (α := J.Cotangent)
        ((f : (a : J.Cotangent) → J.Cotangent)
            ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) z ⋯)) :
          J.Cotangent)
        (0 : J.Cotangent)),
    Eq (α := J.Cotangent)
      ((f : (a : J.Cotangent) → J.Cotangent)
          ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) (y + z) ⋯)) :
        J.Cotangent)
      (0 : J.Cotangent)
⊢ Eq (α := J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) x ⋯)) :
      J.Cotangent)
    (0 : J.Cotangent)

Tactic:
induction h using Submodule.mul_induction_on' with
    | mem_mul_mem y hy z hz =>
      rcases Submodule.mem_map.mp (le (f.mem_range_self (J.toCotangent ⟨z, hz⟩))) with ⟨w, hw, eqz⟩
      have mem_bot := Ideal.mul_mem_mul hy (Submodule.mem_comap.mp hw)
      simp only [← mul_assoc, sq, Submodule.bot_mul, Submodule.mem_bot] at mem_bot
      have eq0 : y • w = 0 := SetCoe.ext mem_bot
      have : ⟨y * z, Ideal.mul_le_left (Submodule.mul_mem_mul hy hz)⟩ = y • (⟨z, hz⟩ : J) := rfl
      rw [this, map_smul, map_smul, ← eqz, ← map_smul, eq0, map_zero]
    | add y ymem z zmem hy hz =>
      have : (⟨y + z, Ideal.mul_le_left (add_mem ymem zmem)⟩ : J) =
        ⟨y, Ideal.mul_le_left ymem⟩ + ⟨z, Ideal.mul_le_left zmem⟩ := rfl
      rw [this, map_add, map_add, hy, hz, add_zero]

Premises used: Submodule.mem_bot, mul_assoc, map_zero, map_add, Submodule.bot_mul, add_zero, map_smul
-- Module: Mathlib.RingTheory.Smooth.Quotient
Goal:
R : Type u_1
inst : CommRing R
J I : Ideal R
sq : I * I = ⊥
f : J.Cotangent →ₗ[R] J.Cotangent
le : f.range ≤ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J))
⊢ ∀ {x : R} (h : x ∈ I * J),
    Eq (α := J.Cotangent)
      ((f : (a : J.Cotangent) → J.Cotangent)
          ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) x ⋯)) :
        J.Cotangent)
      (0 : J.Cotangent)

Tactic:
have {x : R} (h : x ∈ I * J) : f (J.toCotangent ⟨x, Ideal.mul_le_left h⟩) = 0 := by
    induction h using Submodule.mul_induction_on' with
    | mem_mul_mem y hy z hz =>
      rcases Submodule.mem_map.mp (le (f.mem_range_self (J.toCotangent ⟨z, hz⟩))) with ⟨w, hw, eqz⟩
      have mem_bot := Ideal.mul_mem_mul hy (Submodule.mem_comap.mp hw)
      simp only [← mul_assoc, sq, Submodule.bot_mul, Submodule.mem_bot] at mem_bot
      have eq0 : y • w = 0 := SetCoe.ext mem_bot
      have : ⟨y * z, Ideal.mul_le_left (Submodule.mul_mem_mul hy hz)⟩ = y • (⟨z, hz⟩ : J) := rfl
      rw [this, map_smul, map_smul, ← eqz, ← map_smul, eq0, map_zero]
    | add y ymem z zmem hy hz =>
      have : (⟨y + z, Ideal.mul_le_left (add_mem ymem zmem)⟩ : J) =
        ⟨y, Ideal.mul_le_left ymem⟩ + ⟨z, Ideal.mul_le_left zmem⟩ := rfl
      rw [this, map_add, map_add, hy, hz, add_zero]
-- Module: Mathlib.RingTheory.Smooth.Quotient
Goal:
R : Type u_1
inst : CommRing R
J I : Ideal R
sq : I * I = ⊥
f : J.Cotangent →ₗ[R] J.Cotangent
le : f.range ≤ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J))
this :
  ∀ {x : R} (h : x ∈ I * J),
    Eq (α := J.Cotangent)
      ((f : (a : J.Cotangent) → J.Cotangent)
          ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) x ⋯)) :
        J.Cotangent)
      (0 : J.Cotangent)
x : J.Cotangent
hx : x ∈ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J))
rcases :
  ∀ (x' : ↥J) (hx' : x' ∈ Submodule.comap (Submodule.subtype J) (I * J))
    (eq : (J.toCotangent : (a : ↥J) → J.Cotangent) x' = x), x ∈ f.ker
⊢ x ∈ f.ker

Tactic:
rcases Submodule.mem_map.mp hx with ⟨x', hx', eq⟩

Premises used: Submodule.mem_map, Iff.mp
-- Module: Mathlib.RingTheory.Smooth.Quotient
Goal:
R : Type u_1
inst : CommRing R
J I : Ideal R
sq : I * I = ⊥
f : J.Cotangent →ₗ[R] J.Cotangent
le : f.range ≤ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J))
this :
  ∀ {x : R} (h : x ∈ I * J),
    Eq (α := J.Cotangent)
      ((f : (a : J.Cotangent) → J.Cotangent)
          ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) x ⋯)) :
        J.Cotangent)
      (0 : J.Cotangent)
x : J.Cotangent
hx : x ∈ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J))
x' : ↥J
hx' : x' ∈ Submodule.comap (Submodule.subtype J) (I * J)
eq : (J.toCotangent : (a : ↥J) → J.Cotangent) x' = x
⊢ x ∈ f.ker

Tactic:
simpa [← eq] using this hx'
-- Module: Mathlib.RingTheory.Smooth.Quotient
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
R' : Type u_3
S' : Type u_4
inst_2 : CommRing R'
inst_3 : CommRing S'
f : R →+* S
flat : f.Flat
qR : R →+* R'
qS : S →+* S'
g : R' →+* S'
surjR : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R) (β := R') (⇑qR : (a : R) → R')
surjS : Function.Surjective.{u_2 + 1, u_4 + 1} (α := S) (β := S') (⇑qS : (a : S) → S')
comm : qS.comp f = g.comp qR
sq0 : HPow.hPow (α := Ideal R) (β := ℕ) (ker qR) 2 = ⊥
eqmap : Eq (α := Ideal S) (ker qS) (Ideal.map f (ker qR))
smoothq : g.FormallySmooth
⊢ Module.Flat R S

Tactic:
algebraize [f, qR, qS, g, qS.comp f]

Premises used: RingHom.comp
-- Module: Mathlib.RingTheory.Smooth.Quotient
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
R' : Type u_3
S' : Type u_4
inst_2 : CommRing R'
inst_3 : CommRing S'
f : R →+* S
flat : f.Flat
qR : R →+* R'
qS : S →+* S'
g : R' →+* S'
surjR : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R) (β := R') (⇑qR : (a : R) → R')
surjS : Function.Surjective.{u_2 + 1, u_4 + 1} (α := S) (β := S') (⇑qS : (a : S) → S')
comm : qS.comp f = g.comp qR
sq0 : HPow.hPow (α := Ideal R) (β := ℕ) (ker qR) 2 = ⊥
eqmap : Eq (α := Ideal S) (ker qS) (Ideal.map f (ker qR))
smoothq : g.FormallySmooth
algebraizeInst : Module.Flat R S
⊢ Algebra.FormallySmooth R' S'

Tactic:
algebraize [f, qR, qS, g, qS.comp f]

Premises used: RingHom.comp
-- Module: Mathlib.RingTheory.Smooth.Quotient
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
R' : Type u_3
S' : Type u_4
inst_2 : CommRing R'
inst_3 : CommRing S'
f : R →+* S
flat : f.Flat
qR : R →+* R'
qS : S →+* S'
g : R' →+* S'
surjR : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R) (β := R') (⇑qR : (a : R) → R')
surjS : Function.Surjective.{u_2 + 1, u_4 + 1} (α := S) (β := S') (⇑qS : (a : S) → S')
comm : qS.comp f = g.comp qR
sq0 : HPow.hPow (α := Ideal R) (β := ℕ) (ker qR) 2 = ⊥
eqmap : Eq (α := Ideal S) (ker qS) (Ideal.map f (ker qR))
smoothq : g.FormallySmooth
algInst : Algebra R S := f.toAlgebra
algInst_1 : Algebra R R' := qR.toAlgebra
algInst_2 : Algebra S S' := qS.toAlgebra
algInst_3 : Algebra R' S' := g.toAlgebra
algInst_4 : Algebra R S' := (qS.comp f).toAlgebra
scalarTowerInst : IsScalarTower R S S' := ⋯
algebraizeInst : Module.Flat R S
algebraizeInst_1 : Algebra.FormallySmooth R' S'
h : IsScalarTower R R' S' := ⋯
⊢ f.FormallySmooth

Tactic:
Algebra.FormallySmooth.of_surjective_of_ker_eq_map_of_flat surjR surjS eqmap sq0 ‹_›

Premises used: Algebra.FormallySmooth.of_surjective_of_ker_eq_map_of_flat, RingHom.FormallySmooth
-- Module: Mathlib.RingTheory.Smooth.Quotient
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
R' : Type u_3
S' : Type u_4
inst_2 : CommRing R'
inst_3 : CommRing S'
f : R →+* S
flat : f.Flat
qR : R →+* R'
qS : S →+* S'
g : R' →+* S'
surjR : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R) (β := R') (⇑qR : (a : R) → R')
surjS : Function.Surjective.{u_2 + 1, u_4 + 1} (α := S) (β := S') (⇑qS : (a : S) → S')
comm : qS.comp f = g.comp qR
sq0 : HPow.hPow (α := Ideal R) (β := ℕ) (ker qR) 2 = ⊥
eqmap : Eq (α := Ideal S) (ker qS) (Ideal.map f (ker qR))
smoothq : g.FormallySmooth
algInst : Algebra R S := f.toAlgebra
algInst_1 : Algebra R R' := qR.toAlgebra
algInst_2 : Algebra S S' := qS.toAlgebra
algInst_3 : Algebra R' S' := g.toAlgebra
algInst_4 : Algebra R S' := (qS.comp f).toAlgebra
scalarTowerInst : IsScalarTower R S S' := ⋯
algebraizeInst : Module.Flat R S
algebraizeInst_1 : Algebra.FormallySmooth R' S'
h : IsScalarTower R R' S' := ⋯
⊢ f.FormallySmooth

Tactic:
exact Algebra.FormallySmooth.of_surjective_of_ker_eq_map_of_flat surjR surjS eqmap sq0 ‹_›

Premises used: Algebra.FormallySmooth.of_surjective_of_ker_eq_map_of_flat
-- Module: Mathlib.RingTheory.Smooth.StandardSmooth
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
inst_4 : Finite ι
P : SubmersivePresentation R S ι σ
⊢ IsStandardSmooth R S

Tactic:
⟨_, _, _, inferInstance, ⟨P.reindex (Fintype.equivFin _).symm (Fintype.equivFin _).symm⟩⟩

Premises used: inferInstance, Algebra.SubmersivePresentation.reindex, Nonempty.intro, Fintype.equivFin, And.intro, Algebra.IsStandardSmooth.mk, Exists.intro, Equiv.symm
-- Module: Mathlib.RingTheory.Smooth.StandardSmooth
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
inst_4 : Finite ι
P : SubmersivePresentation R S ι σ
⊢ IsStandardSmooth R S

Tactic:
exact ⟨_, _, _, inferInstance, ⟨P.reindex (Fintype.equivFin _).symm (Fintype.equivFin _).symm⟩⟩
-- Module: Mathlib.RingTheory.Smooth.StandardSmooth
Goal:
n : ℕ
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
inst_4 : Finite ι
P : SubmersivePresentation R S ι σ
hP : P.dimension = n
⊢ IsStandardSmoothOfRelativeDimension n R S

Tactic:
⟨⟨_, _, _, inferInstance,
    P.reindex (Fintype.equivFin _).symm (Fintype.equivFin σ).symm, ?_⟩⟩

Premises used: inferInstance, Algebra.SubmersivePresentation.reindex, Fintype.equivFin, Exists.intro, Equiv.symm, Algebra.IsStandardSmoothOfRelativeDimension.mk
-- Module: Mathlib.RingTheory.Smooth.StandardSmooth
Goal:
n : ℕ
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
inst_4 : Finite ι
P : SubmersivePresentation R S ι σ
hP : P.dimension = n
refine :
  Presentation.dimension (ι := Fin (Fintype.card ι)) (σ := Fin (Fintype.card σ))
      (PreSubmersivePresentation.toPresentation
        (toPreSubmersivePresentation (P.reindex (Equiv.symm (Fintype.equivFin ι)) (Equiv.symm (Fintype.equivFin σ))))) =
    n
⊢ IsStandardSmoothOfRelativeDimension n R S

Tactic:
refine ⟨⟨_, _, _, inferInstance,
    P.reindex (Fintype.equivFin _).symm (Fintype.equivFin σ).symm, ?_⟩⟩
-- Module: Mathlib.RingTheory.Smooth.StandardSmooth
Goal:
n : ℕ
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
inst_4 : Finite ι
P : SubmersivePresentation R S ι σ
hP : P.dimension = n
⊢ Presentation.dimension (ι := Fin (Fintype.card ι)) (σ := Fin (Fintype.card σ))
      (PreSubmersivePresentation.toPresentation
        (toPreSubmersivePresentation (P.reindex (Equiv.symm (Fintype.equivFin ι)) (Equiv.symm (Fintype.equivFin σ))))) =
    n

Tactic:
simp [hP]
-- Module: Mathlib.RingTheory.Smooth.StandardSmooth
Goal:
n : ℕ
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
H : IsStandardSmoothOfRelativeDimension n R S
⊢ IsStandardSmooth R S

Tactic:
⟨_, _, _, H.out.choose_spec.choose_spec.choose_spec.choose,
    H.out.choose_spec.choose_spec.choose_spec.choose_spec.nonempty⟩

Premises used: Exists.choose_spec, Exists.nonempty, And.intro, Algebra.IsStandardSmooth.mk, Exists.intro, Exists.choose, Algebra.IsStandardSmoothOfRelativeDimension.out
-- Module: Mathlib.RingTheory.Smooth.StandardSmooth
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
h : Function.Bijective.{u + 1, v + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ IsStandardSmoothOfRelativeDimension 0 R S

Tactic:
⟨_, _, _, inferInstance,
    SubmersivePresentation.ofBijectiveAlgebraMap h, Presentation.ofBijectiveAlgebraMap_dimension h⟩

Premises used: Algebra.SubmersivePresentation.ofBijectiveAlgebraMap, inferInstance, Algebra.Presentation.ofBijectiveAlgebraMap_dimension, Exists.intro, Algebra.IsStandardSmoothOfRelativeDimension.mk
-- Module: Mathlib.RingTheory.Smooth.StandardSmooth
Goal:
n m : ℕ
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
⊢ IsStandardSmoothOfRelativeDimension 0 R R

Tactic:
IsStandardSmoothOfRelativeDimension.of_algebraMap_bijective Function.bijective_id

Premises used: Function.bijective_id, Algebra.IsStandardSmoothOfRelativeDimension.of_algebraMap_bijective
-- Module: Mathlib.RingTheory.Smooth.StandardSmooth
Goal:
n m : ℕ
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
inst_4 : IsStandardSmooth R S
obtain :
  ∀ (w w_1 : Type) (w_2 : Finite w_1), Finite w → ∀ (P : SubmersivePresentation R S w w_1), FinitePresentation R S
⊢ FinitePresentation R S

Tactic:
obtain ⟨_, _, _, _, ⟨P⟩⟩ := ‹IsStandardSmooth R S›

Premises used: Algebra.IsStandardSmooth
-- Module: Mathlib.RingTheory.Smooth.StandardSmooth
Goal:
n m : ℕ
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
inst_4 : IsStandardSmooth R S
w w_1 : Type
w_2 : Finite w_1
left : Finite w
P : SubmersivePresentation R S w w_1
⊢ FinitePresentation R S

Tactic:
P.finitePresentation_of_isFinite

Premises used: Algebra.SubmersivePresentation.toPreSubmersivePresentation, Algebra.PreSubmersivePresentation.toPresentation, Algebra.Presentation.finitePresentation_of_isFinite
-- Module: Mathlib.RingTheory.Smooth.StandardSmooth
Goal:
n m : ℕ
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
inst_4 : IsStandardSmooth R S
w w_1 : Type
w_2 : Finite w_1
left : Finite w
P : SubmersivePresentation R S w w_1
⊢ FinitePresentation R S

Tactic:
exact P.finitePresentation_of_isFinite

Premises used: Algebra.SubmersivePresentation.toPreSubmersivePresentation, Algebra.PreSubmersivePresentation.toPresentation, Algebra.Presentation.finitePresentation_of_isFinite
-- Module: Mathlib.RingTheory.Smooth.StandardSmooth
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_1
inst_3 : CommRing T
inst_4 : Algebra R T
e : S ≃ₐ[R] T
inst_5 : IsStandardSmooth R S
obtain : ∀ (w w_1 : Type) (w_2 : Finite w_1), Finite w → ∀ (P : SubmersivePresentation R S w w_1), IsStandardSmooth R T
⊢ IsStandardSmooth R T

Tactic:
obtain ⟨_, _, _, _, ⟨P⟩⟩ := ‹IsStandardSmooth R S›

Premises used: Algebra.IsStandardSmooth
-- Module: Mathlib.RingTheory.Smooth.StandardSmooth
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_1
inst_3 : CommRing T
inst_4 : Algebra R T
e : S ≃ₐ[R] T
inst_5 : IsStandardSmooth R S
w w_1 : Type
w_2 : Finite w_1
left : Finite w
P : SubmersivePresentation R S w w_1
⊢ IsStandardSmooth R T

Tactic:
(P.ofAlgEquiv e).isStandardSmooth

Premises used: Algebra.SubmersivePresentation.isStandardSmooth, Algebra.SubmersivePresentation.ofAlgEquiv
-- Module: Mathlib.RingTheory.Smooth.StandardSmooth
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_1
inst_3 : CommRing T
inst_4 : Algebra R T
e : S ≃ₐ[R] T
inst_5 : IsStandardSmooth R S
w w_1 : Type
w_2 : Finite w_1
left : Finite w
P : SubmersivePresentation R S w w_1
⊢ IsStandardSmooth R T

Tactic:
exact (P.ofAlgEquiv e).isStandardSmooth

Premises used: Algebra.SubmersivePresentation.isStandardSmooth, Algebra.SubmersivePresentation.ofAlgEquiv
-- Module: Mathlib.RingTheory.Smooth.StandardSmooth
Goal:
n : ℕ
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_1
inst_3 : CommRing T
inst_4 : Algebra R T
e : S ≃ₐ[R] T
inst_5 : IsStandardSmoothOfRelativeDimension n R S
obtain :
  ∀ (w w_1 : Type) (w_2 : Finite w_1),
    Finite w →
      ∀ (P : SubmersivePresentation R S w w_1) (hP : P.dimension = n), IsStandardSmoothOfRelativeDimension n R T
⊢ IsStandardSmoothOfRelativeDimension n R T

Tactic:
obtain ⟨_, _, _, _, ⟨P, hP⟩⟩ := ‹IsStandardSmoothOfRelativeDimension n R S›

Premises used: Algebra.IsStandardSmoothOfRelativeDimension
-- Module: Mathlib.RingTheory.Smooth.StandardSmooth
Goal:
n : ℕ
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_1
inst_3 : CommRing T
inst_4 : Algebra R T
e : S ≃ₐ[R] T
inst_5 : IsStandardSmoothOfRelativeDimension n R S
w w_1 : Type
w_2 : Finite w_1
w_3 : Finite w
P : SubmersivePresentation R S w w_1
hP : P.dimension = n
⊢ (P.ofAlgEquiv e).dimension = n

Tactic:
simpa