awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : Group α
s t : Set α
x : αᵐᵒᵖ
a : α
h : a ∈ x • s
ha : a ∈ t
⊢ ∃ (a : α) (b : α), (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = unop x
have mp : ∀ (b : α) (hb : b ∈ s) (h : x • b ∈ x • s) (ha : x • b ∈ t), ∃ (a : α) (b : α), (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = unop x
Tactic: obtain ⟨b, hb, rfl⟩ := mem_smul_set.mp h
Cleared hypotheses: a, h, ha
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pointwise.Set.Basic (hypothesis)
Goal:
α : Type u_2
inst : Group α
s t : Set α
x : αᵐᵒᵖ
a b : α
H : a⁻¹ * b = unop x
ha : a ∈ s
hb : b ∈ t
⊢ (x • s ∩ t).Nonempty
have this : op (a⁻¹ * b) = x
Tactic: have : MulOpposite.op (a⁻¹ * b) = x := congr_arg MulOpposite.op H
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : Group α
s t : Set α
x : αᵐᵒᵖ
⊢ x • s ∩ t ≠ ∅ ↔ ∃ (a : α) (b : α), (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = unop x
have rw : (x • s ∩ t).Nonempty ↔ ∃ (a : α) (b : α), (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = unop x
Tactic: rw [← nonempty_iff_ne_empty, op_smul_inter_nonempty_iff]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : Group α
s t : Set α
x : αᵐᵒᵖ
rw : (x • s ∩ t).Nonempty ↔ ∃ (a : α) (b : α), (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = unop x
⊢ x • s ∩ t ≠ ∅ ↔ ∃ (a : α) (b : α), (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = unop x
have rw₁ : (∃ (a : α) (b : α), (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = unop x) ↔ ∃ (a : α) (b : α), (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = unop x
Tactic: rw [← nonempty_iff_ne_empty, op_smul_inter_nonempty_iff]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : MulAction α β
s : Set β
⊢ Eq.{u_3 + 1} (α := Set β) (⋃ (g : α), g • s) {a : β | ∃ (g : α), g • a ∈ s}
have simp_rw : Eq.{u_3 + 1} (α := Set β) (⋃ (g : α), g • s) (⋃ (i : α), {x : β | i • x ∈ s})
Tactic: simp_rw [← iUnion_setOf, ← iUnion_inv_smul, ← preimage_smul, preimage]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : MulAction α β
s : Set β
simp_rw : Eq.{u_3 + 1} (α := Set β) (⋃ (g : α), g • s) (⋃ (i : α), {x : β | i • x ∈ s})
⊢ Eq.{u_3 + 1} (α := Set β) (⋃ (g : α), g • s) {a : β | ∃ (g : α), g • a ∈ s}
have simp_rw₁ : Eq.{u_3 + 1} (α := Set β) (⋃ (g : α), g⁻¹ • s) (⋃ (i : α), {x : β | i • x ∈ s})
Tactic: simp_rw [← iUnion_setOf, ← iUnion_inv_smul, ← preimage_smul, preimage]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : MulAction α β
s : Set β
simp_rw : Eq.{u_3 + 1} (α := Set β) (⋃ (g : α), g • s) (⋃ (i : α), {x : β | i • x ∈ s})
simp_rw₁ : Eq.{u_3 + 1} (α := Set β) (⋃ (g : α), g⁻¹ • s) (⋃ (i : α), {x : β | i • x ∈ s})
⊢ Eq.{u_3 + 1} (α := Set β) (⋃ (g : α), g • s) {a : β | ∃ (g : α), g • a ∈ s}
have simp_rw₂ : Eq.{u_3 + 1} (α := Set β) (⋃ (g : α), (fun (x : β) ↦ g • x) ⁻¹' s) (⋃ (i : α), {x : β | i • x ∈ s})
Tactic: simp_rw [← iUnion_setOf, ← iUnion_inv_smul, ← preimage_smul, preimage]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : Group α
a : α
s : Set α
⊢ (a • s)⁻¹ = op a⁻¹ • s⁻¹
have h : ∀ (x : α), x ∈ (a • s)⁻¹ ↔ x ∈ op a⁻¹ • s⁻¹
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : Group α
a : α
s : Set α
⊢ (op a • s)⁻¹ = a⁻¹ • s⁻¹
have h : ∀ (x : α), x ∈ (op a • s)⁻¹ ↔ x ∈ a⁻¹ • s⁻¹
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : MulAction α β
s : Set β
⊢ Pairwise.{u_2} (α := α) (onFun.{u_2 + 1, u_3 + 1, 1} (β := Set β) Disjoint fun (a : α) ↦ a • s) ↔
    ∀ (a : α), (a • s ∩ s).Nonempty → a = 1
have simp_rw : (∀ ⦃i j : α⦄, ((j⁻¹ * i) • s ∩ s).Nonempty → i = j) ↔ ∀ (a : α), (a • s ∩ s).Nonempty → a = 1
Tactic: simp_rw [Pairwise, disjoint_smul_set_right, ← mul_smul,
    ← not_imp_not (b := _ ≠ _), not_ne_iff, not_disjoint_iff_nonempty_inter]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : Group α
s t : Set α
a b : α
⊢ ∃ (z : α), a • s ∩ b • t ⊆ z • (s⁻¹ * s ∩ (t⁻¹ * t))
have inl : ∀ (hAB : a • s ∩ b • t = ∅), ∃ (z : α), a • s ∩ b • t ⊆ z • (s⁻¹ * s ∩ (t⁻¹ * t))
Tactic: obtain hAB | ⟨z, hzA, hzB⟩ := (a • s ∩ b • t).eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : Group α
s t : Set α
a b : α
inl : ∀ (hAB : a • s ∩ b • t = ∅), ∃ (z : α), a • s ∩ b • t ⊆ z • (s⁻¹ * s ∩ (t⁻¹ * t))
⊢ ∃ (z : α), a • s ∩ b • t ⊆ z • (s⁻¹ * s ∩ (t⁻¹ * t))
have inr : ∀ (z : α) (hzA : z ∈ a • s) (hzB : z ∈ b • t), ∃ (z : α), a • s ∩ b • t ⊆ z • (s⁻¹ * s ∩ (t⁻¹ * t))
Tactic: obtain hAB | ⟨z, hzA, hzB⟩ := (a • s ∩ b • t).eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : Group α
s t : Set α
a b z : α
hzA : z ∈ a • s
hzB : z ∈ b • t
⊢ ∃ (z : α), a • s ∩ b • t ⊆ z • (s⁻¹ * s ∩ (t⁻¹ * t))
have inr : a • s ∩ b • t ⊆ z • (s⁻¹ * s ∩ (t⁻¹ * t))
Tactic: refine ⟨z, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : Group α
s t : Set α
a b z : α
hzA : z ∈ a • s
hzB : z ∈ b • t
⊢ a • s ∩ b • t ⊆ z • s⁻¹ * s ∩ (z • t⁻¹ * t)
have h₁ : a • s ⊆ z • s⁻¹ * s
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : Group α
s t : Set α
a b z : α
hzA : z ∈ a • s
hzB : z ∈ b • t
h₁ : a • s ⊆ z • s⁻¹ * s
⊢ a • s ∩ b • t ⊆ z • s⁻¹ * s ∩ (z • t⁻¹ * t)
have h₂ : b • t ⊆ z • t⁻¹ * t
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : Group α
s t : Set α
a b z : α
hzA : z ∈ a • s
hzB : z ∈ b • t
⊢ a • s ⊆ z • s⁻¹ * s
have h₁ : a ∈ z • s⁻¹
Tactic: apply smul_set_subset_mul
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : Group α
s t : Set α
a b z : α
hzA : z ∈ a • s
hzB : z ∈ b • t
⊢ b • t ⊆ z • t⁻¹ * t
have h₂ : b ∈ z • t⁻¹
Tactic: apply smul_set_subset_mul
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : Group α
s t : Set α
a b z : α
hzA : z ∈ a • s
hzB : z ∈ b • t
⊢ z • s⁻¹ * s ∩ (z • t⁻¹ * t) = z • (s⁻¹ * s ∩ (t⁻¹ * t))
have simp_rw : z • s⁻¹ * s ∩ (z • t⁻¹ * t) = z • (s⁻¹ * s) ∩ z • (t⁻¹ * t)
Tactic: simp_rw [Set.smul_set_inter, smul_mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : Group α
s t : Set α
a b z : α
hzA : z ∈ a • s
hzB : z ∈ b • t
⊢ a • s ∩ b • t ⊆ z • (s⁻¹ * s ∩ (t⁻¹ * t))
have a₁ : a • s ∩ b • t ⊆ z • s⁻¹ * s ∩ (z • t⁻¹ * t)
Tactic: calc
    a • s ∩ b • t ⊆ (z • s⁻¹) * s ∩ ((z • t⁻¹) * t) := by
      gcongr <;> apply smul_set_subset_mul <;> simpa
    _ = z • ((s⁻¹ * s) ∩ (t⁻¹ * t)) := by simp_rw [Set.smul_set_inter, smul_mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : Group α
s t : Set α
a b z : α
hzA : z ∈ a • s
hzB : z ∈ b • t
a₁ : a • s ∩ b • t ⊆ z • s⁻¹ * s ∩ (z • t⁻¹ * t)
⊢ a • s ∩ b • t ⊆ z • (s⁻¹ * s ∩ (t⁻¹ * t))
have a₂ : z • s⁻¹ * s ∩ (z • t⁻¹ * t) = z • (s⁻¹ * s ∩ (t⁻¹ * t))
Tactic: calc
    a • s ∩ b • t ⊆ (z • s⁻¹) * s ∩ ((z • t⁻¹) * t) := by
      gcongr <;> apply smul_set_subset_mul <;> simpa
    _ = z • ((s⁻¹ * s) ∩ (t⁻¹ * t)) := by simp_rw [Set.smul_set_inter, smul_mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pointwise.Set.Basic (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : CommGroup β
inst_2 : FunLike F α β
inst_3 : MonoidHomClass F α β
x : α × β
s : Set α
f : F
⊢ HSMul.hSMul (β := Set (α × β)) x (graphOn (⇑f : (a : α) → β) s) =
    graphOn
      (fun (a : α) ↦ HMul.hMul (β := β) (HDiv.hDiv (β := β) x.2 ((f : (a : α) → β) x.1 : β)) ((f : (a : α) → β) a : β))
      (x.1 • s)
have h : ∀ (a : α) (b : β),
  (a, b) ∈ HSMul.hSMul (β := Set (α × β)) x (graphOn (⇑f : (a : α) → β) s) ↔
    Membership.mem (γ := Set (α × β))
      (graphOn
        (fun (a : α) ↦
          HMul.hMul (β := β) (HDiv.hDiv (β := β) x.2 ((f : (a : α) → β) x.1 : β)) ((f : (a : α) → β) a : β))
        (x.1 • s))
      (a, b)
Tactic: ext ⟨a, b⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : CommGroup α
a : α
s : Set α
b : α
t : Set α
⊢ a • s / b • t = (a / b) • (s / t)
have simp_rw : HDiv.hDiv (α := Set α) ((fun (x : α) ↦ a • x) '' s) ((fun (x : α) ↦ b • x) '' t) =
  (fun (x : α) ↦ (a / b) • x) '' (s / t)
Tactic: simp_rw [← image_smul, smul_eq_mul, ← singleton_mul, mul_div_mul_comm _ s,
    singleton_div_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : CommGroup α
a : α
s : Set α
b : α
t : Set α
simp_rw :
  HDiv.hDiv (α := Set α) ((fun (x : α) ↦ a • x) '' s) ((fun (x : α) ↦ b • x) '' t) =
    (fun (x : α) ↦ (a / b) • x) '' (s / t)
⊢ a • s / b • t = (a / b) • (s / t)
have simp_rw₁ : HDiv.hDiv (α := Set α) ((fun (a_1 : α) ↦ a * a_1) '' s) ((fun (a : α) ↦ b * a) '' t) =
  (fun (a_1 : α) ↦ a / b * a_1) '' (s / t)
Tactic: simp_rw [← image_smul, smul_eq_mul, ← singleton_mul, mul_div_mul_comm _ s,
    singleton_div_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : CommGroup α
a : α
s : Set α
b : α
t : Set α
simp_rw :
  HDiv.hDiv (α := Set α) ((fun (x : α) ↦ a • x) '' s) ((fun (x : α) ↦ b • x) '' t) =
    (fun (x : α) ↦ (a / b) • x) '' (s / t)
simp_rw₁ :
  HDiv.hDiv (α := Set α) ((fun (a_1 : α) ↦ a * a_1) '' s) ((fun (a : α) ↦ b * a) '' t) =
    (fun (a_1 : α) ↦ a / b * a_1) '' (s / t)
⊢ a • s / b • t = (a / b) • (s / t)
have simp_rw₂ : {a} * s / ({b} * t) = {a / b} * (s / t)
Tactic: simp_rw [← image_smul, smul_eq_mul, ← singleton_mul, mul_div_mul_comm _ s,
    singleton_div_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pointwise.Set.Basic (goal)
Goal:
α : Type u_2
inst : CommGroup α
a : α
s : Set α
b : α
t : Set α
simp_rw :
  HDiv.hDiv (α := Set α) ((fun (x : α) ↦ a • x) '' s) ((fun (x : α) ↦ b • x) '' t) =
    (fun (x : α) ↦ (a / b) • x) '' (s / t)
simp_rw₁ :
  HDiv.hDiv (α := Set α) ((fun (a_1 : α) ↦ a * a_1) '' s) ((fun (a : α) ↦ b * a) '' t) =
    (fun (a_1 : α) ↦ a / b * a_1) '' (s / t)
simp_rw₂ : {a} * s / ({b} * t) = {a / b} * (s / t)
⊢ a • s / b • t = (a / b) • (s / t)
have simp_rw₃ : HDiv.hDiv (α := Set α) {a} {b} * (s / t) = {a / b} * (s / t)
Tactic: simp_rw [← image_smul, smul_eq_mul, ← singleton_mul, mul_div_mul_comm _ s,
    singleton_div_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pretransitive (goal)
Goal:
G : Type u_2
X : Type u_5
inst : Group G
inst_1 : MulAction G X
x₀ : X
ha : ∀ (x : X), ∃ (g : G), g • x₀ = x
⊢ IsPretransitive G X
have exists_smul_eq : ∀ (x y : X), ∃ (g : G), g • x = y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pretransitive (goal)
Goal:
G : Type u_2
X : Type u_5
inst : Group G
inst_1 : MulAction G X
x₀ : X
ha : ∀ (x : X), ∃ (g : G), g • x₀ = x
x y : X
⊢ ∃ (g : G), g • x = y
have exists_smul_eq : ∀ (g : G), ∃ (g_1 : G), g_1 • g • x₀ = y
Tactic: rcases ha x with ⟨g, rfl⟩
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Pretransitive (goal)
Goal:
G : Type u_2
X : Type u_5
inst : Group G
inst_1 : MulAction G X
x₀ : X
ha : ∀ (x : X), ∃ (g : G), g • x₀ = x
y : X
g : G
⊢ ∃ (g_1 : G), g_1 • g • x₀ = y
have exists_smul_eq : ∀ (h : G), ∃ (g_1 : G), g_1 • g • x₀ = h • x₀
Tactic: rcases ha y with ⟨h, rfl⟩
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Prod (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst : SMul M α
inst_1 : SMul M β
inst_2 : SMul N α
inst_3 : SMul N β
a : M
x : α × β
inst_4 : SMul M N
inst_5 : IsScalarTower M N α
inst_6 : IsScalarTower M N β
x_1 : M
x_2 : N
x_3 : α × β
⊢ (x_1 • x_2) • x_3 = x_1 • x_2 • x_3
have fst : ((x_1 • x_2) • x_3).1 = (x_1 • x_2 • x_3).1
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Prod (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst : SMul M α
inst_1 : SMul M β
inst_2 : SMul N α
inst_3 : SMul N β
a : M
x : α × β
inst_4 : SMul M N
inst_5 : IsScalarTower M N α
inst_6 : IsScalarTower M N β
x_1 : M
x_2 : N
x_3 : α × β
fst : ((x_1 • x_2) • x_3).1 = (x_1 • x_2 • x_3).1
⊢ (x_1 • x_2) • x_3 = x_1 • x_2 • x_3
have snd : ((x_1 • x_2) • x_3).2 = (x_1 • x_2 • x_3).2
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Prod (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst : SMul M α
inst_1 : SMul M β
inst_2 : SMul N α
inst_3 : SMul N β
a : M
x : α × β
inst_4 : SMulCommClass M N α
inst_5 : SMulCommClass M N β
x_1 : M
x_2 : N
x_3 : α × β
⊢ x_1 • x_2 • x_3 = x_2 • x_1 • x_3
have fst : (x_1 • x_2 • x_3).1 = (x_2 • x_1 • x_3).1
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Prod (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst : SMul M α
inst_1 : SMul M β
inst_2 : SMul N α
inst_3 : SMul N β
a : M
x : α × β
inst_4 : SMulCommClass M N α
inst_5 : SMulCommClass M N β
x_1 : M
x_2 : N
x_3 : α × β
fst : (x_1 • x_2 • x_3).1 = (x_2 • x_1 • x_3).1
⊢ x_1 • x_2 • x_3 = x_2 • x_1 • x_3
have snd : (x_1 • x_2 • x_3).2 = (x_2 • x_1 • x_3).2
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Prod (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : MulAction M α
inst_2 : MulAction M β
x x_1 : M
x_2 : α × β
⊢ (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.Action.Prod (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : MulAction M α
inst_2 : MulAction M β
x x_1 : M
x_2 : α × β
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.Action.Prod (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : MulAction M α
inst_2 : MulAction M β
x : α × β
⊢ HSMul.hSMul (α := M) 1 x = x
have fst : (HSMul.hSMul (α := M) 1 x).1 = x.1
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Prod (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : MulAction M α
inst_2 : MulAction M β
x : α × β
fst : (HSMul.hSMul (α := M) 1 x).1 = x.1
⊢ HSMul.hSMul (α := M) 1 x = x
have snd : (HSMul.hSMul (α := M) 1 x).2 = x.2
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Prod (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulAction M α
inst_3 : MulAction N α
inst_4 : SMulCommClass M N α
x y : M × N
a : α
⊢ (x * y) • a = x • y • a
have change : (x.1 * y.1) • (x.2 * y.2) • a = x.1 • x.2 • y.1 • y.2 • a
Tactic: change (x.1 * y.1) • (x.2 * y.2) • a = x.1 • x.2 • y.1 • y.2 • a
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Prod (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulAction M α
inst_3 : MulAction N α
inst_4 : SMulCommClass M N α
x y : M × N
a : α
⊢ (x.1 * y.1) • (x.2 * y.2) • a = x.1 • x.2 • y.1 • y.2 • a
have rw : x.1 • y.1 • (x.2 * y.2) • a = x.1 • x.2 • y.1 • y.2 • a
Tactic: rw [mul_smul, mul_smul, smul_comm y.1 x.2]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Prod (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulAction M α
inst_3 : MulAction N α
inst_4 : SMulCommClass M N α
x y : M × N
a : α
rw : x.1 • y.1 • (x.2 * y.2) • a = x.1 • x.2 • y.1 • y.2 • a
⊢ (x.1 * y.1) • (x.2 * y.2) • a = x.1 • x.2 • y.1 • y.2 • a
have rw₁ : x.1 • y.1 • x.2 • y.2 • a = x.1 • x.2 • y.1 • y.2 • a
Tactic: rw [mul_smul, mul_smul, smul_comm y.1 x.2]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Prod (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulAction M α
inst_3 : MulAction N α
inst_4 : SMulCommClass M N α
x y : M × N
a : α
rw : x.1 • y.1 • (x.2 * y.2) • a = x.1 • x.2 • y.1 • y.2 • a
rw₁ : x.1 • y.1 • x.2 • y.2 • a = x.1 • x.2 • y.1 • y.2 • a
⊢ (x.1 * y.1) • (x.2 * y.2) • a = x.1 • x.2 • y.1 • y.2 • a
have rw₂ : x.1 • x.2 • y.1 • y.2 • a = x.1 • x.2 • y.1 • y.2 • a
Tactic: rw [mul_smul, mul_smul, smul_comm y.1 x.2]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Prod (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : Monoid N
x : MulAction (M × N) α
instM : MulAction M α := compHom (M := M × N) α (MonoidHom.inl M N)
instN : MulAction N α := compHom (M := M × N) α (MonoidHom.inr M N)
m : M
n : N
a : α
⊢ m • n • a = n • m • a
have change : HSMul.hSMul (α := M × N) (m, 1) (HSMul.hSMul (α := M × N) (1, n) a) =
  HSMul.hSMul (α := M × N) (1, n) (HSMul.hSMul (α := M × N) (m, 1) a)
Tactic: change (m, (1 : N)) • ((1 : M), n) • a = ((1 : M), n) • (m, (1 : N)) • a
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Prod (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : Monoid N
x : MulAction (M × N) α
instM : MulAction M α := compHom (M := M × N) α (MonoidHom.inl M N)
instN : MulAction N α := compHom (M := M × N) α (MonoidHom.inr M N)
m : M
n : N
a : α
⊢ HSMul.hSMul (α := M × N) (m, 1) (HSMul.hSMul (α := M × N) (1, n) a) =
    HSMul.hSMul (α := M × N) (1, n) (HSMul.hSMul (α := M × N) (m, 1) a)
have simp_rw : ((m, 1) * (1, n)) • a = ((1, n) * (m, 1)) • a
Tactic: simp_rw [smul_smul, Prod.mk_mul_mk, mul_one, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Prod (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : Monoid N
x : MulAction (M × N) α
instM : MulAction M α := compHom (M := M × N) α (MonoidHom.inl M N)
instN : MulAction N α := compHom (M := M × N) α (MonoidHom.inr M N)
m : M
n : N
a : α
simp_rw : ((m, 1) * (1, n)) • a = ((1, n) * (m, 1)) • a
⊢ HSMul.hSMul (α := M × N) (m, 1) (HSMul.hSMul (α := M × N) (1, n) a) =
    HSMul.hSMul (α := M × N) (1, n) (HSMul.hSMul (α := M × N) (m, 1) a)
have simp_rw₁ : (m * 1, 1 * n) • a = (1 * m, n * 1) • a
Tactic: simp_rw [smul_smul, Prod.mk_mul_mk, mul_one, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Prod (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : Monoid N
x : MulAction (M × N) α
instM : MulAction M α := compHom (M := M × N) α (MonoidHom.inl M N)
instN : MulAction N α := compHom (M := M × N) α (MonoidHom.inr M N)
m : M
n : N
a : α
simp_rw : ((m, 1) * (1, n)) • a = ((1, n) * (m, 1)) • a
simp_rw₁ : (m * 1, 1 * n) • a = (1 * m, n * 1) • a
⊢ HSMul.hSMul (α := M × N) (m, 1) (HSMul.hSMul (α := M × N) (1, n) a) =
    HSMul.hSMul (α := M × N) (1, n) (HSMul.hSMul (α := M × N) (m, 1) a)
have simp_rw₂ : (m, 1 * n) • a = (1 * m, n) • a
Tactic: simp_rw [smul_smul, Prod.mk_mul_mk, mul_one, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Prod (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : Monoid N
toSemigroupAction : SemigroupAction (M × N) α
one_smul : ∀ (b : α), HSMul.hSMul (α := M × N) 1 b = b
⊢ prodOfSMulCommClass M N α = { toSemigroupAction := toSemigroupAction, one_smul := one_smul : MulAction (M × N) α }
have smul : ∀ (m : M) (n : N) (a : α), SMul.smul (m, n) a = SMul.smul (m, n) a
Tactic: ext ⟨m, n⟩ a
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Prod (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : Monoid N
toSemigroupAction : SemigroupAction (M × N) α
one_smul : ∀ (b : α), HSMul.hSMul (α := M × N) 1 b = b
m : M
n : N
a : α
⊢ SMul.smul (m, n) a = SMul.smul (m, n) a
have smul : HSMul.hSMul (α := M × N) (m, 1) (HSMul.hSMul (α := M × N) (1, n) a) = SMul.smul (m, n) a
Tactic: change (m, (1 : N)) • ((1 : M), n) • a = _
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Prod (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : Monoid N
toSemigroupAction : SemigroupAction (M × N) α
one_smul : ∀ (b : α), HSMul.hSMul (α := M × N) 1 b = b
m : M
n : N
a : α
⊢ HSMul.hSMul (α := M × N) (m, 1) (HSMul.hSMul (α := M × N) (1, n) a) = SMul.smul (m, n) a
have smul : (m, n) • a = SMul.smul (m, n) a
Tactic: rw [← mul_smul, Prod.mk_mul_mk, mul_one, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Prod (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : Monoid N
hM : MulAction M α
hN : MulAction N α
snd : SMulCommClass M N α
⊢ Eq (α := (x : MulAction M α) ×' (x_1 : MulAction N α) ×' SMulCommClass M N α)
    (PSigma.mk (β := fun (x : MulAction M α) ↦ (x_1 : MulAction N α) ×' SMulCommClass M N α)
      (compHom (M := M × N) α (MonoidHom.inl M N))
      (PSigma.mk (β := fun (x : MulAction N α) ↦ SMulCommClass M N α) (compHom (M := M × N) α (MonoidHom.inr M N)) ⋯))
    (PSigma.mk (β := fun (x : MulAction M α) ↦ (x_1 : MulAction N α) ×' SMulCommClass M N α) hM
      (PSigma.mk (β := fun (x : MulAction N α) ↦ SMulCommClass M N α) hN snd))
have h : compHom (M := M × N) α (MonoidHom.inl M N) = hM
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Prod (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : Monoid N
hM : MulAction M α
hN : MulAction N α
snd : SMulCommClass M N α
h : compHom (M := M × N) α (MonoidHom.inl M N) = hM
⊢ Eq (α := (x : MulAction M α) ×' (x_1 : MulAction N α) ×' SMulCommClass M N α)
    (PSigma.mk (β := fun (x : MulAction M α) ↦ (x_1 : MulAction N α) ×' SMulCommClass M N α)
      (compHom (M := M × N) α (MonoidHom.inl M N))
      (PSigma.mk (β := fun (x : MulAction N α) ↦ SMulCommClass M N α) (compHom (M := M × N) α (MonoidHom.inr M N)) ⋯))
    (PSigma.mk (β := fun (x : MulAction M α) ↦ (x_1 : MulAction N α) ×' SMulCommClass M N α) hM
      (PSigma.mk (β := fun (x : MulAction N α) ↦ SMulCommClass M N α) hN snd))
have h₁ : HEq (α := (x : MulAction N α) ×' SMulCommClass M N α)
  (PSigma.mk (β := fun (x : MulAction N α) ↦ SMulCommClass M N α) (compHom (M := M × N) α (MonoidHom.inr M N)) sorry) (β :=
  (x : MulAction N α) ×' SMulCommClass M N α) (PSigma.mk (β := fun (x : MulAction N α) ↦ SMulCommClass M N α) hN snd)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Prod (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : Monoid N
hM : MulAction M α
hN : MulAction N α
snd : SMulCommClass M N α
⊢ compHom (M := M × N) α (MonoidHom.inl M N) = hM
have h : ∀ (m : M) (a : α), SMul.smul m a = SMul.smul m a
Tactic: ext m a
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Prod (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : Monoid N
hM : MulAction M α
hN : MulAction N α
snd : SMulCommClass M N α
m : M
a : α
| SMul.smul m a
have rw : SMul.smul m (HSMul.hSMul.{u_2, u_5, u_5} (α := N) 1 a)
Tactic: rw [← hN.one_smul a]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Prod (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : Monoid N
hM : MulAction M α
hN : MulAction N α
snd : SMulCommClass M N α
m : M
a : α
⊢ SMul.smul m a = SMul.smul m a
have h : SMul.smul m a = SMul.smul m (HSMul.hSMul.{u_2, u_5, u_5} (α := N) 1 a)
Tactic: conv_rhs => rw [← hN.one_smul a]