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

Goal state before:
pp: α : 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
⊢ ↑r ⊆ ↑(insert a r)

Tactic:
rw [Finset.coe_subset]

Goal state after:
α : 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
⊢ r ⊆ insert a r
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case inr
α : Type u_2
β : Type u_3
inst✝² : SemilatticeSup β
inst✝¹ : OrderBot β
inst✝ : WellFoundedGT β
f : α → β
h✝ : Nonempty α
t : Finset α
ht : ∀ x ∈ Set.range fun x ↦ x.sup f, ¬(fun x ↦ x.sup f) t < x
a : α
⊢ f a ≤ t.sup f

Tactic:
have := ht (f a ⊔ t.sup f) ⟨insert a t, by simp⟩

Goal state after:
case inr
α : Type u_2
β : Type u_3
inst✝² : SemilatticeSup β
inst✝¹ : OrderBot β
inst✝ : WellFoundedGT β
f : α → β
h✝ : Nonempty α
t : Finset α
ht : ∀ x ∈ Set.range fun x ↦ x.sup f, ¬(fun x ↦ x.sup f) t < x
a : α
this : ¬(fun x ↦ x.sup f) t < f a ⊔ t.sup f
⊢ f a ≤ t.sup f
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case singleton
α : Type u_2
ι : Type u_5
inst✝ : BooleanAlgebra α
s : Finset ι
f : ι → α
a : α
a✝ : ι
⊢ ({a✝}.inf fun b ↦ a \ f b) = a \ {a✝}.sup f

Tactic:
| singleton =>

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

Goal state before:
pp: case singleton
α : Type u_2
ι : Type u_5
inst✝ : BooleanAlgebra α
s : Finset ι
f : ι → α
a : α
a✝ : ι
⊢ ({a✝}.inf fun b ↦ f b \ a) = {a✝}.inf f \ a

Tactic:
| singleton =>

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

Goal state before:
pp: case insert.inr.inl
α : 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
hs : s.Nonempty
ha : f a ≤ s.sup f
⊢ max (f a) (s.sup f) ∈ f '' insert a ↑s

pp: case insert.inr.inr
α : 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
hs : s.Nonempty
ha : s.sup f ≤ f a
⊢ max (f a) (s.sup f) ∈ f '' insert a ↑s

Tactic:
· rw [sup_eq_right.mpr ha]
        exact Set.image_mono (Set.subset_insert a s) (h hs)

Goal state after:
case insert.inr.inr
α : 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
hs : s.Nonempty
ha : s.sup f ≤ f a
⊢ max (f a) (s.sup f) ∈ f '' insert a ↑s
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case singleton
α : Type u_2
ι : Type u_5
inst✝ : DistribLattice α
s : Finset ι
hs : s.Nonempty
f : ι → α
a : α
a✝ : ι
⊢ a ⊓ {a✝}.sup' ⋯ f = {a✝}.sup' ⋯ fun i ↦ a ⊓ f i

Tactic:
| singleton =>

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompletePartialOrderSup α
p : ι → Prop
f : Subtype p → α
hp : ∀ (i : ι), p i
⊢ ⨆ i, f ⟨i, ⋯⟩ = iSup f

Tactic:
simp only [iSup]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : ConditionallyCompletePartialOrderSup α
inst✝ : Preorder β
f : β → α
a : β
hf : Monotone f
hd : Directed (fun x1 x2 ↦ x1 ≤ x2) fun x ↦ f ↑x
⊢ ⨆ x, f ↑x = f a

Tactic:
have H : BddAbove (range fun x : Iic a ↦ f x) := ⟨f a, fun _ ↦ by aesop⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : ConditionallyCompletePartialOrderSup α
inst✝ : Preorder β
f : β → α
a : β
hf : Monotone f
hd : Directed (fun x1 x2 ↦ x1 ≤ x2) fun x ↦ f ↑x
H : BddAbove (range fun x ↦ f ↑x)
⊢ ⨆ x, f ↑x = f a
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 ∅
h' : (image f s).Nonempty
⊢ OrderDual.toDual (⨅ i ∈ s, f i) = (image (⇑OrderDual.toDual) (image f s)).max' ⋯

Tactic:
toDual_iInf

Goal state after:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, f x ≤ sInf ∅
h' : (image f s).Nonempty
⊢ ⨆ i, OrderDual.toDual (⨅ (_ : i ∈ s), f i) = (image (⇑OrderDual.toDual) (image f s)).max' ⋯
Module: Mathlib.Order.Interval.Set.WithBotTop

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

Tactic:
← preimage_coe_Iio,

Goal state after:
α : Type u_1
inst✝ : Preorder α
a : α
⊢ some '' some ⁻¹' Iio ↑a = Iio ↑a
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Multiset ι
f : ι → α
h : s ≠ 0
⊢ ∃ x ∈ s, sSup ∅ ≤ f x

Tactic:
simpa using exists_mem_of_ne_zero h

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
p q : Prop
f : p ∧ q → α
hp : p
hq : q
⊢ ⨆ (ih : p ∧ q), f ih = ⨆ (h₁ : p), ⨆ (h₂ : q), f ⋯

Tactic:
simp [hp, hq, iSup_of_empty']

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
p q : Prop
f : p ∧ q → α
hp : p
hq : ¬q
⊢ ⨆ (ih : p ∧ q), f ih = ⨆ (h₁ : p), ⨆ (h₂ : q), f ⋯

Tactic:
simp [hp, hq, iSup_of_empty']

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
p q : Prop
f : p ∧ q → α
hp : ¬p
hq : q
⊢ ⨆ (ih : p ∧ q), f ih = ⨆ (h₁ : p), ⨆ (h₂ : q), f ⋯

Tactic:
simp [hp, hq, iSup_of_empty']

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
p q : Prop
f : p ∧ q → α
hp : ¬p
hq : ¬q
⊢ ⨆ (ih : p ∧ q), f ih = ⨆ (h₁ : p), ⨆ (h₂ : q), f ⋯

Tactic:
simp [hp, hq, iSup_of_empty']

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
⊢ ⨅ i, ↑(f i) < ⊤ ↔ Nonempty ι

Tactic:
lt_top_iff_ne_top,

Goal state after:
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
⊢ ⨅ i, ↑(f i) ≠ ⊤ ↔ Nonempty ι
Module: Mathlib.Order.Cover

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst✝ : DecidableEq ι
⊢ a ⋖ b ↔ ∃ i x, a i ⋖ x ∧ b = Function.update a i x

Tactic:
rw [covBy_iff]

Goal state after:
ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst✝ : DecidableEq ι
⊢ (∃ i, a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → a j = b j) ↔ ∃ i x, a i ⋖ x ∧ b = Function.update a i x
Module: Mathlib.Data.Finset.Sigma

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Finset ι
t : (i : ι) → Finset (α i)
p : (i : ι) → α i → Prop
inst✝ : (i : ι) → DecidablePred (p i)
⊢ {x ∈ s.sigma t | p x.fst x.snd} = s.sigma fun i ↦ filter (p i) (t i)

Tactic:
by
  simp [filter_sigma]

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst✝ : DecidableEq ι
⊢ a ⋖ b ↔ ∃ i x, x ⋖ b i ∧ a = Function.update b i x

Tactic:
rw [covBy_iff]

Goal state after:
ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst✝ : DecidableEq ι
⊢ (∃ i, a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → a j = b j) ↔ ∃ i x, x ⋖ b i ∧ a = Function.update b i x
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₁ : LocallyFiniteOrderTop α
h₀_finset_Ioi h₀_finset_Ici : α → Finset α
h₀_finset_mem_Ici : ∀ (a x : α), x ∈ h₀_finset_Ici a ↔ a ≤ x
h₀_finset_mem_Ioi : ∀ (a x : α), x ∈ h₀_finset_Ioi a ↔ a < x
⊢ { finsetIoi := h₀_finset_Ioi, finsetIci := h₀_finset_Ici, finset_mem_Ici := h₀_finset_mem_Ici,
      finset_mem_Ioi := h₀_finset_mem_Ioi } =
    h₁

Tactic:
obtain ⟨h₁_finset_Ioi, h₁_finset_Ici, h₁_finset_mem_Ici, h₁_finset_mem_Ioi⟩ := h₁

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀_finset_Ioi h₀_finset_Ici : α → Finset α
h₀_finset_mem_Ici : ∀ (a x : α), x ∈ h₀_finset_Ici a ↔ a ≤ x
h₀_finset_mem_Ioi : ∀ (a x : α), x ∈ h₀_finset_Ioi a ↔ a < x
h₁_finset_Ioi h₁_finset_Ici : α → Finset α
h₁_finset_mem_Ici : ∀ (a x : α), x ∈ h₁_finset_Ici a ↔ a ≤ x
h₁_finset_mem_Ioi : ∀ (a x : α), x ∈ h₁_finset_Ioi a ↔ a < x
⊢ { finsetIoi := h₀_finset_Ioi, finsetIci := h₀_finset_Ici, finset_mem_Ici := h₀_finset_mem_Ici,
      finset_mem_Ioi := h₀_finset_mem_Ioi } =
    { finsetIoi := h₁_finset_Ioi, finsetIci := h₁_finset_Ici, finset_mem_Ici := h₁_finset_mem_Ici,
      finset_mem_Ioi := h₁_finset_mem_Ioi }
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: case inr
n a : ℕ
ha : a ≠ 0
⊢ image (fun x ↦ x % a) (Ico n (n + a)) = range a

Tactic:
ext i

Goal state after:
case inr
n a : ℕ
ha : a ≠ 0
i : ℕ
⊢ i ∈ image (fun x ↦ x % a) (Ico n (n + a)) ↔ i ∈ range a
Module: Mathlib.Order.OrderIsoNat

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

Tactic:
induction x with

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

Goal state before:
pp: α : Type u_2
a b : α
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DenselyOrdered α
⊢ (↑(Ioo a b)).Nonempty ↔ a < b

Tactic:
coe_Ioo,

Goal state after:
α : Type u_2
a b : α
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DenselyOrdered α
⊢ (Set.Ioo a b).Nonempty ↔ a < b
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DenselyOrdered α
⊢ ↑(Ioo a b) = ∅ ↔ ¬a < b

Tactic:
coe_Ioo,

Goal state after:
α : Type u_2
a b : α
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DenselyOrdered α
⊢ Set.Ioo a b = ∅ ↔ ¬a < b
Module: Mathlib.Order.Interval.Finset.Basic

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

Tactic:
coe_Ioo,

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

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

Tactic:
coe_Ioo,

Goal state after:
α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ Set.Ioo a b ⊆ ↑(Ioc a b)
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_6
r : α → α → Prop
a : α
⊢ Acc r a → {b | ReflTransGen r b a}.WellFoundedOn r

Tactic:
refine fun h => ⟨fun b => InvImage.accessible Subtype.val ?_⟩

Goal state after:
α : Type u_6
r : α → α → Prop
a : α
h : Acc r a
b : { x // x ∈ {b | ReflTransGen r b a} }
⊢ Acc r ↑b
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h₁ : a₁ ≤ b₁
⊢ Set.Icc a₁ b₁ ⊆ ↑(Ioo a₂ b₂) ↔ a₂ < a₁ ∧ b₁ < b₂

Tactic:
coe_Ioo,

Goal state after:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h₁ : a₁ ≤ b₁
⊢ Set.Icc a₁ b₁ ⊆ Set.Ioo a₂ b₂ ↔ a₂ < a₁ ∧ b₁ < b₂
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
⊢ (Iio a).Nonempty ↔ ¬IsMin a

Tactic:
by
  contrapose!; exact Iio_eq_empty

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

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

Tactic:
coe_Ioo,

Goal state after:
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidableEq α
h : a < b
⊢ insert a (Set.Ioo a b) = ↑(Ico a b)
Module: Mathlib.Order.Interval.Finset.Basic

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

Tactic:
coe_Ioo,

Goal state after:
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidableEq α
h : a < b
⊢ insert b (Set.Ioo a b) = ↑(Ioc a b)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a ≤ b
⊢ Icc a b = cons b (Ico a b) ⋯

Tactic:
classical rw [cons_eq_insert, Ico_insert_right h]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : Preorder α
p : α → Prop
inst✝⁵ : DecidablePred p
y : α
F : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : Preorder M
inst✝³ : Preorder N
inst✝² : EquivLike F M N
inst✝¹ : OrderIsoClass F M N
f : F
inst✝ : LocallyFiniteOrder N
⊢ ∀ (a b x : M), x ∈ map { toFun := EquivLike.inv f, inj' := ⋯ } (finsetIoc (f a) (f b)) ↔ a < x ∧ x ≤ b

Tactic:
simp [finset_mem_Ioc, EquivLike.inv_apply_eq, map_lt_map_iff]

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

Goal state before:
pp: α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
⊢ Disjoint (Ioc a₁ a₂) (Ioc b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁

Tactic:
by
  simp_rw [disjoint_iff_inter_eq_empty, Ioc_inter_Ioc, Ioc_eq_empty_iff, not_lt]

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
a b : α
h : ⟦a⟧ = ⟦b⟧
⊢ ⟦a⟧ = ⟦b⟧

Tactic:
rw [@Quotient.eq] at h ⊢
  exact mem_orbit_of_mem_orbit_subgroup h

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case neg
α : Type u_2
r : α → α → Prop
inst✝ : IsPreorder α r
s : Set α
h : s.PartiallyWellOrderedOn r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ x ∈ l, x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (f (g m)).head! (f (g n)).head!
hf' :
  (∀ (n : ℕ), (if n < g 0 then f n else (f (g (n - g 0))).tail) ∈ {l | ∀ x ∈ l, x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < g 0 then f m else (f (g (m - g 0))).tail)
          (if n < g 0 then f n else (f (g (n - g 0))).tail)
m n' : ℕ
mn : m < g 0 + n'
hn : ¬g 0 + n' < g 0
hm : ¬m < g 0
hmn : List.SublistForall₂ r (f (g (m - g 0))).tail (f (g n')).tail
⊢ False

Tactic:
← Nat.sub_lt_iff_lt_add' (le_of_not_gt hm)

Goal state after:
case neg
α : Type u_2
r : α → α → Prop
inst✝ : IsPreorder α r
s : Set α
h : s.PartiallyWellOrderedOn r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ x ∈ l, x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (f (g m)).head! (f (g n)).head!
hf' :
  (∀ (n : ℕ), (if n < g 0 then f n else (f (g (n - g 0))).tail) ∈ {l | ∀ x ∈ l, x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < g 0 then f m else (f (g (m - g 0))).tail)
          (if n < g 0 then f n else (f (g (n - g 0))).tail)
m n' : ℕ
mn : m - g 0 < n'
hn : ¬g 0 + n' < g 0
hm : ¬m < g 0
hmn : List.SublistForall₂ r (f (g (m - g 0))).tail (f (g n')).tail
⊢ False
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: case refine_2
G : Type u_1
inst✝ : Group G
g h : G
⊢ h ∈ centralizer {g} → h ∈ normalizer {g}

Tactic:
refine fun hh g ↦ ⟨?_, ?_⟩

Goal state after:
case refine_2.refine_1
G : Type u_1
inst✝ : Group G
g✝ h : G
hh : h ∈ centralizer {g✝}
g : G
⊢ g ∈ {g✝} → h * g * h⁻¹ ∈ {g✝}

case refine_2.refine_2
G : Type u_1
inst✝ : Group G
g✝ h : G
hh : h ∈ centralizer {g✝}
g : G
⊢ h * g * h⁻¹ ∈ {g✝} → g ∈ {g✝}
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case e'_5
ι : Type u_1
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
hι : WellFounded (rι on f)
hπ : ∀ (i : ι), (f ⁻¹' {i}).WellFoundedOn (rπ i on g i)
c c' : γ
h : (Sigma.Lex rι rπ on fun c ↦ ⟨f c, g (f c) c⟩) c c'
h' : f c = f c'
h'' :
  rπ ((fun c ↦ ⟨f c, g (f c) c⟩) c').fst (h' ▸ ((fun c ↦ ⟨f c, g (f c) c⟩) c).snd) ((fun c ↦ ⟨f c, g (f c) c⟩) c').snd
⊢ ⟨⟨f c, ⋯⟩, ⟨c, ⋯⟩⟩ = ⟨⟨f c', ⋯⟩, ⟨c, h'⟩⟩

pp: case inr.convert_6
ι : Type u_1
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
hι : WellFounded (rι on f)
hπ : ∀ (i : ι), (f ⁻¹' {i}).WellFoundedOn (rπ i on g i)
c c' : γ
h : (Sigma.Lex rι rπ on fun c ↦ ⟨f c, g (f c) c⟩) c c'
h' : f c = f c'
h'' :
  rπ ((fun c ↦ ⟨f c, g (f c) c⟩) c').fst (h' ▸ ((fun c ↦ ⟨f c, g (f c) c⟩) c).snd) ((fun c ↦ ⟨f c, g (f c) c⟩) c').snd
⊢ Subrel (rπ ↑⟨f c', ⋯⟩ on g ↑⟨f c', ⋯⟩) (fun x ↦ x ∈ f ⁻¹' {↑⟨f c', ⋯⟩}) ⟨c, h'⟩ ⟨c', ⋯⟩

Tactic:
· exact PSigma.subtype_ext (Subtype.ext h') rfl

Goal state after:
case inr.convert_6
ι : Type u_1
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
hι : WellFounded (rι on f)
hπ : ∀ (i : ι), (f ⁻¹' {i}).WellFoundedOn (rπ i on g i)
c c' : γ
h : (Sigma.Lex rι rπ on fun c ↦ ⟨f c, g (f c) c⟩) c c'
h' : f c = f c'
h'' :
  rπ ((fun c ↦ ⟨f c, g (f c) c⟩) c').fst (h' ▸ ((fun c ↦ ⟨f c, g (f c) c⟩) c).snd) ((fun c ↦ ⟨f c, g (f c) c⟩) c').snd
⊢ Subrel (rπ ↑⟨f c', ⋯⟩ on g ↑⟨f c', ⋯⟩) (fun x ↦ x ∈ f ⁻¹' {↑⟨f c', ⋯⟩}) ⟨c, h'⟩ ⟨c', ⋯⟩
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set G
p : (x : G) → x ∈ closure s → Prop
one : p 1 ⋯
mul_left : ∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ closure s), p y hy → p (x * y) ⋯
inv_mul_cancel : ∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ closure s), p y hy → p (x⁻¹ * y) ⋯
x : G
h : x ∈ closure s
⊢ p x h

Tactic:
by
  revert h
  simp_rw [← mem_toSubmonoid, closure_toSubmonoid] at *
  intro h
  induction h using Submonoid.closure_induction_left with
  | one => exact one
  | mul_left x hx y hy ih =>
    cases hx with
    | inl hx => exact mul_left _ hx _ hy ih
    | inr hx => simpa only [inv_inv] using inv_mul_cancel _ hx _ hy ih

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

Goal state before:
pp: case cons
α : Type u_3
β : Type u_4
inst✝ : Monoid β
f g : α → β
x : α
s : Finset α
hnotMem : x ∉ s
ih :
  ∀ (comm_ff : (↑s).Pairwise (Commute on f)) (comm_gg : (↑s).Pairwise (Commute on g))
    (comm_gf : (↑s).Pairwise fun x y ↦ Commute (g x) (f y)),
    s.noncommProd (f * g) ⋯ = s.noncommProd f comm_ff * s.noncommProd g comm_gg
comm_ff : (↑(cons x s hnotMem)).Pairwise (Commute on f)
comm_gg : (↑(cons x s hnotMem)).Pairwise (Commute on g)
comm_gf : (↑(cons x s hnotMem)).Pairwise fun x y ↦ Commute (g x) (f y)
⊢ (cons x s hnotMem).noncommProd (f * g) ⋯ =
    (cons x s hnotMem).noncommProd f comm_ff * (cons x s hnotMem).noncommProd g comm_gg

Tactic:
| cons x s hnotMem ih =>

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

Goal state before:
pp: ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
⊢ univ.noncommProd (fun i ↦ Pi.mulSingle i (x i)) ⋯ = x

Tactic:
ext i

Goal state after:
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ univ.noncommProd (fun i ↦ Pi.mulSingle i (x i)) ⋯ i = x i
Module: Mathlib.Data.Setoid.Basic

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : ι → Sort u_5
r : (i : ι) → Setoid (α i)
q : Quotient piSetoid
x y : (i : ι) → α i
hxy : piSetoid x y
⊢ (fun i ↦ Quotient.mk'' (x i)) = fun i ↦ Quotient.mk'' (y i)

Tactic:
ext i

Goal state after:
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : ι → Sort u_5
r : (i : ι) → Setoid (α i)
q : Quotient piSetoid
x y : (i : ι) → α i
hxy : piSetoid x y
i : ι
⊢ Quotient.mk'' (x i) = Quotient.mk'' (y i)
Module: Mathlib.Data.Setoid.Basic

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : ι → Sort u_5
r : (i : ι) → Setoid (α i)
q : (i : ι) → Quotient (r i)
⊢ (fun q ↦ q.liftOn' (fun x i ↦ Quotient.mk'' (x i)) ⋯) ((fun x ↦ Quotient.mk'' fun i ↦ (x i).out) q) = q

Tactic:
ext i

Goal state after:
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : ι → Sort u_5
r : (i : ι) → Setoid (α i)
q : (i : ι) → Quotient (r i)
i : ι
⊢ (fun q ↦ q.liftOn' (fun x i ↦ Quotient.mk'' (x i)) ⋯) ((fun x ↦ Quotient.mk'' fun i ↦ (x i).out) q) i = q i
Module: Mathlib.GroupTheory.Congruence.Defs

Goal state before:
pp: case refine_2.refine_2
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
inst✝ : Monoid M
c : Con M
u : c.Quotientˣ
f : (x y : M) → c (x * y) 1 → c (y * x) 1 → α
Hf :
  ∀ (x y : M) (hxy : c (x * y) 1) (hyx : c (y * x) 1) (x' y' : M) (hxy' : c (x' * y') 1) (hyx' : c (y' * x') 1),
    c x x' → c y y' → f x y hxy hyx = f x' y' hxy' hyx'
x y x' y' : M
hx : c x x'
hy : c y y'
Hxy : ↑x * ↑y = 1
Hxy' : ↑x' * ↑y' = 1
⊢ ∀ (a : ↑y * ↑x = 1) (a' : ↑y' * ↑x' = 1), a ≍ a' → f x y ⋯ ⋯ ≍ f x' y' ⋯ ⋯

Tactic:
rintro Hyx Hyx' -
      exact heq_of_eq (Hf _ _ _ _ _ _ _ _ hx hy)

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

Goal state before:
pp: α : Type u
L₁ L₂ : List (α × Bool)
h : Red L₁ L₂
⊢ ∃ n, L₁.length = L₂.length + 2 * n

Tactic:
induction h with
  | refl => exact ⟨0, rfl⟩
  | tail _h₁₂ h₂₃ ih =>
    rcases ih with ⟨n, eq⟩
    exists 1 + n
    simp [Nat.mul_add, eq, (Step.length h₂₃).symm, add_assoc]

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

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : Unique α
x : FreeGroup α
⊢ (fun x ↦ of default ^ x) ((fun x ↦ ((map 1) x).sum) x) = x

Tactic:
induction x with

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

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : Unique α
x : ℤ
⊢ (fun x ↦ ((map 1) x).sum) ((fun x ↦ of default ^ x) x) = x

Tactic:
induction x with

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

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : Unique α
x : FreeAddGroup α
⊢ (fun x ↦ x • FreeAddGroup.of default) ((fun x ↦ FreeAddGroup.sum ((FreeAddGroup.map 1) x)) x) = x

Tactic:
induction x with

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
s : Finset ι
inst✝ : CommMonoid M
f : ↥s → M
⊢ ∏ x, f x = ∏ x ∈ s, extend Subtype.val f 1 x

Tactic:
by
  rw [univ_eq_attach, ← Finset.prod_attach s]
  congr with ⟨x, hx⟩
  rw [Subtype.val_injective.extend_apply]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : N.Normal
x y : G
⊢ x⁻¹ * y ∈ N ↔ ∃ z ∈ N, x * z = y

Tactic:
simp only [← _root_.eq_inv_mul_iff_mul_eq, exists_eq_right]

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
P : Submonoid M
Q : Submonoid N
hP : P.FG
hQ : Q.FG
⊢ (P.prod Q).FG

Tactic:
by
  classical
  obtain ⟨bM, hbM⟩ := hP
  obtain ⟨bN, hbN⟩ := hQ
  refine ⟨bM ×ˢ singleton 1 ∪ singleton 1 ×ˢ bN, ?_⟩
  push_cast
  simp [closure_union, hbM, hbN]

Goal state after: