diagram chase thingy

Stream: Is there code for X?

[Alex Kontorovich]

Surely this exists already in mathlib? (And if not, where would it reasonably go?)

import data.set.basic

lemma commutative_diagram_thingy {α β A B : Type*} {f : α → β} {g : A → B} {mA : A → α} {mB : B → β}
   (h : f ∘ mA = mB ∘ g) : ∀ K : set B, mA '' (g ⁻¹' K) ⊆ f ⁻¹' (mB '' K) :=
begin
  rintros K x ⟨a , ha₁, rfl⟩,
  change (f ∘ mA) a ∈ _,
  rw h,
  refine ⟨g a, ha₁, rfl⟩,
end

[Adam Topaz]

Does tidy solve this goal?

[Adam Topaz]

Oh it wont

[Alex Kontorovich]

Almost! Just doesn't know that the diagram commutes?... How do I tell it?

[Adam Topaz]

Maybe you can change the hypothesis to be "for all x, blah blah"?

[Adam Topaz]

import data.set.basic

lemma commutative_diagram_thingy {α β A B : Type*} {f : α → β} {g : A → B} {mA : A → α} {mB : B → β}
   (h : ∀ x, f (mA x) = mB (g x)) : ∀ K : set B, mA '' (g ⁻¹' K) ⊆ f ⁻¹' (mB '' K) :=
by tidy

[David Wärn]

This is also not so bad to do by hand if you use lemmas instead of unfolding definitions

import data.set.basic

lemma commutative_diagram_thingy {α β A B : Type*} {f : α → β} {g : A → B} {mA : A → α} {mB : B → β}
   (h : f ∘ mA = mB ∘ g) : ∀ K : set B, mA '' (g ⁻¹' K) ⊆ f ⁻¹' (mB '' K) :=
begin
  intro K,
  rw [←set.image_subset_iff, ←set.image_comp, h, set.image_comp],
  apply set.image_subset,
  apply set.image_preimage_subset,
end