-- Mathlib/RingTheory/SimpleRing/Field.lean
lemma isField_center (A : Type*) [Ring A] [IsSimpleRing A] : IsField (Subring.center A) where
  exists_pair_ne := ⟨0, 1, zero_ne_one⟩
  mul_comm := mul_comm
  mul_inv_cancel

Proof state:
A : Type u_1
inst✝¹ : Ring A
inst✝ : IsSimpleRing A
x : A
hx1✝ : x ∈ Subring.center A
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
I : TwoSidedIdeal A := mk' (Set.range fun x_1 => x * x_1) ⋯ ⋯ ⋯ ⋯ ⋯
y : A
hy : x * y = 1
a : A
⊢ y * (a * x) * y = y * (a * x * y)

Tactic:
rw [mul_assoc]

Result:
no goals

Proof state:
A : Type u_1
inst✝¹ : Ring A
inst✝ : IsSimpleRing A
x : A
hx1✝ : x ∈ Subring.center A
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
I : TwoSidedIdeal A := mk' (Set.range fun x_1 => x * x_1) ⋯ ⋯ ⋯ ⋯ ⋯
y : A
hy : x * y = 1
a : A
⊢ y * (a * x * y) = y * (a * (x * y))

Tactic:
rw [mul_assoc a x y]

Result:
no goals

Proof state:
A : Type u_1
inst✝¹ : Ring A
inst✝ : IsSimpleRing A
x : A
hx1✝ : x ∈ Subring.center A
hx1 : ∀ (g : A), g * x = x * g
hx2 : ⟨x, hx1✝⟩ ≠ 0
⊢ x ≠ 0

Tactic:
simpa [Subtype.ext_iff] using hx2

Result:
no goals

Proof state:
A : Type u_1
inst✝¹ : Ring A
inst✝ : IsSimpleRing A
x : A
hx1✝ : x ∈ Subring.center A
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
I : TwoSidedIdeal A := mk' (Set.range fun x_1 => x * x_1) ⋯ ⋯ ⋯ ⋯ ⋯
y : A
hy : x * y = 1
a : A
⊢ x * y * a * y = y * x * a * y

Tactic:
rw [hx1]

Result:
no goals

Proof state:
case mk
A : Type u_1
inst✝¹ : Ring A
inst✝ : IsSimpleRing A
x : A
hx1 : x ∈ Subring.center A
hx2 : ⟨x, hx1⟩ ≠ 0
⊢ ∃ b, ⟨x, hx1⟩ * b = 1

Tactic:
rw [Subring.mem_center_iff] at hx1

Result:
case mk
A : Type u_1
inst✝¹ : Ring A
inst✝ : IsSimpleRing A
x : A
hx1✝ : x ∈ Subring.center A
hx1 : ∀ (g : A), g * x = x * g
hx2 : ⟨x, hx1✝⟩ ≠ 0
⊢ ∃ b, ⟨x, hx1✝⟩ * b = 1

Proof state:
A : Type u_1
inst✝¹ : Ring A
inst✝ : IsSimpleRing A
x : A
hx1✝ : x ∈ Subring.center A
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
I : TwoSidedIdeal A := mk' (Set.range fun x_1 => x * x_1) ⋯ ⋯ ⋯ ⋯ ⋯
⊢ x * 1 = x

Tactic:
simp

Result:
no goals

Proof state:
A : Type u_1
inst✝¹ : Ring A
inst✝ : IsSimpleRing A
x : A
hx1✝ : x ∈ Subring.center A
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
I : TwoSidedIdeal A := mk' (Set.range fun x_1 => x * x_1) ⋯ ⋯ ⋯ ⋯ ⋯
y : A
hy : x * y = 1
⊢ ⟨x, hx1✝⟩ * ⟨y, ⋯⟩ = 1

Tactic:
ext

Result:
case a
A : Type u_1
inst✝¹ : Ring A
inst✝ : IsSimpleRing A
x : A
hx1✝ : x ∈ Subring.center A
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
I : TwoSidedIdeal A := mk' (Set.range fun x_1 => x * x_1) ⋯ ⋯ ⋯ ⋯ ⋯
y : A
hy : x * y = 1
⊢ ↑(⟨x, hx1✝⟩ * ⟨y, ⋯⟩) = ↑1

Proof state:
case mk
A : Type u_1
inst✝¹ : Ring A
inst✝ : IsSimpleRing A
x : A
hx1✝ : x ∈ Subring.center A
hx1 : ∀ (g : A), g * x = x * g
hx2 : ⟨x, hx1✝⟩ ≠ 0
⊢ ∃ b, ⟨x, hx1✝⟩ * b = 1

Tactic:
replace hx2 : x ≠ 0 := by simpa [Subtype.ext_iff] using hx2

Result:
case mk
A : Type u_1
inst✝¹ : Ring A
inst✝ : IsSimpleRing A
x : A
hx1✝ : x ∈ Subring.center A
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
⊢ ∃ b, ⟨x, hx1✝⟩ * b = 1

Proof state:
A : Type u_1
inst✝¹ : Ring A
inst✝ : IsSimpleRing A
x : A
hx1✝ : x ∈ Subring.center A
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
⊢ ∀ {x_1 y : A}, (y ∈ Set.range fun x_2 => x * x_2) → x_1 * y ∈ Set.range fun x_2 => x * x_2

Tactic:
rintro a _ ⟨c, rfl⟩

Result:
case intro
A : Type u_1
inst✝¹ : Ring A
inst✝ : IsSimpleRing A
x : A
hx1✝ : x ∈ Subring.center A
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
a c : A
⊢ a * (fun x_1 => x * x_1) c ∈ Set.range fun x_1 => x * x_1

Proof state:
A : Type u_1
inst✝¹ : Ring A
inst✝ : IsSimpleRing A
x : A
hx1✝ : x ∈ Subring.center A
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
a c : A
⊢ x * (a * c) = a * (x * c)

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

Result:
no goals

Proof state:
case mk.intro
A : Type u_1
inst✝¹ : Ring A
inst✝ : IsSimpleRing A
x : A
hx1✝ : x ∈ Subring.center A
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
I : TwoSidedIdeal A := mk' (Set.range fun x_1 => x * x_1) ⋯ ⋯ ⋯ ⋯ ⋯
y : A
hy : x * y = 1
a : A
⊢ a * y = y * a

Tactic:
calc a * y
  _ = (x * y) * a * y := by rw [hy, one_mul]
  _ = (y * x) * a * y := by rw [hx1]
  _ = y * (x * a) * y := by rw [mul_assoc y x a]
  _ = y * (a * x) * y := by rw [hx1]
  _ = y * ((a * x) * y) := by rw [mul_assoc]
  _ = y * (a * (x * y)) := by rw [mul_assoc a x y]
  _ = y * a := by rw [hy, mul_one]

Result:
no goals

Proof state:
case intro
A : Type u_1
inst✝¹ : Ring A
inst✝ : IsSimpleRing A
x✝ : A
hx1✝ : x✝ ∈ Subring.center A
hx1 : ∀ (g : A), g * x✝ = x✝ * g
hx2 : x✝ ≠ 0
x : A
⊢ -(fun x => x✝ * x) x ∈ Set.range fun x => x✝ * x

Tactic:
exact ⟨-x, by simp⟩

Result:
no goals

Proof state:
A : Type u_1
inst✝¹ : Ring A
inst✝ : IsSimpleRing A
x✝ : A
hx1✝ : x✝ ∈ Subring.center A
hx1 : ∀ (g : A), g * x✝ = x✝ * g
hx2 : x✝ ≠ 0
x : A
⊢ (fun x => x✝ * x) (-x) = -(fun x => x✝ * x) x

Tactic:
simp

Result:
no goals

Proof state:
case mk
A : Type u_1
inst✝¹ : Ring A
inst✝ : IsSimpleRing A
x : A
hx1✝ : x ∈ Subring.center A
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
I : TwoSidedIdeal A := mk' (Set.range fun x_1 => x * x_1) ⋯ ⋯ ⋯ ⋯ ⋯
mem : 1 ∈ I
⊢ ∃ b, ⟨x, hx1✝⟩ * b = 1

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

Result:
case mk
A : Type u_1
inst✝¹ : Ring A
inst✝ : IsSimpleRing A
x : A
hx1✝ : x ∈ Subring.center A
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
I : TwoSidedIdeal A := mk' (Set.range fun x_1 => x * x_1) ⋯ ⋯ ⋯ ⋯ ⋯
mem : ∃ y, x * y = 1
⊢ ∃ b, ⟨x, hx1✝⟩ * b = 1