awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
K : Type u_2
inst : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
hd' : ∀ x ∈ I, x ≠ 0 → ∃ (r : K[ε]), ε = r * x
p : K[ε]
⊢ ε * p ∈ I
have refine_2 : ∀ (y : K[ε]) (hyI : y ∈ I) (hy0 : y ≠ 0), ε * p ∈ I
Tactic: obtain ⟨y, hyI, hy0⟩ := Submodule.exists_mem_ne_zero_of_ne_bot hb
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
K : Type u_2
inst : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
hd' : ∀ x ∈ I, x ≠ 0 → ∃ (r : K[ε]), ε = r * x
p y : K[ε]
hyI : y ∈ I
hy0 : y ≠ 0
⊢ ε * p ∈ I
have refine_2 : ∀ (r : K[ε]) (hr : ε = r * y), ε * p ∈ I
Tactic: obtain ⟨r, hr⟩ := hd' _ hyI hy0
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
K : Type u_2
inst : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
hd' : ∀ x ∈ I, x ≠ 0 → ∃ (r : K[ε]), ε = r * x
p y : K[ε]
hyI : y ∈ I
hy0 : y ≠ 0
r : K[ε]
hr : ε = r * y
⊢ ε * p ∈ I
have refine_2 : p * r * y ∈ I
Tactic: rw [(commute_eps_left _).eq, hr, ← mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
K : Type u_2
inst : DivisionRing K
⊢ Ideal.IsMaximal (α := K[ε]) (Ideal.span {ε})
have refine_1 : Ne (α := Ideal K[ε]) (Ideal.span {ε}) ⊤
Tactic: refine ⟨?_, fun I hI ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
K : Type u_2
inst : DivisionRing K
refine_1 : Ne (α := Ideal K[ε]) (Ideal.span {ε}) ⊤
⊢ Ideal.IsMaximal (α := K[ε]) (Ideal.span {ε})
have refine_2 : ∀ (I : Ideal K[ε]) (hI : Ideal.span {ε} < I), I = ⊤
Tactic: refine ⟨?_, fun I hI ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
K : Type u_2
inst : DivisionRing K
I : Ideal K[ε]
hI : Ideal.span {ε} < I
⊢ I = ⊤
have refine_2 : ∀ (hI : LT.lt (α := Ideal K[ε]) (Ideal.span {ε}) ⊥), Eq.{u_2 + 1} (α := Ideal K[ε]) ⊥ ⊤
Tactic: rcases ideal_trichotomy I with rfl | rfl | rfl
Cleared hypotheses: I, hI
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
K : Type u_2
inst : DivisionRing K
I : Ideal K[ε]
hI : Ideal.span {ε} < I
refine_2 : ∀ (hI : LT.lt (α := Ideal K[ε]) (Ideal.span {ε}) ⊥), Eq.{u_2 + 1} (α := Ideal K[ε]) ⊥ ⊤
⊢ I = ⊤
have refine_2₁ : ∀ (hI : LT.lt (α := Ideal K[ε]) (Ideal.span {ε}) (Ideal.span {ε})), Eq (α := Ideal K[ε]) (Ideal.span {ε}) ⊤
Tactic: rcases ideal_trichotomy I with rfl | rfl | rfl
Cleared hypotheses: I, hI
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
K : Type u_2
inst : DivisionRing K
I : Ideal K[ε]
hI : Ideal.span {ε} < I
refine_2 : ∀ (hI : LT.lt (α := Ideal K[ε]) (Ideal.span {ε}) ⊥), Eq.{u_2 + 1} (α := Ideal K[ε]) ⊥ ⊤
refine_2₁ : ∀ (hI : LT.lt (α := Ideal K[ε]) (Ideal.span {ε}) (Ideal.span {ε})), Eq (α := Ideal K[ε]) (Ideal.span {ε}) ⊤
⊢ I = ⊤
have refine_2₂ : ∀ (hI : LT.lt (α := Ideal K[ε]) (Ideal.span {ε}) ⊤), Eq.{u_2 + 1} (α := Ideal K[ε]) ⊤ ⊤
Tactic: rcases ideal_trichotomy I with rfl | rfl | rfl
Cleared hypotheses: I, hI
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
R : Type u_1
K : Type u_2
inst : DivisionRing K
I : Ideal K[ε]
⊢ Submodule.IsPrincipal I
have inl : Submodule.IsPrincipal.{u_2, u_2} (R := K[ε]) (M := K[ε]) ⊥
Tactic: rcases ideal_trichotomy I with rfl | rfl | rfl
Cleared hypotheses: I
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
R : Type u_1
K : Type u_2
inst : DivisionRing K
I : Ideal K[ε]
inl : Submodule.IsPrincipal.{u_2, u_2} (R := K[ε]) (M := K[ε]) ⊥
⊢ Submodule.IsPrincipal I
have inr : Submodule.IsPrincipal (R := K[ε]) (Ideal.span {ε})
Tactic: rcases ideal_trichotomy I with rfl | rfl | rfl
Cleared hypotheses: I
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
R : Type u_1
K : Type u_2
inst : DivisionRing K
I : Ideal K[ε]
inl : Submodule.IsPrincipal.{u_2, u_2} (R := K[ε]) (M := K[ε]) ⊥
inr : Submodule.IsPrincipal (R := K[ε]) (Ideal.span {ε})
⊢ Submodule.IsPrincipal I
have inr₁ : Submodule.IsPrincipal.{u_2, u_2} (R := K[ε]) (M := K[ε]) ⊤
Tactic: rcases ideal_trichotomy I with rfl | rfl | rfl
Cleared hypotheses: I
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
K : Type u_2
inst : DivisionRing K
a b : K[ε]
⊢ ∃ (c : K[ε]), a * c = b ∨ b * c = a
have inl : ∀ (ha : IsUnit a), ∃ (c : K[ε]), a * c = b ∨ b * c = a
Tactic: rcases isUnit_or_isNilpotent a with ha | ha
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
K : Type u_2
inst : DivisionRing K
a b : K[ε]
inl : ∀ (ha : IsUnit a), ∃ (c : K[ε]), a * c = b ∨ b * c = a
⊢ ∃ (c : K[ε]), a * c = b ∨ b * c = a
have inr : ∀ (ha : IsNilpotent a), ∃ (c : K[ε]), a * c = b ∨ b * c = a
Tactic: rcases isUnit_or_isNilpotent a with ha | ha
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
K : Type u_2
inst : DivisionRing K
a b : K[ε]
ha : IsUnit a
⊢ ∃ (c : K[ε]), a * c = b ∨ b * c = a
have inl : ∀ (a : K[ε]ˣ), ∃ (c : K[ε]), (↑a : K[ε]) * c = b ∨ b * c = (↑a : K[ε])
Tactic: lift a to K[ε]ˣ using ha
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
K : Type u_2
inst : DivisionRing K
a b : K[ε]
ha : IsNilpotent a
⊢ ∃ (c : K[ε]), a * c = b ∨ b * c = a
have inr : ∀ (hb : IsUnit b), ∃ (c : K[ε]), a * c = b ∨ b * c = a
Tactic: rcases isUnit_or_isNilpotent b with hb | hb
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
K : Type u_2
inst : DivisionRing K
a b : K[ε]
ha : IsNilpotent a
inr : ∀ (hb : IsUnit b), ∃ (c : K[ε]), a * c = b ∨ b * c = a
⊢ ∃ (c : K[ε]), a * c = b ∨ b * c = a
have inr₁ : ∀ (hb : IsNilpotent b), ∃ (c : K[ε]), a * c = b ∨ b * c = a
Tactic: rcases isUnit_or_isNilpotent b with hb | hb
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
K : Type u_2
inst : DivisionRing K
a b : K[ε]
ha : IsNilpotent a
hb : IsUnit b
⊢ ∃ (c : K[ε]), a * c = b ∨ b * c = a
have inr : ∀ (b : K[ε]ˣ), ∃ (c : K[ε]), a * c = (↑b : K[ε]) ∨ (↑b : K[ε]) * c = a
Tactic: lift b to K[ε]ˣ using hb
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (hypothesis)
Goal:
K : Type u_2
inst : DivisionRing K
a b : K[ε]
ha : IsNilpotent a
hb : IsNilpotent b
⊢ ∃ (c : K[ε]), a * c = b ∨ b * c = a
have ha₁ : ε ∣ a
Tactic: rw [isNilpotent_iff_eps_dvd] at ha hb
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (hypothesis)
Goal:
K : Type u_2
inst : DivisionRing K
a b : K[ε]
ha : IsNilpotent a
hb : IsNilpotent b
ha₁ : ε ∣ a
⊢ ∃ (c : K[ε]), a * c = b ∨ b * c = a
have hb₁ : ε ∣ b
Tactic: rw [isNilpotent_iff_eps_dvd] at ha hb
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
K : Type u_2
inst : DivisionRing K
a b : K[ε]
ha : ε ∣ a
hb : ε ∣ b
⊢ ∃ (c : K[ε]), a * c = b ∨ b * c = a
have inr : ∀ (x : K[ε]), ∃ (c : K[ε]), ε * x * c = b ∨ b * c = ε * x
Tactic: obtain ⟨x, rfl⟩ := ha
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
K : Type u_2
inst : DivisionRing K
b : K[ε]
hb : ε ∣ b
x : K[ε]
⊢ ∃ (c : K[ε]), ε * x * c = b ∨ b * c = ε * x
have inr : ∀ (y : K[ε]), ∃ (c : K[ε]), ε * x * c = ε * y ∨ ε * y * c = ε * x
Tactic: obtain ⟨y, rfl⟩ := hb
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
K : Type u_2
inst : DivisionRing K
x y : K[ε]
⊢ ∃ (c : K[ε]), ε * x * c = ε * y ∨ ε * y * c = ε * x
have inr : ∃ (c : TrivSqZeroExt K K), fst x * c.fst = fst y ∨ fst y * c.fst = fst x
Tactic: suffices ∃ c, fst x * fst c = fst y ∨ fst y * fst c = fst x by
    simpa [TrivSqZeroExt.ext_iff] using this
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
K : Type u_2
inst : DivisionRing K
x y : K[ε]
⊢ ∃ (c : TrivSqZeroExt K K), fst x * c.fst = fst y ∨ fst y * c.fst = fst x
have inr : ∀ (hx : fst x = 0), ∃ (c : TrivSqZeroExt K K), fst x * c.fst = fst y ∨ fst y * c.fst = fst x
Tactic: rcases eq_or_ne (fst x) 0 with hx | hx
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
K : Type u_2
inst : DivisionRing K
x y : K[ε]
inr : ∀ (hx : fst x = 0), ∃ (c : TrivSqZeroExt K K), fst x * c.fst = fst y ∨ fst y * c.fst = fst x
⊢ ∃ (c : TrivSqZeroExt K K), fst x * c.fst = fst y ∨ fst y * c.fst = fst x
have inr₁ : ∀ (hx : fst x ≠ 0), ∃ (c : TrivSqZeroExt K K), fst x * c.fst = fst y ∨ fst y * c.fst = fst x
Tactic: rcases eq_or_ne (fst x) 0 with hx | hx
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
K : Type u_2
inst : DivisionRing K
x y : K[ε]
hx : fst x = 0
⊢ ∃ (c : TrivSqZeroExt K K), fst x * c.fst = fst y ∨ fst y * c.fst = fst x
have inr : fst y * fst ε = fst x
Tactic: refine ⟨ε, Or.inr ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
K : Type u_2
inst : DivisionRing K
x y : K[ε]
hx : fst x ≠ 0
⊢ ∃ (c : TrivSqZeroExt K K), fst x * c.fst = fst y ∨ fst y * c.fst = fst x
have inr : fst x * fst (M := K) (inl ((fst x)⁻¹ * fst y)) = fst y ∨ fst y * fst (M := K) (inl ((fst x)⁻¹ * fst y)) = fst x
Tactic: refine ⟨inl ((fst x)⁻¹ * fst y), ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.EssentialFiniteness (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : EssFiniteType R S
⊢ FiniteType.{u_1, u_2} R ↥(EssFiniteType.subalgebra R S)
have out : Subalgebra.FG.{u_1, u_2} (R := R) (A := ↥(EssFiniteType.subalgebra R S)) ⊤
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.EssentialFiniteness (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : EssFiniteType R S
⊢ Subalgebra.FG.{u_1, u_2} (R := R) (A := ↥(EssFiniteType.subalgebra R S)) ⊤
have out : Subalgebra.FG (adjoin R (↑(EssFiniteType.finset R S) : Set S))
Tactic: rw [Subalgebra.fg_top, EssFiniteType.subalgebra]
-- Lean 4 proof step from Mathlib.RingTheory.EssentialFiniteness (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Finset S
⊢ IsLocalization
      (Submonoid.comap (F := ↥(adjoin R (↑σ : Set S)) →+* S) (algebraMap (↥(adjoin R (↑σ : Set S))) S)
        (IsUnit.submonoid S))
      S ↔
    ∀ (s : S),
      ∃ (t : S),
        Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) t ∧
          IsUnit t ∧ Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) (s * t)
have mp : IsLocalization
    (Submonoid.comap (F := ↥(adjoin R (↑σ : Set S)) →+* S) (algebraMap (↥(adjoin R (↑σ : Set S))) S)
      (IsUnit.submonoid S))
    S →
  ∀ (s : S),
    ∃ (t : S),
      Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) t ∧
        IsUnit t ∧ Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) (s * t)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.EssentialFiniteness (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Finset S
mp :
  IsLocalization
      (Submonoid.comap (F := ↥(adjoin R (↑σ : Set S)) →+* S) (algebraMap (↥(adjoin R (↑σ : Set S))) S)
        (IsUnit.submonoid S))
      S →
    ∀ (s : S),
      ∃ (t : S),
        Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) t ∧
          IsUnit t ∧ Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) (s * t)
⊢ IsLocalization
      (Submonoid.comap (F := ↥(adjoin R (↑σ : Set S)) →+* S) (algebraMap (↥(adjoin R (↑σ : Set S))) S)
        (IsUnit.submonoid S))
      S ↔
    ∀ (s : S),
      ∃ (t : S),
        Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) t ∧
          IsUnit t ∧ Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) (s * t)
have mpr : (∀ (s : S),
    ∃ (t : S),
      Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) t ∧
        IsUnit t ∧ Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) (s * t)) →
  IsLocalization
    (Submonoid.comap (F := ↥(adjoin R (↑σ : Set S)) →+* S) (algebraMap (↥(adjoin R (↑σ : Set S))) S)
      (IsUnit.submonoid S))
    S
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.EssentialFiniteness (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Finset S
hσ :
  IsLocalization
    (Submonoid.comap (F := ↥(adjoin R (↑σ : Set S)) →+* S) (algebraMap (↥(adjoin R (↑σ : Set S))) S)
      (IsUnit.submonoid S))
    S
s : S
⊢ ∃ (t : S),
    Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) t ∧
      IsUnit t ∧ Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) (s * t)
have mp : ∀ (x : S) (hx : Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) x) (t : S)
  (ht : Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) t)
  (ht' :
    Membership.mem (γ := Submonoid ↥(adjoin R (↑σ : Set S)))
      (Submonoid.comap (F := ↥(adjoin R (↑σ : Set S)) →+* S) (algebraMap (↥(adjoin R (↑σ : Set S))) S)
        (IsUnit.submonoid S))
      (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) x) t ht))
  (h :
    HMul.hMul (β := S) s
        ((algebraMap (↥(adjoin R (↑σ : Set S))) S : (a : ↥(adjoin R (↑σ : Set S))) → S)
            (↑(Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) x) x hx,
                    Subtype.mk (p := fun (x : ↥(adjoin R (↑σ : Set S))) ↦
                      Membership.mem (γ := Submonoid ↥(adjoin R (↑σ : Set S)))
                        (Submonoid.comap (F := ↥(adjoin R (↑σ : Set S)) →+* S) (algebraMap (↥(adjoin R (↑σ : Set S))) S)
                          (IsUnit.submonoid S))
                        x)
                      (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) x) t
                        ht)
                      ht').2 :
              ↥(adjoin R (↑σ : Set S))) :
          S) =
      (algebraMap (↥(adjoin R (↑σ : Set S))) S : (a : ↥(adjoin R (↑σ : Set S))) → S)
        (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) x) x hx,
            Subtype.mk (p := fun (x : ↥(adjoin R (↑σ : Set S))) ↦
              Membership.mem (γ := Submonoid ↥(adjoin R (↑σ : Set S)))
                (Submonoid.comap (F := ↥(adjoin R (↑σ : Set S)) →+* S) (algebraMap (↥(adjoin R (↑σ : Set S))) S)
                  (IsUnit.submonoid S))
                x)
              (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) x) t ht)
              ht').1),
  ∃ (t : S),
    Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) t ∧
      IsUnit t ∧ Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) (s * t)
Tactic: obtain ⟨⟨⟨x, hx⟩, ⟨t, ht⟩, ht'⟩, h⟩ := hσ.1.2 s
-- Lean 4 proof step from Mathlib.RingTheory.EssentialFiniteness (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Finset S
hσ :
  ∀ (s : S),
    ∃ (t : S),
      Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) t ∧
        IsUnit t ∧ Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) (s * t)
⊢ IsLocalization
    (Submonoid.comap (F := ↥(adjoin R (↑σ : Set S)) →+* S) (algebraMap (↥(adjoin R (↑σ : Set S))) S)
      (IsUnit.submonoid S))
    S
have mpr : Submonoid.IsLocalizationMap (N := S)
  (Submonoid.comap (F := ↥(adjoin R (↑σ : Set S)) →+* S) (algebraMap (↥(adjoin R (↑σ : Set S))) S) (IsUnit.submonoid S))
  (⇑(algebraMap (↥(adjoin R (↑σ : Set S))) S) : (a : ↥(adjoin R (↑σ : Set S))) → S)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.EssentialFiniteness (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Finset S
hσ :
  ∀ (s : S),
    ∃ (t : S),
      Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) t ∧
        IsUnit t ∧ Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) (s * t)
⊢ Submonoid.IsLocalizationMap (N := S)
    (Submonoid.comap (F := ↥(adjoin R (↑σ : Set S)) →+* S) (algebraMap (↥(adjoin R (↑σ : Set S))) S)
      (IsUnit.submonoid S))
    (⇑(algebraMap (↥(adjoin R (↑σ : Set S))) S) : (a : ↥(adjoin R (↑σ : Set S))) → S)
have mpr : ∀
  (y :
    ↥(Submonoid.comap (F := ↥(adjoin R (↑σ : Set S)) →+* S) (algebraMap (↥(adjoin R (↑σ : Set S))) S)
        (IsUnit.submonoid S))),
  IsUnit (M := S)
    ((algebraMap (↥(adjoin R (↑σ : Set S))) S : (a : ↥(adjoin R (↑σ : Set S))) → S) (↑y : ↥(adjoin R (↑σ : Set S))) : S)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.EssentialFiniteness (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Finset S
hσ :
  ∀ (s : S),
    ∃ (t : S),
      Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) t ∧
        IsUnit t ∧ Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) (s * t)
mpr :
  ∀
    (y :
      ↥(Submonoid.comap (F := ↥(adjoin R (↑σ : Set S)) →+* S) (algebraMap (↥(adjoin R (↑σ : Set S))) S)
          (IsUnit.submonoid S))),
    IsUnit (M := S)
      ((algebraMap (↥(adjoin R (↑σ : Set S))) S : (a : ↥(adjoin R (↑σ : Set S))) → S) (↑y : ↥(adjoin R (↑σ : Set S))) :
        S)
⊢ Submonoid.IsLocalizationMap (N := S)
    (Submonoid.comap (F := ↥(adjoin R (↑σ : Set S)) →+* S) (algebraMap (↥(adjoin R (↑σ : Set S))) S)
      (IsUnit.submonoid S))
    (⇑(algebraMap (↥(adjoin R (↑σ : Set S))) S) : (a : ↥(adjoin R (↑σ : Set S))) → S)
have mpr₁ : ∀ (z : S),
  ∃ (x :
    ↥(adjoin R (↑σ : Set S)) ×
      ↥(Submonoid.comap (F := ↥(adjoin R (↑σ : Set S)) →+* S) (algebraMap (↥(adjoin R (↑σ : Set S))) S)
          (IsUnit.submonoid S))),
    HMul.hMul (β := S) z
        ((algebraMap (↥(adjoin R (↑σ : Set S))) S : (a : ↥(adjoin R (↑σ : Set S))) → S)
            (↑x.2 : ↥(adjoin R (↑σ : Set S))) :
          S) =
      (algebraMap (↥(adjoin R (↑σ : Set S))) S : (a : ↥(adjoin R (↑σ : Set S))) → S) x.1
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.EssentialFiniteness (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Finset S
hσ :
  ∀ (s : S),
    ∃ (t : S),
      Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) t ∧
        IsUnit t ∧ Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) (s * t)
mpr :
  ∀
    (y :
      ↥(Submonoid.comap (F := ↥(adjoin R (↑σ : Set S)) →+* S) (algebraMap (↥(adjoin R (↑σ : Set S))) S)
          (IsUnit.submonoid S))),
    IsUnit (M := S)
      ((algebraMap (↥(adjoin R (↑σ : Set S))) S : (a : ↥(adjoin R (↑σ : Set S))) → S) (↑y : ↥(adjoin R (↑σ : Set S))) :
        S)
mpr₁ :
  ∀ (z : S),
    ∃ (x :
      ↥(adjoin R (↑σ : Set S)) ×
        ↥(Submonoid.comap (F := ↥(adjoin R (↑σ : Set S)) →+* S) (algebraMap (↥(adjoin R (↑σ : Set S))) S)
            (IsUnit.submonoid S))),
      HMul.hMul (β := S) z
          ((algebraMap (↥(adjoin R (↑σ : Set S))) S : (a : ↥(adjoin R (↑σ : Set S))) → S)
              (↑x.2 : ↥(adjoin R (↑σ : Set S))) :
            S) =
        (algebraMap (↥(adjoin R (↑σ : Set S))) S : (a : ↥(adjoin R (↑σ : Set S))) → S) x.1
⊢ Submonoid.IsLocalizationMap (N := S)
    (Submonoid.comap (F := ↥(adjoin R (↑σ : Set S)) →+* S) (algebraMap (↥(adjoin R (↑σ : Set S))) S)
      (IsUnit.submonoid S))
    (⇑(algebraMap (↥(adjoin R (↑σ : Set S))) S) : (a : ↥(adjoin R (↑σ : Set S))) → S)
have mpr₂ : ∀ {x y : ↥(adjoin R (↑σ : Set S))},
  Eq (α := S) ((algebraMap (↥(adjoin R (↑σ : Set S))) S : (a : ↥(adjoin R (↑σ : Set S))) → S) x : S)
      ((algebraMap (↥(adjoin R (↑σ : Set S))) S : (a : ↥(adjoin R (↑σ : Set S))) → S) y : S) →
    ∃ (c :
      ↥(Submonoid.comap (F := ↥(adjoin R (↑σ : Set S)) →+* S) (algebraMap (↥(adjoin R (↑σ : Set S))) S)
          (IsUnit.submonoid S))),
      (↑c : ↥(adjoin R (↑σ : Set S))) * x = (↑c : ↥(adjoin R (↑σ : Set S))) * y
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.EssentialFiniteness (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Finset S
hσ :
  ∀ (s : S),
    ∃ (t : S),
      Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) t ∧
        IsUnit t ∧ Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) (s * t)
s : S
⊢ ∃ (x :
    ↥(adjoin R (↑σ : Set S)) ×
      ↥(Submonoid.comap (F := ↥(adjoin R (↑σ : Set S)) →+* S) (algebraMap (↥(adjoin R (↑σ : Set S))) S)
          (IsUnit.submonoid S))),
    HMul.hMul (β := S) s
        ((algebraMap (↥(adjoin R (↑σ : Set S))) S : (a : ↥(adjoin R (↑σ : Set S))) → S)
            (↑x.2 : ↥(adjoin R (↑σ : Set S))) :
          S) =
      (algebraMap (↥(adjoin R (↑σ : Set S))) S : (a : ↥(adjoin R (↑σ : Set S))) → S) x.1
have mpr : ∀ (t : S) (ht : Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) t) (ht' : IsUnit t)
  (h : Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) (s * t)),
  ∃ (x :
    ↥(adjoin R (↑σ : Set S)) ×
      ↥(Submonoid.comap (F := ↥(adjoin R (↑σ : Set S)) →+* S) (algebraMap (↥(adjoin R (↑σ : Set S))) S)
          (IsUnit.submonoid S))),
    HMul.hMul (β := S) s
        ((algebraMap (↥(adjoin R (↑σ : Set S))) S : (a : ↥(adjoin R (↑σ : Set S))) → S)
            (↑x.2 : ↥(adjoin R (↑σ : Set S))) :
          S) =
      (algebraMap (↥(adjoin R (↑σ : Set S))) S : (a : ↥(adjoin R (↑σ : Set S))) → S) x.1
Tactic: obtain ⟨t, ht, ht', h⟩ := hσ s
-- Lean 4 proof step from Mathlib.RingTheory.EssentialFiniteness (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
⊢ EssFiniteType R S ↔
    ∃ (σ : Finset S),
      ∀ (s : S),
        ∃ (t : S),
          Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) t ∧
            IsUnit t ∧ Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) (s * t)
have simp_rw : EssFiniteType R S ↔
  ∃ (σ : Finset S),
    IsLocalization
      (Submonoid.comap (F := ↥(adjoin R (↑σ : Set S)) →+* S) (algebraMap (↥(adjoin R (↑σ : Set S))) S)
        (IsUnit.submonoid S))
      S
Tactic: simp_rw [← essFiniteType_cond_iff]
-- Lean 4 proof step from Mathlib.RingTheory.EssentialFiniteness (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
⊢ EssFiniteType R S ↔
    ∃ (σ : Finset S),
      IsLocalization
        (Submonoid.comap (F := ↥(adjoin R (↑σ : Set S)) →+* S) (algebraMap (↥(adjoin R (↑σ : Set S))) S)
          (IsUnit.submonoid S))
        S
have mp : EssFiniteType R S →
  ∃ (σ : Finset S),
    IsLocalization
      (Submonoid.comap (F := ↥(adjoin R (↑σ : Set S)) →+* S) (algebraMap (↥(adjoin R (↑σ : Set S))) S)
        (IsUnit.submonoid S))
      S
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.EssentialFiniteness (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
mp :
  EssFiniteType R S →
    ∃ (σ : Finset S),
      IsLocalization
        (Submonoid.comap (F := ↥(adjoin R (↑σ : Set S)) →+* S) (algebraMap (↥(adjoin R (↑σ : Set S))) S)
          (IsUnit.submonoid S))
        S
⊢ EssFiniteType R S ↔
    ∃ (σ : Finset S),
      IsLocalization
        (Submonoid.comap (F := ↥(adjoin R (↑σ : Set S)) →+* S) (algebraMap (↥(adjoin R (↑σ : Set S))) S)
          (IsUnit.submonoid S))
        S
have mpr : (∃ (σ : Finset S),
    IsLocalization
      (Submonoid.comap (F := ↥(adjoin R (↑σ : Set S)) →+* S) (algebraMap (↥(adjoin R (↑σ : Set S))) S)
        (IsUnit.submonoid S))
      S) →
  EssFiniteType R S
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.EssentialFiniteness (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : FiniteType R S
⊢ EssFiniteType R S
have obtain : ∀ (s : Finset S) (hs : Eq (α := Subalgebra R S) (adjoin R (↑s : Set S)) ⊤), EssFiniteType R S
Tactic: obtain ⟨s, hs⟩ := ‹FiniteType R S›
-- Lean 4 proof step from Mathlib.RingTheory.EssentialFiniteness (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : FiniteType R S
s : Finset S
hs : Eq (α := Subalgebra R S) (adjoin R (↑s : Set S)) ⊤
⊢ EssFiniteType R S
have rw : ∃ (σ : Finset S),
  ∀ (s : S),
    ∃ (t : S),
      Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) t ∧
        IsUnit t ∧ Membership.mem (γ := Subalgebra R S) (adjoin R (↑σ : Set S)) (s * t)
Tactic: rw [essFiniteType_iff]