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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a b : (i : ι) × α i
inst✝¹ : Std.Trichotomous r
inst✝ : ∀ (i : ι), Std.Total (s i)
⊢ ∀ (a b : (i : ι) × α i), Lex r s a b ∨ Lex r s b a

Tactic:
by
    rintro ⟨i, a⟩ ⟨j, b⟩
    obtain hij | rfl | hji := trichotomous_of r i j
    · exact Or.inl (Lex.left _ _ hij)
    · obtain hab | hba := total_of (s i) a b
      · exact Or.inl (Lex.right _ _ hab)
      · exact Or.inr (Lex.right _ _ hba)
    · exact Or.inr (Lex.left _ _ hji)

Goal state after:
Module: Mathlib.Logic.Embedding.Set

Goal state before:
pp: α : Sort u_1
β : Type u_2
p : β → Prop
e : α ≃ Subtype p
x : β
hs : x ∈ ofPred p
⊢ e.asEmbedding (e.symm ⟨x, hs⟩) = x

Tactic:
by simp

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

Goal state before:
pp: case refine_3
M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
motive : (x : M) → x ∈ ⨆ i, S i → Prop
mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), motive x ⋯
one : motive 1 ⋯
mul : ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), motive x hx → motive y hy → motive (x * y) ⋯
x✝ : M
hx : x✝ ∈ ⨆ i, S i
x y : M
⊢ (∃ (hm : x ∈ ⨆ i, S i), motive x hm) →
    (∃ (hm : y ∈ ⨆ i, S i), motive y hm) → ∃ (hm : x * y ∈ ⨆ i, S i), motive (x * y) hm

Tactic:
rintro ⟨_, Cx⟩ ⟨_, Cy⟩
    exact ⟨_, mul _ _ _ _ Cx Cy⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
⊢ Set.range ⇑e = Set.univ

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
p : α → Prop
h : ∀ (x : α), p x
⊢ ∀ {a b : Subtype p}, r ((Equiv.subtypeUnivEquiv h) a) ((Equiv.subtypeUnivEquiv h) b) ↔ Subrel r p a b

Tactic:
by simp

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

Goal state before:
pp: case inl.inl
M : Type u_1
inst✝ : Monoid M
a : M
ha : IsIdempotentElem a
⊢ 1 * 1 ∈ {1, a}

Tactic:
rw [one_mul]

Goal state after:
case inl.inl
M : Type u_1
inst✝ : Monoid M
a : M
ha : IsIdempotentElem a
⊢ 1 ∈ {1, a}
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: case inl.inr
M : Type u_1
inst✝ : Monoid M
b✝ : M
ha : IsIdempotentElem b✝
⊢ 1 * b✝ ∈ {1, b✝}

Tactic:
rw [one_mul]

Goal state after:
case inl.inr
M : Type u_1
inst✝ : Monoid M
b✝ : M
ha : IsIdempotentElem b✝
⊢ b✝ ∈ {1, b✝}
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 simp

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 simp

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 simp

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 simp

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 simp

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 simp

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 simp

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 simp

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 : β✝
α : Type u_4
β : Type u_5
s : Finset α × Finset β
⊢ (fun s ↦ (s.toLeft, s.toRight)) ((fun s ↦ s.1.disjSum s.2) s) = s

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
l₁ l₂ : List α
⊢ (l₁ ++ l₂).maximum = max l₁.maximum l₂.maximum

Tactic:
induction l₁ with

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
l✝ : List α
b : WithBot α
a : α
l : List α
ih : (∀ (a : α), a ∈ l → ↑a ≤ b) → l.maximum ≤ b
h : ∀ (a_1 : α), a_1 ∈ a :: l → ↑a_1 ≤ b
⊢ a ∈ a :: l

Tactic:
by simp

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : SemilatticeInf α
inst✝¹ : SemilatticeInf β
f : F
inst✝ : InfHomClass F α β
hf : Injective ⇑f
x y : α
⊢ f x ≤ f y ↔ x ≤ y

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ OrderHomClass.mono f h⟩

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : SemilatticeInf α
inst✝¹ : SemilatticeInf β
f : F
inst✝ : InfHomClass F α β
hf : Injective ⇑f
x y : α
h : f x ≤ f y
⊢ x ≤ y
Module: Mathlib.Order.Hom.Lattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : FunLike F α β
inst✝¹ : Max α
inst✝ : SemilatticeSup β
P : β → Prop
Psup : ∀ ⦃x y : β⦄, P x → P y → P (x ⊔ y)
this : SemilatticeSup { x // P x } := Subtype.semilatticeSup Psup
⊢ ∀ (a b : { x // P x }), ↑(a ⊔ b) = ↑a ⊔ ↑b

Tactic:
by simp

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

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : OrderTop α
s : Finset α
⊢ (∃ b ∈ s, ↑b = ⊤) ↔ ⊤ ∈ s

Tactic:
by simp

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

Goal state before:
pp: α : Type u
β : Type u_1
γ : Type u_2
f : α → β → γ
p : γ → Prop
x✝ : [].length = [].length
⊢ Forall p (zipWith f [] []) ↔ Forall₂ (fun x y ↦ p (f x y)) [] []

Tactic:
by simp

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

Goal state before:
pp: α : Type u
l : List α
⊢ map Prod.fst l.revzip = l

Tactic:
rw [← unzip_fst, unzip_revzip]

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

Goal state before:
pp: α : Type u
l : List α
⊢ map Prod.fst l.revzip = l

Tactic:
by
  rw [← unzip_fst, unzip_revzip]

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

Goal state before:
pp: α : Type u
a : α
r₁ r₂ : List (List α)
⊢ ∀ (x : Array (List α)) (y : List α), x.toList ++ [a :: y] = (x.push (a :: y)).toList

Tactic:
by simp

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
x : α
s : Finset α
h : ∃ y ∈ s, x < y
Hne : {x_1 ∈ s | x < x_1}.Nonempty
aux : {x_1 ∈ s | x < x_1}.min' Hne ∈ s ∧ x < {x_1 ∈ s | x < x_1}.min' Hne
⊢ x < {x_1 ∈ s | x < x_1}.min' Hne

Tactic:
by simp

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

Goal state before:
pp: case swap
α : Type u_1
l₁ l₂ : List α
a b : α
l✝ : List α
⊢ List.map (cons a) (powersetAux' l✝) ++ List.map (cons b) (powersetAux' l✝) ++
      List.map (cons b ∘ cons a) (powersetAux' l✝) ~
    List.map (cons b) (powersetAux' l✝) ++ List.map (cons a) (powersetAux' l✝) ++
      List.map (cons a ∘ cons b) (powersetAux' l✝)

Tactic:
(by funext s; simp [cons_swap] : cons b ∘ cons a = cons a ∘ cons b)

Goal state after:
case swap
α : Type u_1
l₁ l₂ : List α
a b : α
l✝ : List α
⊢ List.map (cons a) (powersetAux' l✝) ++ List.map (cons b) (powersetAux' l✝) ++
      List.map (cons a ∘ cons b) (powersetAux' l✝) ~
    List.map (cons b) (powersetAux' l✝) ++ List.map (cons a) (powersetAux' l✝) ++
      List.map (cons a ∘ cons b) (powersetAux' l✝)
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
a : α
r : List (List α)
⊢ ∀ (x : Array (List α)) (y : List α), x.toList ++ [y, a :: y] = ((x.push y).push (a :: y)).toList

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
s : Multiset α
⊢ ∀ (a : List α), (powerset ⟦a⟧).card = 2 ^ card ⟦a⟧

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
l : List α
x : Multiset α × Multiset α
h : ∃ a b, (a, b) ∈ l.sublists.revzip ∧ (↑a, ↑b) = x
⊢ x.1 + x.2 = ↑l

Tactic:
rcases h with ⟨l₁, l₂, h, rfl, rfl⟩

Goal state after:
α : Type u_1
l l₁ l₂ : List α
h : (l₁, l₂) ∈ l.sublists.revzip
⊢ (↑l₁, ↑l₂).1 + (↑l₁, ↑l₂).2 = ↑l
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: α : Type u_1
l : List α
x : Multiset α × Multiset α
h : ∃ a b, (a, b) ∈ l.sublists'.revzip ∧ (↑a, ↑b) = x
⊢ x.1 + x.2 = ↑l

Tactic:
rcases h with ⟨l₁, l₂, h, rfl, rfl⟩

Goal state after:
α : Type u_1
l l₁ l₂ : List α
h : (l₁, l₂) ∈ l.sublists'.revzip
⊢ (↑l₁, ↑l₂).1 + (↑l₁, ↑l₂).2 = ↑l
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
l : List α
l' : List (Multiset α)
H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ l'.revzip → x.1 + x.2 = ↑l
⊢ Forall₂ (fun p s ↦ p = (s, ↑l - s)) l'.revzip (List.map Prod.fst l'.revzip)

Tactic:
forall₂_map_right_iff,

Goal state after:
α : Type u_2
inst✝ : DecidableEq α
l : List α
l' : List (Multiset α)
H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ l'.revzip → x.1 + x.2 = ↑l
⊢ Forall₂ (fun a c ↦ a = (c.1, ↑l - c.1)) l'.revzip l'.revzip
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
l₁ l₂ : List α
⊢ foldr (fun a acc ↦ flatMap (fun x ↦ [x, a :: x]) acc) (foldr (fun a acc ↦ flatMap (fun x ↦ [x, a :: x]) acc) [[]] l₂)
      l₁ =
    do
    let x ← foldr (fun a acc ↦ flatMap (fun x ↦ [x, a :: x]) acc) [[]] l₂
    map (fun x_1 ↦ x_1 ++ x) (foldr (fun a acc ↦ flatMap (fun x ↦ [x, a :: x]) acc) [[]] l₁)

Tactic:
induction l₁ with

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

Goal state before:
pp: α : Type u
l : List α
a : α
⊢ (l ++ [a]).sublists = l.sublists ++ map (fun x ↦ x ++ [a]) l.sublists

Tactic:
rw [sublists_append, sublists_singleton, bind_eq_flatMap, flatMap_cons, flatMap_cons, flatMap_nil,
     map_id'' append_nil, append_nil]

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

Goal state before:
pp: α : Type u_1
l : List α
this : DecidableEq α
⊢ List.map (fun x ↦ (x, ↑l - x)) (powersetAux l) ~ List.map (fun x ↦ (x, ↑l - x)) (powersetAux' l)

Tactic:
exact powersetAux_perm_powersetAux'.map _

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

Goal state before:
pp: α : Type u
l : List α
⊢ (sublistsLen 0 l).length = l.length.choose 0

Tactic:
by simp

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

Goal state before:
pp: α : Type u
n✝ : ℕ
⊢ (sublistsLen (n✝ + 1) []).length = [].length.choose (n✝ + 1)

Tactic:
by simp

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

Goal state before:
pp: α : Type u
l : List α
⊢ sublistsLen 0 l <+ l.sublists'

Tactic:
by simp

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

Goal state before:
pp: case succ.swap.succ
α : Type u_1
l₁ l₂ : List α
a b : α
l✝ : List α
n✝ : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → powersetCardAux (n✝ + 1) l₁ ~ powersetCardAux (n✝ + 1) l₂
⊢ List.map (cons a) (powersetCardAux (n✝ + 1) l✝) ++ List.map (cons b) (powersetCardAux (n✝ + 1) l✝) ++
      List.map (cons b ∘ cons a) (powersetCardAux n✝ l✝) ~
    List.map (cons b) (powersetCardAux (n✝ + 1) l✝) ++ List.map (cons a) (powersetCardAux (n✝ + 1) l✝) ++
      List.map (cons a ∘ cons b) (powersetCardAux n✝ l✝)

Tactic:
(by funext s; simp [cons_swap] : cons b ∘ cons a = cons a ∘ cons b)

Goal state after:
case succ.swap.succ
α : Type u_1
l₁ l₂ : List α
a b : α
l✝ : List α
n✝ : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → powersetCardAux (n✝ + 1) l₁ ~ powersetCardAux (n✝ + 1) l₂
⊢ List.map (cons a) (powersetCardAux (n✝ + 1) l✝) ++ List.map (cons b) (powersetCardAux (n✝ + 1) l✝) ++
      List.map (cons a ∘ cons b) (powersetCardAux n✝ l✝) ~
    List.map (cons b) (powersetCardAux (n✝ + 1) l✝) ++ List.map (cons a) (powersetCardAux (n✝ + 1) l✝) ++
      List.map (cons a ∘ cons b) (powersetCardAux n✝ l✝)
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
β : Type v
f : α → β
⊢ (map f []).sublists = map (map f) [].sublists

Tactic:
by simp

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
⊢ (map f []).sublists' = map (map f) [].sublists'

Tactic:
by simp

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

Goal state before:
pp: α : Type u
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l'.sublists.zip l'.sublists.reverse → l₁ ++ l₂ ~ l'
l₁ l₂ : List α
h :
  (l₁, l₂) ∈
    (l'.sublists ++ map (fun x ↦ x ++ [a]) l'.sublists).zip
      ((map (fun x ↦ x ++ [a]) l'.sublists).reverse ++ l'.sublists.reverse)
⊢ l'.sublists.length = (map (fun x ↦ x ++ [a]) l'.sublists).reverse.length

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case cons
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
f g : β → α
a✝ : β
s✝ : Finset β
h✝ : a✝ ∉ s✝
ih : s✝.sup (f ⊔ g) = s✝.sup f ⊔ s✝.sup g
⊢ (cons a✝ s✝ h✝).sup (f ⊔ g) = (cons a✝ s✝ h✝).sup f ⊔ (cons a✝ s✝ h✝).sup g

Tactic:
sup_cons,

Goal state after:
case cons
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
f g : β → α
a✝ : β
s✝ : Finset β
h✝ : a✝ ∉ s✝
ih : s✝.sup (f ⊔ g) = s✝.sup f ⊔ s✝.sup g
⊢ (f ⊔ g) a✝ ⊔ s✝.sup (f ⊔ g) = (cons a✝ s✝ h✝).sup f ⊔ (cons a✝ s✝ h✝).sup g
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case cons
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
f g : β → α
a✝ : β
s✝ : Finset β
h✝ : a✝ ∉ s✝
ih : s✝.sup (f ⊔ g) = s✝.sup f ⊔ s✝.sup g
⊢ (f ⊔ g) a✝ ⊔ s✝.sup (f ⊔ g) = (cons a✝ s✝ h✝).sup f ⊔ (cons a✝ s✝ h✝).sup g

Tactic:
sup_cons,

Goal state after:
case cons
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
f g : β → α
a✝ : β
s✝ : Finset β
h✝ : a✝ ∉ s✝
ih : s✝.sup (f ⊔ g) = s✝.sup f ⊔ s✝.sup g
⊢ (f ⊔ g) a✝ ⊔ s✝.sup (f ⊔ g) = f a✝ ⊔ s✝.sup f ⊔ (cons a✝ s✝ h✝).sup g
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case cons
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
f g : β → α
a✝ : β
s✝ : Finset β
h✝ : a✝ ∉ s✝
ih : s✝.sup (f ⊔ g) = s✝.sup f ⊔ s✝.sup g
⊢ (f ⊔ g) a✝ ⊔ s✝.sup (f ⊔ g) = f a✝ ⊔ s✝.sup f ⊔ (cons a✝ s✝ h✝).sup g

Tactic:
sup_cons,

Goal state after:
case cons
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
f g : β → α
a✝ : β
s✝ : Finset β
h✝ : a✝ ∉ s✝
ih : s✝.sup (f ⊔ g) = s✝.sup f ⊔ s✝.sup g
⊢ (f ⊔ g) a✝ ⊔ s✝.sup (f ⊔ g) = f a✝ ⊔ s✝.sup f ⊔ (g a✝ ⊔ s✝.sup g)
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_5
inst✝⁵ : SemilatticeSup α
inst✝⁴ : OrderBot α
inst✝³ : SemilatticeSup β
inst✝² : OrderBot β
inst✝¹ : FunLike F α β
inst✝ : SupBotHomClass F α β
f : F
s✝ : Finset ι
g : ι → α
i : ι
s : Finset ι
x✝ : i ∉ s
h : f (s.sup g) = s.sup (⇑f ∘ g)
⊢ f ((cons i s x✝).sup g) = (cons i s x✝).sup (⇑f ∘ g)

Tactic:
sup_cons,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_5
inst✝⁵ : SemilatticeSup α
inst✝⁴ : OrderBot α
inst✝³ : SemilatticeSup β
inst✝² : OrderBot β
inst✝¹ : FunLike F α β
inst✝ : SupBotHomClass F α β
f : F
s✝ : Finset ι
g : ι → α
i : ι
s : Finset ι
x✝ : i ∉ s
h : f (s.sup g) = s.sup (⇑f ∘ g)
⊢ f (g i ⊔ s.sup g) = (cons i s x✝).sup (⇑f ∘ g)
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_5
inst✝⁵ : SemilatticeSup α
inst✝⁴ : OrderBot α
inst✝³ : SemilatticeSup β
inst✝² : OrderBot β
inst✝¹ : FunLike F α β
inst✝ : SupBotHomClass F α β
f : F
s✝ : Finset ι
g : ι → α
i : ι
s : Finset ι
x✝ : i ∉ s
h : f (s.sup g) = s.sup (⇑f ∘ g)
⊢ f (g i ⊔ s.sup g) = (cons i s x✝).sup (⇑f ∘ g)

Tactic:
sup_cons,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_5
inst✝⁵ : SemilatticeSup α
inst✝⁴ : OrderBot α
inst✝³ : SemilatticeSup β
inst✝² : OrderBot β
inst✝¹ : FunLike F α β
inst✝ : SupBotHomClass F α β
f : F
s✝ : Finset ι
g : ι → α
i : ι
s : Finset ι
x✝ : i ∉ s
h : f (s.sup g) = s.sup (⇑f ∘ g)
⊢ f (g i ⊔ s.sup g) = (⇑f ∘ g) i ⊔ s.sup (⇑f ∘ g)
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case cons
α : Type u_7
β : Type u_8
inst✝ : GeneralizedBooleanAlgebra α
f : β → α
a : α
a✝ : β
s✝ : Finset β
h✝ : a✝ ∉ s✝
h : (s✝.sup fun b ↦ f b \ a) = s✝.sup f \ a
⊢ ((cons a✝ s✝ h✝).sup fun b ↦ f b \ a) = (cons a✝ s✝ h✝).sup f \ a

Tactic:
sup_cons,

Goal state after:
case cons
α : Type u_7
β : Type u_8
inst✝ : GeneralizedBooleanAlgebra α
f : β → α
a : α
a✝ : β
s✝ : Finset β
h✝ : a✝ ∉ s✝
h : (s✝.sup fun b ↦ f b \ a) = s✝.sup f \ a
⊢ (f a✝ \ a ⊔ s✝.sup fun b ↦ f b \ a) = (cons a✝ s✝ h✝).sup f \ a
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case cons
α : Type u_7
β : Type u_8
inst✝ : GeneralizedBooleanAlgebra α
f : β → α
a : α
a✝ : β
s✝ : Finset β
h✝ : a✝ ∉ s✝
h : (s✝.sup fun b ↦ f b \ a) = s✝.sup f \ a
⊢ (f a✝ \ a ⊔ s✝.sup fun b ↦ f b \ a) = (cons a✝ s✝ h✝).sup f \ a

Tactic:
sup_cons,

Goal state after:
case cons
α : Type u_7
β : Type u_8
inst✝ : GeneralizedBooleanAlgebra α
f : β → α
a : α
a✝ : β
s✝ : Finset β
h✝ : a✝ ∉ s✝
h : (s✝.sup fun b ↦ f b \ a) = s✝.sup f \ a
⊢ (f a✝ \ a ⊔ s✝.sup fun b ↦ f b \ a) = (f a✝ ⊔ s✝.sup f) \ a
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : SemilatticeSup α
inst✝² : OrderBot α
inst✝¹ : SemilatticeSup γ
inst✝ : OrderBot γ
s : Finset β
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
bot : g ⊥ = ⊥
c : β
t : Finset β
hc : c ∉ t
ih : g (t.sup f) = t.sup (g ∘ f)
⊢ g ((cons c t hc).sup f) = (cons c t hc).sup (g ∘ f)

Tactic:
sup_cons,

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : SemilatticeSup α
inst✝² : OrderBot α
inst✝¹ : SemilatticeSup γ
inst✝ : OrderBot γ
s : Finset β
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
bot : g ⊥ = ⊥
c : β
t : Finset β
hc : c ∉ t
ih : g (t.sup f) = t.sup (g ∘ f)
⊢ g (f c ⊔ t.sup f) = (cons c t hc).sup (g ∘ f)
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : SemilatticeSup α
inst✝² : OrderBot α
inst✝¹ : SemilatticeSup γ
inst✝ : OrderBot γ
s : Finset β
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
bot : g ⊥ = ⊥
c : β
t : Finset β
hc : c ∉ t
ih : g (t.sup f) = t.sup (g ∘ f)
⊢ g (f c ⊔ t.sup f) = (cons c t hc).sup (g ∘ f)

Tactic:
sup_cons,

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : SemilatticeSup α
inst✝² : OrderBot α
inst✝¹ : SemilatticeSup γ
inst✝ : OrderBot γ
s : Finset β
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
bot : g ⊥ = ⊥
c : β
t : Finset β
hc : c ∉ t
ih : g (t.sup f) = t.sup (g ∘ f)
⊢ g (f c ⊔ t.sup f) = (g ∘ f) c ⊔ t.sup (g ∘ f)
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ ∅ ∈ s.powerset

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ s ∈ s.powerset

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Set.Finite.Range

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : DecidableEq α
f : ι → α
inst✝ : Fintype (PLift ι)
⊢ ∀ (x : α), x ∈ Finset.image (f ∘ PLift.down) Finset.univ ↔ x ∈ range f

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
s✝ t s : Finset α
p : Finset α → Prop
inst✝ : (t : Finset α) → Decidable (p t)
⊢ (∃ t, ∃ (_ : t ⊆ s), p t) ↔ ∃ t ⊆ s, p t

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
s✝ t s : Finset α
p : Finset α → Prop
inst✝ : (t : Finset α) → Decidable (p t)
⊢ (∀ t ⊆ s, p t) ↔ ∀ t ⊆ s, p t

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : SemilatticeSup α
inst✝² : OrderBot α
s : Finset β
f : β → α
inst✝¹ : One α
inst✝ : IsBotOneClass α
⊢ s.sup f = 1 ↔ ∀ i ∈ s, f i = 1

Tactic:
by
  simp [← bot_eq_one]

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : SemilatticeSup β
inst✝¹ : OrderBot β
inst✝ : WellFoundedGT β
f : α → β
h✝ : Nonempty α
t : Finset α
ht : ∀ x ∈ Set.range fun x ↦ x.sup f, ¬(fun x ↦ x.sup f) t < x
a : α
⊢ (fun x ↦ x.sup f) (insert a t) = f a ⊔ t.sup f

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
⊢ none ∉ map Embedding.some s

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
⊢ some a = none ∨ some a ∈ (map Embedding.some s).val ↔ ∀ a_1 ∈ some a, a_1 ∈ s

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
⊢ some a ∈ insertNone s ↔ a ∈ s

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ none ∈ insertNone s

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
n : ℕ
s : Finset α
h : n ≤ #s
⊢ ∀ (a : Finset α), a ⊆ s ∧ #a = n → a ∈ powersetCard n s

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
s : Finset (Option α)
p : Option α → Prop
⊢ (∀ a ∈ eraseNone s, p (some a)) ↔ ∀ (a : α), some a ∈ s → p (some a)

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case cons
α : Type u_2
ι : Type u_5
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
f : ι → α
a : α
a✝ : ι
s✝ : Finset ι
h✝ : a✝ ∉ s✝
h : a ⊓ s✝.sup f = s✝.sup fun i ↦ a ⊓ f i
⊢ a ⊓ (cons a✝ s✝ h✝).sup f = (cons a✝ s✝ h✝).sup fun i ↦ a ⊓ f i

Tactic:
sup_cons,

Goal state after:
case cons
α : Type u_2
ι : Type u_5
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
f : ι → α
a : α
a✝ : ι
s✝ : Finset ι
h✝ : a✝ ∉ s✝
h : a ⊓ s✝.sup f = s✝.sup fun i ↦ a ⊓ f i
⊢ a ⊓ (f a✝ ⊔ s✝.sup f) = (cons a✝ s✝ h✝).sup fun i ↦ a ⊓ f i
Module: Mathlib.Data.Set.Pairwise.Lattice

Goal state before:
pp: α : Type u_1
ι : Type u_2
s t : Set ι
f : ι → Set α
h : (s ∪ t).PairwiseDisjoint f
i : ι
hi : i ∈ s \ t
a : α
ha : a ∈ f i
⊢ a ∉ ⋃ x ∈ t, f x

Tactic:
rw [mem_iUnion₂]

Goal state after:
α : Type u_1
ι : Type u_2
s t : Set ι
f : ι → Set α
h : (s ∪ t).PairwiseDisjoint f
i : ι
hi : i ∈ s \ t
a : α
ha : a ∈ f i
⊢ ¬∃ i, ∃ (_ : i ∈ t), a ∈ f i
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case cons
α : Type u_2
ι : Type u_5
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
f : ι → α
a : α
a✝ : ι
s✝ : Finset ι
h✝ : a✝ ∉ s✝
h : a ⊓ s✝.sup f = s✝.sup fun i ↦ a ⊓ f i
⊢ a ⊓ (f a✝ ⊔ s✝.sup f) = (cons a✝ s✝ h✝).sup fun i ↦ a ⊓ f i

Tactic:
sup_cons,

Goal state after:
case cons
α : Type u_2
ι : Type u_5
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
f : ι → α
a : α
a✝ : ι
s✝ : Finset ι
h✝ : a✝ ∉ s✝
h : a ⊓ s✝.sup f = s✝.sup fun i ↦ a ⊓ f i
⊢ a ⊓ (f a✝ ⊔ s✝.sup f) = a ⊓ f a✝ ⊔ s✝.sup fun i ↦ a ⊓ f i
Module: Mathlib.Data.Fintype.Option

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝ : Fintype α
a : Option α
⊢ a ∈ insertNone univ

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Fintype.Option

Goal state before:
pp: α : Type u_3
inst✝ : Fintype α
⊢ none ∉ map Embedding.some univ

Tactic:
by simp

Goal state after: