awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Algebra.Equiv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Semiring C
inst_6 : TopologicalSpace C
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : Algebra R C
g : A ≃A[R] B
f' : A ≃ₐ[R] B
continuous_toFun : Continuous[inst_2, inst_4] f'.toFun
continuous_invFun : Continuous[inst_4, inst_2] f'.invFun
h₁ :
  { toAlgEquiv := f', continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun : A ≃A[R] B }.toFun =
    g.toFun
h₂ :
  { toAlgEquiv := f', continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun :
        A ≃A[R] B }.invFun =
    g.invFun
obtain :
  ∀ (g' : A ≃ₐ[R] B) (continuous_toFun_1 : Continuous[inst_2, inst_4] g'.toFun)
    (continuous_invFun_1 : Continuous[inst_4, inst_2] g'.invFun)
    (h₁ :
      { toAlgEquiv := f', continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun :
            A ≃A[R] B }.toFun =
        { toAlgEquiv := g', continuous_toFun := continuous_toFun_1, continuous_invFun := continuous_invFun_1 :
            A ≃A[R] B }.toFun)
    (h₂ :
      { toAlgEquiv := f', continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun :
            A ≃A[R] B }.invFun =
        { toAlgEquiv := g', continuous_toFun := continuous_toFun_1, continuous_invFun := continuous_invFun_1 :
            A ≃A[R] B }.invFun),
    { toAlgEquiv := f', continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun : A ≃A[R] B } =
      { toAlgEquiv := g', continuous_toFun := continuous_toFun_1, continuous_invFun := continuous_invFun_1 }
⊢ { toAlgEquiv := f', continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun : A ≃A[R] B } = g

Tactic:
obtain ⟨g', _⟩ := g
-- Module: Mathlib.Topology.Algebra.Algebra.Equiv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
e : A ≃A[R] B
a : A
⊢ Eq.{u_3 + 1} (α := B) (((↑e : A →A[R] B) : (a : A) → B) a : B) ((e : (a : A) → B) a : B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Algebra.Equiv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
e : A ≃ₐ[R] B
he : Continuous[inst_2, inst_4] e.toFun
he' : Continuous[inst_4, inst_2] e.invFun
⊢ Eq (α := (a : A) → B)
    (⇑{ toAlgEquiv := e, continuous_toFun := he, continuous_invFun := he' : A ≃A[R] B } : (a : A) → B)
    (⇑e : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Algebra.Equiv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
e : A ≃A[R] B
⊢ Eq (α := (a : A) → B) (⇑(↑e : A →A[R] B) : (a : A) → B) (⇑e : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Algebra.Equiv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
e : A ≃ₐ[R] B
continuous_toFun : Continuous[inst_2, inst_4] e.toFun
continuous_invFun : Continuous[inst_4, inst_2] e.invFun
continuous_toFun_1 :
  Continuous[inst_2, inst_4]
    { toAlgEquiv := e, continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun : A ≃A[R] B }.toFun
continuous_invFun_1 :
  Continuous[inst_4, inst_2]
    { toAlgEquiv := e, continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun : A ≃A[R] B }.invFun
⊢ { toAlgEquiv := e, continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun : A ≃A[R] B } =
    {
      toAlgEquiv :=
        { toAlgEquiv := e, continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun :
            A ≃A[R] B }.toAlgEquiv,
      continuous_toFun := continuous_toFun_1, continuous_invFun := continuous_invFun_1 }

Tactic:
rfl
-- Module: Mathlib.Topology.Algebra.Algebra.Equiv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
f g : A ≃A[R] B
h : Eq (α := (a : A) → B) (⇑f : (a : A) → B) (⇑g : (a : A) → B)
⊢ f = g

Tactic:
toAlgEquiv_injective <| AlgEquiv.ext <| congr_fun h

Premises used: ContinuousAlgEquiv.toAlgEquiv_injective, AlgEquiv.ext, congr_fun
-- Module: Mathlib.Topology.Algebra.Algebra.Equiv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
⊢ Function.Injective (α := A ≃A[R] B) toContinuousAlgHom

Tactic:
fun _ _ h => ext <| funext <| ContinuousAlgHom.ext_iff.1 h

Premises used: funext, ContinuousAlgHom.ext_iff, Iff.mp, ContinuousAlgEquiv.ext, Function.Injective
-- Module: Mathlib.Topology.Algebra.Algebra.Equiv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
f g : A ≃A[R] B
⊢ (↑f : A →A[R] B) = (↑g : A →A[R] B) ↔ f = g

Tactic:
coe_injective.eq_iff

Premises used: Function.Injective.eq_iff, ContinuousAlgEquiv.coe_injective
-- Module: Mathlib.Topology.Algebra.Algebra.Equiv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
e : A ≃A[R] B
⊢ Eq (α := (a : A) → B) (⇑e.toAlgEquiv : (a : A) → B) (⇑e : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Algebra.Equiv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
e : A ≃A[R] B
a : A
⊢ Eq.{u_3 + 1} (α := B) (((↑e : A ≃L[R] B) : (a : A) → B) a : B) ((e : (a : A) → B) a : B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Algebra.Equiv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
e : A ≃A[R] B
⊢ Eq (α := (a : A) → B) (⇑(↑e : A ≃L[R] B) : (a : A) → B) (⇑e : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Algebra.Equiv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
e : A ≃A[R] B
⊢ (↑(↑e : A ≃L[R] B) : A →L[R] B) = (↑e : A →A[R] B).toContinuousLinearMap

Tactic:
rfl

Premises used: AlgHom.toLinearMap, ContinuousAlgHom.toContinuousLinearMap, rfl, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Topology.Algebra.Algebra.Equiv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
e : A ≃A[R] B
⊢ (↑(↑e : A ≃L[R] B) : A ≃ₗ[R] B) = (↑e.toAlgEquiv : A ≃ₗ[R] B)

Tactic:
rfl

Premises used: AlgEquiv.toLinearEquiv, rfl
-- Module: Mathlib.Topology.Algebra.Algebra.Equiv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
e : A ≃A[R] B
⊢ IsOpenMap.{u_2, u_3} (X := A) (Y := B) (⇑e : (a : A) → B)

Tactic:
e.toHomeomorph.isOpenMap

Premises used: ContinuousAlgEquiv.toHomeomorph, Homeomorph.isOpenMap
-- Module: Mathlib.Topology.Algebra.Algebra.Equiv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
e : A ≃A[R] B
S : Set A
⊢ Eq.{u_3 + 1} (α := Set B) ((⇑e : (a : A) → B) '' closure[inst_2] S) (closure[inst_4] ((⇑e : (a : A) → B) '' S))

Tactic:
e.toHomeomorph.image_closure S

Premises used: ContinuousAlgEquiv.toHomeomorph, Homeomorph.image_closure
-- Module: Mathlib.Topology.Algebra.Algebra.Equiv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
e : A ≃A[R] B
S : Set B
⊢ Eq.{u_2 + 1} (α := Set A) ((⇑e : (a : A) → B) ⁻¹' closure[inst_4] S) (closure[inst_2] ((⇑e : (a : A) → B) ⁻¹' S))

Tactic:
e.toHomeomorph.preimage_closure S

Premises used: ContinuousAlgEquiv.toHomeomorph, Homeomorph.preimage_closure
-- Module: Mathlib.Topology.Algebra.Algebra.Equiv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
e : A ≃A[R] B
S : Set A
⊢ IsClosed[inst_4] ((⇑e : (a : A) → B) '' S) ↔ IsClosed[inst_2] S

Tactic:
e.toHomeomorph.isClosed_image

Premises used: ContinuousAlgEquiv.toHomeomorph, Homeomorph.isClosed_image
-- Module: Mathlib.Topology.Algebra.Algebra.Equiv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
e : A ≃A[R] B
a : A
⊢ Eq.{u_3 + 1} (α := Filter B) (Filter.map (⇑e : (a : A) → B) (𝓝 a) : Filter B) (𝓝 ((e : (a : A) → B) a) : Filter B)

Tactic:
e.toHomeomorph.map_nhds_eq a

Premises used: ContinuousAlgEquiv.toHomeomorph, Homeomorph.map_nhds_eq
-- Module: Mathlib.Topology.Algebra.Algebra.Equiv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
e : A ≃A[R] B
a : A
⊢ Eq.{u_3 + 1} (α := B) ((e : (a : A) → B) a : B) (0 : B) ↔ a = 0

Tactic:
e.toAlgEquiv.toLinearEquiv.map_eq_zero_iff

Premises used: LinearEquiv.map_eq_zero_iff, AlgEquiv.toLinearEquiv, ContinuousAlgEquiv.toAlgEquiv
-- Module: Mathlib.Topology.Algebra.Algebra.Equiv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
e : A ≃A[R] B
⊢ Continuous[inst_2, inst_4] (⇑e : (a : A) → B)

Tactic:
e.continuous_toFun

Premises used: ContinuousAlgEquiv.continuous_toFun
-- Module: Mathlib.Topology.Algebra.Algebra.Equiv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
e : A ≃A[R] B
S : Set A
⊢ ContinuousOn.{u_2, u_3} (Y := B) (⇑e : (a : A) → B) S

Tactic:
e.continuous.continuousOn

Premises used: Continuous.continuousOn, ContinuousAlgEquiv.continuous
-- Module: Mathlib.Topology.Algebra.Algebra.Equiv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
e : A ≃A[R] B
a : A
⊢ ContinuousAt.{u_2, u_3} (Y := B) (⇑e : (a : A) → B) a

Tactic:
e.continuous.continuousAt

Premises used: ContinuousAlgEquiv.continuous, Continuous.continuousAt
-- Module: Mathlib.Topology.Algebra.Algebra.Equiv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
e : A ≃A[R] B
S : Set A
a : A
⊢ ContinuousWithinAt.{u_2, u_3} (Y := B) (⇑e : (a : A) → B) S a

Tactic:
e.continuous.continuousWithinAt

Premises used: ContinuousAlgEquiv.continuous, Continuous.continuousWithinAt
-- Module: Mathlib.Topology.Algebra.Algebra.Equiv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
α : Type u_5
inst_7 : TopologicalSpace α
e : A ≃A[R] B
f : α → A
⊢ Continuous[inst_7, inst_4] ((⇑e : (a : A) → B) ∘ f) ↔ Continuous[inst_7, inst_2] f

Tactic:
e.toHomeomorph.comp_continuous_iff

Premises used: ContinuousAlgEquiv.toHomeomorph, Homeomorph.comp_continuous_iff
-- Module: Mathlib.Topology.Algebra.Algebra.Equiv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
β : Type u_5
inst_7 : TopologicalSpace β
e : A ≃A[R] B
g : B → β
⊢ Continuous[inst_2, inst_7] (g ∘ (⇑e : (a : A) → B)) ↔ Continuous[inst_4, inst_7] g

Tactic:
e.toHomeomorph.comp_continuous_iff'

Premises used: ContinuousAlgEquiv.toHomeomorph, Homeomorph.comp_continuous_iff'
-- Module: Mathlib.Topology.Algebra.Algebra.Equiv
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Algebra R A
a : A
⊢ (refl R A : (a : A) → A) a = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Algebra.Equiv
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Algebra R A
⊢ Eq (α := A →A[R] A) (↑(refl R A) : A →A[R] A) (ContinuousAlgHom.id R A)

Tactic:
rfl

Premises used: AlgEquiv.toAlgHom, ContinuousAlgEquiv.toContinuousAlgHom, AlgHom.id, ContinuousAlgHom.id, rfl
-- Module: Mathlib.Topology.Algebra.Algebra.Equiv
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Algebra R A
⊢ Eq (α := A ≃L[R] A) (↑(refl R A) : A ≃L[R] A) (ContinuousLinearEquiv.refl R A)

Tactic:
rfl

Premises used: ContinuousAlgEquiv.toContinuousLinearEquiv, ContinuousLinearEquiv.refl, LinearEquiv.refl, rfl
-- Module: Mathlib.Topology.Algebra.Algebra.Equiv
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Algebra R A
⊢ Eq (α := (a : A) → A) (⇑(refl R A) : (a : A) → A) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Algebra.Equiv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
e : A ≃A[R] B
b : B
⊢ (e : (a : A) → B) ((e.symm : (a : B) → A) b : A) = b

Tactic:
e.1.right_inv b

Premises used: Equiv.right_inv, AlgEquiv.toEquiv, ContinuousAlgEquiv.toAlgEquiv
-- Module: Mathlib.Topology.Algebra.Algebra.Equiv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
e : A ≃A[R] B
a : A
⊢ (e.symm : (a : B) → A) ((e : (a : A) → B) a : B) = a

Tactic:
e.1.left_inv a

Premises used: AlgEquiv.toEquiv, ContinuousAlgEquiv.toAlgEquiv, Equiv.left_inv
-- Module: Mathlib.Topology.Algebra.Algebra.Equiv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
e : A ≃A[R] B
S : Set A
⊢ Set.image.{u_3, u_2} (α := B) (⇑e.symm : (a : B) → A) ((⇑e : (a : A) → B) '' S) = S

Tactic:
e.toEquiv.symm_image_image S

Premises used: AlgEquiv.toEquiv, ContinuousAlgEquiv.toAlgEquiv, Equiv.symm_image_image
-- Module: Mathlib.Topology.Algebra.Algebra.Equiv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
e : A ≃A[R] B
S : Set B
⊢ Set.image.{u_2, u_3} (α := A) (⇑e : (a : A) → B) ((⇑e.symm : (a : B) → A) '' S) = S

Tactic:
e.symm.symm_image_image S

Premises used: ContinuousAlgEquiv.symm, ContinuousAlgEquiv.symm_image_image
-- Module: Mathlib.Topology.Algebra.Algebra.Equiv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
e : A ≃A[R] B
⊢ e.symm.toAlgEquiv = e.symm

Tactic:
rfl

Premises used: AlgEquiv.symm, rfl
-- Module: Mathlib.Topology.Algebra.Algebra.Equiv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
e : A ≃A[R] B
⊢ e.symm.toHomeomorph = e.toHomeomorph.symm

Tactic:
rfl

Premises used: Homeomorph.symm, Equiv.symm, rfl
-- Module: Mathlib.Topology.Algebra.Algebra.Equiv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
e : A ≃A[R] B
⊢ (↑e.symm : B ≃L[R] A) = (↑e : A ≃L[R] B).symm

Tactic:
rfl

Premises used: ContinuousLinearEquiv.symm, LinearEquiv.symm, ContinuousAlgEquiv.toContinuousLinearEquiv, LinearEquiv.toEquiv, rfl
-- Module: Mathlib.Topology.Algebra.Algebra.Equiv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
e : A ≃A[R] B
a : A
⊢ Filter.map.{u_3, u_2} (α := B) ((⇑e.symm : (a : B) → A) : (a : B) → A) (𝓝 ((e : (a : A) → B) a) : Filter B) = 𝓝 a

Tactic:
e.toHomeomorph.symm_map_nhds_eq a

Premises used: ContinuousAlgEquiv.toHomeomorph, Homeomorph.symm_map_nhds_eq
-- Module: Mathlib.Topology.Algebra.Algebra.Equiv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Semiring C
inst_6 : TopologicalSpace C
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : Algebra R C
e₁ : A ≃A[R] B
e₂ : B ≃A[R] C
⊢ (e₁.trans e₂).toAlgEquiv = e₁.trans e₂.toAlgEquiv

Tactic:
rfl

Premises used: AlgEquiv.trans, rfl
-- Module: Mathlib.Topology.Algebra.Algebra.Equiv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Semiring C
inst_6 : TopologicalSpace C
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : Algebra R C
e₁ : A ≃A[R] B
e₂ : B ≃A[R] C
⊢ (↑(e₁.trans e₂) : A ≃L[R] C) = (↑e₁ : A ≃L[R] B).trans (↑e₂ : B ≃L[R] C)

Tactic:
rfl

Premises used: ContinuousAlgEquiv.toContinuousLinearEquiv, ContinuousLinearEquiv.trans, LinearEquiv.toEquiv, LinearEquiv.trans, rfl
-- Module: Mathlib.Topology.Algebra.Algebra.Equiv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Semiring C
inst_6 : TopologicalSpace C
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : Algebra R C
e₁ : A ≃A[R] B
e₂ : B ≃A[R] C
a : A
⊢ Eq.{u_4 + 1} (α := C) ((e₁.trans e₂ : (a : A) → C) a : C) ((e₂ : (a : B) → C) ((e₁ : (a : A) → B) a : B) : C)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Algebra.Equiv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Semiring C
inst_6 : TopologicalSpace C
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : Algebra R C
e₁ : B ≃A[R] A
e₂ : C ≃A[R] B
a : A
⊢ Eq.{u_4 + 1} (α := C) (((e₂.trans e₁).symm : (a : A) → C) a : C)
    ((e₂.symm : (a : B) → C) ((e₁.symm : (a : A) → B) a : B) : C)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Algebra.Equiv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Semiring C
inst_6 : TopologicalSpace C
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : Algebra R C
e₁ : A ≃A[R] B
e₂ : B ≃A[R] C
⊢ (↑e₂.toAlgEquiv : B →ₐ[R] C).comp (↑e₁.toAlgEquiv : A →ₐ[R] B) = (↑(↑(e₁.trans e₂) : A →A[R] C) : A →ₐ[R] C)

Tactic:
rfl
-- Module: Mathlib.Topology.Algebra.Algebra.Equiv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
e : A ≃A[R] B
⊢ (↑e : A →A[R] B).comp (↑e.symm : B →A[R] A) = ContinuousAlgHom.id R B

Tactic:
ContinuousAlgHom.ext e.apply_symm_apply

Premises used: ContinuousAlgHom.ext, ContinuousAlgEquiv.apply_symm_apply
-- Module: Mathlib.Topology.Algebra.Algebra.Equiv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
e : A ≃A[R] B
⊢ (↑e.symm : B →A[R] A).comp (↑e : A →A[R] B) = ContinuousAlgHom.id R A

Tactic:
ContinuousAlgHom.ext e.symm_apply_apply

Premises used: ContinuousAlgHom.ext, ContinuousAlgEquiv.symm_apply_apply
-- Module: Mathlib.Topology.Algebra.Algebra.Equiv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
e : A ≃A[R] B
⊢ Eq.{u_2 + 1} (α := A → A)
    (Function.comp.{u_2 + 1, u_3 + 1, u_2 + 1} (β := B) (⇑e.symm : (a : B) → A) (⇑e : (a : A) → B)) id

Tactic:
funext <| e.symm_apply_apply

Premises used: funext, ContinuousAlgEquiv.symm_apply_apply
-- Module: Mathlib.Topology.Algebra.Algebra.Equiv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
e : A ≃A[R] B
⊢ Eq.{u_2 + 1} (α := A → A)
    (Function.comp.{u_2 + 1, u_3 + 1, u_2 + 1} (β := B) (⇑e.symm : (a : B) → A) (⇑e : (a : A) → B)) id

Tactic:
exact funext <| e.symm_apply_apply

Premises used: funext, ContinuousAlgEquiv.symm_apply_apply
-- Module: Mathlib.Topology.Algebra.Algebra.Equiv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
e : A ≃A[R] B
⊢ Eq.{u_3 + 1} (α := B → B)
    (Function.comp.{u_3 + 1, u_2 + 1, u_3 + 1} (β := A) (⇑e : (a : A) → B) (⇑e.symm : (a : B) → A)) id

Tactic:
funext <| e.apply_symm_apply

Premises used: funext, ContinuousAlgEquiv.apply_symm_apply
-- Module: Mathlib.Topology.Algebra.Algebra.Equiv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
e : A ≃A[R] B
⊢ e.symm.symm = e

Tactic:
rfl

Premises used: AlgEquiv.symm, ContinuousAlgEquiv.symm, Equiv.symm, rfl
-- Module: Mathlib.Topology.Algebra.Algebra.Equiv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
⊢ Function.Bijective (α := A ≃A[R] B) 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, ContinuousAlgEquiv.symm_symm
-- Module: Mathlib.Topology.Algebra.Algebra.Equiv
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Algebra R A
⊢ Eq (α := A ≃A[R] A) (symm (refl R A)) (refl R A)

Tactic:
rfl

Premises used: AlgEquiv.symm, ContinuousAlgEquiv.symm, ContinuousAlgEquiv.refl, Equiv.symm, AlgEquiv.refl, Equiv.refl, rfl