awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.Pi.Lemmas (goal)
Goal:
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
M : ι → Type u_3
i : I
inst : (i : ι) → Monoid (M i)
inst_1 : ∀ (i : ι), IsMulTorsionFree.{u_3} (M i)
n : ℕ
hn : n ≠ 0
a b : (i : ι) → M i
hab : Eq (α := (i : ι) → M i) ((fun (a : (i : ι) → M i) ↦ a ^ n) a) ((fun (a : (i : ι) → M i) ↦ a ^ n) b)
⊢ a = b
have h : ∀ (i : ι), a i = b i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.Group.Pi.Lemmas (goal)
Goal:
ι : Type u_1
α_1 : Type u_2
I_1 : Type u
f_1 : I_1 → Type v
M : ι → Type u_3
i : I_1
inst : (i : I_1) → Mul (f_1 i)
α : Type u_4
β : Type u_5
inst_1 : Mul α
inst_2 : Mul β
f : α →ₙ* β
I : Type u_6
x x_1 : I → α
⊢ (⇑f : (a : α) → β) ∘ (x * x_1) = HMul.hMul (α := I → β) ((⇑f : (a : α) → β) ∘ x) ((⇑f : (a : α) → β) ∘ x_1)
have h : ∀ (x_2 : I),
  ((⇑f : (a : α) → β) ∘ (x * x_1)) x_2 =
    HMul.hMul (α := I → β) (β := I → β) ((⇑f : (a : α) → β) ∘ x) ((⇑f : (a : α) → β) ∘ x_1) x_2
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Pi.Lemmas (goal)
Goal:
ι : Type u_1
α_1 : Type u_2
I_1 : Type u
f_1 : I_1 → Type v
M : ι → Type u_3
i : I_1
inst : (i : I_1) → MulOneClass (f_1 i)
α : Type u_4
β : Type u_5
inst_1 : MulOneClass α
inst_2 : MulOneClass β
f : α →* β
I : Type u_6
⊢ Eq (α := I → β) (Function.comp.{u_6 + 1, u_4 + 1, u_5 + 1} (β := α) (⇑f : (a : α) → β) 1) 1
have h : ∀ (x : I), Eq.{u_5 + 1} (α := β) (Function.comp.{u_6 + 1, u_4 + 1, u_5 + 1} (β := α) (⇑f : (a : α) → β) 1 x) (1 x)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Pi.Lemmas (goal)
Goal:
ι : Type u_1
α_1 : Type u_2
I_1 : Type u
f_1 : I_1 → Type v
M : ι → Type u_3
i : I_1
inst : (i : I_1) → MulOneClass (f_1 i)
α : Type u_4
β : Type u_5
inst_1 : MulOneClass α
inst_2 : MulOneClass β
f : α →* β
I : Type u_6
x x_1 : I → α
⊢ (⇑f : (a : α) → β) ∘ (x * x_1) = HMul.hMul (α := I → β) ((⇑f : (a : α) → β) ∘ x) ((⇑f : (a : α) → β) ∘ x_1)
have h : ∀ (x_2 : I),
  ((⇑f : (a : α) → β) ∘ (x * x_1)) x_2 =
    HMul.hMul (α := I → β) (β := I → β) ((⇑f : (a : α) → β) ∘ x) ((⇑f : (a : α) → β) ∘ x_1) x_2
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Pi.Lemmas (goal)
Goal:
I : Type u
f : I → Type v
inst : DecidableEq I
inst_1 : (i : I) → MulOneClass (f i)
i j : I
hij : i ≠ j
x : f i
y : f j
⊢ Commute (mulSingle (M := f) i x) (mulSingle (M := f) j y)
have h : ∀ (k : I), (mulSingle (M := f) i x * mulSingle (M := f) j y) k = (mulSingle (M := f) j y * mulSingle (M := f) i x) k
Tactic: ext k
-- Lean 4 proof step from Mathlib.Algebra.Group.Pi.Lemmas (goal)
Goal:
I : Type u
f : I → Type v
inst : DecidableEq I
inst_1 : (i : I) → MulOneClass (f i)
i j : I
hij : i ≠ j
x : f i
y : f j
k : I
⊢ (mulSingle (M := f) i x * mulSingle (M := f) j y) k = (mulSingle (M := f) j y * mulSingle (M := f) i x) k
have pos : i = k → (mulSingle (M := f) i x * mulSingle (M := f) j y) k = (mulSingle (M := f) j y * mulSingle (M := f) i x) k
Tactic: by_cases i = k
-- Lean 4 proof step from Mathlib.Algebra.Group.Pi.Lemmas (goal)
Goal:
I : Type u
f : I → Type v
inst : DecidableEq I
inst_1 : (i : I) → MulOneClass (f i)
i j : I
hij : i ≠ j
x : f i
y : f j
k : I
pos : i = k → (mulSingle (M := f) i x * mulSingle (M := f) j y) k = (mulSingle (M := f) j y * mulSingle (M := f) i x) k
⊢ (mulSingle (M := f) i x * mulSingle (M := f) j y) k = (mulSingle (M := f) j y * mulSingle (M := f) i x) k
have neg : ¬i = k → (mulSingle (M := f) i x * mulSingle (M := f) j y) k = (mulSingle (M := f) j y * mulSingle (M := f) i x) k
Tactic: by_cases i = k
-- Lean 4 proof step from Mathlib.Algebra.Group.Pi.Lemmas (goal)
Goal:
I : Type u
f : I → Type v
inst : DecidableEq I
inst_1 : (i : I) → MulOneClass (f i)
x : (i : I) → f i
i j : I
⊢ Commute (mulSingle (M := f) i (x i)) (mulSingle (M := f) j (x j))
have inl : Commute (mulSingle (M := f) i (x i)) (mulSingle (M := f) i (x i))
Tactic: obtain rfl | hij := Decidable.eq_or_ne i j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Algebra.Group.Pi.Lemmas (goal)
Goal:
I : Type u
f : I → Type v
inst : DecidableEq I
inst_1 : (i : I) → MulOneClass (f i)
x : (i : I) → f i
i j : I
inl : Commute (mulSingle (M := f) i (x i)) (mulSingle (M := f) i (x i))
⊢ Commute (mulSingle (M := f) i (x i)) (mulSingle (M := f) j (x j))
have inr : ∀ (hij : i ≠ j), Commute (mulSingle (M := f) i (x i)) (mulSingle (M := f) j (x j))
Tactic: obtain rfl | hij := Decidable.eq_or_ne i j
-- Lean 4 proof step from Mathlib.Algebra.Group.Pi.Lemmas (goal)
Goal:
I : Type u
f : I → Type v
i : I
inst : DecidableEq I
inst_1 : (i : I) → Group (f i)
g : (i : I) → f i
x : f i
⊢ Function.update (β := f) g i x = g / mulSingle (M := f) i (g i) * mulSingle (M := f) i x
have h : ∀ (j : I), Function.update (β := f) g i x j = (g / mulSingle (M := f) i (g i) * mulSingle (M := f) i x) j
Tactic: ext j
-- Lean 4 proof step from Mathlib.Algebra.Group.Pi.Lemmas (goal)
Goal:
I : Type u
f : I → Type v
i : I
inst : DecidableEq I
inst_1 : (i : I) → Group (f i)
g : (i : I) → f i
x : f i
j : I
⊢ Function.update (β := f) g i x j = (g / mulSingle (M := f) i (g i) * mulSingle (M := f) i x) j
have h : Function.update (β := f) g i x i = (g / mulSingle (M := f) i (g i) * mulSingle (M := f) i x) i
Tactic: rcases eq_or_ne i j with (rfl | h)
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Algebra.Group.Pi.Lemmas (goal)
Goal:
I : Type u
f : I → Type v
i : I
inst : DecidableEq I
inst_1 : (i : I) → Group (f i)
g : (i : I) → f i
x : f i
j : I
h : Function.update (β := f) g i x i = (g / mulSingle (M := f) i (g i) * mulSingle (M := f) i x) i
⊢ Function.update (β := f) g i x j = (g / mulSingle (M := f) i (g i) * mulSingle (M := f) i x) j
have h₁ : ∀ (h : i ≠ j), Function.update (β := f) g i x j = (g / mulSingle (M := f) i (g i) * mulSingle (M := f) i x) j
Tactic: rcases eq_or_ne i j with (rfl | h)
-- Lean 4 proof step from Mathlib.Algebra.Group.Pi.Lemmas (goal)
Goal:
I : Type u
inst : DecidableEq I
M : Type u_4
inst_1 : CommMonoid M
k l m n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
⊢ HMul.hMul (α := (j : I) → M) (mulSingle (M := fun (a : I) ↦ M) k u) (mulSingle (M := fun (j : I) ↦ M) l v) =
      HMul.hMul (α := (j : I) → M) (mulSingle (M := fun (j : I) ↦ M) m u) (mulSingle (M := fun (j : I) ↦ M) n v) ↔
    k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = n
have refine_1 : ∀
  (h :
    HMul.hMul (α := (j : I) → M) (mulSingle (M := fun (a : I) ↦ M) k u) (mulSingle (M := fun (j : I) ↦ M) l v) =
      HMul.hMul (α := (j : I) → M) (mulSingle (M := fun (j : I) ↦ M) m u) (mulSingle (M := fun (j : I) ↦ M) n v)),
  k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = n
Tactic: refine ⟨fun h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Pi.Lemmas (goal)
Goal:
I : Type u
inst : DecidableEq I
M : Type u_4
inst_1 : CommMonoid M
k l m n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
refine_1 :
  ∀
    (h :
      HMul.hMul (α := (j : I) → M) (mulSingle (M := fun (a : I) ↦ M) k u) (mulSingle (M := fun (j : I) ↦ M) l v) =
        HMul.hMul (α := (j : I) → M) (mulSingle (M := fun (j : I) ↦ M) m u) (mulSingle (M := fun (j : I) ↦ M) n v)),
    k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = n
⊢ HMul.hMul (α := (j : I) → M) (mulSingle (M := fun (a : I) ↦ M) k u) (mulSingle (M := fun (j : I) ↦ M) l v) =
      HMul.hMul (α := (j : I) → M) (mulSingle (M := fun (j : I) ↦ M) m u) (mulSingle (M := fun (j : I) ↦ M) n v) ↔
    k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = n
have refine_2 : k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = n →
  HMul.hMul (α := (j : I) → M) (mulSingle (M := fun (a : I) ↦ M) k u) (mulSingle (M := fun (j : I) ↦ M) l v) =
    HMul.hMul (α := (j : I) → M) (mulSingle (M := fun (j : I) ↦ M) m u) (mulSingle (M := fun (j : I) ↦ M) n v)
Tactic: refine ⟨fun h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Pi.Lemmas (hypothesis)
Goal:
I : Type u
inst : DecidableEq I
M : Type u_4
inst_1 : CommMonoid M
k l m n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
h :
  HMul.hMul (α := (j : I) → M) (mulSingle (M := fun (a : I) ↦ M) k u) (mulSingle (M := fun (j : I) ↦ M) l v) =
    HMul.hMul (α := (j : I) → M) (mulSingle (M := fun (j : I) ↦ M) m u) (mulSingle (M := fun (j : I) ↦ M) n v)
⊢ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = n
have hk : HMul.hMul (α := (j : I) → M) (β := (j : I) → M) (mulSingle (M := fun (a : I) ↦ M) k u)
    (mulSingle (M := fun (j : I) ↦ M) l v) k =
  HMul.hMul (α := (j : I) → M) (β := (j : I) → M) (mulSingle (M := fun (j : I) ↦ M) m u)
    (mulSingle (M := fun (j : I) ↦ M) n v) k
Tactic: have hk := congr_fun h k
-- Lean 4 proof step from Mathlib.Algebra.Group.Pi.Lemmas (hypothesis)
Goal:
I : Type u
inst : DecidableEq I
M : Type u_4
inst_1 : CommMonoid M
k l m n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
h :
  HMul.hMul (α := (j : I) → M) (mulSingle (M := fun (a : I) ↦ M) k u) (mulSingle (M := fun (j : I) ↦ M) l v) =
    HMul.hMul (α := (j : I) → M) (mulSingle (M := fun (j : I) ↦ M) m u) (mulSingle (M := fun (j : I) ↦ M) n v)
hk :
  HMul.hMul (α := (j : I) → M) (β := (j : I) → M) (mulSingle (M := fun (a : I) ↦ M) k u)
      (mulSingle (M := fun (j : I) ↦ M) l v) k =
    HMul.hMul (α := (j : I) → M) (β := (j : I) → M) (mulSingle (M := fun (j : I) ↦ M) m u)
      (mulSingle (M := fun (j : I) ↦ M) n v) k
⊢ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = n
have hl : HMul.hMul (α := (j : I) → M) (β := (j : I) → M) (mulSingle (M := fun (a : I) ↦ M) k u)
    (mulSingle (M := fun (j : I) ↦ M) l v) l =
  HMul.hMul (α := (j : I) → M) (β := (j : I) → M) (mulSingle (M := fun (j : I) ↦ M) m u)
    (mulSingle (M := fun (j : I) ↦ M) n v) l
Tactic: have hl := congr_fun h l
-- Lean 4 proof step from Mathlib.Algebra.Group.Pi.Lemmas (hypothesis)
Goal:
I : Type u
inst : DecidableEq I
M : Type u_4
inst_1 : CommMonoid M
k l m n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
h :
  HMul.hMul (α := (j : I) → M) (mulSingle (M := fun (a : I) ↦ M) k u) (mulSingle (M := fun (j : I) ↦ M) l v) =
    HMul.hMul (α := (j : I) → M) (mulSingle (M := fun (j : I) ↦ M) m u) (mulSingle (M := fun (j : I) ↦ M) n v)
hk :
  HMul.hMul (α := (j : I) → M) (β := (j : I) → M) (mulSingle (M := fun (a : I) ↦ M) k u)
      (mulSingle (M := fun (j : I) ↦ M) l v) k =
    HMul.hMul (α := (j : I) → M) (β := (j : I) → M) (mulSingle (M := fun (j : I) ↦ M) m u)
      (mulSingle (M := fun (j : I) ↦ M) n v) k
hl :
  HMul.hMul (α := (j : I) → M) (β := (j : I) → M) (mulSingle (M := fun (a : I) ↦ M) k u)
      (mulSingle (M := fun (j : I) ↦ M) l v) l =
    HMul.hMul (α := (j : I) → M) (β := (j : I) → M) (mulSingle (M := fun (j : I) ↦ M) m u)
      (mulSingle (M := fun (j : I) ↦ M) n v) l
⊢ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = n
have hm : HMul.hMul (α := (j : I) → M) (β := (j : I) → M) (mulSingle (M := fun (a : I) ↦ M) k u)
    (mulSingle (M := fun (j : I) ↦ M) l v) m =
  HMul.hMul (α := (j : I) → M) (β := (j : I) → M) (mulSingle (M := fun (j : I) ↦ M) m u)
    (mulSingle (M := fun (j : I) ↦ M) n v) m
Tactic: have hm := congr_fun h m
-- Lean 4 proof step from Mathlib.Algebra.Group.Pi.Lemmas (hypothesis)
Goal:
I : Type u
inst : DecidableEq I
M : Type u_4
inst_1 : CommMonoid M
k l m n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
h :
  HMul.hMul (α := (j : I) → M) (mulSingle (M := fun (a : I) ↦ M) k u) (mulSingle (M := fun (j : I) ↦ M) l v) =
    HMul.hMul (α := (j : I) → M) (mulSingle (M := fun (j : I) ↦ M) m u) (mulSingle (M := fun (j : I) ↦ M) n v)
hk :
  HMul.hMul (α := (j : I) → M) (β := (j : I) → M) (mulSingle (M := fun (a : I) ↦ M) k u)
      (mulSingle (M := fun (j : I) ↦ M) l v) k =
    HMul.hMul (α := (j : I) → M) (β := (j : I) → M) (mulSingle (M := fun (j : I) ↦ M) m u)
      (mulSingle (M := fun (j : I) ↦ M) n v) k
hl :
  HMul.hMul (α := (j : I) → M) (β := (j : I) → M) (mulSingle (M := fun (a : I) ↦ M) k u)
      (mulSingle (M := fun (j : I) ↦ M) l v) l =
    HMul.hMul (α := (j : I) → M) (β := (j : I) → M) (mulSingle (M := fun (j : I) ↦ M) m u)
      (mulSingle (M := fun (j : I) ↦ M) n v) l
hm :
  HMul.hMul (α := (j : I) → M) (β := (j : I) → M) (mulSingle (M := fun (a : I) ↦ M) k u)
      (mulSingle (M := fun (j : I) ↦ M) l v) m =
    HMul.hMul (α := (j : I) → M) (β := (j : I) → M) (mulSingle (M := fun (j : I) ↦ M) m u)
      (mulSingle (M := fun (j : I) ↦ M) n v) m
⊢ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = n
have hn : HMul.hMul (α := (j : I) → M) (β := (j : I) → M) (mulSingle (M := fun (a : I) ↦ M) k u)
    (mulSingle (M := fun (j : I) ↦ M) l v) n =
  HMul.hMul (α := (j : I) → M) (β := (j : I) → M) (mulSingle (M := fun (j : I) ↦ M) m u)
    (mulSingle (M := fun (j : I) ↦ M) n v) n
Tactic: have hn := congr_fun h n
-- Lean 4 proof step from Mathlib.Algebra.Group.Pi.Lemmas (goal)
Goal:
α : Type u_2
m : Type u_4
n : Type u_5
inst : DecidableEq n
inst_1 : DecidableEq m
inst_2 : One α
σ : n ≃ m
i : m
x : α
⊢ Eq (α := n → α) (mulSingle (M := fun (a : m) ↦ α) i x ∘ (⇑σ : (a : n) → m) : n → α)
    (mulSingle (M := fun (j : n) ↦ α) ((σ.symm : (a : m) → n) i) x : (j : n) → α)
have h : ∀ (x_1 : n),
  Eq.{u_2 + 1} (α := α) ((mulSingle (M := fun (a : m) ↦ α) i x ∘ (⇑σ : (a : n) → m)) x_1 : α)
    (mulSingle (M := fun (j : n) ↦ α) ((σ.symm : (a : m) → n) i) x x_1 : α)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Group.Pi.Lemmas (goal)
Goal:
α : Type u_4
β : α → Type u_5
γ : (a : α) → β a → Type u_6
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (β a)
inst_2 : (a : α) → (b : β a) → One (γ a b)
a : α
b : β a
x : γ a b
⊢ Eq (α := (x : Sigma β) → γ (x.fst (β := β)) (x.snd (β := β)))
    (uncurry (β := β) (γ := γ) (Pi.mulSingle (M := fun (x : α) ↦ (y : β x) → γ x y) a (Pi.mulSingle (M := γ a) b x)))
    (Pi.mulSingle (M := fun (j : Sigma β) ↦ γ (j.fst (β := β)) (j.snd (β := β))) (mk (β := β) a b) x)
have rw : Eq (α := (x : Sigma β) → γ (x.fst (β := β)) (x.snd (β := β)))
  (uncurry (β := β) (γ := γ)
    (curry (β := fun (a : α) ↦ β a) (γ := γ)
      (Pi.mulSingle (M := fun (x : (a : α) × β a) ↦ γ (x.fst (β := fun (a : α) ↦ β a)) (x.snd (β := fun (a : α) ↦ β a)))
        (mk (β := fun (a : α) ↦ β a) a b) x)))
  (Pi.mulSingle (M := fun (j : Sigma β) ↦ γ (j.fst (β := β)) (j.snd (β := β))) (mk (β := β) a b) x)
Tactic: rw [← curry_mulSingle ⟨a, b⟩, uncurry_curry]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pi.Lemmas (goal)
Goal:
α : Type u_4
β : α → Type u_5
γ : (a : α) → β a → Type u_6
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (β a)
inst_2 : (a : α) → (b : β a) → One (γ a b)
a : α
b : β a
x : γ a b
rw :
  Eq (α := (x : Sigma β) → γ (x.fst (β := β)) (x.snd (β := β)))
    (uncurry (β := β) (γ := γ)
      (curry (β := fun (a : α) ↦ β a) (γ := γ)
        (Pi.mulSingle (M := fun (x : (a : α) × β a) ↦
          γ (x.fst (β := fun (a : α) ↦ β a)) (x.snd (β := fun (a : α) ↦ β a))) (mk (β := fun (a : α) ↦ β a) a b) x)))
    (Pi.mulSingle (M := fun (j : Sigma β) ↦ γ (j.fst (β := β)) (j.snd (β := β))) (mk (β := β) a b) x)
⊢ Eq (α := (x : Sigma β) → γ (x.fst (β := β)) (x.snd (β := β)))
    (uncurry (β := β) (γ := γ) (Pi.mulSingle (M := fun (x : α) ↦ (y : β x) → γ x y) a (Pi.mulSingle (M := γ a) b x)))
    (Pi.mulSingle (M := fun (j : Sigma β) ↦ γ (j.fst (β := β)) (j.snd (β := β))) (mk (β := β) a b) x)
have rw₁ : Eq (α := (x : Sigma β) → γ (x.fst (β := β)) (x.snd (β := β)))
  (Pi.mulSingle (M := fun (x : (a : α) × β a) ↦ γ (x.fst (β := fun (a : α) ↦ β a)) (x.snd (β := fun (a : α) ↦ β a)))
    (mk (β := fun (a : α) ↦ β a) a b) x)
  (Pi.mulSingle (M := fun (j : Sigma β) ↦ γ (j.fst (β := β)) (j.snd (β := β))) (mk (β := β) a b) x)
Tactic: rw [← curry_mulSingle ⟨a, b⟩, uncurry_curry]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pi.Units (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
x : (i : ι) → M i
⊢ IsUnit x ↔ ∀ (i : ι), IsUnit (x i)
have simp_rw : (∃ (b : (i : ι) → M i), ∀ (x_1 : ι), (x * b) x_1 = 1 x_1 ∧ (b * x) x_1 = 1 x_1) ↔
  ∀ (i : ι), ∃ (b : M i), x i * b = 1 ∧ b * x i = 1
Tactic: simp_rw [isUnit_iff_exists, funext_iff, ← forall_and]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pi.Units (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
x : (i : ι) → M i
hx : IsUnit x
i : ι
⊢ (↑hx.unit⁻¹ : (i : ι) → M i) i = (↑⋯.unit⁻¹ : M i)
have rw : (↑((MulEquiv.piUnits (M := M) : (a : ((i : ι) → M i)ˣ) → (i : ι) → (M i)ˣ) hx.unit i)⁻¹ : M i) = (↑sorry.unit⁻¹ : M i)
Tactic: rw [← Units.inv_eq_val_inv, ← MulEquiv.val_inv_piUnits_apply]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pi.Units (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
x : (i : ι) → M i
hx : IsUnit x
i : ι
⊢ (↑((MulEquiv.piUnits (M := M) : (a : ((i : ι) → M i)ˣ) → (i : ι) → (M i)ˣ) hx.unit i)⁻¹ : M i) = (↑⋯.unit⁻¹ : M i)
have e_self : (MulEquiv.piUnits (M := M) : (a : ((i : ι) → M i)ˣ) → (i : ι) → (M i)ˣ) hx.unit i = sorry.unit
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Group.Pi.Units (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
x : (i : ι) → M i
hx : IsUnit x
i : ι
⊢ (MulEquiv.piUnits (M := M) : (a : ((i : ι) → M i)ˣ) → (i : ι) → (M i)ˣ) hx.unit i = ⋯.unit
have e_self : (↑((MulEquiv.piUnits (M := M) : (a : ((i : ι) → M i)ˣ) → (i : ι) → (M i)ˣ) hx.unit i) : M i) = (↑sorry.unit : M i)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : One α
s : Finset α
a : α
inst_1 : DecidableEq β
inst_2 : One β
inst_3 : FunLike F α β
inst_4 : OneHomClass F α β
f : F
⊢ Eq.{u_3 + 1} (α := Finset β) (image.{u_2, u_3} (α := α) (⇑f : (a : α) → β) 1) 1
have rw : Eq (α := Finset β) (singleton (α := β) ((f : (a : α) → β) 1 : β)) 1
Tactic: rw [image_one, map_one, singleton_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : One α
s : Finset α
a : α
inst_1 : DecidableEq β
inst_2 : One β
inst_3 : FunLike F α β
inst_4 : OneHomClass F α β
f : F
rw : Eq (α := Finset β) (singleton (α := β) ((f : (a : α) → β) 1 : β)) 1
⊢ Eq.{u_3 + 1} (α := Finset β) (image.{u_2, u_3} (α := α) (⇑f : (a : α) → β) 1) 1
have rw₁ : Eq (α := Finset β) {1} 1
Tactic: rw [image_one, map_one, singleton_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : One α
s : Finset α
a : α
inst_1 : DecidableEq β
inst_2 : One β
inst_3 : FunLike F α β
inst_4 : OneHomClass F α β
f : F
rw : Eq (α := Finset β) (singleton (α := β) ((f : (a : α) → β) 1 : β)) 1
rw₁ : Eq (α := Finset β) {1} 1
⊢ Eq.{u_3 + 1} (α := Finset β) (image.{u_2, u_3} (α := α) (⇑f : (a : α) → β) 1) 1
have rw₂ : Eq.{u_3 + 1} (α := Finset β) 1 1
Tactic: rw [image_one, map_one, singleton_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
inst : One α
inst_1 : One β
⊢ SProd.sprod (α := Finset α) (β := Finset β) 1 1 = 1
have h : ∀ (a : α × β), a ∈ SProd.sprod (α := Finset α) (β := Finset β) 1 1 ↔ Membership.mem (γ := Finset (α × β)) 1 a
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : InvolutiveInv α
s : Finset α
p : α → Prop
inst_2 : DecidablePred p
⊢ ({x ∈ s | p x})⁻¹ = {x ∈ s⁻¹ | p x⁻¹}
have h : ∀ (a : α), a ∈ ({x ∈ s | p x})⁻¹ ↔ a ∈ {x ∈ s⁻¹ | p x⁻¹}
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : InvolutiveInv α
s : Finset α
⊢ (↑(s.preimage (fun (x : α) ↦ x⁻¹) ⋯) : Set α) = (↑s⁻¹ : Set α)
have rw : (fun (x : α) ↦ x⁻¹) ⁻¹' (↑s : Set α) = (↑s⁻¹ : Set α)
Tactic: rw [coe_preimage, Set.inv_preimage, coe_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : InvolutiveInv α
s : Finset α
rw : (fun (x : α) ↦ x⁻¹) ⁻¹' (↑s : Set α) = (↑s⁻¹ : Set α)
⊢ (↑(s.preimage (fun (x : α) ↦ x⁻¹) ⋯) : Set α) = (↑s⁻¹ : Set α)
have rw₁ : (↑s : Set α)⁻¹ = (↑s⁻¹ : Set α)
Tactic: rw [coe_preimage, Set.inv_preimage, coe_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : InvolutiveInv α
s : Finset α
rw : (fun (x : α) ↦ x⁻¹) ⁻¹' (↑s : Set α) = (↑s⁻¹ : Set α)
rw₁ : (↑s : Set α)⁻¹ = (↑s⁻¹ : Set α)
⊢ (↑(s.preimage (fun (x : α) ↦ x⁻¹) ⋯) : Set α) = (↑s⁻¹ : Set α)
have rw₂ : (↑s : Set α)⁻¹ = (↑s : Set α)⁻¹
Tactic: rw [coe_preimage, Set.inv_preimage, coe_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : InvolutiveInv α
inst_2 : Fintype α
⊢ Eq.{u_2 + 1} (α := Finset α) univ⁻¹ univ
have h : ∀ (a : α), Membership.mem (γ := Finset α) univ⁻¹ a ↔ Membership.mem (γ := Finset α) univ a
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s : Finset α
⊢ (↑(npowRec 0 s) : Set α) = HPow.hPow (β := ℕ) (↑s : Set α) 0
have zero : (↑1 : Set α) = HPow.hPow (β := ℕ) (↑s : Set α) 0
Tactic: rw [npowRec, pow_zero, coe_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s : Finset α
zero : (↑1 : Set α) = HPow.hPow (β := ℕ) (↑s : Set α) 0
⊢ (↑(npowRec 0 s) : Set α) = HPow.hPow (β := ℕ) (↑s : Set α) 0
have zero₁ : (↑1 : Set α) = 1
Tactic: rw [npowRec, pow_zero, coe_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s : Finset α
zero : (↑1 : Set α) = HPow.hPow (β := ℕ) (↑s : Set α) 0
zero₁ : (↑1 : Set α) = 1
⊢ (↑(npowRec 0 s) : Set α) = HPow.hPow (β := ℕ) (↑s : Set α) 0
have zero₂ : Eq.{u_2 + 1} (α := Set α) 1 1
Tactic: rw [npowRec, pow_zero, coe_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s : Finset α
n : ℕ
ih : (↑(npowRec n s) : Set α) = (↑s : Set α) ^ n
⊢ (↑(npowRec (n + 1) s) : Set α) = (↑s : Set α) ^ (n + 1)
have succ : (↑(npowRec n s * s) : Set α) = (↑s : Set α) ^ (n + 1)
Tactic: rw [npowRec, pow_succ, coe_mul, ih]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s : Finset α
n : ℕ
ih : (↑(npowRec n s) : Set α) = (↑s : Set α) ^ n
succ : (↑(npowRec n s * s) : Set α) = (↑s : Set α) ^ (n + 1)
⊢ (↑(npowRec (n + 1) s) : Set α) = (↑s : Set α) ^ (n + 1)
have succ₁ : (↑(npowRec n s * s) : Set α) = (↑s : Set α) ^ n * (↑s : Set α)
Tactic: rw [npowRec, pow_succ, coe_mul, ih]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s : Finset α
n : ℕ
ih : (↑(npowRec n s) : Set α) = (↑s : Set α) ^ n
succ : (↑(npowRec n s * s) : Set α) = (↑s : Set α) ^ (n + 1)
succ₁ : (↑(npowRec n s * s) : Set α) = (↑s : Set α) ^ n * (↑s : Set α)
⊢ (↑(npowRec (n + 1) s) : Set α) = (↑s : Set α) ^ (n + 1)
have succ₂ : (↑(npowRec n s) : Set α) * (↑s : Set α) = (↑s : Set α) ^ n * (↑s : Set α)
Tactic: rw [npowRec, pow_succ, coe_mul, ih]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s : Finset α
n : ℕ
ih : (↑(npowRec n s) : Set α) = (↑s : Set α) ^ n
succ : (↑(npowRec n s * s) : Set α) = (↑s : Set α) ^ (n + 1)
succ₁ : (↑(npowRec n s * s) : Set α) = (↑s : Set α) ^ n * (↑s : Set α)
succ₂ : (↑(npowRec n s) : Set α) * (↑s : Set α) = (↑s : Set α) ^ n * (↑s : Set α)
⊢ (↑(npowRec (n + 1) s) : Set α) = (↑s : Set α) ^ (n + 1)
have succ₃ : (↑s : Set α) ^ n * (↑s : Set α) = (↑s : Set α) ^ n * (↑s : Set α)
Tactic: rw [npowRec, pow_succ, coe_mul, ih]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s : Finset α
n : ℕ
⊢ (↑(npowRec n s) : Set α) = (↑s : Set α) ^ n
have zero : (↑(npowRec 0 s) : Set α) = HPow.hPow (β := ℕ) (↑s : Set α) 0
Tactic: induction n with
  | zero => rw [npowRec, pow_zero, coe_one]
  | succ n ih => rw [npowRec, pow_succ, coe_mul, ih]
Cleared hypotheses: n