mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Notation.Defs

Goal state before:
pp: α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Mul α
a : α
b : P → α
c : ¬P → α
⊢ (a * if h : P then b h else c h) = if h : P then a * b h else a * c h

Tactic:
split

Goal state after:
case isTrue
α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Mul α
a : α
b : P → α
c : ¬P → α
h✝ : P
⊢ a * b h✝ = a * b h✝

case isFalse
α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Mul α
a : α
b : P → α
c : ¬P → α
h✝ : ¬P
⊢ a * c h✝ = a * c h✝
Module: Mathlib.Algebra.Notation.Defs

Goal state before:
pp: α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Mul α
a : P → α
b : ¬P → α
c : α
⊢ (if h : P then a h else b h) * c = if h : P then a h * c else b h * c

Tactic:
split

Goal state after:
case isTrue
α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Mul α
a : P → α
b : ¬P → α
c : α
h✝ : P
⊢ a h✝ * c = a h✝ * c

case isFalse
α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Mul α
a : P → α
b : ¬P → α
c : α
h✝ : ¬P
⊢ b h✝ * c = b h✝ * c
Module: Mathlib.Algebra.Notation.Defs

Goal state before:
pp: α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Mul α
a : P → α
b : ¬P → α
c : P → α
d : ¬P → α
⊢ ((if h : P then a h else b h) * if h : P then c h else d h) = if h : P then a h * c h else b h * d h

Tactic:
split

Goal state after:
case isTrue
α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Mul α
a : P → α
b : ¬P → α
c : P → α
d : ¬P → α
h✝ : P
⊢ a h✝ * c h✝ = a h✝ * c h✝

case isFalse
α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Mul α
a : P → α
b : ¬P → α
c : P → α
d : ¬P → α
h✝ : ¬P
⊢ b h✝ * d h✝ = b h✝ * d h✝
Module: Mathlib.Algebra.Notation.Defs

Goal state before:
pp: α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Mul α
a b c d : α
⊢ ((if P then a else b) * if P then c else d) = if P then a * c else b * d

Tactic:
split

Goal state after:
case isTrue
α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Mul α
a b c d : α
h✝ : P
⊢ a * c = a * c

case isFalse
α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Mul α
a b c d : α
h✝ : ¬P
⊢ b * d = b * d
Module: Mathlib.Algebra.Notation.Defs

Goal state before:
pp: α : Type u_3
P : Prop
inst✝¹ : Decidable P
inst✝ : Neg α
b c : α
⊢ (-if P then b else c) = if P then -b else -c

Tactic:
split

Goal state after:
case isTrue
α : Type u_3
P : Prop
inst✝¹ : Decidable P
inst✝ : Neg α
b c : α
h✝ : P
⊢ -b = -b

case isFalse
α : Type u_3
P : Prop
inst✝¹ : Decidable P
inst✝ : Neg α
b c : α
h✝ : ¬P
⊢ -c = -c
Module: Mathlib.Algebra.Notation.Defs

Goal state before:
pp: α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Div α
a : α
b : P → α
c : ¬P → α
⊢ (a / if h : P then b h else c h) = if h : P then a / b h else a / c h

Tactic:
split

Goal state after:
case isTrue
α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Div α
a : α
b : P → α
c : ¬P → α
h✝ : P
⊢ a / b h✝ = a / b h✝

case isFalse
α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Div α
a : α
b : P → α
c : ¬P → α
h✝ : ¬P
⊢ a / c h✝ = a / c h✝
Module: Mathlib.Algebra.Notation.Defs

Goal state before:
pp: α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Div α
a : P → α
b : ¬P → α
c : α
⊢ (if h : P then a h else b h) / c = if h : P then a h / c else b h / c

Tactic:
split

Goal state after:
case isTrue
α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Div α
a : P → α
b : ¬P → α
c : α
h✝ : P
⊢ a h✝ / c = a h✝ / c

case isFalse
α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Div α
a : P → α
b : ¬P → α
c : α
h✝ : ¬P
⊢ b h✝ / c = b h✝ / c
Module: Mathlib.Algebra.Notation.Defs

Goal state before:
pp: α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Div α
a : P → α
b : ¬P → α
c : P → α
d : ¬P → α
⊢ ((if h : P then a h else b h) / if h : P then c h else d h) = if h : P then a h / c h else b h / d h

Tactic:
split

Goal state after:
case isTrue
α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Div α
a : P → α
b : ¬P → α
c : P → α
d : ¬P → α
h✝ : P
⊢ a h✝ / c h✝ = a h✝ / c h✝

case isFalse
α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Div α
a : P → α
b : ¬P → α
c : P → α
d : ¬P → α
h✝ : ¬P
⊢ b h✝ / d h✝ = b h✝ / d h✝
Module: Mathlib.Algebra.Group.Defs

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

Tactic:
rw [mul_assoc, mul_inv_cancel, mul_one]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: P Q : Prop
⊢ ¬Xor P Q ↔ (P ↔ Q)

Tactic:
simp only [not_and, Xor, not_or, not_not, ← iff_iff_implies_and_implies]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α β : Sort u
a : α
b : β
⊢ a ≍ b ↔ ∃ h, cast h a = b

Tactic:
by
  simp only [heq_comm (a := a), heq_iff_exists_eq_cast, eq_comm]

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

Goal state before:
pp: α : Type u_4
β : Sort u_5
f : α → β
I : Injective f
a : α
b : β
h : partialInv f b = some a
hpi : partialInv f b = if h : ∃ a, f a = b then some (Classical.choose h) else none
h' : ¬∃ a, f a = b
⊢ f a = b

Tactic:
rw [hpi, dif_neg h'] at h; contradiction

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

Goal state before:
pp: α : Type u
f : α → α
m n : ℕ
a : α
hf : Injective f
ha : f^[m] a = f^[n] a
h : n ≤ m
⊢ f^[m - n + ?m.30] a = f^[?m.30] a

Tactic:
by rwa [Nat.sub_add_cancel h]

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

Goal state before:
pp: case cons
α : Type u
β : Type v
f : α → α
b : β
l : List β
H : ∀ (a : α), foldl (fun b x ↦ f b) a l = f^[l.length] a
a : α
⊢ foldl (fun b x ↦ f b) a (b :: l) = f^[(b :: l).length] a

Tactic:
length_cons,

Goal state after:
case cons
α : Type u
β : Type v
f : α → α
b : β
l : List β
H : ∀ (a : α), foldl (fun b x ↦ f b) a l = f^[l.length] a
a : α
⊢ foldl (fun b x ↦ f b) a (b :: l) = f^[l.length + 1] a
Module: Mathlib.Logic.Function.Iterate

Goal state before:
pp: α : Type u
β : Type v
f : β → β
b : β
a : α
l : List α
⊢ foldr (fun x ↦ f) b (a :: l) = f^[(a :: l).length] b

Tactic:
length_cons,

Goal state after:
α : Type u
β : Type v
f : β → β
b : β
a : α
l : List α
⊢ foldr (fun x ↦ f) b (a :: l) = f^[l.length + 1] b
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 : β → δ
h : Injective (map f g)
a₁ a₂ : α
ha : f a₁ = f a₂
inhabited_h : Inhabited β
⊢ a₁ = a₂

Tactic:
injection
        @h (a₁, default) (a₂, default) (congr_arg (fun c : γ => Prod.mk c (g default)) ha :)

Goal state after:
Module: Mathlib.Tactic.CongrExclamation

Goal state before:
pp: case refl
α : Sort u
β β' : Sort v
h' : ∀ (a : α), β = β'
⊢ (α → β) = (α → β')

Tactic:
change (∀ (x : α), (fun _ => β) x) = _

Goal state after:
case refl
α : Sort u
β β' : Sort v
h' : ∀ (a : α), β = β'
⊢ ((x : α) → (fun x ↦ β) x) = (α → β')
Module: Mathlib.Order.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝² : Preorder β
inst✝¹ : LE α
inst✝ : LT α
f : α → β
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
x✝¹ x✝ : α
⊢ x✝¹ < x✝ ↔ f x✝¹ ≤ f x✝ ∧ ¬f x✝ ≤ f x✝¹

Tactic:
← lt,

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝² : Preorder β
inst✝¹ : LE α
inst✝ : LT α
f : α → β
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
x✝¹ x✝ : α
⊢ f x✝¹ < f x✝ ↔ f x✝¹ ≤ f x✝ ∧ ¬f x✝ ≤ f x✝¹
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✝ : α
⊢ (if f x✝¹ < f x✝ then Ordering.lt else if f x✝¹ = f x✝ then Ordering.eq else Ordering.gt) =
    if x✝¹ < x✝ then Ordering.lt else if x✝¹ = x✝ then Ordering.eq else Ordering.gt

Tactic:
← lt,

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✝ : α
⊢ (if f x✝¹ < f x✝ then Ordering.lt else if f x✝¹ = f x✝ then Ordering.eq else Ordering.gt) =
    if f x✝¹ < f x✝ then Ordering.lt else if x✝¹ = x✝ then Ordering.eq else Ordering.gt
Module: Mathlib.Order.BoundedOrder.Basic

Goal state before:
pp: α : Type u
inst✝¹ : Top α
p : Prop
inst✝ : Decidable p
a : p → α
b : ¬p → α
ha : ∀ (h : p), a h ≠ ⊤
hb : ∀ (h : ¬p), b h ≠ ⊤
⊢ (if h : p then a h else b h) ≠ ⊤

Tactic:
split

Goal state after:
case isTrue
α : Type u
inst✝¹ : Top α
p : Prop
inst✝ : Decidable p
a : p → α
b : ¬p → α
ha : ∀ (h : p), a h ≠ ⊤
hb : ∀ (h : ¬p), b h ≠ ⊤
h✝ : p
⊢ a h✝ ≠ ⊤

case isFalse
α : Type u
inst✝¹ : Top α
p : Prop
inst✝ : Decidable p
a : p → α
b : ¬p → α
ha : ∀ (h : p), a h ≠ ⊤
hb : ∀ (h : ¬p), b h ≠ ⊤
h✝ : ¬p
⊢ b h✝ ≠ ⊤
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
x y z : α
h : IsCompl y z
⊢ x ⊓ y ≤ ⊥ ↔ x ≤ z

Tactic:
← h.le_sup_right_iff_inf_left_le,

Goal state after:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
x y z : α
h : IsCompl y z
⊢ x ≤ ⊥ ⊔ z ↔ x ≤ z
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 : α
⊢ b ⊔ (a ⊔ b) = a ⊔ b

Tactic:
sup_comm,

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 : α
⊢ a ⊔ b ⊔ b = a ⊔ b
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
a b : α
⊢ b ⊓ (a ⊓ b) = a ⊓ b

Tactic:
by rw [inf_comm, inf_assoc, inf_idem]

Goal state after:
Module: Mathlib.Order.Lattice

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

Tactic:
sup_comm,

Goal state after:
α : Type u
inst✝ : SemilatticeSup α
a b c : α
⊢ c ⊔ (a ⊔ b) = c ⊔ b ⊔ a
Module: Mathlib.Order.Lattice

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

Tactic:
sup_comm,

Goal state after:
α : Type u
inst✝ : SemilatticeSup α
a b c : α
⊢ b ⊔ c ⊔ a = b ⊔ (c ⊔ a)
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u_1
inst✝¹ : Max α
inst✝ : Min α
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
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
sup_inf_self : ∀ (a b : α), a ⊔ a ⊓ b = a
inf_sup_self : ∀ (a b : α), a ⊓ (a ⊔ b) = a
a b : α
h : b ⊓ a = a
⊢ b ⊓ a ⊔ b = b

Tactic:
sup_comm,

Goal state after:
α : Type u_1
inst✝¹ : Max α
inst✝ : Min α
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
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
sup_inf_self : ∀ (a b : α), a ⊔ a ⊓ b = a
inf_sup_self : ∀ (a b : α), a ⊓ (a ⊔ b) = a
a b : α
h : b ⊓ a = a
⊢ b ⊔ b ⊓ a = b
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
h : b ≤ a
⊢ a \ b ⊔ b = a

Tactic:
sup_comm,

Goal state after:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
h : b ≤ a
⊢ b ⊔ a \ b = a
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ (a ⊔ b) \ a = b \ a

Tactic:
sup_comm,

Goal state after:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ (b ⊔ a) \ a = b \ a
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
sup_comm,

Goal state after:
α : Type u
inst✝ : GeneralizedBooleanAlgebra α
x y : α
⊢ x ⊓ y ⊔ x \ y = x
Module: Mathlib.Order.BooleanAlgebra.Set

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

Tactic:
ext x; simp [and_iff_left_of_imp (ne_of_mem_of_not_mem · h)]

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

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

Tactic:
by grind [sdiff_le', inf_of_le_right, inf_eq_right, inf_sdiff_self_right, bot_sup_eq,
            inf_sup_right]

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

Goal state before:
pp: α : Type u
β : Type u_1
x✝ y✝ z✝ : α
inst✝ : GeneralizedBooleanAlgebra α
y x z : α
h : y ≤ x ⊔ z
⊢ x ⊔ (z ⊔ x) ≤ z ⊔ x

Tactic:
sup_comm,

Goal state after:
α : Type u
β : Type u_1
x✝ y✝ z✝ : α
inst✝ : GeneralizedBooleanAlgebra α
y x z : α
h : y ≤ x ⊔ z
⊢ z ⊔ x ⊔ x ≤ z ⊔ x
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hd : Disjoint x z
hz : z ≤ y
hs : (x ⊔ z) ⊓ y = y
⊢ (x ⊔ z) ⊓ y ⊔ z = y

Tactic:
hs,

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hd : Disjoint x z
hz : z ≤ y
hs : (x ⊔ z) ⊓ y = y
⊢ y ⊔ z = y
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
sup_comm,

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x \ (y \ z) = x ⊓ y ⊓ z ⊔ x \ y
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
sup_comm,

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x \ y ⊔ z ⊓ x = x \ y ⊔ x ⊓ z
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
sup_comm,

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (z ⊓ x ⊔ z \ x) ⊓ (z \ x ⊔ y) ⊓ (z \ y ⊔ z ⊓ y ⊓ x) = z ⊓ (z \ x ⊔ y) ⊓ (z ⊓ (z \ y ⊔ x))
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x : α
inst✝ : BooleanAlgebra α
⊢ xᶜ ⊔ x = ⊤

Tactic:
sup_comm,

Goal state after:
α : Type u
x : α
inst✝ : BooleanAlgebra α
⊢ x ⊔ xᶜ = ⊤
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y : α
inst✝ : BooleanAlgebra α
⊢ xᶜ \ yᶜ = y \ x

Tactic:
by rw [sdiff_compl, sdiff_eq, inf_comm]

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ≤ b ∧ b ≤ a ↔ a = b

Tactic:
le_antisymm_iff

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:
by
    intro x
    cases x
    · intro n
      exfalso
      exact h n
    · intro _
      exact rfl

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
sup_comm,

Goal state after:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ∆ b ⊔ a ⊓ b = a ⊔ b
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_4
W : α → Sort w
Z : β → Sort z
h₁ : α ≃ β
h₂ : (a : α) → W a ≃ Z (h₁ a)
f : (a : α) → W a
a : α
⊢ (piCongrLeft Z h₁) ((piCongrRight h₂) f) (h₁ a) = (h₂ a) (f a)

Tactic:
piCongrLeft_apply_apply,

Goal state after:
α : Sort u_1
β : Sort u_4
W : α → Sort w
Z : β → Sort z
h₁ : α ≃ β
h₂ : (a : α) → W a ≃ Z (h₁ a)
f : (a : α) → W a
a : α
⊢ (piCongrRight h₂) f a = (h₂ a) (f a)
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
a b : α
⊢ a ⇔ b = ⊥ ↔ IsCompl a b

Tactic:
rw [bihimp_eq', ← compl_sup, sup_eq_bot_iff, compl_eq_bot, isCompl_iff, disjoint_iff,
    codisjoint_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t₁ t₂ : Set β
⊢ s ×ˢ (t₁ ∪ t₂) = s ×ˢ t₁ ∪ s ×ˢ t₂

Tactic:
ext ⟨x, y⟩
  simp [and_or_left]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
a : α
⊢ insert a s ×ˢ t = Prod.mk a '' t ∪ s ×ˢ t

Tactic:
by
  simp only [insert_eq, union_prod, singleton_prod]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_5
f : ι → α
s : Set α
h : ∀ (x : ι), f x ∈ s
⊢ range (codRestrict f s h) = Subtype.val ⁻¹' range f

Tactic:
ext; simp [Subtype.ext_iff]

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

Goal state before:
pp: α : Type u_1
s : Set α
σ : Equiv.Perm α
hs : {a | σ a ≠ a} ⊆ s
⊢ ⇑σ '' s = s

Tactic:
by
  ext i
  obtain hi | hi := eq_or_ne (σ i) i
  · refine ⟨?_, fun h => ⟨i, h, hi⟩⟩
    rintro ⟨j, hj, h⟩
    rwa [σ.injective (hi.trans h.symm)]
  · refine iff_of_true ⟨σ.symm i, hs fun h => hi ?_, σ.apply_symm_apply _⟩ (hs hi)
    grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x : α
inst✝¹ : (y : α) → Decidable (y ∈ {x})
inst✝ : DecidableEq α
f g : α → β
⊢ {x}.piecewise f g = update g x (f x)

Tactic:
by
  ext y
  by_cases hy : y = x
  · subst y
    simp
  · simp [hy]

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

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
f : α → β
s : Set α
x✝ : β
⊢ (x✝ ∈ range fun x ↦ f ↑x) → x✝ ∈ f '' s

Tactic:
rintro ⟨⟨x, h1⟩, h2⟩

Goal state after:
case mpr
α : Type u_1
β : Type u_2
f : α → β
s : Set α
x✝ : β
x : α
h1 : x ∈ s
h2 : (fun x ↦ f ↑x) ⟨x, h1⟩ = x✝
⊢ x✝ ∈ f '' s
Module: Mathlib.Data.Set.Image

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

Tactic:
rw [← image_preimage_coe, ← image_preimage_coe]

Goal state after:
case mp
α : Type u_1
s t u : Set α
⊢ val ⁻¹' t ⊆ val ⁻¹' u → val '' val ⁻¹' t ⊆ val '' val ⁻¹' u
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set (α × β)
x✝ : ∃ f t, s = graphOn f t
f : α → β
t : Set α
hs : s = graphOn f t
⊢ s = graphOn f (Prod.fst '' s)

Tactic:
hs,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set (α × β)
x✝ : ∃ f t, s = graphOn f t
f : α → β
t : Set α
hs : s = graphOn f t
⊢ graphOn f t = graphOn f (Prod.fst '' graphOn f t)
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
inst✝ : Nonempty α
h : SurjOn f s t
⊢ InvOn (invFunOn f s) f (invFunOn f s '' t) t

Tactic:
refine ⟨?_, h.rightInvOn_invFunOn⟩
  rintro _ ⟨y, hy, rfl⟩
  rw [h.rightInvOn_invFunOn hy]

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

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

Tactic:
obtain rfl | hxa := eq_or_ne x a <;>
    obtain rfl | hxb := eq_or_ne x b

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

case inl.inr
α : Type u_1
s : Set α
inst✝ : DecidableEq α
b : α
hb : b ∈ s
x : α
ha : x ∈ s
hxb : x ≠ b
⊢ (swap x b) x ∈ s ↔ x ∈ s

case inr.inl
α : Type u_1
s : Set α
inst✝ : DecidableEq α
a : α
ha : a ∈ s
x : α
hxa : x ≠ a
hb : x ∈ s
⊢ (swap a x) x ∈ s ↔ x ∈ s

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a b : α
h : b * a = 1
⊢ b = 1 / a

Tactic:
eq_inv_of_mul_eq_one_left h,

Goal state after:
α : Type u_1
inst✝ : DivisionMonoid α
a b : α
h : b * a = 1
⊢ a⁻¹ = 1 / a
Module: Mathlib.Algebra.Group.InjSurj

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
inst✝² : Mul M₁
inst✝¹ : Mul M₂
inst✝ : IsLeftCancelMul M₂
f : M₁ → M₂
hf : Injective f
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x y z : M₁
H : (fun x_1 ↦ x * x_1) y = (fun x_1 ↦ x * x_1) z
⊢ ?m.31 x y z H * f y = ?m.31 x y z H * f z

Tactic:
simpa only [mul] using congrArg f H

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

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
inst✝² : Mul M₁
inst✝¹ : Mul M₂
inst✝ : IsRightCancelMul M₂
f : M₁ → M₂
hf : Injective f
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x y z : M₁
H : (fun x_1 ↦ x_1 * x) y = (fun x_1 ↦ x_1 * x) z
⊢ f y * ?m.31 x y z H = f z * ?m.31 x y z H

Tactic:
simpa only [mul] using congrArg f H

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

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

Tactic:
obtain ⟨u, hu⟩ := h
  rw [← hu, ← Units.val_inv_eq_inv_val]
  exact Units.isUnit _

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

Goal state before:
pp: α : Type u_4
inst✝ : DecidableEq α
i j : α
σ : Perm α
⊢ σ * swap i j * swap i j = σ

Tactic:
by
  rw [mul_assoc, swap_mul_self, mul_one]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : One R
⊢ Nat.binCast 0 = 0

Tactic:
by simp only [Nat.binCast]

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

Goal state before:
pp: α : Type u
R : Type v
inst✝¹ : MulZeroClass α
inst✝ : HasDistribNeg α
⊢ -0 = 0

Tactic:
rw [← zero_mul (0 : α), ← neg_mul, mul_zero, mul_zero]

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

Goal state before:
pp: R : Type u_6
S : Type u_7
inst✝³ : NonAssocSemiring R
inst✝² : NonAssocSemiring S
F : Type u_8
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
n : ℕ
hn : NeZero ↑n
⊢ NeZero (f ↑n)

Tactic:
simp only [map_natCast, hn]

Goal state after:
Module: Mathlib.Algebra.Ring.Hom.Defs

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : CommRing β
f : β →+ α
h : ∀ (x : β), f (x * x) = f x * f x
h_two : 2 ≠ 0
h_one : f 1 = 1
x y : β
hxy : f (x * y) + f y * f y + (f x * f x + f (x * y)) - f x * f x - f x * f y - f x * f y - f y * f y = 0
⊢ (↑f).toFun (x * y) = (↑f).toFun x * (↑f).toFun y

Tactic:
simp only [add_assoc, add_sub_assoc, add_sub_cancel] at hxy

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : CommRing β
f : β →+ α
h : ∀ (x : β), f (x * x) = f x * f x
h_two : 2 ≠ 0
h_one : f 1 = 1
x y : β
hxy : f (x * y) + (f (x * y) - f x * f y - f x * f y) = 0
⊢ (↑f).toFun (x * y) = (↑f).toFun x * (↑f).toFun y
Module: Mathlib.Algebra.Ring.Units

Goal state before:
pp: α : Type u
inst✝ : CommRing α
a b : α
u₁ u₂ : αˣ
⊢ a /ₚ u₁ - b /ₚ u₂ = (a * ↑u₂ - ↑u₁ * b) /ₚ (u₁ * u₂)

Tactic:
by
  simp only [sub_eq_add_neg, neg_divp, divp_add_divp, mul_neg]

Goal state after: