awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.LocalRing.Etale
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing S
inst_4 : IsLocalRing R
inst_5 : Module.Finite R S
inst_6 : FaithfulSMul R S
inst_7 : FormallyUnramified R S
β : S
hβ :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := (ResidueField R)[X]) (β := ResidueField S)
    (⇑(aeval ((residue S : (a : S) → ResidueField S) β) :
          AlgHom.{u_1, u_1, u_2} (ResidueField R) (ResidueField R)[X] (ResidueField S)) :
      (a : (ResidueField R)[X]) → ResidueField S)
s : S
h : Membership.mem (γ := Submodule R S) ⊤ s
q : R[X]
hp :
  Eq.{u_2 + 1} (α := ResidueField S)
    (((aeval ((residue S : (a : S) → ResidueField S) β) :
            AlgHom.{u_1, u_1, u_2} (ResidueField R) (ResidueField R)[X] (ResidueField S)) :
          (a : (ResidueField R)[X]) → ResidueField S)
        (map (residue R) q) :
      ResidueField S)
    ((residue S : (a : S) → ResidueField S) s : ResidueField S)
mp :
  Eq (α := HasQuotient.Quotient S (B := Ideal S) (maximalIdeal S : Ideal S))
    ((Ideal.Quotient.mk (maximalIdeal S) : (a : S) → S ⧸ maximalIdeal S) s :
      HasQuotient.Quotient S (B := Ideal S) (maximalIdeal S : Ideal S))
    ((Ideal.Quotient.mk (maximalIdeal S) : (a : S) → S ⧸ maximalIdeal S) ((aeval β : (a : R[X]) → S) q) :
      HasQuotient.Quotient S (B := Ideal S) (maximalIdeal S : Ideal S))
⊢ Membership.mem (γ := Submodule R S)
    (Submodule.restrictScalars R (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)))
    (HSub.hSub (β := S) s ((aeval β : (a : R[X]) → S) q : S))

Tactic:
rw [Algebra.FormallyUnramified.map_maximalIdeal, Submodule.restrictScalars_mem,
        ← Ideal.Quotient.eq]

Premises used: Ideal.Quotient.eq, Submodule.restrictScalars_mem, Algebra.FormallyUnramified.map_maximalIdeal
-- Module: Mathlib.RingTheory.LocalRing.Etale
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing S
inst_4 : IsLocalRing R
inst_5 : Module.Finite R S
inst_6 : FaithfulSMul R S
inst_7 : FormallyUnramified R S
β : S
hβ :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := (ResidueField R)[X]) (β := ResidueField S)
    (⇑(aeval ((residue S : (a : S) → ResidueField S) β) :
          AlgHom.{u_1, u_1, u_2} (ResidueField R) (ResidueField R)[X] (ResidueField S)) :
      (a : (ResidueField R)[X]) → ResidueField S)
s : S
h : Membership.mem (γ := Submodule R S) ⊤ s
q : R[X]
hp :
  Eq.{u_2 + 1} (α := ResidueField S)
    (((aeval ((residue S : (a : S) → ResidueField S) β) :
            AlgHom.{u_1, u_1, u_2} (ResidueField R) (ResidueField R)[X] (ResidueField S)) :
          (a : (ResidueField R)[X]) → ResidueField S)
        (map (residue R) q) :
      ResidueField S)
    ((residue S : (a : S) → ResidueField S) s : ResidueField S)
⊢ Eq (α := ResidueField S) ((residue S : (a : S) → ResidueField S) ((aeval β : (a : R[X]) → S) q) : ResidueField S)
    ((residue S : (a : S) → ResidueField S) s : ResidueField S)

Tactic:
rw [← map_aeval_eq_aeval_map (ψ := residue S) (φ := residue R) rfl] at hp

Premises used: Polynomial.map_aeval_eq_aeval_map, rfl
-- Module: Mathlib.RingTheory.LocalRing.Etale
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing S
inst_4 : IsLocalRing R
inst_5 : Module.Finite R S
inst_6 : FaithfulSMul R S
inst_7 : FormallyUnramified R S
β : S
hβ :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := (ResidueField R)[X]) (β := ResidueField S)
    (⇑(aeval ((residue S : (a : S) → ResidueField S) β) :
          AlgHom.{u_1, u_1, u_2} (ResidueField R) (ResidueField R)[X] (ResidueField S)) :
      (a : (ResidueField R)[X]) → ResidueField S)
s : S
h : Membership.mem (γ := Submodule R S) ⊤ s
q : R[X]
hp :
  Eq (α := ResidueField S) ((residue S : (a : S) → ResidueField S) ((aeval β : (a : R[X]) → S) q) : ResidueField S)
    ((residue S : (a : S) → ResidueField S) s : ResidueField S)
⊢ Eq (α := HasQuotient.Quotient S (B := Ideal S) (maximalIdeal S : Ideal S))
    ((Ideal.Quotient.mk (maximalIdeal S) : (a : S) → S ⧸ maximalIdeal S) s :
      HasQuotient.Quotient S (B := Ideal S) (maximalIdeal S : Ideal S))
    ((Ideal.Quotient.mk (maximalIdeal S) : (a : S) → S ⧸ maximalIdeal S) ((aeval β : (a : R[X]) → S) q) :
      HasQuotient.Quotient S (B := Ideal S) (maximalIdeal S : Ideal S))

Tactic:
hp.symm

Premises used: IsLocalRing.ResidueField, Eq.symm
-- Module: Mathlib.RingTheory.LocalRing.Etale
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing S
inst_4 : IsLocalRing R
inst_5 : Module.Finite R S
inst_6 : FaithfulSMul R S
inst_7 : FormallyUnramified R S
β : S
hβ :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := (ResidueField R)[X]) (β := ResidueField S)
    (⇑(aeval ((residue S : (a : S) → ResidueField S) β) :
          AlgHom.{u_1, u_1, u_2} (ResidueField R) (ResidueField R)[X] (ResidueField S)) :
      (a : (ResidueField R)[X]) → ResidueField S)
s : S
h : Membership.mem (γ := Submodule R S) ⊤ s
q : R[X]
hp :
  Eq (α := ResidueField S) ((residue S : (a : S) → ResidueField S) ((aeval β : (a : R[X]) → S) q) : ResidueField S)
    ((residue S : (a : S) → ResidueField S) s : ResidueField S)
⊢ Eq (α := HasQuotient.Quotient S (B := Ideal S) (maximalIdeal S : Ideal S))
    ((Ideal.Quotient.mk (maximalIdeal S) : (a : S) → S ⧸ maximalIdeal S) s :
      HasQuotient.Quotient S (B := Ideal S) (maximalIdeal S : Ideal S))
    ((Ideal.Quotient.mk (maximalIdeal S) : (a : S) → S ⧸ maximalIdeal S) ((aeval β : (a : R[X]) → S) q) :
      HasQuotient.Quotient S (B := Ideal S) (maximalIdeal S : Ideal S))

Tactic:
exact hp.symm

Premises used: Eq.symm
-- Module: Mathlib.RingTheory.LocalRing.Etale
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing S
inst_4 : IsLocalRing R
inst_5 : Module.Finite R S
inst_6 : FaithfulSMul R S
inst_7 : FormallyUnramified R S
β : S
hβ_gen : Eq (α := Subalgebra R S) R[β] ⊤
mpr :
  ∀ (hβ_gen : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R[X]) (β := S) (⇑(aeval β) : (a : R[X]) → S)),
    Function.Surjective.{u_1 + 1, u_2 + 1} (α := (ResidueField R)[X]) (β := ResidueField S)
      (⇑(aeval ((residue S : (a : S) → ResidueField S) β) :
            AlgHom.{u_1, u_1, u_2} (ResidueField R) (ResidueField R)[X] (ResidueField S)) :
        (a : (ResidueField R)[X]) → ResidueField S)
⊢ Eq (α := Subalgebra.{u_1, u_2} (ResidueField R) (ResidueField S))
    (ResidueField R)[((residue S : (a : S) → ResidueField S) β : ResidueField S)] ⊤

Tactic:
rw [Algebra.adjoin_singleton_eq_range_aeval, AlgHom.range_eq_top] at *

Premises used: Algebra.adjoin_singleton_eq_range_aeval, AlgHom.range_eq_top
-- Module: Mathlib.RingTheory.LocalRing.Etale
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing S
inst_4 : IsLocalRing R
inst_5 : Module.Finite R S
inst_6 : FaithfulSMul R S
inst_7 : FormallyUnramified R S
β : S
hβ_gen : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R[X]) (β := S) (⇑(aeval β) : (a : R[X]) → S)
x : ResidueField S
mpr :
  ∀ (s : S),
    ∃ (a : (ResidueField R)[X]),
      Eq.{u_2 + 1} (α := ResidueField S)
        (((aeval ((residue S : (a : S) → ResidueField S) β) :
                AlgHom.{u_1, u_1, u_2} (ResidueField R) (ResidueField R)[X] (ResidueField S)) :
              (a : (ResidueField R)[X]) → ResidueField S)
            a :
          ResidueField S)
        ((residue S : (a : S) → ResidueField S) s : ResidueField S)
⊢ ∃ (a : (ResidueField R)[X]),
    ((aeval ((residue S : (a : S) → ResidueField S) β) :
            AlgHom.{u_1, u_1, u_2} (ResidueField R) (ResidueField R)[X] (ResidueField S)) :
          (a : (ResidueField R)[X]) → ResidueField S)
        a =
      x

Tactic:
obtain ⟨s, rfl⟩ := residue_surjective (R := S) x

Premises used: rfl, IsLocalRing.residue_surjective
-- Module: Mathlib.RingTheory.LocalRing.Etale
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing S
inst_4 : IsLocalRing R
inst_5 : Module.Finite R S
inst_6 : FaithfulSMul R S
inst_7 : FormallyUnramified R S
β : S
hβ_gen : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R[X]) (β := S) (⇑(aeval β) : (a : R[X]) → S)
s : S
mpr :
  ∀ (p : R[X]),
    ∃ (a : (ResidueField R)[X]),
      Eq.{u_2 + 1} (α := ResidueField S)
        (((aeval ((residue S : (a : S) → ResidueField S) β) :
                AlgHom.{u_1, u_1, u_2} (ResidueField R) (ResidueField R)[X] (ResidueField S)) :
              (a : (ResidueField R)[X]) → ResidueField S)
            a :
          ResidueField S)
        ((residue S : (a : S) → ResidueField S) ((aeval β : (a : R[X]) → S) p) : ResidueField S)
⊢ ∃ (a : (ResidueField R)[X]),
    Eq.{u_2 + 1} (α := ResidueField S)
      (((aeval ((residue S : (a : S) → ResidueField S) β) :
              AlgHom.{u_1, u_1, u_2} (ResidueField R) (ResidueField R)[X] (ResidueField S)) :
            (a : (ResidueField R)[X]) → ResidueField S)
          a :
        ResidueField S)
      ((residue S : (a : S) → ResidueField S) s : ResidueField S)

Tactic:
obtain ⟨p, rfl⟩ := hβ_gen s

Premises used: rfl
-- Module: Mathlib.RingTheory.LocalRing.Etale
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing S
inst_4 : IsLocalRing R
inst_5 : Module.Finite R S
inst_6 : FaithfulSMul R S
inst_7 : FormallyUnramified R S
β : S
hβ_gen : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R[X]) (β := S) (⇑(aeval β) : (a : R[X]) → S)
p : R[X]
rw rw₁ :
  Eq (α := ResidueField S) ((residue S : (a : S) → ResidueField S) ((aeval β : (a : R[X]) → S) p) : ResidueField S)
    ((residue S : (a : S) → ResidueField S) ((aeval β : (a : R[X]) → S) p) : ResidueField S)
⊢ Eq.{u_2 + 1} (α := ResidueField S)
    (((aeval ((residue S : (a : S) → ResidueField S) β) :
            AlgHom.{u_1, u_1, u_2} (ResidueField R) (ResidueField R)[X] (ResidueField S)) :
          (a : (ResidueField R)[X]) → ResidueField S)
        (map (residue R) p) :
      ResidueField S)
    ((residue S : (a : S) → ResidueField S) ((aeval β : (a : R[X]) → S) p) : ResidueField S)

Tactic:
rw [← map_aeval_eq_aeval_map (ψ := residue S) (φ := residue R) rfl p β]

Premises used: Polynomial.map_aeval_eq_aeval_map, rfl
-- Module: Mathlib.RingTheory.LocalRing.Etale
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing S
inst_4 : IsLocalRing R
inst_5 : Module.Finite R S
inst_6 : FaithfulSMul R S
inst_7 : FormallyUnramified R S
β : S
hβ_gen : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R[X]) (β := S) (⇑(aeval β) : (a : R[X]) → S)
p : R[X]
⊢ ∃ (a : (ResidueField R)[X]),
    Eq.{u_2 + 1} (α := ResidueField S)
      (((aeval ((residue S : (a : S) → ResidueField S) β) :
              AlgHom.{u_1, u_1, u_2} (ResidueField R) (ResidueField R)[X] (ResidueField S)) :
            (a : (ResidueField R)[X]) → ResidueField S)
          a :
        ResidueField S)
      ((residue S : (a : S) → ResidueField S) ((aeval β : (a : R[X]) → S) p) : ResidueField S)

Tactic:
exact ⟨p.map (residue R), by
      rw [← map_aeval_eq_aeval_map (ψ := residue S) (φ := residue R) rfl p β]⟩
-- Module: Mathlib.RingTheory.LocalRing.Etale
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing S
inst_4 : IsLocalRing R
inst_5 : Module.Finite R S
inst_6 : FaithfulSMul R S
inst_7 : FormallyUnramified R S
obtain :
  ∀ (β₀ : ResidueField S)
    (hβ₀ : Eq (α := IntermediateField.{u_1, u_2} (ResidueField R) (ResidueField S)) (ResidueField R)⟮β₀⟯ ⊤),
    ∃ (β : S), Eq (α := Subalgebra R S) R[β] ⊤
⊢ ∃ (β : S), Eq (α := Subalgebra R S) R[β] ⊤

Tactic:
obtain ⟨β₀, hβ₀⟩ := Field.exists_primitive_element (ResidueField R) (ResidueField S)

Premises used: Field.exists_primitive_element, IsLocalRing.ResidueField
-- Module: Mathlib.RingTheory.LocalRing.Etale
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing S
inst_4 : IsLocalRing R
inst_5 : Module.Finite R S
inst_6 : FaithfulSMul R S
inst_7 : FormallyUnramified R S
β₀ : ResidueField S
hβ₀ : Eq (α := IntermediateField.{u_1, u_2} (ResidueField R) (ResidueField S)) (ResidueField R)⟮β₀⟯ ⊤
obtain : ∀ (β : S) (hβ : (residue S : (a : S) → ResidueField S) β = β₀), ∃ (β : S), Eq (α := Subalgebra R S) R[β] ⊤
⊢ ∃ (β : S), Eq (α := Subalgebra R S) R[β] ⊤

Tactic:
obtain ⟨β, hβ⟩ := residue_surjective (R := S) β₀

Premises used: IsLocalRing.residue_surjective
-- Module: Mathlib.RingTheory.LocalRing.Etale
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing S
inst_4 : IsLocalRing R
inst_5 : Module.Finite R S
inst_6 : FaithfulSMul R S
inst_7 : FormallyUnramified R S
β₀ : ResidueField S
hβ₀ : Eq (α := IntermediateField.{u_1, u_2} (ResidueField R) (ResidueField S)) (ResidueField R)⟮β₀⟯ ⊤
β : S
hβ : (residue S : (a : S) → ResidueField S) β = β₀
⊢ ∃ (β : S), Eq (α := Subalgebra R S) R[β] ⊤

Tactic:
⟨β, adjoin_residue_eq_top_iff_adjoin_eq_top β |>.mp ?_⟩

Premises used: Exists.intro, Iff.mp, IsLocalRing.adjoin_residue_eq_top_iff_adjoin_eq_top
-- Module: Mathlib.RingTheory.LocalRing.Etale
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing S
inst_4 : IsLocalRing R
inst_5 : Module.Finite R S
inst_6 : FaithfulSMul R S
inst_7 : FormallyUnramified R S
β₀ : ResidueField S
hβ₀ : Eq (α := IntermediateField.{u_1, u_2} (ResidueField R) (ResidueField S)) (ResidueField R)⟮β₀⟯ ⊤
β : S
hβ : (residue S : (a : S) → ResidueField S) β = β₀
refine :
  Eq (α := Subalgebra.{u_1, u_2} (ResidueField R) (ResidueField S))
    (ResidueField R)[((residue S : (a : S) → ResidueField S) β : ResidueField S)] ⊤
⊢ ∃ (β : S), Eq (α := Subalgebra R S) R[β] ⊤

Tactic:
refine ⟨β, adjoin_residue_eq_top_iff_adjoin_eq_top β |>.mp ?_⟩
-- Module: Mathlib.RingTheory.LocalRing.Etale
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing S
inst_4 : IsLocalRing R
inst_5 : Module.Finite R S
inst_6 : FaithfulSMul R S
inst_7 : FormallyUnramified R S
β₀ : ResidueField S
hβ₀ : Eq (α := IntermediateField.{u_1, u_2} (ResidueField R) (ResidueField S)) (ResidueField R)⟮β₀⟯ ⊤
β : S
hβ : (residue S : (a : S) → ResidueField S) β = β₀
rw : Eq (α := Subalgebra.{u_1, u_2} (ResidueField R) (ResidueField S)) (ResidueField R)[β₀] ⊤
rw₁ :
  Eq (α := Subalgebra.{u_1, u_2} (ResidueField R) (ResidueField S))
    (IntermediateField.toSubalgebra (ResidueField R)⟮β₀⟯) ⊤
rw₂ : Eq.{u_2 + 1} (α := Subalgebra.{u_1, u_2} (ResidueField R) (ResidueField S)) (IntermediateField.toSubalgebra ⊤) ⊤
rw₃ rw₄ : Eq.{u_2 + 1} (α := Subalgebra.{u_1, u_2} (ResidueField R) (ResidueField S)) ⊤ ⊤
⊢ Eq (α := Subalgebra.{u_1, u_2} (ResidueField R) (ResidueField S))
    (ResidueField R)[((residue S : (a : S) → ResidueField S) β : ResidueField S)] ⊤

Tactic:
rw [hβ,
    ← IntermediateField.adjoin_simple_toSubalgebra_of_isAlgebraic (IsAlgebraic.of_finite _ _),
    hβ₀, IntermediateField.top_toSubalgebra]

Premises used: IsAlgebraic.of_finite, IntermediateField.top_toSubalgebra, IntermediateField.adjoin_simple_toSubalgebra_of_isAlgebraic
-- Module: Mathlib.RingTheory.LocalRing.Etale
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing S
inst_4 : IsLocalRing R
inst_5 : Module.Finite R S
inst_6 : FaithfulSMul R S
inst_7 : Etale R S
⊢ Module.Free R S

Tactic:
have : Module.Free R S := Module.free_of_flat_of_isLocalRing
-- Module: Mathlib.RingTheory.LocalRing.Etale
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing S
inst_4 : IsLocalRing R
inst_5 : Module.Finite R S
inst_6 : FaithfulSMul R S
inst_7 : Etale R S
this : Module.Free R S
refine_2 :
  ∀
    (e :
      HasQuotient.Quotient S (B := Ideal S)
          (Ideal.map (F := R →+* S) (algebraMap R S)
            (maximalIdeal R)) ≃ₗ[HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R)]
        HasQuotient.Quotient S (B := Ideal S) (maximalIdeal S : Ideal S)),
    Module.finrank R S = Module.finrank.{u_1, u_2} (ResidueField R) (ResidueField S)
refine_1 :
  ∀ (c : HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R))
    (x : HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R))),
    ((RingEquiv.toAddEquiv (Ideal.quotEquivOfEq ⋯) :
            HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) ≃+
              HasQuotient.Quotient S (B := Ideal S) (maximalIdeal S : Ideal S)) :
          (a : S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R)) → S ⧸ maximalIdeal S)
        (c • x) =
      HSMul.hSMul (β := HasQuotient.Quotient S (B := Ideal S) (maximalIdeal S : Ideal S)) c
        (((RingEquiv.toAddEquiv (Ideal.quotEquivOfEq ⋯) :
                HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) ≃+
                  HasQuotient.Quotient S (B := Ideal S) (maximalIdeal S : Ideal S)) :
              (a : S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R)) → S ⧸ maximalIdeal S)
            x :
          HasQuotient.Quotient S (B := Ideal S) (maximalIdeal S : Ideal S))
⊢ Module.finrank R S = Module.finrank.{u_1, u_2} (ResidueField R) (ResidueField S)

Tactic:
have e := AddEquiv.toLinearEquiv (R := R ⧸ maximalIdeal R) (Ideal.quotEquivOfEq <|
      Algebra.FormallyUnramified.map_maximalIdeal (R := R) (S := S)).toAddEquiv
    ?_
-- Module: Mathlib.RingTheory.LocalRing.Etale
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing S
inst_4 : IsLocalRing R
inst_5 : Module.Finite R S
inst_6 : FaithfulSMul R S
inst_7 : Etale R S
this : Module.Free R S
e :
  HasQuotient.Quotient S (B := Ideal S)
      (Ideal.map (F := R →+* S) (algebraMap R S)
        (maximalIdeal R)) ≃ₗ[HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R)]
    HasQuotient.Quotient S (B := Ideal S) (maximalIdeal S : Ideal S)
refine_2 :
  Module.finrank.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R))
      (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R))) =
    Module.finrank.{u_1, u_2} (ResidueField R) (ResidueField S)
⊢ Module.finrank R S = Module.finrank.{u_1, u_2} (ResidueField R) (ResidueField S)

Tactic:
rw [← finrank_quotient_map (R := R) (S := S)]

Premises used: IsLocalRing.finrank_quotient_map
-- Module: Mathlib.RingTheory.LocalRing.Etale
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing S
inst_4 : IsLocalRing R
inst_5 : Module.Finite R S
inst_6 : FaithfulSMul R S
inst_7 : Etale R S
this : Module.Free R S
e :
  HasQuotient.Quotient S (B := Ideal S)
      (Ideal.map (F := R →+* S) (algebraMap R S)
        (maximalIdeal R)) ≃ₗ[HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R)]
    HasQuotient.Quotient S (B := Ideal S) (maximalIdeal S : Ideal S)
⊢ Module.finrank.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R))
      (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R))) =
    Module.finrank.{u_1, u_2} (ResidueField R) (ResidueField S)

Tactic:
e.finrank_eq

Premises used: LinearEquiv.finrank_eq, IsLocalRing.ResidueField
-- Module: Mathlib.RingTheory.LocalRing.Etale
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing S
inst_4 : IsLocalRing R
inst_5 : Module.Finite R S
inst_6 : FaithfulSMul R S
inst_7 : Etale R S
this : Module.Free R S
e :
  HasQuotient.Quotient S (B := Ideal S)
      (Ideal.map (F := R →+* S) (algebraMap R S)
        (maximalIdeal R)) ≃ₗ[HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R)]
    HasQuotient.Quotient S (B := Ideal S) (maximalIdeal S : Ideal S)
⊢ Module.finrank.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R))
      (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R))) =
    Module.finrank.{u_1, u_2} (ResidueField R) (ResidueField S)

Tactic:
exact e.finrank_eq

Premises used: LinearEquiv.finrank_eq
-- Module: Mathlib.RingTheory.LocalRing.Etale
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing S
inst_4 : IsLocalRing R
inst_5 : Module.Finite R S
inst_6 : FaithfulSMul R S
inst_7 : Etale R S
this : Module.Free R S
r : HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R)
x : HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R))
refine_1 :
  ∀ (r : R),
    ((RingEquiv.toAddEquiv (Ideal.quotEquivOfEq ⋯) :
            HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) ≃+
              HasQuotient.Quotient S (B := Ideal S) (maximalIdeal S : Ideal S)) :
          (a : S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R)) → S ⧸ maximalIdeal S)
        (HSMul.hSMul (α := HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R))
          ((Ideal.Quotient.mk (maximalIdeal R) : (a : R) → R ⧸ maximalIdeal R) r :
            HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R : Ideal R))
          x) =
      HSMul.hSMul (α := HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R)) (β :=
        HasQuotient.Quotient S (B := Ideal S) (maximalIdeal S : Ideal S))
        ((Ideal.Quotient.mk (maximalIdeal R) : (a : R) → R ⧸ maximalIdeal R) r :
          HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R : Ideal R))
        (((RingEquiv.toAddEquiv (Ideal.quotEquivOfEq ⋯) :
                HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) ≃+
                  HasQuotient.Quotient S (B := Ideal S) (maximalIdeal S : Ideal S)) :
              (a : S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R)) → S ⧸ maximalIdeal S)
            x :
          HasQuotient.Quotient S (B := Ideal S) (maximalIdeal S : Ideal S))
⊢ ((RingEquiv.toAddEquiv (Ideal.quotEquivOfEq ⋯) :
          HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) ≃+
            HasQuotient.Quotient S (B := Ideal S) (maximalIdeal S : Ideal S)) :
        (a : S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R)) → S ⧸ maximalIdeal S)
      (r • x) =
    HSMul.hSMul (β := HasQuotient.Quotient S (B := Ideal S) (maximalIdeal S : Ideal S)) r
      (((RingEquiv.toAddEquiv (Ideal.quotEquivOfEq ⋯) :
              HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) ≃+
                HasQuotient.Quotient S (B := Ideal S) (maximalIdeal S : Ideal S)) :
            (a : S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R)) → S ⧸ maximalIdeal S)
          x :
        HasQuotient.Quotient S (B := Ideal S) (maximalIdeal S : Ideal S))

Tactic:
obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective r

Premises used: Ideal.Quotient.mk_surjective, rfl