awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Pi (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
α : Type u_5
inst_3 : Finite α
f : M →ₗ[R] α → R
s : Surjective (α := M) (β := α → R) (⇑f : (a : M) → α → R)
h :
  ∀ (x y : α),
    Eq.{u_1 + 1} (α := R)
      (((f ∘ₗ f.splittingOfFunOnFintypeSurjective s) ∘ₗ single R (fun (i : α) ↦ R) x : (a : R) → α → R) 1 y : R)
      (((id ∘ₗ single R (fun (i : α) ↦ R) x : R →ₗ[R] α → R) : (a : R) → α → R) 1 y : R)
⊢ f ∘ₗ f.splittingOfFunOnFintypeSurjective s = id
have h₁ : ∀ (x y : α),
  Eq.{u_1 + 1} (α := R)
    ((f : (a : M) → α → R)
        (sum
          ((LinearEquiv.symm (linearEquivFunOnFinite R R α) : (a : (i : α) → R) → α →₀ R)
            (Pi.single (M := fun (i : α) ↦ R) x 1))
          fun (x : α) (r : R) ↦
          r •
            sorry.choose (p := fun (a : M) ↦
              Eq (α := α → R) ((f : (a : M) → α → R) a : α → R) ((⇑(Finsupp.single x 1) : (a : α) → R) : (a : α) → R)))
        y :
      R)
    (Pi.single (M := fun (i : α) ↦ R) x 1 y : R)
Tactic: classical
  ext x y
  dsimp [splittingOfFunOnFintypeSurjective]
  rw [linearEquivFunOnFinite_symm_single, Finsupp.sum_single_index, one_smul,
    (s (Finsupp.single x 1)).choose_spec, Finsupp.single_eq_pi_single]
  rw [zero_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Pi (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
α : Type u_5
inst_3 : Finite α
f : M →ₗ[R] α → R
s : Surjective (α := M) (β := α → R) (⇑f : (a : M) → α → R)
h :
  ∀ (x y : α),
    Eq.{u_1 + 1} (α := R)
      (((f ∘ₗ f.splittingOfFunOnFintypeSurjective s) ∘ₗ single R (fun (i : α) ↦ R) x : (a : R) → α → R) 1 y : R)
      (((id ∘ₗ single R (fun (i : α) ↦ R) x : R →ₗ[R] α → R) : (a : R) → α → R) 1 y : R)
h₁ :
  ∀ (x y : α),
    Eq.{u_1 + 1} (α := R)
      ((f : (a : M) → α → R)
          (sum
            ((LinearEquiv.symm (linearEquivFunOnFinite R R α) : (a : (i : α) → R) → α →₀ R)
              (Pi.single (M := fun (i : α) ↦ R) x 1))
            fun (x : α) (r : R) ↦
            r •
              ⋯.choose (p := fun (a : M) ↦
                Eq (α := α → R) ((f : (a : M) → α → R) a : α → R)
                  ((⇑(Finsupp.single x 1) : (a : α) → R) : (a : α) → R)))
          y :
        R)
      (Pi.single (M := fun (i : α) ↦ R) x 1 y : R)
⊢ f ∘ₗ f.splittingOfFunOnFintypeSurjective s = id
have h₂ : ∀ (x y : α),
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0
      (sorry.choose (p := fun (a : M) ↦
        Eq (α := α → R) ((f : (a : M) → α → R) a : α → R) ((⇑(Finsupp.single x 1) : (a : α) → R) : (a : α) → R))) =
    0
Tactic: classical
  ext x y
  dsimp [splittingOfFunOnFintypeSurjective]
  rw [linearEquivFunOnFinite_symm_single, Finsupp.sum_single_index, one_smul,
    (s (Finsupp.single x 1)).choose_spec, Finsupp.single_eq_pi_single]
  rw [zero_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Pi (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₗ[R] N
I : Type u_6
⊢ Eq (α := Submodule R (I →₀ M)) (ker (mapRange.linearMap f)) (submodule fun (x : I) ↦ f.ker)
have h : ∀ (x : I →₀ M),
  Membership.mem (γ := Submodule R (I →₀ M)) (ker (mapRange.linearMap f)) x ↔
    Membership.mem (γ := Submodule R (I →₀ M)) (submodule fun (x : I) ↦ f.ker) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Pi (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₗ[R] N
hf : f.ker = ⊥
I : Type u_6
⊢ Eq (α := Submodule R (I →₀ N)) (LinearMap.range (mapRange.linearMap f)) (submodule fun (x : I) ↦ f.range)
have h : ∀ (x : I →₀ N),
  Membership.mem (γ := Submodule R (I →₀ N)) (LinearMap.range (mapRange.linearMap f)) x ↔
    Membership.mem (γ := Submodule R (I →₀ N)) (submodule fun (x : I) ↦ f.range) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Pi (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₗ[R] N
hf : f.ker = ⊥
I : Type u_6
x : I →₀ N
⊢ Membership.mem (γ := Submodule R (I →₀ N)) (LinearMap.range (mapRange.linearMap f)) x ↔
    Membership.mem (γ := Submodule R (I →₀ N)) (submodule fun (x : I) ↦ f.range) x
have h : Membership.mem (γ := Submodule R (I →₀ N)) (LinearMap.range (mapRange.linearMap f)) x →
  Membership.mem (γ := Submodule R (I →₀ N)) (submodule fun (x : I) ↦ f.range) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Pi (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₗ[R] N
hf : f.ker = ⊥
I : Type u_6
x : I →₀ N
h :
  Membership.mem (γ := Submodule R (I →₀ N)) (LinearMap.range (mapRange.linearMap f)) x →
    Membership.mem (γ := Submodule R (I →₀ N)) (submodule fun (x : I) ↦ f.range) x
⊢ Membership.mem (γ := Submodule R (I →₀ N)) (LinearMap.range (mapRange.linearMap f)) x ↔
    Membership.mem (γ := Submodule R (I →₀ N)) (submodule fun (x : I) ↦ f.range) x
have h₁ : Membership.mem (γ := Submodule R (I →₀ N)) (submodule fun (x : I) ↦ f.range) x →
  Membership.mem (γ := Submodule R (I →₀ N)) (LinearMap.range (mapRange.linearMap f)) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Pi (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₗ[R] N
hf : f.ker = ⊥
I : Type u_6
x : I →₀ N
hx : Membership.mem (γ := Submodule R (I →₀ N)) (submodule fun (x : I) ↦ f.range) x
⊢ Membership.mem (γ := Submodule R (I →₀ N)) (LinearMap.range (mapRange.linearMap f)) x
have h : ∀ (y : (i : I) → M) (hy : ∀ (i : I), Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) (y i) : N) ((x : (a : I) → N) i : N)),
  Membership.mem (γ := Submodule R (I →₀ N)) (LinearMap.range (mapRange.linearMap f)) x
Tactic: choose y hy using hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Pi (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₗ[R] N
hf : f.ker = ⊥
I : Type u_6
x : I →₀ N
y : (i : I) → M
hy : ∀ (i : I), Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) (y i) : N) ((x : (a : I) → N) i : N)
⊢ (mapRange.linearMap f : (a : I →₀ M) → I →₀ N) { support := x.support, toFun := y, mem_support_toFun := ⋯ } = x
have h : ∀ (a : I),
  Eq.{u_3 + 1} (α := N)
    ((((mapRange.linearMap f : (a : I →₀ M) → I →₀ N) { support := x.support, toFun := y, mem_support_toFun := sorry } :
            I →₀ N) :
          (a : I) → N)
        a :
      N)
    ((x : (a : I) → N) a : N)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Pi (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₗ[R] N
hf : f.ker = ⊥
I : Type u_6
x : I →₀ N
y : (i : I) → M
hy : ∀ (i : I), Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) (y i) : N) ((x : (a : I) → N) i : N)
⊢ Membership.mem (γ := Submodule R (I →₀ N)) (LinearMap.range (mapRange.linearMap f)) x
have h : ∀ (i : I), i ∈ x.support ↔ y i ≠ 0
Tactic: refine ⟨⟨x.support, y, fun i => ?_⟩, by ext; simp_all⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Pi (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₗ[R] N
hf : f.ker = ⊥
I : Type u_6
x : I →₀ N
y : (i : I) → M
hy : ∀ (i : I), Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) (y i) : N) ((x : (a : I) → N) i : N)
i : I
⊢ i ∈ x.support ↔ y i ≠ 0
have h : i ∈ x.support → y i ≠ 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Pi (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₗ[R] N
hf : f.ker = ⊥
I : Type u_6
x : I →₀ N
y : (i : I) → M
hy : ∀ (i : I), Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) (y i) : N) ((x : (a : I) → N) i : N)
i : I
h : i ∈ x.support → y i ≠ 0
⊢ i ∈ x.support ↔ y i ≠ 0
have h₁ : y i ≠ 0 → i ∈ x.support
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Pi (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₗ[R] N
hf : f.ker = ⊥
I : Type u_6
x : I →₀ N
y : (i : I) → M
hy : ∀ (i : I), Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) (y i) : N) ((x : (a : I) → N) i : N)
i : I
⊢ i ∈ x.support → y i ≠ 0
have h : y i = 0 → i ∉ x.support
Tactic: contrapose
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Pi (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₗ[R] N
hf : f.ker = ⊥
I : Type u_6
x : I →₀ N
y : (i : I) → M
hy : ∀ (i : I), Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) (y i) : N) ((x : (a : I) → N) i : N)
i : I
⊢ y i ≠ 0 → i ∈ x.support
have h : i ∉ x.support → y i = 0
Tactic: contrapose
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Pi (goal)
Goal:
M : Type u_5
inst : AddCommMonoid M
X : Type u_6
Y : Type u_7
inst_1 : Fintype X
inst_2 : Finite Y
inst_3 : DecidableEq Y
f : X → Y
s : X → M
y : Y
⊢ map f s y = ∑ x : X with f x = y, s x
have obtain : ∀ (s : X →₀ M),
  Eq.{u_5 + 1} (α := M) (map f ((equivFunOnFinite : (a : X →₀ M) → X → M) s) y)
    (∑ x : X with f x = y, (equivFunOnFinite : (a : X →₀ M) → X → M) s x)
Tactic: obtain ⟨s, rfl⟩ := Finsupp.equivFunOnFinite.surjective s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Pi (goal)
Goal:
M : Type u_5
inst : AddCommMonoid M
X : Type u_6
Y : Type u_7
inst_1 : Fintype X
inst_2 : Finite Y
inst_3 : DecidableEq Y
f : X → Y
y : Y
s : X →₀ M
⊢ Eq.{u_5 + 1} (α := M) (map f ((equivFunOnFinite : (a : X →₀ M) → X → M) s) y)
    (∑ x : X with f x = y, (equivFunOnFinite : (a : X →₀ M) → X → M) s x)
have dsimp : Eq.{u_5 + 1} (α := M)
  ((mapDomain f ((Equiv.symm equivFunOnFinite : (a : X → M) → X →₀ M) ((equivFunOnFinite : (a : X →₀ M) → X → M) s)) :
        (a : Y) → M)
      y :
    M)
  (∑ x : X with f x = y, (s : (a : X) → M) x : M)
Tactic: dsimp [map]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Pi (goal)
Goal:
M : Type u_5
inst : AddCommMonoid M
X : Type u_6
Y : Type u_7
inst_1 : Fintype X
inst_2 : Finite Y
inst_3 : DecidableEq Y
f : X → Y
y : Y
s : X →₀ M
⊢ Eq.{u_5 + 1} (α := M)
    ((mapDomain f ((Equiv.symm equivFunOnFinite : (a : X → M) → X →₀ M) ((equivFunOnFinite : (a : X →₀ M) → X → M) s)) :
          (a : Y) → M)
        y :
      M)
    (∑ x : X with f x = y, (s : (a : X) → M) x : M)
have simp : Eq.{u_5 + 1} (α := M) ((mapDomain f s : (a : Y) → M) y : M) (∑ x : X with f x = y, (s : (a : X) → M) x : M)
Tactic: simp only [Equiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Pi (goal)
Goal:
M : Type u_5
inst : AddCommMonoid M
X : Type u_6
Y : Type u_7
inst_1 : Fintype X
inst_2 : Finite Y
inst_3 : DecidableEq Y
f : X → Y
y : Y
s : X →₀ M
⊢ Eq.{u_5 + 1} (α := M) ((mapDomain f s : (a : Y) → M) y : M) (∑ x : X with f x = y, (s : (a : X) → M) x : M)
have nth_rw : Eq.{u_5 + 1} (α := M) ((mapDomain f (∑ a : X, Finsupp.single a ((s : (a : X) → M) a)) : (a : Y) → M) y : M)
  (∑ x : X with f x = y, (s : (a : X) → M) x : M)
Tactic: nth_rw 1 [← Finsupp.univ_sum_single s]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Pi (goal)
Goal:
M : Type u_5
inst : AddCommMonoid M
X : Type u_6
Y : Type u_7
inst_1 : Fintype X
inst_2 : Finite Y
inst_3 : DecidableEq Y
f : X → Y
y : Y
s : X →₀ M
⊢ Eq.{u_5 + 1} (α := M) ((mapDomain f (∑ a : X, Finsupp.single a ((s : (a : X) → M) a)) : (a : Y) → M) y : M)
    (∑ x : X with f x = y, (s : (a : X) → M) x : M)
have rw : Eq.{u_5 + 1} (α := M) ((∑ i : X, mapDomain f (Finsupp.single i ((s : (a : X) → M) i)) : (a : Y) → M) y : M)
  (∑ x : X with f x = y, (s : (a : X) → M) x : M)
Tactic: rw [Finsupp.mapDomain_finsetSum]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Pi (goal)
Goal:
M : Type u_5
inst : AddCommMonoid M
X : Type u_6
Y : Type u_7
inst_1 : Fintype X
inst_2 : Finite Y
inst_3 : DecidableEq Y
f : X → Y
y : Y
s : X →₀ M
⊢ Eq.{u_5 + 1} (α := M) ((∑ i : X, mapDomain f (Finsupp.single i ((s : (a : X) → M) i)) : (a : Y) → M) y : M)
    (∑ x : X with f x = y, (s : (a : X) → M) x : M)
have simp : Eq.{u_5 + 1} (α := M) (∑ c : X, ((Finsupp.single (f c) ((s : (a : X) → M) c) : Y →₀ M) : (a : Y) → M) y)
  (∑ a : X, if f a = y then (s : (a : X) → M) a else 0)
Tactic: simp [Finset.sum_filter]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Pi (goal)
Goal:
M : Type u_5
inst : AddCommMonoid M
X : Type u_6
Y : Type u_7
inst_1 : Fintype X
inst_2 : Finite Y
inst_3 : DecidableEq Y
f : X → Y
y : Y
s : X →₀ M
⊢ Eq.{u_5 + 1} (α := M) (∑ c : X, ((Finsupp.single (f c) ((s : (a : X) → M) c) : Y →₀ M) : (a : Y) → M) y)
    (∑ a : X, if f a = y then (s : (a : X) → M) a else 0)
have e_f : Eq (α := X → M) (fun (c : X) ↦ ((Finsupp.single (f c) ((s : (a : X) → M) c) : Y →₀ M) : (a : Y) → M) y) fun (a : X) ↦
  if f a = y then (s : (a : X) → M) a else 0
Tactic: congr
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Pi (goal)
Goal:
M : Type u_5
inst : AddCommMonoid M
X : Type u_6
inst_1 : Finite X
⊢ Eq (α := (s : X → M) → X → M) (map _root_.id) _root_.id
have h : ∀ (s : X → M) (x : X), map _root_.id s x = _root_.id s x
Tactic: ext s
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Pi (goal)
Goal:
M : Type u_5
inst : AddCommMonoid M
X : Type u_6
Y : Type u_7
Z : Type u_8
inst_1 : Finite X
inst_2 : Finite Y
inst_3 : Finite Z
g : Y → Z
f : X → Y
⊢ Eq (α := (s : X → M) → Z → M) (map (g ∘ f)) (map g ∘ map f)
have h : ∀ (s : X → M) (x : Z), map (g ∘ f) s x = (map g ∘ map f) s x
Tactic: ext s
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Span (goal)
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s t : Set α
h : Disjoint s t
⊢ LE.le (α := Submodule R (α →₀ M)) (⨆ a ∈ s, LinearMap.range (lsingle a)) (⨅ a ∈ t, ker (lapply a))
have refine : ∀ (a₁ : α) (h₁ : a₁ ∈ s), Eq.{u_2 + 1} (α := Submodule R M) (comap (lsingle a₁) (⨅ a ∈ t, ker (lapply a))) ⊤
Tactic: refine iSup_le fun a₁ => iSup_le fun h₁ => range_le_iff_comap.2 ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Span (goal)
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s t : Set α
h : Disjoint s t
a₁ : α
h₁ : a₁ ∈ s
⊢ Eq.{u_2 + 1} (α := Submodule R M) (comap (lsingle a₁) (⨅ a ∈ t, ker (lapply a))) ⊤
have simp : ∀ ⦃x : M⦄,
  Membership.mem (γ := Submodule R M) ⊤ x →
    ∀ (i : α) (i_1 : i ∈ t), Eq (α := M) ((lapply i ∘ₗ lsingle a₁ : (a : M) → M) x : M) (0 : M)
Tactic: simp only [(ker_comp _ _).symm, eq_top_iff, SetLike.le_def, mem_ker, comap_iInf, mem_iInf]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Span (hypothesis)
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s t : Set α
h : Disjoint s t
a₁ : α
h₁ : a₁ ∈ s
b : M
h_1 : Membership.mem (γ := Submodule R M) ⊤ b
a₂ : α
h₂ : a₂ ∈ t
⊢ Eq (α := M) ((lapply a₂ ∘ₗ lsingle a₁ : (a : M) → M) b : M) (0 : M)
have this : a₂ ≠ a₁
Tactic: have : a₂ ≠ a₁ := fun eq => h.le_bot ⟨h₁, eq.symm ▸ h₂⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Span (goal)
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ LE.le (α := Submodule R (α →₀ M)) (⨅ (a : α), ker (lapply a)) ⊥
have simp : ∀ ⦃x : α →₀ M⦄, (∀ (i : α), Eq.{u_2 + 1} (α := M) ((x : (a : α) → M) i : M) (0 : M)) → x = 0
Tactic: simp only [SetLike.le_def, mem_iInf, mem_ker, mem_bot, lapply_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Span (goal)
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq (α := Submodule R (α →₀ M)) (⨆ (a : α), LinearMap.range (lsingle a)) ⊤
have refine : ∀ (f : α →₀ M),
  Membership.mem (γ := Submodule R (α →₀ M)) ⊤ f →
    Membership.mem (γ := Submodule R (α →₀ M)) (⨆ (a : α), LinearMap.range (lsingle a)) f
Tactic: refine eq_top_iff.2 <| SetLike.le_def.2 fun f _ => ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Span (goal)
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : α →₀ M
h : Membership.mem (γ := Submodule R (α →₀ M)) ⊤ f
⊢ Membership.mem (γ := Submodule R (α →₀ M)) (⨆ (a : α), LinearMap.range (lsingle a)) f
have rw : Membership.mem (γ := Submodule R (α →₀ M)) (⨆ (a : α), LinearMap.range (lsingle a)) (f.sum single)
Tactic: rw [← sum_single f]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Span (goal)
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s t : Set α
hs : Disjoint s t
⊢ Disjoint (α := Submodule R (α →₀ M)) (⨆ a ∈ s, LinearMap.range (lsingle a)) (⨆ a ∈ t, LinearMap.range (lsingle a))
have s₁ : Disjoint (α := Submodule R (α →₀ M)) (⨅ a ∈ sᶜ, ker (lapply a)) (⨅ a ∈ tᶜ, ker (lapply a))
Tactic: refine
    (Disjoint.mono
      (lsingle_range_le_ker_lapply s sᶜ disjoint_compl_right)
      (lsingle_range_le_ker_lapply t tᶜ disjoint_compl_right))
      ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Span (goal)
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s t : Set α
hs : Disjoint s t
⊢ Disjoint (α := Submodule R (α →₀ M)) (⨅ a ∈ sᶜ, ker (lapply a)) (⨅ a ∈ tᶜ, ker (lapply a))
have rw : LE.le (α := Submodule R (α →₀ M)) ((⨅ a ∈ sᶜ, ker (lapply a)) ⊓ ⨅ a ∈ tᶜ, ker (lapply a)) ⊥
Tactic: rw [disjoint_iff_inf_le]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Span (goal)
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s t : Set α
hs : Disjoint s t
⊢ LE.le (α := Submodule R (α →₀ M)) ((⨅ a ∈ sᶜ, ker (lapply a)) ⊓ ⨅ a ∈ tᶜ, ker (lapply a)) ⊥
have refine : ∀ (i : α), LE.le (α := Submodule R (α →₀ M)) ((⨅ a ∈ sᶜ, ker (lapply a)) ⊓ ⨅ a ∈ tᶜ, ker (lapply a)) (ker (lapply i))
Tactic: refine le_trans (le_iInf fun i => ?_) iInf_ker_lapply_le_bot
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Span (goal)
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s t : Set α
hs : Disjoint s t
i : α
⊢ LE.le (α := Submodule R (α →₀ M)) ((⨅ a ∈ sᶜ, ker (lapply a)) ⊓ ⨅ a ∈ tᶜ, ker (lapply a)) (ker (lapply i))
have pos : ∀ (his : i ∈ s),
  LE.le (α := Submodule R (α →₀ M)) ((⨅ a ∈ sᶜ, ker (lapply a)) ⊓ ⨅ a ∈ tᶜ, ker (lapply a)) (ker (lapply i))
Tactic: by_cases his : i ∈ s
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Span (goal)
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s t : Set α
hs : Disjoint s t
i : α
pos :
  ∀ (his : i ∈ s),
    LE.le (α := Submodule R (α →₀ M)) ((⨅ a ∈ sᶜ, ker (lapply a)) ⊓ ⨅ a ∈ tᶜ, ker (lapply a)) (ker (lapply i))
⊢ LE.le (α := Submodule R (α →₀ M)) ((⨅ a ∈ sᶜ, ker (lapply a)) ⊓ ⨅ a ∈ tᶜ, ker (lapply a)) (ker (lapply i))
have neg : ∀ (his : i ∉ s),
  LE.le (α := Submodule R (α →₀ M)) ((⨅ a ∈ sᶜ, ker (lapply a)) ⊓ ⨅ a ∈ tᶜ, ker (lapply a)) (ker (lapply i))
Tactic: by_cases his : i ∈ s
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Span (goal)
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s t : Set α
hs : Disjoint s t
i : α
his : i ∈ s
⊢ LE.le (α := Submodule R (α →₀ M)) ((⨅ a ∈ sᶜ, ker (lapply a)) ⊓ ⨅ a ∈ tᶜ, ker (lapply a)) (ker (lapply i))
have pos : ∀ (hit : i ∈ t),
  LE.le (α := Submodule R (α →₀ M)) ((⨅ a ∈ sᶜ, ker (lapply a)) ⊓ ⨅ a ∈ tᶜ, ker (lapply a)) (ker (lapply i))
Tactic: by_cases hit : i ∈ t
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Span (goal)
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s t : Set α
hs : Disjoint s t
i : α
his : i ∈ s
pos :
  ∀ (hit : i ∈ t),
    LE.le (α := Submodule R (α →₀ M)) ((⨅ a ∈ sᶜ, ker (lapply a)) ⊓ ⨅ a ∈ tᶜ, ker (lapply a)) (ker (lapply i))
⊢ LE.le (α := Submodule R (α →₀ M)) ((⨅ a ∈ sᶜ, ker (lapply a)) ⊓ ⨅ a ∈ tᶜ, ker (lapply a)) (ker (lapply i))
have neg : ∀ (hit : i ∉ t),
  LE.le (α := Submodule R (α →₀ M)) ((⨅ a ∈ sᶜ, ker (lapply a)) ⊓ ⨅ a ∈ tᶜ, ker (lapply a)) (ker (lapply i))
Tactic: by_cases hit : i ∈ t
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Span (goal)
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s t : Set α
hs : Disjoint s t
i : α
⊢ LE.le (α := Submodule R (α →₀ M)) ((⨅ a ∈ sᶜ, ker (lapply a)) ⊓ ⨅ a ∈ tᶜ, ker (lapply a)) (ker (lapply i))
have pos : ∀ (his : i ∈ s),
  LE.le (α := Submodule R (α →₀ M)) ((⨅ a ∈ sᶜ, ker (lapply a)) ⊓ ⨅ a ∈ tᶜ, ker (lapply a)) (ker (lapply i))
Tactic: classical
    by_cases his : i ∈ s
    · by_cases hit : i ∈ t
      · exact (hs.le_bot ⟨his, hit⟩).elim
      exact inf_le_of_right_le (iInf_le_of_le i <| iInf_le _ hit)
    exact inf_le_of_left_le (iInf_le_of_le i <| iInf_le _ his)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Span (goal)
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s t : Set α
hs : Disjoint s t
i : α
pos :
  ∀ (his : i ∈ s),
    LE.le (α := Submodule R (α →₀ M)) ((⨅ a ∈ sᶜ, ker (lapply a)) ⊓ ⨅ a ∈ tᶜ, ker (lapply a)) (ker (lapply i))
⊢ LE.le (α := Submodule R (α →₀ M)) ((⨅ a ∈ sᶜ, ker (lapply a)) ⊓ ⨅ a ∈ tᶜ, ker (lapply a)) (ker (lapply i))
have neg : ∀ (his : i ∉ s),
  LE.le (α := Submodule R (α →₀ M)) ((⨅ a ∈ sᶜ, ker (lapply a)) ⊓ ⨅ a ∈ tᶜ, ker (lapply a)) (ker (lapply i))
Tactic: classical
    by_cases his : i ∈ s
    · by_cases hit : i ∈ t
      · exact (hs.le_bot ⟨his, hit⟩).elim
      exact inf_le_of_right_le (iInf_le_of_le i <| iInf_le _ hit)
    exact inf_le_of_left_le (iInf_le_of_le i <| iInf_le _ his)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Span (goal)
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
a : α
⊢ Eq (α := Submodule R (α →₀ M)) (span R (single a '' s)) (map (lsingle a) (span R s))
have rw : Eq (α := Submodule R (α →₀ M)) (span R (single a '' s)) (span R ((⇑(lsingle a) : (a : M) → α →₀ M) '' s))
Tactic: rw [← span_image]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Span (goal)
Goal:
α : Type u_1
R : Type u_5
inst : Semiring R
β : Type u_7
u : α → β
⊢ Eq (α := Submodule R (β →₀ R)) (LinearMap.range (lmapDomain R R u)) (span R (Set.range fun (x : α) ↦ single (u x) 1))
have refine_1 : LE.le (α := Submodule R (β →₀ R)) (LinearMap.range (lmapDomain R R u)) (span R (Set.range fun (x : α) ↦ single (u x) 1))
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Span (goal)
Goal:
α : Type u_1
R : Type u_5
inst : Semiring R
β : Type u_7
u : α → β
refine_1 :
  LE.le (α := Submodule R (β →₀ R)) (LinearMap.range (lmapDomain R R u))
    (span R (Set.range fun (x : α) ↦ single (u x) 1))
⊢ Eq (α := Submodule R (β →₀ R)) (LinearMap.range (lmapDomain R R u)) (span R (Set.range fun (x : α) ↦ single (u x) 1))
have refine_2 : LE.le (α := Submodule R (β →₀ R)) (span R (Set.range fun (x : α) ↦ single (u x) 1)) (LinearMap.range (lmapDomain R R u))
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Span (goal)
Goal:
α : Type u_1
R : Type u_5
inst : Semiring R
β : Type u_7
u : α → β
i : α
s : R
⊢ Membership.mem (α := β →₀ R) (γ := Submodule R (β →₀ R)) (span R (Set.range fun (x : α) ↦ single (u x) 1))
    ((lmapDomain R R u : (a : α →₀ R) → β →₀ R) (single i s) : β →₀ R)
have refine_1 : Membership.mem (γ := Submodule R (β →₀ R)) (span R (Set.range fun (x : α) ↦ single (u x) 1))
  (HSMul.hSMul (β := β →₀ R) s (single (u i) 1))
Tactic: rw [lmapDomain_apply, mapDomain_single, ← Finsupp.smul_single_one]