awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
hG : Group G
inst : Finite G
tfae_1_to_2 : ∀ (a : IsNilpotent G), NormalizerCondition G
tfae_2_to_3 : ∀ (a : NormalizerCondition G) (H : Subgroup G), IsCoatom H → H.Normal
tfae_3_to_4 :
  ∀ (a : ∀ (H : Subgroup G), IsCoatom H → H.Normal) (p : ℕ) (_hp : Fact (Nat.Prime p)) (P : Sylow p G),
    (↑P : Subgroup G).Normal
⊢ ∀ (a : ∀ (p : ℕ) (_hp : Fact (Nat.Prime p)) (P : Sylow p G), (↑P : Subgroup G).Normal),
    Nonempty.{u_1 + 1} (((p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) ≃* G)

Tactic:
tfae_have 4 → 5
  | h => Nonempty.intro (Sylow.directProductOfNormal fun {p hp hP} => h p hp hP)
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
hG : Group G
inst : Finite G
tfae_1_to_2 : ∀ (a : IsNilpotent G), NormalizerCondition G
tfae_2_to_3 : ∀ (a : NormalizerCondition G) (H : Subgroup G), IsCoatom H → H.Normal
tfae_3_to_4 :
  ∀ (a : ∀ (H : Subgroup G), IsCoatom H → H.Normal) (p : ℕ) (_hp : Fact (Nat.Prime p)) (P : Sylow p G),
    (↑P : Subgroup G).Normal
tfae_4_to_5 :
  ∀ (a : ∀ (p : ℕ) (_hp : Fact (Nat.Prime p)) (P : Sylow p G), (↑P : Subgroup G).Normal),
    Nonempty.{u_1 + 1} (((p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) ≃* G)
⊢ Nonempty.{u_1 + 1} (((p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) ≃* G)

Tactic:
5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
hG : Group G
inst : Finite G
tfae_1_to_2 : ∀ (a : IsNilpotent G), NormalizerCondition G
tfae_2_to_3 : ∀ (a : NormalizerCondition G) (H : Subgroup G), IsCoatom H → H.Normal
tfae_3_to_4 :
  ∀ (a : ∀ (H : Subgroup G), IsCoatom H → H.Normal) (p : ℕ) (_hp : Fact (Nat.Prime p)) (P : Sylow p G),
    (↑P : Subgroup G).Normal
tfae_4_to_5 :
  ∀ (a : ∀ (p : ℕ) (_hp : Fact (Nat.Prime p)) (P : Sylow p G), (↑P : Subgroup G).Normal),
    Nonempty.{u_1 + 1} (((p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) ≃* G)
⊢ IsNilpotent G

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
hG : Group G
inst : Finite G
tfae_1_to_2 : ∀ (a : IsNilpotent G), NormalizerCondition G
tfae_2_to_3 : ∀ (a : NormalizerCondition G) (H : Subgroup G), IsCoatom H → H.Normal
tfae_3_to_4 :
  ∀ (a : ∀ (H : Subgroup G), IsCoatom H → H.Normal) (p : ℕ) (_hp : Fact (Nat.Prime p)) (P : Sylow p G),
    (↑P : Subgroup G).Normal
tfae_4_to_5 :
  ∀ (a : ∀ (p : ℕ) (_hp : Fact (Nat.Prime p)) (P : Sylow p G), (↑P : Subgroup G).Normal),
    Nonempty.{u_1 + 1} (((p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) ≃* G)
⊢ ∀ (a : Nonempty.{u_1 + 1} (((p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) ≃* G)),
    IsNilpotent G

Tactic:
5 → 1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
hG : Group G
inst : Finite G
tfae_1_to_2 : ∀ (a : IsNilpotent G), NormalizerCondition G
tfae_2_to_3 : ∀ (a : NormalizerCondition G) (H : Subgroup G), IsCoatom H → H.Normal
tfae_3_to_4 :
  ∀ (a : ∀ (H : Subgroup G), IsCoatom H → H.Normal) (p : ℕ) (_hp : Fact (Nat.Prime p)) (P : Sylow p G),
    (↑P : Subgroup G).Normal
tfae_4_to_5 :
  ∀ (a : ∀ (p : ℕ) (_hp : Fact (Nat.Prime p)) (P : Sylow p G), (↑P : Subgroup G).Normal),
    Nonempty.{u_1 + 1} (((p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) ≃* G)
⊢ ∀ (a : Nonempty.{u_1 + 1} (((p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) ≃* G)),
    IsNilpotent G

Tactic:
tfae_have 5 → 1
  | ⟨e⟩ => isNilpotent_of_product_of_sylow_group e
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
hG : Group G
inst : Finite G
tfae_1_to_2 : ∀ (a : IsNilpotent G), NormalizerCondition G
tfae_2_to_3 : ∀ (a : NormalizerCondition G) (H : Subgroup G), IsCoatom H → H.Normal
tfae_3_to_4 :
  ∀ (a : ∀ (H : Subgroup G), IsCoatom H → H.Normal) (p : ℕ) (_hp : Fact (Nat.Prime p)) (P : Sylow p G),
    (↑P : Subgroup G).Normal
tfae_4_to_5 :
  ∀ (a : ∀ (p : ℕ) (_hp : Fact (Nat.Prime p)) (P : Sylow p G), (↑P : Subgroup G).Normal),
    Nonempty.{u_1 + 1} (((p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) ≃* G)
tfae_5_to_1 :
  ∀ (a : Nonempty.{u_1 + 1} (((p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) ≃* G)),
    IsNilpotent G
⊢ [IsNilpotent G, NormalizerCondition G, ∀ (H : Subgroup G), IsCoatom H → H.Normal,
      ∀ (p : ℕ) (_hp : Fact (Nat.Prime p)) (P : Sylow p G), (↑P : Subgroup G).Normal,
      Nonempty.{u_1 + 1} (((p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) ≃* G)].TFAE

Tactic:
tfae_finish
-- Module: Mathlib.GroupTheory.NoncommCoprod
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : Mul M
inst_1 : Mul N
inst_2 : Semigroup 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 mn' : M × N
⊢ HMul.hMul (α := P) (β := P) ((f : (a : M) → P) (mn * mn').1 : P) ((g : (a : N) → P) (mn * mn').2 : P) =
    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:
simpa using (comm _ _).mul_mul_mul_comm _ _

Premises used: Commute.mul_mul_mul_comm
-- Module: Mathlib.GroupTheory.NoncommCoprod
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : Mul M
inst_1 : Mul N
inst_2 : Semigroup 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)
rw₁ 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)
⊢ (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)

Tactic:
rw [← comm, noncommCoprod_apply]

Premises used: MulHom.noncommCoprod_apply
-- Module: Mathlib.GroupTheory.NoncommCoprod
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : Mul M
inst_1 : Mul N
inst_2 : Semigroup P
f : M →ₙ* P
g : N →ₙ* P
Q : Type u_4
inst_3 : Semigroup Q
h : P →ₙ* Q
comm : ∀ (m : M) (n : N), Commute.{u_3} (S := P) ((f : (a : M) → P) m : P) ((g : (a : N) → P) n : P)
⊢ h.comp (f.noncommCoprod g comm) = (h.comp f).noncommCoprod (h.comp g) ⋯

Tactic:
ext fun _ => map_mul h _ _

Premises used: Prod.fst, map_mul, MulHom.ext, Prod.snd, DFunLike.coe
-- Module: Mathlib.GroupTheory.NoncommCoprod
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)
⊢ HMul.hMul (α := P) (β := P) ((f : (a : M) → P) 1.1 : P) ((g : (a : N) → P) 1.2 : P) = 1

Tactic:
simp only [Prod.fst_one, Prod.snd_one, map_one, mul_one]

Premises used: map_one, mul_one, Prod.snd_one, Prod.fst_one
-- Module: Mathlib.GroupTheory.NoncommCoprod
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)
rw₁ 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)
⊢ (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)

Tactic:
rw [← comm, MonoidHom.noncommCoprod_apply]

Premises used: MonoidHom.noncommCoprod_apply
-- Module: Mathlib.GroupTheory.NoncommCoprod
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)
x : M
⊢ Eq.{u_3 + 1} (α := P) (((f.noncommCoprod g comm).comp (inl M N) : (a : M) → P) x : P) ((f : (a : M) → P) x : P)

Tactic:
simp
-- Module: Mathlib.GroupTheory.NoncommCoprod
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)
x : N
⊢ Eq.{u_3 + 1} (α := P) (((f.noncommCoprod g comm).comp (inr M N) : (a : N) → P) x : P) ((g : (a : N) → P) x : P)

Tactic:
simp
-- Module: Mathlib.GroupTheory.NoncommCoprod
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 × N →* P
x : M × N
⊢ Eq.{u_3 + 1} (α := P) (((f.comp (inl M N)).noncommCoprod (f.comp (inr M N)) ⋯ : (a : M × N) → P) x : P)
    ((f : (a : M × N) → P) x : P)

Tactic:
simp [inl_apply, inr_apply, ← map_mul]

Premises used: MonoidHom.inr_apply, MonoidHom.inl_apply, map_mul
-- Module: Mathlib.GroupTheory.NoncommCoprod
Goal:
M : Type u_4
N : Type u_5
inst : Monoid M
inst_1 : Monoid N
⊢ Eq (α := M × N →* M × N) (noncommCoprod (inl M N) (inr M N) ⋯) (id (M × N))

Tactic:
noncommCoprod_unique <| .id (M × N)

Premises used: MonoidHom.inr, MonoidHom.inl, MonoidHom.noncommCoprod_unique, MonoidHom.id, Prod
-- Module: Mathlib.GroupTheory.NoncommCoprod
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)
Q : Type u_4
inst_3 : Monoid Q
h : P →* Q
x : M × N
⊢ Eq.{u_4 + 1} (α := Q) ((h.comp (f.noncommCoprod g comm) : (a : M × N) → Q) x : Q)
    (((h.comp f).noncommCoprod (h.comp g) ⋯ : (a : M × N) → Q) x : Q)

Tactic:
simp
-- Module: Mathlib.GroupTheory.NoncommCoprod
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)
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 ≤ ⊥
⊢ 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

Tactic:
simp only [injective_iff_map_eq_one, disjoint_iff_inf_le,
    noncommCoprod_apply, Prod.forall, Prod.mk_eq_one]

Premises used: MonoidHom.noncommCoprod_apply, Prod.mk_eq_one, Prod.forall, disjoint_iff_inf_le, injective_iff_map_eq_one
-- Module: Mathlib.GroupTheory.NoncommCoprod
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 ≤ ⊥

Tactic:
⟨fun h ↦ ⟨fun x ↦ ?_, fun x ↦ ?_, ?_⟩, ?_⟩

Premises used: And.intro, Iff.intro
-- Module: Mathlib.GroupTheory.NoncommCoprod
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 ≤ ⊥
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
⊢ (∀ (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:
refine ⟨fun h ↦ ⟨fun x ↦ ?_, fun x ↦ ?_, ?_⟩, ?_⟩
-- Module: Mathlib.GroupTheory.NoncommCoprod
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 : M
⊢ Eq.{u_6 + 1} (α := P) ((f : (a : M) → P) x : P) (1 : P) → x = 1

Tactic:
simpa using h x 1

Premises used: OfNat.ofNat
-- Module: Mathlib.GroupTheory.NoncommCoprod
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 : N
⊢ Eq.{u_6 + 1} (α := P) ((g : (a : N) → P) x : P) (1 : P) → x = 1

Tactic:
simpa using h 1 x

Premises used: OfNat.ofNat
-- Module: Mathlib.GroupTheory.NoncommCoprod
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
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
⊢ x ∈ f.range ⊓ g.range → Membership.mem (γ := Subgroup P) ⊥ x

Tactic:
⟨⟨y, hy⟩, z, hz⟩
-- Module: Mathlib.GroupTheory.NoncommCoprod
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
rw₃ rw₄ : Eq.{u_6 + 1} (α := P) 1 1
⊢ 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]

Premises used: map_inv, mul_inv_cancel
-- Module: Mathlib.GroupTheory.NoncommCoprod
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
refine_3₂ refine_3₃ refine_3₄ refine_3₅ :
  ∀ (hy : x = 1) (z : N) (hz : (g : (a : N) → P) z = x), Membership.mem (γ := Subgroup P) ⊥ 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

Premises used: eq_comm, Inv.inv, And.left, map_one
-- Module: Mathlib.GroupTheory.NoncommCoprod
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
rwa : Eq.{u_6 + 1} (α := P) (((f : (a : M) → P) a)⁻¹ : P) ((g : (a : N) → P) b : P)
rwa₁ rwa₂ rwa₃ rwa₄ : 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)

Tactic:
rwa [map_inv, inv_eq_iff_mul_eq_one]

Premises used: map_inv, inv_eq_iff_mul_eq_one
-- Module: Mathlib.GroupTheory.NoncommCoprod
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
⊢ 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⟩
-- Module: Mathlib.GroupTheory.NoncommCoprod
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)
rwa₁ rwa₂ rwa₃ 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)
⊢ Eq.{u_6 + 1} (α := P) ((f : (a : M) → P) a : P) (1 : P)

Tactic:
rwa [key, mul_one] at h

Premises used: mul_one
-- Module: Mathlib.GroupTheory.NoncommCoprod
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)
⊢ a = 1 ∧ b = 1

Tactic:
exact ⟨hf a (by rwa [key, mul_one] at h), hg b key⟩
-- Module: Mathlib.GroupTheory.NoncommCoprod
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
a₁ : f.range ⊔ g.range ≤ (f.noncommCoprod g comm).range (G := M × N)
⊢ (f.noncommCoprod g comm).range (G := M × N) = f.range ⊔ g.range

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.GroupTheory.NoncommCoprod
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 × N
⊢ Membership.mem (α := P) (f.range ⊔ g.range) ((f.noncommCoprod g comm : (a : M × N) → P) a : P)

Tactic:
mul_mem (mem_sup_left ⟨a.1, rfl⟩) (mem_sup_right ⟨a.2, rfl⟩)

Premises used: Set.Mem, Subgroup.mem_sup_left, Prod.fst, Exists.intro, Subgroup.mem_sup_right, Prod.snd, rfl, MulMemClass.mul_mem
-- Module: Mathlib.GroupTheory.NoncommCoprod
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 × N
⊢ Membership.mem (α := P) (f.range ⊔ g.range) ((f.noncommCoprod g comm : (a : M × N) → P) a : P)

Tactic:
exact mul_mem (mem_sup_left ⟨a.1, rfl⟩) (mem_sup_right ⟨a.2, rfl⟩)
-- Module: Mathlib.GroupTheory.NoncommCoprod
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) ∧ g.range ≤ (f.noncommCoprod g comm).range (G := M × N)
⊢ f.range ⊔ g.range ≤ (f.noncommCoprod g comm).range (G := M × N)

Tactic:
rw [sup_le_iff]

Premises used: sup_le_iff
-- Module: Mathlib.GroupTheory.NoncommCoprod
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)
a₁ : g.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)

Tactic:
constructor
-- Module: Mathlib.GroupTheory.NoncommCoprod
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
rw₂ rw₃ : Eq.{u_6 + 1} (α := P) ((f : (a : M) → P) (a, 1).1 : P) ((f : (a : M) → P) a : P)
⊢ Eq.{u_6 + 1} (α := P) ((f.noncommCoprod g comm : (a : M × N) → P) (a, 1) : P) ((f : (a : M) → P) a : P)

Tactic:
rw [noncommCoprod_apply, map_one, mul_one]

Premises used: MonoidHom.noncommCoprod_apply, map_one, mul_one