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

Goal state before:
pp: case zero
b : Bool
⊢ bit b 0 = 0 ↔ 0 = 0 ∧ b = false

Tactic:
cases b

Goal state after:
case zero.false
⊢ bit false 0 = 0 ↔ 0 = 0 ∧ false = false

case zero.true
⊢ bit true 0 = 0 ↔ 0 = 0 ∧ true = false
Module: Mathlib.Data.Nat.BinaryRec

Goal state before:
pp: case succ
b : Bool
n✝ : Nat
⊢ bit b (n✝ + 1) = 0 ↔ n✝ + 1 = 0 ∧ b = false

Tactic:
cases b

Goal state after:
case succ.false
n✝ : Nat
⊢ bit false (n✝ + 1) = 0 ↔ n✝ + 1 = 0 ∧ false = false

case succ.true
n✝ : Nat
⊢ bit true (n✝ + 1) = 0 ↔ n✝ + 1 = 0 ∧ true = false
Module: Mathlib.Data.Nat.BinaryRec

Goal state before:
pp: b : Bool
x n : Nat
⊢ bit b x < 2 ^ (n + 1) ↔ x < 2 ^ n

Tactic:
cases b

Goal state after:
case false
x n : Nat
⊢ bit false x < 2 ^ (n + 1) ↔ x < 2 ^ n

case true
x n : Nat
⊢ bit true x < 2 ^ (n + 1) ↔ x < 2 ^ n
Module: Mathlib.Data.Nat.BinaryRec

Goal state before:
pp: case zero
motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → (n = 0 → b = true) → motive n → motive (Nat.bit b n)
b : Bool
ih : motive 0
h : ¬(0 = 0 → b = true)
⊢ 0 = 0 ∧ b = false

Tactic:
cases b

Goal state after:
case zero.false
motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → (n = 0 → b = true) → motive n → motive (Nat.bit b n)
ih : motive 0
h : ¬(0 = 0 → false = true)
⊢ 0 = 0 ∧ false = false

case zero.true
motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → (n = 0 → b = true) → motive n → motive (Nat.bit b n)
ih : motive 0
h : ¬(0 = 0 → true = true)
⊢ 0 = 0 ∧ true = false
Module: Mathlib.Data.Nat.BinaryRec

Goal state before:
pp: case succ
motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → (n = 0 → b = true) → motive n → motive (Nat.bit b n)
b : Bool
n✝ : Nat
ih : motive (n✝ + 1)
h : ¬(n✝ + 1 = 0 → b = true)
⊢ n✝ + 1 = 0 ∧ b = false

Tactic:
cases b

Goal state after:
case succ.false
motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → (n = 0 → b = true) → motive n → motive (Nat.bit b n)
n✝ : Nat
ih : motive (n✝ + 1)
h : ¬(n✝ + 1 = 0 → false = true)
⊢ n✝ + 1 = 0 ∧ false = false

case succ.true
motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → (n = 0 → b = true) → motive n → motive (Nat.bit b n)
n✝ : Nat
ih : motive (n✝ + 1)
h : ¬(n✝ + 1 = 0 → true = true)
⊢ n✝ + 1 = 0 ∧ true = false
Module: Mathlib.Data.Nat.BinaryRec

Goal state before:
pp: b : Bool
n : Nat
⊢ bit b n = 2 * n + b.toNat

Tactic:
cases b

Goal state after:
case false
n : Nat
⊢ bit false n = 2 * n + false.toNat

case true
n : Nat
⊢ bit true n = 2 * n + true.toNat
Module: Mathlib.Data.Nat.BinaryRec

Goal state before:
pp: b : Bool
n : Nat
⊢ b.toNat < 2

Tactic:
cases b

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

case true
n : Nat
⊢ true.toNat < 2
Module: Mathlib.Data.Nat.BinaryRec

Goal state before:
pp: b : Bool
n : Nat
⊢ bit b n % 2 = b.toNat

Tactic:
cases b

Goal state after:
case false
n : Nat
⊢ bit false n % 2 = false.toNat

case true
n : Nat
⊢ bit true n % 2 = true.toNat
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
k : ℕ
m : M
⊢ npowRec (k + 1) m = 1 * npowRec' (k + 1) m

Tactic:
induction k using Nat.strongRecOn with
  | ind k' ih =>
    match k' with
    | 0 => rfl
    | k + 1 =>
      rw [npowRec, npowRec'_succ k.succ_ne_zero, ← mul_assoc]
      congr
      simp [ih]

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

Goal state before:
pp: case bit
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
k : ℕ
b : Bool
k' : ℕ
k'0 : k' ≠ 0
ih :
  ∀ (m n : M),
    k' ≠ 0 →
      Nat.binaryRec (motive := fun x ↦ M → M → M) (fun y x ↦ y)
          (fun bn _n fn y x ↦ fn (bif bn then y * x else y) (x * x)) k' m n =
        m * npowRec' k' n
m n : M
hk : Nat.bit b k' ≠ 0
⊢ (bif b then m * n else m) * npowRec' k' (n * n) = m * npowRec' (Nat.bit b k') n

Tactic:
cases b

Goal state after:
case bit.false
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
k k' : ℕ
k'0 : k' ≠ 0
ih :
  ∀ (m n : M),
    k' ≠ 0 →
      Nat.binaryRec (motive := fun x ↦ M → M → M) (fun y x ↦ y)
          (fun bn _n fn y x ↦ fn (bif bn then y * x else y) (x * x)) k' m n =
        m * npowRec' k' n
m n : M
hk : Nat.bit false k' ≠ 0
⊢ (bif false then m * n else m) * npowRec' k' (n * n) = m * npowRec' (Nat.bit false k') n

case bit.true
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
k k' : ℕ
k'0 : k' ≠ 0
ih :
  ∀ (m n : M),
    k' ≠ 0 →
      Nat.binaryRec (motive := fun x ↦ M → M → M) (fun y x ↦ y)
          (fun bn _n fn y x ↦ fn (bif bn then y * x else y) (x * x)) k' m n =
        m * npowRec' k' n
m n : M
hk : Nat.bit true k' ≠ 0
⊢ (bif true then m * n else m) * npowRec' k' (n * n) = m * npowRec' (Nat.bit true k') n
Module: Mathlib.Logic.Function.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
f : α → β
I : Injective f
a b : α
⊢ (f a == f b) = (a == b)

Tactic:
by_cases h : a == b

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
f : α → β
I : Injective f
a b : α
h : (a == b) = true
⊢ (f a == f b) = (a == b)

case neg
α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
f : α → β
I : Injective f
a b : α
h : ¬(a == b) = true
⊢ (f a == f b) = (a == b)
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a : G
⊢ a / a = 1

Tactic:
rw [div_eq_mul_inv, mul_inv_cancel a]

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
f : α → β
inst✝ : Subsingleton α
g : α → β
x y : α
⊢ f x = g y ↔ f = g

Tactic:
refine ⟨fun h ↦ funext fun z ↦ ?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
α : Sort u_1
β : Sort u_2
f : α → β
inst✝ : Subsingleton α
g : α → β
x y : α
h : f x = g y
z : α
⊢ f z = g z

case refine_2
α : Sort u_1
β : Sort u_2
f : α → β
inst✝ : Subsingleton α
g : α → β
x y : α
h : f = g
⊢ f x = g y
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: ι : Sort u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
β : ι → Sort u_3
f : (i : ι) → α i → β i
g : (i : ι) → α i
i : ι
a : α i
j : ι
⊢ Pi.map f (update g i a) j = update (Pi.map f g) i (f i a) j

Tactic:
obtain rfl | hij := eq_or_ne j i

Goal state after:
case inl
ι : Sort u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
β : ι → Sort u_3
f : (i : ι) → α i → β i
g : (i : ι) → α i
j : ι
a : α j
⊢ Pi.map f (update g j a) j = update (Pi.map f g) j (f j a) j

case inr
ι : Sort u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
β : ι → Sort u_3
f : (i : ι) → α i → β i
g : (i : ι) → α i
i : ι
a : α i
j : ι
hij : j ≠ i
⊢ Pi.map f (update g i a) j = update (Pi.map f g) i (f i a) j
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a b : α
h : ∀ (b : α), ¬r a b
⊢ ReflTransGen r a b ↔ b = a

Tactic:
cases_head_iff

Goal state after:
α : Type u_1
r : α → α → Prop
a b : α
h : ∀ (b : α), ¬r a b
⊢ (a = b ∨ ∃ c, r a c ∧ ReflTransGen r c b) ↔ b = a
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
  cases x <;> rfl

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✝ : Div γ
⊢ Sum.elim (a / a') (b / b') = Sum.elim a b / Sum.elim a' b'

Tactic:
ext x
  cases x <;> rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty β
inst✝ : Nonempty δ
f₁ : α → β
g₁ : γ → δ
f₂ : β → α
g₂ : δ → γ
h : LeftInverse (map f₁ g₁) (map f₂ g₂)
b : β
inhabited_h : Inhabited δ
⊢ f₁ (f₂ b) = b

Tactic:
exact congr_arg Prod.fst (h (b, default))

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a✝ b✝ c a b : α
⊢ compare a b = (compare b a).swap

Tactic:
by
    cases _ : compare b a <;>
      simp_all [Ordering.swap, compare_eq_iff_eq, compare_lt_iff_lt, compare_gt_iff_gt]

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
A_le A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), A_le a a
le_trans✝¹ : ∀ (a b c : α), A_le a b → A_le b c → A_le a c
lt_iff_le_not_ge✝¹ : ∀ (a b : α), A_lt a b ↔ A_le a b ∧ ¬A_le b a
le_antisymm✝¹ : ∀ (a b : α), A_le a b → A_le b a → a = b
A_min A_max : α → α → α
A_compare : α → α → Ordering
le_total✝¹ : ∀ (a b : α), A_le a b ∨ A_le b a
A_decidableLE : DecidableLE α
A_decidableEq : DecidableEq α
A_decidableLT : DecidableLT α
A_min_def : ∀ (a b : α), A_min a b = if A_le a b then a else b
A_max_def : ∀ (a b : α), A_max a b = if A_le a b then b else a
A_compare_canonical : ∀ (a b : α), A_compare a b = compareOfLessAndEq a b
B_min B_max : α → α → α
B_compare : α → α → Ordering
le_refl✝ : ∀ (a : α), A_le a a
le_trans✝ : ∀ (a b c : α), A_le a b → A_le b c → A_le a c
le_antisymm✝ : ∀ (a b : α), A_le a b → A_le b a → a = b
le_total✝ : ∀ (a b : α), A_le a b ∨ A_le b a
lt_iff_le_not_ge✝ : ∀ (a b : α), A_lt a b ↔ A_le a b ∧ ¬A_le b a
B_min_def : ∀ (a b : α), B_min a b = if A_le a b then a else b
B_max_def : ∀ (a b : α), B_max a b = if A_le a b then b else a
B_compare_canonical : ∀ (a b : α), B_compare a b = compareOfLessAndEq a b
a b : α
⊢ A_min a b = B_min a b

Tactic:
exact (A_min_def _ _).trans (B_min_def _ _).symm

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

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

Tactic:
cases b

Goal state after:
case false
⊢ (false.toNat == 1) = false

case true
⊢ (true.toNat == 1) = true
Module: Mathlib.Data.Nat.Init

Goal state before:
pp: m n : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
h1 : n ≤ m
h2 : n ≤ m + 1
| leRec refl le_succ_of_le h2 = le_succ_of_le h1 (leRec refl le_succ_of_le h1)

Tactic:
conv =>

Goal state after:
m n : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
h1 : n ≤ m
h2 : n ≤ m + 1
| le_succ_of_le h1 (leRec refl le_succ_of_le h1)
Module: Mathlib.Data.Nat.Init

Goal state before:
pp: case step
n m k : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
hnm : n ≤ m
m✝ : ℕ
hmk : m.le m✝
ih : leRec refl le_succ_of_le ⋯ = leRec (leRec refl (fun x h ↦ le_succ_of_le h) hnm) (fun x h ↦ le_succ_of_le ⋯) hmk
⊢ le_succ_of_le ⋯ (leRec refl le_succ_of_le ⋯) =
    leRec (leRec refl (fun x h ↦ le_succ_of_le h) hnm) (fun x h ↦ le_succ_of_le ⋯) ⋯

Tactic:
ih,

Goal state after:
case step
n m k : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
hnm : n ≤ m
m✝ : ℕ
hmk : m.le m✝
ih : leRec refl le_succ_of_le ⋯ = leRec (leRec refl (fun x h ↦ le_succ_of_le h) hnm) (fun x h ↦ le_succ_of_le ⋯) hmk
⊢ le_succ_of_le ⋯ (leRec (leRec refl (fun x h ↦ le_succ_of_le h) hnm) (fun x h ↦ le_succ_of_le ⋯) hmk) =
    leRec (leRec refl (fun x h ↦ le_succ_of_le h) hnm) (fun x h ↦ le_succ_of_le ⋯) ⋯
Module: Mathlib.Data.Nat.Init

Goal state before:
pp: n : ℕ
motive : (m : ℕ) → m ≤ n + 1 → Sort u_1
of_succ : (k : ℕ) → (h : k < n + 1) → motive (k + 1) h → motive k ⋯
self : motive (n + 1) ⋯
⊢ decreasingInduction of_succ self ⋯ = of_succ n ⋯ self

Tactic:
dsimp only [decreasingInduction]; rw [leRec_succ']

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

Goal state before:
pp: case step
m n k : ℕ
hmn : m ≤ n
m✝ : ℕ
hnk : n.le m✝
ih :
  ∀ {motive : (m : ℕ) → m ≤ m✝ → Sort u_1} (of_succ : (k : ℕ) → (h : k < m✝) → motive (k + 1) h → motive k ⋯)
    (self : motive m✝ ⋯),
    decreasingInduction of_succ self ⋯ =
      decreasingInduction (fun x x_1 ↦ of_succ x ⋯) (decreasingInduction of_succ self hnk) hmn
motive : (m : ℕ) → m ≤ m✝.succ → Sort u_1
of_succ : (k : ℕ) → (h : k < m✝.succ) → motive (k + 1) h → motive k ⋯
self : motive m✝.succ ⋯
⊢ decreasingInduction (fun x x_1 ↦ of_succ x ⋯) (of_succ m✝ ⋯ self) ⋯ =
    decreasingInduction (fun x x_1 ↦ of_succ x ⋯) (decreasingInduction of_succ self ⋯) hmn

Tactic:
ih,

Goal state after:
case step
m n k : ℕ
hmn : m ≤ n
m✝ : ℕ
hnk : n.le m✝
ih :
  ∀ {motive : (m : ℕ) → m ≤ m✝ → Sort u_1} (of_succ : (k : ℕ) → (h : k < m✝) → motive (k + 1) h → motive k ⋯)
    (self : motive m✝ ⋯),
    decreasingInduction of_succ self ⋯ =
      decreasingInduction (fun x x_1 ↦ of_succ x ⋯) (decreasingInduction of_succ self hnk) hmn
motive : (m : ℕ) → m ≤ m✝.succ → Sort u_1
of_succ : (k : ℕ) → (h : k < m✝.succ) → motive (k + 1) h → motive k ⋯
self : motive m✝.succ ⋯
⊢ decreasingInduction (fun x x_1 ↦ of_succ x ⋯) (decreasingInduction (fun x x_1 ↦ of_succ x ⋯) (of_succ m✝ ⋯ self) hnk)
      hmn =
    decreasingInduction (fun x x_1 ↦ of_succ x ⋯) (decreasingInduction of_succ self ⋯) hmn
Module: Mathlib.Data.Set.Basic

Goal state before:
pp: α : Type u
s : Set α
inst✝ : Subsingleton α
⊢ s.Nonempty → s = univ

Tactic:
by
  rintro ⟨x, hx⟩
  exact eq_univ_of_forall fun y => by rwa [Subsingleton.elim y x]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝ : LinearOrder α
a b : α
p : α → Prop
ha : p a
hb : p b
h : b ≤ a
⊢ p (max a b)

Tactic:
sup_eq_left.2 h

Goal state after:
α : Type u
inst✝ : LinearOrder α
a b : α
p : α → Prop
ha : p a
hb : p b
h : b ≤ a
⊢ p a
Module: Mathlib.Order.Heyting.Basic

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

Tactic:
cases le_compl_self.1 (le_of_eq h)

Goal state after:
case refl
α : Type u_2
inst✝¹ : HeytingAlgebra α
inst✝ : Nontrivial α
h : ⊥ = ⊥ᶜ
⊢ False
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
rw [← inf_inf_sdiff, sup_inf_sdiff]

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

Goal state before:
pp: case some.some
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x val✝¹ : α
h1 : e.symm (some (e.removeNoneAux x)) = some val✝¹
val✝ : β
h2 : e (some x) = some val✝
⊢ some (e.symm.removeNoneAux (e.removeNoneAux x)) = some x

Tactic:
removeNoneAux_some _ ⟨_, h1⟩

Goal state after:
case some.some
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x val✝¹ : α
h1 : e.symm (some (e.removeNoneAux x)) = some val✝¹
val✝ : β
h2 : e (some x) = some val✝
⊢ e.symm (some (e.removeNoneAux x)) = some x
Module: Mathlib.Logic.Equiv.Option

Goal state before:
pp: case some
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
x : β
e : α ≃ { y // y ≠ x }
a : α
⊢ (if ↑(e a) = x then none else some a) = some a

Tactic:
exact if_neg (e a).property

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
x : β
e : { e // e none = x }
b : { y // y ≠ x }
⊢ some (((optionSubtype x) e).symm b) = (↑e).symm ↑b

Tactic:
by
  dsimp only [optionSubtype]
  simp

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
| x ⊓ y \ z ⊓ x \ y

Tactic:
rw [← inf_sdiff_left]

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
| x ⊓ (y \ z ⊓ y) ⊓ x \ y
Module: Mathlib.Logic.Equiv.Sum

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
b : Bool
⊢ Sum.elim (fun x ↦ false) (fun x ↦ true) ((fun b ↦ Bool.casesOn b (inl PUnit.unit) (inr PUnit.unit)) b) = b

Tactic:
cases b

Goal state after:
case false
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
⊢ Sum.elim (fun x ↦ false) (fun x ↦ true) ((fun b ↦ Bool.casesOn b (inl PUnit.unit) (inr PUnit.unit)) false) = false

case true
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
⊢ Sum.elim (fun x ↦ false) (fun x ↦ true) ((fun b ↦ Bool.casesOn b (inl PUnit.unit) (inr PUnit.unit)) true) = true
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
rw [← h, sdiff_sdiff_eq_self hy]

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

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

Tactic:
intro x_in_u x_in_v

Goal state after:
case mp
α : Type u_1
s u v : Set α
hsuv : s ⊆ u ∪ v
H : s ∩ (u ∩ v) = ∅
x : α
x_in_s : x ∈ s
x_in_u : ⟨x, x_in_s⟩ ∈ Subtype.val ⁻¹' u
x_in_v : ⟨x, x_in_s⟩ ∈ Subtype.val ⁻¹' v
⊢ False
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Set γ
f : α → γ
g : β → γ
⊢ Sum.elim f g ⁻¹' s = Sum.inl '' f ⁻¹' s ∪ Sum.inr '' g ⁻¹' s

Tactic:
by
  ext (_ | _) <;> simp

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

Goal state before:
pp: ι : Type u_8
α : ι → Type u_9
s : Set ι
t t' : (i : ι) → Set (α i)
inst✝ : (x : ι) → Decidable (x ∈ s)
⊢ univ.pi (s.piecewise t t') = s.pi t ∩ sᶜ.pi t'

Tactic:
by
  simp [compl_eq_univ_sdiff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s s₁ s₂ : Set α
f : α → β
h : InjOn f s
h₁ : s₁ ⊆ s
h₂ : s₂ ⊆ s
⊢ f '' s₁ ⊆ f '' s₂ ↔ s₁ ⊆ s₂

Tactic:
refine ⟨fun h' ↦ ?_, image_mono⟩
  rw [← h.preimage_image_inter h₁, ← h.preimage_image_inter h₂]
  exact inter_subset_inter_left _ (preimage_mono h')

Goal state after:
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 : z ≤ b
| cast ⋯
      (match z - 1 - b with
      | ofNat n => inductionOn'.pos b zero succ n
      | -[n+1] => inductionOn'.neg b zero pred n) =
    pred z hz
      (cast ⋯
        (match z - b with
        | ofNat n => inductionOn'.pos b zero succ n
        | -[n+1] => inductionOn'.neg b zero pred n))

Tactic:
conv =>

Goal state after:
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 : z ≤ b
| cast ⋯
    (match z - 1 - b with
    | ofNat n => inductionOn'.pos b zero succ n
    | -[n+1] =>
      match n with
      | 0 => pred b ⋯ zero
      | n.succ => cast ⋯ (pred (b + -[n+1]) ⋯ (inductionOn'.neg b zero pred n)))
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝² : Monoid β
p r : α → α → Prop
inst✝¹ : Std.Total r
f : α → α → β
inst✝ : Std.Symm p
hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c
a b✝ c✝ : α
pab✝ : p a b✝
pbc✝ : p b✝ c✝
pac✝ : p a c✝
b c : α
rbc : r b c
pab : p a b
pbc : p b c
pac : p a c
rba : r b a
⊢ 1 * f a c = f a b * f b c

Tactic:
← hf_swap pab,

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝² : Monoid β
p r : α → α → Prop
inst✝¹ : Std.Total r
f : α → α → β
inst✝ : Std.Symm p
hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c
a b✝ c✝ : α
pab✝ : p a b✝
pbc✝ : p b✝ c✝
pac✝ : p a c✝
b c : α
rbc : r b c
pab : p a b
pbc : p b c
pac : p a c
rba : r b a
⊢ f a b * f b a * f a c = f a b * f b c
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: α : Type u
inst✝ : DivisionMonoid α
b : α
h : IsUnit b
a : α
⊢ a * b⁻¹ * b = a

Tactic:
h.inv_mul_cancel_right

Goal state after:
α : Type u
inst✝ : DivisionMonoid α
b : α
h : IsUnit b
a : α
⊢ a = a
Module: Mathlib.Control.Basic

Goal state before:
pp: m : Type u → Type v
h : Applicative m
inst✝ : CommApplicative m
α β γ : Type u
a : m α
b : m β
f : α → β → γ
⊢ (fun p ↦ f p.fst p.snd) <$> (Prod.mk <$> a <*> b) = (fun b a ↦ f a b) <$> b <*> a

Tactic:
rw [@CommApplicative.commutative_prod m h]
      simp [map_seq, map_map]
      rfl

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

Goal state before:
pp: case pos
M₀ : Type u_1
inst✝¹ : MulZeroClass M₀
inst✝ : IsLeftCancelMulZero M₀
a b c : M₀
ha : a = 0
⊢ a * b = a * c ↔ b = c ∨ a = 0

Tactic:
simp only [ha, zero_mul, or_true]

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

Goal state before:
pp: case succ
α : Type u_4
p : α → Prop
f : Perm α
hf : ∀ (x : α), p (f x) ↔ p x
n : ℕ
ih : f.subtypePerm hf ^ n = (f ^ n).subtypePerm ⋯
⊢ f.subtypePerm hf * f.subtypePerm hf ^ n = (f * f ^ n).subtypePerm ⋯

Tactic:
ih,

Goal state after:
case succ
α : Type u_4
p : α → Prop
f : Perm α
hf : ∀ (x : α), p (f x) ↔ p x
n : ℕ
ih : f.subtypePerm hf ^ n = (f ^ n).subtypePerm ⋯
⊢ f.subtypePerm hf * (f ^ n).subtypePerm ⋯ = (f * f ^ n).subtypePerm ⋯
Module: Mathlib.Data.Nat.Cast.Defs

Goal state before:
pp: case succ
R : Type u_1
inst✝ : AddMonoidWithOne R
m n : ℕ
ih : ↑(m + n) = ↑m + ↑n
⊢ ↑(m + n) + 1 = ↑m + ↑(n + 1)

Tactic:
ih,

Goal state after:
case succ
R : Type u_1
inst✝ : AddMonoidWithOne R
m n : ℕ
ih : ↑(m + n) = ↑m + ↑n
⊢ ↑m + ↑n + 1 = ↑m + ↑(n + 1)
Module: Mathlib.Data.Nat.Cast.Defs

Goal state before:
pp: case ind.succ
R : Type u_1
inst✝ : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → m.binCast = ↑m
⊢ (if (k + 1) % 2 = 0 then ((k + 1) / 2).binCast + ((k + 1) / 2).binCast
    else ((k + 1) / 2).binCast + ((k + 1) / 2).binCast + 1) =
    ↑(k + 1)

Tactic:
by_cases h : (k + 1) % 2 = 0

Goal state after:
case pos
R : Type u_1
inst✝ : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → m.binCast = ↑m
h : (k + 1) % 2 = 0
⊢ (if (k + 1) % 2 = 0 then ((k + 1) / 2).binCast + ((k + 1) / 2).binCast
    else ((k + 1) / 2).binCast + ((k + 1) / 2).binCast + 1) =
    ↑(k + 1)

case neg
R : Type u_1
inst✝ : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → m.binCast = ↑m
h : ¬(k + 1) % 2 = 0
⊢ (if (k + 1) % 2 = 0 then ((k + 1) / 2).binCast + ((k + 1) / 2).binCast
    else ((k + 1) / 2).binCast + ((k + 1) / 2).binCast + 1) =
    ↑(k + 1)
Module: Mathlib.Data.Nat.Cast.Defs

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → m.binCast = ↑m
h : (k + 1) % 2 = 0
| (if (k + 1) % 2 = 0 then ((k + 1) / 2).binCast + ((k + 1) / 2).binCast
    else ((k + 1) / 2).binCast + ((k + 1) / 2).binCast + 1) =
    ↑(k + 1)

Tactic:
conv =>

Goal state after:
R : Type u_1
inst✝ : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → m.binCast = ↑m
h : (k + 1) % 2 = 0
| ↑((k + 1) % 2 + 2 * ((k + 1) / 2))
Module: Mathlib.Data.Nat.Cast.Defs

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → m.binCast = ↑m
h : ¬(k + 1) % 2 = 0
| (if (k + 1) % 2 = 0 then ((k + 1) / 2).binCast + ((k + 1) / 2).binCast
    else ((k + 1) / 2).binCast + ((k + 1) / 2).binCast + 1) =
    ↑(k + 1)

Tactic:
conv =>

Goal state after:
R : Type u_1
inst✝ : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → m.binCast = ↑m
h : ¬(k + 1) % 2 = 0
| ↑((k + 1) % 2 + 2 * ((k + 1) / 2))
Module: Mathlib.Data.Int.Cast.Basic

Goal state before:
pp: case succ
R : Type u
inst✝ : AddGroupWithOne R
m n n✝ : ℕ
e : n - m = n✝ + 1
⊢ -(↑n - ↑m) = ↑m - ↑n

Tactic:
neg_sub

Goal state after:
case succ
R : Type u
inst✝ : AddGroupWithOne R
m n n✝ : ℕ
e : n - m = n✝ + 1
⊢ ↑m - ↑n = ↑m - ↑n
Module: Mathlib.Algebra.Ring.Defs

Goal state before:
pp: case succ
α : Type u
inst✝ : NonAssocSemiring α
a : α
n : ℕ
ih : n • a = ↑n * a
⊢ n • a + a = ↑(n + 1) * a

Tactic:
ih,

Goal state after:
case succ
α : Type u
inst✝ : NonAssocSemiring α
a : α
n : ℕ
ih : n • a = ↑n * a
⊢ ↑n * a + a = ↑(n + 1) * a
Module: Mathlib.Algebra.Group.Nat.Even

Goal state before:
pp: case inl
m n : ℕ
h₁ : m % 2 = 0
⊢ Even (m * n) ↔ Even m ∨ Even n

Tactic:
rcases mod_two_eq_zero_or_one n with h₂ | h₂

Goal state after:
case inl.inl
m n : ℕ
h₁ : m % 2 = 0
h₂ : n % 2 = 0
⊢ Even (m * n) ↔ Even m ∨ Even n

case inl.inr
m n : ℕ
h₁ : m % 2 = 0
h₂ : n % 2 = 1
⊢ Even (m * n) ↔ Even m ∨ Even n