How to use theorems in the general case to the specific...

Stream: new members

[Kent Van Vels]

If I have proven something about a BooleanAlgebra, say, what is the proper leverage that proof for a special case of Set X. Where we know that the structure on Set X is a Boolean Algebra. What follows in a MWE. I know the specific result is actually in mathlib, so I know I can just use that. I am interested in the correct way to do this in general.

import Mathlib.Tactic
--set_option pp.explicit true

variable {X Y: Type*} [BooleanAlgebra X] (A : X) (AA : Set Y)

theorem T_for_BAlg : Aᶜ = ⊤  ↔ A = ⊥ := compl_eq_top

theorem T_for_set : AAᶜ = Set.univ ↔ AA = ∅ := by
  have h1 : BooleanAlgebra (Set Y) := Set.instBooleanAlgebraSet
  have h2 := T_for_BAlg AA
  rw [←Set.top_eq_univ,←Set.bot_eq_empty]
  exact h2 --doesn't work

If one uncomments the `(set_option pp.explicit true) line, then the goal is shown to be definitionally unequal to h2 but it seems like it should be. Any help is appreciated.

[Ruben Van de Velde]

Remove the h1

[Ruben Van de Velde]

It's redundant (finding the instance is lean's job), and by using have rather than let, lean can no longer see that it's actually the same instance that comes up in Set.bot_eq_empty and friends

[Kent Van Vels]

Ok, that makes sense. I thought that I tried it without my h2 line before. Thanks for the help.

[Kent Van Vels]

You are Dutch, correct? Do you know any Van Vels there?

[Notification Bot]

Kent Van Vels has marked this topic as resolved.

[Notification Bot]

Kent Van Vels has marked this topic as unresolved.