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

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

Tactic:
simp [bit_val]

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

Goal state before:
pp: case true
n : Nat
⊢ bit true n % 2 = true.toNat

Tactic:
simp [bit_val]

Goal state after:
Module: Mathlib.Logic.Unique

Goal state before:
pp: α : Sort u_1
p : α → Prop
x✝¹ : ∃! a, p a
a : α
ha : (fun a ↦ p a) a
he : ∀ (y : α), (fun a ↦ p a) y → y = a
x✝ : Subtype p
b : α
hb : p b
⊢ ⟨b, hb⟩ = default

Tactic:
congr
      exact he b hb

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

Goal state before:
pp: α : Sort u
inst✝ : DecidableEq α
β : Sort u_1
f : α → β
a' : α
b : β
a : α
⊢ update f a' b a = if a = a' then b else f a

Tactic:
by
  rcases Decidable.eq_or_ne a a' with rfl | hne <;> simp [*]

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

Goal state before:
pp: case refine_1
ι : Sort u_1
α : ι → Sort u_2
β : ι → Sort u_3
inst✝ : ∀ (i : ι), Nonempty (α i)
f : (i : ι) → α i → β i
h : Injective (Pi.map f)
i : ι
x y : α i
hxy : f i x = f i y
this : Inhabited ((i : ι) → α i)
⊢ Pi.map f (update default i x) = Pi.map f (update default i y)

Tactic:
rw [Pi.map_update, Pi.map_update, hxy]

Goal state after:
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 : β
⊢ curry (update f aa' b) = update (curry f) aa'.fst (update (curry f aa'.fst) aa'.snd b)

Tactic:
by
  ext a a'
  let ⟨a₂, a₂'⟩ := aa'
  obtain rfl | ha := eq_or_ne a a₂ <;> obtain rfl | ha' := eq_or_ne a' a₂' <;> simp [*]

Goal state after:
Module: Mathlib.Logic.Relation

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

Tactic:
induction h with
  | inl hba => exact of_rel hba
  | inr hab => exact of_rel_symm hab

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
x y : α
⊢ ReflGen (TransGen r) x y ↔ ReflTransGen r x y

Tactic:
[

Goal state after:
α : Type u_1
r : α → α → Prop
x y : α
⊢ ReflGen (TransGen r) x y ↔ ReflTransGen r x y
Module: Mathlib.Algebra.Opposites

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

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : Add α
⊢ IsCancelAdd αᵐᵒᵖ ↔ IsCancelAdd α
Module: Mathlib.Algebra.Group.Action.Faithful

Goal state before:
pp: M : Type u_4
N : Type u_5
P : Type u_6
Q : Type u_7
inst✝⁹ : SMul M N
inst✝⁸ : SMul M P
inst✝⁷ : SMul M Q
inst✝⁶ : SMul N P
inst✝⁵ : SMul N Q
inst✝⁴ : SMul P Q
inst✝³ : FaithfulSMul P Q
inst✝² : IsScalarTower M N Q
inst✝¹ : IsScalarTower M P Q
inst✝ : IsScalarTower N P Q
m : M
n : N
p : P
⊢ (m • n) • p = m • n • p

Tactic:
[

Goal state after:
M : Type u_4
N : Type u_5
P : Type u_6
Q : Type u_7
inst✝⁹ : SMul M N
inst✝⁸ : SMul M P
inst✝⁷ : SMul M Q
inst✝⁶ : SMul N P
inst✝⁵ : SMul N Q
inst✝⁴ : SMul P Q
inst✝³ : FaithfulSMul P Q
inst✝² : IsScalarTower M N Q
inst✝¹ : IsScalarTower M P Q
inst✝ : IsScalarTower N P Q
m : M
n : N
p : P
⊢ (m • n) • p = m • n • p
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M : Type u_9
N : Type u_10
P : Type u_11
Q : Type u_12
inst✝⁹ : SMul M N
inst✝⁸ : SMul M P
inst✝⁷ : SMul M Q
inst✝⁶ : SMul P Q
inst✝⁵ : Monoid N
inst✝⁴ : MulAction N P
inst✝³ : MulAction N Q
inst✝² : IsScalarTower M N P
inst✝¹ : IsScalarTower M N Q
inst✝ : IsScalarTower M P Q
h : Surjective fun m ↦ m • 1
p : P
q : Q
m : M
⊢ ((m • 1) • p) • q = (m • 1) • p • q

Tactic:
[

Goal state after:
M : Type u_9
N : Type u_10
P : Type u_11
Q : Type u_12
inst✝⁹ : SMul M N
inst✝⁸ : SMul M P
inst✝⁷ : SMul M Q
inst✝⁶ : SMul P Q
inst✝⁵ : Monoid N
inst✝⁴ : MulAction N P
inst✝³ : MulAction N Q
inst✝² : IsScalarTower M N P
inst✝¹ : IsScalarTower M N Q
inst✝ : IsScalarTower M P Q
h : Surjective fun m ↦ m • 1
p : P
q : Q
m : M
⊢ ((m • 1) • p) • q = (m • 1) • p • q
Module: Mathlib.Data.Option.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : γ → α → β
x : α → β
i : Option γ
y : α
⊢ i.elim x f y = i.elim (x y) fun j ↦ f j y

Tactic:
by rw [elim_comp fun f : α → β => f y]

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) → InvolutiveInv (f i)
x✝¹ : (i : I) → f i
x✝ : I
⊢ x✝¹⁻¹⁻¹ x✝ = x✝¹ x✝

Tactic:
exact inv_inv _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
x₁ : α
y₁ : β
x₂ : α
y₂ : β
⊢ (x₁, y₁) = (x₂, y₂) → ⦃P : Sort u_5⦄ → (x₁ = x₂ → y₁ = y₂ → P) → P

Tactic:
by
  intros h P w
  cases h
  exact w rfl rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
hab : a = b
⊢ a ≤ b

Tactic:
by rw [hab]

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

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

pp: case gt
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.gt
⊢ Ordering.gt ≠ Ordering.gt ↔ a ≤ b

Tactic:
· simpa using le_of_eq <| compare_eq_iff_eq.1 h

Goal state after:
case gt
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.gt
⊢ Ordering.gt ≠ Ordering.gt ↔ a ≤ b
Module: Mathlib.Order.Max

Goal state before:
pp: α : Type u_1
inst✝ : LE α
⊢ NoBotOrder α ↔ ∀ (x : α), ¬IsBot x

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : LE α
⊢ NoBotOrder α ↔ ∀ (x : α), ¬IsBot x
Module: Mathlib.Order.Max

Goal state before:
pp: α : Type u_3
inst✝ : PartialOrder α
i j : α
h : IsBot i
⊢ IsMin j ↔ j = i

Tactic:
[

Goal state after:
α : Type u_3
inst✝ : PartialOrder α
i j : α
h : IsBot i
⊢ IsMin j ↔ j = i
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✝ : α
⊢ x✝¹ ⊓ x✝ = if x✝¹ ≤ x✝ then x✝¹ else x✝

Tactic:
[

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✝ : α
⊢ x✝¹ ⊓ x✝ = if x✝¹ ≤ x✝ then x✝¹ else 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✝ : α
⊢ x✝¹ ⊔ x✝ = if x✝¹ ≤ x✝ then x✝ else x✝¹

Tactic:
[

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✝ : α
⊢ x✝¹ ⊔ x✝ = if x✝¹ ≤ x✝ then x✝ else 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✝ : α
⊢ Ord.compare x✝¹ x✝ = compareOfLessAndEq x✝¹ x✝

Tactic:
[

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✝ : α
⊢ Ord.compare x✝¹ x✝ = compareOfLessAndEq x✝¹ x✝
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : LT α
inst✝ : DenselyOrdered α
⊢ ∀ (a₁ a₂ : α), a₁ < a₂ → ∃ a, a < a₂ ∧ a₁ < a

Tactic:
[

Goal state after:
α : Type u_2
inst✝¹ : LT α
inst✝ : DenselyOrdered α
⊢ ∀ (a₁ a₂ : α), a₁ < a₂ → ∃ a, a < a₂ ∧ a₁ < a
Module: Mathlib.Order.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : DenselyOrdered α
inst✝ : DenselyOrdered β
a b : α × β
⊢ a < b → ∃ a_2, a < a_2 ∧ a_2 < b

Tactic:
[

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : DenselyOrdered α
inst✝ : DenselyOrdered β
a b : α × β
⊢ a < b → ∃ a_2, a < a_2 ∧ a_2 < b
Module: Mathlib.Order.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝¹ : (i : ι) → Preorder (π i)
inst✝ : ∀ (i : ι), DenselyOrdered (π i)
a b : (i : ι) → π i
⊢ a < b → ∃ a_2, a < a_2 ∧ a_2 < b

Tactic:
[

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝¹ : (i : ι) → Preorder (π i)
inst✝ : ∀ (i : ι), DenselyOrdered (π i)
a b : (i : ι) → π i
⊢ a < b → ∃ a_2, a < a_2 ∧ a_2 < b
Module: Mathlib.Order.Monotone.Defs

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : γ → α
g : γ → β
⊢ (Monotone fun x ↦ (f x, g x)) ↔ Monotone f ∧ Monotone g

Tactic:
[

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : γ → α
g : γ → β
⊢ (Monotone fun x ↦ (f x, g x)) ↔ Monotone f ∧ Monotone g
Module: Mathlib.Order.BoundedOrder.Lattice

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
a b : α
⊢ min a b = ⊥ ↔ a = ⊥ ∨ b = ⊥

Tactic:
[

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
a b : α
⊢ min a b = ⊥ ↔ a = ⊥ ∨ b = ⊥
Module: Mathlib.Order.PropInstances

Goal state before:
pp: ι : Type u_1
α' : ι → Type u_3
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → BoundedOrder (α' i)
f g : (i : ι) → α' i
⊢ IsCompl f g ↔ ∀ (i : ι), IsCompl (f i) (g i)

Tactic:
[

Goal state after:
ι : Type u_1
α' : ι → Type u_3
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → BoundedOrder (α' i)
f g : (i : ι) → α' i
⊢ IsCompl f g ↔ ∀ (i : ι), IsCompl (f i) (g i)
Module: Mathlib.Tactic.Lift

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
coeβα : β → α
condβα : α → Prop
coeδγ : δ → γ
condδγ : γ → Prop
inst✝¹ : CanLift α β coeβα condβα
inst✝ : CanLift γ δ coeδγ condδγ
x : α
y : γ
hx : condβα (x, y).fst
hy : condδγ (x, y).snd
⊢ ∃ y_1, map coeβα coeδγ y_1 = (x, y)

Tactic:
rcases CanLift.prf (β := β) x hx with ⟨x, rfl⟩

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
coeβα : β → α
condβα : α → Prop
coeδγ : δ → γ
condδγ : γ → Prop
inst✝¹ : CanLift α β coeβα condβα
inst✝ : CanLift γ δ coeδγ condδγ
y : γ
x : β
hx : condβα (coeβα x, y).fst
hy : condδγ (coeβα x, y).snd
⊢ ∃ y_1, map coeβα coeδγ y_1 = (coeβα x, y)
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
⊢ ¬Monotone f ∧ ¬Antitone f ↔ ∃ a b c, a < b ∧ b < c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)

Tactic:
[

Goal state after:
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
⊢ ¬Monotone f ∧ ¬Antitone f ↔ ∃ a b c, a < b ∧ b < c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
x y x' y' : α
h : IsCompl x y
h' : IsCompl x' y'
⊢ (x' ⊔ (x ⊔ y)) ⊓ (x' ⊔ x ⊔ y') = ⊤

Tactic:
h.sup_eq_top,

Goal state after:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
x y x' y' : α
h : IsCompl x y
h' : IsCompl x' y'
⊢ (x' ⊔ ⊤) ⊓ (x' ⊔ x ⊔ y') = ⊤
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : BoundedOrder α
inst✝ : BoundedOrder β
x y : α × β
⊢ IsCompl x y ↔ IsCompl x.fst y.fst ∧ IsCompl x.snd y.snd

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : BoundedOrder α
inst✝ : BoundedOrder β
x y : α × β
⊢ IsCompl x y ↔ IsCompl x.fst y.fst ∧ IsCompl x.snd y.snd
Module: Mathlib.Data.Set.Basic

Goal state before:
pp: α : Type u
s t : Set α
⊢ (s ∩ t).Nonempty ↔ ∃ x, x ∈ s ∧ x ∈ t

Tactic:
[

Goal state after:
α : Type u
s t : Set α
⊢ (s ∩ t).Nonempty ↔ ∃ x, x ∈ s ∧ x ∈ t
Module: Mathlib.Data.Set.Basic

Goal state before:
pp: α : Type u
s t : Set α
⊢ (s ∩ t).Nonempty ↔ ∃ x, x ∈ t ∧ x ∈ s

Tactic:
[

Goal state after:
α : Type u
s t : Set α
⊢ (s ∩ t).Nonempty ↔ ∃ x, x ∈ t ∧ x ∈ s
Module: Mathlib.Data.Set.Basic

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

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

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a b : Complementeds α
⊢ IsCompl ↑a ↑b ↔ IsCompl a b

Tactic:
[

Goal state after:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a b : Complementeds α
⊢ IsCompl ↑a ↑b ↔ IsCompl a b
Module: Mathlib.Data.Set.Basic

Goal state before:
pp: α : Type u
s : Set α
p q : α → Prop
⊢ {x | x ∈ s ∧ p x} = {x | x ∈ s ∧ q x} ↔ ∀ (x : α), x ∈ s → (p x ↔ q x)

Tactic:
[

Goal state after:
α : Type u
s : Set α
p q : α → Prop
⊢ {x | x ∈ s ∧ p x} = {x | x ∈ s ∧ q x} ↔ ∀ (x : α), x ∈ s → (p x ↔ q x)
Module: Mathlib.Data.Set.Basic

Goal state before:
pp: α : Type u
s : Set α
p : α → Prop
⊢ {x | x ∈ s ∧ p x} = s ↔ ∀ (x : α), x ∈ s → p x

Tactic:
[

Goal state after:
α : Type u
s : Set α
p : α → Prop
⊢ {x | x ∈ s ∧ p x} = s ↔ ∀ (x : α), x ∈ s → p x
Module: Mathlib.Data.Set.Basic

Goal state before:
pp: α : Type u
s : Set α
p : α → Prop
⊢ {x | x ∈ s ∧ p x} = ∅ ↔ ∀ (x : α), x ∈ s → ¬p x

Tactic:
[

Goal state after:
α : Type u
s : Set α
p : α → Prop
⊢ {x | x ∈ s ∧ p x} = ∅ ↔ ∀ (x : α), x ∈ s → ¬p x
Module: Mathlib.Data.Set.Insert

Goal state before:
pp: α : Type u_1
β : Type u_2
s t✝ : Set α
a b : α
inst✝ : DecidableEq α
t : Set α
x : α
h : ¬x ∈ t
⊢ RightInverse (fun y ↦ y.elim ⟨x, ⋯⟩ fun z ↦ ⟨↑z, ⋯⟩) fun y ↦ if h : ↑y = x then none else some ⟨↑y, ⋯⟩

Tactic:
rintro (_ | y) <;> grind

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

Goal state before:
pp: α : Type u
s : Set α
⊢ ¬s.Subsingleton ↔ s.Nontrivial

Tactic:
[

Goal state after:
α : Type u
s : Set α
⊢ ¬s.Subsingleton ↔ s.Nontrivial
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
⊢ d ≤ a ⇨ b ⇨ c ↔ d ≤ a ⊓ b ⇨ c

Tactic:
[

Goal state after:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
⊢ d ≤ a ⇨ b ⇨ c ↔ d ≤ a ⊓ b ⇨ c
Module: Mathlib.Order.Heyting.Basic

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

Tactic:
[

Goal state after:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c : α
⊢ a ⇨ b ⇨ c = b ⇨ a ⇨ c
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
⊢ d ≤ a ⇨ b ⊓ c ↔ d ≤ (a ⇨ b) ⊓ (a ⇨ c)

Tactic:
[

Goal state after:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
⊢ d ≤ a ⇨ b ⊓ c ↔ d ≤ (a ⇨ b) ⊓ (a ⇨ c)
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
⊢ a ≤ d ⇨ c ∧ b ≤ d ⇨ c ↔ d ≤ a ⇨ c ∧ d ≤ b ⇨ c

Tactic:
[

Goal state after:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
⊢ a ≤ d ⇨ c ∧ b ≤ d ⇨ c ↔ d ≤ a ⇨ c ∧ d ≤ b ⇨ c
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedHeytingAlgebra α
a✝ b✝ c✝ d a b c : α
⊢ a ⊓ (b ⊔ c) ≤ a ⊓ b ⊔ a ⊓ c

Tactic:
[

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedHeytingAlgebra α
a✝ b✝ c✝ d a b c : α
⊢ a ⊓ (b ⊔ c) ≤ a ⊓ b ⊔ a ⊓ c
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ (a \ b) \ c ≤ d ↔ a \ (b ⊔ c) ≤ d

Tactic:
[

Goal state after:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ (a \ b) \ c ≤ d ↔ a \ (b ⊔ c) ≤ d
Module: Mathlib.Order.Heyting.Basic

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

Tactic:
rw [sdiff_sdiff_comm, sdiff_self, bot_sdiff]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedCoheytingAlgebra α
a✝ b✝ c✝ d a b c : α
⊢ (a ⊔ b) ⊓ (a ⊔ c) ≤ a ⊔ b ⊓ c

Tactic:
[

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedCoheytingAlgebra α
a✝ b✝ c✝ d a b c : α
⊢ (a ⊔ b) ⊓ (a ⊔ c) ≤ a ⊔ b ⊓ c
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ (a ⊔ b)ᶜ = aᶜ ⊓ bᶜ

Tactic:
[

Goal state after:
α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ (a ⊔ b)ᶜ = aᶜ ⊓ bᶜ
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ a ⇨ bᶜ = b ⇨ aᶜ

Tactic:
[

Goal state after:
α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ a ⇨ bᶜ = b ⇨ aᶜ
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ Disjoint aᶜᶜ b ↔ Disjoint a b

Tactic:
[

Goal state after:
α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ Disjoint aᶜᶜ b ↔ Disjoint a b
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ Disjoint a bᶜᶜ ↔ Disjoint a b

Tactic:
[

Goal state after:
α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ Disjoint a bᶜᶜ ↔ Disjoint a b
Module: Mathlib.Logic.Equiv.Option

Goal state before:
pp: α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
h : ∃ x', e (some x) = some x'
⊢ some (e.removeNoneAux x) = e (some x)

Tactic:
by
  simp [removeNoneAux, Option.isSome_iff_exists.mpr h]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁶ : Max α
inst✝⁵ : Min α
inst✝⁴ : LE α
inst✝³ : LT α
inst✝² : Top α
inst✝¹ : HImp α
inst✝ : GeneralizedHeytingAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_top : f ⊤ = ⊤
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
a b c : α
⊢ a ≤ b ⇨ c ↔ a ⊓ b ≤ c

Tactic:
rw [← le, ← le, map_himp, map_inf, le_himp_iff]

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

Goal state before:
pp: α : Type u_1
a b : α
hab : a ≠ b
s : Set α
⊢ insert a (s \ {b}) = insert a s \ {b}

Tactic:
[

Goal state after:
α : Type u_1
a b : α
hab : a ≠ b
s : Set α
⊢ insert a (s \ {b}) = insert a s \ {b}
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
⊢ a ⊓ b \ c = b ⊓ a \ c

Tactic:
[

Goal state after:
α : Type u
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
⊢ a ⊓ b \ c = b ⊓ a \ c
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
⊢ a \ b ⊓ c = (a ⊓ c) \ (b ⊓ c)

Tactic:
[

Goal state after:
α : Type u
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
⊢ a \ b ⊓ c = (a ⊓ c) \ (b ⊓ c)
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ Disjoint (x \ z) y ↔ Disjoint x (y \ z)

Tactic:
[

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ Disjoint (x \ z) y ↔ Disjoint x (y \ z)

Tactic:
by
  simp_rw [disjoint_iff, sdiff_inf_right_comm, inf_sdiff_assoc]

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
[

Goal state after:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ∆ b = ⊥ ↔ a = b
Module: Mathlib.Order.SymmDiff

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

Tactic:
[

Goal state after:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
⊢ a ∆ b ≤ c ↔ a ≤ b ⊔ c ∧ b ≤ a ⊔ c
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
⊢ a ∆ b ⊓ c = (a ⊓ c) ∆ (b ⊓ c)

Tactic:
[

Goal state after:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
⊢ a ∆ b ⊓ c = (a ⊓ c) ∆ (b ⊓ c)
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: α : Sort u_1
inst✝ : DecidableEq α
a : α
⊢ Injective fun x ↦ swap x a

Tactic:
[

Goal state after:
α : Sort u_1
inst✝ : DecidableEq α
a : α
⊢ Injective fun x ↦ swap x a
Module: Mathlib.Order.SymmDiff

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

Tactic:
[

Goal state after:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
⊢ a ∆ (b ∆ c) = b ∆ (a ∆ c)
Module: Mathlib.Order.SymmDiff

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

Tactic:
[

Goal state after:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
⊢ a ∆ b ∆ c = a ∆ c ∆ b
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ a ∆ b ∆ (c ∆ d) = a ∆ c ∆ (b ∆ d)

Tactic:
[

Goal state after:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ a ∆ b ∆ (c ∆ d) = a ∆ c ∆ (b ∆ d)
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ⇔ (b ⇔ c) = b ⇔ (a ⇔ c)

Tactic:
[

Goal state after:
α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ⇔ (b ⇔ c) = b ⇔ (a ⇔ c)
Module: Mathlib.Order.SymmDiff

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

Tactic:
[

Goal state after:
α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ⇔ b ⇔ c = a ⇔ c ⇔ b
Module: Mathlib.Order.SymmDiff

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

Tactic:
bihimp_assoc,

Goal state after:
α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ⇔ (b ⇔ c) = a ⇔ (c ⇔ b)
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
a b c d : α
⊢ a ⇔ b ⇔ (c ⇔ d) = a ⇔ c ⇔ (b ⇔ d)

Tactic:
[

Goal state after:
α : Type u_2
inst✝ : BooleanAlgebra α
a b c d : α
⊢ a ⇔ b ⇔ (c ⇔ d) = a ⇔ c ⇔ (b ⇔ d)