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

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

Tactic:
by decide

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

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

Tactic:
by decide

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

Goal state before:
pp: case pos
motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → motive n → motive (Nat.bit b n)
b : Bool
n : Nat
h : bit false 0 zero = zero ∨ (n = 0 → b = true)
h' : Nat.bit b n = 0
⊢ binaryRec zero bit (Nat.bit b n) = bit b n (binaryRec zero bit n)

pp: case neg
motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → motive n → motive (Nat.bit b n)
b : Bool
n : Nat
h : bit false 0 zero = zero ∨ (n = 0 → b = true)
h' : ¬Nat.bit b n = 0
⊢ binaryRec zero bit (Nat.bit b n) = bit b n (binaryRec zero bit n)

Tactic:
case pos =>
    obtain ⟨rfl, rfl⟩ := bit_eq_zero_iff.mp h'
    simp only [Bool.false_eq_true, imp_false, not_true_eq_false, or_false] at h
    unfold binaryRec
    exact h.symm

Goal state after:
case neg
motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → motive n → motive (Nat.bit b n)
b : Bool
n : Nat
h : bit false 0 zero = zero ∨ (n = 0 → b = true)
h' : ¬Nat.bit b n = 0
⊢ binaryRec zero bit (Nat.bit b n) = bit b n (binaryRec zero bit n)
Module: Mathlib.Order.Defs.Unbundled

Goal state before:
pp: α : Sort u_1
r : α → α → Prop
a✝ b✝ c : α
inst✝¹ : DecidableRel r
inst✝ : Trichotomous r
a b : α
⊢ ¬Decidable.decide (r a b) = true → ¬Decidable.decide (r b a) = true → a = b

Tactic:
simpa using trichotomous a b

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

Goal state before:
pp: α : Type u_1
⊢ Subsingleton α → ∀ (x y : α), x = y

Tactic:
intro h

Goal state after:
α : Type u_1
h : Subsingleton α
⊢ ∀ (x y : α), x = y
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Type u
f : α → Type (max u v)
⊢ ¬Surjective f

Tactic:
by
  intro hf
  let T : Type max u v := Sigma f
  cases hf (Set T) with | intro U hU =>
  let g : Set T → T := fun s ↦ ⟨U, cast hU.symm s⟩
  have hg : Injective g := by
    intro s t h
    suffices cast hU (g s).2 = cast hU (g t).2 by
      simp only [g, cast_cast, cast_eq] at this
      assumption
    · congr
  exact cantor_injective g hg

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case tail
α : Type u_1
r : α → α → Prop
motive : {a b : α} → TransGen r a b → Prop
a b : α
single : ∀ {a b : α} (h : r a b), motive ⋯
trans : ∀ {a b c : α} (h₁ : TransGen r a b) (h₂ : TransGen r b c), motive h₁ → motive h₂ → motive ⋯
b✝ c✝ : α
hab : TransGen r a b✝
hbc : r b✝ c✝
h_ih : motive hab
⊢ motive ⋯

Tactic:
exact trans hab (.single hbc) h_ih (single hbc)

Goal state after:
Module: Mathlib.Data.Quot

Goal state before:
pp: α : Sort u_3
r : α → α → Prop
iseqv✝¹ : Equivalence r
p : α → α → Prop
iseqv✝ : Equivalence p
Eq : ∀ (a b : α), { r := r, iseqv := iseqv✝¹ } a b ↔ { r := p, iseqv := iseqv✝ } a b
⊢ { r := r, iseqv := iseqv✝¹ } = { r := p, iseqv := iseqv✝ }

Tactic:
have : r = p := funext fun a ↦ funext fun b ↦ propext <| Eq a b

Goal state after:
α : Sort u_3
r : α → α → Prop
iseqv✝¹ : Equivalence r
p : α → α → Prop
iseqv✝ : Equivalence p
Eq : ∀ (a b : α), { r := r, iseqv := iseqv✝¹ } a b ↔ { r := p, iseqv := iseqv✝ } a b
this : r = p
⊢ { r := r, iseqv := iseqv✝¹ } = { r := p, iseqv := iseqv✝ }
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a b : α
h : Equivalence r
⊢ EqvGen r a b → r a b

Tactic:
intro h

Goal state after:
α : Type u_1
r : α → α → Prop
a b : α
h✝ : Equivalence r
h : EqvGen r a b
⊢ r a b
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α β γ : Sort u_1
h : α = β
h2 : β = γ
x : α
⊢ (Equiv.cast ⋯) x = ((Equiv.cast h).trans (Equiv.cast h2)) x

Tactic:
subst h h2

Goal state after:
α : Sort u_1
x : α
⊢ (Equiv.cast ⋯) x = ((Equiv.cast ⋯).trans (Equiv.cast ⋯)) x
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β : Sort v
f : α ≃ β
g : β ≃ α
⊢ ⇑g ∘ ⇑f = ⇑(Equiv.refl α) ↔ f = g.symm

Tactic:
coe_refl,

Goal state after:
α : Sort u
β : Sort v
f : α ≃ β
g : β ≃ α
⊢ ⇑g ∘ ⇑f = id ↔ f = g.symm
Module: Mathlib.Logic.Equiv.Defs

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

Tactic:
rw [trans_eq_refl_iff_eq_symm]
  exact ⟨fun h ↦ h ▸ rfl, fun h ↦ h ▸ rfl⟩

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

Goal state before:
pp: α : Type u
β : Type v
x : α ⊕ β
a : α
⊢ x = inl a ↔ ∃ h, x.getLeft h = a

Tactic:
cases x

Goal state after:
case inl
α : Type u
β : Type v
a val✝ : α
⊢ inl val✝ = inl a ↔ ∃ h, (inl val✝).getLeft h = a

case inr
α : Type u
β : Type v
a : α
val✝ : β
⊢ inr val✝ = inl a ↔ ∃ h, (inr val✝).getLeft h = a
Module: Mathlib.Data.Sum.Basic

Goal state before:
pp: α : Type u
β : Type v
x : α ⊕ β
b : β
⊢ x = inr b ↔ ∃ h, x.getRight h = b

Tactic:
cases x

Goal state after:
case inl
α : Type u
β : Type v
b : β
val✝ : α
⊢ inl val✝ = inr b ↔ ∃ h, (inl val✝).getRight h = b

case inr
α : Type u
β : Type v
b val✝ : β
⊢ inr val✝ = inr b ↔ ∃ h, (inr val✝).getRight h = b
Module: Mathlib.Logic.IsEmpty.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
⊢ IsEmpty (α ×' β) ↔ IsEmpty α ∨ IsEmpty β

Tactic:
by
  simp only [← not_nonempty_iff, nonempty_pprod, not_and_or]

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 γ
x : α ⊕ β
⊢ Sum.elim (a * a') (b * b') x = (Sum.elim a b * Sum.elim a' b') x

Tactic:
cases x

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

case inr
α : Type u_1
β : Type u_2
γ : Type u_3
a a' : α → γ
b b' : β → γ
inst✝ : Mul γ
val✝ : β
⊢ Sum.elim (a * a') (b * b') (inr val✝) = (Sum.elim a b * Sum.elim a' b') (inr val✝)
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 γ
x : α ⊕ β
⊢ Sum.elim (a / a') (b / b') x = (Sum.elim a b / Sum.elim a' b') x

Tactic:
cases x

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

case inr
α : Type u_1
β : Type u_2
γ : Type u_3
a a' : α → γ
b b' : β → γ
inst✝ : Div γ
val✝ : β
⊢ Sum.elim (a / a') (b / b') (inr val✝) = (Sum.elim a b / Sum.elim a' b') (inr val✝)
Module: Mathlib.Order.Defs.LinearOrder

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

Tactic:
by
  rw [← min_assoc, min_comm a, min_assoc]

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
x y : α × β
h₁ : x.fst < y.fst
h₂ : x.snd ≤ y.snd
⊢ x < y

Tactic:
simp [lt_iff, *]

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
x y : α × β
h₁ : x.fst ≤ y.fst
h₂ : x.snd < y.snd
⊢ x < y

Tactic:
simp [lt_iff, *]

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a₁ a₂ : α
b₁ b₂ : β
h₁ : a₁ < a₂
h₂ : b₁ ≤ b₂
⊢ (a₁, b₁) < (a₂, b₂)

Tactic:
simp [lt_iff, *]

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a₁ a₂ : α
b₁ b₂ : β
h₁ : a₁ ≤ a₂
h₂ : b₁ < b₂
⊢ (a₁, b₁) < (a₂, b₂)

Tactic:
simp [lt_iff, *]

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

Goal state before:
pp: ⊢ ¬true = false

Tactic:
by decide

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

Goal state before:
pp: ⊢ ¬false = true

Tactic:
by decide

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

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

Tactic:
by decide

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

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

Tactic:
by decide

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

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

Tactic:
by decide

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

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

Tactic:
by decide

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

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

Tactic:
by decide

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

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

Tactic:
by decide

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

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

Tactic:
by decide

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

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

Tactic:
by decide

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

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

Tactic:
by decide

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

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

Tactic:
by decide

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

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

Tactic:
by decide

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

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

Tactic:
by decide

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

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

Tactic:
by decide

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

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

Tactic:
by 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:
by 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:
by decide

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

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

Tactic:
by decide

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

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

Tactic:
by decide

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

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

Tactic:
by decide

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

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

Tactic:
by 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:
by decide

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

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

Tactic:
by decide

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

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

Tactic:
by 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:
by 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:
by decide

Goal state after:
Module: Mathlib.Order.PropInstances

Goal state before:
pp: case mp
ι : Type u_1
α' : ι → Type u_3
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
⊢ Disjoint f g → ∀ (i : ι), Disjoint (f i) (g i)

Tactic:
intro h

Goal state after:
case mp
ι : Type u_1
α' : ι → Type u_3
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
h : Disjoint f g
⊢ ∀ (i : ι), Disjoint (f i) (g i)
Module: Mathlib.Order.PropInstances

Goal state before:
pp: case mpr
ι : Type u_1
α' : ι → Type u_3
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
⊢ (∀ (i : ι), Disjoint (f i) (g i)) → Disjoint f g

Tactic:
intro h

Goal state after:
case mpr
ι : Type u_1
α' : ι → Type u_3
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
h : ∀ (i : ι), Disjoint (f i) (g i)
⊢ Disjoint f g
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a b c : α
hab : Disjoint a b
hbc : Codisjoint b c
⊢ a ⊓ (b ⊔ c) ≤ (a ⊔ c) ⊓ (b ⊔ c)

Tactic:
exact inf_le_inf_right _ le_sup_left

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
x y : α × β
⊢ Disjoint x y → Disjoint x.fst y.fst ∧ Disjoint x.snd y.snd

Tactic:
intro h

Goal state after:
case mp
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
x y : α × β
h : Disjoint x y
⊢ Disjoint x.fst y.fst ∧ Disjoint x.snd y.snd
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: f : ℕ → ℕ
b n : ℕ
hfmono : Monotone f
hfb : ∀ (m : ℕ), f m ≤ b
hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)
hbn : b ≤ n
m : ℕ
hmb : m ≤ b
hm : f m = f (m + 1)
key : ∀ (k : ℕ), k ≥ m → f k = f m
⊢ f n = f b

Tactic:
exact (key n (hmb.trans hbn)).trans (key b hmb).symm

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α✝ : Type u
β : Type v
α : Type u_1
inst✝ : Max α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
sup_idem : ∀ (a : α), a ⊔ a = a
a b c : α
hab : a ⊔ b = b
hbc : b ⊔ c = c
⊢ a ⊔ c = c

Tactic:
← hbc,

Goal state after:
α✝ : Type u
β : Type v
α : Type u_1
inst✝ : Max α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
sup_idem : ∀ (a : α), a ⊔ a = a
a b c : α
hab : a ⊔ b = b
hbc : b ⊔ c = c
⊢ a ⊔ (b ⊔ c) = b ⊔ c
Module: Mathlib.Order.Lattice

Goal state before:
pp: α✝ : Type u
β : Type v
α : Type u_1
inst✝ : Min α
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
inf_idem : ∀ (a : α), a ⊓ a = a
c b a : α
hbc : b ⊓ c = c
hab : a ⊓ b = b
⊢ a ⊓ c = c

Tactic:
← hbc,

Goal state after:
α✝ : Type u
β : Type v
α : Type u_1
inst✝ : Min α
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
inf_idem : ∀ (a : α), a ⊓ a = a
c b a : α
hbc : b ⊓ c = c
hab : a ⊓ b = b
⊢ a ⊓ (b ⊓ c) = b ⊓ c
Module: Mathlib.Order.Lattice

Goal state before:
pp: case mp
α : Type u
inst✝ : SemilatticeSup α
a b : α
⊢ a ≤ b → ∃ c, b = a ⊔ c

Tactic:
intro h

Goal state after:
case mp
α : Type u
inst✝ : SemilatticeSup α
a b : α
h : a ≤ b
⊢ ∃ c, b = a ⊔ c
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝ : SemilatticeSup α
a b : α
⊢ a ⊔ b = b ⊔ a

Tactic:
by apply le_antisymm <;> simp

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

Goal state before:
pp: case mp
α : Type u
s : Set α
⊢ Subsingleton ↑s → s.Subsingleton

Tactic:
intro h

Goal state after:
case mp
α : Type u
s : Set α
h : Subsingleton ↑s
⊢ s.Subsingleton
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
e : α ≃ β
inst✝ : PartialOrder β
preorder : Preorder α := e.preorder
⊢ PartialOrder α

Tactic:
apply e.injective.partialOrder <;> intros

Goal state after:
case le
α : Type u
β : Type v
e : α ≃ β
inst✝ : PartialOrder β
preorder : Preorder α := e.preorder
x✝ y✝ : α
⊢ e x✝ ≤ e y✝ ↔ x✝ ≤ y✝

case lt
α : Type u
β : Type v
e : α ≃ β
inst✝ : PartialOrder β
preorder : Preorder α := e.preorder
x✝ y✝ : α
⊢ e x✝ < e y✝ ↔ x✝ < y✝
Module: Mathlib.Order.Heyting.Basic

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

Tactic:
intro h

Goal state after:
α : Type u_2
inst✝¹ : HeytingAlgebra α
a : α
inst✝ : Nontrivial α
h : a = aᶜ
⊢ False
Module: Mathlib.Order.BooleanAlgebra.Set

Goal state before:
pp: α : Type u_1
s : Set α
⊢ sᶜ ∪ s = univ

Tactic:
union_comm,

Goal state after:
α : Type u_1
s : Set α
⊢ s ∪ sᶜ = univ
Module: Mathlib.Order.BooleanAlgebra.Set

Goal state before:
pp: α : Type u_1
a b : α
hab : a ≠ b
⊢ {a, b} \ {b} = {a}

Tactic:
pair_comm,

Goal state after:
α : Type u_1
a b : α
hab : a ≠ b
⊢ {b, a} \ {b} = {a}
Module: Mathlib.Order.BooleanAlgebra.Set

Goal state before:
pp: α : Type u_1
t s s' : Set α
⊢ s ∩ tᶜ ∪ s' ∩ t = s' ∩ t ∪ s \ t

Tactic:
union_comm,

Goal state after:
α : Type u_1
t s s' : Set α
⊢ s' ∩ t ∪ s ∩ tᶜ = s' ∩ t ∪ s \ t
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : HeytingAlgebra β
generalizedHeytingAlgebra : GeneralizedHeytingAlgebra α := e.generalizedHeytingAlgebra
bot : Bot α := e.bot
compl : Compl α := e.compl
⊢ HeytingAlgebra α

Tactic:
apply e.injective.heytingAlgebra <;> intros <;> first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
by 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.12
p : Option α → Type v
h : ∀ (a : p none), False
x : Option α
⊢ ∀ (a : p x), x.isSome = true

Tactic:
cases x

Goal state after:
case none
α✝ : 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.12
p : Option α → Type v
h : ∀ (a : p none), False
⊢ ∀ (a : p none), none.isSome = true

case some
α✝ : 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.12
p : Option α → Type v
h : ∀ (a : p none), False
val✝ : α
⊢ ∀ (a : p (some val✝)), (some val✝).isSome = true
Module: Mathlib.Order.SymmDiff

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

Tactic:
symmDiff_sdiff_left

Goal state after:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
⊢ a \ b = a \ b
Module: Mathlib.Data.Set.Image

Goal state before:
pp: case mp
α : Type u_1
s : Set α
a : α
t : Set α
⊢ t ∈ 𝒫 insert a s → t ∈ 𝒫 s ∪ insert a '' 𝒫 s

Tactic:
intro h

Goal state after:
case mp
α : Type u_1
s : Set α
a : α
t : Set α
h : t ∈ 𝒫 insert a s
⊢ t ∈ 𝒫 s ∪ insert a '' 𝒫 s
Module: Mathlib.Data.Set.Piecewise

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f f' g : α → β
t : Set α
⊢ (∀ ⦃x : α⦄, x ∈ t → s.piecewise f f' x = g x) ↔ ∀ (x : α), (x ∈ t ∩ s → f x = g x) ∧ (x ∈ t ∩ sᶜ → f' x = g x)

Tactic:
refine forall_congr' fun a => ?_

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f f' g : α → β
t : Set α
a : α
⊢ a ∈ t → s.piecewise f f' a = g a ↔ (a ∈ t ∩ s → f a = g a) ∧ (a ∈ t ∩ sᶜ → f' a = g a)
Module: Mathlib.Data.Set.Image

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
⊢ f ⁻¹' s ⊆ f ⁻¹' t → s ⊆ t

Tactic:
intro h

Goal state after:
case mp
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
h : f ⁻¹' s ⊆ f ⁻¹' t
⊢ s ⊆ t
Module: Mathlib.Data.Set.Image

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
⊢ s ⊆ t → f ⁻¹' s ⊆ f ⁻¹' t

Tactic:
intro h

Goal state after:
case mpr
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
h : s ⊆ t
⊢ f ⁻¹' s ⊆ f ⁻¹' t
Module: Mathlib.Data.Set.Image

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

Tactic:
intro h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ f '' s = range fun x ↦ f ↑x

Tactic:
ext
  constructor
  · rintro ⟨x, h1, h2⟩
    exact ⟨⟨x, h1⟩, h2⟩
  · rintro ⟨⟨x, h1⟩, h2⟩
    exact ⟨x, h1, h2⟩

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

Goal state before:
pp: case mpr
α : Type u_1
s t u : Set α
⊢ s ∩ t ⊆ s ∩ u → val ⁻¹' t ⊆ val ⁻¹' u

Tactic:
intro h

Goal state after:
case mpr
α : Type u_1
s t u : Set α
h : s ∩ t ⊆ s ∩ u
⊢ val ⁻¹' t ⊆ val ⁻¹' u
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
i : ι
inst✝ : DecidableEq ι
hi : i ∈ s
f : (j : ι) → α j
a : α i
t : (j : ι) → α j → Set (β j)
⊢ ({x | x i ∈ t i a} ∩ (s \ {i}).pi fun j ↦ t j (update f i a j)) = {x | x i ∈ t i a} ∩ (s \ {i}).pi fun j ↦ t j (f j)

Tactic:
pi_update_of_notMem

Goal state after:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
i : ι
inst✝ : DecidableEq ι
hi : i ∈ s
f : (j : ι) → α j
a : α i
t : (j : ι) → α j → Set (β j)
⊢ ({x | x i ∈ t i a} ∩ (s \ {i}).pi fun j ↦ t j (f j)) = {x | x i ∈ t i a} ∩ (s \ {i}).pi fun j ↦ t j (f j)

case hi
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
i : ι
inst✝ : DecidableEq ι
hi : i ∈ s
f : (j : ι) → α j
a : α i
t : (j : ι) → α j → Set (β j)
⊢ ¬i ∈ s \ {i}
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
g : OneHom N P
f₁ f₂ : OneHom M N
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
x : M
⊢ g (f₁ x) = g (f₂ x)

Tactic:
← OneHom.comp_apply,

Goal state after:
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
g : OneHom N P
f₁ f₂ : OneHom M N
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
x : M
⊢ (g.comp f₁) x = g (f₂ x)
Module: Mathlib.Data.Set.Function

Goal state before:
pp: case mp.inr
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
ht : t.Nonempty
⊢ SurjOn f s t → ∃ s', s' ⊆ s ∧ BijOn f s' t

Tactic:
intro h

Goal state after:
case mp.inr
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
ht : t.Nonempty
h : SurjOn f s t
⊢ ∃ s', s' ⊆ s ∧ BijOn f s' t
Module: Mathlib.Algebra.Group.InjSurj

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
inst✝¹ : Mul M₂
inst✝ : CommMagma M₁
f : M₁ → M₂
hf : Surjective f
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x y : M₁
⊢ f x * f y = f y * f x

Tactic:
by rw [← mul, ← mul, mul_comm]

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

Goal state before:
pp: case inl
α : 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
rab : r a b
⊢ f a c = f a b * f b c

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
⊢ f a c = f a b * f b c

Tactic:
· exact hmul rab rbc pab pbc pac

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 c = f a b * f b c
Module: Mathlib.Algebra.Group.Units.Defs

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

Tactic:
simp only [HPow.hPow, Pow.pow]; simp [pow_succ]

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

Goal state before:
pp: M₀ : Type u_1
M₀' : Type u_2
inst✝¹ : MulZeroOneClass M₀
inst✝ : Nontrivial M₀
⊢ 1 ≠ 0

Tactic:
intro h

Goal state after:
M₀ : Type u_1
M₀' : Type u_2
inst✝¹ : MulZeroOneClass M₀
inst✝ : Nontrivial M₀
h : 1 = 0
⊢ False