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

Goal state before:
pp: 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

Tactic:
rfl

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✝² : ¬f a = f b
h✝¹ : ¬a < b
h✝ : a = b
⊢ False
Module: Mathlib.Order.Basic

Goal state before:
pp: 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

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: 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

Tactic:
grind

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

Goal state before:
pp: a : Bool
⊢ ((!a) = true) = (a = false)

Tactic:
grind

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

Goal state before:
pp: a b : Bool
⊢ ((a && b) = false) = (a = false ∨ b = false)

Tactic:
grind

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

Goal state before:
pp: a b : Bool
⊢ ((a || b) = false) = (a = false ∧ b = false)

Tactic:
grind

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

Goal state before:
pp: a : Bool
⊢ ((!a) = false) = (a = true)

Tactic:
grind

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

Goal state before:
pp: b : Bool
⊢ ¬b = true ↔ b = false

Tactic:
grind

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

Goal state before:
pp: a b : Bool
⊢ (a ^^ b) = true ↔ Xor (a = true) (b = true)

Tactic:
grind

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

Goal state before:
pp: b : Bool
⊢ b = false ∨ b = true

Tactic:
grind

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

Goal state before:
pp: a b : Bool
H : b = true
⊢ (a || b) = true

Tactic:
grind

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

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

Tactic:
grind

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

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

Tactic:
rfl

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

Goal state before:
pp: case true
⊢ (true.toNat == 1) = true

Tactic:
rfl

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

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : Bot γ
x : α → β
⊢ ⊥ ∘ x = ⊥

Tactic:
rfl

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

Goal state before:
pp: case inr.inr.refine_1
n m : ℕ
h : m < n
hm : m ≠ 0
⊢ 0 < n - m

Tactic:
grind

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

Goal state before:
pp: case inr.inr.refine_2
n m : ℕ
h : m < n
hm : m ≠ 0
⊢ n - m < n

Tactic:
grind

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
δ : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
f : α → γ
g : β → δ
hf : StrictAnti f
hg : StrictAnti g
a b : α × β
⊢ a < b → Prod.map f g b < Prod.map f g a

Tactic:
by
  simp only [Prod.lt_iff]
  exact Or.imp (And.imp hf.imp hg.antitone.imp) (And.imp hf.antitone.imp hg.imp)

Goal state after:
Module: Mathlib.Order.RelClasses

Goal state before:
pp: α : Type u
β : Type v
r✝ : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a b c : α
hab : r a b
hbc : r b c
⊢ r a c

Tactic:
rcases trichotomous_of r a c with (hac | rfl | hca)
    · exact hac
    · exact asymm_of r hab hbc |>.elim
    · exact IsWellFounded.wf.asymmetric₃ a b c hab hbc hca |>.elim

Goal state after:
Module: Mathlib.Order.RelClasses

Goal state before:
pp: α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
x✝¹ x✝ : α × β
a₁ : α
a₂ : β
hab hba : ¬Prod.Lex r s (a₁, a₂) (a₁, a₂)
⊢ (a₁, a₂) = (a₁, a₂)

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.RelClasses

Goal state before:
pp: α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝ : LinearOrder α
⊢ ∀ (a b : α), ¬a < b → ¬b < a → a = b

Tactic:
grind

Goal state after:
Module: Mathlib.Order.BoundedOrder.Lattice

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
a b : α
ha : a ≠ ⊥
hb : b ≠ ⊥
⊢ min a b ≠ ⊥

Tactic:
grind

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
a b : α
hab : Disjoint a b
⊢ a = b ↔ a = ⊥ ∧ b = ⊥

Tactic:
grind

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
a b : α
hab : Disjoint a b
⊢ a ≠ b ↔ a ≠ ⊥ ∨ b ≠ ⊥

Tactic:
grind

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
a b : α
h : a ≤ b
⊢ Disjoint a b ↔ a = ⊥

Tactic:
grind

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : BoundedOrder α
a b : α
h : Disjoint a b
ha : a ≠ ⊥
⊢ b ≠ ⊤

Tactic:
grind

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s : Set α
hf : StrictMonoOn f s
a : α
ha hb : a ∈ s
⊢ f a = f a

Tactic:
rfl

Goal state after:
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, m ≤ b ∧ f m = f (m + 1)

Tactic:
by
    contrapose! hfb
    let rec strictMono : ∀ m ≤ b + 1, m ≤ f m
    | 0, _ => Nat.zero_le _
    | m + 1, hmb => (strictMono _ <| m.le_succ.trans hmb).trans_lt <| (hfmono m.le_succ).lt_of_ne <|
        hfb _ <| Nat.le_of_succ_le_succ hmb
    exact ⟨b + 1, strictMono _ le_rfl⟩

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

Goal state before:
pp: case zero
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n →
      ∀ {f : ℕ → ℕ},
        Antitone f →
          (∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)) → f 0 = m → ∃ n, n ≤ m ∧ ∀ (m : ℕ), n ≤ m → f m = f n
f : ℕ → ℕ
hfmono : Antitone f
hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)
h : f 0 = n
heq : f 0 = f 1
⊢ f 0 = f (0 + 1)

Tactic:
grind

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

Goal state before:
pp: case succ
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n →
      ∀ {f : ℕ → ℕ},
        Antitone f →
          (∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)) → f 0 = m → ∃ n, n ≤ m ∧ ∀ (m : ℕ), n ≤ m → f m = f n
f : ℕ → ℕ
hfmono : Antitone f
hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)
h : f 0 = n
heq : f 0 = f 1
n✝ : ℕ
a✝ : f n✝ = f (n✝ + 1)
⊢ f (n✝ + 1) = f (n✝ + 1 + 1)

Tactic:
grind

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

Goal state before:
pp: case zero
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n →
      ∀ {f : ℕ → ℕ},
        Antitone f →
          (∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)) → f 0 = m → ∃ n, n ≤ m ∧ ∀ (m : ℕ), n ≤ m → f m = f n
f : ℕ → ℕ
hfmono : Antitone f
hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)
h : f 0 = n
heq : f 0 = f 1
flat : ∀ (j : ℕ), f j = f (j + 1)
x✝ : 0 ≤ 0
⊢ f 0 = f 0

Tactic:
grind

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

Goal state before:
pp: case succ
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n →
      ∀ {f : ℕ → ℕ},
        Antitone f →
          (∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)) → f 0 = m → ∃ n, n ≤ m ∧ ∀ (m : ℕ), n ≤ m → f m = f n
f : ℕ → ℕ
hfmono : Antitone f
hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)
h : f 0 = n
heq : f 0 = f 1
flat : ∀ (j : ℕ), f j = f (j + 1)
n✝ : ℕ
a✝ : 0 ≤ n✝ → f n✝ = f 0
x✝ : 0 ≤ n✝ + 1
⊢ f (n✝ + 1) = f 0

Tactic:
grind

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

Goal state before:
pp: α : Type u
s : Set α
inst✝ : Subsingleton α
x : α
hx : x ∈ s
y : α
⊢ y ∈ s

Tactic:
by rwa [Subsingleton.elim y x]

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

Goal state before:
pp: α : Type u
s t : Set α
⊢ ¬Disjoint s t ↔ ∃ x, x ∈ s ∧ x ∈ t

Tactic:
grind

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

Goal state before:
pp: α : Type u
s t : Set α
⊢ Disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ t → a ≠ b

Tactic:
grind

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

Goal state before:
pp: n : ℕ
ih :
  ∀ (m : ℕ),
    m < n →
      ∀ {f : ℕ → ℕ},
        Antitone f →
          (∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)) → f 0 = m → ∃ n, n ≤ m ∧ ∀ (m : ℕ), n ≤ m → f m = f n
f : ℕ → ℕ
hfmono : Antitone f
hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)
h : f 0 = n
heq : ¬f 0 = f 1
hlt : f 1 < f 0
g : ℕ → ℕ := fun i ↦ f (i + 1)
hg_anti : Antitone g
⊢ f 1 < n

Tactic:
grind

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

Goal state before:
pp: n : ℕ
ih :
  ∀ (m : ℕ),
    m < n →
      ∀ {f : ℕ → ℕ},
        Antitone f →
          (∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)) → f 0 = m → ∃ n, n ≤ m ∧ ∀ (m : ℕ), n ≤ m → f m = f n
f : ℕ → ℕ
hfmono : Antitone f
hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)
h : f 0 = n
heq : ¬f 0 = f 1
hlt : f 1 < f 0
g : ℕ → ℕ := fun i ↦ f (i + 1)
hg_anti : Antitone g
⊢ ∀ (m : ℕ), g m = g (m + 1) → g (m + 1) = g (m + 2)

Tactic:
grind

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

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

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
s t : Set α
a : α
⊢ ¬a ∈ s → s ≠ insert a t

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
s : Set α
a : α
⊢ insert a s = s ↔ a ∈ s

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
s : Set α
a : α
⊢ insert a s ≠ s ↔ ¬a ∈ s

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
s t : Set α
a : α
⊢ insert a s ⊆ t ↔ a ∈ t ∧ s ⊆ t

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
s t : Set α
a : α
ha : a ∈ t
hs : s ⊆ t
⊢ insert a s ⊆ t

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
s t : Set α
a : α
h : s ⊆ t
⊢ insert a s ⊆ insert a t

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
s t : Set α
a : α
ha : ¬a ∈ s
⊢ insert a s ⊆ insert a t ↔ s ⊆ t

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
s t : Set α
a : α
ha : ¬a ∈ s
⊢ s ⊆ insert a t ↔ s ⊆ t

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
s t : Set α
⊢ s ⊂ t ↔ ∃ a, ¬a ∈ s ∧ insert a s ⊆ t

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
s t : Set α
a : α
hst : s ⊆ t
hat : a ∈ t
has : ¬a ∈ s
⊢ s ⊂ t

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
s : Set α
a : α
h : ¬a ∈ s
⊢ s ⊂ insert a s

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
a b : α
s : Set α
⊢ insert a (insert b s) = insert b (insert a s)

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
a : α
s : Set α
⊢ insert a (insert a s) = insert a s

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
s t : Set α
a : α
⊢ insert a s ∪ t = insert a (s ∪ t)

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
s t : Set α
a : α
⊢ s ∪ insert a t = insert a (s ∪ t)

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
a : α
s t : Set α
⊢ insert a (s ∩ t) = insert a s ∩ insert a t

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
a : α
s t : Set α
⊢ insert a (s ∪ t) = insert a s ∪ insert a t

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
P : α → Prop
a : α
s : Set α
H : ∀ (x : α), x ∈ insert a s → P x
x : α
h : x ∈ s
⊢ P x

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
P : α → Prop
a : α
s : Set α
H : ∀ (x : α), x ∈ s → P x
ha : P a
x : α
h : x ∈ insert a s
⊢ P x

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
P : α → Prop
a : α
s : Set α
⊢ (∃ x, x ∈ insert a s ∧ P x) ↔ P a ∨ ∃ x, x ∈ s ∧ P x

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
P : α → Prop
a : α
s : Set α
⊢ (∀ (x : α), x ∈ insert a s → P x) ↔ P a ∧ ∀ (x : α), x ∈ s → P x

Tactic:
grind

Goal state after:
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
y : { i // i ∈ insert x t }
h : ¬↑y = x
⊢ ↑y ∈ t

Tactic:
grind

Goal state after:
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
y : Option { i // i ∈ t }
z : { i // i ∈ t }
⊢ ↑z ∈ insert x t

Tactic:
grind

Goal state after:
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
y : { i // i ∈ insert x t }
⊢ (fun y ↦ y.elim ⟨x, ⋯⟩ fun z ↦ ⟨↑z, ⋯⟩) ((fun y ↦ if h : ↑y = x then none else some ⟨↑y, ⋯⟩) y) = y

Tactic:
grind

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

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

Tactic:
grind

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

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

Tactic:
grind

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

Goal state before:
pp: case neg
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n →
      ∀ {f : ℕ → ℕ},
        Antitone f →
          (∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)) → f 0 = m → ∃ n, n ≤ m ∧ ∀ (m : ℕ), n ≤ m → f m = f n
f : ℕ → ℕ
hfmono : Antitone f
hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)
h : f 0 = n
heq : ¬f 0 = f 1
hlt : f 1 < f 0
g : ℕ → ℕ := fun i ↦ f (i + 1)
hg_anti : Antitone g
p : ℕ
hp : p ≤ f 1
m : ℕ
hp' : g (m - 1) = g p
hm : p + 1 ≤ m
⊢ f m = f (p + 1)

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
s : Set α
x✝ : ∃ a, s = {a}
a : α
h : s = {a}
⊢ (fun a ↦ a ∈ s) a ∧ ∀ (y : α), (fun a ↦ a ∈ s) y → y = a

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
s : Set α
x✝ : ∃! a, a ∈ s
a : α
h : (fun a ↦ a ∈ s) a ∧ ∀ (y : α), (fun a ↦ a ∈ s) y → y = a
⊢ s = {a}

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
s : Set α
x : α
⊢ s ⊆ {x} ↔ s = ∅ ∨ s = {x}

Tactic:
grind

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

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

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
s t : Set α
a : α
h : a ∈ s
⊢ s ∩ insert a t = insert a (s ∩ t)

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
s t : Set α
a : α
h : a ∈ t
⊢ insert a s ∩ t = insert a (s ∩ t)

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
s t : Set α
a : α
h : ¬a ∈ s
⊢ s ∩ insert a t = s ∩ t

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
s t : Set α
a : α
h : ¬a ∈ t
⊢ insert a s ∩ t = s ∩ t

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
s : Set α
a b : α
⊢ {a, b} ⊆ s ↔ a ∈ s ∧ b ∈ s

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
s : Set α
a b : α
⊢ s ⊆ {a, b} ↔ ∀ (x : α), x ∈ s → x = a ∨ x = b

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
s : Set α
x y : α
⊢ s ⊆ {x, y} → s = ∅ ∨ s = {x} ∨ s = {y} ∨ s = {x, y}

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
s : Set α
x y : α
⊢ s = ∅ ∨ s = {x} ∨ s = {y} ∨ s = {x, y} → s ⊆ {x, y}

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
x y : β
hp : ∃ a, p a
hn : ∃ a, ¬p a
⊢ (range fun a ↦ if p a then x else y) = {x, y}

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
x : α
⊢ 𝒫 {x} = {∅, {x}}

Tactic:
grind

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

Goal state before:
pp: α : Type u_3
β : Type u_4
a : α
⊢ Prod.fst ⁻¹' {a} = range fun x ↦ (a, x)

Tactic:
grind

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

Goal state before:
pp: α : Type u_3
β : Type u_4
b : β
⊢ Prod.snd ⁻¹' {b} = range fun x ↦ (x, b)

Tactic:
grind

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝ : LinearOrder α
a b c : α
⊢ a ≤ max b c ↔ a ≤ b ∨ a ≤ c

Tactic:
grind

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝ : LinearOrder α
a b c : α
⊢ a < max b c ↔ a < b ∨ a < c

Tactic:
grind

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case le
α : Type u
β : Type v
e : α ≃ β
inst✝ : Preorder β
le : LE α := e.le
lt : LT α := e.lt
x✝ y✝ : α
⊢ e x✝ ≤ e y✝ ↔ x✝ ≤ y✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case lt
α : Type u
β : Type v
e : α ≃ β
inst✝ : Preorder β
le : LE α := e.le
lt : LT α := e.lt
x✝ y✝ : α
⊢ e x✝ < e y✝ ↔ x✝ < y✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.Lattice

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

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case lt
α : Type u
β : Type v
e : α ≃ β
inst✝ : PartialOrder β
preorder : Preorder α := e.preorder
x✝ y✝ : α
⊢ e x✝ < e y✝ ↔ x✝ < y✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case le
α : Type u
β : Type v
e : α ≃ β
inst✝¹ : LinearOrder β
inst✝ : DecidableEq α
max : Max α := e.max
min : Min α := e.min
preorder : Preorder α := e.preorder
compare : Ord α := e.ord
x✝ y✝ : α
⊢ e x✝ ≤ e y✝ ↔ x✝ ≤ y✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case lt
α : Type u
β : Type v
e : α ≃ β
inst✝¹ : LinearOrder β
inst✝ : DecidableEq α
max : Max α := e.max
min : Min α := e.min
preorder : Preorder α := e.preorder
compare : Ord α := e.ord
x✝ y✝ : α
⊢ e x✝ < e y✝ ↔ x✝ < y✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case min
α : Type u
β : Type v
e : α ≃ β
inst✝¹ : LinearOrder β
inst✝ : DecidableEq α
max : Max α := e.max
min : Min α := e.min
preorder : Preorder α := e.preorder
compare : Ord α := e.ord
x✝ y✝ : α
⊢ e (x✝ ⊓ y✝) = Min.min (e x✝) (e y✝)

Tactic:
rfl

Goal state after:
case min
α : Type u
β : Type v
e : α ≃ β
inst✝¹ : LinearOrder β
inst✝ : DecidableEq α
max : Max α := e.max
min : Min α := e.min
preorder : Preorder α := e.preorder
compare : Ord α := e.ord
x✝ y✝ : α
⊢ e (x✝ ⊓ y✝) = Min.min (e x✝) (e y✝)
Module: Mathlib.Order.Lattice

Goal state before:
pp: case max
α : Type u
β : Type v
e : α ≃ β
inst✝¹ : LinearOrder β
inst✝ : DecidableEq α
max : Max α := e.max
min : Min α := e.min
preorder : Preorder α := e.preorder
compare : Ord α := e.ord
x✝ y✝ : α
⊢ e (x✝ ⊔ y✝) = Max.max (e x✝) (e y✝)

Tactic:
rfl

Goal state after:
case max
α : Type u
β : Type v
e : α ≃ β
inst✝¹ : LinearOrder β
inst✝ : DecidableEq α
max : Max α := e.max
min : Min α := e.min
preorder : Preorder α := e.preorder
compare : Ord α := e.ord
x✝ y✝ : α
⊢ e (x✝ ⊔ y✝) = Max.max (e x✝) (e y✝)
Module: Mathlib.Order.Lattice

Goal state before:
pp: case compare
α : Type u
β : Type v
e : α ≃ β
inst✝¹ : LinearOrder β
inst✝ : DecidableEq α
max : Max α := e.max
min : Min α := e.min
preorder : Preorder α := e.preorder
compare : Ord α := e.ord
x✝ y✝ : α
⊢ Ord.compare (e x✝) (e y✝) = Ord.compare x✝ y✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case le
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeSup β
max : Max α := e.max
partialOrder : PartialOrder α := e.partialOrder
x✝ y✝ : α
⊢ e x✝ ≤ e y✝ ↔ x✝ ≤ y✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case lt
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeSup β
max : Max α := e.max
partialOrder : PartialOrder α := e.partialOrder
x✝ y✝ : α
⊢ e x✝ < e y✝ ↔ x✝ < y✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case map_sup
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeSup β
max : Max α := e.max
partialOrder : PartialOrder α := e.partialOrder
a✝ b✝ : α
⊢ e (a✝ ⊔ b✝) = e a✝ ⊔ e b✝

Tactic:
rfl

Goal state after:
case map_sup
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeSup β
max : Max α := e.max
partialOrder : PartialOrder α := e.partialOrder
a✝ b✝ : α
⊢ e (a✝ ⊔ b✝) = e a✝ ⊔ e b✝
Module: Mathlib.Order.Lattice

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

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

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case le
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeInf β
min : Min α := e.min
partialOrder : PartialOrder α := e.partialOrder
x✝ y✝ : α
⊢ e y✝ ≤ e x✝ ↔ y✝ ≤ x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case lt
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeInf β
min : Min α := e.min
partialOrder : PartialOrder α := e.partialOrder
x✝ y✝ : α
⊢ e y✝ < e x✝ ↔ y✝ < x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case map_inf
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeInf β
min : Min α := e.min
partialOrder : PartialOrder α := e.partialOrder
a✝ b✝ : α
⊢ e (a✝ ⊓ b✝) = e a✝ ⊓ e b✝

Tactic:
rfl

Goal state after:
case map_inf
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeInf β
min : Min α := e.min
partialOrder : PartialOrder α := e.partialOrder
a✝ b✝ : α
⊢ e (a✝ ⊓ b✝) = e a✝ ⊓ e b✝
Module: Mathlib.Order.Lattice

Goal state before:
pp: case le
α : Type u
β : Type v
e : α ≃ β
inst✝ : Lattice β
semilatticeSup : SemilatticeSup α := e.semilatticeSup
semilatticeInf : SemilatticeInf α := e.semilatticeInf
x✝ y✝ : α
⊢ e x✝ ≤ e y✝ ↔ x✝ ≤ y✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case lt
α : Type u
β : Type v
e : α ≃ β
inst✝ : Lattice β
semilatticeSup : SemilatticeSup α := e.semilatticeSup
semilatticeInf : SemilatticeInf α := e.semilatticeInf
x✝ y✝ : α
⊢ e x✝ < e y✝ ↔ x✝ < y✝

Tactic:
rfl

Goal state after: