mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Idempotent

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
n✝ : ℕ
h : IsIdempotentElem a
n : ℕ
x✝ : IsIdempotentElem (a ^ n)
⊢ a ^ (n.succ * 2) = (a ^ 2) ^ n.succ

Tactic:
← pow_mul'

Goal state after:
M : Type u_1
inst✝ : Monoid M
a : M
n✝ : ℕ
h : IsIdempotentElem a
n : ℕ
x✝ : IsIdempotentElem (a ^ n)
⊢ a ^ (n.succ * 2) = a ^ (n.succ * 2)
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝⁵ : Monoid M
inst✝⁴ : Preorder M
inst✝³ : MulLeftStrictMono M
inst✝² : MulLeftMono M
inst✝¹ : MulRightStrictMono M
inst✝ : MulRightMono M
l : List ι
f g : ι → M
h₁ : ∀ (i : ι), i ∈ l → f i ≤ g i
h₂ : ∃ i, i ∈ l ∧ f i < g i
⊢ (map f l).prod < (map g l).prod

Tactic:
induction l with

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
hH₁ : H₁.Normal
hH₂ : H₂.Normal
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
⊢ Commute x y

Tactic:
suffices x * y * x⁻¹ * y⁻¹ = 1 by
    change x * y = y * x
    · rw [mul_assoc, mul_eq_one_iff_eq_inv] at this
      simpa

Goal state after:
G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
hH₁ : H₁.Normal
hH₂ : H₂.Normal
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
⊢ x * y * x⁻¹ * y⁻¹ = 1
Module: Mathlib.Algebra.Order.BigOperators.Group.List

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

Tactic:
induction l with

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_one : f 1 ≤ 1
hp_one : p 1
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 α
hpl : ∀ (a : α), a ∈ l → p a
⊢ f l.prod ≤ (map f l).prod

Tactic:
induction l with

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:
induction l with

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

Goal state before:
pp: M : Type u_3
N : Type u_4
inst✝² : AddZeroClass M
inst✝¹ : Zero N
inst✝ : LinearOrder N
f : M → N
h0 : f 0 ≤ 0
hadd : ∀ (x y : M), f (x + y) ≤ max (f x) (f y)
l : List M
⊢ f l.sum ≤ foldr max 0 (map f l)

Tactic:
induction l with

Goal state after:
Module: Mathlib.Data.Sigma.Lex

Goal state before:
pp: case inr.inl.inr.inl
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b : (i : ι) × α i
inst✝¹ : Std.Trichotomous r
inst✝ : ∀ (i : ι), Std.Trichotomous (s i)
i : ι
a : α i
⊢ Lex r s ⟨i, a⟩ ⟨i, a⟩ ∨ ⟨i, a⟩ = ⟨i, a⟩ ∨ Lex r s ⟨i, a⟩ ⟨i, a⟩

Tactic:
exact Or.inr (Or.inl rfl)

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

Goal state before:
pp: α : Type u_5
β : Type u_6
inst✝³ : Monoid α
inst✝² : AddMonoid β
inst✝¹ : Preorder β
inst✝ : AddLeftMono β
l : List α
f : α → β
h_one : f 1 ≤ 0
h_mul : ∀ (a b : α), f (a * b) ≤ f a + f b
⊢ f l.prod ≤ (map f l).sum

Tactic:
induction l with

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
l : List α
b : WithBot α
h : ∀ (a : α), a ∈ l → ↑a ≤ b
⊢ l.maximum ≤ b

Tactic:
induction l with

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
l : List α
i : ℕ
w : i < l.length
h : 0 < l.length
⊢ l[i] ≤ maximum_of_length_pos h

Tactic:
by
  apply le_maximum_of_length_pos_of_mem
  exact getElem_mem _

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

Goal state before:
pp: case cons
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l : List α
hd : α
tl : List α
IH : tl ≠ [] → ↑(foldr max ⊥ tl) = tl.maximum
h : hd :: tl ≠ []
⊢ ↑(foldr max ⊥ (hd :: tl)) = (hd :: tl).maximum

Tactic:
rw [maximum_cons, foldr, WithBot.coe_max]

Goal state after:
case cons
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l : List α
hd : α
tl : List α
IH : tl ≠ [] → ↑(foldr max ⊥ tl) = tl.maximum
h : hd :: tl ≠ []
⊢ max ↑hd ↑(foldr max ⊥ tl) = max (↑hd) tl.maximum
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l : List α
h : l ≠ []
⊢ ↑(foldr max ⊥ l) = l.maximum

Tactic:
induction l with

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

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

Tactic:
induction l with

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

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

Tactic:
induction l with

Goal state after:
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:
induction l with

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

Goal state before:
pp: case insert
α : Type u_2
inst✝ : LinearOrder α
a✝² : α
s✝ : Finset α
a✝¹ : a✝² ∉ s✝
a✝ : ∀ {a : α}, s✝.max = ↑a → a ∈ s✝
⊢ ∀ {a : α}, (insert a✝² s✝).max = ↑a → a ∈ insert a✝² s✝

Tactic:
grind [WithBot.coe_eq_coe]

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

Goal state before:
pp: α : Type u
l : List α
⊢ l.reverse.sublists = map reverse l.sublists'

Tactic:
induction l with

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

Goal state before:
pp: case cons_cons
α : Type u
l₁ l₂ l₁✝ l₂✝ : List α
a : α
a✝ : l₁✝ <+ l₂✝
ih : l₁✝.sublists' <+ l₂✝.sublists'
⊢ (a :: l₁✝).sublists' <+ (a :: l₂✝).sublists'

Tactic:
rw [sublists'_cons, sublists'_cons]
    exact ih.append (ih.map _)

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

Goal state before:
pp: case mpr
α : Type u_1
κ : Sort u_4
r : α → α → Prop
f : κ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) f
H : ∀ (n : κ), (f n).Pairwise r
i : α
⊢ i ∈ ⋃ n, f n → ∀ ⦃y : α⦄, y ∈ ⋃ n, f n → i ≠ y → r i y

Tactic:
hi

Goal state after:
case mpr
α : Type u_1
κ : Sort u_4
r : α → α → Prop
f : κ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) f
H : ∀ (n : κ), (f n).Pairwise r
i : α
hi : i ∈ ⋃ n, f n
⊢ ∀ ⦃y : α⦄, y ∈ ⋃ n, f n → i ≠ y → r i y
Module: Mathlib.Data.Set.Pairwise.Lattice

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set (Set α)
hd : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) s
⊢ (⋃₀ s).Pairwise r ↔ ∀ a ∈ s, a.Pairwise r

Tactic:
by
  rw [sUnion_eq_iUnion, pairwise_iUnion hd.directed_val, SetCoe.forall]

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

Goal state before:
pp: α : Type u
l : List α
⊢ flatMap (fun n ↦ sublistsLen n l) (range (l.length + 1)) ~ l.sublists'

Tactic:
induction l with

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

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
f : ι → α
inst✝ : Finite ι
⊢ Finite ↑(range f)

Tactic:
by
  classical
  have := Fintype.ofFinite (PLift ι)
  infer_instance

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

Goal state before:
pp: case refine_1
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
h : (s ×ˢ t).PairwiseDisjoint f
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i ≠ j
⊢ (Disjoint on fun i ↦ ⨆ i' ∈ t, f (i, i')) i j

Tactic:
simp_rw [Function.onFun, iSup_disjoint_iff, disjoint_iSup_iff]

Goal state after:
case refine_1
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
h : (s ×ˢ t).PairwiseDisjoint f
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i ≠ j
⊢ ∀ i_1 ∈ t, ∀ i_3 ∈ t, Disjoint (f (i, i_1)) (f (j, i_3))
Module: Mathlib.Data.Set.Pairwise.Lattice

Goal state before:
pp: case refine_2
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
h : (s ×ˢ t).PairwiseDisjoint f
i : ι'
hi : i ∈ t
j : ι'
hj : j ∈ t
hij : i ≠ j
⊢ (Disjoint on fun i' ↦ ⨆ i ∈ s, f (i, i')) i j

Tactic:
simp_rw [Function.onFun, iSup_disjoint_iff, disjoint_iSup_iff]

Goal state after:
case refine_2
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
h : (s ×ˢ t).PairwiseDisjoint f
i : ι'
hi : i ∈ t
j : ι'
hj : j ∈ t
hij : i ≠ j
⊢ ∀ i_1 ∈ s, ∀ i_3 ∈ s, Disjoint (f (i_1, i)) (f (i_3, j))
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
ι : Type u_1
s : ι → Set α
hs : Pairwise fun i j ↦ Disjoint (s i) (s j)
h : (⋃ i, s i).Finite
⊢ (∀ (i : ι), (s i).Finite) ∧ {i | (s i).Nonempty}.Finite

Tactic:
refine ⟨fun i ↦ h.subset <| subset_iUnion _ _, ?_⟩

Goal state after:
α : Type u
ι : Type u_1
s : ι → Set α
hs : Pairwise fun i j ↦ Disjoint (s i) (s j)
h : (⋃ i, s i).Finite
⊢ {i | (s i).Nonempty}.Finite
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: case pos
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : (image f s).Nonempty
i : ι
h✝ : i ∈ s
⊢ ∃ a ∈ s, f i ≤ f a

pp: case neg
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : (image f s).Nonempty
i : ι
h✝ : i ∉ s
⊢ ∃ a ∈ s, sSup ∅ ≤ f a

Tactic:
· exact ⟨_, by assumption, le_rfl⟩

Goal state after:
case neg
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : (image f s).Nonempty
i : ι
h✝ : i ∉ s
⊢ ∃ a ∈ s, sSup ∅ ≤ f a
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: case refine_2
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : (image f s).Nonempty
i : ι
⊢ i ∈ s → ∃ a, f i ≤ if a ∈ s then f a else sSup ∅

Tactic:
hi

Goal state after:
case refine_2
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : (image f s).Nonempty
i : ι
hi : i ∈ s
⊢ ∃ a, f i ≤ if a ∈ s then f a else sSup ∅
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case pos
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range f)
hf' : sSup ∅ ≤ iSup f
h✝¹ : Nonempty (Subtype p)
this : Nonempty ι
i : ι
h✝ : p i
⊢ f ⟨i, h✝⟩ ≤ iSup f

pp: case neg
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range f)
hf' : sSup ∅ ≤ iSup f
h✝¹ : Nonempty (Subtype p)
this : Nonempty ι
i : ι
h✝ : ¬p i
⊢ sSup ∅ ≤ iSup f

Tactic:
· exact le_ciSup hf ?_

Goal state after:
case neg
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range f)
hf' : sSup ∅ ≤ iSup f
h✝¹ : Nonempty (Subtype p)
this : Nonempty ι
i : ι
h✝ : ¬p i
⊢ sSup ∅ ≤ iSup f
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u_1
ι : Type u_2
f : ι → Set α
c : Set ι
hn : c.Nonempty
hc : DirectedOn (fun i j ↦ f i ⊆ f j) c
s : Finset α
hs : ↑s ⊆ ⋃ x, f ↑x
this : Nonempty ↑c
⊢ ∃ i ∈ c, ↑s ⊆ f i

Tactic:
simpa using (directed_comp.2 hc.directed_val).exists_mem_subset_of_finset_subset_biUnion hs

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
x y : α × β
h : x ⩿ y
ha : x.1 ≠ y.1
hb : x.2 ≠ y.2
⊢ False

Tactic:
exact
    h.2 (mk_lt_mk.2 <| Or.inl ⟨ha.lt_of_le h.1.1, le_rfl⟩)
      (mk_lt_mk.2 <| Or.inr ⟨le_rfl, hb.lt_of_le h.1.2⟩)

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
P : α → Prop
x : α
inst✝ : Preorder α
⊢ Minimal P x ↔ P x ∧ ∀ ⦃y : α⦄, y < x → ¬P y

Tactic:
by
  simp [Minimal, lt_iff_le_not_ge, imp.swap]

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
P : Set α → Prop
s : Set α
hP : ∀ ⦃s t : Set α⦄, P t → s ⊆ t → P s
hs : P s
h : ¬Maximal P s
⊢ ∃ x, ¬x ∈ s ∧ P (insert x s)

Tactic:
simpa [Set.maximal_iff_forall_insert hP, hs] using h

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

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝² : LinearOrder α
inst✝¹ : PartialOrder β
inst✝ : Finite α
f g : α →o β
hf : Function.Injective ⇑f
hg : Function.Injective ⇑g
⊢ Set.range ⇑f = Set.range ⇑g ↔ f = g

Tactic:
refine ⟨fun h ↦ ?_, by rintro rfl; rfl⟩
  ext : 2
  exact DFunLike.congr_fun ((OrderEmbedding.range_eq_iff
    (f := .ofStrictMono f (f.monotone.strictMono_of_injective hf))
    (g := .ofStrictMono g (g.monotone.strictMono_of_injective hg))).1 (by simpa)) _

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b x : α
⊢ x ∈ Icc a b ↔ a ≤ x ∧ x ≤ b

Tactic:
Icc,

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b x : α
⊢ x ∈ (Finset.Icc a b).val ↔ a ≤ x ∧ x ≤ b
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderTop α
a x : α
⊢ x ∈ Finset.Ioi a ↔ a < x

Tactic:
Finset.mem_Ioi

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderTop α
a x : α
⊢ a < x ↔ a < x
Module: Mathlib.Order.Interval.Multiset

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

Tactic:
Icc,

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b : α
⊢ (Finset.Icc a b).val = 0 ↔ ¬a ≤ b
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a : α
⊢ Icc a a = {a}

Tactic:
Icc,

Goal state after:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a : α
⊢ (Finset.Icc a a).val = {a}
Module: Mathlib.Order.Interval.Finset.Basic

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

Tactic:
by
  simpa [← coe_subset] using Set.Icc_subset_Icc ha hb

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₂
⊢ Ioc a b₁ ⊆ Ioo a b₂

Tactic:
rw [← coe_subset, coe_Ioc, coe_Ioo]

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

Goal state before:
pp: case refine_2
ι : Type u_3
α : ι → Type u_4
inst✝¹ : Finite ι
r : (i : ι) → α i → α i → Prop
inst✝ : ∀ (i : ι), IsPreorder (α i) (r i)
hr : ∀ (i : ι), WellQuasiOrdered (r i)
this✝ : Fintype ι
this : IsPreorder ((i : ι) → α i) fun a b ↦ ∀ (i : ι), r i (a i) (b i)
i : ι
s : Finset ι
⊢ ∀ (h : i ∉ s),
    (∀ (f : ℕ → (i : ι) → α i), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ s, r i ((f ∘ ⇑g) a i) ((f ∘ ⇑g) b i)) →
      ∀ (f : ℕ → (i : ι) → α i),
        ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i_1 ∈ Finset.cons i s h, r i_1 ((f ∘ ⇑g) a i_1) ((f ∘ ⇑g) b i_1)

Tactic:
hi

Goal state after:
case refine_2
ι : Type u_3
α : ι → Type u_4
inst✝¹ : Finite ι
r : (i : ι) → α i → α i → Prop
inst✝ : ∀ (i : ι), IsPreorder (α i) (r i)
hr : ∀ (i : ι), WellQuasiOrdered (r i)
this✝ : Fintype ι
this : IsPreorder ((i : ι) → α i) fun a b ↦ ∀ (i : ι), r i (a i) (b i)
i : ι
s : Finset ι
hi : i ∉ s
⊢ (∀ (f : ℕ → (i : ι) → α i), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ s, r i ((f ∘ ⇑g) a i) ((f ∘ ⇑g) b i)) →
    ∀ (f : ℕ → (i : ι) → α i),
      ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i_1 ∈ Finset.cons i s hi, r i_1 ((f ∘ ⇑g) a i_1) ((f ∘ ⇑g) b i_1)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a < b
⊢ Ioc a b = insert b (Ioo a b)

Tactic:
Ioo_insert_right h

Goal state after:
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a < b
⊢ Ioc a b = Ioc a b
Module: Mathlib.Algebra.Group.Submonoid.Pointwise

Goal state before:
pp: case a
G : Type u_2
inst✝ : Group G
s : Set G
⊢ closure s⁻¹ ≤ (closure s)⁻¹

Tactic:
rw [closure_le, coe_inv, ← Set.inv_subset, inv_inv]

Goal state after:
case a
G : Type u_2
inst✝ : Group G
s : Set G
⊢ s ⊆ ↑(closure s)
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a : α
⊢ orbit G a = orbit G (g⁻¹ • g • a)

Tactic:
inv_smul_smul

Goal state after:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a : α
⊢ orbit G a = orbit G a
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case refine_2
ι : Type u_1
α : ι → Type u_6
inst✝¹ : Finite ι
r : (i : ι) → α i → α i → Prop
inst✝ : ∀ (i : ι), IsPreorder (α i) (r i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), (s i).PartiallyWellOrderedOn (r i)
this✝ : Fintype ι
this : IsPreorder ((i : ι) → α i) fun a b ↦ ∀ (i : ι), r i (a i) (b i)
i : ι
t : Finset ι
⊢ ∀ (h : i ∉ t),
    (∀ (f : ℕ → (i : ι) → α i),
        (∀ (n : ℕ) (i : ι), f n i ∈ s i) → ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ t, r i ((f ∘ ⇑g) a i) ((f ∘ ⇑g) b i)) →
      ∀ (f : ℕ → (i : ι) → α i),
        (∀ (n : ℕ) (i : ι), f n i ∈ s i) →
          ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i_1 ∈ Finset.cons i t h, r i_1 ((f ∘ ⇑g) a i_1) ((f ∘ ⇑g) b i_1)

Tactic:
hi

Goal state after:
case refine_2
ι : Type u_1
α : ι → Type u_6
inst✝¹ : Finite ι
r : (i : ι) → α i → α i → Prop
inst✝ : ∀ (i : ι), IsPreorder (α i) (r i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), (s i).PartiallyWellOrderedOn (r i)
this✝ : Fintype ι
this : IsPreorder ((i : ι) → α i) fun a b ↦ ∀ (i : ι), r i (a i) (b i)
i : ι
t : Finset ι
hi : i ∉ t
⊢ (∀ (f : ℕ → (i : ι) → α i),
      (∀ (n : ℕ) (i : ι), f n i ∈ s i) → ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ t, r i ((f ∘ ⇑g) a i) ((f ∘ ⇑g) b i)) →
    ∀ (f : ℕ → (i : ι) → α i),
      (∀ (n : ℕ) (i : ι), f n i ∈ s i) →
        ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i_1 ∈ Finset.cons i t hi, r i_1 ((f ∘ ⇑g) a i_1) ((f ∘ ⇑g) b i_1)
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: case refine_1
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : α
a b : ↑(orbit G x)
h : a ∈ orbit (↥H) b
⊢ ↑a ∈ orbit ↥H ↑b

Tactic:
rcases h with ⟨g, rfl⟩

Goal state after:
case refine_1
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : α
b : ↑(orbit G x)
g : ↥H
⊢ ↑((fun m ↦ m • b) g) ∈ orbit ↥H ↑b
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: case refine_2
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : Quotient G α
a b : ↑x.orbit
h : a ∈ MulAction.orbit (↥H) b
⊢ ↑a ∈ MulAction.orbit ↥H ↑b

Tactic:
rcases h with ⟨g, rfl⟩

Goal state after:
case refine_2
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : Quotient G α
b : ↑x.orbit
g : ↥H
⊢ ↑((fun m ↦ m • b) g) ∈ MulAction.orbit ↥H ↑b
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
rk : α → ℕ
s : Set α
n : ℕ
f : ℕ → α
hf : IsBadSeq r s f
h : ∃ k g, (∀ m < n, f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = k
h1 : ∀ m < n, f m = Classical.choose ⋯ m
h2 : IsBadSeq r s (Classical.choose ⋯)
h3 : rk (Classical.choose ⋯ n) = Nat.find h
⊢ IsBadSeq r s (Classical.choose ⋯)

Tactic:
convert! h2

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case succ
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
fs : (n : ℕ) → { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } :=
  fun t ↦
    Nat.rec ⟨↑(minBadSeqOfBadSeq r rk s 0 f0 hf0), ⋯⟩ (fun n fn ↦ ⟨↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn ⋯), ⋯⟩) t
m k : ℕ
ih : ↑(fs m) m = ↑(fs (m + k)) m
⊢ ↑(fs (m + k)) m = ↑(fs (m + (k + 1))) m

Tactic:
(minBadSeqOfBadSeq r rk s (m + k + 1) (fs (m + k)).1 (fs (m + k)).2.1).2.1 m
        (Nat.lt_succ_iff.2 (Nat.add_le_add_left k.zero_le m))

Goal state after:
case succ
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
fs : (n : ℕ) → { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } :=
  fun t ↦
    Nat.rec ⟨↑(minBadSeqOfBadSeq r rk s 0 f0 hf0), ⋯⟩ (fun n fn ↦ ⟨↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn ⋯), ⋯⟩) t
m k : ℕ
ih : ↑(fs m) m = ↑(fs (m + k)) m
⊢ ↑(minBadSeqOfBadSeq r rk s (m + k + 1) ↑(fs (m + k)) ⋯) m = ↑(fs (m + (k + 1))) m
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : Preorder β
f : α → β
h : ∀ (a b : α), a ⋖ b → f a < f b
a b : α
hab : a < b
this : (a < b) ≤ (TransGen LT.lt on f) a b
⊢ f a < f b

Tactic:
transGen_eq_self

Goal state after:
α : Type u_2
β : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : Preorder β
f : α → β
h : ∀ (a b : α), a ⋖ b → f a < f b
a b : α
hab : a < b
this : (a < b) ≤ (LT.lt on f) a b
⊢ f a < f b
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: G : Type u_1
β : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G β
α : Type u_4
inst✝² : Group α
inst✝¹ : MulAction α β
inst✝ : SMulCommClass G α β
a : α
b : β
⊢ stabilizer G (a⁻¹ • a • b) = stabilizer G b

Tactic:
inv_smul_smul

Goal state after:
G : Type u_1
β : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G β
α : Type u_4
inst✝² : Group α
inst✝¹ : MulAction α β
inst✝ : SMulCommClass G α β
a : α
b : β
⊢ stabilizer G b = stabilizer G b
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: ι : Type u_2
A : ι → Type u_3
inst✝ : (i : ι) → Mul (A i)
x : (i : ι) → A i
x✝ :
  (∀ (a : (i : ι) → A i) (x_1 : ι), x x_1 * a x_1 = a x_1 * x x_1) ∧
    (∀ (b c : (i : ι) → A i) (x_1 : ι), x x_1 * (b x_1 * c x_1) = x x_1 * b x_1 * c x_1) ∧
      ∀ (a b : (i : ι) → A i) (x_1 : ι), a x_1 * b x_1 * x x_1 = a x_1 * (b x_1 * x x_1)
i : ι
h1 : ∀ (a : (i : ι) → A i) (x_1 : ι), x x_1 * a x_1 = a x_1 * x x_1
h2 : ∀ (b c : (i : ι) → A i) (x_1 : ι), x x_1 * (b x_1 * c x_1) = x x_1 * b x_1 * c x_1
h3 : ∀ (a b : (i : ι) → A i) (x_1 : ι), a x_1 * b x_1 * x x_1 = a x_1 * (b x_1 * x x_1)
a : A i
⊢ x i * a = a * x i

Tactic:
by simpa using h1 (update x i a) i

Goal state after:
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: case refine_1
G : Type u_1
inst✝ : Group G
s : Set G
g : G
hg : g ∈ centralizer s
h : G
hh : h ∈ s
⊢ g * h * g⁻¹ ∈ s

Tactic:
simpa [← hg h hh]

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

Goal state before:
pp: α : Type u_3
inst✝ : Monoid α
l : List α
comm : {x | x ∈ ↑l}.Pairwise Commute
⊢ List.foldr (fun x1 x2 ↦ x1 * x2) 1 l = l.prod

Tactic:
induction l with

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

Goal state before:
pp: α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H K : Subgroup G
hH : H.Normal
hK : K.Normal
n : G
hmem : n ∈ H ⊔ K
g : G
⊢ g * n * g⁻¹ ∈ H ⊔ K

Tactic:
rw [← SetLike.mem_coe, normal_mul] at hmem ⊢

Goal state after:
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H K : Subgroup G
hH : H.Normal
hK : K.Normal
n : G
hmem : n ∈ ↑H * ↑K
g : G
⊢ g * n * g⁻¹ ∈ ↑H * ↑K
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: α : Type u_6
a : Multiset α
l : List (Multiset α)
⊢ Disjoint l.sum a ↔ ∀ b ∈ l, Disjoint b a

Tactic:
induction l with

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

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
c : Con M
⊢ c.toSetoid = ⊤ ↔ c = ⊤

Tactic:
← toSetoid_top,

Goal state after:
M : Type u_1
inst✝ : Mul M
c : Con M
⊢ c.toSetoid = ⊤.toSetoid ↔ c = ⊤
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
s₁ s₂ : Finset ι
inst✝¹ : CommMonoid M
f : ι → M
inst✝ : DecidableEq ι
h : Disjoint s₁ s₂
⊢ ∏ x ∈ s₁ ∪ s₂, f x = (∏ x ∈ s₁, f x) * ∏ x ∈ s₂, f x

Tactic:
← prod_union_inter,

Goal state after:
ι : Type u_1
M : Type u_4
s₁ s₂ : Finset ι
inst✝¹ : CommMonoid M
f : ι → M
inst✝ : DecidableEq ι
h : Disjoint s₁ s₂
⊢ ∏ x ∈ s₁ ∪ s₂, f x = (∏ x ∈ s₁ ∪ s₂, f x) * ∏ x ∈ s₁ ∩ s₂, f x