-- 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:
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

Tactic:
exact hy

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 * x * a * y = y * (x * a) * y

Tactic:
rw [mul_assoc y x a]

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
b a : A
⊢ (fun x_1 => x * x_1) a * b ∈ Set.range fun x_1 => x * x_1

Tactic:
exact ⟨a * b, by dsimp; rw [← mul_assoc, ← hx1, 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
b a : A
⊢ (fun x_1 => x * x_1) (a * b) = (fun x_1 => x * x_1) a * b

Tactic:
dsimp

Result:
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 a : A
⊢ x * (a * b) = x * a * b

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
⊢ (fun x_1 => x * x_1) (a * c) = a * (fun x_1 => x * x_1) c

Tactic:
dsimp

Result:
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)

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 : ∃ y, x * y = 1
⊢ ∃ b, ⟨x, hx1✝⟩ * b = 1

Tactic:
obtain ⟨y, hy⟩ := mem

Result:
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
⊢ ∃ 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 ∈ I

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

Result:
no goals

Proof state:
A : Type u_1
inst✝¹ : Ring A
inst✝ : IsSimpleRing A
⊢ ∀ {a : ↥(Subring.center A)}, a ≠ 0 → ∃ b, a * b = 1

Tactic:
rintro ⟨x, hx1⟩ hx2

Result:
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

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}, (x_1 ∈ Set.range fun x_2 => x * x_2) → x_1 * y ∈ Set.range fun x_2 => x * x_2

Tactic:
rintro _ b ⟨a, 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
b a : A
⊢ (fun x_1 => x * x_1) a * b ∈ Set.range fun x_1 => x * x_1

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
⊢ ∃ b, ⟨x, hx1✝⟩ * b = 1

Tactic:
refine ⟨⟨y, Subring.mem_center_iff.2 fun a ↦ ?_⟩, by ext; exact hy⟩

Result:
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

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
b a : A
⊢ x * (a * b) = x * a * b

Tactic:
rw [← mul_assoc, ← hx1, 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

Tactic:
rw [hy, mul_one]

Result:
no goals

Proof state:
case intro.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 y : A
⊢ (fun x => x✝ * x) x + (fun x => x✝ * x) y ∈ Set.range fun x => x✝ * x

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

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
⊢ a * y = x * y * a * y

Tactic:
rw [hy, one_mul]

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
a c : A
⊢ a * (fun x_1 => x * x_1) c ∈ Set.range fun x_1 => x * x_1

Tactic:
exact ⟨a * c, by dsimp; rw [← mul_assoc, ← hx1, mul_assoc]⟩

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) ⋯ ⋯ ⋯ ⋯ ⋯
⊢ ∃ b, ⟨x, hx1✝⟩ * b = 1

Tactic:
have mem : 1 ∈ I := one_mem_of_ne_zero_mem I hx2 (by simpa [I, mem_mk'] using ⟨1, by simp⟩)

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 : 1 ∈ I
⊢ ∃ 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},
    (x_1 ∈ Set.range fun x_2 => x * x_2) → (y ∈ Set.range fun x_2 => x * x_2) → x_1 + y ∈ Set.range fun x_2 => x * x_2

Tactic:
rintro _ _ ⟨x, rfl⟩ ⟨y, rfl⟩

Result:
case intro.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 y : A
⊢ (fun x => x✝ * x) x + (fun x => x✝ * x) y ∈ Set.range fun x => x✝ * x

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
⊢ (fun x_1 => x * x_1) 0 = 0

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
⊢ ∀ {x_1 : A}, (x_1 ∈ Set.range fun x_2 => x * x_2) → -x_1 ∈ Set.range fun x_2 => x * x_2

Tactic:
rintro _ ⟨x, 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
x : A
⊢ -(fun x => x✝ * x) x ∈ Set.range fun x => x✝ * x

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 * (x * a) * y = y * (a * x) * y

Tactic:
rw [hx1]

Result:
no goals