awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Nat (goal)
Goal:
z : ℤ
hz : (normalize : (a : ℤ) → ℤ) z = z
pos : ∀ (h : 0 ≤ z), 0 ≤ z
⊢ 0 ≤ z
have neg : ∀ (h : z < 0), 0 ≤ z
Tactic: by_cases! h : 0 ≤ z
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Nat (hypothesis)
Goal:
z : ℤ
hz : (normalize : (a : ℤ) → ℤ) z = z
h : z < 0
⊢ 0 ≤ z
have hz₁ : -z = z
Tactic: rw [normalize_of_nonpos h.le] at hz
Cleared hypotheses: hz, h
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Nat (goal)
Goal:
a b : ℤ
⊢ Associated (HMul.hMul (α := ℤ) (↑(a.gcd b) : ℤ) (↑(a.lcm b) : ℤ)) (a * b)
have rw : Associated ((normalize : (a : ℤ) → ℤ) (a * b)) (a * b)
Tactic: rw [← Int.natCast_mul, gcd_mul_lcm, ← natAbs_mul, natCast_natAbs, abs_eq_normalize]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Nat (goal)
Goal:
a : ℤ
⊢ ∃ (u : ℤ), ∃ (x : IsUnit u), (↑a.natAbs : ℤ) = u * a
have inl : ∀ (h : a = (↑a.natAbs : ℤ)), ∃ (u : ℤ), ∃ (x : IsUnit u), (↑a.natAbs : ℤ) = u * a
Tactic: rcases natAbs_eq a with h | h
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Nat (goal)
Goal:
a : ℤ
inl : ∀ (h : a = (↑a.natAbs : ℤ)), ∃ (u : ℤ), ∃ (x : IsUnit u), (↑a.natAbs : ℤ) = u * a
⊢ ∃ (u : ℤ), ∃ (x : IsUnit u), (↑a.natAbs : ℤ) = u * a
have inr : ∀ (h : a = -(↑a.natAbs : ℤ)), ∃ (u : ℤ), ∃ (x : IsUnit u), (↑a.natAbs : ℤ) = u * a
Tactic: rcases natAbs_eq a with h | h
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Nat (goal)
Goal:
a : ℤ
h : a = (↑a.natAbs : ℤ)
⊢ ∃ (u : ℤ), ∃ (x : IsUnit u), (↑a.natAbs : ℤ) = u * a
have h₁ : (↑a.natAbs : ℤ) = 1 * a
Tactic: use 1, isUnit_one
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Nat (goal)
Goal:
a : ℤ
h : a = (↑a.natAbs : ℤ)
⊢ (↑a.natAbs : ℤ) = 1 * a
have h₁ : a = 1 * a
Tactic: rw [← h, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Nat (goal)
Goal:
a : ℤ
h : a = (↑a.natAbs : ℤ)
h₁ : a = 1 * a
⊢ (↑a.natAbs : ℤ) = 1 * a
have h₂ : a = a
Tactic: rw [← h, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Nat (goal)
Goal:
a : ℤ
h : a = -(↑a.natAbs : ℤ)
⊢ ∃ (u : ℤ), ∃ (x : IsUnit u), (↑a.natAbs : ℤ) = u * a
have h₁ : (↑a.natAbs : ℤ) = -1 * a
Tactic: use -1, isUnit_one.neg
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Nat (goal)
Goal:
a : ℤ
h : a = -(↑a.natAbs : ℤ)
⊢ (↑a.natAbs : ℤ) = -1 * a
have h₁ : -a = -1 * a
Tactic: rw [← neg_eq_iff_eq_neg.mpr h]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Nat (goal)
Goal:
⊢ Associates ℤ ≃ ℕ
have refine_1 : Function.LeftInverse (fun (x : ℕ) ↦ Associates.mk (↑x : ℤ)) fun (x : Associates ℤ) ↦ x.out.natAbs
Tactic: refine ⟨(·.out.natAbs), (Associates.mk ·), ?_, fun n ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Nat (goal)
Goal:
refine_1 : Function.LeftInverse (fun (x : ℕ) ↦ Associates.mk (↑x : ℤ)) fun (x : Associates ℤ) ↦ x.out.natAbs
⊢ Associates ℤ ≃ ℕ
have refine_2 : ∀ (n : ℕ), (fun (x : Associates ℤ) ↦ x.out.natAbs) ((fun (x : ℕ) ↦ (Associates.mk (↑x : ℤ) : Associates ℤ)) n) = n
Tactic: refine ⟨(·.out.natAbs), (Associates.mk ·), ?_, fun n ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Nat (goal)
Goal:
⊢ Function.LeftInverse (fun (x : ℕ) ↦ Associates.mk (↑x : ℤ)) fun (x : Associates ℤ) ↦ x.out.natAbs
have refine_1 : ∀ (a : ℤ),
  Eq (α := Associates ℤ)
    ((fun (x : ℕ) ↦ (Associates.mk (↑x : ℤ) : Associates ℤ))
      ((fun (x : Associates ℤ) ↦ x.out.natAbs) (Associates.mk a)))
    (Associates.mk a)
Tactic: refine Associates.forall_associated.2 fun a ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Nat (goal)
Goal:
a : ℤ
⊢ Eq (α := Associates ℤ)
    ((fun (x : ℕ) ↦ (Associates.mk (↑x : ℤ) : Associates ℤ))
      ((fun (x : Associates ℤ) ↦ x.out.natAbs) (Associates.mk a)))
    (Associates.mk a)
have refine_1 : a * (↑(normUnit a) : ℤ) = (↑((fun (x : Associates ℤ) ↦ x.out.natAbs) (Associates.mk a)) : ℤ)
Tactic: refine Associates.mk_eq_mk_iff_associated.2 <| Associated.symm <| ⟨normUnit a, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Nat (goal)
Goal:
n : ℕ
⊢ Int.natAbs ((normalize : (a : ℤ) → ℤ) (↑n : ℤ)) = n
have refine_2 : Int.natAbs |(↑n : ℤ)| = n
Tactic: rw [← Int.abs_eq_normalize, Int.natAbs_abs, Int.natAbs_natCast]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Nat (goal)
Goal:
n : ℕ
refine_2 : Int.natAbs |(↑n : ℤ)| = n
⊢ Int.natAbs ((normalize : (a : ℤ) → ℤ) (↑n : ℤ)) = n
have refine_2₁ : Int.natAbs (↑n : ℤ) = n
Tactic: rw [← Int.abs_eq_normalize, Int.natAbs_abs, Int.natAbs_natCast]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Nat (goal)
Goal:
n : ℕ
refine_2 : Int.natAbs |(↑n : ℤ)| = n
refine_2₁ : Int.natAbs (↑n : ℤ) = n
⊢ Int.natAbs ((normalize : (a : ℤ) → ℤ) (↑n : ℤ)) = n
have refine_2₂ : n = n
Tactic: rw [← Int.abs_eq_normalize, Int.natAbs_abs, Int.natAbs_natCast]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Nat (goal)
Goal:
a b : ℤ
⊢ Associated a b ↔ a.natAbs = b.natAbs
have rw : Associated a.natAbs b.natAbs ↔ a.natAbs = b.natAbs
Tactic: rw [← dvd_dvd_iff_associated, ← Int.natAbs_dvd_natAbs, ← Int.natAbs_dvd_natAbs,
    dvd_dvd_iff_associated]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Nat (goal)
Goal:
a b : ℤ
⊢ Associated a b ↔ a = b ∨ a = -b
have rw : a.natAbs = b.natAbs ↔ a = b ∨ a = -b
Tactic: rw [Int.associated_iff_natAbs]
-- Lean 4 proof step from Mathlib.Algebra.GradedMonoid (goal)
Goal:
ι : Type u_1
α : Type u_2
A : ι → Type u_3
inst : AddMonoid ι
inst_1 : GMonoid A
l : List α
fι : α → ι
fA : (a : α) → A (fι a)
⊢ mk (A := A) (List.dProdIndex [] fι) (List.dProd (A := A) [] fι fA) =
    List.prod (List.map (fun (a : α) ↦ mk (A := A) (fι a) (fA a)) [])
have simp : Eq (α := GradedMonoid A) (mk (A := A) 0 (GOne.one (A := A))) 1
Tactic: simp only [List.dProdIndex_nil, List.dProd_nil, List.map_nil, List.prod_nil]
-- Lean 4 proof step from Mathlib.Algebra.GradedMonoid (goal)
Goal:
ι : Type u_1
α : Type u_2
A : ι → Type u_3
inst : AddMonoid ι
inst_1 : GMonoid A
l : List α
f : α → GradedMonoid A
⊢ (List.map f l).prod =
    mk (A := A) (l.dProdIndex fun (i : α) ↦ (f i).fst (β := A))
      (l.dProd (A := A) (fun (i : α) ↦ (f i).fst (β := A)) fun (i : α) ↦ (f i).snd (β := A))
have rw : (List.map f l).prod = List.prod (List.map (fun (a : α) ↦ Sigma.mk (β := A) ((f a).fst (β := A)) ((f a).snd (β := A))) l)
Tactic: rw [GradedMonoid.mk_list_dProd, GradedMonoid.mk]
-- Lean 4 proof step from Mathlib.Algebra.GradedMonoid (goal)
Goal:
ι : Type u_1
A : ι → Type u_3
inst : AddMonoid ι
inst_1 : GMonoid A
n : ℕ
f : Fin n → GradedMonoid A
⊢ (List.ofFn f).prod =
    mk (A := A) ((List.finRange n).dProdIndex fun (i : Fin n) ↦ (f i).fst (β := A))
      ((List.finRange n).dProd (A := A) (fun (i : Fin n) ↦ (f i).fst (β := A)) fun (i : Fin n) ↦ (f i).snd (β := A))
have rw : (List.map f (List.finRange n)).prod =
  mk (A := A) ((List.finRange n).dProdIndex fun (i : Fin n) ↦ (f i).fst (β := A))
    ((List.finRange n).dProd (A := A) (fun (i : Fin n) ↦ (f i).fst (β := A)) fun (i : Fin n) ↦ (f i).snd (β := A))
Tactic: rw [List.ofFn_eq_map, GradedMonoid.list_prod_map_eq_dProd]
-- Lean 4 proof step from Mathlib.Algebra.GradedMonoid (goal)
Goal:
ι : Type u_1
A : ι → Type u_3
inst : AddMonoid ι
inst_1 : GMonoid A
n : ℕ
f : Fin n → GradedMonoid A
rw :
  (List.map f (List.finRange n)).prod =
    mk (A := A) ((List.finRange n).dProdIndex fun (i : Fin n) ↦ (f i).fst (β := A))
      ((List.finRange n).dProd (A := A) (fun (i : Fin n) ↦ (f i).fst (β := A)) fun (i : Fin n) ↦ (f i).snd (β := A))
⊢ (List.ofFn f).prod =
    mk (A := A) ((List.finRange n).dProdIndex fun (i : Fin n) ↦ (f i).fst (β := A))
      ((List.finRange n).dProd (A := A) (fun (i : Fin n) ↦ (f i).fst (β := A)) fun (i : Fin n) ↦ (f i).snd (β := A))
have rw₁ : Eq (α := GradedMonoid A)
  (mk (A := A) ((List.finRange n).dProdIndex fun (i : Fin n) ↦ (f i).fst (β := A))
    ((List.finRange n).dProd (A := A) (fun (i : Fin n) ↦ (f i).fst (β := A)) fun (i : Fin n) ↦ (f i).snd (β := A)))
  (mk (A := A) ((List.finRange n).dProdIndex fun (i : Fin n) ↦ (f i).fst (β := A))
    ((List.finRange n).dProd (A := A) (fun (i : Fin n) ↦ (f i).fst (β := A)) fun (i : Fin n) ↦ (f i).snd (β := A)))
Tactic: rw [List.ofFn_eq_map, GradedMonoid.list_prod_map_eq_dProd]
-- Lean 4 proof step from Mathlib.Algebra.GradedMonoid (goal)
Goal:
ι : Type u_1
R : Type u_2
α : Type u_3
inst : AddMonoid ι
inst_1 : Monoid R
l : List α
fι : α → ι
fA : α → R
⊢ dProd (A := fun (x : ι) ↦ R) [] fι fA = (map fA []).prod
have rw : Eq.{u_2 + 1} (α := R) (@GradedMonoid.GOne.one _ (fun (x : ι) ↦ R) AddZero.toZero _ : R) (1 : R)
Tactic: rw [List.dProd_nil, List.map_nil, List.prod_nil]
-- Lean 4 proof step from Mathlib.Algebra.GradedMonoid (goal)
Goal:
ι : Type u_1
R : Type u_2
α : Type u_3
inst : AddMonoid ι
inst_1 : Monoid R
l : List α
fι : α → ι
fA : α → R
head : α
tail : List α
⊢ (head :: tail).dProd (A := fun (x : ι) ↦ R) fι fA = (map fA (head :: tail)).prod
have rw : @GradedMonoid.GMul.mul _ (fun (x : ι) ↦ R) AddSemigroup.toAdd _ (fι head) (tail.dProdIndex fι) (fA head)
    (map fA tail).prod =
  fA head * (map fA tail).prod
Tactic: rw [List.dProd_cons, List.map_cons, List.prod_cons, List.dProd_monoid tail _ _]
-- Lean 4 proof step from Mathlib.Algebra.GradedMonoid (goal)
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : SetLike S R
inst_1 : Monoid R
inst_2 : AddMonoid ι
A : ι → S
inst_3 : GradedMonoid A
n : ℕ
r : R
i : ι
h : r ∈ A i
⊢ HPow.hPow (β := ℕ) r 0 ∈ A (HSMul.hSMul (α := ℕ) 0 i)
have rw : 1 ∈ A 0
Tactic: rw [pow_zero, zero_nsmul]
-- Lean 4 proof step from Mathlib.Algebra.GradedMonoid (goal)
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : SetLike S R
inst_1 : Monoid R
inst_2 : AddMonoid ι
A : ι → S
inst_3 : GradedMonoid A
n_1 : ℕ
r : R
i : ι
h : r ∈ A i
n : ℕ
⊢ r ^ (n + 1) ∈ A ((n + 1) • i)
have rw : r * r ^ n ∈ A (i + n • i)
Tactic: rw [pow_succ', succ_nsmul']
-- Lean 4 proof step from Mathlib.Algebra.GradedMonoid (goal)
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : SetLike S R
inst_1 : Monoid R
inst_2 : AddMonoid ι
A : ι → S
inst_3 : GradedMonoid A
ι' : Type u_4
l : List ι'
i : ι' → ι
r : ι' → R
h : ∀ (j : ι'), Membership.mem (γ := List ι') [] j → r j ∈ A (i j)
⊢ (List.map r []).prod ∈ A (List.map i []).sum
have rw : 1 ∈ A 0
Tactic: rw [List.map_nil, List.map_nil, List.prod_nil, List.sum_nil]
-- Lean 4 proof step from Mathlib.Algebra.GradedMonoid (goal)
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : SetLike S R
inst_1 : Monoid R
inst_2 : AddMonoid ι
A : ι → S
inst_3 : GradedMonoid A
ι' : Type u_4
l : List ι'
i : ι' → ι
r : ι' → R
head : ι'
tail : List ι'
h : ∀ j ∈ head :: tail, r j ∈ A (i j)
⊢ (List.map r (head :: tail)).prod ∈ A (List.map i (head :: tail)).sum
have rw : r head * (List.map r tail).prod ∈ A (i head + (List.map i tail).sum)
Tactic: rw [List.map_cons, List.map_cons, List.prod_cons, List.sum_cons]
-- Lean 4 proof step from Mathlib.Algebra.GradedMonoid (goal)
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : SetLike S R
inst_1 : Monoid R
inst_2 : AddMonoid ι
A : ι → S
inst_3 : GradedMonoid A
n : ℕ
i : Fin n → ι
r : Fin n → R
h : ∀ (j : Fin n), r j ∈ A (i j)
⊢ (List.ofFn r).prod ∈ A (List.ofFn i).sum
have rw : (List.map r (List.finRange n)).prod ∈ A (List.map i (List.finRange n)).sum
Tactic: rw [List.ofFn_eq_map, List.ofFn_eq_map]
-- Lean 4 proof step from Mathlib.Algebra.GradedMonoid (goal)
Goal:
ι : Type u_1
R : Type u_2
α : Type u_3
S : Type u_4
inst : SetLike S R
inst_1 : Monoid R
inst_2 : AddMonoid ι
A : ι → S
inst_3 : GradedMonoid A
fι : α → ι
fA : (a : α) → ↥(A (fι a))
l : List α
⊢ Eq.{u_2 + 1} (α := R) (↑(List.dProd (A := fun (i : ι) ↦ ↥(A i)) [] fι fA) : R)
    (List.prod (List.map (fun (a : α) ↦ (↑(fA a) : R)) []))
have rw : Eq.{u_2 + 1} (α := R) (↑(@GradedMonoid.GOne.one _ (fun (i : ι) ↦ ↥(A i)) AddZero.toZero _ : ↥(A 0)) : R)
  (List.prod (List.map (fun (a : α) ↦ (↑(fA a) : R)) []))
Tactic: rw [List.dProd_nil, coe_gOne, List.map_nil, List.prod_nil]
-- Lean 4 proof step from Mathlib.Algebra.GradedMonoid (goal)
Goal:
ι : Type u_1
R : Type u_2
α : Type u_3
S : Type u_4
inst : SetLike S R
inst_1 : Monoid R
inst_2 : AddMonoid ι
A : ι → S
inst_3 : GradedMonoid A
fι : α → ι
fA : (a : α) → ↥(A (fι a))
l : List α
rw :
  Eq.{u_2 + 1} (α := R) (↑(@GradedMonoid.GOne.one _ (fun (i : ι) ↦ ↥(A i)) AddZero.toZero _ : ↥(A 0)) : R)
    (List.prod (List.map (fun (a : α) ↦ (↑(fA a) : R)) []))
⊢ Eq.{u_2 + 1} (α := R) (↑(List.dProd (A := fun (i : ι) ↦ ↥(A i)) [] fι fA) : R)
    (List.prod (List.map (fun (a : α) ↦ (↑(fA a) : R)) []))
have rw₁ : Eq.{u_2 + 1} (α := R) 1 (List.prod (List.map (fun (a : α) ↦ (↑(fA a) : R)) []))
Tactic: rw [List.dProd_nil, coe_gOne, List.map_nil, List.prod_nil]
-- Lean 4 proof step from Mathlib.Algebra.GradedMonoid (goal)
Goal:
ι : Type u_1
R : Type u_2
α : Type u_3
S : Type u_4
inst : SetLike S R
inst_1 : Monoid R
inst_2 : AddMonoid ι
A : ι → S
inst_3 : GradedMonoid A
fι : α → ι
fA : (a : α) → ↥(A (fι a))
l : List α
rw :
  Eq.{u_2 + 1} (α := R) (↑(@GradedMonoid.GOne.one _ (fun (i : ι) ↦ ↥(A i)) AddZero.toZero _ : ↥(A 0)) : R)
    (List.prod (List.map (fun (a : α) ↦ (↑(fA a) : R)) []))
rw₁ : Eq.{u_2 + 1} (α := R) 1 (List.prod (List.map (fun (a : α) ↦ (↑(fA a) : R)) []))
⊢ Eq.{u_2 + 1} (α := R) (↑(List.dProd (A := fun (i : ι) ↦ ↥(A i)) [] fι fA) : R)
    (List.prod (List.map (fun (a : α) ↦ (↑(fA a) : R)) []))
have rw₂ : Eq.{u_2 + 1} (α := R) 1 (List.prod [])
Tactic: rw [List.dProd_nil, coe_gOne, List.map_nil, List.prod_nil]
-- Lean 4 proof step from Mathlib.Algebra.GradedMonoid (goal)
Goal:
ι : Type u_1
R : Type u_2
α : Type u_3
S : Type u_4
inst : SetLike S R
inst_1 : Monoid R
inst_2 : AddMonoid ι
A : ι → S
inst_3 : GradedMonoid A
fι : α → ι
fA : (a : α) → ↥(A (fι a))
l : List α
rw :
  Eq.{u_2 + 1} (α := R) (↑(@GradedMonoid.GOne.one _ (fun (i : ι) ↦ ↥(A i)) AddZero.toZero _ : ↥(A 0)) : R)
    (List.prod (List.map (fun (a : α) ↦ (↑(fA a) : R)) []))
rw₁ : Eq.{u_2 + 1} (α := R) 1 (List.prod (List.map (fun (a : α) ↦ (↑(fA a) : R)) []))
rw₂ : Eq.{u_2 + 1} (α := R) 1 (List.prod [])
⊢ Eq.{u_2 + 1} (α := R) (↑(List.dProd (A := fun (i : ι) ↦ ↥(A i)) [] fι fA) : R)
    (List.prod (List.map (fun (a : α) ↦ (↑(fA a) : R)) []))
have rw₃ : Eq.{u_2 + 1} (α := R) 1 1
Tactic: rw [List.dProd_nil, coe_gOne, List.map_nil, List.prod_nil]
-- Lean 4 proof step from Mathlib.Algebra.GradedMonoid (goal)
Goal:
ι : Type u_1
R : Type u_2
α : Type u_3
S : Type u_4
inst : SetLike S R
inst_1 : Monoid R
inst_2 : AddMonoid ι
A : ι → S
inst_3 : GradedMonoid A
fι : α → ι
fA : (a : α) → ↥(A (fι a))
l : List α
head : α
tail : List α
⊢ Eq.{u_2 + 1} (α := R) (↑((head :: tail).dProd (A := fun (i : ι) ↦ ↥(A i)) fι fA) : R)
    (List.prod (List.map (fun (a : α) ↦ (↑(fA a) : R)) (head :: tail)))
have rw : (↑(@GradedMonoid.GMul.mul _ (fun (i : ι) ↦ ↥(A i)) AddSemigroup.toAdd _ _ (tail.dProdIndex fι) (fA head)
          (tail.dProd (A := fun (i : ι) ↦ ↥(A i)) fι fA : ↥(A (tail.dProdIndex fι))) :
        ↥(A (fι head + tail.dProdIndex fι))) :
    R) =
  List.prod (List.map (fun (a : α) ↦ (↑(fA a) : R)) (head :: tail))
Tactic: rw [List.dProd_cons, coe_gMul, List.map_cons, List.prod_cons,
      SetLike.coe_list_dProd _ _ _ tail]
-- Lean 4 proof step from Mathlib.Algebra.GradedMonoid (goal)
Goal:
ι : Type u_1
R : Type u_2
α : Type u_3
S : Type u_4
inst : SetLike S R
inst_1 : Monoid R
inst_2 : AddMonoid ι
A : ι → S
inst_3 : GradedMonoid A
fι : α → ι
fA : (a : α) → ↥(A (fι a))
l : List α
head : α
tail : List α
rw :
  (↑(@GradedMonoid.GMul.mul _ (fun (i : ι) ↦ ↥(A i)) AddSemigroup.toAdd _ _ (tail.dProdIndex fι) (fA head)
            (tail.dProd (A := fun (i : ι) ↦ ↥(A i)) fι fA : ↥(A (tail.dProdIndex fι))) :
          ↥(A (fι head + tail.dProdIndex fι))) :
      R) =
    List.prod (List.map (fun (a : α) ↦ (↑(fA a) : R)) (head :: tail))
⊢ Eq.{u_2 + 1} (α := R) (↑((head :: tail).dProd (A := fun (i : ι) ↦ ↥(A i)) fι fA) : R)
    (List.prod (List.map (fun (a : α) ↦ (↑(fA a) : R)) (head :: tail)))
have rw₁ : (↑(fA head) : R) * (↑(tail.dProd (A := fun (i : ι) ↦ ↥(A i)) fι fA) : R) =
  List.prod (List.map (fun (a : α) ↦ (↑(fA a) : R)) (head :: tail))
Tactic: rw [List.dProd_cons, coe_gMul, List.map_cons, List.prod_cons,
      SetLike.coe_list_dProd _ _ _ tail]
-- Lean 4 proof step from Mathlib.Algebra.GradedMonoid (goal)
Goal:
ι : Type u_1
R : Type u_2
α : Type u_3
S : Type u_4
inst : SetLike S R
inst_1 : Monoid R
inst_2 : AddMonoid ι
A : ι → S
inst_3 : GradedMonoid A
fι : α → ι
fA : (a : α) → ↥(A (fι a))
l : List α
head : α
tail : List α
rw :
  (↑(@GradedMonoid.GMul.mul _ (fun (i : ι) ↦ ↥(A i)) AddSemigroup.toAdd _ _ (tail.dProdIndex fι) (fA head)
            (tail.dProd (A := fun (i : ι) ↦ ↥(A i)) fι fA : ↥(A (tail.dProdIndex fι))) :
          ↥(A (fι head + tail.dProdIndex fι))) :
      R) =
    List.prod (List.map (fun (a : α) ↦ (↑(fA a) : R)) (head :: tail))
rw₁ :
  (↑(fA head) : R) * (↑(tail.dProd (A := fun (i : ι) ↦ ↥(A i)) fι fA) : R) =
    List.prod (List.map (fun (a : α) ↦ (↑(fA a) : R)) (head :: tail))
⊢ Eq.{u_2 + 1} (α := R) (↑((head :: tail).dProd (A := fun (i : ι) ↦ ↥(A i)) fι fA) : R)
    (List.prod (List.map (fun (a : α) ↦ (↑(fA a) : R)) (head :: tail)))
have rw₂ : (↑(fA head) : R) * (↑(tail.dProd (A := fun (i : ι) ↦ ↥(A i)) fι fA) : R) =
  ((↑(fA head) : R) :: List.map (fun (a : α) ↦ (↑(fA a) : R)) tail).prod
Tactic: rw [List.dProd_cons, coe_gMul, List.map_cons, List.prod_cons,
      SetLike.coe_list_dProd _ _ _ tail]
-- Lean 4 proof step from Mathlib.Algebra.GradedMonoid (goal)
Goal:
ι : Type u_1
R : Type u_2
α : Type u_3
S : Type u_4
inst : SetLike S R
inst_1 : Monoid R
inst_2 : AddMonoid ι
A : ι → S
inst_3 : GradedMonoid A
fι : α → ι
fA : (a : α) → ↥(A (fι a))
l : List α
head : α
tail : List α
rw :
  (↑(@GradedMonoid.GMul.mul _ (fun (i : ι) ↦ ↥(A i)) AddSemigroup.toAdd _ _ (tail.dProdIndex fι) (fA head)
            (tail.dProd (A := fun (i : ι) ↦ ↥(A i)) fι fA : ↥(A (tail.dProdIndex fι))) :
          ↥(A (fι head + tail.dProdIndex fι))) :
      R) =
    List.prod (List.map (fun (a : α) ↦ (↑(fA a) : R)) (head :: tail))
rw₁ :
  (↑(fA head) : R) * (↑(tail.dProd (A := fun (i : ι) ↦ ↥(A i)) fι fA) : R) =
    List.prod (List.map (fun (a : α) ↦ (↑(fA a) : R)) (head :: tail))
rw₂ :
  (↑(fA head) : R) * (↑(tail.dProd (A := fun (i : ι) ↦ ↥(A i)) fι fA) : R) =
    ((↑(fA head) : R) :: List.map (fun (a : α) ↦ (↑(fA a) : R)) tail).prod
⊢ Eq.{u_2 + 1} (α := R) (↑((head :: tail).dProd (A := fun (i : ι) ↦ ↥(A i)) fι fA) : R)
    (List.prod (List.map (fun (a : α) ↦ (↑(fA a) : R)) (head :: tail)))
have rw₃ : (↑(fA head) : R) * (↑(tail.dProd (A := fun (i : ι) ↦ ↥(A i)) fι fA) : R) =
  (↑(fA head) : R) * List.prod (List.map (fun (a : α) ↦ (↑(fA a) : R)) tail)
Tactic: rw [List.dProd_cons, coe_gMul, List.map_cons, List.prod_cons,
      SetLike.coe_list_dProd _ _ _ tail]
-- Lean 4 proof step from Mathlib.Algebra.GradedMonoid (goal)
Goal:
ι : Type u_1
R : Type u_2
α : Type u_3
S : Type u_4
inst : SetLike S R
inst_1 : Monoid R
inst_2 : AddMonoid ι
A : ι → S
inst_3 : GradedMonoid A
fι : α → ι
fA : (a : α) → ↥(A (fι a))
l : List α
head : α
tail : List α
rw :
  (↑(@GradedMonoid.GMul.mul _ (fun (i : ι) ↦ ↥(A i)) AddSemigroup.toAdd _ _ (tail.dProdIndex fι) (fA head)
            (tail.dProd (A := fun (i : ι) ↦ ↥(A i)) fι fA : ↥(A (tail.dProdIndex fι))) :
          ↥(A (fι head + tail.dProdIndex fι))) :
      R) =
    List.prod (List.map (fun (a : α) ↦ (↑(fA a) : R)) (head :: tail))
rw₁ :
  (↑(fA head) : R) * (↑(tail.dProd (A := fun (i : ι) ↦ ↥(A i)) fι fA) : R) =
    List.prod (List.map (fun (a : α) ↦ (↑(fA a) : R)) (head :: tail))
rw₂ :
  (↑(fA head) : R) * (↑(tail.dProd (A := fun (i : ι) ↦ ↥(A i)) fι fA) : R) =
    ((↑(fA head) : R) :: List.map (fun (a : α) ↦ (↑(fA a) : R)) tail).prod
rw₃ :
  (↑(fA head) : R) * (↑(tail.dProd (A := fun (i : ι) ↦ ↥(A i)) fι fA) : R) =
    (↑(fA head) : R) * List.prod (List.map (fun (a : α) ↦ (↑(fA a) : R)) tail)
⊢ Eq.{u_2 + 1} (α := R) (↑((head :: tail).dProd (A := fun (i : ι) ↦ ↥(A i)) fι fA) : R)
    (List.prod (List.map (fun (a : α) ↦ (↑(fA a) : R)) (head :: tail)))
have rw₄ : (↑(fA head) : R) * List.prod (List.map (fun (a : α) ↦ (↑(fA a) : R)) tail) =
  (↑(fA head) : R) * List.prod (List.map (fun (a : α) ↦ (↑(fA a) : R)) tail)
Tactic: rw [List.dProd_cons, coe_gMul, List.map_cons, List.prod_cons,
      SetLike.coe_list_dProd _ _ _ tail]
-- Lean 4 proof step from Mathlib.Algebra.GradedMonoid (goal)
Goal:
ι : Type u_2
R : Type u_3
S : Type u_4
inst : SetLike S R
inst_1 : CommMonoid R
inst_2 : AddCommMonoid ι
A : ι → S
inst_3 : GradedMonoid A
κ : Type u_5
i : κ → ι
g : κ → R
F : Finset κ
hF : ∀ k ∈ F, g k ∈ A (i k)
⊢ ∏ k ∈ F, g k ∈ A (∑ k ∈ F, i k)
have empty : ∀ (hF : ∀ (k : κ), Membership.mem (γ := Finset κ) ∅ k → g k ∈ A (i k)), ∏ k ∈ ∅, g k ∈ A (∑ k ∈ ∅, i k)
Tactic: induction F using Finset.induction_on
Cleared hypotheses: hF
-- Lean 4 proof step from Mathlib.Algebra.GradedMonoid (goal)
Goal:
ι : Type u_2
R : Type u_3
S : Type u_4
inst : SetLike S R
inst_1 : CommMonoid R
inst_2 : AddCommMonoid ι
A : ι → S
inst_3 : GradedMonoid A
κ : Type u_5
i : κ → ι
g : κ → R
F : Finset κ
hF : ∀ k ∈ F, g k ∈ A (i k)
empty : ∀ (hF : ∀ (k : κ), Membership.mem (γ := Finset κ) ∅ k → g k ∈ A (i k)), ∏ k ∈ ∅, g k ∈ A (∑ k ∈ ∅, i k)
⊢ ∏ k ∈ F, g k ∈ A (∑ k ∈ F, i k)
have insert : ∀ (a : κ) (s : Finset κ),
  a ∉ s →
    (∀ (hF : ∀ k ∈ s, g k ∈ A (i k)), ∏ k ∈ s, g k ∈ A (∑ k ∈ s, i k)) →
      ∀ (hF : ∀ k ∈ insert a s, g k ∈ A (i k)), ∏ k ∈ insert a s, g k ∈ A (∑ k ∈ insert a s, i k)
Tactic: induction F using Finset.induction_on
Cleared hypotheses: hF
-- Lean 4 proof step from Mathlib.Algebra.GradedMonoid (goal)
Goal:
ι : Type u_2
R : Type u_3
S : Type u_4
inst : SetLike S R
inst_1 : CommMonoid R
inst_2 : AddCommMonoid ι
A : ι → S
inst_3 : GradedMonoid A
κ : Type u_5
i : κ → ι
g : κ → R
F : Finset κ
j : κ
F' : Finset κ
hF2 : j ∉ F'
h3 : ∀ (hF : ∀ k ∈ F', g k ∈ A (i k)), ∏ k ∈ F', g k ∈ A (∑ k ∈ F', i k)
hF : ∀ k ∈ insert j F', g k ∈ A (i k)
⊢ ∏ k ∈ insert j F', g k ∈ A (∑ k ∈ insert j F', i k)
have rw : g j * ∏ x ∈ F', g x ∈ A (i j + ∑ x ∈ F', i x)
Tactic: rw [Finset.prod_insert hF2, Finset.sum_insert hF2]
-- Lean 4 proof step from Mathlib.Algebra.GradedMonoid (goal)
Goal:
ι : Type u_2
R : Type u_3
S : Type u_4
inst : SetLike S R
inst_1 : CommMonoid R
inst_2 : AddCommMonoid ι
A : ι → S
inst_3 : GradedMonoid A
κ : Type u_5
i : κ → ι
g : κ → R
F : Finset κ
j : κ
F' : Finset κ
hF2 : j ∉ F'
h3 : ∀ (hF : ∀ k ∈ F', g k ∈ A (i k)), ∏ k ∈ F', g k ∈ A (∑ k ∈ F', i k)
hF : ∀ k ∈ insert j F', g k ∈ A (i k)
⊢ g j * ∏ x ∈ F', g x ∈ A (i j + ∑ x ∈ F', i x)
have apply : ∏ x ∈ F', g x ∈ A (∑ x ∈ F', i x)
Tactic: apply SetLike.mul_mem_graded (by grind)
-- Lean 4 proof step from Mathlib.Algebra.GradedMonoid (goal)
Goal:
ι : Type u_2
R : Type u_3
S : Type u_4
inst : SetLike S R
inst_1 : CommMonoid R
inst_2 : AddCommMonoid ι
A : ι → S
inst_3 : GradedMonoid A
κ : Type u_5
i : κ → ι
g : κ → R
F : Finset κ
hF : ∀ k ∈ F, g k ∈ A (i k)
⊢ ∏ k ∈ F, g k ∈ A (∑ k ∈ F, i k)
have empty : ∀ (hF : ∀ (k : κ), Membership.mem (γ := Finset κ) ∅ k → g k ∈ A (i k)), ∏ k ∈ ∅, g k ∈ A (∑ k ∈ ∅, i k)
Tactic: classical
  induction F using Finset.induction_on
  · simp [GradedOne.one_mem]
  · case insert j F' hF2 h3 =>
    rw [Finset.prod_insert hF2, Finset.sum_insert hF2]
    apply SetLike.mul_mem_graded (by grind)
    grind
Cleared hypotheses: hF
-- Lean 4 proof step from Mathlib.Algebra.GradedMonoid (goal)
Goal:
ι : Type u_2
R : Type u_3
S : Type u_4
inst : SetLike S R
inst_1 : CommMonoid R
inst_2 : AddCommMonoid ι
A : ι → S
inst_3 : GradedMonoid A
κ : Type u_5
i : κ → ι
g : κ → R
F : Finset κ
hF : ∀ k ∈ F, g k ∈ A (i k)
empty : ∀ (hF : ∀ (k : κ), Membership.mem (γ := Finset κ) ∅ k → g k ∈ A (i k)), ∏ k ∈ ∅, g k ∈ A (∑ k ∈ ∅, i k)
⊢ ∏ k ∈ F, g k ∈ A (∑ k ∈ F, i k)
have insert : ∀ (a : κ) (s : Finset κ),
  a ∉ s →
    (∀ (hF : ∀ k ∈ s, g k ∈ A (i k)), ∏ k ∈ s, g k ∈ A (∑ k ∈ s, i k)) →
      ∀ (hF : ∀ k ∈ insert a s, g k ∈ A (i k)), ∏ k ∈ insert a s, g k ∈ A (∑ k ∈ insert a s, i k)
Tactic: classical
  induction F using Finset.induction_on
  · simp [GradedOne.one_mem]
  · case insert j F' hF2 h3 =>
    rw [Finset.prod_insert hF2, Finset.sum_insert hF2]
    apply SetLike.mul_mem_graded (by grind)
    grind
Cleared hypotheses: hF
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Basic (goal)
Goal:
α : Type u_5
β : Type u_6
inst : Group α
inst_1 : MulAction α β
⊢ IsCancelSMul α β ↔ ∀ (g : α) (x : β), g • x = x → g = 1
have refine : ∀ (H : ∀ (g : α) (x : β), g • x = x → g = 1) (g h : α) (x : β), g • x = h • x → g = h
Tactic: refine ⟨fun H _ _ ↦ IsCancelSMul.eq_one_of_smul, fun H ↦ ⟨fun g h x ↦ ?_⟩⟩