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
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.symm.symm : (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
a : A
b : B
⊢ (e.symm : (a : B) → A) b = a ↔ b = (e : (a : A) → B) a

Tactic:
e.toEquiv.symm_apply_eq

Premises used: Equiv.symm_apply_eq, 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
b : B
⊢ a = (e.symm : (a : B) → A) b ↔ (e : (a : A) → B) a = b

Tactic:
e.toEquiv.eq_symm_apply

Premises used: AlgEquiv.toEquiv, ContinuousAlgEquiv.toAlgEquiv, Equiv.eq_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
S : Set A
⊢ Eq.{u_3 + 1} (α := Set B) ((⇑e : (a : A) → B) '' S) ((⇑e.symm : (a : B) → A) ⁻¹' S)

Tactic:
e.toEquiv.image_eq_preimage_symm S

Premises used: Equiv.image_eq_preimage_symm, 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
S : Set B
rw : Eq.{u_2 + 1} (α := Set A) ((⇑e.symm.symm : (a : A) → B) ⁻¹' S) ((⇑e : (a : A) → B) ⁻¹' S)
rw₁ rw₂ : Eq.{u_2 + 1} (α := Set A) ((⇑e : (a : A) → B) ⁻¹' S) ((⇑e : (a : A) → B) ⁻¹' S)
⊢ Eq.{u_2 + 1} (α := Set A) ((⇑e.symm : (a : B) → A) '' S) ((⇑e : (a : A) → B) ⁻¹' S)

Tactic:
rw [e.symm.image_eq_preimage_symm, e.symm_symm]

Premises used: ContinuousAlgEquiv.symm, ContinuousAlgEquiv.image_eq_preimage_symm, ContinuousAlgEquiv.symm_symm
-- 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.preimage.{u_3, u_2} (β := A) (⇑e.symm : (a : B) → A) ((⇑e : (a : A) → B) ⁻¹' S) = S

Tactic:
e.toEquiv.symm_preimage_preimage S

Premises used: Equiv.symm_preimage_preimage, 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
S : Set A
⊢ Set.preimage.{u_2, u_3} (β := B) (⇑e : (a : A) → B) ((⇑e.symm : (a : B) → A) ⁻¹' S) = S

Tactic:
e.symm.symm_preimage_preimage S

Premises used: ContinuousAlgEquiv.symm, ContinuousAlgEquiv.symm_preimage_preimage
-- Module: Mathlib.Topology.Algebra.Algebra.Equiv
Goal:
R : Type u_1
inst : CommSemiring R
E₁ : Type u_5
E₂ : Type u_6
inst_1 : UniformSpace E₁
inst_2 : UniformSpace E₂
inst_3 : Ring E₁
inst_4 : IsUniformAddGroup E₁
inst_5 : Algebra R E₁
inst_6 : Ring E₂
inst_7 : IsUniformAddGroup E₂
inst_8 : Algebra R E₂
e : E₁ ≃A[R] E₂
⊢ IsUniformEmbedding.{u_5, u_6} (α := E₁) (β := E₂) (⇑e : (a : E₁) → E₂)

Tactic:
e.toAlgEquiv.isUniformEmbedding e.toContinuousAlgHom.uniformContinuous
    e.symm.toContinuousAlgHom.uniformContinuous

Premises used: Equiv.isUniformEmbedding, ContinuousAlgEquiv.symm, ContinuousAlgHom.uniformContinuous, ContinuousAlgEquiv.toContinuousAlgHom, AlgEquiv.toEquiv, ContinuousAlgEquiv.toAlgEquiv
-- Module: Mathlib.Topology.Algebra.Algebra.Equiv
Goal:
R : Type u_1
inst : CommSemiring R
E₁ : Type u_5
E₂ : Type u_6
inst_1 : UniformSpace E₁
inst_2 : UniformSpace E₂
inst_3 : Ring E₁
inst_4 : IsUniformAddGroup E₁
inst_5 : Algebra R E₁
inst_6 : Ring E₂
inst_7 : IsUniformAddGroup E₂
inst_8 : Algebra R E₂
e : E₁ ≃ₐ[R] E₂
h₁ : Continuous[inst_1.toTopologicalSpace, inst_2.toTopologicalSpace] (⇑e : (a : E₁) → E₂)
h₂ : Continuous[inst_2.toTopologicalSpace, inst_1.toTopologicalSpace] (⇑e.symm : (a : E₂) → E₁)
dsimp : Continuous[inst_2.toTopologicalSpace, inst_1.toTopologicalSpace] (⇑e.symm : (a : E₂) → E₁)
⊢ Continuous[inst_2.toTopologicalSpace, inst_1.toTopologicalSpace] e.invFun

Tactic:
dsimp
-- Module: Mathlib.Topology.Algebra.Algebra.Equiv
Goal:
R : Type u_1
inst : CommSemiring R
E₁ : Type u_5
E₂ : Type u_6
inst_1 : UniformSpace E₁
inst_2 : UniformSpace E₂
inst_3 : Ring E₁
inst_4 : IsUniformAddGroup E₁
inst_5 : Algebra R E₁
inst_6 : Ring E₂
inst_7 : IsUniformAddGroup E₂
inst_8 : Algebra R E₂
e : E₁ ≃ₐ[R] E₂
h₁ : Continuous[inst_1.toTopologicalSpace, inst_2.toTopologicalSpace] (⇑e : (a : E₁) → E₂)
h₂ : Continuous[inst_2.toTopologicalSpace, inst_1.toTopologicalSpace] (⇑e.symm : (a : E₂) → E₁)
⊢ Continuous[inst_2.toTopologicalSpace, inst_1.toTopologicalSpace] (⇑e.symm : (a : E₂) → E₁)

Tactic:
fun_prop
-- 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
⊢ Function.Surjective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑e : (a : A) → B)

Tactic:
e.toAlgEquiv.surjective

Premises used: ContinuousAlgEquiv.toAlgEquiv, AlgEquiv.surjective
-- Module: Mathlib.Topology.Algebra.Algebra.Equiv
Goal:
R : Type u_1
A_1 : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : Semiring A_1
inst_2 : TopologicalSpace A_1
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Semiring C
inst_6 : TopologicalSpace C
inst_7 : Algebra R A_1
inst_8 : Algebra R B
inst_9 : Algebra R C
ι : Type u_5
A : ι → Type u_6
inst_10 : (i : ι) → Semiring (A i)
inst_11 : (i : ι) → Algebra.{u_1, u_6} R (A i)
inst_12 : (i : ι) → TopologicalSpace (A i)
i j : ι
h : i = j
refl :
  Continuous[inst_12 i, inst_12 i] (Equiv.toFun (AlgEquiv.toEquiv.{u_1, u_6, u_6} (R := R) (AlgEquiv.cast (A := A) ⋯)))
⊢ Continuous[inst_12 i, inst_12 j] (Equiv.toFun (AlgEquiv.toEquiv.{u_1, u_6, u_6} (R := R) (AlgEquiv.cast (A := A) h)))

Tactic:
cases h
-- Module: Mathlib.Topology.Algebra.Algebra.Equiv
Goal:
R : Type u_1
A_1 : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : Semiring A_1
inst_2 : TopologicalSpace A_1
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Semiring C
inst_6 : TopologicalSpace C
inst_7 : Algebra R A_1
inst_8 : Algebra R B
inst_9 : Algebra R C
ι : Type u_5
A : ι → Type u_6
inst_10 : (i : ι) → Semiring (A i)
inst_11 : (i : ι) → Algebra.{u_1, u_6} R (A i)
inst_12 : (i : ι) → TopologicalSpace (A i)
i : ι
__spread.0 : A i ≃ₐ[R] A i := AlgEquiv.cast (A := A) ⋯
⊢ Continuous[inst_12 i, inst_12 i] (Equiv.toFun (AlgEquiv.toEquiv.{u_1, u_6, u_6} (R := R) (AlgEquiv.cast (A := A) ⋯)))

Tactic:
continuous_id

Premises used: cast, continuous_id
-- Module: Mathlib.Topology.Algebra.Algebra.Equiv
Goal:
R : Type u_1
A_1 : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : Semiring A_1
inst_2 : TopologicalSpace A_1
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Semiring C
inst_6 : TopologicalSpace C
inst_7 : Algebra R A_1
inst_8 : Algebra R B
inst_9 : Algebra R C
ι : Type u_5
A : ι → Type u_6
inst_10 : (i : ι) → Semiring (A i)
inst_11 : (i : ι) → Algebra.{u_1, u_6} R (A i)
inst_12 : (i : ι) → TopologicalSpace (A i)
i : ι
__spread.0 : A i ≃ₐ[R] A i := AlgEquiv.cast (A := A) ⋯
⊢ Continuous[inst_12 i, inst_12 i] (Equiv.toFun (AlgEquiv.toEquiv.{u_1, u_6, u_6} (R := R) (AlgEquiv.cast (A := A) ⋯)))

Tactic:
exact continuous_id

Premises used: continuous_id
-- Module: Mathlib.Topology.Algebra.Algebra.Equiv
Goal:
R : Type u_1
A_1 : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : Semiring A_1
inst_2 : TopologicalSpace A_1
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Semiring C
inst_6 : TopologicalSpace C
inst_7 : Algebra R A_1
inst_8 : Algebra R B
inst_9 : Algebra R C
ι : Type u_5
A : ι → Type u_6
inst_10 : (i : ι) → Semiring (A i)
inst_11 : (i : ι) → Algebra.{u_1, u_6} R (A i)
inst_12 : (i : ι) → TopologicalSpace (A i)
i j : ι
h : i = j
refl :
  Continuous[inst_12 i, inst_12 i] (Equiv.invFun (AlgEquiv.toEquiv.{u_1, u_6, u_6} (R := R) (AlgEquiv.cast (A := A) ⋯)))
⊢ Continuous[inst_12 j, inst_12 i] (Equiv.invFun (AlgEquiv.toEquiv.{u_1, u_6, u_6} (R := R) (AlgEquiv.cast (A := A) h)))

Tactic:
cases h
-- Module: Mathlib.Topology.Algebra.Algebra.Equiv
Goal:
R : Type u_1
A_1 : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : Semiring A_1
inst_2 : TopologicalSpace A_1
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Semiring C
inst_6 : TopologicalSpace C
inst_7 : Algebra R A_1
inst_8 : Algebra R B
inst_9 : Algebra R C
ι : Type u_5
A : ι → Type u_6
inst_10 : (i : ι) → Semiring (A i)
inst_11 : (i : ι) → Algebra.{u_1, u_6} R (A i)
inst_12 : (i : ι) → TopologicalSpace (A i)
i : ι
__spread.0 : A i ≃ₐ[R] A i := AlgEquiv.cast (A := A) ⋯
⊢ Continuous[inst_12 i, inst_12 i] (Equiv.invFun (AlgEquiv.toEquiv.{u_1, u_6, u_6} (R := R) (AlgEquiv.cast (A := A) ⋯)))

Tactic:
continuous_id

Premises used: cast, continuous_id
-- Module: Mathlib.Topology.Algebra.Algebra.Equiv
Goal:
R : Type u_1
A_1 : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : Semiring A_1
inst_2 : TopologicalSpace A_1
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Semiring C
inst_6 : TopologicalSpace C
inst_7 : Algebra R A_1
inst_8 : Algebra R B
inst_9 : Algebra R C
ι : Type u_5
A : ι → Type u_6
inst_10 : (i : ι) → Semiring (A i)
inst_11 : (i : ι) → Algebra.{u_1, u_6} R (A i)
inst_12 : (i : ι) → TopologicalSpace (A i)
i : ι
__spread.0 : A i ≃ₐ[R] A i := AlgEquiv.cast (A := A) ⋯
⊢ Continuous[inst_12 i, inst_12 i] (Equiv.invFun (AlgEquiv.toEquiv.{u_1, u_6, u_6} (R := R) (AlgEquiv.cast (A := A) ⋯)))

Tactic:
exact continuous_id

Premises used: continuous_id
-- Module: Mathlib.Topology.Algebra.Algebra.Equiv
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_5
A : ι → Type u_6
inst_1 : (i : ι) → Semiring (A i)
inst_2 : (i : ι) → Algebra.{u_1, u_6} R (A i)
inst_3 : (i : ι) → TopologicalSpace (A i)
i j : ι
h : i = j
x : A i
⊢ Eq (α := A j) ((cast (A := A) h : (a : A i) → A j) x : A j) ((Equiv.cast ⋯ : (a : A i) → A j) x : A j)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Algebra.Equiv
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_5
A : ι → Type u_6
inst_1 : (i : ι) → Semiring (A i)
inst_2 : (i : ι) → Algebra.{u_1, u_6} R (A i)
inst_3 : (i : ι) → TopologicalSpace (A i)
i j : ι
h : i = j
x : A j
⊢ Eq (α := A i) ((symm (cast (A := A) h) : (a : A j) → A i) x : A i) ((Equiv.cast ⋯ : (a : A j) → A i) x : A i)

Tactic:
rfl

Premises used: cast, rfl
-- Module: Mathlib.Topology.Algebra.Algebra.Rat
Goal:
A : Type u_1
inst : DivisionRing A
inst_1 : TopologicalSpace A
inst_2 : SeparatelyContinuousMul A
inst_3 : CharZero A
r : ℚ
⊢ Continuous (Y := A) fun (x : A) ↦ r • x

Tactic:
simpa only [Algebra.smul_def] using continuous_id.const_mul _

Premises used: continuous_id, Algebra.smul_def, Continuous.const_mul
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
A : Type u
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : TopologicalSpace R
inst_4 : TopologicalSpace A
inst_5 : ContinuousSMul R A
rw : Continuous[inst_3, inst_4] fun (r : R) ↦ HSMul.hSMul (β := A) r 1
⊢ Continuous[inst_3, inst_4] (⇑(algebraMap R A) : (a : R) → A)

Tactic:
rw [algebraMap_eq_smul_one']

Premises used: Algebra.algebraMap_eq_smul_one'
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
A : Type u
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : TopologicalSpace R
inst_4 : TopologicalSpace A
inst_5 : ContinuousSMul R A
⊢ Continuous[inst_3, inst_4] fun (r : R) ↦ HSMul.hSMul (β := A) r 1

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
A : Type u
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : TopologicalSpace R
inst_4 : TopologicalSpace A
inst_5 : ContinuousMul A
⊢ Continuous[inst_3, inst_4] (⇑(algebraMap R A) : (a : R) → A) ↔
    Continuous[instTopologicalSpaceProd, inst_4] fun (p : R × A) ↦ p.1 • p.2

Tactic:
⟨fun h => ?_, fun h => have : ContinuousSMul R A := ⟨h⟩; continuous_algebraMap _ _⟩

Premises used: continuous_algebraMap, Iff.intro, ContinuousSMul.mk
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
A : Type u
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : TopologicalSpace R
inst_4 : TopologicalSpace A
inst_5 : ContinuousMul A
refine :
  ∀ (h : Continuous[inst_3, inst_4] (⇑(algebraMap R A) : (a : R) → A)),
    Continuous[instTopologicalSpaceProd, inst_4] fun (p : R × A) ↦ p.1 • p.2
⊢ Continuous[inst_3, inst_4] (⇑(algebraMap R A) : (a : R) → A) ↔
    Continuous[instTopologicalSpaceProd, inst_4] fun (p : R × A) ↦ p.1 • p.2

Tactic:
refine ⟨fun h => ?_, fun h => have : ContinuousSMul R A := ⟨h⟩; continuous_algebraMap _ _⟩
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
A : Type u
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : TopologicalSpace R
inst_4 : TopologicalSpace A
inst_5 : ContinuousMul A
h : Continuous[inst_3, inst_4] (⇑(algebraMap R A) : (a : R) → A)
simp :
  Continuous[instTopologicalSpaceProd, inst_4] fun (p : R × A) ↦
    HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) p.1 : A) p.2
⊢ Continuous[instTopologicalSpaceProd, inst_4] fun (p : R × A) ↦ p.1 • p.2

Tactic:
simp only [Algebra.smul_def]

Premises used: Algebra.smul_def
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
A : Type u
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : TopologicalSpace R
inst_4 : TopologicalSpace A
inst_5 : ContinuousMul A
h : Continuous[inst_3, inst_4] (⇑(algebraMap R A) : (a : R) → A)
⊢ Continuous[instTopologicalSpaceProd, inst_4] fun (p : R × A) ↦
    HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) p.1 : A) p.2

Tactic:
(h.comp continuous_fst).mul continuous_snd

Premises used: Continuous.comp, continuous_snd, continuous_fst, Continuous.mul
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
A : Type u
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : TopologicalSpace R
inst_4 : TopologicalSpace A
inst_5 : ContinuousMul A
h : Continuous[inst_3, inst_4] (⇑(algebraMap R A) : (a : R) → A)
⊢ Continuous[instTopologicalSpaceProd, inst_4] fun (p : R × A) ↦
    HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) p.1 : A) p.2

Tactic:
exact (h.comp continuous_fst).mul continuous_snd

Premises used: Continuous.comp, continuous_snd, continuous_fst, Continuous.mul
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
A : Type u
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : TopologicalSpace R
inst_4 : TopologicalSpace A
inst_5 : ContinuousMul A
h : Continuous[inst_3, inst_4] (⇑(algebraMap R A) : (a : R) → A)
⊢ ContinuousSMul R A

Tactic:
⟨(continuous_algebraMap_iff_smul R A).1 h⟩

Premises used: continuous_algebraMap_iff_smul, ContinuousSMul.mk, Iff.mp
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
A : Type u
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : TopologicalSpace R
inst_4 : TopologicalSpace A
S : Subalgebra R A
X : Type u_2
inst_5 : TopologicalSpace X
inst_6 : MulAction A X
inst_7 : ContinuousSMul A X
⊢ ContinuousSMul.{u, u_2} (↥S) X

Tactic:
Subsemiring.continuousSMul S.toSubsemiring X

Premises used: Set.Mem, Subalgebra.toSubsemiring, Subsemiring.continuousSMul
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
A : Type u
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : TopologicalSpace R
inst_4 : TopologicalSpace A
inst_5 : PartialOrder A
inst_6 : IsOrderedRing A
inst_7 : ContinuousMul A
⊢ ContinuousMul.{u} (↑(Icc 0 1) : Type u)

Tactic:
Topology.IsInducing.subtypeVal.continuousMul Icc.coeMonoidWithZeroHom

Premises used: Topology.IsInducing.continuousMul, Set.Icc.coeMonoidWithZeroHom, Topology.IsInducing.subtypeVal
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
A : Type u
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : TopologicalSpace R
inst_4 : TopologicalSpace A
inst_5 : PartialOrder A
inst_6 : IsOrderedRing A
inst_7 : ContinuousMul A
⊢ ContinuousMul.{u} (↑(Ico 0 1) : Type u)

Tactic:
Topology.IsInducing.subtypeVal.continuousMul Ico.coeMulHom

Premises used: Topology.IsInducing.continuousMul, Set.Ico.coeMulHom, Topology.IsInducing.subtypeVal
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
A : Type u
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : TopologicalSpace R
inst_4 : TopologicalSpace A
inst_5 : PartialOrder A
inst_6 : IsStrictOrderedRing A
inst_7 : ContinuousMul A
⊢ ContinuousMul.{u} (↑(Ioc 0 1) : Type u)

Tactic:
Topology.IsInducing.subtypeVal.continuousMul Ioc.coeMonoidHom

Premises used: Set.Ioc.coeMonoidHom, Topology.IsInducing.continuousMul, Topology.IsInducing.subtypeVal
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
A : Type u
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : TopologicalSpace R
inst_4 : TopologicalSpace A
inst_5 : PartialOrder A
inst_6 : IsStrictOrderedRing A
inst_7 : ContinuousMul A
⊢ ContinuousMul.{u} (↑(Ioo 0 1) : Type u)

Tactic:
Topology.IsInducing.subtypeVal.continuousMul Ioo.coeMulHom

Premises used: Topology.IsInducing.continuousMul, Set.Ioo.coeMulHom, Topology.IsInducing.subtypeVal
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
A : Type u
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : TopologicalSpace R
inst_4 : TopologicalSpace A
inst_5 : ContinuousSMul R A
⊢ Eq (α := (a : R) → A) (⇑(algebraMapCLM R A) : (a : R) → A) (⇑(algebraMap R A) : (a : R) → A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
A : Type u
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : TopologicalSpace R
inst_4 : TopologicalSpace A
inst_5 : ContinuousSMul R A
⊢ Eq (α := R →ₗ[R] A) (↑(algebraMapCLM R A) : R →ₗ[R] A) (Algebra.linearMap R A)

Tactic:
rfl

Premises used: Algebra.linearMap, rfl
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
A : Type u
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : TopologicalSpace R
inst_4 : TopologicalSpace A
inst_5 : ContinuousSMul R A
h : Eq.{u + 1} (α := A) ((toSpanSingleton R 1 : (a : R) → A) 1 : A) ((algebraMapCLM R A : (a : R) → A) 1 : A)
⊢ Eq (α := R →L[R] A) (toSpanSingleton R 1) (algebraMapCLM R A)

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
A : Type u
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : TopologicalSpace R
inst_4 : TopologicalSpace A
inst_5 : ContinuousSMul R A
⊢ Eq.{u + 1} (α := A) ((toSpanSingleton R 1 : (a : R) → A) 1 : A) ((algebraMapCLM R A : (a : R) → A) 1 : A)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
A : Type u
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : TopologicalSpace R
inst_4 : TopologicalSpace A
inst_5 : IsTopologicalSemiring A
inst_6 : DiscreteTopology R
⊢ ContinuousSMul R A

Tactic:
continuousSMul_of_algebraMap _ _ continuous_of_discreteTopology

Premises used: continuousSMul_of_algebraMap, continuous_of_discreteTopology
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
B : Type u_3
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) ((fun (f : A →A[R] B) ↦ ((⇑f.toAlgHom : (a : A) → B) : (a : A) → B)) f)
    ((fun (f : A →A[R] B) ↦ ((⇑f.toAlgHom : (a : A) → B) : (a : A) → B)) g)
mk :
  ∀ (toAlgHom : A →ₐ[R] B) (cont : Continuous[inst_2, inst_4] (↑(↑toAlgHom.toRingHom : A →* B) : OneHom A B).toFun)
    (h :
      Eq (α := (a : A) → B)
        ((fun (f : A →A[R] B) ↦ ((⇑f.toAlgHom : (a : A) → B) : (a : A) → B)) { toAlgHom := toAlgHom, cont := cont })
        ((fun (f : A →A[R] B) ↦ ((⇑f.toAlgHom : (a : A) → B) : (a : A) → B)) g)),
    { toAlgHom := toAlgHom, cont := cont : A →A[R] B } = g
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
B : Type u_3
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
g : A →A[R] B
toAlgHom : A →ₐ[R] B
cont : Continuous[inst_2, inst_4] (↑(↑toAlgHom.toRingHom : A →* B) : OneHom A B).toFun
h :
  Eq (α := (a : A) → B)
    ((fun (f : A →A[R] B) ↦ ((⇑f.toAlgHom : (a : A) → B) : (a : A) → B)) { toAlgHom := toAlgHom, cont := cont })
    ((fun (f : A →A[R] B) ↦ ((⇑f.toAlgHom : (a : A) → B) : (a : A) → B)) g)
mk :
  ∀ (toAlgHom_1 : A →ₐ[R] B)
    (cont_1 : Continuous[inst_2, inst_4] (↑(↑toAlgHom_1.toRingHom : A →* B) : OneHom A B).toFun)
    (h :
      Eq (α := (a : A) → B)
        ((fun (f : A →A[R] B) ↦ ((⇑f.toAlgHom : (a : A) → B) : (a : A) → B)) { toAlgHom := toAlgHom, cont := cont })
        ((fun (f : A →A[R] B) ↦ ((⇑f.toAlgHom : (a : A) → B) : (a : A) → B))
          { toAlgHom := toAlgHom_1, cont := cont_1 })),
    { toAlgHom := toAlgHom, cont := cont : A →A[R] B } = { toAlgHom := toAlgHom_1, cont := cont_1 }
⊢ { toAlgHom := toAlgHom, cont := cont : A →A[R] B } = g

Tactic:
cases g
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
B : Type u_3
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
toAlgHom : A →ₐ[R] B
cont : Continuous[inst_2, inst_4] (↑(↑toAlgHom.toRingHom : A →* B) : OneHom A B).toFun
toAlgHom_1 : A →ₐ[R] B
cont_1 : Continuous[inst_2, inst_4] (↑(↑toAlgHom_1.toRingHom : A →* B) : OneHom A B).toFun
h :
  Eq (α := (a : A) → B)
    ((fun (f : A →A[R] B) ↦ ((⇑f.toAlgHom : (a : A) → B) : (a : A) → B)) { toAlgHom := toAlgHom, cont := cont })
    ((fun (f : A →A[R] B) ↦ ((⇑f.toAlgHom : (a : A) → B) : (a : A) → B)) { toAlgHom := toAlgHom_1, cont := cont_1 })
mk : toAlgHom = toAlgHom_1
⊢ { toAlgHom := toAlgHom, cont := cont : A →A[R] B } = { toAlgHom := toAlgHom_1, cont := cont_1 }

Tactic:
simp only [mk.injEq]

Premises used: ContinuousAlgHom.mk.injEq
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
B : Type u_3
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
toAlgHom : A →ₐ[R] B
cont : Continuous[inst_2, inst_4] (↑(↑toAlgHom.toRingHom : A →* B) : OneHom A B).toFun
toAlgHom_1 : A →ₐ[R] B
cont_1 : Continuous[inst_2, inst_4] (↑(↑toAlgHom_1.toRingHom : A →* B) : OneHom A B).toFun
h :
  Eq (α := (a : A) → B)
    ((fun (f : A →A[R] B) ↦ ((⇑f.toAlgHom : (a : A) → B) : (a : A) → B)) { toAlgHom := toAlgHom, cont := cont })
    ((fun (f : A →A[R] B) ↦ ((⇑f.toAlgHom : (a : A) → B) : (a : A) → B)) { toAlgHom := toAlgHom_1, cont := cont_1 })
⊢ toAlgHom = toAlgHom_1

Tactic:
AlgHom.ext (congrFun h)

Premises used: AlgHom.ext, congrFun