-- Mathlib/Algebra/Group/Graph.lean
/-- **Line test** for monoid isomorphisms.

Let `f : G → H × I` be a homomorphism to a product of monoids. Assume that `f` is surjective on both
factors and that the image of `f` intersects every "vertical line" `{(h, i) | i : I}` and every
"horizontal line" `{(h, i) | h : H}` at most once. Then the image of `f` is the graph of some monoid
isomorphism `f' : H ≃ I`. -/
@[to_additive "**Line test** for monoid isomorphisms.

Let `f : G → H × I` be a homomorphism to a product of monoids. Assume that `f` is surjective on both
factors and that the image of `f` intersects every \"vertical line\" `{(h, i) | i : I}` and every
\"horizontal line\" `{(h, i) | h : H}` at most once. Then the image of `f` is the graph of some
monoid isomorphism `f' : H ≃ I`."]
lemma exists_mulEquiv_mrange_eq_mgraph {f : G →* H × I} (hf₁ : Surjective (Prod.fst ∘ f))
    (hf₂ : Surjective (Prod.snd ∘ f)) (hf : ∀ g₁ g₂, (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2) :
    ∃ e : H ≃* I, mrange f = e.toMonoidHom.mgraph

Proof state:
G : Type u_1
H : Type u_2
I : Type u_3
inst✝² : Monoid G
inst✝¹ : Monoid H
inst✝ : Monoid I
f : G →* H × I
hf₁ : Surjective (Prod.fst ∘ ⇑f)
hf₂ : Surjective (Prod.snd ∘ ⇑f)
hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : H →* I
he₁ : mrange f = e₁.mgraph
⊢ Surjective (Prod.fst ∘ ⇑(MulEquiv.prodComm.toMonoidHom.comp f))

Tactic:
simpa

Result:
no goals

Proof state:
case intro.intro
G : Type u_1
H : Type u_2
I : Type u_3
inst✝² : Monoid G
inst✝¹ : Monoid H
inst✝ : Monoid I
f : G →* H × I
hf₁ : Surjective (Prod.fst ∘ ⇑f)
hf₂ : Surjective (Prod.snd ∘ ⇑f)
hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : H →* I
he₁ : mrange f = e₁.mgraph
e₂ : I →* H
he₂ : mrange (MulEquiv.prodComm.toMonoidHom.comp f) = e₂.mgraph
⊢ ∃ e, mrange f = e.toMonoidHom.mgraph

Tactic:
have he₁₂ h i : e₁ h = i ↔ e₂ i = h := by
  rw [SetLike.ext_iff] at he₁ he₂
  aesop (add simp [Prod.swap_eq_iff_eq_swap])

Result:
case intro.intro
G : Type u_1
H : Type u_2
I : Type u_3
inst✝² : Monoid G
inst✝¹ : Monoid H
inst✝ : Monoid I
f : G →* H × I
hf₁ : Surjective (Prod.fst ∘ ⇑f)
hf₂ : Surjective (Prod.snd ∘ ⇑f)
hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : H →* I
he₁ : mrange f = e₁.mgraph
e₂ : I →* H
he₂ : mrange (MulEquiv.prodComm.toMonoidHom.comp f) = e₂.mgraph
he₁₂ : ∀ (h : H) (i : I), e₁ h = i ↔ e₂ i = h
⊢ ∃ e, mrange f = e.toMonoidHom.mgraph

Proof state:
G : Type u_1
H : Type u_2
I : Type u_3
inst✝² : Monoid G
inst✝¹ : Monoid H
inst✝ : Monoid I
f : G →* H × I
hf₁ : Surjective (Prod.fst ∘ ⇑f)
hf₂ : Surjective (Prod.snd ∘ ⇑f)
hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
⊢ ∃ e, mrange f = e.toMonoidHom.mgraph

Tactic:
obtain ⟨e₁, he₁⟩ := f.exists_mrange_eq_mgraph hf₁ fun _ _ ↦ (hf _ _).1

Result:
case intro
G : Type u_1
H : Type u_2
I : Type u_3
inst✝² : Monoid G
inst✝¹ : Monoid H
inst✝ : Monoid I
f : G →* H × I
hf₁ : Surjective (Prod.fst ∘ ⇑f)
hf₂ : Surjective (Prod.snd ∘ ⇑f)
hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : H →* I
he₁ : mrange f = e₁.mgraph
⊢ ∃ e, mrange f = e.toMonoidHom.mgraph

Proof state:
G : Type u_1
H : Type u_2
I : Type u_3
inst✝² : Monoid G
inst✝¹ : Monoid H
inst✝ : Monoid I
f : G →* H × I
hf₁ : Surjective (Prod.fst ∘ ⇑f)
hf₂ : Surjective (Prod.snd ∘ ⇑f)
hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : H →* I
he₁ : ∀ (x : H × I), x ∈ mrange f ↔ x ∈ e₁.mgraph
e₂ : I →* H
he₂ : ∀ (x : I × H), x ∈ mrange (MulEquiv.prodComm.toMonoidHom.comp f) ↔ x ∈ e₂.mgraph
h : H
i : I
⊢ e₁ h = i ↔ e₂ i = h

Tactic:
aesop (add simp [Prod.swap_eq_iff_eq_swap])

Result:
no goals

Proof state:
G : Type u_1
H : Type u_2
I : Type u_3
inst✝² : Monoid G
inst✝¹ : Monoid H
inst✝ : Monoid I
f : G →* H × I
hf₁ : Surjective (Prod.fst ∘ ⇑f)
hf₂ : Surjective (Prod.snd ∘ ⇑f)
hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : H →* I
he₁ : mrange f = e₁.mgraph
e₂ : I →* H
he₂ : mrange (MulEquiv.prodComm.toMonoidHom.comp f) = e₂.mgraph
h : H
i : I
⊢ e₁ h = i ↔ e₂ i = h

Tactic:
rw [SetLike.ext_iff] at he₁ he₂

Result:
G : Type u_1
H : Type u_2
I : Type u_3
inst✝² : Monoid G
inst✝¹ : Monoid H
inst✝ : Monoid I
f : G →* H × I
hf₁ : Surjective (Prod.fst ∘ ⇑f)
hf₂ : Surjective (Prod.snd ∘ ⇑f)
hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : H →* I
he₁ : ∀ (x : H × I), x ∈ mrange f ↔ x ∈ e₁.mgraph
e₂ : I →* H
he₂ : ∀ (x : I × H), x ∈ mrange (MulEquiv.prodComm.toMonoidHom.comp f) ↔ x ∈ e₂.mgraph
h : H
i : I
⊢ e₁ h = i ↔ e₂ i = h

Proof state:
G : Type u_1
H : Type u_2
I : Type u_3
inst✝² : Monoid G
inst✝¹ : Monoid H
inst✝ : Monoid I
f : G →* H × I
hf₁ : Surjective (Prod.fst ∘ ⇑f)
hf₂ : Surjective (Prod.snd ∘ ⇑f)
hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : H →* I
he₁ : mrange f = e₁.mgraph
e₂ : I →* H
he₂ : mrange (MulEquiv.prodComm.toMonoidHom.comp f) = e₂.mgraph
he₁₂ : ∀ (h : H) (i : I), e₁ h = i ↔ e₂ i = h
h : H
⊢ e₂ (e₁ h) = h

Tactic:
rw [← he₁₂]

Result:
no goals

Proof state:
case intro.intro
G : Type u_1
H : Type u_2
I : Type u_3
inst✝² : Monoid G
inst✝¹ : Monoid H
inst✝ : Monoid I
f : G →* H × I
hf₁ : Surjective (Prod.fst ∘ ⇑f)
hf₂ : Surjective (Prod.snd ∘ ⇑f)
hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : H →* I
he₁ : mrange f = e₁.mgraph
e₂ : I →* H
he₂ : mrange (MulEquiv.prodComm.toMonoidHom.comp f) = e₂.mgraph
he₁₂ : ∀ (h : H) (i : I), e₁ h = i ↔ e₂ i = h
⊢ ∃ e, mrange f = e.toMonoidHom.mgraph

Tactic:
exact ⟨
{ toFun := e₁
  map_mul' := e₁.map_mul'
  invFun := e₂
  left_inv := fun h ↦ by rw [← he₁₂]
  right_inv := fun i ↦ by rw [he₁₂] }, he₁⟩

Result:
no goals

Proof state:
G : Type u_1
H : Type u_2
I : Type u_3
inst✝² : Monoid G
inst✝¹ : Monoid H
inst✝ : Monoid I
f : G →* H × I
hf₁ : Surjective (Prod.fst ∘ ⇑f)
hf₂ : Surjective (Prod.snd ∘ ⇑f)
hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : H →* I
he₁ : mrange f = e₁.mgraph
⊢ ∀ (g₁ g₂ : G),
    ((MulEquiv.prodComm.toMonoidHom.comp f) g₁).1 = ((MulEquiv.prodComm.toMonoidHom.comp f) g₂).1 →
      ((MulEquiv.prodComm.toMonoidHom.comp f) g₁).2 = ((MulEquiv.prodComm.toMonoidHom.comp f) g₂).2

Tactic:
simp [hf]

Result:
no goals

Proof state:
G : Type u_1
H : Type u_2
I : Type u_3
inst✝² : Monoid G
inst✝¹ : Monoid H
inst✝ : Monoid I
f : G →* H × I
hf₁ : Surjective (Prod.fst ∘ ⇑f)
hf₂ : Surjective (Prod.snd ∘ ⇑f)
hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : H →* I
he₁ : mrange f = e₁.mgraph
e₂ : I →* H
he₂ : mrange (MulEquiv.prodComm.toMonoidHom.comp f) = e₂.mgraph
he₁₂ : ∀ (h : H) (i : I), e₁ h = i ↔ e₂ i = h
i : I
⊢ e₁ (e₂ i) = i

Tactic:
rw [he₁₂]

Result:
no goals

Proof state:
case intro
G : Type u_1
H : Type u_2
I : Type u_3
inst✝² : Monoid G
inst✝¹ : Monoid H
inst✝ : Monoid I
f : G →* H × I
hf₁ : Surjective (Prod.fst ∘ ⇑f)
hf₂ : Surjective (Prod.snd ∘ ⇑f)
hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : H →* I
he₁ : mrange f = e₁.mgraph
⊢ ∃ e, mrange f = e.toMonoidHom.mgraph

Tactic:
obtain ⟨e₂, he₂⟩ := (MulEquiv.prodComm.toMonoidHom.comp f).exists_mrange_eq_mgraph (by simpa) <|
  by simp [hf]

Result:
case intro.intro
G : Type u_1
H : Type u_2
I : Type u_3
inst✝² : Monoid G
inst✝¹ : Monoid H
inst✝ : Monoid I
f : G →* H × I
hf₁ : Surjective (Prod.fst ∘ ⇑f)
hf₂ : Surjective (Prod.snd ∘ ⇑f)
hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : H →* I
he₁ : mrange f = e₁.mgraph
e₂ : I →* H
he₂ : mrange (MulEquiv.prodComm.toMonoidHom.comp f) = e₂.mgraph
⊢ ∃ e, mrange f = e.toMonoidHom.mgraph