awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Sigma (goal)
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : CommMonoid β
r : Finset (γ × α)
s : Finset γ
t : γ → Finset α
h : ∀ (p : γ × α), p ∈ r ↔ p.1 ∈ s ∧ p.2 ∈ t p.1
f : γ × α → β
⊢ Eq.{u_4 + 1} (α := β) (∏ p ∈ r, f p)
    (∏ x ∈ s.sigma (α := fun (a : γ) ↦ α) t, f (x.fst (β := fun (a : γ) ↦ α), x.snd (β := fun (a : γ) ↦ α)))
have hst : ∀ (i : γ × α),
  i ∈ r ↔
    Membership.mem (α := (_ : γ) × α) (s.sigma (α := fun (a : γ) ↦ α) t)
      (((Equiv.sigmaEquivProd γ α).symm : (a : γ × α) → (_ : γ) × α) i : (_ : γ) × α)
Tactic: apply prod_equiv (Equiv.sigmaEquivProd _ _).symm
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Sigma (goal)
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : CommMonoid β
r : Finset (γ × α)
s : Finset γ
t : γ → Finset α
h : ∀ (p : γ × α), p ∈ r ↔ p.1 ∈ s ∧ p.2 ∈ t p.1
f : γ × α → β
hst :
  ∀ (i : γ × α),
    i ∈ r ↔
      Membership.mem (α := (_ : γ) × α) (s.sigma (α := fun (a : γ) ↦ α) t)
        (((Equiv.sigmaEquivProd γ α).symm : (a : γ × α) → (_ : γ) × α) i : (_ : γ) × α)
⊢ Eq.{u_4 + 1} (α := β) (∏ p ∈ r, f p)
    (∏ x ∈ s.sigma (α := fun (a : γ) ↦ α) t, f (x.fst (β := fun (a : γ) ↦ α), x.snd (β := fun (a : γ) ↦ α)))
have hfg : ∀ i ∈ r,
  f i =
    f
      (Sigma.fst (β := fun (a : γ) ↦ α) (((Equiv.sigmaEquivProd γ α).symm : (a : γ × α) → (_ : γ) × α) i),
        Sigma.snd (β := fun (a : γ) ↦ α) (((Equiv.sigmaEquivProd γ α).symm : (a : γ × α) → (_ : γ) × α) i))
Tactic: apply prod_equiv (Equiv.sigmaEquivProd _ _).symm
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Sigma (goal)
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : CommMonoid β
r : Finset (α × γ)
s : Finset γ
t : γ → Finset α
h : ∀ (p : α × γ), p ∈ r ↔ p.2 ∈ s ∧ p.1 ∈ t p.2
f : α × γ → β
⊢ Eq.{u_4 + 1} (α := β) (∏ p ∈ r, f p) (∏ c ∈ s, ∏ a ∈ t c, f (a, c))
have refine : Eq.{u_4 + 1} (α := β) (∏ p ∈ r, f p)
  (∏ x ∈ s.sigma (α := fun (a : γ) ↦ α) t, f (x.snd (β := fun (a : γ) ↦ α), x.fst (β := fun (a : γ) ↦ α)))
Tactic: refine Eq.trans ?_ (prod_sigma s t fun p => f (p.2, p.1))
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Sigma (goal)
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : CommMonoid β
r : Finset (α × γ)
s : Finset γ
t : γ → Finset α
h : ∀ (p : α × γ), p ∈ r ↔ p.2 ∈ s ∧ p.1 ∈ t p.2
f : α × γ → β
⊢ Eq.{u_4 + 1} (α := β) (∏ p ∈ r, f p)
    (∏ x ∈ s.sigma (α := fun (a : γ) ↦ α) t, f (x.snd (β := fun (a : γ) ↦ α), x.fst (β := fun (a : γ) ↦ α)))
have hst : ∀ (i : α × γ),
  i ∈ r ↔
    Membership.mem (α := (_ : γ) × α) (s.sigma (α := fun (a : γ) ↦ α) t)
      (((Equiv.prodComm α γ).trans (Equiv.sigmaEquivProd γ α).symm : (a : α × γ) → (_ : γ) × α) i : (_ : γ) × α)
Tactic: apply prod_equiv ((Equiv.prodComm _ _).trans (Equiv.sigmaEquivProd _ _).symm)
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Sigma (goal)
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : CommMonoid β
r : Finset (α × γ)
s : Finset γ
t : γ → Finset α
h : ∀ (p : α × γ), p ∈ r ↔ p.2 ∈ s ∧ p.1 ∈ t p.2
f : α × γ → β
hst :
  ∀ (i : α × γ),
    i ∈ r ↔
      Membership.mem (α := (_ : γ) × α) (s.sigma (α := fun (a : γ) ↦ α) t)
        (((Equiv.prodComm α γ).trans (Equiv.sigmaEquivProd γ α).symm : (a : α × γ) → (_ : γ) × α) i : (_ : γ) × α)
⊢ Eq.{u_4 + 1} (α := β) (∏ p ∈ r, f p)
    (∏ x ∈ s.sigma (α := fun (a : γ) ↦ α) t, f (x.snd (β := fun (a : γ) ↦ α), x.fst (β := fun (a : γ) ↦ α)))
have hfg : ∀ i ∈ r,
  f i =
    f
      (Sigma.snd (β := fun (a : γ) ↦ α)
          (((Equiv.prodComm α γ).trans (Equiv.sigmaEquivProd γ α).symm : (a : α × γ) → (_ : γ) × α) i),
        Sigma.fst (β := fun (a : γ) ↦ α)
          (((Equiv.prodComm α γ).trans (Equiv.sigmaEquivProd γ α).symm : (a : α × γ) → (_ : γ) × α) i))
Tactic: apply prod_equiv ((Equiv.prodComm _ _).trans (Equiv.sigmaEquivProd _ _).symm)
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Sigma (hypothesis)
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : CommMonoid β
s : Finset γ
t : γ → Finset α
t' : Finset α
s' : α → Finset γ
h : ∀ (x : γ) (y : α), x ∈ s ∧ y ∈ t x ↔ x ∈ s' y ∧ y ∈ t'
f : γ → α → β
⊢ Eq.{u_4 + 1} (α := β) (∏ x ∈ s, ∏ y ∈ t x, f x y) (∏ y ∈ t', ∏ x ∈ s' y, f x y)
have this : ∀ (z : γ × α),
  Membership.mem (γ := Finset (γ × α)) (s.biUnion fun (x : γ) ↦ map (Embedding.sectR x α) (t x)) z ↔
    z.1 ∈ s ∧ z.2 ∈ t z.1
Tactic: have : ∀ z : γ × α, (z ∈ s.biUnion fun x => (t x).map <| Function.Embedding.sectR x _) ↔
      z.1 ∈ s ∧ z.2 ∈ t z.1 := by
      rintro ⟨x, y⟩
      simp only [mem_biUnion, mem_map, Function.Embedding.sectR_apply, Prod.mk.injEq,
        exists_eq_right, ← and_assoc]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Sigma (goal)
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : CommMonoid β
s : Finset γ
t : γ → Finset α
t' : Finset α
s' : α → Finset γ
h : ∀ (x : γ) (y : α), x ∈ s ∧ y ∈ t x ↔ x ∈ s' y ∧ y ∈ t'
f : γ → α → β
⊢ Eq.{u_4 + 1} (α := β) (∏ x ∈ s, ∏ y ∈ t x, f x y) (∏ y ∈ t', ∏ x ∈ s' y, f x y)
have have : ∀ (z : γ × α),
  Membership.mem (γ := Finset (γ × α)) (s.biUnion fun (x : γ) ↦ map (Embedding.sectR x α) (t x)) z ↔
    z.1 ∈ s ∧ z.2 ∈ t z.1
Tactic: classical
    have : ∀ z : γ × α, (z ∈ s.biUnion fun x => (t x).map <| Function.Embedding.sectR x _) ↔
      z.1 ∈ s ∧ z.2 ∈ t z.1 := by
      rintro ⟨x, y⟩
      simp only [mem_biUnion, mem_map, Function.Embedding.sectR_apply, Prod.mk.injEq,
        exists_eq_right, ← and_assoc]
    exact
      (prod_finset_product' _ _ _ this).symm.trans
        ((prod_finset_product_right' _ _ _) fun ⟨x, y⟩ => (this _).trans ((h x y).trans and_comm))
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Sigma (goal)
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : CommMonoid β
s : Finset γ
t : γ → Finset α
t' : Finset α
s' : α → Finset γ
h : ∀ (x : γ) (y : α), x ∈ s ∧ y ∈ t x ↔ x ∈ s' y ∧ y ∈ t'
f : γ → α → β
have :
  ∀ (z : γ × α),
    Membership.mem (γ := Finset (γ × α)) (s.biUnion fun (x : γ) ↦ map (Embedding.sectR x α) (t x)) z ↔
      z.1 ∈ s ∧ z.2 ∈ t z.1
⊢ Eq.{u_4 + 1} (α := β) (∏ x ∈ s, ∏ y ∈ t x, f x y) (∏ y ∈ t', ∏ x ∈ s' y, f x y)
have have₁ : ∀
  (this :
    ∀ (z : γ × α),
      Membership.mem (γ := Finset (γ × α)) (s.biUnion fun (x : γ) ↦ map (Embedding.sectR x α) (t x)) z ↔
        z.1 ∈ s ∧ z.2 ∈ t z.1),
  Eq.{u_4 + 1} (α := β) (∏ x ∈ s, ∏ y ∈ t x, f x y) (∏ y ∈ t', ∏ x ∈ s' y, f x y)
Tactic: classical
    have : ∀ z : γ × α, (z ∈ s.biUnion fun x => (t x).map <| Function.Embedding.sectR x _) ↔
      z.1 ∈ s ∧ z.2 ∈ t z.1 := by
      rintro ⟨x, y⟩
      simp only [mem_biUnion, mem_map, Function.Embedding.sectR_apply, Prod.mk.injEq,
        exists_eq_right, ← and_assoc]
    exact
      (prod_finset_product' _ _ _ this).symm.trans
        ((prod_finset_product_right' _ _ _) fun ⟨x, y⟩ => (this _).trans ((h x y).trans and_comm))
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Sigma (goal)
Goal:
κ : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst : CommMonoid β
s : Finset γ
t : Finset α
u : Finset κ
f : γ → α → κ → β
⊢ Eq.{u_4 + 1} (α := β) (∏ x ∈ s, ∏ y ∈ t, ∏ z ∈ u, f x y z) (∏ z ∈ u, ∏ x ∈ s, ∏ y ∈ t, f x y z)
have simp_rw : Eq.{u_4 + 1} (α := β) (∏ x ∈ s, ∏ y ∈ u, ∏ x_1 ∈ t, f x x_1 y) (∏ z ∈ u, ∏ x ∈ s, ∏ y ∈ t, f x y z)
Tactic: simp_rw [prod_comm (s := t), prod_comm (s := s)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
M : Type u_4
N : Type u_5
inst : Monoid M
inst_1 : Monoid N
l : List M
F : Type u_8
inst_2 : FunLike F M N
inst_3 : MulHomClass F M N
f : F
hl_1 : l ≠ []
x : M
xs : List M
hl : x :: xs ≠ []
⊢ Eq.{u_5 + 1} (α := N) (prod (map (⇑f : (a : M) → N) (x :: xs)) : N) ((f : (a : M) → N) (x :: xs).prod : N)
have nil : ∀ (x : M) (hl : [x] ≠ []),
  Eq.{u_5 + 1} (α := N) (prod (map (⇑f : (a : M) → N) [x]) : N) ((f : (a : M) → N) [x].prod : N)
Tactic: induction xs generalizing x
Cleared hypotheses: x, xs, hl
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
M : Type u_4
N : Type u_5
inst : Monoid M
inst_1 : Monoid N
l : List M
F : Type u_8
inst_2 : FunLike F M N
inst_3 : MulHomClass F M N
f : F
hl_1 : l ≠ []
x : M
xs : List M
hl : x :: xs ≠ []
nil :
  ∀ (x : M) (hl : [x] ≠ []),
    Eq.{u_5 + 1} (α := N) (prod (map (⇑f : (a : M) → N) [x]) : N) ((f : (a : M) → N) [x].prod : N)
⊢ Eq.{u_5 + 1} (α := N) (prod (map (⇑f : (a : M) → N) (x :: xs)) : N) ((f : (a : M) → N) (x :: xs).prod : N)
have cons : ∀ (head : M) (tail : List M),
  (∀ (x : M) (hl : x :: tail ≠ []),
      Eq.{u_5 + 1} (α := N) (prod (map (⇑f : (a : M) → N) (x :: tail)) : N) ((f : (a : M) → N) (x :: tail).prod : N)) →
    ∀ (x : M) (hl : x :: head :: tail ≠ []),
      Eq.{u_5 + 1} (α := N) (prod (map (⇑f : (a : M) → N) (x :: head :: tail)) : N)
        ((f : (a : M) → N) (x :: head :: tail).prod : N)
Tactic: induction xs generalizing x
Cleared hypotheses: x, xs, hl
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
M : Type u_4
N : Type u_5
inst : Monoid M
inst_1 : Monoid N
l : List M
F : Type u_8
inst_2 : FunLike F M N
inst_3 : MonoidHomClass F M N
f : F
⊢ Eq.{u_5 + 1} (α := N) (prod (map (⇑f : (a : M) → N) l) : N) ((f : (a : M) → N) l.prod : N)
have simp : Eq.{u_5 + 1} (α := N)
  (foldr (fun (x : M) (y : N) ↦ HMul.hMul (α := N) ((f : (a : M) → N) x : N) y) ((f : (a : M) → N) 1) l : N)
  ((f : (a : M) → N) (foldr (fun (x1 x2 : M) ↦ x1 * x2) 1 l) : N)
Tactic: simp only [prod, foldr_map, ← map_one f]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
N : Type u_5
P : Type u_6
inst : Monoid M
inst_1 : Monoid N
inst_2 : Monoid P
l : List ι
f : M → N → P
hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d
f₁ : ι → M
f₂ : ι → N
hl_1 : l ≠ []
x : ι
xs : List ι
hl : x :: xs ≠ []
⊢ prod (map (fun (i : ι) ↦ f (f₁ i) (f₂ i)) (x :: xs)) = f (map f₁ (x :: xs)).prod (map f₂ (x :: xs)).prod
have nil : ∀ (x : ι) (hl : [x] ≠ []), prod (map (fun (i : ι) ↦ f (f₁ i) (f₂ i)) [x]) = f (map f₁ [x]).prod (map f₂ [x]).prod
Tactic: induction xs generalizing x
Cleared hypotheses: x, xs, hl
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
N : Type u_5
P : Type u_6
inst : Monoid M
inst_1 : Monoid N
inst_2 : Monoid P
l : List ι
f : M → N → P
hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d
f₁ : ι → M
f₂ : ι → N
hl_1 : l ≠ []
x : ι
xs : List ι
hl : x :: xs ≠ []
nil : ∀ (x : ι) (hl : [x] ≠ []), prod (map (fun (i : ι) ↦ f (f₁ i) (f₂ i)) [x]) = f (map f₁ [x]).prod (map f₂ [x]).prod
⊢ prod (map (fun (i : ι) ↦ f (f₁ i) (f₂ i)) (x :: xs)) = f (map f₁ (x :: xs)).prod (map f₂ (x :: xs)).prod
have cons : ∀ (head : ι) (tail : List ι),
  (∀ (x : ι) (hl : x :: tail ≠ []),
      prod (map (fun (i : ι) ↦ f (f₁ i) (f₂ i)) (x :: tail)) = f (map f₁ (x :: tail)).prod (map f₂ (x :: tail)).prod) →
    ∀ (x : ι) (hl : x :: head :: tail ≠ []),
      prod (map (fun (i : ι) ↦ f (f₁ i) (f₂ i)) (x :: head :: tail)) =
        f (map f₁ (x :: head :: tail)).prod (map f₂ (x :: head :: tail)).prod
Tactic: induction xs generalizing x
Cleared hypotheses: x, xs, hl
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
N : Type u_5
P : Type u_6
inst : Monoid M
inst_1 : Monoid N
inst_2 : Monoid P
l : List ι
f : M → N → P
hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d
hf' : f 1 1 = 1
f₁ : ι → M
f₂ : ι → N
⊢ prod (map (fun (i : ι) ↦ f (f₁ i) (f₂ i)) l) = f (map f₁ l).prod (map f₂ l).prod
have simp : foldr (fun (x : ι) (y : P) ↦ f (f₁ x) (f₂ x) * y) 1 l =
  f (foldr (fun (x : ι) (y : M) ↦ f₁ x * y) 1 l) (foldr (fun (x : ι) (y : N) ↦ f₂ x * y) 1 l)
Tactic: simp only [prod_eq_foldr, foldr_map]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
N : Type u_5
P : Type u_6
inst : Monoid M
inst_1 : Monoid N
inst_2 : Monoid P
l : List ι
f : M → N → P
hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d
hf' : f 1 1 = 1
f₁ : ι → M
f₂ : ι → N
⊢ foldr (fun (x : ι) (y : P) ↦ f (f₁ x) (f₂ x) * y) 1 l =
    f (foldr (fun (x : ι) (y : M) ↦ f₁ x * y) 1 l) (foldr (fun (x : ι) (y : N) ↦ f₂ x * y) 1 l)
have rw : foldr (fun (x : ι) (y : P) ↦ f (f₁ x) (f₂ x) * y) 1 l = foldr (fun (x : ι) (y : P) ↦ f (f₁ x) (f₂ x) * y) (f 1 1) l
Tactic: rw [← foldr_hom₂ l f _ _ ((fun x y => f (f₁ x) (f₂ x) * y)) _ _ (by simp [hf]), hf']
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
N : Type u_5
P : Type u_6
inst : Monoid M
inst_1 : Monoid N
inst_2 : Monoid P
l : List ι
f : M → N → P
hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d
hf' : f 1 1 = 1
f₁ : ι → M
f₂ : ι → N
rw : foldr (fun (x : ι) (y : P) ↦ f (f₁ x) (f₂ x) * y) 1 l = foldr (fun (x : ι) (y : P) ↦ f (f₁ x) (f₂ x) * y) (f 1 1) l
⊢ foldr (fun (x : ι) (y : P) ↦ f (f₁ x) (f₂ x) * y) 1 l =
    f (foldr (fun (x : ι) (y : M) ↦ f₁ x * y) 1 l) (foldr (fun (x : ι) (y : N) ↦ f₂ x * y) 1 l)
have rw₁ : Eq.{u_6 + 1} (α := P) (foldr (fun (x : ι) (y : P) ↦ f (f₁ x) (f₂ x) * y) 1 l)
  (foldr (fun (x : ι) (y : P) ↦ f (f₁ x) (f₂ x) * y) 1 l)
Tactic: rw [← foldr_hom₂ l f _ _ ((fun x y => f (f₁ x) (f₂ x) * y)) _ _ (by simp [hf]), hf']
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
N : Type u_5
inst : Monoid M
inst_1 : Monoid N
L : List ι
f : ι → M
G : Type u_8
inst_2 : FunLike G M N
inst_3 : MonoidHomClass G M N
g : G
⊢ Eq.{u_5 + 1} (α := N) (prod (map ((⇑g : (a : M) → N) ∘ f) L) : N) ((g : (a : M) → N) (map f L).prod : N)
have rw : Eq.{u_5 + 1} (α := N) (prod (map ((⇑g : (a : M) → N) ∘ f) L)) (prod (map (⇑g : (a : M) → N) (map f L)))
Tactic: rw [← prod_hom, map_map]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
N : Type u_5
inst : Monoid M
inst_1 : Monoid N
L : List ι
f : ι → M
G : Type u_8
inst_2 : FunLike G M N
inst_3 : MonoidHomClass G M N
g : G
rw : Eq.{u_5 + 1} (α := N) (prod (map ((⇑g : (a : M) → N) ∘ f) L)) (prod (map (⇑g : (a : M) → N) (map f L)))
⊢ Eq.{u_5 + 1} (α := N) (prod (map ((⇑g : (a : M) → N) ∘ f) L) : N) ((g : (a : M) → N) (map f L).prod : N)
have rw₁ : Eq.{u_5 + 1} (α := N) (prod (map ((⇑g : (a : M) → N) ∘ f) L)) (prod (map ((⇑g : (a : M) → N) ∘ f) L))
Tactic: rw [← prod_hom, map_map]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
M : Type u_4
inst : Monoid M
L : List M
i : ℕ
p : i < L.length
⊢ (take (i + 1) L).prod = (take i L).prod * getElem (valid := fun (as : List M) (i : ℕ) ↦ i < as.length) L i p
have rw : (take i L).prod * [getElem (valid := fun (as : List M) (i : ℕ) ↦ i < as.length) L i p].prod =
  (take i L).prod * getElem (valid := fun (as : List M) (i : ℕ) ↦ i < as.length) L i p
Tactic: rw [← take_concat_get' _ _ p, prod_append]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
M : Type u_4
inst : Monoid M
L : List M
h : L.prod ≠ 1
⊢ 0 < L.length
have nil : ∀ (h : Ne.{u_4 + 1} (α := M) (prod []) 1), 0 < length.{u_4} (α := M) []
Tactic: cases L
Cleared hypotheses: L, h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
M : Type u_4
inst : Monoid M
L : List M
h : L.prod ≠ 1
nil : ∀ (h : Ne.{u_4 + 1} (α := M) (prod []) 1), 0 < length.{u_4} (α := M) []
⊢ 0 < L.length
have cons : ∀ (head : M) (tail : List M) (h : (head :: tail).prod ≠ 1), 0 < (head :: tail).length
Tactic: cases L
Cleared hypotheses: L, h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
M : Type u_4
inst : Monoid M
l : List M
⊢ (getElem? (valid := fun (as : List M) (i : ℕ) ↦ i < as.length) l 0).getD 1 * l.tail.prod = l.prod
have nil : (getElem? (valid := fun (as : List M) (i : ℕ) ↦ i < as.length) [] 0).getD 1 * prod (tail []) = prod []
Tactic: cases l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
M : Type u_4
inst : Monoid M
l : List M
nil : (getElem? (valid := fun (as : List M) (i : ℕ) ↦ i < as.length) [] 0).getD 1 * prod (tail []) = prod []
⊢ (getElem? (valid := fun (as : List M) (i : ℕ) ↦ i < as.length) l 0).getD 1 * l.tail.prod = l.prod
have cons : ∀ (head : M) (tail : List M),
  (getElem? (valid := fun (as : List M) (i : ℕ) ↦ i < as.length) (head :: tail) 0).getD 1 * (head :: tail).tail.prod =
    (head :: tail).prod
Tactic: cases l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
M : Type u_4
inst : Monoid M
inst_1 : Inhabited M
l : List M
h : l ≠ []
⊢ l.headI * l.tail.prod = l.prod
have nil : ∀ (h : Ne.{u_4 + 1} (α := List M) [] []), HMul.hMul (α := M) (headI []) (prod (tail [])) = prod []
Tactic: cases l
Cleared hypotheses: l, h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
M : Type u_4
inst : Monoid M
inst_1 : Inhabited M
l : List M
h : l ≠ []
nil : ∀ (h : Ne.{u_4 + 1} (α := List M) [] []), HMul.hMul (α := M) (headI []) (prod (tail [])) = prod []
⊢ l.headI * l.tail.prod = l.prod
have cons : ∀ (head : M) (tail : List M) (h : head :: tail ≠ []),
  (head :: tail).headI * (head :: tail).tail.prod = (head :: tail).prod
Tactic: cases l
Cleared hypotheses: l, h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
M : Type u_4
inst : Monoid M
inst_1 : Inhabited M
l : List M
h : l ≠ []
⊢ l.headI * l.tail.prod = l.prod
have nil : ∀ (h : Ne.{u_4 + 1} (α := List M) [] []), HMul.hMul (α := M) (headI []) (prod (tail [])) = prod []
Tactic: cases l <;> [contradiction; simp]
Cleared hypotheses: l, h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
M : Type u_4
inst : Monoid M
inst_1 : Inhabited M
l : List M
h : l ≠ []
nil : ∀ (h : Ne.{u_4 + 1} (α := List M) [] []), HMul.hMul (α := M) (headI []) (prod (tail [])) = prod []
⊢ l.headI * l.tail.prod = l.prod
have cons : ∀ (head : M) (tail : List M) (h : head :: tail ≠ []),
  (head :: tail).headI * (head :: tail).tail.prod = (head :: tail).prod
Tactic: cases l <;> [contradiction; simp]
Cleared hypotheses: l, h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (hypothesis)
Goal:
M : Type u_4
inst : Monoid M
y z : M
l : List M
IH : ∀ (h : ∀ (x : M), x ∈ l → Commute y x), Commute y l.prod
h : ∀ (x : M), x ∈ z :: l → Commute y x
⊢ Commute y (z :: l).prod
have h₁ : Commute y z ∧ ∀ (x : M), x ∈ l → Commute y x
Tactic: rw [List.forall_mem_cons] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
M : Type u_4
inst : Monoid M
y z : M
l : List M
IH : ∀ (h : ∀ (x : M), x ∈ l → Commute y x), Commute y l.prod
h : Commute y z ∧ ∀ (x : M), x ∈ l → Commute y x
⊢ Commute y (z :: l).prod
have cons : Commute y (z * l.prod)
Tactic: rw [List.prod_cons]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
M : Type u_4
inst : Monoid M
l : List M
y : M
h : ∀ (x : M), x ∈ l → Commute y x
⊢ Commute y l.prod
have nil : ∀ (h : ∀ (x : M), Membership.mem (γ := List M) [] x → Commute y x), Commute y (prod [])
Tactic: induction l with
  | nil => simp
  | cons z l IH =>
    rw [List.forall_mem_cons] at h
    rw [List.prod_cons]
    exact Commute.mul_right h.1 (IH h.2)
Cleared hypotheses: l, h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
M : Type u_4
inst : Monoid M
l : List M
y : M
h : ∀ (x : M), x ∈ l → Commute y x
nil : ∀ (h : ∀ (x : M), Membership.mem (γ := List M) [] x → Commute y x), Commute y (prod [])
⊢ Commute y l.prod
have cons : ∀ (z : M) (l : List M) (IH : ∀ (h : ∀ (x : M), x ∈ l → Commute y x), Commute y l.prod)
  (h : ∀ (x : M), x ∈ z :: l → Commute y x), Commute y (z :: l).prod
Tactic: induction l with
  | nil => simp
  | cons z l IH =>
    rw [List.forall_mem_cons] at h
    rw [List.prod_cons]
    exact Commute.mul_right h.1 (IH h.2)
Cleared hypotheses: l, h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
M : Type u_4
inst : Monoid M
f : ℕ → M
n : ℕ
⊢ (map f (range n.succ)).prod = (map f (range n)).prod * f n
have rw : (map f (range n ++ [n])).prod = (map f (range n)).prod * f n
Tactic: rw [range_succ, map_append, map_singleton, prod_append, prod_cons, prod_nil, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
M : Type u_4
inst : Monoid M
f : ℕ → M
n : ℕ
rw : (map f (range n ++ [n])).prod = (map f (range n)).prod * f n
⊢ (map f (range n.succ)).prod = (map f (range n)).prod * f n
have rw₁ : (map f (range n) ++ map f [n]).prod = (map f (range n)).prod * f n
Tactic: rw [range_succ, map_append, map_singleton, prod_append, prod_cons, prod_nil, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
M : Type u_4
inst : Monoid M
f : ℕ → M
n : ℕ
rw : (map f (range n ++ [n])).prod = (map f (range n)).prod * f n
rw₁ : (map f (range n) ++ map f [n]).prod = (map f (range n)).prod * f n
⊢ (map f (range n.succ)).prod = (map f (range n)).prod * f n
have rw₂ : (map f (range n) ++ [f n]).prod = (map f (range n)).prod * f n
Tactic: rw [range_succ, map_append, map_singleton, prod_append, prod_cons, prod_nil, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
M : Type u_4
inst : Monoid M
f : ℕ → M
n : ℕ
rw : (map f (range n ++ [n])).prod = (map f (range n)).prod * f n
rw₁ : (map f (range n) ++ map f [n]).prod = (map f (range n)).prod * f n
rw₂ : (map f (range n) ++ [f n]).prod = (map f (range n)).prod * f n
⊢ (map f (range n.succ)).prod = (map f (range n)).prod * f n
have rw₃ : (map f (range n)).prod * [f n].prod = (map f (range n)).prod * f n
Tactic: rw [range_succ, map_append, map_singleton, prod_append, prod_cons, prod_nil, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
M : Type u_4
inst : Monoid M
f : ℕ → M
n : ℕ
rw : (map f (range n ++ [n])).prod = (map f (range n)).prod * f n
rw₁ : (map f (range n) ++ map f [n]).prod = (map f (range n)).prod * f n
rw₂ : (map f (range n) ++ [f n]).prod = (map f (range n)).prod * f n
rw₃ : (map f (range n)).prod * [f n].prod = (map f (range n)).prod * f n
⊢ (map f (range n.succ)).prod = (map f (range n)).prod * f n
have rw₄ : (map f (range n)).prod * (f n * prod []) = (map f (range n)).prod * f n
Tactic: rw [range_succ, map_append, map_singleton, prod_append, prod_cons, prod_nil, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
M : Type u_4
inst : Monoid M
f : ℕ → M
n : ℕ
rw : (map f (range n ++ [n])).prod = (map f (range n)).prod * f n
rw₁ : (map f (range n) ++ map f [n]).prod = (map f (range n)).prod * f n
rw₂ : (map f (range n) ++ [f n]).prod = (map f (range n)).prod * f n
rw₃ : (map f (range n)).prod * [f n].prod = (map f (range n)).prod * f n
rw₄ : (map f (range n)).prod * (f n * prod []) = (map f (range n)).prod * f n
⊢ (map f (range n.succ)).prod = (map f (range n)).prod * f n
have rw₅ : (map f (range n)).prod * (f n * 1) = (map f (range n)).prod * f n
Tactic: rw [range_succ, map_append, map_singleton, prod_append, prod_cons, prod_nil, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
M : Type u_4
inst : Monoid M
f : ℕ → M
n : ℕ
rw : (map f (range n ++ [n])).prod = (map f (range n)).prod * f n
rw₁ : (map f (range n) ++ map f [n]).prod = (map f (range n)).prod * f n
rw₂ : (map f (range n) ++ [f n]).prod = (map f (range n)).prod * f n
rw₃ : (map f (range n)).prod * [f n].prod = (map f (range n)).prod * f n
rw₄ : (map f (range n)).prod * (f n * prod []) = (map f (range n)).prod * f n
rw₅ : (map f (range n)).prod * (f n * 1) = (map f (range n)).prod * f n
⊢ (map f (range n.succ)).prod = (map f (range n)).prod * f n
have rw₆ : (map f (range n)).prod * f n = (map f (range n)).prod * f n
Tactic: rw [range_succ, map_append, map_singleton, prod_append, prod_cons, prod_nil, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
M : Type u_4
inst : Monoid M
f : ℕ → M
n : ℕ
⊢ (map f (range n.succ)).prod = f 0 * prod (map (fun (i : ℕ) ↦ f i.succ) (range n))
have rw : (map f (0 :: map Nat.succ (range n))).prod = f 0 * prod (map (fun (i : ℕ) ↦ f i.succ) (range n))
Tactic: rw [range_succ_eq_map]