awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : CommRing 𝕜
inst_1 : NoZeroDivisors 𝕜
inst_2 : TopologicalSpace 𝕜
inst_3 : ContinuousAdd 𝕜
inst_4 : ContinuousConstSMul 𝕜 𝕜
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : Algebra 𝕜 A
φ ψ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))
h : Eq (α := Ideal A) (RingHom.ker φ) (RingHom.ker ψ)
x : A
this :
  Membership.mem (γ := Ideal A) (RingHom.ker φ)
    (HSub.hSub (β := A) x ((algebraMap 𝕜 A : (a : 𝕜) → A) ((ψ : (a : A) → 𝕜) x : 𝕜) : A))
⊢ Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : A) → 𝕜) x : 𝕜) ((ψ : (a : A) → 𝕜) x : 𝕜)
have h₁ : ∀
  (this :
    Eq.{u_1 + 1} (α := 𝕜)
      ((φ : (a : A) → 𝕜) (HSub.hSub (β := A) x ((algebraMap 𝕜 A : (a : 𝕜) → A) ((ψ : (a : A) → 𝕜) x : 𝕜) : A)) : 𝕜)
      (0 : 𝕜)),
  Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : A) → 𝕜) x : 𝕜) ((ψ : (a : A) → 𝕜) x : 𝕜)
Tactic: rwa [RingHom.mem_ker, map_sub, AlgHomClass.commutes, sub_eq_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : CommRing 𝕜
inst_1 : NoZeroDivisors 𝕜
inst_2 : TopologicalSpace 𝕜
inst_3 : ContinuousAdd 𝕜
inst_4 : ContinuousConstSMul 𝕜 𝕜
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : Algebra 𝕜 A
φ ψ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))
h : Eq (α := Ideal A) (RingHom.ker φ) (RingHom.ker ψ)
x : A
this :
  Membership.mem (γ := Ideal A) (RingHom.ker φ)
    (HSub.hSub (β := A) x ((algebraMap 𝕜 A : (a : 𝕜) → A) ((ψ : (a : A) → 𝕜) x : 𝕜) : A))
h₁ :
  ∀
    (this :
      Eq.{u_1 + 1} (α := 𝕜)
        ((φ : (a : A) → 𝕜) (HSub.hSub (β := A) x ((algebraMap 𝕜 A : (a : 𝕜) → A) ((ψ : (a : A) → 𝕜) x : 𝕜) : A)) : 𝕜)
        (0 : 𝕜)),
    Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : A) → 𝕜) x : 𝕜) ((ψ : (a : A) → 𝕜) x : 𝕜)
⊢ Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : A) → 𝕜) x : 𝕜) ((ψ : (a : A) → 𝕜) x : 𝕜)
have h₂ : ∀
  (this :
    HSub.hSub (α := 𝕜) (β := 𝕜) ((φ : (a : A) → 𝕜) x : 𝕜)
        ((φ : (a : A) → 𝕜) ((algebraMap 𝕜 A : (a : 𝕜) → A) ((ψ : (a : A) → 𝕜) x : 𝕜) : A) : 𝕜) =
      0),
  Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : A) → 𝕜) x : 𝕜) ((ψ : (a : A) → 𝕜) x : 𝕜)
Tactic: rwa [RingHom.mem_ker, map_sub, AlgHomClass.commutes, sub_eq_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : CommRing 𝕜
inst_1 : NoZeroDivisors 𝕜
inst_2 : TopologicalSpace 𝕜
inst_3 : ContinuousAdd 𝕜
inst_4 : ContinuousConstSMul 𝕜 𝕜
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : Algebra 𝕜 A
φ ψ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))
h : Eq (α := Ideal A) (RingHom.ker φ) (RingHom.ker ψ)
x : A
this :
  Membership.mem (γ := Ideal A) (RingHom.ker φ)
    (HSub.hSub (β := A) x ((algebraMap 𝕜 A : (a : 𝕜) → A) ((ψ : (a : A) → 𝕜) x : 𝕜) : A))
h₁ :
  ∀
    (this :
      Eq.{u_1 + 1} (α := 𝕜)
        ((φ : (a : A) → 𝕜) (HSub.hSub (β := A) x ((algebraMap 𝕜 A : (a : 𝕜) → A) ((ψ : (a : A) → 𝕜) x : 𝕜) : A)) : 𝕜)
        (0 : 𝕜)),
    Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : A) → 𝕜) x : 𝕜) ((ψ : (a : A) → 𝕜) x : 𝕜)
h₂ :
  ∀
    (this :
      HSub.hSub (α := 𝕜) (β := 𝕜) ((φ : (a : A) → 𝕜) x : 𝕜)
          ((φ : (a : A) → 𝕜) ((algebraMap 𝕜 A : (a : 𝕜) → A) ((ψ : (a : A) → 𝕜) x : 𝕜) : A) : 𝕜) =
        0),
    Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : A) → 𝕜) x : 𝕜) ((ψ : (a : A) → 𝕜) x : 𝕜)
⊢ Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : A) → 𝕜) x : 𝕜) ((ψ : (a : A) → 𝕜) x : 𝕜)
have h₃ : ∀
  (this :
    HSub.hSub (α := 𝕜) (β := 𝕜) ((φ : (a : A) → 𝕜) x : 𝕜)
        ((algebraMap 𝕜 𝕜 : (a : 𝕜) → 𝕜) ((ψ : (a : A) → 𝕜) x : 𝕜) : 𝕜) =
      0),
  Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : A) → 𝕜) x : 𝕜) ((ψ : (a : A) → 𝕜) x : 𝕜)
Tactic: rwa [RingHom.mem_ker, map_sub, AlgHomClass.commutes, sub_eq_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : CommRing 𝕜
inst_1 : NoZeroDivisors 𝕜
inst_2 : TopologicalSpace 𝕜
inst_3 : ContinuousAdd 𝕜
inst_4 : ContinuousConstSMul 𝕜 𝕜
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : Algebra 𝕜 A
φ ψ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))
h : Eq (α := Ideal A) (RingHom.ker φ) (RingHom.ker ψ)
x : A
this :
  Membership.mem (γ := Ideal A) (RingHom.ker φ)
    (HSub.hSub (β := A) x ((algebraMap 𝕜 A : (a : 𝕜) → A) ((ψ : (a : A) → 𝕜) x : 𝕜) : A))
h₁ :
  ∀
    (this :
      Eq.{u_1 + 1} (α := 𝕜)
        ((φ : (a : A) → 𝕜) (HSub.hSub (β := A) x ((algebraMap 𝕜 A : (a : 𝕜) → A) ((ψ : (a : A) → 𝕜) x : 𝕜) : A)) : 𝕜)
        (0 : 𝕜)),
    Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : A) → 𝕜) x : 𝕜) ((ψ : (a : A) → 𝕜) x : 𝕜)
h₂ :
  ∀
    (this :
      HSub.hSub (α := 𝕜) (β := 𝕜) ((φ : (a : A) → 𝕜) x : 𝕜)
          ((φ : (a : A) → 𝕜) ((algebraMap 𝕜 A : (a : 𝕜) → A) ((ψ : (a : A) → 𝕜) x : 𝕜) : A) : 𝕜) =
        0),
    Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : A) → 𝕜) x : 𝕜) ((ψ : (a : A) → 𝕜) x : 𝕜)
h₃ :
  ∀
    (this :
      HSub.hSub (α := 𝕜) (β := 𝕜) ((φ : (a : A) → 𝕜) x : 𝕜)
          ((algebraMap 𝕜 𝕜 : (a : 𝕜) → 𝕜) ((ψ : (a : A) → 𝕜) x : 𝕜) : 𝕜) =
        0),
    Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : A) → 𝕜) x : 𝕜) ((ψ : (a : A) → 𝕜) x : 𝕜)
⊢ Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : A) → 𝕜) x : 𝕜) ((ψ : (a : A) → 𝕜) x : 𝕜)
have h₄ : ∀
  (this :
    Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : A) → 𝕜) x : 𝕜) ((algebraMap 𝕜 𝕜 : (a : 𝕜) → 𝕜) ((ψ : (a : A) → 𝕜) x : 𝕜) : 𝕜)),
  Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : A) → 𝕜) x : 𝕜) ((ψ : (a : A) → 𝕜) x : 𝕜)
Tactic: rwa [RingHom.mem_ker, map_sub, AlgHomClass.commutes, sub_eq_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : CommRing 𝕜
inst_1 : NoZeroDivisors 𝕜
inst_2 : TopologicalSpace 𝕜
inst_3 : IsTopologicalRing 𝕜
inst_4 : TopologicalSpace A
inst_5 : Semiring A
inst_6 : Algebra 𝕜 A
⊢ Eq (α := C((↑(characterSpace 𝕜 A) : Type (max u_1 u_2)), 𝕜))
    { toFun := fun (φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) ↦ (φ : (a : A) → 𝕜) 1, continuous_toFun := ⋯ } 1
have h : ∀ (a : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))),
  Eq.{u_1 + 1} (α := 𝕜)
    (({ toFun := fun (φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) ↦ (φ : (a : A) → 𝕜) 1, continuous_toFun := sorry } :
          (a : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) → 𝕜)
        a :
      𝕜)
    ((1 : (a : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) → 𝕜) a : 𝕜)
Tactic: ext a
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : CommRing 𝕜
inst_1 : NoZeroDivisors 𝕜
inst_2 : TopologicalSpace 𝕜
inst_3 : IsTopologicalRing 𝕜
inst_4 : TopologicalSpace A
inst_5 : Semiring A
inst_6 : Algebra 𝕜 A
a b : A
⊢ { toFun := fun (φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) ↦ (φ : (a : A) → 𝕜) (a * b),
      continuous_toFun := ⋯ } =
    HMul.hMul (α := C((↑(characterSpace 𝕜 A) : Type (max u_1 u_2)), 𝕜))
      { toFun := fun (φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) ↦ (φ : (a : A) → 𝕜) a, continuous_toFun := ⋯ :
        C((↑(characterSpace 𝕜 A) : Type (max u_1 u_2)), 𝕜) }
      { toFun := fun (φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) ↦ (φ : (a : A) → 𝕜) b, continuous_toFun := ⋯ :
        C((↑(characterSpace 𝕜 A) : Type (max u_1 u_2)), 𝕜) }
have h : ∀ (a_1 : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))),
  Eq.{u_1 + 1} (α := 𝕜)
    (({ toFun := fun (φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) ↦ (φ : (a : A) → 𝕜) (a * b),
            continuous_toFun := sorry } :
          (a : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) → 𝕜)
        a_1 :
      𝕜)
    ((HMul.hMul (α := C((↑(characterSpace 𝕜 A) : Type (max u_1 u_2)), 𝕜))
            { toFun := fun (φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) ↦ (φ : (a : A) → 𝕜) a,
              continuous_toFun := sorry : C((↑(characterSpace 𝕜 A) : Type (max u_1 u_2)), 𝕜) }
            { toFun := fun (φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) ↦ (φ : (a : A) → 𝕜) b,
              continuous_toFun := sorry : C((↑(characterSpace 𝕜 A) : Type (max u_1 u_2)), 𝕜) } :
          (a : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) → 𝕜)
        a_1 :
      𝕜)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : CommRing 𝕜
inst_1 : NoZeroDivisors 𝕜
inst_2 : TopologicalSpace 𝕜
inst_3 : IsTopologicalRing 𝕜
inst_4 : TopologicalSpace A
inst_5 : Semiring A
inst_6 : Algebra 𝕜 A
⊢ Eq (α := C((↑(characterSpace 𝕜 A) : Type (max u_1 u_2)), 𝕜))
    { toFun := fun (φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) ↦ (φ : (a : A) → 𝕜) 0, continuous_toFun := ⋯ } 0
have h : ∀ (a : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))),
  Eq.{u_1 + 1} (α := 𝕜)
    (({ toFun := fun (φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) ↦ (φ : (a : A) → 𝕜) 0, continuous_toFun := sorry } :
          (a : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) → 𝕜)
        a :
      𝕜)
    ((0 : (a : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) → 𝕜) a : 𝕜)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : CommRing 𝕜
inst_1 : NoZeroDivisors 𝕜
inst_2 : TopologicalSpace 𝕜
inst_3 : IsTopologicalRing 𝕜
inst_4 : TopologicalSpace A
inst_5 : Semiring A
inst_6 : Algebra 𝕜 A
a b : A
⊢ { toFun := fun (φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) ↦ (φ : (a : A) → 𝕜) (a + b),
      continuous_toFun := ⋯ } =
    HAdd.hAdd (α := C((↑(characterSpace 𝕜 A) : Type (max u_1 u_2)), 𝕜))
      { toFun := fun (φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) ↦ (φ : (a : A) → 𝕜) a, continuous_toFun := ⋯ :
        C((↑(characterSpace 𝕜 A) : Type (max u_1 u_2)), 𝕜) }
      { toFun := fun (φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) ↦ (φ : (a : A) → 𝕜) b, continuous_toFun := ⋯ :
        C((↑(characterSpace 𝕜 A) : Type (max u_1 u_2)), 𝕜) }
have h : ∀ (a_1 : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))),
  Eq.{u_1 + 1} (α := 𝕜)
    (({ toFun := fun (φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) ↦ (φ : (a : A) → 𝕜) (a + b),
            continuous_toFun := sorry } :
          (a : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) → 𝕜)
        a_1 :
      𝕜)
    ((HAdd.hAdd (α := C((↑(characterSpace 𝕜 A) : Type (max u_1 u_2)), 𝕜))
            { toFun := fun (φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) ↦ (φ : (a : A) → 𝕜) a,
              continuous_toFun := sorry : C((↑(characterSpace 𝕜 A) : Type (max u_1 u_2)), 𝕜) }
            { toFun := fun (φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) ↦ (φ : (a : A) → 𝕜) b,
              continuous_toFun := sorry : C((↑(characterSpace 𝕜 A) : Type (max u_1 u_2)), 𝕜) } :
          (a : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) → 𝕜)
        a_1 :
      𝕜)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : CommRing 𝕜
inst_1 : NoZeroDivisors 𝕜
inst_2 : TopologicalSpace 𝕜
inst_3 : IsTopologicalRing 𝕜
inst_4 : TopologicalSpace A
inst_5 : Semiring A
inst_6 : Algebra 𝕜 A
k : 𝕜
⊢ Eq (α := C((↑(characterSpace 𝕜 A) : Type (max u_1 u_2)), 𝕜))
    ({
        toFun := fun (φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) ↦
          (φ : (a : A) → 𝕜) ((algebraMap 𝕜 A : (a : 𝕜) → A) k : A),
        continuous_toFun := ⋯ } :
      C((↑(characterSpace 𝕜 A) : Type (max u_1 u_2)), 𝕜))
    ((algebraMap 𝕜 C((↑(characterSpace 𝕜 A) : Type (max u_1 u_2)), 𝕜) :
          (a : 𝕜) → C((↑(characterSpace 𝕜 A) : Type (max u_1 u_2)), 𝕜))
        k :
      C((↑(characterSpace 𝕜 A) : Type (max u_1 u_2)), 𝕜))
have h : ∀ (a : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))),
  Eq.{u_1 + 1} (α := 𝕜)
    ((({
              toFun := fun (φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) ↦
                (φ : (a : A) → 𝕜) ((algebraMap 𝕜 A : (a : 𝕜) → A) k : A),
              continuous_toFun := sorry } :
            C((↑(characterSpace 𝕜 A) : Type (max u_1 u_2)), 𝕜)) :
          (a : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) → 𝕜)
        a :
      𝕜)
    ((((algebraMap 𝕜 C((↑(characterSpace 𝕜 A) : Type (max u_1 u_2)), 𝕜) :
                (a : 𝕜) → C((↑(characterSpace 𝕜 A) : Type (max u_1 u_2)), 𝕜))
              k :
            C((↑(characterSpace 𝕜 A) : Type (max u_1 u_2)), 𝕜)) :
          (a : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) → 𝕜)
        a :
      𝕜)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap (goal)
Goal:
R : Type u_1
𝕜₂ : Type u_3
𝕜₃ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst : Semiring R
inst_1 : NormedField 𝕜₂
inst_2 : NormedField 𝕜₃
inst_3 : AddCommMonoid E
inst_4 : Module R E
inst_5 : TopologicalSpace E
inst_6 : AddCommGroup F
inst_7 : Module 𝕜₂ F
inst_8 : TopologicalSpace F
inst_9 : AddCommGroup G
inst_10 : Module 𝕜₃ G
inst_11 : TopologicalSpace G
inst_12 : IsTopologicalAddGroup G
inst_13 : ContinuousConstSMul 𝕜₃ G
σ₁₃ : R →+* 𝕜₃
σ₂₃ : 𝕜₂ →+* 𝕜₃
f : E →SL[σ₁₃] F →SL[σ₂₃] G
x x' : E
y : F
⊢ (((f : (a : E) → F →SL[σ₂₃] G) (x + x') : F →SL[σ₂₃] G) : (a : F) → G) y =
    HAdd.hAdd (α := G) (β := G) ((((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) y : G)
      ((((f : (a : E) → F →SL[σ₂₃] G) x' : F →SL[σ₂₃] G) : (a : F) → G) y : G)
have rw : (HAdd.hAdd (α := F →SL[σ₂₃] G) (β := F →SL[σ₂₃] G) ((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G)
        ((f : (a : E) → F →SL[σ₂₃] G) x' : F →SL[σ₂₃] G) :
      (a : F) → G)
    y =
  HAdd.hAdd (α := G) (β := G) ((((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) y : G)
    ((((f : (a : E) → F →SL[σ₂₃] G) x' : F →SL[σ₂₃] G) : (a : F) → G) y : G)
Tactic: rw [f.map_add, add_apply]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap (goal)
Goal:
R : Type u_1
𝕜₂ : Type u_3
𝕜₃ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst : Semiring R
inst_1 : NormedField 𝕜₂
inst_2 : NormedField 𝕜₃
inst_3 : AddCommMonoid E
inst_4 : Module R E
inst_5 : TopologicalSpace E
inst_6 : AddCommGroup F
inst_7 : Module 𝕜₂ F
inst_8 : TopologicalSpace F
inst_9 : AddCommGroup G
inst_10 : Module 𝕜₃ G
inst_11 : TopologicalSpace G
inst_12 : IsTopologicalAddGroup G
inst_13 : ContinuousConstSMul 𝕜₃ G
σ₁₃ : R →+* 𝕜₃
σ₂₃ : 𝕜₂ →+* 𝕜₃
f : E →SL[σ₁₃] F →SL[σ₂₃] G
x x' : E
y : F
rw :
  (HAdd.hAdd (α := F →SL[σ₂₃] G) (β := F →SL[σ₂₃] G) ((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G)
          ((f : (a : E) → F →SL[σ₂₃] G) x' : F →SL[σ₂₃] G) :
        (a : F) → G)
      y =
    HAdd.hAdd (α := G) (β := G) ((((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) y : G)
      ((((f : (a : E) → F →SL[σ₂₃] G) x' : F →SL[σ₂₃] G) : (a : F) → G) y : G)
⊢ (((f : (a : E) → F →SL[σ₂₃] G) (x + x') : F →SL[σ₂₃] G) : (a : F) → G) y =
    HAdd.hAdd (α := G) (β := G) ((((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) y : G)
      ((((f : (a : E) → F →SL[σ₂₃] G) x' : F →SL[σ₂₃] G) : (a : F) → G) y : G)
have rw₁ : HAdd.hAdd (α := G) (β := G) ((((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) y : G)
    ((((f : (a : E) → F →SL[σ₂₃] G) x' : F →SL[σ₂₃] G) : (a : F) → G) y : G) =
  HAdd.hAdd (α := G) (β := G) ((((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) y : G)
    ((((f : (a : E) → F →SL[σ₂₃] G) x' : F →SL[σ₂₃] G) : (a : F) → G) y : G)
Tactic: rw [f.map_add, add_apply]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap (goal)
Goal:
R : Type u_1
𝕜₂ : Type u_3
𝕜₃ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst : Semiring R
inst_1 : NormedField 𝕜₂
inst_2 : NormedField 𝕜₃
inst_3 : AddCommMonoid E
inst_4 : Module R E
inst_5 : TopologicalSpace E
inst_6 : AddCommGroup F
inst_7 : Module 𝕜₂ F
inst_8 : TopologicalSpace F
inst_9 : AddCommGroup G
inst_10 : Module 𝕜₃ G
inst_11 : TopologicalSpace G
inst_12 : IsTopologicalAddGroup G
inst_13 : ContinuousConstSMul 𝕜₃ G
σ₁₃ : R →+* 𝕜₃
σ₂₃ : 𝕜₂ →+* 𝕜₃
f : E →SL[σ₁₃] F →SL[σ₂₃] G
y : F
⊢ Eq.{u_7 + 1} (α := G) (((f : (a : E) → F →SL[σ₂₃] G) 0 : (a : F) → G) y : G) (0 : G)
have rw : Eq.{u_7 + 1} (α := G) ((0 : (a : F) → G) y : G) (0 : G)
Tactic: rw [f.map_zero, zero_apply]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap (goal)
Goal:
R : Type u_1
𝕜₂ : Type u_3
𝕜₃ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst : Semiring R
inst_1 : NormedField 𝕜₂
inst_2 : NormedField 𝕜₃
inst_3 : AddCommMonoid E
inst_4 : Module R E
inst_5 : TopologicalSpace E
inst_6 : AddCommGroup F
inst_7 : Module 𝕜₂ F
inst_8 : TopologicalSpace F
inst_9 : AddCommGroup G
inst_10 : Module 𝕜₃ G
inst_11 : TopologicalSpace G
inst_12 : IsTopologicalAddGroup G
inst_13 : ContinuousConstSMul 𝕜₃ G
σ₁₃ : R →+* 𝕜₃
σ₂₃ : 𝕜₂ →+* 𝕜₃
f : E →SL[σ₁₃] F →SL[σ₂₃] G
y : F
rw : Eq.{u_7 + 1} (α := G) ((0 : (a : F) → G) y : G) (0 : G)
⊢ Eq.{u_7 + 1} (α := G) (((f : (a : E) → F →SL[σ₂₃] G) 0 : (a : F) → G) y : G) (0 : G)
have rw₁ : Eq.{u_7 + 1} (α := G) 0 0
Tactic: rw [f.map_zero, zero_apply]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap (goal)
Goal:
R : Type u_1
𝕜₂ : Type u_3
𝕜₃ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst : Semiring R
inst_1 : NormedField 𝕜₂
inst_2 : NormedField 𝕜₃
inst_3 : AddCommMonoid E
inst_4 : Module R E
inst_5 : TopologicalSpace E
inst_6 : AddCommGroup F
inst_7 : Module 𝕜₂ F
inst_8 : TopologicalSpace F
inst_9 : AddCommGroup G
inst_10 : Module 𝕜₃ G
inst_11 : TopologicalSpace G
inst_12 : IsTopologicalAddGroup G
inst_13 : ContinuousConstSMul 𝕜₃ G
σ₁₃ : R →+* 𝕜₃
σ₂₃ : 𝕜₂ →+* 𝕜₃
f : E →SL[σ₁₃] F →SL[σ₂₃] G
c : R
x : E
y : F
⊢ (((f : (a : E) → F →SL[σ₂₃] G) (c • x) : F →SL[σ₂₃] G) : (a : F) → G) y =
    HSMul.hSMul.{u_4, u_7, u_7} (α := 𝕜₃) (β := G) ((σ₁₃ : (a : R) → 𝕜₃) c : 𝕜₃)
      ((((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) y : G)
have rw : (HSMul.hSMul (α := 𝕜₃) (β := F →SL[σ₂₃] G) ((σ₁₃ : (a : R) → 𝕜₃) c : 𝕜₃)
        ((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) :
      (a : F) → G)
    y =
  HSMul.hSMul.{u_4, u_7, u_7} (α := 𝕜₃) (β := G) ((σ₁₃ : (a : R) → 𝕜₃) c : 𝕜₃)
    ((((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) y : G)
Tactic: rw [f.map_smulₛₗ, smul_apply]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap (goal)
Goal:
R : Type u_1
𝕜₂ : Type u_3
𝕜₃ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst : Semiring R
inst_1 : NormedField 𝕜₂
inst_2 : NormedField 𝕜₃
inst_3 : AddCommMonoid E
inst_4 : Module R E
inst_5 : TopologicalSpace E
inst_6 : AddCommGroup F
inst_7 : Module 𝕜₂ F
inst_8 : TopologicalSpace F
inst_9 : AddCommGroup G
inst_10 : Module 𝕜₃ G
inst_11 : TopologicalSpace G
inst_12 : IsTopologicalAddGroup G
inst_13 : ContinuousConstSMul 𝕜₃ G
σ₁₃ : R →+* 𝕜₃
σ₂₃ : 𝕜₂ →+* 𝕜₃
f : E →SL[σ₁₃] F →SL[σ₂₃] G
c : R
x : E
y : F
rw :
  (HSMul.hSMul (α := 𝕜₃) (β := F →SL[σ₂₃] G) ((σ₁₃ : (a : R) → 𝕜₃) c : 𝕜₃)
          ((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) :
        (a : F) → G)
      y =
    HSMul.hSMul.{u_4, u_7, u_7} (α := 𝕜₃) (β := G) ((σ₁₃ : (a : R) → 𝕜₃) c : 𝕜₃)
      ((((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) y : G)
⊢ (((f : (a : E) → F →SL[σ₂₃] G) (c • x) : F →SL[σ₂₃] G) : (a : F) → G) y =
    HSMul.hSMul.{u_4, u_7, u_7} (α := 𝕜₃) (β := G) ((σ₁₃ : (a : R) → 𝕜₃) c : 𝕜₃)
      ((((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) y : G)
have rw₁ : HSMul.hSMul.{u_4, u_7, u_7} (α := 𝕜₃) (β := G) ((σ₁₃ : (a : R) → 𝕜₃) c : 𝕜₃)
    ((((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) y : G) =
  HSMul.hSMul.{u_4, u_7, u_7} (α := 𝕜₃) (β := G) ((σ₁₃ : (a : R) → 𝕜₃) c : 𝕜₃)
    ((((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) y : G)
Tactic: rw [f.map_smulₛₗ, smul_apply]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap (goal)
Goal:
𝕜₂ : Type u_3
𝕜₃ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst : NormedField 𝕜₂
inst_1 : NormedField 𝕜₃
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜₃ E
inst_4 : TopologicalSpace E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜₂ F
inst_7 : TopologicalSpace F
inst_8 : AddCommGroup G
inst_9 : Module 𝕜₃ G
inst_10 : TopologicalSpace G
inst_11 : IsTopologicalAddGroup G
inst_12 : ContinuousConstSMul 𝕜₃ G
σ₂₃ : 𝕜₂ →+* 𝕜₃
f : E →L[𝕜₃] F →SL[σ₂₃] G
c : 𝕜₃
x : E
y : F
⊢ (((f : (a : E) → F →SL[σ₂₃] G) (c • x) : F →SL[σ₂₃] G) : (a : F) → G) y =
    HSMul.hSMul (β := G) c ((((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) y : G)
have rw : (HSMul.hSMul (β := F →SL[σ₂₃] G) c ((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) y =
  HSMul.hSMul (β := G) c ((((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) y : G)
Tactic: rw [f.map_smul, smul_apply]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap (goal)
Goal:
𝕜₂ : Type u_3
𝕜₃ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst : NormedField 𝕜₂
inst_1 : NormedField 𝕜₃
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜₃ E
inst_4 : TopologicalSpace E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜₂ F
inst_7 : TopologicalSpace F
inst_8 : AddCommGroup G
inst_9 : Module 𝕜₃ G
inst_10 : TopologicalSpace G
inst_11 : IsTopologicalAddGroup G
inst_12 : ContinuousConstSMul 𝕜₃ G
σ₂₃ : 𝕜₂ →+* 𝕜₃
f : E →L[𝕜₃] F →SL[σ₂₃] G
c : 𝕜₃
x : E
y : F
rw :
  (HSMul.hSMul (β := F →SL[σ₂₃] G) c ((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) y =
    HSMul.hSMul (β := G) c ((((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) y : G)
⊢ (((f : (a : E) → F →SL[σ₂₃] G) (c • x) : F →SL[σ₂₃] G) : (a : F) → G) y =
    HSMul.hSMul (β := G) c ((((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) y : G)
have rw₁ : HSMul.hSMul (β := G) c ((((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) y : G) =
  HSMul.hSMul (β := G) c ((((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) y : G)
Tactic: rw [f.map_smul, smul_apply]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap (goal)
Goal:
R : Type u_1
𝕜₂ : Type u_3
𝕜₃ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst : Semiring R
inst_1 : NormedField 𝕜₂
inst_2 : NormedField 𝕜₃
inst_3 : AddCommGroup E
inst_4 : Module R E
inst_5 : TopologicalSpace E
inst_6 : AddCommGroup F
inst_7 : Module 𝕜₂ F
inst_8 : TopologicalSpace F
inst_9 : AddCommGroup G
inst_10 : Module 𝕜₃ G
inst_11 : TopologicalSpace G
inst_12 : IsTopologicalAddGroup G
inst_13 : ContinuousConstSMul 𝕜₃ G
σ₁₃ : R →+* 𝕜₃
σ₂₃ : 𝕜₂ →+* 𝕜₃
f : E →SL[σ₁₃] F →SL[σ₂₃] G
x x' : E
y : F
⊢ (((f : (a : E) → F →SL[σ₂₃] G) (x - x') : F →SL[σ₂₃] G) : (a : F) → G) y =
    HSub.hSub (α := G) (β := G) ((((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) y : G)
      ((((f : (a : E) → F →SL[σ₂₃] G) x' : F →SL[σ₂₃] G) : (a : F) → G) y : G)
have rw : (HSub.hSub (α := F →SL[σ₂₃] G) (β := F →SL[σ₂₃] G) ((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G)
        ((f : (a : E) → F →SL[σ₂₃] G) x' : F →SL[σ₂₃] G) :
      (a : F) → G)
    y =
  HSub.hSub (α := G) (β := G) ((((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) y : G)
    ((((f : (a : E) → F →SL[σ₂₃] G) x' : F →SL[σ₂₃] G) : (a : F) → G) y : G)
Tactic: rw [map_sub, sub_apply]