awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommCoprod (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : Monoid P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute.{u_3} (S := P) ((f : (a : M) → P) m : P) ((g : (a : N) → P) n : P)
mn : M × N
⊢ (f.noncommCoprod g comm : (a : M × N) → P) mn =
    HMul.hMul (α := P) (β := P) ((g : (a : N) → P) mn.2 : P) ((f : (a : M) → P) mn.1 : P)
have rw : (f.noncommCoprod g comm : (a : M × N) → P) mn =
  HMul.hMul (α := P) (β := P) ((f : (a : M) → P) mn.1 : P) ((g : (a : N) → P) mn.2 : P)
Tactic: rw [← comm, MonoidHom.noncommCoprod_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommCoprod (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : Monoid P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute.{u_3} (S := P) ((f : (a : M) → P) m : P) ((g : (a : N) → P) n : P)
mn : M × N
rw :
  (f.noncommCoprod g comm : (a : M × N) → P) mn =
    HMul.hMul (α := P) (β := P) ((f : (a : M) → P) mn.1 : P) ((g : (a : N) → P) mn.2 : P)
⊢ (f.noncommCoprod g comm : (a : M × N) → P) mn =
    HMul.hMul (α := P) (β := P) ((g : (a : N) → P) mn.2 : P) ((f : (a : M) → P) mn.1 : P)
have rw₁ : HMul.hMul (α := P) (β := P) ((f : (a : M) → P) mn.1 : P) ((g : (a : N) → P) mn.2 : P) =
  HMul.hMul (α := P) (β := P) ((f : (a : M) → P) mn.1 : P) ((g : (a : N) → P) mn.2 : P)
Tactic: rw [← comm, MonoidHom.noncommCoprod_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommCoprod (goal)
Goal:
M : Type u_4
N : Type u_5
P : Type u_6
inst : Group M
inst_1 : Group N
inst_2 : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute.{u_6} (S := P) ((f : (a : M) → P) m : P) ((g : (a : N) → P) n : P)
⊢ Function.Injective (α := M × N) (β := P) (⇑(f.noncommCoprod g comm) : (a : M × N) → P) ↔
    Function.Injective.{u_4 + 1, u_6 + 1} (α := M) (β := P) (⇑f : (a : M) → P) ∧
      Function.Injective.{u_5 + 1, u_6 + 1} (α := N) (β := P) (⇑g : (a : N) → P) ∧ Disjoint f.range g.range
have simp : (∀ (a : M) (b : N),
    HMul.hMul (α := P) (β := P) ((f : (a : M) → P) a : P) ((g : (a : N) → P) b : P) = 1 → a = 1 ∧ b = 1) ↔
  (∀ (a : M), Eq.{u_6 + 1} (α := P) ((f : (a : M) → P) a : P) (1 : P) → a = 1) ∧
    (∀ (a : N), Eq.{u_6 + 1} (α := P) ((g : (a : N) → P) a : P) (1 : P) → a = 1) ∧ f.range ⊓ g.range ≤ ⊥
Tactic: simp only [injective_iff_map_eq_one, disjoint_iff_inf_le,
    noncommCoprod_apply, Prod.forall, Prod.mk_eq_one]
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommCoprod (goal)
Goal:
M : Type u_4
N : Type u_5
P : Type u_6
inst : Group M
inst_1 : Group N
inst_2 : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute.{u_6} (S := P) ((f : (a : M) → P) m : P) ((g : (a : N) → P) n : P)
⊢ (∀ (a : M) (b : N),
      HMul.hMul (α := P) (β := P) ((f : (a : M) → P) a : P) ((g : (a : N) → P) b : P) = 1 → a = 1 ∧ b = 1) ↔
    (∀ (a : M), Eq.{u_6 + 1} (α := P) ((f : (a : M) → P) a : P) (1 : P) → a = 1) ∧
      (∀ (a : N), Eq.{u_6 + 1} (α := P) ((g : (a : N) → P) a : P) (1 : P) → a = 1) ∧ f.range ⊓ g.range ≤ ⊥
have refine_1 : ∀
  (h :
    ∀ (a : M) (b : N),
      HMul.hMul (α := P) (β := P) ((f : (a : M) → P) a : P) ((g : (a : N) → P) b : P) = 1 → a = 1 ∧ b = 1)
  (x : M), Eq.{u_6 + 1} (α := P) ((f : (a : M) → P) x : P) (1 : P) → x = 1
Tactic: refine ⟨fun h ↦ ⟨fun x ↦ ?_, fun x ↦ ?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommCoprod (goal)
Goal:
M : Type u_4
N : Type u_5
P : Type u_6
inst : Group M
inst_1 : Group N
inst_2 : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute.{u_6} (S := P) ((f : (a : M) → P) m : P) ((g : (a : N) → P) n : P)
refine_1 :
  ∀
    (h :
      ∀ (a : M) (b : N),
        HMul.hMul (α := P) (β := P) ((f : (a : M) → P) a : P) ((g : (a : N) → P) b : P) = 1 → a = 1 ∧ b = 1)
    (x : M), Eq.{u_6 + 1} (α := P) ((f : (a : M) → P) x : P) (1 : P) → x = 1
⊢ (∀ (a : M) (b : N),
      HMul.hMul (α := P) (β := P) ((f : (a : M) → P) a : P) ((g : (a : N) → P) b : P) = 1 → a = 1 ∧ b = 1) ↔
    (∀ (a : M), Eq.{u_6 + 1} (α := P) ((f : (a : M) → P) a : P) (1 : P) → a = 1) ∧
      (∀ (a : N), Eq.{u_6 + 1} (α := P) ((g : (a : N) → P) a : P) (1 : P) → a = 1) ∧ f.range ⊓ g.range ≤ ⊥
have refine_2 : ∀
  (h :
    ∀ (a : M) (b : N),
      HMul.hMul (α := P) (β := P) ((f : (a : M) → P) a : P) ((g : (a : N) → P) b : P) = 1 → a = 1 ∧ b = 1)
  (x : N), Eq.{u_6 + 1} (α := P) ((g : (a : N) → P) x : P) (1 : P) → x = 1
Tactic: refine ⟨fun h ↦ ⟨fun x ↦ ?_, fun x ↦ ?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommCoprod (goal)
Goal:
M : Type u_4
N : Type u_5
P : Type u_6
inst : Group M
inst_1 : Group N
inst_2 : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute.{u_6} (S := P) ((f : (a : M) → P) m : P) ((g : (a : N) → P) n : P)
refine_1 :
  ∀
    (h :
      ∀ (a : M) (b : N),
        HMul.hMul (α := P) (β := P) ((f : (a : M) → P) a : P) ((g : (a : N) → P) b : P) = 1 → a = 1 ∧ b = 1)
    (x : M), Eq.{u_6 + 1} (α := P) ((f : (a : M) → P) x : P) (1 : P) → x = 1
refine_2 :
  ∀
    (h :
      ∀ (a : M) (b : N),
        HMul.hMul (α := P) (β := P) ((f : (a : M) → P) a : P) ((g : (a : N) → P) b : P) = 1 → a = 1 ∧ b = 1)
    (x : N), Eq.{u_6 + 1} (α := P) ((g : (a : N) → P) x : P) (1 : P) → x = 1
⊢ (∀ (a : M) (b : N),
      HMul.hMul (α := P) (β := P) ((f : (a : M) → P) a : P) ((g : (a : N) → P) b : P) = 1 → a = 1 ∧ b = 1) ↔
    (∀ (a : M), Eq.{u_6 + 1} (α := P) ((f : (a : M) → P) a : P) (1 : P) → a = 1) ∧
      (∀ (a : N), Eq.{u_6 + 1} (α := P) ((g : (a : N) → P) a : P) (1 : P) → a = 1) ∧ f.range ⊓ g.range ≤ ⊥
have refine_3 : ∀
  (h :
    ∀ (a : M) (b : N),
      HMul.hMul (α := P) (β := P) ((f : (a : M) → P) a : P) ((g : (a : N) → P) b : P) = 1 → a = 1 ∧ b = 1),
  f.range ⊓ g.range ≤ ⊥
Tactic: refine ⟨fun h ↦ ⟨fun x ↦ ?_, fun x ↦ ?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommCoprod (goal)
Goal:
M : Type u_4
N : Type u_5
P : Type u_6
inst : Group M
inst_1 : Group N
inst_2 : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute.{u_6} (S := P) ((f : (a : M) → P) m : P) ((g : (a : N) → P) n : P)
refine_1 :
  ∀
    (h :
      ∀ (a : M) (b : N),
        HMul.hMul (α := P) (β := P) ((f : (a : M) → P) a : P) ((g : (a : N) → P) b : P) = 1 → a = 1 ∧ b = 1)
    (x : M), Eq.{u_6 + 1} (α := P) ((f : (a : M) → P) x : P) (1 : P) → x = 1
refine_2 :
  ∀
    (h :
      ∀ (a : M) (b : N),
        HMul.hMul (α := P) (β := P) ((f : (a : M) → P) a : P) ((g : (a : N) → P) b : P) = 1 → a = 1 ∧ b = 1)
    (x : N), Eq.{u_6 + 1} (α := P) ((g : (a : N) → P) x : P) (1 : P) → x = 1
refine_3 :
  ∀
    (h :
      ∀ (a : M) (b : N),
        HMul.hMul (α := P) (β := P) ((f : (a : M) → P) a : P) ((g : (a : N) → P) b : P) = 1 → a = 1 ∧ b = 1),
    f.range ⊓ g.range ≤ ⊥
⊢ (∀ (a : M) (b : N),
      HMul.hMul (α := P) (β := P) ((f : (a : M) → P) a : P) ((g : (a : N) → P) b : P) = 1 → a = 1 ∧ b = 1) ↔
    (∀ (a : M), Eq.{u_6 + 1} (α := P) ((f : (a : M) → P) a : P) (1 : P) → a = 1) ∧
      (∀ (a : N), Eq.{u_6 + 1} (α := P) ((g : (a : N) → P) a : P) (1 : P) → a = 1) ∧ f.range ⊓ g.range ≤ ⊥
have refine_4 : (∀ (a : M), Eq.{u_6 + 1} (α := P) ((f : (a : M) → P) a : P) (1 : P) → a = 1) ∧
    (∀ (a : N), Eq.{u_6 + 1} (α := P) ((g : (a : N) → P) a : P) (1 : P) → a = 1) ∧ f.range ⊓ g.range ≤ ⊥ →
  ∀ (a : M) (b : N), HMul.hMul (α := P) (β := P) ((f : (a : M) → P) a : P) ((g : (a : N) → P) b : P) = 1 → a = 1 ∧ b = 1
Tactic: refine ⟨fun h ↦ ⟨fun x ↦ ?_, fun x ↦ ?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommCoprod (goal)
Goal:
M : Type u_4
N : Type u_5
P : Type u_6
inst : Group M
inst_1 : Group N
inst_2 : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute.{u_6} (S := P) ((f : (a : M) → P) m : P) ((g : (a : N) → P) n : P)
h :
  ∀ (a : M) (b : N), HMul.hMul (α := P) (β := P) ((f : (a : M) → P) a : P) ((g : (a : N) → P) b : P) = 1 → a = 1 ∧ b = 1
x : P
⊢ x ∈ f.range ⊓ g.range → Membership.mem (γ := Subgroup P) ⊥ x
have refine_3 : ∀ (y : M) (hy : (f : (a : M) → P) y = x) (z : N) (hz : (g : (a : N) → P) z = x), Membership.mem (γ := Subgroup P) ⊥ x
Tactic: ⟨⟨y, hy⟩, z, hz⟩
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommCoprod (goal)
Goal:
M : Type u_4
N : Type u_5
P : Type u_6
inst : Group M
inst_1 : Group N
inst_2 : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute.{u_6} (S := P) ((f : (a : M) → P) m : P) ((g : (a : N) → P) n : P)
h :
  ∀ (a : M) (b : N), HMul.hMul (α := P) (β := P) ((f : (a : M) → P) a : P) ((g : (a : N) → P) b : P) = 1 → a = 1 ∧ b = 1
x : P
y : M
hy : (f : (a : M) → P) y = x
z : N
hz : (g : (a : N) → P) z = x
⊢ HMul.hMul (α := P) (β := P) ((f : (a : M) → P) y : P) ((g : (a : N) → P) z⁻¹ : P) = 1
have rw : HMul.hMul (α := P) (β := P) ((f : (a : M) → P) y : P) (((g : (a : N) → P) z)⁻¹ : P) = 1
Tactic: rw [map_inv, hy, hz, mul_inv_cancel]
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommCoprod (goal)
Goal:
M : Type u_4
N : Type u_5
P : Type u_6
inst : Group M
inst_1 : Group N
inst_2 : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute.{u_6} (S := P) ((f : (a : M) → P) m : P) ((g : (a : N) → P) n : P)
h :
  ∀ (a : M) (b : N), HMul.hMul (α := P) (β := P) ((f : (a : M) → P) a : P) ((g : (a : N) → P) b : P) = 1 → a = 1 ∧ b = 1
x : P
y : M
hy : (f : (a : M) → P) y = x
z : N
hz : (g : (a : N) → P) z = x
rw : HMul.hMul (α := P) (β := P) ((f : (a : M) → P) y : P) (((g : (a : N) → P) z)⁻¹ : P) = 1
⊢ HMul.hMul (α := P) (β := P) ((f : (a : M) → P) y : P) ((g : (a : N) → P) z⁻¹ : P) = 1
have rw₁ : HMul.hMul (β := P) x (((g : (a : N) → P) z)⁻¹ : P) = 1
Tactic: rw [map_inv, hy, hz, mul_inv_cancel]
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommCoprod (goal)
Goal:
M : Type u_4
N : Type u_5
P : Type u_6
inst : Group M
inst_1 : Group N
inst_2 : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute.{u_6} (S := P) ((f : (a : M) → P) m : P) ((g : (a : N) → P) n : P)
h :
  ∀ (a : M) (b : N), HMul.hMul (α := P) (β := P) ((f : (a : M) → P) a : P) ((g : (a : N) → P) b : P) = 1 → a = 1 ∧ b = 1
x : P
y : M
hy : (f : (a : M) → P) y = x
z : N
hz : (g : (a : N) → P) z = x
rw : HMul.hMul (α := P) (β := P) ((f : (a : M) → P) y : P) (((g : (a : N) → P) z)⁻¹ : P) = 1
rw₁ : HMul.hMul (β := P) x (((g : (a : N) → P) z)⁻¹ : P) = 1
⊢ HMul.hMul (α := P) (β := P) ((f : (a : M) → P) y : P) ((g : (a : N) → P) z⁻¹ : P) = 1
have rw₂ : x * x⁻¹ = 1
Tactic: rw [map_inv, hy, hz, mul_inv_cancel]
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommCoprod (goal)
Goal:
M : Type u_4
N : Type u_5
P : Type u_6
inst : Group M
inst_1 : Group N
inst_2 : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute.{u_6} (S := P) ((f : (a : M) → P) m : P) ((g : (a : N) → P) n : P)
h :
  ∀ (a : M) (b : N), HMul.hMul (α := P) (β := P) ((f : (a : M) → P) a : P) ((g : (a : N) → P) b : P) = 1 → a = 1 ∧ b = 1
x : P
y : M
hy : (f : (a : M) → P) y = x
z : N
hz : (g : (a : N) → P) z = x
rw : HMul.hMul (α := P) (β := P) ((f : (a : M) → P) y : P) (((g : (a : N) → P) z)⁻¹ : P) = 1
rw₁ : HMul.hMul (β := P) x (((g : (a : N) → P) z)⁻¹ : P) = 1
rw₂ : x * x⁻¹ = 1
⊢ HMul.hMul (α := P) (β := P) ((f : (a : M) → P) y : P) ((g : (a : N) → P) z⁻¹ : P) = 1
have rw₃ : Eq.{u_6 + 1} (α := P) 1 1
Tactic: rw [map_inv, hy, hz, mul_inv_cancel]
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommCoprod (goal)
Goal:
M : Type u_4
N : Type u_5
P : Type u_6
inst : Group M
inst_1 : Group N
inst_2 : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute.{u_6} (S := P) ((f : (a : M) → P) m : P) ((g : (a : N) → P) n : P)
h :
  ∀ (a : M) (b : N), HMul.hMul (α := P) (β := P) ((f : (a : M) → P) a : P) ((g : (a : N) → P) b : P) = 1 → a = 1 ∧ b = 1
x : P
y : M
hy : (f : (a : M) → P) y = x
z : N
hz : (g : (a : N) → P) z = x
⊢ Membership.mem (γ := Subgroup P) ⊥ x
have refine_3 : ∀ (hy : (f : (a : M) → P) 1 = x) (z : N) (hz : (g : (a : N) → P) z = x), Membership.mem (γ := Subgroup P) ⊥ x
Tactic: rwa [(h y z⁻¹ (by rw [map_inv, hy, hz, mul_inv_cancel])).1, map_one, eq_comm] at hy
Cleared hypotheses: hy, z, hz
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommCoprod (goal)
Goal:
M : Type u_4
N : Type u_5
P : Type u_6
inst : Group M
inst_1 : Group N
inst_2 : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute.{u_6} (S := P) ((f : (a : M) → P) m : P) ((g : (a : N) → P) n : P)
h :
  ∀ (a : M) (b : N), HMul.hMul (α := P) (β := P) ((f : (a : M) → P) a : P) ((g : (a : N) → P) b : P) = 1 → a = 1 ∧ b = 1
x : P
y : M
hy : (f : (a : M) → P) y = x
z : N
hz : (g : (a : N) → P) z = x
refine_3 : ∀ (hy : (f : (a : M) → P) 1 = x) (z : N) (hz : (g : (a : N) → P) z = x), Membership.mem (γ := Subgroup P) ⊥ x
⊢ Membership.mem (γ := Subgroup P) ⊥ x
have refine_3₁ : ∀ (hy : 1 = x) (z : N) (hz : (g : (a : N) → P) z = x), Membership.mem (γ := Subgroup P) ⊥ x
Tactic: rwa [(h y z⁻¹ (by rw [map_inv, hy, hz, mul_inv_cancel])).1, map_one, eq_comm] at hy
Cleared hypotheses: hy, z, hz
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommCoprod (goal)
Goal:
M : Type u_4
N : Type u_5
P : Type u_6
inst : Group M
inst_1 : Group N
inst_2 : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute.{u_6} (S := P) ((f : (a : M) → P) m : P) ((g : (a : N) → P) n : P)
h :
  ∀ (a : M) (b : N), HMul.hMul (α := P) (β := P) ((f : (a : M) → P) a : P) ((g : (a : N) → P) b : P) = 1 → a = 1 ∧ b = 1
x : P
y : M
hy : (f : (a : M) → P) y = x
z : N
hz : (g : (a : N) → P) z = x
refine_3 : ∀ (hy : (f : (a : M) → P) 1 = x) (z : N) (hz : (g : (a : N) → P) z = x), Membership.mem (γ := Subgroup P) ⊥ x
refine_3₁ : ∀ (hy : 1 = x) (z : N) (hz : (g : (a : N) → P) z = x), Membership.mem (γ := Subgroup P) ⊥ x
⊢ Membership.mem (γ := Subgroup P) ⊥ x
have refine_3₂ : ∀ (hy : x = 1) (z : N) (hz : (g : (a : N) → P) z = x), Membership.mem (γ := Subgroup P) ⊥ x
Tactic: rwa [(h y z⁻¹ (by rw [map_inv, hy, hz, mul_inv_cancel])).1, map_one, eq_comm] at hy
Cleared hypotheses: hy, z, hz
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommCoprod (goal)
Goal:
M : Type u_4
N : Type u_5
P : Type u_6
inst : Group M
inst_1 : Group N
inst_2 : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute.{u_6} (S := P) ((f : (a : M) → P) m : P) ((g : (a : N) → P) n : P)
hf : ∀ (a : M), Eq.{u_6 + 1} (α := P) ((f : (a : M) → P) a : P) (1 : P) → a = 1
hg : ∀ (a : N), Eq.{u_6 + 1} (α := P) ((g : (a : N) → P) a : P) (1 : P) → a = 1
hp : f.range ⊓ g.range ≤ ⊥
a : M
b : N
h : HMul.hMul (α := P) (β := P) ((f : (a : M) → P) a : P) ((g : (a : N) → P) b : P) = 1
⊢ Eq.{u_6 + 1} (α := P) ((f : (a : M) → P) a⁻¹ : P) ((g : (a : N) → P) b : P)
have rwa : Eq.{u_6 + 1} (α := P) (((f : (a : M) → P) a)⁻¹ : P) ((g : (a : N) → P) b : P)
Tactic: rwa [map_inv, inv_eq_iff_mul_eq_one]
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommCoprod (hypothesis)
Goal:
M : Type u_4
N : Type u_5
P : Type u_6
inst : Group M
inst_1 : Group N
inst_2 : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute.{u_6} (S := P) ((f : (a : M) → P) m : P) ((g : (a : N) → P) n : P)
hf : ∀ (a : M), Eq.{u_6 + 1} (α := P) ((f : (a : M) → P) a : P) (1 : P) → a = 1
hg : ∀ (a : N), Eq.{u_6 + 1} (α := P) ((g : (a : N) → P) a : P) (1 : P) → a = 1
hp : f.range ⊓ g.range ≤ ⊥
a : M
b : N
h : HMul.hMul (α := P) (β := P) ((f : (a : M) → P) a : P) ((g : (a : N) → P) b : P) = 1
⊢ a = 1 ∧ b = 1
have key : Membership.mem.{u_6, u_6} (α := P) (γ := Subgroup P) ⊥ ((g : (a : N) → P) b : P)
Tactic: have key := hp ⟨⟨a⁻¹, by rwa [map_inv, inv_eq_iff_mul_eq_one]⟩, b, rfl⟩
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommCoprod (goal)
Goal:
M : Type u_4
N : Type u_5
P : Type u_6
inst : Group M
inst_1 : Group N
inst_2 : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute.{u_6} (S := P) ((f : (a : M) → P) m : P) ((g : (a : N) → P) n : P)
hf : ∀ (a : M), Eq.{u_6 + 1} (α := P) ((f : (a : M) → P) a : P) (1 : P) → a = 1
hg : ∀ (a : N), Eq.{u_6 + 1} (α := P) ((g : (a : N) → P) a : P) (1 : P) → a = 1
hp : f.range ⊓ g.range ≤ ⊥
a : M
b : N
h : HMul.hMul (α := P) (β := P) ((f : (a : M) → P) a : P) ((g : (a : N) → P) b : P) = 1
key : Membership.mem.{u_6, u_6} (α := P) (γ := Subgroup P) ⊥ ((g : (a : N) → P) b : P)
⊢ Eq.{u_6 + 1} (α := P) ((f : (a : M) → P) a : P) (1 : P)
have rwa : ∀ (h : HMul.hMul (α := P) (β := P) ((f : (a : M) → P) a : P) (1 : P) = 1)
  (key : Membership.mem.{u_6, u_6} (α := P) (γ := Subgroup P) ⊥ ((g : (a : N) → P) b : P)),
  Eq.{u_6 + 1} (α := P) ((f : (a : M) → P) a : P) (1 : P)
Tactic: rwa [key, mul_one] at h
Cleared hypotheses: h, key
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommCoprod (goal)
Goal:
M : Type u_4
N : Type u_5
P : Type u_6
inst : Group M
inst_1 : Group N
inst_2 : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute.{u_6} (S := P) ((f : (a : M) → P) m : P) ((g : (a : N) → P) n : P)
hf : ∀ (a : M), Eq.{u_6 + 1} (α := P) ((f : (a : M) → P) a : P) (1 : P) → a = 1
hg : ∀ (a : N), Eq.{u_6 + 1} (α := P) ((g : (a : N) → P) a : P) (1 : P) → a = 1
hp : f.range ⊓ g.range ≤ ⊥
a : M
b : N
h : HMul.hMul (α := P) (β := P) ((f : (a : M) → P) a : P) ((g : (a : N) → P) b : P) = 1
key : Membership.mem.{u_6, u_6} (α := P) (γ := Subgroup P) ⊥ ((g : (a : N) → P) b : P)
rwa :
  ∀ (h : HMul.hMul (α := P) (β := P) ((f : (a : M) → P) a : P) (1 : P) = 1)
    (key : Membership.mem.{u_6, u_6} (α := P) (γ := Subgroup P) ⊥ ((g : (a : N) → P) b : P)),
    Eq.{u_6 + 1} (α := P) ((f : (a : M) → P) a : P) (1 : P)
⊢ Eq.{u_6 + 1} (α := P) ((f : (a : M) → P) a : P) (1 : P)
have rwa₁ : ∀ (h : Eq.{u_6 + 1} (α := P) ((f : (a : M) → P) a : P) (1 : P))
  (key : Membership.mem.{u_6, u_6} (α := P) (γ := Subgroup P) ⊥ ((g : (a : N) → P) b : P)),
  Eq.{u_6 + 1} (α := P) ((f : (a : M) → P) a : P) (1 : P)
Tactic: rwa [key, mul_one] at h
Cleared hypotheses: h, key
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommCoprod (goal)
Goal:
M : Type u_4
N : Type u_5
P : Type u_6
inst : Group M
inst_1 : Group N
inst_2 : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute.{u_6} (S := P) ((f : (a : M) → P) m : P) ((g : (a : N) → P) n : P)
⊢ (f.noncommCoprod g comm).range (G := M × N) = f.range ⊔ g.range
have a : (f.noncommCoprod g comm).range (G := M × N) ≤ f.range ⊔ g.range
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommCoprod (goal)
Goal:
M : Type u_4
N : Type u_5
P : Type u_6
inst : Group M
inst_1 : Group N
inst_2 : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute.{u_6} (S := P) ((f : (a : M) → P) m : P) ((g : (a : N) → P) n : P)
a : (f.noncommCoprod g comm).range (G := M × N) ≤ f.range ⊔ g.range
⊢ (f.noncommCoprod g comm).range (G := M × N) = f.range ⊔ g.range
have a₁ : f.range ⊔ g.range ≤ (f.noncommCoprod g comm).range (G := M × N)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommCoprod (goal)
Goal:
M : Type u_4
N : Type u_5
P : Type u_6
inst : Group M
inst_1 : Group N
inst_2 : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute.{u_6} (S := P) ((f : (a : M) → P) m : P) ((g : (a : N) → P) n : P)
⊢ f.range ⊔ g.range ≤ (f.noncommCoprod g comm).range (G := M × N)
have a : f.range ≤ (f.noncommCoprod g comm).range (G := M × N) ∧ g.range ≤ (f.noncommCoprod g comm).range (G := M × N)
Tactic: rw [sup_le_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommCoprod (goal)
Goal:
M : Type u_4
N : Type u_5
P : Type u_6
inst : Group M
inst_1 : Group N
inst_2 : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute.{u_6} (S := P) ((f : (a : M) → P) m : P) ((g : (a : N) → P) n : P)
⊢ f.range ≤ (f.noncommCoprod g comm).range (G := M × N) ∧ g.range ≤ (f.noncommCoprod g comm).range (G := M × N)
have a : f.range ≤ (f.noncommCoprod g comm).range (G := M × N)
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommCoprod (goal)
Goal:
M : Type u_4
N : Type u_5
P : Type u_6
inst : Group M
inst_1 : Group N
inst_2 : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute.{u_6} (S := P) ((f : (a : M) → P) m : P) ((g : (a : N) → P) n : P)
a : f.range ≤ (f.noncommCoprod g comm).range (G := M × N)
⊢ f.range ≤ (f.noncommCoprod g comm).range (G := M × N) ∧ g.range ≤ (f.noncommCoprod g comm).range (G := M × N)
have a₁ : g.range ≤ (f.noncommCoprod g comm).range (G := M × N)
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommCoprod (goal)
Goal:
M : Type u_4
N : Type u_5
P : Type u_6
inst : Group M
inst_1 : Group N
inst_2 : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute.{u_6} (S := P) ((f : (a : M) → P) m : P) ((g : (a : N) → P) n : P)
a : M
⊢ Eq.{u_6 + 1} (α := P) ((f.noncommCoprod g comm : (a : M × N) → P) (a, 1) : P) ((f : (a : M) → P) a : P)
have rw : HMul.hMul (α := P) (β := P) ((f : (a : M) → P) (a, 1).1 : P) ((g : (a : N) → P) (a, 1).2 : P) = (f : (a : M) → P) a
Tactic: rw [noncommCoprod_apply, map_one, mul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommCoprod (goal)
Goal:
M : Type u_4
N : Type u_5
P : Type u_6
inst : Group M
inst_1 : Group N
inst_2 : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute.{u_6} (S := P) ((f : (a : M) → P) m : P) ((g : (a : N) → P) n : P)
a : M
rw : HMul.hMul (α := P) (β := P) ((f : (a : M) → P) (a, 1).1 : P) ((g : (a : N) → P) (a, 1).2 : P) = (f : (a : M) → P) a
⊢ Eq.{u_6 + 1} (α := P) ((f.noncommCoprod g comm : (a : M × N) → P) (a, 1) : P) ((f : (a : M) → P) a : P)
have rw₁ : HMul.hMul (α := P) (β := P) ((f : (a : M) → P) (a, 1).1 : P) (1 : P) = (f : (a : M) → P) a
Tactic: rw [noncommCoprod_apply, map_one, mul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommCoprod (goal)
Goal:
M : Type u_4
N : Type u_5
P : Type u_6
inst : Group M
inst_1 : Group N
inst_2 : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute.{u_6} (S := P) ((f : (a : M) → P) m : P) ((g : (a : N) → P) n : P)
a : M
rw : HMul.hMul (α := P) (β := P) ((f : (a : M) → P) (a, 1).1 : P) ((g : (a : N) → P) (a, 1).2 : P) = (f : (a : M) → P) a
rw₁ : HMul.hMul (α := P) (β := P) ((f : (a : M) → P) (a, 1).1 : P) (1 : P) = (f : (a : M) → P) a
⊢ Eq.{u_6 + 1} (α := P) ((f.noncommCoprod g comm : (a : M × N) → P) (a, 1) : P) ((f : (a : M) → P) a : P)
have rw₂ : Eq.{u_6 + 1} (α := P) ((f : (a : M) → P) (a, 1).1 : P) ((f : (a : M) → P) a : P)
Tactic: rw [noncommCoprod_apply, map_one, mul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommCoprod (goal)
Goal:
M : Type u_4
N : Type u_5
P : Type u_6
inst : Group M
inst_1 : Group N
inst_2 : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute.{u_6} (S := P) ((f : (a : M) → P) m : P) ((g : (a : N) → P) n : P)
a : N
⊢ Eq.{u_6 + 1} (α := P) ((f.noncommCoprod g comm : (a : M × N) → P) (1, a) : P) ((g : (a : N) → P) a : P)
have rw : HMul.hMul (α := P) (β := P) ((f : (a : M) → P) (1, a).1 : P) ((g : (a : N) → P) (1, a).2 : P) = (g : (a : N) → P) a
Tactic: rw [noncommCoprod_apply, map_one, one_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommCoprod (goal)
Goal:
M : Type u_4
N : Type u_5
P : Type u_6
inst : Group M
inst_1 : Group N
inst_2 : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute.{u_6} (S := P) ((f : (a : M) → P) m : P) ((g : (a : N) → P) n : P)
a : N
rw : HMul.hMul (α := P) (β := P) ((f : (a : M) → P) (1, a).1 : P) ((g : (a : N) → P) (1, a).2 : P) = (g : (a : N) → P) a
⊢ Eq.{u_6 + 1} (α := P) ((f.noncommCoprod g comm : (a : M × N) → P) (1, a) : P) ((g : (a : N) → P) a : P)
have rw₁ : HMul.hMul (α := P) (β := P) (1 : P) ((g : (a : N) → P) (1, a).2 : P) = (g : (a : N) → P) a
Tactic: rw [noncommCoprod_apply, map_one, one_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommCoprod (goal)
Goal:
M : Type u_4
N : Type u_5
P : Type u_6
inst : Group M
inst_1 : Group N
inst_2 : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute.{u_6} (S := P) ((f : (a : M) → P) m : P) ((g : (a : N) → P) n : P)
a : N
rw : HMul.hMul (α := P) (β := P) ((f : (a : M) → P) (1, a).1 : P) ((g : (a : N) → P) (1, a).2 : P) = (g : (a : N) → P) a
rw₁ : HMul.hMul (α := P) (β := P) (1 : P) ((g : (a : N) → P) (1, a).2 : P) = (g : (a : N) → P) a
⊢ Eq.{u_6 + 1} (α := P) ((f.noncommCoprod g comm : (a : M × N) → P) (1, a) : P) ((g : (a : N) → P) a : P)
have rw₂ : Eq.{u_6 + 1} (α := P) ((g : (a : N) → P) (1, a).2 : P) ((g : (a : N) → P) a : P)
Tactic: rw [noncommCoprod_apply, map_one, one_mul]