mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Prod.Lex

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMaxOrder β
⊢ ∀ (a : Lex (α × β)), ∃ b, a < b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
ha : IsIdempotentElem a
⊢ ∀ {a_1 b : M}, a_1 ∈ {1, a} → b ∈ {1, a} → a_1 * b ∈ {1, a}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
ha : IsIdempotentElem a
S : Submonoid M := { carrier := {1, a}, mul_mem' := ⋯, one_mem' := ⋯ }
⊢ S ≤ powers a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
a x : M
n : ℕ
hpos : 0 < n
hx : x ^ n = 1
z : ↥(powers x)
⊢ z ^ 0 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
a x✝ : M
n : ℕ
hpos : 0 < n
hx : x✝ ^ n = 1
m : ℕ
x : ↥(powers x✝)
⊢ ↑(x ^ ↑m.succ) = ↑(x ^ ↑m * x)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
a x✝ : M
n : ℕ
hpos : 0 < n
hx : x✝ ^ n = 1
m : ℕ
x : ↥(powers x✝)
⊢ x ^ Int.negSucc m = (x ^ ↑m.succ) ^ (n - 1)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
a x : M
n : ℕ
hpos : 0 < n
hx : x ^ n = 1
y : ↥(powers x)
⊢ ↑(y ^ (n - 1) * y) = ↑1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
A : Type u_2
B : Type u_3
inst✝¹ : Monoid M
a : M
inst✝ : DecidableEq M
n : M
h : Function.Injective fun m ↦ n ^ m
x✝¹ x✝ : Multiplicative ℕ
⊢ pow n (Multiplicative.toAdd (x✝¹ * x✝)) = pow n (Multiplicative.toAdd x✝¹) * pow n (Multiplicative.toAdd x✝)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
inst✝³ : Monoid M
N : Type u_4
F : Type u_5
inst✝² : Monoid N
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
f : F
m : M
⊢ map f (powers m) = powers (f m)

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o : Option α
⊢ foldl (argAux r) o [] = none ↔ [] = [] ∧ o = none

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
N : Type u_4
α : Type u_5
inst✝³ : Monoid M
inst✝² : MulAction M N
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ x ∈ s, ∀ (y : N) (z : α), (x • y) • z = x • y • z
⊢ IsScalarTower M N α

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case some
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o : Option α
tl : List α
hd val✝ : α
⊢ (some val✝ = none ↔ tl = [] ∧ o = none) →
    (Option.rec (some hd) (fun val ↦ if r hd val then some hd else some val) (some val✝) = none ↔
      (tl = [] ∧ [hd] = []) ∧ o = none)

Tactic:
simp only

Goal state after:
case some
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o : Option α
tl : List α
hd val✝ : α
⊢ (some val✝ = none ↔ tl = [] ∧ o = none) →
    ((if r hd val✝ then some hd else some val✝) = none ↔ (tl = [] ∧ [hd] = []) ∧ o = none)
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o : Option α
tl : List α
hd : α
⊢ (foldl (argAux r) o tl = none ↔ tl = [] ∧ o = none) →
    (foldl (argAux r) o (tl ++ [hd]) = none ↔ tl ++ [hd] = [] ∧ o = none)

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
⊢ ∀ (a m : α), m ∈ foldl (argAux r) (some a) [] → m ∈ [a]

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Order.Lemmas

Goal state before:
pp: S : Set ℕ
⊢ S = Set.univ → 0 ∈ S ∧ ∀ (k : ℕ), k ∈ S → k + 1 ∈ S

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
⊢ ∀ (l : List α) (a : α),
    (∀ (a m : α), m ∈ foldl (argAux r) (some a) l → m ∈ a :: l) →
      ∀ (a_2 m : α), m ∈ foldl (argAux r) (some a_2) (l ++ [a]) → m ∈ a_2 :: (l ++ [a])

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Order.Lemmas

Goal state before:
pp: p : ℕ → Prop
H' : ¬p 0
H : ∃ n, p n
k : ℕ := Nat.find H
hk : p k
this : 0 < k
⊢ p (k - 1 + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
N : Type u_4
α : Type u_5
inst✝² : Monoid M
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ x ∈ s, ∀ (y : N) (z : α), x • y • z = y • x • z
⊢ SMulCommClass M N α

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Order.Lemmas

Goal state before:
pp: p : ℕ → Prop
H' : ¬p 0
H : ∃ n, p n
⊢ ∃ n, ¬p n ∧ p (n + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: N : Type u_4
inst✝ : CommMonoid N
s t : Submonoid N
⊢ s ⊔ t = mrange (s.subtype.coprod t.subtype)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: N : Type u_4
inst✝ : CommMonoid N
s t : Submonoid N
⊢ s ⊔ t = mrange (s.subtype.coprod t.subtype)

Tactic:
by
  rw [mrange_eq_map, ← mrange_inl_sup_mrange_inr, map_sup, map_mrange, coprod_comp_inl, map_mrange,
    coprod_comp_inr, mrange_subtype, mrange_subtype]

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: N : Type u_4
inst✝ : CommMonoid N
s t : Submonoid N
x : N
⊢ x ∈ s ⊔ t ↔ ∃ y ∈ s, ∃ z ∈ t, y * z = x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: N : Type u_4
inst✝ : CommMonoid N
P : N → Prop
s t : Submonoid N
⊢ (∀ x ∈ s ⊔ t, P x) ↔ ∀ x₁ ∈ s, ∀ x₂ ∈ t, P (x₁ * x₂)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: N : Type u_4
inst✝ : CommMonoid N
P : N → Prop
s t : Submonoid N
⊢ (∃ x ∈ s ⊔ t, P x) ↔ ∃ x₁ ∈ s, ∃ x₂ ∈ t, P (x₁ * x₂)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: A : Type u_2
inst✝ : AddMonoid A
x y : A
⊢ y ∈ closure {x} ↔ ∃ n, n • x = y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: A : Type u_2
inst✝ : AddMonoid A
⊢ closure {0} = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : AddMonoid A
x n : A
i : ℕ
⊢ (fun i ↦ i • x) i = n ↔ ((multiplesHom A) x) i = n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: A : Type u_4
inst✝ : CommMonoid A
a b c : A
⊢ c ∈ closure {a, b} ↔ ∃ m n, a ^ m * b ^ n = c

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
x : M
⊢ ⇑Additive.ofMul '' ↑(Submonoid.powers x) = ↑(AddSubmonoid.multiples (Additive.ofMul x))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: A : Type u_2
inst✝ : AddMonoid A
x : A
⊢ ⇑Multiplicative.ofAdd '' ↑(AddSubmonoid.multiples x) = ↑(Submonoid.powers (Multiplicative.ofAdd x))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: ⊢ AddSubmonoid.closure {1} = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
hr₀ : Std.Irrefl r
hr₁ : IsTrans α r
⊢ ∀ {a m : α} {o : Option α}, a ∈ l → m ∈ foldl (argAux r) o l → ¬r a m

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder β
inst✝ : DecidableLT β
f : α → β
a : α
l : List α
⊢ argmax f (l ++ [a]) = Option.casesOn (argmax f l) (some a) fun c ↦ if f c < f a then some a else some c

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder β
inst✝ : DecidableLT β
f : α → β
m : α
⊢ m ∈ argmax f [] → m ∈ []

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder β
inst✝ : DecidableLT β
f : α → β
hd : α
tl : List α
m : α
⊢ m ∈ argmax f (hd :: tl) → m ∈ hd :: tl

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder β
inst✝ : DecidableLT β
f : α → β
l : List α
⊢ argmax f l = none ↔ l = []

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : α → β
a : α
l hd : List α
tl : α
ih : argmax f (a :: hd) = Option.casesOn (argmax f hd) (some a) fun c ↦ if f a < f c then some c else some a
⊢ argmax f (a :: (hd ++ [tl])) =
    Option.casesOn (argmax f (hd ++ [tl])) (some a) fun c ↦ if f a < f c then some c else some a

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
m : α
x✝³ : m ∈ argmax f []
x✝² : α
x✝¹ : x✝² ∈ []
x✝ : f m ≤ f x✝²
⊢ idxOf m [] ≤ idxOf x✝² []

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
⊢ (s.disjSum t).card = s.card + t.card

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
x : α ⊕ β
⊢ x ∈ s.disjSum t ↔ (∃ a, a ∈ s ∧ inl a = x) ∨ ∃ b, b ∈ t ∧ inr b = x

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: α : Type u_1
inst✝ : Denumerable α
n : ℕ
b : α
h : decode n = some b
⊢ ofNat α n = b

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: α : Type u_1
inst✝ : Denumerable α
n : ℕ
⊢ encode (ofNat α n) = n

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
inst✝² : Denumerable α✝
inst✝¹ : Denumerable β✝
α : Type ?u.10
β : Type ?u.15
inst✝ : Denumerable α
e : β ≃ α
n : ℕ
⊢ ∃ a ∈ decode n, encode a = n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
a : α
⊢ inl a ∈ s.disjSum t ↔ a ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
b : β
⊢ inr b ∈ s.disjSum t ↔ b ∈ t

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Denumerable α
e : β ≃ α
n : ℕ
⊢ ofNat β n = e.symm (ofNat α n)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
hs : s.Nodup
ht : t.Nodup
⊢ (s.disjSum t).Nodup

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Multiset α
t : Multiset β
f : α ⊕ β → γ
⊢ map f (s.disjSum t) = map (fun x ↦ f (inl x)) s + map (fun x ↦ f (inr x)) t

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
⊢ ∃ a ∈ decode n, encode a = n

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
this : ∃ a ∈ decodeSum n, encodeSum a = bit n.bodd n.div2
⊢ ∃ a ∈ decode n, encode a = n

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
a val✝ : α
h : argmax f tl = some val✝
a✝ : Mem a tl
h✝ : f hd < f val✝
ham : f val✝ ≤ f a
⊢ a ∈ tl

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Lattice

Goal state before:
pp: α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s₁ s₂ : Multiset α
⊢ (s₁ + s₂).sup = fold (fun x1 x2 ↦ x1 ⊔ x2) (⊥ ⊔ ⊥) (s₁ + s₂)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Lattice

Goal state before:
pp: α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Multiset α
a : α
⊢ sup 0 ≤ a ↔ ∀ (b : α), b ∈ 0 → b ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Lattice

Goal state before:
pp: α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Multiset α
a : α
⊢ ∀ (a_1 : α) (s : Multiset α),
    (s.sup ≤ a ↔ ∀ (b : α), b ∈ s → b ≤ a) → ((a_1 ::ₘ s).sup ≤ a ↔ ∀ (b : α), b ∈ a_1 ::ₘ s → b ≤ a)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Lattice

Goal state before:
pp: α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ (s₁.ndunion s₂).sup = s₁.sup ⊔ s₂.sup

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Lattice

Goal state before:
pp: α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ (s₁ ∪ s₂).sup = s₁.sup ⊔ s₂.sup

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Lattice

Goal state before:
pp: α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ (ndinsert a s).sup = a ⊔ s.sup

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Denumerable α
inst✝¹ : Denumerable β
γ : α → Type u_3
inst✝ : (a : α) → Denumerable (γ a)
n : ℕ
⊢ ∃ a ∈ decode n, encode a = n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Lattice

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
m : Multiset (Multiset α)
⊢ m.sup.Nodup ↔ ∀ (a : Multiset α), a ∈ m → a.Nodup

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
m : α
hm : m ∈ argmax f (hd :: tl)
a : α
ha : a ∈ hd :: tl
ham : f m ≤ f a
⊢ idxOf m (hd :: tl) ≤ idxOf a (hd :: tl)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: α : Type u_1
inst✝¹ : Denumerable α
γ : α → Type u_3
inst✝ : (a : α) → Denumerable (γ a)
n : ℕ
⊢ some (ofNat (Sigma γ) n) = some ⟨ofNat α (unpair n).1, ofNat (γ (ofNat α (unpair n).1)) (unpair n).2⟩

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
⊢ ofNat (α × β) n = (ofNat α (unpair n).1, ofNat β (unpair n).2)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: ⊢ ofNat (ℕ × ℕ) = unpair

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝ : Infinite ↑s
x : ↑s
h : ¬∃ n, ↑x + n + 1 ∈ s
a : ℕ
ha : a ∈ s
hax : ↑x + 1 ≤ a
⊢ ↑x + (a - (↑x + 1)) + 1 ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
m : α
inst✝ : DecidableEq α
⊢ (m ∈ l ∧ (∀ (a : α), a ∈ l → f a ≤ f m) ∧ ∀ (a : α), a ∈ l → f m ≤ f a → idxOf m l ≤ idxOf a l) → m ∈ argmax f l

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝ : Infinite ↑s
x : ↑s
h : ¬∃ n, ↑x + n + 1 ∈ s
this : ∀ a ∈ s, a < ↑x + 1
⊢ ∀ a ∈ Multiset.filter (fun x ↦ x ∈ s) (Multiset.range (↑x).succ), a ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLT α
l : List α
a : α
ha : a ∈ l
⊢ ¬l.maximum < ↑a

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝ : Infinite ↑s
x : ↑s
h : ¬∃ n, ↑x + n + 1 ∈ s
this : ∀ a ∈ s, a < ↑x + 1
⊢ ∀ (x_1 : Subtype (Membership.mem s)),
    x_1 ∈ (Multiset.pmap (fun y hy ↦ ⟨y, hy⟩) (Multiset.filter (fun x ↦ x ∈ s) (Multiset.range (↑x).succ)) ⋯).toFinset

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝ : Infinite ↑s
x : ↑s
⊢ ∃ n, ↑x + n + 1 ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ Disjoint (map Embedding.inl s) (map Embedding.inr t)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ s.disjSum t = ∅ ↔ s = ∅ ∧ t = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_4
β : Type u_5
s₁ s₂ : Finset α
t₁ t₂ : Finset β
⊢ s₁.disjSum t₁ = s₂.disjSum t₂ ↔ s₁ = s₂ ∧ t₁ = t₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_4
β : Type u_5
x✝³ x✝² : Finset α
x✝¹ x✝ : Finset β
⊢ x✝³.disjSum x✝¹ = x✝².disjSum x✝ → x✝³ = x✝² ∧ x✝¹ = x✝

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
x y : ↑s
h : ∀ z < x, z ≤ y
hx : ∃ m, ↑y + m + 1 ∈ s
hxy : ↑y + Nat.find hx + 1 < ↑x
⊢ ↑y < ↑y + Nat.find hx + 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
t : Finset β
s₁ s₂ : Finset α
t₁ t₂ : Finset β
a : α
b : β
x : α ⊕ β
u : Finset (α ⊕ β)
⊢ ∀ (a a' : α ⊕ β), ∀ b ∈ Sum.elim some (fun x ↦ none) a, b ∈ Sum.elim some (fun x ↦ none) a' → a = a'

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
t : Finset β
s₁ s₂ : Finset α
t₁ t₂ : Finset β
a : α
b : β
x : α ⊕ β
u : Finset (α ⊕ β)
⊢ ∀ (a a' : α ⊕ β), ∀ b ∈ Sum.elim (fun x ↦ none) some a, b ∈ Sum.elim (fun x ↦ none) some a' → a = a'

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
a : α
⊢ a ∈ u.toLeft ↔ inl a ∈ u

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
b : β
⊢ b ∈ u.toRight ↔ inr b ∈ u

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
h : u ⊆ v
x✝ : α
⊢ x✝ ∈ u.toLeft → x✝ ∈ v.toLeft

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
h : u ⊆ v
x✝ : β
⊢ x✝ ∈ u.toRight → x✝ ∈ v.toRight

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a : α
l : List α
⊢ (l ++ [a]).maximum = max l.maximum ↑a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
⊢ u.toLeft.disjSum u.toRight = u

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
⊢ #u.toLeft + #u.toRight = #u

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ (s.disjSum t).toLeft = s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ (s.disjSum t).toRight = t

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a : α
l : List α
⊢ [a].maximum = max ↑a [].maximum

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
u : Finset (α ⊕ β)
h : s.disjSum t = u
⊢ s = u.toLeft ∧ t = u.toRight

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
u : Finset (α ⊕ β)
h : s = u.toLeft ∧ t = u.toRight
⊢ s.disjSum t = u

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
u : Finset (α ⊕ β)
h : u = s.disjSum t
⊢ u.toLeft = s ∧ u.toRight = t

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
x : ℕ
hx : x ∈ s
⊢ ∀ a ∈ List.filter (fun y ↦ decide (y ∈ s)) (List.range x), a ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
u : Finset (α ⊕ β)
h : u.toLeft = s ∧ u.toRight = t
⊢ u = s.disjSum t

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
u : Finset (α ⊕ β)
⊢ s.disjSum t ⊆ u ↔ s ⊆ u.toLeft ∧ t ⊆ u.toRight

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
u : Finset (α ⊕ β)
⊢ u ⊆ s.disjSum t ↔ u.toLeft ⊆ s ∧ u.toRight ⊆ t

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
u : Finset (α ⊕ β)
⊢ u ⊆ map Embedding.inl s ↔ u.toLeft ⊆ s ∧ u.toRight = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
t : Finset β
u : Finset (α ⊕ β)
⊢ u ⊆ map Embedding.inr t ↔ u.toLeft = ∅ ∧ u.toRight ⊆ t

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
u : Finset (α ⊕ β)
⊢ map Embedding.inl s ⊆ u ↔ s ⊆ u.toLeft

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
t : Finset β
u : Finset (α ⊕ β)
⊢ map Embedding.inr t ⊆ u ↔ t ⊆ u.toRight

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
x : ℕ
hx : x ∈ s
t : List ↑s := List.pmap (fun y hy ↦ ⟨y, hy⟩) (List.filter (fun y ↦ decide (y ∈ s)) (List.range x)) ⋯
ht : t = List.pmap (fun y hy ↦ ⟨y, hy⟩) (List.filter (fun y ↦ decide (y ∈ s)) (List.range x)) ⋯
⊢ ∀ {y : ↑s}, y ∈ t ↔ y < ⟨x, hx⟩

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
⊢ (map (Equiv.sumComm α β).toEmbedding u).toLeft = u.toRight

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
⊢ (map (Equiv.sumComm α β).toEmbedding u).toRight = u.toLeft

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
t : Finset β
s₁ s₂ : Finset α
t₁ t₂ : Finset β
a✝ : α
b✝ : β
x : α ⊕ β
u v : Finset (α ⊕ β)
a : α
b : β
ha : inl a ∉ u
⊢ a ∉ u.toLeft

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
a : α
ha : inl a ∉ u
⊢ (cons (inl a) u ha).toLeft = cons a u.toLeft ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
b : β
hb : inr b ∉ u
⊢ (cons (inr b) u hb).toLeft = u.toLeft

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
a : α
ha : inl a ∉ u
⊢ (cons (inl a) u ha).toRight = u.toRight

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
t : Finset β
s₁ s₂ : Finset α
t₁ t₂ : Finset β
a✝ : α
b✝ : β
x : α ⊕ β
u v : Finset (α ⊕ β)
a : α
b : β
hb : inr b ∉ u
⊢ b ∉ u.toRight

Tactic:
by

Goal state after: