mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: α : Type u_1
l₂ : List α
a : α
inst✝ : DecidableEq α
l₁ : List α
h : ¬a ∈ l₂
⊢ (a :: l₁) ∩ l₂ = l₁ ∩ l₂

Tactic:
by
  simp [Inter.inter, List.inter, h]

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

Goal state before:
pp: α : Type u_1
s : Multiset α
⊢ s.toList = [] ↔ s = 0

Tactic:
by
  rw [← coe_eq_zero, coe_toList]

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

Goal state before:
pp: α : Type u_1
s : Multiset α
⊢ s.toList.length = s.card

Tactic:
by
  rw [← coe_card, coe_toList]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
h : p a
⊢ count a (filter p s) = count a s

Tactic:
exact count_filter_of_pos h

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ t ∪ s = s ↔ t ⊆ s

Tactic:
union_eq_right

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ t ⊆ s ↔ t ⊆ s
Module: Mathlib.Data.Finset.Lattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
a : α
h : a ∈ s₂
x : α
⊢ x ∈ insert a s₁ ∩ s₂ ↔ x ∈ insert a (s₁ ∩ s₂)

Tactic:
have : x = a ∨ x ∈ s₂ ↔ x ∈ s₂ := or_iff_right_of_imp <| by rintro rfl; exact h

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
a : α
h : a ∈ s₂
x : α
this : x = a ∨ x ∈ s₂ ↔ x ∈ s₂
⊢ x ∈ insert a s₁ ∩ s₂ ↔ x ∈ insert a (s₁ ∩ s₂)
Module: Mathlib.Data.Fintype.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Fintype α
f : α → β
⊢ Set.InjOn f Set.univ ↔ Injective f

Tactic:
Set.injOn_univ

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Fintype α
f : α → β
⊢ Injective f ↔ Injective f
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α ≃ β
h : map f.toEmbedding s ⊆ t
x : α
hx : x ∈ s
⊢ f.symm.symm x ∈ map f.toEmbedding s

Tactic:
simp [hx]

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

Goal state before:
pp: α : Type u_1
s t : Set α
inst✝³ : DecidableEq α
inst✝² : Fintype ↑s
inst✝¹ : Fintype ↑t
inst✝ : Fintype ↑(s ∆ t)
a✝ : α
⊢ a✝ ∈ (s ∆ t).toFinset ↔ a✝ ∈ s.toFinset ∆ t.toFinset

Tactic:
simp [mem_symmDiff, Finset.mem_symmDiff]

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

Goal state before:
pp: α : Type u_1
s : Set α
inst✝¹ : Fintype α
inst✝ : Fintype ↑s
⊢ ↑s.toFinset = ↑Finset.univ ↔ s = univ

Tactic:
coe_toFinset,

Goal state after:
α : Type u_1
s : Set α
inst✝¹ : Fintype α
inst✝ : Fintype ↑s
⊢ s = ↑Finset.univ ↔ s = univ
Module: Mathlib.Data.Fintype.Sets

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
s : Set α
inst✝¹ : Fintype ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
a✝ : α
⊢ a✝ ∈ {x | x ∈ s} ↔ a✝ ∈ s.toFinset

Tactic:
mem_filter_univ,

Goal state after:
α : Type u_1
inst✝² : Fintype α
s : Set α
inst✝¹ : Fintype ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
a✝ : α
⊢ a✝ ∈ s ↔ a✝ ∈ s.toFinset
Module: Mathlib.Order.Fin.Basic

Goal state before:
pp: m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
hi : i < n
⊢ ↑(e ⟨i, hi⟩) = i

Tactic:
induction i using Nat.strong_induction_on with

Goal state after:
case h
m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
h : ∀ (m_1 : ℕ), m_1 < i → ∀ (hi : m_1 < n), ↑(e ⟨m_1, hi⟩) = m_1
hi : i < n
⊢ ↑(e ⟨i, hi⟩) = i
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n : ℕ
motive : Fin n → Prop
h : ∀ (j : Fin n), (∀ (k : Fin n), k < j → motive k) → motive j
i : ℕ
hi : i < n
⊢ motive ⟨i, hi⟩

Tactic:
induction i using Nat.strong_induction_on with

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

Goal state before:
pp: α : Type u_1
s : Finset α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : (x : α) → Decidable ¬p x
⊢ #(filter p s) + #({a ∈ s | ¬p a}) = #s

Tactic:
by
  classical
  rw [← card_union_of_disjoint (disjoint_filter_filter_not _ _ _), filter_union_filter_not_eq]

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

Goal state before:
pp: α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
n : ℕ
⊢ P (f n)

Tactic:
induction n using Nat.strong_induction_on with

Goal state after:
case h
α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
n : ℕ
IH : ∀ m < n, P (f m)
⊢ P (f n)
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case neg
m n : ℕ
α : Sort u_2
a : α
as : Fin n → α
bs : Fin m → α
i : ℕ
isLt✝ : i + 1 < n + 1 + m
h : ¬i + 1 < n + 1
⊢ ⋯ ▸ bs (subNat (n + 1) (Fin.cast ⋯ ⟨i + 1, isLt✝⟩) ⋯) = cases a (addCases as bs) (Fin.cast ⋯ ⟨i + 1, isLt✝⟩)

Tactic:
· have : ¬i < n := Nat.not_le_of_gt <| Nat.le_of_lt_succ <| Nat.gt_of_not_le h
      simp [addCases, this]

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

Goal state before:
pp: α : Type u
s t : Set α
inst✝ : DecidableEq α
hs : s.Finite
ht : t.Finite
h : (s ∆ t).Finite
a✝ : α
⊢ a✝ ∈ h.toFinset ↔ a✝ ∈ hs.toFinset ∆ ht.toFinset

Tactic:
simp [mem_symmDiff, Finset.mem_symmDiff]

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

Goal state before:
pp: α : Type u_1
L : List (List α)
x : List α
⊢ x ++ (map (fun x_1 ↦ x_1 ++ x) L).flatten = (map (fun x_1 ↦ x ++ x_1) L).flatten ++ x

Tactic:
induction L with grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s✝ : Finset α
g : α → β
hb : op b b = b
p : α → Prop
inst✝ : DecidablePred p
x : α
s : Finset α
hx : x ∉ s
IH : fold op b (fun i ↦ if p i then f i else g i) s = op (fold op b f (filter p s)) (fold op b g ({i ∈ s | ¬p i}))
h : p x
⊢ x ∉ filter p s

Tactic:
simp [hx]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s✝ : Finset α
g : α → β
hb : op b b = b
p : α → Prop
inst✝ : DecidablePred p
x : α
s : Finset α
hx : x ∉ s
IH : fold op b (fun i ↦ if p i then f i else g i) s = op (fold op b f (filter p s)) (fold op b g ({i ∈ s | ¬p i}))
h : ¬p x
⊢ x ∉ {i ∈ s | ¬p i}

Tactic:
simp [hx]

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

Goal state before:
pp: case cons.tail
α : Type u_1
R : α → α → Prop
a : α
inst✝¹ : Inhabited α
inst✝ : Std.Refl R
head✝ : α
tail✝ : List α
h : Pairwise R (head✝ :: tail✝)
a✝ : Mem a tail✝
⊢ R (head✝ :: tail✝).head! a

Tactic:
exact rel_of_pairwise_cons h (by assumption)

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

Goal state before:
pp: case inl
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : m < (drop (n % l.length) l).length
⊢ l[n % l.length + m]? = l[(m + n) % l.length]?

Tactic:
← add_mod_mod

Goal state after:
case inl
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : m < (drop (n % l.length) l).length
⊢ l[n % l.length + m]? = l[(m + n % l.length) % l.length]?
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: M : Type u_4
N : Type u_5
inst✝³ : Monoid M
inst✝² : Monoid N
F : Type u_8
inst✝¹ : FunLike F M Nᵐᵒᵖ
inst✝ : MonoidHomClass F M Nᵐᵒᵖ
f : F
l : List M
⊢ MulOpposite.unop (f l.prod) = (map (MulOpposite.unop ∘ ⇑f) l).reverse.prod

Tactic:
by
  rw [map_list_prod f l, MulOpposite.unop_list_prod, List.map_map]

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

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

Tactic:
by simp [choose]

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

Goal state before:
pp: case pos
m n : ℕ
hn : n ≠ 0
hm : m = 0
⊢ 0 < n

Tactic:
exact Nat.pos_of_ne_zero hn

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

Goal state before:
pp: G : Type u_2
X : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G X
x₀ : X
ha : ∀ (x : X), ∃ g, g • x₀ = x
y : X
g : G
⊢ ∃ g_1, g_1 • g • x₀ = y

Tactic:
rcases ha y with ⟨h, rfl⟩

Goal state after:
G : Type u_2
X : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G X
x₀ : X
ha : ∀ (x : X), ∃ g, g • x₀ = x
g h : G
⊢ ∃ g_1, g_1 • g • x₀ = h • x₀
Module: Mathlib.Algebra.Group.Pointwise.Set.Finite

Goal state before:
pp: case inl
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
hG : 0 < Fintype.card G
inst✝ : (k : ℕ) → DecidablePred fun x ↦ x ∈ ∅ ^ k
⊢ ∀ (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(∅ ^ k) = Fintype.card ↑(∅ ^ Fintype.card G)

Tactic:
refine fun k hk ↦ Fintype.card_congr ?_

Goal state after:
case inl
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
hG : 0 < Fintype.card G
inst✝ : (k : ℕ) → DecidablePred fun x ↦ x ∈ ∅ ^ k
k : ℕ
hk : Fintype.card G ≤ k
⊢ ↑(∅ ^ k) ≃ ↑(∅ ^ Fintype.card G)
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
a : α
⊢ ((fun x ↦ a⁻¹ * x) '' s ∩ t).Nonempty ↔ ((fun x ↦ x * a) '' s⁻¹ ∩ t⁻¹).Nonempty

Tactic:
← nonempty_inv,

Goal state after:
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
a : α
⊢ ((fun x ↦ a⁻¹ * x) '' s ∩ t)⁻¹.Nonempty ↔ ((fun x ↦ x * a) '' s⁻¹ ∩ t⁻¹).Nonempty
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
a : α
⊢ ((fun x ↦ x * a⁻¹) '' s ∩ t).Nonempty ↔ ((fun x ↦ a * x) '' s⁻¹ ∩ t⁻¹).Nonempty

Tactic:
← nonempty_inv,

Goal state after:
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
a : α
⊢ ((fun x ↦ x * a⁻¹) '' s ∩ t)⁻¹.Nonempty ↔ ((fun x ↦ a * x) '' s⁻¹ ∩ t⁻¹).Nonempty
Module: Mathlib.Algebra.Group.Submonoid.Basic

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
s : Set M
⊢ closure {1} ⊔ closure s = closure s

Tactic:
sup_eq_right,

Goal state after:
M : Type u_1
inst✝ : MulOneClass M
s : Set M
⊢ closure {1} ≤ closure s
Module: Mathlib.Algebra.Group.Subgroup.Defs

Goal state before:
pp: M : Type u_3
S : Type u_4
inst✝¹ : DivInvMonoid M
inst✝ : SetLike S M
hSM : SubgroupClass S M
K : S
x : M
hx : x ∈ K
n : ℕ
⊢ x ^ -[n+1] ∈ K

Tactic:
rw [zpow_negSucc]
    exact inv_mem (pow_mem hx n.succ)

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
S : Type u_4
H : S
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
P : G → Prop
x : G
x_in : x ∈ H
hx : P x⁻¹
⊢ P x⁻¹

Tactic:
simp [hx]

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
S : Type u_4
H : S
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
P : G → Prop
x : G
x_in : x ∈ H
hx : P x
⊢ P x⁻¹⁻¹

Tactic:
simp [hx]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
inst✝ : Nontrivial G
⊢ Nontrivial ↥⊤

Tactic:
nontrivial_iff_ne_bot

Goal state after:
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
inst✝ : Nontrivial G
⊢ ⊤ ≠ ⊥
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: case refine_2
G : Type u_1
inst✝ : Group G
ι : Type u_2
p : ι → Prop
K : ι → Subgroup G
i✝ : ι
hp : p i✝
hK : DirectedOn ((fun x1 x2 ↦ x1 ≤ x2) on K) {i | p i}
x : G
x✝ : ∃ i, p i ∧ x ∈ K i
i : ι
hi' : p i
hi : x ∈ K i
⊢ x ∈ ⨆ i, ⨆ (_ : p i), K i

Tactic:
· apply le_iSup (fun i ↦ ⨆ (_ : p i), K i) i
    simp [hi, hi']

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

Goal state before:
pp: case h
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
f : M →* N
N' : Submonoid N
hf : Surjective ⇑f
y : ↥N'
x : M
hx : f x = ↑y
⊢ ↑((f.submonoidComap N') ⟨x, ⋯⟩) = ↑y

Tactic:
simp [hx]

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

Goal state before:
pp: ι : Type u_4
M : ι → Type u_5
inst✝¹ : (i : ι) → MulOneClass (M i)
inst✝ : DecidableEq ι
S : (i : ι) → Submonoid (M i)
I : Set ι
i : ι
x : M i
hx : x ∈ S i
⊢ x ∈ comap (mulSingle M i) (pi I S)

Tactic:
simp [hx]

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

Goal state before:
pp: case bit
b : Bool
n : ℕ
⊢ (bit b n).bodd.toNat + 2 * (bit b n).div2 = bit b n

Tactic:
simpa using (bit_val b n).symm

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

Goal state before:
pp: case left
G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
hH₁ : H₁.Normal
hH₂ : H₂.Normal
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
⊢ x * (y * x⁻¹ * y⁻¹) ∈ H₁

Tactic:
exact H₁.mul_mem hx (hH₁.conj_mem _ (H₁.inv_mem hx) _)

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

Goal state before:
pp: case cons
α : Type u_5
β : Type u_6
inst✝³ : Monoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
l : List α
ih : l ≠ [] → (∀ (a : α), a ∈ l → p a) → f l.prod ≤ (map f l).prod
hl_nonempty : a :: l ≠ []
hl : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
⊢ f (a * l.prod) ≤ f a * (map f l).prod

Tactic:
by_cases hl_empty : l = []

Goal state after:
case pos
α : Type u_5
β : Type u_6
inst✝³ : Monoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
l : List α
ih : l ≠ [] → (∀ (a : α), a ∈ l → p a) → f l.prod ≤ (map f l).prod
hl_nonempty : a :: l ≠ []
hl : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
hl_empty : l = []
⊢ f (a * l.prod) ≤ f a * (map f l).prod

case neg
α : Type u_5
β : Type u_6
inst✝³ : Monoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
l : List α
ih : l ≠ [] → (∀ (a : α), a ∈ l → p a) → f l.prod ≤ (map f l).prod
hl_nonempty : a :: l ≠ []
hl : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
hl_empty : ¬l = []
⊢ f (a * l.prod) ≤ f a * (map f l).prod
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
s : Set M
x : M
hx : x ∈ ↑(closure s)
⊢ ∃ l, (∀ y ∈ l, y ∈ s) ∧ l.prod = x

Tactic:
closure_eq_image_prod,

Goal state after:
M : Type u_1
inst✝ : Monoid M
s : Set M
x : M
hx : x ∈ List.prod '' {l | ∀ x ∈ l, x ∈ s}
⊢ ∃ l, (∀ y ∈ l, y ∈ s) ∧ l.prod = x
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
⊢ False

Tactic:
exact Fintype.false
    ⟨(((Multiset.range (succ x)).filter (· ∈ s)).pmap
      (fun (y : ℕ) (hy : y ∈ s) => Subtype.mk y hy) (by simp [-Multiset.range_succ])).toFinset,
      by simpa [Subtype.ext_iff, Multiset.mem_filter, -Multiset.range_succ] ⟩

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
⊢ ∀ {a b : Finset (α ⊕ β)},
    { toFun := fun s ↦ (s.toLeft, s.toRight), invFun := fun s ↦ s.1.disjSum s.2, left_inv := ⋯, right_inv := ⋯ } a ≤
        { toFun := fun s ↦ (s.toLeft, s.toRight), invFun := fun s ↦ s.1.disjSum s.2, left_inv := ⋯, right_inv := ⋯ } b ↔
      a ⊆ b

Tactic:
simp [← Finset.coe_subset, Set.subset_def]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : Preorder γ
inst✝² : BoundedOrder α
inst✝¹ : BoundedOrder β
inst✝ : BoundedOrder γ
g : BoundedOrderHom β γ
f₁ f₂ : BoundedOrderHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
rw [← BoundedOrderHom.comp_apply, h, BoundedOrderHom.comp_apply]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Lattice α
inst✝¹ : Lattice β
inst✝ : Lattice γ
g : LatticeHom β γ
f₁ f₂ : LatticeHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
← LatticeHom.comp_apply,

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Lattice α
inst✝¹ : Lattice β
inst✝ : Lattice γ
g : LatticeHom β γ
f₁ f₂ : LatticeHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ (g.comp f₁) a = g (f₂ a)
Module: Mathlib.Order.Hom.Lattice

Goal state before:
pp: case inr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : LinearOrder α
inst✝¹ : Lattice β
inst✝ : OrderHomClass F α β
f : F
a b : α
h : b ≤ a
⊢ f (min a b) = f a ⊓ f b

Tactic:
rw [inf_eq_right.2 h, inf_eq_right.2 (OrderHomClass.mono f h : f b ≤ f a)]

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
a : α
s : Finset α
H : s.Nonempty
⊢ IsGreatest (↑(insert a s)) (max a (s.max' H))

Tactic:
rw [coe_insert]

Goal state after:
α : Type u_2
inst✝ : LinearOrder α
a : α
s : Finset α
H : s.Nonempty
⊢ IsGreatest (insert a ↑s) (max a (s.max' H))
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
a : α
s : Finset α
H : s.Nonempty
⊢ IsLeast (↑(insert a s)) (min a (s.min' H))

Tactic:
rw [coe_insert]

Goal state after:
α : Type u_2
inst✝ : LinearOrder α
a : α
s : Finset α
H : s.Nonempty
⊢ IsLeast (insert a ↑s) (min a (s.min' H))
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: case h
α : Type u_2
a✝ : List α
⊢ ((range (card ⟦a✝⟧ + 1)).bind fun k ↦ powersetCard k ⟦a✝⟧) = powerset ⟦a✝⟧

Tactic:
simp_rw [quot_mk_to_coe, powerset_coe', powersetCard_coe, ← coe_range, coe_bind,
    ← List.map_flatMap, coe_card]

Goal state after:
case h
α : Type u_2
a✝ : List α
⊢ ↑(List.map ofList (flatMap (fun a ↦ sublistsLen a a✝) (List.range (a✝.length + 1)))) = ↑(List.map ofList a✝.sublists')
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case append_singleton.inr
α : 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.zip l'.sublists.reverse
⊢ l₁' ++ [a] ++ id l₂ ~ l' ++ [a]

Tactic:
rw [append_assoc]
      apply (perm_append_comm.append_left _).trans
      rw [← append_assoc]
      exact (ih _ _ h).append_right _

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

Goal state before:
pp: α : Type u_1
s : Finset α
β : Type u_2
inst✝ : DecidableEq β
f : α → β
H : Set.InjOn f ↑s
⊢ Set.InjOn (fun x ↦ image f x) ↑s.powerset

Tactic:
have {z a} (_ : z ⊆ s) (_ : a ∈ s) : a ∈ z ↔ f a ∈ z.image f := by grind [H.eq_iff]
  exact fun _ _ _ _ _ => by grind

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

Goal state before:
pp: case mp
α : Type u_1
s a✝ : Finset α
⊢ a✝ ⊆ s ∧ #a✝ = #s → a✝ = s

pp: case mpr
α : Type u_1
s a✝ : Finset α
⊢ a✝ = s → a✝ ⊆ s ∧ #a✝ = #s

Tactic:
· exact fun ⟨hs, hc⟩ => eq_of_subset_of_card_le hs hc.ge

Goal state after:
case mpr
α : Type u_1
s a✝ : Finset α
⊢ a✝ = s → a✝ ⊆ s ∧ #a✝ = #s
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
⊢ t ⊆ map f s ∧ #t = n → ∃ a, (a ⊆ s ∧ #a = n) ∧ (mapEmbedding f).toEmbedding a = t

Tactic:
intro h
      have : map f (filter (fun x => (f x ∈ t)) s) = t := by grind
      refine ⟨_, ?_, this⟩
      rw [← card_map f, this, h.2]; simp

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝¹ : ConditionallyCompletePartialOrderSup α
inst✝ : Unique ι
s : ι → α
⊢ ⨆ i, s i = s default

Tactic:
by
  have : ∀ i, s i = s default := fun i => congr_arg s (Unique.eq_default i)
  simp only [this, ciSup_const]

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

Goal state before:
pp: case mp.refine_2
ι : 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
⊢ ⨆ (_ : x ∈ s), f x = f x

Tactic:
simp [hx]

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

Goal state before:
pp: case mp.refine_2
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, f x ≤ sInf ∅
h : a < ⨅ i ∈ s, f i
x : ι
hx : x ∈ s
⊢ ⨅ (_ : x ∈ s), f x = f x

Tactic:
simp [hx]

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

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLattice α
s : Set α
hs : BddBelow s
h : sInf s ≤ sInf ∅
⊢ ⨅ i, ↑i = sInf s

Tactic:
rw [← sInf_range, Subtype.range_coe]

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

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
s : Set ι
f : ι → ι'
g : ι' → α
hf : BddAbove (range fun i ↦ g (f ↑i))
hg' : sSup ∅ ≤ ⨆ i, g (f ↑i)
hs : s.Nonempty
hg : BddAbove (range fun i ↦ g ↑i)
⊢ sSup ∅ ≤ ⨆ i, g ↑i

Tactic:
refine hg'.trans ?_

Goal state after:
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
s : Set ι
f : ι → ι'
g : ι' → α
hf : BddAbove (range fun i ↦ g (f ↑i))
hg' : sSup ∅ ≤ ⨆ i, g (f ↑i)
hs : s.Nonempty
hg : BddAbove (range fun i ↦ g ↑i)
⊢ ⨆ i, g (f ↑i) ≤ ⨆ i, g ↑i
Module: Mathlib.Order.CompleteLattice.Finset

Goal state before:
pp: case refine_1
α : Type u_2
ι : Type u_5
inst✝ : CompleteLattice α
s : ι → α
⊢ ⨆ i, s i ≤ ⨆ t, ⨆ i ∈ t, s i

Tactic:
exact iSup_le fun b => le_iSup_of_le {b} <| le_iSup_of_le b <| le_iSup_of_le (by simp) <| le_rfl

Goal state after:
Module: Mathlib.Order.Cover

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

Tactic:
← Ioo_union_left h.lt,

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
Q : ι → Prop
f : ι → α
g : α → β
i : ι
hg : StrictAntiOn g (f '' ofPred Q)
h : MinimalFor Q (g ∘ f) i
⊢ MaximalFor Q f i

Tactic:
by
  refine ⟨h.prop, fun j hj hle ↦ ?_⟩
  by_contra
  exact h.not_lt hj <| hg ⟨i, h.prop, rfl⟩ ⟨j, hj, rfl⟩ <| lt_of_le_not_ge hle this

Goal state after:
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a : α
⊢ (Finset.Ioo a a).val = 0

Tactic:
Finset.Ioo_self,

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a : α
⊢ ∅.val = 0
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: case H
α : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DenselyOrdered α
a : α
i : Finset α
ih : ∀ t ⊂ i, ∀ (b : α), a < b → Icc a b = t → False
b : α
h : a < b
hs : Icc a b = i
⊢ False

Tactic:
| H i ih
   => 

Goal state after:
case H
α : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DenselyOrdered α
a : α
i : Finset α
ih : ∀ t ⊂ i, ∀ (b : α), a < b → Icc a b = t → False
b : α
h : a < b
hs : Icc a b = i
⊢ False
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ Ico a c ⊆ Ico a b ∪ Ico b c

Tactic:
rw [← coe_subset, coe_union, coe_Ico, coe_Ico, coe_Ico]

Goal state after:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ Set.Ico a c ⊆ Set.Ico a b ∪ Set.Ico b c
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: M : Type u_1
α : Type u_3
inst✝¹ : Monoid M
inst✝ : MulAction M α
a₁ a₂ : α
m : M
h : a₂ ∈ orbit M a₁
⊢ m • a₂ ∈ orbit M a₁

Tactic:
obtain ⟨x, rfl⟩ := mem_orbit_iff.mp h

Goal state after:
M : Type u_1
α : Type u_3
inst✝¹ : Monoid M
inst✝ : MulAction M α
a₁ : α
m x : M
h : x • a₁ ∈ orbit M a₁
⊢ m • x • a₁ ∈ orbit M a₁
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
a₁ a₂ b₁ b₂ : α
h₁ : a₁ ∈ [[a₂, b₂]]
h₂ : b₁ ∈ [[a₂, b₂]]
⊢ [[a₁, b₁]] ⊆ [[a₂, b₂]]

Tactic:
by
  rw [mem_uIcc] at h₁ h₂
  exact Icc_subset_Icc (_root_.le_inf h₁.1 h₂.1) (_root_.sup_le h₁.2 h₂.2)

Goal state after: