mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ℕ
IH : ∀ m < n, P (f m)
IH' : ∀ (x : Fin n), P (f ↑x)
⊢ ∀ x ∈ image (fun i ↦ f ↑i) univ, P x

Tactic:
by simp [IH']

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

Goal state before:
pp: case h.inl
P : (α : Type u_4) → [Fintype α] → Prop
hbase : ∀ (α : Type u_4) [inst : Fintype α] [Subsingleton α], P α
hstep :
  ∀ (α : Type u_4) [inst : Fintype α] [Nontrivial α],
    (∀ (β : Type u_4) [inst_2 : Fintype β], card β < card α → P β) → P α
n : ℕ
ih : ∀ m < n, ∀ (α : Type u_4) [inst : Fintype α], card α = m → P α
α : Type u_4
inst✝ : Fintype α
hn : card α = n
hsing : Subsingleton α
⊢ P α

Tactic:
apply hbase

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f : α → α
s : Finset α
hs : Set.MapsTo f ↑s ↑s
hs₀ : s.Nonempty
g : ℕ → Finset α := fun i ↦ image f^[i] s
this : ∀ (i : ℕ), 0 < #(g i)
hg : Antitone g
eq_iff : ∀ (i j : ℕ), #(g i) - 1 = #(g j) - 1 ↔ g i = g j
i j : ℕ
h : i ≤ j
⊢ #(g j) - 1 ≤ #(g i) - 1

Tactic:
gcongr #?_ - 1

Goal state after:
case a
α : Type u_1
inst✝ : DecidableEq α
f : α → α
s : Finset α
hs : Set.MapsTo f ↑s ↑s
hs₀ : s.Nonempty
g : ℕ → Finset α := fun i ↦ image f^[i] s
this : ∀ (i : ℕ), 0 < #(g i)
hg : Antitone g
eq_iff : ∀ (i j : ℕ), #(g i) - 1 = #(g j) - 1 ↔ g i = g j
i j : ℕ
h : i ≤ j
⊢ image f^[j] s ⊆ g i
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case succ.cast
n : ℕ
β : Sort u_2
a : β
q : Fin n → β
b : β
j : Fin n
⊢ snoc q b j.castSucc = snoc (cons a q) b j.castSucc.succ

Tactic:
simp [← castSucc_succ]

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
β : Sort u_2
x : β
p : Fin n → β
⊢ insertNth 0 x p = cons x p

Tactic:
by
  simp [insertNth_zero]

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

Goal state before:
pp: case mp
α : Type u_1
l : List α
x : α
⊢ (∃ f, ∀ (ix : Fin (replicate 2 x).length), (replicate 2 x).get ix = l.get (f ix)) →
    ∃ n m x_1, x = l.get n ∧ x = l.get m

Tactic:
rintro ⟨f, hf⟩
      refine ⟨f ⟨0, by simp⟩, f ⟨1, by simp⟩, f.lt_iff_lt.2 (Nat.zero_lt_one), ?_⟩
      rw [← hf, ← hf]; simp

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Set α
p : Set β → Prop
⊢ (∃ s_1, ↑s_1 ⊆ f '' s ∧ p ↑s_1) ↔ ∃ s_1, ↑s_1 ⊆ s ∧ p (f '' ↑s_1)

Tactic:
Finset.subset_set_image_iff

Goal state after:
α : Type u
β : Type v
f : α → β
s : Set α
p : Set β → Prop
⊢ (∃ s_1, (∃ s', ↑s' ⊆ s ∧ Finset.image f s' = s_1) ∧ p ↑s_1) ↔ ∃ s_1, ↑s_1 ⊆ s ∧ p (f '' ↑s_1)
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: γ : Type u_1
P : γ → Set γ → Prop
h : ∀ (t : Set γ), t.Finite → ∃ c, P c t
this : Nonempty γ
⊢ ∃ u, ∀ (n : ℕ), P (u n) (u '' Iio n)

Tactic:
choose! c hc using h

Goal state after:
γ : Type u_1
P : γ → Set γ → Prop
this : Nonempty γ
c : Set γ → γ
hc : ∀ (t : Set γ), t.Finite → P (c t) t
⊢ ∃ u, ∀ (n : ℕ), P (u n) (u '' Iio n)
Module: Mathlib.Data.Finset.Fold

Goal state before:
pp: α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
s : Finset α
f g : α → β
b₁ b₂ : β
⊢ fold op (op b₁ b₂) (fun x ↦ op (f x) (g x)) s = op (fold op b₁ f s) (fold op b₂ g s)

Tactic:
by
  simp only [fold, fold_distrib]

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

Goal state before:
pp: α : Type u
⊢ ¬univ.Finite ↔ Infinite α

Tactic:
finite_univ_iff,

Goal state after:
α : Type u
⊢ ¬Finite α ↔ Infinite α
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
p : Fin n → Bool
⊢ find? p = if h : ∃ i, p i = true then some (Fin.find (fun x ↦ p x = true) h) else none

Tactic:
split_ifs <;> grind

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
a : α
h : Pairwise R l
ha : a ∈ l.dropLast
⊢ R a (l.getLast ⋯)

Tactic:
rw [← pairwise_reverse] at h

Goal state after:
α : Type u_1
R : α → α → Prop
l : List α
a : α
h : Pairwise (fun b a ↦ R a b) l.reverse
ha : a ∈ l.dropLast
⊢ R a (l.getLast ⋯)
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
n : ℕ
⊢ n ≤ l.length → l.rotate n = drop n l ++ take n l

Tactic:
rw [rotate_eq_rotate']; exact rotate'_eq_drop_append_take

Goal state after:
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: α : Type u_1
a : α
n : ℕ
⊢ n • replicate 1 a = replicate n a

Tactic:
nsmul_replicate,

Goal state after:
α : Type u_1
a : α
n : ℕ
⊢ replicate (n * 1) a = replicate n a
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: G : Type u_7
inst✝ : CommGroup G
a : G
l : List G
⊢ (a :: l).reverse.alternatingProd = (a :: l).alternatingProd ^ (-1) ^ ((a :: l).length + 1)

Tactic:
by
    simp_rw [reverse_cons, alternatingProd_append, alternatingProd_reverse,
      alternatingProd_singleton, alternatingProd_cons, length_reverse, length, pow_succ',
      Int.neg_mul, one_mul, zpow_neg, inv_inv]
    rw [mul_comm, ← div_eq_mul_inv, div_zpow]

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

Goal state before:
pp: α : Type u
l : List α
n : ℕ
x : α
⊢ l.rotate n = [x] ↔ l = [x]

Tactic:
rotate_eq_iff,

Goal state after:
α : Type u
l : List α
n : ℕ
x : α
⊢ l = [x].rotate ([x].length - n % [x].length) ↔ l = [x]
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
n : ℕ
⊢ l.reverse.rotate n = l.reverse.rotate (l.length - (l.length - n % l.length) % l.length)

Tactic:
rotate_eq_iff,

Goal state after:
α : Type u
l : List α
n : ℕ
⊢ l.reverse =
    (l.reverse.rotate (l.length - (l.length - n % l.length) % l.length)).rotate
      ((l.reverse.rotate (l.length - (l.length - n % l.length) % l.length)).length -
        n % (l.reverse.rotate (l.length - (l.length - n % l.length) % l.length)).length)
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_1
β : Type v
s : Multiset α
f : α → Multiset β
f' : α → List β
h' : ∀ (a : α), f a = ↑(f' a)
this : f = fun a ↦ ↑(f' a)
x✝ : Std.Symm fun a b ↦ a.Disjoint b
⊢ ∀ (a : List α),
    (bind (Quot.mk (⇑(List.isSetoid α)) a) f).Nodup ↔
      (∀ (a_1 : α), a_1 ∈ Quot.mk (⇑(List.isSetoid α)) a → (f a_1).Nodup) ∧
        Pairwise (Disjoint on f) (Quot.mk (⇑(List.isSetoid α)) a)

Tactic:
by
    unfold Function.onFun
    simp [this, List.nodup_flatMap, pairwise_coe_iff_pairwise]

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

Goal state before:
pp: case mpr
α : Type u
l : List α
k : ℕ
⊢ l ∈ l.cyclicPermutations.rotate k

Tactic:
mem_rotate

Goal state after:
case mpr
α : Type u
l : List α
k : ℕ
⊢ l ∈ l.cyclicPermutations
Module: Mathlib.Data.List.OffDiag

Goal state before:
pp: α : Type u_1
l : List α
h : l.Nodup
this : DecidableEq α := Classical.decEq α
x y : α
⊢ List.count (x, y) l.offDiag ≤ 1

Tactic:
rw [count_offDiag_eq_mul_sub_ite l x y]

Goal state after:
α : Type u_1
l : List α
h : l.Nodup
this : DecidableEq α := Classical.decEq α
x y : α
⊢ (List.count x l * List.count y l - if x = y then List.count x l else 0) ≤ 1
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: m : ℕ
⊢ (2 * m + 1).choose (m + 1) = (2 * m + 1).choose m

Tactic:
by
  apply choose_symm_of_eq_add
  rw [Nat.add_comm m 1, Nat.add_assoc 1 m m, Nat.add_comm (2 * m) 1, Nat.two_mul m]

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

Goal state before:
pp: n k : ℕ
⊢ n.descFactorial k = k ! * n.choose k

Tactic:
by
  obtain h | h := Nat.lt_or_ge n k
  · rw [descFactorial_eq_zero_iff_lt.2 h, choose_eq_zero_of_lt h, Nat.mul_zero]
  rw [Nat.mul_comm]
  apply Nat.mul_right_cancel (n - k).factorial_pos
  rw [choose_mul_factorial_mul_factorial h, ← factorial_mul_descFactorial h, Nat.mul_comm]

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

Goal state before:
pp: case h₂
ι : Type u_9
α : ι → Type u_10
v : (i : ι) → Set (α i)
hv : (univ.pi v).Nonempty
i : ι
⊢ v i ⊆ (fun x ↦ x i) '' ⋂ k, (fun x ↦ x k) ⁻¹' v k

Tactic:
intro y

Goal state after:
case h₂
ι : Type u_9
α : ι → Type u_10
v : (i : ι) → Set (α i)
hv : (univ.pi v).Nonempty
i : ι
y : α i
⊢ y ∈ v i → y ∈ (fun x ↦ x i) '' ⋂ k, (fun x ↦ x k) ⁻¹' v k
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: case h₂
ι : Type u_9
α : ι → Type u_10
v : (i : ι) → Set (α i)
hv : (univ.pi v).Nonempty
i : ι
y : α i
y_in : y ∈ v i
⊢ y ∈ (fun x ↦ x i) '' ⋂ k, (fun x ↦ x k) ⁻¹' v k

Tactic:
simp only [mem_image, mem_iInter, mem_preimage]

Goal state after:
case h₂
ι : Type u_9
α : ι → Type u_10
v : (i : ι) → Set (α i)
hv : (univ.pi v).Nonempty
i : ι
y : α i
y_in : y ∈ v i
⊢ ∃ x, (∀ (i : ι), x i ∈ v i) ∧ x i = y
Module: Mathlib.Data.Set.Lattice.Image

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

Tactic:
rw [sInter_eq_biInter]

Goal state after:
α : Type u_1
β : Type u_2
S : Set (Set α)
f : α → β
⊢ f '' ⋂ i ∈ S, i ⊆ ⋂ s ∈ S, f '' s
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
inst✝ : Nonempty ι
s : ι → Set α
t : Set β
f : α → β
H : ∀ (i : ι), SurjOn f (s i) t
Hinj : InjOn f (⋃ i, s i)
⊢ SurjOn f (⋂ i, s i) t

Tactic:
intro y

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_5
inst✝ : Nonempty ι
s : ι → Set α
t : Set β
f : α → β
H : ∀ (i : ι), SurjOn f (s i) t
Hinj : InjOn f (⋃ i, s i)
y : β
⊢ y ∈ t → y ∈ f '' ⋂ i, s i
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
ι₁ : Sort u_9
κ₁ : Sort u_10
ι₂ : ι₁ → Sort u_11
k₂ : κ₁ → Sort u_12
f : (i₁ : ι₁) → ι₂ i₁ → Set α
g : (j₁ : κ₁) → k₂ j₁ → Set α
⊢ (⋂ i₁, ⋂ i₂, f i₁ i₂) ∪ ⋂ j₁, ⋂ j₂, g j₁ j₂ = ⋂ i₁, ⋂ i₂, ⋂ j₁, ⋂ j₂, f i₁ i₂ ∪ g j₁ j₂

Tactic:
by
  simp_rw [iInter_union, union_iInter]

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:
rw [sInter_eq_biInter]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
S : Set (Set α)
t : Set β
⊢ image2 f (⋂ i ∈ S, i) t ⊆ ⋂ s ∈ S, image2 f s t
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:
rw [sInter_eq_biInter]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
T : Set (Set β)
⊢ image2 f s (⋂ i ∈ T, i) ⊆ ⋂ t ∈ T, image2 f s t
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: case mp
α : Type u_2
inst✝ : DivisionMonoid α
s : Set α
⊢ IsUnit s → ∃ a, s = {a} ∧ IsUnit a

Tactic:
rintro ⟨u, rfl⟩
    obtain ⟨a, b, ha, hb, h⟩ := Set.mul_eq_one_iff.1 u.mul_inv
    refine ⟨a, ha, ⟨a, b, h, singleton_injective ?_⟩, rfl⟩
    rw [← singleton_mul_singleton, ← ha, ← hb]
    exact u.inv_mul

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
x : G
xH : x ∈ H
n : G
⊢ n ∈ H ↔ x * n ∈ H

Tactic:
H.mul_mem_cancel_left xH

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
x : G
xH : x ∈ H
n : G
⊢ n ∈ H ↔ n ∈ H
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Subsingleton ↥H
⊢ ∀ x ∈ H, x = 1

Tactic:
intro y

Goal state after:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Subsingleton ↥H
y : G
⊢ y ∈ H → y = 1
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: case refine_1
G : Type u_1
inst✝ : Group G
x y : G
hy : y ∈ closure {x}
⊢ ∀ x_1 ∈ {x}, ∃ n, x ^ n = x_1

Tactic:
intro y

Goal state after:
case refine_1
G : Type u_1
inst✝ : Group G
x y✝ : G
hy : y✝ ∈ closure {x}
y : G
⊢ y ∈ {x} → ∃ n, x ^ n = y
Module: Mathlib.Algebra.Group.Subgroup.Map

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ H.subgroupOf K = ⊥.subgroupOf K ↔ H ⊓ K = ⊥

Tactic:
subgroupOf_inj,

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ H ⊓ K = ⊥ ⊓ K ↔ H ⊓ K = ⊥
Module: Mathlib.Algebra.Group.Subgroup.Map

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ H.subgroupOf K = ⊤.subgroupOf K ↔ K ≤ H

Tactic:
subgroupOf_inj,

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ H ⊓ K = ⊤ ⊓ K ↔ K ≤ H
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
f : M →* N
⊢ mker f.mrangeRestrict = mker f

Tactic:
ext x
  change (⟨f x, _⟩ : mrange f) = ⟨1, _⟩ ↔ f x = 1
  simp

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

Goal state before:
pp: M : Type u_1
inst✝¹ : MulOneClass M
S : Submonoid M
inst✝ : Subsingleton ↥S
⊢ ∀ x ∈ S, x = 1

Tactic:
intro y

Goal state after:
M : Type u_1
inst✝¹ : MulOneClass M
S : Submonoid M
inst✝ : Subsingleton ↥S
y : M
⊢ y ∈ S → y = 1
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: motive : ℕ → Sort u
⊢ Function.Injective fun H n ↦ bitCasesOn n H

Tactic:
by
  intro H₁ H₂ h
  ext b n
  simpa only [bitCasesOn_bit] using congr_fun h (bit b n)

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

Goal state before:
pp: n : ℕ
b : Bool
hn : n = 0 → b = true
⊢ (bit b n).bits = b :: n.bits

Tactic:
Nat.bits,

Goal state after:
n : ℕ
b : Bool
hn : n = 0 → b = true
⊢ binaryRec [] (fun b x IH ↦ b :: IH) (bit b n) = b :: n.bits
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: n : ℕ
b : Bool
hn : n = 0 → b = true
⊢ binaryRec [] (fun b x IH ↦ b :: IH) (bit b n) = b :: n.bits

Tactic:
Nat.bits,

Goal state after:
n : ℕ
b : Bool
hn : n = 0 → b = true
⊢ binaryRec [] (fun b x IH ↦ b :: IH) (bit b n) = b :: binaryRec [] (fun b x IH ↦ b :: IH) n
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup G
f : G ≃* N
⊢ map f.toMonoidHom (normalizer ↑H) = normalizer ↑(map f.toMonoidHom H)

Tactic:
by
  ext x
  simp only [mem_normalizer_iff, mem_map_equiv]
  rw [f.toEquiv.forall_congr]
  intro
  simp

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
s : Set N
f : G ≃* N
⊢ normalClosure (⇑f ⁻¹' s) = comap (↑f) (normalClosure s)

Tactic:
have := f.toEquiv.image_symm_eq_preimage s
  simp_all [comap_equiv_eq_map_symm, map_normalClosure s (f.symm : N →* G) f.symm.surjective]

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

Goal state before:
pp: α : 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)
l : List α
hl_nonempty : l ≠ []
hl : ∀ (a : α), a ∈ l → p a
⊢ f l.prod ≤ (map f l).prod

Tactic:
by
  induction l with
  | nil => simp at hl_nonempty
  | cons a l ih =>
    rw [prod_cons, map_cons, prod_cons]
    by_cases hl_empty : l = []
    · simp [hl_empty]
    have hla_restrict : ∀ x, x ∈ l → p x := fun x hx => hl x (mem_cons_of_mem _ hx)
    have hp_sup : p l.prod := prod_induction_nonempty p hp_mul hl_empty hla_restrict
    have hp_a : p a := hl a mem_cons_self
    grw [h_mul a _ hp_a hp_sup, ← ih hl_empty hla_restrict]

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

Goal state before:
pp: M : Type u_3
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedMonoid M
inst✝ : CanonicallyOrderedMul M
l : List M
h : ∀ (x : M), x ∈ l → x = 1
⊢ l.prod = 1

Tactic:
rw [List.eq_replicate_iff.2 ⟨_, h⟩, prod_replicate, one_pow]

Goal state after:
M : Type u_3
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedMonoid M
inst✝ : CanonicallyOrderedMul M
l : List M
h : ∀ (x : M), x ∈ l → x = 1
⊢ ℕ

M : Type u_3
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedMonoid M
inst✝ : CanonicallyOrderedMul M
l : List M
h : ∀ (x : M), x ∈ l → x = 1
⊢ l.length = ?m.52
Module: Mathlib.Algebra.Group.Submonoid.Membership

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

Tactic:
intro y

Goal state after:
case refine_1
M : Type u_1
N : Type u_4
α : Type u_5
inst✝³ : Monoid M
inst✝² : MulAction M N
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ x ∈ s, ∀ (y : N) (z : α), (x • y) • z = x • y • z
x : M
y : N
⊢ ∀ (z : α), (1 • y) • z = 1 • y • z
Module: Mathlib.Algebra.Group.Submonoid.Membership

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

Tactic:
intro y

Goal state after:
case refine_1
M : Type u_1
N : Type u_4
α : Type u_5
inst✝² : Monoid M
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ x ∈ s, ∀ (y : N) (z : α), x • y • z = y • x • z
x : M
y : N
⊢ ∀ (a : α), 1 • y • a = y • 1 • a
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
l : List α
a x b : α
hx : x ∈ l
h : a ≤ x
⊢ a ≤ foldr max b l

Tactic:
by
  induction l with
  | nil => exact absurd hx List.not_mem_nil
  | cons y l IH =>
    simp only [List.foldr]
    obtain rfl | hl := mem_cons.mp hx
    · exact le_max_of_le_left h
    · exact le_max_of_le_right (IH hl)

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∈ t, x < z ∧ z < y
f : α → WithTop α := fun x ↦ {y ∈ t | x < y}.min
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
hxy : x < y
a : α
hat : a ∈ t
hxa : x < a
hay : a < y
b : α
hb : b ∈ {y_1 ∈ t | y < y_1}
⊢ y < b

Tactic:
simpa using (mem_filter.1 hb).2

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

Goal state before:
pp: case nil
α : Type u
⊢ [] <+ [].sublists

Tactic:
simp only [sublists_nil, sublist_cons_self]

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

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

Tactic:
rw [← append_assoc]
      exact (ih _ _ h).append_right _

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

Goal state before:
pp: case mp
α : Type u_1
κ : Sort u_4
r : α → α → Prop
f : κ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) f
⊢ (⋃ n, f n).Pairwise r → ∀ (n : κ), (f n).Pairwise r

Tactic:
intro H n

Goal state after:
case mp
α : Type u_1
κ : Sort u_4
r : α → α → Prop
f : κ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) f
H : (⋃ n, f n).Pairwise r
n : κ
⊢ (f n).Pairwise r
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case cons
α : Type u
h : α
tl : List α
l_ih : flatMap (fun n ↦ sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
⊢ [] :: flatMap (fun a ↦ sublistsLen (a + 1) tl) (range (tl.length + 1)) ++
      map (cons h) (flatMap (fun a ↦ sublistsLen a tl) (range (tl.length + 1))) ~
    tl.sublists' ++ map (cons h) tl.sublists'

Tactic:
rw [← List.singleton_append, ← List.sublistsLen_zero tl]

Goal state after:
case cons
α : Type u
h : α
tl : List α
l_ih : flatMap (fun n ↦ sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
⊢ sublistsLen 0 tl ++ flatMap (fun a ↦ sublistsLen (a + 1) tl) (range (tl.length + 1)) ++
      map (cons h) (flatMap (fun a ↦ sublistsLen a tl) (range (tl.length + 1))) ~
    tl.sublists' ++ map (cons h) tl.sublists'
Module: Mathlib.Data.Set.Pairwise.Lattice

Goal state before:
pp: α : Type u_1
ι : Type u_2
f : ι → Set α
s : Set ι
y : α
h_disjoint : s.PairwiseDisjoint f
hy : y ∈ ⋃ i ∈ s, f i
⊢ ∃! i, i ∈ s ∧ y ∈ f i

Tactic:
by
  refine existsUnique_of_exists_of_unique ?ex ?unique
  · simpa only [mem_iUnion, exists_prop] using hy
  · rintro i j ⟨his, hi⟩ ⟨hjs, hj⟩
    exact h_disjoint.elim his hjs <| not_disjoint_iff.mpr ⟨y, ⟨hi, hj⟩⟩

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

Goal state before:
pp: α : Type u_2
ι : Type u_5
inst✝ : LinearOrder α
s : Finset ι
H : s.Nonempty
f : ι → α
a : α
⊢ ↑a ≤ s.sup (WithBot.some ∘ f) ↔ ∃ b ∈ s, a ≤ f b

Tactic:
Finset.le_sup_iff (WithBot.bot_lt_coe a)

Goal state after:
α : Type u_2
ι : Type u_5
inst✝ : LinearOrder α
s : Finset ι
H : s.Nonempty
f : ι → α
a : α
⊢ (∃ b ∈ s, ↑a ≤ (WithBot.some ∘ f) b) ↔ ∃ b ∈ s, a ≤ f b
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: case mpr
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h : ∃ x ∈ s, sSup ∅ ≤ f x
⊢ (∀ x ∈ s, f x < a) → ⨆ i ∈ s, f i < a

Tactic:
have := hs.ciSup_mem_image _ h
    grind

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

Goal state before:
pp: α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : DecidablePred fun x ↦ x = ⊤
a : α
h : a ≠ ⊤
⊢ subtypeOrderIso.symm a = ↑⟨a, h⟩

Tactic:
rw [OrderIso.symm_apply_eq]

Goal state after:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : DecidablePred fun x ↦ x = ⊤
a : α
h : a ≠ ⊤
⊢ a = subtypeOrderIso ↑⟨a, h⟩
Module: Mathlib.Order.Interval.Set.WithBotTop

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
⊢ some '' Ioi a = Ioo ↑a ⊤

Tactic:
by
  rw [← preimage_coe_Ioi, image_preimage_eq_inter_range, range_coe, Ioi_inter_Iio]

Goal state after:
Module: Mathlib.Order.Interval.Set.WithBotTop

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ some '' Ioc a b = Ioc ↑a ↑b

Tactic:
by
  rw [← preimage_coe_Ioc, image_preimage_eq_inter_range, range_coe,
    inter_eq_self_of_subset_left
      (Subset.trans Ioc_subset_Iic_self <| Iic_subset_Iio.2 <| coe_lt_top b)]

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
t : Set α
a : α
ha : a ∈ t
⊢ t \ {a} ⋖ t

Tactic:
exact sdiff_singleton_covBy ha

Goal state after:
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : DecidableEq α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
⊢ x ∈ {x ∈ finsetIcc a b | a ≠ x} ↔ a < x ∧ x ≤ b

Tactic:
rw [Finset.mem_filter, mem_Icc, and_right_comm, lt_iff_le_and_ne]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a b : ℕ
⊢ Ico 0 (a + b) = Ico 0 a ∪ map (addLeftEmbedding a) (Ico 0 b)

Tactic:
map_eq_image

Goal state after:
a b : ℕ
⊢ Ico 0 (a + b) = Ico 0 a ∪ image (⇑(addLeftEmbedding a)) (Ico 0 b)
Module: Mathlib.GroupTheory.Subgroup.Center

Goal state before:
pp: G : Type u_2
inst✝ : CommGroup G
x : G
⊢ ∀ (g : G), g * x = x * g

Tactic:
intro y

Goal state after:
G : Type u_2
inst✝ : CommGroup G
x y : G
⊢ y * x = x * y