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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ a ∈ s \ t ∪ t \ s ↔ a ∈ s ∧ a ∉ t ∨ a ∈ t ∧ a ∉ s

Tactic:
mem_union,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ a ∈ s \ t ∨ a ∈ t \ s ↔ a ∈ s ∧ a ∉ t ∨ a ∈ t ∧ a ∉ s
Module: Mathlib.Data.Finset.Image

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

Tactic:
by
  simp only [← subset_map_symm, Equiv.symm_symm]

Goal state after:
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
h : 1 ≠ 0
⊢ 1 % (n + 1) ≤ 1

Tactic:
Nat.mod_le

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : ↥s → ↥t
hf : Injective f
⊢ #s ≤ #t

Tactic:
by
  rcases s.eq_empty_or_nonempty with rfl | ⟨a₀, ha₀⟩
  · simp
  · classical
    let f' : α → β := fun a => f (if ha : a ∈ s then ⟨a, ha⟩ else ⟨a₀, ha₀⟩)
    apply card_le_card_of_injOn f'
    · aesop (add safe unfold Set.MapsTo)
    · intro a₁ ha₁ a₂ ha₂ haa
      rw [mem_coe] at ha₁ ha₂
      simp only [f', ha₁, ha₂, ← Subtype.ext_iff] at haa
      exact Subtype.ext_iff.mp (hf haa)

Goal state after:
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
a : Fin (n + 1)
ha : a ≠ last n
⊢ (a.castPred ha).succ = a + 1

Tactic:
by
  cases a using lastCases
  · exact (ha rfl).elim
  · rw [castPred_castSucc, coeSucc_eq_succ]

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

Goal state before:
pp: case zero
α : Type u
f : Fin (succ 0) → α
⊢ ofFn f = (ofFn fun i ↦ f i.castSucc).concat (f (Fin.last 0))

Tactic:
ofFn_zero,

Goal state after:
case zero
α : Type u
f : Fin (succ 0) → α
⊢ ofFn f = [].concat (f (Fin.last 0))
Module: Mathlib.Data.List.OfFn

Goal state before:
pp: case zero
α : Type u
f : Fin (succ 0) → α
⊢ (f 0 :: ofFn fun i ↦ f i.succ) = [f (Fin.last 0)]

Tactic:
ofFn_zero,

Goal state after:
case zero
α : Type u
f : Fin (succ 0) → α
⊢ [f 0] = [f (Fin.last 0)]
Module: Mathlib.Data.List.OfFn

Goal state before:
pp: α : Type u
a : α
l : List α
⊢ ofFn (a :: l).get = a :: l

Tactic:
rw [ofFn_succ]
    congr
    exact ofFn_get l

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

Goal state before:
pp: α : Type u
c : α
⊢ (ofFn fun x ↦ c) = replicate 0 c

Tactic:
ofFn_zero,

Goal state after:
α : Type u
c : α
⊢ [] = replicate 0 c
Module: Mathlib.Data.List.OfFn

Goal state before:
pp: α : Type u
m : ℕ
a : Fin m → α
n : ℕ
⊢ ofFn (Fin.repeat n a) = (replicate n (ofFn a)).flatten

Tactic:
simp_rw [ofFn_mul, ← ofFn_const, Fin.repeat, Fin.modNat, Nat.add_comm,
    Nat.add_mul_mod_self_right, Nat.mod_eq_of_lt (Fin.is_lt _)]

Goal state after:
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ p.succAbove i < p ↔ i.castSucc < p

Tactic:
rcases castSucc_lt_or_lt_succ p i with H | H
  · rwa [iff_true_right H, succAbove_of_castSucc_lt _ _ H]
  · rw [castSucc_lt_iff_succ_le, iff_false_right (Fin.not_le.2 H), succAbove_of_lt_succ _ _ H]
    exact Fin.not_lt.2 <| Fin.le_of_lt H

Goal state after:
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
hi✝ : i ≠ last (n + 1)
hi : ∃ j, j.castSucc = i
⊢ (last n).predAbove i = i.castPred hi✝

Tactic:
rcases hi with ⟨y, rfl⟩

Goal state after:
n : ℕ
y : Fin (n + 1)
hi : y.castSucc ≠ last (n + 1)
⊢ (last n).predAbove y.castSucc = y.castSucc.castPred hi
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inr
n : ℕ
a : Fin n
b : Fin (n + 1)
h : b < a.succ
⊢ a.succ.predAbove b.succ = (a.predAbove b).succ

Tactic:
predAbove_of_lt_succ _ _ h,

Goal state after:
case inr
n : ℕ
a : Fin n
b : Fin (n + 1)
h : b < a.succ
⊢ a.succ.predAbove b.succ = (b.castPred ⋯).succ
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inl
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.castSucc < i
⊢ (i.pred ⋯).predAbove j.castSucc = j

Tactic:
predAbove_of_le_castSucc,

Goal state after:
case inl
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.castSucc < i
⊢ j.castSucc.castPred ⋯ = j

case inl.h
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.castSucc < i
⊢ j.castSucc ≤ (i.pred ⋯).castSucc
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: case intro
α : Type u_1
inst✝ : Finite α
f : α → α
hinj : Injective f
x : α
this : (a : Prop) → Decidable a
val✝ : Fintype α
h₁ : image f univ = univ
h₂ : x ∈ image f univ
⊢ ∃ a, f a = x

Tactic:
obtain ⟨y, h⟩ := mem_image.1 h₂

Goal state after:
case intro
α : Type u_1
inst✝ : Finite α
f : α → α
hinj : Injective f
x : α
this : (a : Prop) → Decidable a
val✝ : Fintype α
h₁ : image f univ = univ
h₂ : x ∈ image f univ
y : α
h : y ∈ univ ∧ f y = x
⊢ ∃ a, f a = x
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 α
a : α
h : a ∉ s
⊢ Multiset.fold op b (f a ::ₘ Multiset.map f s.val) = op (f a) (Multiset.fold op b (Multiset.map f s.val))

Tactic:
fold_cons_left

Goal state after:
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
a : α
h : a ∉ s
⊢ op (f a) (Multiset.fold op b (Multiset.map f s.val)) = op (f a) (Multiset.fold op b (Multiset.map f s.val))
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 α
a : α
inst✝ : DecidableEq α
h : a ∉ s
⊢ Multiset.fold op b (f a ::ₘ Multiset.map f s.val) = op (f a) (Multiset.fold op b (Multiset.map f s.val))

Tactic:
fold_cons_left

Goal state after:
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
h : a ∉ s
⊢ op (f a) (Multiset.fold op b (Multiset.map f s.val)) = op (f a) (Multiset.fold op b (Multiset.map f s.val))
Module: Mathlib.Data.List.Pairwise

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
inst✝ : Std.Refl R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
heq : ¬a = b
⊢ R a b

Tactic:
apply h <;> try (apply hab.subset; simp)
    exact heq

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

Goal state before:
pp: case nil
⊢ Pairwise Disjoint [].ranges

Tactic:
exact Pairwise.nil

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Defs

Goal state before:
pp: case cons
M : Type u_3
inst✝ : CommMonoid M
s✝ : Multiset M
p : M → Prop
p_mul : ∀ (a b : M), p a → p b → p (a * b)
a : M
s : Multiset M
hsa : s ≠ ∅ → (∀ (a : M), a ∈ s → p a) → p s.prod
hs : a ::ₘ s ≠ ∅
p_s : ∀ (a_1 : M), a_1 ∈ a ::ₘ s → p a_1
⊢ p (a ::ₘ s).prod

Tactic:
prod_cons

Goal state after:
case cons
M : Type u_3
inst✝ : CommMonoid M
s✝ : Multiset M
p : M → Prop
p_mul : ∀ (a b : M), p a → p b → p (a * b)
a : M
s : Multiset M
hsa : s ≠ ∅ → (∀ (a : M), a ∈ s → p a) → p s.prod
hs : a ::ₘ s ≠ ∅
p_s : ∀ (a_1 : M), a_1 ∈ a ::ₘ s → p a_1
⊢ p (a * s.prod)
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
a : α
l : List α
n : ℕ
⊢ ((a :: l).rotate' (n + 1)).length = (a :: l).length

Tactic:
rw [List.rotate', length_rotate' (l ++ [a]) n]; simp

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

Goal state before:
pp: M : Type u_8
inst✝ : CommMonoid M
L : List M
⊢ IsUnit L.prod ↔ ∀ (m : M), m ∈ L → IsUnit m

Tactic:
by
  refine ⟨fun h => ?_, prod_isUnit⟩
  induction L with
  | nil => exact fun m' h' => False.elim (not_mem_nil h')
  | cons m L ih =>
    rw [prod_cons, IsUnit.mul_iff] at h
    exact fun m' h' ↦ Or.elim (eq_or_mem_of_mem_cons h') (fun H => H.substr h.1) fun H => ih h.2 _ H

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

Goal state before:
pp: l s : List ℕ
hs : s ∈ l.ranges
⊢ Pairwise (fun x1 x2 ↦ x1 ≠ x2) l.ranges.flatten

Tactic:
by rw [ranges_flatten]; exact nodup_range

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

Goal state before:
pp: α : Type u
l l' : List α
⊢ l.reverse ~r l'.reverse ↔ l ~r l'

Tactic:
by
  simp [isRotated_reverse_comm_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : α → Finset β
inst✝ : DecidableEq β
b : β
⊢ b ∈ s.biUnion t ↔ ∃ a ∈ s, b ∈ t a

Tactic:
by
  simp only [mem_def, biUnion_val, Multiset.mem_dedup, Multiset.mem_bind]

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

Goal state before:
pp: α : Type u_1
β : Type v
l₁ : List α
l₂ : List β
⊢ ((↑l₁).bind fun a ↦ map (Prod.mk a) ↑l₂) = ↑(List.flatMap (fun a ↦ List.map (Prod.mk a) l₂) l₁)

Tactic:
← coe_bind

Goal state after:
α : Type u_1
β : Type v
l₁ : List α
l₂ : List β
⊢ ((↑l₁).bind fun a ↦ map (Prod.mk a) ↑l₂) = (↑l₁).bind fun a ↦ ↑(List.map (Prod.mk a) l₂)
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l l' : List α
h : l.cyclicPermutations = l'.cyclicPermutations
⊢ l = l'

Tactic:
simpa using congr_arg head? h

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

Goal state before:
pp: α : Type u_1
σ : α → Type u_4
l₁ : List α
l₂ : (a : α) → List (σ a)
⊢ ((↑l₁).bind fun a ↦ map (Sigma.mk a) ↑(l₂ a)) = ↑(l₁.sigma l₂)

Tactic:
List.sigma,

Goal state after:
α : Type u_1
σ : α → Type u_4
l₁ : List α
l₂ : (a : α) → List (σ a)
⊢ ((↑l₁).bind fun a ↦ map (Sigma.mk a) ↑(l₂ a)) = ↑(List.flatMap (fun a ↦ List.map (Sigma.mk a) (l₂ a)) l₁)
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_1
σ : α → Type u_4
l₁ : List α
l₂ : (a : α) → List (σ a)
⊢ ((↑l₁).bind fun a ↦ map (Sigma.mk a) ↑(l₂ a)) = ↑(List.flatMap (fun a ↦ List.map (Sigma.mk a) (l₂ a)) l₁)

Tactic:
← coe_bind

Goal state after:
α : Type u_1
σ : α → Type u_4
l₁ : List α
l₂ : (a : α) → List (σ a)
⊢ ((↑l₁).bind fun a ↦ map (Sigma.mk a) ↑(l₂ a)) = (↑l₁).bind fun a ↦ ↑(List.map (Sigma.mk a) (l₂ a))
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
f : α → β
s✝ : Finset α
t : β → Finset γ
this : DecidableEq α
a : α
s : Finset α
x✝ : a ∉ s
ih : (image f s).biUnion t = s.biUnion fun a ↦ t (f a)
⊢ (image f (insert a s)).biUnion t = (insert a s).biUnion fun a ↦ t (f a)

Tactic:
simp only [image_insert, biUnion_insert, ih]

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

Goal state before:
pp: α : Type u
l : List α
k : ℕ
this : (l.rotate k).cyclicPermutations.length = (l.cyclicPermutations.rotate k).length
n : ℕ
hn : n < (l.rotate k).cyclicPermutations.length
hn' : n < (l.cyclicPermutations.rotate k).length
⊢ (l.rotate k).cyclicPermutations.get ⟨n, hn⟩ = (l.cyclicPermutations.rotate k).get ⟨n, hn'⟩

Tactic:
rw [get_rotate, get_cyclicPermutations, rotate_rotate, ← rotate_mod, Nat.add_comm]

Goal state after:
α : Type u
l : List α
k : ℕ
this : (l.rotate k).cyclicPermutations.length = (l.cyclicPermutations.rotate k).length
n : ℕ
hn : n < (l.rotate k).cyclicPermutations.length
hn' : n < (l.cyclicPermutations.rotate k).length
⊢ l.rotate ((↑⟨n, hn⟩ + k) % l.length) = l.cyclicPermutations.get ⟨(↑⟨n, hn'⟩ + k) % l.cyclicPermutations.length, ⋯⟩
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: x✝ : ℕ
hk : x✝ ≤ 0
⊢ 0 < choose 0 x✝

Tactic:
rw [Nat.eq_zero_of_le_zero hk]

Goal state after:
x✝ : ℕ
hk : x✝ ≤ 0
⊢ 0 < choose 0 0
Module: Mathlib.Data.List.OffDiag

Goal state before:
pp: case mp
α : Type u_1
l : List α
h : l.Nodup
x y : α
⊢ (∃ i h j h_1, ¬i = j ∧ l[i] = x ∧ l[j] = y) → (∃ i h, l[i] = x) ∧ (∃ i h, l[i] = y) ∧ ¬x = y

Tactic:
rintro ⟨i, hi, j, hj, hne, rfl, rfl⟩
    exact ⟨⟨i, hi, rfl⟩, ⟨j, hj, rfl⟩, mt h.getElem_inj_iff.1 hne⟩

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

Goal state before:
pp: n : ℕ
⊢ n + 1 + (n + 1).choose n.succ = n + 1 + 1

Tactic:
choose_self

Goal state after:
n : ℕ
⊢ n + 1 + 1 = n + 1 + 1
Module: Mathlib.Data.Finset.Prod

Goal state before:
pp: ι : Type u_4
inst✝² : PartialOrder ι
inst✝¹ : DecidableLE ι
inst✝ : DecidableLT ι
s : Finset ι
a✝ : ι × ι
⊢ a✝ ∈ {i ∈ s.offDiag | i.1 < i.2} ↔ a✝ ∈ {i ∈ s.offDiag | i.1 ≤ i.2}

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

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

Goal state before:
pp: M✝ : Type u_1
G : Type u_2
α✝ : Type u_3
β : Type u_4
M : Type u_5
α : Type u_6
inst✝² : Monoid M
inst✝¹ : MulAction M α
inst✝ : Subsingleton α
x y : α
⊢ 1 • x = y

Tactic:
by
    simp only [one_smul, Subsingleton.elim x y]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
p : ι → Prop
s : (i : ι) → p i → Set α
hp : ∃ i, p i
f : α → β
h : InjOn f (⋃ i, ⋃ (hi : p i), s i hi)
⊢ f '' ⨅ x, s ↑x ⋯ = ⨅ x, f '' s ↑x ⋯

Tactic:
have : Nonempty { i // p i } := nonempty_subtype.2 hp

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_5
p : ι → Prop
s : (i : ι) → p i → Set α
hp : ∃ i, p i
f : α → β
h : InjOn f (⋃ i, ⋃ (hi : p i), s i hi)
this : Nonempty { i // p i }
⊢ f '' ⨅ x, s ↑x ⋯ = ⨅ x, f '' s ↑x ⋯
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
⊢ ⋃ b ∈ t, (fun x ↦ f x b) '' s = image2 f s t

Tactic:
by
  rw [image2_swap, iUnion_image_left]

Goal state after:
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 ∈ ⨆ (_ : p i), K i

Tactic:
simp [hi, hi']

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

Goal state before:
pp: G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Group G'
inst✝⁴ : Group G''
A : Type u_4
inst✝³ : AddGroup A
H✝ K : Subgroup G
k : Set G
N : Type u_5
inst✝² : Group N
P : Type u_6
inst✝¹ : Group P
H : Subgroup G
f : G →* G'
inst✝ : IsMulCommutative ↥H
⊢ ∀ a ∈ map f H, ∀ b ∈ map f H, a * b = b * a

Tactic:
rintro - ⟨a, ha, rfl⟩ - ⟨b, hb, rfl⟩

Goal state after:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Group G'
inst✝⁴ : Group G''
A : Type u_4
inst✝³ : AddGroup A
H✝ K : Subgroup G
k : Set G
N : Type u_5
inst✝² : Group N
P : Type u_6
inst✝¹ : Group P
H : Subgroup G
f : G →* G'
inst✝ : IsMulCommutative ↥H
a : G
ha : a ∈ ↑H
b : G
hb : b ∈ ↑H
⊢ f a * f b = f b * f a
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ H.subgroupOf (H ⊔ K) ⊔ K.subgroupOf (H ⊔ K) = ⊤

Tactic:
← subgroupOf_sup,

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ (H ⊔ K).subgroupOf (H ⊔ K) = ⊤

case hA
G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ H ≤ H ⊔ K

case hA'
G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ K ≤ H ⊔ K
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: case mp.right
N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
h : u ≤ s.prod t
⊢ map (snd M N) u ≤ t

Tactic:
rintro x ⟨⟨y1, y2⟩, ⟨hy1, rfl⟩⟩
      exact (h hy1).2

Goal state after:
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: n : ℕ
h : 2 ≤ n
this : decodeSum n = none
⊢ decode n = none

Tactic:
change (decodeSum n).bind _ = none

Goal state after:
n : ℕ
h : 2 ≤ n
this : decodeSum n = none
⊢ (decodeSum n).bind (some ∘ ⇑Equiv.boolEquivPUnitSumPUnit.symm) = none
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: M : Type u_5
ι : Type u_6
α : ι → Type u_7
inst✝¹ : Monoid M
inst✝ : (i : ι) → MulAction M (α i)
I : Set ι
s : (i : ι) → Set (α i)
c : Mˣ
⊢ ↑c • I.pi s = I.pi (↑c • s)

Tactic:
exact smul_set_pi c I s

Goal state after:
Module: Mathlib.Algebra.Group.Idempotent

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
h : IsUnit a
idem : IsIdempotentElem a
⊢ a = 1

Tactic:
by
    have ⟨q, eq⟩ := h.exists_left_inv
    rw [← eq, ← idem.eq, ← mul_assoc, eq, one_mul, idem.eq]

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

Goal state before:
pp: case cons
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulLeftMono M
hd : M
tl : List M
ih : (∀ (x : M), x ∈ tl → 1 ≤ x) → 1 ≤ tl.prod
hl₁ : ∀ (x : M), x ∈ hd :: tl → 1 ≤ x
⊢ 1 ≤ (hd :: tl).prod

Tactic:
prod_cons

Goal state after:
case cons
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulLeftMono M
hd : M
tl : List M
ih : (∀ (x : M), x ∈ tl → 1 ≤ x) → 1 ≤ tl.prod
hl₁ : ∀ (x : M), x ∈ hd :: tl → 1 ≤ x
⊢ 1 ≤ hd * tl.prod
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:
prod_cons

Goal state after:
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
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
inst✝¹ : MulOneClass M
ι : Sort u_4
inst✝ : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : M
this : x ∈ closure (⋃ i, ↑(S i)) → ∃ i, x ∈ S i
⊢ x ∈ ⨆ i, S i → ∃ i, x ∈ S i

Tactic:
simpa only [closure_iUnion, closure_eq (S _)] using this

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
⊢ (∃ a,
      (Sum.inl a ∈
          match n.bodd, n.div2 with
          | false, m => some (Sum.inl (ofNat α m))
          | x, m => some (Sum.inr (ofNat β m))) ∧
        encodeSum (Sum.inl a) = bit n.bodd n.div2) ∨
    ∃ b,
      (Sum.inr b ∈
          match n.bodd, n.div2 with
          | false, m => some (Sum.inl (ofNat α m))
          | x, m => some (Sum.inr (ofNat β m))) ∧
        encodeSum (Sum.inr b) = bit n.bodd n.div2

Tactic:
cases bodd n <;> simp [bit_val, encodeSum]

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 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
u : Finset (α ⊕ β)
a : α
⊢ a ∈ u.toLeft ↔ inl a ∈ u

Tactic:
by simp [toLeft]

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
l : List α
m : α
a✝ : m ∈ l
h : ∀ (a : α), a ∈ l → a ≤ m
a : α
hal : a ∈ l
⊢ m ≤ a → idxOf m l ≤ idxOf a l

Tactic:
hma

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
l : List α
m : α
a✝ : m ∈ l
h : ∀ (a : α), a ∈ l → a ≤ m
a : α
hal : a ∈ l
hma : m ≤ a
⊢ idxOf m l ≤ idxOf a l
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case cons
α : Type u
l l' l₁ l₂ : List α
a : α
s : l₁ <+ l₂
IH : l₁ ∈ sublistsLen l₁.length l₂
⊢ l₁ ∈ sublistsLen l₁.length (a :: l₂)

Tactic:
rcases l₁ with - | ⟨b, l₁⟩

Goal state after:
case cons.nil
α : Type u
l l' l₂ : List α
a : α
s : [] <+ l₂
IH : [] ∈ sublistsLen [].length l₂
⊢ [] ∈ sublistsLen [].length (a :: l₂)

case cons.cons
α : Type u
l l' l₂ : List α
a b : α
l₁ : List α
s : b :: l₁ <+ l₂
IH : b :: l₁ ∈ sublistsLen (b :: l₁).length l₂
⊢ b :: l₁ ∈ sublistsLen (b :: l₁).length (a :: l₂)
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case cons.cons
α : Type u
l l' l₂ : List α
a b : α
l₁ : List α
s : b :: l₁ <+ l₂
IH : b :: l₁ ∈ sublistsLen (b :: l₁).length l₂
⊢ b :: l₁ ∈ sublistsLen (b :: l₁).length (a :: l₂)

Tactic:
rw [length, sublistsLen_succ_cons]

Goal state after:
case cons.cons
α : Type u
l l' l₂ : List α
a b : α
l₁ : List α
s : b :: l₁ <+ l₂
IH : b :: l₁ ∈ sublistsLen (b :: l₁).length l₂
⊢ b :: l₁ ∈ sublistsLen (l₁.length + 1) l₂ ++ map (cons a) (sublistsLen l₁.length l₂)
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case cons_cons
α : Type u
l l' l₁✝ l₂✝ : List α
a : α
s : l₁✝ <+ l₂✝
IH : l₁✝ ∈ sublistsLen l₁✝.length l₂✝
⊢ a :: l₁✝ ∈ sublistsLen (a :: l₁✝).length (a :: l₂✝)

Tactic:
rw [length, sublistsLen_succ_cons]

Goal state after:
case cons_cons
α : Type u
l l' l₁✝ l₂✝ : List α
a : α
s : l₁✝ <+ l₂✝
IH : l₁✝ ∈ sublistsLen l₁✝.length l₂✝
⊢ a :: l₁✝ ∈ sublistsLen (l₁✝.length + 1) l₂✝ ++ map (cons a) (sublistsLen l₁✝.length l₂✝)
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
R : α → α → Prop
a : α
l : List α
H₁ : ∀ (a' : α), a' ∈ l → R a a'
H₂ : Pairwise R l
l₁ : List α
sl₁ : l₁ <+ l
l₂ : List α
a✝ : l₂ <+ l
⊢ Lex (Function.swap R) l₁ (a :: l₂)

Tactic:
rcases l₁ with - | ⟨b, l₁⟩

Goal state after:
case nil
α : Type u
R : α → α → Prop
a : α
l : List α
H₁ : ∀ (a' : α), a' ∈ l → R a a'
H₂ : Pairwise R l
l₂ : List α
a✝ : l₂ <+ l
sl₁ : [] <+ l
⊢ Lex (Function.swap R) [] (a :: l₂)

case cons
α : Type u
R : α → α → Prop
a : α
l : List α
H₁ : ∀ (a' : α), a' ∈ l → R a a'
H₂ : Pairwise R l
l₂ : List α
a✝ : l₂ <+ l
b : α
l₁ : List α
sl₁ : b :: l₁ <+ l
⊢ Lex (Function.swap R) (b :: l₁) (a :: l₂)
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: 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')

Tactic:
exact coe_eq_coe.mpr ((List.range_bind_sublistsLen_perm _).map _)

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

Goal state before:
pp: α : Type u_1
s : Set (Set α)
hd : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) s
r : α → α → Prop
h : ∀ a ∈ s, a.Pairwise r
x : α
S : Set α
⊢ S ∈ s → x ∈ S → ∀ ⦃y : α⦄, ∀ x_1 ∈ s, y ∈ x_1 → x ≠ y → r x y

Tactic:
hS

Goal state after:
α : Type u_1
s : Set (Set α)
hd : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) s
r : α → α → Prop
h : ∀ a ∈ s, a.Pairwise r
x : α
S : Set α
hS : S ∈ s
⊢ x ∈ S → ∀ ⦃y : α⦄, ∀ x_1 ∈ s, y ∈ x_1 → x ≠ y → r x y
Module: Mathlib.Data.Set.Pairwise.Lattice

Goal state before:
pp: case inr.refine_1
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : s.PairwiseDisjoint fun i ↦ ⨆ i' ∈ t, f (i, i')
ht : t.PairwiseDisjoint fun i' ↦ ⨆ i ∈ s, f (i, i')
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
j : ι
j' : ι'
hj : (j, j').1 ∈ s ∧ (j, j').2 ∈ t
h : (i, i') ≠ (j, j')
hij : i ≠ j
⊢ f (i, i') ≤ (fun i ↦ ⨆ i' ∈ t, f (i, i')) (i, i').1

pp: case inr.refine_2
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : s.PairwiseDisjoint fun i ↦ ⨆ i' ∈ t, f (i, i')
ht : t.PairwiseDisjoint fun i' ↦ ⨆ i ∈ s, f (i, i')
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
j : ι
j' : ι'
hj : (j, j').1 ∈ s ∧ (j, j').2 ∈ t
h : (i, i') ≠ (j, j')
hij : i ≠ j
⊢ f (j, j') ≤ (fun i ↦ ⨆ i' ∈ t, f (i, i')) (j, j').1

Tactic:
· convert! le_iSup₂ (α := α) i' hi.2; rfl

Goal state after:
case inr.refine_2
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : s.PairwiseDisjoint fun i ↦ ⨆ i' ∈ t, f (i, i')
ht : t.PairwiseDisjoint fun i' ↦ ⨆ i ∈ s, f (i, i')
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
j : ι
j' : ι'
hj : (j, j').1 ∈ s ∧ (j, j').2 ∈ t
h : (i, i') ≠ (j, j')
hij : i ≠ j
⊢ f (j, j') ≤ (fun i ↦ ⨆ i' ∈ t, f (i, i')) (j, j').1
Module: Mathlib.Data.Set.Pairwise.Lattice

Goal state before:
pp: α : Type u_5
ι : Type u_6
s : Set ι
f : ι → Set α
h : s.PairwiseDisjoint f
x : ↑(⋃ i ∈ s, f i)
⊢ ↑((biUnionEqSigmaOfDisjoint h) x).snd = ↑x

Tactic:
simp [biUnionEqSigmaOfDisjoint]

Goal state after: