awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
α : Type u_5
s : Set α
n : ℕ
ih :
  HSMul.hSMul (β := Set (α →₀ ℕ)) n ((fun (x : α) ↦ single x 1) '' s) =
    {x : α →₀ ℕ | (degree : (a : α →₀ ℕ) → ℕ) x = n ∧ (↑x.support : Set α) ⊆ s}
f : α →₀ ℕ
h : Membership.mem (γ := Set (α →₀ ℕ)) {x : α →₀ ℕ | (degree : (a : α →₀ ℕ) → ℕ) x = n + 1 ∧ (↑x.support : Set α) ⊆ s} f
f_deg : (degree : (a : α →₀ ℕ) → ℕ) f = n + 1
f_supp : (↑f.support : Set α) ⊆ s
i : α
hi : i ∈ f.support
x : α →₀ ℕ
hx : f = x + single i 1
⊢ i ∈ (↑f.support : Set α)

Tactic:
simp_all
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
α : Type u_5
s : Set α
n : ℕ
ih :
  HSMul.hSMul (β := Set (α →₀ ℕ)) n ((fun (x : α) ↦ single x 1) '' s) =
    {x : α →₀ ℕ | (degree : (a : α →₀ ℕ) → ℕ) x = n ∧ (↑x.support : Set α) ⊆ s}
f : α →₀ ℕ
h : Membership.mem (γ := Set (α →₀ ℕ)) {x : α →₀ ℕ | (degree : (a : α →₀ ℕ) → ℕ) x = n + 1 ∧ (↑x.support : Set α) ⊆ s} f
f_deg : (degree : (a : α →₀ ℕ) → ℕ) f = n + 1
f_supp : (↑f.support : Set α) ⊆ s
i : α
hi : i ∈ f.support
x : α →₀ ℕ
hx : f = x + single i 1
⊢ f ∈
    HAdd.hAdd (α := Set (α →₀ ℕ)) {x : α →₀ ℕ | (degree : (a : α →₀ ℕ) → ℕ) x = n ∧ (↑x.support : Set α) ⊆ s}
      ((fun (x : α) ↦ single x 1) '' s)

Tactic:
exact ⟨x, by aesop (add simp Set.subset_def), _, ⟨_, f_supp (by simp_all), rfl⟩, hx.symm⟩
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
α : Type u_5
n : ℕ
s : Set α
zero :
  HSMul.hSMul (α := ℕ) (β := Set (α →₀ ℕ)) 0 ((fun (x : α) ↦ single x 1) '' s) =
    {x : α →₀ ℕ | Eq (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) x : ℕ) (0 : ℕ) ∧ (↑x.support : Set α) ⊆ s}
succ :
  ∀ (n : ℕ)
    (ih :
      HSMul.hSMul (β := Set (α →₀ ℕ)) n ((fun (x : α) ↦ single x 1) '' s) =
        {x : α →₀ ℕ | (degree : (a : α →₀ ℕ) → ℕ) x = n ∧ (↑x.support : Set α) ⊆ s}),
    HSMul.hSMul (β := Set (α →₀ ℕ)) (n + 1) ((fun (x : α) ↦ single x 1) '' s) =
      {x : α →₀ ℕ | (degree : (a : α →₀ ℕ) → ℕ) x = n + 1 ∧ (↑x.support : Set α) ⊆ s}
⊢ HSMul.hSMul (β := Set (α →₀ ℕ)) n ((fun (x : α) ↦ single x 1) '' s) =
    {x : α →₀ ℕ | (degree : (a : α →₀ ℕ) → ℕ) x = n ∧ (↑x.support : Set α) ⊆ s}

Tactic:
induction n with
  | zero => aesop (add simp degree_eq_zero_iff)
  | succ n ih =>
    rw [succ_nsmul, ih]
    refine subset_antisymm ?_ fun f ⟨f_deg, f_supp⟩ ↦ ?_
    · simp [Set.subset_def, Set.mem_add, @forall_comm (α →₀ ℕ)]; grind
    obtain ⟨i, hi⟩ : f.support.Nonempty := by aesop
    obtain ⟨x, hx⟩ := le_iff_exists_add'.mp
      (show single i 1 ≤ f by simpa [Nat.one_le_iff_ne_zero] using hi)
    exact ⟨x, by aesop (add simp Set.subset_def), _, ⟨_, f_supp (by simp_all), rfl⟩, hx.symm⟩

Premises used: Set.subset_def, forall_comm, subset_antisymm, Finsupp.degree_eq_zero_iff, Set.mem_add, succ_nsmul
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
α : Type u_5
n : ℕ
s : Set α
zero :
  HSMul.hSMul (α := ℕ) (β := Set (α →₀ ℕ)) 0 ((fun (x : α) ↦ single x 1) '' s) =
    {x : α →₀ ℕ | Eq (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) x : ℕ) (0 : ℕ) ∧ (↑x.support : Set α) ⊆ s}
succ :
  ∀ (n : ℕ)
    (ih :
      HSMul.hSMul (β := Set (α →₀ ℕ)) n ((fun (x : α) ↦ single x 1) '' s) =
        {x : α →₀ ℕ | (degree : (a : α →₀ ℕ) → ℕ) x = n ∧ (↑x.support : Set α) ⊆ s}),
    HSMul.hSMul (β := Set (α →₀ ℕ)) (n + 1) ((fun (x : α) ↦ single x 1) '' s) =
      {x : α →₀ ℕ | (degree : (a : α →₀ ℕ) → ℕ) x = n + 1 ∧ (↑x.support : Set α) ⊆ s}
⊢ HSMul.hSMul (β := Set (α →₀ ℕ)) n ((fun (x : α) ↦ single x 1) '' s) =
    {x : α →₀ ℕ | (degree : (a : α →₀ ℕ) → ℕ) x = n ∧ (↑x.support : Set α) ⊆ s}

Tactic:
classical
  induction n with
  | zero => aesop (add simp degree_eq_zero_iff)
  | succ n ih =>
    rw [succ_nsmul, ih]
    refine subset_antisymm ?_ fun f ⟨f_deg, f_supp⟩ ↦ ?_
    · simp [Set.subset_def, Set.mem_add, @forall_comm (α →₀ ℕ)]; grind
    obtain ⟨i, hi⟩ : f.support.Nonempty := by aesop
    obtain ⟨x, hx⟩ := le_iff_exists_add'.mp
      (show single i 1 ≤ f by simpa [Nat.one_le_iff_ne_zero] using hi)
    exact ⟨x, by aesop (add simp Set.subset_def), _, ⟨_, f_supp (by simp_all), rfl⟩, hx.symm⟩

Premises used: Set.subset_def, forall_comm, subset_antisymm, Finsupp.degree_eq_zero_iff, Set.mem_add, succ_nsmul
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
α : Type u_5
β : Type u_6
inst : CommMonoid β
f : α → β
n : ℕ
s : Set α
this :
  ∀ (s : Set (α →₀ ℕ)),
    HPow.hPow (α := Set β) ((fun (x : α →₀ ℕ) ↦ x.prod fun (x1 : α) (x2 : ℕ) ↦ f x1 ^ x2) '' s) n =
      (fun (x : α →₀ ℕ) ↦ x.prod fun (x1 : α) (x2 : ℕ) ↦ f x1 ^ x2) '' (n • s)
⊢ (f '' s) ^ n =
    (fun (x : α →₀ ℕ) ↦ x.prod fun (x1 : α) (x2 : ℕ) ↦ f x1 ^ x2) ''
      {x : α →₀ ℕ | (degree : (a : α →₀ ℕ) → ℕ) x = n ∧ (↑x.support : Set α) ⊆ s}

Tactic:
simp [← nsmul_single_one_image, ← this, Set.image_image]

Premises used: Set.image_image, Finsupp.nsmul_single_one_image
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
α : Type u_5
β : Type u_6
inst : CommMonoid β
f : α → β
n : ℕ
s : Set α
suffices :
  ∀ (s : Set (α →₀ ℕ)),
    HPow.hPow (α := Set β) ((fun (x : α →₀ ℕ) ↦ x.prod fun (x1 : α) (x2 : ℕ) ↦ f x1 ^ x2) '' s) n =
      (fun (x : α →₀ ℕ) ↦ x.prod fun (x1 : α) (x2 : ℕ) ↦ f x1 ^ x2) '' (n • s)
⊢ (f '' s) ^ n =
    (fun (x : α →₀ ℕ) ↦ x.prod fun (x1 : α) (x2 : ℕ) ↦ f x1 ^ x2) ''
      {x : α →₀ ℕ | (degree : (a : α →₀ ℕ) → ℕ) x = n ∧ (↑x.support : Set α) ⊆ s}

Tactic:
suffices ∀ (s : Set (α →₀ ℕ)), ((·.prod (f · ^ ·)) '' s) ^ n = (·.prod (f · ^ ·)) '' (n • s) by
    simp [← nsmul_single_one_image, ← this, Set.image_image]
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
α : Type u_5
β : Type u_6
inst : CommMonoid β
f : α → β
n : ℕ
s_1 : Set α
s : Set (α →₀ ℕ)
⊢ Eq.{u_6 + 1} (α := β)
    (Function.comp (α := Multiplicative (α →₀ ℕ)) (fun (x : α →₀ ℕ) ↦ x.prod fun (x1 : α) (x2 : ℕ) ↦ f x1 ^ x2)
      (⇑Multiplicative.toAdd : (a : Multiplicative (α →₀ ℕ)) → α →₀ ℕ) 1)
    1

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
α : Type u_5
β : Type u_6
inst : CommMonoid β
f : α → β
n : ℕ
s_1 : Set α
s : Set (α →₀ ℕ)
⊢ ∀ (x y : Multiplicative (α →₀ ℕ)),
    OneHom.toFun
        {
          toFun :=
            (fun (x : α →₀ ℕ) ↦ x.prod fun (x1 : α) (x2 : ℕ) ↦ f x1 ^ x2) ∘
              (⇑Multiplicative.toAdd : (a : Multiplicative (α →₀ ℕ)) → α →₀ ℕ),
          map_one' := ⋯ }
        (x * y) =
      HMul.hMul (α := β)
        (OneHom.toFun
          {
            toFun :=
              (fun (x : α →₀ ℕ) ↦ x.prod fun (x1 : α) (x2 : ℕ) ↦ f x1 ^ x2) ∘
                (⇑Multiplicative.toAdd : (a : Multiplicative (α →₀ ℕ)) → α →₀ ℕ),
            map_one' := ⋯ : OneHom.{u_5, u_6} (Multiplicative (α →₀ ℕ)) β }
          x)
        (OneHom.toFun
          {
            toFun :=
              (fun (x : α →₀ ℕ) ↦ x.prod fun (x1 : α) (x2 : ℕ) ↦ f x1 ^ x2) ∘
                (⇑Multiplicative.toAdd : (a : Multiplicative (α →₀ ℕ)) → α →₀ ℕ),
            map_one' := ⋯ : OneHom.{u_5, u_6} (Multiplicative (α →₀ ℕ)) β }
          y)

Tactic:
simp [Finsupp.prod_add_index, pow_add]

Premises used: Finsupp.prod_add_index, pow_add
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
α : Type u_5
β : Type u_6
inst : CommMonoid β
f : α → β
n : ℕ
s_1 : Set α
s : Set (α →₀ ℕ)
refine :
  Eq.{u_6 + 1} (α := Set β)
    ((⇑{
            toFun :=
              (fun (x : α →₀ ℕ) ↦ x.prod fun (x1 : α) (x2 : ℕ) ↦ f x1 ^ x2) ∘
                (⇑Multiplicative.toAdd : (a : Multiplicative (α →₀ ℕ)) → α →₀ ℕ),
            map_one' := ⋯, map_mul' := ⋯ } :
        (a : Multiplicative (α →₀ ℕ)) → β) ''
      s ^ n)
    ((fun (x : α →₀ ℕ) ↦ x.prod fun (x1 : α) (x2 : ℕ) ↦ f x1 ^ x2) '' (n • s))
⊢ HPow.hPow (α := Set β) ((fun (x : α →₀ ℕ) ↦ x.prod fun (x1 : α) (x2 : ℕ) ↦ f x1 ^ x2) '' s) n =
    (fun (x : α →₀ ℕ) ↦ x.prod fun (x1 : α) (x2 : ℕ) ↦ f x1 ^ x2) '' (n • s)

Tactic:
refine (Set.image_pow (⟨⟨(·.prod (f · ^ ·)) ∘ Multiplicative.toAdd, by simp⟩,
    by simp [Finsupp.prod_add_index, pow_add]⟩ : Multiplicative (α →₀ ℕ) →* β) _ _).symm.trans ?_

Premises used: OneHom.mk, Function.comp, MonoidHom.mk, Multiplicative.toAdd, Eq.symm, DFunLike.coe, Set.image_pow, Eq.trans
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
α : Type u_5
β : Type u_6
inst : CommMonoid β
f : α → β
n : ℕ
s_1 : Set α
s : Set (α →₀ ℕ)
⊢ Eq.{u_6 + 1} (α := Set β)
    ((⇑{
            toFun :=
              (fun (x : α →₀ ℕ) ↦ x.prod fun (x1 : α) (x2 : ℕ) ↦ f x1 ^ x2) ∘
                (⇑Multiplicative.toAdd : (a : Multiplicative (α →₀ ℕ)) → α →₀ ℕ),
            map_one' := ⋯, map_mul' := ⋯ } :
        (a : Multiplicative (α →₀ ℕ)) → β) ''
      s ^ n)
    ((fun (x : α →₀ ℕ) ↦ x.prod fun (x1 : α) (x2 : ℕ) ↦ f x1 ^ x2) '' (n • s))

Tactic:
simp [-Function.comp_apply, Set.image_comp, show Multiplicative.toAdd '' s = s from
    Set.image_id _]

Premises used: Set.image_comp, Function.comp_apply, Set.image_id
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
α : Type u_5
β : Type u_6
inst : CommMonoid β
f : α → β
n : ℕ
s : Set α
suffices suffices₁ suffices₂ suffices₃ :
  ∀ (s : Set (α →₀ ℕ)),
    HPow.hPow (α := Set β) ((fun (x : α →₀ ℕ) ↦ x.prod fun (x1 : α) (x2 : ℕ) ↦ f x1 ^ x2) '' s) n =
      (fun (x : α →₀ ℕ) ↦ x.prod fun (x1 : α) (x2 : ℕ) ↦ f x1 ^ x2) '' (n • s)
suffices₄ :
  ∀ (s : Set (α →₀ ℕ)),
    Eq.{u_6 + 1} (α := Set β)
      ((⇑{
              toFun :=
                (fun (x : α →₀ ℕ) ↦ x.prod fun (x1 : α) (x2 : ℕ) ↦ f x1 ^ x2) ∘
                  (⇑Multiplicative.toAdd : (a : Multiplicative (α →₀ ℕ)) → α →₀ ℕ),
              map_one' := ⋯, map_mul' := ⋯ } :
          (a : Multiplicative (α →₀ ℕ)) → β) ''
        s ^ n)
      ((fun (x : α →₀ ℕ) ↦ x.prod fun (x1 : α) (x2 : ℕ) ↦ f x1 ^ x2) '' (n • s))
⊢ (f '' s) ^ n =
    (fun (x : α →₀ ℕ) ↦ x.prod fun (x1 : α) (x2 : ℕ) ↦ f x1 ^ x2) ''
      {x : α →₀ ℕ | (degree : (a : α →₀ ℕ) → ℕ) x = n ∧ (↑x.support : Set α) ⊆ s}

Tactic:
classical
  suffices ∀ (s : Set (α →₀ ℕ)), ((·.prod (f · ^ ·)) '' s) ^ n = (·.prod (f · ^ ·)) '' (n • s) by
    simp [← nsmul_single_one_image, ← this, Set.image_image]
  intro s
  refine (Set.image_pow (⟨⟨(·.prod (f · ^ ·)) ∘ Multiplicative.toAdd, by simp⟩,
    by simp [Finsupp.prod_add_index, pow_add]⟩ : Multiplicative (α →₀ ℕ) →* β) _ _).symm.trans ?_
  simp [-Function.comp_apply, Set.image_comp, show Multiplicative.toAdd '' s = s from
    Set.image_id _]

Premises used: OneHom.mk, Function.comp, MonoidHom.mk, Set.image_comp, Multiplicative.toAdd, Function.comp_apply, Eq.symm, Set.image_id, DFunLike.coe, Set.image_pow, Eq.trans
-- Module: Mathlib.Data.Finsupp.WellFounded
Goal:
α : Type u_1
N : Type u_2
inst : Zero N
r : α → α → Prop
s : N → N → Prop
hbot : ∀ ⦃n : N⦄, ¬s n 0
hs : WellFounded s
x : α →₀ N
h : ∀ a ∈ x.support, Acc (rᶜ ⊓ fun (x1 x2 : α) ↦ x1 ≠ x2) a
rw : Acc (InvImage (DFinsupp.Lex (α := fun (x : α) ↦ N) r fun (x : α) ↦ s) toDFinsupp) x
⊢ Acc (Finsupp.Lex r s) x

Tactic:
rw [lex_eq_invImage_dfinsupp_lex]

Premises used: Finsupp.lex_eq_invImage_dfinsupp_lex
-- Module: Mathlib.Data.Finsupp.WellFounded
Goal:
α : Type u_1
N : Type u_2
inst : Zero N
r : α → α → Prop
s : N → N → Prop
hbot : ∀ ⦃n : N⦄, ¬s n 0
hs : WellFounded s
x : α →₀ N
h : ∀ a ∈ x.support, Acc (rᶜ ⊓ fun (x1 x2 : α) ↦ x1 ≠ x2) a
⊢ Acc (InvImage (DFinsupp.Lex (α := fun (x : α) ↦ N) r fun (x : α) ↦ s) toDFinsupp) x

Tactic:
InvImage.accessible toDFinsupp (DFinsupp.Lex.acc (fun _ => hbot) (fun _ => hs) _ ?_)

Premises used: InvImage.accessible, Finsupp.toDFinsupp, DFinsupp.Lex.acc
-- Module: Mathlib.Data.Finsupp.WellFounded
Goal:
α : Type u_1
N : Type u_2
inst : Zero N
r : α → α → Prop
s : N → N → Prop
hbot : ∀ ⦃n : N⦄, ¬s n 0
hs : WellFounded s
x : α →₀ N
h : ∀ a ∈ x.support, Acc (rᶜ ⊓ fun (x1 x2 : α) ↦ x1 ≠ x2) a
refine : ∀ i ∈ x.toDFinsupp.support (β := fun (x : α) ↦ N), Acc (rᶜ ⊓ fun (x1 x2 : α) ↦ x1 ≠ x2) i
⊢ Acc (InvImage (DFinsupp.Lex (α := fun (x : α) ↦ N) r fun (x : α) ↦ s) toDFinsupp) x

Tactic:
refine InvImage.accessible toDFinsupp (DFinsupp.Lex.acc (fun _ => hbot) (fun _ => hs) _ ?_)

Premises used: InvImage.accessible, Finsupp.toDFinsupp, DFinsupp.Lex.acc
-- Module: Mathlib.Data.Finsupp.WellFounded
Goal:
α : Type u_1
N : Type u_2
inst : Zero N
r : α → α → Prop
s : N → N → Prop
hbot : ∀ ⦃n : N⦄, ¬s n 0
hs : WellFounded s
x : α →₀ N
h : ∀ a ∈ x.support, Acc (rᶜ ⊓ fun (x1 x2 : α) ↦ x1 ≠ x2) a
⊢ ∀ i ∈ x.toDFinsupp.support (β := fun (x : α) ↦ N), Acc (rᶜ ⊓ fun (x1 x2 : α) ↦ x1 ≠ x2) i

Tactic:
simpa only [toDFinsupp_support] using h

Premises used: toDFinsupp_support
-- Module: Mathlib.Data.Finsupp.WellFounded
Goal:
α : Type u_1
N : Type u_2
inst : Zero N
r : α → α → Prop
s : N → N → Prop
hbot : ∀ ⦃n : N⦄, ¬s n 0
hs : WellFounded s
x : α →₀ N
h : ∀ a ∈ x.support, Acc (rᶜ ⊓ fun (x1 x2 : α) ↦ x1 ≠ x2) a
refine : ∀ i ∈ x.toDFinsupp.support (β := fun (x : α) ↦ N), Acc (rᶜ ⊓ fun (x1 x2 : α) ↦ x1 ≠ x2) i
⊢ Acc (InvImage (DFinsupp.Lex (α := fun (x : α) ↦ N) r fun (x : α) ↦ s) toDFinsupp) x

Tactic:
classical
    refine InvImage.accessible toDFinsupp (DFinsupp.Lex.acc (fun _ => hbot) (fun _ => hs) _ ?_)
    simpa only [toDFinsupp_support] using h

Premises used: toDFinsupp_support
-- Module: Mathlib.Data.Finsupp.WellFounded
Goal:
α : Type u_1
N : Type u_2
inst : Zero N
r : α → α → Prop
s : N → N → Prop
hbot : ∀ ⦃n : N⦄, ¬s n 0
hs : WellFounded s
hr : WellFounded (rᶜ ⊓ fun (x1 x2 : α) ↦ x1 ≠ x2)
⊢ WellFounded (α := α →₀ N) (Finsupp.Lex r s)

Tactic:
⟨fun x => Lex.acc hbot hs x fun a _ => hr.apply a⟩

Premises used: WellFounded.apply, WellFounded.intro, Finsupp.Lex.acc
-- Module: Mathlib.Data.Finsupp.WellFounded
Goal:
α : Type u_1
N : Type u_2
inst : Zero N
r : α → α → Prop
s : N → N → Prop
hbot : ∀ ⦃n : N⦄, ¬s n 0
hs : WellFounded s
inst_1 : Std.Trichotomous r
hr : WellFounded (Function.swap (φ := fun (a a_1 : α) ↦ Prop) r)
⊢ WellFounded (α := α →₀ N) (Finsupp.Lex r s)

Tactic:
(lex_eq_invImage_dfinsupp_lex r s).symm ▸
    InvImage.wf _ (DFinsupp.Lex.wellFounded' (fun _ => hbot) (fun _ => hs) hr)

Premises used: Eq.rec, DFinsupp.Lex.wellFounded', Finsupp.lex_eq_invImage_dfinsupp_lex, InvImage.wf, Eq.symm
-- Module: Mathlib.Data.Finsupp.WellFounded
Goal:
α_1 : Type u_1
N_1 : Type u_2
inst : Zero N_1
r : α_1 → α_1 → Prop
s : N_1 → N_1 → Prop
α : Type u_3
N : Type u_4
inst_1 : LT α
inst_2 : Std.Trichotomous fun (x1 x2 : α) ↦ x1 < x2
hα : WellFoundedGT α
inst_3 : AddMonoid N
inst_4 : PartialOrder N
inst_5 : IsBotZeroClass N
hN : WellFoundedLT N
⊢ WellFoundedLT (Lex (α →₀ N))

Tactic:
⟨Lex.wellFounded' (fun _ => not_lt_zero) hN.wf hα.wf⟩

Premises used: IsWellFounded.mk, Finsupp.Lex.wellFounded', IsWellFounded.wf, not_lt_zero
-- Module: Mathlib.Data.Finsupp.WellFounded
Goal:
α_1 : Type u_1
N_1 : Type u_2
inst : Zero N_1
r : α_1 → α_1 → Prop
s : N_1 → N_1 → Prop
α : Type u_3
N : Type u_4
inst_1 : LT α
inst_2 : Std.Trichotomous fun (x1 x2 : α) ↦ x1 < x2
inst_3 : WellFoundedLT α
inst_4 : AddMonoid N
inst_5 : PartialOrder N
inst_6 : IsBotZeroClass N
inst_7 : WellFoundedLT N
⊢ WellFoundedLT (Colex (α →₀ N))

Tactic:
Lex.wellFoundedLT (α := αᵒᵈ)

Premises used: Colex, Finsupp.Lex.wellFoundedLT, OrderDual
-- Module: Mathlib.Data.Finsupp.WellFounded
Goal:
α : Type u_1
N : Type u_2
inst : Zero N
r : α → α → Prop
s : N → N → Prop
inst_1 : IsStrictTotalOrder α r
inst_2 : Finite α
hs : WellFounded s
⊢ WellFounded (α := α →₀ N) (Finsupp.Lex r s)

Tactic:
InvImage.wf (@equivFunOnFinite α N _ _) (Pi.Lex.wellFounded r fun _ => hs)

Premises used: InvImage, Finsupp.equivFunOnFinite, Finsupp.Lex, InvImage.wf, DFunLike.coe, Pi.Lex.wellFounded
-- Module: Mathlib.Data.Finsupp.WellFounded
Goal:
α : Type u_1
N : Type u_2
inst : Zero N
inst_1 : LinearOrder α
inst_2 : Finite α
inst_3 : LT N
hwf : WellFoundedLT N
⊢ WellFoundedLT (Lex (α →₀ N))

Tactic:
⟨Finsupp.Lex.wellFounded_of_finite (· < ·) hwf.1⟩

Premises used: IsWellFounded.mk, IsWellFounded.wf, LT.lt, Finsupp.Lex.wellFounded_of_finite
-- Module: Mathlib.Data.Finsupp.WellFounded
Goal:
α : Type u_1
N : Type u_2
inst : Zero N
inst_1 : LinearOrder α
inst_2 : Finite α
inst_3 : LT N
inst_4 : WellFoundedLT N
⊢ WellFoundedLT (Colex (α →₀ N))

Tactic:
Lex.wellFoundedLT_of_finite (α := αᵒᵈ)

Premises used: Colex, OrderDual, Finsupp.Lex.wellFoundedLT_of_finite
-- Module: Mathlib.Data.Finsupp.WellFounded
Goal:
α : Type u_1
N : Type u_2
inst : Zero N
inst_1 : Preorder N
inst_2 : WellFoundedLT N
hbot : ∀ (n : N), ¬n < 0
⊢ WellFoundedLT (α →₀ N)

Tactic:
⟨InvImage.wf toDFinsupp (DFinsupp.wellFoundedLT fun _ a => hbot a).wf⟩

Premises used: IsWellFounded.mk, Finsupp.toDFinsupp, IsWellFounded.wf, InvImage.wf
-- Module: Mathlib.Data.Finsupp.WellFounded
Goal:
α : Type u_1
N_1 : Type u_2
inst : Zero N_1
r : α → α → Prop
s : N_1 → N_1 → Prop
N : Type u_3
inst_1 : AddMonoid N
inst_2 : PartialOrder N
inst_3 : IsBotZeroClass N
inst_4 : WellFoundedLT N
⊢ WellFoundedLT (α →₀ N)

Tactic:
Finsupp.wellFoundedLT fun _ => not_lt_zero

Premises used: Finsupp.wellFoundedLT, not_lt_zero
-- Module: Mathlib.Data.Finsupp.WellFounded
Goal:
α : Type u_1
N : Type u_2
inst : Zero N
r : α → α → Prop
s : N → N → Prop
inst_1 : Finite α
inst_2 : Preorder N
inst_3 : WellFoundedLT N
⊢ WellFoundedLT (α →₀ N)

Tactic:
⟨InvImage.wf equivFunOnFinite Function.wellFoundedLT.wf⟩

Premises used: IsWellFounded.mk, Finsupp.equivFunOnFinite, IsWellFounded.wf, InvImage.wf, DFunLike.coe
-- Module: Mathlib.Data.Fintype.Basic
Goal:
n : ℕ
⊢ univ = { val := (↑(List.finRange n) : Multiset (Fin n)), nodup := ⋯ : Finset (Fin n) }

Tactic:
rfl

Premises used: Finset.univ, rfl
-- Module: Mathlib.Data.Fintype.Basic
Goal:
⊢ Eq (α := Finset (Fin 2)) univ {0, 1}

Tactic:
rfl

Premises used: Finset.univ, List.ofFn, Fin.ofNat, Fin.foldr.loop, List.finRange, Multiset.ndinsert, rfl, ite
-- Module: Mathlib.Data.Fintype.Basic
Goal:
n : ℕ
⊢ val univ = (↑(List.finRange n) : Multiset (Fin n))

Tactic:
rfl

Premises used: Multiset.ofList, rfl
-- Module: Mathlib.Data.Fintype.Basic
Goal:
α : Type u_4
inst : Finite α
rcases : ∀ (n : ℕ) (e : α ≃ Fin n), Nonempty.{u_4 + 1} (Fintype α)
⊢ Nonempty.{u_4 + 1} (Fintype α)

Tactic:
rcases Finite.exists_equiv_fin α with ⟨n, ⟨e⟩⟩

Premises used: Finite.exists_equiv_fin
-- Module: Mathlib.Data.Fintype.Basic
Goal:
α : Type u_4
inst : Finite α
n : ℕ
e : α ≃ Fin n
⊢ Nonempty.{u_4 + 1} (Fintype α)

Tactic:
⟨.ofEquiv _ e.symm⟩

Premises used: Fintype.ofEquiv, Nonempty.intro, Equiv.symm
-- Module: Mathlib.Data.Fintype.Basic
Goal:
α : Type u_4
inst : Finite α
n : ℕ
e : α ≃ Fin n
⊢ Nonempty.{u_4 + 1} (Fintype α)

Tactic:
exact ⟨.ofEquiv _ e.symm⟩
-- Module: Mathlib.Data.Fintype.Basic
Goal:
n : ℕ
h : ∀ (a : Fin n), a ∈ (finRange n).toFinset ↔ Membership.mem (γ := Finset (Fin n)) univ a
⊢ (finRange n).toFinset = univ

Tactic:
ext
-- Module: Mathlib.Data.Fintype.Basic
Goal:
n : ℕ
a : Fin n
⊢ a ∈ (finRange n).toFinset ↔ Membership.mem (γ := Finset (Fin n)) univ a

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Basic
Goal:
α : Type u_1
n : ℕ
f : Fin n → α
⊢ Multiset.map f (Finset.val univ) = (↑(List.ofFn f) : Multiset α)

Tactic:
simp [List.ofFn_eq_map, univ_def]

Premises used: Fin.univ_def, List.ofFn_eq_map
-- Module: Mathlib.Data.Fintype.Basic
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
f : Fin n → α
⊢ image f univ = (List.ofFn f).toFinset

Tactic:
simp [Finset.image]

Premises used: Finset.image
-- Module: Mathlib.Data.Fintype.Basic
Goal:
α : Type u_1
n : ℕ
f : Fin n ↪ α
⊢ map f univ = { val := (↑(List.ofFn (n := n) (⇑f : (a : Fin n) → α)) : Multiset α), nodup := ⋯ }

Tactic:
simp [Finset.map]

Premises used: Finset.map
-- Module: Mathlib.Data.Fintype.Basic
Goal:
n : ℕ
i : Fin (n + 1)
h : ∀ (m : Fin (n + 1)), m ∈ image i.succAbove univ ↔ Membership.mem (γ := Finset (Fin (n + 1))) {i}ᶜ m
⊢ image i.succAbove univ = {i}ᶜ

Tactic:
ext m
-- Module: Mathlib.Data.Fintype.Basic
Goal:
n : ℕ
i m : Fin (n + 1)
⊢ m ∈ image i.succAbove univ ↔ Membership.mem (γ := Finset (Fin (n + 1))) {i}ᶜ m

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Basic
Goal:
n : ℕ
rw : Eq (α := Finset (Fin (n + 1))) (image (succAbove 0) univ) {0}ᶜ
rw₁ rw₂ : Eq (α := Finset (Fin (n + 1))) {0}ᶜ {0}ᶜ
⊢ Eq (α := Finset (Fin (n + 1))) (image succ univ) {0}ᶜ

Tactic:
rw [← Fin.succAbove_zero, Fin.image_succAbove_univ]

Premises used: Fin.succAbove_zero, Fin.image_succAbove_univ
-- Module: Mathlib.Data.Fintype.Basic
Goal:
n : ℕ
rw : image (last n).succAbove univ = {last n}ᶜ
rw₁ rw₂ : Eq (α := Finset (Fin (n + 1))) {last n}ᶜ {last n}ᶜ
⊢ Eq (α := Finset (Fin (n + 1))) (image castSucc univ) {last n}ᶜ

Tactic:
rw [← Fin.succAbove_last, Fin.image_succAbove_univ]

Premises used: Fin.succAbove_last, Fin.image_succAbove_univ
-- Module: Mathlib.Data.Fintype.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
⊢ 0 ∉ map { toFun := succ, inj' := ⋯ : Fin n ↪ Fin (n + 1) } univ

Tactic:
simp [map_eq_image]

Premises used: Finset.map_eq_image
-- Module: Mathlib.Data.Fintype.Basic
Goal:
n : ℕ
⊢ univ = Finset.cons 0 (map { toFun := succ, inj' := ⋯ : Fin n ↪ Fin (n + 1) } univ) ⋯

Tactic:
simp [map_eq_image]

Premises used: Finset.map_eq_image
-- Module: Mathlib.Data.Fintype.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
⊢ last n ∉ map castSuccEmb univ

Tactic:
simp [map_eq_image]

Premises used: Finset.map_eq_image
-- Module: Mathlib.Data.Fintype.Basic
Goal:
n : ℕ
⊢ univ = Finset.cons (last n) (map castSuccEmb univ) ⋯

Tactic:
simp [map_eq_image]

Premises used: Finset.map_eq_image
-- Module: Mathlib.Data.Fintype.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
p : Fin (n + 1)
⊢ p ∉ map p.succAboveEmb univ

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Basic
Goal:
n : ℕ
p : Fin (n + 1)
⊢ univ = Finset.cons p (map p.succAboveEmb univ) ⋯

Tactic:
simp [map_eq_image]

Premises used: Finset.map_eq_image
-- Module: Mathlib.Data.Fintype.Basic
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
⊢ image l.get univ = l.toFinset

Tactic:
simp [univ_image_def]

Premises used: Fin.univ_image_def
-- Module: Mathlib.Data.Fintype.Basic
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
l : List α
f : α → β
⊢ image (fun (i : Fin l.length) ↦ f (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (↑i : ℕ) ⋯)) univ =
    (List.map f l).toFinset

Tactic:
simp only [univ_image_def, List.ofFn_getElem_eq_map]

Premises used: Fin.univ_image_def, List.ofFn_getElem_eq_map
-- Module: Mathlib.Data.Fintype.Basic
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
l : List α
f : α → β
⊢ image (fun (x : Fin l.length) ↦ f (l.get x)) univ = (List.map f l).toFinset

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Basic
Goal:
a : Fin 2
⊢ a = 0 ↔ a = 0

Tactic:
rfl
-- Module: Mathlib.Data.Fintype.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
y : α
⊢ ∀ (x : α), Membership.mem (γ := Finset α) {y} x ↔ x = y

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
y : α
⊢ ∀ (x : α), Membership.mem (γ := Finset α) {y} x ↔ y = x

Tactic:
simp [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Data.Fintype.Basic
Goal:
⊢ Eq (α := Finset Empty) univ ∅

Tactic:
rfl

Premises used: Finset.univ, rfl
-- Module: Mathlib.Data.Fintype.Basic
Goal:
⊢ Eq.{u_4 + 1} (α := Finset PEmpty.{u_4 + 1}) univ ∅

Tactic:
rfl

Premises used: Finset.univ, rfl
-- Module: Mathlib.Data.Fintype.Basic
Goal:
⊢ Eq (α := Finset Unit) univ {()}

Tactic:
rfl

Premises used: Finset.univ, rfl
-- Module: Mathlib.Data.Fintype.Basic
Goal:
⊢ Eq (α := Finset PUnit.{u_4 + 1}) univ {PUnit.unit}

Tactic:
rfl

Premises used: Finset.univ, rfl
-- Module: Mathlib.Data.Fintype.Basic
Goal:
⊢ Eq (α := Finset Bool) univ {true, false}

Tactic:
rfl

Premises used: Finset.univ, Multiset.cons, Multiset.ofList, Multiset.ndinsert, rfl, ite
-- Module: Mathlib.Data.Fintype.Basic
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst : DecidableEq α
inst_1 : Fintype (α × β)
inst_2 : Nonempty β
a : α
⊢ Membership.mem (γ := Finset α) (image (α := α × β) Prod.fst univ) a

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Basic
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst : DecidableEq β
inst_1 : Fintype (α × β)
inst_2 : Nonempty α
b : β
⊢ Membership.mem (γ := Finset β) (image (α := α × β) Prod.snd univ) b

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
p : Prop
inst : Decidable p
x : PLift p
h : p
⊢ Membership.mem (γ := Finset (PLift p)) (if h : p then {{ down := h : PLift p }} else ∅) { down := h : PLift p }

Tactic:
simp [h]
-- Module: Mathlib.Data.Fintype.Basic
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ : Type u_3
α : Prop
β : α → Prop
inst : Decidable α
inst_1 : (a : α) → Decidable (β a)
h : ∃ (a : α), β a
x : (a : α) ×' β a
fst : α
snd : β fst
⊢ Membership.mem (γ := Finset ((a : α) ×' β a)) {mk (β := fun (a : α) ↦ β a) ⋯ ⋯} (mk (β := fun (a : α) ↦ β a) fst snd)

Tactic:
simp