awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ (s ×ˢ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty

Tactic:
nonempty_product

Premises used: Finset.nonempty_product
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ (s ×ˢ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty

Tactic:
exact nonempty_product

Premises used: Finset.nonempty_product
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
t : Finset β
a : α
h :
  ∀ (x : α) (y : β),
    (x, y) ∈ SProd.sprod (α := Finset α) {a} t ↔ (x, y) ∈ map { toFun := Prod.mk a, inj' := ⋯ : β ↪ α × β } t
⊢ SProd.sprod (α := Finset α) {a} t = map { toFun := Prod.mk a, inj' := ⋯ } t

Tactic:
ext ⟨x, y⟩
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
t : Finset β
a x : α
y : β
⊢ (x, y) ∈ SProd.sprod (α := Finset α) {a} t ↔ (x, y) ∈ map { toFun := Prod.mk a, inj' := ⋯ : β ↪ α × β } t

Tactic:
simp [and_left_comm, eq_comm]

Premises used: and_left_comm, eq_comm
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
s : Finset α
b : β
h :
  ∀ (x : α) (y : β),
    (x, y) ∈ SProd.sprod (β := Finset β) s {b} ↔ (x, y) ∈ map { toFun := fun (i : α) ↦ (i, b), inj' := ⋯ : α ↪ α × β } s
⊢ SProd.sprod (β := Finset β) s {b} = map { toFun := fun (i : α) ↦ (i, b), inj' := ⋯ } s

Tactic:
ext ⟨x, y⟩
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
s : Finset α
b : β
x : α
y : β
⊢ (x, y) ∈ SProd.sprod (β := Finset β) s {b} ↔ (x, y) ∈ map { toFun := fun (i : α) ↦ (i, b), inj' := ⋯ : α ↪ α × β } s

Tactic:
simp [and_left_comm, eq_comm]

Premises used: and_left_comm, eq_comm
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
a : α
b : β
⊢ SProd.sprod (α := Finset α) (β := Finset β) {a} {b} = {(a, b)}

Tactic:
simp only [product_singleton, Function.Embedding.coeFn_mk, map_singleton]

Premises used: Finset.product_singleton, Finset.map_singleton, Function.Embedding.coeFn_mk
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
s s' : Finset α
t : Finset β
inst : DecidableEq α
inst_1 : DecidableEq β
⊢ (s ∪ s') ×ˢ t = s ×ˢ t ∪ s' ×ˢ t

Tactic:
grind
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t t' : Finset β
inst : DecidableEq α
inst_1 : DecidableEq β
⊢ s ×ˢ (t ∪ t') = s ×ˢ t ∪ s ×ˢ t'

Tactic:
grind
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
s s' : Finset α
t : Finset β
inst : DecidableEq α
inst_1 : DecidableEq β
⊢ (s ∩ s') ×ˢ t = s ×ˢ t ∩ s' ×ˢ t

Tactic:
grind
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t t' : Finset β
inst : DecidableEq α
inst_1 : DecidableEq β
⊢ s ×ˢ (t ∩ t') = s ×ˢ t ∩ s ×ˢ t'

Tactic:
grind
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
s s' : Finset α
t t' : Finset β
inst : DecidableEq α
inst_1 : DecidableEq β
⊢ s ×ˢ t ∩ s' ×ˢ t' = (s ∩ s') ×ˢ (t ∩ t')

Tactic:
grind
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
s s' : Finset α
t t' : Finset β
simp_rw :
  Disjoint (↑(s ×ˢ t) : Set (α × β)) (↑(s' ×ˢ t') : Set (α × β)) ↔
    Disjoint (↑s : Set α) (↑s' : Set α) ∨ Disjoint (↑t : Set β) (↑t' : Set β)
simp_rw₁ :
  Disjoint ((↑s : Set α) ×ˢ (↑t : Set β)) ((↑s' : Set α) ×ˢ (↑t' : Set β)) ↔
    Disjoint (↑s : Set α) (↑s' : Set α) ∨ Disjoint (↑t : Set β) (↑t' : Set β)
⊢ Disjoint (s ×ˢ t) (s' ×ˢ t') ↔ Disjoint s s' ∨ Disjoint t t'

Tactic:
simp_rw [← disjoint_coe, coe_product, Set.disjoint_prod]

Premises used: Finset.disjoint_coe, Set.disjoint_prod, Finset.coe_product
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
s s' : Finset α
t : Finset β
hs : Disjoint s s'
⊢ s.disjUnion s' hs ×ˢ t = (s ×ˢ t).disjUnion (s' ×ˢ t) ⋯

Tactic:
eq_of_veq <| Multiset.add_product _ _ _

Premises used: Finset.eq_of_veq, Multiset.add_product
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t t' : Finset β
ht : Disjoint t t'
⊢ s ×ˢ t.disjUnion t' ht = (s ×ˢ t).disjUnion (s ×ˢ t') ⋯

Tactic:
eq_of_veq <| Multiset.product_add _ _ _

Premises used: Finset.eq_of_veq, Multiset.product_add
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Finset α
⊢ Function.Injective (β := α × α) fun (a : α) ↦ (a, a)

Tactic:
simp [Function.Injective]

Premises used: Function.Injective
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Finset α
mk :
  ∀ (val : Multiset α) (s : List α) (hs : Nodup (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) s)),
    Nodup
      (Quotient.map List.offDiag ⋯
        { val := Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) s, nodup := hs : Finset α }.val)
⊢ Nodup (Quotient.map List.offDiag ⋯ s.val)

Tactic:
rcases s with ⟨⟨s⟩, hs⟩
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset α
val : Multiset α
s : List α
hs : Nodup (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) s)
⊢ Nodup
    (Quotient.map List.offDiag ⋯
      { val := Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) s, nodup := hs : Finset α }.val)

Tactic:
hs.offDiag

Premises used: Multiset.Nodup, List.Nodup.offDiag
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset α
val : Multiset α
s : List α
hs : Nodup (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) s)
⊢ Nodup
    (Quotient.map List.offDiag ⋯
      { val := Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) s, nodup := hs : Finset α }.val)

Tactic:
exact hs.offDiag

Premises used: List.Nodup.offDiag
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
s : Finset α
x : α × α
⊢ x ∈ s.diag ↔ x.1 ∈ s ∧ x.1 = x.2

Tactic:
aesop (add simp diag)

Premises used: Finset.diag
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
s : Finset α
x : α × α
mk :
  ∀ (val : Multiset α) (s : List α) (hs : Nodup (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) s)),
    x ∈ { val := Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) s, nodup := hs : Finset α }.offDiag ↔
      x.1 ∈ { val := Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) s, nodup := hs : Finset α } ∧
        x.2 ∈ { val := Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) s, nodup := hs : Finset α } ∧ x.1 ≠ x.2
⊢ x ∈ s.offDiag ↔ x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2

Tactic:
rcases s with ⟨⟨s⟩, hs⟩
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
x : α × α
val : Multiset α
s : List α
hs : Nodup (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) s)
⊢ x ∈ { val := Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) s, nodup := hs : Finset α }.offDiag ↔
    x.1 ∈ { val := Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) s, nodup := hs : Finset α } ∧
      x.2 ∈ { val := Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) s, nodup := hs : Finset α } ∧ x.1 ≠ x.2

Tactic:
hs.mem_offDiag

Premises used: Set.Mem, setOf, Multiset.Mem, List.Nodup.mem_offDiag
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
x : α × α
val : Multiset α
s : List α
hs : Nodup (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) s)
⊢ x ∈ { val := Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) s, nodup := hs : Finset α }.offDiag ↔
    x.1 ∈ { val := Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) s, nodup := hs : Finset α } ∧
      x.2 ∈ { val := Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) s, nodup := hs : Finset α } ∧ x.1 ≠ x.2

Tactic:
exact hs.mem_offDiag

Premises used: List.Nodup.mem_offDiag
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
s : Finset α
⊢ s.diag.Nonempty ↔ s.Nonempty

Tactic:
simp [diag]

Premises used: Finset.diag
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
s : Finset α
⊢ s.diag = ∅ ↔ s = ∅

Tactic:
simp [diag]

Premises used: Finset.diag
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
h : ∀ (a : α × α), a ∈ s.diag ↔ a ∈ {a ∈ s ×ˢ s | a.1 = a.2}
⊢ s.diag = {a ∈ s ×ˢ s | a.1 = a.2}

Tactic:
ext
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
a : α × α
⊢ a ∈ s.diag ↔ a ∈ {a ∈ s ×ˢ s | a.1 = a.2}

Tactic:
simp +contextual
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α × α → β
s : Finset α
⊢ image f s.diag = image (fun (x : α) ↦ f (x, x)) s

Tactic:
grind
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
s : Finset α
⊢ (↑s.offDiag : Set (α × α)) = (↑s : Set α).offDiag

Tactic:
Set.ext fun _ => mem_offDiag

Premises used: Set.ext, Finset.mem_offDiag
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
s : Finset α
⊢ #s.diag = #s

Tactic:
simp [diag]

Premises used: Finset.diag
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
s : Finset α
rw : #s.offDiag = HPow.hPow (β := ℕ) (#s) 2 - #s
⊢ #s.offDiag = #s * #s - #s

Tactic:
rw [← sq]

Premises used: sq
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
s : Finset α
mk :
  ∀ (val : Multiset α) (s : List α) (hs : Nodup (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) s)),
    #{ val := Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) s, nodup := hs : Finset α }.offDiag =
      HPow.hPow (β := ℕ) (#{ val := Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) s, nodup := hs : Finset α })
          2 -
        #{ val := Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) s, nodup := hs : Finset α }
⊢ #s.offDiag = HPow.hPow (β := ℕ) (#s) 2 - #s

Tactic:
rcases s with ⟨⟨s⟩, hs⟩
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
val : Multiset α
s : List α
hs : Nodup (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) s)
⊢ #{ val := Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) s, nodup := hs : Finset α }.offDiag =
    HPow.hPow (β := ℕ) (#{ val := Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) s, nodup := hs : Finset α }) 2 -
      #{ val := Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) s, nodup := hs : Finset α }

Tactic:
apply List.length_offDiag

Premises used: List.length_offDiag
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
x x_1 : Finset α
⊢ x ≤ x_1 → x.diag ≤ x_1.diag

Tactic:
simp [diag]

Premises used: Finset.diag
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
⊢ Monotone.{u_1, u_1} (α := Finset α) offDiag

Tactic:
fun _ _ h _ hx =>
  mem_offDiag.2 <| And.imp (@h _) (And.imp_left <| @h _) <| mem_offDiag.1 hx

Premises used: Iff.mpr, And.imp, Monotone, And.imp_left, Iff.mp, Finset.mem_offDiag
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Finset (α × α)) (diag ∅) ∅

Tactic:
rfl

Premises used: Multiset.map, List.map, Finset.map, Multiset.zero, Finset.diag, Finset.empty, Multiset.ofList, rfl
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Finset (α × α)) (offDiag ∅) ∅

Tactic:
rfl

Premises used: Quotient.map, Multiset.zero, Finset.empty, List.offDiag, Finset.offDiag, Multiset.ofList, Quot.map, rfl, List.flatten
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
⊢ s.diag ∪ s.offDiag = s ×ˢ s

Tactic:
grind
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
s : Finset α
⊢ Disjoint s.diag s.offDiag

Tactic:
simp [disjoint_left]

Premises used: Finset.disjoint_left
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
⊢ s ×ˢ s \ s.diag = s.offDiag

Tactic:
grind
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
⊢ s ×ˢ s \ s.offDiag = s.diag

Tactic:
grind
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
s t : Finset α
inst : DecidableEq α
⊢ (s ∩ t).diag = s.diag ∩ t.diag

Tactic:
grind
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
s t : Finset α
inst : DecidableEq α
push_cast : ((↑s : Set α) ∩ (↑t : Set α)).offDiag = (↑s : Set α).offDiag ∩ (↑t : Set α).offDiag
⊢ (↑(s ∩ t).offDiag : Set (α × α)) = (↑(s.offDiag ∩ t.offDiag) : Set (α × α))

Tactic:
push_cast
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
s t : Finset α
inst : DecidableEq α
⊢ ((↑s : Set α) ∩ (↑t : Set α)).offDiag = (↑s : Set α).offDiag ∩ (↑t : Set α).offDiag

Tactic:
Set.offDiag_inter _ _

Premises used: Set.offDiag_inter
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
s t : Finset α
inst : DecidableEq α
⊢ ((↑s : Set α) ∩ (↑t : Set α)).offDiag = (↑s : Set α).offDiag ∩ (↑t : Set α).offDiag

Tactic:
exact Set.offDiag_inter _ _

Premises used: Set.offDiag_inter
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
s t : Finset α
inst : DecidableEq α
⊢ (s ∪ t).diag = s.diag ∪ t.diag

Tactic:
grind
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
s t : Finset α
inst : DecidableEq α
h : Disjoint s t
push_cast :
  ((↑s : Set α) ∪ (↑t : Set α)).offDiag =
    (↑s : Set α).offDiag ∪ (↑t : Set α).offDiag ∪ (↑s : Set α) ×ˢ (↑t : Set α) ∪ (↑t : Set α) ×ˢ (↑s : Set α)
⊢ (↑(s ∪ t).offDiag : Set (α × α)) = (↑(s.offDiag ∪ t.offDiag ∪ s ×ˢ t ∪ t ×ˢ s) : Set (α × α))

Tactic:
push_cast
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
s t : Finset α
inst : DecidableEq α
h : Disjoint s t
⊢ ((↑s : Set α) ∪ (↑t : Set α)).offDiag =
    (↑s : Set α).offDiag ∪ (↑t : Set α).offDiag ∪ (↑s : Set α) ×ˢ (↑t : Set α) ∪ (↑t : Set α) ×ˢ (↑s : Set α)

Tactic:
Set.offDiag_union (disjoint_coe.2 h)

Premises used: Iff.mpr, Finset.disjoint_coe, Set.offDiag_union
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
s t : Finset α
inst : DecidableEq α
h : Disjoint s t
⊢ ((↑s : Set α) ∪ (↑t : Set α)).offDiag =
    (↑s : Set α).offDiag ∪ (↑t : Set α).offDiag ∪ (↑s : Set α) ×ˢ (↑t : Set α) ∪ (↑t : Set α) ×ˢ (↑s : Set α)

Tactic:
exact Set.offDiag_union (disjoint_coe.2 h)

Premises used: Iff.mpr, Finset.disjoint_coe, Set.offDiag_union
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
a : α
⊢ Eq (α := Finset (α × α)) (offDiag {a}) ∅

Tactic:
simp [← Finset.card_eq_zero]

Premises used: Finset.card_eq_zero
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
a : α
⊢ Eq (α := Finset (α × α)) (diag {a}) {(a, a)}

Tactic:
grind
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
a : α
⊢ (insert a s).diag = insert (a, a) s.diag

Tactic:
grind
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
a : α
has : a ∉ s
⊢ (insert a s).offDiag = s.offDiag ∪ SProd.sprod (α := Finset α) {a} s ∪ SProd.sprod (β := Finset α) s {a}

Tactic:
grind
-- Module: Mathlib.Data.Finset.Prod
Goal:
ι : Type u_4
inst : PartialOrder ι
inst_1 : DecidableLE ι
inst_2 : DecidableLT ι
s : Finset ι
h : ∀ (a : ι × ι), a ∈ {i ∈ s.offDiag | i.1 < i.2} ↔ a ∈ {i ∈ s.offDiag | i.1 ≤ i.2}
⊢ {i ∈ s.offDiag | i.1 < i.2} = {i ∈ s.offDiag | i.1 ≤ i.2}

Tactic:
ext
-- Module: Mathlib.Data.Finset.Prod
Goal:
ι : Type u_4
inst : PartialOrder ι
inst_1 : DecidableLE ι
inst_2 : DecidableLT ι
s : Finset ι
a : ι × ι
⊢ a ∈ {i ∈ s.offDiag | i.1 < i.2} ↔ a ∈ {i ∈ s.offDiag | i.1 ≤ i.2}

Tactic:
simpa using fun _ _ a ↦ (Ne.le_iff_lt a).symm

Premises used: Ne.le_iff_lt, Iff.symm
-- Module: Mathlib.Data.Finset.Range
Goal:
n : ℕ
⊢ (range n).val = Multiset.range n

Tactic:
rfl

Premises used: Multiset.ofList, Multiset.range, rfl
-- Module: Mathlib.Data.Finset.Range
Goal:
n : ℕ
⊢ (Multiset.range n).toFinset = range n

Tactic:
Finset.val_injective (Finset.range n).nodup.dedup

Premises used: Finset.nodup, Finset.val_injective, Finset.range, Multiset.Nodup.dedup
-- Module: Mathlib.Data.Finset.Range
Goal:
n m : ℕ
⊢ m ∈ range n ↔ m < n

Tactic:
Multiset.mem_range

Premises used: Set.Mem, setOf, Multiset.mem_range, Multiset.Mem
-- Module: Mathlib.Data.Finset.Range
Goal:
n : ℕ
⊢ (↑(range n) : Set ℕ) = Set.Iio n

Tactic:
Set.ext fun _ => mem_range

Premises used: Set.ext, Finset.mem_range
-- Module: Mathlib.Data.Finset.Range
Goal:
⊢ range 0 = ∅

Tactic:
rfl

Premises used: Multiset.zero, Finset.empty, List.range, Finset.range, Multiset.ofList, Multiset.range, rfl, List.range.loop
-- Module: Mathlib.Data.Finset.Range
Goal:
⊢ range 1 = {0}

Tactic:
rfl

Premises used: Multiset.cons, List.range, Finset.range, Multiset.ofList, Multiset.range, rfl, List.range.loop
-- Module: Mathlib.Data.Finset.Range
Goal:
n : ℕ
⊢ range (n + 1) = insert n (range n)

Tactic:
grind
-- Module: Mathlib.Data.Finset.Range
Goal:
n : ℕ
⊢ n ∉ range n

Tactic:
grind
-- Module: Mathlib.Data.Finset.Range
Goal:
n : ℕ
⊢ n ∈ range (n + 1)

Tactic:
grind
-- Module: Mathlib.Data.Finset.Range
Goal:
n : ℕ
s : Finset ℕ
⊢ range n ⊆ s ↔ ∀ x < n, x ∈ s

Tactic:
grind
-- Module: Mathlib.Data.Finset.Range
Goal:
s : Finset ℕ
n : ℕ
⊢ s ⊆ range n ↔ ∀ x ∈ s, x < n

Tactic:
grind
-- Module: Mathlib.Data.Finset.Range
Goal:
n m : ℕ
⊢ range n ⊆ range m ↔ n ≤ m

Tactic:
grind
-- Module: Mathlib.Data.Finset.Range
Goal:
⊢ Monotone range

Tactic:
fun _ _ => range_subset_range.2

Premises used: Iff.mpr, Monotone, Finset.range_subset_range
-- Module: Mathlib.Data.Finset.Range
Goal:
x : ℕ
⊢ range x < range (x + 1)

Tactic:
simp [ssubset_def]

Premises used: Finset.ssubset_def
-- Module: Mathlib.Data.Finset.Range
Goal:
a b : ℕ
⊢ a ∈ range b.succ ↔ a ≤ b

Tactic:
grind
-- Module: Mathlib.Data.Finset.Range
Goal:
n x : ℕ
hx : x ∈ range n
⊢ x ≤ n

Tactic:
grind
-- Module: Mathlib.Data.Finset.Range
Goal:
n x : ℕ
hx : x ∈ range n
⊢ n - x ≠ 0

Tactic:
grind
-- Module: Mathlib.Data.Finset.Range
Goal:
n : ℕ
h : (range n).Nonempty
k : ℕ
hk : k ∈ range n
⊢ n ≠ 0

Tactic:
grind
-- Module: Mathlib.Data.Finset.Range
Goal:
n : ℕ
h : n ≠ 0
⊢ 0 ∈ range n

Tactic:
grind
-- Module: Mathlib.Data.Finset.Range
Goal:
n : ℕ
⊢ range n = ∅ ↔ n = 0

Tactic:
grind [nonempty_range_iff]

Premises used: Finset.nonempty_range_iff
-- Module: Mathlib.Data.Finset.Range
Goal:
n : ℕ
⊢ (range (n + 1)).Nonempty

Tactic:
nonempty_range_iff.2 n.succ_ne_zero

Premises used: Iff.mpr, Finset.nonempty_range_iff, Nat.succ_ne_zero
-- Module: Mathlib.Data.Finset.Range
Goal:
n : ℕ
hn : 1 < n
rw : (Set.Iio n).Nontrivial
⊢ (range n).Nontrivial

Tactic:
rw [Finset.Nontrivial, Finset.coe_range]

Premises used: Finset.coe_range, Finset.Nontrivial
-- Module: Mathlib.Data.Finset.Range
Goal:
n : ℕ
hn : 1 < n
⊢ 0 ∈ Set.Iio n

Tactic:
grind
-- Module: Mathlib.Data.Finset.Range
Goal:
n : ℕ
hn : 1 < n
⊢ (Set.Iio n).Nontrivial

Tactic:
exact ⟨0, by grind, 1, hn, Nat.zero_ne_one⟩
-- Module: Mathlib.Data.Finset.Range
Goal:
s : Finset ℕ
⊢ ∃ (n : ℕ), ∅ ⊆ range n

Tactic:
simp
-- Module: Mathlib.Data.Finset.Range
Goal:
s : Finset ℕ
a : ℕ
x : Finset ℕ
h : a ∉ x
h_1 : ∃ (n : ℕ), x ⊆ range n
n : ℕ
hn : x ⊆ range n
⊢ insert a x ⊆ range (max (a + 1) n)

Tactic:
grind
-- Module: Mathlib.Data.Finset.Range
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
k j : ℕ
⊢ j + k ∉ range k

Tactic:
simp
-- Module: Mathlib.Data.Finset.Range
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
k : ℕ
⊢ Function.LeftInverse (fun (j : ℕ) ↦ Subtype.mk (p := fun (n : ℕ) ↦ n ∉ range k) (j + k) ⋯)
    fun (i : { n : ℕ // n ∉ range k }) ↦ (↑i : ℕ) - k

Tactic:
grind
-- Module: Mathlib.Data.Finset.Range
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
k : ℕ
⊢ Function.RightInverse (fun (j : ℕ) ↦ Subtype.mk (p := fun (n : ℕ) ↦ n ∉ range k) (j + k) ⋯)
    fun (i : { n : ℕ // n ∉ range k }) ↦ (↑i : ℕ) - k

Tactic:
grind
-- Module: Mathlib.Data.Finset.Range
Goal:
k : ℕ
⊢ Eq (α := (a : { n : ℕ // n ∉ range k }) → ℕ) (⇑(notMemRangeEquiv k) : (a : { n : ℕ // n ∉ range k }) → ℕ)
    fun (i : { n : ℕ // n ∉ range k }) ↦ (↑i : ℕ) - k

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finset.Range
Goal:
k : ℕ
⊢ Eq (α := (a : ℕ) → { n : ℕ // n ∉ range k }) (⇑(notMemRangeEquiv k).symm : (a : ℕ) → { n : ℕ // n ∉ range k })
    fun (j : ℕ) ↦ Subtype.mk (p := fun (n : ℕ) ↦ n ∉ range k) (j + k) ⋯

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finset.SDiff
Goal:
α : Type u_1
inst : DecidableEq α
s₁ s₂ : Finset α
⊢ (s₁ \ s₂).val = s₁.val - s₂.val

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finset.SDiff
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
a : α
⊢ a ∈ s \ t ↔ a ∈ s ∧ a ∉ t

Tactic:
mem_sub_of_nodup s.2

Premises used: Multiset.mem_sub_of_nodup, Set.Mem, setOf, Finset.nodup, Multiset.Mem
-- Module: Mathlib.Data.Finset.SDiff
Goal:
α : Type u_1
inst : DecidableEq α
s₁ s₂ : Finset α
⊢ s₁ ∩ (s₂ \ s₁) = ∅

Tactic:
grind
-- Module: Mathlib.Data.Finset.SDiff
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : DecidableEq α
s t u v : Finset α
a b : α
⊢ ∀ (a b : Finset α), a ⊓ b ⊔ a \ b = a

Tactic:
grind
-- Module: Mathlib.Data.Finset.SDiff
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : DecidableEq α
s t u v : Finset α
a b : α
⊢ ∀ (a b : Finset α), a ⊓ b ⊓ a \ b = ⊥

Tactic:
grind
-- Module: Mathlib.Data.Finset.SDiff
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
a : α
h : a ∈ t
⊢ a ∉ s \ t

Tactic:
grind
-- Module: Mathlib.Data.Finset.SDiff
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
a : α
h : a ∉ s
⊢ a ∉ s \ t

Tactic:
simp [h]
-- Module: Mathlib.Data.Finset.SDiff
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
h : s ⊆ t
⊢ s ∪ t \ s = t

Tactic:
grind
-- Module: Mathlib.Data.Finset.SDiff
Goal:
α : Type u_1
inst : DecidableEq α
s₁ s₂ : Finset α
h : s₁ ⊆ s₂
⊢ s₂ \ s₁ ∪ s₁ = s₂

Tactic:
grind
-- Module: Mathlib.Data.Finset.SDiff
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Finset α
⊢ (s ∩ t) \ u = s ∩ (t \ u)

Tactic:
inf_sdiff_assoc ..

Premises used: inf_sdiff_assoc
-- Module: Mathlib.Data.Finset.SDiff
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Finset α
⊢ s \ t ∩ u = (s ∩ u) \ t

Tactic:
sdiff_inf_right_comm ..

Premises used: sdiff_inf_right_comm
-- Module: Mathlib.Data.Finset.SDiff
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Finset α
⊢ s ∩ (t \ u) = t ∩ (s \ u)

Tactic:
inf_sdiff_left_comm ..

Premises used: inf_sdiff_left_comm
-- Module: Mathlib.Data.Finset.SDiff
Goal:
α : Type u_1
inst : DecidableEq α
s₁ s₂ : Finset α
⊢ s₂ \ s₁ ∩ s₁ = ∅

Tactic:
inf_sdiff_self_left

Premises used: inf_sdiff_self_left
-- Module: Mathlib.Data.Finset.SDiff
Goal:
α : Type u_1
inst : DecidableEq α
s₁ : Finset α
⊢ s₁ \ s₁ = ∅

Tactic:
_root_.sdiff_self

Premises used: sdiff_self
-- Module: Mathlib.Data.Finset.SDiff
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Finset α
⊢ s \ (t ∩ u) = s \ t ∪ s \ u

Tactic:
sdiff_inf

Premises used: sdiff_inf
-- Module: Mathlib.Data.Finset.SDiff
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ s \ (s ∩ t) = s \ t

Tactic:
sdiff_inf_self_left _ _

Premises used: sdiff_inf_self_left
-- Module: Mathlib.Data.Finset.SDiff
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ s \ (t ∩ s) = s \ t

Tactic:
sdiff_inf_self_right _ _

Premises used: sdiff_inf_self_right
-- Module: Mathlib.Data.Finset.SDiff
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
⊢ s \ ∅ = s

Tactic:
sdiff_bot

Premises used: sdiff_bot
-- Module: Mathlib.Data.Finset.SDiff
Goal:
α : Type u_1
inst : DecidableEq α
s t u v : Finset α
hst : s ⊆ t
hvu : v ⊆ u
⊢ s \ u ⊆ t \ v

Tactic:
grind
-- Module: Mathlib.Data.Finset.SDiff
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Finset α
h : s ⊆ t
⊢ s \ u ⊆ t \ u

Tactic:
gcongr
-- Module: Mathlib.Data.Finset.SDiff
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Finset α
h : s ⊆ t
⊢ u \ t ⊆ u \ s

Tactic:
gcongr
-- Module: Mathlib.Data.Finset.SDiff
Goal:
α : Type u_1
inst : DecidableEq α
s t r : Finset α
hs : s ⊆ r
ht : t ⊆ r
⊢ r \ s ⊆ r \ t ↔ t ⊆ s

Tactic:
simpa only [← le_eq_subset] using sdiff_le_sdiff_iff_le hs ht

Premises used: sdiff_le_sdiff_iff_le, Finset.le_eq_subset
-- Module: Mathlib.Data.Finset.SDiff
Goal:
α : Type u_1
inst : DecidableEq α
s₁ s₂ : Finset α
⊢ (↑(s₁ \ s₂) : Set α) = (↑s₁ : Set α) \ (↑s₂ : Set α)

Tactic:
Set.ext fun _ => mem_sdiff

Premises used: Set.ext, Finset.mem_sdiff
-- Module: Mathlib.Data.Finset.SDiff
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ s ∪ t \ s = s ∪ t

Tactic:
sup_sdiff_self_right _ _

Premises used: sup_sdiff_self_right
-- Module: Mathlib.Data.Finset.SDiff
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ s \ t ∪ t = s ∪ t

Tactic:
sup_sdiff_self_left _ _

Premises used: sup_sdiff_self_left
-- Module: Mathlib.Data.Finset.SDiff
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ (s ∪ t) \ s = t \ s

Tactic:
sup_sdiff_left_self

Premises used: sup_sdiff_left_self
-- Module: Mathlib.Data.Finset.SDiff
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ (s ∪ t) \ t = s \ t

Tactic:
sup_sdiff_right_self

Premises used: sup_sdiff_right_self