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

Goal state before:
pp: ι : Type u_5
inst✝ : DecidableEq ι
α : ι → Type u_4
s t : Finset ι
h : Disjoint s t
f : (i : ↥s) → α ↑i
g : (i : ↥t) → α ↑i
i : ι
hi : i ∈ t
hi' : i ∈ s ∪ t
⊢ ({ toFun := fun f ↦ (fun i ↦ f (Sum.inl i), fun i' ↦ f (Sum.inr i')), invFun := fun g t_1 ↦ Sum.rec g.1 g.2 t_1,
              left_inv := ⋯, right_inv := ⋯ }.symm.trans
        { toFun := fun f x ↦ f ((Finset.union s t h).symm.symm x),
            invFun := fun f x ↦ ⋯ ▸ f ((Finset.union s t h).symm x), left_inv := ⋯, right_inv := ⋯ }.symm)
      (f, g) ⟨i, hi'⟩ =
    g ⟨i, hi⟩

Tactic:
trans_apply,

Goal state after:
ι : Type u_5
inst✝ : DecidableEq ι
α : ι → Type u_4
s t : Finset ι
h : Disjoint s t
f : (i : ↥s) → α ↑i
g : (i : ↥t) → α ↑i
i : ι
hi : i ∈ t
hi' : i ∈ s ∪ t
⊢ { toFun := fun f x ↦ f ((Finset.union s t h).symm.symm x), invFun := fun f x ↦ ⋯ ▸ f ((Finset.union s t h).symm x),
          left_inv := ⋯, right_inv := ⋯ }.symm
      ({ toFun := fun f ↦ (fun i ↦ f (Sum.inl i), fun i' ↦ f (Sum.inr i')), invFun := fun g t_1 ↦ Sum.rec g.1 g.2 t_1,
            left_inv := ⋯, right_inv := ⋯ }.symm
        (f, g))
      ⟨i, hi'⟩ =
    g ⟨i, hi⟩
Module: Mathlib.Data.Fin.Rev

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
h : i ≠ 0
h' : i.rev ≠ last n
⊢ (i.pred h).rev = i.rev.castPred h'

Tactic:
← castSucc_inj,

Goal state after:
n : ℕ
i : Fin (n + 1)
h : i ≠ 0
h' : i.rev ≠ last n
⊢ (i.pred h).rev.castSucc = (i.rev.castPred h').castSucc
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n : ℕ
u v : Fin n
⊢ ↑↑(u - v) = if v ≤ u then ↑↑u - ↑↑v else ↑↑u - ↑↑v + ↑n

Tactic:
Fin.sub_def

Goal state after:
n : ℕ
u v : Fin n
⊢ ↑↑⟨(n - ↑v + ↑u) % n, ⋯⟩ = if v ≤ u then ↑↑u - ↑↑v else ↑↑u - ↑↑v + ↑n
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ succ 0 = 1

Tactic:
by
  cases n
  · exact (NeZero.ne 0 rfl).elim
  · rfl

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ succ 1 = 2

Tactic:
by
  cases n
  · exact (NeZero.ne 0 rfl).elim
  · rfl

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

Goal state before:
pp: n : ℕ
h : ¬last (n + 1) = 0
⊢ (last n).succ.pred ⋯ = last n

Tactic:
pred_succ

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

Goal state before:
pp: α : Type u
m n : ℕ
a : Fin m → α
b : Fin n → α
⊢ ofFn (Fin.append a b) = ofFn a ++ ofFn b

Tactic:
ofFn_add

Goal state after:
α : Type u
m n : ℕ
a : Fin m → α
b : Fin n → α
⊢ ((ofFn fun i ↦ Fin.append a b (Fin.castLE ⋯ i)) ++ ofFn fun i ↦ Fin.append a b (Fin.natAdd m i)) = ofFn a ++ ofFn b
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
a : Fin (n + 2)
b : Fin (n + 1)
ha : a ≠ last (n + 1)
⊢ a.succAbove b = last (n + 1) ↔ b = last n

Tactic:
← succAbove_ne_last_last ha,

Goal state after:
n : ℕ
a : Fin (n + 2)
b : Fin (n + 1)
ha : a ≠ last (n + 1)
⊢ a.succAbove b = a.succAbove (last n) ↔ b = last n
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
p i : Fin n
h : p ≤ i
⊢ i.succ.pred ⋯ = i

Tactic:
pred_succ

Goal state after:
n : ℕ
p i : Fin n
h : p ≤ i
⊢ i = i
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ #s = 1 ↔ ∃! a, a ∈ s

Tactic:
by
  simp [card_eq_one, Finset.singleton_iff_unique_mem]

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ 1 < #s ↔ ∃ a ∈ s, ∃ b ∈ s, a ≠ b

Tactic:
by
  contrapose!; exact card_le_one

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

Goal state before:
pp: case inr
n : ℕ
i : Fin (n + 1)
j : Fin n
h : i ≤ j.castSucc
⊢ j.succ.pred ⋯ = j

pp: case inr.h
n : ℕ
i : Fin (n + 1)
j : Fin n
h : i ≤ j.castSucc
⊢ (i.castPred ⋯).castSucc < j.succ

Tactic:
pred_succ

Goal state after:
case inr
n : ℕ
i : Fin (n + 1)
j : Fin n
h : i ≤ j.castSucc
⊢ j = j

case inr.h
n : ℕ
i : Fin (n + 1)
j : Fin n
h : i ≤ j.castSucc
⊢ (i.castPred ⋯).castSucc < j.succ
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case refine_2
α : Sort u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
i : Fin n
⊢ append x₀ x (natAdd 1 i) = (cons (x₀ 0) x ∘ Fin.cast ⋯) (natAdd 1 i)

Tactic:
rw [Fin.append_right, Function.comp_apply, Fin.cast_natAdd, eq_comm, Fin.addNat_one]

Goal state after:
case refine_2
α : Sort u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
i : Fin n
⊢ cons (x₀ 0) x i.succ = x i
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: m n : ℕ
α : Sort u_1
xs : Fin m → α
ys : Fin n → α
finSumFinEquiv : Fin m ⊕ Fin n ≃ Fin (m + n) :=
  { toFun := Sum.elim (castAdd n) (natAdd m), invFun := fun i ↦ addCases Sum.inl Sum.inr i, left_inv := ⋯,
    right_inv := ⋯ }
⊢ Injective (append xs ys) ↔ Injective (Sum.elim xs ys)

Tactic:
← append_comp_sumElim,

Goal state after:
m n : ℕ
α : Sort u_1
xs : Fin m → α
ys : Fin n → α
finSumFinEquiv : Fin m ⊕ Fin n ≃ Fin (m + n) :=
  { toFun := Sum.elim (castAdd n) (natAdd m), invFun := fun i ↦ addCases Sum.inl Sum.inr i, left_inv := ⋯,
    right_inv := ⋯ }
⊢ Injective (append xs ys) ↔ Injective (append xs ys ∘ Sum.elim (castAdd n) (natAdd m))
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)
i : ℕ
⊢ g (i + 1) ⊆ g i

Tactic:
g,

Goal state after:
α : 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)
i : ℕ
⊢ image f^[i + 1] s ⊆ image f^[i] s
Module: Mathlib.Data.Fintype.EquivFin

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type ?u.8
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ Trunc (α ≃ Fin univ.val.card)

Tactic:
exact
    Quot.recOnSubsingleton
      (motive := fun s : Multiset α =>
        (∀ x : α, x ∈ s) → s.Nodup → Trunc (α ≃ Fin (Multiset.card s)))
      univ.val
      (fun l (h : ∀ x : α, x ∈ l) (nd : l.Nodup) => Trunc.mk (nd.getEquivOfForallMemList _ h).symm)
      mem_univ_val univ.2

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

Goal state before:
pp: case h.h₂
α : Type u_1
β : Type u_2
inst✝ : Fintype α
s : Finset β
hsn : Fintype.card α = #s
f : α ↪ β
hf : Set.range ⇑f ⊆ ↑s
⊢ #s ≤ #(map f univ)

Tactic:
simp [← hsn]

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

Goal state before:
pp: case mpr.refine_1
α : Type u_1
l l' : List α
f : Fin l.length ↪o Fin l'.length
hf : ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)
i j : ℕ
h : i < j
⊢ (if hi : i < l.length then ↑(f ⟨i, hi⟩) else i + l'.length) <
    if hi : j < l.length then ↑(f ⟨j, hi⟩) else j + l'.length

Tactic:
split_ifs with hi hj hj

Goal state after:
case pos
α : Type u_1
l l' : List α
f : Fin l.length ↪o Fin l'.length
hf : ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)
i j : ℕ
h : i < j
hi : i < l.length
hj : j < l.length
⊢ ↑(f ⟨i, hi⟩) < ↑(f ⟨j, hj⟩)

case neg
α : Type u_1
l l' : List α
f : Fin l.length ↪o Fin l'.length
hf : ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)
i j : ℕ
h : i < j
hi : i < l.length
hj : ¬j < l.length
⊢ ↑(f ⟨i, hi⟩) < j + l'.length

case pos
α : Type u_1
l l' : List α
f : Fin l.length ↪o Fin l'.length
hf : ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)
i j : ℕ
h : i < j
hi : ¬i < l.length
hj : j < l.length
⊢ i + l'.length < ↑(f ⟨j, hj⟩)

case neg
α : Type u_1
l l' : List α
f : Fin l.length ↪o Fin l'.length
hf : ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)
i j : ℕ
h : i < j
hi : ¬i < l.length
hj : ¬j < l.length
⊢ i + l'.length < j + l'.length
Module: Mathlib.Data.Finset.Fold

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
b : β
s✝ : Finset α
c : β
h : op c (op b c) = op b c
x : α
s : Finset α
hx : x ∉ s
IH : ∀ [hd : Decidable (s = ∅)], fold op b (fun x ↦ c) s = if s = ∅ then b else op b c
hd : Decidable (insert x s = ∅)
h✝ : s = ∅
⊢ op c b = op b c

Tactic:
rw [hc.comm]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Infinite α
f : α → β
hi : Injective f
⊢ (f '' univ).Infinite

Tactic:
infinite_image_iff hi.injOn

Goal state after:
α : Type u
β : Type v
inst✝ : Infinite α
f : α → β
hi : Injective f
⊢ univ.Infinite
Module: Mathlib.Data.List.Pairwise

Goal state before:
pp: case refine_1
α : Type u_3
l : List α
R : α → α → Prop
h : ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length), i < j → R l[i] l[j]
l' : List α
hne : 1 < l'.length
x✝ : l' <:+: l
l₁ l₂ : List α
hl : l₁ ++ l' ++ l₂ = l
⊢ R (l'.head ⋯) (l'.getLast ⋯)

Tactic:
grind [getElem_append_left', getElem_append_right']

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:
refine ⟨fun h => ?_, prod_isUnit⟩

Goal state after:
M : Type u_8
inst✝ : CommMonoid M
L : List M
h : IsUnit L.prod
⊢ ∀ (m : M), m ∈ L → IsUnit m
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_1
σ : α → Type u_4
a : α
s : Multiset α
t : (a : α) → Multiset (σ a)
⊢ (a ::ₘ s).sigma t = map (Sigma.mk a) (t a) + s.sigma t

Tactic:
simp [Multiset.sigma]

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

Goal state before:
pp: α : Type u_1
σ : α → Type u_4
s t : Multiset α
u : (a : α) → Multiset (σ a)
⊢ (s + t).sigma u = s.sigma u + t.sigma u

Tactic:
simp [Multiset.sigma]

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

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

Tactic:
Nat.add_mul _ _ (k + 1 + 1),

Goal state after:
n k : ℕ
⊢ (n + 1 + 1) * (n + 1).choose (k + 1) = (n + 1).choose (k + 1) * (k + 1 + 1) + (n + 1).choose (k + 1 + 1) * (k + 1 + 1)
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: case cons
α : 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
⊢ (f ∈ (t a).bind fun b ↦ map (Pi.cons m a b) (m.pi t)) ↔ ∀ (a_1 : α) (h : a_1 ∈ a ::ₘ m), f a_1 h ∈ t a_1

Tactic:
mem_bind,

Goal state after:
case cons
α : 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
⊢ (∃ a_1, a_1 ∈ t a ∧ f ∈ map (Pi.cons m a a_1) (m.pi t)) ↔ ∀ (a_1 : α) (h : a_1 ∈ a ::ₘ m), f a_1 h ∈ t a_1
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

pp: case mpr
α : Type u_2
inst✝ : DivisionMonoid α
s : Set α
⊢ (∃ a, s = {a} ∧ IsUnit a) → IsUnit s

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:
case mpr
α : Type u_2
inst✝ : DivisionMonoid α
s : Set α
⊢ (∃ a, s = {a} ∧ IsUnit a) → IsUnit s
Module: Mathlib.Algebra.Group.Subgroup.Defs

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
A : Type u_2
inst✝ : AddGroup A
H K✝ K : Subgroup G
s : Set G
hs : s = ↑K
x✝ : G
hx : x✝ ∈ s
⊢ x✝⁻¹ ∈ s

Tactic:
by simpa [hs] using hx

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

Goal state before:
pp: F : Type u_3
G : Type u_4
H : Type u_5
S : Type u_6
inst✝⁷ : Group G
inst✝⁶ : Group H
inst✝⁵ : FunLike F G H
inst✝⁴ : MonoidHomClass F G H
f : F
inst✝³ : SetLike S G
inst✝² : OneMemClass S G
inst✝¹ : MulMemClass S G
inst✝ : InvMemClass S G
s : S
h : InjOn ⇑f ↑s
a : G
ha : a ∈ s
ha' : f a = 1
⊢ a = 1

Tactic:
refine h ha (one_mem s) ?_

Goal state after:
F : Type u_3
G : Type u_4
H : Type u_5
S : Type u_6
inst✝⁷ : Group G
inst✝⁶ : Group H
inst✝⁵ : FunLike F G H
inst✝⁴ : MonoidHomClass F G H
f : F
inst✝³ : SetLike S G
inst✝² : OneMemClass S G
inst✝¹ : MulMemClass S G
inst✝ : InvMemClass S G
s : S
h : InjOn ⇑f ↑s
a : G
ha : a ∈ s
ha' : f a = 1
⊢ f a = f 1
Module: Mathlib.Algebra.Group.Subgroup.Map

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
h : Surjective ⇑f
x : N
a✝ : x ∈ ⊤
⊢ x ∈ map f ⊤

Tactic:
obtain ⟨y, hy⟩ := h x

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
h : Surjective ⇑f
x : N
a✝ : x ∈ ⊤
y : G
hy : f y = x
⊢ x ∈ map f ⊤
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.Subgroup.Lattice

Goal state before:
pp: C : Type u_2
inst✝ : CommGroup C
x y z : C
⊢ z ∈ closure {x, y} ↔ ∃ m n, x ^ m * y ^ n = z

Tactic:
by
  rw [← Set.singleton_union, Subgroup.closure_union, mem_sup]
  simp_rw [mem_closure_singleton, exists_exists_eq_and]

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H : Subgroup G
x : Gᵐᵒᵖ
⊢ (∀ (n : G), n * MulOpposite.unop x ∈ H ↔ MulOpposite.unop x * n ∈ H) ↔ x ∈ normalizer ↑H.op

Tactic:
mem_normalizer_iff'

Goal state after:
G : Type u_2
inst✝ : Group G
H : Subgroup G
x : Gᵐᵒᵖ
⊢ (∀ (n : G), n * MulOpposite.unop x ∈ H ↔ MulOpposite.unop x * n ∈ H) ↔ ∀ (n : Gᵐᵒᵖ), n * x ∈ H.op ↔ x * n ∈ H.op
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: a₁ a₂ b : ℕ
h : a₁ < a₂
⊢ pair a₁ b < pair a₂ b

Tactic:
by_cases h₁ : a₁ < b <;> simp only [pair, h₁, ↓reduceIte, Nat.add_assoc]

Goal state after:
case pos
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
⊢ b * b + a₁ < if a₂ < b then b * b + a₂ else a₂ * a₂ + (a₂ + b)

case neg
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : ¬a₁ < b
⊢ a₁ * a₁ + (a₁ + b) < if a₂ < b then b * b + a₂ else a₂ * a₂ + (a₂ + b)
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Group α
s t : Set α
a b : α
⊢ ∃ z, a • s ∩ b • t ⊆ z • (s⁻¹ * s ∩ (t⁻¹ * t))

Tactic:
obtain hAB | ⟨z, hzA, hzB⟩ := (a • s ∩ b • t).eq_empty_or_nonempty

Goal state after:
case inl
α : Type u_2
inst✝ : Group α
s t : Set α
a b : α
hAB : a • s ∩ b • t = ∅
⊢ ∃ z, a • s ∩ b • t ⊆ z • (s⁻¹ * s ∩ (t⁻¹ * t))

case inr
α : Type u_2
inst✝ : Group α
s t : Set α
a b z : α
hzA : z ∈ a • s
hzB : z ∈ b • t
⊢ ∃ z, a • s ∩ b • t ⊆ z • (s⁻¹ * s ∩ (t⁻¹ * t))
Module: Mathlib.Algebra.FreeMonoid.Basic

Goal state before:
pp: α : Type u_1
a : FreeMonoid α
⊢ a.reverse.reverse = a

Tactic:
by
  apply List.reverse_reverse

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝⁵ : Monoid M
inst✝⁴ : LinearOrder M
inst✝³ : MulLeftStrictMono M
inst✝² : MulLeftMono M
inst✝¹ : MulRightStrictMono M
inst✝ : MulRightMono M
l : List ι
hl : l ≠ []
f g : ι → M
h : ∀ (x : ι), x ∈ l → g x < f x
⊢ (map g l).prod < (map f l).prod

Tactic:
exact prod_lt_prod_of_ne_nil hl _ _ h

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

Goal state before:
pp: M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Preorder M
inst✝ : IsOrderedMonoid M
l : List M
hl₁ : ∀ (x : M), x ∈ l → 1 ≤ x
⊢ ∀ (x : M), x ∈ l → x ≤ l.prod

Tactic:
induction l
  · simp
  simp_rw [prod_cons, forall_mem_cons] at hl₁ ⊢
  constructor
  case cons.left => exact le_mul_of_one_le_right' (one_le_prod_of_one_le hl₁.2)
  case cons.right hd tl ih => exact fun x H => le_mul_of_one_le_of_le hl₁.1 (ih hl₁.right x H)

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

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

Tactic:
refine Exists.elim (?_ : ∃ Hx, motive x Hx) fun (hx : x ∈ ⨆ i, S i) (hc : motive x hx) => hc

Goal state after:
M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
motive : (x : M) → x ∈ ⨆ i, S i → Prop
mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), motive x ⋯
one : motive 1 ⋯
mul : ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), motive x hx → motive y hy → motive (x * y) ⋯
x : M
hx : x ∈ ⨆ i, S i
⊢ ∃ (Hx : x ∈ ⨆ i, S i), motive x Hx
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: 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
⊢ IsScalarTower M N α

Tactic:
refine ⟨fun x => Submonoid.induction_of_closure_eq_top_left htop x ?_ ?_⟩
  · intro y z
    rw [one_smul, one_smul]
  · clear x
    intro x hx x' hx' y z
    rw [mul_smul, mul_smul, hs x hx, hx']

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

Goal state before:
pp: α : Type u
l init tail : List α
⊢ (init, tail) ∈ l.inits.zip l.tails ↔ init ++ tail = l

Tactic:
by
  induction l generalizing init tail <;> simp_rw [tails, inits, zip_cons_cons]
  case nil => simp
  case cons hd tl ih =>
    constructor <;> rw [mem_cons, zip_map_left, mem_map, Prod.exists]
    · rintro (⟨rfl, rfl⟩ | ⟨_, _, h, rfl, rfl⟩)
      · simp
      · simp [ih.mp h]
    · rcases init with - | ⟨hd', tl'⟩
      · simp
      · intro h
        right
        use tl', tail
        simp_all

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

Goal state before:
pp: α : Type u
β : Type v
l : List α
n : ℕ
f : List α → β
r : List β
⊢ sublistsLenAux n l f r = map f (sublistsLen n l) ++ r

Tactic:
sublistsLen,

Goal state after:
α : Type u
β : Type v
l : List α
n : ℕ
f : List α → β
r : List β
⊢ sublistsLenAux n l f r = map f (sublistsLenAux n l id []) ++ r
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
n : ℕ
a : α
l : List α
⊢ sublistsLen (n + 1) (a :: l) = sublistsLen (n + 1) l ++ map (cons a) (sublistsLen n l)

Tactic:
sublistsLen,

Goal state after:
α : Type u
n : ℕ
a : α
l : List α
⊢ sublistsLenAux (n + 1) (a :: l) id [] = sublistsLen (n + 1) l ++ map (cons a) (sublistsLen n l)
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: α : Type u_1
s t : Multiset α
le : s ≤ t
l₁✝ l₂✝ : List α
hsub : l₁✝ <+ l₂✝
⊢ (↑l₁✝).powerset ≤ (↑l₂✝).powerset

Tactic:
by
      rw [powerset_coe', powerset_coe', coe_le]
      apply Sublist.subperm
      apply Sublist.map
      exact Sublist.sublists' hsub

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

Goal state before:
pp: case insert
α : Type u_7
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Set α
hs : s.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
a : α
r : Finset α
a✝ : a ∉ r
ih : (∀ x ∈ r, ∃ y ∈ s, x ≤ y) → ∃ x ∈ s, r.sup id ≤ x
h : ∀ x ∈ insert a r, ∃ y ∈ s, x ≤ y
incs : ↑r ⊆ ↑(insert a r)
⊢ ∃ x ∈ s, (insert a r).sup id ≤ x

Tactic:
obtain ⟨x, ⟨hxs, hsx_sup⟩⟩ := ih fun x hx => h x <| incs hx

Goal state after:
case insert
α : Type u_7
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Set α
hs : s.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
a : α
r : Finset α
a✝ : a ∉ r
ih : (∀ x ∈ r, ∃ y ∈ s, x ≤ y) → ∃ x ∈ s, r.sup id ≤ x
h : ∀ x ∈ insert a r, ∃ y ∈ s, x ≤ y
incs : ↑r ⊆ ↑(insert a r)
x : α
hxs : x ∈ s
hsx_sup : r.sup id ≤ x
⊢ ∃ x ∈ s, (insert a r).sup id ≤ x
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case insert
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s✝ : Finset ι
f : ι → α
a : ι
s : Finset ι
a✝ : a ∉ s
h : s.Nonempty → s.sup f ∈ f '' ↑s
hs : (insert a s).Nonempty
⊢ max (f a) (s.sup f) ∈ f '' ↑(insert a s)

Tactic:
cases s.eq_empty_or_nonempty with
    | inl hs => simp [hs]
    | inr hs =>
      simp only [Finset.coe_insert]
      rcases le_total (f a) (s.sup f) with (ha | ha)
      · rw [sup_eq_right.mpr ha]
        exact Set.image_mono (Set.subset_insert a s) (h hs)
      · rw [sup_eq_left.mpr ha]
        apply Set.mem_image_of_mem _ (Set.mem_insert a ↑s)

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

Goal state before:
pp: case h₁
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompletePartialOrderSup α
p : ι → Prop
f : Subtype p → α
hp : ∀ (i : ι), p i
⊢ (range fun i ↦ f ⟨i, ⋯⟩) ⊆ range f

pp: case h₂
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompletePartialOrderSup α
p : ι → Prop
f : Subtype p → α
hp : ∀ (i : ι), p i
⊢ range f ⊆ range fun i ↦ f ⟨i, ⋯⟩

Tactic:
· rintro - ⟨i, rfl⟩
    simp

Goal state after:
case h₂
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompletePartialOrderSup α
p : ι → Prop
f : Subtype p → α
hp : ∀ (i : ι), p i
⊢ range f ⊆ range fun i ↦ f ⟨i, ⋯⟩
Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed

Goal state before:
pp: case h₂
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompletePartialOrderSup α
p : ι → Prop
f : Subtype p → α
hp : ∀ (i : ι), p i
⊢ range f ⊆ range fun i ↦ f ⟨i, ⋯⟩

Tactic:
· rintro - ⟨i, rfl⟩
    simp

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

Goal state before:
pp: α : Type u
β : Type v
f : β → Set α
s : Set β
hs : s.PairwiseDisjoint f
⊢ Pairwise fun i j ↦ Disjoint (⋃ (_ : i ∈ s), f i) (⋃ (_ : j ∈ s), f j)

Tactic:
aesop (add unfold safe [Pairwise, PairwiseDisjoint, Set.Pairwise])

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, f x ≤ sInf ∅
⊢ ⨅ i ∈ s, f i ∈ image f s

Tactic:
rw [ciInf_eq_min'_image _ h]
  exact min'_mem (image f s) _

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

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

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

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

Goal state before:
pp: case inr
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
gt : iSup f < sSup ∅
⊢ ⨆ i, ⨆ (h : p i), f ⟨i, h⟩ = max (iSup f) (sSup ∅)

Tactic:
have ⟨i, hi⟩ := not_forall.mp hp

Goal state after:
case inr
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
gt : iSup f < sSup ∅
i : ι
hi : ¬p i
⊢ ⨆ i, ⨆ (h : p i), f ⟨i, h⟩ = max (iSup f) (sSup ∅)
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ a₂ : α
b : β
h : ∀ ⦃c : α⦄, a₁ < c → ¬c < a₂
c : α × β
h₁ : (a₁, b) < c
h₂ : c < (a₂, b)
⊢ False

Tactic:
have : c.2 = b := h₂.le.2.antisymm h₁.le.2

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ a₂ : α
b : β
h : ∀ ⦃c : α⦄, a₁ < c → ¬c < a₂
c : α × β
h₁ : (a₁, b) < c
h₂ : c < (a₂, b)
this : c.2 = b
⊢ False
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: case inl
α : Type u_2
inst✝ : LinearOrder α
hs : ∅.Finite
hs' : IsCofinal ∅
⊢ ∃ t, t.Subsingleton ∧ IsCofinal t

Tactic:
use ∅

Goal state after:
case h
α : Type u_2
inst✝ : LinearOrder α
hs : ∅.Finite
hs' : IsCofinal ∅
⊢ ∅.Subsingleton ∧ IsCofinal ∅
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
β : Type u_3
a : α
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
f : α → β
ha : a ∈ s
hf : ∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)
h : Minimal (fun x ↦ x ∈ f '' s) (f a)
y : α
hys : (fun x ↦ x ∈ s) y
⊢ f y ≤ f a → f a ≤ f y

Tactic:
exact h.le_of_le (mem_image_of_mem f hys)

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
β : Type u_3
a : α
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
f : α → β
ha : a ∈ s
hf : ∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)
⊢ Minimal (fun x ↦ x ∈ f '' s) (f a) ↔ Minimal (fun x ↦ x ∈ s) a

Tactic:
refine ⟨fun h ↦ ⟨ha, fun y hys ↦ ?_⟩, minimal_mem_image_monotone hf⟩
  rw [← hf ha hys, ← hf hys ha]
  exact h.le_of_le (mem_image_of_mem f hys)

Goal state after: