awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → AddZeroClass (β i)
inst_1 : (i : ι) → AddZeroClass (β₁ i)
inst_2 : (i : ι) → AddZeroClass (β₂ i)
f : (i : ι) → AddMonoidHom.{v₁, v₂} (β₁ i) (β₂ i)
f₂ : (i : ι) → AddMonoidHom.{v, v₁} (β i) (β₁ i)
⊢ (addMonoidHom (β₁ := β) (β₂ := β₂) fun (i : ι) ↦ (f i).comp (f₂ i)) =
    (addMonoidHom (β₁ := β₁) (β₂ := β₂) f).comp (addMonoidHom (β₁ := β) (β₂ := β₁) f₂)
have h : ∀ (x : Π₀ (i : ι), β i) (i : ι),
  (((addMonoidHom (β₁ := β) (β₂ := β₂) fun (i : ι) ↦ (f i).comp (f₂ i) : (a : Π₀ (i : ι), β i) → Π₀ (i : ι), β₂ i) x :
          Π₀ (i : ι), β₂ i) :
        (a : ι) → β₂ a)
      i =
    ((((addMonoidHom (β₁ := β₁) (β₂ := β₂) f).comp (addMonoidHom (β₁ := β) (β₂ := β₁) f₂) :
              (a : Π₀ (i : ι), β i) → Π₀ (i : ι), β₂ i)
            x :
          Π₀ (i : ι), β₂ i) :
        (a : ι) → β₂ a)
      i
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → AddZeroClass (β i)
inst_1 : (i : ι) → AddZeroClass (β₁ i)
inst_2 : (i : ι) → AddZeroClass (β₂ i)
e : (i : ι) → AddEquiv.{v₁, v₂} (β₁ i) (β₂ i)
x : Π₀ (i : ι), β₁ i
⊢ mapRange (β₁ := β₂) (β₂ := β₁) (fun (i : ι) (x : β₂ i) ↦ ((e i).symm : (a : β₂ i) → β₁ i) x) ⋯
      (mapRange (β₁ := β₁) (β₂ := β₂) (fun (i : ι) (x : β₁ i) ↦ (e i : (a : β₁ i) → β₂ i) x) ⋯ x) =
    x
have rw : mapRange (β₁ := β₁) (β₂ := β₁)
    (fun (i : ι) ↦ (fun (x : β₂ i) ↦ ((e i).symm : (a : β₂ i) → β₁ i) x) ∘ fun (x : β₁ i) ↦ (e i : (a : β₁ i) → β₂ i) x)
    sorry x =
  x
Tactic: rw [← mapRange_comp]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → AddZeroClass (β i)
inst_1 : (i : ι) → AddZeroClass (β₁ i)
inst_2 : (i : ι) → AddZeroClass (β₂ i)
e : (i : ι) → AddEquiv.{v₁, v₂} (β₁ i) (β₂ i)
x : Π₀ (i : ι), β₁ i
rw :
  mapRange (β₁ := β₁) (β₂ := β₁)
      (fun (i : ι) ↦
        (fun (x : β₂ i) ↦ ((e i).symm : (a : β₂ i) → β₁ i) x) ∘ fun (x : β₁ i) ↦ (e i : (a : β₁ i) → β₂ i) x)
      ⋯ x =
    x
⊢ mapRange (β₁ := β₂) (β₂ := β₁) (fun (i : ι) (x : β₂ i) ↦ ((e i).symm : (a : β₂ i) → β₁ i) x) ⋯
      (mapRange (β₁ := β₁) (β₂ := β₂) (fun (i : ι) (x : β₁ i) ↦ (e i : (a : β₁ i) → β₂ i) x) ⋯ x) =
    x
have h : ∀ (i : ι),
  Eq.{v₁ + 1} (α := β₁ i)
    (((fun (x : β₂ i) ↦ ((e i).symm : (a : β₂ i) → β₁ i) x) ∘ fun (x : β₁ i) ↦ (e i : (a : β₁ i) → β₂ i) x) 0) 0
Tactic: rw [← mapRange_comp]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → AddZeroClass (β i)
inst_1 : (i : ι) → AddZeroClass (β₁ i)
inst_2 : (i : ι) → AddZeroClass (β₂ i)
e : (i : ι) → AddEquiv.{v₁, v₂} (β₁ i) (β₂ i)
x : Π₀ (i : ι), β₁ i
⊢ mapRange (β₁ := β₁) (β₂ := β₁)
      (fun (i : ι) ↦
        (fun (x : β₂ i) ↦ ((e i).symm : (a : β₂ i) → β₁ i) x) ∘ fun (x : β₁ i) ↦ (e i : (a : β₁ i) → β₂ i) x)
      ⋯ x =
    x
have simp_rw : mapRange (β₁ := β₁) (β₂ := β₁) (fun (i : ι) ↦ id) sorry x = x
Tactic: simp_rw [AddEquiv.symm_comp_self]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → AddZeroClass (β i)
inst_1 : (i : ι) → AddZeroClass (β₁ i)
inst_2 : (i : ι) → AddZeroClass (β₂ i)
e : (i : ι) → AddEquiv.{v₁, v₂} (β₁ i) (β₂ i)
x : Π₀ (i : ι), β₁ i
⊢ ∀ (i : ι),
    Eq.{v₁ + 1} (α := β₁ i)
      (((fun (x : β₂ i) ↦ ((e i).symm : (a : β₂ i) → β₁ i) x) ∘ fun (x : β₁ i) ↦ (e i : (a : β₁ i) → β₂ i) x) 0) 0
have h : ∀ (i : ι), Eq.{v₁ + 1} (α := β₁ i) (id 0) 0
Tactic: simp_rw [AddEquiv.symm_comp_self]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → AddZeroClass (β i)
inst_1 : (i : ι) → AddZeroClass (β₁ i)
inst_2 : (i : ι) → AddZeroClass (β₂ i)
e : (i : ι) → AddEquiv.{v₁, v₂} (β₁ i) (β₂ i)
x : Π₀ (i : ι), β₂ i
⊢ mapRange (β₁ := β₁) (β₂ := β₂) (fun (i : ι) (x : β₁ i) ↦ (e i : (a : β₁ i) → β₂ i) x) ⋯
      (mapRange (β₁ := β₂) (β₂ := β₁) (fun (i : ι) (x : β₂ i) ↦ ((e i).symm : (a : β₂ i) → β₁ i) x) ⋯ x) =
    x
have rw : mapRange (β₁ := β₂) (β₂ := β₂)
    (fun (i : ι) ↦ (fun (x : β₁ i) ↦ (e i : (a : β₁ i) → β₂ i) x) ∘ fun (x : β₂ i) ↦ ((e i).symm : (a : β₂ i) → β₁ i) x)
    sorry x =
  x
Tactic: rw [← mapRange_comp]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → AddZeroClass (β i)
inst_1 : (i : ι) → AddZeroClass (β₁ i)
inst_2 : (i : ι) → AddZeroClass (β₂ i)
e : (i : ι) → AddEquiv.{v₁, v₂} (β₁ i) (β₂ i)
x : Π₀ (i : ι), β₂ i
rw :
  mapRange (β₁ := β₂) (β₂ := β₂)
      (fun (i : ι) ↦
        (fun (x : β₁ i) ↦ (e i : (a : β₁ i) → β₂ i) x) ∘ fun (x : β₂ i) ↦ ((e i).symm : (a : β₂ i) → β₁ i) x)
      ⋯ x =
    x
⊢ mapRange (β₁ := β₁) (β₂ := β₂) (fun (i : ι) (x : β₁ i) ↦ (e i : (a : β₁ i) → β₂ i) x) ⋯
      (mapRange (β₁ := β₂) (β₂ := β₁) (fun (i : ι) (x : β₂ i) ↦ ((e i).symm : (a : β₂ i) → β₁ i) x) ⋯ x) =
    x
have h : ∀ (i : ι),
  Eq.{v₂ + 1} (α := β₂ i)
    (((fun (x : β₁ i) ↦ (e i : (a : β₁ i) → β₂ i) x) ∘ fun (x : β₂ i) ↦ ((e i).symm : (a : β₂ i) → β₁ i) x) 0) 0
Tactic: rw [← mapRange_comp]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → AddZeroClass (β i)
inst_1 : (i : ι) → AddZeroClass (β₁ i)
inst_2 : (i : ι) → AddZeroClass (β₂ i)
e : (i : ι) → AddEquiv.{v₁, v₂} (β₁ i) (β₂ i)
x : Π₀ (i : ι), β₂ i
⊢ mapRange (β₁ := β₂) (β₂ := β₂)
      (fun (i : ι) ↦
        (fun (x : β₁ i) ↦ (e i : (a : β₁ i) → β₂ i) x) ∘ fun (x : β₂ i) ↦ ((e i).symm : (a : β₂ i) → β₁ i) x)
      ⋯ x =
    x
have simp_rw : mapRange (β₁ := β₂) (β₂ := β₂) (fun (i : ι) ↦ id) sorry x = x
Tactic: simp_rw [AddEquiv.self_comp_symm]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → AddZeroClass (β i)
inst_1 : (i : ι) → AddZeroClass (β₁ i)
inst_2 : (i : ι) → AddZeroClass (β₂ i)
e : (i : ι) → AddEquiv.{v₁, v₂} (β₁ i) (β₂ i)
x : Π₀ (i : ι), β₂ i
⊢ ∀ (i : ι),
    Eq.{v₂ + 1} (α := β₂ i)
      (((fun (x : β₁ i) ↦ (e i : (a : β₁ i) → β₂ i) x) ∘ fun (x : β₂ i) ↦ ((e i).symm : (a : β₂ i) → β₁ i) x) 0) 0
have h : ∀ (i : ι), Eq.{v₂ + 1} (α := β₂ i) (id 0) 0
Tactic: simp_rw [AddEquiv.self_comp_symm]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → AddZeroClass (β i)
inst_1 : (i : ι) → AddZeroClass (β₁ i)
inst_2 : (i : ι) → AddZeroClass (β₂ i)
f : (i : ι) → AddEquiv.{v, v₁} (β i) (β₁ i)
f₂ : (i : ι) → AddEquiv.{v₁, v₂} (β₁ i) (β₂ i)
⊢ (addEquiv (β₁ := β) (β₂ := β₂) fun (i : ι) ↦ (f i).trans (f₂ i)) =
    (addEquiv (β₁ := β) (β₂ := β₁) f).trans (addEquiv (β₁ := β₁) (β₂ := β₂) f₂)
have h : ∀ (x : Π₀ (i : ι), β i) (i : ι),
  (((addEquiv (β₁ := β) (β₂ := β₂) fun (i : ι) ↦ (f i).trans (f₂ i) : (a : Π₀ (i : ι), β i) → Π₀ (i : ι), β₂ i) x :
          Π₀ (i : ι), β₂ i) :
        (a : ι) → β₂ a)
      i =
    ((((addEquiv (β₁ := β) (β₂ := β₁) f).trans (addEquiv (β₁ := β₁) (β₂ := β₂) f₂) :
              (a : Π₀ (i : ι), β i) → Π₀ (i : ι), β₂ i)
            x :
          Π₀ (i : ι), β₂ i) :
        (a : ι) → β₂ a)
      i
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Ext (goal)
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
x : Π₀ (i : ι), β i
h : Membership.mem (γ := AddSubmonoid (Π₀ (i : ι), β i)) ⊤ x
⊢ Membership.mem (γ := AddSubmonoid (Π₀ (i : ι), β i)) (AddSubmonoid.closure (⋃ (i : ι), Set.range (single (β := β) i)))
    x
have h0 : Membership.mem (γ := AddSubmonoid (Π₀ (i : ι), β i)) (AddSubmonoid.closure (⋃ (i : ι), Set.range (single (β := β) i))) 0
Tactic: apply DFinsupp.induction x
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Ext (goal)
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
x : Π₀ (i : ι), β i
h : Membership.mem (γ := AddSubmonoid (Π₀ (i : ι), β i)) ⊤ x
h0 :
  Membership.mem (γ := AddSubmonoid (Π₀ (i : ι), β i)) (AddSubmonoid.closure (⋃ (i : ι), Set.range (single (β := β) i)))
    0
⊢ Membership.mem (γ := AddSubmonoid (Π₀ (i : ι), β i)) (AddSubmonoid.closure (⋃ (i : ι), Set.range (single (β := β) i)))
    x
have ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i),
  (f : (a : ι) → β a) i = 0 →
    b ≠ 0 →
      Membership.mem (γ := AddSubmonoid (Π₀ (i : ι), β i))
          (AddSubmonoid.closure (⋃ (i : ι), Set.range (single (β := β) i))) f →
        Membership.mem (γ := AddSubmonoid (Π₀ (i : ι), β i))
          (AddSubmonoid.closure (⋃ (i : ι), Set.range (single (β := β) i))) (single (β := β) i b + f)
Tactic: apply DFinsupp.induction x
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Ext (goal)
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
γ : Type w
inst_2 : AddZeroClass γ
f g : (Π₀ (i : ι), β i) →+ γ
H :
  ∀ (i : ι) (y : β i),
    Eq.{w + 1} (α := γ) ((f : (a : Π₀ (i : ι), β i) → γ) (single (β := β) i y) : γ)
      ((g : (a : Π₀ (i : ι), β i) → γ) (single (β := β) i y) : γ)
⊢ f = g
have refine : ∀ (f_1 : Π₀ (i : ι), β i)
  (hf : Membership.mem (γ := Set (Π₀ (i : ι), β i)) (⋃ (i : ι), Set.range (single (β := β) i)) f_1),
  Eq.{w + 1} (α := γ) ((f : (a : Π₀ (i : ι), β i) → γ) f_1 : γ) ((g : (a : Π₀ (i : ι), β i) → γ) f_1 : γ)
Tactic: refine AddMonoidHom.eq_of_eqOn_denseM add_closure_iUnion_range_single fun f hf => ?_
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Ext (hypothesis)
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
γ : Type w
inst_2 : AddZeroClass γ
f_1 g : (Π₀ (i : ι), β i) →+ γ
H :
  ∀ (i : ι) (y : β i),
    Eq.{w + 1} (α := γ) ((f_1 : (a : Π₀ (i : ι), β i) → γ) (single (β := β) i y) : γ)
      ((g : (a : Π₀ (i : ι), β i) → γ) (single (β := β) i y) : γ)
f : Π₀ (i : ι), β i
hf : Membership.mem (γ := Set (Π₀ (i : ι), β i)) (⋃ (i : ι), Set.range (single (β := β) i)) f
⊢ Eq.{w + 1} (α := γ) ((f_1 : (a : Π₀ (i : ι), β i) → γ) f : γ) ((g : (a : Π₀ (i : ι), β i) → γ) f : γ)
have hf₁ : ∃ (i : ι) (y : β i), single (β := β) i y = f
Tactic: simp only [Set.mem_iUnion, Set.mem_range] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Data.DFinsupp.FiniteInfinite (goal)
Goal:
ι_1 : Type u
γ : Type w
β : ι_1 → Type v
β₁ : ι_1 → Type v₁
β₂ : ι_1 → Type v₂
ι : Type u_1
π : ι → Type u_2
inst : ∀ (i : ι), Nontrivial.{u_2} (π i)
inst_1 : (i : ι) → Zero (π i)
inst_2 : Infinite ι
this : DecidableEq ι := Classical.decEq ι
⊢ Infinite (Π₀ (i : ι), π i)
have choose : ∀ (m : (i : ι) → π i) (hm : ∀ (i : ι), m i ≠ 0), Infinite (Π₀ (i : ι), π i)
Tactic: choose m hm using fun i => exists_ne (0 : π i)
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Interval (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (α i)
s_1 : Finset ι
f : Π₀ (i : ι), α i
t_1 : (i : ι) → Finset (α i)
s : Finset ι
t : (i : ι) → Finset (α i)
⊢ Function.Injective (β := Π₀ (i : ι), α i) fun (f : (a : ι) → a ∈ s → α a) ↦
    DFinsupp.mk (β := α) s fun (i : (↑(↑s : Set ι) : Type u_1)) ↦ f (↑i : ι) ⋯
have refine : ∀ (f g : (a : ι) → a ∈ s → α a)
  (h :
    Eq (α := (i : (↑(↑s : Set ι) : Type u_1)) → α (↑i : ι)) (fun (i : (↑(↑s : Set ι) : Type u_1)) ↦ f (↑i : ι) sorry)
      fun (i : (↑(↑s : Set ι) : Type u_1)) ↦ g (↑i : ι) sorry),
  f = g
Tactic: refine (mk_injective _).comp fun f g h => ?_
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Interval (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (α i)
s_1 : Finset ι
f_1 : Π₀ (i : ι), α i
t_1 : (i : ι) → Finset (α i)
s : Finset ι
t : (i : ι) → Finset (α i)
f g : (a : ι) → a ∈ s → α a
h :
  Eq (α := (i : (↑(↑s : Set ι) : Type u_1)) → α (↑i : ι)) (fun (i : (↑(↑s : Set ι) : Type u_1)) ↦ f (↑i : ι) ⋯)
    fun (i : (↑(↑s : Set ι) : Type u_1)) ↦ g (↑i : ι) ⋯
⊢ f = g
have h₁ : ∀ (i : ι) (hi : i ∈ s), f i hi = g i hi
Tactic: ext i hi
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Interval (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
t : (i : ι) → Finset (α i)
inst_2 : (i : ι) → DecidableEq (α i)
⊢ Membership.mem (γ := Finset (Π₀ (i : ι), α i)) (s.dfinsupp (α := α) t) f ↔
    f.support (β := α) ⊆ s ∧ ∀ i ∈ s, (f : (a : ι) → α a) i ∈ t i
have refine_1 : (∃ a ∈ s.pi (β := α) t,
    ({
            toFun := fun (f : (a : ι) → a ∈ s → α a) ↦
              DFinsupp.mk (β := α) s fun (i : (↑(↑s : Set ι) : Type u_1)) ↦ f (↑i : ι) sorry,
            inj' := sorry } :
          (a : (a : ι) → a ∈ s → α a) → Π₀ (i : ι), α i)
        a =
      f) →
  f.support (β := α) ⊆ s ∧ ∀ i ∈ s, (f : (a : ι) → α a) i ∈ t i
Tactic: refine mem_map.trans ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Interval (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
t : (i : ι) → Finset (α i)
inst_2 : (i : ι) → DecidableEq (α i)
refine_1 :
  (∃ a ∈ s.pi (β := α) t,
      ({
              toFun := fun (f : (a : ι) → a ∈ s → α a) ↦
                DFinsupp.mk (β := α) s fun (i : (↑(↑s : Set ι) : Type u_1)) ↦ f (↑i : ι) ⋯,
              inj' := ⋯ } :
            (a : (a : ι) → a ∈ s → α a) → Π₀ (i : ι), α i)
          a =
        f) →
    f.support (β := α) ⊆ s ∧ ∀ i ∈ s, (f : (a : ι) → α a) i ∈ t i
⊢ Membership.mem (γ := Finset (Π₀ (i : ι), α i)) (s.dfinsupp (α := α) t) f ↔
    f.support (β := α) ⊆ s ∧ ∀ i ∈ s, (f : (a : ι) → α a) i ∈ t i
have refine_2 : (f.support (β := α) ⊆ s ∧ ∀ i ∈ s, (f : (a : ι) → α a) i ∈ t i) →
  ∃ a ∈ s.pi (β := α) t,
    ({
            toFun := fun (f : (a : ι) → a ∈ s → α a) ↦
              DFinsupp.mk (β := α) s fun (i : (↑(↑s : Set ι) : Type u_1)) ↦ f (↑i : ι) sorry,
            inj' := sorry } :
          (a : (a : ι) → a ∈ s → α a) → Π₀ (i : ι), α i)
        a =
      f
Tactic: refine mem_map.trans ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Interval (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (α i)
s : Finset ι
t : (i : ι) → Finset (α i)
inst_2 : (i : ι) → DecidableEq (α i)
f : (a : ι) → a ∈ s → α a
hf : f ∈ s.pi (β := α) t
⊢ support (β := α)
        (({
              toFun := fun (f : (a : ι) → a ∈ s → α a) ↦
                DFinsupp.mk (β := α) s fun (i : (↑(↑s : Set ι) : Type u_1)) ↦ f (↑i : ι) ⋯,
              inj' := ⋯ } :
            (a : (a : ι) → a ∈ s → α a) → Π₀ (i : ι), α i)
          f) ⊆
      s ∧
    ∀ i ∈ s,
      ((({
                    toFun := fun (f : (a : ι) → a ∈ s → α a) ↦
                      DFinsupp.mk (β := α) s fun (i : (↑(↑s : Set ι) : Type u_1)) ↦ f (↑i : ι) ⋯,
                    inj' := ⋯ : ((a : ι) → a ∈ s → α a) ↪ Π₀ (i : ι), α i } :
                  (a : (a : ι) → a ∈ s → α a) → Π₀ (i : ι), α i)
                f :
              Π₀ (i : ι), α i) :
            (a : ι) → α a)
          i ∈
        t i
have refine_1 : support (β := α) (DFinsupp.mk (β := α) s fun (i : (↑(↑s : Set ι) : Type u_1)) ↦ f (↑i : ι) sorry) ⊆ s ∧
  ∀ i ∈ s, (DFinsupp.mk (β := α) s fun (i : (↑(↑s : Set ι) : Type u_1)) ↦ f (↑i : ι) sorry : (a : ι) → α a) i ∈ t i
Tactic: rw [Function.Embedding.coeFn_mk]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Interval (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (α i)
s : Finset ι
t : (i : ι) → Finset (α i)
inst_2 : (i : ι) → DecidableEq (α i)
f : (a : ι) → a ∈ s → α a
hf : f ∈ s.pi (β := α) t
⊢ support (β := α) (DFinsupp.mk (β := α) s fun (i : (↑(↑s : Set ι) : Type u_1)) ↦ f (↑i : ι) ⋯) ⊆ s ∧
    ∀ i ∈ s, (DFinsupp.mk (β := α) s fun (i : (↑(↑s : Set ι) : Type u_1)) ↦ f (↑i : ι) ⋯ : (a : ι) → α a) i ∈ t i
have refine_1 : ∀ (i : ι) (hi : i ∈ s),
  (DFinsupp.mk (β := α) s fun (i : (↑(↑s : Set ι) : Type u_1)) ↦ f (↑i : ι) sorry : (a : ι) → α a) i ∈ t i
Tactic: refine ⟨support_mk_subset, fun i hi => ?_⟩
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Interval (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (α i)
s : Finset ι
t : (i : ι) → Finset (α i)
inst_2 : (i : ι) → DecidableEq (α i)
f : (a : ι) → a ∈ s → α a
hf : f ∈ s.pi (β := α) t
i : ι
hi : i ∈ s
⊢ (DFinsupp.mk (β := α) s fun (i : (↑(↑s : Set ι) : Type u_1)) ↦ f (↑i : ι) ⋯ : (a : ι) → α a) i ∈ t i
have h : (DFinsupp.mk (β := α) s fun (i : (↑(↑s : Set ι) : Type u_1)) ↦ f (↑i : ι) sorry : (a : ι) → α a) i = f i hi
Tactic: convert! mem_pi.1 hf i hi
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Interval (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
t : (i : ι) → Finset (α i)
inst_2 : (i : ι) → DecidableEq (α i)
⊢ (f.support (β := α) ⊆ s ∧ ∀ i ∈ s, (f : (a : ι) → α a) i ∈ t i) →
    ∃ a ∈ s.pi (β := α) t,
      ({
              toFun := fun (f : (a : ι) → a ∈ s → α a) ↦
                DFinsupp.mk (β := α) s fun (i : (↑(↑s : Set ι) : Type u_1)) ↦ f (↑i : ι) ⋯,
              inj' := ⋯ } :
            (a : (a : ι) → a ∈ s → α a) → Π₀ (i : ι), α i)
          a =
        f
have refine_2 : ∀ (h : f.support (β := α) ⊆ s ∧ ∀ i ∈ s, (f : (a : ι) → α a) i ∈ t i),
  (({
          toFun := fun (f : (a : ι) → a ∈ s → α a) ↦
            DFinsupp.mk (β := α) s fun (i : (↑(↑s : Set ι) : Type u_1)) ↦ f (↑i : ι) sorry,
          inj' := sorry } :
        (a : (a : ι) → a ∈ s → α a) → Π₀ (i : ι), α i)
      fun (i : ι) (x : i ∈ s) ↦ (f : (a : ι) → α a) i) =
    f
Tactic: refine fun h => ⟨fun i _ => f i, mem_pi.2 h.2, ?_⟩
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Interval (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
t : (i : ι) → Finset (α i)
inst_2 : (i : ι) → DecidableEq (α i)
h : f.support (β := α) ⊆ s ∧ ∀ i ∈ s, (f : (a : ι) → α a) i ∈ t i
⊢ (({
          toFun := fun (f : (a : ι) → a ∈ s → α a) ↦
            DFinsupp.mk (β := α) s fun (i : (↑(↑s : Set ι) : Type u_1)) ↦ f (↑i : ι) ⋯,
          inj' := ⋯ } :
        (a : (a : ι) → a ∈ s → α a) → Π₀ (i : ι), α i)
      fun (i : ι) (x : i ∈ s) ↦ (f : (a : ι) → α a) i) =
    f
have refine_2 : ∀ (i : ι),
  (({
              toFun := fun (f : (a : ι) → a ∈ s → α a) ↦
                DFinsupp.mk (β := α) s fun (i : (↑(↑s : Set ι) : Type u_1)) ↦ f (↑i : ι) sorry,
              inj' := sorry : ((a : ι) → a ∈ s → α a) ↪ Π₀ (i : ι), α i } :
            (a : (a : ι) → a ∈ s → α a) → Π₀ (i : ι), α i)
          fun (i : ι) (x : i ∈ s) ↦ (f : (a : ι) → α a) i :
        (a : ι) → α a)
      i =
    (f : (a : ι) → α a) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Interval (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
t : (i : ι) → Finset (α i)
inst_2 : (i : ι) → DecidableEq (α i)
h : f.support (β := α) ⊆ s ∧ ∀ i ∈ s, (f : (a : ι) → α a) i ∈ t i
i : ι
⊢ (({
              toFun := fun (f : (a : ι) → a ∈ s → α a) ↦
                DFinsupp.mk (β := α) s fun (i : (↑(↑s : Set ι) : Type u_1)) ↦ f (↑i : ι) ⋯,
              inj' := ⋯ : ((a : ι) → a ∈ s → α a) ↪ Π₀ (i : ι), α i } :
            (a : (a : ι) → a ∈ s → α a) → Π₀ (i : ι), α i)
          fun (i : ι) (x : i ∈ s) ↦ (f : (a : ι) → α a) i :
        (a : ι) → α a)
      i =
    (f : (a : ι) → α a) i
have refine_2 : (if i ∈ s then (f : (a : ι) → α a) i else 0) = (f : (a : ι) → α a) i
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Interval (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
inst_2 : (i : ι) → DecidableEq (α i)
t : Π₀ (i : ι), Finset (α i)
ht : t.support (β := fun (i : ι) ↦ Finset (α i)) ⊆ s
⊢ Membership.mem (γ := Finset (Π₀ (i : ι), α i)) (s.dfinsupp (α := α) (⇑t : (a : ι) → Finset (α a))) f ↔
    ∀ (i : ι), (f : (a : ι) → α a) i ∈ (t : (a : ι) → Finset (α a)) i
have refine_1 : ∀ (i : ι) (h : (i ∈ f.support (β := α) → i ∈ s) ∧ (i ∈ s → (f : (a : ι) → α a) i ∈ (t : (a : ι) → Finset (α a)) i)),
  (f : (a : ι) → α a) i ∈ (t : (a : ι) → Finset (α a)) i
Tactic: refine mem_dfinsupp_iff.trans (forall_and.symm.trans <| forall_congr' fun i =>
      ⟨ fun h => ?_,
        fun h => ⟨fun hi => ht <| mem_support_iff.2 fun H => mem_support_iff.1 hi ?_, fun _ => h⟩⟩)
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Interval (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
inst_2 : (i : ι) → DecidableEq (α i)
t : Π₀ (i : ι), Finset (α i)
ht : t.support (β := fun (i : ι) ↦ Finset (α i)) ⊆ s
refine_1 :
  ∀ (i : ι) (h : (i ∈ f.support (β := α) → i ∈ s) ∧ (i ∈ s → (f : (a : ι) → α a) i ∈ (t : (a : ι) → Finset (α a)) i)),
    (f : (a : ι) → α a) i ∈ (t : (a : ι) → Finset (α a)) i
⊢ Membership.mem (γ := Finset (Π₀ (i : ι), α i)) (s.dfinsupp (α := α) (⇑t : (a : ι) → Finset (α a))) f ↔
    ∀ (i : ι), (f : (a : ι) → α a) i ∈ (t : (a : ι) → Finset (α a)) i
have refine_2 : ∀ (i : ι) (h : (f : (a : ι) → α a) i ∈ (t : (a : ι) → Finset (α a)) i) (hi : i ∈ f.support (β := α))
  (H : (t : (a : ι) → Finset (α a)) i = 0), (f : (a : ι) → α a) i = 0
Tactic: refine mem_dfinsupp_iff.trans (forall_and.symm.trans <| forall_congr' fun i =>
      ⟨ fun h => ?_,
        fun h => ⟨fun hi => ht <| mem_support_iff.2 fun H => mem_support_iff.1 hi ?_, fun _ => h⟩⟩)
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Interval (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
inst_2 : (i : ι) → DecidableEq (α i)
t : Π₀ (i : ι), Finset (α i)
ht : t.support (β := fun (i : ι) ↦ Finset (α i)) ⊆ s
i : ι
h : (i ∈ f.support (β := α) → i ∈ s) ∧ (i ∈ s → (f : (a : ι) → α a) i ∈ (t : (a : ι) → Finset (α a)) i)
⊢ (f : (a : ι) → α a) i ∈ (t : (a : ι) → Finset (α a)) i
have pos : ∀ (hi : i ∈ s), (f : (a : ι) → α a) i ∈ (t : (a : ι) → Finset (α a)) i
Tactic: by_cases hi : i ∈ s
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Interval (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
inst_2 : (i : ι) → DecidableEq (α i)
t : Π₀ (i : ι), Finset (α i)
ht : t.support (β := fun (i : ι) ↦ Finset (α i)) ⊆ s
i : ι
h : (i ∈ f.support (β := α) → i ∈ s) ∧ (i ∈ s → (f : (a : ι) → α a) i ∈ (t : (a : ι) → Finset (α a)) i)
pos : ∀ (hi : i ∈ s), (f : (a : ι) → α a) i ∈ (t : (a : ι) → Finset (α a)) i
⊢ (f : (a : ι) → α a) i ∈ (t : (a : ι) → Finset (α a)) i
have neg : ∀ (hi : i ∉ s), (f : (a : ι) → α a) i ∈ (t : (a : ι) → Finset (α a)) i
Tactic: by_cases hi : i ∈ s
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Interval (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
inst_2 : (i : ι) → DecidableEq (α i)
t : Π₀ (i : ι), Finset (α i)
ht : t.support (β := fun (i : ι) ↦ Finset (α i)) ⊆ s
i : ι
h : (i ∈ f.support (β := α) → i ∈ s) ∧ (i ∈ s → (f : (a : ι) → α a) i ∈ (t : (a : ι) → Finset (α a)) i)
hi : i ∉ s
⊢ (f : (a : ι) → α a) i ∈ (t : (a : ι) → Finset (α a)) i
have neg : Membership.mem (γ := Finset (α i)) 0 0
Tactic: rw [notMem_support_iff.1 (mt h.1 hi), notMem_support_iff.1 (notMem_mono ht hi)]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Interval (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
inst_2 : (i : ι) → DecidableEq (α i)
t : Π₀ (i : ι), Finset (α i)
ht : t.support (β := fun (i : ι) ↦ Finset (α i)) ⊆ s
i : ι
h : (f : (a : ι) → α a) i ∈ (t : (a : ι) → Finset (α a)) i
hi : i ∈ f.support (β := α)
H : (t : (a : ι) → Finset (α a)) i = 0
⊢ (f : (a : ι) → α a) i = 0
have refine_2 : ∀ (h : Membership.mem (γ := Finset (α i)) 0 ((f : (a : ι) → α a) i)) (hi : i ∈ f.support (β := α))
  (H : (t : (a : ι) → Finset (α a)) i = 0), (f : (a : ι) → α a) i = 0
Tactic: rwa [H, mem_zero] at h
Cleared hypotheses: h, hi, H