How to apply this seemingly simple theorem in lean using con

Stream: new members

[guiwan]

--The theorem can be described as follows:

Theorem Th1 (h1) (h2): [cs= ct, is= it, is ⊆ t ∧ t ⊆ cs].TFAE

--Here, "h1" and "h2" are conditions, "s" and "t" are sets, the corresponding notations "cs", "ct", "is", "it" are also sets. "TFAE" meas that the three terms in "[ ]" are equivalent.

--My goal: apply this Theorem to get the relations: when "h1" and "h2" are satisfied, "cs= ct" -> "cs= ct". ("->"means derive to)

[Notification Bot]

This topic was moved here from #rss > How to apply this seemingly simple theorem in lean using con by Kim Morrison.

[Ruben Van de Velde]

Please read #backticks and update your post accordingly