awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
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
s : δ → Set α
this : DecidablePred fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : δ), s i) x
x : α
a : M
l : α →₀ M
h : x ∉ l.support
h_1 : a ≠ 0
ih :
  Membership.mem (γ := Submodule R (α →₀ M))
    (comap (Submodule.subtype (supported M R (⋃ (i : δ), s i)) ∘ₗ restrictDom M R (⋃ (i : δ), s i))
      (⨆ (i : δ), supported M R (s i)))
    l
⊢ Membership.mem (γ := Submodule R (α →₀ M))
    (comap (Submodule.subtype (supported M R (⋃ (i : δ), s i)) ∘ₗ restrictDom M R (⋃ (i : δ), s i))
      (⨆ (i : δ), supported M R (s i)))
    (single x a + l)

Tactic:
add_mem ?_ ih

Premises used: AddMemClass.add_mem
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
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
s : δ → Set α
this : DecidablePred fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : δ), s i) x
x : α
a : M
l : α →₀ M
h : x ∉ l.support
h_1 : a ≠ 0
ih :
  Membership.mem (γ := Submodule R (α →₀ M))
    (comap (Submodule.subtype (supported M R (⋃ (i : δ), s i)) ∘ₗ restrictDom M R (⋃ (i : δ), s i))
      (⨆ (i : δ), supported M R (s i)))
    l
single_add :
  Membership.mem (γ := Submodule R (α →₀ M))
    (comap (Submodule.subtype (supported M R (⋃ (i : δ), s i)) ∘ₗ restrictDom M R (⋃ (i : δ), s i))
      (⨆ (i : δ), supported M R (s i)))
    (single x a)
⊢ Membership.mem (γ := Submodule R (α →₀ M))
    (comap (Submodule.subtype (supported M R (⋃ (i : δ), s i)) ∘ₗ restrictDom M R (⋃ (i : δ), s i))
      (⨆ (i : δ), supported M R (s i)))
    (single x a + l)

Tactic:
refine add_mem ?_ ih

Premises used: AddMemClass.add_mem
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
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
s : δ → Set α
this : DecidablePred fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : δ), s i) x
x : α
a : M
l : α →₀ M
h : x ∉ l.support
h_1 : a ≠ 0
ih :
  Membership.mem (γ := Submodule R (α →₀ M))
    (comap (Submodule.subtype (supported M R (⋃ (i : δ), s i)) ∘ₗ restrictDom M R (⋃ (i : δ), s i))
      (⨆ (i : δ), supported M R (s i)))
    l
pos :
  ∀ (h : ∃ (i : δ), x ∈ s i),
    Membership.mem (γ := Submodule R (α →₀ M))
      (comap (Submodule.subtype (supported M R (⋃ (i : δ), s i)) ∘ₗ restrictDom M R (⋃ (i : δ), s i))
        (⨆ (i : δ), supported M R (s i)))
      (single x a)
neg :
  ∀ (h : ¬∃ (i : δ), x ∈ s i),
    Membership.mem (γ := Submodule R (α →₀ M))
      (comap (Submodule.subtype (supported M R (⋃ (i : δ), s i)) ∘ₗ restrictDom M R (⋃ (i : δ), s i))
        (⨆ (i : δ), supported M R (s i)))
      (single x a)
⊢ Membership.mem (γ := Submodule R (α →₀ M))
    (comap (Submodule.subtype (supported M R (⋃ (i : δ), s i)) ∘ₗ restrictDom M R (⋃ (i : δ), s i))
      (⨆ (i : δ), supported M R (s i)))
    (single x a)

Tactic:
by_cases h : ∃ i, x ∈ s i
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
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
s : δ → Set α
this : DecidablePred fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : δ), s i) x
x : α
a : M
l : α →₀ M
h_1 : x ∉ l.support
h_2 : a ≠ 0
ih :
  Membership.mem (γ := Submodule R (α →₀ M))
    (comap (Submodule.subtype (supported M R (⋃ (i : δ), s i)) ∘ₗ restrictDom M R (⋃ (i : δ), s i))
      (⨆ (i : δ), supported M R (s i)))
    l
h : ∃ (i : δ), x ∈ s i
pos : Membership.mem (γ := Submodule R (α →₀ M)) (⨆ (i : δ), supported M R (s i)) (single x a)
⊢ Membership.mem (γ := Submodule R (α →₀ M))
    (comap (Submodule.subtype (supported M R (⋃ (i : δ), s i)) ∘ₗ restrictDom M R (⋃ (i : δ), s i))
      (⨆ (i : δ), supported M R (s i)))
    (single x a)

Tactic:
simp only [mem_comap, coe_comp, coe_subtype, Function.comp_apply, restrictDom_apply,
        mem_iUnion, h, filter_single_of_pos]

Premises used: Finsupp.restrictDom_apply, Submodule.mem_comap, Set.mem_iUnion, LinearMap.coe_comp, Finsupp.filter_single_of_pos, Submodule.coe_subtype, Function.comp_apply
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
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
s : δ → Set α
this : DecidablePred fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : δ), s i) x
x : α
a : M
l : α →₀ M
h_1 : x ∉ l.support
h_2 : a ≠ 0
ih :
  Membership.mem (γ := Submodule R (α →₀ M))
    (comap (Submodule.subtype (supported M R (⋃ (i : δ), s i)) ∘ₗ restrictDom M R (⋃ (i : δ), s i))
      (⨆ (i : δ), supported M R (s i)))
    l
h : ∃ (i : δ), x ∈ s i
pos : ∀ (i : δ) (hi : x ∈ s i), Membership.mem (γ := Submodule R (α →₀ M)) (⨆ (i : δ), supported M R (s i)) (single x a)
⊢ Membership.mem (γ := Submodule R (α →₀ M)) (⨆ (i : δ), supported M R (s i)) (single x a)

Tactic:
obtain ⟨i, hi⟩ := h
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
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
s : δ → Set α
this : DecidablePred fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : δ), s i) x
x : α
a : M
l : α →₀ M
h : x ∉ l.support
h_1 : a ≠ 0
ih :
  Membership.mem (γ := Submodule R (α →₀ M))
    (comap (Submodule.subtype (supported M R (⋃ (i : δ), s i)) ∘ₗ restrictDom M R (⋃ (i : δ), s i))
      (⨆ (i : δ), supported M R (s i)))
    l
i : δ
hi : x ∈ s i
⊢ Membership.mem (γ := Submodule R (α →₀ M)) (⨆ (i : δ), supported M R (s i)) (single x a)

Tactic:
le_iSup (fun i => supported M R (s i)) i (single_mem_supported R _ hi)

Premises used: Set.Mem, Finsupp.supported, le_iSup, Finsupp.single_mem_supported
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
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
s : δ → Set α
this : DecidablePred fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : δ), s i) x
x : α
a : M
l : α →₀ M
h : x ∉ l.support
h_1 : a ≠ 0
ih :
  Membership.mem (γ := Submodule R (α →₀ M))
    (comap (Submodule.subtype (supported M R (⋃ (i : δ), s i)) ∘ₗ restrictDom M R (⋃ (i : δ), s i))
      (⨆ (i : δ), supported M R (s i)))
    l
i : δ
hi : x ∈ s i
⊢ Membership.mem (γ := Submodule R (α →₀ M)) (⨆ (i : δ), supported M R (s i)) (single x a)

Tactic:
exact le_iSup (fun i => supported M R (s i)) i (single_mem_supported R _ hi)

Premises used: Finsupp.supported, le_iSup, Finsupp.single_mem_supported
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
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
s : δ → Set α
this : DecidablePred fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : δ), s i) x
x : α
a : M
l : α →₀ M
h_1 : x ∉ l.support
h_2 : a ≠ 0
ih :
  Membership.mem (γ := Submodule R (α →₀ M))
    (comap (Submodule.subtype (supported M R (⋃ (i : δ), s i)) ∘ₗ restrictDom M R (⋃ (i : δ), s i))
      (⨆ (i : δ), supported M R (s i)))
    l
h : ¬∃ (i : δ), x ∈ s i
⊢ Membership.mem (γ := Submodule R (α →₀ M))
    (comap (Submodule.subtype (supported M R (⋃ (i : δ), s i)) ∘ₗ restrictDom M R (⋃ (i : δ), s i))
      (⨆ (i : δ), supported M R (s i)))
    (single x a)

Tactic:
simp [h]
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
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
s : δ → Set α
this : DecidablePred fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : δ), s i) x
l : α →₀ M
zero :
  Membership.mem (γ := Submodule R (α →₀ M))
    (comap (Submodule.subtype (supported M R (⋃ (i : δ), s i)) ∘ₗ restrictDom M R (⋃ (i : δ), s i))
      (⨆ (i : δ), supported M R (s i)))
    0
single_add :
  ∀ (x : α) (a : M) (l : α →₀ M),
    x ∉ l.support →
      a ≠ 0 →
        ∀
          (ih :
            Membership.mem (γ := Submodule R (α →₀ M))
              (comap (Submodule.subtype (supported M R (⋃ (i : δ), s i)) ∘ₗ restrictDom M R (⋃ (i : δ), s i))
                (⨆ (i : δ), supported M R (s i)))
              l),
          Membership.mem (γ := Submodule R (α →₀ M))
            (comap (Submodule.subtype (supported M R (⋃ (i : δ), s i)) ∘ₗ restrictDom M R (⋃ (i : δ), s i))
              (⨆ (i : δ), supported M R (s i)))
            (single x a + l)
⊢ Membership.mem (γ := Submodule R (α →₀ M))
    (comap (Submodule.subtype (supported M R (⋃ (i : δ), s i)) ∘ₗ restrictDom M R (⋃ (i : δ), s i))
      (⨆ (i : δ), supported M R (s i)))
    l

Tactic:
induction l using Finsupp.induction with
  | zero => exact zero_mem _
  | single_add x a l _ _ ih =>
    refine add_mem ?_ ih
    by_cases h : ∃ i, x ∈ s i
    · simp only [mem_comap, coe_comp, coe_subtype, Function.comp_apply, restrictDom_apply,
        mem_iUnion, h, filter_single_of_pos]
      obtain ⟨i, hi⟩ := h
      exact le_iSup (fun i => supported M R (s i)) i (single_mem_supported R _ hi)
    · simp [h]

Premises used: Finsupp.restrictDom_apply, Submodule.mem_comap, Set.mem_iUnion, LinearMap.coe_comp, Finsupp.single_add, Finsupp.filter_single_of_pos, Submodule.coe_subtype, Submodule.zero, Function.comp_apply, ZeroMemClass.zero_mem
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
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 α
rw :
  Eq (α := Submodule R (α →₀ M)) (supported M R (⋃ (b : Bool), bif b then s else t)) (supported M R s ⊔ supported M R t)
rw₁ :
  Eq (α := Submodule R (α →₀ M)) (⨆ (i : Bool), supported M R (bif i then s else t)) (supported M R s ⊔ supported M R t)
rw₂ :
  Eq (α := Submodule R (α →₀ M)) (supported M R (bif true then s else t) ⊔ supported M R (bif false then s else t))
    (supported M R s ⊔ supported M R t)
rw₃ :
  Eq (α := Submodule R (α →₀ M)) (supported M R s ⊔ supported M R (bif false then s else t))
    (supported M R s ⊔ supported M R t)
rw₄ rw₅ : Eq (α := Submodule R (α →₀ M)) (supported M R s ⊔ supported M R t) (supported M R s ⊔ supported M R t)
⊢ Eq (α := Submodule R (α →₀ M)) (supported M R (s ∪ t)) (supported M R s ⊔ supported M R t)

Tactic:
rw [Set.union_eq_iUnion, supported_iUnion, iSup_bool_eq, cond_true, cond_false]

Premises used: iSup_bool_eq, cond_true, Finsupp.supported_iUnion, Set.union_eq_iUnion, cond_false
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
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
s : ι → Set α
x : α →₀ M
⊢ Membership.mem (γ := Submodule R (α →₀ M)) (supported M R (⋂ (i : ι), s i)) x ↔
    Membership.mem (γ := Submodule R (α →₀ M)) (⨅ (i : ι), supported M R (s i)) x

Tactic:
simp [mem_supported, subset_iInter_iff]

Premises used: Finsupp.mem_supported, Set.subset_iInter_iff
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
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 α
rw :
  Eq (α := Submodule R (α →₀ M)) (supported M R (bif true then s else t) ⊓ supported M R (bif false then s else t))
    (supported M R s ⊓ supported M R t)
⊢ Eq (α := Submodule R (α →₀ M)) (supported M R (s ∩ t)) (supported M R s ⊓ supported M R t)

Tactic:
rw [Set.inter_eq_iInter, supported_iInter, iInf_bool_eq]

Premises used: Finsupp.supported_iInter, iInf_bool_eq, Set.inter_eq_iInter
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
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 α
⊢ Eq (α := Submodule R (α →₀ M)) (supported M R (bif true then s else t) ⊓ supported M R (bif false then s else t))
    (supported M R s ⊓ supported M R t)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
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
rw : Eq (α := Submodule R (α →₀ M)) (supported M R (s ∩ t)) ⊥
rw₁ : Eq (α := Submodule R (α →₀ M)) (supported M R ∅) ⊥
rw₂ rw₃ : Eq (α := Submodule R (α →₀ M)) ⊥ ⊥
⊢ Eq (α := Submodule R (α →₀ M)) (supported M R s ⊓ supported M R t) ⊥

Tactic:
rw [← supported_inter, disjoint_iff_inter_eq_empty.1 h, supported_empty]

Premises used: Finsupp.supported_inter, Set.disjoint_iff_inter_eq_empty, Finsupp.supported_empty, Iff.mp
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial M
s t : Set α
⊢ Disjoint (α := Submodule R (α →₀ M)) (supported M R s) (supported M R t) ↔ Disjoint s t

Tactic:
⟨fun h => Set.disjoint_left.mpr fun x hx1 hx2 => ?_, disjoint_supported_supported⟩

Premises used: Iff.mpr, Set.disjoint_left, Finsupp.disjoint_supported_supported, Iff.intro
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial M
s t : Set α
refine :
  ∀ (h : Disjoint (α := Submodule R (α →₀ M)) (supported M R s) (supported M R t)) (x : α) (hx1 : x ∈ s) (hx2 : x ∈ t),
    False
⊢ Disjoint (α := Submodule R (α →₀ M)) (supported M R s) (supported M R t) ↔ Disjoint s t

Tactic:
refine ⟨fun h => Set.disjoint_left.mpr fun x hx1 hx2 => ?_, disjoint_supported_supported⟩
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial M
s t : Set α
h : Disjoint (α := Submodule R (α →₀ M)) (supported M R s) (supported M R t)
x : α
hx1 : x ∈ s
hx2 : x ∈ t
rcases : ∀ (y : M) (hy : y ≠ 0), False
⊢ False

Tactic:
rcases exists_ne (0 : M) with ⟨y, hy⟩

Premises used: exists_ne, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial M
s t : Set α
h : Disjoint (α := Submodule R (α →₀ M)) (supported M R s) (supported M R t)
x : α
hx1 : x ∈ s
hx2 : x ∈ t
y : M
hy : y ≠ 0
⊢ Membership.mem (γ := Submodule R (α →₀ M)) ⊥ (single x y)

Tactic:
have := h.le_bot ⟨single_mem_supported R y hx1, single_mem_supported R y hx2⟩
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial M
s t : Set α
h : Disjoint (α := Submodule R (α →₀ M)) (supported M R s) (supported M R t)
x : α
hx1 : x ∈ s
hx2 : x ∈ t
y : M
hy : y ≠ 0
this : Membership.mem (γ := Submodule R (α →₀ M)) ⊥ (single x y)
⊢ y = 0

Tactic:
rw [mem_bot, single_eq_zero] at this

Premises used: Submodule.mem_bot, Finsupp.single_eq_zero
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial M
s t : Set α
h : Disjoint (α := Submodule R (α →₀ M)) (supported M R s) (supported M R t)
x : α
hx1 : x ∈ s
hx2 : x ∈ t
y : M
hy : y ≠ 0
this : y = 0
⊢ False

Tactic:
hy this
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial M
s t : Set α
h : Disjoint (α := Submodule R (α →₀ M)) (supported M R s) (supported M R t)
x : α
hx1 : x ∈ s
hx2 : x ∈ t
y : M
hy : y ≠ 0
this : y = 0
⊢ False

Tactic:
exact hy this
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
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 : Codisjoint s t
rw : Eq (α := Submodule R (α →₀ M)) (supported M R s ⊔ supported M R t) ⊤
rw₁ : LE.le (α := Submodule R (α →₀ M)) ⊤ (supported M R s ⊔ supported M R t)
rw₂ : LE.le (α := Submodule R (α →₀ M)) ⊤ (supported M R (s ∪ t))
rw₃ : LE.le (α := Submodule R (α →₀ M)) ⊤ (supported M R univ)
rw₄ rw₅ : LE.le (α := Submodule R (α →₀ M)) ⊤ ⊤
⊢ Codisjoint (α := Submodule R (α →₀ M)) (supported M R s) (supported M R t)

Tactic:
rw [codisjoint_iff, eq_top_iff, ← supported_union,
    show s ∪ t = .univ from codisjoint_iff.mp h, supported_univ]

Premises used: eq_top_iff, Finsupp.supported_univ, codisjoint_iff, Finsupp.supported_union, Iff.mp
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial M
s t : Set α
⊢ Codisjoint (α := Submodule R (α →₀ M)) (supported M R s) (supported M R t) ↔ Codisjoint s t

Tactic:
⟨fun h ↦ codisjoint_iff.mpr (eq_top_iff.mpr fun a ↦ ?_), codisjoint_supported_supported⟩

Premises used: Iff.mpr, eq_top_iff, codisjoint_iff, Finsupp.codisjoint_supported_supported, Iff.intro
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial M
s t : Set α
refine :
  ∀ (h : Codisjoint (α := Submodule R (α →₀ M)) (supported M R s) (supported M R t)) (a : α),
    Membership.mem (γ := Set α) ⊤ a → a ∈ s ⊔ t
⊢ Codisjoint (α := Submodule R (α →₀ M)) (supported M R s) (supported M R t) ↔ Codisjoint s t

Tactic:
refine ⟨fun h ↦ codisjoint_iff.mpr (eq_top_iff.mpr fun a ↦ ?_), codisjoint_supported_supported⟩
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial M
s t : Set α
h : Codisjoint (α := Submodule R (α →₀ M)) (supported M R s) (supported M R t)
a : α
obtain : ∀ (x : M) (hx : x ≠ 0), Membership.mem (γ := Set α) ⊤ a → a ∈ s ⊔ t
⊢ Membership.mem (γ := Set α) ⊤ a → a ∈ s ⊔ t

Tactic:
obtain ⟨x, hx⟩ := exists_ne (0 : M)

Premises used: exists_ne, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial M
s t : Set α
h : Codisjoint (α := Submodule R (α →₀ M)) (supported M R s) (supported M R t)
a : α
x : M
hx : x ≠ 0
rw :
  ∀ (h : ∀ (x : α →₀ M), Membership.mem (γ := Submodule R (α →₀ M)) (supported M R (s ∪ t)) x) (a : α) (x : M)
    (hx : x ≠ 0), Membership.mem (γ := Set α) ⊤ a → a ∈ s ⊔ t
⊢ Membership.mem (γ := Set α) ⊤ a → a ∈ s ⊔ t

Tactic:
rw [codisjoint_iff, ← supported_union, eq_top_iff'] at h

Premises used: Submodule.eq_top_iff', codisjoint_iff, Finsupp.supported_union
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial M
s t : Set α
h : ∀ (x : α →₀ M), Membership.mem (γ := Submodule R (α →₀ M)) (supported M R (s ∪ t)) x
a : α
x : M
hx : x ≠ 0
⊢ Membership.mem (γ := Set α) ⊤ a → a ∈ s ⊔ t

Tactic:
simpa [Finsupp.mem_supported, Finsupp.support_single _ hx] using h (Finsupp.single a x)

Premises used: Finsupp.support_single, Finsupp.mem_supported, Finsupp.single
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
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
s : Set α
F : ↥(supported M R s) ≃ Finsupp.{u_1, u_2} (↑s : Type u_1) M := restrictSupportEquiv s M
refine :
  IsLinearMap R (M := ↥(supported M R s)) (M₂ := Finsupp.{u_1, u_2} (↑s : Type u_1) M)
    (⇑F : (a : ↥(supported M R s)) → (↑s : Type u_1) →₀ M)
⊢ ↥(supported M R s) ≃ₗ[R] Finsupp.{u_1, u_2} (↑s : Type u_1) M

Tactic:
refine F.toLinearEquiv ?_

Premises used: Equiv.toLinearEquiv
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
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
s : Set α
F : ↥(supported M R s) ≃ Finsupp.{u_1, u_2} (↑s : Type u_1) M := restrictSupportEquiv s M
⊢ Eq (α := (a : ↥(supported M R s)) → Finsupp.{u_1, u_2} (↑s : Type u_1) M)
    (⇑F : (a : ↥(supported M R s)) → (↑s : Type u_1) →₀ M)
    (⇑(lsubtypeDomain s ∘ₗ Submodule.subtype (supported M R s)) : (a : ↥(supported M R s)) → (↑s : Type u_1) →₀ M)

Tactic:
have :
    (F : supported M R s → ↥s →₀ M) =
      (lsubtypeDomain s : (α →₀ M) →ₗ[R] s →₀ M).comp (Submodule.subtype (supported M R s)) :=
    rfl
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
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
s : Set α
F : ↥(supported M R s) ≃ Finsupp.{u_1, u_2} (↑s : Type u_1) M := restrictSupportEquiv s M
this :
  Eq (α := (a : ↥(supported M R s)) → Finsupp.{u_1, u_2} (↑s : Type u_1) M)
    (⇑F : (a : ↥(supported M R s)) → (↑s : Type u_1) →₀ M)
    (⇑(lsubtypeDomain s ∘ₗ Submodule.subtype (supported M R s)) : (a : ↥(supported M R s)) → (↑s : Type u_1) →₀ M)
rw :
  IsLinearMap R (M := ↥(supported M R s)) (M₂ := Finsupp.{u_1, u_2} (↑s : Type u_1) M)
    (⇑(lsubtypeDomain s ∘ₗ Submodule.subtype (supported M R s)) : (a : ↥(supported M R s)) → (↑s : Type u_1) →₀ M)
⊢ IsLinearMap R (M := ↥(supported M R s)) (M₂ := Finsupp.{u_1, u_2} (↑s : Type u_1) M)
    (⇑F : (a : ↥(supported M R s)) → (↑s : Type u_1) →₀ M)

Tactic:
rw [this]
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
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
s : Set α
F : ↥(supported M R s) ≃ Finsupp.{u_1, u_2} (↑s : Type u_1) M := restrictSupportEquiv s M
this :
  Eq (α := (a : ↥(supported M R s)) → Finsupp.{u_1, u_2} (↑s : Type u_1) M)
    (⇑F : (a : ↥(supported M R s)) → (↑s : Type u_1) →₀ M)
    (⇑(lsubtypeDomain s ∘ₗ Submodule.subtype (supported M R s)) : (a : ↥(supported M R s)) → (↑s : Type u_1) →₀ M)
⊢ IsLinearMap R (M := ↥(supported M R s)) (M₂ := Finsupp.{u_1, u_2} (↑s : Type u_1) M)
    (⇑(lsubtypeDomain s ∘ₗ Submodule.subtype (supported M R s)) : (a : ↥(supported M R s)) → (↑s : Type u_1) →₀ M)

Tactic:
LinearMap.isLinear _

Premises used: LinearMap.isLinear
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
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
s : Set α
F : ↥(supported M R s) ≃ Finsupp.{u_1, u_2} (↑s : Type u_1) M := restrictSupportEquiv s M
this :
  Eq (α := (a : ↥(supported M R s)) → Finsupp.{u_1, u_2} (↑s : Type u_1) M)
    (⇑F : (a : ↥(supported M R s)) → (↑s : Type u_1) →₀ M)
    (⇑(lsubtypeDomain s ∘ₗ Submodule.subtype (supported M R s)) : (a : ↥(supported M R s)) → (↑s : Type u_1) →₀ M)
⊢ IsLinearMap R (M := ↥(supported M R s)) (M₂ := Finsupp.{u_1, u_2} (↑s : Type u_1) M)
    (⇑(lsubtypeDomain s ∘ₗ Submodule.subtype (supported M R s)) : (a : ↥(supported M R s)) → (↑s : Type u_1) →₀ M)

Tactic:
exact LinearMap.isLinear _

Premises used: LinearMap.isLinear
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
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 α
inst_3 : DecidablePred fun (x : α) ↦ x ∈ s
f : Finsupp.{u_1, u_2} (↑s : Type u_1) M
⊢ (↑((Equiv.symm (restrictSupportEquiv s M) : (a : (↑s : Type u_1) →₀ M) → { f : α →₀ M // (↑f.support : Set α) ⊆ s })
          f) :
      α →₀ M) =
    f.extendDomain (P := fun (x : α) ↦ x ∈ s)

Tactic:
restrictSupportEquiv_symm_apply_coe ..

Premises used: Finsupp.restrictSupportEquiv_symm_apply_coe
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
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 α
inst_3 : DecidablePred fun (x : α) ↦ x ∈ s
f : Finsupp.{u_1, u_2} (↑s : Type u_1) M
⊢ (↑((LinearEquiv.symm (supportedEquivFinsupp s) : (a : (↑s : Type u_1) →₀ M) → ↥(supported M R s)) f) : α →₀ M) =
    f.extendDomain (P := fun (x : α) ↦ x ∈ s)

Tactic:
convert! restrictSupportEquiv_symm_apply_coe ..

Premises used: Finsupp.restrictSupportEquiv_symm_apply_coe