awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin
Goal:
R : Type u
inst : Ring R
inst_1 : IsSemisimpleRing R
⊢ ∃ (n : ℕ) (D : Fin n → Ideal R) (d : Fin n → ℕ),
    (∀ (i : Fin n), IsSimpleModule R ↥(D i)) ∧
      (∀ (i : Fin n), NeZero (d i)) ∧
        Nonempty.{u + 1} (R ≃+* ((i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (Module.End R ↥(D i))ᵐᵒᵖ))

Tactic:
have ⟨n, S, d, hS, hd, ⟨e⟩⟩ := exists_algEquiv_pi_matrix_end_mulOpposite ℕ R
  ⟨n, S, d, hS, hd, ⟨e⟩⟩

Premises used: Exists, IsSemisimpleRing.exists_algEquiv_pi_matrix_end_mulOpposite, Nonempty.intro, And, Nat, And.intro, AlgEquiv.toRingEquiv, Exists.intro, Nonempty, _private.0.IsSemisimpleRing.exists_ringEquiv_pi_matrix_end_mulOpposite.match_1, RingEquiv
-- Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin
Goal:
R : Type u
inst : Ring R
inst_1 : IsSemisimpleRing R
⊢ ∃ (n : ℕ) (D : Fin n → Type u) (d : Fin n → ℕ) (x : (i : Fin n) → DivisionRing (D i)),
    (∀ (i : Fin n), NeZero (d i)) ∧ Nonempty.{u + 1} (R ≃+* ((i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (D i)))

Tactic:
have ⟨n, D, d, _, _, hd, ⟨e⟩⟩ := exists_algEquiv_pi_matrix_divisionRing ℕ R
  ⟨n, D, d, _, hd, ⟨e⟩⟩

Premises used: Exists, _private.0.IsSemisimpleRing.exists_ringEquiv_pi_matrix_divisionRing.match_1, IsSemisimpleRing.exists_algEquiv_pi_matrix_divisionRing, Nonempty.intro, And, Nat, And.intro, AlgEquiv.toRingEquiv, Exists.intro, Nonempty, RingEquiv
-- Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin
Goal:
R₀ : Type u_1
R : Type u
inst : CommSemiring R₀
inst_1 : Ring R
inst_2 : Algebra R₀ R
inst_3 : IsSemisimpleRing R
n : Type u_2
inst_4 : Fintype n
inst_5 : DecidableEq n
⊢ IsSemisimpleRing (Matrix n n R)

Tactic:
(isEmpty_or_nonempty n).elim (fun _ ↦ inferInstance) fun _ ↦
    have ⟨_, _, _, _, _, ⟨e⟩⟩ := exists_ringEquiv_pi_matrix_divisionRing R
    (e.mapMatrix (m := n).trans Matrix.piRingEquiv).symm.isSemisimpleRing

Premises used: Matrix, inferInstance, isEmpty_or_nonempty, IsSemisimpleRing.exists_ringEquiv_pi_matrix_divisionRing, IsSemisimpleRing, RingEquiv.mapMatrix, RingEquiv.trans, Matrix.piRingEquiv, RingEquiv.isSemisimpleRing, Or.elim, _private.0.IsSemisimpleRing.instMatrix.match_1, RingEquiv.symm
-- Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin
Goal:
R₀ : Type u_1
R : Type u
inst : CommSemiring R₀
inst_1 : Ring R
inst_2 : Algebra R₀ R
inst_3 : IsSemisimpleRing R
⊢ IsSemisimpleRing.{u} Rᵐᵒᵖ

Tactic:
have ⟨_, _, _, _, _, ⟨e⟩⟩ := exists_ringEquiv_pi_matrix_divisionRing R
  ((e.op.trans (.piMulOpposite _)).trans (.piCongrRight fun _ ↦ .symm .mopMatrix)).symm
    |>.isSemisimpleRing

Premises used: RingEquiv.piMulOpposite, RingEquiv.op, Matrix, MulOpposite, RingEquiv.piCongrRight, RingEquiv.mopMatrix, IsSemisimpleRing.exists_ringEquiv_pi_matrix_divisionRing, IsSemisimpleRing, RingEquiv.trans, RingEquiv.isSemisimpleRing, Fin, DFunLike.coe, _private.0.IsSemisimpleRing.instMatrix.match_1, RingEquiv.symm
-- Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin
Goal:
R : Type u
inst : Ring R
⊢ IsSemisimpleRing.{u} Rᵐᵒᵖ ↔ IsSemisimpleRing R

Tactic:
⟨fun _ ↦ (RingEquiv.opOp R).symm.isSemisimpleRing, fun _ ↦ inferInstance⟩

Premises used: RingEquiv.opOp, inferInstance, Iff.intro, RingEquiv.isSemisimpleRing, RingEquiv.symm
-- Module: Mathlib.RingTheory.SimpleRing.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
inst_1 : IsSimpleRing R
obtain : ∀ (x : R), Membership.mem (γ := TwoSidedIdeal R) ⊤ x → ∀ (hx : x ∉ ⊥), Nontrivial R
⊢ Nontrivial R

Tactic:
obtain ⟨x, _, hx⟩ := SetLike.exists_of_lt (bot_lt_top : (⊥ : TwoSidedIdeal R) < ⊤)

Premises used: SetLike.exists_of_lt, bot_lt_top
-- Module: Mathlib.RingTheory.SimpleRing.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
inst_1 : IsSimpleRing R
x : R
left : Membership.mem (γ := TwoSidedIdeal R) ⊤ x
hx : x ∉ ⊥
w w₁ : R
h : x ≠ 0
⊢ Nontrivial R

Tactic:
use x, 0, hx
-- Module: Mathlib.RingTheory.SimpleRing.Basic
Goal:
A : Type u_2
inst : NonAssocRing A
inst_1 : IsSimpleRing A
I : TwoSidedIdeal A
hI : I ≠ ⊥
⊢ 1 ∈ I

Tactic:
(eq_bot_or_eq_top I).resolve_left hI ▸ ⟨⟩

Premises used: Eq.rec, Or.resolve_left, Eq.symm, IsSimpleOrder.eq_bot_or_eq_top, True.intro
-- Module: Mathlib.RingTheory.SimpleRing.Basic
Goal:
A : Type u_2
inst : NonAssocRing A
inst_1 : IsSimpleRing A
x : A
hx : x ≠ 0
hxI : Membership.mem (γ := TwoSidedIdeal A) ⊥ x
⊢ False

Tactic:
hx hxI
-- Module: Mathlib.RingTheory.SimpleRing.Basic
Goal:
A : Type u_2
inst : NonAssocRing A
inst_1 : IsSimpleRing A
x : A
hx : x ≠ 0
hxI : Membership.mem (γ := TwoSidedIdeal A) ⊥ x
⊢ False

Tactic:
exact hx hxI
-- Module: Mathlib.RingTheory.SimpleRing.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
A : Type u_2
inst_1 : DivisionRing A
I : TwoSidedIdeal A
rw : ¬I = ⊥ → 1 ∈ I
⊢ I = ⊥ ∨ I = ⊤

Tactic:
rw [or_iff_not_imp_left, ← I.one_mem_iff]

Premises used: TwoSidedIdeal.one_mem_iff, Classical.or_iff_not_imp_left
-- Module: Mathlib.RingTheory.SimpleRing.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
A : Type u_2
inst_1 : DivisionRing A
I : TwoSidedIdeal A
H : ¬I = ⊥
obtain : ∀ (x : A) (hx1 : x ∈ I) (hx2 : x ≠ 0), 1 ∈ I
⊢ 1 ∈ I

Tactic:
obtain ⟨x, hx1, hx2 : x ≠ 0⟩ := SetLike.exists_of_lt (bot_lt_iff_ne_bot.mpr H : ⊥ < I)

Premises used: Iff.mpr, SetLike.exists_of_lt, bot_lt_iff_ne_bot
-- Module: Mathlib.RingTheory.SimpleRing.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
A : Type u_2
inst_1 : DivisionRing A
I : TwoSidedIdeal A
H : ¬I = ⊥
x : A
hx1 : x ∈ I
hx2 : x ≠ 0
⊢ 1 ∈ I

Tactic:
simpa [inv_mul_cancel₀ hx2] using I.mul_mem_left x⁻¹ _ hx1

Premises used: TwoSidedIdeal.mul_mem_left, Inv.inv, inv_mul_cancel₀
-- Module: Mathlib.RingTheory.SimpleRing.Basic
Goal:
R : Type u_2
S : Type u_3
inst : NonAssocRing R
inst_1 : IsSimpleRing R
inst_2 : NonAssocSemiring S
f : R →+* S
h : Eq (α := TwoSidedIdeal R) (TwoSidedIdeal.ker f) ⊤
⊢ Membership.mem (γ := TwoSidedIdeal R) (TwoSidedIdeal.ker f) 1

Tactic:
have mem : 1 ∈ TwoSidedIdeal.ker f := h.symm ▸ TwoSidedIdeal.mem_top _
-- Module: Mathlib.RingTheory.SimpleRing.Basic
Goal:
R : Type u_2
S : Type u_3
inst : NonAssocRing R
inst_1 : IsSimpleRing R
inst_2 : NonAssocSemiring S
f : R →+* S
h : Eq (α := TwoSidedIdeal R) (TwoSidedIdeal.ker f) ⊤
mem : Membership.mem (γ := TwoSidedIdeal R) (TwoSidedIdeal.ker f) 1
rwa : ∀ (mem : Eq.{u_3 + 1} (α := S) ((f : (a : R) → S) 1 : S) (0 : S)), Eq.{u_3 + 1} (α := S) 0 1
rwa₁ : ∀ (mem : Eq.{u_3 + 1} (α := S) 1 0), Eq.{u_3 + 1} (α := S) 0 1
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (mem : Eq.{u_3 + 1} (α := S) 0 1), Eq.{u_3 + 1} (α := S) 0 1
⊢ Eq.{u_3 + 1} (α := S) 0 1

Tactic:
rwa [TwoSidedIdeal.mem_ker, map_one, eq_comm] at mem

Premises used: eq_comm, map_one, TwoSidedIdeal.mem_ker
-- Module: Mathlib.RingTheory.SimpleRing.Basic
Goal:
R : Type u_2
S : Type u_3
inst : NonAssocRing R
inst_1 : IsSimpleRing R
inst_2 : NonAssocSemiring S
inst_3 : Nontrivial S
f : R →+* S
⊢ Function.Injective.{u_2 + 1, u_3 + 1} (α := R) (β := S) (⇑f : (a : R) → S)

Tactic:
injective_ringHom_or_subsingleton_codomain f |>.resolve_right fun r => not_subsingleton _ r

Premises used: IsSimpleRing.injective_ringHom_or_subsingleton_codomain, not_subsingleton, Or.resolve_right
-- Module: Mathlib.RingTheory.SimpleRing.Basic
Goal:
R : Type u
inst : NonAssocRing R
inst_1 : Nontrivial R
H :
  ∀ {S : Type u} [inst_2 : NonAssocSemiring S] (f : R →+* S),
    Function.Injective (α := R) (β := S) (⇑f : (a : R) → S) ∨ Subsingleton S
x : Type u
x_1 : NonAssocSemiring x
h : Nontrivial x
f : R →+* x
⊢ ¬Subsingleton x

Tactic:
simpa [not_subsingleton_iff_nontrivial]

Premises used: not_subsingleton_iff_nontrivial
-- Module: Mathlib.RingTheory.SimpleRing.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
inst_1 : IsSimpleRing R
⊢ IsSimpleRing.{u_1} Rᵐᵒᵖ

Tactic:
⟨TwoSidedIdeal.opOrderIso.symm.isSimpleOrder⟩

Premises used: IsSimpleRing.mk, TwoSidedIdeal.opOrderIso, OrderIso.symm, OrderIso.isSimpleOrder
-- Module: Mathlib.RingTheory.SimpleRing.Congr
Goal:
R : Type u_1
inst : Ring R
e : TwoSidedIdeal R ≃o { I : Ideal R // I.IsTwoSided } := orderIsoIsTwoSided
simp_rw :
  (Nontrivial R ∧
      ∀ (a : Ideal R) (b : a.IsTwoSided),
        Eq (α := { I : Ideal R // I.IsTwoSided })
            ((e : (a : TwoSidedIdeal R) → { I : Ideal R // I.IsTwoSided })
                ((e.toEquiv (r := fun (x1 x2 : TwoSidedIdeal R) ↦ x1 ≤ x2) (s :=
                        fun (x1 x2 : { I : Ideal R // I.IsTwoSided }) ↦ x1 ≤ x2).symm :
                    (a : { I : Ideal R // I.IsTwoSided }) → TwoSidedIdeal R)
                  (Subtype.mk (p := fun (a : Ideal R) ↦ a.IsTwoSided) a b)) :
              { I : Ideal R // I.IsTwoSided })
            ((e : (a : TwoSidedIdeal R) → { I : Ideal R // I.IsTwoSided }) ⊥ : { I : Ideal R // I.IsTwoSided }) ∨
          Eq (α := { I : Ideal R // I.IsTwoSided })
            ((e : (a : TwoSidedIdeal R) → { I : Ideal R // I.IsTwoSided })
                ((e.toEquiv (r := fun (x1 x2 : TwoSidedIdeal R) ↦ x1 ≤ x2) (s :=
                        fun (x1 x2 : { I : Ideal R // I.IsTwoSided }) ↦ x1 ≤ x2).symm :
                    (a : { I : Ideal R // I.IsTwoSided }) → TwoSidedIdeal R)
                  (Subtype.mk (p := fun (a : Ideal R) ↦ a.IsTwoSided) a b)) :
              { I : Ideal R // I.IsTwoSided })
            ((e : (a : TwoSidedIdeal R) → { I : Ideal R // I.IsTwoSided }) ⊤ : { I : Ideal R // I.IsTwoSided })) ↔
    Nontrivial R ∧ ∀ (I : Ideal R), I.IsTwoSided → I = ⊥ ∨ I = ⊤
⊢ IsSimpleRing R ↔ Nontrivial R ∧ ∀ (I : Ideal R), I.IsTwoSided → I = ⊥ ∨ I = ⊤

Tactic:
simp_rw [isSimpleRing_iff, isSimpleOrder_iff, orderIsoRingCon.toEquiv.nontrivial_congr,
    RingCon.nontrivial_iff, e.forall_congr_left, Subtype.forall, ← e.injective.eq_iff]

Premises used: Equiv.nontrivial_congr, Equiv.forall_congr_left, Function.Injective.eq_iff, Subtype.forall, isSimpleRing_iff, RingCon.nontrivial_iff, isSimpleOrder_iff, OrderIso.injective, TwoSidedIdeal.orderIsoRingCon, RelIso.toEquiv
-- Module: Mathlib.RingTheory.SimpleRing.Congr
Goal:
R : Type u_1
inst : Ring R
e : TwoSidedIdeal R ≃o { I : Ideal R // I.IsTwoSided } := orderIsoIsTwoSided
⊢ (Nontrivial R ∧
      ∀ (a : Ideal R) (b : a.IsTwoSided),
        Eq (α := { I : Ideal R // I.IsTwoSided })
            ((e : (a : TwoSidedIdeal R) → { I : Ideal R // I.IsTwoSided })
                ((e.toEquiv (r := fun (x1 x2 : TwoSidedIdeal R) ↦ x1 ≤ x2) (s :=
                        fun (x1 x2 : { I : Ideal R // I.IsTwoSided }) ↦ x1 ≤ x2).symm :
                    (a : { I : Ideal R // I.IsTwoSided }) → TwoSidedIdeal R)
                  (Subtype.mk (p := fun (a : Ideal R) ↦ a.IsTwoSided) a b)) :
              { I : Ideal R // I.IsTwoSided })
            ((e : (a : TwoSidedIdeal R) → { I : Ideal R // I.IsTwoSided }) ⊥ : { I : Ideal R // I.IsTwoSided }) ∨
          Eq (α := { I : Ideal R // I.IsTwoSided })
            ((e : (a : TwoSidedIdeal R) → { I : Ideal R // I.IsTwoSided })
                ((e.toEquiv (r := fun (x1 x2 : TwoSidedIdeal R) ↦ x1 ≤ x2) (s :=
                        fun (x1 x2 : { I : Ideal R // I.IsTwoSided }) ↦ x1 ≤ x2).symm :
                    (a : { I : Ideal R // I.IsTwoSided }) → TwoSidedIdeal R)
                  (Subtype.mk (p := fun (a : Ideal R) ↦ a.IsTwoSided) a b)) :
              { I : Ideal R // I.IsTwoSided })
            ((e : (a : TwoSidedIdeal R) → { I : Ideal R // I.IsTwoSided }) ⊤ : { I : Ideal R // I.IsTwoSided })) ↔
    Nontrivial R ∧ ∀ (I : Ideal R), I.IsTwoSided → I = ⊥ ∨ I = ⊤

Tactic:
simp [e, Subtype.ext_iff]

Premises used: Subtype.ext_iff
-- Module: Mathlib.RingTheory.SimpleRing.Field
Goal:
A : Type u_1
inst : Ring A
inst_1 : IsSimpleRing A
x : A
hx1 : Membership.mem (γ := Subring A) (Subring.center A) x
hx2 : Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subring A) (Subring.center A) x) x hx1 ≠ 0
⊢ ∀ (g : A), g * x = x * g

Tactic:
rw [Subring.mem_center_iff] at hx1

Premises used: Subring.mem_center_iff
-- Module: Mathlib.RingTheory.SimpleRing.Field
Goal:
A : Type u_1
inst : Ring A
inst_1 : IsSimpleRing A
x : A
hx1 : Membership.mem (γ := Subring A) (Subring.center A) x
hx2 : Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subring A) (Subring.center A) x) x hx1 ≠ 0
hx1₁ : ∀ (g : A), g * x = x * g
⊢ Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subring A) (Subring.center A) x) x hx1 ≠ 0

Tactic:
rw [Subring.mem_center_iff] at hx1

Premises used: Subring.mem_center_iff
-- Module: Mathlib.RingTheory.SimpleRing.Field
Goal:
A : Type u_1
inst : Ring A
inst_1 : IsSimpleRing A
x : A
hx1_1 : Membership.mem (γ := Subring A) (Subring.center A) x
hx1 : ∀ (g : A), g * x = x * g
hx2 : Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subring A) (Subring.center A) x) x hx1_1 ≠ 0
⊢ x ≠ 0

Tactic:
simpa [Subtype.ext_iff] using hx2

Premises used: Subtype.ext_iff
-- Module: Mathlib.RingTheory.SimpleRing.Field
Goal:
A : Type u_1
inst : Ring A
inst_1 : IsSimpleRing A
x : A
hx1_1 : Membership.mem (γ := Subring A) (Subring.center A) x
hx1 : ∀ (g : A), g * x = x * g
hx2 : Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subring A) (Subring.center A) x) x hx1_1 ≠ 0
⊢ x ≠ 0

Tactic:
replace hx2 : x ≠ 0 := by simpa [Subtype.ext_iff] using hx2
-- Module: Mathlib.RingTheory.SimpleRing.Field
Goal:
A : Type u_1
inst : Ring A
inst_1 : IsSimpleRing A
x : A
hx1_1 : Membership.mem (γ := Subring A) (Subring.center A) x
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
⊢ Eq.{u_1 + 1} (α := A) ((fun (x_1 : A) ↦ x * x_1) 0) 0

Tactic:
simp
-- Module: Mathlib.RingTheory.SimpleRing.Field
Goal:
A : Type u_1
inst : Ring A
inst_1 : IsSimpleRing A
x_1 : A
hx1_1 : Membership.mem (γ := Subring A) (Subring.center A) x_1
hx1 : ∀ (g : A), g * x_1 = x_1 * g
hx2 : x_1 ≠ 0
x y : A
⊢ Membership.mem (γ := Set A) (Set.range fun (x : A) ↦ x_1 * x)
    (HAdd.hAdd (α := A) ((fun (x : A) ↦ x_1 * x) x) ((fun (x : A) ↦ x_1 * x) y))

Tactic:
⟨x + y, mul_add _ _ _⟩

Premises used: Set.Mem, setOf, HAdd.hAdd, Exists.intro, mul_add, Set.range
-- Module: Mathlib.RingTheory.SimpleRing.Field
Goal:
A : Type u_1
inst : Ring A
inst_1 : IsSimpleRing A
x_1 : A
hx1_1 : Membership.mem (γ := Subring A) (Subring.center A) x_1
hx1 : ∀ (g : A), g * x_1 = x_1 * g
hx2 : x_1 ≠ 0
x y : A
⊢ Membership.mem (γ := Set A) (Set.range fun (x : A) ↦ x_1 * x)
    (HAdd.hAdd (α := A) ((fun (x : A) ↦ x_1 * x) x) ((fun (x : A) ↦ x_1 * x) y))

Tactic:
exact ⟨x + y, mul_add _ _ _⟩
-- Module: Mathlib.RingTheory.SimpleRing.Field
Goal:
A : Type u_1
inst : Ring A
inst_1 : IsSimpleRing A
x_1 : A
hx1_1 : Membership.mem (γ := Subring A) (Subring.center A) x_1
hx1 : ∀ (g : A), g * x_1 = x_1 * g
hx2 : x_1 ≠ 0
x : A
⊢ Eq.{u_1 + 1} (α := A) ((fun (x : A) ↦ x_1 * x) (-x)) (-(fun (x : A) ↦ x_1 * x) x)

Tactic:
simp
-- Module: Mathlib.RingTheory.SimpleRing.Field
Goal:
A : Type u_1
inst : Ring A
inst_1 : IsSimpleRing A
x_1 : A
hx1_1 : Membership.mem (γ := Subring A) (Subring.center A) x_1
hx1 : ∀ (g : A), g * x_1 = x_1 * g
hx2 : x_1 ≠ 0
x : A
⊢ Membership.mem (γ := Set A) (Set.range fun (x : A) ↦ x_1 * x) (-(fun (x : A) ↦ x_1 * x) x)

Tactic:
exact ⟨-x, by simp⟩
-- Module: Mathlib.RingTheory.SimpleRing.Field
Goal:
A : Type u_1
inst : Ring A
inst_1 : IsSimpleRing A
x : A
hx1_1 : Membership.mem (γ := Subring A) (Subring.center A) x
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
a c : A
dsimp : x * (a * c) = a * (x * c)
⊢ (fun (x_1 : A) ↦ x * x_1) (a * c) = a * (fun (x_1 : A) ↦ x * x_1) c

Tactic:
dsimp
-- Module: Mathlib.RingTheory.SimpleRing.Field
Goal:
A : Type u_1
inst : Ring A
inst_1 : IsSimpleRing A
x : A
hx1_1 : Membership.mem (γ := Subring A) (Subring.center A) x
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
a c : A
rw : x * a * c = a * (x * c)
rw₁ : a * x * c = a * (x * c)
rw₂ rw₃ : a * (x * c) = a * (x * c)
⊢ x * (a * c) = a * (x * c)

Tactic:
rw [← mul_assoc, ← hx1, mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.RingTheory.SimpleRing.Field
Goal:
A : Type u_1
inst : Ring A
inst_1 : IsSimpleRing A
x : A
hx1_1 : Membership.mem (γ := Subring A) (Subring.center A) x
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
a c : A
⊢ Membership.mem (γ := Set A) (Set.range fun (x_1 : A) ↦ x * x_1) (a * (fun (x_1 : A) ↦ x * x_1) c)

Tactic:
exact ⟨a * c, by dsimp; rw [← mul_assoc, ← hx1, mul_assoc]⟩
-- Module: Mathlib.RingTheory.SimpleRing.Field
Goal:
A : Type u_1
inst : Ring A
inst_1 : IsSimpleRing A
x : A
hx1_1 : Membership.mem (γ := Subring A) (Subring.center A) x
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
b a : A
dsimp : x * (a * b) = x * a * b
⊢ (fun (x_1 : A) ↦ x * x_1) (a * b) = (fun (x_1 : A) ↦ x * x_1) a * b

Tactic:
dsimp
-- Module: Mathlib.RingTheory.SimpleRing.Field
Goal:
A : Type u_1
inst : Ring A
inst_1 : IsSimpleRing A
x : A
hx1_1 : Membership.mem (γ := Subring A) (Subring.center A) x
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
b a : A
rw : x * a * b = x * a * b
rw₁ : a * x * b = a * x * b
rw₂ rw₃ : a * (x * b) = a * (x * b)
⊢ x * (a * b) = x * a * b

Tactic:
rw [← mul_assoc, ← hx1, mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.RingTheory.SimpleRing.Field
Goal:
A : Type u_1
inst : Ring A
inst_1 : IsSimpleRing A
x : A
hx1_1 : Membership.mem (γ := Subring A) (Subring.center A) x
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
b a : A
⊢ Membership.mem (γ := Set A) (Set.range fun (x_1 : A) ↦ x * x_1) ((fun (x_1 : A) ↦ x * x_1) a * b)

Tactic:
exact ⟨a * b, by dsimp; rw [← mul_assoc, ← hx1, mul_assoc]⟩
-- Module: Mathlib.RingTheory.SimpleRing.Field
Goal:
A : Type u_1
inst : Ring A
inst_1 : IsSimpleRing A
x : A
hx1_1 : Membership.mem (γ := Subring A) (Subring.center A) x
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
I : TwoSidedIdeal A := mk' (Set.range fun (x_1 : A) ↦ x * x_1) ⋯ ⋯ ⋯ ⋯ ⋯
⊢ x * 1 = x

Tactic:
simp
-- Module: Mathlib.RingTheory.SimpleRing.Field
Goal:
A : Type u_1
inst : Ring A
inst_1 : IsSimpleRing A
x : A
hx1_1 : Membership.mem (γ := Subring A) (Subring.center A) x
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
I : TwoSidedIdeal A := mk' (Set.range fun (x_1 : A) ↦ x * x_1) ⋯ ⋯ ⋯ ⋯ ⋯
⊢ x ∈ I

Tactic:
simpa [I, mem_mk'] using ⟨1, by simp⟩

Premises used: TwoSidedIdeal.mem_mk'
-- Module: Mathlib.RingTheory.SimpleRing.Field
Goal:
A : Type u_1
inst : Ring A
inst_1 : IsSimpleRing A
x : A
hx1_1 : Membership.mem (γ := Subring A) (Subring.center A) x
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
I : TwoSidedIdeal A := mk' (Set.range fun (x_1 : A) ↦ x * x_1) ⋯ ⋯ ⋯ ⋯ ⋯
⊢ 1 ∈ I

Tactic:
have mem : 1 ∈ I := one_mem_of_ne_zero_mem I hx2 (by simpa [I, mem_mk'] using ⟨1, by simp⟩)
-- Module: Mathlib.RingTheory.SimpleRing.Field
Goal:
A : Type u_1
inst : Ring A
inst_1 : IsSimpleRing A
x : A
hx1_1 : Membership.mem (γ := Subring A) (Subring.center A) x
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
I : TwoSidedIdeal A := mk' (Set.range fun (x_1 : A) ↦ x * x_1) ⋯ ⋯ ⋯ ⋯ ⋯
mem : 1 ∈ I
⊢ ∃ (y : A), x * y = 1

Tactic:
simp only [TwoSidedIdeal.mem_mk', Set.mem_range, I] at mem

Premises used: Set.mem_range, TwoSidedIdeal.mem_mk'
-- Module: Mathlib.RingTheory.SimpleRing.Field
Goal:
A : Type u_1
inst : Ring A
inst_1 : IsSimpleRing A
x : A
hx1_1 : Membership.mem (γ := Subring A) (Subring.center A) x
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
I : TwoSidedIdeal A := mk' (Set.range fun (x_1 : A) ↦ x * x_1) ⋯ ⋯ ⋯ ⋯ ⋯
mem : ∃ (y : A), x * y = 1
obtain :
  ∀ (y : A) (hy : x * y = 1),
    ∃ (b : ↥(Subring.center A)),
      Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subring A) (Subring.center A) x) x hx1_1 * b = 1
⊢ ∃ (b : ↥(Subring.center A)),
    Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subring A) (Subring.center A) x) x hx1_1 * b = 1

Tactic:
obtain ⟨y, hy⟩ := mem
-- Module: Mathlib.RingTheory.SimpleRing.Field
Goal:
A : Type u_1
inst : Ring A
inst_1 : IsSimpleRing A
x : A
hx1_1 : Membership.mem (γ := Subring A) (Subring.center A) x
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
I : TwoSidedIdeal A := mk' (Set.range fun (x_1 : A) ↦ x * x_1) ⋯ ⋯ ⋯ ⋯ ⋯
y : A
hy : x * y = 1
a :
  (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subring A) (Subring.center A) x) x hx1_1 *
          Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subring A) (Subring.center A) x) y ⋯) :
      A) =
    (↑1 : A)
⊢ Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subring A) (Subring.center A) x) x hx1_1 *
      Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subring A) (Subring.center A) x) y ⋯ =
    1

Tactic:
ext
-- Module: Mathlib.RingTheory.SimpleRing.Field
Goal:
A : Type u_1
inst : Ring A
inst_1 : IsSimpleRing A
x : A
hx1_1 : Membership.mem (γ := Subring A) (Subring.center A) x
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
I : TwoSidedIdeal A := mk' (Set.range fun (x_1 : A) ↦ x * x_1) ⋯ ⋯ ⋯ ⋯ ⋯
y : A
hy : x * y = 1
⊢ (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subring A) (Subring.center A) x) x hx1_1 *
          Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subring A) (Subring.center A) x) y ⋯) :
      A) =
    (↑1 : A)

Tactic:
hy
-- Module: Mathlib.RingTheory.SimpleRing.Field
Goal:
A : Type u_1
inst : Ring A
inst_1 : IsSimpleRing A
x : A
hx1_1 : Membership.mem (γ := Subring A) (Subring.center A) x
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
I : TwoSidedIdeal A := mk' (Set.range fun (x_1 : A) ↦ x * x_1) ⋯ ⋯ ⋯ ⋯ ⋯
y : A
hy : x * y = 1
⊢ (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subring A) (Subring.center A) x) x hx1_1 *
          Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subring A) (Subring.center A) x) y ⋯) :
      A) =
    (↑1 : A)

Tactic:
exact hy
-- Module: Mathlib.RingTheory.SimpleRing.Field
Goal:
A : Type u_1
inst : Ring A
inst_1 : IsSimpleRing A
x : A
hx1_1 : Membership.mem (γ := Subring A) (Subring.center A) x
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
I : TwoSidedIdeal A := mk' (Set.range fun (x_1 : A) ↦ x * x_1) ⋯ ⋯ ⋯ ⋯ ⋯
y : A
hy : x * y = 1
refine : ∀ (a : A), a * y = y * a
⊢ ∃ (b : ↥(Subring.center A)),
    Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subring A) (Subring.center A) x) x hx1_1 * b = 1

Tactic:
refine ⟨⟨y, Subring.mem_center_iff.2 fun a ↦ ?_⟩, by ext; exact hy⟩
-- Module: Mathlib.RingTheory.SimpleRing.Field
Goal:
A : Type u_1
inst : Ring A
inst_1 : IsSimpleRing A
x : A
hx1_1 : Membership.mem (γ := Subring A) (Subring.center A) x
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
I : TwoSidedIdeal A := mk' (Set.range fun (x_1 : A) ↦ x * x_1) ⋯ ⋯ ⋯ ⋯ ⋯
y : A
hy : x * y = 1
a : A
rw : a * y = 1 * a * y
rw₁ rw₂ : a * y = a * y
⊢ a * y = x * y * a * y

Tactic:
rw [hy, one_mul]

Premises used: one_mul
-- Module: Mathlib.RingTheory.SimpleRing.Field
Goal:
A : Type u_1
inst : Ring A
inst_1 : IsSimpleRing A
x : A
hx1_1 : Membership.mem (γ := Subring A) (Subring.center A) x
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
I : TwoSidedIdeal A := mk' (Set.range fun (x_1 : A) ↦ x * x_1) ⋯ ⋯ ⋯ ⋯ ⋯
y : A
hy : x * y = 1
a : A
rw rw₁ : x * y * a * y = x * y * a * y
⊢ x * y * a * y = y * x * a * y

Tactic:
rw [hx1]
-- Module: Mathlib.RingTheory.SimpleRing.Field
Goal:
A : Type u_1
inst : Ring A
inst_1 : IsSimpleRing A
x : A
hx1_1 : Membership.mem (γ := Subring A) (Subring.center A) x
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
I : TwoSidedIdeal A := mk' (Set.range fun (x_1 : A) ↦ x * x_1) ⋯ ⋯ ⋯ ⋯ ⋯
y : A
hy : x * y = 1
a : A
rw rw₁ : y * (x * a) * y = y * (x * a) * y
⊢ y * x * a * y = y * (x * a) * y

Tactic:
rw [mul_assoc y x a]

Premises used: mul_assoc
-- Module: Mathlib.RingTheory.SimpleRing.Field
Goal:
A : Type u_1
inst : Ring A
inst_1 : IsSimpleRing A
x : A
hx1_1 : Membership.mem (γ := Subring A) (Subring.center A) x
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
I : TwoSidedIdeal A := mk' (Set.range fun (x_1 : A) ↦ x * x_1) ⋯ ⋯ ⋯ ⋯ ⋯
y : A
hy : x * y = 1
a : A
rw rw₁ : y * (x * a) * y = y * (x * a) * y
⊢ y * (x * a) * y = y * (a * x) * y

Tactic:
rw [hx1]
-- Module: Mathlib.RingTheory.SimpleRing.Field
Goal:
A : Type u_1
inst : Ring A
inst_1 : IsSimpleRing A
x : A
hx1_1 : Membership.mem (γ := Subring A) (Subring.center A) x
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
I : TwoSidedIdeal A := mk' (Set.range fun (x_1 : A) ↦ x * x_1) ⋯ ⋯ ⋯ ⋯ ⋯
y : A
hy : x * y = 1
a : A
rw rw₁ : y * (a * x * y) = y * (a * x * y)
⊢ y * (a * x) * y = y * (a * x * y)

Tactic:
rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.RingTheory.SimpleRing.Field
Goal:
A : Type u_1
inst : Ring A
inst_1 : IsSimpleRing A
x : A
hx1_1 : Membership.mem (γ := Subring A) (Subring.center A) x
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
I : TwoSidedIdeal A := mk' (Set.range fun (x_1 : A) ↦ x * x_1) ⋯ ⋯ ⋯ ⋯ ⋯
y : A
hy : x * y = 1
a : A
rw rw₁ : y * (a * (x * y)) = y * (a * (x * y))
⊢ y * (a * x * y) = y * (a * (x * y))

Tactic:
rw [mul_assoc a x y]

Premises used: mul_assoc