Is the following proof using the same theorems in mathlib?

Stream: new members

[Shanghe Chen]

Hi! Doing exercises of MIL Chapter 4 and using simp in them,
I am kind of afraid that I am using the same theorems in mathlib when writing simp.
How do I konw if this happened or not? The exercises are:

import Mathlib.Tactic
open Set
open Function
variable {α β : Type*}
variable (f : α -> β)
variable {I : Type*} (A : I -> Set α) (B : I -> Set β)

theorem mytest1 : (f ⁻¹' ⋃ i, B i) = ⋃ i, f ⁻¹' B i := by
  ext x; constructor
  rintro ⟨s, ⟨i, rfl⟩, fx_in_s: f x ∈ B i⟩
  simp
  use i
  rintro ⟨s, ⟨i, rfl⟩, fx_in_s: f x ∈ B i⟩
  simp
  use i

theorem mytest2 : (f ⁻¹' ⋂ i, B i) = ⋂ i, f ⁻¹' B i := by
  ext x; constructor
  rintro ax
  simp at *
  intro i
  apply ax
  rintro ax
  simp at *
  apply ax

[Floris van Doorn]

You can replace simp by simp? to see what Mathlib lemmas were used.

[Shanghe Chen]

Ah it's very awesome! I saw them showing up:
image.png

[Shanghe Chen]

Yeah... preimage_iUnion is exactly the same as the first exercise, which is used in simp. It does be kind of a cyclic proof..

[Floris van Doorn]

You can try the proof without simp. Or you can use simp [-some_lemma] to exclude some_lemma from that simp-call.

[Shanghe Chen]

Yeah I will redo them without using simp. It's too powerful for a beginer hahaha