mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Tactic.Translate.Reorder

Goal state before:
pp: r✝ r : ArgReorder
n : Nat
cycle : { l // 2 ≤ l.length }
⊢ cycle.val ≠ []

Tactic:
by grind

Goal state after:
Module: Mathlib.Tactic.Translate.Reorder

Goal state before:
pp: n : Nat
map✝¹ : Vector (Option (Fin n)) n
map✝ : Vector (Option (Fin n)) n := map✝¹
perm✝ : List { l // 2 ≤ l.length } := []
i : Nat
h : i ∈ *...n
__r✝² : Option Permutation := __s✝¹.fst
__s✝ : Vector (Option (Fin n)) n × List { l // 2 ≤ l.length } := __s✝¹.snd
map : Vector (Option (Fin n)) n := __s✝.fst
perm : List { l // 2 ≤ l.length } := __s✝.snd
j✝ : Fin n
j : Fin n := j✝
__r✝ : Unit
⊢ 2 ≤ [i, ↑j].length

Tactic:
by grind

Goal state after:
Module: Mathlib.Tactic.Translate.Reorder

Goal state before:
pp: n : Nat
map✝³ : Vector (Option (Fin n)) n
map✝² : Vector (Option (Fin n)) n := map✝³
perm✝ : List { l // 2 ≤ l.length } := []
i : Nat
h : i ∈ *...n
__r✝⁷ : Option Permutation := __s✝⁴.fst
__s✝³ : Vector (Option (Fin n)) n × List { l // 2 ≤ l.length } := __s✝⁴.snd
map✝¹ : Vector (Option (Fin n)) n := __s✝³.fst
perm : List { l // 2 ≤ l.length } := __s✝³.snd
j✝² : Fin n
j✝¹ : Fin n := j✝²
__r✝⁵ : Unit
cycle✝ : { l // 2 ≤ l.length } := ⟨[i, ↑j✝¹], ⋯⟩
x✝ : Unit
__r✝³ : Option Permutation := __s✝².fst
__s✝¹ : Vector (Option (Fin n)) n × Fin n × { l // 2 ≤ l.length } := __s✝².snd
map✝ : Vector (Option (Fin n)) n := __s✝¹.fst
__s✝ : Fin n × { l // 2 ≤ l.length } := __s✝¹.snd
j✝ : Fin n := __s✝.fst
cycle : { l // 2 ≤ l.length } := __s✝.snd
j' : Fin n
map : Vector (Option (Fin n)) n := map✝.set! (↑j✝) none
__r✝¹ : Unit
j : Fin n := j'
⊢ 2 ≤ (cycle.val ++ [↑j]).length

Tactic:
by grind

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

Goal state before:
pp: case succ.zero
n0 : ¬0 + 1 = 0
⊢ (if (0 + 1) >>> 1 = 0 then 0 else ((0 + 1) >>> 1).log2.succ) < if 0 + 1 = 0 then 0 else (0 + 1).log2.succ

pp: case succ.succ
n : Nat
n0 : ¬n + 1 + 1 = 0
⊢ (if (n + 1 + 1) >>> 1 = 0 then 0 else ((n + 1 + 1) >>> 1).log2.succ) <
    if n + 1 + 1 = 0 then 0 else (n + 1 + 1).log2.succ

Tactic:
· simp

Goal state after:
case succ.succ
n : Nat
n0 : ¬n + 1 + 1 = 0
⊢ (if (n + 1 + 1) >>> 1 = 0 then 0 else ((n + 1 + 1) >>> 1).log2.succ) <
    if n + 1 + 1 = 0 then 0 else (n + 1 + 1).log2.succ
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
a : M
⊢ a ^ 2 = a * a

Tactic:
by rw [pow_succ, pow_one]

Goal state after:
Module: Mathlib.Logic.ExistsUnique

Goal state before:
pp: α : Sort u_1
p : α → Sort u_2
inst✝ : ∀ (x : α), Subsingleton (p x)
q : (x : α) → p x → Prop
h : ∃! x, ∃! hx, q x hx
y₁ y₂ : α
hpy₁ : p y₁
hqy₁ : q y₁ hpy₁
hpy₂ : p y₂
hqy₂ : q y₂ hpy₂
⊢ y₁ = y₂

Tactic:
simp only [existsUnique_iff_exists] at h
  exact h.unique ⟨hpy₁, hqy₁⟩ ⟨hpy₂, hqy₂⟩

Goal state after:
Module: Mathlib.Logic.ExistsUnique

Goal state before:
pp: α✝ : Sort u_1
α : Type u_2
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
hx : p x
h : ∀ (y : α), y ∈ xs → p y → x = y
⊢ (fun x_1 ↦ x_1 ∈ x :: xs ∧ p x_1) x ∧ ∀ (y : α), (fun x_1 ↦ x_1 ∈ x :: xs ∧ p x_1) y → y = x

Tactic:
by grind

Goal state after:
Module: Mathlib.Logic.ExistsUnique

Goal state before:
pp: α✝ : Sort u_1
α : Type u_2
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
hx : p x
x✝ : ∃! x_1, x_1 ∈ x :: xs ∧ p x_1
y : α
hy : y ∈ xs
hp : p y
z : α
h : (fun x_1 ↦ x_1 ∈ x :: xs ∧ p x_1) z ∧ ∀ (y : α), (fun x_1 ↦ x_1 ∈ x :: xs ∧ p x_1) y → y = z
⊢ z = y

Tactic:
by grind

Goal state after:
Module: Mathlib.Logic.ExistsUnique

Goal state before:
pp: α✝ : Sort u_1
α : Type u_2
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
hx : ¬p x
this : Decidable (∃! x, x ∈ xs ∧ p x)
⊢ (∃! x, x ∈ xs ∧ p x) ↔ ∃! x_1, x_1 ∈ x :: xs ∧ p x_1

Tactic:
by grind

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a b : G
⊢ a * (a⁻¹ * b) = b

Tactic:
rw [← mul_assoc, mul_inv_cancel, one_mul]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a✝ b✝ a b c : G
h : (fun x ↦ a * x) b = (fun x ↦ a * x) c
⊢ a⁻¹ * (a * c) = c

Tactic:
inv_mul_cancel_left

Goal state after:
G : Type u_1
inst✝ : Group G
a✝ b✝ a b c : G
h : (fun x ↦ a * x) b = (fun x ↦ a * x) c
⊢ c = c
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: G : Type u_1
inst✝ : CommGroup G
a b : G
⊢ a⁻¹ * (a * b) = b

Tactic:
inv_mul_cancel_left

Goal state after:
G : Type u_1
inst✝ : CommGroup G
a b : G
⊢ b = b
Module: Mathlib.Logic.Basic

Goal state before:
pp: ⊢ Xor True = Not

Tactic:
by grind

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: ⊢ Xor False = id

Tactic:
by grind

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: a b : Prop
⊢ Xor a b = Xor b a

Tactic:
by grind

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: a : Prop
⊢ Xor a a = False

Tactic:
by grind

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: a b : Prop
⊢ Xor (¬a) b ↔ (a ↔ b)

Tactic:
by grind

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: a b : Prop
⊢ Xor a ¬b ↔ (a ↔ b)

Tactic:
by grind

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: a b : Prop
⊢ Xor (¬a) ¬b ↔ Xor a b

Tactic:
by grind

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: a b : Prop
h : Xor a b
⊢ a ∨ b

Tactic:
by grind

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_3
β : Sort u_4
γ : Sort u_5
f : α → β → γ
P : Prop
inst✝ : Decidable P
x y : α
z : β
⊢ f (if P then x else y) z = if P then f x z else f y z

Tactic:
by grind

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

Goal state before:
pp: α β : Sort u_3
h : α = β
⊢ Bijective h.mp

Tactic:
cases h
  exact ⟨fun _ _ ↦ id, fun x ↦ ⟨x, rfl⟩⟩

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

Goal state before:
pp: α β : Sort u_3
h : α = β
⊢ Bijective h.mpr

Tactic:
cases h
  exact ⟨fun _ _ ↦ id, fun x ↦ ⟨x, rfl⟩⟩

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

Goal state before:
pp: α β : Sort u_3
h : α = β
⊢ Bijective (cast h)

Tactic:
cases h
  exact ⟨fun _ _ ↦ id, fun x ↦ ⟨x, rfl⟩⟩

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case inl
α : Type u_1
r : α → α → Prop
a b : α
hba : r b a
⊢ SymmGen (Function.swap r) a b

Tactic:
exact of_rel hba

Goal state after:
Module: Mathlib.Data.Subtype

Goal state before:
pp: α : Sort u_1
p q : α → Prop
h : ∀ (x : α), p x ↔ q x
a1 : { x // p x }
a2 : { x // q x }
⊢ ∀ (a2' : { x // p x }), a1 ≍ a2' ↔ ↑a1 = ↑a2'

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Subtype

Goal state before:
pp: α β : Sort u_4
p : α → Prop
q : β → Prop
a : { x // p x }
b : { y // q y }
h : α = β
h' : p ≍ q
⊢ a ≍ b ↔ ↑a ≍ ↑b

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Subtype

Goal state before:
pp: α : Sort u_1
p : α → Prop
a : { a // p a }
b : α
⊢ ↑a = b ↔ ∃ h, a = ⟨b, h⟩

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Subtype

Goal state before:
pp: α : Sort u_1
p : α → Prop
a : Subtype p
b : α
⊢ (∃ h, ⟨b, h⟩ = a) ↔ b = ↑a

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Subtype

Goal state before:
pp: α : Sort u_5
β : α → Type u_4
ne : ∀ (a : α), Nonempty (β a)
p : α → Prop
f : (x : Subtype p) → β ↑x
⊢ ((fun f ↦ restrict p f) fun x ↦ if h : p x then f ⟨x, h⟩ else ⋯.some) = f

Tactic:
by grind

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
p : β → β → Prop
f : α → β
h : r ≤ (TransGen p on f)
⊢ TransGen r ≤ (TransGen p on f)

Tactic:
intro _ _ hab

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
p : β → β → Prop
f : α → β
h : r ≤ (TransGen p on f)
i✝¹ i✝ : α
hab : TransGen r i✝¹ i✝
⊢ (TransGen p on f) i✝¹ i✝
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
p : β → β → Prop
f : α → β
h : r ≤ (ReflTransGen p on f)
⊢ ReflTransGen r ≤ (ReflTransGen p on f)

Tactic:
intro _ _ hab

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
p : β → β → Prop
f : α → β
h : r ≤ (ReflTransGen p on f)
i✝¹ i✝ : α
hab : ReflTransGen r i✝¹ i✝
⊢ (ReflTransGen p on f) i✝¹ i✝
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
i✝¹ i✝ : α
h : ReflTransGen r i✝¹ i✝
⊢ EqvGen r i✝¹ i✝

Tactic:
induction h using ReflTransGen.trans_induction_on with
  | refl => exact .refl _
  | trans _ _ h1 h2 => exact _root_.trans h1 h2
  | single h => exact .rel _ _ h

Goal state after:
Module: Mathlib.Algebra.Opposites

Goal state before:
pp: α : Type u_1
inst✝ : Add α
⊢ IsLeftCancelAdd α ∧ IsRightCancelAdd αᵐᵒᵖ ↔ IsLeftCancelAdd α ∧ IsRightCancelAdd α

Tactic:
isRightCancelAdd_iff

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

Goal state before:
pp: α✝ : Sort u
β✝ : Sort v
γ : Sort w
α β : Sort ?u.7
h : α = β
⊢ LeftInverse (cast ⋯) (cast h)

Tactic:
by grind

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

Goal state before:
pp: α✝ : Sort u
β✝ : Sort v
γ : Sort w
α β : Sort ?u.7
h : α = β
⊢ RightInverse (cast ⋯) (cast h)

Tactic:
by grind

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
e : α ≃ β
x : β
y : α
⊢ e.symm x = y ↔ x = e y

Tactic:
by grind

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
e : α ≃ β
x : β
y : α
⊢ y = e.symm x ↔ e y = x

Tactic:
by grind

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

Goal state before:
pp: α : Sort u
β : Sort v
e : α ≃ β
⊢ e.trans (Equiv.refl β) = e

Tactic:
by grind

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

Goal state before:
pp: α : Sort u
β : Sort v
e : α ≃ β
⊢ e.symm.trans e = Equiv.refl β

Tactic:
by grind

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

Goal state before:
pp: α : Sort u
β : Sort v
e : α ≃ β
⊢ e.trans e.symm = Equiv.refl α

Tactic:
by grind

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

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
δ : Sort u_1
ab : α ≃ β
bc : β ≃ γ
cd : γ ≃ δ
⊢ (ab.trans bc).trans cd = ab.trans (bc.trans cd)

Tactic:
by grind

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

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
δ : Sort u_1
ab : α ≃ β
cd : γ ≃ δ
ac : α ≃ γ
⊢ (fun bd ↦ ab.trans (bd.trans cd.symm)) ((fun ac ↦ (ab.symm.trans ac).trans cd) ac) = ac

Tactic:
by grind

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

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
δ : Sort u_1
ab : α ≃ β
cd : γ ≃ δ
ac : β ≃ δ
⊢ (fun ac ↦ (ab.symm.trans ac).trans cd) ((fun bd ↦ ab.trans (bd.trans cd.symm)) ac) = ac

Tactic:
by grind

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
⊢ (Equiv.refl α).equivCongr (Equiv.refl β) = Equiv.refl (α ≃ β)

Tactic:
by grind

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

Goal state before:
pp: α' : Type u_1
β' : Type u_2
e : α' ≃ β'
p p' : Perm α'
⊢ Equiv.trans (e.permCongr p) (e.permCongr p') = e.permCongr (Equiv.trans p p')

Tactic:
by grind

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

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
α₁ : Sort u_1
β₁ : Sort u_2
α₂ : Sort u_3
β₂ : Sort u_4
e₁ : α₁ ≃ α₂
e₂ : β₁ ≃ β₂
f : α₁ → β₁
⊢ (fun f ↦ ⇑e₂.symm ∘ f ∘ ⇑e₁) ((fun f ↦ ⇑e₂ ∘ f ∘ ⇑e₁.symm) f) = f

Tactic:
by grind

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

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
α₁ : Sort u_1
β₁ : Sort u_2
α₂ : Sort u_3
β₂ : Sort u_4
e₁ : α₁ ≃ α₂
e₂ : β₁ ≃ β₂
f : α₂ → β₂
⊢ (fun f ↦ ⇑e₂ ∘ f ∘ ⇑e₁.symm) ((fun f ↦ ⇑e₂.symm ∘ f ∘ ⇑e₁) f) = f

Tactic:
by grind

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

Goal state before:
pp: α₁ : Sort u_1
β₁ : Sort u_2
γ₁ : Sort u_3
α₂ : Sort u_4
β₂ : Sort u_5
γ₂ : Sort u_6
ea : α₁ ≃ α₂
eb : β₁ ≃ β₂
ec : γ₁ ≃ γ₂
f : α₁ → β₁
g : β₁ → γ₁
⊢ (ea.arrowCongr ec) (g ∘ f) = (eb.arrowCongr ec) g ∘ (ea.arrowCongr eb) f

Tactic:
by grind

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

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
β₁ : α → Sort u_1
β₂ : α → Sort u_2
F : (a : α) → β₁ a ≃ β₂ a
⊢ LeftInverse (fun a ↦ ⟨a.fst, (F a.fst).symm a.snd⟩) fun a ↦ ⟨a.fst, (F a.fst) a.snd⟩

Tactic:
by grind

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

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
β₁ : α → Sort u_1
β₂ : α → Sort u_2
F : (a : α) → β₁ a ≃ β₂ a
⊢ RightInverse (fun a ↦ ⟨a.fst, (F a.fst).symm a.snd⟩) fun a ↦ ⟨a.fst, (F a.fst) a.snd⟩

Tactic:
by grind

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

Goal state before:
pp: α✝ : Sort u
β : Sort v
γ : Sort w
α : Type ?u.20
β₁ : α → Type u_1
β₂ : α → Type u_2
F : (a : α) → β₁ a ≃ β₂ a
⊢ LeftInverse (fun a ↦ ⟨a.fst, (F a.fst).symm a.snd⟩) fun a ↦ ⟨a.fst, (F a.fst) a.snd⟩

Tactic:
by grind

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

Goal state before:
pp: α✝ : Sort u
β : Sort v
γ : Sort w
α : Type ?u.20
β₁ : α → Type u_1
β₂ : α → Type u_2
F : (a : α) → β₁ a ≃ β₂ a
⊢ RightInverse (fun a ↦ ⟨a.fst, (F a.fst).symm a.snd⟩) fun a ↦ ⟨a.fst, (F a.fst) a.snd⟩

Tactic:
by grind

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

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
i : Fin 2
⊢ (fun b ↦ bif b then 1 else 0) ((fun i ↦ i == 1) i) = i

Tactic:
by grind

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

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
b : Bool
⊢ (fun i ↦ i == 1) ((fun b ↦ bif b then 1 else 0) b) = b

Tactic:
by grind

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

Goal state before:
pp: α : Type u
β : Type v
x : α ⊕ β
h₁ : x.isLeft = true
h₂ : x.getLeft?.isSome = true
⊢ x.getLeft h₁ = x.getLeft?.get h₂

Tactic:
by grind

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

Goal state before:
pp: α : Type u
β : Type v
x : α ⊕ β
h₁ : x.isRight = true
h₂ : x.getRight?.isSome = true
⊢ x.getRight h₁ = x.getRight?.get h₂

Tactic:
by grind

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

Goal state before:
pp: p : Prop
inst✝ : Decidable p
u : Unit
⊢ _root_.guard p = some u ↔ p

Tactic:
grind [cases Option, _root_.guard]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x : α × β
y : β × α
⊢ x.swap = y ↔ x = y.swap

Tactic:
by grind

Goal state after:
Module: Mathlib.Order.Defs.PartialOrder

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ (b ≤ a ∧ ∀ ⦃c : α⦄, b < c → ¬c < a) = (b ≤ a ∧ ∀ ⦃c : α⦄, c < a → ¬b < c)

Tactic:
by grind

Goal state after:
Module: Mathlib.Order.Defs.PartialOrder

Goal state before:
pp: α : Type u_2
inst✝ : LT α
a b : α
⊢ (b < a ∧ ∀ ⦃c : α⦄, b < c → ¬c < a) = (b < a ∧ ∀ ⦃c : α⦄, c < a → ¬b < c)

Tactic:
by grind

Goal state after:
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
motive : α → Prop
ha : a ≤ b → motive a
hb : b ≤ a → motive b
⊢ motive (min a b)

Tactic:
rw [min_def]; split_ifs with h
  exacts [ha h, hb (le_of_not_ge h)]

Goal state after:
Module: Mathlib.Order.Max

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
a : α
inst✝ : Nontrivial α
ha : IsBot a
ha' : IsMax a
⊢ False

Tactic:
obtain ⟨b, hb⟩ := exists_ne a

Goal state after:
α : Type u_1
inst✝¹ : PartialOrder α
a : α
inst✝ : Nontrivial α
ha : IsBot a
ha' : IsMax a
b : α
hb : b ≠ a
⊢ False
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
x y x' y' : α
ltc : x < y ↔ x' < y'
gtc : y < x ↔ y' < x'
⊢ x = y ↔ x' = y'

Tactic:
by grind

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

Goal state before:
pp: a : Bool
⊢ ((!a) = true) = (a = false)

Tactic:
by grind

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

Goal state before:
pp: a b : Bool
⊢ ((a && b) = false) = (a = false ∨ b = false)

Tactic:
by grind

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

Goal state before:
pp: a b : Bool
⊢ ((a || b) = false) = (a = false ∧ b = false)

Tactic:
by grind

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

Goal state before:
pp: a : Bool
⊢ ((!a) = false) = (a = true)

Tactic:
by grind

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

Goal state before:
pp: b : Bool
⊢ ¬b = true ↔ b = false

Tactic:
by grind

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

Goal state before:
pp: a b : Bool
⊢ (a ^^ b) = true ↔ Xor (a = true) (b = true)

Tactic:
by grind

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

Goal state before:
pp: b : Bool
⊢ b = false ∨ b = true

Tactic:
by grind

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

Goal state before:
pp: a b : Bool
H : b = true
⊢ (a || b) = true

Tactic:
by grind

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

Goal state before:
pp: b : Bool
⊢ (b.toNat == 0) = !b

Tactic:
by grind

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

Goal state before:
pp: case refl
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Injective next
⊢ Injective (leRecOn ⋯ fun {k} ↦ next)

Tactic:
intro x y H

Goal state after:
case refl
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Injective next
x y : C n
H : leRecOn ⋯ (fun {k} ↦ next) x = leRecOn ⋯ (fun {k} ↦ next) y
⊢ x = y
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)
⊢ Injective (leRecOn ⋯ fun {k} ↦ next)

Tactic:
intro x y H

Goal state after:
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 : leRecOn ⋯ (fun {k} ↦ next) x = leRecOn ⋯ (fun {k} ↦ next) y
⊢ x = y
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 : ℕ), Surjective next
m✝ : ℕ
hnm : n.le m✝
ih : Surjective (leRecOn hnm fun {k} ↦ next)
w : C m✝
⊢ ∃ a, leRecOn ⋯ (fun {k} ↦ next) a = next w

Tactic:
obtain ⟨x, rfl⟩ := ih w

Goal state after:
case step
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Surjective next
m✝ : ℕ
hnm : n.le m✝
ih : Surjective (leRecOn hnm fun {k} ↦ next)
x : C n
⊢ ∃ a, leRecOn ⋯ (fun {k} ↦ next) a = next (leRecOn hnm (fun {k} ↦ next) x)
Module: Mathlib.Data.Nat.Basic

Goal state before:
pp: case inr.inl
n : ℕ
h : 0 < n
⊢ n ∣ n - 0 ↔ 0 = 0 ∨ n ≤ 0

pp: case inr.inr
n m : ℕ
h : m < n
hm : m ≠ 0
⊢ n ∣ n - m ↔ m = 0 ∨ n ≤ m

Tactic:
· simp

Goal state after:
case inr.inr
n m : ℕ
h : m < n
hm : m ≠ 0
⊢ n ∣ n - m ↔ m = 0 ∨ n ≤ m
Module: Mathlib.Order.RelClasses

Goal state before:
pp: α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝ : LinearOrder α
⊢ ∀ (a b : α), ¬a < b → ¬b < a → a = b

Tactic:
by grind

Goal state after:
Module: Mathlib.Order.PropInstances

Goal state before:
pp: ⊢ LinearOrder Prop

Tactic:
by
  classical
  exact Lattice.toLinearOrder Prop

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
a b : α
hab : Disjoint a b
⊢ a = b ↔ a = ⊥ ∧ b = ⊥

Tactic:
by grind

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
a b : α
hab : Disjoint a b
⊢ a ≠ b ↔ a ≠ ⊥ ∨ b ≠ ⊥

Tactic:
by grind

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
a b : α
h : a ≤ b
⊢ Disjoint a b ↔ a = ⊥

Tactic:
by grind

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
  exact ⟨fun n ↦ Nat.recOn n a fun _ ↦ g, strictMono_nat_of_lt_succ fun n ↦ hg _, rfl⟩

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

Goal state before:
pp: α : Type u
s t : Set α
⊢ ¬Disjoint s t ↔ ∃ x, x ∈ s ∧ x ∈ t

Tactic:
by grind

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

Goal state before:
pp: α : Type u
s t : Set α
⊢ Disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ t → a ≠ b

Tactic:
by grind

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

Goal state before:
pp: n : ℕ
ih :
  ∀ (m : ℕ),
    m < n →
      ∀ {f : ℕ → ℕ},
        Antitone f →
          (∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)) → f 0 = m → ∃ n, n ≤ m ∧ ∀ (m : ℕ), n ≤ m → f m = f n
f : ℕ → ℕ
hfmono : Antitone f
hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)
h : f 0 = n
heq : ¬f 0 = f 1
hlt : f 1 < f 0
g : ℕ → ℕ := fun i ↦ f (i + 1)
hg_anti : Antitone g
⊢ f 1 < n

Tactic:
by grind

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

Goal state before:
pp: α : Type u
p : Prop
inst✝ : Decidable p
t : ¬p → Set α
x : α
⊢ (x ∈ if h : p then ∅ else t h) ↔ ∃ h, x ∈ t h

Tactic:
by
  simp only [mem_dite, mem_empty_iff_false, imp_false]
  exact ⟨fun h => ⟨h.1, h.2 h.1⟩, fun ⟨h₁, h₂⟩ => ⟨fun h => h₁ h, fun _ => h₂⟩⟩

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

Goal state before:
pp: n : ℕ
ih :
  ∀ (m : ℕ),
    m < n →
      ∀ {f : ℕ → ℕ},
        Antitone f →
          (∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)) → f 0 = m → ∃ n, n ≤ m ∧ ∀ (m : ℕ), n ≤ m → f m = f n
f : ℕ → ℕ
hfmono : Antitone f
hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)
h : f 0 = n
heq : ¬f 0 = f 1
hlt : f 1 < f 0
g : ℕ → ℕ := fun i ↦ f (i + 1)
hg_anti : Antitone g
⊢ ∀ (m : ℕ), g m = g (m + 1) → g (m + 1) = g (m + 2)

Tactic:
by grind

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

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

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
s t : Set α
a : α
⊢ ¬a ∈ s → s ≠ insert a t

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
s : Set α
a : α
⊢ insert a s = s ↔ a ∈ s

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
s : Set α
a : α
⊢ insert a s ≠ s ↔ ¬a ∈ s

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
s t : Set α
a : α
⊢ insert a s ⊆ t ↔ a ∈ t ∧ s ⊆ t

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
s t : Set α
a : α
ha : a ∈ t
hs : s ⊆ t
⊢ insert a s ⊆ t

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
s t : Set α
a : α
h : s ⊆ t
⊢ insert a s ⊆ insert a t

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
s t : Set α
a : α
ha : ¬a ∈ s
⊢ insert a s ⊆ insert a t ↔ s ⊆ t

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
s t : Set α
a : α
ha : ¬a ∈ s
⊢ s ⊆ insert a t ↔ s ⊆ t

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
s t : Set α
⊢ s ⊂ t ↔ ∃ a, ¬a ∈ s ∧ insert a s ⊆ t

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
s t : Set α
a : α
hst : s ⊆ t
hat : a ∈ t
has : ¬a ∈ s
⊢ s ⊂ t

Tactic:
by grind

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

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

Tactic:
by grind

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

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

Tactic:
by grind

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

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

Tactic:
by grind

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

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

Tactic:
by grind

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

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

Tactic:
by grind

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

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

Tactic:
by grind

Goal state after: