mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Defs.Unbundled

Goal state before:
pp: case inl
α : Sort u_1
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : Std.Trichotomous r
a b c : α
h₁ : ¬r b a
h₂ : r b c
h₃ : r a b
⊢ r a c

Tactic:
exact _root_.trans h₃ h₂

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

Goal state before:
pp: case inr.inr
α : Sort u_1
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : Std.Trichotomous r
a b c : α
h₁ : r a b
h₂ : ¬r c b
h₃ : r c b
⊢ r a c

Tactic:
· exact absurd h₃ h₂

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

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

Tactic:
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: M : Type u_2
inst✝ : Monoid M
a : M
⊢ a ^ 2 * a = a * a * a

Tactic:
pow_two

Goal state after:
M : Type u_2
inst✝ : Monoid M
a : M
⊢ a * a * a = a * a * a
Module: Mathlib.Algebra.Group.Defs

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

Tactic:
pow_two

Goal state after:
M : Type u_2
inst✝ : Monoid M
a : M
⊢ a * (a * a) = a * (a * a)
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
w : α
hp : p w
hq : q w hp
H : ∀ (y : α) (hy : p y), q y hy → y = w
⊢ ∃! x, ∃! hx, q x hx

Tactic:
by
  simp only [existsUnique_iff_exists]
  exact ExistsUnique.intro w ⟨hp, hq⟩ fun y ⟨hyp, hyq⟩ ↦ H y hyp hyq

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

Goal state before:
pp: G : Type u_1
inst✝ : DivInvMonoid G
a : G
⊢ a ^ 2 = a * a

Tactic:
pow_two

Goal state after:
G : Type u_1
inst✝ : DivInvMonoid G
a : G
⊢ a * a = a * a
Module: Mathlib.Logic.Nontrivial.Defs

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Nontrivial (α → β)
f g : α → β
h : ¬∀ (x : α), f x = g x
⊢ Nontrivial β

Tactic:
Classical.not_forall

Goal state after:
α : Type u_3
β : Type u_4
inst✝ : Nontrivial (α → β)
f g : α → β
h : ∃ x, ¬f x = g x
⊢ Nontrivial β
Module: Mathlib.Logic.Basic

Goal state before:
pp: case pos
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
hp : P
⊢ (if P ∧ Q then a else b) = if P then if Q then a else b else b

Tactic:
by_cases hq : Q

Goal state after:
case pos
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
hp : P
hq : Q
⊢ (if P ∧ Q then a else b) = if P then if Q then a else b else b

case neg
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
hp : P
hq : ¬Q
⊢ (if P ∧ Q then a else b) = if P then if Q then a else b else b
Module: Mathlib.Logic.Basic

Goal state before:
pp: case neg
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
hp : ¬P
⊢ (if P ∧ Q then a else b) = if P then if Q then a else b else b

Tactic:
by_cases hq : Q

Goal state after:
case pos
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
hp : ¬P
hq : Q
⊢ (if P ∧ Q then a else b) = if P then if Q then a else b else b

case neg
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
hp : ¬P
hq : ¬Q
⊢ (if P ∧ Q then a else b) = if P then if Q then a else b else b
Module: Mathlib.Logic.Basic

Goal state before:
pp: case pos
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
hp : P
⊢ (if P ∨ Q then a else b) = if P then a else if Q then a else b

Tactic:
by_cases hq : Q

Goal state after:
case pos
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
hp : P
hq : Q
⊢ (if P ∨ Q then a else b) = if P then a else if Q then a else b

case neg
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
hp : P
hq : ¬Q
⊢ (if P ∨ Q then a else b) = if P then a else if Q then a else b
Module: Mathlib.Logic.Basic

Goal state before:
pp: case neg
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
hp : ¬P
⊢ (if P ∨ Q then a else b) = if P then a else if Q then a else b

Tactic:
by_cases hq : Q

Goal state after:
case pos
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
hp : ¬P
hq : Q
⊢ (if P ∨ Q then a else b) = if P then a else if Q then a else b

case neg
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
hp : ¬P
hq : ¬Q
⊢ (if P ∨ Q then a else b) = if P then a else if Q then a else b
Module: Mathlib.Logic.Unique

Goal state before:
pp: α : Sort u_1
inst✝ : Unique α
p : α → Prop
h : p default
x : α
⊢ p x

Tactic:
Unique.eq_default x

Goal state after:
α : Sort u_1
inst✝ : Unique α
p : α → Prop
h : p default
x : α
⊢ p default
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Type u_1
α' : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f : α × α' → β
aa' : α × α'
b : β
a : α
a' : α'
a₂ : α
a₂' : α'
⊢ curry (update f (a₂, a₂') b) a a' =
    update (curry f) (a₂, a₂').fst (update (curry f (a₂, a₂').fst) (a₂, a₂').snd b) a a'

Tactic:
obtain rfl | ha := eq_or_ne a a₂ <;> obtain rfl | ha' := eq_or_ne a' a₂'

Goal state after:
case inl.inl
α : Type u_1
α' : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f : α × α' → β
aa' : α × α'
b : β
a : α
a' : α'
⊢ curry (update f (a, a') b) a a' = update (curry f) (a, a').fst (update (curry f (a, a').fst) (a, a').snd b) a a'

case inl.inr
α : Type u_1
α' : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f : α × α' → β
aa' : α × α'
b : β
a : α
a' a₂' : α'
ha' : a' ≠ a₂'
⊢ curry (update f (a, a₂') b) a a' = update (curry f) (a, a₂').fst (update (curry f (a, a₂').fst) (a, a₂').snd b) a a'

case inr.inl
α : Type u_1
α' : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f : α × α' → β
aa' : α × α'
b : β
a : α
a' : α'
a₂ : α
ha : a ≠ a₂
⊢ curry (update f (a₂, a') b) a a' = update (curry f) (a₂, a').fst (update (curry f (a₂, a').fst) (a₂, a').snd b) a a'

case inr.inr
α : Type u_1
α' : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f : α × α' → β
aa' : α × α'
b : β
a : α
a' : α'
a₂ : α
a₂' : α'
ha : a ≠ a₂
ha' : a' ≠ a₂'
⊢ curry (update f (a₂, a₂') b) a a' =
    update (curry f) (a₂, a₂').fst (update (curry f (a₂, a₂').fst) (a₂, a₂').snd b) a a'
Module: Mathlib.Data.FunLike.Basic

Goal state before:
pp: F : Sort u_1
α : Sort u_2
β : Sort u_3
i : FunLike F α β
P : Prop
inst✝ : Decidable P
f : P → F
g : ¬P → F
x : α
⊢ (if h : P then f h else g h) x = if h : P then (f h) x else (g h) x

Tactic:
split_ifs

Goal state after:
case pos
F : Sort u_1
α : Sort u_2
β : Sort u_3
i : FunLike F α β
P : Prop
inst✝ : Decidable P
f : P → F
g : ¬P → F
x : α
h✝ : P
⊢ (f h✝) x = (f h✝) x

case neg
F : Sort u_1
α : Sort u_2
β : Sort u_3
i : FunLike F α β
P : Prop
inst✝ : Decidable P
f : P → F
g : ¬P → F
x : α
h✝ : ¬P
⊢ (g h✝) x = (g h✝) x
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ Function.swap (TransGen r) ≤ TransGen (Function.swap r)

Tactic:
intro _ _ h

Goal state after:
α : Type u_1
r : α → α → Prop
i✝¹ i✝ : α
h : Function.swap (TransGen r) i✝¹ i✝
⊢ TransGen (Function.swap r) i✝¹ i✝
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ Function.swap (ReflTransGen r) ≤ ReflTransGen (Function.swap r)

Tactic:
intro _ _ h

Goal state after:
α : Type u_1
r : α → α → Prop
i✝¹ i✝ : α
h : Function.swap (ReflTransGen r) i✝¹ i✝
⊢ ReflTransGen (Function.swap r) i✝¹ i✝
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r p : α → α → Prop
hrp : r ≤ p
⊢ EqvGen r ≤ EqvGen p

Tactic:
intro _ _ h

Goal state after:
α : Type u_1
r p : α → α → Prop
hrp : r ≤ p
i✝¹ i✝ : α
h : EqvGen r i✝¹ i✝
⊢ EqvGen p i✝¹ i✝
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ TransGen r ≤ EqvGen r

Tactic:
intro _ _ h

Goal state after:
α : Type u_1
r : α → α → Prop
i✝¹ i✝ : α
h : TransGen r i✝¹ i✝
⊢ EqvGen r i✝¹ i✝
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ ReflTransGen r ≤ EqvGen r

Tactic:
intro _ _ h

Goal state after:
α : Type u_1
r : α → α → Prop
i✝¹ i✝ : α
h : ReflTransGen r i✝¹ i✝
⊢ EqvGen r i✝¹ i✝
Module: Mathlib.Logic.Function.Iterate

Goal state before:
pp: α : Type u
f : α → α
n : ℕ
⊢ f^[n.succ] = f ∘ f^[n]

Tactic:
by
  rw [iterate_succ, (Commute.self_iterate f n).comp_eq]

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

Goal state before:
pp: α : Type u_4
β : Type u_5
R : α → β → Prop
inst✝ : IsEmpty α
⊢ BiTotal R ↔ IsEmpty β

Tactic:
simp only [BiTotal, leftTotal_empty, rightTotal_iff_isEmpty_right, true_and]

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

Goal state before:
pp: I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
inst✝ : (i : I) → DivisionMonoid (f i)
⊢ ∀ (a b : (i : I) → f i), a * b = 1 → a⁻¹ = b

Tactic:
intro _ _ h

Goal state after:
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h✝ : I → Type v₃
x y : (i : I) → f i
i : I
inst✝ : (i : I) → DivisionMonoid (f i)
a✝ b✝ : (i : I) → f i
h : a✝ * b✝ = 1
⊢ a✝⁻¹ = b✝
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ max a b = if b ≤ a then a else b

Tactic:
by
  obtain h | h | h := lt_trichotomy a b <;> simp [le_of_lt, not_le_of_gt, h, max_def]

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : c ≤ a
h₂ : c ≤ b
⊢ c ≤ if a ≤ b then a else b

Tactic:
split_ifs

Goal state after:
case pos
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : c ≤ a
h₂ : c ≤ b
h✝ : a ≤ b
⊢ c ≤ a

case neg
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : c ≤ a
h₂ : c ≤ b
h✝ : ¬a ≤ b
⊢ c ≤ b
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ compare a b = Ordering.lt ↔ a < b

Tactic:
LinearOrder.compare_eq_compareOfLessAndEq,

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ compareOfLessAndEq a b = Ordering.lt ↔ a < b
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ compare a b = Ordering.eq ↔ a = b

Tactic:
LinearOrder.compare_eq_compareOfLessAndEq,

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ compareOfLessAndEq a b = Ordering.eq ↔ a = b
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ compare a b = Ordering.gt ↔ b < a

Tactic:
LinearOrder.compare_eq_compareOfLessAndEq,

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ compareOfLessAndEq a b = Ordering.gt ↔ b < a
Module: Mathlib.Order.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝⁸ : LinearOrder β
inst✝⁷ : LE α
inst✝⁶ : LT α
inst✝⁵ : Max α
inst✝⁴ : Min α
inst✝³ : Ord α
inst✝² : DecidableEq α
inst✝¹ : DecidableLE α
inst✝ : DecidableLT α
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
min : ∀ (x y : α), f (x ⊓ y) = Min.min (f x) (f y)
max : ∀ (x y : α), f (x ⊔ y) = Max.max (f x) (f y)
compare : ∀ (x y : α), Ord.compare (f x) (f y) = Ord.compare x y
x✝¹ x✝ : α
⊢ Ord.compare (f x✝¹) (f x✝) = compareOfLessAndEq x✝¹ x✝

Tactic:
LinearOrder.compare_eq_compareOfLessAndEq,

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝⁸ : LinearOrder β
inst✝⁷ : LE α
inst✝⁶ : LT α
inst✝⁵ : Max α
inst✝⁴ : Min α
inst✝³ : Ord α
inst✝² : DecidableEq α
inst✝¹ : DecidableLE α
inst✝ : DecidableLT α
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
min : ∀ (x y : α), f (x ⊓ y) = Min.min (f x) (f y)
max : ∀ (x y : α), f (x ⊔ y) = Max.max (f x) (f y)
compare : ∀ (x y : α), Ord.compare (f x) (f y) = Ord.compare x y
x✝¹ x✝ : α
⊢ compareOfLessAndEq (f x✝¹) (f x✝) = compareOfLessAndEq x✝¹ x✝
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
⊢ (if f a < f b then Ordering.lt else if f a = f b then Ordering.eq else Ordering.gt) =
    if a < b then Ordering.lt else if a = b then Ordering.eq else Ordering.gt

Tactic:
split_ifs

Goal state after:
case pos
α : Type u_2
β : Type u_3
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝¹ : f a < f b
h✝ : a < b
⊢ Ordering.lt = Ordering.lt

case pos
α : Type u_2
β : Type u_3
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝² : f a < f b
h✝¹ : ¬a < b
h✝ : a = b
⊢ False

case neg
α : Type u_2
β : Type u_3
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝² : f a < f b
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ False

case pos
α : Type u_2
β : Type u_3
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝² : ¬f a < f b
h✝¹ : f a = f b
h✝ : a < b
⊢ False

case pos
α : Type u_2
β : Type u_3
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : f a = f b
h✝¹ : ¬a < b
h✝ : a = b
⊢ Ordering.eq = Ordering.eq

case neg
α : Type u_2
β : Type u_3
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : f a = f b
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ False

case pos
α : Type u_2
β : Type u_3
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝² : ¬f a < f b
h✝¹ : ¬f a = f b
h✝ : a < b
⊢ False

case pos
α : Type u_2
β : Type u_3
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : ¬f a = f b
h✝¹ : ¬a < b
h✝ : a = b
⊢ False

case neg
α : Type u_2
β : Type u_3
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : ¬f a = f b
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ Ordering.gt = Ordering.gt
Module: Mathlib.Data.Nat.Init

Goal state before:
pp: n : ℕ
hn : n % 2 = 1
⊢ 2 * (n / 2) = n - 1

Tactic:
by
  lia

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

Goal state before:
pp: a b c d e m✝ n✝ k : ℕ
p : ℕ → Prop
n : ℕ
motive : (m : ℕ) → m ≤ n → Sort u_1
of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯
self : motive n ⋯
m : ℕ
mn : m ≤ n
⊢ motive m mn

Tactic:
induction mn using leRec with
  | refl => exact self
  | @le_succ_of_le k _ ih =>
    apply ih (fun i hi => of_succ i (le_succ_of_le hi)) (of_succ k (lt_succ_self _) self)

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

Goal state before:
pp: n : ℕ
⊢ ¬2 ∣ 2 * n + 1

Tactic:
by
  lia

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

Goal state before:
pp: case refine_1
α : Type u
inst✝ : Preorder α
f : ℕ → α
k : ℕ
h : Monotone fun n ↦ f (n + k)
x : ℕ
hx : x ∈ {x | k ≤ x}
y : ℕ
hy : y ∈ {x | k ≤ x}
hle : x ≤ y
⊢ f (x - k + k) ≤ f (y - k + k)

Tactic:
rw [← Nat.sub_le_sub_iff_right hy] at hle

Goal state after:
case refine_1
α : Type u
inst✝ : Preorder α
f : ℕ → α
k : ℕ
h : Monotone fun n ↦ f (n + k)
x : ℕ
hx : x ∈ {x | k ≤ x}
y : ℕ
hy : y ∈ {x | k ≤ x}
hle : x - k ≤ y - k
⊢ f (x - k + k) ≤ f (y - k + k)
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 univ else t h) ↔ ∀ (h : ¬p), x ∈ t h

Tactic:
split_ifs

Goal state after:
case pos
α : Type u
p : Prop
inst✝ : Decidable p
t : ¬p → Set α
x : α
h✝ : p
⊢ x ∈ univ ↔ ∀ (h : ¬p), x ∈ t h

case neg
α : Type u
p : Prop
inst✝ : Decidable p
t : ¬p → Set α
x : α
h✝ : ¬p
⊢ x ∈ t h✝ ↔ ∀ (h : ¬p), x ∈ t h
Module: Mathlib.Data.Set.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Set α → Set β
hf : Injective f
h2 : f ∅ = ∅
s : Set α
⊢ f s ≠ f ∅ ↔ s ≠ ∅

Tactic:
hf.ne_iff

Goal state after:
α : Type u_1
β : Type u_2
f : Set α → Set β
hf : Injective f
h2 : f ∅ = ∅
s : Set α
⊢ s ≠ ∅ ↔ s ≠ ∅
Module: Mathlib.Order.Lattice

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

Tactic:
let partialOrder := e.partialOrder

Goal state after:
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeSup β
max : Max α := e.max
partialOrder : PartialOrder α := e.partialOrder
⊢ SemilatticeSup α
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeInf β
min : Min α := e.min
⊢ SemilatticeInf α

Tactic:
let partialOrder := e.partialOrder

Goal state after:
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeInf β
min : Min α := e.min
partialOrder : PartialOrder α := e.partialOrder
⊢ SemilatticeInf α
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
h : Codisjoint a b
⊢ b ⇨ a = ⊤ ⇨ a

Tactic:
← h.eq_top,

Goal state after:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
h : Codisjoint a b
⊢ b ⇨ a = a ⊔ b ⇨ a
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
α : Type u
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
a : α
⊢ Option.elim' default Subtype.val (if h : a = default then none else some ⟨a, h⟩) = a

Tactic:
split_ifs

Goal state after:
case pos
α✝ : 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
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
a : α
h✝ : a = default
⊢ Option.elim' default Subtype.val none = a

case neg
α✝ : 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
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
a : α
h✝ : ¬a = default
⊢ Option.elim' default Subtype.val (some ⟨a, h✝⟩) = a
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
α : Type u_9
p : α → Prop
inst✝ : DecidablePred p
a : α
⊢ Sum.elim Subtype.val Subtype.val (if h : p a then Sum.inl ⟨a, h⟩ else Sum.inr ⟨a, h⟩) = a

Tactic:
split_ifs

Goal state after:
case pos
α✝ : 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
p : α → Prop
inst✝ : DecidablePred p
a : α
h✝ : p a
⊢ Sum.elim Subtype.val Subtype.val (Sum.inl ⟨a, h✝⟩) = a

case neg
α✝ : 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
p : α → Prop
inst✝ : DecidablePred p
a : α
h✝ : ¬p a
⊢ Sum.elim Subtype.val Subtype.val (Sum.inr ⟨a, h✝⟩) = a
Module: Mathlib.Order.BooleanAlgebra.Basic

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

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

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

Goal state before:
pp: α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
p : α → Prop
inst✝ : DecidablePred p
x₀ : { a // p a } → β
x✝ : { x // x ∘ Subtype.val = x₀ }
x : α → β
hx : x ∘ Subtype.val = x₀
a : α
⊢ (if h : p a then x₀ ⟨a, h⟩ else x a) = x a

Tactic:
split_ifs

Goal state after:
case pos
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
p : α → Prop
inst✝ : DecidablePred p
x₀ : { a // p a } → β
x✝ : { x // x ∘ Subtype.val = x₀ }
x : α → β
hx : x ∘ Subtype.val = x₀
a : α
h✝ : p a
⊢ x₀ ⟨a, h✝⟩ = x a

case neg
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
p : α → Prop
inst✝ : DecidablePred p
x₀ : { a // p a } → β
x✝ : { x // x ∘ Subtype.val = x₀ }
x : α → β
hx : x ∘ Subtype.val = x₀
a : α
h✝ : ¬p a
⊢ x a = x a
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
p₁ : α → Prop
s₁ : Setoid α
s₂ : Setoid (Subtype p₁)
p₂ : Quotient s₁ → Prop
hp₂ : ∀ (a : α), p₁ a ↔ p₂ ⟦a⟧
h : ∀ (x y : Subtype p₁), s₂ x y ↔ s₁ ↑x ↑y
a : { x // p₂ x }
⊢ (fun a ↦ a.liftOn (fun a ↦ ⟨⟦↑a⟧, ⋯⟩) ⋯)
      ((fun a ↦ Quotient.hrecOn (motive := fun x ↦ p₂ x → Quotient s₂) (↑a) (fun a h ↦ ⟦⟨a, ⋯⟩⟧) ⋯ ⋯) a) =
    a

Tactic:
by
    obtain ⟨a, ha⟩ := a
    induction a using Quotient.inductionOn
    rfl

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

Goal state before:
pp: α : Sort u_1
inst✝ : DecidableEq α
r a : α
⊢ (if r = a then a else if r = a then a else r) = r

Tactic:
split_ifs

Goal state after:
case pos
α : Sort u_1
inst✝ : DecidableEq α
r a : α
h✝ : r = a
⊢ a = r

case neg
α : Sort u_1
inst✝ : DecidableEq α
r a : α
h✝ : ¬r = a
⊢ r = r
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: α : Sort u_1
inst✝ : DecidableEq α
r a b : α
⊢ (if (if r = a then b else if r = b then a else r) = a then b
    else if (if r = a then b else if r = b then a else r) = b then a else if r = a then b else if r = b then a else r) =
    r

Tactic:
split_ifs

Goal state after:
case pos
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h✝¹ : r = a
h✝ : b = a
⊢ b = r

case pos
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h✝² : r = a
h✝¹ : ¬b = a
h✝ : b = b
⊢ a = r

case neg
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h✝² : r = a
h✝¹ : ¬b = a
h✝ : ¬b = b
⊢ b = r

case pos
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h✝² : ¬r = a
h✝¹ : r = b
h✝ : a = a
⊢ b = r

case pos
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h✝³ : ¬r = a
h✝² : r = b
h✝¹ : ¬a = a
h✝ : a = b
⊢ a = r

case neg
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h✝³ : ¬r = a
h✝² : r = b
h✝¹ : ¬a = a
h✝ : ¬a = b
⊢ a = r

case neg
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h✝¹ : ¬r = a
h✝ : ¬r = b
⊢ r = r
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
h : a ≤ (a ⊔ b) \ (a ⊓ b)
⊢ Disjoint a b

Tactic:
exact disjoint_iff_inf_le.mpr (le_sdiff_right.1 <| inf_le_of_left_le h).le

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

Goal state before:
pp: α : Sort u_1
inst✝ : DecidableEq α
r a b : α
⊢ (if r = a then b else if r = b then a else r) = if r = b then a else if r = a then b else r

Tactic:
split_ifs

Goal state after:
case pos
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h✝¹ : r = a
h✝ : r = b
⊢ b = a

case neg
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h✝¹ : r = a
h✝ : ¬r = b
⊢ b = b

case pos
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h✝¹ : ¬r = a
h✝ : r = b
⊢ a = a

case neg
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h✝¹ : ¬r = a
h✝ : ¬r = b
⊢ r = r
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ f '' s ⊆ f '' univ

Tactic:
exact image_mono (subset_univ _)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ f '' (f ⁻¹' s)ᶜ = range f \ s

Tactic:
compl_eq_univ_sdiff,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ f '' (univ \ f ⁻¹' s) = range f \ s