How to simplify structure construction + field extraction

Stream: new members

[Golol]

Quick question: If I have {my_field := expression}.my_field,
then how can I simplify this to expression? simp works, but I'd like to know what function I would have to apply to perform this manually.
As always, thanks for all the help I'm getting here!

[Kenny Lau]

dsimp only

[Mario Carneiro]

In term mode, you don't have to apply anything at all to perform this reduction

[Mario Carneiro]

it will just naturally happen if you apply a theorem that wouldn't otherwise typecheck

[Mario Carneiro]

in fact, this is what refl does - you apply a theorem that says a = a but the two sides aren't obviously the same so lean performs reduction until they are

[Golol]

I have a proof of

h: ∀ (a : set α), (∃ (j : I) P j a) \iff p i a

how can I apply this to prove the following

{a : set \a |  (∃ (j : I) P j a} = {a : set \a | Pi a}

I thought I could rw h or intro a but it doesn't work.

[Reid Barton]

Start with ext a

[Patrick Massot]

Also have a look at docs#set.ext

[Mario Carneiro]

which, by the way, is an application of set.ext in term mode

[Patrick Massot]

Ha ha! I was faster!

[Golol]

omg thx guys :D

[Patrick Massot]

Golol, what we mean is you can have a look at:

example {α : Type*} {P Q : α → Prop} (h : ∀ x, P x ↔ Q x) : {x | P x} = {x | Q x} :=
set.ext h
--funext (λ x, propext $ h x)

[Patrick Massot]

where the commented line is the proof hidden under set.ext h

[Golol]

Aah, good old functional extensionality

[Golol]

Alright, I need this one extra thing. My situation is the following:

β: Type u
m: measurable_space β
x: set β
h: m.is_measurable' x
⊢ measurable_space.generate_measurable m.is_measurable' x

Here I know that the inductively generated type measurable_space.generate_measurable m.is_measurable'
must at least make every set measurable which is in m.is_measurable' due to the constructor basic.
I couldn't manage to do induction on measurable_space.generate_measurable m.is_measurable... how can I use that with the basic case I can finish my proof?

[Reid Barton]

There is nothing to induct on here, just use the constructor basic as you said.

[Reid Barton]

Induction is the opposite process--"destructing" a value of type generate_measurable .... Here generate_measurable is in the goal, so you want to construct a value, which is what the constructors do.

[Golol]

Oh of course, I was totally stuck on this. Finally done!