-- Mathlib/GroupTheory/NoncommCoprod.lean
lemma noncommCoprod_range {M N P : Type*} [Group M] [Group N] [Group P]
    (f : M →* P) (g : N →* P) (comm : ∀ (m : M) (n : N), Commute (f m) (g n)) :
    (noncommCoprod f g comm).range = f.range ⊔ g.range

Proof state:
case a.left.intro
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
a : M
⊢ f a ∈ (f.noncommCoprod g comm).range

Tactic:
exact ⟨(a, 1), by rw [noncommCoprod_apply, map_one, mul_one]⟩

Result:
no goals

Proof state:
case a.intro
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
a : M × N
⊢ (f.noncommCoprod g comm) a ∈ f.range ⊔ g.range

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

Result:
no goals

Proof state:
case a
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
⊢ (f.noncommCoprod g comm).range ≤ f.range ⊔ g.range

Tactic:
rintro - ⟨a, rfl⟩

Result:
case a.intro
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
a : M × N
⊢ (f.noncommCoprod g comm) a ∈ f.range ⊔ g.range

Proof state:
case a
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
⊢ f.range ≤ (f.noncommCoprod g comm).range ∧ g.range ≤ (f.noncommCoprod g comm).range

Tactic:
constructor

Result:
case a.left
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
⊢ f.range ≤ (f.noncommCoprod g comm).range

case a.right
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
⊢ g.range ≤ (f.noncommCoprod g comm).range

Proof state:
case a.right
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
⊢ g.range ≤ (f.noncommCoprod g comm).range

Tactic:
rintro - ⟨a, rfl⟩

Result:
case a.right.intro
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
a : N
⊢ g a ∈ (f.noncommCoprod g comm).range

Proof state:
case a.left
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
⊢ f.range ≤ (f.noncommCoprod g comm).range

Tactic:
rintro - ⟨a, rfl⟩

Result:
case a.left.intro
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
a : M
⊢ f a ∈ (f.noncommCoprod g comm).range

Proof state:
case a.right.intro
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
a : N
⊢ g a ∈ (f.noncommCoprod g comm).range

Tactic:
exact ⟨(1, a), by rw [noncommCoprod_apply, map_one, one_mul]⟩

Result:
no goals

Proof state:
case a
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
⊢ f.range ⊔ g.range ≤ (f.noncommCoprod g comm).range

Tactic:
rw [sup_le_iff]

Result:
case a
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
⊢ f.range ≤ (f.noncommCoprod g comm).range ∧ g.range ≤ (f.noncommCoprod g comm).range

Proof state:
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
a : M
⊢ (f.noncommCoprod g comm) (a, 1) = f a

Tactic:
rw [noncommCoprod_apply, map_one, mul_one]

Result:
no goals

Proof state:
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
a : N
⊢ (f.noncommCoprod g comm) (1, a) = g a

Tactic:
rw [noncommCoprod_apply, map_one, one_mul]

Result:
no goals

Proof state:
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
⊢ (f.noncommCoprod g comm).range = f.range ⊔ g.range

Tactic:
apply le_antisymm

Result:
case a
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
⊢ (f.noncommCoprod g comm).range ≤ f.range ⊔ g.range

case a
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
⊢ f.range ⊔ g.range ≤ (f.noncommCoprod g comm).range