awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.ListOfFn (goal)
Goal:
α : Type u_1
inst : Monoid α
l : List (Set α)
a : α
⊢ a ∈ l.prod ↔
    ∃ (l' : List ((s : Set α) × (↑s : Type u_1))),
      List.prod
            (List.map
              (fun (x : (s : Set α) × (↑s : Type u_1)) ↦ (↑(x.snd (β := fun (s : Set α) ↦ (↑s : Type u_1))) : α)) l') =
          a ∧
        List.map (Sigma.fst (β := fun (s : Set α) ↦ (↑s : Type u_1))) l' = l
have h : ∀ (n : ℕ) (f : Fin n → Set α),
  a ∈ (List.ofFn f).prod ↔
    ∃ (l' : List ((s : Set α) × (↑s : Type u_1))),
      List.prod
            (List.map
              (fun (x : (s : Set α) × (↑s : Type u_1)) ↦ (↑(x.snd (β := fun (s : Set α) ↦ (↑s : Type u_1))) : α)) l') =
          a ∧
        List.map (Sigma.fst (β := fun (s : Set α) ↦ (↑s : Type u_1))) l' = List.ofFn f
Tactic: induction l using List.ofFnRec with | _ n f
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.ListOfFn (goal)
Goal:
α : Type u_1
inst : Monoid α
a : α
n : ℕ
f : Fin n → Set α
⊢ a ∈ (List.ofFn f).prod ↔
    ∃ (l' : List ((s : Set α) × (↑s : Type u_1))),
      List.prod
            (List.map
              (fun (x : (s : Set α) × (↑s : Type u_1)) ↦ (↑(x.snd (β := fun (s : Set α) ↦ (↑s : Type u_1))) : α)) l') =
          a ∧
        List.map (Sigma.fst (β := fun (s : Set α) ↦ (↑s : Type u_1))) l' = List.ofFn f
have h : (∃ (f_1 : (i : Fin n) → (↑(f i) : Type u_1)), List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f_1 i) : α)) = a) ↔
  ∃ (x : Fin n → (s : Set α) × (↑s : Type u_1)),
    List.prod
          (List.ofFn
            ((fun (x : (s : Set α) × (↑s : Type u_1)) ↦ (↑(x.snd (β := fun (s : Set α) ↦ (↑s : Type u_1))) : α)) ∘ x)) =
        a ∧
      Sigma.fst (β := fun (s : Set α) ↦ (↑s : Type u_1)) ∘ x = f
Tactic: simp only [mem_prod_list_ofFn, List.exists_iff_exists_tuple, List.map_ofFn, List.ofFn_inj',
    Sigma.mk.inj_iff, and_left_comm, exists_and_left, exists_eq_left, heq_eq_eq]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.ListOfFn (goal)
Goal:
α : Type u_1
inst : Monoid α
a : α
n : ℕ
f : Fin n → Set α
⊢ (∃ (f_1 : (i : Fin n) → (↑(f i) : Type u_1)), List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f_1 i) : α)) = a) ↔
    ∃ (x : Fin n → (s : Set α) × (↑s : Type u_1)),
      List.prod
            (List.ofFn
              ((fun (x : (s : Set α) × (↑s : Type u_1)) ↦ (↑(x.snd (β := fun (s : Set α) ↦ (↑s : Type u_1))) : α)) ∘
                x)) =
          a ∧
        Sigma.fst (β := fun (s : Set α) ↦ (↑s : Type u_1)) ∘ x = f
have h : (∃ (f_1 : (i : Fin n) → (↑(f i) : Type u_1)), List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f_1 i) : α)) = a) →
  ∃ (x : Fin n → (s : Set α) × (↑s : Type u_1)),
    List.prod
          (List.ofFn
            ((fun (x : (s : Set α) × (↑s : Type u_1)) ↦ (↑(x.snd (β := fun (s : Set α) ↦ (↑s : Type u_1))) : α)) ∘ x)) =
        a ∧
      Sigma.fst (β := fun (s : Set α) ↦ (↑s : Type u_1)) ∘ x = f
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.ListOfFn (goal)
Goal:
α : Type u_1
inst : Monoid α
a : α
n : ℕ
f : Fin n → Set α
h :
  (∃ (f_1 : (i : Fin n) → (↑(f i) : Type u_1)), List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f_1 i) : α)) = a) →
    ∃ (x : Fin n → (s : Set α) × (↑s : Type u_1)),
      List.prod
            (List.ofFn
              ((fun (x : (s : Set α) × (↑s : Type u_1)) ↦ (↑(x.snd (β := fun (s : Set α) ↦ (↑s : Type u_1))) : α)) ∘
                x)) =
          a ∧
        Sigma.fst (β := fun (s : Set α) ↦ (↑s : Type u_1)) ∘ x = f
⊢ (∃ (f_1 : (i : Fin n) → (↑(f i) : Type u_1)), List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f_1 i) : α)) = a) ↔
    ∃ (x : Fin n → (s : Set α) × (↑s : Type u_1)),
      List.prod
            (List.ofFn
              ((fun (x : (s : Set α) × (↑s : Type u_1)) ↦ (↑(x.snd (β := fun (s : Set α) ↦ (↑s : Type u_1))) : α)) ∘
                x)) =
          a ∧
        Sigma.fst (β := fun (s : Set α) ↦ (↑s : Type u_1)) ∘ x = f
have h₁ : (∃ (x : Fin n → (s : Set α) × (↑s : Type u_1)),
    List.prod
          (List.ofFn
            ((fun (x : (s : Set α) × (↑s : Type u_1)) ↦ (↑(x.snd (β := fun (s : Set α) ↦ (↑s : Type u_1))) : α)) ∘ x)) =
        a ∧
      Sigma.fst (β := fun (s : Set α) ↦ (↑s : Type u_1)) ∘ x = f) →
  ∃ (f_1 : (i : Fin n) → (↑(f i) : Type u_1)), List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f_1 i) : α)) = a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.ListOfFn (goal)
Goal:
α : Type u_1
inst : Monoid α
s : Set α
a : α
n : ℕ
⊢ a ∈ s ^ n ↔ ∃ (f : Fin n → (↑s : Type u_1)), List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : α)) = a
have rw : a ∈ s ^ n ↔ Membership.mem (γ := Set α) (List.prod (List.ofFn (n := n) fun (a : Fin n) ↦ s)) a
Tactic: rw [← mem_prod_list_ofFn, List.ofFn_const, List.prod_replicate]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.ListOfFn (goal)
Goal:
α : Type u_1
inst : Monoid α
s : Set α
a : α
n : ℕ
rw : a ∈ s ^ n ↔ Membership.mem (γ := Set α) (List.prod (List.ofFn (n := n) fun (a : Fin n) ↦ s)) a
⊢ a ∈ s ^ n ↔ ∃ (f : Fin n → (↑s : Type u_1)), List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : α)) = a
have rw₁ : a ∈ s ^ n ↔ a ∈ (List.replicate n s).prod
Tactic: rw [← mem_prod_list_ofFn, List.ofFn_const, List.prod_replicate]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.ListOfFn (goal)
Goal:
α : Type u_1
inst : Monoid α
s : Set α
a : α
n : ℕ
rw : a ∈ s ^ n ↔ Membership.mem (γ := Set α) (List.prod (List.ofFn (n := n) fun (a : Fin n) ↦ s)) a
rw₁ : a ∈ s ^ n ↔ a ∈ (List.replicate n s).prod
⊢ a ∈ s ^ n ↔ ∃ (f : Fin n → (↑s : Type u_1)), List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : α)) = a
have rw₂ : a ∈ s ^ n ↔ a ∈ s ^ n
Tactic: rw [← mem_prod_list_ofFn, List.ofFn_const, List.prod_replicate]
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Scalar (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : SMul.{u_2, u_3} αᵐᵒᵖ β
inst_1 : SMul β γ
inst_2 : SMul α γ
a : α
s : Set β
t : Set γ
h : ∀ (a : α) (b : β) (c : γ), (op a • b) • c = b • a • c
⊢ (op a • s) • t = s • a • t
have h₁ : ∀ (x : γ), x ∈ (op a • s) • t ↔ x ∈ s • a • t
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Pointwise.Set.Small (goal)
Goal:
α : Type u_1
β : Type u_2
s t : Set α
inst : InvolutiveNeg α
inst_1 : Small.{u, u_1} (↑s : Type u_1)
⊢ Small.{u, u_1} (↑(-s) : Type u_1)
have rw : Small.{u, u_1} (↑((fun (x : α) ↦ -x) '' s) : Type u_1)
Tactic: rw [← Set.image_neg_eq_neg]
-- Lean 4 proof step from Mathlib.Algebra.Group.Prod (goal)
Goal:
M : Type u_3
N : Type u_4
inst : MulOneClass M
inst_1 : Mul N
b₁ b₂ : N
⊢ HMul.hMul (α := M × N) (1, b₁) (1, b₂) = (1, b₁ * b₂)
have rw : (HMul.hMul (α := M) 1 1, b₁ * b₂) = (1, b₁ * b₂)
Tactic: rw [mk_mul_mk, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Prod (goal)
Goal:
M : Type u_3
N : Type u_4
inst : MulOneClass M
inst_1 : Mul N
b₁ b₂ : N
rw : (HMul.hMul (α := M) 1 1, b₁ * b₂) = (1, b₁ * b₂)
⊢ HMul.hMul (α := M × N) (1, b₁) (1, b₂) = (1, b₁ * b₂)
have rw₁ : Eq (α := M × N) (1, b₁ * b₂) (1, b₁ * b₂)
Tactic: rw [mk_mul_mk, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Prod (goal)
Goal:
M : Type u_3
N : Type u_4
inst : Mul M
inst_1 : MulOneClass N
a₁ a₂ : M
⊢ HMul.hMul (α := M × N) (a₁, 1) (a₂, 1) = (a₁ * a₂, 1)
have rw : (a₁ * a₂, HMul.hMul (α := N) 1 1) = (a₁ * a₂, 1)
Tactic: rw [mk_mul_mk, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Prod (goal)
Goal:
M : Type u_3
N : Type u_4
inst : Mul M
inst_1 : MulOneClass N
a₁ a₂ : M
rw : (a₁ * a₂, HMul.hMul (α := N) 1 1) = (a₁ * a₂, 1)
⊢ HMul.hMul (α := M × N) (a₁, 1) (a₂, 1) = (a₁ * a₂, 1)
have rw₁ : Eq (α := M × N) (a₁ * a₂, 1) (a₁ * a₂, 1)
Tactic: rw [mk_mul_mk, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Prod (goal)
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : Semigroup M
inst_1 : Semigroup N
x x_1 x_2 : M × N
⊢ x * x_1 * x_2 = x * (x_1 * x_2)
have fst : (x * x_1 * x_2).1 = (x * (x_1 * x_2)).1
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Prod (goal)
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : Semigroup M
inst_1 : Semigroup N
x x_1 x_2 : M × N
fst : (x * x_1 * x_2).1 = (x * (x_1 * x_2)).1
⊢ x * x_1 * x_2 = x * (x_1 * x_2)
have snd : (x * x_1 * x_2).2 = (x * (x_1 * x_2)).2
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Prod (goal)
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : CommSemigroup G
inst_1 : CommSemigroup H
x x_1 : G × H
⊢ x * x_1 = x_1 * x
have fst : (x * x_1).1 = (x_1 * x).1
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Prod (goal)
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : CommSemigroup G
inst_1 : CommSemigroup H
x x_1 : G × H
fst : (x * x_1).1 = (x_1 * x).1
⊢ x * x_1 = x_1 * x
have snd : (x * x_1).2 = (x_1 * x).2
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Prod (goal)
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : MulOneClass M
inst_1 : MulOneClass N
x : M × N
⊢ 1 * x = x
have fst : (1 * x).1 = x.1
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Prod (goal)
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : MulOneClass M
inst_1 : MulOneClass N
x : M × N
fst : (1 * x).1 = x.1
⊢ 1 * x = x
have snd : (1 * x).2 = x.2
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Prod (goal)
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : MulOneClass M
inst_1 : MulOneClass N
x : M × N
⊢ x * 1 = x
have fst : (x * 1).1 = x.1
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Prod (goal)
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : MulOneClass M
inst_1 : MulOneClass N
x : M × N
fst : (x * 1).1 = x.1
⊢ x * 1 = x
have snd : (x * 1).2 = x.2
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Prod (goal)
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : Monoid M
inst_1 : Monoid N
inst_2 : IsMulTorsionFree M
inst_3 : IsMulTorsionFree N
n : ℕ
hn : n ≠ 0
a b : M × N
hab : Eq (α := M × N) ((fun (a : M × N) ↦ a ^ n) a) ((fun (a : M × N) ↦ a ^ n) b)
⊢ a = b
have fst : a.1 = b.1
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Prod (goal)
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : Monoid M
inst_1 : Monoid N
inst_2 : IsMulTorsionFree M
inst_3 : IsMulTorsionFree N
n : ℕ
hn : n ≠ 0
a b : M × N
hab : Eq (α := M × N) ((fun (a : M × N) ↦ a ^ n) a) ((fun (a : M × N) ↦ a ^ n) b)
fst : a.1 = b.1
⊢ a = b
have snd : a.2 = b.2
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Prod (goal)
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : Monoid M
inst_1 : Monoid N
inst_2 : IsMulTorsionFree M
inst_3 : IsMulTorsionFree N
n : ℕ
hn : n ≠ 0
a b : M × N
hab : Eq (α := M × N) ((fun (a : M × N) ↦ a ^ n) a) ((fun (a : M × N) ↦ a ^ n) b)
⊢ a.1 = b.1
have fst : Eq.{u_3 + 1} (α := M) ((fun (a : M) ↦ a ^ n) a.1) ((fun (a : M) ↦ a ^ n) b.1)
Tactic: apply pow_left_injective hn
-- Lean 4 proof step from Mathlib.Algebra.Group.Prod (goal)
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : Monoid M
inst_1 : Monoid N
inst_2 : IsMulTorsionFree M
inst_3 : IsMulTorsionFree N
n : ℕ
hn : n ≠ 0
a b : M × N
hab : Eq (α := M × N) ((fun (a : M × N) ↦ a ^ n) a) ((fun (a : M × N) ↦ a ^ n) b)
⊢ a.2 = b.2
have snd : Eq.{u_4 + 1} (α := N) ((fun (a : N) ↦ a ^ n) a.2) ((fun (a : N) ↦ a ^ n) b.2)
Tactic: apply pow_left_injective hn
-- Lean 4 proof step from Mathlib.Algebra.Group.Prod (goal)
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : DivInvMonoid G
inst_1 : DivInvMonoid H
x x_1 : G × H
⊢ x / x_1 = x * x_1⁻¹
have fst : (x / x_1).1 = (x * x_1⁻¹).1
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Prod (goal)
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : DivInvMonoid G
inst_1 : DivInvMonoid H
x x_1 : G × H
fst : (x / x_1).1 = (x * x_1⁻¹).1
⊢ x / x_1 = x * x_1⁻¹
have snd : (x / x_1).2 = (x * x_1⁻¹).2
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Prod (goal)
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : DivInvMonoid G
inst_1 : DivInvMonoid H
x : G × H
⊢ (DivInvMonoid.zpow 0 x.1, DivInvMonoid.zpow 0 x.2) = 1
have fst : (DivInvMonoid.zpow 0 x.1, DivInvMonoid.zpow 0 x.2).1 = 1.1
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Prod (goal)
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : DivInvMonoid G
inst_1 : DivInvMonoid H
x : G × H
fst : (DivInvMonoid.zpow 0 x.1, DivInvMonoid.zpow 0 x.2).1 = 1.1
⊢ (DivInvMonoid.zpow 0 x.1, DivInvMonoid.zpow 0 x.2) = 1
have snd : (DivInvMonoid.zpow 0 x.1, DivInvMonoid.zpow 0 x.2).2 = 1.2
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Prod (goal)
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : DivInvMonoid G
inst_1 : DivInvMonoid H
x : ℕ
x_1 : G × H
⊢ (DivInvMonoid.zpow (↑x.succ : ℤ) x_1.1, DivInvMonoid.zpow (↑x.succ : ℤ) x_1.2) =
    (DivInvMonoid.zpow (↑x : ℤ) x_1.1, DivInvMonoid.zpow (↑x : ℤ) x_1.2) * x_1
have fst : (DivInvMonoid.zpow (↑x.succ : ℤ) x_1.1, DivInvMonoid.zpow (↑x.succ : ℤ) x_1.2).1 =
  ((DivInvMonoid.zpow (↑x : ℤ) x_1.1, DivInvMonoid.zpow (↑x : ℤ) x_1.2) * x_1).1
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Prod (goal)
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : DivInvMonoid G
inst_1 : DivInvMonoid H
x : ℕ
x_1 : G × H
fst :
  (DivInvMonoid.zpow (↑x.succ : ℤ) x_1.1, DivInvMonoid.zpow (↑x.succ : ℤ) x_1.2).1 =
    ((DivInvMonoid.zpow (↑x : ℤ) x_1.1, DivInvMonoid.zpow (↑x : ℤ) x_1.2) * x_1).1
⊢ (DivInvMonoid.zpow (↑x.succ : ℤ) x_1.1, DivInvMonoid.zpow (↑x.succ : ℤ) x_1.2) =
    (DivInvMonoid.zpow (↑x : ℤ) x_1.1, DivInvMonoid.zpow (↑x : ℤ) x_1.2) * x_1
have snd : (DivInvMonoid.zpow (↑x.succ : ℤ) x_1.1, DivInvMonoid.zpow (↑x.succ : ℤ) x_1.2).2 =
  ((DivInvMonoid.zpow (↑x : ℤ) x_1.1, DivInvMonoid.zpow (↑x : ℤ) x_1.2) * x_1).2
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Prod (goal)
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : DivInvMonoid G
inst_1 : DivInvMonoid H
x : ℕ
x_1 : G × H
⊢ (DivInvMonoid.zpow (Int.negSucc x) x_1.1, DivInvMonoid.zpow (Int.negSucc x) x_1.2) =
    (DivInvMonoid.zpow (↑x.succ : ℤ) x_1.1, DivInvMonoid.zpow (↑x.succ : ℤ) x_1.2)⁻¹
have fst : (DivInvMonoid.zpow (Int.negSucc x) x_1.1, DivInvMonoid.zpow (Int.negSucc x) x_1.2).1 =
  (DivInvMonoid.zpow (↑x.succ : ℤ) x_1.1, DivInvMonoid.zpow (↑x.succ : ℤ) x_1.2)⁻¹.1
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Prod (goal)
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : DivInvMonoid G
inst_1 : DivInvMonoid H
x : ℕ
x_1 : G × H
fst :
  (DivInvMonoid.zpow (Int.negSucc x) x_1.1, DivInvMonoid.zpow (Int.negSucc x) x_1.2).1 =
    (DivInvMonoid.zpow (↑x.succ : ℤ) x_1.1, DivInvMonoid.zpow (↑x.succ : ℤ) x_1.2)⁻¹.1
⊢ (DivInvMonoid.zpow (Int.negSucc x) x_1.1, DivInvMonoid.zpow (Int.negSucc x) x_1.2) =
    (DivInvMonoid.zpow (↑x.succ : ℤ) x_1.1, DivInvMonoid.zpow (↑x.succ : ℤ) x_1.2)⁻¹
have snd : (DivInvMonoid.zpow (Int.negSucc x) x_1.1, DivInvMonoid.zpow (Int.negSucc x) x_1.2).2 =
  (DivInvMonoid.zpow (↑x.succ : ℤ) x_1.1, DivInvMonoid.zpow (↑x.succ : ℤ) x_1.2)⁻¹.2
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Prod (goal)
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : DivisionCommMonoid G
inst_1 : DivisionCommMonoid H
x x_1 : G × H
g₁ : G
h₁ : H
fst : G
snd : H
⊢ (g₁, h₁) * (fst, snd) = (fst, snd) * (g₁, h₁)
have rw : (fst * g₁, snd * h₁) = (fst, snd) * (g₁, h₁)
Tactic: rw [mk_mul_mk, mul_comm g₁, mul_comm h₁]
-- Lean 4 proof step from Mathlib.Algebra.Group.Prod (goal)
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : Group G
inst_1 : Group H
x : G × H
⊢ x⁻¹ * x = 1
have fst : (x⁻¹ * x).1 = 1.1
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Prod (goal)
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : Group G
inst_1 : Group H
x : G × H
fst : (x⁻¹ * x).1 = 1.1
⊢ x⁻¹ * x = 1
have snd : (x⁻¹ * x).2 = 1.2
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Prod (goal)
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : CommMonoid M
inst_1 : CommMonoid N
x x_1 : M × N
m₁ : M
n₁ : N
fst : M
snd : N
⊢ (m₁, n₁) * (fst, snd) = (fst, snd) * (m₁, n₁)
have rw : (m₁ * fst, n₁ * snd) = (fst, snd) * (m₁, n₁)
Tactic: rw [mk_mul_mk, mk_mul_mk, mul_comm m₁, mul_comm n₁]
-- Lean 4 proof step from Mathlib.Algebra.Group.Prod (goal)
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : CommMonoid M
inst_1 : CommMonoid N
x x_1 : M × N
m₁ : M
n₁ : N
fst : M
snd : N
rw : (m₁ * fst, n₁ * snd) = (fst, snd) * (m₁, n₁)
⊢ (m₁, n₁) * (fst, snd) = (fst, snd) * (m₁, n₁)
have rw₁ : (m₁ * fst, n₁ * snd) = (fst * m₁, snd * n₁)
Tactic: rw [mk_mul_mk, mk_mul_mk, mul_comm m₁, mul_comm n₁]
-- Lean 4 proof step from Mathlib.Algebra.Group.Prod (goal)
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : CommMonoid M
inst_1 : CommMonoid N
x x_1 : M × N
m₁ : M
n₁ : N
fst : M
snd : N
rw : (m₁ * fst, n₁ * snd) = (fst, snd) * (m₁, n₁)
rw₁ : (m₁ * fst, n₁ * snd) = (fst * m₁, snd * n₁)
⊢ (m₁, n₁) * (fst, snd) = (fst, snd) * (m₁, n₁)
have rw₂ : (fst * m₁, n₁ * snd) = (fst * m₁, snd * n₁)
Tactic: rw [mk_mul_mk, mk_mul_mk, mul_comm m₁, mul_comm n₁]
-- Lean 4 proof step from Mathlib.Algebra.Group.Prod (goal)
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : CommMonoid M
inst_1 : CommMonoid N
x x_1 : M × N
m₁ : M
n₁ : N
fst : M
snd : N
rw : (m₁ * fst, n₁ * snd) = (fst, snd) * (m₁, n₁)
rw₁ : (m₁ * fst, n₁ * snd) = (fst * m₁, snd * n₁)
rw₂ : (fst * m₁, n₁ * snd) = (fst * m₁, snd * n₁)
⊢ (m₁, n₁) * (fst, snd) = (fst, snd) * (m₁, n₁)
have rw₃ : (fst * m₁, snd * n₁) = (fst * m₁, snd * n₁)
Tactic: rw [mk_mul_mk, mk_mul_mk, mul_comm m₁, mul_comm n₁]
-- Lean 4 proof step from Mathlib.Algebra.Group.Prod (goal)
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : CommGroup G
inst_1 : CommGroup H
x x_1 : G × H
g₁ : G
h₁ : H
fst : G
snd : H
⊢ (g₁, h₁) * (fst, snd) = (fst, snd) * (g₁, h₁)
have rw : (g₁ * fst, h₁ * snd) = (fst, snd) * (g₁, h₁)
Tactic: rw [mk_mul_mk, mk_mul_mk, mul_comm g₁, mul_comm h₁]
-- Lean 4 proof step from Mathlib.Algebra.Group.Prod (goal)
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : CommGroup G
inst_1 : CommGroup H
x x_1 : G × H
g₁ : G
h₁ : H
fst : G
snd : H
rw : (g₁ * fst, h₁ * snd) = (fst, snd) * (g₁, h₁)
⊢ (g₁, h₁) * (fst, snd) = (fst, snd) * (g₁, h₁)
have rw₁ : (g₁ * fst, h₁ * snd) = (fst * g₁, snd * h₁)
Tactic: rw [mk_mul_mk, mk_mul_mk, mul_comm g₁, mul_comm h₁]
-- Lean 4 proof step from Mathlib.Algebra.Group.Prod (goal)
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : CommGroup G
inst_1 : CommGroup H
x x_1 : G × H
g₁ : G
h₁ : H
fst : G
snd : H
rw : (g₁ * fst, h₁ * snd) = (fst, snd) * (g₁, h₁)
rw₁ : (g₁ * fst, h₁ * snd) = (fst * g₁, snd * h₁)
⊢ (g₁, h₁) * (fst, snd) = (fst, snd) * (g₁, h₁)
have rw₂ : (fst * g₁, h₁ * snd) = (fst * g₁, snd * h₁)
Tactic: rw [mk_mul_mk, mk_mul_mk, mul_comm g₁, mul_comm h₁]
-- Lean 4 proof step from Mathlib.Algebra.Group.Prod (goal)
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : CommGroup G
inst_1 : CommGroup H
x x_1 : G × H
g₁ : G
h₁ : H
fst : G
snd : H
rw : (g₁ * fst, h₁ * snd) = (fst, snd) * (g₁, h₁)
rw₁ : (g₁ * fst, h₁ * snd) = (fst * g₁, snd * h₁)
rw₂ : (fst * g₁, h₁ * snd) = (fst * g₁, snd * h₁)
⊢ (g₁, h₁) * (fst, snd) = (fst, snd) * (g₁, h₁)
have rw₃ : (fst * g₁, snd * h₁) = (fst * g₁, snd * h₁)
Tactic: rw [mk_mul_mk, mk_mul_mk, mul_comm g₁, mul_comm h₁]
-- Lean 4 proof step from Mathlib.Algebra.Group.Prod (goal)
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : Monoid M
inst_1 : Monoid N
x : Prod.{u_3, u_4} Mˣ Nˣ
u₁ : Mˣ
u₂ : Nˣ
⊢ (MonoidHom.prod (Units.map (MonoidHom.fst M N)) (Units.map (MonoidHom.snd M N)) : (a : (M × N)ˣ) → Mˣ × Nˣ)
      ((fun (u : Prod.{u_3, u_4} Mˣ Nˣ) ↦
          { val := ((↑u.1 : M), (↑u.2 : N)), inv := ((↑u.1⁻¹ : M), (↑u.2⁻¹ : N)), val_inv := ⋯, inv_val := ⋯ :
            (M × N)ˣ })
        (u₁, u₂)) =
    (u₁, u₂)
have simp : (MonoidHom.mk' (fun (u : (M × N)ˣ) ↦ { val := (↑u : M × N).1, inv := (↑u⁻¹ : M × N).1, val_inv := sorry, inv_val := sorry }) sorry :
        (a : (M × N)ˣ) → Mˣ)
      { val := ((↑u₁ : M), (↑u₂ : N)), inv := ((↑u₁⁻¹ : M), (↑u₂⁻¹ : N)), val_inv := sorry, inv_val := sorry } =
    u₁ ∧
  (MonoidHom.mk' (fun (u : (M × N)ˣ) ↦ { val := (↑u : M × N).2, inv := (↑u⁻¹ : M × N).2, val_inv := sorry, inv_val := sorry })
          sorry :
        (a : (M × N)ˣ) → Nˣ)
      { val := ((↑u₁ : M), (↑u₂ : N)), inv := ((↑u₁⁻¹ : M), (↑u₂⁻¹ : N)), val_inv := sorry, inv_val := sorry } =
    u₂
Tactic: simp only [Units.map, MonoidHom.coe_fst, Units.inv_eq_val_inv,
      MonoidHom.coe_snd, MonoidHom.prod_apply, Prod.mk.injEq]
-- Lean 4 proof step from Mathlib.Algebra.Group.Semiconj.Basic (goal)
Goal:
G : Type u_1
inst : DivisionMonoid G
a x y : G
⊢ SemiconjBy a⁻¹ x⁻¹ y⁻¹ ↔ SemiconjBy a y x
have simp_rw : a⁻¹ * x⁻¹ = y⁻¹ * a⁻¹ ↔ a * y = x * a
Tactic: simp_rw [SemiconjBy, ← mul_inv_rev, inv_inj, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Semiconj.Basic (goal)
Goal:
G : Type u_1
inst : DivisionMonoid G
a x y : G
simp_rw : a⁻¹ * x⁻¹ = y⁻¹ * a⁻¹ ↔ a * y = x * a
⊢ SemiconjBy a⁻¹ x⁻¹ y⁻¹ ↔ SemiconjBy a y x
have simp_rw₁ : (x * a)⁻¹ = (a * y)⁻¹ ↔ a * y = x * a
Tactic: simp_rw [SemiconjBy, ← mul_inv_rev, inv_inj, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Semiconj.Basic (goal)
Goal:
G : Type u_1
inst : DivisionMonoid G
a x y : G
simp_rw : a⁻¹ * x⁻¹ = y⁻¹ * a⁻¹ ↔ a * y = x * a
simp_rw₁ : (x * a)⁻¹ = (a * y)⁻¹ ↔ a * y = x * a
⊢ SemiconjBy a⁻¹ x⁻¹ y⁻¹ ↔ SemiconjBy a y x
have simp_rw₂ : x * a = a * y ↔ a * y = x * a
Tactic: simp_rw [SemiconjBy, ← mul_inv_rev, inv_inj, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Semiconj.Basic (goal)
Goal:
G : Type u_1
inst : Group G
a x y : G
⊢ SemiconjBy a⁻¹ y x ↔ SemiconjBy a x y
have simp_rw : a⁻¹ * y = x * a⁻¹ ↔ a * x = y * a
Tactic: simp_rw [SemiconjBy, eq_mul_inv_iff_mul_eq, mul_assoc, inv_mul_eq_iff_eq_mul, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Semiconj.Basic (goal)
Goal:
G : Type u_1
inst : Group G
a x y : G
simp_rw : a⁻¹ * y = x * a⁻¹ ↔ a * x = y * a
⊢ SemiconjBy a⁻¹ y x ↔ SemiconjBy a x y
have simp_rw₁ : a⁻¹ * y * a = x ↔ a * x = y * a
Tactic: simp_rw [SemiconjBy, eq_mul_inv_iff_mul_eq, mul_assoc, inv_mul_eq_iff_eq_mul, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Semiconj.Basic (goal)
Goal:
G : Type u_1
inst : Group G
a x y : G
simp_rw : a⁻¹ * y = x * a⁻¹ ↔ a * x = y * a
simp_rw₁ : a⁻¹ * y * a = x ↔ a * x = y * a
⊢ SemiconjBy a⁻¹ y x ↔ SemiconjBy a x y
have simp_rw₂ : a⁻¹ * (y * a) = x ↔ a * x = y * a
Tactic: simp_rw [SemiconjBy, eq_mul_inv_iff_mul_eq, mul_assoc, inv_mul_eq_iff_eq_mul, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Semiconj.Basic (goal)
Goal:
G : Type u_1
inst : Group G
a x y : G
simp_rw : a⁻¹ * y = x * a⁻¹ ↔ a * x = y * a
simp_rw₁ : a⁻¹ * y * a = x ↔ a * x = y * a
simp_rw₂ : a⁻¹ * (y * a) = x ↔ a * x = y * a
⊢ SemiconjBy a⁻¹ y x ↔ SemiconjBy a x y
have simp_rw₃ : y * a = a * x ↔ a * x = y * a
Tactic: simp_rw [SemiconjBy, eq_mul_inv_iff_mul_eq, mul_assoc, inv_mul_eq_iff_eq_mul, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Semiconj.Basic (goal)
Goal:
G : Type u_1
inst : Group G
a x y : G
⊢ SemiconjBy a x⁻¹ y⁻¹ ↔ SemiconjBy a x y
have rw : SemiconjBy a⁻¹ y⁻¹ x⁻¹ ↔ SemiconjBy a x y
Tactic: rw [← inv_symm_left_iff, inv_inv_symm_iff]
-- Lean 4 proof step from Mathlib.Algebra.Group.Semiconj.Basic (goal)
Goal:
G : Type u_1
inst : Group G
a x y : G
rw : SemiconjBy a⁻¹ y⁻¹ x⁻¹ ↔ SemiconjBy a x y
⊢ SemiconjBy a x⁻¹ y⁻¹ ↔ SemiconjBy a x y
have rw₁ : SemiconjBy a x y ↔ SemiconjBy a x y
Tactic: rw [← inv_symm_left_iff, inv_inv_symm_iff]