awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Lex (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : (i : ι) → Preorder (α i)
r : ι → ι → Prop
inst_2 : IsStrictOrder ι r
x y : Π₀ (i : ι), α i
hlt_1 : x < y
hle : (⇑x : (a : ι) → α a) ≤ (⇑y : (a : ι) → α a)
j : ι
hlt : (x : (a : ι) → α a) j < (y : (a : ι) → α a) j
have have₁ have₂ :
  ∀ (this : (↑(x.neLocus (N := α) y) : Set ι).WellFoundedOn r),
    ∃ (i : ι),
      (∀ (j : ι),
          r j i → (x : (a : ι) → α a) j ≤ (y : (a : ι) → α a) j ∧ (y : (a : ι) → α a) j ≤ (x : (a : ι) → α a) j) ∧
        (x : (a : ι) → α a) i < (y : (a : ι) → α a) i
have₃ :
  ∀ (this : (↑(x.neLocus (N := α) y) : Set ι).WellFoundedOn r)
    (i : { x_1 : ι // x_1 ∈ (↑(x.neLocus (N := α) y) : Set ι) })
    (hi :
      Membership.mem (γ := Set { x_1 : ι // x_1 ∈ (↑(x.neLocus (N := α) y) : Set ι) })
        {i : { x_1 : ι // x_1 ∈ (↑(x.neLocus (N := α) y) : Set ι) } |
          LT.lt (α := α (↑i : ι)) ((x : (a : ι) → α a) (↑i : ι)) ((y : (a : ι) → α a) (↑i : ι))}
        i)
    (hl :
      ∀ (x_1 : { x_1 : ι // x_1 ∈ (↑(x.neLocus (N := α) y) : Set ι) }),
        Membership.mem (γ := Set { x_2 : ι // x_2 ∈ (↑(x.neLocus (N := α) y) : Set ι) })
            {i : { x_2 : ι // x_2 ∈ (↑(x.neLocus (N := α) y) : Set ι) } |
              LT.lt (α := α (↑i : ι)) ((x : (a : ι) → α a) (↑i : ι)) ((y : (a : ι) → α a) (↑i : ι))}
            x_1 →
          ¬Subrel r (fun (x_2 : ι) ↦ x_2 ∈ (↑(x.neLocus (N := α) y) : Set ι)) x_1 i),
    ∃ (i : ι),
      (∀ (j : ι),
          r j i → (x : (a : ι) → α a) j ≤ (y : (a : ι) → α a) j ∧ (y : (a : ι) → α a) j ≤ (x : (a : ι) → α a) j) ∧
        (x : (a : ι) → α a) i < (y : (a : ι) → α a) i
⊢ ∃ (i : ι),
    (∀ (j : ι), r j i → (x : (a : ι) → α a) j ≤ (y : (a : ι) → α a) j ∧ (y : (a : ι) → α a) j ≤ (x : (a : ι) → α a) j) ∧
      (x : (a : ι) → α a) i < (y : (a : ι) → α a) i
have have₄ : ∀ (this : (↑(x.neLocus (N := α) y) : Set ι).WellFoundedOn r)
  (i : { x_1 : ι // x_1 ∈ (↑(x.neLocus (N := α) y) : Set ι) })
  (hi :
    Membership.mem (γ := Set { x_1 : ι // x_1 ∈ (↑(x.neLocus (N := α) y) : Set ι) })
      {i : { x_1 : ι // x_1 ∈ (↑(x.neLocus (N := α) y) : Set ι) } |
        LT.lt (α := α (↑i : ι)) ((x : (a : ι) → α a) (↑i : ι)) ((y : (a : ι) → α a) (↑i : ι))}
      i)
  (hl :
    ∀ (x_1 : { x_1 : ι // x_1 ∈ (↑(x.neLocus (N := α) y) : Set ι) }),
      Membership.mem (γ := Set { x_2 : ι // x_2 ∈ (↑(x.neLocus (N := α) y) : Set ι) })
          {i : { x_2 : ι // x_2 ∈ (↑(x.neLocus (N := α) y) : Set ι) } |
            LT.lt (α := α (↑i : ι)) ((x : (a : ι) → α a) (↑i : ι)) ((y : (a : ι) → α a) (↑i : ι))}
          x_1 →
        ¬Subrel r (fun (x_2 : ι) ↦ x_2 ∈ (↑(x.neLocus (N := α) y) : Set ι)) x_1 i)
  (k : ι) (hk : r k (↑i : ι)), (y : (a : ι) → α a) k ≤ (x : (a : ι) → α a) k
Tactic: classical
  have : (x.neLocus y : Set ι).WellFoundedOn r := (x.neLocus y).finite_toSet.wellFoundedOn
  obtain ⟨i, hi, hl⟩ := this.has_min { i | x i < y i } ⟨⟨j, mem_neLocus.2 hlt.ne⟩, hlt⟩
  refine ⟨i, fun k hk ↦ ⟨hle k, ?_⟩, hi⟩
  exact of_not_not fun h ↦ hl ⟨k, mem_neLocus.2 (ne_of_not_le h).symm⟩ ((hle k).lt_of_not_ge h) hk
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Lex (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : (i : ι) → PartialOrder (α i)
r : ι → ι → Prop
inst_2 : IsStrictOrder ι r
x y : Π₀ (i : ι), α i
hlt : x < y
⊢ Pi.Lex (β := α) r (fun {i : ι} (x1 x2 : α i) ↦ x1 < x2) (⇑x : (a : ι) → α a) (⇑y : (a : ι) → α a)
have simp_rw : ∃ (i : ι),
  (∀ (j : ι), r j i → (x : (a : ι) → α a) j ≤ (y : (a : ι) → α a) j ∧ (y : (a : ι) → α a) j ≤ (x : (a : ι) → α a) j) ∧
    (x : (a : ι) → α a) i < (y : (a : ι) → α a) i
Tactic: simp_rw [Pi.Lex, le_antisymm_iff]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Lex (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : LinearOrder ι
inst_2 : (i : ι) → LinearOrder (α i)
P : Lex (Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i) → Sort u_3
h_lt :
  {f g : Π₀ (i : ι), α i} →
    LT.lt (α := Lex (Π₀ (i : ι), α i))
        ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) f : Lex (Π₀ (i : ι), α i))
        ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) g : Lex (Π₀ (i : ι), α i)) →
      P ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) f)
        ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) g)
h_eq :
  {f g : Π₀ (i : ι), α i} →
    Eq (α := Lex (Π₀ (i : ι), α i)) ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) f : Lex (Π₀ (i : ι), α i))
        ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) g : Lex (Π₀ (i : ι), α i)) →
      P ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) f)
        ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) g)
h_gt :
  {f g : Π₀ (i : ι), α i} →
    LT.lt (α := Lex (Π₀ (i : ι), α i))
        ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) g : Lex (Π₀ (i : ι), α i))
        ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) f : Lex (Π₀ (i : ι), α i)) →
      P ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) f)
        ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) g)
f g : Π₀ (i : ι), α i
wit : ι
h : (f.neLocus (N := α) g).min = (↑wit : WithTop ι)
⊢ P ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) f)
    ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) g)
have h₁ : (f : (a : ι) → α a) wit < (g : (a : ι) → α a) wit →
  P ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) f)
    ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) g)
Tactic: apply (mem_neLocus.mp <| Finset.mem_of_min h).lt_or_gt.by_cases
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Lex (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : LinearOrder ι
inst_2 : (i : ι) → LinearOrder (α i)
P : Lex (Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i) → Sort u_3
h_lt :
  {f g : Π₀ (i : ι), α i} →
    LT.lt (α := Lex (Π₀ (i : ι), α i))
        ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) f : Lex (Π₀ (i : ι), α i))
        ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) g : Lex (Π₀ (i : ι), α i)) →
      P ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) f)
        ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) g)
h_eq :
  {f g : Π₀ (i : ι), α i} →
    Eq (α := Lex (Π₀ (i : ι), α i)) ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) f : Lex (Π₀ (i : ι), α i))
        ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) g : Lex (Π₀ (i : ι), α i)) →
      P ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) f)
        ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) g)
h_gt :
  {f g : Π₀ (i : ι), α i} →
    LT.lt (α := Lex (Π₀ (i : ι), α i))
        ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) g : Lex (Π₀ (i : ι), α i))
        ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) f : Lex (Π₀ (i : ι), α i)) →
      P ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) f)
        ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) g)
f g : Π₀ (i : ι), α i
wit : ι
h : (f.neLocus (N := α) g).min = (↑wit : WithTop ι)
h₁ :
  (f : (a : ι) → α a) wit < (g : (a : ι) → α a) wit →
    P ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) f)
      ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) g)
⊢ P ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) f)
    ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) g)
have h₂ : (g : (a : ι) → α a) wit < (f : (a : ι) → α a) wit →
  P ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) f)
    ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) g)
Tactic: apply (mem_neLocus.mp <| Finset.mem_of_min h).lt_or_gt.by_cases
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Lex (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : LinearOrder ι
inst_2 : (i : ι) → LinearOrder (α i)
P : Lex (Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i) → Sort u_3
h_lt :
  {f g : Π₀ (i : ι), α i} →
    LT.lt (α := Lex (Π₀ (i : ι), α i))
        ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) f : Lex (Π₀ (i : ι), α i))
        ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) g : Lex (Π₀ (i : ι), α i)) →
      P ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) f)
        ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) g)
h_eq :
  {f g : Π₀ (i : ι), α i} →
    Eq (α := Lex (Π₀ (i : ι), α i)) ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) f : Lex (Π₀ (i : ι), α i))
        ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) g : Lex (Π₀ (i : ι), α i)) →
      P ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) f)
        ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) g)
h_gt :
  {f g : Π₀ (i : ι), α i} →
    LT.lt (α := Lex (Π₀ (i : ι), α i))
        ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) g : Lex (Π₀ (i : ι), α i))
        ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) f : Lex (Π₀ (i : ι), α i)) →
      P ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) f)
        ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) g)
f g : Π₀ (i : ι), α i
wit : ι
h : (f.neLocus (N := α) g).min = (↑wit : WithTop ι)
hwit : (g : (a : ι) → α a) wit < (f : (a : ι) → α a) wit
j : ι
hj : (fun (x1 x2 : ι) ↦ x1 < x2) j wit
⊢ Finset.min
      (neLocus (N := α)
        ((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i)
          ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) g))
        ((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i)
          ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) f))) =
    (↑wit : WithTop ι)
have rwa : Finset.min
    (neLocus (N := α)
      ((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i)
        ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) f))
      ((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i)
        ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) g))) =
  (↑wit : WithTop ι)
Tactic: rwa [neLocus_comm]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Lex (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : LinearOrder ι
inst_2 : (i : ι) → PartialOrder (α i)
a b : Π₀ (i : ι), α i
h : a ≤ b
⊢ LE.le (α := Lex (Π₀ (i : ι), α i)) ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) a : Lex (Π₀ (i : ι), α i))
    ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) b : Lex (Π₀ (i : ι), α i))
have refine : ∀
  (hne :
    ¬Eq (α := Lex (Π₀ (i : ι), α i)) ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) a : Lex (Π₀ (i : ι), α i))
        ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) b : Lex (Π₀ (i : ι), α i))),
  LT.lt (α := Lex (Π₀ (i : ι), α i)) ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) a : Lex (Π₀ (i : ι), α i))
    ((toLex : (a : Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i)) b : Lex (Π₀ (i : ι), α i))
Tactic: refine le_of_lt_or_eq (or_iff_not_imp_right.2 fun hne ↦ ?_)
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Lex (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → AddMonoid (α i)
inst_2 : (i : ι) → LinearOrder (α i)
inst_3 : ∀ (i : ι), AddLeftStrictMono.{u_2} (α i)
x x_1 x_2 : Lex (Π₀ (i : ι), α i)
h : x_1 < x_2
a : ι
lta :
  ∀ (j : ι),
    (fun (x1 x2 : ι) ↦ x1 < x2) j a →
      (((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) x_1 : Π₀ (i : ι), α i) : (a : ι) → α a) j =
        (((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) x_2 : Π₀ (i : ι), α i) : (a : ι) → α a) j
ha :
  (fun {i : ι} ↦ ((fun (x : ι) (x1 x2 : α x) ↦ x1 < x2) i : α i → α i → Prop))
    ((((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) x_1 : Π₀ (i : ι), α i) : (a : ι) → α a) a)
    ((((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) x_2 : Π₀ (i : ι), α i) : (a : ι) → α a) a)
⊢ (fun {i : ι} ↦ ((fun (x : ι) (x1 x2 : α x) ↦ x1 < x2) i : α i → α i → Prop))
    ((((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) (x + x_1) : Π₀ (i : ι), α i) : (a : ι) → α a) a)
    ((((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) (x + x_2) : Π₀ (i : ι), α i) : (a : ι) → α a) a)
have dsimp : (((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) x : Π₀ (i : ι), α i) : (a : ι) → α a) a +
    (((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) x_1 : Π₀ (i : ι), α i) : (a : ι) → α a) a <
  (((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) x : Π₀ (i : ι), α i) : (a : ι) → α a) a +
    (((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) x_2 : Π₀ (i : ι), α i) : (a : ι) → α a) a
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Lex (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → AddMonoid (α i)
inst_2 : (i : ι) → LinearOrder (α i)
inst_3 : ∀ (i : ι), AddRightStrictMono.{u_2} (α i)
f x x_1 : Lex (Π₀ (i : ι), α i)
h : x < x_1
a : ι
lta :
  ∀ (j : ι),
    (fun (x1 x2 : ι) ↦ x1 < x2) j a →
      (((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) x : Π₀ (i : ι), α i) : (a : ι) → α a) j =
        (((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) x_1 : Π₀ (i : ι), α i) : (a : ι) → α a) j
ha :
  (fun {i : ι} ↦ ((fun (x : ι) (x1 x2 : α x) ↦ x1 < x2) i : α i → α i → Prop))
    ((((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) x : Π₀ (i : ι), α i) : (a : ι) → α a) a)
    ((((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) x_1 : Π₀ (i : ι), α i) : (a : ι) → α a) a)
⊢ (fun {i : ι} ↦ ((fun (x : ι) (x1 x2 : α x) ↦ x1 < x2) i : α i → α i → Prop))
    ((((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i)
            (Function.swap (φ := fun (a a_1 : Lex (Π₀ (i : ι), α i)) ↦ Lex (Π₀ (i : ι), α i))
              (fun (x1 x2 : Lex (Π₀ (i : ι), α i)) ↦ x1 + x2) f x) :
          Π₀ (i : ι), α i) :
        (a : ι) → α a)
      a)
    ((((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i)
            (Function.swap (φ := fun (a a_1 : Lex (Π₀ (i : ι), α i)) ↦ Lex (Π₀ (i : ι), α i))
              (fun (x1 x2 : Lex (Π₀ (i : ι), α i)) ↦ x1 + x2) f x_1) :
          Π₀ (i : ι), α i) :
        (a : ι) → α a)
      a)
have dsimp : (((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) x : Π₀ (i : ι), α i) : (a : ι) → α a) a +
    (((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) f : Π₀ (i : ι), α i) : (a : ι) → α a) a <
  (((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) x_1 : Π₀ (i : ι), α i) : (a : ι) → α a) a +
    (((ofLex : (a : Lex (Π₀ (i : ι), α i)) → Π₀ (i : ι), α i) f : Π₀ (i : ι), α i) : (a : ι) → α a) a
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Module (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : (i : ι) → SMulZeroClass.{w, v} γ (β i)
p : ι → Prop
inst_2 : DecidablePred p
r : γ
f : Π₀ (i : ι), β i
⊢ filter (β := β) p (r • f) = r • filter (β := β) p f
have h : ∀ (i : ι), (filter (β := β) p (r • f) : (a : ι) → β a) i = (r • filter (β := β) p f : (a : ι) → β a) i
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Module (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → SMulZeroClass.{w, v} γ (β i)
s : Finset ι
c : γ
x : (i : (↑(↑s : Set ι) : Type u)) → β (↑i : ι)
i : ι
⊢ (mk (β := β) s (c • x) : (a : ι) → β a) i = (HSMul.hSMul (β := Π₀ (i : ι), β i) c (mk (β := β) s x) : (a : ι) → β a) i
have simp : (if H : i ∈ s then (c • x) (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0) =
  HSMul.hSMul (β := β i) c (if H : i ∈ s then x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0)
Tactic: simp only [smul_apply, mk_apply]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Module (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → SMulZeroClass.{w, v} γ (β i)
s : Finset ι
c : γ
x : (i : (↑(↑s : Set ι) : Type u)) → β (↑i : ι)
i : ι
⊢ (if H : i ∈ s then (c • x) (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0) =
    HSMul.hSMul (β := β i) c (if H : i ∈ s then x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0)
have pos : ∀ (h : i ∈ s),
  (c • x) (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) =
    HSMul.hSMul (β := β i) c
      (x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) :
        β (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) : ι))
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Module (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → SMulZeroClass.{w, v} γ (β i)
s : Finset ι
c : γ
x : (i : (↑(↑s : Set ι) : Type u)) → β (↑i : ι)
i : ι
pos :
  ∀ (h : i ∈ s),
    (c • x) (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) =
      HSMul.hSMul (β := β i) c
        (x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) :
          β (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) : ι))
⊢ (if H : i ∈ s then (c • x) (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0) =
    HSMul.hSMul (β := β i) c (if H : i ∈ s then x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0)
have neg : i ∉ s → 0 = HSMul.hSMul (β := β i) c 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Module (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → SMulZeroClass.{w, v} γ (β i)
s : Finset ι
c : γ
x : (i : (↑(↑s : Set ι) : Type u)) → β (↑i : ι)
i : ι
h : i ∉ s
⊢ 0 = HSMul.hSMul (β := β i) c 0
have neg : Eq.{v + 1} (α := β i) 0 0
Tactic: rw [smul_zero]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Module (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → SMulZeroClass.{w, v} γ (β i)
s : Finset ι
c : γ
x : (i : (↑(↑s : Set ι) : Type u)) → β (↑i : ι)
i : ι
⊢ (if H : i ∈ s then (c • x) (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0) =
    HSMul.hSMul (β := β i) c (if H : i ∈ s then x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0)
have pos : ∀ (h : i ∈ s),
  (c • x) (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) =
    HSMul.hSMul (β := β i) c
      (x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) :
        β (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) : ι))
Tactic: split_ifs <;> [rfl; rw [smul_zero]]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Module (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → SMulZeroClass.{w, v} γ (β i)
s : Finset ι
c : γ
x : (i : (↑(↑s : Set ι) : Type u)) → β (↑i : ι)
i : ι
pos :
  ∀ (h : i ∈ s),
    (c • x) (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) =
      HSMul.hSMul (β := β i) c
        (x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) :
          β (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) : ι))
⊢ (if H : i ∈ s then (c • x) (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0) =
    HSMul.hSMul (β := β i) c (if H : i ∈ s then x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0)
have neg : i ∉ s → 0 = HSMul.hSMul (β := β i) c 0
Tactic: split_ifs <;> [rfl; rw [smul_zero]]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Module (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → SMulZeroClass.{w, v} γ (β i)
i_1 : ι
c : γ
x : β i_1
i : ι
⊢ (single (β := β) i_1 (c • x) : (a : ι) → β a) i =
    (HSMul.hSMul (β := Π₀ (i : ι), β i) c (single (β := β) i_1 x) : (a : ι) → β a) i
have simp : (if h : i_1 = i then Eq.rec (motive := fun (x : ι) (x_1 : i_1 = x) ↦ β x) (c • x) sorry else 0) =
  HSMul.hSMul (β := β i) c (if h : i_1 = i then Eq.rec (motive := fun (x : ι) (x_1 : i_1 = x) ↦ β x) x sorry else 0)
Tactic: simp only [smul_apply, single_apply]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Module (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → SMulZeroClass.{w, v} γ (β i)
i_1 : ι
c : γ
x : β i_1
i : ι
⊢ (if h : i_1 = i then Eq.rec (motive := fun (x : ι) (x_1 : i_1 = x) ↦ β x) (c • x) ⋯ else 0) =
    HSMul.hSMul (β := β i) c (if h : i_1 = i then Eq.rec (motive := fun (x : ι) (x_1 : i_1 = x) ↦ β x) x ⋯ else 0)
have pos : ∀ (h : i_1 = i),
  Eq.rec (motive := fun (x : ι) (x_1 : i_1 = x) ↦ β x) (c • x) sorry =
    HSMul.hSMul (β := β i) c (Eq.rec (motive := fun (x : ι) (x_1 : i_1 = x) ↦ β x) x sorry : β i)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Module (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → SMulZeroClass.{w, v} γ (β i)
i_1 : ι
c : γ
x : β i_1
i : ι
pos :
  ∀ (h : i_1 = i),
    Eq.rec (motive := fun (x : ι) (x_1 : i_1 = x) ↦ β x) (c • x) ⋯ =
      HSMul.hSMul (β := β i) c (Eq.rec (motive := fun (x : ι) (x_1 : i_1 = x) ↦ β x) x ⋯ : β i)
⊢ (if h : i_1 = i then Eq.rec (motive := fun (x : ι) (x_1 : i_1 = x) ↦ β x) (c • x) ⋯ else 0) =
    HSMul.hSMul (β := β i) c (if h : i_1 = i then Eq.rec (motive := fun (x : ι) (x_1 : i_1 = x) ↦ β x) x ⋯ else 0)
have neg : ∀ (h : ¬i_1 = i), 0 = HSMul.hSMul (β := β i) c 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Module (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → SMulZeroClass.{w, v} γ (β i)
i_1 : ι
c : γ
x : β i_1
i : ι
h : i_1 = i
⊢ Eq.rec (motive := fun (x : ι) (x_1 : i_1 = x) ↦ β x) (c • x) ⋯ =
    HSMul.hSMul (β := β i) c (Eq.rec (motive := fun (x : ι) (x_1 : i_1 = x) ↦ β x) x ⋯ : β i)
have pos : Eq.rec (motive := fun (x : ι) (x_1 : i_1 = x) ↦ β x) (c • x) sorry =
  HSMul.hSMul (β := β i_1) c (Eq.rec (motive := fun (x : ι) (x_1 : i_1 = x) ↦ β x) x sorry : β i_1)
Tactic: cases h
Cleared hypotheses: i, h
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Module (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → SMulZeroClass.{w, v} γ (β i)
i_1 : ι
c : γ
x : β i_1
i : ι
h : ¬i_1 = i
⊢ 0 = HSMul.hSMul (β := β i) c 0
have neg : Eq.{v + 1} (α := β i) 0 0
Tactic: rw [smul_zero]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Module (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
κ : Type u_1
inst : (i : ι) → Zero (β i)
inst_1 : (i : ι) → SMulZeroClass.{w, v} γ (β i)
h : κ → ι
hh : Function.Injective h
r : γ
f : Π₀ (i : ι), β i
⊢ comapDomain (β := β) h hh (r • f) = r • comapDomain (β := β) h hh f
have h₁ : ∀ (i : κ),
  (comapDomain (β := β) h hh (r • f) : (a : κ) → β (h a)) i = (r • comapDomain (β := β) h hh f : (a : κ) → β (h a)) i
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Module (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
κ : Type u_1
inst : (i : ι) → Zero (β i)
inst_1 : (i : ι) → SMulZeroClass.{w, v} γ (β i)
h : κ → ι
hh : Function.Injective h
r : γ
f : Π₀ (i : ι), β i
i : κ
⊢ (comapDomain (β := β) h hh (r • f) : (a : κ) → β (h a)) i = (r • comapDomain (β := β) h hh f : (a : κ) → β (h a)) i
have h₁ : (comapDomain (β := β) h hh (r • f) : (a : κ) → β (h a)) i = r • (comapDomain (β := β) h hh f : (a : κ) → β (h a)) i
Tactic: rw [smul_apply, comapDomain_apply, smul_apply, comapDomain_apply]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Module (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
κ : Type u_1
inst : (i : ι) → Zero (β i)
inst_1 : (i : ι) → SMulZeroClass.{w, v} γ (β i)
h : κ → ι
hh : Function.Injective h
r : γ
f : Π₀ (i : ι), β i
i : κ
h₁ : (comapDomain (β := β) h hh (r • f) : (a : κ) → β (h a)) i = r • (comapDomain (β := β) h hh f : (a : κ) → β (h a)) i
⊢ (comapDomain (β := β) h hh (r • f) : (a : κ) → β (h a)) i = (r • comapDomain (β := β) h hh f : (a : κ) → β (h a)) i
have h₂ : (r • f : (a : ι) → β a) (h i) = r • (comapDomain (β := β) h hh f : (a : κ) → β (h a)) i
Tactic: rw [smul_apply, comapDomain_apply, smul_apply, comapDomain_apply]