awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn_1 : n < (permutations'Aux x as).length
hn' : as.insertIdx n x = a
m : ℕ
hm_1 : m < (permutations'Aux x bs).length
hm' : bs.insertIdx m x = a
hl : as.length = bs.length
hn : n ≤ as.length
hm : m ≤ bs.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (as.insertIdx n x) m ⋯ = x
hx' : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (bs.insertIdx m x) n ⋯ = x
cons : ∀ (ht : n < m), False
⊢ False
have cons₁ : ∀ (ht : n = m), False
Tactic: rcases lt_trichotomy n m with (ht | ht | ht)
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn_1 : n < (permutations'Aux x as).length
hn' : as.insertIdx n x = a
m : ℕ
hm_1 : m < (permutations'Aux x bs).length
hm' : bs.insertIdx m x = a
hl : as.length = bs.length
hn : n ≤ as.length
hm : m ≤ bs.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (as.insertIdx n x) m ⋯ = x
hx' : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (bs.insertIdx m x) n ⋯ = x
cons : ∀ (ht : n < m), False
cons₁ : ∀ (ht : n = m), False
⊢ False
have cons₂ : ∀ (ht : m < n), False
Tactic: rcases lt_trichotomy n m with (ht | ht | ht)
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn_1 : n < (permutations'Aux x as).length
hn' : as.insertIdx n x = a
m : ℕ
hm_1 : m < (permutations'Aux x bs).length
hm' : bs.insertIdx m x = a
hl : as.length = bs.length
hn : n ≤ as.length
hm : m ≤ bs.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (as.insertIdx n x) m ⋯ = x
hx' : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (bs.insertIdx m x) n ⋯ = x
ht : n < m
⊢ False
have cons : x ∈ bs
Tactic: suffices x ∈ bs by exact h x (hb.subset this) rfl
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn_1 : n < (permutations'Aux x as).length
hn' : as.insertIdx n x = a
m : ℕ
hm_1 : m < (permutations'Aux x bs).length
hm' : bs.insertIdx m x = a
hl : as.length = bs.length
hn : n ≤ as.length
hm : m ≤ bs.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (as.insertIdx n x) m ⋯ = x
hx' : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (bs.insertIdx m x) n ⋯ = x
ht : n < m
⊢ x ∈ bs
have cons : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) bs n sorry ∈ bs
Tactic: rw [← hx', getElem_insertIdx_of_lt ht]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (hypothesis)
Goal:
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn_1 : n < (permutations'Aux x as).length
hn' : as.insertIdx n x = a
m : ℕ
hm_1 : m < (permutations'Aux x bs).length
hm' : bs.insertIdx m x = a
hl : as.length = bs.length
hn : n ≤ as.length
hm : m ≤ bs.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (as.insertIdx n x) m ⋯ = x
hx' : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (bs.insertIdx m x) n ⋯ = x
ht : n = m
⊢ False
have hn'₁ : as.insertIdx m x = a
Tactic: simp only [ht] at hm' hn'
Cleared hypotheses: hn'
-- Lean 4 proof step from Mathlib.Data.List.Permutation (hypothesis)
Goal:
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn_1 : n < (permutations'Aux x as).length
m : ℕ
hm_1 : m < (permutations'Aux x bs).length
hm' : bs.insertIdx m x = a
hl : as.length = bs.length
hn : n ≤ as.length
hm : m ≤ bs.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (as.insertIdx n x) m ⋯ = x
hx' : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (bs.insertIdx m x) n ⋯ = x
ht : n = m
hn' : as.insertIdx m x = a
⊢ False
have hn'₁ : as.insertIdx m x = bs.insertIdx m x
Tactic: rw [← hm'] at hn'
Cleared hypotheses: hn'
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn_1 : n < (permutations'Aux x as).length
hn' : as.insertIdx n x = a
m : ℕ
hm_1 : m < (permutations'Aux x bs).length
hm' : bs.insertIdx m x = a
hl : as.length = bs.length
hn : n ≤ as.length
hm : m ≤ bs.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (as.insertIdx n x) m ⋯ = x
hx' : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (bs.insertIdx m x) n ⋯ = x
ht : m < n
⊢ False
have cons : x ∈ as
Tactic: suffices x ∈ as by exact h x (ha.subset this) rfl
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn_1 : n < (permutations'Aux x as).length
hn' : as.insertIdx n x = a
m : ℕ
hm_1 : m < (permutations'Aux x bs).length
hm' : bs.insertIdx m x = a
hl : as.length = bs.length
hn : n ≤ as.length
hm : m ≤ bs.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (as.insertIdx n x) m ⋯ = x
hx' : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (bs.insertIdx m x) n ⋯ = x
ht : m < n
⊢ x ∈ as
have cons : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) as m sorry ∈ as
Tactic: rw [← hx, getElem_insertIdx_of_lt ht]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
s : List α
hs : s.Nodup
⊢ s.permutations'.Nodup
have nil : Nodup.{u_1} (α := List α) (permutations' [])
Tactic: induction hs with
  | nil => simp
  | @cons x l h h' IH =>
    rw [permutations']
    rw [nodup_flatMap]
    constructor
    · intro ys hy
      rw [mem_permutations'] at hy
      rw [nodup_permutations'Aux_iff, hy.mem_iff]
      exact fun H => h x H rfl
    · refine IH.pairwise_of_forall_ne fun as ha bs hb H => ?_
      rw [Function.onFun, disjoint_iff_ne]
      rintro a ha' b hb' rfl
      obtain ⟨⟨n, hn⟩, hn'⟩ := get_of_mem ha'
      obtain ⟨⟨m, hm⟩, hm'⟩ := get_of_mem hb'
      rw [mem_permutations'] at ha hb
      have hl : as.length = bs.length := (ha.trans hb.symm).length_eq
      simp only [Nat.lt_succ_iff, length_permutations'Aux] at hn hm
      rw [get_permutations'Aux] at hn' hm'
      have hx : (as.insertIdx n x)[m]'(by
          rwa [length_insertIdx_of_le_length hn, Nat.lt_succ_iff, hl]) = x := by
        simp [hn', ← hm']
      have hx' : (bs.insertIdx m x)[n]'(by
          rwa [length_insertIdx_of_le_length hm, Nat.lt_succ_iff, ← hl]) = x := by
        simp [hm', ← hn']
      rcases lt_trichotomy n m with (ht | ht | ht)
      · suffices x ∈ bs by exact h x (hb.subset this) rfl
        rw [← hx', getElem_insertIdx_of_lt ht]
        exact getElem_mem _
      · simp only [ht] at hm' hn'
        rw [← hm'] at hn'
        exact H (insertIdx_injective _ _ hn')
      · suffices x ∈ as by exact h x (ha.subset this) rfl
        rw [← hx, getElem_insertIdx_of_lt ht]
        exact getElem_mem _
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
s : List α
hs : s.Nodup
nil : Nodup.{u_1} (α := List α) (permutations' [])
⊢ s.permutations'.Nodup
have cons : ∀ {x : α} {l : List α} (h : ∀ (a' : α), a' ∈ l → x ≠ a') (h' : Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) l)
  (IH : l.permutations'.Nodup), (x :: l).permutations'.Nodup
Tactic: induction hs with
  | nil => simp
  | @cons x l h h' IH =>
    rw [permutations']
    rw [nodup_flatMap]
    constructor
    · intro ys hy
      rw [mem_permutations'] at hy
      rw [nodup_permutations'Aux_iff, hy.mem_iff]
      exact fun H => h x H rfl
    · refine IH.pairwise_of_forall_ne fun as ha bs hb H => ?_
      rw [Function.onFun, disjoint_iff_ne]
      rintro a ha' b hb' rfl
      obtain ⟨⟨n, hn⟩, hn'⟩ := get_of_mem ha'
      obtain ⟨⟨m, hm⟩, hm'⟩ := get_of_mem hb'
      rw [mem_permutations'] at ha hb
      have hl : as.length = bs.length := (ha.trans hb.symm).length_eq
      simp only [Nat.lt_succ_iff, length_permutations'Aux] at hn hm
      rw [get_permutations'Aux] at hn' hm'
      have hx : (as.insertIdx n x)[m]'(by
          rwa [length_insertIdx_of_le_length hn, Nat.lt_succ_iff, hl]) = x := by
        simp [hn', ← hm']
      have hx' : (bs.insertIdx m x)[n]'(by
          rwa [length_insertIdx_of_le_length hm, Nat.lt_succ_iff, ← hl]) = x := by
        simp [hm', ← hn']
      rcases lt_trichotomy n m with (ht | ht | ht)
      · suffices x ∈ bs by exact h x (hb.subset this) rfl
        rw [← hx', getElem_insertIdx_of_lt ht]
        exact getElem_mem _
      · simp only [ht] at hm' hn'
        rw [← hm'] at hn'
        exact H (insertIdx_injective _ _ hn')
      · suffices x ∈ as by exact h x (ha.subset this) rfl
        rw [← hx, getElem_insertIdx_of_lt ht]
        exact getElem_mem _
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
x y : α
s : List α
⊢ take 2 (x :: y :: s).permutations = [x :: y :: s, y :: x :: s]
have nil : take 2 [x, y].permutations = [[x, y], [y, x]]
Tactic: induction s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
x y : α
s : List α
nil : take 2 [x, y].permutations = [[x, y], [y, x]]
⊢ take 2 (x :: y :: s).permutations = [x :: y :: s, y :: x :: s]
have cons : ∀ (head : α) (tail : List α),
  take 2 (x :: y :: tail).permutations = [x :: y :: tail, y :: x :: tail] →
    take 2 (x :: y :: head :: tail).permutations = [x :: y :: head :: tail, y :: x :: head :: tail]
Tactic: induction s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
s : List α
⊢ s.permutations.Nodup ↔ s.Nodup
have refine : s.permutations.Nodup → s.Nodup
Tactic: refine ⟨?_, nodup_permutations s⟩
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
s : List α
⊢ s.permutations.Nodup → s.Nodup
have contrapose : ¬s.Nodup → ¬s.permutations.Nodup
Tactic: contrapose
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
s : List α
⊢ ¬s.Nodup → ¬s.permutations.Nodup
have rw : (∃ (x : α), Duplicate x s) → ¬s.permutations.Nodup
Tactic: rw [← exists_duplicate_iff_not_nodup]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (hypothesis)
Goal:
α : Type u_1
s : List α
x : α
hs : Duplicate x s
⊢ ¬s.permutations.Nodup
have hs₁ : [x, x] <+ s
Tactic: rw [duplicate_iff_sublist] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
s : List α
x : α
hs : [x, x] <+ s
⊢ ¬s.permutations.Nodup
have obtain : ∀ (l : List α) (ht : s ~ [x, x] ++ l), ¬s.permutations.Nodup
Tactic: obtain ⟨l, ht⟩ := List.Sublist.exists_perm_append hs
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
s : List α
x : α
hs : [x, x] <+ s
l : List α
ht : s ~ [x, x] ++ l
⊢ ¬s.permutations.Nodup
have rw : ∃ (x_1 : List α), Duplicate x_1 ([x, x] ++ l).permutations
Tactic: rw [List.Perm.nodup_iff (List.Perm.permutations ht), ← exists_duplicate_iff_not_nodup]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
s : List α
x : α
hs : [x, x] <+ s
l : List α
ht : s ~ [x, x] ++ l
⊢ ∃ (x_1 : List α), Duplicate x_1 ([x, x] ++ l).permutations
have h : Duplicate (x :: x :: l) ([x, x] ++ l).permutations
Tactic: use x :: x :: l
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
s : List α
x : α
hs : [x, x] <+ s
l : List α
ht : s ~ [x, x] ++ l
⊢ Duplicate (x :: x :: l) ([x, x] ++ l).permutations
have h : take 2 (x :: x :: l).permutations <+ ([x, x] ++ l).permutations
Tactic: rw [List.duplicate_iff_sublist, ← permutations_take_two]
-- Lean 4 proof step from Mathlib.Data.List.Pi (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
α : ι → Type u_2
fs : (i : ι) → List (α i)
⊢ Eq (α := Multiset ((a : ι) → Membership.mem (γ := Multiset ι) (↑[] : Multiset ι) a → α a))
    (Multiset.pi (β := α) (↑[] : Multiset ι) fun (x : ι) ↦ (↑(fs x) : Multiset (α x)))
    (↑(pi (α := α) [] fs) : Multiset ((i : ι) → i ∈ [] → α i))
have nil : Multiset.Pi.empty α = Pi.nil α
Tactic: simp only [Multiset.coe_nil, Multiset.pi_zero, pi_nil, Multiset.coe_singleton,
      Multiset.singleton_inj]
-- Lean 4 proof step from Mathlib.Data.List.Pi (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
α : ι → Type u_2
fs : (i : ι) → List (α i)
⊢ Multiset.Pi.empty α = Pi.nil α
have nil : ∀ (i : ι) (hi : Membership.mem (γ := Multiset ι) 0 i), Multiset.Pi.empty α i hi = Pi.nil α i hi
Tactic: ext i hi
-- Lean 4 proof step from Mathlib.Data.List.Pi (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
α : ι → Type u_2
l : List ι
fs : (i : ι) → List (α i)
⊢ ((↑l : Multiset ι).pi (β := α) fun (x : ι) ↦ (↑(fs x) : Multiset (α x))) =
    (↑(l.pi (α := α) fs) : Multiset ((i : ι) → i ∈ l → α i))
have 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: 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]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Pi (goal)
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))
⊢ ((↑l : Multiset ι).pi (β := α) fun (x : ι) ↦ (↑(fs x) : Multiset (α x))) =
    (↑(l.pi (α := α) fs) : Multiset ((i : ι) → i ∈ l → α i))
have 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))
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]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Prime (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
p : M
L : List M
pp : Prime p
⊢ p ∣ L.prod ↔ ∃ (a : M), a ∈ L ∧ p ∣ a
have mp : p ∣ L.prod → ∃ (a : M), a ∈ L ∧ p ∣ a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.Prime (goal)
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
⊢ p ∣ L.prod ↔ ∃ (a : M), a ∈ L ∧ p ∣ a
have mpr : (∃ (a : M), a ∈ L ∧ p ∣ a) → p ∣ L.prod
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.Prime (hypothesis)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
p : M
pp : Prime p
h : p ∣ prod []
⊢ ∃ (a : M), Membership.mem (γ := List M) [] a ∧ p ∣ a
have h₁ : p ∣ 1
Tactic: rw [prod_nil] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Prime (hypothesis)
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
⊢ ∃ (a : M), a ∈ L_hd :: L_tl ∧ p ∣ a
have h₁ : p ∣ L_hd * L_tl.prod
Tactic: rw [prod_cons] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Prime (goal)
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
⊢ ∃ (a : M), a ∈ L_hd :: L_tl ∧ p ∣ a
have mp : ∀ (hd : p ∣ L_hd), ∃ (a : M), a ∈ L_hd :: L_tl ∧ p ∣ a
Tactic: rcases pp.dvd_or_dvd h with hd | hd
-- Lean 4 proof step from Mathlib.Data.List.Prime (goal)
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
⊢ ∃ (a : M), a ∈ L_hd :: L_tl ∧ p ∣ a
have mp₁ : ∀ (hd : p ∣ L_tl.prod), ∃ (a : M), a ∈ L_hd :: L_tl ∧ p ∣ a
Tactic: rcases pp.dvd_or_dvd h with hd | hd
-- Lean 4 proof step from Mathlib.Data.List.Prime (goal)
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
⊢ ∃ (a : M), a ∈ L_hd :: L_tl ∧ p ∣ a
have mp : ∀ (x : M) (hx1 : x ∈ L_tl) (hx2 : p ∣ x), ∃ (a : M), a ∈ L_hd :: L_tl ∧ p ∣ a
Tactic: obtain ⟨x, hx1, hx2⟩ := L_ih hd
-- Lean 4 proof step from Mathlib.Data.List.Prime (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
p : M
L : List M
pp : Prime p
h : p ∣ L.prod
⊢ ∃ (a : M), a ∈ L ∧ p ∣ a
have mp : ∀ (h : p ∣ prod []), ∃ (a : M), Membership.mem (γ := List M) [] a ∧ 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⟩
Cleared hypotheses: L, h
-- Lean 4 proof step from Mathlib.Data.List.Prime (goal)
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
⊢ ∃ (a : M), a ∈ L ∧ p ∣ a
have 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
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⟩
Cleared hypotheses: L, h
-- Lean 4 proof step from Mathlib.Data.List.Prime (goal)
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
⊢ p ∈ L
have obtain : ∀ (x : M) (hx1 : x ∈ L) (hx2 : p ∣ x), p ∈ L
Tactic: obtain ⟨x, hx1, hx2⟩ := hp.dvd_prod_iff.mp hpL
-- Lean 4 proof step from Mathlib.Data.List.Prime (hypothesis)
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
⊢ a :: l₁ ~ b :: l₂
have hl₁' : ∀ (p : M), p ∈ l₁ → Prime p
Tactic: have hl₁' : ∀ p ∈ l₁, Prime p := fun p hp => hl₁ p (mem_cons_of_mem _ hp)
-- Lean 4 proof step from Mathlib.Data.List.Prime (hypothesis)
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
⊢ a :: l₁ ~ b :: l₂
have hl₂' : ∀ (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)
-- Lean 4 proof step from Mathlib.Data.List.Prime (goal)
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
have rw : a ∣ a * l₁.prod
Tactic: rw [prod_cons]
-- Lean 4 proof step from Mathlib.Data.List.Prime (hypothesis)
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 :: l₁ ~ b :: l₂
have ha : 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 _ _)
-- Lean 4 proof step from Mathlib.Data.List.Prime (hypothesis)
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₂
⊢ a :: l₁ ~ b :: l₂
have hb : b :: l₂ ~ a :: (b :: l₂).erase a
Tactic: have hb : b :: l₂ ~ a :: (b :: l₂).erase a := perm_cons_erase ha
-- Lean 4 proof step from Mathlib.Data.List.Prime (goal)
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
⊢ a * l₁.prod = a * ((b :: l₂).erase a).prod
have rwa : (a :: l₁).prod = a * ((b :: l₂).erase a).prod
Tactic: rwa [← prod_cons, ← prod_cons, ← hb.prod_eq]
-- Lean 4 proof step from Mathlib.Data.List.Prime (goal)
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
⊢ a * l₁.prod = a * ((b :: l₂).erase a).prod
have rwa₁ : (a :: l₁).prod = (a :: (b :: l₂).erase a).prod
Tactic: rwa [← prod_cons, ← prod_cons, ← hb.prod_eq]