MulEquiv between infs

Stream: Is there code for X?

[Alex Brodbelt]

Is there such a 'theorem'? and of this kind in general?

import Mathlib

def MulEquiv.inf_trans_right {G : Type*} [Group G] (A B C : Subgroup G) (m : A ≃* C) : (A ⊓ B :) ≃ (C ⊓ B :) := sorry

[Alex Brodbelt]

Wait this is silly. Ok now the question makes sense

[Alex Brodbelt]

I'll form a better question later, I think I need a different approach for my original problem (not this). After staring at it for a while I do not think this is sensible.

[Floris van Doorn]

This is false as currently stated.

[Alex Brodbelt]

Hmm I thought so :/

[Jz Pan]

I think this is not correct, as there are easy examples of A=B isomorphic to C but A and C are disjoint.