[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f fab : α → β
fbc : β → γ
ga ga' : α → α
gb gb' : β → β
gc gc' : γ → γ
h : Semiconj f ga gb
h' : Semiconj f ga' gb'
x : α
⊢ f ((ga ∘ ga') x) = (gb ∘ gb') (f x)
[PROOFSTEP]
simp only [comp_apply, h.eq, h'.eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f fab : α → β
fbc : β → γ
ga ga' : α → α
gb gb' : β → β
gc gc' : γ → γ
hab : Semiconj fab ga gb
hbc : Semiconj fbc gb gc
x : α
⊢ (fbc ∘ fab) (ga x) = gc ((fbc ∘ fab) x)
[PROOFSTEP]
simp only [comp_apply, hab.eq, hbc.eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f fab : α → β
fbc : β → γ
ga ga' : α → α
gb gb' : β → β
gc gc' : γ → γ
h : Semiconj f ga gb
ha : RightInverse ga' ga
hb : LeftInverse gb' gb
x : α
⊢ f (ga' x) = gb' (f x)
[PROOFSTEP]
rw [← hb (f (ga' x)), ← h.eq, ha x]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
ga : α → α → α
gb : β → β → β
f' : β → γ
gc : γ → γ → γ
hf' : Semiconj₂ f' gb gc
hf : Semiconj₂ f ga gb
x y : α
⊢ (f' ∘ f) (ga x y) = gc ((f' ∘ f) x) ((f' ∘ f) y)
[PROOFSTEP]
simp only [hf'.eq, hf.eq, comp_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
ga : α → α → α
gb : β → β → β
inst✝ : IsAssociative α ga
h : Semiconj₂ f ga gb
h_surj : Surjective f
x₁ x₂ x₃ : α
⊢ gb (gb (f x₁) (f x₂)) (f x₃) = gb (f x₁) (gb (f x₂) (f x₃))
[PROOFSTEP]
simp only [← h.eq, @IsAssociative.assoc _ ga]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
ga : α → α → α
gb : β → β → β
inst✝ : IsAssociative β gb
h : Semiconj₂ f ga gb
h_inj : Injective f
x₁ x₂ x₃ : α
⊢ f (ga (ga x₁ x₂) x₃) = f (ga x₁ (ga x₂ x₃))
[PROOFSTEP]
simp only [h.eq, @IsAssociative.assoc _ gb]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
ga : α → α → α
gb : β → β → β
inst✝ : IsIdempotent α ga
h : Semiconj₂ f ga gb
h_surj : Surjective f
x : α
⊢ gb (f x) (f x) = f x
[PROOFSTEP]
simp only [← h.eq, @IsIdempotent.idempotent _ ga]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
ga : α → α → α
gb : β → β → β
inst✝ : IsIdempotent β gb
h : Semiconj₂ f ga gb
h_inj : Injective f
x : α
⊢ f (ga x x) = f x
[PROOFSTEP]
rw [h.eq, @IsIdempotent.idempotent _ gb]
