mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
β : Type u_1
x✝ y✝ z : α
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
x y : α × β
⊢ x ⇨ y = y ⊔ xᶜ

Tactic:
ext

Goal state after:
case fst
α : Type u
β : Type u_1
x✝ y✝ z : α
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
x y : α × β
⊢ (x ⇨ y).fst = (y ⊔ xᶜ).fst

case snd
α : Type u
β : Type u_1
x✝ y✝ z : α
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
x y : α × β
⊢ (x ⇨ y).snd = (y ⊔ xᶜ).snd
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: α : Sort u_1
p : α → Prop
h : ∀ (a : α), p a ↔ p ((Equiv.refl α) a)
⊢ (Equiv.refl α).subtypeEquiv h = Equiv.refl { a // p a }

Tactic:
ext

Goal state after:
α : Sort u_1
p : α → Prop
h : ∀ (a : α), p a ↔ p ((Equiv.refl α) a)
x✝ : { a // p a }
⊢ ↑(((Equiv.refl α).subtypeEquiv h) x✝) = ↑((Equiv.refl { a // p a }) x✝)
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
⊢ a ∆ b \ b = a \ b

Tactic:
rw [symmDiff_comm, symmDiff_sdiff_left]

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

Goal state before:
pp: α : Type u_9
inst✝ : DecidableEq α
s : Set α
i j : α
hi : i ∈ s
hj : ¬j ∈ s
a : α
⊢ a ∈ Set.image (⇑(swap i j)) s ↔ a ∈ insert j s \ {i}

Tactic:
constructor

Goal state after:
case mp
α : Type u_9
inst✝ : DecidableEq α
s : Set α
i j : α
hi : i ∈ s
hj : ¬j ∈ s
a : α
⊢ a ∈ Set.image (⇑(swap i j)) s → a ∈ insert j s \ {i}

case mpr
α : Type u_9
inst✝ : DecidableEq α
s : Set α
i j : α
hi : i ∈ s
hj : ¬j ∈ s
a : α
⊢ a ∈ insert j s \ {i} → a ∈ Set.image (⇑(swap i j)) s
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_4
P : Sort u_9
e : α ≃ β
⊢ (piCongrLeft' (fun x ↦ P) e).symm = piCongrLeft' (fun a ↦ P) e.symm

Tactic:
ext

Goal state after:
α : Sort u_1
β : Sort u_4
P : Sort u_9
e : α ≃ β
x✝¹ : β → P
x✝ : α
⊢ (piCongrLeft' (fun x ↦ P) e).symm x✝¹ x✝ = (piCongrLeft' (fun a ↦ P) e.symm) x✝¹ x✝
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
a b : α
⊢ bᶜ \ aᶜ ⊔ aᶜ \ bᶜ = a ∆ b

Tactic:
by simp_rw [compl_sdiff_compl, sdiff_eq, symmDiff_eq]

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

Goal state before:
pp: α : Type u_1
p : α → Prop
⊢ p ⁻¹' {True} = {a | p a}

Tactic:
ext

Goal state after:
α : Type u_1
p : α → Prop
x✝ : α
⊢ x✝ ∈ p ⁻¹' {True} ↔ x✝ ∈ {a | p a}
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
p : α → Prop
⊢ p ⁻¹' {False} = {a | ¬p a}

Tactic:
ext

Goal state after:
α : Type u_1
p : α → Prop
x✝ : α
⊢ x✝ ∈ p ⁻¹' {False} ↔ x✝ ∈ {a | ¬p a}
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
s u v : Set α
hsuv : s ⊆ u ∪ v
H : s ∩ (u ∩ v) = ∅
x : α
x_in_s : x ∈ s
⊢ ⟨x, x_in_s⟩ ∈ Subtype.val ⁻¹' u ↔ ⟨x, x_in_s⟩ ∈ (Subtype.val ⁻¹' v)ᶜ

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
s u v : Set α
hsuv : s ⊆ u ∪ v
H : s ∩ (u ∩ v) = ∅
x : α
x_in_s : x ∈ s
⊢ ⟨x, x_in_s⟩ ∈ Subtype.val ⁻¹' u → ⟨x, x_in_s⟩ ∈ (Subtype.val ⁻¹' v)ᶜ

case mpr
α : Type u_1
s u v : Set α
hsuv : s ⊆ u ∪ v
H : s ∩ (u ∩ v) = ∅
x : α
x_in_s : x ∈ s
⊢ ⟨x, x_in_s⟩ ∈ (Subtype.val ⁻¹' v)ᶜ → ⟨x, x_in_s⟩ ∈ Subtype.val ⁻¹' u
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
⊢ image id = id

Tactic:
ext

Goal state after:
α : Type u_1
x✝¹ : Set α
x✝ : α
⊢ x✝ ∈ id '' x✝¹ ↔ x✝ ∈ id x✝¹
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
s : Set α
⊢ (fun x ↦ x) '' s = s

Tactic:
ext

Goal state after:
α : Type u_1
s : Set α
x✝ : α
⊢ x✝ ∈ (fun x ↦ x) '' s ↔ x✝ ∈ s
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
⊢ s ×ˢ ∅ = ∅

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
x✝ : α × β
⊢ x✝ ∈ s ×ˢ ∅ ↔ x✝ ∈ ∅
Module: Mathlib.Data.Set.Image

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

Tactic:
constructor

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

case mpr
α : Type u_1
β : Type u_2
f : α → β
s s' : Set β
⊢ f ⁻¹' s ⊆ f ⁻¹' s' → range f ∩ s ⊆ range f ∩ s'
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
t : Set β
⊢ ∅ ×ˢ t = ∅

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
t : Set β
x✝ : α × β
⊢ x✝ ∈ ∅ ×ˢ t ↔ x✝ ∈ ∅
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
⊢ univ ×ˢ univ = univ

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
x✝ : α × β
⊢ x✝ ∈ univ ×ˢ univ ↔ x✝ ∈ univ
Module: Mathlib.Data.Set.Image

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

Tactic:
← image_union,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s t : Set α
⊢ f '' s ⊆ f '' (t ∪ s \ t)
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
⊢ Disjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) ↔ Disjoint s₁ s₂ ∨ Disjoint t₁ t₂

Tactic:
disjoint_left,

Goal state after:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
⊢ (∀ ⦃a : α × β⦄, a ∈ s₁ ×ˢ t₁ → ¬a ∈ s₂ ×ˢ t₂) ↔ (∀ ⦃a : α⦄, a ∈ s₁ → ¬a ∈ s₂) ∨ ∀ ⦃a : β⦄, a ∈ t₁ → ¬a ∈ t₂
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β
g : γ → δ
s : Set α
t : Set γ
⊢ Prod.map f g '' s ×ˢ t = (f '' s) ×ˢ (g '' t)

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β
g : γ → δ
s : Set α
t : Set γ
x✝ : β × δ
⊢ x✝ ∈ Prod.map f g '' s ×ˢ t ↔ x✝ ∈ (f '' s) ×ˢ (g '' t)
Module: Mathlib.Data.Set.Restrict

Goal state before:
pp: α : Type u_1
ι : Sort u_5
f : ι → α
s : Set α
h : ∀ (x : ι), f x ∈ s
⊢ range (codRestrict f s h) = Subtype.val ⁻¹' range f

Tactic:
ext

Goal state after:
α : Type u_1
ι : Sort u_5
f : ι → α
s : Set α
h : ∀ (x : ι), f x ∈ s
x✝ : ↑s
⊢ x✝ ∈ range (codRestrict f s h) ↔ x✝ ∈ Subtype.val ⁻¹' range f
Module: Mathlib.Data.Set.Restrict

Goal state before:
pp: α : Type u_1
β : Type u_2
t : Set β
f : α → β
u : Set ↑t
⊢ Subtype.val '' t.restrictPreimage f ⁻¹' u = f ⁻¹' Subtype.val '' u

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
t : Set β
f : α → β
u : Set ↑t
x✝ : α
⊢ x✝ ∈ Subtype.val '' t.restrictPreimage f ⁻¹' u ↔ x✝ ∈ f ⁻¹' Subtype.val '' u
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
s : Set α
a : α
t : Set α
⊢ t ∈ 𝒫 insert a s ↔ t ∈ 𝒫 s ∪ insert a '' 𝒫 s

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
s : Set α
a : α
t : Set α
⊢ t ∈ 𝒫 insert a s → t ∈ 𝒫 s ∪ insert a '' 𝒫 s

case mpr
α : Type u_1
s : Set α
a : α
t : Set α
⊢ t ∈ 𝒫 s ∪ insert a '' 𝒫 s → t ∈ 𝒫 insert a s
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
⊢ s ×ˢ t = s₁ ×ˢ t₁ ↔ s = s₁ ∧ t = t₁

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
⊢ s ×ˢ t = s₁ ×ˢ t₁ → s = s₁ ∧ t = t₁

case mpr
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
⊢ s = s₁ ∧ t = t₁ → s ×ˢ t = s₁ ×ˢ t₁
Module: Mathlib.Data.Set.Image

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

Tactic:
constructor

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

case mpr
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
⊢ s ⊆ t → f ⁻¹' s ⊆ f ⁻¹' t
Module: Mathlib.Data.Set.Image

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

Tactic:
constructor

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

case mpr
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
ht : t ⊆ range f
⊢ s = t → f ⁻¹' s = f ⁻¹' t
Module: Mathlib.Data.Set.Piecewise

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
y : β
⊢ y ∈ range (s.piecewise f g) ↔ y ∈ f '' s ∪ g '' sᶜ

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
y : β
⊢ y ∈ range (s.piecewise f g) → y ∈ f '' s ∪ g '' sᶜ

case mpr
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
y : β
⊢ y ∈ f '' s ∪ g '' sᶜ → y ∈ range (s.piecewise f g)
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set β
⊢ Sum.inl ⁻¹' Sum.inr '' s = ∅

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
s : Set β
x✝ : α
⊢ x✝ ∈ Sum.inl ⁻¹' Sum.inr '' s ↔ x✝ ∈ ∅
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
⊢ Sum.inr ⁻¹' Sum.inl '' s = ∅

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
x✝ : β
⊢ x✝ ∈ Sum.inr ⁻¹' Sum.inl '' s ↔ x✝ ∈ ∅
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ f '' s = range fun x ↦ f ↑x

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
x✝ : β
⊢ x✝ ∈ f '' s ↔ x✝ ∈ range fun x ↦ f ↑x
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
x✝ : β
⊢ x✝ ∈ f '' s ↔ x✝ ∈ range fun x ↦ f ↑x

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
β : Type u_2
f : α → β
s : Set α
x✝ : β
⊢ x✝ ∈ f '' s → x✝ ∈ range fun x ↦ f ↑x

case mpr
α : Type u_1
β : Type u_2
f : α → β
s : Set α
x✝ : β
⊢ (x✝ ∈ range fun x ↦ f ↑x) → x✝ ∈ f '' s
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
x : ↑(range f)
⊢ rangeFactorization f (rangeSplitting f x) = x

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
x : ↑(range f)
⊢ ↑(rangeFactorization f (rangeSplitting f x)) = ↑x
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_5
β : Type u_6
γ : Type u_7
γ' : Type u_8
δ : Type u_9
δ' : Type u_10
h : β → α
f : γ → β
f₁ : γ' → α
f₂ : γ → γ'
g : δ → β
g₁ : δ' → α
g₂ : δ → δ'
hf : h ∘ f = f₁ ∘ f₂
hg : h ∘ g = g₁ ∘ g₂
hfg : range f ∪ range g = univ
s : Set β
⊢ h '' s = h '' (s ∩ range f) ∪ h '' (s ∩ range g)

Tactic:
← image_union,

Goal state after:
α : Type u_5
β : Type u_6
γ : Type u_7
γ' : Type u_8
δ : Type u_9
δ' : Type u_10
h : β → α
f : γ → β
f₁ : γ' → α
f₂ : γ → γ'
g : δ → β
g₁ : δ' → α
g₂ : δ → δ'
hf : h ∘ f = f₁ ∘ f₂
hg : h ∘ g = g₁ ∘ g₂
hfg : range f ∪ range g = univ
s : Set β
⊢ h '' s = h '' (s ∩ range f ∪ s ∩ range g)
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: X : Type u_1
Y : Sort u_2
f : X → Y
s : Set X
x : Pullback f f
⊢ x ∈ toPullbackDiag f '' s ↔ x ∈ pullbackDiagonal f ∩ Subtype.val ⁻¹' s ×ˢ s

Tactic:
constructor

Goal state after:
case mp
X : Type u_1
Y : Sort u_2
f : X → Y
s : Set X
x : Pullback f f
⊢ x ∈ toPullbackDiag f '' s → x ∈ pullbackDiagonal f ∩ Subtype.val ⁻¹' s ×ˢ s

case mpr
X : Type u_1
Y : Sort u_2
f : X → Y
s : Set X
x : Pullback f f
⊢ x ∈ pullbackDiagonal f ∩ Subtype.val ⁻¹' s ×ˢ s → x ∈ toPullbackDiag f '' s
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_5
β : Type u_6
γ : Type u_7
γ' : Type u_8
δ : Type u_9
δ' : Type u_10
h : β → α
f : γ → β
f₁ : γ' → α
f₂ : γ → γ'
g : δ → β
g₁ : δ' → α
g₂ : δ → δ'
hf : h ∘ f = f₁ ∘ f₂
hg : h ∘ g = g₁ ∘ g₂
hfg : range f ∪ range g = univ
s : Set β
⊢ h '' s = h '' (s ∩ (range f ∪ range g))

Tactic:
hfg,

Goal state after:
α : Type u_5
β : Type u_6
γ : Type u_7
γ' : Type u_8
δ : Type u_9
δ' : Type u_10
h : β → α
f : γ → β
f₁ : γ' → α
f₂ : γ → γ'
g : δ → β
g₁ : δ' → α
g₂ : δ → δ'
hf : h ∘ f = f₁ ∘ f₂
hg : h ∘ g = g₁ ∘ g₂
hfg : range f ∪ range g = univ
s : Set β
⊢ h '' s = h '' (s ∩ univ)
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
⊢ (x.1 ∈ s ∨ x.1 ∈ t) ∧ (x.2 ∈ s ∨ x.2 ∈ t) ∧ ¬x.1 = x.2 ↔
    ((x.1 ∈ s ∧ x.2 ∈ s ∧ ¬x.1 = x.2 ∨ x.1 ∈ t ∧ x.2 ∈ t ∧ ¬x.1 = x.2) ∨ x.1 ∈ s ∧ x.2 ∈ t) ∨ x.1 ∈ t ∧ x.2 ∈ s

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
⊢ (x.1 ∈ s ∨ x.1 ∈ t) ∧ (x.2 ∈ s ∨ x.2 ∈ t) ∧ ¬x.1 = x.2 →
    ((x.1 ∈ s ∧ x.2 ∈ s ∧ ¬x.1 = x.2 ∨ x.1 ∈ t ∧ x.2 ∈ t ∧ ¬x.1 = x.2) ∨ x.1 ∈ s ∧ x.2 ∈ t) ∨ x.1 ∈ t ∧ x.2 ∈ s

case mpr
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
⊢ ((x.1 ∈ s ∧ x.2 ∈ s ∧ ¬x.1 = x.2 ∨ x.1 ∈ t ∧ x.2 ∈ t ∧ ¬x.1 = x.2) ∨ x.1 ∈ s ∧ x.2 ∈ t) ∨ x.1 ∈ t ∧ x.2 ∈ s →
    (x.1 ∈ s ∨ x.1 ∈ t) ∧ (x.2 ∈ s ∨ x.2 ∈ t) ∧ ¬x.1 = x.2
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : Unique ι
t : (i : ι) → Set (α i)
⊢ uniqueElim ⁻¹' univ.pi t = t default

Tactic:
ext

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝ : Unique ι
t : (i : ι) → Set (α i)
x✝ : α default
⊢ x✝ ∈ uniqueElim ⁻¹' univ.pi t ↔ x✝ ∈ t default
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: case refine_1
ι : Type u_1
α : ι → Type u_2
p : ι → Prop
h✝ : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
h : f ∈ s.pi fun i ↦ if p i then t₁ i else t₂ i
⊢ f ∈ {i | i ∈ s ∧ p i}.pi t₁ ∩ {i | i ∈ s ∧ ¬p i}.pi t₂

Tactic:
constructor

Goal state after:
case refine_1.left
ι : Type u_1
α : ι → Type u_2
p : ι → Prop
h✝ : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
h : f ∈ s.pi fun i ↦ if p i then t₁ i else t₂ i
⊢ f ∈ {i | i ∈ s ∧ p i}.pi t₁

case refine_1.right
ι : Type u_1
α : ι → Type u_2
p : ι → Prop
h✝ : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
h : f ∈ s.pi fun i ↦ if p i then t₁ i else t₂ i
⊢ f ∈ {i | i ∈ s ∧ ¬p i}.pi t₂
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
s t u : Set α
⊢ val ⁻¹' t ⊆ val ⁻¹' u ↔ s ∩ t ⊆ s ∩ u

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
s t u : Set α
⊢ val ⁻¹' t ⊆ val ⁻¹' u → s ∩ t ⊆ s ∩ u

case mpr
α : Type u_1
s t u : Set α
⊢ s ∩ t ⊆ s ∩ u → val ⁻¹' t ⊆ val ⁻¹' u
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
inst✝ : Decidable (s.pi t).Nonempty
hi : ¬i ∈ s
xᵢ : α i
⊢ (∃ x, (∀ (i : ι), i ∈ s → x i ∈ t i) ∧ x i = xᵢ) ↔ ∃ x, ∀ (i : ι), i ∈ s → x i ∈ t i

Tactic:
constructor

Goal state after:
case mp
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
inst✝ : Decidable (s.pi t).Nonempty
hi : ¬i ∈ s
xᵢ : α i
⊢ (∃ x, (∀ (i : ι), i ∈ s → x i ∈ t i) ∧ x i = xᵢ) → ∃ x, ∀ (i : ι), i ∈ s → x i ∈ t i

case mpr
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
inst✝ : Decidable (s.pi t).Nonempty
hi : ¬i ∈ s
xᵢ : α i
⊢ (∃ x, ∀ (i : ι), i ∈ s → x i ∈ t i) → ∃ x, (∀ (i : ι), i ∈ s → x i ∈ t i) ∧ x i = xᵢ
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
f : α → α
s : Set α
h : MapsTo f s s
n : ℕ
⊢ (restrict f s s h)^[n] = restrict f^[n] s s ⋯

Tactic:
ext

Goal state after:
α : Type u_1
f : α → α
s : Set α
h : MapsTo f s s
n : ℕ
x✝ : ↑s
⊢ ↑((restrict f s s h)^[n] x✝) = ↑(restrict f^[n] s s ⋯ x✝)
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
i : ι
inst✝ : DecidableEq ι
s : Set (α i)
⊢ eval i ⁻¹' s = {i}.pi (update (fun x ↦ univ) i s)

Tactic:
ext

Goal state after:
ι : Type u_1
α : ι → Type u_2
i : ι
inst✝ : DecidableEq ι
s : Set (α i)
x✝ : (x : ι) → α x
⊢ x✝ ∈ eval i ⁻¹' s ↔ x✝ ∈ {i}.pi (update (fun x ↦ univ) i s)
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
f : ι' ≃ ι
s : Set ι'
t : (i : ι) → Set (α i)
⊢ (⇑(piCongrLeft α f).symm ⁻¹' s.pi fun i' ↦ t (f i')) = (⇑f '' s).pi t

Tactic:
ext

Goal state after:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
f : ι' ≃ ι
s : Set ι'
t : (i : ι) → Set (α i)
x✝ : (b : ι) → α b
⊢ (x✝ ∈ ⇑(piCongrLeft α f).symm ⁻¹' s.pi fun i' ↦ t (f i')) ↔ x✝ ∈ (⇑f '' s).pi t
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
π : ι ⊕ ι' → Type u_4
t : (i : ι ⊕ ι') → Set (π i)
⊢ ⇑(sumPiEquivProdPi π).symm ⁻¹' univ.pi t = (univ.pi fun i ↦ t (Sum.inl i)) ×ˢ univ.pi fun i ↦ t (Sum.inr i)

Tactic:
ext

Goal state after:
ι : Type u_1
ι' : Type u_2
π : ι ⊕ ι' → Type u_4
t : (i : ι ⊕ ι') → Set (π i)
x✝ : ((i : ι) → π (Sum.inl i)) × ((i' : ι') → π (Sum.inr i'))
⊢ x✝ ∈ ⇑(sumPiEquivProdPi π).symm ⁻¹' univ.pi t ↔ x✝ ∈ (univ.pi fun i ↦ t (Sum.inl i)) ×ˢ univ.pi fun i ↦ t (Sum.inr i)
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
t : Set α
h : InjOn f s
⊢ f '' s ⊆ f '' (s ∩ t) ∪ f '' (s \ t)

Tactic:
← image_union,

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
t : Set α
h : InjOn f s
⊢ f '' s ⊆ f '' (s ∩ t ∪ s \ t)
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
x✝ : ∃ t' g, t ⊆ t' ∧ Surjective g ∧ ∀ (x : ↑s), f ↑x = ↑(g x)
y : β
hy : y ∈ t
t' : Set β
g : ↑s → ↑t'
htt' : t ⊆ t'
hg : Surjective g
hfg : ∀ (x : ↑s), f ↑x = ↑(g x)
x : ↑s
hx : g x = ⟨y, ⋯⟩
⊢ f ↑x = y

Tactic:
hfg,

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
x✝ : ∃ t' g, t ⊆ t' ∧ Surjective g ∧ ∀ (x : ↑s), f ↑x = ↑(g x)
y : β
hy : y ∈ t
t' : Set β
g : ↑s → ↑t'
htt' : t ⊆ t'
hg : Surjective g
hfg : ∀ (x : ↑s), f ↑x = ↑(g x)
x : ↑s
hx : g x = ⟨y, ⋯⟩
⊢ ↑(g x) = y
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: ι : Type u_1
M : Type u_4
N : Type u_5
F : Type u_9
inst✝³ : Mul M
inst✝² : Mul N
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
f : F
g h : ι → M
⊢ ⇑f ∘ (g * h) = ⇑f ∘ g * ⇑f ∘ h

Tactic:
ext

Goal state after:
ι : Type u_1
M : Type u_4
N : Type u_5
F : Type u_9
inst✝³ : Mul M
inst✝² : Mul N
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
f : F
g h : ι → M
x✝ : ι
⊢ (⇑f ∘ (g * h)) x✝ = (⇑f ∘ g * ⇑f ∘ h) x✝
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: ι : Type u_1
G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : DivInvMonoid G
inst✝¹ : DivInvMonoid H
inst✝ : MulHomClass F G H
f : F
hf : ∀ (a : G), f a⁻¹ = (f a)⁻¹
g h : ι → G
⊢ ⇑f ∘ (g / h) = ⇑f ∘ g / ⇑f ∘ h

Tactic:
ext

Goal state after:
ι : Type u_1
G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : DivInvMonoid G
inst✝¹ : DivInvMonoid H
inst✝ : MulHomClass F G H
f : F
hf : ∀ (a : G), f a⁻¹ = (f a)⁻¹
g h : ι → G
x✝ : ι
⊢ (⇑f ∘ (g / h)) x✝ = (⇑f ∘ g / ⇑f ∘ h) x✝
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: ι : Type u_1
G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : Group G
inst✝¹ : DivisionMonoid H
inst✝ : MonoidHomClass F G H
f : F
g : ι → G
⊢ ⇑f ∘ g⁻¹ = (⇑f ∘ g)⁻¹

Tactic:
ext

Goal state after:
ι : Type u_1
G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : Group G
inst✝¹ : DivisionMonoid H
inst✝ : MonoidHomClass F G H
f : F
g : ι → G
x✝ : ι
⊢ (⇑f ∘ g⁻¹) x✝ = (⇑f ∘ g)⁻¹ x✝
Module: Mathlib.Algebra.Group.Equiv.Defs

Goal state before:
pp: M : Type u_4
N : Type u_5
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
e : M ≃* N
⊢ (↑e).comp ↑e.symm = MonoidHom.id N

Tactic:
ext

Goal state after:
M : Type u_4
N : Type u_5
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
e : M ≃* N
x✝ : N
⊢ ((↑e).comp ↑e.symm) x✝ = (MonoidHom.id N) x✝
Module: Mathlib.Algebra.Group.Equiv.Defs

Goal state before:
pp: M : Type u_4
N : Type u_5
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
e : M ≃* N
⊢ (↑e.symm).comp ↑e = MonoidHom.id M

Tactic:
ext

Goal state after:
M : Type u_4
N : Type u_5
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
e : M ≃* N
x✝ : M
⊢ ((↑e.symm).comp ↑e) x✝ = (MonoidHom.id M) x✝
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: ι : Type u_1
G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : Group G
inst✝¹ : DivisionMonoid H
inst✝ : MonoidHomClass F G H
f : F
g h : ι → G
⊢ ⇑f ∘ (g / h) = ⇑f ∘ g / ⇑f ∘ h

Tactic:
ext

Goal state after:
ι : Type u_1
G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : Group G
inst✝¹ : DivisionMonoid H
inst✝ : MonoidHomClass F G H
f : F
g h : ι → G
x✝ : ι
⊢ (⇑f ∘ (g / h)) x✝ = (⇑f ∘ g / ⇑f ∘ h) x✝
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: ι : Type u_1
G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : Monoid G
inst✝¹ : Monoid H
inst✝ : MonoidHomClass F G H
f : F
g : ι → G
n : ℕ
⊢ ⇑f ∘ (g ^ n) = ⇑f ∘ g ^ n

Tactic:
ext

Goal state after:
ι : Type u_1
G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : Monoid G
inst✝¹ : Monoid H
inst✝ : MonoidHomClass F G H
f : F
g : ι → G
n : ℕ
x✝ : ι
⊢ (⇑f ∘ (g ^ n)) x✝ = (⇑f ∘ g ^ n) x✝
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: ι : Type u_1
G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : DivInvMonoid G
inst✝¹ : DivInvMonoid H
inst✝ : MonoidHomClass F G H
f : F
hf : ∀ (x : G), f x⁻¹ = (f x)⁻¹
g : ι → G
n : ℤ
⊢ ⇑f ∘ (g ^ n) = ⇑f ∘ g ^ n

Tactic:
ext

Goal state after:
ι : Type u_1
G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : DivInvMonoid G
inst✝¹ : DivInvMonoid H
inst✝ : MonoidHomClass F G H
f : F
hf : ∀ (x : G), f x⁻¹ = (f x)⁻¹
g : ι → G
n : ℤ
x✝ : ι
⊢ (⇑f ∘ (g ^ n)) x✝ = (⇑f ∘ g ^ n) x✝
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
f : OneHom N P
⊢ f.comp 1 = 1

Tactic:
ext

Goal state after:
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
f : OneHom N P
x✝ : M
⊢ (f.comp 1) x✝ = 1 x✝
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : MulOne M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
f : N →* P
⊢ f.comp 1 = 1

Tactic:
ext

Goal state after:
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : MulOne M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
f : N →* P
x✝ : M
⊢ (f.comp 1) x✝ = 1 x✝
Module: Mathlib.Data.Set.Function

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

Tactic:
hf.image_inter'

Goal state after:
α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
⊢ f' ⁻¹' s₁ ∩ f '' s = f' ⁻¹' (s₁ ∩ s) ∩ f '' s
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
g : β → α
s : Set α
hgf : LeftInvOn g f s
ginj : InjOn g (g ⁻¹' s)
x : β
⊢ x ∈ f '' s ↔ x ∈ g ⁻¹' s

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
β : Type u_2
f : α → β
g : β → α
s : Set α
hgf : LeftInvOn g f s
ginj : InjOn g (g ⁻¹' s)
x : β
⊢ x ∈ f '' s → x ∈ g ⁻¹' s

case mpr
α : Type u_1
β : Type u_2
f : α → β
g : β → α
s : Set α
hgf : LeftInvOn g f s
ginj : InjOn g (g ⁻¹' s)
x : β
⊢ x ∈ g ⁻¹' s → x ∈ f '' s
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
⊢ SurjOn f s t ↔ ∃ s', s' ⊆ s ∧ BijOn f s' t

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
⊢ SurjOn f s t → ∃ s', s' ⊆ s ∧ BijOn f s' t

case mpr
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
⊢ (∃ s', s' ⊆ s ∧ BijOn f s' t) → SurjOn f s t
Module: Mathlib.Algebra.Group.Hom.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DivisionCommMonoid α
⊢ invMonoidHom.comp invMonoidHom = MonoidHom.id α

Tactic:
ext

Goal state after:
α : Type u_1
inst✝ : DivisionCommMonoid α
x✝ : α
⊢ (invMonoidHom.comp invMonoidHom) x✝ = (MonoidHom.id α) x✝
Module: Mathlib.Algebra.Group.Hom.Basic

Goal state before:
pp: M : Type u_2
N : Type u_3
P : Type u_4
inst✝² : Mul M
inst✝¹ : CommSemigroup N
inst✝ : CommSemigroup P
g : N →ₙ* P
f₁ f₂ : M →ₙ* N
⊢ g.comp (f₁ * f₂) = g.comp f₁ * g.comp f₂

Tactic:
ext

Goal state after:
M : Type u_2
N : Type u_3
P : Type u_4
inst✝² : Mul M
inst✝¹ : CommSemigroup N
inst✝ : CommSemigroup P
g : N →ₙ* P
f₁ f₂ : M →ₙ* N
x✝ : M
⊢ (g.comp (f₁ * f₂)) x✝ = (g.comp f₁ * g.comp f₂) x✝
Module: Mathlib.Algebra.Group.Hom.Basic

Goal state before:
pp: M : Type u_2
N : Type u_3
P : Type u_4
inst✝² : MulOneClass M
inst✝¹ : CommMonoid N
inst✝ : CommMonoid P
g : N →* P
f₁ f₂ : M →* N
⊢ g.comp (f₁ * f₂) = g.comp f₁ * g.comp f₂

Tactic:
ext

Goal state after:
M : Type u_2
N : Type u_3
P : Type u_4
inst✝² : MulOneClass M
inst✝¹ : CommMonoid N
inst✝ : CommMonoid P
g : N →* P
f₁ f₂ : M →* N
x✝ : M
⊢ (g.comp (f₁ * f₂)) x✝ = (g.comp f₁ * g.comp f₂) x✝