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

Goal state before:
pp: α : Sort u_1
b c : α
h : b = c
a : α
⊢ a = b ↔ a = c

Tactic:
by rw [h]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
a b : α
h : ∀ {c : α}, a = c ↔ b = c
⊢ a = b

Tactic:
by rw [h]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
a✝ b : α
h : a✝ = b
a : α
⊢ a✝ = a ↔ b = a

Tactic:
by rw [h]

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
f : α → β
γ : Type u_4
inst✝ : Nontrivial γ
⊢ (Injective fun g ↦ g ∘ f) ↔ Surjective f

Tactic:
by
  refine ⟨not_imp_not.mp fun not_surj inj ↦ not_subsingleton γ ⟨fun c c' ↦ ?_⟩,
    (·.injective_comp_right)⟩
  have ⟨b₀, hb⟩ := not_forall.mp not_surj
  classical have := inj (a₁ := fun _ ↦ c) (a₂ := (if · = b₀ then c' else c)) ?_
  · simpa using congr_fun this b₀
  ext a; simp only [comp_apply, if_neg fun h ↦ hb ⟨a, h⟩]

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

Goal state before:
pp: case neg.hb
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
a : α₃
h₃ : ¬∃ b, f₂₃ b = a
⊢ ¬∃ a_1, (f₂₃ ∘ f₁₂) a_1 = a

Tactic:
exact fun h ↦ h₃ (Exists.casesOn h fun c hc ↦ Exists.intro (f₁₂ c) (hc))

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
γ : β → Sort v
f : α → β
g : β → α
h : LeftInverse g f
C : (a : α) → γ (f a)
a : α
⊢ C (g (f a)) ≍ C a

Tactic:
by rw [h]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
r : α → α → Prop
a b c : α
inst✝ : Std.Symm r
x y : α
h : TransGen r x y
⊢ TransGen r y x

Tactic:
by
    induction h with
    | single i => exact .single <| symm i
    | tail _ h₁ h₂ => exact .head (symm h₁) h₂

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r r' : α → α → Prop
inst✝ : IsTrans α r'
h : r ≤ r'
⊢ TransGen r ≤ r'

Tactic:
by
  simpa [transGen_eq_self] using TransGen.mono h

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ ReflTransGen (TransGen r) = ReflTransGen r

Tactic:
simp only [← reflGen_transGen, transGen_eq_self]

Goal state after:
Module: Mathlib.Logic.Function.Conjugate

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
ga ga' : α → α
gb gb' : β → β
h : Semiconj f ga gb
ha : RightInverse ga' ga
hb : LeftInverse gb' gb
x : α
⊢ f (ga' x) = gb' (f x)

Tactic:
rw [← hb (f (ga' x)), ← h.eq, ha x]

Goal state after:
Module: Mathlib.Logic.Function.Iterate

Goal state before:
pp: α : Type u
f : α → α
m n : ℕ
x : α
⊢ f^[m + n] x = f^[m] (f^[n] x)

Tactic:
rw [iterate_add f m n]

Goal state after:
α : Type u
f : α → α
m n : ℕ
x : α
⊢ (f^[m] ∘ f^[n]) x = f^[m] (f^[n] x)
Module: Mathlib.Logic.Function.Iterate

Goal state before:
pp: α : Type u
f : α → α
m n : ℕ
⊢ f^[m * (n + 1)] = f^[m]^[n + 1]

Tactic:
simp only [Nat.mul_succ, iterate_one, iterate_add, iterate_mul m n]

Goal state after:
Module: Mathlib.Algebra.Group.Pi.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
a a' : α → γ
b b' : β → γ
inst✝ : Mul γ
⊢ Sum.elim (a * a') (b * b') = Sum.elim a b * Sum.elim a' b'

Tactic:
ext x

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
a a' : α → γ
b b' : β → γ
inst✝ : Mul γ
x : α ⊕ β
⊢ Sum.elim (a * a') (b * b') x = (Sum.elim a b * Sum.elim a' b') x
Module: Mathlib.Algebra.Group.Pi.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
a a' : α → γ
b b' : β → γ
inst✝ : Div γ
⊢ Sum.elim (a / a') (b / b') = Sum.elim a b / Sum.elim a' b'

Tactic:
ext x

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
a a' : α → γ
b b' : β → γ
inst✝ : Div γ
x : α ⊕ β
⊢ Sum.elim (a / a') (b / b') x = (Sum.elim a b / Sum.elim a' b') x
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: case neg
α : Type u_1
inst✝ : LinearOrder α
a b : α
h1 : ¬(fun x1 x2 ↦ x1 < x2) a b
h2 : ¬(fun x1 x2 ↦ x1 < x2) b a
⊢ Ordering.eq.Compares a b

Tactic:
· exact le_antisymm (not_lt.1 h2) (not_lt.1 h1)

Goal state after:
Module: Mathlib.Lean.Meta.CongrTheorems

Goal state before:
pp: α β : Sort u
inst✝ : FastSubsingleton α
h₂ : α = β
a : α
b : β
this : Subsingleton α
⊢ a ≍ b

Tactic:
exact Subsingleton.helim h₂ a b

Goal state after:
Module: Mathlib.Logic.Function.ULift

Goal state before:
pp: α : Type u_1
a b : ULift α
h : a = b
⊢ a.down = b.down

Tactic:
by rw [h]

Goal state after:
Module: Mathlib.Logic.Function.ULift

Goal state before:
pp: α : Sort u_1
a b : PLift α
h : a = b
⊢ a.down = b.down

Tactic:
by rw [h]

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : DenselyOrdered α
inst✝ : DenselyOrdered β
a b : α × β
⊢ a < b → ∃ a_2, a < a_2 ∧ a_2 < b

Tactic:
Prod.lt_iff

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : DenselyOrdered α
inst✝ : DenselyOrdered β
a b : α × β
⊢ a.fst < b.fst ∧ a.snd ≤ b.snd ∨ a.fst ≤ b.fst ∧ a.snd < b.snd →
    ∃ a_2,
      (a.fst < a_2.fst ∧ a.snd ≤ a_2.snd ∨ a.fst ≤ a_2.fst ∧ a.snd < a_2.snd) ∧
        (a_2.fst < b.fst ∧ a_2.snd ≤ b.snd ∨ a_2.fst ≤ b.fst ∧ a_2.snd < b.snd)
Module: Mathlib.Data.Nat.Init

Goal state before:
pp: case of_succ
a b c d e m n k✝ : ℕ
p : ℕ → Prop
P : ℕ → Sort u_1
hP : P n
k : ℕ
hk : k < n
ih : ((k_1 : ℕ) → k_1 < n → k + 1 ≤ k_1 → P (k_1 + 1) → P k_1) → P (k + 1)
h : (k_1 : ℕ) → k_1 < n → k ≤ k_1 → P (k_1 + 1) → P k_1
⊢ P k

Tactic:
| of_succ k hk ih =>

Goal state after:
Module: Mathlib.Data.Nat.Init

Goal state before:
pp: m n✝ : ℕ
h : m = n✝
n : ℕ
⊢ m ∣ n ↔ n✝ ∣ n

Tactic:
by rw [h]

Goal state after:
Module: Mathlib.Data.Nat.Init

Goal state before:
pp: m n✝ : ℕ
h : m = n✝
n : ℕ
⊢ n ∣ m ↔ n ∣ n✝

Tactic:
by rw [h]

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

Goal state before:
pp: case refine_1
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a c : α
h : f a < f a ∧ f c < f a ∨ f a < f a ∧ f a < f c
⊢ False

Tactic:
simp at h

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

Goal state before:
pp: case refine_2
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b : α
h : f a < f b ∧ f b < f b ∨ f b < f a ∧ f b < f b
⊢ False

Tactic:
simp at h

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

Goal state before:
pp: case zero
β : Type v
r : β → β → Prop
inst✝ : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a : ℤ
⊢ r (f a) (f (a + ↑(Nat.succ 0)))

Tactic:
rw [Int.ofNat_one]; apply h

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
⊢ RightInverse (fun y ↦ y.elim ⟨x, ⋯⟩ fun z ↦ ⟨↑z, ⋯⟩) fun y ↦ if h : ↑y = x then none else some ⟨↑y, ⋯⟩

Tactic:
by rintro (_ | y) <;> grind

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝ : DistribLattice α
a b c : α
⊢ (a ⊔ b) ⊓ c = a ⊓ c ⊔ b ⊓ c

Tactic:
simp only [inf_sup_left, inf_comm _ c]

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

Goal state before:
pp: α : Type u
s : Set α
p : Set α → Prop
hs : s.Subsingleton
he : p ∅
h₁ : ∀ (x : α), p {x}
⊢ p s

Tactic:
rcases hs.eq_empty_or_singleton with (rfl | ⟨x, rfl⟩)

Goal state after:
case inl
α : Type u
p : Set α → Prop
he : p ∅
h₁ : ∀ (x : α), p {x}
hs : ∅.Subsingleton
⊢ p ∅

case inr
α : Type u
p : Set α → Prop
he : p ∅
h₁ : ∀ (x : α), p {x}
x : α
hs : {x}.Subsingleton
⊢ p {x}
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeSup β
⊢ SemilatticeSup α

Tactic:
let max := e.max
  let partialOrder := e.partialOrder
  apply e.injective.semilatticeSup <;> intros <;> first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Control.EquivFunctor

Goal state before:
pp: f : Type u₀ → Type u₁
inst✝¹ : Functor f
inst✝ : LawfulFunctor f
α β γ : Type u₀
k : α ≃ β
h : β ≃ γ
⊢ Functor.map ⇑(k.trans h) = Functor.map ⇑h ∘ Functor.map ⇑k

Tactic:
ext x

Goal state after:
f : Type u₀ → Type u₁
inst✝¹ : Functor f
inst✝ : LawfulFunctor f
α β γ : Type u₀
k : α ≃ β
h : β ≃ γ
x : f α
⊢ ⇑(k.trans h) <$> x = (Functor.map ⇑h ∘ Functor.map ⇑k) x
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: case refl
α : Type u_2
inst✝¹ : HeytingAlgebra α
inst✝ : Nontrivial α
h : ⊥ = ⊥ᶜ
⊢ False

Tactic:
simp at h

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

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

Tactic:
ext x

Goal state after:
α : Type u_1
s : Set α
a : α
h : ¬a ∈ s
x : α
⊢ x ∈ insert a s \ {a} ↔ x ∈ s
Module: Mathlib.Order.BooleanAlgebra.Set

Goal state before:
pp: α : Type u_1
t s₁ s₂ s₁' s₂' : Set α
⊢ t.ite (s₁ ∩ s₂) (s₁' ∩ s₂') = t.ite s₁ s₁' ∩ t.ite s₂ s₂'

Tactic:
ext x

Goal state after:
α : Type u_1
t s₁ s₂ s₁' s₂' : Set α
x : α
⊢ x ∈ t.ite (s₁ ∩ s₂) (s₁' ∩ s₂') ↔ x ∈ t.ite s₁ s₁' ∩ t.ite s₂ s₂'
Module: Mathlib.Order.BooleanAlgebra.Set

Goal state before:
pp: α : Type u_1
t s₁ s₂ : Set α
h : s₁ ⊆ s₂
⊢ t.ite s₁ s₂ = s₁ ∪ s₂ \ t

Tactic:
ext x

Goal state after:
α : Type u_1
t s₁ s₂ : Set α
h : s₁ ⊆ s₂
x : α
⊢ x ∈ t.ite s₁ s₂ ↔ x ∈ s₁ ∪ s₂ \ t
Module: Mathlib.Order.BooleanAlgebra.Set

Goal state before:
pp: α : Type u_1
t s₁ s₂ : Set α
h : s₂ ⊆ s₁
⊢ t.ite s₁ s₂ = s₁ ∩ t ∪ s₂

Tactic:
ext x

Goal state after:
α : Type u_1
t s₁ s₂ : Set α
h : s₂ ⊆ s₁
x : α
⊢ x ∈ t.ite s₁ s₂ ↔ x ∈ s₁ ∩ t ∪ s₂
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ y \ z ⊔ (z ⊓ x ⊔ x \ y) = (x ⊔ (z ⊓ x ⊔ x \ y)) ⊓ (y \ z ⊔ (z ⊓ x ⊔ x \ y))

Tactic:
by
          rw [sup_inf_right]

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ ((y \ z ⊔ x) ⊓ (y \ z ⊔ z) ⊔ x \ y) = x ⊓ (y \ z ⊔ (x ⊓ z ⊔ x ⊓ y) ⊔ x \ y)

Tactic:
sdiff_sup_self',

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ ((y \ z ⊔ x) ⊓ (y ⊔ z) ⊔ x \ y) = x ⊓ (y \ z ⊔ (x ⊓ z ⊔ x ⊓ y) ⊔ x \ y)
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (y ⊓ (x ⊓ (x ⊔ z)) ⊔ x \ z) ⊓ (x ⊓ y ⊓ z ⊔ y \ z) = x ⊓ y ⊔ x \ z ⊓ y \ z

Tactic:
by rw [inf_sup_self, sup_inf_inf_sdiff, inf_comm y, sup_inf_left]

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

Goal state before:
pp: ε : Type u_9
p : ε → Prop
inst✝ : DecidablePred p
⊢ subtypeCongr (Equiv.refl { a // p a }) (Equiv.refl { a // ¬p a }) = Equiv.refl ε

Tactic:
ext x

Goal state after:
ε : Type u_9
p : ε → Prop
inst✝ : DecidablePred p
x : ε
⊢ (subtypeCongr (Equiv.refl { a // p a }) (Equiv.refl { a // ¬p a })) x = (Equiv.refl ε) x
Module: Mathlib.Order.SymmDiff

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

Tactic:
rw [sup_assoc]
    exact le_sup_of_le_right le_sdiff_sup

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

Goal state before:
pp: α' : Type u_9
β' : Type u_10
p : β' → Prop
inst✝ : DecidablePred p
f : α' ≃ Subtype p
e e' : Perm α'
⊢ Equiv.trans (e.extendDomain f) (e'.extendDomain f) = extendDomain (Equiv.trans e e') f

Tactic:
simp [Perm.extendDomain, permCongr_trans]

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
⊢ b ≤ a ∆ b ↔ Disjoint a b

Tactic:
rw [symmDiff_comm, le_symmDiff_iff_left, disjoint_comm]

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

Goal state before:
pp: α : Sort u_1
β : Sort u_4
inst✝ : DecidableEq α
f : α ≃ β
a : α
b : β
⊢ (f.setValue a b) a = b

Tactic:
simp [setValue, swap_apply_left]

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 : β i × ((j : { j // j ≠ i }) → β ↑j)
⊢ (fun f ↦ (f i, fun j ↦ f ↑j)) ((fun f j ↦ if h : j = i then ⋯ ▸ f.fst else f.snd ⟨j, h⟩) f) = f

Tactic:
ext x

Goal state after:
case fst
α✝ : 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 : β i × ((j : { j // j ≠ i }) → β ↑j)
⊢ ((fun f ↦ (f i, fun j ↦ f ↑j)) ((fun f j ↦ if h : j = i then ⋯ ▸ f.fst else f.snd ⟨j, h⟩) f)).fst = f.fst

case snd
α✝ : 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 : β i × ((j : { j // j ≠ i }) → β ↑j)
x : { j // j ≠ i }
⊢ ((fun f ↦ (f i, fun j ↦ f ↑j)) ((fun f j ↦ if h : j = i then ⋯ ▸ f.fst else f.snd ⟨j, h⟩) f)).snd x = f.snd x
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:
by
  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: case refine_1
α : 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
⊢ b ∈ f '' s

pp: case refine_2
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
h' : SurjOn f s t
x✝ : ↑t
b : β
hb : b ∈ t
⊢ ∃ a, restrict f s t h a = ⟨b, hb⟩

Tactic:
· obtain ⟨⟨a, ha⟩, ha'⟩ := h' ⟨b, hb⟩
    replace ha' : f a = b := by simpa [Subtype.ext_iff] using ha'
    rw [← ha']
    exact mem_image_of_mem f ha

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
h' : SurjOn f s t
x✝ : ↑t
b : β
hb : b ∈ t
⊢ ∃ a, restrict f s t h a = ⟨b, hb⟩
Module: Mathlib.Data.Set.Piecewise

Goal state before:
pp: α : Type u_1
δ : α → Sort u_7
s : Set α
f : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
⊢ s.piecewise f f = f

Tactic:
ext x

Goal state after:
α : Type u_1
δ : α → Sort u_7
s : Set α
f : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
x : α
⊢ s.piecewise f f x = f x
Module: Mathlib.Data.Set.Prod

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

Tactic:
rw [prod_eq_prod_iff_of_nonempty h]

Goal state after:
case inr
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
⊢ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s = s₁ ∧ t = t₁
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
ht : t.Nonempty
⊢ s = s₁ ∧ True ∨ (s = ∅ ∨ False) ∧ (s₁ = ∅ ∨ False) ↔ s = s₁

Tactic:
and_true,

Goal state after:
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
ht : t.Nonempty
⊢ s = s₁ ∨ (s = ∅ ∨ False) ∧ (s₁ = ∅ ∨ False) ↔ s = s₁
Module: Mathlib.Data.Set.Prod

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

Tactic:
ext x

Goal state after:
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
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
s t : Set α
h : Disjoint s t
⊢ (s ∪ t).offDiag = s.offDiag ∪ t.offDiag ∪ s ×ˢ t ∪ t ×ˢ s

Tactic:
ext x

Goal state after:
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
⊢ x ∈ (s ∪ t).offDiag ↔ x ∈ s.offDiag ∪ t.offDiag ∪ s ×ˢ t ∪ t ×ˢ s
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
s t : Set α
h : t ⊆ s
⊢ val '' {x | ↑x ∈ t} = t

Tactic:
ext x

Goal state after:
α : Type u_1
s t : Set α
h : t ⊆ s
x : α
⊢ x ∈ val '' {x | ↑x ∈ t} ↔ x ∈ t
Module: Mathlib.Data.Set.Prod

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

Tactic:
ext x

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
inst✝ : DecidableEq ι
f : (i : ι) → α i
hi : i ∈ s
hf : ∀ (j : ι), j ∈ s → j ≠ i → f j ∈ t j
⊢ update f i ⁻¹' s.pi t = t i

Tactic:
ext x

Goal state after:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
inst✝ : DecidableEq ι
f : (i : ι) → α i
hi : i ∈ s
hf : ∀ (j : ι), j ∈ s → j ≠ i → f j ∈ t j
x : α i
⊢ x ∈ update f i ⁻¹' s.pi t ↔ x ∈ t i
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
⊢ Prod.snd '' graphOn f s = f '' s

Tactic:
ext x

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
x : β
⊢ x ∈ Prod.snd '' graphOn f s ↔ x ∈ f '' s
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2
⊢ range f = graphOn (fun h ↦ (f ⋯.choose).2) univ

Tactic:
ext x

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2
x : β × γ
⊢ x ∈ range f ↔ x ∈ graphOn (fun h ↦ (f ⋯.choose).2) univ
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₁ ∩ f '' s

Tactic:
by
  apply Subset.antisymm
  · rintro _ ⟨x, ⟨h₁, h⟩, rfl⟩
    exact ⟨by rwa [mem_preimage, hf h], mem_image_of_mem _ h⟩
  · rintro _ ⟨h₁, ⟨x, h, rfl⟩⟩
    exact mem_image_of_mem _ ⟨by rwa [← hf h], h⟩

Goal state after:
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)
⊢ f '' s = g ⁻¹' s

Tactic:
ext x

Goal state after:
α : 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
Module: Mathlib.Data.Int.Init

Goal state before:
pp: motive : ℤ → Sort u_1
z b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
hz : b ≤ z
⊢ Int.inductionOn' (z + 1) b zero succ pred = succ z hz (Int.inductionOn' z b zero succ pred)

Tactic:
unfold Int.inductionOn'
  rw! [show z - b = (z - b).toNat by lia, show z + 1 - b = ((z - b).toNat + 1 : ℕ) by lia]
  grind [inductionOn'.pos, show b + (z - b).toNat = z by lia]

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
⊢ MapsTo f (s ∪ r) t'

pp: case refine_3
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
⊢ InjOn f (s ∪ r)

pp: case refine_4
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
y : β
hyt' : y ∈ t'
⊢ y ∈ f '' (s ∪ r)

Tactic:
· rw [mapsTo_iff_image_subset, image_union, hbij.image_eq, h.image_eq, union_subset_iff]
    exact ⟨htt', sdiff_subset.trans inter_subset_right⟩

Goal state after:
case refine_3
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
⊢ InjOn f (s ∪ r)

case refine_4
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
y : β
hyt' : y ∈ t'
⊢ y ∈ f '' (s ∪ r)
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : Classical.choice n ∈ s
⊢ invFun f ⁻¹' s = f '' s ∪ (range f)ᶜ

Tactic:
ext x

Goal state after:
α : Type u_1
β : Type u_2
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : Classical.choice n ∈ s
x : β
⊢ x ∈ invFun f ⁻¹' s ↔ x ∈ f '' s ∪ (range f)ᶜ
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : ¬Classical.choice n ∈ s
⊢ invFun f ⁻¹' s = f '' s

Tactic:
ext x

Goal state after:
α : Type u_1
β : Type u_2
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : ¬Classical.choice n ∈ s
x : β
⊢ x ∈ invFun f ⁻¹' s ↔ x ∈ f '' s
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: G : Type u_3
inst✝ : CommGroup G
a b : G
⊢ a * (b / a) = b

Tactic:
by
  rw [← mul_div_assoc, mul_div_cancel_left]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_1
inst✝¹ : MonoidWithZero M₀
inst✝ : Nontrivial M₀
h : 0 ^ 0 = 0
⊢ False

Tactic:
simp at h

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: G₀ : Type u_4
G₀' : Type u_5
inst✝⁴ : GroupWithZero G₀
inst✝³ : GroupWithZero G₀'
inst✝² : MulActionWithZero G₀ G₀'
inst✝¹ : SMulCommClass G₀ G₀' G₀'
inst✝ : IsScalarTower G₀ G₀' G₀'
c : G₀
x : G₀'
⊢ (c • x)⁻¹ = c⁻¹ • x⁻¹

Tactic:
by
  obtain rfl | hc := eq_or_ne c 0
  · simp only [inv_zero, zero_smul]
  obtain rfl | hx := eq_or_ne x 0
  · simp only [inv_zero, smul_zero]
  · refine inv_eq_of_mul_eq_one_left ?_
    rw [smul_mul_smul_comm, inv_mul_cancel₀ hc, inv_mul_cancel₀ hx, one_smul]

Goal state after:
Module: Mathlib.Algebra.Divisibility.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
h : a = b
⊢ a ∣ b

Tactic:
by rw [h]

Goal state after:
Module: Mathlib.Algebra.Divisibility.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
h : a = b
⊢ a ∣ᵣ b

Tactic:
by rw [h]

Goal state after:
Module: Mathlib.Algebra.Divisibility.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommSemigroup α
inst✝ : DecompositionMonoid α
k m n : α
⊢ (∃ d₁ d₂, d₁ ∣ m ∧ d₂ ∣ n ∧ k = d₁ * d₂) → k ∣ m * n

Tactic:
rintro ⟨d₁, d₂, hy, hz, rfl⟩

Goal state after:
α : Type u_1
inst✝¹ : CommSemigroup α
inst✝ : DecompositionMonoid α
m n d₁ d₂ : α
hy : d₁ ∣ m
hz : d₂ ∣ n
⊢ d₁ * d₂ ∣ m * n
Module: Mathlib.Algebra.GroupWithZero.Semiconj

Goal state before:
pp: case pos
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a y : G₀
ha : ¬a = 0
h : SemiconjBy a 0 y
⊢ SemiconjBy a 0⁻¹ y⁻¹

Tactic:
simp only [SemiconjBy, mul_zero, @eq_comm _ _ (y * a), mul_eq_zero] at h

Goal state after:
case pos
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a y : G₀
ha : ¬a = 0
h : y = 0 ∨ a = 0
⊢ SemiconjBy a 0⁻¹ y⁻¹
Module: Mathlib.Algebra.Ring.Commute

Goal state before:
pp: R : Type u
inst✝ : Ring R
n : ℕ
⊢ (-1) ^ n = (-1) ^ (n % 2)

Tactic:
rw [← Nat.mod_add_div n 2, pow_add, pow_mul]

Goal state after:
R : Type u
inst✝ : Ring R
n : ℕ
⊢ (-1) ^ (n % 2) * ((-1) ^ 2) ^ (n / 2) = (-1) ^ ((n % 2 + 2 * (n / 2)) % 2)
Module: Mathlib.Algebra.Module.NatInt

Goal state before:
pp: case ofNat
R : Type u_1
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
b : M
a✝ : ℕ
⊢ ↑(ofNat a✝) • b = ofNat a✝ • b

Tactic:
| ofNat =>

Goal state after:
Module: Mathlib.Algebra.Module.NatInt

Goal state before:
pp: case ofNat
R✝ : Type u_1
S : Type u_2
M✝ : Type u_3
M₂ : Type u_4
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : R
y : M
a✝ : ℕ
⊢ (Int.ofNat a✝ • x) • y = Int.ofNat a✝ • x • y

Tactic:
| ofNat =>

Goal state after: