awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Pi
Goal:
ι : Type u_1
inst : DecidableEq ι
α : ι → Type u_2
fs : (i : ι) → List (α i)
nil : Multiset.Pi.empty α = Pi.nil α
⊢ Eq (α := Multiset ((a : ι) → Membership.mem (γ := Multiset ι) (↑[] : Multiset ι) a → α a))
    (Multiset.pi (β := α) (↑[] : Multiset ι) fun (x : ι) ↦ (↑(fs x) : Multiset (α x)))
    (↑(pi (α := α) [] fs) : Multiset ((i : ι) → i ∈ [] → α i))

Tactic:
simp only [Multiset.coe_nil, Multiset.pi_zero, pi_nil, Multiset.coe_singleton,
      Multiset.singleton_inj]

Premises used: Multiset.singleton_inj, Multiset.coe_singleton, Multiset.pi_zero, List.pi_nil, Multiset.coe_nil
-- Module: Mathlib.Data.List.Pi
Goal:
ι : Type u_1
inst : DecidableEq ι
α : ι → Type u_2
fs : (i : ι) → List (α i)
nil : ∀ (i : ι) (hi : Membership.mem (γ := Multiset ι) 0 i), Multiset.Pi.empty α i hi = Pi.nil α i hi
⊢ Multiset.Pi.empty α = Pi.nil α

Tactic:
ext i hi
-- Module: Mathlib.Data.List.Pi
Goal:
ι : Type u_1
inst : DecidableEq ι
α : ι → Type u_2
fs : (i : ι) → List (α i)
i : ι
hi : Membership.mem (γ := Multiset ι) 0 i
⊢ Multiset.Pi.empty α i hi = Pi.nil α i hi

Tactic:
simp at hi
-- Module: Mathlib.Data.List.Pi
Goal:
ι : Type u_1
inst : DecidableEq ι
α : ι → Type u_2
fs : (i : ι) → List (α i)
i : ι
l : List ι
ih :
  ((↑l : Multiset ι).pi (β := α) fun (x : ι) ↦ (↑(fs x) : Multiset (α x))) =
    (↑(l.pi (α := α) fs) : Multiset ((i : ι) → i ∈ l → α i))
⊢ ((↑(i :: l) : Multiset ι).pi (β := α) fun (x : ι) ↦ (↑(fs x) : Multiset (α x))) =
    (↑((i :: l).pi (α := α) fs) : Multiset ((i_1 : ι) → i_1 ∈ i :: l → α i_1))

Tactic:
simp [ih, Multiset.coe_bind, ← Multiset.cons_coe]

Premises used: Multiset.coe_bind, Multiset.cons_coe
-- Module: Mathlib.Data.List.Pi
Goal:
ι : Type u_1
inst : DecidableEq ι
α : ι → Type u_2
l : List ι
fs : (i : ι) → List (α i)
nil :
  Eq (α := Multiset ((a : ι) → Membership.mem (γ := Multiset ι) (↑[] : Multiset ι) a → α a))
    (Multiset.pi (β := α) (↑[] : Multiset ι) fun (x : ι) ↦ (↑(fs x) : Multiset (α x)))
    (↑(pi (α := α) [] fs) : Multiset ((i : ι) → i ∈ [] → α i))
cons :
  ∀ (i : ι) (l : List ι)
    (ih :
      ((↑l : Multiset ι).pi (β := α) fun (x : ι) ↦ (↑(fs x) : Multiset (α x))) =
        (↑(l.pi (α := α) fs) : Multiset ((i : ι) → i ∈ l → α i))),
    ((↑(i :: l) : Multiset ι).pi (β := α) fun (x : ι) ↦ (↑(fs x) : Multiset (α x))) =
      (↑((i :: l).pi (α := α) fs) : Multiset ((i_1 : ι) → i_1 ∈ i :: l → α i_1))
⊢ ((↑l : Multiset ι).pi (β := α) fun (x : ι) ↦ (↑(fs x) : Multiset (α x))) =
    (↑(l.pi (α := α) fs) : Multiset ((i : ι) → i ∈ l → α i))

Tactic:
induction l with
  | nil =>
    simp only [Multiset.coe_nil, Multiset.pi_zero, pi_nil, Multiset.coe_singleton,
      Multiset.singleton_inj]
    ext i hi
    simp at hi
  | cons i l ih =>
    simp [ih, Multiset.coe_bind, ← Multiset.cons_coe]

Premises used: Multiset.coe_bind, Multiset.singleton_inj, List.cons, Multiset.cons_coe, Multiset.coe_singleton, Multiset.pi_zero, List.pi_nil, List.nil, Multiset.coe_nil
-- Module: Mathlib.Data.List.Pi
Goal:
ι : Type u_1
inst : DecidableEq ι
α : ι → Type u_2
l : List ι
fs : (i : ι) → List (α i)
f : (i : ι) → i ∈ l → α i
⊢ f ∈ l.pi (α := α) fs ↔ ∀ (i : ι) (hi : i ∈ l), f i hi ∈ fs i

Tactic:
simpa [Multiset.pi_coe] using Multiset.mem_pi ↑l (fs ·) f

Premises used: Multiset.mem_pi, Multiset.pi_coe
-- Module: Mathlib.Data.List.Prime
Goal:
M : Type u_1
inst : CommMonoidWithZero M
p : M
L : List M
pp : Prime p
mp : p ∣ L.prod → ∃ (a : M), a ∈ L ∧ p ∣ a
mpr : (∃ (a : M), a ∈ L ∧ p ∣ a) → p ∣ L.prod
⊢ p ∣ L.prod ↔ ∃ (a : M), a ∈ L ∧ p ∣ a

Tactic:
constructor
-- Module: Mathlib.Data.List.Prime
Goal:
M : Type u_1
inst : CommMonoidWithZero M
p : M
pp : Prime p
h : p ∣ prod []
⊢ p ∣ 1

Tactic:
rw [prod_nil] at h

Premises used: List.prod_nil
-- Module: Mathlib.Data.List.Prime
Goal:
M : Type u_1
inst : CommMonoidWithZero M
p : M
pp : Prime p
h : p ∣ 1
⊢ ∃ (a : M), Membership.mem (γ := List M) [] a ∧ p ∣ a

Tactic:
absurd h pp.not_dvd_one

Premises used: Prime.not_dvd_one, absurd
-- Module: Mathlib.Data.List.Prime
Goal:
M : Type u_1
inst : CommMonoidWithZero M
p : M
pp : Prime p
h : p ∣ 1
⊢ ∃ (a : M), Membership.mem (γ := List M) [] a ∧ p ∣ a

Tactic:
exact absurd h pp.not_dvd_one

Premises used: Prime.not_dvd_one, absurd
-- Module: Mathlib.Data.List.Prime
Goal:
M : Type u_1
inst : CommMonoidWithZero M
p : M
pp : Prime p
L_hd : M
L_tl : List M
L_ih : ∀ (h : p ∣ L_tl.prod), ∃ (a : M), a ∈ L_tl ∧ p ∣ a
h : p ∣ (L_hd :: L_tl).prod
⊢ p ∣ L_hd * L_tl.prod

Tactic:
rw [prod_cons] at h

Premises used: List.prod_cons
-- Module: Mathlib.Data.List.Prime
Goal:
M : Type u_1
inst : CommMonoidWithZero M
p : M
pp : Prime p
L_hd : M
L_tl : List M
L_ih : ∀ (h : p ∣ L_tl.prod), ∃ (a : M), a ∈ L_tl ∧ p ∣ a
h : p ∣ L_hd * L_tl.prod
mp : ∀ (hd : p ∣ L_hd), ∃ (a : M), a ∈ L_hd :: L_tl ∧ p ∣ a
mp₁ : ∀ (hd : p ∣ L_tl.prod), ∃ (a : M), a ∈ L_hd :: L_tl ∧ p ∣ a
⊢ ∃ (a : M), a ∈ L_hd :: L_tl ∧ p ∣ a

Tactic:
rcases pp.dvd_or_dvd h with hd | hd

Premises used: Prime.dvd_or_dvd
-- Module: Mathlib.Data.List.Prime
Goal:
M : Type u_1
inst : CommMonoidWithZero M
p : M
pp : Prime p
L_hd : M
L_tl : List M
L_ih : ∀ (h : p ∣ L_tl.prod), ∃ (a : M), a ∈ L_tl ∧ p ∣ a
h : p ∣ L_hd * L_tl.prod
hd : p ∣ L_hd
⊢ ∃ (a : M), a ∈ L_hd :: L_tl ∧ p ∣ a

Tactic:
⟨L_hd, mem_cons_self, hd⟩

Premises used: And.intro, Exists.intro, List.mem_cons_self
-- Module: Mathlib.Data.List.Prime
Goal:
M : Type u_1
inst : CommMonoidWithZero M
p : M
pp : Prime p
L_hd : M
L_tl : List M
L_ih : ∀ (h : p ∣ L_tl.prod), ∃ (a : M), a ∈ L_tl ∧ p ∣ a
h : p ∣ L_hd * L_tl.prod
hd : p ∣ L_hd
⊢ ∃ (a : M), a ∈ L_hd :: L_tl ∧ p ∣ a

Tactic:
exact ⟨L_hd, mem_cons_self, hd⟩
-- Module: Mathlib.Data.List.Prime
Goal:
M : Type u_1
inst : CommMonoidWithZero M
p : M
pp : Prime p
L_hd : M
L_tl : List M
L_ih : ∀ (h : p ∣ L_tl.prod), ∃ (a : M), a ∈ L_tl ∧ p ∣ a
h : p ∣ L_hd * L_tl.prod
hd : p ∣ L_tl.prod
mp : ∀ (x : M) (hx1 : x ∈ L_tl) (hx2 : p ∣ x), ∃ (a : M), a ∈ L_hd :: L_tl ∧ p ∣ a
⊢ ∃ (a : M), a ∈ L_hd :: L_tl ∧ p ∣ a

Tactic:
obtain ⟨x, hx1, hx2⟩ := L_ih hd
-- Module: Mathlib.Data.List.Prime
Goal:
M : Type u_1
inst : CommMonoidWithZero M
p : M
pp : Prime p
L_hd : M
L_tl : List M
L_ih : ∀ (h : p ∣ L_tl.prod), ∃ (a : M), a ∈ L_tl ∧ p ∣ a
h : p ∣ L_hd * L_tl.prod
hd : p ∣ L_tl.prod
x : M
hx1 : x ∈ L_tl
hx2 : p ∣ x
⊢ ∃ (a : M), a ∈ L_hd :: L_tl ∧ p ∣ a

Tactic:
⟨x, mem_cons_of_mem L_hd hx1, hx2⟩

Premises used: List.mem_cons_of_mem, And.intro, Exists.intro
-- Module: Mathlib.Data.List.Prime
Goal:
M : Type u_1
inst : CommMonoidWithZero M
p : M
pp : Prime p
L_hd : M
L_tl : List M
L_ih : ∀ (h : p ∣ L_tl.prod), ∃ (a : M), a ∈ L_tl ∧ p ∣ a
h : p ∣ L_hd * L_tl.prod
hd : p ∣ L_tl.prod
x : M
hx1 : x ∈ L_tl
hx2 : p ∣ x
⊢ ∃ (a : M), a ∈ L_hd :: L_tl ∧ p ∣ a

Tactic:
exact ⟨x, mem_cons_of_mem L_hd hx1, hx2⟩
-- Module: Mathlib.Data.List.Prime
Goal:
M : Type u_1
inst : CommMonoidWithZero M
p : M
L : List M
pp : Prime p
h : p ∣ L.prod
mp : ∀ (h : p ∣ prod []), ∃ (a : M), Membership.mem (γ := List M) [] a ∧ p ∣ a
mp₁ :
  ∀ (L_hd : M) (L_tl : List M) (L_ih : ∀ (h : p ∣ L_tl.prod), ∃ (a : M), a ∈ L_tl ∧ p ∣ a)
    (h : p ∣ (L_hd :: L_tl).prod), ∃ (a : M), a ∈ L_hd :: L_tl ∧ p ∣ a
⊢ ∃ (a : M), a ∈ L ∧ p ∣ a

Tactic:
induction L with
    | nil =>
      rw [prod_nil] at h
      exact absurd h pp.not_dvd_one
    | cons L_hd L_tl L_ih =>
      rw [prod_cons] at h
      rcases pp.dvd_or_dvd h with hd | hd
      · exact ⟨L_hd, mem_cons_self, hd⟩
      · obtain ⟨x, hx1, hx2⟩ := L_ih hd
        exact ⟨x, mem_cons_of_mem L_hd hx1, hx2⟩

Premises used: Prime.dvd_or_dvd, List.cons, List.prod_nil, List.prod_cons, List.nil
-- Module: Mathlib.Data.List.Prime
Goal:
M : Type u_1
inst : CommMonoidWithZero M
p : M
L : List M
pp : Prime p
⊢ (∃ (a : M), a ∈ L ∧ p ∣ a) → p ∣ L.prod

Tactic:
fun ⟨a, ha1, ha2⟩ => dvd_trans ha2 (dvd_prod ha1)

Premises used: Dvd.dvd, dvd_trans, _private.0.Prime.dvd_prod_iff.match_1, List.prod, List.dvd_prod
-- Module: Mathlib.Data.List.Prime
Goal:
M : Type u_1
inst : CommMonoidWithZero M
p : M
L : List M
pp : Prime p
⊢ (∃ (a : M), a ∈ L ∧ p ∣ a) → p ∣ L.prod

Tactic:
exact fun ⟨a, ha1, ha2⟩ => dvd_trans ha2 (dvd_prod ha1)
-- Module: Mathlib.Data.List.Prime
Goal:
M : Type u_1
inst : CommMonoidWithZero M
p : M
L : List M
pp : Prime p
hL : ∀ (a : M), a ∈ L → ¬p ∣ a
⊢ ¬p ∣ L.prod

Tactic:
mt (Prime.dvd_prod_iff pp).1 <| not_exists.2 fun a => not_and.2 (hL a)

Premises used: Iff.mpr, not_exists, mt, Prime.dvd_prod_iff, Iff.mp, not_and
-- Module: Mathlib.Data.List.Prime
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
inst_2 : Subsingleton.{u_1 + 1} Mˣ
p : M
hp : Prime p
L : List M
hL : ∀ (q : M), q ∈ L → Prime q
hpL : p ∣ L.prod
obtain : ∀ (x : M) (hx1 : x ∈ L) (hx2 : p ∣ x), p ∈ L
⊢ p ∈ L

Tactic:
obtain ⟨x, hx1, hx2⟩ := hp.dvd_prod_iff.mp hpL

Premises used: Prime.dvd_prod_iff, Iff.mp
-- Module: Mathlib.Data.List.Prime
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
inst_2 : Subsingleton.{u_1 + 1} Mˣ
p : M
hp : Prime p
L : List M
hL : ∀ (q : M), q ∈ L → Prime q
hpL : p ∣ L.prod
x : M
hx1 : x ∈ L
hx2 : p ∣ x
rwa rwa₁ rwa₂ rwa₃ : x ∈ L
⊢ p ∈ L

Tactic:
rwa [(prime_dvd_prime_iff_eq hp (hL x hx1)).mp hx2]

Premises used: Iff.mp, prime_dvd_prime_iff_eq
-- Module: Mathlib.Data.List.Prime
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
inst_2 : Subsingleton.{u_1 + 1} Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : (a :: l₁).prod = (b :: l₂).prod
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
⊢ ∀ (p : M), p ∈ l₁ → Prime p

Tactic:
have hl₁' : ∀ p ∈ l₁, Prime p := fun p hp => hl₁ p (mem_cons_of_mem _ hp)
-- Module: Mathlib.Data.List.Prime
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
inst_2 : Subsingleton.{u_1 + 1} Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : (a :: l₁).prod = (b :: l₂).prod
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
hl₁' : ∀ (p : M), p ∈ l₁ → Prime p
⊢ ∀ (p : M), p ∈ (b :: l₂).erase a → Prime p

Tactic:
have hl₂' : ∀ p ∈ (b :: l₂).erase a, Prime p := fun p hp => hl₂ p (mem_of_mem_erase hp)
-- Module: Mathlib.Data.List.Prime
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
inst_2 : Subsingleton.{u_1 + 1} Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : (a :: l₁).prod = (b :: l₂).prod
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
hl₁' : ∀ (p : M), p ∈ l₁ → Prime p
hl₂' : ∀ (p : M), p ∈ (b :: l₂).erase a → Prime p
rw : a ∣ a * l₁.prod
⊢ a ∣ (a :: l₁).prod

Tactic:
rw [prod_cons]

Premises used: List.prod_cons
-- Module: Mathlib.Data.List.Prime
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
inst_2 : Subsingleton.{u_1 + 1} Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : (a :: l₁).prod = (b :: l₂).prod
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
hl₁' : ∀ (p : M), p ∈ l₁ → Prime p
hl₂' : ∀ (p : M), p ∈ (b :: l₂).erase a → Prime p
⊢ a ∣ a * l₁.prod

Tactic:
dvd_mul_right _ _

Premises used: dvd_mul_right
-- Module: Mathlib.Data.List.Prime
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
inst_2 : Subsingleton.{u_1 + 1} Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : (a :: l₁).prod = (b :: l₂).prod
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
hl₁' : ∀ (p : M), p ∈ l₁ → Prime p
hl₂' : ∀ (p : M), p ∈ (b :: l₂).erase a → Prime p
⊢ a ∣ a * l₁.prod

Tactic:
exact dvd_mul_right _ _

Premises used: dvd_mul_right
-- Module: Mathlib.Data.List.Prime
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
inst_2 : Subsingleton.{u_1 + 1} Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : (a :: l₁).prod = (b :: l₂).prod
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
hl₁' : ∀ (p : M), p ∈ l₁ → Prime p
hl₂' : ∀ (p : M), p ∈ (b :: l₂).erase a → Prime p
⊢ a ∈ b :: l₂

Tactic:
have ha : a ∈ b :: l₂ :=
        mem_list_primes_of_dvd_prod (hl₁ a mem_cons_self) hl₂
          (h ▸ by rw [prod_cons]; exact dvd_mul_right _ _)
-- Module: Mathlib.Data.List.Prime
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
inst_2 : Subsingleton.{u_1 + 1} Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : (a :: l₁).prod = (b :: l₂).prod
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
hl₁' : ∀ (p : M), p ∈ l₁ → Prime p
hl₂' : ∀ (p : M), p ∈ (b :: l₂).erase a → Prime p
ha : a ∈ b :: l₂
⊢ b :: l₂ ~ a :: (b :: l₂).erase a

Tactic:
have hb : b :: l₂ ~ a :: (b :: l₂).erase a := perm_cons_erase ha
-- Module: Mathlib.Data.List.Prime
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
inst_2 : Subsingleton.{u_1 + 1} Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : (a :: l₁).prod = (b :: l₂).prod
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
hl₁' : ∀ (p : M), p ∈ l₁ → Prime p
hl₂' : ∀ (p : M), p ∈ (b :: l₂).erase a → Prime p
ha : a ∈ b :: l₂
hb : b :: l₂ ~ a :: (b :: l₂).erase a
rwa : (a :: l₁).prod = a * ((b :: l₂).erase a).prod
rwa₁ : (a :: l₁).prod = (a :: (b :: l₂).erase a).prod
rwa₂ rwa₃ rwa₄ rwa₅ : (a :: l₁).prod = (b :: l₂).prod
⊢ a * l₁.prod = a * ((b :: l₂).erase a).prod

Tactic:
rwa [← prod_cons, ← prod_cons, ← hb.prod_eq]

Premises used: List.Perm.prod_eq, List.prod_cons
-- Module: Mathlib.Data.List.Prime
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
inst_2 : Subsingleton.{u_1 + 1} Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : (a :: l₁).prod = (b :: l₂).prod
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
hl₁' : ∀ (p : M), p ∈ l₁ → Prime p
hl₂' : ∀ (p : M), p ∈ (b :: l₂).erase a → Prime p
ha : a ∈ b :: l₂
hb : b :: l₂ ~ a :: (b :: l₂).erase a
⊢ l₁.prod = ((b :: l₂).erase a).prod

Tactic:
have hl : prod l₁ = prod ((b :: l₂).erase a) :=
        (mul_right_inj' (hl₁ a mem_cons_self).ne_zero).1 <| by
          rwa [← prod_cons, ← prod_cons, ← hb.prod_eq]
-- Module: Mathlib.Data.List.Prime
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
inst_2 : Subsingleton.{u_1 + 1} Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : (a :: l₁).prod = (b :: l₂).prod
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
hl₁' : ∀ (p : M), p ∈ l₁ → Prime p
hl₂' : ∀ (p : M), p ∈ (b :: l₂).erase a → Prime p
ha : a ∈ b :: l₂
hb : b :: l₂ ~ a :: (b :: l₂).erase a
hl : l₁.prod = ((b :: l₂).erase a).prod
⊢ a :: l₁ ~ b :: l₂

Tactic:
Perm.trans ((perm_of_prod_eq_prod hl hl₁' hl₂').cons _) hb.symm

Premises used: List.Perm.cons, List.Perm.trans, List.Perm.symm
-- Module: Mathlib.Data.List.Prime
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
inst_2 : Subsingleton.{u_1 + 1} Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : (a :: l₁).prod = (b :: l₂).prod
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
hl₁' : ∀ (p : M), p ∈ l₁ → Prime p
hl₂' : ∀ (p : M), p ∈ (b :: l₂).erase a → Prime p
ha : a ∈ b :: l₂
hb : b :: l₂ ~ a :: (b :: l₂).erase a
hl : l₁.prod = ((b :: l₂).erase a).prod
⊢ a :: l₁ ~ b :: l₂

Tactic:
exact Perm.trans ((perm_of_prod_eq_prod hl hl₁' hl₂').cons _) hb.symm

Premises used: List.Perm.cons, List.Perm.trans, List.Perm.symm
-- Module: Mathlib.Data.List.Prime
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
inst_2 : Subsingleton.{u_1 + 1} Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : (a :: l₁).prod = (b :: l₂).prod
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
have have₁ have₂ : ∀ (hl₁' : ∀ (p : M), p ∈ l₁ → Prime p), a :: l₁ ~ b :: l₂
have₃ : ∀ (hl₁' : ∀ (p : M), p ∈ l₁ → Prime p) (hl₂' : ∀ (p : M), p ∈ (b :: l₂).erase a → Prime p), a :: l₁ ~ b :: l₂
have₄ :
  ∀ (hl₁' : ∀ (p : M), p ∈ l₁ → Prime p) (hl₂' : ∀ (p : M), p ∈ (b :: l₂).erase a → Prime p) (ha : a ∈ b :: l₂),
    a :: l₁ ~ b :: l₂
have₅ :
  ∀ (hl₁' : ∀ (p : M), p ∈ l₁ → Prime p) (hl₂' : ∀ (p : M), p ∈ (b :: l₂).erase a → Prime p) (ha : a ∈ b :: l₂)
    (hb : b :: l₂ ~ a :: (b :: l₂).erase a), a :: l₁ ~ b :: l₂
have₆ :
  ∀ (hl₁' : ∀ (p : M), p ∈ l₁ → Prime p) (hl₂' : ∀ (p : M), p ∈ (b :: l₂).erase a → Prime p) (ha : a ∈ b :: l₂)
    (hb : b :: l₂ ~ a :: (b :: l₂).erase a) (hl : l₁.prod = ((b :: l₂).erase a).prod), a :: l₁ ~ b :: l₂
⊢ a :: l₁ ~ b :: l₂

Tactic:
classical
      have hl₁' : ∀ p ∈ l₁, Prime p := fun p hp => hl₁ p (mem_cons_of_mem _ hp)
      have hl₂' : ∀ p ∈ (b :: l₂).erase a, Prime p := fun p hp => hl₂ p (mem_of_mem_erase hp)
      have ha : a ∈ b :: l₂ :=
        mem_list_primes_of_dvd_prod (hl₁ a mem_cons_self) hl₂
          (h ▸ by rw [prod_cons]; exact dvd_mul_right _ _)
      have hb : b :: l₂ ~ a :: (b :: l₂).erase a := perm_cons_erase ha
      have hl : prod l₁ = prod ((b :: l₂).erase a) :=
        (mul_right_inj' (hl₁ a mem_cons_self).ne_zero).1 <| by
          rwa [← prod_cons, ← prod_cons, ← hb.prod_eq]
      exact Perm.trans ((perm_of_prod_eq_prod hl hl₁' hl₂').cons _) hb.symm
-- Module: Mathlib.Data.List.ProdSigma
Goal:
α : Type u_1
β : Type u_2
l : List β
⊢ SProd.sprod (α := List α) [] l = []

Tactic:
rfl

Premises used: List.product, rfl, List.flatten
-- Module: Mathlib.Data.List.ProdSigma
Goal:
α : Type u_1
β : Type u_2
a : α
l₁ : List α
l₂ : List β
⊢ (a :: l₁) ×ˢ l₂ = map (fun (b : β) ↦ (a, b)) l₂ ++ l₁ ×ˢ l₂

Tactic:
rfl

Premises used: List.product, rfl, List.flatten
-- Module: Mathlib.Data.List.ProdSigma
Goal:
α : Type u_1
β : Type u_2
head : α
l : List α
⊢ SProd.sprod (β := List β) (head :: l) [] = []

Tactic:
simp [product_cons, product_nil l]

Premises used: List.product_cons
-- Module: Mathlib.Data.List.ProdSigma
Goal:
α : Type u_1
β : Type u_2
l₁ : List α
l₂ : List β
a : α
b : β
⊢ (a, b) ∈ l₁ ×ˢ l₂ ↔ a ∈ l₁ ∧ b ∈ l₂

Tactic:
simp_all [SProd.sprod, product, mem_flatMap, mem_map, Prod.ext_iff, and_left_comm]

Premises used: List.product, SProd.sprod, Prod.ext_iff, and_left_comm, List.mem_flatMap, List.mem_map
-- Module: Mathlib.Data.List.ProdSigma
Goal:
α : Type u_1
β : Type u_2
l₂ : List β
⊢ (SProd.sprod (α := List α) [] l₂).length = length.{u_1} (α := α) [] * l₂.length

Tactic:
(Nat.zero_mul _).symm

Premises used: Nat.zero_mul, Eq.symm
-- Module: Mathlib.Data.List.ProdSigma
Goal:
α : Type u_1
β : Type u_2
l₂ : List β
⊢ (SProd.sprod (α := List α) [] l₂).length = length.{u_1} (α := α) [] * l₂.length

Tactic:
exact (Nat.zero_mul _).symm

Premises used: Nat.zero_mul, Eq.symm
-- Module: Mathlib.Data.List.ProdSigma
Goal:
α : Type u_1
β : Type u_2
l₂ : List β
x : α
l₁ : List α
IH : (l₁ ×ˢ l₂).length = l₁.length * l₂.length
⊢ ((x :: l₁) ×ˢ l₂).length = (x :: l₁).length * l₂.length

Tactic:
simp only [length, product_cons, length_append, IH, Nat.add_mul, Nat.one_mul, length_map,
      Nat.add_comm]

Premises used: List.product_cons, List.length_append, List.length_map, List.length, Nat.one_mul, Nat.add_mul, Nat.add_comm
-- Module: Mathlib.Data.List.ProdSigma
Goal:
α : Type u_1
β : Type u_2
l₁ : List α
l₂ : List β
nil : (SProd.sprod (α := List α) [] l₂).length = length.{u_1} (α := α) [] * l₂.length
cons :
  ∀ (x : α) (l₁ : List α) (IH : (l₁ ×ˢ l₂).length = l₁.length * l₂.length),
    ((x :: l₁) ×ˢ l₂).length = (x :: l₁).length * l₂.length
⊢ (l₁ ×ˢ l₂).length = l₁.length * l₂.length

Tactic:
induction l₁ with
  | nil => exact (Nat.zero_mul _).symm
  | cons x l₁ IH =>
    simp only [length, product_cons, length_append, IH, Nat.add_mul, Nat.one_mul, length_map,
      Nat.add_comm]

Premises used: List.product_cons, List.length_append, List.cons, Nat.zero_mul, List.length_map, Eq.symm, List.length, Nat.one_mul, Nat.add_mul, List.nil, Nat.add_comm
-- Module: Mathlib.Data.List.ProdSigma
Goal:
α : Type u_1
σ : α → Type u_3
l : (a : α) → List (σ a)
⊢ List.sigma (σ := σ) [] l = []

Tactic:
rfl

Premises used: List.sigma, rfl, List.flatten
-- Module: Mathlib.Data.List.ProdSigma
Goal:
α : Type u_1
σ : α → Type u_3
a : α
l₁ : List α
l₂ : (a : α) → List (σ a)
⊢ (a :: l₁).sigma (σ := σ) l₂ = map (Sigma.mk (β := σ) a) (l₂ a) ++ l₁.sigma (σ := σ) l₂

Tactic:
rfl

Premises used: List.sigma, rfl, List.flatten
-- Module: Mathlib.Data.List.ProdSigma
Goal:
α : Type u_1
σ : α → Type u_3
head : α
l : List α
⊢ Eq (α := List ((a : α) × σ a)) ((head :: l).sigma (σ := σ) fun (a : α) ↦ []) []

Tactic:
simp [sigma_cons, sigma_nil l]

Premises used: List.sigma_cons
-- Module: Mathlib.Data.List.ProdSigma
Goal:
α : Type u_1
σ : α → Type u_3
l₁ : List α
l₂ : (a : α) → List (σ a)
a : α
b : σ a
⊢ Sigma.mk (β := σ) a b ∈ l₁.sigma (σ := σ) l₂ ↔ a ∈ l₁ ∧ b ∈ l₂ a

Tactic:
simp [List.sigma, mem_flatMap, mem_map, exists_and_left, and_left_comm,
    exists_eq_left, exists_eq_right]

Premises used: List.sigma, exists_eq_right, exists_and_left, and_left_comm, exists_eq_left, List.mem_flatMap, List.mem_map
-- Module: Mathlib.Data.List.ProdSigma
Goal:
α : Type u_1
β : Type u_2
x : α
y : β
xs : List (α × β)
⊢ (y, x) ∈ map Prod.swap xs ↔ (x, y) ∈ xs

Tactic:
simp
-- Module: Mathlib.Data.List.Range
Goal:
n m i : ℕ
H : i < (range' n m).length
⊢ getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (range' n m) i H = n + i

Tactic:
simp
-- Module: Mathlib.Data.List.Range
Goal:
r : ℕ → ℕ → Prop
⊢ IsChain r (range 0) ↔ ∀ (m : ℕ), m < HSub.hSub (α := ℕ) 0 1 → r m m.succ

Tactic:
simp
-- Module: Mathlib.Data.List.Range
Goal:
r : ℕ → ℕ → Prop
n : ℕ
hn : IsChain r (range n) ↔ ∀ (m : ℕ), m < n - 1 → r m m.succ
succ :
  ∀ (hn : IsChain r (range n) ↔ ∀ (m : ℕ), m + 1 < n → r m m.succ),
    IsChain r (range n ++ [n]) ↔ ∀ (m : ℕ), m < n → r m m.succ
⊢ IsChain r (range (n + 1)) ↔ ∀ (m : ℕ), m < n + 1 - 1 → r m m.succ

Tactic:
simp only [range_succ, Nat.add_one_sub_one, Nat.lt_sub_iff_add_lt] at hn ⊢

Premises used: Nat.add_one_sub_one, Nat.lt_sub_iff_add_lt, List.range_succ
-- Module: Mathlib.Data.List.Range
Goal:
r : ℕ → ℕ → Prop
hn : IsChain r (range 0) ↔ ∀ (m : ℕ), m + 1 < 0 → r m m.succ
⊢ IsChain r (range 0 ++ [0]) ↔ ∀ (m : ℕ), m < 0 → r m m.succ

Tactic:
simp
-- Module: Mathlib.Data.List.Range
Goal:
r : ℕ → ℕ → Prop
n : ℕ
hn : IsChain r (range (n + 1)) ↔ ∀ (m : ℕ), m + 1 < n + 1 → r m m.succ
succ :
  ∀ (hn : IsChain r (range n ++ [n]) ↔ ∀ (m : ℕ), m < n → r m (m + 1)),
    IsChain r (range n ++ [n]) ∧ r n (n + 1) ↔ ∀ (m : ℕ), m < n + 1 → r m (m + 1)
⊢ IsChain r (range (n + 1) ++ [n + 1]) ↔ ∀ (m : ℕ), m < n + 1 → r m m.succ

Tactic:
simp only [range_succ, Nat.add_lt_add_iff_right, succ_eq_add_one, append_assoc, cons_append,
        nil_append, isChain_append_cons_cons, IsChain.singleton, and_true] at hn ⊢

Premises used: Nat.succ_eq_add_one, and_true, List.append_assoc, List.IsChain.singleton, List.nil_append, List.isChain_append_cons_cons, Nat.add_lt_add_iff_right, List.cons_append, List.range_succ
-- Module: Mathlib.Data.List.Range
Goal:
r : ℕ → ℕ → Prop
n : ℕ
hn : IsChain r (range n ++ [n]) ↔ ∀ (m : ℕ), m < n → r m (m + 1)
succ : (∀ (m : ℕ), m < n → r m (m + 1)) ∧ r n (n + 1) ↔ ∀ (m : ℕ), m < n + 1 → r m (m + 1)
succ₁ succ₂ : (∀ (m : ℕ), m < n → r m (m + 1)) ∧ r n (n + 1) ↔ (∀ (m : ℕ), m < n → r m (m + 1)) ∧ r n (n + 1)
⊢ IsChain r (range n ++ [n]) ∧ r n (n + 1) ↔ ∀ (m : ℕ), m < n + 1 → r m (m + 1)

Tactic:
rw [hn, forall_lt_succ_right]

Premises used: Nat.forall_lt_succ_right
-- Module: Mathlib.Data.List.Range
Goal:
r : ℕ → ℕ → Prop
n : ℕ
hn : IsChain r (range n) ↔ ∀ (m : ℕ), m + 1 < n → r m m.succ
succ :
  ∀ (hn : IsChain r (range 0) ↔ ∀ (m : ℕ), m + 1 < 0 → r m m.succ),
    IsChain r (range 0 ++ [0]) ↔ ∀ (m : ℕ), m < 0 → r m m.succ
succ₁ :
  ∀ (n : ℕ) (hn : IsChain r (range (n + 1)) ↔ ∀ (m : ℕ), m + 1 < n + 1 → r m m.succ),
    IsChain r (range (n + 1) ++ [n + 1]) ↔ ∀ (m : ℕ), m < n + 1 → r m m.succ
⊢ IsChain r (range n ++ [n]) ↔ ∀ (m : ℕ), m < n → r m m.succ

Tactic:
cases n with
    | zero => simp
    | succ n =>
      simp only [range_succ, Nat.add_lt_add_iff_right, succ_eq_add_one, append_assoc, cons_append,
        nil_append, isChain_append_cons_cons, IsChain.singleton, and_true] at hn ⊢
      rw [hn, forall_lt_succ_right]

Premises used: Nat.succ_eq_add_one, and_true, List.append_assoc, List.IsChain.singleton, List.nil_append, List.isChain_append_cons_cons, Nat.zero, Nat.add_lt_add_iff_right, Nat.succ, List.cons_append, Nat.forall_lt_succ_right, List.range_succ