awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Complement (goal)
Goal:
R : Type u_1
inst : Ring R
E : Type u_2
F : Type u_3
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module R E
inst_4 : IsTopologicalAddGroup E
inst_5 : TopologicalSpace F
inst_6 : AddCommGroup F
inst_7 : Module R F
inst_8 : ContinuousAdd F
p q : Submodule R E
h : IsTopCompl p q
φ₁ φ₂ : ContinuousLinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (↥p) F
ψ₁ ψ₂ : ContinuousLinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (↥q) F
⊢ ofIsTopCompl h (φ₁ + φ₂) (ψ₁ + ψ₂) = ofIsTopCompl h φ₁ ψ₁ + ofIsTopCompl h φ₂ ψ₂
have h₁ : ∀ (x : E),
  Eq.{u_3 + 1} (α := F) ((ofIsTopCompl h (φ₁ + φ₂) (ψ₁ + ψ₂) : (a : E) → F) x : F)
    ((ofIsTopCompl h φ₁ ψ₁ + ofIsTopCompl h φ₂ ψ₂ : (a : E) → F) x : F)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic (goal)
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
M₂ : Type u_6
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₁ M₁
inst_7 : Module R₂ M₂
f g : M₁ →SL[σ₁₂] M₂
H : (↑f : M₁ →ₛₗ[σ₁₂] M₂) = (↑g : M₁ →ₛₗ[σ₁₂] M₂)
⊢ f = g
have mk : ∀ (toLinearMap : M₁ →ₛₗ[σ₁₂] M₂) (cont : Continuous[inst_2, inst_4] toLinearMap.toFun)
  (H : (↑{ toLinearMap := toLinearMap, cont := cont : M₁ →SL[σ₁₂] M₂ } : M₁ →ₛₗ[σ₁₂] M₂) = (↑g : M₁ →ₛₗ[σ₁₂] M₂)),
  { toLinearMap := toLinearMap, cont := cont : M₁ →SL[σ₁₂] M₂ } = g
Tactic: cases f
Cleared hypotheses: f, H
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic (goal)
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
M₂ : Type u_6
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₁ M₁
inst_7 : Module R₂ M₂
g : M₁ →SL[σ₁₂] M₂
toLinearMap : M₁ →ₛₗ[σ₁₂] M₂
cont : Continuous[inst_2, inst_4] toLinearMap.toFun
H : (↑{ toLinearMap := toLinearMap, cont := cont : M₁ →SL[σ₁₂] M₂ } : M₁ →ₛₗ[σ₁₂] M₂) = (↑g : M₁ →ₛₗ[σ₁₂] M₂)
⊢ { toLinearMap := toLinearMap, cont := cont : M₁ →SL[σ₁₂] M₂ } = g
have mk : ∀ (toLinearMap_1 : M₁ →ₛₗ[σ₁₂] M₂) (cont_1 : Continuous[inst_2, inst_4] toLinearMap_1.toFun)
  (H :
    (↑{ toLinearMap := toLinearMap, cont := cont : M₁ →SL[σ₁₂] M₂ } : M₁ →ₛₗ[σ₁₂] M₂) =
      (↑{ toLinearMap := toLinearMap_1, cont := cont_1 : M₁ →SL[σ₁₂] M₂ } : M₁ →ₛₗ[σ₁₂] M₂)),
  { toLinearMap := toLinearMap, cont := cont : M₁ →SL[σ₁₂] M₂ } = { toLinearMap := toLinearMap_1, cont := cont_1 }
Tactic: cases g
Cleared hypotheses: g, H
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic (goal)
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
M₂ : Type u_6
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₁ M₁
inst_7 : Module R₂ M₂
⊢ Eq (α := Set ((a : M₁) → M₂)) (Set.range (ι := M₁ →SL[σ₁₂] M₂) (DFunLike.coe (β := fun (x : M₁) ↦ M₂)))
    ({f : M₁ → M₂ | Continuous[inst_2, inst_4] f} ∩
      Set.range (ι := M₁ →ₛₗ[σ₁₂] M₂) (DFunLike.coe (β := fun (x : M₁) ↦ M₂)))
have h : ∀ (f : (a : M₁) → M₂),
  Membership.mem (γ := Set ((a : M₁) → M₂)) (Set.range (ι := M₁ →SL[σ₁₂] M₂) (DFunLike.coe (β := fun (x : M₁) ↦ M₂)))
      f ↔
    Membership.mem (γ := Set ((a : M₁) → M₂))
      ({f : M₁ → M₂ | Continuous[inst_2, inst_4] f} ∩
        Set.range (ι := M₁ →ₛₗ[σ₁₂] M₂) (DFunLike.coe (β := fun (x : M₁) ↦ M₂)))
      f
Tactic: ext f
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic (goal)
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
M₂ : Type u_6
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₁ M₁
inst_7 : Module R₂ M₂
f : (a : M₁) → M₂
⊢ Membership.mem (γ := Set ((a : M₁) → M₂)) (Set.range (ι := M₁ →SL[σ₁₂] M₂) (DFunLike.coe (β := fun (x : M₁) ↦ M₂)))
      f ↔
    Membership.mem (γ := Set ((a : M₁) → M₂))
      ({f : M₁ → M₂ | Continuous[inst_2, inst_4] f} ∩
        Set.range (ι := M₁ →ₛₗ[σ₁₂] M₂) (DFunLike.coe (β := fun (x : M₁) ↦ M₂)))
      f
have h : Membership.mem (γ := Set ((a : M₁) → M₂)) (Set.range (ι := M₁ →SL[σ₁₂] M₂) (DFunLike.coe (β := fun (x : M₁) ↦ M₂))) f →
  Membership.mem (γ := Set ((a : M₁) → M₂))
    ({f : M₁ → M₂ | Continuous[inst_2, inst_4] f} ∩
      Set.range (ι := M₁ →ₛₗ[σ₁₂] M₂) (DFunLike.coe (β := fun (x : M₁) ↦ M₂)))
    f
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic (goal)
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
M₂ : Type u_6
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₁ M₁
inst_7 : Module R₂ M₂
f : (a : M₁) → M₂
h :
  Membership.mem (γ := Set ((a : M₁) → M₂)) (Set.range (ι := M₁ →SL[σ₁₂] M₂) (DFunLike.coe (β := fun (x : M₁) ↦ M₂)))
      f →
    Membership.mem (γ := Set ((a : M₁) → M₂))
      ({f : M₁ → M₂ | Continuous[inst_2, inst_4] f} ∩
        Set.range (ι := M₁ →ₛₗ[σ₁₂] M₂) (DFunLike.coe (β := fun (x : M₁) ↦ M₂)))
      f
⊢ Membership.mem (γ := Set ((a : M₁) → M₂)) (Set.range (ι := M₁ →SL[σ₁₂] M₂) (DFunLike.coe (β := fun (x : M₁) ↦ M₂)))
      f ↔
    Membership.mem (γ := Set ((a : M₁) → M₂))
      ({f : M₁ → M₂ | Continuous[inst_2, inst_4] f} ∩
        Set.range (ι := M₁ →ₛₗ[σ₁₂] M₂) (DFunLike.coe (β := fun (x : M₁) ↦ M₂)))
      f
have h₁ : Membership.mem (γ := Set ((a : M₁) → M₂))
    ({f : M₁ → M₂ | Continuous[inst_2, inst_4] f} ∩
      Set.range (ι := M₁ →ₛₗ[σ₁₂] M₂) (DFunLike.coe (β := fun (x : M₁) ↦ M₂)))
    f →
  Membership.mem (γ := Set ((a : M₁) → M₂)) (Set.range (ι := M₁ →SL[σ₁₂] M₂) (DFunLike.coe (β := fun (x : M₁) ↦ M₂))) f
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic (goal)
Goal:
R₁ : Type u_1
inst : Semiring R₁
M₁ : Type u_4
inst_1 : TopologicalSpace M₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R₁ M₁
inst_4 : TopologicalSpace R₁
inst_5 : ContinuousSMul R₁ M₁
inst_6 : ContinuousAdd M₁
f : M₁ →L[R₁] M₁
s : Submodule R₁ M₁
hs : s ∈ Module.End.invtSubmodule (↑f : M₁ →ₗ[R₁] M₁)
⊢ s.topologicalClosure ∈ Module.End.invtSubmodule (↑f : M₁ →ₗ[R₁] M₁)
have rw : ∀ (hs : Submodule.map (↑f : M₁ →ₗ[R₁] M₁) s ≤ s),
  Submodule.map (↑f : M₁ →ₗ[R₁] M₁) s.topologicalClosure ≤ s.topologicalClosure
Tactic: rw [Module.End.mem_invtSubmodule_iff_map_le] at hs ⊢
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic (goal)
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
M₂ : Type u_6
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₁ M₁
inst_7 : Module R₂ M₂
inst_8 : RingHomSurjective σ₁₂
inst_9 : TopologicalSpace R₁
inst_10 : TopologicalSpace R₂
inst_11 : ContinuousSMul R₁ M₁
inst_12 : ContinuousAdd M₁
inst_13 : ContinuousSMul R₂ M₂
inst_14 : ContinuousAdd M₂
f : M₁ →SL[σ₁₂] M₂
hf' : DenseRange.{u_6, u_4} (X := M₂) (α := M₁) (⇑f : (a : M₁) → M₂)
s : Submodule R₁ M₁
hs : s.topologicalClosure = ⊤
⊢ (Submodule.map (↑f : M₁ →ₛₗ[σ₁₂] M₂) s).topologicalClosure = ⊤
have rw : ∀ (hs : (↑s.topologicalClosure : Set M₁) = (↑⊤ : Set M₁)),
  (↑(Submodule.map (↑f : M₁ →ₛₗ[σ₁₂] M₂) s).topologicalClosure : Set M₂) = (↑⊤ : Set M₂)
Tactic: rw [SetLike.ext'_iff] at hs ⊢
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic (goal)
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
M₂ : Type u_6
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₁ M₁
inst_7 : Module R₂ M₂
inst_8 : RingHomSurjective σ₁₂
inst_9 : TopologicalSpace R₁
inst_10 : TopologicalSpace R₂
inst_11 : ContinuousSMul R₁ M₁
inst_12 : ContinuousAdd M₁
inst_13 : ContinuousSMul R₂ M₂
inst_14 : ContinuousAdd M₂
f : M₁ →SL[σ₁₂] M₂
hf' : DenseRange.{u_6, u_4} (X := M₂) (α := M₁) (⇑f : (a : M₁) → M₂)
s : Submodule R₁ M₁
hs : (↑s.topologicalClosure : Set M₁) = (↑⊤ : Set M₁)
⊢ (↑(Submodule.map (↑f : M₁ →ₛₗ[σ₁₂] M₂) s).topologicalClosure : Set M₂) = (↑⊤ : Set M₂)
have simp : ∀ (hs : Dense (↑s : Set M₁)), Dense (↑(Submodule.map (↑f : M₁ →ₛₗ[σ₁₂] M₂) s) : Set M₂)
Tactic: simp only [Submodule.topologicalClosure_coe, Submodule.top_coe, ← dense_iff_closure_eq] at hs ⊢
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic (goal)
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
M₂ : Type u_6
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₁ M₁
inst_7 : Module R₂ M₂
f : M₁ →SL[σ₁₂] M₂
hf : f ≠ 0
⊢ ∃ (x : M₁), Ne.{u_6 + 1} (α := M₂) ((f : (a : M₁) → M₂) x : M₂) (0 : M₂)
have by_contra! : ∀ (h : ∀ (x : M₁), Eq.{u_6 + 1} (α := M₂) ((f : (a : M₁) → M₂) x : M₂) (0 : M₂)), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic (goal)
Goal:
R₁ : Type u_1
inst : Semiring R₁
M₁ : Type u_4
inst_1 : TopologicalSpace M₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R₁ M₁
f : M₁ →L[R₁] M₁
⊢ (↑f : M₁ →ₗ[R₁] M₁) = LinearMap.id ↔ f = ContinuousLinearMap.id R₁ M₁
have rw : (↑f : M₁ →ₗ[R₁] M₁) = (↑(ContinuousLinearMap.id R₁ M₁) : M₁ →ₗ[R₁] M₁) ↔ f = ContinuousLinearMap.id R₁ M₁
Tactic: rw [← coe_id, coe_inj]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic (goal)
Goal:
R₁ : Type u_1
inst : Semiring R₁
M₁ : Type u_4
inst_1 : TopologicalSpace M₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R₁ M₁
f : M₁ →L[R₁] M₁
rw : (↑f : M₁ →ₗ[R₁] M₁) = (↑(ContinuousLinearMap.id R₁ M₁) : M₁ →ₗ[R₁] M₁) ↔ f = ContinuousLinearMap.id R₁ M₁
⊢ (↑f : M₁ →ₗ[R₁] M₁) = LinearMap.id ↔ f = ContinuousLinearMap.id R₁ M₁
have rw₁ : f = ContinuousLinearMap.id R₁ M₁ ↔ f = ContinuousLinearMap.id R₁ M₁
Tactic: rw [← coe_id, coe_inj]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic (goal)
Goal:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst_3 : TopologicalSpace M₁
inst_4 : AddCommMonoid M₁
M'₁ : Type u_5
inst_5 : TopologicalSpace M'₁
inst_6 : AddCommMonoid M'₁
M₂ : Type u_6
inst_7 : TopologicalSpace M₂
inst_8 : AddCommMonoid M₂
M₃ : Type u_7
inst_9 : TopologicalSpace M₃
inst_10 : AddCommMonoid M₃
M₄ : Type u_8
inst_11 : TopologicalSpace M₄
inst_12 : AddCommMonoid M₄
inst_13 : Module R₁ M₁
inst_14 : Module R₁ M'₁
inst_15 : Module R₂ M₂
inst_16 : Module R₃ M₃
inst_17 : ContinuousAdd M₂
a b c : M₁ →SL[σ₁₂] M₂
⊢ a + b + c = a + (b + c)
have h : ∀ (x : M₁), Eq.{u_6 + 1} (α := M₂) ((a + b + c : (a : M₁) → M₂) x : M₂) ((a + (b + c) : (a : M₁) → M₂) x : M₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic (goal)
Goal:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst_3 : TopologicalSpace M₁
inst_4 : AddCommMonoid M₁
M'₁ : Type u_5
inst_5 : TopologicalSpace M'₁
inst_6 : AddCommMonoid M'₁
M₂ : Type u_6
inst_7 : TopologicalSpace M₂
inst_8 : AddCommMonoid M₂
M₃ : Type u_7
inst_9 : TopologicalSpace M₃
inst_10 : AddCommMonoid M₃
M₄ : Type u_8
inst_11 : TopologicalSpace M₄
inst_12 : AddCommMonoid M₄
inst_13 : Module R₁ M₁
inst_14 : Module R₁ M'₁
inst_15 : Module R₂ M₂
inst_16 : Module R₃ M₃
inst_17 : ContinuousAdd M₂
a : M₁ →SL[σ₁₂] M₂
⊢ 0 + a = a
have h : ∀ (x : M₁), Eq.{u_6 + 1} (α := M₂) ((0 + a : (a : M₁) → M₂) x : M₂) ((a : (a : M₁) → M₂) x : M₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic (goal)
Goal:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst_3 : TopologicalSpace M₁
inst_4 : AddCommMonoid M₁
M'₁ : Type u_5
inst_5 : TopologicalSpace M'₁
inst_6 : AddCommMonoid M'₁
M₂ : Type u_6
inst_7 : TopologicalSpace M₂
inst_8 : AddCommMonoid M₂
M₃ : Type u_7
inst_9 : TopologicalSpace M₃
inst_10 : AddCommMonoid M₃
M₄ : Type u_8
inst_11 : TopologicalSpace M₄
inst_12 : AddCommMonoid M₄
inst_13 : Module R₁ M₁
inst_14 : Module R₁ M'₁
inst_15 : Module R₂ M₂
inst_16 : Module R₃ M₃
inst_17 : ContinuousAdd M₂
a : M₁ →SL[σ₁₂] M₂
⊢ a + 0 = a
have h : ∀ (x : M₁), Eq.{u_6 + 1} (α := M₂) ((a + 0 : (a : M₁) → M₂) x : M₂) ((a : (a : M₁) → M₂) x : M₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic (goal)
Goal:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst_3 : TopologicalSpace M₁
inst_4 : AddCommMonoid M₁
M'₁ : Type u_5
inst_5 : TopologicalSpace M'₁
inst_6 : AddCommMonoid M'₁
M₂ : Type u_6
inst_7 : TopologicalSpace M₂
inst_8 : AddCommMonoid M₂
M₃ : Type u_7
inst_9 : TopologicalSpace M₃
inst_10 : AddCommMonoid M₃
M₄ : Type u_8
inst_11 : TopologicalSpace M₄
inst_12 : AddCommMonoid M₄
inst_13 : Module R₁ M₁
inst_14 : Module R₁ M'₁
inst_15 : Module R₂ M₂
inst_16 : Module R₃ M₃
inst_17 : ContinuousAdd M₂
f : M₁ →SL[σ₁₂] M₂
⊢ HSMul.hSMul (α := ℕ) 0 f = 0
have h : ∀ (x : M₁), Eq.{u_6 + 1} (α := M₂) ((HSMul.hSMul (α := ℕ) 0 f : (a : M₁) → M₂) x : M₂) ((0 : (a : M₁) → M₂) x : M₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic (goal)
Goal:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst_3 : TopologicalSpace M₁
inst_4 : AddCommMonoid M₁
M'₁ : Type u_5
inst_5 : TopologicalSpace M'₁
inst_6 : AddCommMonoid M'₁
M₂ : Type u_6
inst_7 : TopologicalSpace M₂
inst_8 : AddCommMonoid M₂
M₃ : Type u_7
inst_9 : TopologicalSpace M₃
inst_10 : AddCommMonoid M₃
M₄ : Type u_8
inst_11 : TopologicalSpace M₄
inst_12 : AddCommMonoid M₄
inst_13 : Module R₁ M₁
inst_14 : Module R₁ M'₁
inst_15 : Module R₂ M₂
inst_16 : Module R₃ M₃
inst_17 : ContinuousAdd M₂
n : ℕ
f : M₁ →SL[σ₁₂] M₂
⊢ (n + 1) • f = n • f + f
have h : ∀ (x : M₁), Eq.{u_6 + 1} (α := M₂) (((n + 1) • f : (a : M₁) → M₂) x : M₂) ((n • f + f : (a : M₁) → M₂) x : M₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic (goal)
Goal:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst_3 : TopologicalSpace M₁
inst_4 : AddCommMonoid M₁
M'₁ : Type u_5
inst_5 : TopologicalSpace M'₁
inst_6 : AddCommMonoid M'₁
M₂ : Type u_6
inst_7 : TopologicalSpace M₂
inst_8 : AddCommMonoid M₂
M₃ : Type u_7
inst_9 : TopologicalSpace M₃
inst_10 : AddCommMonoid M₃
M₄ : Type u_8
inst_11 : TopologicalSpace M₄
inst_12 : AddCommMonoid M₄
inst_13 : Module R₁ M₁
inst_14 : Module R₁ M'₁
inst_15 : Module R₂ M₂
inst_16 : Module R₃ M₃
inst_17 : ContinuousAdd M₂
a b : M₁ →SL[σ₁₂] M₂
⊢ a + b = b + a
have h : ∀ (x : M₁), Eq.{u_6 + 1} (α := M₂) ((a + b : (a : M₁) → M₂) x : M₂) ((b + a : (a : M₁) → M₂) x : M₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic (goal)
Goal:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst_3 : TopologicalSpace M₁
inst_4 : AddCommMonoid M₁
M₂ : Type u_6
inst_5 : TopologicalSpace M₂
inst_6 : AddCommMonoid M₂
M₃ : Type u_7
inst_7 : TopologicalSpace M₃
inst_8 : AddCommMonoid M₃
inst_9 : Module R₁ M₁
inst_10 : Module R₂ M₂
inst_11 : Module R₃ M₃
inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
g : M₂ →SL[σ₂₃] M₃
⊢ Eq (α := M₁ →SL[σ₁₃] M₃) (g.comp (σ₁₂ := σ₁₂) 0) 0
have h : ∀ (x : M₁), Eq.{u_7 + 1} (α := M₃) ((g.comp (σ₁₂ := σ₁₂) 0 : (a : M₁) → M₃) x : M₃) ((0 : (a : M₁) → M₃) x : M₃)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic (goal)
Goal:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst_3 : TopologicalSpace M₁
inst_4 : AddCommMonoid M₁
M₂ : Type u_6
inst_5 : TopologicalSpace M₂
inst_6 : AddCommMonoid M₂
M₃ : Type u_7
inst_7 : TopologicalSpace M₃
inst_8 : AddCommMonoid M₃
inst_9 : Module R₁ M₁
inst_10 : Module R₂ M₂
inst_11 : Module R₃ M₃
inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M₁ →SL[σ₁₂] M₂
⊢ Eq (α := M₁ →SL[σ₁₃] M₃) (comp (σ₂₃ := σ₂₃) 0 f) 0
have h : ∀ (x : M₁), Eq.{u_7 + 1} (α := M₃) ((comp (σ₂₃ := σ₂₃) 0 f : (a : M₁) → M₃) x : M₃) ((0 : (a : M₁) → M₃) x : M₃)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic (goal)
Goal:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst_3 : TopologicalSpace M₁
inst_4 : AddCommMonoid M₁
M₂ : Type u_6
inst_5 : TopologicalSpace M₂
inst_6 : AddCommMonoid M₂
M₃ : Type u_7
inst_7 : TopologicalSpace M₃
inst_8 : AddCommMonoid M₃
inst_9 : Module R₁ M₁
inst_10 : Module R₂ M₂
inst_11 : Module R₃ M₃
inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_13 : ContinuousAdd M₂
inst_14 : ContinuousAdd M₃
g : M₂ →SL[σ₂₃] M₃
f₁ f₂ : M₁ →SL[σ₁₂] M₂
⊢ g ∘SL (f₁ + f₂) = g ∘SL f₁ + g ∘SL f₂
have h : ∀ (x : M₁),
  Eq.{u_7 + 1} (α := M₃) ((g ∘SL (f₁ + f₂) : (a : M₁) → M₃) x : M₃) ((g ∘SL f₁ + g ∘SL f₂ : (a : M₁) → M₃) x : M₃)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic (goal)
Goal:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst_3 : TopologicalSpace M₁
inst_4 : AddCommMonoid M₁
M₂ : Type u_6
inst_5 : TopologicalSpace M₂
inst_6 : AddCommMonoid M₂
M₃ : Type u_7
inst_7 : TopologicalSpace M₃
inst_8 : AddCommMonoid M₃
inst_9 : Module R₁ M₁
inst_10 : Module R₂ M₂
inst_11 : Module R₃ M₃
inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_13 : ContinuousAdd M₃
g₁ g₂ : M₂ →SL[σ₂₃] M₃
f : M₁ →SL[σ₁₂] M₂
⊢ (g₁ + g₂) ∘SL f = g₁ ∘SL f + g₂ ∘SL f
have h : ∀ (x : M₁),
  Eq.{u_7 + 1} (α := M₃) (((g₁ + g₂) ∘SL f : (a : M₁) → M₃) x : M₃) ((g₁ ∘SL f + g₂ ∘SL f : (a : M₁) → M₃) x : M₃)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic (goal)
Goal:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst_3 : TopologicalSpace M₁
inst_4 : AddCommMonoid M₁
M₂ : Type u_6
inst_5 : TopologicalSpace M₂
inst_6 : AddCommMonoid M₂
M₃ : Type u_7
inst_7 : TopologicalSpace M₃
inst_8 : AddCommMonoid M₃
inst_9 : Module R₁ M₁
inst_10 : Module R₂ M₂
inst_11 : Module R₃ M₃
inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
ι : Type u_9
s : Finset ι
inst_13 : ContinuousAdd M₂
inst_14 : ContinuousAdd M₃
g : M₂ →SL[σ₂₃] M₃
f : ι → M₁ →SL[σ₁₂] M₂
⊢ Eq (α := M₁ →SL[σ₁₃] M₃) (g.comp (σ₁₂ := σ₁₂) (∑ i ∈ s, f i)) (∑ i ∈ s, g ∘SL f i)
have h : ∀ (x : M₁),
  Eq.{u_7 + 1} (α := M₃) ((g.comp (σ₁₂ := σ₁₂) (∑ i ∈ s, f i) : (a : M₁) → M₃) x : M₃)
    ((∑ i ∈ s, g ∘SL f i : (a : M₁) → M₃) x : M₃)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic (goal)
Goal:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst_3 : TopologicalSpace M₁
inst_4 : AddCommMonoid M₁
M₂ : Type u_6
inst_5 : TopologicalSpace M₂
inst_6 : AddCommMonoid M₂
M₃ : Type u_7
inst_7 : TopologicalSpace M₃
inst_8 : AddCommMonoid M₃
inst_9 : Module R₁ M₁
inst_10 : Module R₂ M₂
inst_11 : Module R₃ M₃
inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
ι : Type u_9
s : Finset ι
inst_13 : ContinuousAdd M₃
g : ι → M₂ →SL[σ₂₃] M₃
f : M₁ →SL[σ₁₂] M₂
⊢ Eq (α := M₁ →SL[σ₁₃] M₃) (comp (σ₂₃ := σ₂₃) (∑ i ∈ s, g i) f) (∑ i ∈ s, g i ∘SL f)
have h : ∀ (x : M₁),
  Eq.{u_7 + 1} (α := M₃) ((comp (σ₂₃ := σ₂₃) (∑ i ∈ s, g i) f : (a : M₁) → M₃) x : M₃)
    ((∑ i ∈ s, g i ∘SL f : (a : M₁) → M₃) x : M₃)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic (goal)
Goal:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst_3 : TopologicalSpace M₁
inst_4 : AddCommMonoid M₁
M₂ : Type u_6
inst_5 : TopologicalSpace M₂
inst_6 : AddCommMonoid M₂
M₃ : Type u_7
inst_7 : TopologicalSpace M₃
inst_8 : AddCommMonoid M₃
inst_9 : Module R₁ M₁
inst_10 : Module R₂ M₂
inst_11 : Module R₃ M₃
inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
g : M₂ →SL[σ₂₃] M₃
f₁ f₂ : M₁ →SL[σ₁₂] M₂
hg : Function.Injective.{u_6 + 1, u_7 + 1} (α := M₂) (β := M₃) (⇑g : (a : M₂) → M₃)
h : g ∘SL f₁ = g ∘SL f₂
⊢ f₁ = f₂
have h₁ : ∀ (x : M₁), Eq.{u_6 + 1} (α := M₂) ((f₁ : (a : M₁) → M₂) x : M₂) ((f₂ : (a : M₁) → M₂) x : M₂)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic (goal)
Goal:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst_3 : TopologicalSpace M₁
inst_4 : AddCommMonoid M₁
M'₁ : Type u_5
inst_5 : TopologicalSpace M'₁
inst_6 : AddCommMonoid M'₁
M₂ : Type u_6
inst_7 : TopologicalSpace M₂
inst_8 : AddCommMonoid M₂
M₃ : Type u_7
inst_9 : TopologicalSpace M₃
inst_10 : AddCommMonoid M₃
M₄ : Type u_8
inst_11 : TopologicalSpace M₄
inst_12 : AddCommMonoid M₄
inst_13 : Module R₁ M₁
inst_14 : Module R₁ M'₁
inst_15 : Module R₂ M₂
inst_16 : Module R₃ M₃
inst_17 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
T : (M₁ →L[R₁] M₁)ˣ
x : M₁
⊢ ((↑T⁻¹ : M₁ →L[R₁] M₁) : (a : M₁) → M₁) (((↑T : M₁ →L[R₁] M₁) : (a : M₁) → M₁) x : M₁) = x
have rw : ((↑T⁻¹ : M₁ →L[R₁] M₁) * (↑T : M₁ →L[R₁] M₁) : (a : M₁) → M₁) x = x
Tactic: rw [← mul_apply, Units.inv_mul, one_apply]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic (goal)
Goal:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst_3 : TopologicalSpace M₁
inst_4 : AddCommMonoid M₁
M'₁ : Type u_5
inst_5 : TopologicalSpace M'₁
inst_6 : AddCommMonoid M'₁
M₂ : Type u_6
inst_7 : TopologicalSpace M₂
inst_8 : AddCommMonoid M₂
M₃ : Type u_7
inst_9 : TopologicalSpace M₃
inst_10 : AddCommMonoid M₃
M₄ : Type u_8
inst_11 : TopologicalSpace M₄
inst_12 : AddCommMonoid M₄
inst_13 : Module R₁ M₁
inst_14 : Module R₁ M'₁
inst_15 : Module R₂ M₂
inst_16 : Module R₃ M₃
inst_17 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
T : (M₁ →L[R₁] M₁)ˣ
x : M₁
rw : ((↑T⁻¹ : M₁ →L[R₁] M₁) * (↑T : M₁ →L[R₁] M₁) : (a : M₁) → M₁) x = x
⊢ ((↑T⁻¹ : M₁ →L[R₁] M₁) : (a : M₁) → M₁) (((↑T : M₁ →L[R₁] M₁) : (a : M₁) → M₁) x : M₁) = x
have rw₁ : (1 : (a : M₁) → M₁) x = x
Tactic: rw [← mul_apply, Units.inv_mul, one_apply]