mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.BinaryRec

Goal state before:
pp: n : Nat
b : Bool
⊢ bit b n = 0 ↔ n = 0 ∧ b = false

Tactic:
by
  cases n <;> cases b <;> simp [bit, Nat.two_mul, ← Nat.add_assoc]

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

Goal state before:
pp: n : Nat
hn : n >>> 1 ≠ 0
⊢ 0 < 2

Tactic:
decide

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

Goal state before:
pp: n : Nat
n0 : ¬n + 1 + 1 = 0
⊢ 2 ≠ 0

Tactic:
decide

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

Goal state before:
pp: case false
n : Nat
⊢ false.toNat < 2

Tactic:
decide

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

Goal state before:
pp: case true
n : Nat
⊢ true.toNat < 2

Tactic:
decide

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

Goal state before:
pp: case H
b : Bool
n : Nat
⊢ 0 < 2

Tactic:
decide

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
ex : ∀ (x y : M), x * y = 1 → ∃ z, z * x = 1
x y : M
h : x * y = 1
z : M
hz : z * x = 1
⊢ y * x = 1

Tactic:
rwa [show y = z by simpa [mul_assoc, h] using congr_arg (· * y) hz.symm]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a b✝ c : α
h : ∀ (a b c : α), r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a c
d e : α
a✝ : ReflTransGen r a d
hde : r d e
b : α
hdb : ReflTransGen r d b
⊢ ∃ a, ReflTransGen r e a ∧ ReflGen r b a

Tactic:
induction hdb with

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

Goal state before:
pp: α : Type u
f : α → α
n : ℕ
hn : 0 < n
⊢ f^[n.pred.succ] = f^[n]

Tactic:
Nat.succ_pred_eq_of_pos hn

Goal state after:
α : Type u
f : α → α
n : ℕ
hn : 0 < n
⊢ f^[n] = f^[n]
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M : Type u_1
N : Type u_2
G✝ : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
G : Type u_9
P : Type u_10
inst✝¹ : Group G
inst✝ : MulAction G P
a : G
b c : P
h : a • b = a • c
⊢ b = c

Tactic:
rw [← inv_smul_smul a b, h, inv_smul_smul]

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
⊢ IsEquiv α (fun x1 x2 ↦ x1 ≠ x2)ᶜ

Tactic:
convert! eq_isEquiv α

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
x✝¹ x✝ : α
⊢ (fun x1 x2 ↦ x1 ≠ x2)ᶜ = Eq
Module: Mathlib.Data.Bool.Basic

Goal state before:
pp: ⊢ ¬true = false

Tactic:
decide

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

Goal state before:
pp: ⊢ ¬false = true

Tactic:
decide

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

Goal state before:
pp: ⊢ ∀ {a b : Bool}, (a && b) = true → a = true

Tactic:
decide

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

Goal state before:
pp: ⊢ ∀ {a b : Bool}, a = true → b = true → (a && b) = true

Tactic:
decide

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

Goal state before:
pp: ⊢ ∀ {a b : Bool}, (a && b) = true → b = true

Tactic:
decide

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

Goal state before:
pp: ⊢ ∀ {a b : Bool}, a = !b ↔ a ≠ b

Tactic:
decide

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

Goal state before:
pp: ⊢ ∀ {a b : Bool}, (!a) = b ↔ a ≠ b

Tactic:
decide

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

Goal state before:
pp: ⊢ ∀ (b : Bool), (!b) ≠ b

Tactic:
decide

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

Goal state before:
pp: ⊢ ∀ (b : Bool), b ≠ !b

Tactic:
decide

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

Goal state before:
pp: ⊢ ∀ (a b : Bool), a = b ∨ a = !b

Tactic:
decide

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

Goal state before:
pp: ⊢ ∀ {x y : Bool}, (x ^^ y) = true ↔ x ≠ y

Tactic:
decide

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

Goal state before:
pp: ⊢ ∀ (a : Bool), a ≤ a

Tactic:
decide

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

Goal state before:
pp: ⊢ ∀ (a b c : Bool), a ≤ b → b ≤ c → a ≤ c

Tactic:
decide

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

Goal state before:
pp: ⊢ ∀ (a b : Bool), a < b ↔ a ≤ b ∧ ¬b ≤ a

Tactic:
decide

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

Goal state before:
pp: ⊢ ∀ (a b : Bool), a ≤ b → b ≤ a → a = b

Tactic:
decide

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

Goal state before:
pp: ⊢ ∀ (a b : Bool), a ≤ b ∨ b ≤ a

Tactic:
decide

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

Goal state before:
pp: ⊢ ∀ (a b : Bool), min a b = if a ≤ b then a else b

Tactic:
decide

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

Goal state before:
pp: ⊢ ∀ (a b : Bool), max a b = if a ≤ b then b else a

Tactic:
decide

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

Goal state before:
pp: ⊢ ∀ {x y : Bool}, x < y ↔ x = false ∧ y = true

Tactic:
decide

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

Goal state before:
pp: ⊢ ∀ {x y : Bool}, x ≤ y ↔ x = true → y = true

Tactic:
decide

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

Goal state before:
pp: ⊢ ∀ (x y : Bool), (x && y) ≤ x

Tactic:
decide

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

Goal state before:
pp: ⊢ ∀ (x y : Bool), (x && y) ≤ y

Tactic:
decide

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

Goal state before:
pp: ⊢ ∀ {x y z : Bool}, x ≤ y → x ≤ z → x ≤ (y && z)

Tactic:
decide

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

Goal state before:
pp: ⊢ ∀ (x y : Bool), x ≤ (x || y)

Tactic:
decide

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

Goal state before:
pp: ⊢ ∀ (x y : Bool), y ≤ (x || y)

Tactic:
decide

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

Goal state before:
pp: ⊢ ∀ {x y z : Bool}, x ≤ z → y ≤ z → (x || y) ≤ z

Tactic:
decide

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

Goal state before:
pp: case step
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Injective next
m✝ : ℕ
hnm : n.le m✝
ih : Injective (leRecOn hnm fun {k} ↦ next)
x y : C n
H : next (leRecOn hnm (fun {k} ↦ next) x) = next (leRecOn hnm (fun {k} ↦ next) y)
⊢ x = y

Tactic:
exact ih (Hnext _ H)

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

Goal state before:
pp: case inl
⊢ 2 * 0 ^ 2 + 1 ≤ 2 ^ (2 * 0)

Tactic:
decide

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

Goal state before:
pp: k : ℕ
hk : k > 0
hk0 : 0 < 2 * k ^ 2
⊢ 2 ≠ 1

Tactic:
decide

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
⊢ Antitone (⇑toDual ∘ f ∘ ⇑ofDual) ↔ Antitone f

Tactic:
by
  rw [antitone_toDual_comp_iff, monotone_comp_ofDual_iff]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
⊢ MonotoneOn (⇑toDual ∘ f ∘ ⇑ofDual) s ↔ MonotoneOn f s

Tactic:
rw [monotoneOn_toDual_comp_iff, antitoneOn_comp_ofDual_iff]

Goal state after:
Module: Mathlib.Tactic.Lift

Goal state before:
pp: ι : Sort u_1
α : ι → Sort u_2
ne : ∀ (i : ι), Nonempty (α i)
p : ι → Prop
f : (i : Subtype p) → α i.val
⊢ ∃ g, (fun i ↦ g i.val) = f

Tactic:
haveI : DecidablePred p := fun i ↦ Classical.propDecidable (p i)
  exact ⟨fun i => if hi : p i then f ⟨i, hi⟩ else Classical.choice (ne i),
    funext fun i ↦ dif_pos i.2⟩

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

Goal state before:
pp: α : Type u
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
⊢ ∃ f, StrictMono f ∧ f 0 = a

Tactic:
choose g hg using fun x : α ↦ exists_gt x

Goal state after:
α : Type u
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
g : α → α
hg : ∀ (x : α), x < g x
⊢ ∃ f, StrictMono f ∧ f 0 = a
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: n : ℕ
⊢ n ^ n ≤ (n + 1) ^ (n + 1)

Tactic:
Nat.pow_succ

Goal state after:
n : ℕ
⊢ n ^ n ≤ (n + 1) ^ n * (n + 1)
Module: Mathlib.Order.Monotone.Basic

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

Tactic:
induction n with
  | zero => rw [Int.ofNat_one]; apply h
  | succ n ihn => rw [Int.natCast_succ, ← Int.add_assoc]; exact _root_.trans ihn (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:
by
  simpa +contextual [Set.ext_iff, iff_iff_implies_and_implies, forall_and, List.eq_replicate_iff,
    List.length_pos_iff_exists_mem] using ⟨fun _ _ ↦ ⟨_, ‹_›⟩, fun x hx h ↦ h _ hx ▸ hx⟩

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case inl.refine_3
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeInf β
hf : AntitoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : x ≤ y
this : f y ≤ f x
⊢ f (max x y) = f x ⊓ f y

Tactic:
first
    | assumption
    | simp only [*, sup_of_le_left, sup_of_le_right, inf_of_le_left, inf_of_le_right]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case inl.refine_1
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeInf β
hf : AntitoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : x ≤ y
⊢ x ∈ s

Tactic:
first
    | assumption
    | simp only [*, sup_of_le_left, sup_of_le_right, inf_of_le_left, inf_of_le_right]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case inl.refine_2
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeInf β
hf : AntitoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : x ≤ y
⊢ y ∈ s

Tactic:
first
    | assumption
    | simp only [*, sup_of_le_left, sup_of_le_right, inf_of_le_left, inf_of_le_right]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case inr.refine_3
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeInf β
hf : AntitoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : y ≤ x
this : f x ≤ f y
⊢ f (max x y) = f x ⊓ f y

Tactic:
first
    | assumption
    | simp only [*, sup_of_le_left, sup_of_le_right, inf_of_le_left, inf_of_le_right]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case inr.refine_1
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeInf β
hf : AntitoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : y ≤ x
⊢ y ∈ s

Tactic:
first
    | assumption
    | simp only [*, sup_of_le_left, sup_of_le_right, inf_of_le_left, inf_of_le_right]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case inr.refine_2
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeInf β
hf : AntitoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : y ≤ x
⊢ x ∈ s

Tactic:
first
    | assumption
    | simp only [*, sup_of_le_left, sup_of_le_right, inf_of_le_left, inf_of_le_right]

Goal state after:
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_inf_iff,

Goal state after:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
⊢ d ⊓ a ≤ b ∧ d ⊓ a ≤ c ↔ d ≤ a ⇨ b ∧ d ≤ 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 ⇨ c) ⊓ (b ⇨ c)

Tactic:
le_inf_iff,

Goal state after:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
⊢ d ≤ a ⊔ b ⇨ c ↔ d ≤ a ⇨ c ∧ d ≤ b ⇨ 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 : αᵒᵈ
⊢ toDual (ofDual b ⇨ ofDual a) ≤ c ↔ a ≤ b ⊔ c

Tactic:
rw [sup_comm]; exact le_himp_iff

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedCoheytingAlgebra α
a✝ b✝ c✝ d a b c : α
⊢ ((a ⊔ b) ⊓ (a ⊔ c)) \ a ≤ b ⊓ c

Tactic:
le_inf_iff,

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

Goal state before:
pp: α : Type u_2
inst✝ : HeytingAlgebra α
a : α
⊢ a ≤ aᶜ ↔ a = ⊥

Tactic:
rw [le_compl_iff_disjoint_left, disjoint_self]

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

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

Tactic:
exact (eq_of_inf_eq_sup_eq i s).symm

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

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

Tactic:
← compl_compl_inf_distrib

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
γ : Type u_3
e₁ : α ≃ β
e₂ : β ≃ γ
x : Option α
⊢ (e₁.trans e₂).optionCongr x = (e₁.optionCongr.trans e₂.optionCongr) x

Tactic:
symm

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
e₁ : α ≃ β
e₂ : β ≃ γ
x : Option α
⊢ (e₁.optionCongr.trans e₂.optionCongr) x = (e₁.trans e₂).optionCongr x
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : HeytingAlgebra α
a✝ b✝ : α
a b c : αᵒᵈ
⊢ toDual (ofDual b ⇨ ofDual a) ≤ c ↔ a ≤ b ⊔ c

Tactic:
rw [sup_comm]; exact le_himp_iff

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: ⊢ ∀ (p q : Bool), p ∆ q = (p ^^ q)

Tactic:
decide

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
α : Type u_9
β : α → Type u_10
a✝ : α
x✝ : { s // s.fst = a✝ }
a : Sigma β
h : a.fst = a✝
⊢ (fun b ↦ ⟨⟨a✝, b⟩, ⋯⟩)
      ((fun x ↦
          match x with
          | ⟨⟨fst, b⟩, h⟩ => h ▸ b)
        ⟨a, h⟩) =
    ⟨a, h⟩

Tactic:
cases h; simp

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : CoheytingAlgebra α
a : α
⊢ (￢a) ∆ a = ⊤

Tactic:
eq_top_iff,

Goal state after:
α : Type u_2
inst✝ : CoheytingAlgebra α
a : α
⊢ ⊤ ≤ (￢a) ∆ a
Module: Mathlib.Order.SymmDiff

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

Tactic:
simp only [(· ∆ ·), sdiff_sdiff_sup_sdiff']

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

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

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

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

Goal state before:
pp: case inr
α : Type u_1
s : Set α
σ : Equiv.Perm α
hs : {a | σ a ≠ a} ⊆ s
i : α
hi : σ i ≠ i
⊢ i ∈ ⇑σ '' s ↔ i ∈ s

Tactic:
refine iff_of_true ⟨σ.symm i, hs fun h => hi ?_, σ.apply_symm_apply _⟩ (hs hi)

Goal state after:
case inr
α : Type u_1
s : Set α
σ : Equiv.Perm α
hs : {a | σ a ≠ a} ⊆ s
i : α
hi : σ i ≠ i
h : σ ((Equiv.symm σ) i) = (Equiv.symm σ) i
⊢ σ i = i
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
ι : Sort u_4
f : ι → α
inst✝ : Nonempty ι
y : α
h : ∀ (x : α), (∃ y, f y = x) ↔ x = y
x✝ : ι
⊢ ∃ y, f y = f x✝

Tactic:
exists_apply_eq_apply

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 = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅)

Tactic:
symm

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
⊢ (s.pi t).Nonempty ↔ ∀ (i : ι), ∃ x, i ∈ s → x ∈ t i

Tactic:
simp [Classical.skolem, Set.Nonempty]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
t : (i : ι) → Set (α i)
⊢ (univ.pi t).Nonempty ↔ ∀ (i : ι), (t i).Nonempty

Tactic:
simp [Classical.skolem, Set.Nonempty]

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

Goal state before:
pp: α : Type u_1
t : Set α
p : Set α → Prop
⊢ (∃ s, p (val '' s)) ↔ ∃ s, s ⊆ t ∧ p s

Tactic:
← exists_subset_range_and_iff,

Goal state after:
α : Type u_1
t : Set α
p : Set α → Prop
⊢ (∃ s, s ⊆ range val ∧ p s) ↔ ∃ s, s ⊆ t ∧ p s
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 : ℤ
x✝ : ι
⊢ (⇑f ∘ (g ^ n)) x✝ = (⇑f ∘ g ^ n) x✝

Tactic:
simp [map_zpow' f hf]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Nonempty α
f : α → β
s : Set α
⊢ invFunOn f s '' f '' s ⊆ s

Tactic:
rintro _ ⟨_, ⟨x, hx, rfl⟩, rfl⟩; exact invFunOn_apply_mem hx

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

Goal state before:
pp: m n : ℕ
⊢ (↑m).gcd -[n+1] = m.gcd (n + 1)

Tactic:
simp [gcd]

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

Goal state before:
pp: m n : ℕ
⊢ -[m+1].gcd ↑n = (m + 1).gcd n

Tactic:
simp [gcd]

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

Goal state before:
pp: m n : ℕ
⊢ -[m+1].gcd -[n+1] = (m + 1).gcd (n + 1)

Tactic:
simp [gcd]

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

Goal state before:
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 [image_union, h.image_eq, hbij.image_eq, union_sdiff_self]

Goal state after:
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 ∈ t ∪ f '' s₁ ∩ t'
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : DecidableEq α
a b : α
ha : a ∈ s
hb : b ∈ s
x : α
⊢ (swap a b) x ∈ s ↔ x ∈ s

Tactic:
obtain rfl | hxa := eq_or_ne x a

Goal state after:
case inl
α : Type u_1
s : Set α
inst✝ : DecidableEq α
b : α
hb : b ∈ s
x : α
ha : x ∈ s
⊢ (swap x b) x ∈ s ↔ x ∈ s

case inr
α : Type u_1
s : Set α
inst✝ : DecidableEq α
a b : α
ha : a ∈ s
hb : b ∈ s
x : α
hxa : x ≠ a
⊢ (swap a b) x ∈ s ↔ x ∈ s
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
a : M
n m : ℕ
ha : a ^ n = 1
⊢ a ^ (m % n + n * (m / n)) = a ^ (m % n)

Tactic:
simp [pow_add, pow_mul, ha]

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a : G
n : ℕ
⊢ a ^ (Int.negSucc (n + 1) + 1) = (a ^ (n + 1))⁻¹

Tactic:
rw [Int.negSucc_eq, Int.neg_add, Int.neg_add_cancel_right]

Goal state after:
G : Type u_3
inst✝ : Group G
a : G
n : ℕ
⊢ a ^ (-↑(n + 1)) = (a ^ (n + 1))⁻¹
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a✝ b u : αˣ
n : ℕ
a : αˣ
⊢ ↑a ^ n * ↑a⁻¹ ^ n = 1

Tactic:
by rw [← a.commute_coe_inv.mul_pow]; simp

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

Goal state before:
pp: α : Type u
inst✝ : DivisionMonoid α
a b : α
ha : IsUnit a
hb : IsUnit b
⊢ IsUnit (a / b)

Tactic:
rw [div_eq_mul_inv]

Goal state after:
α : Type u
inst✝ : DivisionMonoid α
a b : α
ha : IsUnit a
hb : IsUnit b
⊢ IsUnit (a * b⁻¹)
Module: Mathlib.Control.Basic

Goal state before:
pp: m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
a : m α
⊢ joinM (pure <$> a) = a

Tactic:
simp only [joinM, id, ← bind_pure_comp, bind_assoc, pure_bind, bind_pure]

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

Goal state before:
pp: M₀ : Type u_1
inst✝ : MulZeroClass M₀
a b : M₀
h : a ≠ 0 → b = 0
this : Decidable (a = 0)
ha : a = 0
⊢ a * b = 0

Tactic:
by rw [ha, zero_mul]

Goal state after:
Module: Mathlib.Data.Nat.Cast.Defs

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ 1 + 1 = 2

Tactic:
decide

Goal state after:
Module: Mathlib.Data.Nat.Cast.Defs

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ 1 + 1 + 1 = 3

Tactic:
decide

Goal state after:
Module: Mathlib.Data.Nat.Cast.Defs

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ 1 + 1 + 1 + 1 = 4

Tactic:
decide

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

Goal state before:
pp: M : Type u_1
M₀ : Type u_2
M₀' : Type u_3
G₀ : Type u_4
G₀' : Type u_5
N : Type u_6
A : Type u_7
A' : Type u_8
B : Type u_9
α : Type u_10
β : Type u_11
inst✝² : Group α
inst✝¹ : GroupWithZero β
inst✝ : MulDistribMulAction α β
g : α
⊢ ¬g • 0 * (g • 0)⁻¹ = 1

Tactic:
rw [← smul_one g, ← inv_smul_eq_iff, smul_mul', inv_smul_smul, zero_mul]
    exact zero_ne_one

Goal state after:
Module: Mathlib.Algebra.Group.Nat.Even

Goal state before:
pp: m n : ℕ
⊢ ¬Even 25394535

Tactic:
decide

Goal state after:
Module: Mathlib.Algebra.Group.Int.Even

Goal state before:
pp: m n : ℤ
⊢ ¬Even 25394535

Tactic:
decide

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

Goal state before:
pp: M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹ : MulOneClass M
inst✝ : CommGroup N
f : M →* N
n : ℤ
x y : M
⊢ (⇑f ^ n) (x * y) = (⇑f ^ n) x * (⇑f ^ n) y

Tactic:
by simp [mul_zpow]

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

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a b c : G₀
hac : Commute a c
hbc : Commute b c
⊢ Commute (a / b) c

Tactic:
rw [div_eq_mul_inv]

Goal state after:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a b c : G₀
hac : Commute a c
hbc : Commute b c
⊢ Commute (a * b⁻¹) c
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: case inr.inl
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
a b : M₀
h : IsUnit a ∨ IsUnit b
ha : ¬IsUnit a
hb : IsUnit b
⊢ (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ

Tactic:
have : ¬ IsUnit (a * b) := by simpa [hb.mul_right_iff]
    simp [Ring.inverse_non_unit, ha, this]

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

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
a b : G₀
ha : a ≠ 0
hb : b ≠ 0
⊢ a / b ≠ 0

Tactic:
rw [div_eq_mul_inv]

Goal state after:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a b : G₀
ha : a ≠ 0
hb : b ≠ 0
⊢ a * b⁻¹ ≠ 0
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
a b c : G₀
hb : b ≠ 0
h : b = a⁻¹ * c
⊢ a * b = c

Tactic:
rwa [← eq_inv_mul_iff_mul_eq₀]

Goal state after:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a b c : G₀
hb : b ≠ 0
h : b = a⁻¹ * c
⊢ a ≠ 0
Module: Mathlib.Algebra.Ring.Commute

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
a b : R
inst✝ : NoZeroDivisors R
h : Commute a b
⊢ a + b = 0 ∨ a - b = 0 ↔ a = b ∨ a = -b

Tactic:
add_eq_zero_iff_eq_neg,

Goal state after:
R : Type u
inst✝¹ : Ring R
a b : R
inst✝ : NoZeroDivisors R
h : Commute a b
⊢ a = -b ∨ a - b = 0 ↔ a = b ∨ a = -b
Module: Mathlib.Data.Int.Cast.Lemmas

Goal state before:
pp: F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : CommGroup α
inst✝ : AddCommGroup β
a b : α
n : Multiplicative ℤ
⊢ ((zpowersHom α).toFun (a * b)) n = ((zpowersHom α).toFun a * (zpowersHom α).toFun b) n

Tactic:
by simp [mul_zpow]

Goal state after:
Module: Mathlib.Algebra.Order.ZeroLEOne

Goal state before:
pp: α : Type u_1
⊢ 0 ≤ 1

Tactic:
decide

Goal state after:
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
m n : ℕ
⊢ ¬Even 25394535

Tactic:
decide

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE

Goal state before:
pp: α : Type u
inst✝³ : MulOneClass α
inst✝² : Preorder α
inst✝¹ : ExistsMulOfLE α
a b : α
inst✝ : MulLeftReflectLE α
h : a ≤ b
⊢ ∃ c, 1 ≤ c ∧ a * c = b

Tactic:
by
  obtain ⟨c, rfl⟩ := exists_mul_of_le h; exact ⟨c, one_le_of_le_mul_right h, rfl⟩

Goal state after: