-- Mathlib/GroupTheory/NoncommCoprod.lean
lemma noncommCoprod_injective {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)) :
    Function.Injective (noncommCoprod f g comm) ↔
      (Function.Injective f ∧ Function.Injective g ∧ _root_.Disjoint f.range g.range)

Proof state:
case refine_3
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)
h : ∀ (a : M) (b : N), f a * g b = 1 → a = 1 ∧ b = 1
x : P
y : M
hy : f y = x
z : N
hz : g z = x
⊢ x ∈ ⊥

Tactic:
rwa [(h y z⁻¹ (by rw [map_inv, hy, hz, mul_inv_cancel])).1, map_one, eq_comm] at hy

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)
h : ∀ (a : M) (b : N), f a * g b = 1 → a = 1 ∧ b = 1
x : P
y : M
hy : f y = x
z : N
hz : g z = x
⊢ f y * g z⁻¹ = 1

Tactic:
rw [map_inv, hy, hz, mul_inv_cancel]

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 : M) (b : N), f a * g b = 1 → a = 1 ∧ b = 1) ↔
    (∀ (a : M), f a = 1 → a = 1) ∧ (∀ (a : N), g a = 1 → a = 1) ∧ f.range ⊓ g.range ≤ ⊥

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

Result:
case refine_1
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)
h : ∀ (a : M) (b : N), f a * g b = 1 → a = 1 ∧ b = 1
x : M
⊢ f x = 1 → x = 1

case refine_2
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)
h : ∀ (a : M) (b : N), f a * g b = 1 → a = 1 ∧ b = 1
x : N
⊢ g x = 1 → x = 1

case refine_3
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)
h : ∀ (a : M) (b : N), f a * g b = 1 → a = 1 ∧ b = 1
⊢ f.range ⊓ g.range ≤ ⊥

case refine_4
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 = 1 → a = 1) ∧ (∀ (a : N), g a = 1 → a = 1) ∧ f.range ⊓ g.range ≤ ⊥ →
    ∀ (a : M) (b : N), f a * g b = 1 → a = 1 ∧ b = 1

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)
⊢ Function.Injective ⇑(f.noncommCoprod g comm) ↔
    Function.Injective ⇑f ∧ Function.Injective ⇑g ∧ 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]

Result:
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) (b : N), f a * g b = 1 → a = 1 ∧ b = 1) ↔
    (∀ (a : M), f a = 1 → a = 1) ∧ (∀ (a : N), g a = 1 → a = 1) ∧ f.range ⊓ g.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)
hf : ∀ (a : M), f a = 1 → a = 1
hg : ∀ (a : N), g a = 1 → a = 1
hp : f.range ⊓ g.range ≤ ⊥
a : M
b : N
h : f a * g b = 1
key : g b ∈ ⊥
⊢ f a = 1

Tactic:
rwa [key, mul_one] at h

Result:
no goals

Proof state:
case refine_4
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)
hf : ∀ (a : M), f a = 1 → a = 1
hg : ∀ (a : N), g a = 1 → a = 1
hp : f.range ⊓ g.range ≤ ⊥
a : M
b : N
h : f a * g b = 1
key : g b ∈ ⊥
⊢ a = 1 ∧ b = 1

Tactic:
exact ⟨hf a (by rwa [key, mul_one] at h), hg b key⟩

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)
hf : ∀ (a : M), f a = 1 → a = 1
hg : ∀ (a : N), g a = 1 → a = 1
hp : f.range ⊓ g.range ≤ ⊥
a : M
b : N
h : f a * g b = 1
⊢ f a⁻¹ = g b

Tactic:
rwa [map_inv, inv_eq_iff_mul_eq_one]

Result:
no goals

Proof state:
case refine_4
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)
hf : ∀ (a : M), f a = 1 → a = 1
hg : ∀ (a : N), g a = 1 → a = 1
hp : f.range ⊓ g.range ≤ ⊥
a : M
b : N
h : f a * g b = 1
⊢ a = 1 ∧ b = 1

Tactic:
have key := hp ⟨⟨a⁻¹, by rwa [map_inv, inv_eq_iff_mul_eq_one]⟩, b, rfl⟩

Result:
case refine_4
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)
hf : ∀ (a : M), f a = 1 → a = 1
hg : ∀ (a : N), g a = 1 → a = 1
hp : f.range ⊓ g.range ≤ ⊥
a : M
b : N
h : f a * g b = 1
key : g b ∈ ⊥
⊢ a = 1 ∧ b = 1

Proof state:
case refine_3
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)
h : ∀ (a : M) (b : N), f a * g b = 1 → a = 1 ∧ b = 1
⊢ f.range ⊓ g.range ≤ ⊥

Tactic:
intro x ⟨⟨y, hy⟩, z, hz⟩

Result:
case refine_3
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)
h : ∀ (a : M) (b : N), f a * g b = 1 → a = 1 ∧ b = 1
x : P
y : M
hy : f y = x
z : N
hz : g z = x
⊢ x ∈ ⊥

Proof state:
case refine_4
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 = 1 → a = 1) ∧ (∀ (a : N), g a = 1 → a = 1) ∧ f.range ⊓ g.range ≤ ⊥ →
    ∀ (a : M) (b : N), f a * g b = 1 → a = 1 ∧ b = 1

Tactic:
intro ⟨hf, hg, hp⟩ a b h

Result:
case refine_4
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)
hf : ∀ (a : M), f a = 1 → a = 1
hg : ∀ (a : N), g a = 1 → a = 1
hp : f.range ⊓ g.range ≤ ⊥
a : M
b : N
h : f a * g b = 1
⊢ a = 1 ∧ b = 1

Proof state:
case refine_2
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)
h : ∀ (a : M) (b : N), f a * g b = 1 → a = 1 ∧ b = 1
x : N
⊢ g x = 1 → x = 1

Tactic:
simpa using h 1 x

Result:
no goals

Proof state:
case refine_1
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)
h : ∀ (a : M) (b : N), f a * g b = 1 → a = 1 ∧ b = 1
x : M
⊢ f x = 1 → x = 1

Tactic:
simpa using h x 1

Result:
no goals