[GOAL]
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e f g : A₁ ≃ₐ[R] A₂
h₁ : (fun f => f.toFun) f = (fun f => f.toFun) g
h₂ : (fun f => f.invFun) f = (fun f => f.invFun) g
⊢ f = g
[PROOFSTEP]
obtain ⟨⟨f, _⟩, _⟩ := f
[GOAL]
case mk.mk
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e g : A₁ ≃ₐ[R] A₂
f : A₁ → A₂
invFun✝ : A₂ → A₁
left_inv✝ : Function.LeftInverse invFun✝ f
right_inv✝ : Function.RightInverse invFun✝ f
map_mul'✝ :
  ∀ (x y : A₁),
    Equiv.toFun { toFun := f, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } (x * y) =
      Equiv.toFun { toFun := f, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } x *
        Equiv.toFun { toFun := f, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } y
map_add'✝ :
  ∀ (x y : A₁),
    Equiv.toFun { toFun := f, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } (x + y) =
      Equiv.toFun { toFun := f, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } x +
        Equiv.toFun { toFun := f, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } y
commutes'✝ :
  ∀ (r : R),
    Equiv.toFun { toFun := f, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }
        (↑(algebraMap R A₁) r) =
      ↑(algebraMap R A₂) r
h₁ :
  (fun f => f.toFun)
      { toEquiv := { toFun := f, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
        map_mul' := map_mul'✝, map_add' := map_add'✝, commutes' := commutes'✝ } =
    (fun f => f.toFun) g
h₂ :
  (fun f => f.invFun)
      { toEquiv := { toFun := f, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
        map_mul' := map_mul'✝, map_add' := map_add'✝, commutes' := commutes'✝ } =
    (fun f => f.invFun) g
⊢ { toEquiv := { toFun := f, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }, map_mul' := map_mul'✝,
      map_add' := map_add'✝, commutes' := commutes'✝ } =
    g
[PROOFSTEP]
obtain ⟨⟨g, _⟩, _⟩ := g
[GOAL]
case mk.mk.mk.mk
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
f : A₁ → A₂
invFun✝¹ : A₂ → A₁
left_inv✝¹ : Function.LeftInverse invFun✝¹ f
right_inv✝¹ : Function.RightInverse invFun✝¹ f
map_mul'✝¹ :
  ∀ (x y : A₁),
    Equiv.toFun { toFun := f, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } (x * y) =
      Equiv.toFun { toFun := f, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } x *
        Equiv.toFun { toFun := f, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } y
map_add'✝¹ :
  ∀ (x y : A₁),
    Equiv.toFun { toFun := f, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } (x + y) =
      Equiv.toFun { toFun := f, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } x +
        Equiv.toFun { toFun := f, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } y
commutes'✝¹ :
  ∀ (r : R),
    Equiv.toFun { toFun := f, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ }
        (↑(algebraMap R A₁) r) =
      ↑(algebraMap R A₂) r
g : A₁ → A₂
invFun✝ : A₂ → A₁
left_inv✝ : Function.LeftInverse invFun✝ g
right_inv✝ : Function.RightInverse invFun✝ g
map_mul'✝ :
  ∀ (x y : A₁),
    Equiv.toFun { toFun := g, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } (x * y) =
      Equiv.toFun { toFun := g, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } x *
        Equiv.toFun { toFun := g, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } y
map_add'✝ :
  ∀ (x y : A₁),
    Equiv.toFun { toFun := g, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } (x + y) =
      Equiv.toFun { toFun := g, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } x +
        Equiv.toFun { toFun := g, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } y
commutes'✝ :
  ∀ (r : R),
    Equiv.toFun { toFun := g, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }
        (↑(algebraMap R A₁) r) =
      ↑(algebraMap R A₂) r
h₁ :
  (fun f => f.toFun)
      { toEquiv := { toFun := f, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ },
        map_mul' := map_mul'✝¹, map_add' := map_add'✝¹, commutes' := commutes'✝¹ } =
    (fun f => f.toFun)
      { toEquiv := { toFun := g, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
        map_mul' := map_mul'✝, map_add' := map_add'✝, commutes' := commutes'✝ }
h₂ :
  (fun f => f.invFun)
      { toEquiv := { toFun := f, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ },
        map_mul' := map_mul'✝¹, map_add' := map_add'✝¹, commutes' := commutes'✝¹ } =
    (fun f => f.invFun)
      { toEquiv := { toFun := g, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
        map_mul' := map_mul'✝, map_add' := map_add'✝, commutes' := commutes'✝ }
⊢ { toEquiv := { toFun := f, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ },
      map_mul' := map_mul'✝¹, map_add' := map_add'✝¹, commutes' := commutes'✝¹ } =
    { toEquiv := { toFun := g, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
      map_mul' := map_mul'✝, map_add' := map_add'✝, commutes' := commutes'✝ }
[PROOFSTEP]
congr
[GOAL]
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e f g : A₁ ≃ₐ[R] A₂
h₁ : (fun f => f.toFun) f = (fun f => f.toFun) g
h₂ : (fun f => f.invFun) f = (fun f => f.invFun) g
⊢ f = g
[PROOFSTEP]
obtain ⟨⟨f, _⟩, _⟩ := f
[GOAL]
case mk.mk
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e g : A₁ ≃ₐ[R] A₂
f : A₁ → A₂
invFun✝ : A₂ → A₁
left_inv✝ : Function.LeftInverse invFun✝ f
right_inv✝ : Function.RightInverse invFun✝ f
map_mul'✝ :
  ∀ (x y : A₁),
    Equiv.toFun { toFun := f, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } (x * y) =
      Equiv.toFun { toFun := f, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } x *
        Equiv.toFun { toFun := f, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } y
map_add'✝ :
  ∀ (x y : A₁),
    Equiv.toFun { toFun := f, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } (x + y) =
      Equiv.toFun { toFun := f, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } x +
        Equiv.toFun { toFun := f, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } y
commutes'✝ :
  ∀ (r : R),
    Equiv.toFun { toFun := f, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }
        (↑(algebraMap R A₁) r) =
      ↑(algebraMap R A₂) r
h₁ :
  (fun f => f.toFun)
      { toEquiv := { toFun := f, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
        map_mul' := map_mul'✝, map_add' := map_add'✝, commutes' := commutes'✝ } =
    (fun f => f.toFun) g
h₂ :
  (fun f => f.invFun)
      { toEquiv := { toFun := f, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
        map_mul' := map_mul'✝, map_add' := map_add'✝, commutes' := commutes'✝ } =
    (fun f => f.invFun) g
⊢ { toEquiv := { toFun := f, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }, map_mul' := map_mul'✝,
      map_add' := map_add'✝, commutes' := commutes'✝ } =
    g
[PROOFSTEP]
obtain ⟨⟨g, _⟩, _⟩ := g
[GOAL]
case mk.mk.mk.mk
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
f : A₁ → A₂
invFun✝¹ : A₂ → A₁
left_inv✝¹ : Function.LeftInverse invFun✝¹ f
right_inv✝¹ : Function.RightInverse invFun✝¹ f
map_mul'✝¹ :
  ∀ (x y : A₁),
    Equiv.toFun { toFun := f, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } (x * y) =
      Equiv.toFun { toFun := f, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } x *
        Equiv.toFun { toFun := f, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } y
map_add'✝¹ :
  ∀ (x y : A₁),
    Equiv.toFun { toFun := f, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } (x + y) =
      Equiv.toFun { toFun := f, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } x +
        Equiv.toFun { toFun := f, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } y
commutes'✝¹ :
  ∀ (r : R),
    Equiv.toFun { toFun := f, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ }
        (↑(algebraMap R A₁) r) =
      ↑(algebraMap R A₂) r
g : A₁ → A₂
invFun✝ : A₂ → A₁
left_inv✝ : Function.LeftInverse invFun✝ g
right_inv✝ : Function.RightInverse invFun✝ g
map_mul'✝ :
  ∀ (x y : A₁),
    Equiv.toFun { toFun := g, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } (x * y) =
      Equiv.toFun { toFun := g, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } x *
        Equiv.toFun { toFun := g, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } y
map_add'✝ :
  ∀ (x y : A₁),
    Equiv.toFun { toFun := g, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } (x + y) =
      Equiv.toFun { toFun := g, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } x +
        Equiv.toFun { toFun := g, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } y
commutes'✝ :
  ∀ (r : R),
    Equiv.toFun { toFun := g, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }
        (↑(algebraMap R A₁) r) =
      ↑(algebraMap R A₂) r
h₁ :
  (fun f => f.toFun)
      { toEquiv := { toFun := f, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ },
        map_mul' := map_mul'✝¹, map_add' := map_add'✝¹, commutes' := commutes'✝¹ } =
    (fun f => f.toFun)
      { toEquiv := { toFun := g, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
        map_mul' := map_mul'✝, map_add' := map_add'✝, commutes' := commutes'✝ }
h₂ :
  (fun f => f.invFun)
      { toEquiv := { toFun := f, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ },
        map_mul' := map_mul'✝¹, map_add' := map_add'✝¹, commutes' := commutes'✝¹ } =
    (fun f => f.invFun)
      { toEquiv := { toFun := g, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
        map_mul' := map_mul'✝, map_add' := map_add'✝, commutes' := commutes'✝ }
⊢ { toEquiv := { toFun := f, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ },
      map_mul' := map_mul'✝¹, map_add' := map_add'✝¹, commutes' := commutes'✝¹ } =
    { toEquiv := { toFun := g, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
      map_mul' := map_mul'✝, map_add' := map_add'✝, commutes' := commutes'✝ }
[PROOFSTEP]
congr
  -- Porting note: the default simps projection was `e.toEquiv.toFun`, it should be `FunLike.coe`
[GOAL]
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
r : R
x : A₁
⊢ ↑e (r • x) = r • ↑e x
[PROOFSTEP]
simp only [Algebra.smul_def, map_mul, commutes]
[GOAL]
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e✝ e : A₁ ≃ₐ[R] A₂
src✝ : A₂ ≃+* A₁ := RingEquiv.symm (toRingEquiv e)
r : R
⊢ Equiv.toFun src✝.toEquiv (↑(algebraMap R A₂) r) = ↑(algebraMap R A₁) r
[PROOFSTEP]
rw [← e.toRingEquiv.symm_apply_apply (algebraMap R A₁ r)]
[GOAL]
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e✝ e : A₁ ≃ₐ[R] A₂
src✝ : A₂ ≃+* A₁ := RingEquiv.symm (toRingEquiv e)
r : R
⊢ Equiv.toFun src✝.toEquiv (↑(algebraMap R A₂) r) =
    ↑(RingEquiv.symm (toRingEquiv e)) (↑(toRingEquiv e) (↑(algebraMap R A₁) r))
[PROOFSTEP]
congr
[GOAL]
case e_a
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e✝ e : A₁ ≃ₐ[R] A₂
src✝ : A₂ ≃+* A₁ := RingEquiv.symm (toRingEquiv e)
r : R
⊢ ↑(algebraMap R A₂) r = ↑(toRingEquiv e) (↑(algebraMap R A₁) r)
[PROOFSTEP]
change _ = e _
[GOAL]
case e_a
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e✝ e : A₁ ≃ₐ[R] A₂
src✝ : A₂ ≃+* A₁ := RingEquiv.symm (toRingEquiv e)
r : R
⊢ ↑(algebraMap R A₂) r = ↑e (↑(algebraMap R A₁) r)
[PROOFSTEP]
rw [e.commutes]
[GOAL]
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e✝ e : A₁ ≃ₐ[R] A₂
⊢ symm (symm e) = e
[PROOFSTEP]
ext
[GOAL]
case h
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e✝ e : A₁ ≃ₐ[R] A₂
a✝ : A₁
⊢ ↑(symm (symm e)) a✝ = ↑e a✝
[PROOFSTEP]
rfl
[GOAL]
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e e₁ : A₁ ≃ₐ[R] A₂
e₂ : A₂ ≃ₐ[R] A₃
src✝ : A₁ ≃+* A₃ := RingEquiv.trans (toRingEquiv e₁) (toRingEquiv e₂)
r : R
⊢ Equiv.toFun e₂.toEquiv (Equiv.toFun e₁.toEquiv (↑(algebraMap R A₁) r)) = ↑(algebraMap R A₃) r
[PROOFSTEP]
rw [e₁.commutes', e₂.commutes']
[GOAL]
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e✝ e : A₁ ≃ₐ[R] A₂
⊢ AlgHom.comp ↑e ↑(symm e) = AlgHom.id R A₂
[PROOFSTEP]
ext
[GOAL]
case H
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e✝ e : A₁ ≃ₐ[R] A₂
x✝ : A₂
⊢ ↑(AlgHom.comp ↑e ↑(symm e)) x✝ = ↑(AlgHom.id R A₂) x✝
[PROOFSTEP]
simp
[GOAL]
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e✝ e : A₁ ≃ₐ[R] A₂
⊢ AlgHom.comp ↑(symm e) ↑e = AlgHom.id R A₁
[PROOFSTEP]
ext
[GOAL]
case H
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e✝ e : A₁ ≃ₐ[R] A₂
x✝ : A₁
⊢ ↑(AlgHom.comp ↑(symm e) ↑e) x✝ = ↑(AlgHom.id R A₁) x✝
[PROOFSTEP]
simp
[GOAL]
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
e₁ : A₁ ≃ₐ[R] A₁'
e₂ : A₂ ≃ₐ[R] A₂'
f : A₁ →ₐ[R] A₂
⊢ (fun f => AlgHom.comp (AlgHom.comp (↑(symm e₂)) f) ↑e₁) ((fun f => AlgHom.comp (AlgHom.comp (↑e₂) f) ↑(symm e₁)) f) =
    f
[PROOFSTEP]
simp only [AlgHom.comp_assoc, toAlgHom_eq_coe, symm_comp]
[GOAL]
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
e₁ : A₁ ≃ₐ[R] A₁'
e₂ : A₂ ≃ₐ[R] A₂'
f : A₁ →ₐ[R] A₂
⊢ AlgHom.comp (↑(symm e₂)) (AlgHom.comp (↑e₂) (AlgHom.comp f (AlgHom.id R A₁))) = f
[PROOFSTEP]
simp only [← AlgHom.comp_assoc, symm_comp, AlgHom.id_comp, AlgHom.comp_id]
[GOAL]
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
e₁ : A₁ ≃ₐ[R] A₁'
e₂ : A₂ ≃ₐ[R] A₂'
f : A₁' →ₐ[R] A₂'
⊢ (fun f => AlgHom.comp (AlgHom.comp (↑e₂) f) ↑(symm e₁)) ((fun f => AlgHom.comp (AlgHom.comp (↑(symm e₂)) f) ↑e₁) f) =
    f
[PROOFSTEP]
simp only [AlgHom.comp_assoc, toAlgHom_eq_coe, comp_symm]
[GOAL]
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
e₁ : A₁ ≃ₐ[R] A₁'
e₂ : A₂ ≃ₐ[R] A₂'
f : A₁' →ₐ[R] A₂'
⊢ AlgHom.comp (↑e₂) (AlgHom.comp (↑(symm e₂)) (AlgHom.comp f (AlgHom.id R A₁'))) = f
[PROOFSTEP]
simp only [← AlgHom.comp_assoc, comp_symm, AlgHom.id_comp, AlgHom.comp_id]
[GOAL]
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
e₁ : A₁ ≃ₐ[R] A₁'
e₂ : A₂ ≃ₐ[R] A₂'
e₃ : A₃ ≃ₐ[R] A₃'
f : A₁ →ₐ[R] A₂
g : A₂ →ₐ[R] A₃
⊢ ↑(arrowCongr e₁ e₃) (AlgHom.comp g f) = AlgHom.comp (↑(arrowCongr e₂ e₃) g) (↑(arrowCongr e₁ e₂) f)
[PROOFSTEP]
ext
[GOAL]
case H
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
e₁ : A₁ ≃ₐ[R] A₁'
e₂ : A₂ ≃ₐ[R] A₂'
e₃ : A₃ ≃ₐ[R] A₃'
f : A₁ →ₐ[R] A₂
g : A₂ →ₐ[R] A₃
x✝ : A₁'
⊢ ↑(↑(arrowCongr e₁ e₃) (AlgHom.comp g f)) x✝ = ↑(AlgHom.comp (↑(arrowCongr e₂ e₃) g) (↑(arrowCongr e₁ e₂) f)) x✝
[PROOFSTEP]
simp only [arrowCongr, Equiv.coe_fn_mk, AlgHom.comp_apply]
[GOAL]
case H
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
e₁ : A₁ ≃ₐ[R] A₁'
e₂ : A₂ ≃ₐ[R] A₂'
e₃ : A₃ ≃ₐ[R] A₃'
f : A₁ →ₐ[R] A₂
g : A₂ →ₐ[R] A₃
x✝ : A₁'
⊢ ↑↑e₃ (↑g (↑f (↑↑(symm e₁) x✝))) = ↑↑e₃ (↑g (↑↑(symm e₂) (↑↑e₂ (↑f (↑↑(symm e₁) x✝)))))
[PROOFSTEP]
congr
[GOAL]
case H.h.e_6.h.h.e_6.h
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
e₁ : A₁ ≃ₐ[R] A₁'
e₂ : A₂ ≃ₐ[R] A₂'
e₃ : A₃ ≃ₐ[R] A₃'
f : A₁ →ₐ[R] A₂
g : A₂ →ₐ[R] A₃
x✝ : A₁'
⊢ ↑f (↑↑(symm e₁) x✝) = ↑↑(symm e₂) (↑↑e₂ (↑f (↑↑(symm e₁) x✝)))
[PROOFSTEP]
exact (e₂.symm_apply_apply _).symm
[GOAL]
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
⊢ arrowCongr refl refl = Equiv.refl (A₁ →ₐ[R] A₂)
[PROOFSTEP]
ext
[GOAL]
case H.H
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
x✝¹ : A₁ →ₐ[R] A₂
x✝ : A₁
⊢ ↑(↑(arrowCongr refl refl) x✝¹) x✝ = ↑(↑(Equiv.refl (A₁ →ₐ[R] A₂)) x✝¹) x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e e₁ : A₁ ≃ₐ[R] A₂
e₁' : A₁' ≃ₐ[R] A₂'
e₂ : A₂ ≃ₐ[R] A₃
e₂' : A₂' ≃ₐ[R] A₃'
⊢ arrowCongr (trans e₁ e₂) (trans e₁' e₂') = (arrowCongr e₁ e₁').trans (arrowCongr e₂ e₂')
[PROOFSTEP]
ext
[GOAL]
case H.H
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e e₁ : A₁ ≃ₐ[R] A₂
e₁' : A₁' ≃ₐ[R] A₂'
e₂ : A₂ ≃ₐ[R] A₃
e₂' : A₂' ≃ₐ[R] A₃'
x✝¹ : A₁ →ₐ[R] A₁'
x✝ : A₃
⊢ ↑(↑(arrowCongr (trans e₁ e₂) (trans e₁' e₂')) x✝¹) x✝ = ↑(↑((arrowCongr e₁ e₁').trans (arrowCongr e₂ e₂')) x✝¹) x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
e₁ : A₁ ≃ₐ[R] A₁'
e₂ : A₂ ≃ₐ[R] A₂'
⊢ (arrowCongr e₁ e₂).symm = arrowCongr (symm e₁) (symm e₂)
[PROOFSTEP]
ext
[GOAL]
case H.H
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
e₁ : A₁ ≃ₐ[R] A₁'
e₂ : A₂ ≃ₐ[R] A₂'
x✝¹ : A₁' →ₐ[R] A₂'
x✝ : A₁
⊢ ↑(↑(arrowCongr e₁ e₂).symm x✝¹) x✝ = ↑(↑(arrowCongr (symm e₁) (symm e₂)) x✝¹) x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e✝ e : A₁ ≃ₐ[R] A₂
e' : A₁' ≃ₐ[R] A₂'
ψ : A₁ ≃ₐ[R] A₁'
⊢ (fun ψ => trans e (trans ψ (symm e'))) ((fun ψ => trans (symm e) (trans ψ e')) ψ) = ψ
[PROOFSTEP]
ext
[GOAL]
case h
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e✝ e : A₁ ≃ₐ[R] A₂
e' : A₁' ≃ₐ[R] A₂'
ψ : A₁ ≃ₐ[R] A₁'
a✝ : A₁
⊢ ↑((fun ψ => trans e (trans ψ (symm e'))) ((fun ψ => trans (symm e) (trans ψ e')) ψ)) a✝ = ↑ψ a✝
[PROOFSTEP]
simp_rw [trans_apply, symm_apply_apply]
[GOAL]
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e✝ e : A₁ ≃ₐ[R] A₂
e' : A₁' ≃ₐ[R] A₂'
ψ : A₂ ≃ₐ[R] A₂'
⊢ (fun ψ => trans (symm e) (trans ψ e')) ((fun ψ => trans e (trans ψ (symm e'))) ψ) = ψ
[PROOFSTEP]
ext
[GOAL]
case h
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e✝ e : A₁ ≃ₐ[R] A₂
e' : A₁' ≃ₐ[R] A₂'
ψ : A₂ ≃ₐ[R] A₂'
a✝ : A₂
⊢ ↑((fun ψ => trans (symm e) (trans ψ e')) ((fun ψ => trans e (trans ψ (symm e'))) ψ)) a✝ = ↑ψ a✝
[PROOFSTEP]
simp_rw [trans_apply, apply_symm_apply]
[GOAL]
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
⊢ equivCongr refl refl = Equiv.refl (A₁ ≃ₐ[R] A₁')
[PROOFSTEP]
ext
[GOAL]
case H.h
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
x✝ : A₁ ≃ₐ[R] A₁'
a✝ : A₁
⊢ ↑(↑(equivCongr refl refl) x✝) a✝ = ↑(↑(Equiv.refl (A₁ ≃ₐ[R] A₁')) x✝) a✝
[PROOFSTEP]
rfl
[GOAL]
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
l : A₁ ≃ₗ[R] A₂
map_mul✝ : ∀ (x y : A₁), ↑l (x * y) = ↑l x * ↑l y
commutes✝ : ∀ (r : R), ↑l (↑(algebraMap R A₁) r) = ↑(algebraMap R A₂) r
map_mul : ∀ (x y : A₁), ↑(toLinearEquiv e) (x * y) = ↑(toLinearEquiv e) x * ↑(toLinearEquiv e) y
commutes : ∀ (r : R), ↑(toLinearEquiv e) (↑(algebraMap R A₁) r) = ↑(algebraMap R A₂) r
⊢ ofLinearEquiv (toLinearEquiv e) map_mul commutes = e
[PROOFSTEP]
ext
[GOAL]
case h
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
l : A₁ ≃ₗ[R] A₂
map_mul✝ : ∀ (x y : A₁), ↑l (x * y) = ↑l x * ↑l y
commutes✝ : ∀ (r : R), ↑l (↑(algebraMap R A₁) r) = ↑(algebraMap R A₂) r
map_mul : ∀ (x y : A₁), ↑(toLinearEquiv e) (x * y) = ↑(toLinearEquiv e) x * ↑(toLinearEquiv e) y
commutes : ∀ (r : R), ↑(toLinearEquiv e) (↑(algebraMap R A₁) r) = ↑(algebraMap R A₂) r
a✝ : A₁
⊢ ↑(ofLinearEquiv (toLinearEquiv e) map_mul commutes) a✝ = ↑e a✝
[PROOFSTEP]
rfl
[GOAL]
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
l : A₁ ≃ₗ[R] A₂
map_mul : ∀ (x y : A₁), ↑l (x * y) = ↑l x * ↑l y
commutes : ∀ (r : R), ↑l (↑(algebraMap R A₁) r) = ↑(algebraMap R A₂) r
⊢ toLinearEquiv (ofLinearEquiv l map_mul commutes) = l
[PROOFSTEP]
ext
[GOAL]
case h
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
l : A₁ ≃ₗ[R] A₂
map_mul : ∀ (x y : A₁), ↑l (x * y) = ↑l x * ↑l y
commutes : ∀ (r : R), ↑l (↑(algebraMap R A₁) r) = ↑(algebraMap R A₂) r
x✝ : A₁
⊢ ↑(toLinearEquiv (ofLinearEquiv l map_mul commutes)) x✝ = ↑l x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e ϕ : A₁ ≃ₐ[R] A₂
src✝ : (A₁ ≃ₐ[R] A₁) ≃ A₂ ≃ₐ[R] A₂ := equivCongr ϕ ϕ
ψ χ : A₁ ≃ₐ[R] A₁
⊢ Equiv.toFun
      { toFun := fun ψ => trans (symm ϕ) (trans ψ ϕ), invFun := fun ψ => trans ϕ (trans ψ (symm ϕ)),
        left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
        right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
      (ψ * χ) =
    Equiv.toFun
        { toFun := fun ψ => trans (symm ϕ) (trans ψ ϕ), invFun := fun ψ => trans ϕ (trans ψ (symm ϕ)),
          left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
          right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        ψ *
      Equiv.toFun
        { toFun := fun ψ => trans (symm ϕ) (trans ψ ϕ), invFun := fun ψ => trans ϕ (trans ψ (symm ϕ)),
          left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
          right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        χ
[PROOFSTEP]
ext
[GOAL]
case h
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e ϕ : A₁ ≃ₐ[R] A₂
src✝ : (A₁ ≃ₐ[R] A₁) ≃ A₂ ≃ₐ[R] A₂ := equivCongr ϕ ϕ
ψ χ : A₁ ≃ₐ[R] A₁
a✝ : A₂
⊢ ↑(Equiv.toFun
          { toFun := fun ψ => trans (symm ϕ) (trans ψ ϕ), invFun := fun ψ => trans ϕ (trans ψ (symm ϕ)),
            left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
          (ψ * χ))
      a✝ =
    ↑(Equiv.toFun
            { toFun := fun ψ => trans (symm ϕ) (trans ψ ϕ), invFun := fun ψ => trans ϕ (trans ψ (symm ϕ)),
              left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
              right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
            ψ *
          Equiv.toFun
            { toFun := fun ψ => trans (symm ϕ) (trans ψ ϕ), invFun := fun ψ => trans ϕ (trans ψ (symm ϕ)),
              left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
              right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
            χ)
      a✝
[PROOFSTEP]
simp only [mul_apply, trans_apply, symm_apply_apply]
[GOAL]
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
⊢ autCongr refl = MulEquiv.refl (A₁ ≃ₐ[R] A₁)
[PROOFSTEP]
ext
[GOAL]
case h.h
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
x✝ : A₁ ≃ₐ[R] A₁
a✝ : A₁
⊢ ↑(↑(autCongr refl) x✝) a✝ = ↑(↑(MulEquiv.refl (A₁ ≃ₐ[R] A₁)) x✝) a✝
[PROOFSTEP]
rfl
[GOAL]
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e✝ e : A₁ ≃ₐ[R] A₂
y : R
x : A₁
h : ↑(algebraMap R A₂) y = ↑e x
⊢ ↑(algebraMap R A₁) y = x
[PROOFSTEP]
simpa using e.symm.toAlgHom.algebraMap_eq_apply h
