mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
m : Multiset α
t : (a : α) → Multiset (β a)
f : (a : α) → a ∈ m → β a
⊢ f ∈ m.pi t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a

Tactic:
induction m using Multiset.induction_on with
  | empty =>
    have : f = Pi.empty β := funext (fun _ => funext fun h => (notMem_zero _ h).elim)
    simp only [this, pi_zero, mem_singleton, true_iff]
    intro _ h; exact (notMem_zero _ h).elim
  | cons a m ih => ?_
  simp_rw [pi_cons, mem_bind, mem_map, ih]
  constructor
  · rintro ⟨b, hb, f', hf', rfl⟩ a' ha'
    by_cases h : a' = a
    · subst h
      rwa [Pi.cons_same]
    · rw [Pi.cons_ne _ h]
      apply hf'
  · intro hf
    refine ⟨_, hf a (mem_cons_self _ _), _, fun a ha => hf a (mem_cons_of_mem ha), ?_⟩
    rw [Pi.cons_eta]

Goal state after:
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
α : Sort u_3
β : α → Sort u_4
inst✝¹ : Finite α
inst✝ : ∀ (a : α), Finite (β a)
⊢ Finite ((a : α) → β a)

Tactic:
classical
  have := Fintype.ofFinite (PLift α)
  have := fun a => Fintype.ofFinite (PLift (β a))
  exact
    Finite.of_equiv (∀ a : PLift α, PLift (β (Equiv.plift a)))
      (Equiv.piCongr Equiv.plift fun _ => Equiv.plift)

Goal state after:
Module: Mathlib.Algebra.Group.Pi.Lemmas

Goal state before:
pp: I : Type u
f : I → Type v
inst✝¹ : DecidableEq I
inst✝ : (i : I) → MulOneClass (f i)
i j : I
hij : i ≠ j
⊢ ∀ (x : f i) (y : f j), Commute (mulSingle i x) (mulSingle j y)

Tactic:
x

Goal state after:
I : Type u
f : I → Type v
inst✝¹ : DecidableEq I
inst✝ : (i : I) → MulOneClass (f i)
i j : I
hij : i ≠ j
x : f i
⊢ ∀ (y : f j), Commute (mulSingle i x) (mulSingle j y)
Module: Mathlib.Algebra.Group.Submonoid.Basic

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
s : Set M
motive : (x y : M) → x ∈ closure s → y ∈ closure s → Prop
mem : ∀ (x y : M) (hx : x ∈ s) (hy : y ∈ s), motive x y ⋯ ⋯
one_left : ∀ (x : M) (hx : x ∈ closure s), motive 1 x ⋯ hx
one_right : ∀ (x : M) (hx : x ∈ closure s), motive x 1 hx ⋯
mul_left :
  ∀ (x y z : M) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    motive x z hx hz → motive y z hy hz → motive (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : M) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    motive z x hz hx → motive z y hz hy → motive z (x * y) hz ⋯
x y : M
hx : x ∈ closure s
hy : y ∈ closure s
⊢ motive x y hx hy

Tactic:
induction hy using closure_induction with
  | mem z hz => induction hx using closure_induction with
    | mem _ h => exact mem _ _ h hz
    | one => exact one_left _ (subset_closure hz)
    | mul _ _ _ _ h₁ h₂ => exact mul_left _ _ _ _ _ _ h₁ h₂
  | one => exact one_right x hx
  | mul _ _ _ _ h₁ h₂ => exact mul_right _ _ _ _ _ hx h₁ h₂

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H < ⊤ → H < normalizer ↑H ↔ normalizer ↑H = H → H = ⊤

Tactic:
simp only [lt_iff_le_and_ne, le_normalizer, Ne]

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H ≤ ⊤ ∧ ¬H = ⊤ → True ∧ ¬H = normalizer ↑H ↔ normalizer ↑H = H → H = ⊤
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
s : Set β
⊢ Pairwise (Disjoint on fun a ↦ a • s) ↔ ∀ (a : α), (a • s ∩ s).Nonempty → a = 1

Tactic:
simp_rw [Pairwise, disjoint_smul_set_right, ← mul_smul,
    ← not_imp_not (b := _ ≠ _), not_ne_iff, not_disjoint_iff_nonempty_inter]
  exact ⟨fun h a ↦ by simpa using @h a 1,
    fun h i j ne ↦ by simpa [inv_mul_eq_one, eq_comm] using h _ ne⟩

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
⊢ ∀ (a m : α), m ∈ foldl (argAux r) (some a) [] → m ∈ [a]

Tactic:
by simp [eq_comm]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Multiset α
a : α
⊢ ∀ (a_1 : α) (s : Multiset α),
    (s.sup ≤ a ↔ ∀ (b : α), b ∈ s → b ≤ a) → ((a_1 ::ₘ s).sup ≤ a ↔ ∀ (b : α), b ∈ a_1 ::ₘ s → b ≤ a)

Tactic:
by simp +contextual [or_imp, forall_and]

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

Goal state before:
pp: α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ (dedup ?m.26).sup = s₁.sup ⊔ s₂.sup

pp: α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ ∀ (a : α), a ∈ s₁.ndunion s₂ ↔ a ∈ ?m.26

pp: α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ Multiset α

Tactic:
sup_dedup,

Goal state after:
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ sup ?m.35 = s₁.sup ⊔ s₂.sup

α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ Multiset α

α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ ∀ (a : α), a ∈ s₁.ndunion s₂ ↔ a ∈ ?m.35
Module: Mathlib.Data.Multiset.Lattice

Goal state before:
pp: α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ (dedup ?m.26).sup = s₁.sup ⊔ s₂.sup

pp: α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ ∀ (a : α), a ∈ s₁ ∪ s₂ ↔ a ∈ ?m.26

pp: α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ Multiset α

Tactic:
sup_dedup,

Goal state after:
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ sup ?m.35 = s₁.sup ⊔ s₂.sup

α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ Multiset α

α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ ∀ (a : α), a ∈ s₁ ∪ s₂ ↔ a ∈ ?m.35
Module: Mathlib.Data.Multiset.Lattice

Goal state before:
pp: α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ (dedup ?m.23).sup = a ⊔ s.sup

pp: α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ ∀ (a_1 : α), a_1 ∈ ndinsert a s ↔ a_1 ∈ ?m.23

pp: α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ Multiset α

Tactic:
sup_dedup,

Goal state after:
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ sup ?m.32 = a ⊔ s.sup

α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ Multiset α

α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ ∀ (a_1 : α), a_1 ∈ ndinsert a s ↔ a_1 ∈ ?m.32
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case cons
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
a y : α
l : List α
IH : (∀ (x : α), x ∈ l → x ≤ a) → foldr max ⊥ l ≤ a
h : ∀ (x : α), x ∈ y :: l → x ≤ a
⊢ foldr max ⊥ (y :: l) ≤ a

Tactic:
| cons y l IH =>

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

Goal state before:
pp: case cons
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
a x : α
h : a ≤ x
y : α
l : List α
IH : x ∈ l → a ≤ foldr max ⊥ l
hx : x ∈ y :: l
⊢ a ≤ foldr max ⊥ (y :: l)

Tactic:
| cons y l IH =>

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

Goal state before:
pp: case cons
α : Type u_1
inst✝ : LinearOrder α
a x b : α
h : a ≤ x
y : α
l : List α
IH : x ∈ l → a ≤ foldr max b l
hx : x ∈ y :: l
⊢ a ≤ foldr max b (y :: l)

Tactic:
| cons y l IH =>

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

Goal state before:
pp: case inl
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 : a ≤ b
⊢ f (min a b) = f a ⊓ f b

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_left.2 h, inf_eq_left.2 (OrderHomClass.mono f h : f a ≤ f b)]

Goal state after:
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
Module: Mathlib.Order.Hom.BoundedLattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : BooleanAlgebra α
inst✝² : BooleanAlgebra β
inst✝¹ : FunLike F α β
inst✝ : BoundedLatticeHomClass F α β
f : F
a b : α
⊢ f (a ∆ b) = f a ∆ f b

Tactic:
rw [symmDiff, symmDiff, map_sup, map_sdiff', map_sdiff']

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

Goal state before:
pp: α : Type u
a : α
r₁✝ r₁ : List (List α)
l : List α
ih : ∀ (r₂ : List (List α)), sublists'Aux a r₁ r₂ = r₂ ++ map (cons a) r₁
r₂ : List (List α)
⊢ sublists'Aux a (r₁ ++ [l]) r₂ = r₂ ++ (map (cons a) r₁ ++ map (cons a) [l])

Tactic:
map_singleton,

Goal state after:
α : Type u
a : α
r₁✝ r₁ : List (List α)
l : List α
ih : ∀ (r₂ : List (List α)), sublists'Aux a r₁ r₂ = r₂ ++ map (cons a) r₁
r₂ : List (List α)
⊢ sublists'Aux a (r₁ ++ [l]) r₂ = r₂ ++ (map (cons a) r₁ ++ [a :: l])
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: case H.inl
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : DecidableEq ι
f : ι → α
motive : Finset ι → Prop
empty : motive ∅
insert : ∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f x ≤ f a) → motive s → motive (Insert.insert a s)
s : Finset ι
ihs : ∀ s_1 ∈ s, motive (s.erase s_1)
hne : image f s = ∅
⊢ motive s

Tactic:
simp only [image_eq_empty] at hne

Goal state after:
case H.inl
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : DecidableEq ι
f : ι → α
motive : Finset ι → Prop
empty : motive ∅
insert : ∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f x ≤ f a) → motive s → motive (Insert.insert a s)
s : Finset ι
ihs : ∀ s_1 ∈ s, motive (s.erase s_1)
hne : s = ∅
⊢ motive s
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
l : List α
⊢ sublistsLen 1 [] = map (fun x ↦ [x]) [].reverse

Tactic:
sublistsLen_succ_nil,

Goal state after:
α : Type u
l : List α
⊢ [] = map (fun x ↦ [x]) [].reverse
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: case h
α : Type u_2
a✝ : List α
⊢ ((↑(List.range ((↑a✝).card + 1))).bind fun a ↦ ↑(List.map ofList (sublistsLen a a✝))) =
    ↑(List.map ofList a✝.sublists')

Tactic:
coe_bind,

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

Goal state before:
pp: case inl.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' : ι'
hj : (i, j').1 ∈ s ∧ (i, j').2 ∈ t
h : (i, i') ≠ (i, j')
⊢ f (i, i') ≤ (fun i' ↦ ⨆ i ∈ s, f (i, i')) (i, i').2

Tactic:
convert! le_iSup₂ (α := α) i hi.1; rfl

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
s t : Set ι
f : ι → Set α
h : (s ∪ t).PairwiseDisjoint f
i : ι
hi : i ∈ s \ t
a : α
ha : a ∈ f i
⊢ ¬∃ i, ∃ (_ : i ∈ t), a ∈ f i

Tactic:
rintro ⟨j, hj, haj⟩

Goal state after:
α : Type u_1
ι : Type u_2
s t : Set ι
f : ι → Set α
h : (s ∪ t).PairwiseDisjoint f
i : ι
hi : i ∈ s \ t
a : α
ha : a ∈ f i
j : ι
hj : j ∈ t
haj : a ∈ f j
⊢ False
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: case a
α : Type u_1
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
⊢ ∀ (b : Finset α), b ⊆ u ∧ #b = n.succ → id b ⊆ u

Tactic:
rintro x ⟨h, -⟩

Goal state after:
case a
α : Type u_1
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
x : Finset α
h : x ⊆ u
⊢ id x ⊆ u
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: case a
α : Type u_1
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
x : α
hx : x ∈ u
t : Finset α
ht : t ∈ powersetCard n (u.erase x)
⊢ insert x t ∈ powersetCard n.succ (u.erase x) ∪ image (insert x) (powersetCard n (u.erase x))

Tactic:
exact mem_union_right _ (mem_image_of_mem _ ht)

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

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

Tactic:
have h₁ : ∀ m, f m ≤ g n := fun m => hf.forall_le_of_antitone hg h m n

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Set ι
hs : s.Finite
h : ∃ x ∈ s, f x ≤ sInf ∅
⊢ ⨅ i ∈ s, f i ∈ f '' s

Tactic:
lift s to Finset ι using hs
  simp only [Finset.mem_coe] at h
  simpa using Finset.ciInf_mem_image f h

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

Goal state before:
pp: case mp
ι : 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 ∈ s, f x < a

Tactic:
x

Goal state after:
case mp
ι : 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 : ι
⊢ x ∈ s → f x < a
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
ι : Type u_1
s : ι → Set α
a : Set ι
ha : a.Infinite
hs : InjOn s a
⊢ (⋃ x, s ↑x).Infinite

Tactic:
have _ := ha.to_subtype

Goal state after:
α : Type u
ι : Type u_1
s : ι → Set α
a : Set ι
ha : a.Infinite
hs : InjOn s a
x✝ : Infinite ↑a
⊢ (⋃ x, s ↑x).Infinite
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: case mp
ι : 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 ∈ s, a < f x

Tactic:
x

Goal state after:
case mp
ι : 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 : ι
⊢ x ∈ s → a < f x
Module: Mathlib.Order.Interval.Set.WithBotTop

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
⊢ Ici ↑a ∩ Iio ⊤ = Ico ↑a ⊤

Tactic:
Ici_inter_Iio

Goal state after:
α : Type u_1
inst✝ : Preorder α
a : α
⊢ Ico ↑a ⊤ = Ico ↑a ⊤
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
a b : α
f : α ↪o β
hab : a ⩿ b
h : (range ⇑f).OrdConnected
⊢ f a ⩿ f b

Tactic:
by
  refine ⟨f.monotone hab.le, fun c ha hb => ?_⟩
  obtain ⟨c, rfl⟩ := h.out (mem_range_self _) (mem_range_self _) ⟨ha.le, hb.le⟩
  rw [f.lt_iff_lt] at ha hb
  exact hab.2 ha hb

Goal state after:
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝¹ : LE α
inst✝ : IsTrans α LE.le
f : ι → α
s : Set ι
h : (f '' s).Finite
hs : s.Nonempty
⊢ ∃ i, MaximalFor (fun x ↦ x ∈ s) f i

Tactic:
obtain ⟨_, ⟨a, ha, rfl⟩, hmax⟩ := Finite.exists_maximalFor id (f '' s) h (hs.image f)

Goal state after:
ι : Type u_1
α : Type u_2
inst✝¹ : LE α
inst✝ : IsTrans α LE.le
f : ι → α
s : Set ι
h : (f '' s).Finite
hs : s.Nonempty
a : ι
ha : a ∈ s
hmax : ∀ ⦃j : α⦄, (fun x ↦ x ∈ f '' s) j → id (f a) ≤ id j → id j ≤ id (f a)
⊢ ∃ i, MaximalFor (fun x ↦ x ∈ s) f i
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b : α
⊢ Ioc a b = 0 ↔ ¬a < b

Tactic:
rw [Ioc, Finset.val_eq_zero, Finset.Ioc_eq_empty_iff]

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

Goal state before:
pp: b : ℕ
⊢ #(Icc ⊥ b) = b + 1

Tactic:
card_Icc,

Goal state after:
b : ℕ
⊢ b + 1 - ⊥ = b + 1
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: case inl.succ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : ℕ → α
g : ℕ ↪o ℕ
hr : ∀ (n : ℕ), r (f (g n)) (f (g (n + 1)))
m x : ℕ
ih : m < m.succ + x → r (f (g m)) (f (g (m.succ + x)))
mn : m < m.succ + (x + 1)
⊢ r (f (g m)) (f (g (m.succ + (x + 1))))

Tactic:
| succ x ih =>

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

Goal state before:
pp: case succ
n✝ : ℕ
⊢ image (fun j ↦ n✝ + 1 - 1 - j) (range (n✝ + 1)) = range (n✝ + 1)

Tactic:
rw [Finset.range_eq_Ico, Nat.Ico_image_const_sub_eq_Ico (Nat.zero_le _)]

Goal state after:
case succ
n✝ : ℕ
⊢ Ico (n✝ + 1 - 1 + 1 - (n✝ + 1)) (n✝ + 1 - 1 + 1 - 0) = Ico 0 (n✝ + 1)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h : b₁ < b₂
⊢ Ioc a b₁ ⊆ Ioo a b₂

Tactic:
by
  rw [← coe_subset, coe_Ioc, coe_Ioo]
  exact Set.Ioc_subset_Ioo_right h

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

Goal state before:
pp: α : Type u_2
a b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h : b₁ < b₂
⊢ Icc a b₁ ⊆ Ico a b₂

Tactic:
rw [← coe_subset, coe_Icc, coe_Ico]

Goal state after:
α : Type u_2
a b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h : b₁ < b₂
⊢ Set.Icc a b₁ ⊆ Set.Ico a b₂
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
s : Set α
f : (Subrel r fun x ↦ x ∈ s) ↪r fun a b ↦ r a b ∧ a ∈ s ∧ b ∈ s
h : s.WellFoundedOn r
t : Set α
ht : t.Nonempty
⊢ ∃ m ∈ t, ∀ x ∈ t, ¬(r x m ∧ x ∈ s ∧ m ∈ s)

Tactic:
by_cases hst : (s ∩ t).Nonempty

Goal state after:
case pos
α : Type u_2
r : α → α → Prop
s : Set α
f : (Subrel r fun x ↦ x ∈ s) ↪r fun a b ↦ r a b ∧ a ∈ s ∧ b ∈ s
h : s.WellFoundedOn r
t : Set α
ht : t.Nonempty
hst : (s ∩ t).Nonempty
⊢ ∃ m ∈ t, ∀ x ∈ t, ¬(r x m ∧ x ∈ s ∧ m ∈ s)

case neg
α : Type u_2
r : α → α → Prop
s : Set α
f : (Subrel r fun x ↦ x ∈ s) ↪r fun a b ↦ r a b ∧ a ∈ s ∧ b ∈ s
h : s.WellFoundedOn r
t : Set α
ht : t.Nonempty
hst : ¬(s ∩ t).Nonempty
⊢ ∃ m ∈ t, ∀ x ∈ t, ¬(r x m ∧ x ∈ s ∧ m ∈ s)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ Set.Ioo a b ⊆ ↑(Ioc a b)

Tactic:
coe_Ioc

Goal state after:
α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ Set.Ioo a b ⊆ Set.Ioc a b
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
hI : a₂ ≤ b₂
ha : a₂ ≤ a₁
hb : b₁ < b₂
⊢ Icc a₁ b₁ ⊂ Icc a₂ b₂

Tactic:
by
  rw [← coe_ssubset, coe_Icc, coe_Icc]
  exact Set.Icc_ssubset_Icc_right hI ha hb

Goal state after:
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]
  exact Set.Ico_subset_Ico_union_Ico

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : Quotient G α
a b : ↑x.orbit
c : α
h : ⟦a⟧ = ⟦b⟧
hb : b ∈ MulAction.orbit ↥H ⟦a⟧.out
⊢ b ∈ MulAction.orbit (↥H) a

Tactic:
convert! hb using 1

Goal state after:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : Quotient G α
a b : ↑x.orbit
c : α
h : ⟦a⟧ = ⟦b⟧
hb : b ∈ MulAction.orbit ↥H ⟦a⟧.out
⊢ MulAction.orbit (↥H) a = MulAction.orbit ↥H ⟦a⟧.out
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case h
α : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hα : ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ (fun x ↦ (ofLex x).1) '' s) → ∃ g, Monotone (f ∘ ⇑g)
hβ : ∀ (a : α), {y | toLex (a, y) ∈ s}.IsPWO
f : ℕ → Lex (α × β)
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
hg : Monotone fun n ↦ (ofLex f (g n)).1
hhg : ∀ (n : ℕ), (ofLex f (g 0)).1 ≤ (ofLex f (g n)).1
hc : ∀ (n : ℕ), ¬(ofLex f (g 0)).1 < (ofLex f (g n)).1
hhc : ∀ (n : ℕ), (ofLex f (g 0)).1 = (ofLex f (g n)).1
g' : ℕ ↪o ℕ
hg' : Monotone fun n ↦ (ofLex f (g (g' n))).2
⊢ f (g (g' 0)) ≤ f (g (g' 1))

Tactic:
refine Prod.Lex.toLex_le_toLex.mpr <| .inr ⟨?_, ?_⟩

Goal state after:
case h.refine_1
α : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hα : ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ (fun x ↦ (ofLex x).1) '' s) → ∃ g, Monotone (f ∘ ⇑g)
hβ : ∀ (a : α), {y | toLex (a, y) ∈ s}.IsPWO
f : ℕ → Lex (α × β)
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
hg : Monotone fun n ↦ (ofLex f (g n)).1
hhg : ∀ (n : ℕ), (ofLex f (g 0)).1 ≤ (ofLex f (g n)).1
hc : ∀ (n : ℕ), ¬(ofLex f (g 0)).1 < (ofLex f (g n)).1
hhc : ∀ (n : ℕ), (ofLex f (g 0)).1 = (ofLex f (g n)).1
g' : ℕ ↪o ℕ
hg' : Monotone fun n ↦ (ofLex f (g (g' n))).2
⊢ (f (g (g' 0))).1 = (f (g (g' 1))).1

case h.refine_2
α : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hα : ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ (fun x ↦ (ofLex x).1) '' s) → ∃ g, Monotone (f ∘ ⇑g)
hβ : ∀ (a : α), {y | toLex (a, y) ∈ s}.IsPWO
f : ℕ → Lex (α × β)
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
hg : Monotone fun n ↦ (ofLex f (g n)).1
hhg : ∀ (n : ℕ), (ofLex f (g 0)).1 ≤ (ofLex f (g n)).1
hc : ∀ (n : ℕ), ¬(ofLex f (g 0)).1 < (ofLex f (g n)).1
hhc : ∀ (n : ℕ), (ofLex f (g 0)).1 = (ofLex f (g n)).1
g' : ℕ ↪o ℕ
hg' : Monotone fun n ↦ (ofLex f (g (g' n))).2
⊢ (f (g (g' 0))).2 ≤ (f (g (g' 1))).2
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: α : Type u_3
inst✝¹ : Monoid α
inst✝ : DecidableEq α
s : Multiset α
a : α
h : a ∈ s
comm : {x | x ∈ s}.Pairwise Commute
comm' : ∀ x ∈ {x | x ∈ s.erase a}, ∀ x_1 ∈ {x | x ∈ s.erase a}, x ≠ x_1 → Commute x x_1
⊢ ∀ b ∈ s.erase a, Commute a b

Tactic:
intro b hb

Goal state after:
α : Type u_3
inst✝¹ : Monoid α
inst✝ : DecidableEq α
s : Multiset α
a : α
h : a ∈ s
comm : {x | x ∈ s}.Pairwise Commute
comm' : ∀ x ∈ {x | x ∈ s.erase a}, ∀ x_1 ∈ {x | x ∈ s.erase a}, x ≠ x_1 → Commute x x_1
b : α
hb : b ∈ s.erase a
⊢ Commute a b
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
L1 L2 : List (α × Bool)
x : α
b : Bool
⊢ (L1 ++ L2).length + 2 = (L1 ++ (x, b) :: (x, !b) :: L2).length

Tactic:
by rw [List.length_append, List.length_append]; rfl

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
L : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
h : (x1, b1) ≠ (x2, b2)
⊢ Red [(x1, !b1), (x2, b2)] L ↔ L = [(x1, !b1), (x2, b2)]

Tactic:
by
  apply reflTransGen_iff_eq
  generalize eq : [(x1, not b1), (x2, b2)] = L'
  intro L h'
  cases h'
  simp only [List.cons_eq_append_iff, List.cons.injEq, Prod.mk.injEq, and_false,
    List.nil_eq_append_iff, exists_const, or_self, or_false, List.cons_ne_nil] at eq
  rcases eq with ⟨rfl, ⟨rfl, rfl⟩, ⟨rfl, rfl⟩, rfl⟩
  simp at h

Goal state after: