mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
inst✝ : DecidableEq β
f : α → Finset β
⊢ (s.attach.biUnion fun x ↦ f ↑x) = s.biUnion f

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq α
f : ↥s → Finset β
⊢ s.attach.biUnion f = s.biUnion fun a ↦ if h : a ∈ s then f ⟨a, h⟩ else ∅

Tactic:
aesop

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

Goal state before:
pp: n k : ℕ
⊢ n.choose k * (n + 1) = (n + 1).choose k * (n + 1 - k)

Tactic:
cases k with
  | zero => simp
  | succ k =>
    obtain hk | hk := le_or_gt (k + 1) (n + 1)
    · rw [choose_succ_succ, Nat.add_mul, succ_sub_succ, ← choose_succ_right_eq, ← succ_sub_succ,
        Nat.mul_sub_left_distrib, Nat.add_sub_cancel' (Nat.mul_le_mul_left _ hk)]
    · rw [choose_eq_zero_of_lt hk, choose_eq_zero_of_lt (n.lt_succ_self.trans hk), Nat.zero_mul,
        Nat.zero_mul]

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

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
a : α
inst✝ : DecidableEq (δ a)
x : δ a
h : x ∈ t a
f : (b : α) → a ≠ b → δ b
hf : ∀ (b : α) (a : a ≠ b), f b a ∈ t b
⊢ (fun b ↦ if h : a = b then h ▸ x else f b h) ∈ piFinset t

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝² : DecidableEq (ι → α)
s : Finset α
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
⊢ {f ∈ Fintype.piFinset fun x ↦ s | ∃ a ∈ s, const ι a = f} = s.piDiag ι

Tactic:
aesop

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

Goal state before:
pp: case cons.mpr
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
a : α
m : Multiset α
ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ m.pi t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
f : (a_1 : α) → a_1 ∈ a ::ₘ m → β a_1
hf : ∀ (a_1 : α) (h : a_1 ∈ a ::ₘ m), f a_1 h ∈ t a_1
⊢ ∃ a_1, a_1 ∈ t a ∧ ∃ a_2, (∀ (a : α) (h : a ∈ m), a_2 a h ∈ t a) ∧ Pi.cons m a a_1 a_2 = f

Tactic:
refine ⟨_, hf a (mem_cons_self _ _), _, fun a ha => hf a (mem_cons_of_mem ha), ?_⟩

Goal state after:
case cons.mpr
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
a : α
m : Multiset α
ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ m.pi t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
f : (a_1 : α) → a_1 ∈ a ::ₘ m → β a_1
hf : ∀ (a_1 : α) (h : a_1 ∈ a ::ₘ m), f a_1 h ∈ t a_1
⊢ (Pi.cons m a (f a ⋯) fun a_1 ha ↦ f a_1 ⋯) = f
Module: Mathlib.Algebra.Group.Action.End

Goal state before:
pp: G : Type u_1
α : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G α
⊢ toPerm 1 = 1

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Group.Action.End

Goal state before:
pp: G : Type u_1
α : Type u_5
inst✝¹ : AddGroup G
inst✝ : AddAction G α
⊢ toPerm 0 = 1

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
t : Set α
S : Set (Set β)
f : α → β → γ
⊢ image2 f t (⋂₀ S) ⊆ ⋂ s ∈ S, image2 f t s

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
S : Set (Set α)
t : Set β
f : α → β → γ
⊢ image2 f (⋂₀ S) t ⊆ ⋂ s ∈ S, image2 f s t

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Mul α
inst✝ : Mul β
s₁ s₂ : Set α
t₁ t₂ : Set β
x✝ : α × β
⊢ (∃ a b, (a ∈ s₁ ∧ b ∈ t₁) ∧ ∃ a_1 b_1, (a_1 ∈ s₂ ∧ b_1 ∈ t₂) ∧ (a * a_1, b * b_1) = x✝) ↔
    (∃ x, x ∈ s₁ ∧ ∃ y, y ∈ s₂ ∧ x * y = x✝.1) ∧ ∃ x, x ∈ t₁ ∧ ∃ y, y ∈ t₂ ∧ x * y = x✝.2

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
S : Set (Set α)
t : Set β
⊢ image2 f (⋃₀ S) t = ⋃ s ∈ S, image2 f s t

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
T : Set (Set β)
⊢ image2 f s (⋃₀ T) = ⋃ t ∈ T, image2 f s t

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: case ofNat
α : Type u_2
inst✝ : DivisionMonoid α
a✝ : ℕ
hn : Int.ofNat a✝ ≠ 0
⊢ ∅ ^ Int.ofNat a✝ = ∅

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: case negSucc
α : Type u_2
inst✝ : DivisionMonoid α
a✝ : ℕ
hn : Int.negSucc a✝ ≠ 0
⊢ ∅ ^ Int.negSucc a✝ = ∅

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : DivisionMonoid α
a : α
n : ℤ
⊢ {a} ^ n = {a ^ n}

Tactic:
by cases n <;> simp

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H : Subgroup N
⊢ ↑(map f (comap f H)) = ↑(f.range ⊓ H)

Tactic:
by
    rw [coe_map, coe_comap, Set.image_preimage_eq_inter_range, coe_inf, coe_range, Set.inter_comm]

Goal state after:
Module: Mathlib.Algebra.Group.Subsemigroup.MulOpposite

Goal state before:
pp: M : Type u_2
inst✝ : Mul M
s : Set M
⊢ (closure s).op = closure (MulOpposite.unop ⁻¹' s)

Tactic:
closure,

Goal state after:
M : Type u_2
inst✝ : Mul M
s : Set M
⊢ (sInf {S | s ⊆ ↑S}).op = sInf {S | MulOpposite.unop ⁻¹' s ⊆ ↑S}
Module: Mathlib.Algebra.Group.Submonoid.MulOpposite

Goal state before:
pp: M : Type u_2
inst✝ : MulOneClass M
s : Set M
⊢ (closure s).op = closure (MulOpposite.unop ⁻¹' s)

Tactic:
closure,

Goal state after:
M : Type u_2
inst✝ : MulOneClass M
s : Set M
⊢ (sInf {S | s ⊆ ↑S}).op = sInf {S | MulOpposite.unop ⁻¹' s ⊆ ↑S}
Module: Mathlib.Data.Countable.Defs

Goal state before:
pp: α : Sort u
inst✝ : Nonempty α
⊢ ¬Countable α ↔ ∀ (f : ℕ → α), ¬Surjective f

Tactic:
countable_iff_exists_surjective,

Goal state after:
α : Sort u
inst✝ : Nonempty α
⊢ (¬∃ f, Surjective f) ↔ ∀ (f : ℕ → α), ¬Surjective f
Module: Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set G
⊢ (closure s).op = closure (MulOpposite.unop ⁻¹' s)

Tactic:
closure,

Goal state after:
G : Type u_2
inst✝ : Group G
s : Set G
⊢ (sInf {K | s ⊆ ↑K}).op = sInf {K | MulOpposite.unop ⁻¹' s ⊆ ↑K}
Module: Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set G
⊢ (closure s).op = closure (MulOpposite.unop ⁻¹' s)

Tactic:
by
  simp_rw [closure, op_sInf, Set.preimage_ofPred_eq, Subgroup.coe_unop]
  congr with a
  exact MulOpposite.unop_surjective.forall

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

Goal state before:
pp: case inl
m n : ℕ
h : m < n
⊢ max m n ^ 2 + min m n ≤ if m < n then n * n + m else m * m + m + n

pp: case inr
m n : ℕ
h : n ≤ m
⊢ max m n ^ 2 + min m n ≤ if m < n then n * n + m else m * m + m + n

Tactic:
· rw [if_pos h, max_eq_right h.le, min_eq_left h.le, Nat.pow_two]

Goal state after:
case inr
m n : ℕ
h : n ≤ m
⊢ max m n ^ 2 + min m n ≤ if m < n then n * n + m else m * m + m + n
Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g : G
⊢ zpowers g = ⊥ ↔ g = 1

Tactic:
rw [eq_bot_iff, zpowers_le, mem_bot]

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
Hs : Set (Subgroup G)
h : ∀ H ∈ Hs, H.Characteristic
⊢ (sInf Hs).Characteristic

Tactic:
simp [sInf_eq_iInf', characteristic_iInf, h]

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
g : G
⊢ (∀ (h : G), h ∈ s ↔ g⁻¹ * h * g ∈ s) ↔ ∀ (x : G), x ∈ ⇑(MulAut.conj g) '' s ↔ x ∈ s

Tactic:
Set.mem_image,

Goal state after:
G : Type u_1
inst✝ : Group G
s : Set G
g : G
⊢ (∀ (h : G), h ∈ s ↔ g⁻¹ * h * g ∈ s) ↔ ∀ (x : G), (∃ x_1 ∈ s, (MulAut.conj g) x_1 = x) ↔ x ∈ s
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Monoid α
inst✝ : MulAction α β
x✝ : Set β
⊢ 1 • x✝ = x✝

Tactic:
simp only [← image_smul, one_smul, image_id']

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
this : (⨅ g, map (↑(MulAut.conj g)) H).Normal
⊢ H.normalCore = ⨅ g, map (↑(MulAut.conj g)) H

Tactic:
refine le_antisymm (le_iInf fun g ↦ ?_) ?_

Goal state after:
case refine_1
G : Type u_1
inst✝ : Group G
H : Subgroup G
this : (⨅ g, map (↑(MulAut.conj g)) H).Normal
g : G
⊢ H.normalCore ≤ map (↑(MulAut.conj g)) H

case refine_2
G : Type u_1
inst✝ : Group G
H : Subgroup G
this : (⨅ g, map (↑(MulAut.conj g)) H).Normal
⊢ ⨅ g, map (↑(MulAut.conj g)) H ≤ H.normalCore
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: case refine_2
G : Type u_1
inst✝ : Group G
H : Subgroup G
this : (⨅ g, map (↑(MulAut.conj g)) H).Normal
⊢ ⨅ g, map (↑(MulAut.conj g)) H ≤ H.normalCore

Tactic:
· rw [normal_le_normalCore]
    apply iInf_le_of_le 1
    simp [MulAut.one_def]

Goal state after:
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Group α
s t : Set α
x : α
⊢ (x • s ∩ t).Nonempty ↔ ∃ a b, (a ∈ t ∧ b ∈ s) ∧ a / b = x

Tactic:
by
  simp_rw [smul_inter_nonempty_iff, div_eq_mul_inv]

Goal state after:
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: case mpr
α : Type u_2
inst✝ : Group α
s t : Set α
x : αᵐᵒᵖ
⊢ (∃ a b, (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = unop x) → (x • s ∩ t).Nonempty

Tactic:
rintro ⟨a, b, ⟨ha, hb⟩, H⟩

Goal state after:
case mpr
α : Type u_2
inst✝ : Group α
s t : Set α
x : αᵐᵒᵖ
a b : α
H : a⁻¹ * b = unop x
ha : a ∈ s
hb : b ∈ t
⊢ (x • s ∩ t).Nonempty
Module: Mathlib.Algebra.FreeMonoid.Basic

Goal state before:
pp: case mp.of_mul
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective ⇑(map f)
d : β
head : α
a✝¹ : FreeMonoid α
a✝ : (map f) a✝¹ = of d → ∃ a, f a = d
hb : (map f) (of head * a✝¹) = of d
⊢ ∃ a, f a = d

Tactic:
simp only [map_mul, map_of] at hb
      use head
      have H := congr_arg length hb
      simp only [length_mul, length_of, add_eq_left, length_eq_zero] at H
      rw [H, mul_one] at hb
      exact FreeMonoid.of_injective hb

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: case a
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
s : Set G
f : G →* N
hf : Surjective ⇑f
this : (map f (normalClosure s)).Normal
⊢ map f (normalClosure s) ≤ normalClosure (⇑f '' s)

Tactic:
exact map_normalClosure_le s f

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case cons
ι : Type u_1
M : Type u_3
inst✝⁵ : Monoid M
inst✝⁴ : Preorder M
inst✝³ : MulLeftStrictMono M
inst✝² : MulLeftMono M
inst✝¹ : MulRightStrictMono M
inst✝ : MulRightMono M
f g : ι → M
i : ι
l : List ι
ihl : (∀ (i : ι), i ∈ l → f i ≤ g i) → (∃ i, i ∈ l ∧ f i < g i) → (map f l).prod < (map g l).prod
h₁ : ∀ (i_1 : ι), i_1 ∈ i :: l → f i_1 ≤ g i_1
h₂ : ∃ i_1, i_1 ∈ i :: l ∧ f i_1 < g i_1
⊢ (map f (i :: l)).prod < (map g (i :: l)).prod

Tactic:
| cons i l ihl =>

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

Goal state before:
pp: case inr
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
h : Disjoint p q
x : { x // q x }
⊢ (subtypeOrLeftEmbedding p q)
      (Sum.elim (⇑(Subtype.impEmbedding p (fun x ↦ p x ∨ q x) ⋯)) (⇑(Subtype.impEmbedding q (fun x ↦ p x ∨ q x) ⋯))
        (Sum.inr x)) =
    Sum.inr x

Tactic:
| inr x =>

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 x_1 : N), x_1 ∈ s → ∀ x_2 ∈ t, x_1 * x_2 = x → P x) ↔ ∀ x₁ ∈ s, ∀ x₂ ∈ t, P (x₁ * x₂)

Tactic:
aesop

Goal state after:
Module: Mathlib.Logic.Denumerable

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

Tactic:
refine ⟨none, ?_, encode_none⟩

Goal state after:
case zero
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
⊢ none ∈ decode 0
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 : β
u : Finset (α ⊕ β)
⊢ ∀ (a a' : α ⊕ β), ∀ b ∈ Sum.elim some (fun x ↦ none) a, b ∈ Sum.elim some (fun x ↦ none) a' → a = a'

Tactic:
aesop

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 : β
u : Finset (α ⊕ β)
⊢ ∀ (a a' : α ⊕ β), ∀ b ∈ Sum.elim (fun x ↦ none) some a, b ∈ Sum.elim (fun x ↦ none) some a' → a = a'

Tactic:
aesop

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

Goal state before:
pp: α : Type u
β : Type u_1
γ : Type u_2
f : α → β → γ
p : γ → Prop
a : α
l₁ : List α
b : β
l₂ : List β
h : (a :: l₁).length = (b :: l₂).length
⊢ Forall p (zipWith f (a :: l₁) (b :: l₂)) ↔ Forall₂ (fun x y ↦ p (f x y)) (a :: l₁) (b :: l₂)

Tactic:
simp only [length_cons, succ_inj] at h
    simp [forall_zipWith h]

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

Goal state before:
pp: α : Type u
l : List α
⊢ ∀ (x : α) (y : Array (List α)),
    (Array.foldl (fun r l ↦ r.push (x :: l)) y.toList.toArray y.toList.toArray).toList =
      (Array.foldl (fun r l ↦ r.push (x :: l)) y y).toList

Tactic:
intros; congr

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

Goal state before:
pp: α : Type u
n : ℕ
a : α
l : List α
⊢ sublistsLen (n + 1) (a :: l) <+ (a :: l).sublists'

Tactic:
by
    rw [sublistsLen_succ_cons, sublists'_cons]
    exact (sublistsLen_sublist_sublists' _ _).append ((sublistsLen_sublist_sublists' _ _).map _)

Goal state after:
Module: Mathlib.Data.Set.Pairwise.Lattice

Goal state before:
pp: case mpr
α : Type u_1
κ : Sort u_4
r : α → α → Prop
f : κ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) f
H : ∀ (n : κ), (f n).Pairwise r
i : α
hi : i ∈ ⋃ n, f n
j : α
hj : j ∈ ⋃ n, f n
hij : i ≠ j
m : κ
hm : i ∈ f m
⊢ r i j

Tactic:
rcases mem_iUnion.1 hj with ⟨n, hn⟩

Goal state after:
case mpr
α : Type u_1
κ : Sort u_4
r : α → α → Prop
f : κ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) f
H : ∀ (n : κ), (f n).Pairwise r
i : α
hi : i ∈ ⋃ n, f n
j : α
hj : j ∈ ⋃ n, f n
hij : i ≠ j
m : κ
hm : i ∈ f m
n : κ
hn : j ∈ f n
⊢ r i j
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
c : α
⊢ (s₁ ∪ s₂).sup f ≤ c ↔ s₁.sup f ⊔ s₂.sup f ≤ c

Tactic:
simp [or_imp, forall_and]

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Set α
u : Set β
hu : u.Finite
this : Finite ↑u
g : ⦃a : β⦄ → a ∈ u → α
hg : ∀ ⦃a : β⦄ (a_1 : a ∈ u), g a_1 ∈ s
hg' : ∀ ⦃a : β⦄ (a_1 : a ∈ u), f (g a_1) = a
g' : ↑u → α := fun x ↦ g ⋯
a : α
ha : a ∈ range g'
⊢ a ∈ s

Tactic:
aesop

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Set α
u : Set β
hu : u.Finite
this : Finite ↑u
g : ⦃a : β⦄ → a ∈ u → α
hg : ∀ ⦃a : β⦄ (a_1 : a ∈ u), g a_1 ∈ s
hg' : ∀ ⦃a : β⦄ (a_1 : a ∈ u), f (g a_1) = a
g' : ↑u → α := fun x ↦ g ⋯
⊢ f '' range g' = u

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ t ≠ s ∧ t ∈ s.powerset ↔ t ⊂ s

Tactic:
mem_powerset,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ t ≠ s ∧ t ⊆ s ↔ t ⊂ s
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: α : Type u_1
n : ℕ
s : Finset α
h : #s < n
⊢ (#s).choose n = 0

Tactic:
Nat.choose_eq_zero_of_lt h

Goal state after:
α : Type u_1
n : ℕ
s : Finset α
h : #s < n
⊢ 0 = 0
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: case refine_2
α : Type u_1
s a : Finset α
ha : a ∈ (range (#s + 1)).disjiUnion (fun i ↦ powersetCard i s) ⋯
⊢ a ∈ s.powerset

Tactic:
rcases mem_disjiUnion.mp ha with ⟨i, _hi, ha⟩
    exact mem_powerset.mpr (mem_powersetCard.mp ha).1

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

Goal state before:
pp: case refine_2
α : Type u_1
s a : Finset α
ha : a ∈ (range (#s + 1)).disjiUnion (fun i ↦ powersetCard i s) ⋯
⊢ a ∈ s.powerset

Tactic:
· rcases mem_disjiUnion.mp ha with ⟨i, _hi, ha⟩
    exact mem_powerset.mpr (mem_powersetCard.mp ha).1

Goal state after:
Module: Mathlib.Data.Set.Pairwise.Lattice

Goal state before:
pp: α : Type u_1
s : Set α
a : α
ha : a ∉ s
⊢ (𝒫 s).PairwiseDisjoint fun t ↦ {t, insert a t}

Tactic:
by
  rw [pairwiseDisjoint_iff]
  rintro i hi j hj
  have := insert_erase_invOn.2.injOn (notMem_subset hi ha) (notMem_subset hj ha)
  aesop (add simp [Set.Nonempty, Set.subset_def])

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

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

Tactic:
rw [_root_.inf_comm, s.sup_inf_distrib_left]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : DecidableEq β
s₁ s₂ : Finset β
h₁ : s₁.Nonempty
h₂ : s₂.Nonempty
f : β → α
a : α
⊢ (s₁ ∪ s₂).sup' ⋯ f ≤ a ↔ s₁.sup' h₁ f ⊔ s₂.sup' h₂ f ≤ a

Tactic:
simp [or_imp, forall_and]

Goal state after:
Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : ConditionallyCompletePartialOrderSup α
inst✝¹ : Preorder β
inst✝ : IsDirectedOrder β
f g : β → α
hf : Monotone f
hg : Antitone g
h : f ≤ g
n : β
⊢ ⨆ n, f n ∈ Icc (f n) (g n)

Tactic:
have : Nonempty β := ⟨n⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : ConditionallyCompletePartialOrderSup α
inst✝¹ : Preorder β
inst✝ : IsDirectedOrder β
f g : β → α
hf : Monotone f
hg : Antitone g
h : f ≤ g
n : β
this : Nonempty β
⊢ ⨆ n, f n ∈ Icc (f n) (g n)
Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : ConditionallyCompletePartialOrderSup α
inst✝ : Preorder β
f : β → α
a : β
hf : Monotone f
hd : Directed (fun x1 x2 ↦ x1 ≤ x2) fun x ↦ f ↑x
x✝ : α
⊢ (x✝ ∈ range fun x ↦ f ↑x) → x✝ ≤ f a

Tactic:
aesop

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: case refine_1
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : (image f s).Nonempty
⊢ ∀ x ∈ Set.range fun i ↦ ⨆ (_ : i ∈ s), f i, ∃ y ∈ f '' ↑s, x ≤ y

Tactic:
simp only [ciSup_eq_ite, dite_eq_ite, Set.mem_range, Set.mem_image, mem_coe,
      exists_exists_and_eq_and, forall_exists_index, forall_apply_eq_imp_iff]

Goal state after:
case refine_1
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : (image f s).Nonempty
⊢ ∀ (a : ι), ∃ a_1 ∈ s, (if a ∈ s then f a else sSup ∅) ≤ f a_1
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Set α
himage : (f '' s).Finite
hfibers : ∀ x ∈ f '' s, (s ∩ f ⁻¹' {x}).Finite
x : α
⊢ x ∈ s → x ∈ ⋃ i ∈ f '' s, s ∩ f ⁻¹' {i}

Tactic:
aesop

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: case mp.refine_1
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, sSup ∅ ≤ f x
h : ⨆ i ∈ s, f i < a
x : ι
hx : x ∈ s
⊢ BddAbove (range fun i ↦ ⨆ (_ : i ∈ s), f i)

Tactic:
refine (((hs.image f).union (finite_singleton (sSup ∅))).subset ?_).bddAbove

Goal state after:
case mp.refine_1
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, sSup ∅ ≤ f x
h : ⨆ i ∈ s, f i < a
x : ι
hx : x ∈ s
⊢ (range fun i ↦ ⨆ (_ : i ∈ s), f i) ⊆ f '' s ∪ {sSup ∅}
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
ι : Type v
κ : ι → Sort w
inst✝¹ : Nonempty ((a : ι) → κ a)
inst✝ : Order.Frame α
s : Set ι
hs : s.Finite
f : (a : ι) → κ a → α
h : ∀ {κ : ι → Type w} [Nonempty ((a : ι) → κ a)] (f : (a : ι) → κ a → α), ⨅ a ∈ s, ⨆ b, f a b = ⨆ g, ⨅ a ∈ s, f a (g a)
this : Nonempty ((a : ι) → PLift (κ a))
⊢ ⨅ a ∈ s, ⨆ b, f a b = ⨆ g, ⨅ a ∈ s, f a (g a)

Tactic:
simpa [← Equiv.plift.symm.iSup_comp, ← (Equiv.piCongrRight fun _ => Equiv.plift).symm.iSup_comp]
      using h (κ := fun a => PLift (κ a)) fun a b => f a b.down

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Exists p → α
⊢ ⨆ (ih : Exists p), f ih ≤ ⨆ i, ⨆ (h : p i), f ⋯

Tactic:
by_cases! h : Exists p

Goal state after:
case pos
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Exists p → α
h : Exists p
⊢ ⨆ (ih : Exists p), f ih ≤ ⨆ i, ⨆ (h : p i), f ⋯

case neg
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Exists p → α
h : ∀ (x : ι), ¬p x
⊢ ⨆ (ih : Exists p), f ih ≤ ⨆ i, ⨆ (h : p i), f ⋯
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLattice α
p q : Prop
f : p ∧ q → α
⊢ ⨆ (ih : p ∧ q), f ih = ⨆ (h₁ : p), ⨆ (h₂ : q), f ⋯

Tactic:
by_cases hp : p <;> by_cases hq : q

Goal state after:
case pos
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
p q : Prop
f : p ∧ q → α
hp : p
hq : q
⊢ ⨆ (ih : p ∧ q), f ih = ⨆ (h₁ : p), ⨆ (h₂ : q), f ⋯

case neg
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
p q : Prop
f : p ∧ q → α
hp : p
hq : ¬q
⊢ ⨆ (ih : p ∧ q), f ih = ⨆ (h₁ : p), ⨆ (h₂ : q), f ⋯

case pos
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
p q : Prop
f : p ∧ q → α
hp : ¬p
hq : q
⊢ ⨆ (ih : p ∧ q), f ih = ⨆ (h₁ : p), ⨆ (h₂ : q), f ⋯

case neg
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
p q : Prop
f : p ∧ q → α
hp : ¬p
hq : ¬q
⊢ ⨆ (ih : p ∧ q), f ih = ⨆ (h₁ : p), ⨆ (h₂ : q), f ⋯
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ⋖ b
⊢ Ioo a b ∪ {a} = {a}

Tactic:
h.Ioo_eq,

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ⋖ b
⊢ ∅ ∪ {a} = {a}
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a ⋖ b
⊢ Ioo a b ∪ Ici b = Ici b

Tactic:
h.Ioo_eq,

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a ⋖ b
⊢ ∅ ∪ Ici b = Ici b
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a ⋖ b
⊢ Iic a ∪ Ioo a b = Iic a

Tactic:
h.Ioo_eq,

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a ⋖ b
⊢ Iic a ∪ ∅ = Iic a
Module: Mathlib.Data.Set.Sigma

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
s : Set ι
t : (i : ι) → Set (α i)
γ : Type u_7
f : (i : ι) × α i → γ
⊢ f '' s.sigma t = ⋃ i ∈ s, f ∘ Sigma.mk i '' t i

Tactic:
aesop

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
s : Set ι
t : (i : ι) → Set (α i)
⊢ s.sigma t = ⋃ i ∈ s, Sigma.mk i '' t i

Tactic:
aesop

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

Goal state before:
pp: α : Type u
β : Type v
s : Finset β
f : α → β
hf : InjOn f (f ⁻¹' ↑s)
inst✝ : DecidablePred fun x ↦ x ∈ Set.range f
b : β
hb : b ∈ ↑({x ∈ s | x ∈ Set.range f})
⊢ b ∈ f '' ↑(s.preimage f hf)

Tactic:
aesop

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: case refine_1
α : Type u_2
P Q : α → Prop
x : α
inst✝ : PartialOrder α
hPQ : ∀ ⦃x : α⦄, Q x → P x
h : ∀ ⦃x : α⦄, P x → ∃ y, y ≤ x ∧ Q y
h' : Minimal P x
y : α
hyx : y ≤ x
hy : Q y
⊢ Q x

Tactic:
rwa [((h'.le_of_le (hPQ hy)) hyx).antisymm hyx]

Goal state after: