awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DualNumber
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
inr₁ : ∀ (hb : IsNilpotent b), ∃ (c : K[ε]), a * c = b ∨ b * c = a
⊢ ∃ (c : K[ε]), a * c = b ∨ b * c = a

Tactic:
rcases isUnit_or_isNilpotent b with hb | hb

Premises used: TrivSqZeroExt.isUnit_or_isNilpotent
-- Module: Mathlib.RingTheory.DualNumber
Goal:
K : Type u_2
inst : DivisionRing K
a b : K[ε]
ha : IsNilpotent a
hb : IsUnit b
⊢ IsUnit b

Tactic:
hb
-- Module: Mathlib.RingTheory.DualNumber
Goal:
K : Type u_2
inst : DivisionRing K
a b : K[ε]
ha : IsNilpotent a
hb : IsUnit b
inr : ∀ (b : K[ε]ˣ), ∃ (c : K[ε]), a * c = (↑b : K[ε]) ∨ (↑b : K[ε]) * c = a
⊢ ∃ (c : K[ε]), a * c = b ∨ b * c = a

Tactic:
lift b to K[ε]ˣ using hb
-- Module: Mathlib.RingTheory.DualNumber
Goal:
K : Type u_2
inst : DivisionRing K
a : K[ε]
ha : IsNilpotent a
b : K[ε]ˣ
⊢ a * ((↑b⁻¹ : K[ε]) * a) = (↑b : K[ε]) ∨ (↑b : K[ε]) * ((↑b⁻¹ : K[ε]) * a) = a

Tactic:
simp
-- Module: Mathlib.RingTheory.DualNumber
Goal:
K : Type u_2
inst : DivisionRing K
a : K[ε]
ha : IsNilpotent a
b : K[ε]ˣ
⊢ ∃ (c : K[ε]), a * c = (↑b : K[ε]) ∨ (↑b : K[ε]) * c = a

Tactic:
exact ⟨b⁻¹ * a, by simp⟩
-- Module: Mathlib.RingTheory.DualNumber
Goal:
K : Type u_2
inst : DivisionRing K
a b : K[ε]
ha : IsNilpotent a
hb : IsNilpotent b
⊢ ε ∣ a

Tactic:
rw [isNilpotent_iff_eps_dvd] at ha hb

Premises used: DualNumber.isNilpotent_iff_eps_dvd
-- Module: Mathlib.RingTheory.DualNumber
Goal:
K : Type u_2
inst : DivisionRing K
a b : K[ε]
ha : IsNilpotent a
hb : IsNilpotent b
ha₁ : ε ∣ a
⊢ ε ∣ b

Tactic:
rw [isNilpotent_iff_eps_dvd] at ha hb

Premises used: DualNumber.isNilpotent_iff_eps_dvd
-- Module: Mathlib.RingTheory.DualNumber
Goal:
K : Type u_2
inst : DivisionRing K
a b : K[ε]
ha : ε ∣ a
hb : ε ∣ b
inr : ∀ (x : K[ε]), ∃ (c : K[ε]), ε * x * c = b ∨ b * c = ε * x
⊢ ∃ (c : K[ε]), a * c = b ∨ b * c = a

Tactic:
obtain ⟨x, rfl⟩ := ha

Premises used: rfl
-- Module: Mathlib.RingTheory.DualNumber
Goal:
K : Type u_2
inst : DivisionRing K
b : K[ε]
hb : ε ∣ b
x : K[ε]
inr : ∀ (y : K[ε]), ∃ (c : K[ε]), ε * x * c = ε * y ∨ ε * y * c = ε * x
⊢ ∃ (c : K[ε]), ε * x * c = b ∨ b * c = ε * x

Tactic:
obtain ⟨y, rfl⟩ := hb

Premises used: rfl
-- Module: Mathlib.RingTheory.DualNumber
Goal:
K : Type u_2
inst : DivisionRing K
x y : K[ε]
this : ∃ (c : TrivSqZeroExt K K), fst x * c.fst = fst y ∨ fst y * c.fst = fst x
⊢ ∃ (c : K[ε]), ε * x * c = ε * y ∨ ε * y * c = ε * x

Tactic:
simpa [TrivSqZeroExt.ext_iff] using this

Premises used: TrivSqZeroExt.ext_iff
-- Module: Mathlib.RingTheory.DualNumber
Goal:
K : Type u_2
inst : DivisionRing K
x y : K[ε]
inr : ∃ (c : TrivSqZeroExt K K), fst x * c.fst = fst y ∨ fst y * c.fst = fst x
⊢ ∃ (c : K[ε]), ε * x * c = ε * y ∨ ε * y * c = ε * x

Tactic:
suffices ∃ c, fst x * fst c = fst y ∨ fst y * fst c = fst x by
    simpa [TrivSqZeroExt.ext_iff] using this
-- Module: Mathlib.RingTheory.DualNumber
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
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

Tactic:
rcases eq_or_ne (fst x) 0 with hx | hx

Premises used: TrivSqZeroExt.fst, eq_or_ne, OfNat.ofNat
-- Module: Mathlib.RingTheory.DualNumber
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

Tactic:
⟨ε, Or.inr ?_⟩

Premises used: Exists.intro, DualNumber.eps, Or.inr
-- Module: Mathlib.RingTheory.DualNumber
Goal:
K : Type u_2
inst : DivisionRing K
x y : K[ε]
hx : fst x = 0
inr : fst y * fst ε = fst x
⊢ ∃ (c : TrivSqZeroExt K K), fst x * c.fst = fst y ∨ fst y * c.fst = fst x

Tactic:
refine ⟨ε, Or.inr ?_⟩
-- Module: Mathlib.RingTheory.DualNumber
Goal:
K : Type u_2
inst : DivisionRing K
x y : K[ε]
hx : fst x = 0
⊢ fst y * fst ε = fst x

Tactic:
simp [hx]
-- Module: Mathlib.RingTheory.DualNumber
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

Tactic:
⟨inl ((fst x)⁻¹ * fst y), ?_⟩

Premises used: HMul.hMul, TrivSqZeroExt.inl, TrivSqZeroExt.fst, Inv.inv, Exists.intro
-- Module: Mathlib.RingTheory.DualNumber
Goal:
K : Type u_2
inst : DivisionRing K
x y : K[ε]
hx : fst x ≠ 0
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
⊢ ∃ (c : TrivSqZeroExt K K), fst x * c.fst = fst y ∨ fst y * c.fst = fst x

Tactic:
refine ⟨inl ((fst x)⁻¹ * fst y), ?_⟩
-- Module: Mathlib.RingTheory.DualNumber
Goal:
K : Type u_2
inst : DivisionRing K
x y : K[ε]
hx : fst x ≠ 0
⊢ 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:
simp [← mul_assoc, mul_inv_cancel₀ hx]

Premises used: mul_inv_cancel₀, mul_assoc
-- Module: Mathlib.RingTheory.EssentialFiniteness
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : EssFiniteType R S
⊢ Eq.{u_2 + 1} (α := Subalgebra R ↥(subalgebra R S)) (adjoin R {x : ↥(subalgebra R S) | (↑x : S) ∈ finset R S}) ⊤

Tactic:
adjoin_adjoin_coe_preimage

Premises used: Set.Mem, setOf, Algebra.adjoin_adjoin_coe_preimage, Set.preimage
-- Module: Mathlib.RingTheory.EssentialFiniteness
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
out : Subalgebra.FG.{u_1, u_2} (R := R) (A := ↥(EssFiniteType.subalgebra R S)) ⊤
⊢ FiniteType.{u_1, u_2} R ↥(EssFiniteType.subalgebra R S)

Tactic:
constructor
-- Module: Mathlib.RingTheory.EssentialFiniteness
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
out : Subalgebra.FG (adjoin R (↑(EssFiniteType.finset R S) : Set S))
⊢ Subalgebra.FG.{u_1, u_2} (R := R) (A := ↥(EssFiniteType.subalgebra R S)) ⊤

Tactic:
rw [Subalgebra.fg_top, EssFiniteType.subalgebra]

Premises used: Algebra.EssFiniteType.subalgebra, Subalgebra.fg_top
-- Module: Mathlib.RingTheory.EssentialFiniteness
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 (adjoin R (↑(EssFiniteType.finset R S) : Set S))

Tactic:
⟨_, rfl⟩

Premises used: Subalgebra.FG, Exists.intro, rfl
-- Module: Mathlib.RingTheory.EssentialFiniteness
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 (adjoin R (↑(EssFiniteType.finset R S) : Set S))

Tactic:
exact ⟨_, rfl⟩
-- Module: Mathlib.RingTheory.EssentialFiniteness
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
h : EssFiniteType R S
⊢ IsLocalization (R := ↥(subalgebra R S)) (submonoid R S) S

Tactic:
h.cond.choose_spec

Premises used: Exists.choose_spec, Algebra.EssFiniteType.submonoid, Set.Mem, setOf, Algebra.EssFiniteType.cond
-- Module: Mathlib.RingTheory.EssentialFiniteness
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)
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
⊢ 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
-- Module: Mathlib.RingTheory.EssentialFiniteness
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
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)
⊢ ∃ (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

Premises used: IsLocalization'.toIsLocalizationMap, Submonoid.IsLocalizationMap.surj
-- Module: Mathlib.RingTheory.EssentialFiniteness
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 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:
⟨t, ht, ht', h ▸ hx⟩

Premises used: Eq.rec, And.intro, Exists.intro, Eq.symm
-- Module: Mathlib.RingTheory.EssentialFiniteness
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 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:
exact ⟨t, ht, ht', h ▸ hx⟩
-- Module: Mathlib.RingTheory.EssentialFiniteness
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 :
  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)
⊢ IsLocalization
    (Submonoid.comap (F := ↥(adjoin R (↑σ : Set S)) →+* S) (algebraMap (↥(adjoin R (↑σ : Set S))) S)
      (IsUnit.submonoid S))
    S

Tactic:
constructor
-- Module: Mathlib.RingTheory.EssentialFiniteness
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
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
⊢ 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
-- Module: Mathlib.RingTheory.EssentialFiniteness
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)
⊢ ∀
    (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:
fun y ↦ y.prop

Premises used: Set.Mem, setOf, IsUnit, Set.preimage, Subtype.prop
-- Module: Mathlib.RingTheory.EssentialFiniteness
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)
⊢ ∀
    (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:
exact fun y ↦ y.prop
-- Module: Mathlib.RingTheory.EssentialFiniteness
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
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
⊢ ∃ (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
-- Module: Mathlib.RingTheory.EssentialFiniteness
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 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:
⟨⟨⟨_, h⟩, ⟨t, ht⟩, ht'⟩, rfl⟩

Premises used: Prod.mk, Subtype.mk, Exists.intro, rfl
-- Module: Mathlib.RingTheory.EssentialFiniteness
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 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:
exact ⟨⟨⟨_, h⟩, ⟨t, ht⟩, ht'⟩, rfl⟩