awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Pi.Basic
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
h₁ : ∀ (x : I), (a * b * c) x = (a * (b * c)) x
⊢ a * b * c = a * (b * c)

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Pi.Basic
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
x_1 : I
⊢ (a * b * c) x_1 = (a * (b * c)) x_1

Tactic:
mul_assoc _ _ _

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Group.Pi.Basic
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
x_1 : I
⊢ (a * b * c) x_1 = (a * (b * c)) x_1

Tactic:
exact mul_assoc _ _ _

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Group.Pi.Basic
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
h₁ : ∀ (x : I), (a * b) x = (b * a) x
⊢ a * b = b * a

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Pi.Basic
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
x_1 : I
⊢ (a * b) x_1 = (b * a) x_1

Tactic:
mul_comm _ _

Premises used: mul_comm
-- Module: Mathlib.Algebra.Group.Pi.Basic
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
x_1 : I
⊢ (a * b) x_1 = (b * a) x_1

Tactic:
exact mul_comm _ _

Premises used: mul_comm
-- Module: Mathlib.Algebra.Group.Pi.Basic
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
h₁ : ∀ (x : I), HMul.hMul (α := (i : I) → f i) 1 a x = a x
⊢ 1 * a = a

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Pi.Basic
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
x_1 : I
⊢ HMul.hMul (α := (i : I) → f i) 1 a x_1 = a x_1

Tactic:
one_mul _

Premises used: one_mul
-- Module: Mathlib.Algebra.Group.Pi.Basic
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
x_1 : I
⊢ HMul.hMul (α := (i : I) → f i) 1 a x_1 = a x_1

Tactic:
exact one_mul _

Premises used: one_mul
-- Module: Mathlib.Algebra.Group.Pi.Basic
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
h₁ : ∀ (x : I), HMul.hMul (β := (i : I) → f i) a 1 x = a x
⊢ a * 1 = a

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Pi.Basic
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
x_1 : I
⊢ HMul.hMul (β := (i : I) → f i) a 1 x_1 = a x_1

Tactic:
mul_one _

Premises used: mul_one
-- Module: Mathlib.Algebra.Group.Pi.Basic
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
x_1 : I
⊢ HMul.hMul (β := (i : I) → f i) a 1 x_1 = a x_1

Tactic:
exact mul_one _

Premises used: mul_one
-- Module: Mathlib.Algebra.Group.Pi.Basic
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)
h₁ : ∀ (x : I), Eq.{v₁ + 1} (α := f x) (1⁻¹ x) (1 x)
⊢ Eq (α := (i : I) → f i) 1⁻¹ 1

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Pi.Basic
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)
x_1 : I
⊢ Eq.{v₁ + 1} (α := f x_1) (1⁻¹ x_1) (1 x_1)

Tactic:
inv_one

Premises used: inv_one
-- Module: Mathlib.Algebra.Group.Pi.Basic
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)
x_1 : I
⊢ Eq.{v₁ + 1} (α := f x_1) (1⁻¹ x_1) (1 x_1)

Tactic:
exact inv_one

Premises used: inv_one
-- Module: Mathlib.Algebra.Group.Pi.Basic
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
h₁ : ∀ (x : I), HPow.hPow (β := ℕ) (x_1 x) 0 = 1 x
⊢ Eq (α := (i : I) → f i) (fun (i : I) ↦ HPow.hPow (β := ℕ) (x_1 i) 0) 1

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Pi.Basic
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
x_2 : I
⊢ HPow.hPow (β := ℕ) (x_1 x_2) 0 = 1 x_2

Tactic:
Monoid.npow_zero _

Premises used: Monoid.npow_zero
-- Module: Mathlib.Algebra.Group.Pi.Basic
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
x_2 : I
⊢ HPow.hPow (β := ℕ) (x_1 x_2) 0 = 1 x_2

Tactic:
exact Monoid.npow_zero _

Premises used: Monoid.npow_zero
-- Module: Mathlib.Algebra.Group.Pi.Basic
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
h₁ : ∀ (x : I), x_1 x ^ (n + 1) = HMul.hMul (α := (i : I) → f i) (fun (i : I) ↦ x_1 i ^ n) x_1 x
⊢ (fun (i : I) ↦ x_1 i ^ (n + 1)) = (fun (i : I) ↦ x_1 i ^ n) * x_1

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Pi.Basic
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
x_2 : I
⊢ x_1 x_2 ^ (n + 1) = HMul.hMul (α := (i : I) → f i) (fun (i : I) ↦ x_1 i ^ n) x_1 x_2

Tactic:
Monoid.npow_succ _ _

Premises used: Monoid.npow_succ
-- Module: Mathlib.Algebra.Group.Pi.Basic
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
x_2 : I
⊢ x_1 x_2 ^ (n + 1) = HMul.hMul (α := (i : I) → f i) (fun (i : I) ↦ x_1 i ^ n) x_1 x_2

Tactic:
exact Monoid.npow_succ _ _

Premises used: Monoid.npow_succ
-- Module: Mathlib.Algebra.Group.Pi.Basic
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
h₁ : ∀ (x : I), (a / b) x = (a * b⁻¹) x
⊢ a / b = a * b⁻¹

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Pi.Basic
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
x_1 : I
⊢ (a / b) x_1 = (a * b⁻¹) x_1

Tactic:
div_eq_mul_inv _ _

Premises used: div_eq_mul_inv
-- Module: Mathlib.Algebra.Group.Pi.Basic
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
x_1 : I
⊢ (a / b) x_1 = (a * b⁻¹) x_1

Tactic:
exact div_eq_mul_inv _ _

Premises used: div_eq_mul_inv
-- Module: Mathlib.Algebra.Group.Pi.Basic
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
h₁ : ∀ (x : I), HPow.hPow (β := ℤ) (a x) 0 = 1 x
⊢ Eq (α := (i : I) → f i) (fun (i : I) ↦ HPow.hPow (β := ℤ) (a i) 0) 1

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Pi.Basic
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
x_1 : I
⊢ HPow.hPow (β := ℤ) (a x_1) 0 = 1 x_1

Tactic:
DivInvMonoid.zpow_zero' _

Premises used: DivInvMonoid.zpow_zero'
-- Module: Mathlib.Algebra.Group.Pi.Basic
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
x_1 : I
⊢ HPow.hPow (β := ℤ) (a x_1) 0 = 1 x_1

Tactic:
exact DivInvMonoid.zpow_zero' _

Premises used: DivInvMonoid.zpow_zero'
-- Module: Mathlib.Algebra.Group.Pi.Basic
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
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
⊢ (fun (i : I) ↦ HPow.hPow (β := ℤ) (a i) (↑n.succ : ℤ)) = (fun (i : I) ↦ HPow.hPow (β := ℤ) (a i) (↑n : ℤ)) * a

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Pi.Basic
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
x_1 : I
⊢ HPow.hPow (β := ℤ) (a x_1) (↑n.succ : ℤ) =
    HMul.hMul (α := (i : I) → f i) (fun (i : I) ↦ HPow.hPow (β := ℤ) (a i) (↑n : ℤ)) a x_1

Tactic:
DivInvMonoid.zpow_succ' _ _

Premises used: DivInvMonoid.zpow_succ'
-- Module: Mathlib.Algebra.Group.Pi.Basic
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
x_1 : I
⊢ HPow.hPow (β := ℤ) (a x_1) (↑n.succ : ℤ) =
    HMul.hMul (α := (i : I) → f i) (fun (i : I) ↦ HPow.hPow (β := ℤ) (a i) (↑n : ℤ)) a x_1

Tactic:
exact DivInvMonoid.zpow_succ' _ _

Premises used: DivInvMonoid.zpow_succ'
-- Module: Mathlib.Algebra.Group.Pi.Basic
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
h₁ : ∀ (x : I), a x ^ Int.negSucc n = (fun (i : I) ↦ HPow.hPow (β := ℤ) (a i) (↑n.succ : ℤ))⁻¹ x
⊢ Eq (α := (i : I) → f i) (fun (i : I) ↦ a i ^ Int.negSucc n) (fun (i : I) ↦ HPow.hPow (β := ℤ) (a i) (↑n.succ : ℤ))⁻¹

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Pi.Basic
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
x_1 : I
⊢ a x_1 ^ Int.negSucc n = (fun (i : I) ↦ HPow.hPow (β := ℤ) (a i) (↑n.succ : ℤ))⁻¹ x_1

Tactic:
DivInvMonoid.zpow_neg' _ _

Premises used: DivInvMonoid.zpow_neg'
-- Module: Mathlib.Algebra.Group.Pi.Basic
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
x_1 : I
⊢ a x_1 ^ Int.negSucc n = (fun (i : I) ↦ HPow.hPow (β := ℤ) (a i) (↑n.succ : ℤ))⁻¹ x_1

Tactic:
exact DivInvMonoid.zpow_neg' _ _

Premises used: DivInvMonoid.zpow_neg'
-- Module: Mathlib.Algebra.Group.Pi.Basic
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)
h₁ : ∀ (x : I), Eq.{v₁ + 1} (α := f x) (1⁻¹ x) (1 x)
⊢ Eq (α := (i : I) → f i) 1⁻¹ 1

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Pi.Basic
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)
x_1 : I
⊢ Eq.{v₁ + 1} (α := f x_1) (1⁻¹ x_1) (1 x_1)

Tactic:
inv_one

Premises used: inv_one
-- Module: Mathlib.Algebra.Group.Pi.Basic
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)
x_1 : I
⊢ Eq.{v₁ + 1} (α := f x_1) (1⁻¹ x_1) (1 x_1)

Tactic:
exact inv_one

Premises used: inv_one
-- Module: Mathlib.Algebra.Group.Pi.Basic
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
h₁ : ∀ (x : I), x_1⁻¹⁻¹ x = x_1 x
⊢ x_1⁻¹⁻¹ = x_1

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Pi.Basic
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_2 : I
⊢ x_1⁻¹⁻¹ x_2 = x_1 x_2

Tactic:
inv_inv _

Premises used: inv_inv
-- Module: Mathlib.Algebra.Group.Pi.Basic
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_2 : I
⊢ x_1⁻¹⁻¹ x_2 = x_1 x_2

Tactic:
exact inv_inv _

Premises used: inv_inv
-- Module: Mathlib.Algebra.Group.Pi.Basic
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
h₁ : ∀ (x : I), (a * b)⁻¹ x = (b⁻¹ * a⁻¹) x
⊢ (a * b)⁻¹ = b⁻¹ * a⁻¹

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Pi.Basic
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
x_1 : I
⊢ (a * b)⁻¹ x_1 = (b⁻¹ * a⁻¹) x_1

Tactic:
mul_inv_rev _ _

Premises used: mul_inv_rev
-- Module: Mathlib.Algebra.Group.Pi.Basic
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
x_1 : I
⊢ (a * b)⁻¹ x_1 = (b⁻¹ * a⁻¹) x_1

Tactic:
exact mul_inv_rev _ _

Premises used: mul_inv_rev
-- Module: Mathlib.Algebra.Group.Pi.Basic
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 : (i : I) → f i
_ : ∀ (b : (i : I) → f i), a * b = 1 → a⁻¹ = b
⊢ ∀ (b : (i : I) → f i), a * b = 1 → a⁻¹ = b

Tactic:
_
-- Module: Mathlib.Algebra.Group.Pi.Basic
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
h₁ : ∀ (x : I), a⁻¹ x = b x
⊢ a⁻¹ = b

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Pi.Basic
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
x_1 : I
⊢ a⁻¹ x_1 = b x_1

Tactic:
DivisionMonoid.inv_eq_of_mul _ _ (congrFun h _)

Premises used: congrFun, DivisionMonoid.inv_eq_of_mul
-- Module: Mathlib.Algebra.Group.Pi.Basic
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
x_1 : I
⊢ a⁻¹ x_1 = b x_1

Tactic:
exact DivisionMonoid.inv_eq_of_mul _ _ (congrFun h _)

Premises used: congrFun, DivisionMonoid.inv_eq_of_mul
-- Module: Mathlib.Algebra.Group.Pi.Basic
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
h₁ : ∀ (x : I), (a⁻¹ * a) x = 1 x
⊢ a⁻¹ * a = 1

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Pi.Basic
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
x_1 : I
⊢ (a⁻¹ * a) x_1 = 1 x_1

Tactic:
inv_mul_cancel _

Premises used: inv_mul_cancel
-- Module: Mathlib.Algebra.Group.Pi.Basic
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
x_1 : I
⊢ (a⁻¹ * a) x_1 = 1 x_1

Tactic:
exact inv_mul_cancel _

Premises used: inv_mul_cancel
-- Module: Mathlib.Algebra.Group.Pi.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : One γ
f : α → β
x : β
⊢ Eq.{u_3 + 1} (α := γ) (extend f 1 1 x) (1 x)

Tactic:
apply ite_self

Premises used: ite_self
-- Module: Mathlib.Algebra.Group.Pi.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Mul γ
f : α → β
g₁ g₂ : α → γ
e₁ e₂ : β → γ
h : ∀ (x : β), extend f (g₁ * g₂) (e₁ * e₂) x = (extend f g₁ e₁ * extend f g₂ e₂) x
⊢ extend f (g₁ * g₂) (e₁ * e₂) = extend f g₁ e₁ * extend f g₂ e₂

Tactic:
funext x
-- Module: Mathlib.Algebra.Group.Pi.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Mul γ
f : α → β
g₁ g₂ : α → γ
e₁ e₂ : β → γ
x : β
⊢ extend f (g₁ * g₂) (e₁ * e₂) x = (extend f g₁ e₁ * extend f g₂ e₂) x

Tactic:
simp [Function.extend_def, apply_dite₂]

Premises used: Function.extend_def, apply_dite₂
-- Module: Mathlib.Algebra.Group.Pi.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Mul γ
f : α → β
g₁ g₂ : α → γ
e₁ e₂ : β → γ
h h₁ h₂ : ∀ (x : β), extend f (g₁ * g₂) (e₁ * e₂) x = (extend f g₁ e₁ * extend f g₂ e₂) x
⊢ extend f (g₁ * g₂) (e₁ * e₂) = extend f g₁ e₁ * extend f g₂ e₂

Tactic:
classical
  funext x
  simp [Function.extend_def, apply_dite₂]

Premises used: Function.extend_def, apply_dite₂
-- Module: Mathlib.Algebra.Group.Pi.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Inv γ
f : α → β
g : α → γ
e : β → γ
h : ∀ (x : β), extend f g⁻¹ e⁻¹ x = (extend f g e)⁻¹ x
⊢ extend f g⁻¹ e⁻¹ = (extend f g e)⁻¹

Tactic:
funext x
-- Module: Mathlib.Algebra.Group.Pi.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Inv γ
f : α → β
g : α → γ
e : β → γ
x : β
⊢ extend f g⁻¹ e⁻¹ x = (extend f g e)⁻¹ x

Tactic:
simp [Function.extend_def, apply_dite Inv.inv]

Premises used: apply_dite, Function.extend_def, Inv.inv
-- Module: Mathlib.Algebra.Group.Pi.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Inv γ
f : α → β
g : α → γ
e : β → γ
h h₁ h₂ : ∀ (x : β), extend f g⁻¹ e⁻¹ x = (extend f g e)⁻¹ x
⊢ extend f g⁻¹ e⁻¹ = (extend f g e)⁻¹

Tactic:
classical
  funext x
  simp [Function.extend_def, apply_dite Inv.inv]

Premises used: apply_dite, Function.extend_def, Inv.inv
-- Module: Mathlib.Algebra.Group.Pi.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Div γ
f : α → β
g₁ g₂ : α → γ
e₁ e₂ : β → γ
h : ∀ (x : β), extend f (g₁ / g₂) (e₁ / e₂) x = (extend f g₁ e₁ / extend f g₂ e₂) x
⊢ extend f (g₁ / g₂) (e₁ / e₂) = extend f g₁ e₁ / extend f g₂ e₂

Tactic:
funext x
-- Module: Mathlib.Algebra.Group.Pi.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Div γ
f : α → β
g₁ g₂ : α → γ
e₁ e₂ : β → γ
x : β
⊢ extend f (g₁ / g₂) (e₁ / e₂) x = (extend f g₁ e₁ / extend f g₂ e₂) x

Tactic:
simp [Function.extend_def, apply_dite₂]

Premises used: Function.extend_def, apply_dite₂
-- Module: Mathlib.Algebra.Group.Pi.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Div γ
f : α → β
g₁ g₂ : α → γ
e₁ e₂ : β → γ
h h₁ h₂ : ∀ (x : β), extend f (g₁ / g₂) (e₁ / e₂) x = (extend f g₁ e₁ / extend f g₂ e₂) x
⊢ extend f (g₁ / g₂) (e₁ / e₂) = extend f g₁ e₁ / extend f g₂ e₂

Tactic:
classical
  funext x
  simp [Function.extend_def, apply_dite₂]

Premises used: Function.extend_def, apply_dite₂
-- Module: Mathlib.Algebra.Group.Pi.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
b : β
f : α → β
g : β → γ
hg : Injective g
⊢ g ∘ f = const α (g b) ↔ f = const α b

Tactic:
hg.comp_left.eq_iff' rfl

Premises used: Function.Injective.eq_iff', Function.Injective.comp_left, rfl
-- Module: Mathlib.Algebra.Group.Pi.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : One β
inst_1 : One γ
f : α → β
g : β → γ
hg : Injective g
hg0 : g 1 = 1
⊢ g ∘ f = 1 ↔ f = 1

Tactic:
simpa [hg0, const_one] using comp_eq_const_iff 1 f hg

Premises used: Function.const_one, Function.comp_eq_const_iff, OfNat.ofNat
-- Module: Mathlib.Algebra.Group.Pi.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : One β
inst_1 : One γ
f : α → β
g : β → γ
hg : Injective g
hg0 : g 1 = 1
⊢ g ∘ f ≠ 1 ↔ f ≠ 1

Tactic:
(comp_eq_one_iff f hg hg0).ne

Premises used: Function.comp_eq_one_iff, Iff.ne
-- Module: Mathlib.Algebra.Group.Pi.Basic
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
rw₁ rw₂ : x = x
⊢ Pi.mulSingle (M := fun (x : I) ↦ α) i x j = x

Tactic:
rw [Subsingleton.elim j i, Pi.mulSingle_eq_same]

Premises used: Pi.mulSingle_eq_same, Subsingleton.elim
-- Module: Mathlib.Algebra.Group.Pi.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : One γ
⊢ Eq (α := α ⊕ β → γ) (Sum.elim 1 1) 1

Tactic:
Sum.elim_const_const 1

Premises used: Sum.elim_const_const, OfNat.ofNat
-- Module: Mathlib.Algebra.Group.Pi.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : One γ
i : α
c : γ
⊢ Eq (α := α ⊕ β → γ) (Sum.elim (Pi.mulSingle (M := fun (a : α) ↦ γ) i c) 1)
    (Pi.mulSingle (M := fun (j : α ⊕ β) ↦ γ) (inl i) c)

Tactic:
simp only [Pi.mulSingle, Sum.elim_update_left, elim_one_one]

Premises used: Sum.elim_one_one, Sum.elim_update_left, Pi.mulSingle
-- Module: Mathlib.Algebra.Group.Pi.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : One γ
i : β
c : γ
⊢ Eq (α := α ⊕ β → γ) (Sum.elim 1 (Pi.mulSingle (M := fun (a : β) ↦ γ) i c))
    (Pi.mulSingle (M := fun (j : α ⊕ β) ↦ γ) (inr i) c)

Tactic:
simp only [Pi.mulSingle, Sum.elim_update_right, elim_one_one]

Premises used: Sum.elim_one_one, Sum.elim_update_right, Pi.mulSingle
-- Module: Mathlib.Algebra.Group.Pi.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
a : α → γ
b : β → γ
inst : Inv γ
⊢ Sum.elim a⁻¹ b⁻¹ = (Sum.elim a b)⁻¹

Tactic:
(Sum.comp_elim Inv.inv a b).symm

Premises used: Inv.inv, Sum.comp_elim, Eq.symm
-- Module: Mathlib.Algebra.Group.Pi.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
a a' : α → γ
b b' : β → γ
inst : Mul γ
h : ∀ (x : α ⊕ β), Sum.elim (a * a') (b * b') x = (Sum.elim a b * Sum.elim a' b') x
⊢ Sum.elim (a * a') (b * b') = Sum.elim a b * Sum.elim a' b'

Tactic:
ext x
-- Module: Mathlib.Algebra.Group.Pi.Basic
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)
h₁ : ∀ (val : β), Sum.elim (a * a') (b * b') (inr val) = (Sum.elim a b * Sum.elim a' b') (inr val)
⊢ Sum.elim (a * a') (b * b') x = (Sum.elim a b * Sum.elim a' b') x

Tactic:
cases x
-- Module: Mathlib.Algebra.Group.Pi.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
a a' : α → γ
b b' : β → γ
inst : Mul γ
val : α
⊢ Sum.elim (a * a') (b * b') (inl val) = (Sum.elim a b * Sum.elim a' b') (inl val)

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Pi.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
a a' : α → γ
b b' : β → γ
inst : Mul γ
val : β
⊢ Sum.elim (a * a') (b * b') (inr val) = (Sum.elim a b * Sum.elim a' b') (inr val)

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Pi.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
a a' : α → γ
b b' : β → γ
inst : Div γ
h : ∀ (x : α ⊕ β), Sum.elim (a / a') (b / b') x = (Sum.elim a b / Sum.elim a' b') x
⊢ Sum.elim (a / a') (b / b') = Sum.elim a b / Sum.elim a' b'

Tactic:
ext x
-- Module: Mathlib.Algebra.Group.Pi.Basic
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)
h₁ : ∀ (val : β), Sum.elim (a / a') (b / b') (inr val) = (Sum.elim a b / Sum.elim a' b') (inr val)
⊢ Sum.elim (a / a') (b / b') x = (Sum.elim a b / Sum.elim a' b') x

Tactic:
cases x