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

Goal state before:
pp: case pos
α : Type u
β : Type v
inst✝² : Preorder α
inst✝¹ : Preorder β
f g : α → β
hf : StrictMono f
hg : StrictMono g
p : α → Prop
inst✝ : DecidablePred p
hp : ∀ ⦃x y : α⦄, x < y → p y → p x
hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → f x < g y
x y : α
h : x < y
hy : ¬p y
hx : p x
⊢ (fun x ↦ if p x then f x else g x) x < (fun x ↦ if p x then f x else g x) y

Tactic:
simpa using

Goal state after:
case pos
α : Type u
β : Type v
inst✝² : Preorder α
inst✝¹ : Preorder β
f g : α → β
hf : StrictMono f
hg : StrictMono g
p : α → Prop
inst✝ : DecidablePred p
hp : ∀ ⦃x y : α⦄, x < y → p y → p x
hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → f x < g y
x y : α
h : x < y
hy : ¬p y
hx : p x
⊢ f x < g y
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: case neg
α : Type u
β : Type v
inst✝² : Preorder α
inst✝¹ : Preorder β
f g : α → β
hf : StrictMono f
hg : StrictMono g
p : α → Prop
inst✝ : DecidablePred p
hp : ∀ ⦃x y : α⦄, x < y → p y → p x
hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → f x < g y
x y : α
h : x < y
hy : ¬p y
hx : ¬p x
⊢ (fun x ↦ if p x then f x else g x) x < (fun x ↦ if p x then f x else g x) y

Tactic:
simpa using

Goal state after:
case neg
α : Type u
β : Type v
inst✝² : Preorder α
inst✝¹ : Preorder β
f g : α → β
hf : StrictMono f
hg : StrictMono g
p : α → Prop
inst✝ : DecidablePred p
hp : ∀ ⦃x y : α⦄, x < y → p y → p x
hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → f x < g y
x y : α
h : x < y
hy : ¬p y
hx : ¬p x
⊢ g x < g y
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: α : Type u
inst✝ : Preorder α
f : ℤ → α
hf : Antitone f
n : ℤ
x : α
h1 : f (n + 1) < x
h2 : x < f n
a : ℤ
⊢ f a ≠ x

Tactic:
by
  rintro rfl
  exact (hf.reflect_lt h2).not_ge (Int.le_of_lt_add_one <| hf.reflect_lt h1)

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

Goal state before:
pp: α : Type u
s : Set α
inst✝ : IsEmpty ↑s
⊢ s = ∅

Tactic:
simpa using

Goal state after:
α : Type u
s : Set α
inst✝ : IsEmpty ↑s
⊢ s = ∅
Module: Mathlib.Data.Set.Basic

Goal state before:
pp: α : Type u_1
s✝ t u : Set α
p : α → Prop
s : Set { a // p a }
a : { a // p a }
⊢ a ∈ (fun s ↦ {a | ↑a ∈ ↑s}) ((fun s ↦ ⟨{a | ∃ h, ⟨a, h⟩ ∈ s}, ⋯⟩) s) ↔ a ∈ s

Tactic:
exact ⟨fun h ↦ h.2, fun h ↦ ⟨a.property, h⟩⟩

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

Goal state before:
pp: α : Type u_1
l : List α
a : α
⊢ {x | x ∈ l} = {a} ↔ ∃ n, n > 0 ∧ l = List.replicate n a

Tactic:
simpa using

Goal state after:
α : Type u_1
l : List α
a : α
⊢ ((∀ (x : α), x ∈ l → x = a) → a ∈ l → ∃ x, x ∈ l) ∧ ∀ (x : α), x ∈ l → (∀ (x : α), x ∈ l → x = a) → a ∈ l
Module: Mathlib.Data.Set.Insert

Goal state before:
pp: p q : Prop
⊢ q ∈ {p}ᶜ ↔ q ∈ {¬p}

Tactic:
simpa using

Goal state after:
p q : Prop
⊢ ¬(p ↔ q) ↔ (¬p ↔ q)
Module: Mathlib.Order.Lattice

Goal state before:
pp: case refine_1
α : Type u
inst✝ : Lattice α
a c : α
h : a ⊓ a = c ∧ a ⊔ a = c
⊢ a = c ∧ a = c

Tactic:
simpa using

Goal state after:
case refine_1
α : Type u
inst✝ : Lattice α
a c : α
h : a ⊓ a = c ∧ a ⊔ a = c
⊢ a = c
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : Max α
inst✝² : LE α
inst✝¹ : LT α
inst✝ : SemilatticeSup β
f : α → β
hf_inj : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
a b : α
⊢ b ≤ a ⊔ b

Tactic:
rw [← le, map_sup]
    exact le_sup_right

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝¹ : LinearOrder α
p : α → α → Prop
inst✝ : Std.Symm p
⊢ Pairwise p ↔ ∀ ⦃a b : α⦄, a < b → p a b

Tactic:
simpa using

Goal state after:
α : Type u
inst✝¹ : LinearOrder α
p : α → α → Prop
inst✝ : Std.Symm p
⊢ (∀ (x x_1 : α), x < x_1 → p x x_1) → ∀ (x x_1 : α), x_1 < x → p x x_1
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝¹ : LinearOrder α
p : α → α → Prop
inst✝ : Std.Symm p
⊢ Pairwise p ↔ ∀ ⦃a b : α⦄, b < a → p a b

Tactic:
simpa using

Goal state after:
α : Type u
inst✝¹ : LinearOrder α
p : α → α → Prop
inst✝ : Std.Symm p
⊢ (∀ (x x_1 : α), x_1 < x → p x x_1) → ∀ (x x_1 : α), x < x_1 → p x x_1
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c : α
⊢ a ≤ b ⇨ c ↔ b ⊓ a ≤ c

Tactic:
le_himp_iff,

Goal state after:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c : α
⊢ a ⊓ b ≤ c ↔ b ⊓ a ≤ c
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c : α
⊢ a ≤ b ⇨ c ↔ b ≤ a ⇨ c

Tactic:
le_himp_iff,

Goal state after:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c : α
⊢ a ⊓ b ≤ c ↔ b ≤ a ⇨ c
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
⊢ a ≤ a ⇨ b ↔ a ≤ b

Tactic:
le_himp_iff,

Goal state after:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
⊢ a ⊓ a ≤ b ↔ a ≤ b
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
⊢ ⊤ ≤ a ⇨ b ↔ a ≤ b

Tactic:
le_himp_iff,

Goal state after:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
⊢ ⊤ ⊓ a ≤ b ↔ a ≤ b
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
⊢ b ≤ ⊤ ⇨ a ↔ b ≤ a

Tactic:
le_himp_iff,

Goal state after:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
⊢ b ⊓ ⊤ ≤ a ↔ b ≤ a
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
⊢ d ≤ a ⇨ b ⇨ c ↔ d ≤ a ⊓ b ⇨ c

Tactic:
le_himp_iff,

Goal state after:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
⊢ d ⊓ a ⊓ b ≤ c ↔ d ⊓ (a ⊓ b) ≤ c
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c : α
⊢ b ⇨ c ≤ (a ⇨ b) ⇨ a ⇨ c

Tactic:
le_himp_iff,

Goal state after:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c : α
⊢ (b ⇨ c) ⊓ (a ⇨ b) ≤ a ⇨ c
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c : α
⊢ (b ⇨ c) ⊓ (a ⇨ b) ≤ a ⇨ c

Tactic:
le_himp_iff,

Goal state after:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c : α
⊢ (b ⇨ c) ⊓ (a ⇨ b) ⊓ a ≤ c
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c : α
⊢ (b ⇨ c) ⊓ (a ⇨ b) ⊓ a ≤ c

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c : α
⊢ (b ⇨ c) ⊓ (a ⇨ b) ⊓ a ≤ c
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
⊢ d ≤ a ⇨ b ⊓ c ↔ d ≤ (a ⇨ b) ⊓ (a ⇨ c)

Tactic:
le_himp_iff,

Goal state after:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
⊢ d ⊓ a ≤ b ⊓ c ↔ d ≤ (a ⇨ b) ⊓ (a ⇨ c)
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c : α
⊢ (a ⇨ b) ⊓ (b ⇨ c) ≤ a ⇨ c

Tactic:
le_himp_iff,

Goal state after:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c : α
⊢ (a ⇨ b) ⊓ (b ⇨ c) ⊓ a ≤ c
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedHeytingAlgebra α
a✝ b✝ c✝ d a b c : α
⊢ b ≤ a ⇨ b ⊓ a ⊔ c ⊓ a ∧ c ≤ a ⇨ b ⊓ a ⊔ c ⊓ a

Tactic:
le_himp_iff,

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedHeytingAlgebra α
a✝ b✝ c✝ d a b c : α
⊢ b ⊓ a ≤ b ⊓ a ⊔ c ⊓ a ∧ c ⊓ a ≤ b ⊓ a ⊔ c ⊓ a
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
⊢ a ≤ b ⊔ (a \ c ⊔ c \ b)

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
⊢ a ≤ b ⊔ (a \ c ⊔ c \ b)
Module: Mathlib.Control.EquivFunctor

Goal state before:
pp: f : Type u₀ → Type u₁
inst✝¹ : Applicative f
inst✝ : LawfulApplicative f
α β : Type u₀
h : ∀ (γ : Type u₀), Injective pure
e₁ e₂ : α ≃ β
H : mapEquiv f e₁ = mapEquiv f e₂
x : α
⊢ pure (e₁ x) = pure (e₂ x)

Tactic:
simpa using

Goal state after:
f : Type u₀ → Type u₁
inst✝¹ : Applicative f
inst✝ : LawfulApplicative f
α β : Type u₀
h : ∀ (γ : Type u₀), Injective pure
e₁ e₂ : α ≃ β
H : mapEquiv f e₁ = mapEquiv f e₂
x : α
⊢ pure (e₁ x) = pure (e₂ x)
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ a ≤ b ⇨ ⊥ ↔ Disjoint a b

Tactic:
le_himp_iff,

Goal state after:
α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ a ⊓ b ≤ ⊥ ↔ Disjoint a b
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ Disjoint aᶜᶜ (bᶜᶜ ⊓ (a ⊓ b)ᶜ)

Tactic:
disjoint_compl_compl_left_iff,

Goal state after:
α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ Disjoint a (bᶜᶜ ⊓ (a ⊓ b)ᶜ)
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ Disjoint bᶜᶜ (a ⊓ (a ⊓ b)ᶜ)

Tactic:
disjoint_compl_compl_left_iff,

Goal state after:
α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ Disjoint b (a ⊓ (a ⊓ b)ᶜ)
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: case a
α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ (a ⇨ b)ᶜᶜ ≤ aᶜᶜ ⇨ bᶜᶜ

Tactic:
le_himp_iff,

Goal state after:
case a
α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ (a ⇨ b)ᶜᶜ ⊓ aᶜᶜ ≤ bᶜᶜ
Module: Mathlib.Logic.Equiv.Option

Goal state before:
pp: α : Type u_1
β : Type u_2
e : Option α ≃ Option β
h : e.symm none = none
⊢ e none = none

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
h : e.symm none = none
⊢ e none = none
Module: Mathlib.Logic.Equiv.Option

Goal state before:
pp: α : Type u_1
β : Type u_2
e : Option α ≃ Option β
h : e none = none
⊢ e.symm none = none

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
h : e none = none
⊢ e.symm none = none
Module: Mathlib.Logic.Equiv.Option

Goal state before:
pp: case none
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
h : e (some x) = none
⊢ e none = e none ↔ e.symm none = some x

Tactic:
simpa using

Goal state after:
case none
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
h : e (some x) = none
⊢ e.symm none = some x
Module: Mathlib.Logic.Equiv.Option

Goal state before:
pp: case none
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
x : β
e : { e // e none = x }
⊢ ↑((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))
      none =
    ↑e none

Tactic:
simpa using

Goal state after:
case none
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
x : β
e : { e // e none = x }
⊢ x = ↑e none
Module: Mathlib.Data.Sigma.Basic

Goal state before:
pp: α : Type u_1
β : α → Type u_4
γ : Type u_7
inst✝ : Nonempty γ
a : α
f : γ → β a
i : γ
g : γ → β a
h : mk a ∘ f = mk a ∘ g
⊢ a = a ∧ f ≍ g

Tactic:
simpa using

Goal state after:
α : Type u_1
β : α → Type u_4
γ : Type u_7
inst✝ : Nonempty γ
a : α
f : γ → β a
i : γ
g : γ → β a
h : mk a ∘ f = mk a ∘ g
⊢ ∀ (x : γ), f x = g x
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
h : y ≤ x
⊢ x \ (x \ y) = y

Tactic:
by
  rw [sdiff_sdiff_right_self, inf_of_le_right h]

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

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

Tactic:
simpa using

Goal state after:
α : Type u
x y : α
inst✝ : BooleanAlgebra α
h✝ : yᶜ ≤ xᶜ
h : xᶜᶜ ≤ yᶜᶜ
⊢ x ≤ y
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
simpa using

Goal state after:
α : Type u
x y : α
inst✝ : BooleanAlgebra α
h : yᶜ ≤ x
⊢ xᶜ ≤ y
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x : α
inst✝ : BooleanAlgebra α
⊢ xᶜ ≤ x ↔ x = ⊤

Tactic:
simpa using

Goal state after:
α : Type u
x : α
inst✝ : BooleanAlgebra α
⊢ xᶜ ≤ x ↔ x = ⊤
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x : α
inst✝¹ : BooleanAlgebra α
inst✝ : Nontrivial α
⊢ xᶜ < x ↔ x = ⊤

Tactic:
simpa using

Goal state after:
α : Type u
x : α
inst✝¹ : BooleanAlgebra α
inst✝ : Nontrivial α
⊢ xᶜ < x ↔ x = ⊤
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
β : α → Sort v
p : (a : α) → β a → Prop
⊢ LeftInverse (fun f ↦ ⟨fun a ↦ ↑(f a), ⋯⟩) fun f a ↦ ⟨↑f a, ⋯⟩

Tactic:
rintro ⟨f, h⟩
    rfl

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
by
  convert! symmDiff_triangle a b ⊥ <;> rw [symmDiff_bot]

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

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

Tactic:
by
  induction n with
  | zero => simp
  | succ n ih => rw [iterate_succ', iterate_succ', ← ih, image_comp_eq]

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

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

Tactic:
delta Set.restrictPreimage
  rw [← (Subtype.coe_injective).image_injective.eq_iff, ← image_comp, MapsTo.restrict_commutes,
    image_comp, Subtype.image_preimage_coe, Subtype.image_preimage_coe, image_preimage_inter]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
h' : Surjective (restrict f s t h)
b : β
hb : b ∈ t
a : α
ha : a ∈ s
ha' : restrict f s t h ⟨a, ha⟩ = ⟨b, hb⟩
⊢ f a = b

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
h' : Surjective (restrict f s t h)
b : β
hb : b ∈ t
a : α
ha : a ∈ s
ha' : restrict f s t h ⟨a, ha⟩ = ⟨b, hb⟩
⊢ f a = b
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 = ∅

Tactic:
exact h.ne_empty

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s s₁ s₂ : Set α
t t₁ t₂ : Set β
f₁ f₂ : α → β
inst✝ : (i : α) → Decidable (i ∈ s)
h₁ : MapsTo f₁ (s₁ ∩ s) (t₁ ∩ t)
h₂ : MapsTo f₂ (s₂ ∩ sᶜ) (t₂ ∩ tᶜ)
⊢ MapsTo (s.piecewise f₁ f₂) (s.ite s₁ s₂) (t.ite t₁ t₂)

Tactic:
refine (h₁.congr ?_).union_union (h₂.congr ?_)
  exacts [(piecewise_eqOn s f₁ f₂).symm.mono inter_subset_right,
    (piecewise_eqOn_compl s f₁ f₂).symm.mono inter_subset_right]

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
ht : t ⊆ range f
h : f ⁻¹' s = f ⁻¹' t
⊢ s = t

Tactic:
apply Subset.antisymm

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

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

Goal state before:
pp: X : Type u_2
Y : Sort u_3
Z : Type u_1
f : X → Y
g : Z → Y
p₁ p₂ : Pullback f g
he : (p₁, p₂).1.snd = (p₁, p₂).2.snd
⊢ ⟨(p₁, p₂), he⟩ ∈ map_fst ⁻¹' pullbackDiagonal f ↔ ⟨(p₁, p₂), he⟩ ∈ pullbackDiagonal snd

Tactic:
simp_rw [pullbackDiagonal, mem_ofPred, Subtype.ext_iff, Prod.ext_iff]

Goal state after:
X : Type u_2
Y : Sort u_3
Z : Type u_1
f : X → Y
g : Z → Y
p₁ p₂ : Pullback f g
he : (p₁, p₂).1.snd = (p₁, p₂).2.snd
⊢ ⟨(p₁, p₂), he⟩ ∈ map_fst ⁻¹' {p | p.fst = p.snd} ↔
    (↑(fst ⟨(p₁, p₂), he⟩)).1 = (↑(snd ⟨(p₁, p₂), he⟩)).1 ∧ (↑(fst ⟨(p₁, p₂), he⟩)).2 = (↑(snd ⟨(p₁, p₂), he⟩)).2
Module: Mathlib.Algebra.Group.Action.Pi

Goal state before:
pp: ι : Type u_1
M : Type u_2
α : ι → Type u_4
inst✝² : (i : ι) → SMul M (α i)
inst✝¹ : ∀ (i : ι), Nonempty (α i)
i : ι
inst✝ : FaithfulSMul M (α i)
m₁✝ m₂✝ : M
h : ∀ (a : (i : ι) → α i), m₁✝ • a = m₂✝ • a
a : α i
⊢ m₁✝ • a = m₂✝ • a

Tactic:
simpa using

Goal state after:
ι : Type u_1
M : Type u_2
α : ι → Type u_4
inst✝² : (i : ι) → SMul M (α i)
inst✝¹ : ∀ (i : ι), Nonempty (α i)
i : ι
inst✝ : FaithfulSMul M (α i)
m₁✝ m₂✝ : M
h : ∀ (a : (i : ι) → α i), m₁✝ • a = m₂✝ • a
a : α i
⊢ m₁✝ • a = m₂✝ • a
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: 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
i : ι
his : i ∈ s
hpi : p i
⊢ f i ∈ t₁ i

Tactic:
simpa using

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
i : ι
his : i ∈ s
hpi : p i
⊢ f i ∈ t₁ i
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: 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
i : ι
his : i ∈ s
hpi : ¬p i
⊢ f i ∈ t₂ i

Tactic:
simpa using

Goal state after:
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
i : ι
his : i ∈ s
hpi : ¬p i
⊢ f i ∈ t₂ i
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
s : Set α
t : Set ↑s
x : α
x✝ : x ∈ val '' t
y : { x // x ∈ s }
left✝ : y ∈ t
yvaleq : ↑y = x
⊢ ↑y ∈ s

Tactic:
exact y.property

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
h : Disjoint s (range f)
⊢ f ⁻¹' s = ∅

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
h : Disjoint s (range f)
⊢ f ⁻¹' s = ∅
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : 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✝)

Tactic:
simpa using

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
x : α
⊢ MapsTo f (Insert.insert x s) (Insert.insert (f x) t)

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
x : α
⊢ MapsTo f s ({f x} ∪ t)
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
h : s.pi t₁ ⊆ s.pi t₂
hne : (s.pi t₁).Nonempty
i : ι
hi : i ∈ s
⊢ t₁ i ⊆ t₂ i

Tactic:
simpa using

Goal state after:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
h : s.pi t₁ ⊆ s.pi t₂
hne : (s.pi t₁).Nonempty
i : ι
hi : i ∈ s
⊢ t₁ i ⊆ t₂ i
Module: Mathlib.Data.Set.Prod

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

Tactic:
simpa using

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

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

Tactic:
simpa using

Goal state after:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
f : ι' ≃ ι
t : (i : ι) → Set (α i)
⊢ ⇑(piCongrLeft α f) ⁻¹' univ.pi t = univ.pi fun i ↦ t (f i)
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : InjOn f s
x✝¹ x✝ : ↑s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
h' : imageFactorization f s ⟨x, hx⟩ = imageFactorization f s ⟨y, hy⟩
⊢ ⟨x, hx⟩ = ⟨y, hy⟩

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : InjOn f s
x✝¹ x✝ : ↑s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
h' : imageFactorization f s ⟨x, hx⟩ = imageFactorization f s ⟨y, hy⟩
⊢ x = y
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : Injective (imageFactorization f s)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
x✝ : f x = f y
⊢ x = y

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : Injective (imageFactorization f s)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
x✝ : f x = f y
⊢ x = y
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: β : Type u_2
γ : Type u_3
s : Set (β × γ)
hs₁ : Bijective (Prod.fst ∘ Subtype.val)
⊢ ∃ f, s = graphOn f univ

Tactic:
simpa using

Goal state after:
β : Type u_2
γ : Type u_3
s : Set (β × γ)
hs₁ : Bijective (Prod.fst ∘ Subtype.val)
⊢ ∃ f, s = graphOn f univ
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : BijOn f s ∅
⊢ s = ∅

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : BijOn f s ∅
⊢ s = ∅
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
⊢ s = ∅ → BijOn f s ∅

Tactic:
by rintro rfl; exact bijOn_empty f

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

Goal state before:
pp: α : Type u_1
β : Type u_2
t : Set β
f : α → β
h : BijOn f ∅ t
⊢ t = ∅

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
t : Set β
f : α → β
h : BijOn f ∅ t
⊢ t = ∅
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
t : Set β
f : α → β
⊢ t = ∅ → BijOn f ∅ t

Tactic:
by rintro rfl; exact bijOn_empty f

Goal state after:
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: M : Type u_4
N : Type u_5
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : IsMulTorsionFree N
f : M →* N
hf : Injective ⇑f
n : ℕ
hn : n ≠ 0
x y : M
hxy : (fun a ↦ a ^ n) x = (fun a ↦ a ^ n) y
⊢ (fun a ↦ a ^ n) (f x) = (fun a ↦ a ^ n) (f y)

Tactic:
simpa using

Goal state after:
M : Type u_4
N : Type u_5
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : IsMulTorsionFree N
f : M →* N
hf : Injective ⇑f
n : ℕ
hn : n ≠ 0
x y : M
hxy : (fun a ↦ a ^ n) x = (fun a ↦ a ^ n) y
⊢ f x ^ n = f y ^ n
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: M : Type u_4
N : Type u_5
F : Type u_9
inst✝⁴ : MulOne M
inst✝³ : MulOne N
inst✝² : FunLike F M N
inst✝¹ : MonoidHomClass F M N
f : F
hf : Injective ⇑f
inst✝ : IsDedekindFiniteMonoid N
a✝ b✝ : M
eq : a✝ * b✝ = 1
⊢ f (b✝ * a✝) = f 1

Tactic:
simpa using

Goal state after:
M : Type u_4
N : Type u_5
F : Type u_9
inst✝⁴ : MulOne M
inst✝³ : MulOne N
inst✝² : FunLike F M N
inst✝¹ : MonoidHomClass F M N
f : F
hf : Injective ⇑f
inst✝ : IsDedekindFiniteMonoid N
a✝ b✝ : M
eq : a✝ * b✝ = 1
⊢ f a✝ * f b✝ = 1
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
M✝ : Type u_4
N✝ : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
F : Type u_9
inst✝⁵ : MulOne M✝
inst✝⁴ : MulOne N✝
inst✝³ : FunLike F M✝ N✝
inst✝² : MonoidHomClass F M✝ N✝
M : Type u_10
N : Type u_11
inst✝¹ : Monoid M
inst✝ : LeftCancelMonoid N
f : M →ₙ* N
⊢ f 1 * 1 = f 1 * f 1

Tactic:
simpa using

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
M✝ : Type u_4
N✝ : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
F : Type u_9
inst✝⁵ : MulOne M✝
inst✝⁴ : MulOne N✝
inst✝³ : FunLike F M✝ N✝
inst✝² : MonoidHomClass F M✝ N✝
M : Type u_10
N : Type u_11
inst✝¹ : Monoid M
inst✝ : LeftCancelMonoid N
f : M →ₙ* N
⊢ f 1 = f 1 * f 1