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
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
⊢ 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
have 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)
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]
Cleared hypotheses: l
-- 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
s t : Set α
⊢ Eq (α := Submodule R (α →₀ M)) (supported M R (s ∪ t)) (supported M R s ⊔ supported M R t)
have rw : Eq (α := Submodule R (α →₀ M)) (supported M R (⋃ (b : Bool), bif b then s else t)) (supported M R s ⊔ supported M R t)
Tactic: rw [Set.union_eq_iUnion, supported_iUnion, iSup_bool_eq, cond_true, cond_false]
-- 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
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)
⊢ Eq (α := Submodule R (α →₀ M)) (supported M R (s ∪ t)) (supported M R s ⊔ supported M R t)
have rw₁ : Eq (α := Submodule R (α →₀ M)) (⨆ (i : Bool), supported M R (bif i then s else t)) (supported M R s ⊔ supported M R t)
Tactic: rw [Set.union_eq_iUnion, supported_iUnion, iSup_bool_eq, cond_true, cond_false]
-- 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
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)
⊢ Eq (α := Submodule R (α →₀ M)) (supported M R (s ∪ t)) (supported M R s ⊔ supported M R t)
have 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)
Tactic: rw [Set.union_eq_iUnion, supported_iUnion, iSup_bool_eq, cond_true, cond_false]
-- 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
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)
⊢ Eq (α := Submodule R (α →₀ M)) (supported M R (s ∪ t)) (supported M R s ⊔ supported M R t)
have 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)
Tactic: rw [Set.union_eq_iUnion, supported_iUnion, iSup_bool_eq, cond_true, cond_false]
-- 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
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)
⊢ Eq (α := Submodule R (α →₀ M)) (supported M R (s ∪ t)) (supported M R s ⊔ supported M R t)
have rw₄ : Eq (α := Submodule R (α →₀ M)) (supported M R s ⊔ supported M R t) (supported M R s ⊔ supported M R t)
Tactic: rw [Set.union_eq_iUnion, supported_iUnion, iSup_bool_eq, cond_true, cond_false]
-- 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
s t : Set α
⊢ Eq (α := Submodule R (α →₀ M)) (supported M R (s ∩ t)) (supported M R s ⊓ supported M R t)
have 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)
Tactic: rw [Set.inter_eq_iInter, supported_iInter, iInf_bool_eq]
-- 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
s t : Set α
h : Disjoint s t
⊢ Eq (α := Submodule R (α →₀ M)) (supported M R s ⊓ supported M R t) ⊥
have rw : Eq (α := Submodule R (α →₀ M)) (supported M R (s ∩ t)) ⊥
Tactic: rw [← supported_inter, disjoint_iff_inter_eq_empty.1 h, supported_empty]
-- 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
s t : Set α
h : Disjoint s t
rw : Eq (α := Submodule R (α →₀ M)) (supported M R (s ∩ t)) ⊥
⊢ Eq (α := Submodule R (α →₀ M)) (supported M R s ⊓ supported M R t) ⊥
have rw₁ : Eq (α := Submodule R (α →₀ M)) (supported M R ∅) ⊥
Tactic: rw [← supported_inter, disjoint_iff_inter_eq_empty.1 h, supported_empty]
-- 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
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 ∅) ⊥
⊢ Eq (α := Submodule R (α →₀ M)) (supported M R s ⊓ supported M R t) ⊥
have rw₂ : Eq (α := Submodule R (α →₀ M)) ⊥ ⊥
Tactic: rw [← supported_inter, disjoint_iff_inter_eq_empty.1 h, supported_empty]
-- 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
inst_3 : Nontrivial M
s t : Set α
⊢ Disjoint (α := Submodule R (α →₀ M)) (supported M R s) (supported M R t) ↔ Disjoint s t
have refine : ∀ (h : Disjoint (α := Submodule R (α →₀ M)) (supported M R s) (supported M R t)) (x : α) (hx1 : x ∈ s) (hx2 : x ∈ t),
  False
Tactic: refine ⟨fun h => Set.disjoint_left.mpr fun x hx1 hx2 => ?_, disjoint_supported_supported⟩
-- 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
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
⊢ False
have rcases : ∀ (y : M) (hy : y ≠ 0), False
Tactic: rcases exists_ne (0 : M) with ⟨y, hy⟩
-- 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
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
⊢ False
have this : 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⟩
-- 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
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)
⊢ False
have this₁ : y = 0
Tactic: rw [mem_bot, single_eq_zero] 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
s t : Set α
h : Codisjoint s t
⊢ Codisjoint (α := Submodule R (α →₀ M)) (supported M R s) (supported M R t)
have rw : Eq (α := 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]
-- 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
s t : Set α
h : Codisjoint s t
rw : Eq (α := Submodule R (α →₀ M)) (supported M R s ⊔ supported M R t) ⊤
⊢ Codisjoint (α := Submodule R (α →₀ M)) (supported M R s) (supported M R t)
have rw₁ : LE.le (α := 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]
-- 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
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)
⊢ Codisjoint (α := Submodule R (α →₀ M)) (supported M R s) (supported M R t)
have rw₂ : LE.le (α := Submodule R (α →₀ M)) ⊤ (supported M R (s ∪ t))
Tactic: rw [codisjoint_iff, eq_top_iff, ← supported_union,
    show s ∪ t = .univ from codisjoint_iff.mp h, supported_univ]
-- 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
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))
⊢ Codisjoint (α := Submodule R (α →₀ M)) (supported M R s) (supported M R t)
have rw₃ : LE.le (α := Submodule R (α →₀ M)) ⊤ (supported M R univ)
Tactic: rw [codisjoint_iff, eq_top_iff, ← supported_union,
    show s ∪ t = .univ from codisjoint_iff.mp h, supported_univ]
-- 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
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)
⊢ Codisjoint (α := Submodule R (α →₀ M)) (supported M R s) (supported M R t)
have rw₄ : LE.le (α := Submodule R (α →₀ M)) ⊤ ⊤
Tactic: rw [codisjoint_iff, eq_top_iff, ← supported_union,
    show s ∪ t = .univ from codisjoint_iff.mp h, supported_univ]
-- 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
inst_3 : Nontrivial M
s t : Set α
⊢ Codisjoint (α := Submodule R (α →₀ M)) (supported M R s) (supported M R t) ↔ Codisjoint s t
have refine : ∀ (h : Codisjoint (α := Submodule R (α →₀ M)) (supported M R s) (supported M R t)) (a : α),
  Membership.mem (γ := Set α) ⊤ a → a ∈ s ⊔ t
Tactic: refine ⟨fun h ↦ codisjoint_iff.mpr (eq_top_iff.mpr fun a ↦ ?_), codisjoint_supported_supported⟩
-- 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
inst_3 : Nontrivial M
s t : Set α
h : Codisjoint (α := Submodule R (α →₀ M)) (supported M R s) (supported M R t)
a : α
⊢ Membership.mem (γ := Set α) ⊤ a → a ∈ s ⊔ t
have obtain : ∀ (x : M) (hx : x ≠ 0), Membership.mem (γ := Set α) ⊤ a → a ∈ s ⊔ t
Tactic: obtain ⟨x, hx⟩ := exists_ne (0 : M)
-- 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
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
⊢ Membership.mem (γ := Set α) ⊤ a → a ∈ s ⊔ t
have 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
Tactic: rw [codisjoint_iff, ← supported_union, eq_top_iff'] at h
Cleared hypotheses: h, a, x, hx
-- 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
s : Set α
F : ↥(supported M R s) ≃ Finsupp.{u_1, u_2} (↑s : Type u_1) M := restrictSupportEquiv s M
⊢ ↥(supported M R s) ≃ₗ[R] Finsupp.{u_1, u_2} (↑s : Type u_1) M
have 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)
Tactic: refine F.toLinearEquiv ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Supported (hypothesis)
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
⊢ 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)
have 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)
Tactic: have :
    (F : supported M R s → ↥s →₀ M) =
      (lsubtypeDomain s : (α →₀ M) →ₗ[R] s →₀ M).comp (Submodule.subtype (supported M R s)) :=
    rfl
-- 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
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)
    (⇑F : (a : ↥(supported M R s)) → (↑s : Type u_1) →₀ M)
have 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)
Tactic: rw [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 α'
l : α →₀ M
⊢ Membership.mem (γ := Submodule R (α →₀ M)) (supported M R (f ⁻¹' s)) l →
    Membership.mem (γ := Submodule R (α →₀ M)) (comap (lmapDomain M R f) (supported M R s)) l
have Set : ∀ (hl : (↑l.support : Set α) ⊆ f ⁻¹' s),
  Membership.mem (γ := Submodule R (α →₀ M)) (comap (lmapDomain M R f) (supported M R s)) l
Tactic: (hl : (l.support : Set α) ⊆ f ⁻¹' 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 α'
l : α →₀ M
hl : (↑l.support : Set α) ⊆ f ⁻¹' s
⊢ Membership.mem (γ := Submodule R (α →₀ M)) (comap (lmapDomain M R f) (supported M R s)) l
have change : (↑(mapDomain f l).support : Set α') ⊆ s
Tactic: change ↑(mapDomain f l).support ⊆ s
-- 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 α'
l : α →₀ M
hl : (↑l.support : Set α) ⊆ f ⁻¹' s
⊢ (↑(mapDomain f l).support : Set α') ⊆ s
have hl₁ : (↑(Finset.image f l.support) : Set α') ⊆ s
Tactic: rw [← Set.image_subset_iff, ← Finset.coe_image] at hl
Cleared hypotheses: hl
-- 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 α'
⊢ LE.le (α := Submodule R (α →₀ M)) (supported M R (f ⁻¹' s)) (comap (lmapDomain M R f) (supported M R s))
have intro : ∀ ⦃l : α →₀ M⦄,
  Membership.mem (γ := Submodule R (α →₀ M)) (supported M R (f ⁻¹' s)) l →
    Membership.mem (γ := Submodule R (α →₀ M)) (comap (lmapDomain M R f) (supported M R s)) l
Tactic: classical
  intro l (hl : (l.support : Set α) ⊆ f ⁻¹' s)
  change ↑(mapDomain f l).support ⊆ s
  rw [← Set.image_subset_iff, ← Finset.coe_image] at hl
  exact Set.Subset.trans mapDomain_support hl
-- 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 α'
intro :
  ∀ ⦃l : α →₀ M⦄,
    Membership.mem (γ := Submodule R (α →₀ M)) (supported M R (f ⁻¹' s)) l →
      Membership.mem (γ := Submodule R (α →₀ M)) (comap (lmapDomain M R f) (supported M R s)) l
⊢ LE.le (α := Submodule R (α →₀ M)) (supported M R (f ⁻¹' s)) (comap (lmapDomain M R f) (supported M R s))
have intro₁ : ∀ ⦃l : α →₀ M⦄ (hl : (↑l.support : Set α) ⊆ f ⁻¹' s),
  Membership.mem (γ := Submodule R (α →₀ M)) (comap (lmapDomain M R f) (supported M R s)) l
Tactic: classical
  intro l (hl : (l.support : Set α) ⊆ f ⁻¹' s)
  change ↑(mapDomain f l).support ⊆ s
  rw [← Set.image_subset_iff, ← Finset.coe_image] at hl
  exact Set.Subset.trans mapDomain_support hl
-- 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 α'
intro :
  ∀ ⦃l : α →₀ M⦄,
    Membership.mem (γ := Submodule R (α →₀ M)) (supported M R (f ⁻¹' s)) l →
      Membership.mem (γ := Submodule R (α →₀ M)) (comap (lmapDomain M R f) (supported M R s)) l
intro₁ :
  ∀ ⦃l : α →₀ M⦄ (hl : (↑l.support : Set α) ⊆ f ⁻¹' s),
    Membership.mem (γ := Submodule R (α →₀ M)) (comap (lmapDomain M R f) (supported M R s)) l
⊢ LE.le (α := Submodule R (α →₀ M)) (supported M R (f ⁻¹' s)) (comap (lmapDomain M R f) (supported M R s))
have intro₂ : ∀ ⦃l : α →₀ M⦄ (hl : (↑l.support : Set α) ⊆ f ⁻¹' s), (↑(mapDomain f l).support : Set α') ⊆ s
Tactic: classical
  intro l (hl : (l.support : Set α) ⊆ f ⁻¹' s)
  change ↑(mapDomain f l).support ⊆ s
  rw [← Set.image_subset_iff, ← Finset.coe_image] at hl
  exact Set.Subset.trans mapDomain_support hl
-- 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 α'
intro :
  ∀ ⦃l : α →₀ M⦄,
    Membership.mem (γ := Submodule R (α →₀ M)) (supported M R (f ⁻¹' s)) l →
      Membership.mem (γ := Submodule R (α →₀ M)) (comap (lmapDomain M R f) (supported M R s)) l
intro₁ :
  ∀ ⦃l : α →₀ M⦄ (hl : (↑l.support : Set α) ⊆ f ⁻¹' s),
    Membership.mem (γ := Submodule R (α →₀ M)) (comap (lmapDomain M R f) (supported M R s)) l
intro₂ : ∀ ⦃l : α →₀ M⦄ (hl : (↑l.support : Set α) ⊆ f ⁻¹' s), (↑(mapDomain f l).support : Set α') ⊆ s
⊢ LE.le (α := Submodule R (α →₀ M)) (supported M R (f ⁻¹' s)) (comap (lmapDomain M R f) (supported M R s))
have intro₃ : ∀ ⦃l : α →₀ M⦄ (hl : (↑(Finset.image f l.support) : Set α') ⊆ s), (↑(mapDomain f l).support : Set α') ⊆ s
Tactic: classical
  intro l (hl : (l.support : Set α) ⊆ f ⁻¹' s)
  change ↑(mapDomain f l).support ⊆ s
  rw [← Set.image_subset_iff, ← Finset.coe_image] at hl
  exact Set.Subset.trans mapDomain_support hl
-- 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: cases isEmpty_or_nonempty α
-- 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: cases isEmpty_or_nonempty α
-- 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 α
⊢ Eq (α := Submodule R (α' →₀ M)) (map (lmapDomain M R f) (supported M R s)) (supported M R (f '' s))
have inr : LE.le (α := Submodule R (α' →₀ M)) (supported M R (f '' s)) (map (lmapDomain M R f) (supported M R s))
Tactic: refine
    le_antisymm
      (map_le_iff_le_comap.2 <|
        le_trans (supported_mono <| Set.subset_preimage_image _ _)
          (supported_comap_lmapDomain M R _ _))
      ?_