awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.VectorSpace (goal)
Goal:
R : Type u_1
ι : Type u_3
inst : Ring R
α : Type u_4
β : Type u_5
u : α → ι
v : β → ι
hu : Function.Injective u
h : IsCompl (Set.range u) (Set.range v)
i : ι
⊢ Eq (α := α →₀ R)
    ((lcomapDomain u hu : (a : ι →₀ R) → α →₀ R) ((Finsupp.basisSingleOne : (a : ι) → ι →₀ R) i) : α →₀ R)
    (((LinearMap.linearProjOfIsCompl (E := ι →₀ R) (span R (Set.range fun (x : β) ↦ single (v x) 1)) (F := α →₀ R)
              (lmapDomain R R u) ⋯ ⋯ :
            (ι →₀ R) →ₗ[R] α →₀ R) :
          (a : ι →₀ R) → α →₀ R)
        ((Finsupp.basisSingleOne : (a : ι) → ι →₀ R) i) :
      α →₀ R)
have inl : ∀ (i : α),
  Eq (α := α →₀ R)
    ((lcomapDomain u hu : (a : ι →₀ R) → α →₀ R) ((Finsupp.basisSingleOne : (a : ι) → ι →₀ R) (u i)) : α →₀ R)
    (((LinearMap.linearProjOfIsCompl (E := ι →₀ R) (span R (Set.range fun (x : β) ↦ single (v x) 1)) (F := α →₀ R)
              (lmapDomain R R u) sorry sorry :
            (ι →₀ R) →ₗ[R] α →₀ R) :
          (a : ι →₀ R) → α →₀ R)
        ((Finsupp.basisSingleOne : (a : ι) → ι →₀ R) (u i)) :
      α →₀ R)
Tactic: obtain ⟨i, rfl⟩ | ⟨i, rfl⟩ : i ∈ Set.range u ⊔ .range v := by rw [codisjoint_iff.mp h.2]; trivial
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.VectorSpace (goal)
Goal:
R : Type u_1
ι : Type u_3
inst : Ring R
α : Type u_4
β : Type u_5
u : α → ι
v : β → ι
hu : Function.Injective u
h : IsCompl (Set.range u) (Set.range v)
i : ι
inl :
  ∀ (i : α),
    Eq (α := α →₀ R)
      ((lcomapDomain u hu : (a : ι →₀ R) → α →₀ R) ((Finsupp.basisSingleOne : (a : ι) → ι →₀ R) (u i)) : α →₀ R)
      (((LinearMap.linearProjOfIsCompl (E := ι →₀ R) (span R (Set.range fun (x : β) ↦ single (v x) 1)) (F := α →₀ R)
                (lmapDomain R R u) ⋯ ⋯ :
              (ι →₀ R) →ₗ[R] α →₀ R) :
            (a : ι →₀ R) → α →₀ R)
          ((Finsupp.basisSingleOne : (a : ι) → ι →₀ R) (u i)) :
        α →₀ R)
⊢ Eq (α := α →₀ R)
    ((lcomapDomain u hu : (a : ι →₀ R) → α →₀ R) ((Finsupp.basisSingleOne : (a : ι) → ι →₀ R) i) : α →₀ R)
    (((LinearMap.linearProjOfIsCompl (E := ι →₀ R) (span R (Set.range fun (x : β) ↦ single (v x) 1)) (F := α →₀ R)
              (lmapDomain R R u) ⋯ ⋯ :
            (ι →₀ R) →ₗ[R] α →₀ R) :
          (a : ι →₀ R) → α →₀ R)
        ((Finsupp.basisSingleOne : (a : ι) → ι →₀ R) i) :
      α →₀ R)
have inr : ∀ (i : β),
  Eq (α := α →₀ R)
    ((lcomapDomain u hu : (a : ι →₀ R) → α →₀ R) ((Finsupp.basisSingleOne : (a : ι) → ι →₀ R) (v i)) : α →₀ R)
    (((LinearMap.linearProjOfIsCompl (E := ι →₀ R) (span R (Set.range fun (x : β) ↦ single (v x) 1)) (F := α →₀ R)
              (lmapDomain R R u) sorry sorry :
            (ι →₀ R) →ₗ[R] α →₀ R) :
          (a : ι →₀ R) → α →₀ R)
        ((Finsupp.basisSingleOne : (a : ι) → ι →₀ R) (v i)) :
      α →₀ R)
Tactic: obtain ⟨i, rfl⟩ | ⟨i, rfl⟩ : i ∈ Set.range u ⊔ .range v := by rw [codisjoint_iff.mp h.2]; trivial
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.VectorSpace (hypothesis)
Goal:
R : Type u_1
ι : Type u_3
inst : Ring R
α : Type u_4
β : Type u_5
u : α → ι
v : β → ι
hu : Function.Injective u
h : IsCompl (Set.range u) (Set.range v)
i : α
⊢ Eq (α := α →₀ R)
    ((lcomapDomain u hu : (a : ι →₀ R) → α →₀ R) ((Finsupp.basisSingleOne : (a : ι) → ι →₀ R) (u i)) : α →₀ R)
    (((LinearMap.linearProjOfIsCompl (E := ι →₀ R) (span R (Set.range fun (x : β) ↦ single (v x) 1)) (F := α →₀ R)
              (lmapDomain R R u) ⋯ ⋯ :
            (ι →₀ R) →ₗ[R] α →₀ R) :
          (a : ι →₀ R) → α →₀ R)
        ((Finsupp.basisSingleOne : (a : ι) → ι →₀ R) (u i)) :
      α →₀ R)
have this : Eq (α := ι →₀ R) (single (u i) 1) ((lmapDomain R R u : (a : α →₀ R) → ι →₀ R) (single i 1))
Tactic: have : single (u i) 1 = lmapDomain R R u (.single i 1) := by simp
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.VectorSpace (goal)
Goal:
R : Type u_1
ι : Type u_3
inst : Ring R
α : Type u_4
β : Type u_5
u : α → ι
v : β → ι
hu : Function.Injective u
h : IsCompl (Set.range u) (Set.range v)
i : α
this : Eq (α := ι →₀ R) (single (u i) 1) ((lmapDomain R R u : (a : α →₀ R) → ι →₀ R) (single i 1))
⊢ Eq (α := α →₀ R)
    ((lcomapDomain u hu : (a : ι →₀ R) → α →₀ R) ((Finsupp.basisSingleOne : (a : ι) → ι →₀ R) (u i)) : α →₀ R)
    (((LinearMap.linearProjOfIsCompl (E := ι →₀ R) (span R (Set.range fun (x : β) ↦ single (v x) 1)) (F := α →₀ R)
              (lmapDomain R R u) ⋯ ⋯ :
            (ι →₀ R) →ₗ[R] α →₀ R) :
          (a : ι →₀ R) → α →₀ R)
        ((Finsupp.basisSingleOne : (a : ι) → ι →₀ R) (u i)) :
      α →₀ R)
have inl : Eq (α := α →₀ R) (single i 1)
  (((LinearMap.linearProjOfIsCompl (E := ι →₀ R) (span R (Set.range fun (x : β) ↦ single (v x) 1)) (F := α →₀ R)
          (lmapDomain R R u) sorry sorry :
        (ι →₀ R) →ₗ[R] α →₀ R) :
      (a : ι →₀ R) → α →₀ R)
    (single (u i) 1))
Tactic: simp only [coe_basisSingleOne, lcomapDomain_apply, comapDomain_single]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.VectorSpace (goal)
Goal:
R : Type u_1
ι : Type u_3
inst : Ring R
α : Type u_4
β : Type u_5
u : α → ι
v : β → ι
hu : Function.Injective u
h : IsCompl (Set.range u) (Set.range v)
i : α
this : Eq (α := ι →₀ R) (single (u i) 1) ((lmapDomain R R u : (a : α →₀ R) → ι →₀ R) (single i 1))
⊢ Eq (α := α →₀ R) (single i 1)
    (((LinearMap.linearProjOfIsCompl (E := ι →₀ R) (span R (Set.range fun (x : β) ↦ single (v x) 1)) (F := α →₀ R)
            (lmapDomain R R u) ⋯ ⋯ :
          (ι →₀ R) →ₗ[R] α →₀ R) :
        (a : ι →₀ R) → α →₀ R)
      (single (u i) 1))
have inl : Eq (α := α →₀ R) (single i 1)
  (((LinearMap.linearProjOfIsCompl (E := ι →₀ R) (span R (Set.range fun (x : β) ↦ single (v x) 1)) (F := α →₀ R)
          (lmapDomain R R u) sorry sorry :
        (ι →₀ R) →ₗ[R] α →₀ R) :
      (a : ι →₀ R) → α →₀ R)
    ((lmapDomain R R u : (a : α →₀ R) → ι →₀ R) (single i 1)))
Tactic: rw [this, LinearMap.linearProjOfIsCompl_apply_left]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.VectorSpace (goal)
Goal:
R : Type u_1
ι : Type u_3
inst : Ring R
α : Type u_4
β : Type u_5
u : α → ι
v : β → ι
hu : Function.Injective u
h : IsCompl (Set.range u) (Set.range v)
i : α
this : Eq (α := ι →₀ R) (single (u i) 1) ((lmapDomain R R u : (a : α →₀ R) → ι →₀ R) (single i 1))
inl :
  Eq (α := α →₀ R) (single i 1)
    (((LinearMap.linearProjOfIsCompl (E := ι →₀ R) (span R (Set.range fun (x : β) ↦ single (v x) 1)) (F := α →₀ R)
            (lmapDomain R R u) ⋯ ⋯ :
          (ι →₀ R) →ₗ[R] α →₀ R) :
        (a : ι →₀ R) → α →₀ R)
      ((lmapDomain R R u : (a : α →₀ R) → ι →₀ R) (single i 1)))
⊢ Eq (α := α →₀ R) (single i 1)
    (((LinearMap.linearProjOfIsCompl (E := ι →₀ R) (span R (Set.range fun (x : β) ↦ single (v x) 1)) (F := α →₀ R)
            (lmapDomain R R u) ⋯ ⋯ :
          (ι →₀ R) →ₗ[R] α →₀ R) :
        (a : ι →₀ R) → α →₀ R)
      (single (u i) 1))
have inl₁ : Eq (α := α →₀ R) (single i 1) (single i 1)
Tactic: rw [this, LinearMap.linearProjOfIsCompl_apply_left]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.VectorSpace (goal)
Goal:
R : Type u_1
ι : Type u_3
inst : Ring R
α : Type u_4
β : Type u_5
u : α → ι
v : β → ι
hu : Function.Injective u
h : IsCompl (Set.range u) (Set.range v)
i : β
⊢ Eq (α := α →₀ R)
    ((lcomapDomain u hu : (a : ι →₀ R) → α →₀ R) ((Finsupp.basisSingleOne : (a : ι) → ι →₀ R) (v i)) : α →₀ R)
    (((LinearMap.linearProjOfIsCompl (E := ι →₀ R) (span R (Set.range fun (x : β) ↦ single (v x) 1)) (F := α →₀ R)
              (lmapDomain R R u) ⋯ ⋯ :
            (ι →₀ R) →ₗ[R] α →₀ R) :
          (a : ι →₀ R) → α →₀ R)
        ((Finsupp.basisSingleOne : (a : ι) → ι →₀ R) (v i)) :
      α →₀ R)
have inr : Eq (α := α →₀ R)
  ((lcomapDomain u hu : (a : ι →₀ R) → α →₀ R) ((Finsupp.basisSingleOne : (a : ι) → ι →₀ R) (v i)) : α →₀ R)
  (0 : α →₀ R)
Tactic: rw [LinearMap.linearProjOfIsCompl_apply_right']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.VectorSpace (goal)
Goal:
R : Type u_1
ι : Type u_3
inst : Ring R
α : Type u_4
β : Type u_5
u : α → ι
v : β → ι
hu : Function.Injective u
h : IsCompl (Set.range u) (Set.range v)
i : β
inr :
  Eq (α := α →₀ R)
    ((lcomapDomain u hu : (a : ι →₀ R) → α →₀ R) ((Finsupp.basisSingleOne : (a : ι) → ι →₀ R) (v i)) : α →₀ R)
    (0 : α →₀ R)
⊢ Eq (α := α →₀ R)
    ((lcomapDomain u hu : (a : ι →₀ R) → α →₀ R) ((Finsupp.basisSingleOne : (a : ι) → ι →₀ R) (v i)) : α →₀ R)
    (((LinearMap.linearProjOfIsCompl (E := ι →₀ R) (span R (Set.range fun (x : β) ↦ single (v x) 1)) (F := α →₀ R)
              (lmapDomain R R u) ⋯ ⋯ :
            (ι →₀ R) →ₗ[R] α →₀ R) :
          (a : ι →₀ R) → α →₀ R)
        ((Finsupp.basisSingleOne : (a : ι) → ι →₀ R) (v i)) :
      α →₀ R)
have inr₁ : Membership.mem (α := ι →₀ R) (γ := Submodule R (ι →₀ R)) (span R (Set.range fun (x : β) ↦ single (v x) 1))
  ((Finsupp.basisSingleOne : (a : ι) → ι →₀ R) (v i) : ι →₀ R)
Tactic: rw [LinearMap.linearProjOfIsCompl_apply_right']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.VectorSpace (goal)
Goal:
R : Type u_1
ι : Type u_3
inst : Ring R
α : Type u_4
β : Type u_5
u : α → ι
v : β → ι
hu : Function.Injective u
h : IsCompl (Set.range u) (Set.range v)
i : β
⊢ Eq (α := α →₀ R)
    ((lcomapDomain u hu : (a : ι →₀ R) → α →₀ R) ((Finsupp.basisSingleOne : (a : ι) → ι →₀ R) (v i)) : α →₀ R)
    (0 : α →₀ R)
have inr : ∀ (j : α),
  Eq.{u_1 + 1} (α := R)
    ((((lcomapDomain u hu : (a : ι →₀ R) → α →₀ R) ((Finsupp.basisSingleOne : (a : ι) → ι →₀ R) (v i)) : α →₀ R) :
          (a : α) → R)
        j :
      R)
    ((0 : (a : α) → R) j : R)
Tactic: ext j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.VectorSpace (goal)
Goal:
R : Type u_1
ι : Type u_3
inst : Ring R
α : Type u_4
β : Type u_5
u : α → ι
v : β → ι
hu : Function.Injective u
h : IsCompl (Set.range u) (Set.range v)
i : β
j : α
⊢ Eq.{u_1 + 1} (α := R)
    ((((lcomapDomain u hu : (a : ι →₀ R) → α →₀ R) ((Finsupp.basisSingleOne : (a : ι) → ι →₀ R) (v i)) : α →₀ R) :
          (a : α) → R)
        j :
      R)
    ((0 : (a : α) → R) j : R)
have inr : v i = u j → Eq.{u_1 + 1} (α := R) 1 0
Tactic: simp only [coe_basisSingleOne, lcomapDomain_apply, comapDomain_apply, single_apply,
        coe_zero, Pi.zero_apply, ite_eq_right_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.VectorSpace (goal)
Goal:
R : Type u_1
ι : Type u_3
inst : Ring R
α : Type u_4
β : Type u_5
u : α → ι
v : β → ι
hu : Function.Injective u
h : IsCompl (Set.range u) (Set.range v)
⊢ Eq (α := (ι →₀ R) →ₗ[R] α →₀ R) (lcomapDomain u hu)
    (LinearMap.linearProjOfIsCompl (E := ι →₀ R) (span R (Set.range fun (x : β) ↦ single (v x) 1)) (F := α →₀ R)
      (lmapDomain R R u) ⋯ ⋯)
have refine : ∀ (i : ι),
  Eq (α := α →₀ R)
    ((lcomapDomain u hu : (a : ι →₀ R) → α →₀ R) ((Finsupp.basisSingleOne : (a : ι) → ι →₀ R) i) : α →₀ R)
    (((LinearMap.linearProjOfIsCompl (E := ι →₀ R) (span R (Set.range fun (x : β) ↦ single (v x) 1)) (F := α →₀ R)
              (lmapDomain R R u) sorry sorry :
            (ι →₀ R) →ₗ[R] α →₀ R) :
          (a : ι →₀ R) → α →₀ R)
        ((Finsupp.basisSingleOne : (a : ι) → ι →₀ R) i) :
      α →₀ R)
Tactic: classical
  refine Finsupp.basisSingleOne.ext fun i ↦ ?_
  obtain ⟨i, rfl⟩ | ⟨i, rfl⟩ : i ∈ Set.range u ⊔ .range v := by rw [codisjoint_iff.mp h.2]; trivial
  · have : single (u i) 1 = lmapDomain R R u (.single i 1) := by simp
    simp only [coe_basisSingleOne, lcomapDomain_apply, comapDomain_single]
    rw [this, LinearMap.linearProjOfIsCompl_apply_left]
  · rw [LinearMap.linearProjOfIsCompl_apply_right']
    · ext j
      simp only [coe_basisSingleOne, lcomapDomain_apply, comapDomain_apply, single_apply,
        coe_zero, Pi.zero_apply, ite_eq_right_iff]
      intro hij
      exact (Set.disjoint_range_iff.mp h.1 j i hij.symm).elim
    · exact Submodule.subset_span ⟨i, rfl⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.VectorSpace (goal)
Goal:
R : Type u_1
ι : Type u_3
inst : Ring R
α : Type u_4
β : Type u_5
u : α → ι
v : β → ι
hu : Function.Injective u
h : IsCompl (Set.range u) (Set.range v)
refine :
  ∀ (i : ι),
    Eq (α := α →₀ R)
      ((lcomapDomain u hu : (a : ι →₀ R) → α →₀ R) ((Finsupp.basisSingleOne : (a : ι) → ι →₀ R) i) : α →₀ R)
      (((LinearMap.linearProjOfIsCompl (E := ι →₀ R) (span R (Set.range fun (x : β) ↦ single (v x) 1)) (F := α →₀ R)
                (lmapDomain R R u) ⋯ ⋯ :
              (ι →₀ R) →ₗ[R] α →₀ R) :
            (a : ι →₀ R) → α →₀ R)
          ((Finsupp.basisSingleOne : (a : ι) → ι →₀ R) i) :
        α →₀ R)
⊢ Eq (α := (ι →₀ R) →ₗ[R] α →₀ R) (lcomapDomain u hu)
    (LinearMap.linearProjOfIsCompl (E := ι →₀ R) (span R (Set.range fun (x : β) ↦ single (v x) 1)) (F := α →₀ R)
      (lmapDomain R R u) ⋯ ⋯)
have inl : ∀ (i : α),
  Eq (α := α →₀ R)
    ((lcomapDomain u hu : (a : ι →₀ R) → α →₀ R) ((Finsupp.basisSingleOne : (a : ι) → ι →₀ R) (u i)) : α →₀ R)
    (((LinearMap.linearProjOfIsCompl (E := ι →₀ R) (span R (Set.range fun (x : β) ↦ single (v x) 1)) (F := α →₀ R)
              (lmapDomain R R u) sorry sorry :
            (ι →₀ R) →ₗ[R] α →₀ R) :
          (a : ι →₀ R) → α →₀ R)
        ((Finsupp.basisSingleOne : (a : ι) → ι →₀ R) (u i)) :
      α →₀ R)
Tactic: classical
  refine Finsupp.basisSingleOne.ext fun i ↦ ?_
  obtain ⟨i, rfl⟩ | ⟨i, rfl⟩ : i ∈ Set.range u ⊔ .range v := by rw [codisjoint_iff.mp h.2]; trivial
  · have : single (u i) 1 = lmapDomain R R u (.single i 1) := by simp
    simp only [coe_basisSingleOne, lcomapDomain_apply, comapDomain_single]
    rw [this, LinearMap.linearProjOfIsCompl_apply_left]
  · rw [LinearMap.linearProjOfIsCompl_apply_right']
    · ext j
      simp only [coe_basisSingleOne, lcomapDomain_apply, comapDomain_apply, single_apply,
        coe_zero, Pi.zero_apply, ite_eq_right_iff]
      intro hij
      exact (Set.disjoint_range_iff.mp h.1 j i hij.symm).elim
    · exact Submodule.subset_span ⟨i, rfl⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.VectorSpace (goal)
Goal:
R : Type u_1
ι : Type u_3
inst : Ring R
α : Type u_4
β : Type u_5
u : α → ι
v : β → ι
hu : Function.Injective u
h : IsCompl (Set.range u) (Set.range v)
refine :
  ∀ (i : ι),
    Eq (α := α →₀ R)
      ((lcomapDomain u hu : (a : ι →₀ R) → α →₀ R) ((Finsupp.basisSingleOne : (a : ι) → ι →₀ R) i) : α →₀ R)
      (((LinearMap.linearProjOfIsCompl (E := ι →₀ R) (span R (Set.range fun (x : β) ↦ single (v x) 1)) (F := α →₀ R)
                (lmapDomain R R u) ⋯ ⋯ :
              (ι →₀ R) →ₗ[R] α →₀ R) :
            (a : ι →₀ R) → α →₀ R)
          ((Finsupp.basisSingleOne : (a : ι) → ι →₀ R) i) :
        α →₀ R)
inl :
  ∀ (i : α),
    Eq (α := α →₀ R)
      ((lcomapDomain u hu : (a : ι →₀ R) → α →₀ R) ((Finsupp.basisSingleOne : (a : ι) → ι →₀ R) (u i)) : α →₀ R)
      (((LinearMap.linearProjOfIsCompl (E := ι →₀ R) (span R (Set.range fun (x : β) ↦ single (v x) 1)) (F := α →₀ R)
                (lmapDomain R R u) ⋯ ⋯ :
              (ι →₀ R) →ₗ[R] α →₀ R) :
            (a : ι →₀ R) → α →₀ R)
          ((Finsupp.basisSingleOne : (a : ι) → ι →₀ R) (u i)) :
        α →₀ R)
⊢ Eq (α := (ι →₀ R) →ₗ[R] α →₀ R) (lcomapDomain u hu)
    (LinearMap.linearProjOfIsCompl (E := ι →₀ R) (span R (Set.range fun (x : β) ↦ single (v x) 1)) (F := α →₀ R)
      (lmapDomain R R u) ⋯ ⋯)
have inr : ∀ (i : β),
  Eq (α := α →₀ R)
    ((lcomapDomain u hu : (a : ι →₀ R) → α →₀ R) ((Finsupp.basisSingleOne : (a : ι) → ι →₀ R) (v i)) : α →₀ R)
    (((LinearMap.linearProjOfIsCompl (E := ι →₀ R) (span R (Set.range fun (x : β) ↦ single (v x) 1)) (F := α →₀ R)
              (lmapDomain R R u) sorry sorry :
            (ι →₀ R) →ₗ[R] α →₀ R) :
          (a : ι →₀ R) → α →₀ R)
        ((Finsupp.basisSingleOne : (a : ι) → ι →₀ R) (v i)) :
      α →₀ R)
Tactic: classical
  refine Finsupp.basisSingleOne.ext fun i ↦ ?_
  obtain ⟨i, rfl⟩ | ⟨i, rfl⟩ : i ∈ Set.range u ⊔ .range v := by rw [codisjoint_iff.mp h.2]; trivial
  · have : single (u i) 1 = lmapDomain R R u (.single i 1) := by simp
    simp only [coe_basisSingleOne, lcomapDomain_apply, comapDomain_single]
    rw [this, LinearMap.linearProjOfIsCompl_apply_left]
  · rw [LinearMap.linearProjOfIsCompl_apply_right']
    · ext j
      simp only [coe_basisSingleOne, lcomapDomain_apply, comapDomain_apply, single_apply,
        coe_zero, Pi.zero_apply, ite_eq_right_iff]
      intro hij
      exact (Set.disjoint_range_iff.mp h.1 j i hij.symm).elim
    · exact Submodule.subset_span ⟨i, rfl⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.VectorSpace (goal)
Goal:
R : Type u_1
M : Type u_2
n : Type u_3
inst : DecidableEq n
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Finite n
b : Basis n R M
i : n
⊢ Eq.{u_2 + 1} (α := M) ((b.equivFun.symm : (a : n → R) → M) (Pi.single (M := fun (a : n) ↦ R) i 1) : M)
    ((b : (a : n) → M) i : M)
have intro : ∀ (val : Fintype n),
  Eq.{u_2 + 1} (α := M) ((b.equivFun.symm : (a : n → R) → M) (Pi.single (M := fun (a : n) ↦ R) i 1) : M)
    ((b : (a : n) → M) i : M)
Tactic: cases nonempty_fintype n
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.VectorSpace (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
ι : Type u_3
B : Basis ι R S
i : ι
r : R
s : S
⊢ (((B.repr : (a : S) → ι →₀ R) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) r : S) s) : ι →₀ R) : (a : ι) → R)
      i =
    HMul.hMul (β := R) r ((((B.repr : (a : S) → ι →₀ R) s : ι →₀ R) : (a : ι) → R) i : R)
have rw : (((B.repr : (a : S) → ι →₀ R) (HSMul.hSMul (α := S) ((algebraMap R S : (a : R) → S) r : S) s) : ι →₀ R) : (a : ι) → R)
    i =
  HMul.hMul (β := R) r ((((B.repr : (a : S) → ι →₀ R) s : ι →₀ R) : (a : ι) → R) i : R)
Tactic: rw [← smul_eq_mul, ← smul_eq_mul, algebraMap_smul, map_smul, Finsupp.smul_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.VectorSpace (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
ι : Type u_3
B : Basis ι R S
i : ι
r : R
s : S
rw :
  (((B.repr : (a : S) → ι →₀ R) (HSMul.hSMul (α := S) ((algebraMap R S : (a : R) → S) r : S) s) : ι →₀ R) : (a : ι) → R)
      i =
    HMul.hMul (β := R) r ((((B.repr : (a : S) → ι →₀ R) s : ι →₀ R) : (a : ι) → R) i : R)
⊢ (((B.repr : (a : S) → ι →₀ R) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) r : S) s) : ι →₀ R) : (a : ι) → R)
      i =
    HMul.hMul (β := R) r ((((B.repr : (a : S) → ι →₀ R) s : ι →₀ R) : (a : ι) → R) i : R)
have rw₁ : (((B.repr : (a : S) → ι →₀ R) (HSMul.hSMul (α := S) ((algebraMap R S : (a : R) → S) r : S) s) : ι →₀ R) : (a : ι) → R)
    i =
  HSMul.hSMul (β := R) r ((((B.repr : (a : S) → ι →₀ R) s : ι →₀ R) : (a : ι) → R) i : R)
Tactic: rw [← smul_eq_mul, ← smul_eq_mul, algebraMap_smul, map_smul, Finsupp.smul_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.VectorSpace (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
ι : Type u_3
B : Basis ι R S
i : ι
r : R
s : S
rw :
  (((B.repr : (a : S) → ι →₀ R) (HSMul.hSMul (α := S) ((algebraMap R S : (a : R) → S) r : S) s) : ι →₀ R) : (a : ι) → R)
      i =
    HMul.hMul (β := R) r ((((B.repr : (a : S) → ι →₀ R) s : ι →₀ R) : (a : ι) → R) i : R)
rw₁ :
  (((B.repr : (a : S) → ι →₀ R) (HSMul.hSMul (α := S) ((algebraMap R S : (a : R) → S) r : S) s) : ι →₀ R) : (a : ι) → R)
      i =
    HSMul.hSMul (β := R) r ((((B.repr : (a : S) → ι →₀ R) s : ι →₀ R) : (a : ι) → R) i : R)
⊢ (((B.repr : (a : S) → ι →₀ R) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) r : S) s) : ι →₀ R) : (a : ι) → R)
      i =
    HMul.hMul (β := R) r ((((B.repr : (a : S) → ι →₀ R) s : ι →₀ R) : (a : ι) → R) i : R)
have rw₂ : (((B.repr : (a : S) → ι →₀ R) (r • s) : ι →₀ R) : (a : ι) → R) i =
  HSMul.hSMul (β := R) r ((((B.repr : (a : S) → ι →₀ R) s : ι →₀ R) : (a : ι) → R) i : R)
Tactic: rw [← smul_eq_mul, ← smul_eq_mul, algebraMap_smul, map_smul, Finsupp.smul_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.VectorSpace (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
ι : Type u_3
B : Basis ι R S
i : ι
r : R
s : S
rw :
  (((B.repr : (a : S) → ι →₀ R) (HSMul.hSMul (α := S) ((algebraMap R S : (a : R) → S) r : S) s) : ι →₀ R) : (a : ι) → R)
      i =
    HMul.hMul (β := R) r ((((B.repr : (a : S) → ι →₀ R) s : ι →₀ R) : (a : ι) → R) i : R)
rw₁ :
  (((B.repr : (a : S) → ι →₀ R) (HSMul.hSMul (α := S) ((algebraMap R S : (a : R) → S) r : S) s) : ι →₀ R) : (a : ι) → R)
      i =
    HSMul.hSMul (β := R) r ((((B.repr : (a : S) → ι →₀ R) s : ι →₀ R) : (a : ι) → R) i : R)
rw₂ :
  (((B.repr : (a : S) → ι →₀ R) (r • s) : ι →₀ R) : (a : ι) → R) i =
    HSMul.hSMul (β := R) r ((((B.repr : (a : S) → ι →₀ R) s : ι →₀ R) : (a : ι) → R) i : R)
⊢ (((B.repr : (a : S) → ι →₀ R) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) r : S) s) : ι →₀ R) : (a : ι) → R)
      i =
    HMul.hMul (β := R) r ((((B.repr : (a : S) → ι →₀ R) s : ι →₀ R) : (a : ι) → R) i : R)
have rw₃ : (HSMul.hSMul (β := ι →₀ R) r ((B.repr : (a : S) → ι →₀ R) s : ι →₀ R) : (a : ι) → R) i =
  HSMul.hSMul (β := R) r ((((B.repr : (a : S) → ι →₀ R) s : ι →₀ R) : (a : ι) → R) i : R)
Tactic: rw [← smul_eq_mul, ← smul_eq_mul, algebraMap_smul, map_smul, Finsupp.smul_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.VectorSpace (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
ι : Type u_3
B : Basis ι R S
i : ι
r : R
s : S
rw :
  (((B.repr : (a : S) → ι →₀ R) (HSMul.hSMul (α := S) ((algebraMap R S : (a : R) → S) r : S) s) : ι →₀ R) : (a : ι) → R)
      i =
    HMul.hMul (β := R) r ((((B.repr : (a : S) → ι →₀ R) s : ι →₀ R) : (a : ι) → R) i : R)
rw₁ :
  (((B.repr : (a : S) → ι →₀ R) (HSMul.hSMul (α := S) ((algebraMap R S : (a : R) → S) r : S) s) : ι →₀ R) : (a : ι) → R)
      i =
    HSMul.hSMul (β := R) r ((((B.repr : (a : S) → ι →₀ R) s : ι →₀ R) : (a : ι) → R) i : R)
rw₂ :
  (((B.repr : (a : S) → ι →₀ R) (r • s) : ι →₀ R) : (a : ι) → R) i =
    HSMul.hSMul (β := R) r ((((B.repr : (a : S) → ι →₀ R) s : ι →₀ R) : (a : ι) → R) i : R)
rw₃ :
  (HSMul.hSMul (β := ι →₀ R) r ((B.repr : (a : S) → ι →₀ R) s : ι →₀ R) : (a : ι) → R) i =
    HSMul.hSMul (β := R) r ((((B.repr : (a : S) → ι →₀ R) s : ι →₀ R) : (a : ι) → R) i : R)
⊢ (((B.repr : (a : S) → ι →₀ R) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) r : S) s) : ι →₀ R) : (a : ι) → R)
      i =
    HMul.hMul (β := R) r ((((B.repr : (a : S) → ι →₀ R) s : ι →₀ R) : (a : ι) → R) i : R)
have rw₄ : HSMul.hSMul (β := R) r ((((B.repr : (a : S) → ι →₀ R) s : ι →₀ R) : (a : ι) → R) i : R) =
  HSMul.hSMul (β := R) r ((((B.repr : (a : S) → ι →₀ R) s : ι →₀ R) : (a : ι) → R) i : R)
Tactic: rw [← smul_eq_mul, ← smul_eq_mul, algebraMap_smul, map_smul, Finsupp.smul_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FixedSubmodule (goal)
Goal:
R : Type u_4
inst : Ring R
V : Type u_5
inst_1 : AddCommGroup V
inst_2 : Module R V
f : V →ₗ[R] V
⊢ f.fixedSubmodule = (f - id).ker
have h : ∀ (x : V), x ∈ f.fixedSubmodule ↔ x ∈ (f - id).ker
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.FixedSubmodule (goal)
Goal:
R : Type u_1
inst : Semiring R
V : Type u_3
inst_1 : AddCommMonoid V
inst_2 : Module R V
e : V ≃ₗ[R] V
W : Submodule R V
hW : W ≤ (↑e : V →ₗ[R] V).fixedSubmodule
⊢ map (DistribSMul.toLinearMap R V e) W = W
have a : map (DistribSMul.toLinearMap R V e) W ≤ W
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.LinearAlgebra.FixedSubmodule (goal)
Goal:
R : Type u_1
inst : Semiring R
V : Type u_3
inst_1 : AddCommMonoid V
inst_2 : Module R V
e : V ≃ₗ[R] V
W : Submodule R V
hW : W ≤ (↑e : V →ₗ[R] V).fixedSubmodule
a : map (DistribSMul.toLinearMap R V e) W ≤ W
⊢ map (DistribSMul.toLinearMap R V e) W = W
have a₁ : W ≤ map (DistribSMul.toLinearMap R V e) W
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.LinearAlgebra.FixedSubmodule (goal)
Goal:
R : Type u_1
inst : Semiring R
V : Type u_3
inst_1 : AddCommMonoid V
inst_2 : Module R V
e : V ≃ₗ[R] V
W : Submodule R V
hW : W ≤ (↑e : V →ₗ[R] V).fixedSubmodule
x : V
hx : x ∈ W
⊢ Membership.mem (α := V) W ((DistribSMul.toLinearMap R V e : (a : V) → V) x : V)
have a : (e : (a : V) → V) x = x
Tactic: suffices e x = x by simpa [this, coe_coe]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FixedSubmodule (goal)
Goal:
R : Type u_1
inst : Semiring R
V : Type u_3
inst_1 : AddCommMonoid V
inst_2 : Module R V
e : V ≃ₗ[R] V
W : Submodule R V
hW : W ≤ (↑e : V →ₗ[R] V).fixedSubmodule
x : V
hx : x ∈ W
⊢ (e : (a : V) → V) x = x
have a : x ∈ (↑e : V →ₗ[R] V).fixedSubmodule
Tactic: rw [← coe_toLinearMap, ← mem_fixedSubmodule_iff]