awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.ContinuousAffineMap
Goal:
R : Type u_1
S : Type u_2
V : Type u_3
W : Type u_4
inst : Ring S
inst_1 : Ring R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : TopologicalSpace V
inst_5 : IsTopologicalAddGroup V
inst_6 : AddCommGroup W
inst_7 : Module R W
inst_8 : TopologicalSpace W
inst_9 : Module S W
inst_10 : SMulCommClass R S W
inst_11 : ContinuousConstSMul S W
inst_12 : IsTopologicalAddGroup W
f : V →ᴬ[R] W
⊢ Eq (α := V →L[R] W) ((decompLinearEquiv R S V W : (a : V →ᴬ[R] W) → W × (V →L[R] W)) f).2 f.contLinear

Tactic:
rfl

Premises used: ContinuousAffineMap.contLinear, rfl
-- Module: Mathlib.Topology.Algebra.ContinuousAffineMap
Goal:
R : Type u_1
S : Type u_2
V : Type u_3
W : Type u_4
inst : Ring S
inst_1 : Ring R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : TopologicalSpace V
inst_5 : IsTopologicalAddGroup V
inst_6 : AddCommGroup W
inst_7 : Module R W
inst_8 : TopologicalSpace W
inst_9 : Module S W
inst_10 : SMulCommClass R S W
inst_11 : ContinuousConstSMul S W
inst_12 : IsTopologicalAddGroup W
p : W × (V →L[R] W)
x : V
⊢ (((LinearEquiv.symm (decompLinearEquiv R S V W) : (a : W × (V →L[R] W)) → V →ᴬ[R] W) p : V →ᴬ[R] W) : (a : V) → W) x =
    HAdd.hAdd (α := W) ((p.2 : (a : V) → W) x : W) p.1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.ContinuousAffineMap
Goal:
R : Type u_1
S : Type u_2
V : Type u_3
W : Type u_4
inst : Ring S
inst_1 : Ring R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : TopologicalSpace V
inst_5 : IsTopologicalAddGroup V
inst_6 : AddCommGroup W
inst_7 : Module R W
inst_8 : TopologicalSpace W
inst_9 : Module S W
inst_10 : SMulCommClass R S W
inst_11 : ContinuousConstSMul S W
inst_12 : IsTopologicalAddGroup W
p : W × (V →L[R] W)
h :
  ∀ (x : V),
    Eq.{u_4 + 1} (α := W)
      ((contLinear (P := V) (Q := W)
              ((LinearEquiv.symm (decompLinearEquiv R S V W) : (a : W × (V →L[R] W)) → V →ᴬ[R] W) p) :
            (a : V) → W)
          x :
        W)
      ((p.2 : (a : V) → W) x : W)
⊢ contLinear (P := V) (Q := W) ((LinearEquiv.symm (decompLinearEquiv R S V W) : (a : W × (V →L[R] W)) → V →ᴬ[R] W) p) =
    p.2

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.ContinuousAffineMap
Goal:
R : Type u_1
S : Type u_2
V : Type u_3
W : Type u_4
inst : Ring S
inst_1 : Ring R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : TopologicalSpace V
inst_5 : IsTopologicalAddGroup V
inst_6 : AddCommGroup W
inst_7 : Module R W
inst_8 : TopologicalSpace W
inst_9 : Module S W
inst_10 : SMulCommClass R S W
inst_11 : ContinuousConstSMul S W
inst_12 : IsTopologicalAddGroup W
p : W × (V →L[R] W)
x : V
⊢ Eq.{u_4 + 1} (α := W)
    ((contLinear (P := V) (Q := W)
            ((LinearEquiv.symm (decompLinearEquiv R S V W) : (a : W × (V →L[R] W)) → V →ᴬ[R] W) p) :
          (a : V) → W)
        x :
      W)
    ((p.2 : (a : V) → W) x : W)

Tactic:
simp [decompLinearEquiv]

Premises used: ContinuousAffineMap.decompLinearEquiv
-- Module: Mathlib.Topology.Algebra.ContinuousAffineMap
Goal:
R : Type u_1
S : Type u_2
V : Type u_3
W : Type u_4
Q : Type u_5
inst : Ring S
inst_1 : Ring R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : TopologicalSpace V
inst_5 : IsTopologicalAddGroup V
inst_6 : AddCommGroup W
inst_7 : Module R W
inst_8 : TopologicalSpace W
inst_9 : Module S W
inst_10 : SMulCommClass R S W
inst_11 : ContinuousConstSMul S W
inst_12 : AddTorsor W Q
inst_13 : TopologicalSpace Q
inst_14 : IsTopologicalAddGroup W
inst_15 : IsTopologicalAddTorsor Q
f : V →ᴬ[R] Q
⊢ Eq.{u_5 + 1} (α := Q) (((decompAffineEquiv R S V Q : (a : V →ᴬ[R] Q) → Q × (V →L[R] W)) f).1 : Q)
    ((f : (a : V) → Q) 0 : Q)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.ContinuousAffineMap
Goal:
R : Type u_1
S : Type u_2
V : Type u_3
W : Type u_4
Q : Type u_5
inst : Ring S
inst_1 : Ring R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : TopologicalSpace V
inst_5 : IsTopologicalAddGroup V
inst_6 : AddCommGroup W
inst_7 : Module R W
inst_8 : TopologicalSpace W
inst_9 : Module S W
inst_10 : SMulCommClass R S W
inst_11 : ContinuousConstSMul S W
inst_12 : AddTorsor W Q
inst_13 : TopologicalSpace Q
inst_14 : IsTopologicalAddGroup W
inst_15 : IsTopologicalAddTorsor Q
f : V →ᴬ[R] Q
⊢ Eq (α := V →L[R] W) ((decompAffineEquiv R S V Q : (a : V →ᴬ[R] Q) → Q × (V →L[R] W)) f).2 f.contLinear

Tactic:
rfl

Premises used: ContinuousAffineMap.contLinear, rfl
-- Module: Mathlib.Topology.Algebra.ContinuousAffineMap
Goal:
R : Type u_1
S : Type u_2
V : Type u_3
W : Type u_4
Q : Type u_5
inst : Ring S
inst_1 : Ring R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : TopologicalSpace V
inst_5 : IsTopologicalAddGroup V
inst_6 : AddCommGroup W
inst_7 : Module R W
inst_8 : TopologicalSpace W
inst_9 : Module S W
inst_10 : SMulCommClass R S W
inst_11 : ContinuousConstSMul S W
inst_12 : AddTorsor W Q
inst_13 : TopologicalSpace Q
inst_14 : IsTopologicalAddGroup W
inst_15 : IsTopologicalAddTorsor Q
p : Q × (V →L[R] W)
x : V
⊢ (((AffineEquiv.symm (decompAffineEquiv R S V Q) : (a : Q × (V →L[R] W)) → V →ᴬ[R] Q) p : V →ᴬ[R] Q) : (a : V) → Q) x =
    HVAdd.hVAdd.{u_4, u_5, u_5} (α := W) ((p.2 : (a : V) → W) x : W) p.1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.ContinuousAffineMap
Goal:
R : Type u_1
S : Type u_2
V : Type u_3
W : Type u_4
Q : Type u_5
inst : Ring S
inst_1 : Ring R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : TopologicalSpace V
inst_5 : IsTopologicalAddGroup V
inst_6 : AddCommGroup W
inst_7 : Module R W
inst_8 : TopologicalSpace W
inst_9 : Module S W
inst_10 : SMulCommClass R S W
inst_11 : ContinuousConstSMul S W
inst_12 : AddTorsor W Q
inst_13 : TopologicalSpace Q
inst_14 : IsTopologicalAddGroup W
inst_15 : IsTopologicalAddTorsor Q
p : Q × (V →L[R] W)
rw :
  contLinear.{u_1, u_3, u_4, u_3, u_5} (P := V) (Q := Q)
      ((AffineEquiv.symm { toEquiv := decompEquiv R V Q, linear := decompLinearEquiv R S V W, map_vadd' := ⋯ } :
          (a : Q × (V →L[R] W)) → V →ᴬ[R] Q)
        p) =
    p.2
rw₁ :
  contLinear.{u_1, u_3, u_4, u_3, u_5} (P := V) (Q := Q)
      ((Equiv.symm
            (AffineEquiv.toEquiv (k := S)
              { toEquiv := decompEquiv R V Q, linear := decompLinearEquiv R S V W, map_vadd' := ⋯ }) :
          (a : Q × (V →L[R] W)) → V →ᴬ[R] Q)
        p) =
    p.2
rw₂ rw₃ : p.2 = p.2
⊢ contLinear.{u_1, u_3, u_4, u_3, u_5} (P := V) (Q := Q)
      ((AffineEquiv.symm (decompAffineEquiv R S V Q) : (a : Q × (V →L[R] W)) → V →ᴬ[R] Q) p) =
    p.2

Tactic:
rw [decompAffineEquiv, ← AffineEquiv.coe_symm_toEquiv, decompEquiv_symm_contLinear]

Premises used: AffineEquiv.coe_symm_toEquiv, ContinuousAffineMap.decompEquiv_symm_contLinear, ContinuousAffineMap.decompAffineEquiv
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst : Monoid A
inst_1 : Monoid B
inst_2 : Monoid C
inst_3 : Monoid D
inst_4 : TopologicalSpace A
inst_5 : TopologicalSpace B
inst_6 : TopologicalSpace C
inst_7 : TopologicalSpace D
f g : A →ₜ* B
h :
  Eq (α := (a : A) → B) ((fun (f : A →ₜ* B) ↦ (↑f.toMonoidHom : OneHom A B).toFun) f)
    ((fun (f : A →ₜ* B) ↦ (↑f.toMonoidHom : OneHom A B).toFun) g)
obtain :
  ∀ (toFun : A → B) (map_one' : toFun 1 = 1)
    (map_mul' :
      ∀ (x y : A),
        { toFun := toFun, map_one' := map_one' : OneHom A B }.toFun (x * y) =
          { toFun := toFun, map_one' := map_one' : OneHom A B }.toFun x *
            { toFun := toFun, map_one' := map_one' : OneHom A B }.toFun y)
    (continuous_toFun :
      Continuous[inst_4, inst_5]
        (↑{ toFun := toFun, map_one' := map_one', map_mul' := map_mul' : A →* B } : OneHom A B).toFun)
    (h :
      Eq (α := (a : A) → B)
        ((fun (f : A →ₜ* B) ↦ (↑f.toMonoidHom : OneHom A B).toFun)
          { toFun := toFun, map_one' := map_one', map_mul' := map_mul', continuous_toFun := continuous_toFun })
        ((fun (f : A →ₜ* B) ↦ (↑f.toMonoidHom : OneHom A B).toFun) g)),
    { toFun := toFun, map_one' := map_one', map_mul' := map_mul', continuous_toFun := continuous_toFun : A →ₜ* B } = g
⊢ f = g

Tactic:
obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := f
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst : Monoid A
inst_1 : Monoid B
inst_2 : Monoid C
inst_3 : Monoid D
inst_4 : TopologicalSpace A
inst_5 : TopologicalSpace B
inst_6 : TopologicalSpace C
inst_7 : TopologicalSpace D
g : A →ₜ* B
toFun : A → B
map_one' : toFun 1 = 1
map_mul' :
  ∀ (x y : A),
    { toFun := toFun, map_one' := map_one' : OneHom A B }.toFun (x * y) =
      { toFun := toFun, map_one' := map_one' : OneHom A B }.toFun x *
        { toFun := toFun, map_one' := map_one' : OneHom A B }.toFun y
continuous_toFun :
  Continuous[inst_4, inst_5]
    (↑{ toFun := toFun, map_one' := map_one', map_mul' := map_mul' : A →* B } : OneHom A B).toFun
h :
  Eq (α := (a : A) → B)
    ((fun (f : A →ₜ* B) ↦ (↑f.toMonoidHom : OneHom A B).toFun)
      { toFun := toFun, map_one' := map_one', map_mul' := map_mul', continuous_toFun := continuous_toFun })
    ((fun (f : A →ₜ* B) ↦ (↑f.toMonoidHom : OneHom A B).toFun) g)
obtain :
  ∀ (toFun_1 : A → B) (map_one'_1 : toFun_1 1 = 1)
    (map_mul'_1 :
      ∀ (x y : A),
        { toFun := toFun_1, map_one' := map_one'_1 : OneHom A B }.toFun (x * y) =
          { toFun := toFun_1, map_one' := map_one'_1 : OneHom A B }.toFun x *
            { toFun := toFun_1, map_one' := map_one'_1 : OneHom A B }.toFun y)
    (continuous_toFun_1 :
      Continuous[inst_4, inst_5]
        (↑{ toFun := toFun_1, map_one' := map_one'_1, map_mul' := map_mul'_1 : A →* B } : OneHom A B).toFun)
    (h :
      Eq (α := (a : A) → B)
        ((fun (f : A →ₜ* B) ↦ (↑f.toMonoidHom : OneHom A B).toFun)
          { toFun := toFun, map_one' := map_one', map_mul' := map_mul', continuous_toFun := continuous_toFun })
        ((fun (f : A →ₜ* B) ↦ (↑f.toMonoidHom : OneHom A B).toFun)
          { toFun := toFun_1, map_one' := map_one'_1, map_mul' := map_mul'_1,
            continuous_toFun := continuous_toFun_1 })),
    { toFun := toFun, map_one' := map_one', map_mul' := map_mul', continuous_toFun := continuous_toFun : A →ₜ* B } =
      { toFun := toFun_1, map_one' := map_one'_1, map_mul' := map_mul'_1, continuous_toFun := continuous_toFun_1 }
⊢ { toFun := toFun, map_one' := map_one', map_mul' := map_mul', continuous_toFun := continuous_toFun : A →ₜ* B } = g

Tactic:
obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := g
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst : Monoid A
inst_1 : Monoid B
inst_2 : Monoid C
inst_3 : Monoid D
inst_4 : TopologicalSpace A
inst_5 : TopologicalSpace B
inst_6 : TopologicalSpace C
inst_7 : TopologicalSpace D
toFun : A → B
map_one' : toFun 1 = 1
map_mul' :
  ∀ (x y : A),
    { toFun := toFun, map_one' := map_one' : OneHom A B }.toFun (x * y) =
      { toFun := toFun, map_one' := map_one' : OneHom A B }.toFun x *
        { toFun := toFun, map_one' := map_one' : OneHom A B }.toFun y
continuous_toFun :
  Continuous[inst_4, inst_5]
    (↑{ toFun := toFun, map_one' := map_one', map_mul' := map_mul' : A →* B } : OneHom A B).toFun
toFun_1 : A → B
map_one'_1 : toFun_1 1 = 1
map_mul'_1 :
  ∀ (x y : A),
    { toFun := toFun_1, map_one' := map_one'_1 : OneHom A B }.toFun (x * y) =
      { toFun := toFun_1, map_one' := map_one'_1 : OneHom A B }.toFun x *
        { toFun := toFun_1, map_one' := map_one'_1 : OneHom A B }.toFun y
continuous_toFun_1 :
  Continuous[inst_4, inst_5]
    (↑{ toFun := toFun_1, map_one' := map_one'_1, map_mul' := map_mul'_1 : A →* B } : OneHom A B).toFun
h :
  Eq (α := (a : A) → B)
    ((fun (f : A →ₜ* B) ↦ (↑f.toMonoidHom : OneHom A B).toFun)
      { toFun := toFun, map_one' := map_one', map_mul' := map_mul', continuous_toFun := continuous_toFun })
    ((fun (f : A →ₜ* B) ↦ (↑f.toMonoidHom : OneHom A B).toFun)
      { toFun := toFun_1, map_one' := map_one'_1, map_mul' := map_mul'_1, continuous_toFun := continuous_toFun_1 })
⊢ { toFun := toFun, map_one' := map_one', map_mul' := map_mul', continuous_toFun := continuous_toFun : A →ₜ* B } =
    { toFun := toFun_1, map_one' := map_one'_1, map_mul' := map_mul'_1, continuous_toFun := continuous_toFun_1 }

Tactic:
congr
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
A : Type u_2
B : Type u_3
inst : Monoid A
inst_1 : Monoid B
inst_2 : TopologicalSpace A
inst_3 : TopologicalSpace B
f : A →ₜ* B
⊢ f.toMonoidHom = (↑f : A →* B)

Tactic:
rfl

Premises used: MonoidHomClass.toMonoidHom, rfl
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
A : Type u_2
B : Type u_3
inst : Monoid A
inst_1 : Monoid B
inst_2 : TopologicalSpace A
inst_3 : TopologicalSpace B
f : A →ₜ* B
⊢ f.toContinuousMap = (↑f : C(A, B))

Tactic:
rfl

Premises used: toContinuousMap, rfl
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
F_1 : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst : Monoid A
inst_1 : Monoid B
inst_2 : Monoid C
inst_3 : Monoid D
inst_4 : TopologicalSpace A
inst_5 : TopologicalSpace B
inst_6 : TopologicalSpace C
inst_7 : TopologicalSpace D
F : Type u_7
inst_8 : FunLike F A B
inst_9 : MonoidHomClass F A B
inst_10 : ContinuousMapClass F A B
f : F
dsimp : Continuous[inst_4, inst_5] (⇑f : (a : A) → B)
⊢ Continuous[inst_4, inst_5] (OneHom.toFun (↑(↑f : A →* B) : OneHom A B))

Tactic:
dsimp
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
F_1 : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst : Monoid A
inst_1 : Monoid B
inst_2 : Monoid C
inst_3 : Monoid D
inst_4 : TopologicalSpace A
inst_5 : TopologicalSpace B
inst_6 : TopologicalSpace C
inst_7 : TopologicalSpace D
F : Type u_7
inst_8 : FunLike F A B
inst_9 : MonoidHomClass F A B
inst_10 : ContinuousMapClass F A B
f : F
⊢ Continuous[inst_4, inst_5] (⇑f : (a : A) → B)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
A : Type u_2
B : Type u_3
inst : Monoid A
inst_1 : Monoid B
inst_2 : TopologicalSpace A
inst_3 : TopologicalSpace B
F : Type u_7
inst_4 : FunLike F A B
inst_5 : MonoidHomClass F A B
inst_6 : ContinuousMapClass F A B
f : F
⊢ Eq (α := (a : A) → B) (⇑(↑f : A →ₜ* B) : (a : A) → B) (⇑f : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
A : Type u_2
B : Type u_3
inst : Monoid A
inst_1 : Monoid B
inst_2 : TopologicalSpace A
inst_3 : TopologicalSpace B
F : Type u_7
inst_4 : FunLike F A B
inst_5 : MonoidHomClass F A B
inst_6 : ContinuousMapClass F A B
f : F
⊢ Eq (α := A →* B) (↑(↑f : A →ₜ* B) : A →* B) (↑f : A →* B)

Tactic:
rfl

Premises used: ContinuousMonoidHom.toContinuousMonoidHom, MonoidHomClass.toMonoidHom, rfl
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
A : Type u_2
B : Type u_3
inst : Monoid A
inst_1 : Monoid B
inst_2 : TopologicalSpace A
inst_3 : TopologicalSpace B
F : Type u_7
inst_4 : FunLike F A B
inst_5 : MonoidHomClass F A B
inst_6 : ContinuousMapClass F A B
f : F
⊢ Eq (α := C(A, B)) (↑(↑f : A →ₜ* B) : C(A, B)) (↑f : C(A, B))

Tactic:
rfl

Premises used: ContinuousMonoidHom.toContinuousMonoidHom, toContinuousMap, rfl
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
A : Type u_2
B : Type u_3
inst : Monoid A
inst_1 : Monoid B
inst_2 : TopologicalSpace A
inst_3 : TopologicalSpace B
f g : A →ₜ* B
h : ∀ (x : A), Eq.{u_3 + 1} (α := B) ((f : (a : A) → B) x : B) ((g : (a : A) → B) x : B)
⊢ f = g

Tactic:
DFunLike.ext _ _ h

Premises used: DFunLike.ext
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
A : Type u_2
B : Type u_3
inst : Monoid A
inst_1 : Monoid B
inst_2 : TopologicalSpace A
inst_3 : TopologicalSpace B
f g : A →ₜ* B
h : f.toContinuousMap = g.toContinuousMap
⊢ ∀ (x : A), Eq.{u_3 + 1} (α := B) ((f.toContinuousMap : (a : A) → B) x : B) ((g.toContinuousMap : (a : A) → B) x : B)

Tactic:
DFunLike.ext_iff.1 h

Premises used: DFunLike.ext_iff, Iff.mp
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
A : Type u_2
B : Type u_3
inst : Monoid A
inst_1 : Monoid B
inst_2 : TopologicalSpace A
inst_3 : TopologicalSpace B
f g : A →ₜ* B
h : f.toContinuousMap = g.toContinuousMap
⊢ ∀ (x : A), Eq.{u_3 + 1} (α := B) ((f : (a : A) → B) x : B) ((g : (a : A) → B) x : B)

Tactic:
convert! DFunLike.ext_iff.1 h

Premises used: DFunLike.ext_iff, Iff.mp
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
A : Type u_2
B : Type u_3
inst : Monoid A
inst_1 : Monoid B
inst_2 : TopologicalSpace A
inst_3 : TopologicalSpace B
f g : A →ₜ* B
h : f.toMonoidHom = g.toMonoidHom
⊢ ∀ (x : A), Eq.{u_3 + 1} (α := B) ((f.toMonoidHom : (a : A) → B) x : B) ((g.toMonoidHom : (a : A) → B) x : B)

Tactic:
DFunLike.ext_iff.1 h

Premises used: DFunLike.ext_iff, Iff.mp
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
A : Type u_2
B : Type u_3
inst : Monoid A
inst_1 : Monoid B
inst_2 : TopologicalSpace A
inst_3 : TopologicalSpace B
f g : A →ₜ* B
h : f.toMonoidHom = g.toMonoidHom
⊢ ∀ (x : A), Eq.{u_3 + 1} (α := B) ((f : (a : A) → B) x : B) ((g : (a : A) → B) x : B)

Tactic:
convert! DFunLike.ext_iff.1 h

Premises used: DFunLike.ext_iff, Iff.mp
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
A : Type u_2
B : Type u_3
C : Type u_4
inst : Monoid A
inst_1 : Monoid B
inst_2 : Monoid C
inst_3 : TopologicalSpace A
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
g : B →ₜ* C
f : A →ₜ* B
⊢ Eq (α := (a : A) → C) (⇑(g.comp f) : (a : A) → C)
    (Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := B) (⇑g : (a : B) → C) (⇑f : (a : A) → B))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
A : Type u_2
B : Type u_3
inst : Monoid A
inst_1 : Monoid B
inst_2 : TopologicalSpace A
inst_3 : TopologicalSpace B
⊢ Eq (α := (a : A) → B) (⇑1 : (a : A) → B) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
A : Type u_2
inst : Monoid A
inst_1 : TopologicalSpace A
⊢ Eq (α := (a : A) → A) (⇑(id A) : (a : A) → A) _root_.id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
A : Type u_2
E : Type u_6
inst : Monoid A
inst_1 : TopologicalSpace A
inst_2 : CommMonoid E
inst_3 : TopologicalSpace E
inst_4 : ContinuousMul E
f g : A →ₜ* E
a : A
⊢ (f * g : (a : A) → E) a = HMul.hMul (α := E) (β := E) ((f : (a : A) → E) a : E) ((g : (a : A) → E) a : E)

Tactic:
rfl
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
A : Type u_2
E : Type u_6
inst : Monoid A
inst_1 : TopologicalSpace A
inst_2 : CommMonoid E
inst_3 : TopologicalSpace E
inst_4 : ContinuousMul E
f : A →ₜ* E
n : ℕ
a : A
induction : (HPow.hPow (β := ℕ) f 0 : (a : A) → E) a = HPow.hPow (α := E) (β := ℕ) ((f : (a : A) → E) a : E) 0
succ :
  ∀ (n : ℕ),
    (f ^ n : (a : A) → E) a = HPow.hPow (α := E) ((f : (a : A) → E) a : E) n →
      (f ^ (n + 1) : (a : A) → E) a = HPow.hPow (α := E) ((f : (a : A) → E) a : E) (n + 1)
⊢ (f ^ n : (a : A) → E) a = HPow.hPow (α := E) ((f : (a : A) → E) a : E) n

Tactic:
induction n
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
A : Type u_2
E : Type u_6
inst : Monoid A
inst_1 : TopologicalSpace A
inst_2 : CommMonoid E
inst_3 : TopologicalSpace E
inst_4 : ContinuousMul E
f : A →ₜ* E
a : A
rw : (1 : (a : A) → E) a = HPow.hPow (α := E) (β := ℕ) ((f : (a : A) → E) a : E) 0
rw₁ : Eq.{u_6 + 1} (α := E) ((1 : (a : A) → E) a : E) (1 : E)
rw₂ rw₃ : Eq.{u_6 + 1} (α := E) 1 1
⊢ (HPow.hPow (β := ℕ) f 0 : (a : A) → E) a = HPow.hPow (α := E) (β := ℕ) ((f : (a : A) → E) a : E) 0

Tactic:
rw [pow_zero, pow_zero, one_toFun]

Premises used: pow_zero, ContinuousMonoidHom.one_toFun
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
A : Type u_2
E : Type u_6
inst : Monoid A
inst_1 : TopologicalSpace A
inst_2 : CommMonoid E
inst_3 : TopologicalSpace E
inst_4 : ContinuousMul E
f : A →ₜ* E
a : A
⊢ (HPow.hPow (β := ℕ) f 0 : (a : A) → E) a = HPow.hPow (α := E) (β := ℕ) ((f : (a : A) → E) a : E) 0

Tactic:
case zero => rw [pow_zero, pow_zero, one_toFun]

Premises used: pow_zero, ContinuousMonoidHom.one_toFun
-- Module: Mathlib.Topology.Algebra.ContinuousMonoidHom
Goal:
A : Type u_2
E : Type u_6
inst : Monoid A
inst_1 : TopologicalSpace A
inst_2 : CommMonoid E
inst_3 : TopologicalSpace E
inst_4 : ContinuousMul E
f : A →ₜ* E
a : A
n : ℕ
ih : (f ^ n : (a : A) → E) a = HPow.hPow (α := E) ((f : (a : A) → E) a : E) n
rw : (f ^ n * f : (a : A) → E) a = HPow.hPow (α := E) ((f : (a : A) → E) a : E) (n + 1)
rw₁ :
  (f ^ n * f : (a : A) → E) a =
    HMul.hMul (β := E) (HPow.hPow (α := E) ((f : (a : A) → E) a : E) n) ((f : (a : A) → E) a : E)
rw₂ :
  HMul.hMul (α := E) (β := E) ((f ^ n : (a : A) → E) a : E) ((f : (a : A) → E) a : E) =
    HMul.hMul (β := E) (HPow.hPow (α := E) ((f : (a : A) → E) a : E) n) ((f : (a : A) → E) a : E)
rw₃ rw₄ :
  HMul.hMul (β := E) (HPow.hPow (α := E) ((f : (a : A) → E) a : E) n) ((f : (a : A) → E) a : E) =
    HMul.hMul (β := E) (HPow.hPow (α := E) ((f : (a : A) → E) a : E) n) ((f : (a : A) → E) a : E)
⊢ (f ^ (n + 1) : (a : A) → E) a = HPow.hPow (α := E) ((f : (a : A) → E) a : E) (n + 1)

Tactic:
rw [pow_succ, pow_succ, ContinuousMonoidHom.mul_apply, ih]

Premises used: pow_succ, ContinuousMonoidHom.mul_apply
-- 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
f g : M ≃ₜ* N
h₁ : f.toFun = g.toFun
h₂ : f.invFun = g.invFun
mk :
  ∀ (toMulEquiv : M ≃* N) (continuous_toFun : Continuous toMulEquiv.toFun)
    (continuous_invFun : Continuous toMulEquiv.invFun)
    (h₁ :
      { toMulEquiv := toMulEquiv, continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun :
            M ≃ₜ* N }.toFun =
        g.toFun)
    (h₂ :
      { toMulEquiv := toMulEquiv, continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun :
            M ≃ₜ* N }.invFun =
        g.invFun),
    { toMulEquiv := toMulEquiv, continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun :
        M ≃ₜ* N } =
      g
⊢ f = g

Tactic:
cases f
-- 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
g : M ≃ₜ* N
toMulEquiv : M ≃* N
continuous_toFun : Continuous toMulEquiv.toFun
continuous_invFun : Continuous toMulEquiv.invFun
h₁ :
  { toMulEquiv := toMulEquiv, continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun :
        M ≃ₜ* N }.toFun =
    g.toFun
h₂ :
  { toMulEquiv := toMulEquiv, continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun :
        M ≃ₜ* N }.invFun =
    g.invFun
mk :
  ∀ (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, continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun :
        M ≃ₜ* N } =
      { toMulEquiv := toMulEquiv_1, continuous_toFun := continuous_toFun_1, continuous_invFun := continuous_invFun_1 }
⊢ { toMulEquiv := toMulEquiv, continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun : M ≃ₜ* N } =
    g

Tactic:
cases g