awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Algebra R A₁
inst_4 : Algebra R A₂
⊢ Function.Bijective (α := A₁ ≃ₐ[R] A₂) symm

Tactic:
Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩

Premises used: Iff.mpr, Function.bijective_iff_has_inverse, And.intro, Exists.intro, AlgEquiv.symm_symm
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Algebra R A₁
inst_4 : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
f : A₂ → A₁
h₁ : Function.LeftInverse (⇑e : (a : A₁) → A₂) f
h₂ : Function.RightInverse (⇑e : (a : A₁) → A₂) f
h₃ :
  ∀ (x y : A₂),
    { toFun := f, invFun := (⇑e : (a : A₁) → A₂), left_inv := h₁, right_inv := h₂ : A₂ ≃ A₁ }.toFun (x * y) =
      { toFun := f, invFun := (⇑e : (a : A₁) → A₂), left_inv := h₁, right_inv := h₂ : A₂ ≃ A₁ }.toFun x *
        { toFun := f, invFun := (⇑e : (a : A₁) → A₂), left_inv := h₁, right_inv := h₂ : A₂ ≃ A₁ }.toFun y
h₄ :
  ∀ (x y : A₂),
    { toFun := f, invFun := (⇑e : (a : A₁) → A₂), left_inv := h₁, right_inv := h₂ : A₂ ≃ A₁ }.toFun (x + y) =
      { toFun := f, invFun := (⇑e : (a : A₁) → A₂), left_inv := h₁, right_inv := h₂ : A₂ ≃ A₁ }.toFun x +
        { toFun := f, invFun := (⇑e : (a : A₁) → A₂), left_inv := h₁, right_inv := h₂ : A₂ ≃ A₁ }.toFun y
h₅ :
  ∀ (r : R),
    { toFun := f, invFun := (⇑e : (a : A₁) → A₂), left_inv := h₁, right_inv := h₂ : A₂ ≃ A₁ }.toFun
        ((algebraMap R A₂ : (a : R) → A₂) r) =
      (algebraMap R A₁ : (a : R) → A₁) r
⊢ { toFun := f, invFun := (⇑e : (a : A₁) → A₂), left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄,
      commutes' := h₅ : A₂ ≃ₐ[R] A₁ } =
    e.symm

Tactic:
symm_bijective.injective <| ext fun _ => rfl

Premises used: Function.Bijective.injective, AlgEquiv.ext, AlgEquiv.symm_bijective, rfl
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Algebra R A₁
inst_4 : Algebra R A₂
e : A₁ ≃ A₂
h₁ : ∀ (x y : A₁), e.toFun (x * y) = e.toFun x * e.toFun y
h₂ : ∀ (x y : A₁), e.toFun (x + y) = e.toFun x + e.toFun y
h₃ : ∀ (r : R), e.toFun ((algebraMap R A₁ : (a : R) → A₁) r) = (algebraMap R A₂ : (a : R) → A₂) r
⊢ { toEquiv := e, map_mul' := h₁, map_add' := h₂, commutes' := h₃ : A₁ ≃ₐ[R] A₂ }.symm =
    { toEquiv := e.symm, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

Tactic:
rfl

Premises used: AlgEquiv.symm, Equiv.symm, rfl
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type uR
A₁ : Type uA₁
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Algebra R A₁
⊢ Eq.{uA₁ + 1} (α := A₁ ≃ₐ[R] A₁) (symm refl) refl

Tactic:
rfl

Premises used: AlgEquiv.symm, Equiv.symm, AlgEquiv.refl, Equiv.refl, rfl
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Algebra R A₁
inst_4 : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
⊢ e.toRingEquiv.symm = e.symm.toRingEquiv

Tactic:
rfl

Premises used: Equiv.symm, RingEquiv.symm, rfl
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Algebra R A₁
inst_4 : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
⊢ e.symm.toRingEquiv = e.toRingEquiv.symm

Tactic:
rfl

Premises used: Equiv.symm, RingEquiv.symm, rfl
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Algebra R A₁
inst_4 : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
⊢ Eq (α := A₂ ≃+ A₁) (↑e.symm : A₂ ≃+ A₁) (AddEquiv.symm (↑e : A₁ ≃+ A₂))

Tactic:
rfl

Premises used: AddEquivClass.toAddEquiv, Equiv.symm, EquivLike.toEquiv, rfl, AddEquiv.symm
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Algebra R A₁
inst_4 : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
⊢ Eq (α := A₂ ≃* A₁) (↑e.symm : A₂ ≃* A₁) (MulEquiv.symm (↑e : A₁ ≃* A₂))

Tactic:
rfl

Premises used: Equiv.symm, MulEquiv.symm, MulEquivClass.toMulEquiv, EquivLike.toEquiv, rfl
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Algebra R A₁
inst_4 : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
⊢ ∀ (x : A₂), (e : (a : A₁) → A₂) ((e.symm : (a : A₂) → A₁) x : A₁) = x

Tactic:
e.toEquiv.apply_symm_apply

Premises used: Equiv.apply_symm_apply, AlgEquiv.toEquiv
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Algebra R A₁
inst_4 : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
⊢ ∀ (x : A₁), (e.symm : (a : A₂) → A₁) ((e : (a : A₁) → A₂) x : A₂) = x

Tactic:
e.toEquiv.symm_apply_apply

Premises used: Equiv.symm_apply_apply, AlgEquiv.toEquiv
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Algebra R A₁
inst_4 : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
x : A₂
y : A₁
⊢ (e.symm : (a : A₂) → A₁) x = y ↔ x = (e : (a : A₁) → A₂) y

Tactic:
e.toEquiv.symm_apply_eq

Premises used: Equiv.symm_apply_eq, AlgEquiv.toEquiv
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Algebra R A₁
inst_4 : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
x : A₂
y : A₁
⊢ y = (e.symm : (a : A₂) → A₁) x ↔ (e : (a : A₁) → A₂) y = x

Tactic:
e.toEquiv.eq_symm_apply

Premises used: AlgEquiv.toEquiv, Equiv.eq_symm_apply
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Algebra R A₁
inst_4 : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
H :
  ∀ (x : A₂),
    Eq (α := A₂) (((↑e : A₁ →ₐ[R] A₂).comp (↑e.symm : A₂ →ₐ[R] A₁) : (a : A₂) → A₂) x : A₂)
      ((AlgHom.id R A₂ : (a : A₂) → A₂) x : A₂)
⊢ (↑e : A₁ →ₐ[R] A₂).comp (↑e.symm : A₂ →ₐ[R] A₁) = AlgHom.id R A₂

Tactic:
ext
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Algebra R A₁
inst_4 : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
x : A₂
⊢ Eq (α := A₂) (((↑e : A₁ →ₐ[R] A₂).comp (↑e.symm : A₂ →ₐ[R] A₁) : (a : A₂) → A₂) x : A₂)
    ((AlgHom.id R A₂ : (a : A₂) → A₂) x : A₂)

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Algebra R A₁
inst_4 : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
H :
  ∀ (x : A₁),
    Eq (α := A₁) (((↑e.symm : A₂ →ₐ[R] A₁).comp (↑e : A₁ →ₐ[R] A₂) : (a : A₁) → A₁) x : A₁)
      ((AlgHom.id R A₁ : (a : A₁) → A₁) x : A₁)
⊢ (↑e.symm : A₂ →ₐ[R] A₁).comp (↑e : A₁ →ₐ[R] A₂) = AlgHom.id R A₁

Tactic:
ext
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Algebra R A₁
inst_4 : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
x : A₁
⊢ Eq (α := A₁) (((↑e.symm : A₂ →ₐ[R] A₁).comp (↑e : A₁ →ₐ[R] A₂) : (a : A₁) → A₁) x : A₁)
    ((AlgHom.id R A₁ : (a : A₁) → A₁) x : A₁)

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Algebra R A₁
inst_4 : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
⊢ Function.LeftInverse.{uA₁ + 1, uA₂ + 1} (α := A₁) (β := A₂) (⇑e.symm : (a : A₂) → A₁) (⇑e : (a : A₁) → A₂)

Tactic:
e.left_inv

Premises used: AlgEquiv.toEquiv, Equiv.left_inv
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Algebra R A₁
inst_4 : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
⊢ Function.RightInverse.{uA₁ + 1, uA₂ + 1} (α := A₁) (β := A₂) (⇑e.symm : (a : A₂) → A₁) (⇑e : (a : A₁) → A₂)

Tactic:
e.right_inv

Premises used: Equiv.right_inv, AlgEquiv.toEquiv
-- Module: Mathlib.Algebra.Algebra.Equiv
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_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Semiring A₃
inst_4 : Semiring A₁'
inst_5 : Semiring A₂'
inst_6 : Semiring A₃'
inst_7 : Algebra R A₁
inst_8 : Algebra R A₂
inst_9 : Algebra R A₃
inst_10 : Algebra R A₁'
inst_11 : Algebra R A₂'
inst_12 : Algebra R A₃'
e e₁ : A₁ ≃ₐ[R] A₂
e₂ : A₂ ≃ₐ[R] A₃
r : R
rw : e₂.toFun ((algebraMap R A₂ : (a : R) → A₂) r) = (algebraMap R A₃ : (a : R) → A₃) r
rw₁ rw₂ : Eq.{uA₃ + 1} (α := A₃) ((algebraMap R A₃ : (a : R) → A₃) r : A₃) ((algebraMap R A₃ : (a : R) → A₃) r : A₃)
⊢ e₂.toFun (e₁.toFun ((algebraMap R A₁ : (a : R) → A₁) r)) = (algebraMap R A₃ : (a : R) → A₃) r

Tactic:
rw [e₁.commutes', e₂.commutes']

Premises used: AlgEquiv.commutes'
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Semiring A₃
inst_4 : Algebra R A₁
inst_5 : Algebra R A₂
inst_6 : Algebra R A₃
e₁ : A₁ ≃ₐ[R] A₂
e₂ : A₂ ≃ₐ[R] A₃
⊢ Eq (α := (a : A₁) → A₃) (⇑(e₁.trans e₂) : (a : A₁) → A₃)
    (Function.comp.{uA₁ + 1, uA₂ + 1, uA₃ + 1} (β := A₂) (⇑e₂ : (a : A₂) → A₃) (⇑e₁ : (a : A₁) → A₂))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Semiring A₃
inst_4 : Algebra R A₁
inst_5 : Algebra R A₂
inst_6 : Algebra R A₃
e₁ : A₁ ≃ₐ[R] A₂
e₂ : A₂ ≃ₐ[R] A₃
x : A₁
⊢ Eq.{uA₃ + 1} (α := A₃) ((e₁.trans e₂ : (a : A₁) → A₃) x : A₃)
    ((e₂ : (a : A₂) → A₃) ((e₁ : (a : A₁) → A₂) x : A₂) : A₃)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Semiring A₃
inst_4 : Algebra R A₁
inst_5 : Algebra R A₂
inst_6 : Algebra R A₃
e₁ : A₁ ≃ₐ[R] A₂
e₂ : A₂ ≃ₐ[R] A₃
x : A₃
⊢ Eq.{uA₁ + 1} (α := A₁) (((e₁.trans e₂).symm : (a : A₃) → A₁) x : A₁)
    ((e₁.symm : (a : A₂) → A₁) ((e₂.symm : (a : A₃) → A₂) x : A₂) : A₁)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Algebra R A₁
inst_4 : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
h : ∀ (a : A₁), Eq (α := A₁) ((e.trans e.symm : (a : A₁) → A₁) a : A₁) ((refl : (a : A₁) → A₁) a : A₁)
⊢ e.trans e.symm = refl

Tactic:
ext
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Algebra R A₁
inst_4 : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
a : A₁
⊢ Eq (α := A₁) ((e.trans e.symm : (a : A₁) → A₁) a : A₁) ((refl : (a : A₁) → A₁) a : A₁)

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Algebra R A₁
inst_4 : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
h : ∀ (a : A₂), Eq (α := A₂) ((e.symm.trans e : (a : A₂) → A₂) a : A₂) ((refl : (a : A₂) → A₂) a : A₂)
⊢ e.symm.trans e = refl

Tactic:
ext
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Algebra R A₁
inst_4 : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
a : A₂
⊢ Eq (α := A₂) ((e.symm.trans e : (a : A₂) → A₂) a : A₂) ((refl : (a : A₂) → A₂) a : A₂)

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Semiring A₃
inst_4 : Algebra R A₁
inst_5 : Algebra R A₂
inst_6 : Algebra R A₃
e₁ : A₁ ≃ₐ[R] A₂
e₂ : A₂ ≃ₐ[R] A₃
⊢ Eq (α := A₁ →+* A₃) (↑(e₁.trans e₂) : A₁ →+* A₃)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e₂ : A₂ →+* A₃) (↑e₁ : A₁ →+* A₂))

Tactic:
rfl

Premises used: MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, rfl
-- Module: Mathlib.Algebra.Algebra.Equiv
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_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Semiring A₃
inst_4 : Semiring A₁'
inst_5 : Semiring A₂'
inst_6 : Semiring A₃'
inst_7 : Algebra R A₁
inst_8 : Algebra R A₂
inst_9 : Algebra R A₃
inst_10 : Algebra R A₁'
inst_11 : Algebra R A₂'
inst_12 : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
ι : Type u_1
A : ι → Type u_2
inst_13 : (i : ι) → Semiring (A i)
inst_14 : (i : ι) → Algebra.{uR, u_2} R (A i)
i j : ι
h : i = j
x : R
refl :
  Eq.{u_2 + 1} (α := A i)
    (Equiv.toFun (RingEquiv.toEquiv (RingEquiv.cast (R := A) ⋯ : A i ≃+* A i)) ((algebraMap R (A i) : (a : R) → A i) x))
    ((algebraMap R (A i) : (a : R) → A i) x)
⊢ Eq.{u_2 + 1} (α := A j)
    (Equiv.toFun (RingEquiv.toEquiv (RingEquiv.cast (R := A) h : A i ≃+* A j)) ((algebraMap R (A i) : (a : R) → A i) x))
    ((algebraMap R (A j) : (a : R) → A j) x)

Tactic:
cases h
-- Module: Mathlib.Algebra.Algebra.Equiv
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_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Semiring A₃
inst_4 : Semiring A₁'
inst_5 : Semiring A₂'
inst_6 : Semiring A₃'
inst_7 : Algebra R A₁
inst_8 : Algebra R A₂
inst_9 : Algebra R A₃
inst_10 : Algebra R A₁'
inst_11 : Algebra R A₂'
inst_12 : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
ι : Type u_1
A : ι → Type u_2
inst_13 : (i : ι) → Semiring (A i)
inst_14 : (i : ι) → Algebra.{uR, u_2} R (A i)
i : ι
x : R
__spread.0 : A i ≃+* A i := RingEquiv.cast (R := A) ⋯
⊢ Eq.{u_2 + 1} (α := A i)
    (Equiv.toFun (RingEquiv.toEquiv (RingEquiv.cast (R := A) ⋯ : A i ≃+* A i)) ((algebraMap R (A i) : (a : R) → A i) x))
    ((algebraMap R (A i) : (a : R) → A i) x)

Tactic:
rfl
-- Module: Mathlib.Algebra.Algebra.Equiv
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_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Semiring A₃
inst_4 : Semiring A₁'
inst_5 : Semiring A₂'
inst_6 : Semiring A₃'
inst_7 : Algebra R A₁
inst_8 : Algebra R A₂
inst_9 : Algebra R A₃
inst_10 : Algebra R A₁'
inst_11 : Algebra R A₂'
inst_12 : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
e₁ : A₁ ≃ₐ[R] A₁'
e₂ : A₂ ≃ₐ[R] A₂'
f : A₁ →ₐ[R] A₂
simp : (↑e₂.symm : A₂' →ₐ[R] A₂).comp ((↑e₂ : A₂ →ₐ[R] A₂').comp (f.comp (AlgHom.id R A₁))) = f
⊢ (fun (f : A₁' →ₐ[R] A₂') ↦ ((↑e₂.symm : A₂' →ₐ[R] A₂).comp f).comp (↑e₁ : A₁ →ₐ[R] A₁'))
      ((fun (f : A₁ →ₐ[R] A₂) ↦ ((↑e₂ : A₂ →ₐ[R] A₂').comp f).comp (↑e₁.symm : A₁' →ₐ[R] A₁)) f) =
    f

Tactic:
simp only [AlgHom.comp_assoc, symm_comp]

Premises used: AlgHom.comp_assoc, AlgEquiv.symm_comp
-- Module: Mathlib.Algebra.Algebra.Equiv
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_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Semiring A₃
inst_4 : Semiring A₁'
inst_5 : Semiring A₂'
inst_6 : Semiring A₃'
inst_7 : Algebra R A₁
inst_8 : Algebra R A₂
inst_9 : Algebra R A₃
inst_10 : Algebra R A₁'
inst_11 : Algebra R A₂'
inst_12 : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
e₁ : A₁ ≃ₐ[R] A₁'
e₂ : A₂ ≃ₐ[R] A₂'
f : A₁ →ₐ[R] A₂
⊢ (↑e₂.symm : A₂' →ₐ[R] A₂).comp ((↑e₂ : A₂ →ₐ[R] A₂').comp (f.comp (AlgHom.id R A₁))) = f

Tactic:
simp only [← AlgHom.comp_assoc, symm_comp, AlgHom.id_comp, AlgHom.comp_id]

Premises used: AlgHom.comp_assoc, AlgHom.id_comp, AlgEquiv.symm_comp, AlgHom.comp_id
-- Module: Mathlib.Algebra.Algebra.Equiv
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_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Semiring A₃
inst_4 : Semiring A₁'
inst_5 : Semiring A₂'
inst_6 : Semiring A₃'
inst_7 : Algebra R A₁
inst_8 : Algebra R A₂
inst_9 : Algebra R A₃
inst_10 : Algebra R A₁'
inst_11 : Algebra R A₂'
inst_12 : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
e₁ : A₁ ≃ₐ[R] A₁'
e₂ : A₂ ≃ₐ[R] A₂'
f : A₁' →ₐ[R] A₂'
simp : (↑e₂ : A₂ →ₐ[R] A₂').comp ((↑e₂.symm : A₂' →ₐ[R] A₂).comp (f.comp (AlgHom.id R A₁'))) = f
⊢ (fun (f : A₁ →ₐ[R] A₂) ↦ ((↑e₂ : A₂ →ₐ[R] A₂').comp f).comp (↑e₁.symm : A₁' →ₐ[R] A₁))
      ((fun (f : A₁' →ₐ[R] A₂') ↦ ((↑e₂.symm : A₂' →ₐ[R] A₂).comp f).comp (↑e₁ : A₁ →ₐ[R] A₁')) f) =
    f

Tactic:
simp only [AlgHom.comp_assoc, comp_symm]

Premises used: AlgHom.comp_assoc, AlgEquiv.comp_symm
-- Module: Mathlib.Algebra.Algebra.Equiv
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_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Semiring A₃
inst_4 : Semiring A₁'
inst_5 : Semiring A₂'
inst_6 : Semiring A₃'
inst_7 : Algebra R A₁
inst_8 : Algebra R A₂
inst_9 : Algebra R A₃
inst_10 : Algebra R A₁'
inst_11 : Algebra R A₂'
inst_12 : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
e₁ : A₁ ≃ₐ[R] A₁'
e₂ : A₂ ≃ₐ[R] A₂'
f : A₁' →ₐ[R] A₂'
⊢ (↑e₂ : A₂ →ₐ[R] A₂').comp ((↑e₂.symm : A₂' →ₐ[R] A₂).comp (f.comp (AlgHom.id R A₁'))) = f

Tactic:
simp only [← AlgHom.comp_assoc, comp_symm, AlgHom.id_comp, AlgHom.comp_id]

Premises used: AlgHom.comp_assoc, AlgHom.id_comp, AlgEquiv.comp_symm, AlgHom.comp_id
-- Module: Mathlib.Algebra.Algebra.Equiv
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_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Semiring A₃
inst_4 : Semiring A₁'
inst_5 : Semiring A₂'
inst_6 : Semiring A₃'
inst_7 : Algebra R A₁
inst_8 : Algebra R A₂
inst_9 : Algebra R A₃
inst_10 : Algebra R A₁'
inst_11 : Algebra R A₂'
inst_12 : Algebra R A₃'
e₁ : A₁ ≃ₐ[R] A₁'
e₂ : A₂ ≃ₐ[R] A₂'
e₃ : A₃ ≃ₐ[R] A₃'
f : A₁ →ₐ[R] A₂
g : A₂ →ₐ[R] A₃
H :
  ∀ (x : A₁'),
    Eq.{uA₃' + 1} (α := A₃')
      ((((e₁.arrowCongr e₃ : (a : A₁ →ₐ[R] A₃) → A₁' →ₐ[R] A₃') (g.comp f) : A₁' →ₐ[R] A₃') : (a : A₁') → A₃') x : A₃')
      ((AlgHom.comp.{uR, uA₁', uA₂', uA₃'} (B := A₂') ((e₂.arrowCongr e₃ : (a : A₂ →ₐ[R] A₃) → A₂' →ₐ[R] A₃') g)
              ((e₁.arrowCongr e₂ : (a : A₁ →ₐ[R] A₂) → A₁' →ₐ[R] A₂') f) :
            (a : A₁') → A₃')
          x :
        A₃')
⊢ Eq (α := A₁' →ₐ[R] A₃') ((e₁.arrowCongr e₃ : (a : A₁ →ₐ[R] A₃) → A₁' →ₐ[R] A₃') (g.comp f) : A₁' →ₐ[R] A₃')
    (AlgHom.comp.{uR, uA₁', uA₂', uA₃'} (B := A₂') ((e₂.arrowCongr e₃ : (a : A₂ →ₐ[R] A₃) → A₂' →ₐ[R] A₃') g)
        ((e₁.arrowCongr e₂ : (a : A₁ →ₐ[R] A₂) → A₁' →ₐ[R] A₂') f) :
      A₁' →ₐ[R] A₃')

Tactic:
ext
-- Module: Mathlib.Algebra.Algebra.Equiv
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_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Semiring A₃
inst_4 : Semiring A₁'
inst_5 : Semiring A₂'
inst_6 : Semiring A₃'
inst_7 : Algebra R A₁
inst_8 : Algebra R A₂
inst_9 : Algebra R A₃
inst_10 : Algebra R A₁'
inst_11 : Algebra R A₂'
inst_12 : Algebra R A₃'
e₁ : A₁ ≃ₐ[R] A₁'
e₂ : A₂ ≃ₐ[R] A₂'
e₃ : A₃ ≃ₐ[R] A₃'
f : A₁ →ₐ[R] A₂
g : A₂ →ₐ[R] A₃
x : A₁'
⊢ Eq.{uA₃' + 1} (α := A₃')
    ((((e₁.arrowCongr e₃ : (a : A₁ →ₐ[R] A₃) → A₁' →ₐ[R] A₃') (g.comp f) : A₁' →ₐ[R] A₃') : (a : A₁') → A₃') x : A₃')
    ((AlgHom.comp.{uR, uA₁', uA₂', uA₃'} (B := A₂') ((e₂.arrowCongr e₃ : (a : A₂ →ₐ[R] A₃) → A₂' →ₐ[R] A₃') g)
            ((e₁.arrowCongr e₂ : (a : A₁ →ₐ[R] A₂) → A₁' →ₐ[R] A₂') f) :
          (a : A₁') → A₃')
        x :
      A₃')

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Algebra R A₁
inst_4 : Algebra R A₂
⊢ Eq (α := (A₁ →ₐ[R] A₂) ≃ (A₁ →ₐ[R] A₂)) (arrowCongr refl refl) (Equiv.refl (A₁ →ₐ[R] A₂))

Tactic:
rfl

Premises used: AlgEquiv.arrowCongr, AlgHom.comp, Equiv.refl, rfl
-- Module: Mathlib.Algebra.Algebra.Equiv
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_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Semiring A₃
inst_4 : Semiring A₁'
inst_5 : Semiring A₂'
inst_6 : Semiring A₃'
inst_7 : Algebra R A₁
inst_8 : Algebra R A₂
inst_9 : Algebra R A₃
inst_10 : Algebra R A₁'
inst_11 : Algebra R A₂'
inst_12 : Algebra R A₃'
e₁ : A₁ ≃ₐ[R] A₂
e₁' : A₁' ≃ₐ[R] A₂'
e₂ : A₂ ≃ₐ[R] A₃
e₂' : A₂' ≃ₐ[R] A₃'
⊢ (e₁.trans e₂).arrowCongr (e₁'.trans e₂') = (e₁.arrowCongr e₁').trans (e₂.arrowCongr e₂')

Tactic:
rfl

Premises used: AlgEquiv.toAlgHom, AlgEquiv.symm, Equiv.trans, AlgEquiv.arrowCongr, AlgEquiv.trans, Equiv.symm, AlgHom.comp, rfl
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₁' : Type uA₁'
A₂' : Type uA₂'
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Semiring A₁'
inst_4 : Semiring A₂'
inst_5 : Algebra R A₁
inst_6 : Algebra R A₂
inst_7 : Algebra R A₁'
inst_8 : Algebra R A₂'
e₁ : A₁ ≃ₐ[R] A₁'
e₂ : A₂ ≃ₐ[R] A₂'
⊢ (e₁.arrowCongr e₂).symm = e₁.symm.arrowCongr e₂.symm

Tactic:
rfl

Premises used: AlgEquiv.symm, AlgEquiv.arrowCongr, Equiv.symm, AlgHom.comp, rfl
-- Module: Mathlib.Algebra.Algebra.Equiv
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_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Semiring A₃
inst_4 : Semiring A₁'
inst_5 : Semiring A₂'
inst_6 : Semiring A₃'
inst_7 : Algebra R A₁
inst_8 : Algebra R A₂
inst_9 : Algebra R A₃
inst_10 : Algebra R A₁'
inst_11 : Algebra R A₂'
inst_12 : Algebra R A₃'
e_1 e : A₁ ≃ₐ[R] A₂
e' : A₁' ≃ₐ[R] A₂'
ψ : A₁ ≃ₐ[R] A₁'
h :
  ∀ (a : A₁),
    Eq.{uA₁' + 1} (α := A₁')
      (((fun (ψ : A₂ ≃ₐ[R] A₂') ↦ e.trans (ψ.trans e'.symm)) ((fun (ψ : A₁ ≃ₐ[R] A₁') ↦ e.symm.trans (ψ.trans e')) ψ) :
            (a : A₁) → A₁')
          a :
        A₁')
      ((ψ : (a : A₁) → A₁') a : A₁')
⊢ (fun (ψ : A₂ ≃ₐ[R] A₂') ↦ e.trans (ψ.trans e'.symm)) ((fun (ψ : A₁ ≃ₐ[R] A₁') ↦ e.symm.trans (ψ.trans e')) ψ) = ψ

Tactic:
ext
-- Module: Mathlib.Algebra.Algebra.Equiv
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_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Semiring A₃
inst_4 : Semiring A₁'
inst_5 : Semiring A₂'
inst_6 : Semiring A₃'
inst_7 : Algebra R A₁
inst_8 : Algebra R A₂
inst_9 : Algebra R A₃
inst_10 : Algebra R A₁'
inst_11 : Algebra R A₂'
inst_12 : Algebra R A₃'
e_1 e : A₁ ≃ₐ[R] A₂
e' : A₁' ≃ₐ[R] A₂'
ψ : A₁ ≃ₐ[R] A₁'
a : A₁
h h₁ :
  Eq.{uA₁' + 1} (α := A₁') ((e.trans ((e.symm.trans (ψ.trans e')).trans e'.symm) : (a : A₁) → A₁') a : A₁')
    ((ψ : (a : A₁) → A₁') a : A₁')
h₂ :
  Eq.{uA₁' + 1} (α := A₁')
    ((e'.symm : (a : A₂') → A₁')
        ((e' : (a : A₁') → A₂')
            ((ψ : (a : A₁) → A₁') ((e.symm : (a : A₂) → A₁) ((e : (a : A₁) → A₂) a : A₂) : A₁) : A₁') :
          A₂') :
      A₁')
    ((ψ : (a : A₁) → A₁') a : A₁')
⊢ Eq.{uA₁' + 1} (α := A₁')
    (((fun (ψ : A₂ ≃ₐ[R] A₂') ↦ e.trans (ψ.trans e'.symm)) ((fun (ψ : A₁ ≃ₐ[R] A₁') ↦ e.symm.trans (ψ.trans e')) ψ) :
          (a : A₁) → A₁')
        a :
      A₁')
    ((ψ : (a : A₁) → A₁') a : A₁')

Tactic:
simp_rw [trans_apply, symm_apply_apply]

Premises used: AlgEquiv.symm_apply_apply, AlgEquiv.trans_apply
-- Module: Mathlib.Algebra.Algebra.Equiv
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_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Semiring A₃
inst_4 : Semiring A₁'
inst_5 : Semiring A₂'
inst_6 : Semiring A₃'
inst_7 : Algebra R A₁
inst_8 : Algebra R A₂
inst_9 : Algebra R A₃
inst_10 : Algebra R A₁'
inst_11 : Algebra R A₂'
inst_12 : Algebra R A₃'
e_1 e : A₁ ≃ₐ[R] A₂
e' : A₁' ≃ₐ[R] A₂'
ψ : A₂ ≃ₐ[R] A₂'
h :
  ∀ (a : A₂),
    Eq.{uA₂' + 1} (α := A₂')
      (((fun (ψ : A₁ ≃ₐ[R] A₁') ↦ e.symm.trans (ψ.trans e')) ((fun (ψ : A₂ ≃ₐ[R] A₂') ↦ e.trans (ψ.trans e'.symm)) ψ) :
            (a : A₂) → A₂')
          a :
        A₂')
      ((ψ : (a : A₂) → A₂') a : A₂')
⊢ (fun (ψ : A₁ ≃ₐ[R] A₁') ↦ e.symm.trans (ψ.trans e')) ((fun (ψ : A₂ ≃ₐ[R] A₂') ↦ e.trans (ψ.trans e'.symm)) ψ) = ψ

Tactic:
ext