awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
G : Type u
inst : TopologicalSpace G
H : Type v
inst_1 : TopologicalSpace H
M : Type u_1
N : Type u_2
inst_2 : TopologicalSpace M
inst_3 : TopologicalSpace N
inst_4 : Mul M
inst_5 : Mul N
toMulEquiv : M ≃* N
continuous_toFun : Continuous toMulEquiv.toFun
continuous_invFun : Continuous toMulEquiv.invFun
toMulEquiv_1 : M ≃* N
continuous_toFun_1 : Continuous toMulEquiv_1.toFun
continuous_invFun_1 : Continuous toMulEquiv_1.invFun
h₁ :
  { toMulEquiv := toMulEquiv, continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun :
        M ≃ₜ* N }.toFun =
    { toMulEquiv := toMulEquiv_1, continuous_toFun := continuous_toFun_1, continuous_invFun := continuous_invFun_1 :
        M ≃ₜ* N }.toFun
h₂ :
  { toMulEquiv := toMulEquiv, continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun :
        M ≃ₜ* N }.invFun =
    { toMulEquiv := toMulEquiv_1, continuous_toFun := continuous_toFun_1, continuous_invFun := continuous_invFun_1 :
        M ≃ₜ* N }.invFun
mk : toMulEquiv = toMulEquiv_1
⊢ { toMulEquiv := toMulEquiv, continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun : M ≃ₜ* N } =
    { toMulEquiv := toMulEquiv_1, continuous_toFun := continuous_toFun_1, continuous_invFun := continuous_invFun_1 }

Tactic:
congr
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
G : Type u
inst : TopologicalSpace G
H : Type v
inst_1 : TopologicalSpace H
M : Type u_1
N : Type u_2
inst_2 : TopologicalSpace M
inst_3 : TopologicalSpace N
inst_4 : Mul M
inst_5 : Mul N
toMulEquiv : M ≃* N
continuous_toFun : Continuous toMulEquiv.toFun
continuous_invFun : Continuous toMulEquiv.invFun
toMulEquiv_1 : M ≃* N
continuous_toFun_1 : Continuous toMulEquiv_1.toFun
continuous_invFun_1 : Continuous toMulEquiv_1.invFun
h₁ :
  { toMulEquiv := toMulEquiv, continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun :
        M ≃ₜ* N }.toFun =
    { toMulEquiv := toMulEquiv_1, continuous_toFun := continuous_toFun_1, continuous_invFun := continuous_invFun_1 :
        M ≃ₜ* N }.toFun
h₂ :
  { toMulEquiv := toMulEquiv, continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun :
        M ≃ₜ* N }.invFun =
    { toMulEquiv := toMulEquiv_1, continuous_toFun := continuous_toFun_1, continuous_invFun := continuous_invFun_1 :
        M ≃ₜ* N }.invFun
⊢ toMulEquiv = toMulEquiv_1

Tactic:
MulEquiv.ext_iff.mpr (congrFun h₁)

Premises used: Iff.mpr, MulEquiv.ext_iff, congrFun
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
G : Type u
inst : TopologicalSpace G
H : Type v
inst_1 : TopologicalSpace H
M : Type u_1
N : Type u_2
inst_2 : TopologicalSpace M
inst_3 : TopologicalSpace N
inst_4 : Mul M
inst_5 : Mul N
toMulEquiv : M ≃* N
continuous_toFun : Continuous toMulEquiv.toFun
continuous_invFun : Continuous toMulEquiv.invFun
toMulEquiv_1 : M ≃* N
continuous_toFun_1 : Continuous toMulEquiv_1.toFun
continuous_invFun_1 : Continuous toMulEquiv_1.invFun
h₁ :
  { toMulEquiv := toMulEquiv, continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun :
        M ≃ₜ* N }.toFun =
    { toMulEquiv := toMulEquiv_1, continuous_toFun := continuous_toFun_1, continuous_invFun := continuous_invFun_1 :
        M ≃ₜ* N }.toFun
h₂ :
  { toMulEquiv := toMulEquiv, continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun :
        M ≃ₜ* N }.invFun =
    { toMulEquiv := toMulEquiv_1, continuous_toFun := continuous_toFun_1, continuous_invFun := continuous_invFun_1 :
        M ≃ₜ* N }.invFun
⊢ toMulEquiv = toMulEquiv_1

Tactic:
exact MulEquiv.ext_iff.mpr (congrFun h₁)

Premises used: Iff.mpr, MulEquiv.ext_iff, congrFun
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
M : Type u_1
N : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace N
inst_2 : Mul M
inst_3 : Mul N
f g : M ≃ₜ* N
h : ∀ (x : M), Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N)
⊢ f = g

Tactic:
DFunLike.ext f g h

Premises used: DFunLike.ext
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
M : Type u_1
N : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace N
inst_2 : Mul M
inst_3 : Mul N
f : M ≃* N
hf1 : Continuous f.toFun
hf2 : Continuous f.invFun
⊢ Eq (α := (a : M) → N)
    (⇑{ toMulEquiv := f, continuous_toFun := hf1, continuous_invFun := hf2 : M ≃ₜ* N } : (a : M) → N) (⇑f : (a : M) → N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
M : Type u_1
N : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace N
inst_2 : Mul M
inst_3 : Mul N
f : M ≃ₜ* N
⊢ f.toEquiv = (↑f : M ≃ N)

Tactic:
rfl

Premises used: EquivLike.toEquiv, rfl
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
M : Type u_1
N : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace N
inst_2 : Mul M
inst_3 : Mul N
f : M ≃ₜ* N
⊢ f.toMulEquiv = (↑f : M ≃* N)

Tactic:
rfl

Premises used: MulEquivClass.toMulEquiv, EquivLike.toEquiv, rfl
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
M : Type u_1
N : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace N
inst_2 : Mul M
inst_3 : Mul N
f : M ≃ₜ* N
⊢ f.toHomeomorph = (↑f : M ≃ₜ N)

Tactic:
rfl

Premises used: HomeomorphClass.toHomeomorph, EquivLike.toEquiv, rfl
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
M : Type u_1
N : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace N
inst_2 : Mul M
inst_3 : Mul N
f : M ≃ₜ N
h :
  ∀ (x y : M),
    (f : (a : M) → N) (x * y) = HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N)
⊢ Eq (α := (a : M) → N) (⇑(mk' f h) : (a : M) → N) (⇑f : (a : M) → N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
M : Type u_1
N : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace N
inst_2 : Mul M
inst_3 : Mul N
e : M ≃ₜ* N
⊢ Function.Bijective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑e : (a : M) → N)

Tactic:
EquivLike.bijective e

Premises used: EquivLike.bijective
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
M : Type u_1
N : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace N
inst_2 : Mul M
inst_3 : Mul N
e : M ≃ₜ* N
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑e : (a : M) → N)

Tactic:
EquivLike.injective e

Premises used: EquivLike.injective
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
M : Type u_1
N : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace N
inst_2 : Mul M
inst_3 : Mul N
e : M ≃ₜ* N
⊢ Function.Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑e : (a : M) → N)

Tactic:
EquivLike.surjective e

Premises used: EquivLike.surjective
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
M : Type u_1
N : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace N
inst_2 : Mul M
inst_3 : Mul N
e : M ≃ₜ* N
x y : M
⊢ Eq.{u_2 + 1} (α := N) ((e : (a : M) → N) x : N) ((e : (a : M) → N) y : N) ↔ x = y

Tactic:
e.injective.eq_iff

Premises used: Function.Injective.eq_iff, ContinuousMulEquiv.injective
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
G : Type u
inst : TopologicalSpace G
H : Type v
inst_1 : TopologicalSpace H
M : Type u_1
N : Type u_2
inst_2 : TopologicalSpace M
inst_3 : TopologicalSpace N
inst_4 : Mul M
inst_5 : Mul N
dsimp : Continuous.{u_1, u_1} (X := M) id
⊢ Continuous (MulEquiv.toEquiv (MulEquiv.refl M)).toFun

Tactic:
dsimp
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
G : Type u
inst : TopologicalSpace G
H : Type v
inst_1 : TopologicalSpace H
M : Type u_1
N : Type u_2
inst_2 : TopologicalSpace M
inst_3 : TopologicalSpace N
inst_4 : Mul M
inst_5 : Mul N
⊢ Continuous.{u_1, u_1} (X := M) id

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
G : Type u
inst : TopologicalSpace G
H : Type v
inst_1 : TopologicalSpace H
M : Type u_1
N : Type u_2
inst_2 : TopologicalSpace M
inst_3 : TopologicalSpace N
inst_4 : Mul M
inst_5 : Mul N
dsimp : Continuous.{u_1, u_1} (X := M) id
⊢ Continuous (MulEquiv.toEquiv (MulEquiv.refl M)).invFun

Tactic:
dsimp
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
M : Type u_1
inst : TopologicalSpace M
inst_1 : Mul M
⊢ Eq (α := (a : M) → M) (⇑(refl M) : (a : M) → M) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
M : Type u_1
inst : TopologicalSpace M
inst_1 : Mul M
m : M
⊢ (refl M : (a : M) → M) m = m

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
M : Type u_1
N : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace N
inst_2 : Mul M
inst_3 : Mul N
f : M ≃ₜ* N
⊢ f.invFun = (⇑f.symm : (a : N) → M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
M : Type u_1
N : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace N
inst_2 : Mul M
inst_3 : Mul N
f : M ≃ₜ* N
⊢ Eq (α := N ≃ₜ M) (Homeomorph.symm (↑f : M ≃ₜ N)) (↑f.symm : N ≃ₜ M)

Tactic:
rfl

Premises used: HomeomorphClass.toHomeomorph, Homeomorph.symm, Equiv.symm, EquivLike.toEquiv, rfl
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
M : Type u_1
N : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace N
inst_2 : Mul M
inst_3 : Mul N
f : M ≃ₜ* N
⊢ EquivLike.inv f = (⇑f.symm : (a : N) → M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
M : Type u_1
N : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace N
inst_2 : Mul M
inst_3 : Mul N
f : M ≃ₜ* N
⊢ f.symm.symm = f

Tactic:
rfl

Premises used: ContinuousMulEquiv.symm, Equiv.symm, MulEquiv.symm, rfl
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
M : Type u_1
N : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace N
inst_2 : Mul M
inst_3 : Mul N
⊢ Function.Bijective (α := M ≃ₜ* N) 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, ContinuousMulEquiv.symm_symm
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
M : Type u_1
N : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace N
inst_2 : Mul M
inst_3 : Mul N
e : M ≃ₜ* N
y : N
⊢ (e : (a : M) → N) ((e.symm : (a : N) → M) y : M) = y

Tactic:
e.toEquiv.apply_symm_apply y

Premises used: Equiv.apply_symm_apply, MulEquiv.toEquiv, ContinuousMulEquiv.toMulEquiv
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
M : Type u_1
N : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace N
inst_2 : Mul M
inst_3 : Mul N
e : M ≃ₜ* N
x : M
⊢ (e.symm : (a : N) → M) ((e : (a : M) → N) x : N) = x

Tactic:
e.toEquiv.symm_apply_apply x

Premises used: Equiv.symm_apply_apply, MulEquiv.toEquiv, ContinuousMulEquiv.toMulEquiv
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
M : Type u_1
N : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace N
inst_2 : Mul M
inst_3 : Mul N
e : M ≃ₜ* N
⊢ Eq.{u_1 + 1} (α := M → M)
    (Function.comp.{u_1 + 1, u_2 + 1, u_1 + 1} (β := N) (⇑e.symm : (a : N) → M) (⇑e : (a : M) → N)) id

Tactic:
funext e.symm_apply_apply

Premises used: ContinuousMulEquiv.symm_apply_apply, funext
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
M : Type u_1
N : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace N
inst_2 : Mul M
inst_3 : Mul N
e : M ≃ₜ* N
⊢ Eq.{u_2 + 1} (α := N → N)
    (Function.comp.{u_2 + 1, u_1 + 1, u_2 + 1} (β := M) (⇑e : (a : M) → N) (⇑e.symm : (a : N) → M)) id

Tactic:
funext e.apply_symm_apply

Premises used: ContinuousMulEquiv.apply_symm_apply, funext
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
M : Type u_1
N : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace N
inst_2 : Mul M
inst_3 : Mul N
e : M ≃ₜ* N
x : M
y : N
⊢ (e : (a : M) → N) x = y ↔ x = (e.symm : (a : N) → M) y

Tactic:
e.toEquiv.apply_eq_iff_eq_symm_apply

Premises used: MulEquiv.toEquiv, ContinuousMulEquiv.toMulEquiv, Equiv.apply_eq_iff_eq_symm_apply
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
M : Type u_1
N : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace N
inst_2 : Mul M
inst_3 : Mul N
e : M ≃ₜ* N
x : N
y : M
⊢ (e.symm : (a : N) → M) x = y ↔ x = (e : (a : M) → N) y

Tactic:
e.toEquiv.symm_apply_eq

Premises used: Equiv.symm_apply_eq, MulEquiv.toEquiv, ContinuousMulEquiv.toMulEquiv
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
M : Type u_1
N : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace N
inst_2 : Mul M
inst_3 : Mul N
e : M ≃ₜ* N
x : N
y : M
⊢ y = (e.symm : (a : N) → M) x ↔ (e : (a : M) → N) y = x

Tactic:
e.toEquiv.eq_symm_apply

Premises used: MulEquiv.toEquiv, ContinuousMulEquiv.toMulEquiv, Equiv.eq_symm_apply
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
M : Type u_1
N : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace N
inst_2 : Mul M
inst_3 : Mul N
α : Type u_3
e : M ≃ₜ* N
f : N → α
g : M → α
⊢ f = g ∘ (⇑e.symm : (a : N) → M) ↔ f ∘ (⇑e : (a : M) → N) = g

Tactic:
e.toEquiv.eq_comp_symm f g

Premises used: MulEquiv.toEquiv, Equiv.eq_comp_symm, ContinuousMulEquiv.toMulEquiv
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
M : Type u_1
N : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace N
inst_2 : Mul M
inst_3 : Mul N
α : Type u_3
e : M ≃ₜ* N
f : N → α
g : M → α
⊢ g ∘ (⇑e.symm : (a : N) → M) = f ↔ g = f ∘ (⇑e : (a : M) → N)

Tactic:
e.toEquiv.comp_symm_eq f g

Premises used: MulEquiv.toEquiv, Equiv.comp_symm_eq, ContinuousMulEquiv.toMulEquiv
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
M : Type u_1
N : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace N
inst_2 : Mul M
inst_3 : Mul N
α : Type u_3
e : M ≃ₜ* N
f : α → M
g : α → N
⊢ f = (⇑e.symm : (a : N) → M) ∘ g ↔ (⇑e : (a : M) → N) ∘ f = g

Tactic:
e.toEquiv.eq_symm_comp f g

Premises used: Equiv.eq_symm_comp, MulEquiv.toEquiv, ContinuousMulEquiv.toMulEquiv
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
M : Type u_1
N : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace N
inst_2 : Mul M
inst_3 : Mul N
α : Type u_3
e : M ≃ₜ* N
f : α → M
g : α → N
⊢ (⇑e.symm : (a : N) → M) ∘ g = f ↔ g = (⇑e : (a : M) → N) ∘ f

Tactic:
e.toEquiv.symm_comp_eq f g

Premises used: Equiv.symm_comp_eq, MulEquiv.toEquiv, ContinuousMulEquiv.toMulEquiv
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
G : Type u
inst : TopologicalSpace G
H : Type v
inst_1 : TopologicalSpace H
M : Type u_1
N : Type u_2
inst_2 : TopologicalSpace M
inst_3 : TopologicalSpace N
inst_4 : Mul M
inst_5 : Mul N
L : Type u_3
inst_6 : Mul L
inst_7 : TopologicalSpace L
cme1 : M ≃ₜ* N
cme2 : N ≃ₜ* L
⊢ Continuous (cme2.toFun ∘ cme1.toFun)

Tactic:
Continuous.comp cme2.continuous_toFun cme1.continuous_toFun

Premises used: Continuous.comp, ContinuousMulEquiv.continuous_toFun
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
G : Type u
inst : TopologicalSpace G
H : Type v
inst_1 : TopologicalSpace H
M : Type u_1
N : Type u_2
inst_2 : TopologicalSpace M
inst_3 : TopologicalSpace N
inst_4 : Mul M
inst_5 : Mul N
L : Type u_3
inst_6 : Mul L
inst_7 : TopologicalSpace L
cme1 : M ≃ₜ* N
cme2 : N ≃ₜ* L
⊢ Continuous (cme1.trans cme2.toMulEquiv).toFun

Tactic:
convert! Continuous.comp cme2.continuous_toFun cme1.continuous_toFun

Premises used: Continuous.comp, ContinuousMulEquiv.continuous_toFun
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
G : Type u
inst : TopologicalSpace G
H : Type v
inst_1 : TopologicalSpace H
M : Type u_1
N : Type u_2
inst_2 : TopologicalSpace M
inst_3 : TopologicalSpace N
inst_4 : Mul M
inst_5 : Mul N
L : Type u_3
inst_6 : Mul L
inst_7 : TopologicalSpace L
cme1 : M ≃ₜ* N
cme2 : N ≃ₜ* L
⊢ Continuous (cme1.invFun ∘ cme2.invFun)

Tactic:
Continuous.comp cme1.continuous_invFun cme2.continuous_invFun

Premises used: Continuous.comp, ContinuousMulEquiv.continuous_invFun
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
G : Type u
inst : TopologicalSpace G
H : Type v
inst_1 : TopologicalSpace H
M : Type u_1
N : Type u_2
inst_2 : TopologicalSpace M
inst_3 : TopologicalSpace N
inst_4 : Mul M
inst_5 : Mul N
L : Type u_3
inst_6 : Mul L
inst_7 : TopologicalSpace L
cme1 : M ≃ₜ* N
cme2 : N ≃ₜ* L
⊢ Continuous (cme1.trans cme2.toMulEquiv).invFun

Tactic:
convert! Continuous.comp cme1.continuous_invFun cme2.continuous_invFun

Premises used: Continuous.comp, ContinuousMulEquiv.continuous_invFun
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
M : Type u_1
N : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace N
inst_2 : Mul M
inst_3 : Mul N
L : Type u_3
inst_4 : Mul L
inst_5 : TopologicalSpace L
e₁ : M ≃ₜ* N
e₂ : N ≃ₜ* L
⊢ Eq (α := M → L) (⇑(e₁.trans e₂) : (a : M) → L)
    (Function.comp.{u_1 + 1, u_2 + 1, u_3 + 1} (β := N) (⇑e₂ : (a : N) → L) (⇑e₁ : (a : M) → N))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
M : Type u_1
N : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace N
inst_2 : Mul M
inst_3 : Mul N
L : Type u_3
inst_4 : Mul L
inst_5 : TopologicalSpace L
e₁ : M ≃ₜ* N
e₂ : N ≃ₜ* L
m : M
⊢ Eq.{u_3 + 1} (α := L) ((e₁.trans e₂ : (a : M) → L) m : L) ((e₂ : (a : N) → L) ((e₁ : (a : M) → N) m : N) : L)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
M : Type u_1
N : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace N
inst_2 : Mul M
inst_3 : Mul N
L : Type u_3
inst_4 : Mul L
inst_5 : TopologicalSpace L
e₁ : M ≃ₜ* N
e₂ : N ≃ₜ* L
l : L
⊢ Eq.{u_1 + 1} (α := M) (((e₁.trans e₂).symm : (a : L) → M) l : M)
    ((e₁.symm : (a : N) → M) ((e₂.symm : (a : L) → N) l : N) : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
M : Type u_1
N : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace N
inst_2 : Mul M
inst_3 : Mul N
e : M ≃ₜ* N
⊢ e.symm.trans e = refl N

Tactic:
DFunLike.ext _ _ e.apply_symm_apply

Premises used: DFunLike.ext, ContinuousMulEquiv.apply_symm_apply
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
M : Type u_1
N : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace N
inst_2 : Mul M
inst_3 : Mul N
e : M ≃ₜ* N
⊢ e.trans e.symm = refl M

Tactic:
DFunLike.ext _ _ e.symm_apply_apply

Premises used: DFunLike.ext, ContinuousMulEquiv.symm_apply_apply
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
G : Type u
inst : TopologicalSpace G
H : Type v
inst_1 : TopologicalSpace H
inst_2 : Mul G
inst_3 : Mul H
e : G ≃* H
he : ∀ (s : Set H), IsOpen.{u} (X := G) ((⇑e : (a : G) → H) ⁻¹' s) ↔ IsOpen s
⊢ (↑(e.toContinuousMulEquiv he) : G ≃* H) = e

Tactic:
rfl

Premises used: MulEquivClass.toMulEquiv, EquivLike.toEquiv, rfl
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
G : Type u
inst : TopologicalSpace G
H : Type v
inst_1 : TopologicalSpace H
inst_2 : Mul G
inst_3 : Mul H
e : G ≃* H
he : ∀ (s : Set H), IsOpen.{u} (X := G) ((⇑e : (a : G) → H) ⁻¹' s) ↔ IsOpen s
⊢ (↑(e.toContinuousMulEquiv he) : G ≃ₜ H) = e.toHomeomorph he

Tactic:
rfl

Premises used: HomeomorphClass.toHomeomorph, EquivLike.toEquiv, Equiv.toHomeomorph, rfl
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
G : Type u
inst : TopologicalSpace G
H : Type v
inst_1 : TopologicalSpace H
inst_2 : Mul G
inst_3 : Mul H
e : G ≃* H
he : ∀ (s : Set H), IsOpen.{u} (X := G) ((⇑e : (a : G) → H) ⁻¹' s) ↔ IsOpen s
s : Set G
⊢ IsOpen.{v} (X := H) ((⇑e.symm : (a : H) → G) ⁻¹' s) ↔
    IsOpen.{u} (X := G) (Set.preimage.{u, v} (β := H) (⇑e : (a : G) → H) ((⇑e.symm : (a : H) → G) ⁻¹' s))

Tactic:
(he _).symm

Premises used: Iff.symm
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
G : Type u
inst : TopologicalSpace G
H : Type v
inst_1 : TopologicalSpace H
inst_2 : Mul G
inst_3 : Mul H
e : G ≃* H
he : ∀ (s : Set H), IsOpen.{u} (X := G) ((⇑e : (a : G) → H) ⁻¹' s) ↔ IsOpen s
s : Set G
h : s = Set.preimage.{u, v} (β := H) (⇑e : (a : G) → H) ((⇑e.symm : (a : H) → G) ⁻¹' s)
⊢ IsOpen.{v} (X := H) ((⇑e.symm : (a : H) → G) ⁻¹' s) ↔ IsOpen s

Tactic:
convert! (he _).symm

Premises used: Iff.symm
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
G : Type u
inst : TopologicalSpace G
H : Type v
inst_1 : TopologicalSpace H
inst_2 : Mul G
inst_3 : Mul H
e : G ≃* H
he : ∀ (s : Set H), IsOpen.{u} (X := G) ((⇑e : (a : G) → H) ⁻¹' s) ↔ IsOpen s
s : Set G
⊢ s = Set.preimage.{u, v} (β := H) (⇑e : (a : G) → H) ((⇑e.symm : (a : H) → G) ⁻¹' s)

Tactic:
(e.preimage_symm_preimage s).symm

Premises used: MulEquiv.toEquiv, Equiv.preimage_symm_preimage, Eq.symm
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
G : Type u
inst : TopologicalSpace G
H : Type v
inst_1 : TopologicalSpace H
inst_2 : Mul G
inst_3 : Mul H
e : G ≃* H
he : ∀ (s : Set H), IsOpen.{u} (X := G) ((⇑e : (a : G) → H) ⁻¹' s) ↔ IsOpen s
s : Set G
⊢ s = Set.preimage.{u, v} (β := H) (⇑e : (a : G) → H) ((⇑e.symm : (a : H) → G) ⁻¹' s)

Tactic:
exact (e.preimage_symm_preimage s).symm

Premises used: MulEquiv.toEquiv, Equiv.preimage_symm_preimage, Eq.symm
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
G : Type u
inst : TopologicalSpace G
H : Type v
inst_1 : TopologicalSpace H
inst_2 : Mul G
inst_3 : Mul H
e : G ≃* H
he : ∀ (s : Set H), IsOpen.{u} (X := G) ((⇑e : (a : G) → H) ⁻¹' s) ↔ IsOpen s
⊢ (e.toContinuousMulEquiv he).symm = e.symm.toContinuousMulEquiv ⋯

Tactic:
rfl

Premises used: MulEquiv.toContinuousMulEquiv, ContinuousMulEquiv.symm, Equiv.symm, MulEquiv.symm, rfl
-- Module: Mathlib.Topology.Algebra.Equicontinuity
Goal:
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst : TopologicalSpace G
inst_1 : UniformSpace M
inst_2 : Group G
inst_3 : Group M
inst_4 : IsTopologicalGroup G
inst_5 : IsUniformGroup M
inst_6 : FunLike hom G M
inst_7 : MonoidHomClass hom G M
F : ι → hom
hf : EquicontinuousAt.{u_1, u_2, u_3} (X := G) (α := M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F) 1
rw :
  Continuous (X := G) (Y := ι →ᵤ M)
    (comp (β := ι → M) (⇑UniformFun.ofFun : (a : ι → M) → ι →ᵤ M)
      (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F)))
⊢ Equicontinuous.{u_1, u_2, u_3} (X := G) (α := M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F)

Tactic:
rw [equicontinuous_iff_continuous]

Premises used: equicontinuous_iff_continuous
-- Module: Mathlib.Topology.Algebra.Equicontinuity
Goal:
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst : TopologicalSpace G
inst_1 : UniformSpace M
inst_2 : Group G
inst_3 : Group M
inst_4 : IsTopologicalGroup G
inst_5 : IsUniformGroup M
inst_6 : FunLike hom G M
inst_7 : MonoidHomClass hom G M
F : ι → hom
hf : EquicontinuousAt.{u_1, u_2, u_3} (X := G) (α := M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F) 1
⊢ ContinuousAt (X := G) (Y := ι →ᵤ M)
    (comp (β := ι → M) (⇑UniformFun.ofFun : (a : ι → M) → ι →ᵤ M)
      (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F)))
    1

Tactic:
rw [equicontinuousAt_iff_continuousAt] at hf

Premises used: equicontinuousAt_iff_continuousAt
-- Module: Mathlib.Topology.Algebra.Equicontinuity
Goal:
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst : TopologicalSpace G
inst_1 : UniformSpace M
inst_2 : Group G
inst_3 : Group M
inst_4 : IsTopologicalGroup G
inst_5 : IsUniformGroup M
inst_6 : FunLike hom G M
inst_7 : MonoidHomClass hom G M
F : ι → hom
hf :
  ContinuousAt (X := G) (Y := ι →ᵤ M)
    (comp (β := ι → M) (⇑UniformFun.ofFun : (a : ι → M) → ι →ᵤ M)
      (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F)))
    1
h :
  ∀ (x : ι),
    Eq.{u_3 + 1} (α := M) (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F) 1 x) (1 x)
⊢ Eq (α := ι → M) (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F) 1) 1

Tactic:
ext