awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousAffineMap (goal)
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 : IsTopologicalAddTorsor Q
f : V →ᴬ[R] Q
x : V
h h₁ :
  Eq.{u_5 + 1} (α := Q)
    ((HVAdd.hVAdd (α := V →ᴬ[R] W) (β := V →ᴬ[R] Q) (ContinuousLinearMap.toContinuousAffineMap f.contLinear)
            (const R V ((f : (a : V) → Q) 0) : V →ᴬ[R] Q) :
          (a : V) → Q)
        x :
      Q)
    ((f : (a : V) → Q) x : Q)
h₂ :
  HVAdd.hVAdd.{u_4, u_5, u_5} (α := W) (β := Q)
      ((ContinuousLinearMap.toContinuousAffineMap f.contLinear : (a : V) → W) x : W)
      (((const R V ((f : (a : V) → Q) 0) : V →ᴬ[R] Q) : (a : V) → Q) x : Q) =
    (f : (a : V) → Q) x
h₃ :
  HVAdd.hVAdd.{u_4, u_5, u_5} (α := W) (β := Q) ((f.contLinear : (a : V) → W) x : W)
      (((const R V ((f : (a : V) → Q) 0) : V →ᴬ[R] Q) : (a : V) → Q) x : Q) =
    (f : (a : V) → Q) x
h₄ :
  HVAdd.hVAdd.{u_4, u_5, u_5} (α := W) (β := Q) ((f.contLinear : (a : V) → W) x : W)
      (Function.const V ((f : (a : V) → Q) 0) x : Q) =
    (f : (a : V) → Q) x
h₅ :
  HVAdd.hVAdd.{u_4, u_5, u_5} (α := W) (β := Q) ((f.contLinear : (a : V) → W) x : W) ((f : (a : V) → Q) 0 : Q) =
    (f : (a : V) → Q) x
h₆ : Eq.{u_5 + 1} (α := Q) ((f : (a : V) → Q) (HVAdd.hVAdd (β := V) x 0) : Q) ((f : (a : V) → Q) x : Q)
⊢ Eq.{u_5 + 1} (α := Q)
    (((fun (p : Q × (V →L[R] W)) ↦ HVAdd.hVAdd (β := V →ᴬ[R] Q) p.2.toContinuousAffineMap (const R V p.1))
            ((fun (f : V →ᴬ[R] Q) ↦ (((f : (a : V) → Q) 0, f.contLinear) : Q × (V →L[R] W))) f) :
          (a : V) → Q)
        x :
      Q)
    ((f : (a : V) → Q) x : Q)
have h₇ : Eq.{u_5 + 1} (α := Q) ((f : (a : V) → Q) (x + 0) : Q) ((f : (a : V) → Q) x : Q)
Tactic: simp_rw [vadd_apply, f.contLinear.coe_toContinuousAffineMap, coe_const, Function.const_apply,
      ← f.map_vadd, vadd_eq_add, add_zero]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousAffineMap (hypothesis)
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 : IsTopologicalAddTorsor Q
⊢ Function.RightInverse
    (fun (p : Q × (V →L[R] W)) ↦ HVAdd.hVAdd (β := V →ᴬ[R] Q) p.2.toContinuousAffineMap (const R V p.1))
    fun (f : V →ᴬ[R] Q) ↦ ((f : (a : V) → Q) 0, f.contLinear)
have this : IsTopologicalAddGroup W
Tactic: haveI := IsTopologicalAddTorsor.to_isTopologicalAddGroup W Q
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousAffineMap (goal)
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 : IsTopologicalAddTorsor Q
this : IsTopologicalAddGroup W
v : Q
f : V →L[R] W
⊢ (fun (f : V →ᴬ[R] Q) ↦ (((f : (a : V) → Q) 0, f.contLinear) : Q × (V →L[R] W)))
      ((fun (p : Q × (V →L[R] W)) ↦ HVAdd.hVAdd (β := V →ᴬ[R] Q) p.2.toContinuousAffineMap (const R V p.1)) (v, f)) =
    (v, f)
have fst : ((fun (f : V →ᴬ[R] Q) ↦ (((f : (a : V) → Q) 0, f.contLinear) : Q × (V →L[R] W)))
      ((fun (p : Q × (V →L[R] W)) ↦ HVAdd.hVAdd (β := V →ᴬ[R] Q) p.2.toContinuousAffineMap (const R V p.1)) (v, f))).1 =
  (v, f).1
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousAffineMap (goal)
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 : IsTopologicalAddTorsor Q
this : IsTopologicalAddGroup W
v : Q
f : V →L[R] W
fst :
  ((fun (f : V →ᴬ[R] Q) ↦ (((f : (a : V) → Q) 0, f.contLinear) : Q × (V →L[R] W)))
        ((fun (p : Q × (V →L[R] W)) ↦ HVAdd.hVAdd (β := V →ᴬ[R] Q) p.2.toContinuousAffineMap (const R V p.1))
          (v, f))).1 =
    (v, f).1
⊢ (fun (f : V →ᴬ[R] Q) ↦ (((f : (a : V) → Q) 0, f.contLinear) : Q × (V →L[R] W)))
      ((fun (p : Q × (V →L[R] W)) ↦ HVAdd.hVAdd (β := V →ᴬ[R] Q) p.2.toContinuousAffineMap (const R V p.1)) (v, f)) =
    (v, f)
have snd : ∀ (x : V),
  Eq.{u_4 + 1} (α := W)
    ((((fun (f : V →ᴬ[R] Q) ↦ (((f : (a : V) → Q) 0, f.contLinear) : Q × (V →L[R] W)))
              ((fun (p : Q × (V →L[R] W)) ↦ HVAdd.hVAdd (β := V →ᴬ[R] Q) p.2.toContinuousAffineMap (const R V p.1))
                (v, f))).2 :
          (a : V) → W)
        x :
      W)
    (((v, f).2 : (a : V) → W) x : W)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousAffineMap (hypothesis)
Goal:
R : Type u_1
V : Type u_3
W : Type u_4
Q : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalAddGroup V
inst_5 : AddCommGroup W
inst_6 : Module R W
inst_7 : TopologicalSpace W
inst_8 : AddTorsor W Q
inst_9 : TopologicalSpace Q
inst_10 : IsTopologicalAddTorsor Q
p : Q × (V →L[R] W)
⊢ contLinear.{u_1, u_3, u_4, u_3, u_5} (P := V) (Q := Q)
      ((Equiv.symm (decompEquiv R V Q) : (a : Q × (V →L[R] W)) → V →ᴬ[R] Q) p) =
    p.2
have this : IsTopologicalAddGroup W
Tactic: haveI := IsTopologicalAddTorsor.to_isTopologicalAddGroup W Q
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousAffineMap (goal)
Goal:
R : Type u_1
V : Type u_3
W : Type u_4
Q : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalAddGroup V
inst_5 : AddCommGroup W
inst_6 : Module R W
inst_7 : TopologicalSpace W
inst_8 : AddTorsor W Q
inst_9 : TopologicalSpace Q
inst_10 : IsTopologicalAddTorsor Q
p : Q × (V →L[R] W)
this : IsTopologicalAddGroup W
⊢ contLinear.{u_1, u_3, u_4, u_3, u_5} (P := V) (Q := Q)
      ((Equiv.symm (decompEquiv R V Q) : (a : Q × (V →L[R] W)) → V →ᴬ[R] Q) p) =
    p.2
have h : ∀ (x : V),
  Eq.{u_4 + 1} (α := W)
    ((contLinear.{u_1, u_3, u_4, u_3, u_5} (P := V) (Q := Q)
            ((Equiv.symm (decompEquiv R V Q) : (a : Q × (V →L[R] W)) → V →ᴬ[R] Q) p) :
          (a : V) → W)
        x :
      W)
    ((p.2 : (a : V) → W) x : W)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousAffineMap (goal)
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)
⊢ contLinear (P := V) (Q := W) ((LinearEquiv.symm (decompLinearEquiv R S V W) : (a : W × (V →L[R] W)) → V →ᴬ[R] W) p) =
    p.2
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousAffineMap (goal)
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)
⊢ 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
have 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' := sorry } :
        (a : Q × (V →L[R] W)) → V →ᴬ[R] Q)
      p) =
  p.2
Tactic: rw [decompAffineEquiv, ← AffineEquiv.coe_symm_toEquiv, decompEquiv_symm_contLinear]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousAffineMap (goal)
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
⊢ 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
have 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' := sorry }) :
        (a : Q × (V →L[R] W)) → V →ᴬ[R] Q)
      p) =
  p.2
Tactic: rw [decompAffineEquiv, ← AffineEquiv.coe_symm_toEquiv, decompEquiv_symm_contLinear]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousAffineMap (goal)
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
⊢ 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
have rw₂ : p.2 = p.2
Tactic: rw [decompAffineEquiv, ← AffineEquiv.coe_symm_toEquiv, decompEquiv_symm_contLinear]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousMonoidHom (goal)
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)
⊢ f = g
have 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
Tactic: obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousMonoidHom (goal)
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)
⊢ { toFun := toFun, map_one' := map_one', map_mul' := map_mul', continuous_toFun := continuous_toFun : A →ₜ* B } = g
have 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 }
Tactic: obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousMonoidHom (goal)
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] (OneHom.toFun (↑(↑f : A →* B) : OneHom A B))
have dsimp : Continuous[inst_4, inst_5] (⇑f : (a : A) → B)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousMonoidHom (goal)
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
⊢ (f ^ n : (a : A) → E) a = HPow.hPow (α := E) ((f : (a : A) → E) a : E) n
have induction : (HPow.hPow (β := ℕ) f 0 : (a : A) → E) a = HPow.hPow (α := E) (β := ℕ) ((f : (a : A) → E) a : E) 0
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousMonoidHom (goal)
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
⊢ (f ^ n : (a : A) → E) a = HPow.hPow (α := E) ((f : (a : A) → E) a : E) n
have 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)
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousMonoidHom (goal)
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
have rw : (1 : (a : A) → E) a = HPow.hPow (α := E) (β := ℕ) ((f : (a : A) → E) a : E) 0
Tactic: rw [pow_zero, pow_zero, one_toFun]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousMonoidHom (goal)
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
⊢ (HPow.hPow (β := ℕ) f 0 : (a : A) → E) a = HPow.hPow (α := E) (β := ℕ) ((f : (a : A) → E) a : E) 0
have rw₁ : Eq.{u_6 + 1} (α := E) ((1 : (a : A) → E) a : E) (1 : E)
Tactic: rw [pow_zero, pow_zero, one_toFun]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousMonoidHom (goal)
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)
⊢ (HPow.hPow (β := ℕ) f 0 : (a : A) → E) a = HPow.hPow (α := E) (β := ℕ) ((f : (a : A) → E) a : E) 0
have rw₂ : Eq.{u_6 + 1} (α := E) 1 1
Tactic: rw [pow_zero, pow_zero, one_toFun]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousMonoidHom (goal)
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
⊢ (f ^ (n + 1) : (a : A) → E) a = HPow.hPow (α := E) ((f : (a : A) → E) a : E) (n + 1)
have rw : (f ^ n * f : (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]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousMonoidHom (goal)
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)
⊢ (f ^ (n + 1) : (a : A) → E) a = HPow.hPow (α := E) ((f : (a : A) → E) a : E) (n + 1)
have 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)
Tactic: rw [pow_succ, pow_succ, ContinuousMonoidHom.mul_apply, ih]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousMonoidHom (goal)
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)
⊢ (f ^ (n + 1) : (a : A) → E) a = HPow.hPow (α := E) ((f : (a : A) → E) a : E) (n + 1)
have 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)
Tactic: rw [pow_succ, pow_succ, ContinuousMonoidHom.mul_apply, ih]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousMonoidHom (goal)
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)
⊢ (f ^ (n + 1) : (a : A) → E) a = HPow.hPow (α := E) ((f : (a : A) → E) a : E) (n + 1)
have 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)
Tactic: rw [pow_succ, pow_succ, ContinuousMonoidHom.mul_apply, ih]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousMonoidHom (goal)
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
⊢ f = g
have 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
Tactic: cases f
Cleared hypotheses: f, h₁, h₂