[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
S' : Type u_6
inst✝⁵ : Mul R
inst✝⁴ : Mul S
inst✝³ : Add R
inst✝² : Add S
inst✝¹ : Mul S'
inst✝ : Add S'
e f : R ≃+* S
h₁ : (fun f => f.toFun) e = (fun f => f.toFun) f
h₂ : (fun f => f.invFun) e = (fun f => f.invFun) f
⊢ e = f
[PROOFSTEP]
cases e
[GOAL]
case mk
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
S' : Type u_6
inst✝⁵ : Mul R
inst✝⁴ : Mul S
inst✝³ : Add R
inst✝² : Add S
inst✝¹ : Mul S'
inst✝ : Add S'
f : R ≃+* S
toEquiv✝ : R ≃ S
map_mul'✝ : ∀ (x y : R), Equiv.toFun toEquiv✝ (x * y) = Equiv.toFun toEquiv✝ x * Equiv.toFun toEquiv✝ y
map_add'✝ : ∀ (x y : R), Equiv.toFun toEquiv✝ (x + y) = Equiv.toFun toEquiv✝ x + Equiv.toFun toEquiv✝ y
h₁ : (fun f => f.toFun) { toEquiv := toEquiv✝, map_mul' := map_mul'✝, map_add' := map_add'✝ } = (fun f => f.toFun) f
h₂ : (fun f => f.invFun) { toEquiv := toEquiv✝, map_mul' := map_mul'✝, map_add' := map_add'✝ } = (fun f => f.invFun) f
⊢ { toEquiv := toEquiv✝, map_mul' := map_mul'✝, map_add' := map_add'✝ } = f
[PROOFSTEP]
cases f
[GOAL]
case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
S' : Type u_6
inst✝⁵ : Mul R
inst✝⁴ : Mul S
inst✝³ : Add R
inst✝² : Add S
inst✝¹ : Mul S'
inst✝ : Add S'
toEquiv✝¹ : R ≃ S
map_mul'✝¹ : ∀ (x y : R), Equiv.toFun toEquiv✝¹ (x * y) = Equiv.toFun toEquiv✝¹ x * Equiv.toFun toEquiv✝¹ y
map_add'✝¹ : ∀ (x y : R), Equiv.toFun toEquiv✝¹ (x + y) = Equiv.toFun toEquiv✝¹ x + Equiv.toFun toEquiv✝¹ y
toEquiv✝ : R ≃ S
map_mul'✝ : ∀ (x y : R), Equiv.toFun toEquiv✝ (x * y) = Equiv.toFun toEquiv✝ x * Equiv.toFun toEquiv✝ y
map_add'✝ : ∀ (x y : R), Equiv.toFun toEquiv✝ (x + y) = Equiv.toFun toEquiv✝ x + Equiv.toFun toEquiv✝ y
h₁ :
  (fun f => f.toFun) { toEquiv := toEquiv✝¹, map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ } =
    (fun f => f.toFun) { toEquiv := toEquiv✝, map_mul' := map_mul'✝, map_add' := map_add'✝ }
h₂ :
  (fun f => f.invFun) { toEquiv := toEquiv✝¹, map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ } =
    (fun f => f.invFun) { toEquiv := toEquiv✝, map_mul' := map_mul'✝, map_add' := map_add'✝ }
⊢ { toEquiv := toEquiv✝¹, map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ } =
    { toEquiv := toEquiv✝, map_mul' := map_mul'✝, map_add' := map_add'✝ }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_toEquiv
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
S' : Type u_6
inst✝⁵ : Mul R
inst✝⁴ : Mul S
inst✝³ : Add R
inst✝² : Add S
inst✝¹ : Mul S'
inst✝ : Add S'
toEquiv✝¹ : R ≃ S
map_mul'✝¹ : ∀ (x y : R), Equiv.toFun toEquiv✝¹ (x * y) = Equiv.toFun toEquiv✝¹ x * Equiv.toFun toEquiv✝¹ y
map_add'✝¹ : ∀ (x y : R), Equiv.toFun toEquiv✝¹ (x + y) = Equiv.toFun toEquiv✝¹ x + Equiv.toFun toEquiv✝¹ y
toEquiv✝ : R ≃ S
map_mul'✝ : ∀ (x y : R), Equiv.toFun toEquiv✝ (x * y) = Equiv.toFun toEquiv✝ x * Equiv.toFun toEquiv✝ y
map_add'✝ : ∀ (x y : R), Equiv.toFun toEquiv✝ (x + y) = Equiv.toFun toEquiv✝ x + Equiv.toFun toEquiv✝ y
h₁ :
  (fun f => f.toFun) { toEquiv := toEquiv✝¹, map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ } =
    (fun f => f.toFun) { toEquiv := toEquiv✝, map_mul' := map_mul'✝, map_add' := map_add'✝ }
h₂ :
  (fun f => f.invFun) { toEquiv := toEquiv✝¹, map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ } =
    (fun f => f.invFun) { toEquiv := toEquiv✝, map_mul' := map_mul'✝, map_add' := map_add'✝ }
⊢ toEquiv✝¹ = toEquiv✝
[PROOFSTEP]
apply Equiv.coe_fn_injective h₁
[GOAL]
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
R : Type u_4
S : Type u_5
S' : Type u_6
α : Type ?u.47054
β : Type ?u.47060
inst✝³ : Add α
inst✝² : Mul α
inst✝¹ : Add β
inst✝ : Mul β
f : α ≃+* β
⊢ (fun f =>
        let src := ↑AddEquiv.mulOp.symm (toAddEquiv f);
        let src_1 := ↑MulEquiv.op.symm (toMulEquiv f);
        { toEquiv := src.toEquiv,
          map_mul' :=
            (_ :
              ∀ (x y : α),
                Equiv.toFun src_1.toEquiv (x * y) = Equiv.toFun src_1.toEquiv x * Equiv.toFun src_1.toEquiv y),
          map_add' :=
            (_ :
              ∀ (x y : α), Equiv.toFun src.toEquiv (x + y) = Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y) })
      ((fun f =>
          let src := ↑AddEquiv.mulOp (toAddEquiv f);
          let src_1 := ↑MulEquiv.op (toMulEquiv f);
          { toEquiv := src.toEquiv,
            map_mul' :=
              (_ :
                ∀ (x y : αᵐᵒᵖ),
                  Equiv.toFun src_1.toEquiv (x * y) = Equiv.toFun src_1.toEquiv x * Equiv.toFun src_1.toEquiv y),
            map_add' :=
              (_ :
                ∀ (x y : αᵐᵒᵖ),
                  Equiv.toFun src.toEquiv (x + y) = Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y) })
        f) =
    f
[PROOFSTEP]
ext
[GOAL]
case h
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
R : Type u_4
S : Type u_5
S' : Type u_6
α : Type ?u.47054
β : Type ?u.47060
inst✝³ : Add α
inst✝² : Mul α
inst✝¹ : Add β
inst✝ : Mul β
f : α ≃+* β
x✝ : α
⊢ ↑((fun f =>
            let src := ↑AddEquiv.mulOp.symm (toAddEquiv f);
            let src_1 := ↑MulEquiv.op.symm (toMulEquiv f);
            { toEquiv := src.toEquiv,
              map_mul' :=
                (_ :
                  ∀ (x y : α),
                    Equiv.toFun src_1.toEquiv (x * y) = Equiv.toFun src_1.toEquiv x * Equiv.toFun src_1.toEquiv y),
              map_add' :=
                (_ :
                  ∀ (x y : α),
                    Equiv.toFun src.toEquiv (x + y) = Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y) })
          ((fun f =>
              let src := ↑AddEquiv.mulOp (toAddEquiv f);
              let src_1 := ↑MulEquiv.op (toMulEquiv f);
              { toEquiv := src.toEquiv,
                map_mul' :=
                  (_ :
                    ∀ (x y : αᵐᵒᵖ),
                      Equiv.toFun src_1.toEquiv (x * y) = Equiv.toFun src_1.toEquiv x * Equiv.toFun src_1.toEquiv y),
                map_add' :=
                  (_ :
                    ∀ (x y : αᵐᵒᵖ),
                      Equiv.toFun src.toEquiv (x + y) = Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y) })
            f))
      x✝ =
    ↑f x✝
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
R : Type u_4
S : Type u_5
S' : Type u_6
α : Type ?u.47054
β : Type ?u.47060
inst✝³ : Add α
inst✝² : Mul α
inst✝¹ : Add β
inst✝ : Mul β
f : αᵐᵒᵖ ≃+* βᵐᵒᵖ
⊢ (fun f =>
        let src := ↑AddEquiv.mulOp (toAddEquiv f);
        let src_1 := ↑MulEquiv.op (toMulEquiv f);
        { toEquiv := src.toEquiv,
          map_mul' :=
            (_ :
              ∀ (x y : αᵐᵒᵖ),
                Equiv.toFun src_1.toEquiv (x * y) = Equiv.toFun src_1.toEquiv x * Equiv.toFun src_1.toEquiv y),
          map_add' :=
            (_ :
              ∀ (x y : αᵐᵒᵖ),
                Equiv.toFun src.toEquiv (x + y) = Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y) })
      ((fun f =>
          let src := ↑AddEquiv.mulOp.symm (toAddEquiv f);
          let src_1 := ↑MulEquiv.op.symm (toMulEquiv f);
          { toEquiv := src.toEquiv,
            map_mul' :=
              (_ :
                ∀ (x y : α),
                  Equiv.toFun src_1.toEquiv (x * y) = Equiv.toFun src_1.toEquiv x * Equiv.toFun src_1.toEquiv y),
            map_add' :=
              (_ :
                ∀ (x y : α), Equiv.toFun src.toEquiv (x + y) = Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y) })
        f) =
    f
[PROOFSTEP]
ext
[GOAL]
case h
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
R : Type u_4
S : Type u_5
S' : Type u_6
α : Type ?u.47054
β : Type ?u.47060
inst✝³ : Add α
inst✝² : Mul α
inst✝¹ : Add β
inst✝ : Mul β
f : αᵐᵒᵖ ≃+* βᵐᵒᵖ
x✝ : αᵐᵒᵖ
⊢ ↑((fun f =>
            let src := ↑AddEquiv.mulOp (toAddEquiv f);
            let src_1 := ↑MulEquiv.op (toMulEquiv f);
            { toEquiv := src.toEquiv,
              map_mul' :=
                (_ :
                  ∀ (x y : αᵐᵒᵖ),
                    Equiv.toFun src_1.toEquiv (x * y) = Equiv.toFun src_1.toEquiv x * Equiv.toFun src_1.toEquiv y),
              map_add' :=
                (_ :
                  ∀ (x y : αᵐᵒᵖ),
                    Equiv.toFun src.toEquiv (x + y) = Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y) })
          ((fun f =>
              let src := ↑AddEquiv.mulOp.symm (toAddEquiv f);
              let src_1 := ↑MulEquiv.op.symm (toMulEquiv f);
              { toEquiv := src.toEquiv,
                map_mul' :=
                  (_ :
                    ∀ (x y : α),
                      Equiv.toFun src_1.toEquiv (x * y) = Equiv.toFun src_1.toEquiv x * Equiv.toFun src_1.toEquiv y),
                map_add' :=
                  (_ :
                    ∀ (x y : α),
                      Equiv.toFun src.toEquiv (x + y) = Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y) })
            f))
      x✝ =
    ↑f x✝
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
S' : Type u_6
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R ≃+* S
x✝ y x : R
⊢ ↑f x = -1 ↔ x = -1
[PROOFSTEP]
rw [← neg_eq_iff_eq_neg, ← neg_eq_iff_eq_neg, ← map_neg, RingEquiv.map_eq_one_iff]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R✝ : Type u_4
S✝ : Type u_5
S' : Type u_6
inst✝⁴ : NonUnitalNonAssocSemiring R✝
inst✝³ : NonUnitalNonAssocSemiring S✝
inst✝² : NonUnitalNonAssocSemiring S'
R : Type u_7
S : Type u_8
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f g : R ≃+* S
h : f = g
⊢ ↑f = ↑g
[PROOFSTEP]
rw [h]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
S' : Type u_6
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalNonAssocSemiring S'
e : R ≃+* S
⊢ NonUnitalRingHom.comp (toNonUnitalRingHom e) (toNonUnitalRingHom (RingEquiv.symm e)) = NonUnitalRingHom.id S
[PROOFSTEP]
ext
[GOAL]
case a
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
S' : Type u_6
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalNonAssocSemiring S'
e : R ≃+* S
x✝ : S
⊢ ↑(NonUnitalRingHom.comp (toNonUnitalRingHom e) (toNonUnitalRingHom (RingEquiv.symm e))) x✝ =
    ↑(NonUnitalRingHom.id S) x✝
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
S' : Type u_6
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalNonAssocSemiring S'
e : R ≃+* S
⊢ NonUnitalRingHom.comp (toNonUnitalRingHom (RingEquiv.symm e)) (toNonUnitalRingHom e) = NonUnitalRingHom.id R
[PROOFSTEP]
ext
[GOAL]
case a
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
S' : Type u_6
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalNonAssocSemiring S'
e : R ≃+* S
x✝ : R
⊢ ↑(NonUnitalRingHom.comp (toNonUnitalRingHom (RingEquiv.symm e)) (toNonUnitalRingHom e)) x✝ =
    ↑(NonUnitalRingHom.id R) x✝
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R✝ : Type u_4
S✝ : Type u_5
S' : Type u_6
inst✝⁴ : NonAssocSemiring R✝
inst✝³ : NonAssocSemiring S✝
inst✝² : NonAssocSemiring S'
R : Type u_7
S : Type u_8
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
f g : R ≃+* S
h : f = g
⊢ ↑f = ↑g
[PROOFSTEP]
rw [h]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
S' : Type u_6
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring S'
e : R ≃+* S
⊢ RingHom.comp (toRingHom e) (toRingHom (RingEquiv.symm e)) = RingHom.id S
[PROOFSTEP]
ext
[GOAL]
case a
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
S' : Type u_6
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring S'
e : R ≃+* S
x✝ : S
⊢ ↑(RingHom.comp (toRingHom e) (toRingHom (RingEquiv.symm e))) x✝ = ↑(RingHom.id S) x✝
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
S' : Type u_6
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring S'
e : R ≃+* S
⊢ RingHom.comp (toRingHom (RingEquiv.symm e)) (toRingHom e) = RingHom.id R
[PROOFSTEP]
ext
[GOAL]
case a
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
S' : Type u_6
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring S'
e : R ≃+* S
x✝ : R
⊢ ↑(RingHom.comp (toRingHom (RingEquiv.symm e)) (toRingHom e)) x✝ = ↑(RingHom.id R) x✝
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
S' : Type u_6
A : Type u_7
B : Type u_8
inst✝¹ : Semiring A
inst✝ : Semiring B
hB : IsField B
e : A ≃* B
x y : A
⊢ ↑e (x * y) = ↑e (y * x)
[PROOFSTEP]
rw [map_mul, map_mul, hB.mul_comm]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
S' : Type u_6
A : Type u_7
B : Type u_8
inst✝¹ : Semiring A
inst✝ : Semiring B
hB : IsField B
e : A ≃* B
a✝ : A
h : a✝ ≠ 0
⊢ ∃ b, a✝ * b = 1
[PROOFSTEP]
obtain ⟨a', he⟩ := hB.mul_inv_cancel ((e.injective.ne h).trans_eq <| map_zero e)
[GOAL]
case intro
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
S' : Type u_6
A : Type u_7
B : Type u_8
inst✝¹ : Semiring A
inst✝ : Semiring B
hB : IsField B
e : A ≃* B
a✝ : A
h : a✝ ≠ 0
a' : B
he : ↑e a✝ * a' = 1
⊢ ∃ b, a✝ * b = 1
[PROOFSTEP]
exact ⟨e.symm a', e.injective <| by rw [map_mul, map_one, e.apply_symm_apply, he]⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
S' : Type u_6
A : Type u_7
B : Type u_8
inst✝¹ : Semiring A
inst✝ : Semiring B
hB : IsField B
e : A ≃* B
a✝ : A
h : a✝ ≠ 0
a' : B
he : ↑e a✝ * a' = 1
⊢ ↑e (a✝ * ↑(symm e) a') = ↑e 1
[PROOFSTEP]
rw [map_mul, map_one, e.apply_symm_apply, he]
