awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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)
h₂ :
  ∀ (x y : α),
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0
        (⋯.choose (p := fun (a : M) ↦
          Eq (α := α → R) ((f : (a : M) → α → R) a : α → R) ((⇑(Finsupp.single x 1) : (a : α) → R) : (a : α) → R))) =
      0
⊢ f ∘ₗ f.splittingOfFunOnFintypeSurjective s = id

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]

Premises used: Finsupp.sum_single_index, one_smul, zero_smul, LinearMap.splittingOfFunOnFintypeSurjective, Finsupp.linearEquivFunOnFinite_symm_single, Finsupp.single_eq_pi_single
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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)
⊢ LeftInverse (α := α → R) (β := M) (⇑f : (a : M) → α → R) (⇑(f.splittingOfFunOnFintypeSurjective s) : (a : α → R) → M)

Tactic:
fun g =>
  LinearMap.congr_fun (splittingOfFunOnFintypeSurjective_splits f s) g

Premises used: Function.LeftInverse, LinearMap.splittingOfFunOnFintypeSurjective_splits, LinearMap.congr_fun
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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)
⊢ Injective (α := α → R) (β := M) (⇑(f.splittingOfFunOnFintypeSurjective s) : (a : α → R) → M)

Tactic:
(leftInverse_splittingOfFunOnFintypeSurjective f s).injective

Premises used: Function.LeftInverse.injective, LinearMap.leftInverse_splittingOfFunOnFintypeSurjective
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
α : Type u_5
S : α → Submodule R M
x : α →₀ M
⊢ x ∈ submodule S ↔ ∀ (i : α), Membership.mem (α := M) (S i) ((x : (a : α) → M) i : M)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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
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
⊢ Eq (α := Submodule R (I →₀ M)) (ker (mapRange.linearMap f)) (submodule fun (x : I) ↦ f.ker)

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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
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:
simp [Finsupp.ext_iff]

Premises used: Finsupp.ext_iff
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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
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
⊢ Eq (α := Submodule R (I →₀ N)) (LinearMap.range (mapRange.linearMap f)) (submodule fun (x : I) ↦ f.range)

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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
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
⊢ 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
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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 →₀ M
hy : (mapRange.linearMap f : (a : I →₀ M) → I →₀ N) y = x
⊢ Membership.mem (γ := Submodule R (I →₀ N)) (submodule fun (x : I) ↦ f.range) x

Tactic:
simp [← hy]
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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
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
⊢ Membership.mem (γ := Submodule R (I →₀ N)) (LinearMap.range (mapRange.linearMap f)) x

Tactic:
choose y hy using hx
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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)
h :
  ∀ (a : I),
    Eq.{u_3 + 1} (α := N)
      ((((mapRange.linearMap f : (a : I →₀ M) → I →₀ N) { support := x.support, toFun := y, mem_support_toFun := ⋯ } :
              I →₀ N) :
            (a : I) → N)
          a :
        N)
      ((x : (a : I) → N) a : N)
⊢ (mapRange.linearMap f : (a : I →₀ M) → I →₀ N) { support := x.support, toFun := y, mem_support_toFun := ⋯ } = x

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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)
a : I
⊢ Eq.{u_3 + 1} (α := N)
    ((((mapRange.linearMap f : (a : I →₀ M) → I →₀ N) { support := x.support, toFun := y, mem_support_toFun := ⋯ } :
            I →₀ N) :
          (a : I) → N)
        a :
      N)
    ((x : (a : I) → N) a : N)

Tactic:
simp_all
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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)
h : ∀ (i : I), i ∈ x.support ↔ y i ≠ 0
⊢ Membership.mem (γ := Submodule R (I →₀ N)) (LinearMap.range (mapRange.linearMap f)) x

Tactic:
refine ⟨⟨x.support, y, fun i => ?_⟩, by ext; simp_all⟩
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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
h₁ : y i ≠ 0 → i ∈ x.support
⊢ i ∈ x.support ↔ y i ≠ 0

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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 : y i = 0 → i ∉ x.support
⊢ i ∈ x.support → y i ≠ 0

Tactic:
contrapose
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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
⊢ y i ≠ 0 → i ∈ x.support

Tactic:
contrapose
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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

Tactic:
simp_all +contextual [← hy, map_zero, LinearMap.ker_eq_bot'.1 hf]

Premises used: map_zero, LinearMap.ker_eq_bot', Iff.mp
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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

Tactic:
simp_all +contextual [← hy, map_zero, LinearMap.ker_eq_bot'.1 hf]

Premises used: map_zero, LinearMap.ker_eq_bot', Iff.mp
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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
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)
⊢ map f s y = ∑ x : X with f x = y, s x

Tactic:
obtain ⟨s, rfl⟩ := Finsupp.equivFunOnFinite.surjective s

Premises used: Finsupp.equivFunOnFinite, Equiv.surjective, rfl
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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
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)
⊢ 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:
dsimp [map]

Premises used: FunOnFinite.map
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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
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)
⊢ 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:
simp only [Equiv.symm_apply_apply]

Premises used: Equiv.symm_apply_apply
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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
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)
⊢ 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:
nth_rw 1 [← Finsupp.univ_sum_single s]

Premises used: Finsupp.univ_sum_single
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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
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)
⊢ 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:
rw [Finsupp.mapDomain_finsetSum]

Premises used: Finsupp.mapDomain_finsetSum
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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
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)
⊢ 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:
simp [Finset.sum_filter]

Premises used: Finset.sum_filter
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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
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
⊢ 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:
congr
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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 (α := 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:
aesop
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
Goal:
M : Type u_5
inst : AddCommMonoid M
X : Type u_6
Y : Type u_7
inst_1 : Finite X
inst_2 : Finite Y
inst_3 : DecidableEq X
inst_4 : DecidableEq Y
f : X → Y
x : X
m : M
⊢ Eq (α := Y → M) (map f (Pi.single (M := fun (a : X) ↦ M) x m)) (Pi.single (M := fun (j : Y) ↦ M) (f x) m)

Tactic:
simp [map]

Premises used: FunOnFinite.map
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
Goal:
M : Type u_5
inst : AddCommMonoid M
X : Type u_6
inst_1 : Finite X
h : ∀ (s : X → M) (x : X), map _root_.id s x = _root_.id s x
⊢ Eq (α := (s : X → M) → X → M) (map _root_.id) _root_.id

Tactic:
ext s
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
Goal:
M : Type u_5
inst : AddCommMonoid M
X : Type u_6
inst_1 : Finite X
s : X → M
x : X
⊢ map _root_.id s x = _root_.id s x

Tactic:
simp [map]

Premises used: FunOnFinite.map
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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
h : ∀ (s : X → M) (x : Z), map (g ∘ f) s x = (map g ∘ map f) s x
⊢ Eq (α := (s : X → M) → Z → M) (map (g ∘ f)) (map g ∘ map f)

Tactic:
ext s
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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
s : X → M
x : Z
⊢ map (g ∘ f) s x = (map g ∘ map f) s x

Tactic:
simp [map, Finsupp.mapDomain_comp]

Premises used: FunOnFinite.map, Finsupp.mapDomain_comp
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
Goal:
R : Type u_5
M : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
X : Type u_7
Y : Type u_8
inst_3 : Fintype X
inst_4 : Finite Y
inst_5 : DecidableEq Y
f : X → Y
s : X → M
y : Y
⊢ (linearMap R M f : (a : X → M) → Y → M) s y = Finset.sum {x : X | f x = y} s

Tactic:
apply map_apply_apply

Premises used: FunOnFinite.map_apply_apply
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
Goal:
R : Type u_5
M : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
X : Type u_7
Y : Type u_8
inst_3 : Finite X
inst_4 : Finite Y
inst_5 : DecidableEq X
inst_6 : DecidableEq Y
f : X → Y
x : X
m : M
⊢ Eq (α := Y → M) ((linearMap R M f : (a : X → M) → Y → M) (Pi.single (M := fun (a : X) ↦ M) x m) : Y → M)
    (Pi.single (M := fun (j : Y) ↦ M) (f x) m : (j : Y) → M)

Tactic:
apply map_piSingle

Premises used: FunOnFinite.map_piSingle
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
Goal:
R : Type u_5
M : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
X : Type u_7
inst_3 : Finite X
⊢ Eq (α := (X → M) →ₗ[R] X → M) (linearMap R M _root_.id) LinearMap.id

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
Goal:
R : Type u_5
M : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
X : Type u_7
inst_3 : Finite X
⊢ Eq (α := (X → M) →ₗ[R] X → M) (linearMap R M _root_.id) LinearMap.id

Tactic:
classical
  aesop
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
Goal:
R : Type u_5
M : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
X : Type u_7
Y : Type u_8
Z : Type u_9
inst_3 : Finite X
inst_4 : Finite Y
inst_5 : Finite Z
f : X → Y
g : Y → Z
⊢ Eq (α := (X → M) →ₗ[R] Z → M) (linearMap R M (g ∘ f)) (linearMap R M g ∘ₗ linearMap R M f)

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
Goal:
R : Type u_5
M : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
X : Type u_7
Y : Type u_8
Z : Type u_9
inst_3 : Finite X
inst_4 : Finite Y
inst_5 : Finite Z
f : X → Y
g : Y → Z
⊢ Eq (α := (X → M) →ₗ[R] Z → M) (linearMap R M (g ∘ f)) (linearMap R M g ∘ₗ linearMap R M f)

Tactic:
classical
  aesop
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
a : α
⊢ Eq.{u_2 + 1} (α := Submodule R M) (ker (lsingle a)) ⊥

Tactic:
ker_eq_bot_of_injective (single_injective a)

Premises used: Finsupp.single_injective, LinearMap.ker_eq_bot_of_injective
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
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))

Tactic:
iSup_le fun a₁ => iSup_le fun h₁ => range_le_iff_comap.2 ?_

Premises used: Iff.mpr, Set.Mem, LinearMap.range_le_iff_comap, iSup_le
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
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
refine : ∀ (a₁ : α) (h₁ : a₁ ∈ s), Eq.{u_2 + 1} (α := Submodule R M) (comap (lsingle a₁) (⨅ a ∈ t, ker (lapply a))) ⊤
⊢ LE.le (α := Submodule R (α →₀ M)) (⨆ a ∈ s, LinearMap.range (lsingle a)) (⨅ a ∈ t, ker (lapply a))

Tactic:
refine iSup_le fun a₁ => iSup_le fun h₁ => range_le_iff_comap.2 ?_

Premises used: Iff.mpr, LinearMap.range_le_iff_comap, iSup_le
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
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
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)
⊢ Eq.{u_2 + 1} (α := Submodule R M) (comap (lsingle a₁) (⨅ a ∈ t, ker (lapply a))) ⊤

Tactic:
simp only [(ker_comp _ _).symm, eq_top_iff, SetLike.le_def, mem_ker, comap_iInf, mem_iInf]

Premises used: Submodule.mem_iInf, eq_top_iff, SetLike.le_def, Submodule.comap_iInf, LinearMap.ker_comp, LinearMap.mem_ker, Eq.symm
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
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
_ :
  Membership.mem (γ := Submodule R M) ⊤ b →
    ∀ (i : α) (i_1 : i ∈ t), Eq (α := M) ((lapply i ∘ₗ lsingle a₁ : (a : M) → M) b : M) (0 : M)
⊢ Membership.mem (γ := Submodule R M) ⊤ b →
    ∀ (i : α) (i_1 : i ∈ t), Eq (α := M) ((lapply i ∘ₗ lsingle a₁ : (a : M) → M) b : M) (0 : M)

Tactic:
_
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
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
⊢ a₂ ≠ a₁

Tactic:
have : a₂ ≠ a₁ := fun eq => h.le_bot ⟨h₁, eq.symm ▸ h₂⟩
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
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
this : a₂ ≠ a₁
⊢ Eq (α := M) ((lapply a₂ ∘ₗ lsingle a₁ : (a : M) → M) b : M) (0 : M)

Tactic:
single_eq_of_ne this

Premises used: Function.update, Finsupp.single_eq_of_ne, Pi.single, dite
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
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
this : a₂ ≠ a₁
⊢ Eq (α := M) ((lapply a₂ ∘ₗ lsingle a₁ : (a : M) → M) b : M) (0 : M)

Tactic:
exact single_eq_of_ne this

Premises used: Finsupp.single_eq_of_ne
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
simp : ∀ ⦃x : α →₀ M⦄, (∀ (i : α), Eq.{u_2 + 1} (α := M) ((x : (a : α) → M) i : M) (0 : M)) → x = 0
⊢ LE.le (α := Submodule R (α →₀ M)) (⨅ (a : α), ker (lapply a)) ⊥

Tactic:
simp only [SetLike.le_def, mem_iInf, mem_ker, mem_bot, lapply_apply]

Premises used: Submodule.mem_iInf, Submodule.mem_bot, SetLike.le_def, LinearMap.mem_ker, Finsupp.lapply_apply
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ ∀ ⦃x : α →₀ M⦄, (∀ (i : α), Eq.{u_2 + 1} (α := M) ((x : (a : α) → M) i : M) (0 : M)) → x = 0

Tactic:
fun a h => Finsupp.ext h

Premises used: Finsupp.ext
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ ∀ ⦃x : α →₀ M⦄, (∀ (i : α), Eq.{u_2 + 1} (α := M) ((x : (a : α) → M) i : M) (0 : M)) → x = 0

Tactic:
exact fun a h => Finsupp.ext h

Premises used: Finsupp.ext
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
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)) ⊤

Tactic:
eq_top_iff.2 <| SetLike.le_def.2 fun f _ => ?_

Premises used: Iff.mpr, eq_top_iff, SetLike.le_def