awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.DFinsupp.Defs
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 : ι) ↦ id) ⋯ x = x

Tactic:
simp
-- Module: Mathlib.Data.DFinsupp.Defs
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
h : ∀ (i : ι), Eq.{v₂ + 1} (α := β₂ i) (id 0) 0
⊢ ∀ (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:
simp_rw [AddEquiv.self_comp_symm]

Premises used: AddEquiv.self_comp_symm
-- Module: Mathlib.Data.DFinsupp.Defs
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) (id 0) 0

Tactic:
simp
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β₁ : ι → Type v₁
inst : (i : ι) → AddZeroClass (β₁ i)
⊢ Eq (α := (Π₀ (i : ι), β₁ i) ≃+ Π₀ (i : ι), β₁ i) (addEquiv (β₁ := β₁) (β₂ := β₁) fun (i : ι) ↦ AddEquiv.refl (β₁ i))
    (AddEquiv.refl (Π₀ (i : ι), β₁ i))

Tactic:
AddEquiv.ext mapRange_id

Premises used: AddEquiv.ext, DFinsupp.mapRange_id, rfl
-- Module: Mathlib.Data.DFinsupp.Defs
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)
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
⊢ (addEquiv (β₁ := β) (β₂ := β₂) fun (i : ι) ↦ (f i).trans (f₂ i)) =
    (addEquiv (β₁ := β) (β₂ := β₁) f).trans (addEquiv (β₁ := β₁) (β₂ := β₂) f₂)

Tactic:
ext
-- Module: Mathlib.Data.DFinsupp.Defs
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)
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:
simp
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → AddZeroClass (β₁ i)
inst_1 : (i : ι) → AddZeroClass (β₂ i)
e : (i : ι) → AddEquiv.{v₁, v₂} (β₁ i) (β₂ i)
⊢ (addEquiv (β₁ := β₁) (β₂ := β₂) e).symm = addEquiv (β₁ := β₂) (β₂ := β₁) fun (i : ι) ↦ (e i).symm

Tactic:
rfl

Premises used: DFinsupp.mapRange, DFinsupp.mapRange.addEquiv, Equiv.symm, rfl, AddEquiv.symm
-- Module: Mathlib.Data.DFinsupp.Encodable
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : Countable ι
inst_2 : ∀ (i : ι), Countable.{u_2 + 1} (α i)
x : Encodable ι := Encodable.ofCountable ι
x_1 : (i : ι) → Encodable (α i) := fun (i : ι) ↦ Encodable.ofCountable (α i)
⊢ Countable (Π₀ (i : ι), α i)

Tactic:
infer_instance
-- Module: Mathlib.Data.DFinsupp.Encodable
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : Countable ι
inst_2 : ∀ (i : ι), Countable.{u_2 + 1} (α i)
let let₁ let₂ let₃ : Countable (Π₀ (i : ι), α i)
⊢ Countable (Π₀ (i : ι), α i)

Tactic:
classical
    let _ := Encodable.ofCountable ι
    let _ := fun i ↦ Encodable.ofCountable (α i)
    infer_instance
-- Module: Mathlib.Data.DFinsupp.Ext
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
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)
⊢ Membership.mem (γ := AddSubmonoid (Π₀ (i : ι), β i)) (AddSubmonoid.closure (⋃ (i : ι), Set.range (single (β := β) i)))
    x

Tactic:
apply DFinsupp.induction x

Premises used: DFinsupp.induction
-- Module: Mathlib.Data.DFinsupp.Ext
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)))
    0

Tactic:
AddSubmonoid.zero_mem _

Premises used: AddSubmonoid.zero_mem, Set.Mem
-- Module: Mathlib.Data.DFinsupp.Ext
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)))
    0

Tactic:
exact AddSubmonoid.zero_mem _

Premises used: AddSubmonoid.zero_mem
-- Module: Mathlib.Data.DFinsupp.Ext
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
x : Π₀ (i : ι), β i
h : Membership.mem (γ := AddSubmonoid (Π₀ (i : ι), β i)) ⊤ x
⊢ ∀ (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:
fun a b f _ _ hf =>
      AddSubmonoid.add_mem _
        (AddSubmonoid.subset_closure <| Set.mem_iUnion.2 ⟨a, Set.mem_range_self _⟩) hf

Premises used: AddSubmonoid.add_mem, Set.mem_range_self, Iff.mpr, Set.Mem, DFinsupp.single, Set.mem_iUnion, AddSubmonoid.subset_closure, AddSubmonoid.closure, Exists.intro, Set.range, Set.iUnion
-- Module: Mathlib.Data.DFinsupp.Ext
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
x : Π₀ (i : ι), β i
h : Membership.mem (γ := AddSubmonoid (Π₀ (i : ι), β i)) ⊤ x
⊢ ∀ (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:
exact fun a b f _ _ hf =>
      AddSubmonoid.add_mem _
        (AddSubmonoid.subset_closure <| Set.mem_iUnion.2 ⟨a, Set.mem_range_self _⟩) hf

Premises used: AddSubmonoid.add_mem, Set.mem_range_self, Iff.mpr, Set.mem_iUnion, AddSubmonoid.subset_closure, AddSubmonoid.closure, Exists.intro, Set.range, Set.iUnion
-- Module: Mathlib.Data.DFinsupp.Ext
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

Tactic:
AddMonoidHom.eq_of_eqOn_denseM add_closure_iUnion_range_single fun f hf => ?_

Premises used: AddMonoidHom.eq_of_eqOn_denseM, DFinsupp.add_closure_iUnion_range_single
-- Module: Mathlib.Data.DFinsupp.Ext
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) : γ)
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 : γ)
⊢ f = g

Tactic:
refine AddMonoidHom.eq_of_eqOn_denseM add_closure_iUnion_range_single fun f hf => ?_

Premises used: AddMonoidHom.eq_of_eqOn_denseM, DFinsupp.add_closure_iUnion_range_single
-- Module: Mathlib.Data.DFinsupp.Ext
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
⊢ ∃ (i : ι) (y : β i), single (β := β) i y = f

Tactic:
simp only [Set.mem_iUnion, Set.mem_range] at hf

Premises used: Set.mem_range, Set.mem_iUnion
-- Module: Mathlib.Data.DFinsupp.Ext
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 : ∃ (i : ι) (y : β i), single (β := β) i y = f
rcases :
  ∀ (x : ι) (y : β x),
    Eq.{w + 1} (α := γ) ((f_1 : (a : Π₀ (i : ι), β i) → γ) (single (β := β) x y) : γ)
      ((g : (a : Π₀ (i : ι), β i) → γ) (single (β := β) x y) : γ)
⊢ Eq.{w + 1} (α := γ) ((f_1 : (a : Π₀ (i : ι), β i) → γ) f : γ) ((g : (a : Π₀ (i : ι), β i) → γ) f : γ)

Tactic:
rcases hf with ⟨x, y, rfl⟩

Premises used: rfl
-- Module: Mathlib.Data.DFinsupp.Ext
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) : γ)
x : ι
y : β x
⊢ Eq.{w + 1} (α := γ) ((f : (a : Π₀ (i : ι), β i) → γ) (single (β := β) x y) : γ)
    ((g : (a : Π₀ (i : ι), β i) → γ) (single (β := β) x y) : γ)

Tactic:
apply H
-- Module: Mathlib.Data.DFinsupp.Ext
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
γ : Type w
inst_2 : AddZeroClass γ
f g : (Π₀ (i : ι), β i) →+ γ
H : ∀ (x : ι), f.comp (singleAddHom β x) = g.comp (singleAddHom β x)
⊢ f = g

Tactic:
addHom_ext fun x => DFunLike.congr_fun (H x)

Premises used: DFunLike.congr_fun, DFinsupp.addHom_ext
-- Module: Mathlib.Data.DFinsupp.FiniteInfinite
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 ι
choose : ∀ (m : (i : ι) → π i) (hm : ∀ (i : ι), m i ≠ 0), Infinite (Π₀ (i : ι), π i)
⊢ Infinite (Π₀ (i : ι), π i)

Tactic:
choose m hm using fun i => exists_ne (0 : π i)

Premises used: exists_ne, OfNat.ofNat
-- Module: Mathlib.Data.DFinsupp.FiniteInfinite
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 ι
m : (i : ι) → π i
hm : ∀ (i : ι), m i ≠ 0
⊢ Infinite (Π₀ (i : ι), π i)

Tactic:
Infinite.of_injective _ (DFinsupp.single_left_injective hm)

Premises used: Infinite.of_injective, DFinsupp.single_left_injective
-- Module: Mathlib.Data.DFinsupp.FiniteInfinite
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 ι
m : (i : ι) → π i
hm : ∀ (i : ι), m i ≠ 0
⊢ Infinite (Π₀ (i : ι), π i)

Tactic:
exact Infinite.of_injective _ (DFinsupp.single_left_injective hm)

Premises used: Infinite.of_injective, DFinsupp.single_left_injective
-- Module: Mathlib.Data.DFinsupp.FiniteInfinite
Goal:
ι : Type u_1
π : ι → Type u_2
i : ι
inst : Infinite.{u_2 + 1} (π i)
inst_1 : (i : ι) → Zero (π i)
⊢ Infinite (Π₀ (i : ι), π i)

Tactic:
letI := Classical.decEq ι
  Infinite.of_injective (fun j => DFinsupp.single i j) DFinsupp.single_injective

Premises used: Infinite.of_injective, DFinsupp.single, DFinsupp.single_injective
-- Module: Mathlib.Data.DFinsupp.FiniteInfinite
Goal:
ι_1 : Type u
γ : Type w
β : ι_1 → Type v
β₁ : ι_1 → Type v₁
β₂ : ι_1 → Type v₂
ι : Type u_1
π : ι → Type u_2
inst : ∀ (i : ι), Infinite.{u_2 + 1} (π i)
inst_1 : (i : ι) → Zero (π i)
inst_2 : Nonempty ι
⊢ Infinite (Π₀ (i : ι), π i)

Tactic:
DFinsupp.infinite_of_exists_right (Classical.arbitrary ι)

Premises used: DFinsupp.infinite_of_exists_right, Classical.arbitrary
-- Module: Mathlib.Data.DFinsupp.Interval
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 : ι) ⋯

Tactic:
(mk_injective _).comp fun f g h => ?_

Premises used: DFinsupp.mk, DFinsupp.mk_injective, Function.Injective.comp
-- Module: Mathlib.Data.DFinsupp.Interval
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)
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 : ι) ⋯)
        fun (i : (↑(↑s : Set ι) : Type u_1)) ↦ g (↑i : ι) ⋯),
    f = g
⊢ Function.Injective (β := Π₀ (i : ι), α i) fun (f : (a : ι) → a ∈ s → α a) ↦
    DFinsupp.mk (β := α) s fun (i : (↑(↑s : Set ι) : Type u_1)) ↦ f (↑i : ι) ⋯

Tactic:
refine (mk_injective _).comp fun f g h => ?_

Premises used: DFinsupp.mk_injective, Function.Injective.comp
-- Module: Mathlib.Data.DFinsupp.Interval
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 : ι) ⋯
h₁ : ∀ (i : ι) (hi : i ∈ s), f i hi = g i hi
⊢ f = g

Tactic:
ext i hi
-- Module: Mathlib.Data.DFinsupp.Interval
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 : ι) ⋯
i : ι
hi : i ∈ s
⊢ f (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i hi) : ι) ⋯ =
    g (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i hi) : ι) ⋯

Tactic:
congr_fun h ⟨i, hi⟩

Premises used: Subtype.mk, congr_fun
-- Module: Mathlib.Data.DFinsupp.Interval
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 : ι) ⋯
i : ι
hi : i ∈ s
⊢ f i hi = g i hi

Tactic:
convert! congr_fun h ⟨i, hi⟩

Premises used: Subtype.mk, congr_fun
-- Module: Mathlib.Data.DFinsupp.Interval
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (α i)
s : Finset ι
t : (i : ι) → Finset (α i)
⊢ card (α := Π₀ (i : ι), α i) (s.dfinsupp (α := α) t) = ∏ i ∈ s, #(t i)

Tactic:
(card_map _).trans <| card_pi _ _

Premises used: Finset.card_pi, Finset.card_map, Finset.dfinsupp, Eq.trans
-- Module: Mathlib.Data.DFinsupp.Interval
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

Tactic:
mem_map.trans ⟨?_, ?_⟩

Premises used: Set.Mem, setOf, Iff.intro, Iff.trans, Finset.mem_map
-- Module: Mathlib.Data.DFinsupp.Interval
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
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 : ι) ⋯,
              inj' := ⋯ } :
            (a : (a : ι) → a ∈ s → α a) → Π₀ (i : ι), α i)
          a =
        f
⊢ Membership.mem (γ := Finset (Π₀ (i : ι), α i)) (s.dfinsupp (α := α) t) f ↔
    f.support (β := α) ⊆ s ∧ ∀ i ∈ s, (f : (a : ι) → α a) i ∈ t i

Tactic:
refine mem_map.trans ⟨?_, ?_⟩

Premises used: Iff.intro, Iff.trans, Finset.mem_map
-- Module: Mathlib.Data.DFinsupp.Interval
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
refine_1 :
  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
⊢ 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

Tactic:
rw [Function.Embedding.coeFn_mk]

Premises used: Function.Embedding.coeFn_mk
-- Module: Mathlib.Data.DFinsupp.Interval
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

Tactic:
⟨support_mk_subset, fun i hi => ?_⟩

Premises used: DFinsupp.support_mk_subset, And.intro
-- Module: Mathlib.Data.DFinsupp.Interval
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
refine_1 :
  ∀ (i : ι) (hi : i ∈ s),
    (DFinsupp.mk (β := α) s fun (i : (↑(↑s : Set ι) : Type u_1)) ↦ f (↑i : ι) ⋯ : (a : ι) → α a) i ∈ t i
⊢ 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

Tactic:
refine ⟨support_mk_subset, fun i hi => ?_⟩
-- Module: Mathlib.Data.DFinsupp.Interval
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
⊢ f i hi ∈ t i

Tactic:
mem_pi.1 hf i hi

Premises used: Finset.mem_pi, Iff.mp
-- Module: Mathlib.Data.DFinsupp.Interval
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
h : (DFinsupp.mk (β := α) s fun (i : (↑(↑s : Set ι) : Type u_1)) ↦ f (↑i : ι) ⋯ : (a : ι) → α a) i = f i hi
⊢ (DFinsupp.mk (β := α) s fun (i : (↑(↑s : Set ι) : Type u_1)) ↦ f (↑i : ι) ⋯ : (a : ι) → α a) i ∈ t i

Tactic:
convert! mem_pi.1 hf i hi

Premises used: Finset.mem_pi, Iff.mp
-- Module: Mathlib.Data.DFinsupp.Interval
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 = f i hi

Tactic:
mk_of_mem hi

Premises used: DFinsupp.mk_of_mem
-- Module: Mathlib.Data.DFinsupp.Interval
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 = f i hi

Tactic:
exact mk_of_mem hi

Premises used: DFinsupp.mk_of_mem
-- Module: Mathlib.Data.DFinsupp.Interval
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

Tactic:
fun h => ⟨fun i _ => f i, mem_pi.2 h.2, ?_⟩

Premises used: Iff.mpr, And.right, And.intro, Finset.mem_pi, Exists.intro, DFunLike.coe