awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.Opposite (goal)
Goal:
α : Type u_1
inst : Mul α
a x y : αᵐᵒᵖ
⊢ SemiconjBy (unop a) (unop y) (unop x) ↔ SemiconjBy a x y
have conv_rhs : SemiconjBy (unop a) (unop y) (unop x) ↔ SemiconjBy a x y
Tactic: conv_rhs => rw [← op_unop a, ← op_unop x, ← op_unop y, semiconjBy_op]
-- Lean 4 proof step from Mathlib.Algebra.Group.Opposite (goal)
Goal:
α : Type u_1
inst : Mul α
a x y : αᵐᵒᵖ
conv_rhs : SemiconjBy (unop a) (unop y) (unop x) ↔ SemiconjBy a x y
⊢ SemiconjBy (unop a) (unop y) (unop x) ↔ SemiconjBy a x y
have conv_rhs₁ : SemiconjBy (unop a) (unop y) (unop x) ↔ SemiconjBy (unop a) (unop y) (unop x)
Tactic: conv_rhs => rw [← op_unop a, ← op_unop x, ← op_unop y, semiconjBy_op]
-- Lean 4 proof step from Mathlib.Algebra.Group.Opposite (goal)
Goal:
α : Type u_1
inst : MulOne α
⊢ IsDedekindFiniteMonoid.{u_1} αᵐᵒᵖ ↔ IsDedekindFiniteMonoid α
have simp_rw : (∀ (a a_1 : α),
    HMul.hMul (α := αᵐᵒᵖ) (β := αᵐᵒᵖ) ((opEquiv : (a : α) → αᵐᵒᵖ) a : αᵐᵒᵖ) ((opEquiv : (a : α) → αᵐᵒᵖ) a_1 : αᵐᵒᵖ) =
        1 →
      HMul.hMul (α := αᵐᵒᵖ) (β := αᵐᵒᵖ) ((opEquiv : (a : α) → αᵐᵒᵖ) a_1 : αᵐᵒᵖ) ((opEquiv : (a : α) → αᵐᵒᵖ) a : αᵐᵒᵖ) =
        1) ↔
  ∀ {a b : α}, a * b = 1 → b * a = 1
Tactic: simp_rw [isDedekindFiniteMonoid_iff, ← opEquiv.forall_congr_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.PNatPowAssoc (goal)
Goal:
M : Type u_1
inst : Mul M
inst_1 : Pow M ℕ+
inst_2 : PNatPowAssoc M
x : M
m : ℕ+
⊢ x ^ (m * 1) = HPow.hPow (β := ℕ+) (x ^ m) 1
have one : x ^ (m * 1) = x ^ m
Tactic: rw [ppow_one, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.PNatPowAssoc (goal)
Goal:
M : Type u_1
inst : Mul M
inst_1 : Pow M ℕ+
inst_2 : PNatPowAssoc M
x : M
m : ℕ+
one : x ^ (m * 1) = x ^ m
⊢ x ^ (m * 1) = HPow.hPow (β := ℕ+) (x ^ m) 1
have one₁ : x ^ m = x ^ m
Tactic: rw [ppow_one, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.PNatPowAssoc (goal)
Goal:
M : Type u_1
inst : Mul M
inst_1 : Pow M ℕ+
inst_2 : PNatPowAssoc M
x : M
m k : ℕ+
hk : x ^ (m * k) = (x ^ m) ^ k
⊢ x ^ (m * (k + 1)) = (x ^ m) ^ (k + 1)
have succ : x ^ (m * (k + 1)) = (x ^ m) ^ k * HPow.hPow (β := ℕ+) (x ^ m) 1
Tactic: rw [ppow_add, ppow_one, mul_add, ppow_add, mul_one, hk]
-- Lean 4 proof step from Mathlib.Algebra.Group.PNatPowAssoc (goal)
Goal:
M : Type u_1
inst : Mul M
inst_1 : Pow M ℕ+
inst_2 : PNatPowAssoc M
x : M
m k : ℕ+
hk : x ^ (m * k) = (x ^ m) ^ k
succ : x ^ (m * (k + 1)) = (x ^ m) ^ k * HPow.hPow (β := ℕ+) (x ^ m) 1
⊢ x ^ (m * (k + 1)) = (x ^ m) ^ (k + 1)
have succ₁ : x ^ (m * (k + 1)) = (x ^ m) ^ k * x ^ m
Tactic: rw [ppow_add, ppow_one, mul_add, ppow_add, mul_one, hk]
-- Lean 4 proof step from Mathlib.Algebra.Group.PNatPowAssoc (goal)
Goal:
M : Type u_1
inst : Mul M
inst_1 : Pow M ℕ+
inst_2 : PNatPowAssoc M
x : M
m k : ℕ+
hk : x ^ (m * k) = (x ^ m) ^ k
succ : x ^ (m * (k + 1)) = (x ^ m) ^ k * HPow.hPow (β := ℕ+) (x ^ m) 1
succ₁ : x ^ (m * (k + 1)) = (x ^ m) ^ k * x ^ m
⊢ x ^ (m * (k + 1)) = (x ^ m) ^ (k + 1)
have succ₂ : x ^ (m * k + m * 1) = (x ^ m) ^ k * x ^ m
Tactic: rw [ppow_add, ppow_one, mul_add, ppow_add, mul_one, hk]
-- Lean 4 proof step from Mathlib.Algebra.Group.PNatPowAssoc (goal)
Goal:
M : Type u_1
inst : Mul M
inst_1 : Pow M ℕ+
inst_2 : PNatPowAssoc M
x : M
m k : ℕ+
hk : x ^ (m * k) = (x ^ m) ^ k
succ : x ^ (m * (k + 1)) = (x ^ m) ^ k * HPow.hPow (β := ℕ+) (x ^ m) 1
succ₁ : x ^ (m * (k + 1)) = (x ^ m) ^ k * x ^ m
succ₂ : x ^ (m * k + m * 1) = (x ^ m) ^ k * x ^ m
⊢ x ^ (m * (k + 1)) = (x ^ m) ^ (k + 1)
have succ₃ : x ^ (m * k) * x ^ (m * 1) = (x ^ m) ^ k * x ^ m
Tactic: rw [ppow_add, ppow_one, mul_add, ppow_add, mul_one, hk]
-- Lean 4 proof step from Mathlib.Algebra.Group.PNatPowAssoc (goal)
Goal:
M : Type u_1
inst : Mul M
inst_1 : Pow M ℕ+
inst_2 : PNatPowAssoc M
x : M
m k : ℕ+
hk : x ^ (m * k) = (x ^ m) ^ k
succ : x ^ (m * (k + 1)) = (x ^ m) ^ k * HPow.hPow (β := ℕ+) (x ^ m) 1
succ₁ : x ^ (m * (k + 1)) = (x ^ m) ^ k * x ^ m
succ₂ : x ^ (m * k + m * 1) = (x ^ m) ^ k * x ^ m
succ₃ : x ^ (m * k) * x ^ (m * 1) = (x ^ m) ^ k * x ^ m
⊢ x ^ (m * (k + 1)) = (x ^ m) ^ (k + 1)
have succ₄ : x ^ (m * k) * x ^ m = (x ^ m) ^ k * x ^ m
Tactic: rw [ppow_add, ppow_one, mul_add, ppow_add, mul_one, hk]
-- Lean 4 proof step from Mathlib.Algebra.Group.PNatPowAssoc (goal)
Goal:
M : Type u_1
inst : Mul M
inst_1 : Pow M ℕ+
inst_2 : PNatPowAssoc M
x : M
m k : ℕ+
hk : x ^ (m * k) = (x ^ m) ^ k
succ : x ^ (m * (k + 1)) = (x ^ m) ^ k * HPow.hPow (β := ℕ+) (x ^ m) 1
succ₁ : x ^ (m * (k + 1)) = (x ^ m) ^ k * x ^ m
succ₂ : x ^ (m * k + m * 1) = (x ^ m) ^ k * x ^ m
succ₃ : x ^ (m * k) * x ^ (m * 1) = (x ^ m) ^ k * x ^ m
succ₄ : x ^ (m * k) * x ^ m = (x ^ m) ^ k * x ^ m
⊢ x ^ (m * (k + 1)) = (x ^ m) ^ (k + 1)
have succ₅ : (x ^ m) ^ k * x ^ m = (x ^ m) ^ k * x ^ m
Tactic: rw [ppow_add, ppow_one, mul_add, ppow_add, mul_one, hk]
-- Lean 4 proof step from Mathlib.Algebra.Group.PNatPowAssoc (goal)
Goal:
M : Type u_1
inst : Mul M
inst_1 : Pow M ℕ+
inst_2 : PNatPowAssoc M
x : M
m n : ℕ+
⊢ x ^ (m * n) = (x ^ m) ^ n
have one : x ^ (m * 1) = HPow.hPow (β := ℕ+) (x ^ m) 1
Tactic: induction n with
  | one => rw [ppow_one, mul_one]
  | succ k hk => rw [ppow_add, ppow_one, mul_add, ppow_add, mul_one, hk]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Group.PNatPowAssoc (goal)
Goal:
M : Type u_1
inst : Mul M
inst_1 : Pow M ℕ+
inst_2 : PNatPowAssoc M
x : M
m n : ℕ+
one : x ^ (m * 1) = HPow.hPow (β := ℕ+) (x ^ m) 1
⊢ x ^ (m * n) = (x ^ m) ^ n
have succ : ∀ (k : ℕ+) (hk : x ^ (m * k) = (x ^ m) ^ k), x ^ (m * (k + 1)) = (x ^ m) ^ (k + 1)
Tactic: induction n with
  | one => rw [ppow_one, mul_one]
  | succ k hk => rw [ppow_add, ppow_one, mul_add, ppow_add, mul_one, hk]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Group.PNatPowAssoc (goal)
Goal:
M : Type u_1
inst : Mul M
inst_1 : Pow M ℕ+
inst_2 : PNatPowAssoc M
x : M
m n : ℕ+
⊢ x ^ (m * n) = (x ^ n) ^ m
have rw : x ^ (n * m) = (x ^ n) ^ m
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.PNatPowAssoc (goal)
Goal:
M : Type u_1
ι : Type u_2
α : ι → Type u_3
inst : (i : ι) → Mul (α i)
inst_1 : (i : ι) → Pow (α i) ℕ+
inst_2 : ∀ (i : ι), PNatPowAssoc.{u_3} (α i)
x x_1 : ℕ+
x_2 : (i : ι) → α i
⊢ x_2 ^ (x + x_1) = x_2 ^ x * x_2 ^ x_1
have h : ∀ (x_3 : ι), (x_2 ^ (x + x_1)) x_3 = (x_2 ^ x * x_2 ^ x_1) x_3
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.PNatPowAssoc (goal)
Goal:
M : Type u_1
ι : Type u_2
α : ι → Type u_3
inst : (i : ι) → Mul (α i)
inst_1 : (i : ι) → Pow (α i) ℕ+
inst_2 : ∀ (i : ι), PNatPowAssoc.{u_3} (α i)
x : (i : ι) → α i
⊢ HPow.hPow (β := ℕ+) x 1 = x
have h : ∀ (x_1 : ι), HPow.hPow (β := ℕ+) x 1 x_1 = x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.PNatPowAssoc (goal)
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
inst_1 : Pow M ℕ+
inst_2 : PNatPowAssoc M
inst_3 : Mul N
inst_4 : Pow N ℕ+
inst_5 : PNatPowAssoc N
x x_1 : ℕ+
x_2 : M × N
⊢ x_2 ^ (x + x_1) = x_2 ^ x * x_2 ^ x_1
have fst : (x_2 ^ (x + x_1)).1 = (x_2 ^ x * x_2 ^ x_1).1
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.PNatPowAssoc (goal)
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
inst_1 : Pow M ℕ+
inst_2 : PNatPowAssoc M
inst_3 : Mul N
inst_4 : Pow N ℕ+
inst_5 : PNatPowAssoc N
x x_1 : ℕ+
x_2 : M × N
fst : (x_2 ^ (x + x_1)).1 = (x_2 ^ x * x_2 ^ x_1).1
⊢ x_2 ^ (x + x_1) = x_2 ^ x * x_2 ^ x_1
have snd : (x_2 ^ (x + x_1)).2 = (x_2 ^ x * x_2 ^ x_1).2
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.PNatPowAssoc (goal)
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
inst_1 : Pow M ℕ+
inst_2 : PNatPowAssoc M
inst_3 : Mul N
inst_4 : Pow N ℕ+
inst_5 : PNatPowAssoc N
x : M × N
⊢ HPow.hPow (β := ℕ+) x 1 = x
have fst : (HPow.hPow (β := ℕ+) x 1).1 = x.1
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.PNatPowAssoc (goal)
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
inst_1 : Pow M ℕ+
inst_2 : PNatPowAssoc M
inst_3 : Mul N
inst_4 : Pow N ℕ+
inst_5 : PNatPowAssoc N
x : M × N
fst : (HPow.hPow (β := ℕ+) x 1).1 = x.1
⊢ HPow.hPow (β := ℕ+) x 1 = x
have snd : (HPow.hPow (β := ℕ+) x 1).2 = x.2
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.PNatPowAssoc (goal)
Goal:
M : Type u_1
inst : Monoid M
inst_1 : Pow M ℕ+
inst_2 : PNatPowAssoc M
x : M
⊢ HPow.hPow (β := ℕ+) x 1 = x ^ (↑1 : ℕ)
have one : x = x ^ (↑1 : ℕ)
Tactic: rw [ppow_one, PNat.one_coe, pow_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.PNatPowAssoc (goal)
Goal:
M : Type u_1
inst : Monoid M
inst_1 : Pow M ℕ+
inst_2 : PNatPowAssoc M
x : M
one : x = x ^ (↑1 : ℕ)
⊢ HPow.hPow (β := ℕ+) x 1 = x ^ (↑1 : ℕ)
have one₁ : x = HPow.hPow (β := ℕ) x 1
Tactic: rw [ppow_one, PNat.one_coe, pow_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.PNatPowAssoc (goal)
Goal:
M : Type u_1
inst : Monoid M
inst_1 : Pow M ℕ+
inst_2 : PNatPowAssoc M
x : M
one : x = x ^ (↑1 : ℕ)
one₁ : x = HPow.hPow (β := ℕ) x 1
⊢ HPow.hPow (β := ℕ+) x 1 = x ^ (↑1 : ℕ)
have one₂ : x = x
Tactic: rw [ppow_one, PNat.one_coe, pow_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.PNatPowAssoc (goal)
Goal:
M : Type u_1
inst : Monoid M
inst_1 : Pow M ℕ+
inst_2 : PNatPowAssoc M
x : M
k : ℕ+
hk : x ^ k = x ^ (↑k : ℕ)
⊢ x ^ (k + 1) = x ^ (↑(k + 1) : ℕ)
have succ : x ^ k * HPow.hPow (β := ℕ+) x 1 = x ^ (↑(k + 1) : ℕ)
Tactic: rw [ppow_add, ppow_one, PNat.add_coe, pow_add, PNat.one_coe, pow_one, ← hk]
-- Lean 4 proof step from Mathlib.Algebra.Group.PNatPowAssoc (goal)
Goal:
M : Type u_1
inst : Monoid M
inst_1 : Pow M ℕ+
inst_2 : PNatPowAssoc M
x : M
k : ℕ+
hk : x ^ k = x ^ (↑k : ℕ)
succ : x ^ k * HPow.hPow (β := ℕ+) x 1 = x ^ (↑(k + 1) : ℕ)
⊢ x ^ (k + 1) = x ^ (↑(k + 1) : ℕ)
have succ₁ : x ^ k * x = x ^ (↑(k + 1) : ℕ)
Tactic: rw [ppow_add, ppow_one, PNat.add_coe, pow_add, PNat.one_coe, pow_one, ← hk]
-- Lean 4 proof step from Mathlib.Algebra.Group.PNatPowAssoc (goal)
Goal:
M : Type u_1
inst : Monoid M
inst_1 : Pow M ℕ+
inst_2 : PNatPowAssoc M
x : M
k : ℕ+
hk : x ^ k = x ^ (↑k : ℕ)
succ : x ^ k * HPow.hPow (β := ℕ+) x 1 = x ^ (↑(k + 1) : ℕ)
succ₁ : x ^ k * x = x ^ (↑(k + 1) : ℕ)
⊢ x ^ (k + 1) = x ^ (↑(k + 1) : ℕ)
have succ₂ : x ^ k * x = x ^ ((↑k : ℕ) + (↑1 : ℕ))
Tactic: rw [ppow_add, ppow_one, PNat.add_coe, pow_add, PNat.one_coe, pow_one, ← hk]
-- Lean 4 proof step from Mathlib.Algebra.Group.PNatPowAssoc (goal)
Goal:
M : Type u_1
inst : Monoid M
inst_1 : Pow M ℕ+
inst_2 : PNatPowAssoc M
x : M
k : ℕ+
hk : x ^ k = x ^ (↑k : ℕ)
succ : x ^ k * HPow.hPow (β := ℕ+) x 1 = x ^ (↑(k + 1) : ℕ)
succ₁ : x ^ k * x = x ^ (↑(k + 1) : ℕ)
succ₂ : x ^ k * x = x ^ ((↑k : ℕ) + (↑1 : ℕ))
⊢ x ^ (k + 1) = x ^ (↑(k + 1) : ℕ)
have succ₃ : x ^ k * x = x ^ (↑k : ℕ) * x ^ (↑1 : ℕ)
Tactic: rw [ppow_add, ppow_one, PNat.add_coe, pow_add, PNat.one_coe, pow_one, ← hk]
-- Lean 4 proof step from Mathlib.Algebra.Group.PNatPowAssoc (goal)
Goal:
M : Type u_1
inst : Monoid M
inst_1 : Pow M ℕ+
inst_2 : PNatPowAssoc M
x : M
k : ℕ+
hk : x ^ k = x ^ (↑k : ℕ)
succ : x ^ k * HPow.hPow (β := ℕ+) x 1 = x ^ (↑(k + 1) : ℕ)
succ₁ : x ^ k * x = x ^ (↑(k + 1) : ℕ)
succ₂ : x ^ k * x = x ^ ((↑k : ℕ) + (↑1 : ℕ))
succ₃ : x ^ k * x = x ^ (↑k : ℕ) * x ^ (↑1 : ℕ)
⊢ x ^ (k + 1) = x ^ (↑(k + 1) : ℕ)
have succ₄ : x ^ k * x = x ^ (↑k : ℕ) * HPow.hPow (β := ℕ) x 1
Tactic: rw [ppow_add, ppow_one, PNat.add_coe, pow_add, PNat.one_coe, pow_one, ← hk]
-- Lean 4 proof step from Mathlib.Algebra.Group.PNatPowAssoc (goal)
Goal:
M : Type u_1
inst : Monoid M
inst_1 : Pow M ℕ+
inst_2 : PNatPowAssoc M
x : M
k : ℕ+
hk : x ^ k = x ^ (↑k : ℕ)
succ : x ^ k * HPow.hPow (β := ℕ+) x 1 = x ^ (↑(k + 1) : ℕ)
succ₁ : x ^ k * x = x ^ (↑(k + 1) : ℕ)
succ₂ : x ^ k * x = x ^ ((↑k : ℕ) + (↑1 : ℕ))
succ₃ : x ^ k * x = x ^ (↑k : ℕ) * x ^ (↑1 : ℕ)
succ₄ : x ^ k * x = x ^ (↑k : ℕ) * HPow.hPow (β := ℕ) x 1
⊢ x ^ (k + 1) = x ^ (↑(k + 1) : ℕ)
have succ₅ : x ^ k * x = x ^ (↑k : ℕ) * x
Tactic: rw [ppow_add, ppow_one, PNat.add_coe, pow_add, PNat.one_coe, pow_one, ← hk]
-- Lean 4 proof step from Mathlib.Algebra.Group.PNatPowAssoc (goal)
Goal:
M : Type u_1
inst : Monoid M
inst_1 : Pow M ℕ+
inst_2 : PNatPowAssoc M
x : M
k : ℕ+
hk : x ^ k = x ^ (↑k : ℕ)
succ : x ^ k * HPow.hPow (β := ℕ+) x 1 = x ^ (↑(k + 1) : ℕ)
succ₁ : x ^ k * x = x ^ (↑(k + 1) : ℕ)
succ₂ : x ^ k * x = x ^ ((↑k : ℕ) + (↑1 : ℕ))
succ₃ : x ^ k * x = x ^ (↑k : ℕ) * x ^ (↑1 : ℕ)
succ₄ : x ^ k * x = x ^ (↑k : ℕ) * HPow.hPow (β := ℕ) x 1
succ₅ : x ^ k * x = x ^ (↑k : ℕ) * x
⊢ x ^ (k + 1) = x ^ (↑(k + 1) : ℕ)
have succ₆ : x ^ k * x = x ^ k * x
Tactic: rw [ppow_add, ppow_one, PNat.add_coe, pow_add, PNat.one_coe, pow_one, ← hk]
-- Lean 4 proof step from Mathlib.Algebra.Group.PNatPowAssoc (goal)
Goal:
M : Type u_1
inst : Monoid M
inst_1 : Pow M ℕ+
inst_2 : PNatPowAssoc M
x : M
n : ℕ+
⊢ x ^ n = x ^ (↑n : ℕ)
have one : HPow.hPow (β := ℕ+) x 1 = x ^ (↑1 : ℕ)
Tactic: induction n with
  | one => rw [ppow_one, PNat.one_coe, pow_one]
  | succ k hk => rw [ppow_add, ppow_one, PNat.add_coe, pow_add, PNat.one_coe, pow_one, ← hk]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Group.PNatPowAssoc (goal)
Goal:
M : Type u_1
inst : Monoid M
inst_1 : Pow M ℕ+
inst_2 : PNatPowAssoc M
x : M
n : ℕ+
one : HPow.hPow (β := ℕ+) x 1 = x ^ (↑1 : ℕ)
⊢ x ^ n = x ^ (↑n : ℕ)
have succ : ∀ (k : ℕ+) (hk : x ^ k = x ^ (↑k : ℕ)), x ^ (k + 1) = x ^ (↑(k + 1) : ℕ)
Tactic: induction n with
  | one => rw [ppow_one, PNat.one_coe, pow_one]
  | succ k hk => rw [ppow_add, ppow_one, PNat.add_coe, pow_add, PNat.one_coe, pow_one, ← hk]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Group.Pi.Basic (goal)
Goal:
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
inst : (i : I) → Semigroup (f i)
a b c : (i : I) → f i
⊢ a * b * c = a * (b * c)
have h₁ : ∀ (x : I), (a * b * c) x = (a * (b * c)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Pi.Basic (goal)
Goal:
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
inst : (i : I) → CommSemigroup (f i)
a b : (i : I) → f i
⊢ a * b = b * a
have h₁ : ∀ (x : I), (a * b) x = (b * a) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Pi.Basic (goal)
Goal:
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
inst : (i : I) → MulOneClass (f i)
a : (i : I) → f i
⊢ 1 * a = a
have h₁ : ∀ (x : I), HMul.hMul (α := (i : I) → f i) 1 a x = a x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Pi.Basic (goal)
Goal:
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
inst : (i : I) → MulOneClass (f i)
a : (i : I) → f i
⊢ a * 1 = a
have h₁ : ∀ (x : I), HMul.hMul (β := (i : I) → f i) a 1 x = a x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Pi.Basic (goal)
Goal:
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
inst : (i : I) → InvOneClass (f i)
⊢ Eq (α := (i : I) → f i) 1⁻¹ 1
have h₁ : ∀ (x : I), Eq.{v₁ + 1} (α := f x) (1⁻¹ x) (1 x)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Pi.Basic (goal)
Goal:
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
inst : (i : I) → Monoid (f i)
x_1 : (i : I) → f i
⊢ Eq (α := (i : I) → f i) (fun (i : I) ↦ HPow.hPow (β := ℕ) (x_1 i) 0) 1
have h₁ : ∀ (x : I), HPow.hPow (β := ℕ) (x_1 x) 0 = 1 x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Pi.Basic (goal)
Goal:
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
inst : (i : I) → Monoid (f i)
n : ℕ
x_1 : (i : I) → f i
⊢ (fun (i : I) ↦ x_1 i ^ (n + 1)) = (fun (i : I) ↦ x_1 i ^ n) * x_1
have h₁ : ∀ (x : I), x_1 x ^ (n + 1) = HMul.hMul (α := (i : I) → f i) (fun (i : I) ↦ x_1 i ^ n) x_1 x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Pi.Basic (goal)
Goal:
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
inst : (i : I) → DivInvMonoid (f i)
a b : (i : I) → f i
⊢ a / b = a * b⁻¹
have h₁ : ∀ (x : I), (a / b) x = (a * b⁻¹) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Pi.Basic (goal)
Goal:
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
inst : (i : I) → DivInvMonoid (f i)
a : (i : I) → f i
⊢ Eq (α := (i : I) → f i) (fun (i : I) ↦ HPow.hPow (β := ℤ) (a i) 0) 1
have h₁ : ∀ (x : I), HPow.hPow (β := ℤ) (a x) 0 = 1 x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Pi.Basic (goal)
Goal:
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
inst : (i : I) → DivInvMonoid (f i)
n : ℕ
a : (i : I) → f i
⊢ (fun (i : I) ↦ HPow.hPow (β := ℤ) (a i) (↑n.succ : ℤ)) = (fun (i : I) ↦ HPow.hPow (β := ℤ) (a i) (↑n : ℤ)) * a
have h₁ : ∀ (x : I),
  HPow.hPow (β := ℤ) (a x) (↑n.succ : ℤ) =
    HMul.hMul (α := (i : I) → f i) (fun (i : I) ↦ HPow.hPow (β := ℤ) (a i) (↑n : ℤ)) a x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Pi.Basic (goal)
Goal:
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
inst : (i : I) → DivInvMonoid (f i)
n : ℕ
a : (i : I) → f i
⊢ Eq (α := (i : I) → f i) (fun (i : I) ↦ a i ^ Int.negSucc n) (fun (i : I) ↦ HPow.hPow (β := ℤ) (a i) (↑n.succ : ℤ))⁻¹
have h₁ : ∀ (x : I), a x ^ Int.negSucc n = (fun (i : I) ↦ HPow.hPow (β := ℤ) (a i) (↑n.succ : ℤ))⁻¹ x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Pi.Basic (goal)
Goal:
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
inst : (i : I) → DivInvOneMonoid (f i)
⊢ Eq (α := (i : I) → f i) 1⁻¹ 1
have h₁ : ∀ (x : I), Eq.{v₁ + 1} (α := f x) (1⁻¹ x) (1 x)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Pi.Basic (goal)
Goal:
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
inst : (i : I) → InvolutiveInv (f i)
x_1 : (i : I) → f i
⊢ x_1⁻¹⁻¹ = x_1
have h₁ : ∀ (x : I), x_1⁻¹⁻¹ x = x_1 x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Pi.Basic (goal)
Goal:
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
inst : (i : I) → DivisionMonoid (f i)
a b : (i : I) → f i
⊢ (a * b)⁻¹ = b⁻¹ * a⁻¹
have h₁ : ∀ (x : I), (a * b)⁻¹ x = (b⁻¹ * a⁻¹) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Pi.Basic (goal)
Goal:
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h_1 : I → Type v₃
x y : (i : I) → f i
i : I
inst : (i : I) → DivisionMonoid (f i)
a b : (i : I) → f i
h : a * b = 1
⊢ a⁻¹ = b
have h₁ : ∀ (x : I), a⁻¹ x = b x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Pi.Basic (goal)
Goal:
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
inst : (i : I) → Group (f i)
a : (i : I) → f i
⊢ a⁻¹ * a = 1
have h₁ : ∀ (x : I), (a⁻¹ * a) x = 1 x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Pi.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Mul γ
f : α → β
g₁ g₂ : α → γ
e₁ e₂ : β → γ
⊢ extend f (g₁ * g₂) (e₁ * e₂) = extend f g₁ e₁ * extend f g₂ e₂
have h : ∀ (x : β), extend f (g₁ * g₂) (e₁ * e₂) x = (extend f g₁ e₁ * extend f g₂ e₂) x
Tactic: funext x
-- Lean 4 proof step from Mathlib.Algebra.Group.Pi.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Mul γ
f : α → β
g₁ g₂ : α → γ
e₁ e₂ : β → γ
⊢ extend f (g₁ * g₂) (e₁ * e₂) = extend f g₁ e₁ * extend f g₂ e₂
have h : ∀ (x : β), extend f (g₁ * g₂) (e₁ * e₂) x = (extend f g₁ e₁ * extend f g₂ e₂) x
Tactic: classical
  funext x
  simp [Function.extend_def, apply_dite₂]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pi.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Inv γ
f : α → β
g : α → γ
e : β → γ
⊢ extend f g⁻¹ e⁻¹ = (extend f g e)⁻¹
have h : ∀ (x : β), extend f g⁻¹ e⁻¹ x = (extend f g e)⁻¹ x
Tactic: funext x
-- Lean 4 proof step from Mathlib.Algebra.Group.Pi.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Inv γ
f : α → β
g : α → γ
e : β → γ
⊢ extend f g⁻¹ e⁻¹ = (extend f g e)⁻¹
have h : ∀ (x : β), extend f g⁻¹ e⁻¹ x = (extend f g e)⁻¹ x
Tactic: classical
  funext x
  simp [Function.extend_def, apply_dite Inv.inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pi.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Div γ
f : α → β
g₁ g₂ : α → γ
e₁ e₂ : β → γ
⊢ extend f (g₁ / g₂) (e₁ / e₂) = extend f g₁ e₁ / extend f g₂ e₂
have h : ∀ (x : β), extend f (g₁ / g₂) (e₁ / e₂) x = (extend f g₁ e₁ / extend f g₂ e₂) x
Tactic: funext x
-- Lean 4 proof step from Mathlib.Algebra.Group.Pi.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Div γ
f : α → β
g₁ g₂ : α → γ
e₁ e₂ : β → γ
⊢ extend f (g₁ / g₂) (e₁ / e₂) = extend f g₁ e₁ / extend f g₂ e₂
have h : ∀ (x : β), extend f (g₁ / g₂) (e₁ / e₂) x = (extend f g₁ e₁ / extend f g₂ e₂) x
Tactic: classical
  funext x
  simp [Function.extend_def, apply_dite₂]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pi.Basic (goal)
Goal:
I : Type u
α : Type u_4
inst : DecidableEq I
inst_1 : Subsingleton I
inst_2 : One α
i : I
x : α
j : I
⊢ Pi.mulSingle (M := fun (x : I) ↦ α) i x j = x
have rw : Pi.mulSingle (M := fun (x : I) ↦ α) i x i = x
Tactic: rw [Subsingleton.elim j i, Pi.mulSingle_eq_same]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pi.Basic (goal)
Goal:
I : Type u
α : Type u_4
inst : DecidableEq I
inst_1 : Subsingleton I
inst_2 : One α
i : I
x : α
j : I
rw : Pi.mulSingle (M := fun (x : I) ↦ α) i x i = x
⊢ Pi.mulSingle (M := fun (x : I) ↦ α) i x j = x
have rw₁ : x = x
Tactic: rw [Subsingleton.elim j i, Pi.mulSingle_eq_same]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pi.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
a a' : α → γ
b b' : β → γ
inst : Mul γ
⊢ Sum.elim (a * a') (b * b') = Sum.elim a b * Sum.elim a' b'
have h : ∀ (x : α ⊕ β), Sum.elim (a * a') (b * b') x = (Sum.elim a b * Sum.elim a' b') x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Group.Pi.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
a a' : α → γ
b b' : β → γ
inst : Mul γ
x : α ⊕ β
⊢ Sum.elim (a * a') (b * b') x = (Sum.elim a b * Sum.elim a' b') x
have h : ∀ (val : α), Sum.elim (a * a') (b * b') (inl val) = (Sum.elim a b * Sum.elim a' b') (inl val)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Group.Pi.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
a a' : α → γ
b b' : β → γ
inst : Mul γ
x : α ⊕ β
h : ∀ (val : α), Sum.elim (a * a') (b * b') (inl val) = (Sum.elim a b * Sum.elim a' b') (inl val)
⊢ Sum.elim (a * a') (b * b') x = (Sum.elim a b * Sum.elim a' b') x
have h₁ : ∀ (val : β), Sum.elim (a * a') (b * b') (inr val) = (Sum.elim a b * Sum.elim a' b') (inr val)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Group.Pi.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
a a' : α → γ
b b' : β → γ
inst : Div γ
⊢ Sum.elim (a / a') (b / b') = Sum.elim a b / Sum.elim a' b'
have h : ∀ (x : α ⊕ β), Sum.elim (a / a') (b / b') x = (Sum.elim a b / Sum.elim a' b') x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Group.Pi.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
a a' : α → γ
b b' : β → γ
inst : Div γ
x : α ⊕ β
⊢ Sum.elim (a / a') (b / b') x = (Sum.elim a b / Sum.elim a' b') x
have h : ∀ (val : α), Sum.elim (a / a') (b / b') (inl val) = (Sum.elim a b / Sum.elim a' b') (inl val)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Group.Pi.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
a a' : α → γ
b b' : β → γ
inst : Div γ
x : α ⊕ β
h : ∀ (val : α), Sum.elim (a / a') (b / b') (inl val) = (Sum.elim a b / Sum.elim a' b') (inl val)
⊢ Sum.elim (a / a') (b / b') x = (Sum.elim a b / Sum.elim a' b') x
have h₁ : ∀ (val : β), Sum.elim (a / a') (b / b') (inr val) = (Sum.elim a b / Sum.elim a' b') (inr val)
Tactic: cases x
Cleared hypotheses: x