awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Supported (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
α' : Type u_7
f : α → α'
s : Set α
h : Nonempty α
l : α' →₀ M
hl : Membership.mem (γ := Submodule R (α' →₀ M)) (supported M R (f '' s)) l
⊢ Membership.mem (γ := Submodule R (α' →₀ M)) (map (lmapDomain M R f) (supported M R s)) l
have inr : ∀ (x : α)
  (hx :
    x ∈ (↑(support.{u_1, u_2} (M := M) ((lmapDomain M R (Function.invFunOn f s) : (a : α' →₀ M) → α →₀ M) l)) : Set α)),
  x ∈ s
Tactic: refine ⟨(lmapDomain M R (Function.invFunOn f s) : (α' →₀ M) →ₗ[R] α →₀ M) l, fun x hx => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Supported (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
α' : Type u_7
f : α → α'
s : Set α
h : Nonempty α
l : α' →₀ M
hl : Membership.mem (γ := Submodule R (α' →₀ M)) (supported M R (f '' s)) l
inr :
  ∀ (x : α)
    (hx :
      x ∈
        (↑(support.{u_1, u_2} (M := M) ((lmapDomain M R (Function.invFunOn f s) : (a : α' →₀ M) → α →₀ M) l)) : Set α)),
    x ∈ s
⊢ Membership.mem (γ := Submodule R (α' →₀ M)) (map (lmapDomain M R f) (supported M R s)) l
have inr₁ : (lmapDomain M R f : (a : α →₀ M) → α' →₀ M) ((lmapDomain M R (Function.invFunOn f s) : (a : α' →₀ M) → α →₀ M) l) = l
Tactic: refine ⟨(lmapDomain M R (Function.invFunOn f s) : (α' →₀ M) →ₗ[R] α →₀ M) l, fun x hx => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Supported (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
α' : Type u_7
f : α → α'
s : Set α
h : Nonempty α
l : α' →₀ M
hl : Membership.mem (γ := Submodule R (α' →₀ M)) (supported M R (f '' s)) l
x : α
hx : x ∈ (↑(support.{u_1, u_2} (M := M) ((lmapDomain M R (Function.invFunOn f s) : (a : α' →₀ M) → α →₀ M) l)) : Set α)
⊢ x ∈ s
have inr : ∀ (c : α') (hc : c ∈ l.support)
  (hx :
    Function.invFunOn f s c ∈
      (↑(support.{u_1, u_2} (M := M) ((lmapDomain M R (Function.invFunOn f s) : (a : α' →₀ M) → α →₀ M) l)) : Set α)),
  Function.invFunOn f s c ∈ s
Tactic: rcases Finset.mem_image.1 (mapDomain_support hx) with ⟨c, hc, rfl⟩
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Supported (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
α' : Type u_7
f : α → α'
s : Set α
h : Nonempty α
l : α' →₀ M
hl : Membership.mem (γ := Submodule R (α' →₀ M)) (supported M R (f '' s)) l
⊢ (lmapDomain M R f : (a : α →₀ M) → α' →₀ M) ((lmapDomain M R (Function.invFunOn f s) : (a : α' →₀ M) → α →₀ M) l) = l
have inr : (lmapDomain M R (f ∘ Function.invFunOn f s) : (a : α' →₀ M) → α' →₀ M) l = l
Tactic: rw [← LinearMap.comp_apply, ← lmapDomain_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Supported (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
α' : Type u_7
f : α → α'
s : Set α
h : Nonempty α
l : α' →₀ M
hl : Membership.mem (γ := Submodule R (α' →₀ M)) (supported M R (f '' s)) l
⊢ (lmapDomain M R (f ∘ Function.invFunOn f s) : (a : α' →₀ M) → α' →₀ M) l = l
have inr : ∀ (c : α') (hc : c ∈ l.support), (f ∘ Function.invFunOn f s) c = _root_.id c
Tactic: refine (mapDomain_congr fun c hc => ?_).trans mapDomain_id
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Supported (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
α' : Type u_7
f : α → α'
s : Set α
⊢ Eq (α := Submodule R (α' →₀ M)) (map (lmapDomain M R f) (supported M R s)) (supported M R (f '' s))
have inl : IsEmpty α → Eq (α := Submodule R (α' →₀ M)) (map (lmapDomain M R f) (supported M R s)) (supported M R (f '' s))
Tactic: classical
  cases isEmpty_or_nonempty α
  · simp [s.eq_empty_of_isEmpty]
  refine
    le_antisymm
      (map_le_iff_le_comap.2 <|
        le_trans (supported_mono <| Set.subset_preimage_image _ _)
          (supported_comap_lmapDomain M R _ _))
      ?_
  intro l hl
  refine ⟨(lmapDomain M R (Function.invFunOn f s) : (α' →₀ M) →ₗ[R] α →₀ M) l, fun x hx => ?_, ?_⟩
  · rcases Finset.mem_image.1 (mapDomain_support hx) with ⟨c, hc, rfl⟩
    exact Function.invFunOn_mem (by simpa using hl hc)
  · rw [← LinearMap.comp_apply, ← lmapDomain_comp]
    refine (mapDomain_congr fun c hc => ?_).trans mapDomain_id
    exact Function.invFunOn_eq (by simpa using hl hc)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Supported (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
α' : Type u_7
f : α → α'
s : Set α
inl : IsEmpty α → Eq (α := Submodule R (α' →₀ M)) (map (lmapDomain M R f) (supported M R s)) (supported M R (f '' s))
⊢ Eq (α := Submodule R (α' →₀ M)) (map (lmapDomain M R f) (supported M R s)) (supported M R (f '' s))
have inr : Nonempty α → Eq (α := Submodule R (α' →₀ M)) (map (lmapDomain M R f) (supported M R s)) (supported M R (f '' s))
Tactic: classical
  cases isEmpty_or_nonempty α
  · simp [s.eq_empty_of_isEmpty]
  refine
    le_antisymm
      (map_le_iff_le_comap.2 <|
        le_trans (supported_mono <| Set.subset_preimage_image _ _)
          (supported_comap_lmapDomain M R _ _))
      ?_
  intro l hl
  refine ⟨(lmapDomain M R (Function.invFunOn f s) : (α' →₀ M) →ₗ[R] α →₀ M) l, fun x hx => ?_, ?_⟩
  · rcases Finset.mem_image.1 (mapDomain_support hx) with ⟨c, hc, rfl⟩
    exact Function.invFunOn_mem (by simpa using hl hc)
  · rw [← LinearMap.comp_apply, ← lmapDomain_comp]
    refine (mapDomain_congr fun c hc => ?_).trans mapDomain_id
    exact Function.invFunOn_eq (by simpa using hl hc)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Supported (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
α' : Type u_7
f : α → α'
s : Set α
inl : IsEmpty α → Eq (α := Submodule R (α' →₀ M)) (map (lmapDomain M R f) (supported M R s)) (supported M R (f '' s))
inr inr₁ :
  Nonempty α → Eq (α := Submodule R (α' →₀ M)) (map (lmapDomain M R f) (supported M R s)) (supported M R (f '' s))
⊢ Eq (α := Submodule R (α' →₀ M)) (map (lmapDomain M R f) (supported M R s)) (supported M R (f '' s))
have inr₂ : Nonempty α → LE.le (α := Submodule R (α' →₀ M)) (supported M R (f '' s)) (map (lmapDomain M R f) (supported M R s))
Tactic: classical
  cases isEmpty_or_nonempty α
  · simp [s.eq_empty_of_isEmpty]
  refine
    le_antisymm
      (map_le_iff_le_comap.2 <|
        le_trans (supported_mono <| Set.subset_preimage_image _ _)
          (supported_comap_lmapDomain M R _ _))
      ?_
  intro l hl
  refine ⟨(lmapDomain M R (Function.invFunOn f s) : (α' →₀ M) →ₗ[R] α →₀ M) l, fun x hx => ?_, ?_⟩
  · rcases Finset.mem_image.1 (mapDomain_support hx) with ⟨c, hc, rfl⟩
    exact Function.invFunOn_mem (by simpa using hl hc)
  · rw [← LinearMap.comp_apply, ← lmapDomain_comp]
    refine (mapDomain_congr fun c hc => ?_).trans mapDomain_id
    exact Function.invFunOn_eq (by simpa using hl hc)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Supported (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
α' : Type u_7
f : α → α'
s : Set α
inl : IsEmpty α → Eq (α := Submodule R (α' →₀ M)) (map (lmapDomain M R f) (supported M R s)) (supported M R (f '' s))
inr inr₁ :
  Nonempty α → Eq (α := Submodule R (α' →₀ M)) (map (lmapDomain M R f) (supported M R s)) (supported M R (f '' s))
inr₂ :
  Nonempty α → LE.le (α := Submodule R (α' →₀ M)) (supported M R (f '' s)) (map (lmapDomain M R f) (supported M R s))
⊢ Eq (α := Submodule R (α' →₀ M)) (map (lmapDomain M R f) (supported M R s)) (supported M R (f '' s))
have inr₃ : Nonempty α →
  ∀ ⦃l : α' →₀ M⦄ (hl : Membership.mem (γ := Submodule R (α' →₀ M)) (supported M R (f '' s)) l),
    Membership.mem (γ := Submodule R (α' →₀ M)) (map (lmapDomain M R f) (supported M R s)) l
Tactic: classical
  cases isEmpty_or_nonempty α
  · simp [s.eq_empty_of_isEmpty]
  refine
    le_antisymm
      (map_le_iff_le_comap.2 <|
        le_trans (supported_mono <| Set.subset_preimage_image _ _)
          (supported_comap_lmapDomain M R _ _))
      ?_
  intro l hl
  refine ⟨(lmapDomain M R (Function.invFunOn f s) : (α' →₀ M) →ₗ[R] α →₀ M) l, fun x hx => ?_, ?_⟩
  · rcases Finset.mem_image.1 (mapDomain_support hx) with ⟨c, hc, rfl⟩
    exact Function.invFunOn_mem (by simpa using hl hc)
  · rw [← LinearMap.comp_apply, ← lmapDomain_comp]
    refine (mapDomain_congr fun c hc => ?_).trans mapDomain_id
    exact Function.invFunOn_eq (by simpa using hl hc)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Supported (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
α' : Type u_7
f : α → α'
s : Set α
inl : IsEmpty α → Eq (α := Submodule R (α' →₀ M)) (map (lmapDomain M R f) (supported M R s)) (supported M R (f '' s))
inr inr₁ :
  Nonempty α → Eq (α := Submodule R (α' →₀ M)) (map (lmapDomain M R f) (supported M R s)) (supported M R (f '' s))
inr₂ :
  Nonempty α → LE.le (α := Submodule R (α' →₀ M)) (supported M R (f '' s)) (map (lmapDomain M R f) (supported M R s))
inr₃ :
  Nonempty α →
    ∀ ⦃l : α' →₀ M⦄ (hl : Membership.mem (γ := Submodule R (α' →₀ M)) (supported M R (f '' s)) l),
      Membership.mem (γ := Submodule R (α' →₀ M)) (map (lmapDomain M R f) (supported M R s)) l
⊢ Eq (α := Submodule R (α' →₀ M)) (map (lmapDomain M R f) (supported M R s)) (supported M R (f '' s))
have inr₄ : ∀ (h : Nonempty α) ⦃l : α' →₀ M⦄ (hl : Membership.mem (γ := Submodule R (α' →₀ M)) (supported M R (f '' s)) l) (x : α)
  (hx :
    x ∈ (↑(support.{u_1, u_2} (M := M) ((lmapDomain M R (Function.invFunOn f s) : (a : α' →₀ M) → α →₀ M) l)) : Set α)),
  x ∈ s
Tactic: classical
  cases isEmpty_or_nonempty α
  · simp [s.eq_empty_of_isEmpty]
  refine
    le_antisymm
      (map_le_iff_le_comap.2 <|
        le_trans (supported_mono <| Set.subset_preimage_image _ _)
          (supported_comap_lmapDomain M R _ _))
      ?_
  intro l hl
  refine ⟨(lmapDomain M R (Function.invFunOn f s) : (α' →₀ M) →ₗ[R] α →₀ M) l, fun x hx => ?_, ?_⟩
  · rcases Finset.mem_image.1 (mapDomain_support hx) with ⟨c, hc, rfl⟩
    exact Function.invFunOn_mem (by simpa using hl hc)
  · rw [← LinearMap.comp_apply, ← lmapDomain_comp]
    refine (mapDomain_congr fun c hc => ?_).trans mapDomain_id
    exact Function.invFunOn_eq (by simpa using hl hc)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Supported (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
α' : Type u_7
f : α → α'
s : Set α
inl : IsEmpty α → Eq (α := Submodule R (α' →₀ M)) (map (lmapDomain M R f) (supported M R s)) (supported M R (f '' s))
inr inr₁ :
  Nonempty α → Eq (α := Submodule R (α' →₀ M)) (map (lmapDomain M R f) (supported M R s)) (supported M R (f '' s))
inr₂ :
  Nonempty α → LE.le (α := Submodule R (α' →₀ M)) (supported M R (f '' s)) (map (lmapDomain M R f) (supported M R s))
inr₃ :
  Nonempty α →
    ∀ ⦃l : α' →₀ M⦄ (hl : Membership.mem (γ := Submodule R (α' →₀ M)) (supported M R (f '' s)) l),
      Membership.mem (γ := Submodule R (α' →₀ M)) (map (lmapDomain M R f) (supported M R s)) l
inr₄ :
  ∀ (h : Nonempty α) ⦃l : α' →₀ M⦄ (hl : Membership.mem (γ := Submodule R (α' →₀ M)) (supported M R (f '' s)) l) (x : α)
    (hx :
      x ∈
        (↑(support.{u_1, u_2} (M := M) ((lmapDomain M R (Function.invFunOn f s) : (a : α' →₀ M) → α →₀ M) l)) : Set α)),
    x ∈ s
⊢ Eq (α := Submodule R (α' →₀ M)) (map (lmapDomain M R f) (supported M R s)) (supported M R (f '' s))
have inr₅ : ∀ (h : Nonempty α) ⦃l : α' →₀ M⦄ (hl : Membership.mem (γ := Submodule R (α' →₀ M)) (supported M R (f '' s)) l),
  (lmapDomain M R f : (a : α →₀ M) → α' →₀ M) ((lmapDomain M R (Function.invFunOn f s) : (a : α' →₀ M) → α →₀ M) l) = l
Tactic: classical
  cases isEmpty_or_nonempty α
  · simp [s.eq_empty_of_isEmpty]
  refine
    le_antisymm
      (map_le_iff_le_comap.2 <|
        le_trans (supported_mono <| Set.subset_preimage_image _ _)
          (supported_comap_lmapDomain M R _ _))
      ?_
  intro l hl
  refine ⟨(lmapDomain M R (Function.invFunOn f s) : (α' →₀ M) →ₗ[R] α →₀ M) l, fun x hx => ?_, ?_⟩
  · rcases Finset.mem_image.1 (mapDomain_support hx) with ⟨c, hc, rfl⟩
    exact Function.invFunOn_mem (by simpa using hl hc)
  · rw [← LinearMap.comp_apply, ← lmapDomain_comp]
    refine (mapDomain_congr fun c hc => ?_).trans mapDomain_id
    exact Function.invFunOn_eq (by simpa using hl hc)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Supported (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
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
⊢ Disjoint (α := Submodule R (α →₀ M)) (supported M R s) (ker (lmapDomain M R f))
have rw : LE.le (α := Submodule R (α →₀ M)) (supported M R s ⊓ ker (lmapDomain M R f)) ⊥
Tactic: rw [disjoint_iff_inf_le]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Supported (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
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ (↑(supported M R s) : Set (α →₀ M))
h₂ : l ∈ (↑(ker (lmapDomain M R f)) : Set (α →₀ M))
⊢ Membership.mem (γ := Submodule R (α →₀ M)) ⊥ l
have h₃ : Eq (α := α' →₀ M) (l.sum fun (a : α) ↦ single (f a)) 0
Tactic: rw [SetLike.mem_coe, mem_ker, lmapDomain_apply, mapDomain] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Supported (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
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ (↑(supported M R s) : Set (α →₀ M))
h₂ : Eq (α := α' →₀ M) (l.sum fun (a : α) ↦ single (f a)) 0
⊢ l = 0
have h : ∀ (x : α), Eq.{u_2 + 1} (α := M) ((l : (a : α) → M) x : M) ((0 : (a : α) → M) x : M)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Supported (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
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ (↑(supported M R s) : Set (α →₀ M))
h₂ : Eq (α := α' →₀ M) (l.sum fun (a : α) ↦ single (f a)) 0
x : α
⊢ Eq.{u_2 + 1} (α := M) ((l : (a : α) → M) x : M) ((0 : (a : α) → M) x : M)
have h : ∀ (this : DecidablePred fun (x : α) ↦ x ∈ s), Eq.{u_2 + 1} (α := M) ((l : (a : α) → M) x : M) ((0 : (a : α) → M) x : M)
Tactic: haveI := Classical.decPred fun x => x ∈ s
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Supported (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
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ (↑(supported M R s) : Set (α →₀ M))
h₂ : Eq (α := α' →₀ M) (l.sum fun (a : α) ↦ single (f a)) 0
x : α
this : DecidablePred fun (x : α) ↦ x ∈ s
⊢ Eq.{u_2 + 1} (α := M) ((l : (a : α) → M) x : M) ((0 : (a : α) → M) x : M)
have pos : ∀ (xs : x ∈ s), Eq.{u_2 + 1} (α := M) ((l : (a : α) → M) x : M) ((0 : (a : α) → M) x : M)
Tactic: by_cases xs : x ∈ s
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Supported (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
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ (↑(supported M R s) : Set (α →₀ M))
h₂ : Eq (α := α' →₀ M) (l.sum fun (a : α) ↦ single (f a)) 0
x : α
this : DecidablePred fun (x : α) ↦ x ∈ s
pos : ∀ (xs : x ∈ s), Eq.{u_2 + 1} (α := M) ((l : (a : α) → M) x : M) ((0 : (a : α) → M) x : M)
⊢ Eq.{u_2 + 1} (α := M) ((l : (a : α) → M) x : M) ((0 : (a : α) → M) x : M)
have neg : ∀ (xs : x ∉ s), Eq.{u_2 + 1} (α := M) ((l : (a : α) → M) x : M) ((0 : (a : α) → M) x : M)
Tactic: by_cases xs : x ∈ s
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Supported (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
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ (↑(supported M R s) : Set (α →₀ M))
h₂ : Eq (α := α' →₀ M) (l.sum fun (a : α) ↦ single (f a)) 0
x : α
this : DecidablePred fun (x : α) ↦ x ∈ s
xs : x ∈ s
⊢ Eq.{u_2 + 1} (α := M) ((l.sum fun (a : α) ↦ single (f a) : (a : α') → M) (f x) : M) (0 : M)
have rw : Eq.{u_2 + 1} (α := M) ((0 : (a : α') → M) (f x) : M) (0 : M)
Tactic: rw [h₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Supported (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
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ (↑(supported M R s) : Set (α →₀ M))
h₂ : Eq (α := α' →₀ M) (l.sum fun (a : α) ↦ single (f a)) 0
x : α
this : DecidablePred fun (x : α) ↦ x ∈ s
xs : x ∈ s
⊢ Eq.{u_2 + 1} (α := M) ((l : (a : α) → M) x : M) ((0 : (a : α) → M) x : M)
have this₁ : Eq.{u_2 + 1} (α := M) ((l.sum fun (a : α) ↦ single (f a) : (a : α') → M) (f x) : M) (0 : M)
Tactic: have : Finsupp.sum l (fun a => Finsupp.single (f a)) (f x) = 0 := by
      rw [h₂]
      rfl
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Supported (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
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ (↑(supported M R s) : Set (α →₀ M))
h₂ : Eq (α := α' →₀ M) (l.sum fun (a : α) ↦ single (f a)) 0
x : α
this_1 : DecidablePred fun (x : α) ↦ x ∈ s
xs : x ∈ s
this : Eq.{u_2 + 1} (α := M) ((l.sum fun (a : α) ↦ single (f a) : (a : α') → M) (f x) : M) (0 : M)
⊢ Eq.{u_2 + 1} (α := M) ((l : (a : α) → M) x : M) ((0 : (a : α) → M) x : M)
have pos : ∀ (this : Eq.{u_2 + 1} (α := M) ((l : (a : α) → M) x : M) (0 : M)),
  Eq.{u_2 + 1} (α := M) ((l : (a : α) → M) x : M) ((0 : (a : α) → M) x : M)
Tactic: rw [Finsupp.sum_apply, Finsupp.sum_eq_single x, single_eq_same] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Supported (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
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ (↑(supported M R s) : Set (α →₀ M))
h₂ : Eq (α := α' →₀ M) (l.sum fun (a : α) ↦ single (f a)) 0
x : α
this_1 : DecidablePred fun (x : α) ↦ x ∈ s
xs : x ∈ s
this : Eq.{u_2 + 1} (α := M) ((l.sum fun (a : α) ↦ single (f a) : (a : α') → M) (f x) : M) (0 : M)
pos :
  ∀ (this : Eq.{u_2 + 1} (α := M) ((l : (a : α) → M) x : M) (0 : M)),
    Eq.{u_2 + 1} (α := M) ((l : (a : α) → M) x : M) ((0 : (a : α) → M) x : M)
⊢ Eq.{u_2 + 1} (α := M) ((l : (a : α) → M) x : M) ((0 : (a : α) → M) x : M)
have pos₁ : ∀ (this : Eq (α := M) (l.sum fun (a₁ : α) (b : M) ↦ (single (f a₁) b : (a : α') → M) (f x)) 0) (b : α),
  Ne.{u_2 + 1} (α := M) ((l : (a : α) → M) b : M) (0 : M) →
    b ≠ x → Eq.{u_2 + 1} (α := M) (((single (f b) ((l : (a : α) → M) b) : α' →₀ M) : (a : α') → M) (f x) : M) (0 : M)
Tactic: rw [Finsupp.sum_apply, Finsupp.sum_eq_single x, single_eq_same] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Supported (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
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ (↑(supported M R s) : Set (α →₀ M))
h₂ : Eq (α := α' →₀ M) (l.sum fun (a : α) ↦ single (f a)) 0
x : α
this_1 : DecidablePred fun (x : α) ↦ x ∈ s
xs : x ∈ s
this : Eq.{u_2 + 1} (α := M) ((l.sum fun (a : α) ↦ single (f a) : (a : α') → M) (f x) : M) (0 : M)
pos :
  ∀ (this : Eq.{u_2 + 1} (α := M) ((l : (a : α) → M) x : M) (0 : M)),
    Eq.{u_2 + 1} (α := M) ((l : (a : α) → M) x : M) ((0 : (a : α) → M) x : M)
pos₁ :
  ∀ (this : Eq (α := M) (l.sum fun (a₁ : α) (b : M) ↦ (single (f a₁) b : (a : α') → M) (f x)) 0) (b : α),
    Ne.{u_2 + 1} (α := M) ((l : (a : α) → M) b : M) (0 : M) →
      b ≠ x → Eq.{u_2 + 1} (α := M) (((single (f b) ((l : (a : α) → M) b) : α' →₀ M) : (a : α') → M) (f x) : M) (0 : M)
⊢ Eq.{u_2 + 1} (α := M) ((l : (a : α) → M) x : M) ((0 : (a : α) → M) x : M)
have pos₂ : ∀ (this : Eq (α := M) (l.sum fun (a₁ : α) (b : M) ↦ (single (f a₁) b : (a : α') → M) (f x)) 0),
  Eq.{u_2 + 1} (α := M) ((l : (a : α) → M) x : M) (0 : M) →
    Eq.{u_2 + 1} (α := M) ((single (f x) 0 : (a : α') → M) (f x) : M) (0 : M)
Tactic: rw [Finsupp.sum_apply, Finsupp.sum_eq_single x, single_eq_same] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Supported (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
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ (↑(supported M R s) : Set (α →₀ M))
h₂ : Eq (α := α' →₀ M) (l.sum fun (a : α) ↦ single (f a)) 0
x : α
this_1 : DecidablePred fun (x : α) ↦ x ∈ s
xs : x ∈ s
this : Eq (α := M) (l.sum fun (a₁ : α) (b : M) ↦ (single (f a₁) b : (a : α') → M) (f x)) 0
y : α
hy : Ne.{u_2 + 1} (α := M) ((l : (a : α) → M) y : M) (0 : M)
xy : y ≠ x
⊢ Eq.{u_2 + 1} (α := M) (((single (f y) ((l : (a : α) → M) y) : α' →₀ M) : (a : α') → M) (f x) : M) (0 : M)
have h₃ : ∀ (x : α), Ne.{u_2 + 1} (α := M) ((l : (a : α) → M) x : M) (0 : M) → x ∈ s
Tactic: simp only [SetLike.mem_coe, mem_supported, subset_def, mem_support_iff] at h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Supported (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
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ (↑(supported M R s) : Set (α →₀ M))
h₂ : Eq (α := α' →₀ M) (l.sum fun (a : α) ↦ single (f a)) 0
x : α
this : DecidablePred fun (x : α) ↦ x ∈ s
xs : x ∉ s
⊢ Eq.{u_2 + 1} (α := M) ((l : (a : α) → M) x : M) ((0 : (a : α) → M) x : M)
have neg : ∀ (h : ¬Eq.{u_2 + 1} (α := M) ((l : (a : α) → M) x : M) ((0 : (a : α) → M) x : M)), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Supported (goal)
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : AddCommMonoid P
inst_7 : Module R P
α' : Type u_7
s : Set α
t : Set α'
e : Equiv.{u_1 + 1, u_7 + 1} (↑s : Type u_1) (↑t : Type u_7)
⊢ ↥(supported M R s) ≃ₗ[R] ↥(supported M R t)
have haveI : (this : DecidablePred fun (x : α) ↦ x ∈ s) → ↥(supported M R s) ≃ₗ[R] ↥(supported M R t)
Tactic: haveI := Classical.decPred fun x => x ∈ s
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Supported (goal)
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : AddCommMonoid P
inst_7 : Module R P
α' : Type u_7
s : Set α
t : Set α'
e : Equiv.{u_1 + 1, u_7 + 1} (↑s : Type u_1) (↑t : Type u_7)
this : DecidablePred fun (x : α) ↦ x ∈ s
⊢ ↥(supported M R s) ≃ₗ[R] ↥(supported M R t)
have haveI : (this : DecidablePred fun (x : α') ↦ x ∈ t) → ↥(supported M R s) ≃ₗ[R] ↥(supported M R t)
Tactic: haveI := Classical.decPred fun x => x ∈ t