mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Set.Insert

Goal state before:
pp: α : Type u_1
P : α → Prop
a : α
s : Set α
H : ∀ (x : α), x ∈ insert a s → P x
x : α
h : x ∈ s
⊢ P x

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Set.Insert

Goal state before:
pp: α : Type u_1
P : α → Prop
a : α
s : Set α
H : ∀ (x : α), x ∈ s → P x
ha : P a
x : α
h : x ∈ insert a s
⊢ P x

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Set.Insert

Goal state before:
pp: α : Type u_1
P : α → Prop
a : α
s : Set α
⊢ (∃ x, x ∈ insert a s ∧ P x) ↔ P a ∨ ∃ x, x ∈ s ∧ P x

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Set.Insert

Goal state before:
pp: α : Type u_1
P : α → Prop
a : α
s : Set α
⊢ (∀ (x : α), x ∈ insert a s → P x) ↔ P a ∧ ∀ (x : α), x ∈ s → P x

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Set.Insert

Goal state before:
pp: α : Type u_1
β : Type u_2
s t✝ : Set α
a b : α
inst✝ : DecidableEq α
t : Set α
x : α
h✝ : ¬x ∈ t
y : { i // i ∈ insert x t }
h : ¬↑y = x
⊢ ↑y ∈ t

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Set.Insert

Goal state before:
pp: α : Type u_1
β : Type u_2
s t✝ : Set α
a b : α
inst✝ : DecidableEq α
t : Set α
x : α
h : ¬x ∈ t
y : Option { i // i ∈ t }
z : { i // i ∈ t }
⊢ ↑z ∈ insert x t

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Set.Insert

Goal state before:
pp: α : Type u_1
β : Type u_2
s t✝ : Set α
a b : α
inst✝ : DecidableEq α
t : Set α
x : α
h : ¬x ∈ t
y : { i // i ∈ insert x t }
⊢ (fun y ↦ y.elim ⟨x, ⋯⟩ fun z ↦ ⟨↑z, ⋯⟩) ((fun y ↦ if h : ↑y = x then none else some ⟨↑y, ⋯⟩) y) = y

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Set.Insert

Goal state before:
pp: α : Type u_1
s : Set α
x✝ : ∃ a, s = {a}
a : α
h : s = {a}
⊢ (fun a ↦ a ∈ s) a ∧ ∀ (y : α), (fun a ↦ a ∈ s) y → y = a

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Set.Insert

Goal state before:
pp: α : Type u_1
s : Set α
x✝ : ∃! a, a ∈ s
a : α
h : (fun a ↦ a ∈ s) a ∧ ∀ (y : α), (fun a ↦ a ∈ s) y → y = a
⊢ s = {a}

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Set.Insert

Goal state before:
pp: α : Type u_1
s : Set α
x : α
⊢ s ⊆ {x} ↔ s = ∅ ∨ s = {x}

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Set.Insert

Goal state before:
pp: α : Type u_1
a : α
s : Set α
h : ¬a ∈ s
⊢ insert a s \ s = {a}

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Set.Insert

Goal state before:
pp: α : Type u_1
s t : Set α
a : α
h : a ∈ s
⊢ s ∩ insert a t = insert a (s ∩ t)

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Set.Insert

Goal state before:
pp: α : Type u_1
s t : Set α
a : α
h : a ∈ t
⊢ insert a s ∩ t = insert a (s ∩ t)

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Set.Insert

Goal state before:
pp: α : Type u_1
s t : Set α
a : α
h : ¬a ∈ s
⊢ s ∩ insert a t = s ∩ t

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Set.Insert

Goal state before:
pp: α : Type u_1
s t : Set α
a : α
h : ¬a ∈ t
⊢ insert a s ∩ t = s ∩ t

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Set.Insert

Goal state before:
pp: α : Type u_1
s : Set α
a b : α
⊢ {a, b} ⊆ s ↔ a ∈ s ∧ b ∈ s

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Set.Insert

Goal state before:
pp: α : Type u_1
s : Set α
a b : α
⊢ s ⊆ {a, b} ↔ ∀ (x : α), x ∈ s → x = a ∨ x = b

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Set.Insert

Goal state before:
pp: α : Type u_1
s : Set α
x y : α
⊢ s ⊆ {x, y} → s = ∅ ∨ s = {x} ∨ s = {y} ∨ s = {x, y}

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Set.Insert

Goal state before:
pp: α : Type u_1
s : Set α
x y : α
⊢ s = ∅ ∨ s = {x} ∨ s = {y} ∨ s = {x, y} → s ⊆ {x, y}

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Set.Insert

Goal state before:
pp: α : Type u_1
x : α
⊢ 𝒫 {x} = {∅, {x}}

Tactic:
by grind

Goal state after:
Module: Mathlib.Logic.Equiv.Option

Goal state before:
pp: case some
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
x : β
e : { e // e none = x }
val✝ : α
⊢ ↑((fun e ↦
            ⟨{ toFun := fun a ↦ a.casesOn' x (Subtype.val ∘ ⇑e),
                invFun := fun b ↦ if h : b = x then none else some (e.symm ⟨b, h⟩), left_inv := ⋯, right_inv := ⋯ },
              ⋯⟩)
          ((fun e ↦
              { toFun := fun a ↦ ⟨↑e (some a), ⋯⟩, invFun := fun b ↦ ((↑e).symm ↑b).get ⋯, left_inv := ⋯,
                right_inv := ⋯ })
            e))
      (some val✝) =
    ↑e (some val✝)

Tactic:
· simp

Goal state after:
Module: Mathlib.Logic.Equiv.Option

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α✝
a b : α✝
α : Type w
s : α ⊕ PUnit
⊢ (fun o ↦ o.elim (inr PUnit.unit) inl) ((fun s ↦ Sum.elim some (fun x ↦ none) s) s) = s

Tactic:
rcases s with (_ | ⟨⟨⟩⟩)

Goal state after:
case inl
α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α✝
a b : α✝
α : Type w
val✝ : α
⊢ (fun o ↦ o.elim (inr PUnit.unit) inl) ((fun s ↦ Sum.elim some (fun x ↦ none) s) (inl val✝)) = inl val✝

case inr
α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α✝
a b : α✝
α : Type w
⊢ (fun o ↦ o.elim (inr PUnit.unit) inl) ((fun s ↦ Sum.elim some (fun x ↦ none) s) (inr PUnit.unit)) = inr PUnit.unit
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CoheytingAlgebra β
generalizedCoheytingAlgebra : GeneralizedCoheytingAlgebra α := e.generalizedCoheytingAlgebra
top : Top α := e.top
hnot : HNot α := e.hnot
⊢ CoheytingAlgebra α

Tactic:
apply e.injective.coheytingAlgebra <;> intros <;> first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : x < z \ y
hyz : y ≤ z
h' : z \ y ⊔ y ≤ x ⊔ y
⊢ (z \ y) \ y ≤ x

Tactic:
exact (sdiff_le_sdiff_of_sup_le_sup_right h').trans sdiff_le

Goal state after:
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
β : Type u_1
x y z : α
inst✝ : BooleanAlgebra α
a b : α
⊢ a ⊓ (b ⊓ bᶜ) = ⊥

Tactic:
inf_compl_eq_bot',

Goal state after:
α : Type u
β : Type u_1
x y z : α
inst✝ : BooleanAlgebra α
a b : α
⊢ a ⊓ ⊥ = ⊥
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y : α
inst✝ : BooleanAlgebra α
h : yᶜ ≤ x
⊢ xᶜ ≤ y

Tactic:
by
  simpa only [compl_compl] using compl_le_compl h

Goal state after:
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
p : α → Prop
inst✝ : DecidablePred p
x₀ : { a // p a } → β
x : { a // ¬p a } → β
x✝ : { a // ¬p a }
a : α
h : ¬p a
⊢ (if h : p a then x₀ ⟨a, h⟩ else x ⟨a, h⟩) = x ⟨a, h⟩

Tactic:
rw [dif_neg h]

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
h : Disjoint a b
⊢ a ∆ b = a ⊔ b

Tactic:
rw [symmDiff, h.sdiff_eq_left, h.sdiff_eq_right]

Goal state after:
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
X : Sort u_9
Y : Sort u_10
inst✝ : DecidableEq X
x : X
f : { x' // x' ≠ x } → Y
y : Y
⊢ (fun x' ↦ if h : x' ≠ x then f ⟨x', h⟩ else y) ∘ Subtype.val = f

Tactic:
by grind

Goal state after:
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : GeneralizedBooleanAlgebra β
bot : Bot α := e.bot
sdiff : SDiff α := e.sdiff
⊢ GeneralizedBooleanAlgebra α

Tactic:
let distribLattice := e.distribLattice

Goal state after:
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : GeneralizedBooleanAlgebra β
bot : Bot α := e.bot
sdiff : SDiff α := e.sdiff
distribLattice : DistribLattice α := e.distribLattice
⊢ GeneralizedBooleanAlgebra α
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: α : Sort u_1
inst✝ : DecidableEq α
x y : α
h : swap x y = Equiv.refl α
⊢ (Equiv.refl α) x = (Equiv.refl α) y

Tactic:
by grind

Goal state after:
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: α : Sort u_1
inst✝ : DecidableEq α
x y : α
⊢ x = y → swap x y = Equiv.refl α

Tactic:
by grind

Goal state after:
Module: Mathlib.Logic.Equiv.Prod

Goal state before:
pp: α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
e₁ : α ≃ β
e₂ : γ ≃ δ
⊢ LeftInverse (fun x ↦ ⟨e₁.symm x.fst, e₂.symm x.snd⟩) fun x ↦ ⟨e₁ x.fst, e₂ x.snd⟩

Tactic:
by grind

Goal state after:
Module: Mathlib.Logic.Equiv.Prod

Goal state before:
pp: α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
e₁ : α ≃ β
e₂ : γ ≃ δ
⊢ RightInverse (fun x ↦ ⟨e₁.symm x.fst, e₂.symm x.snd⟩) fun x ↦ ⟨e₁ x.fst, e₂ x.snd⟩

Tactic:
by grind

Goal state after:
Module: Mathlib.Logic.Equiv.Prod

Goal state before:
pp: α : Sort u_1
α₁✝ : Sort u_2
α₂✝ : Sort u_3
β : Sort u_4
β₁✝ : Sort u_5
β₂✝ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α₁ : Type u_9
α₂ : Type u_10
β₁ : Type u_11
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
⊢ LeftInverse (fun ab ↦ ((e ab.snd).symm ab.fst, ab.snd)) fun ab ↦ ((e ab.snd) ab.fst, ab.snd)

Tactic:
by grind

Goal state after:
Module: Mathlib.Logic.Equiv.Prod

Goal state before:
pp: α : Sort u_1
α₁✝ : Sort u_2
α₂✝ : Sort u_3
β : Sort u_4
β₁✝ : Sort u_5
β₂✝ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α₁ : Type u_9
α₂ : Type u_10
β₁ : Type u_11
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
⊢ RightInverse (fun ab ↦ ((e ab.snd).symm ab.fst, ab.snd)) fun ab ↦ ((e ab.snd) ab.fst, ab.snd)

Tactic:
by grind

Goal state after:
Module: Mathlib.Logic.Equiv.Prod

Goal state before:
pp: α : Sort u_1
α₁✝ : Sort u_2
α₂✝ : Sort u_3
β : Sort u_4
β₁✝ : Sort u_5
β₂✝ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α₁ : Type u_9
α₂ : Type u_10
β₁ : Type u_11
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
⊢ LeftInverse (fun ab ↦ (ab.fst, (e ab.fst).symm ab.snd)) fun ab ↦ (ab.fst, (e ab.fst) ab.snd)

Tactic:
by grind

Goal state after:
Module: Mathlib.Logic.Equiv.Prod

Goal state before:
pp: α : Sort u_1
α₁✝ : Sort u_2
α₂✝ : Sort u_3
β : Sort u_4
β₁✝ : Sort u_5
β₂✝ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α₁ : Type u_9
α₂ : Type u_10
β₁ : Type u_11
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
⊢ RightInverse (fun ab ↦ (ab.fst, (e ab.fst).symm ab.snd)) fun ab ↦ (ab.fst, (e ab.fst) ab.snd)

Tactic:
by grind

Goal state after:
Module: Mathlib.Logic.Equiv.Prod

Goal state before:
pp: α : Sort u_1
α₁✝ : Sort u_2
α₂✝ : Sort u_3
β : Sort u_4
β₁✝ : Sort u_5
β₂✝ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α₁ : Type u_9
α₂ : Type u_10
β₁ : Type u_11
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
e₁ : α₁ ≃ α₂
e₂ : α₁ → β₁ ≃ β₂
⊢ LeftInverse (fun y ↦ (e₁.symm y.fst, (e₂ (e₁.symm y.fst)).symm y.snd)) fun x ↦ (e₁ x.fst, (e₂ x.fst) x.snd)

Tactic:
by grind

Goal state after:
Module: Mathlib.Logic.Equiv.Prod

Goal state before:
pp: α : Sort u_1
α₁✝ : Sort u_2
α₂✝ : Sort u_3
β : Sort u_4
β₁✝ : Sort u_5
β₂✝ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α₁ : Type u_9
α₂ : Type u_10
β₁ : Type u_11
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
e₁ : α₁ ≃ α₂
e₂ : α₁ → β₁ ≃ β₂
⊢ RightInverse (fun y ↦ (e₁.symm y.fst, (e₂ (e₁.symm y.fst)).symm y.snd)) fun x ↦ (e₁ x.fst, (e₂ x.fst) x.snd)

Tactic:
by grind

Goal state after:
Module: Mathlib.Logic.Equiv.Prod

Goal state before:
pp: α : Sort u_1
α₁✝ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁✝ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α₁ : Type u_9
β₁ : Type u_10
inst✝ : DecidableEq α₁
a : α₁
e : Perm β₁
⊢ LeftInverse (fun ab ↦ if ab.fst = a then (a, (Equiv.symm e) ab.snd) else ab) fun ab ↦
    if ab.fst = a then (a, e ab.snd) else ab

Tactic:
by grind

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ a ∆ (b ∆ (c ∆ d)) = a ∆ (c ∆ (b ∆ d))

Tactic:
symmDiff_left_comm

Goal state after:
Module: Mathlib.Logic.Equiv.Prod

Goal state before:
pp: α : Sort u_1
α₁✝ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁✝ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α₁ : Type u_9
β₁ : Type u_10
inst✝ : DecidableEq α₁
a : α₁
e : Perm β₁
⊢ RightInverse (fun ab ↦ if ab.fst = a then (a, (Equiv.symm e) ab.snd) else ab) fun ab ↦
    if ab.fst = a then (a, e ab.snd) else ab

Tactic:
by grind

Goal state after:
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
P : α → Sort u_9
e : α ≃ β
f : (a : α) → P a
⊢ (fun f x ↦ ⋯ ▸ f (e x)) ((fun f x ↦ f (e.symm x)) f) = f

Tactic:
by grind

Goal state after:
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
P : α → Sort u_9
e : α ≃ β
f : (b : β) → P (e.symm b)
⊢ (fun f x ↦ f (e.symm x)) ((fun f x ↦ ⋯ ▸ f (e x)) f) = f

Tactic:
by grind

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
ha : Disjoint a c
hb : Disjoint b c
⊢ Disjoint (a ∆ b) c

Tactic:
by
  rw [symmDiff_eq_sup_sdiff_inf]
  exact (ha.sup_left hb).disjoint_sdiff_left

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ⇔ (b ⇔ c) = b ⇔ (a ⇔ c)

Tactic:
by simp_rw [← bihimp_assoc, bihimp_comm]

Goal state after:
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_4
W : α → Sort w
Z : β → Sort z
h₁ : α ≃ β
h₂ : (b : β) → W (h₁.symm b) ≃ Z b
f : (b : β) → Z b
b : β
⊢ (h₁.piCongr' h₂).symm f (h₁.symm b) = (h₂ b).symm (f b)

Tactic:
by
  simp [piCongr', piCongr_apply_apply]

Goal state after:
Module: Mathlib.Logic.Equiv.Prod

Goal state before:
pp: α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
ι : Type u_9
α : ι → Type u_10
β : Type u_11
⊢ LeftInverse (fun p ↦ (⟨p.fst, p.snd.fst⟩, p.snd.snd)) fun p ↦ ⟨p.fst.fst, (p.fst.snd, p.snd)⟩

Tactic:
by grind

Goal state after:
Module: Mathlib.Logic.Equiv.Prod

Goal state before:
pp: α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
ι : Type u_9
α : ι → Type u_10
β : Type u_11
⊢ RightInverse (fun p ↦ (⟨p.fst, p.snd.fst⟩, p.snd.snd)) fun p ↦ ⟨p.fst.fst, (p.fst.snd, p.snd)⟩

Tactic:
by grind

Goal state after:
Module: Mathlib.Logic.Equiv.Prod

Goal state before:
pp: α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_9
x✝ : Bool → α
⊢ (fun p b ↦ if b = true then p.snd else p.fst) ((fun f ↦ (f false, f true)) x✝) = x✝

Tactic:
by grind

Goal state after:
Module: Mathlib.Logic.Equiv.Prod

Goal state before:
pp: α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_9
p : α → Prop
β : α → Type u_10
inst✝ : DecidablePred p
f : (i : α) → β i
⊢ (fun f x ↦ if h : p x then f.fst ⟨x, h⟩ else f.snd ⟨x, h⟩) ((fun f ↦ (fun x ↦ f ↑x, fun x ↦ f ↑x)) f) = f

Tactic:
by grind

Goal state after:
Module: Mathlib.Logic.Equiv.Prod

Goal state before:
pp: α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_9
inst✝ : DecidableEq α
i : α
β : α → Type u_10
f : (j : α) → β j
⊢ (fun f j ↦ if h : j = i then ⋯ ▸ f.fst else f.snd ⟨j, h⟩) ((fun f ↦ (f i, fun j ↦ f ↑j)) f) = f

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
b : β
s : Set β
inst✝ : Decidable (b ∈ s)
⊢ (fun x ↦ b) ⁻¹' s = if b ∈ s then univ else ∅

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
p : α → Prop
s : Set (Subtype p)
t : Set α
⊢ s = Subtype.val ⁻¹' t ↔ ∀ (x : α) (h : p x), ⟨x, h⟩ ∈ s ↔ x ∈ t

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s : Set α
a : α
⊢ a ∈ s → f a ∈ f '' s

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s t : Set α
h : s ⊆ t
⊢ f '' s ⊆ f '' t

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
⊢ image (g ∘ f) = image g ∘ image f

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
⊢ image g ∘ image f = image (g ∘ f)

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
β' : Type u_5
f : β → γ
g : α → β
f' : α → β'
g' : β' → γ
h_comm : ∀ (a : α), f (g a) = g' (f' a)
⊢ f '' g '' s = g' '' f' '' s

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s t : Set α
⊢ f '' (s ∪ t) = f '' s ∪ f '' t

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
⊢ f '' ∅ = ∅

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
a : α
⊢ f '' {a} = {f a}

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Set.Image

Goal state before:
pp: case succ
α : Type u_1
f : α → α
n : ℕ
ih : image f^[n] = (image f)^[n]
⊢ image (f ∘ f^[n]) = image f ∘ image f^[n]

Tactic:
image_comp_eq

Goal state after:
case succ
α : Type u_1
f : α → α
n : ℕ
ih : image f^[n] = (image f)^[n]
⊢ image f ∘ image f^[n] = image f ∘ image f^[n]
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
a : α
s : Set α
⊢ f '' insert a s = insert (f a) (f '' s)

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
a b : α
⊢ f '' {a, b} = {f a, f b}

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set β
hs : s.Nonempty
f : α → β
hf : Surjective f
y : β
hy : y ∈ s
x : α
hx : f x = y
⊢ x ∈ f ⁻¹' s

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
h : Surjective f
x : β
hx : x ∈ s
y : α
e : f y = x
⊢ y ∈ f ⁻¹' s ∧ f y = x

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ f '' (s ∩ f ⁻¹' t) = f '' s ∩ t

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
b : β
hb : b ∈ t
⊢ (fun a ↦ (a, b)) ⁻¹' s ×ˢ t = s

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
a : α
ha : a ∈ s
⊢ Prod.mk a ⁻¹' s ×ˢ t = t

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
b : β
hb : ¬b ∈ t
⊢ (fun a ↦ (a, b)) ⁻¹' s ×ˢ t = ∅

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
a : α
ha : ¬a ∈ s
⊢ Prod.mk a ⁻¹' s ×ˢ t = ∅

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
b : β
inst✝ : DecidablePred fun x ↦ x ∈ t
⊢ (fun a ↦ (a, b)) ⁻¹' s ×ˢ t = if b ∈ t then s else ∅

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
a : α
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ Prod.mk a ⁻¹' s ×ˢ t = if a ∈ s then t else ∅

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
b : β
inst✝ : DecidablePred fun x ↦ x ∈ t
f : γ → α
⊢ (fun a ↦ (f a, b)) ⁻¹' s ×ˢ t = if b ∈ t then f ⁻¹' s else ∅

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
δ : Type u_4
s : Set α
t : Set β
a : α
inst✝ : DecidablePred fun x ↦ x ∈ s
g : δ → β
⊢ (fun b ↦ (a, g b)) ⁻¹' s ×ˢ t = if a ∈ s then g ⁻¹' t else ∅

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ Prod.swap ⁻¹' s ×ˢ t = t ×ˢ s

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
⊢ (range fun x ↦ (f x, g x)) ⊆ range f ×ˢ range g

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
s : Set α
⊢ (fun x ↦ (f x, g x)) '' s ⊆ (f '' s) ×ˢ (g '' s)

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
b : β
hb : b ∈ t
⊢ (fun a ↦ (a, b)) '' s ⊆ s ×ˢ t

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
a : α
ha : a ∈ s
⊢ Prod.mk a '' t ⊆ s ×ˢ t

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
⊢ s ×ˢ t \ s₁ ×ˢ t₁ = s ×ˢ (t \ t₁) ∪ (s \ s₁) ×ˢ t

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Set.Restrict

Goal state before:
pp: α : Type u_1
ι : Sort u_5
f : ι → α
⊢ Surjective (codRestrict f (range f) ⋯)

Tactic:
rintro ⟨b, ⟨a, rfl⟩⟩

Goal state after:
α : Type u_1
ι : Sort u_5
f : ι → α
a : ι
⊢ ∃ a_1, codRestrict f (range f) ⋯ a_1 = ⟨f a, ⋯⟩
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
s : Set α
a : α
t : Set α
h : t ∈ 𝒫 insert a s
hs : a ∈ t
⊢ t \ {a} ∈ 𝒫 s ∧ insert a (t \ {a}) = t

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
ι : Sort u_4
f : ι → α
p : ↑(range f) → Prop
⊢ (∀ (a : ↑(range f)), p a) ↔ ∀ (i : ι), p ⟨f i, ⋯⟩

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
ι : Sort u_4
f : ι → α
p : ↑(range f) → Prop
⊢ (∃ a, p a) ↔ ∃ i, p ⟨f i, ⋯⟩

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
⊢ f '' univ = range f

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ f '' s ⊆ range f

Tactic:
← image_univ

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ f '' s ⊆ f '' univ
Module: Mathlib.Data.Set.Image

Goal state before:
pp: i : ℕ
⊢ i ∈ range Nat.succ → 0 < i

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set β
hs : s.Nonempty
f : α → β
hf : s ⊆ range f
w✝ : β
hy : w✝ ∈ s
x : α
hx : f x = w✝
⊢ x ∈ f ⁻¹' s

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ range f = s ↔ (∀ (a : α), f a ∈ s) ∧ ∀ (b : β), b ∈ s → ∃ a, f a = b

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
⊢ range (g ∘ f) ⊆ range g

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
⊢ f '' s ∪ f '' sᶜ = range f

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
hs : s ⊆ range f
⊢ f '' f ⁻¹' s = s

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ f '' f ⁻¹' s = s ↔ s ⊆ range f

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Set.Image

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
⊢ f ⁻¹' s ⊆ f ⁻¹' t → s ⊆ t

pp: case mpr
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
⊢ s ⊆ t → f ⁻¹' s ⊆ f ⁻¹' t

Tactic:
· intro h x hx
    rcases hs hx with ⟨y, rfl⟩
    exact h hx

Goal state after:
case mpr
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
⊢ s ⊆ t → f ⁻¹' s ⊆ f ⁻¹' t