mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: case coe.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : WithTop α
a✝ : α
⊢ (x ∈
      match ↑a✝, ⊤ with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ico a b)) ↔
    ↑a✝ ≤ x ∧ x < ⊤

Tactic:
cases x

Goal state after:
case coe.top.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝ : α
⊢ (⊤ ∈
      match ↑a✝, ⊤ with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ico a b)) ↔
    ↑a✝ ≤ ⊤ ∧ ⊤ < ⊤

case coe.top.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝¹ a✝ : α
⊢ (↑a✝ ∈
      match ↑a✝¹, ⊤ with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ico a b)) ↔
    ↑a✝¹ ≤ ↑a✝ ∧ ↑a✝ < ⊤
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: case coe.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : WithTop α
a✝¹ a✝ : α
⊢ (x ∈
      match ↑a✝¹, ↑a✝ with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ico a b)) ↔
    ↑a✝¹ ≤ x ∧ x < ↑a✝

Tactic:
cases x

Goal state after:
case coe.coe.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝¹ a✝ : α
⊢ (⊤ ∈
      match ↑a✝¹, ↑a✝ with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ico a b)) ↔
    ↑a✝¹ ≤ ⊤ ∧ ⊤ < ↑a✝

case coe.coe.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝² a✝¹ a✝ : α
⊢ (↑a✝ ∈
      match ↑a✝², ↑a✝¹ with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ico a b)) ↔
    ↑a✝² ≤ ↑a✝ ∧ ↑a✝ < ↑a✝¹
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: case inr.mpr.inl.refine_2
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ i + a * (n / a + 1) < n + a

pp: case inr.mpr.inl.refine_3
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ (i + a * (n / a + 1)) % a = i

Tactic:
· refine lt_of_lt_of_le (Nat.add_lt_add_right hi (a * (n / a + 1))) ?_
      rw [Nat.mul_add, mul_one, ← add_assoc, hn]

Goal state after:
case inr.mpr.inl.refine_3
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ (i + a * (n / a + 1)) % a = i
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ WellFoundedGT α ↔ ∀ (a : ℕ →o α), ∃ n, ∀ (m : ℕ), n ≤ m → ¬a n < a m

Tactic:
refine ⟨fun h a => ?_, fun h => ?_⟩
  · obtain ⟨x, ⟨n, rfl⟩, H⟩ := h.wf.has_min _ (Set.range_nonempty a)
    exact ⟨n, fun m _ => H _ (Set.mem_range_self _)⟩
  · rw [WellFoundedGT, isWellFounded_iff, RelEmbedding.wellFounded_iff_isEmpty]
    refine ⟨fun a => ?_⟩
    obtain ⟨n, hn⟩ := h (a.swap : _ →r _).toOrderHom
    exact hn n.succ n.lt_succ_self.le ((RelEmbedding.map_rel_iff _).2 n.lt_succ_self)

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

Goal state before:
pp: case top.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : WithTop α
⊢ (x ∈
      match ⊤, ⊤ with
      | none, x => ∅
      | Option.some a, none => insertTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioc a b)) ↔
    ⊤ < x ∧ x ≤ ⊤

Tactic:
cases x

Goal state after:
case top.top.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
⊢ (⊤ ∈
      match ⊤, ⊤ with
      | none, x => ∅
      | Option.some a, none => insertTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioc a b)) ↔
    ⊤ < ⊤ ∧ ⊤ ≤ ⊤

case top.top.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝ : α
⊢ (↑a✝ ∈
      match ⊤, ⊤ with
      | none, x => ∅
      | Option.some a, none => insertTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioc a b)) ↔
    ⊤ < ↑a✝ ∧ ↑a✝ ≤ ⊤
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: case top.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : WithTop α
a✝ : α
⊢ (x ∈
      match ⊤, ↑a✝ with
      | none, x => ∅
      | Option.some a, none => insertTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioc a b)) ↔
    ⊤ < x ∧ x ≤ ↑a✝

Tactic:
cases x

Goal state after:
case top.coe.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝ : α
⊢ (⊤ ∈
      match ⊤, ↑a✝ with
      | none, x => ∅
      | Option.some a, none => insertTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioc a b)) ↔
    ⊤ < ⊤ ∧ ⊤ ≤ ↑a✝

case top.coe.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝¹ a✝ : α
⊢ (↑a✝ ∈
      match ⊤, ↑a✝¹ with
      | none, x => ∅
      | Option.some a, none => insertTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioc a b)) ↔
    ⊤ < ↑a✝ ∧ ↑a✝ ≤ ↑a✝¹
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: case coe.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : WithTop α
a✝ : α
⊢ (x ∈
      match ↑a✝, ⊤ with
      | none, x => ∅
      | Option.some a, none => insertTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioc a b)) ↔
    ↑a✝ < x ∧ x ≤ ⊤

Tactic:
cases x

Goal state after:
case coe.top.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝ : α
⊢ (⊤ ∈
      match ↑a✝, ⊤ with
      | none, x => ∅
      | Option.some a, none => insertTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioc a b)) ↔
    ↑a✝ < ⊤ ∧ ⊤ ≤ ⊤

case coe.top.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝¹ a✝ : α
⊢ (↑a✝ ∈
      match ↑a✝¹, ⊤ with
      | none, x => ∅
      | Option.some a, none => insertTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioc a b)) ↔
    ↑a✝¹ < ↑a✝ ∧ ↑a✝ ≤ ⊤
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: case coe.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : WithTop α
a✝¹ a✝ : α
⊢ (x ∈
      match ↑a✝¹, ↑a✝ with
      | none, x => ∅
      | Option.some a, none => insertTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioc a b)) ↔
    ↑a✝¹ < x ∧ x ≤ ↑a✝

Tactic:
cases x

Goal state after:
case coe.coe.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝¹ a✝ : α
⊢ (⊤ ∈
      match ↑a✝¹, ↑a✝ with
      | none, x => ∅
      | Option.some a, none => insertTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioc a b)) ↔
    ↑a✝¹ < ⊤ ∧ ⊤ ≤ ↑a✝

case coe.coe.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝² a✝¹ a✝ : α
⊢ (↑a✝ ∈
      match ↑a✝², ↑a✝¹ with
      | none, x => ∅
      | Option.some a, none => insertTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioc a b)) ↔
    ↑a✝² < ↑a✝ ∧ ↑a✝ ≤ ↑a✝¹
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: case mp
α : Type u_1
r : α → α → Prop
inst✝ : IsPreorder α r
⊢ WellQuasiOrdered r → ∀ (f : ℕ → α), ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))

Tactic:
intro h

Goal state after:
case mp
α : Type u_1
r : α → α → Prop
inst✝ : IsPreorder α r
h : WellQuasiOrdered r
⊢ ∀ (f : ℕ → α), ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: case mpr
α : Type u_1
r : α → α → Prop
inst✝ : IsPreorder α r
⊢ (∀ (f : ℕ → α), ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))) → WellQuasiOrdered r

Tactic:
intro h

Goal state after:
case mpr
α : Type u_1
r : α → α → Prop
inst✝ : IsPreorder α r
h : ∀ (f : ℕ → α), ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))
⊢ WellQuasiOrdered r
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: case top.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : WithTop α
⊢ (x ∈
      match ⊤, ⊤ with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioo a b)) ↔
    ⊤ < x ∧ x < ⊤

Tactic:
cases x

Goal state after:
case top.top.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
⊢ (⊤ ∈
      match ⊤, ⊤ with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioo a b)) ↔
    ⊤ < ⊤ ∧ ⊤ < ⊤

case top.top.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝ : α
⊢ (↑a✝ ∈
      match ⊤, ⊤ with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioo a b)) ↔
    ⊤ < ↑a✝ ∧ ↑a✝ < ⊤
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: case top.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : WithTop α
a✝ : α
⊢ (x ∈
      match ⊤, ↑a✝ with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioo a b)) ↔
    ⊤ < x ∧ x < ↑a✝

Tactic:
cases x

Goal state after:
case top.coe.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝ : α
⊢ (⊤ ∈
      match ⊤, ↑a✝ with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioo a b)) ↔
    ⊤ < ⊤ ∧ ⊤ < ↑a✝

case top.coe.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝¹ a✝ : α
⊢ (↑a✝ ∈
      match ⊤, ↑a✝¹ with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioo a b)) ↔
    ⊤ < ↑a✝ ∧ ↑a✝ < ↑a✝¹
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: case coe.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : WithTop α
a✝ : α
⊢ (x ∈
      match ↑a✝, ⊤ with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioo a b)) ↔
    ↑a✝ < x ∧ x < ⊤

Tactic:
cases x

Goal state after:
case coe.top.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝ : α
⊢ (⊤ ∈
      match ↑a✝, ⊤ with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioo a b)) ↔
    ↑a✝ < ⊤ ∧ ⊤ < ⊤

case coe.top.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝¹ a✝ : α
⊢ (↑a✝ ∈
      match ↑a✝¹, ⊤ with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioo a b)) ↔
    ↑a✝¹ < ↑a✝ ∧ ↑a✝ < ⊤
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: case coe.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : WithTop α
a✝¹ a✝ : α
⊢ (x ∈
      match ↑a✝¹, ↑a✝ with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioo a b)) ↔
    ↑a✝¹ < x ∧ x < ↑a✝

Tactic:
cases x

Goal state after:
case coe.coe.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝¹ a✝ : α
⊢ (⊤ ∈
      match ↑a✝¹, ↑a✝ with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioo a b)) ↔
    ↑a✝¹ < ⊤ ∧ ⊤ < ↑a✝

case coe.coe.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝² a✝¹ a✝ : α
⊢ (↑a✝ ∈
      match ↑a✝², ↑a✝¹ with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioo a b)) ↔
    ↑a✝² < ↑a✝ ∧ ↑a✝ < ↑a✝¹
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DenselyOrdered α
a b : α
⊢ ¬a < b

Tactic:
intro h

Goal state after:
α : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DenselyOrdered α
a b : α
h : a < b
⊢ False
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrder α
⊢ Ioo a b ⊆ Ioi a

Tactic:
simpa [← coe_subset] using Set.Ioo_subset_Ioi_self

Goal state after:
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 α
U V : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
⊢ (∀ x ∈ U, ∀ (g : G), g • x ∉ V) → Disjoint (f '' U) (f '' V)

Tactic:
intro h

Goal state after:
case refine_2
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U V : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
h : ∀ x ∈ U, ∀ (g : G), g • x ∉ V
⊢ Disjoint (f '' U) (f '' V)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
a b : α
⊢ [[a, b]] = [[b, a]]

Tactic:
rw [uIcc, uIcc, inf_comm, sup_comm]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
ϕ : G ≃* G
g : G
hg : g ∈ comap ϕ.toMonoidHom (center G)
⊢ ∀ (g_1 : G), g_1 * g = g * g_1

Tactic:
intro h

Goal state after:
G : Type u_1
inst✝ : Group G
ϕ : G ≃* G
g : G
hg : g ∈ comap ϕ.toMonoidHom (center G)
h : G
⊢ h * g = g * h
Module: Mathlib.GroupTheory.Subgroup.Center

Goal state before:
pp: case refine_3.mk
G : Type u_2
inst✝ : Group G
a✝ : ConjClasses G
g : G
hg : (carrier (Quot.mk (⇑(IsConj.setoid G)) g)).Subsingleton
⊢ ∀ (g_1 : G), g_1 * g = g * g_1

Tactic:
intro h

Goal state after:
case refine_3.mk
G : Type u_2
inst✝ : Group G
a✝ : ConjClasses G
g : G
hg : (carrier (Quot.mk (⇑(IsConj.setoid G)) g)).Subsingleton
h : G
⊢ h * g = g * h
Module: Mathlib.GroupTheory.Subgroup.Centralizer

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

Tactic:
simpa using hh _ rfl

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: ι : Type u_1
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
s : Set γ
hι : s.WellFoundedOn (rι on f)
hπ : ∀ (i : ι), (s ∩ f ⁻¹' {i}).WellFoundedOn (rπ i on g i)
⊢ s.WellFoundedOn (Sigma.Lex rι rπ on fun c ↦ ⟨f c, g (f c) c⟩)

Tactic:
change WellFounded (Sigma.Lex rι rπ on fun c : s => ⟨f c, g (f c) c⟩)

Goal state after:
ι : Type u_1
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
s : Set γ
hι : s.WellFoundedOn (rι on f)
hπ : ∀ (i : ι), (s ∩ f ⁻¹' {i}).WellFoundedOn (rπ i on g i)
⊢ WellFounded (Sigma.Lex rι rπ on fun c ↦ ⟨f ↑c, g (f ↑c) ↑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 ⋯
x : G
mul_left : ∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ Submonoid.closure (s ∪ s⁻¹)), p y ⋯ → p (x * y) ⋯
inv_mul_cancel : ∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ Submonoid.closure (s ∪ s⁻¹)), p y ⋯ → p (x⁻¹ * y) ⋯
⊢ ∀ (h : x ∈ Submonoid.closure (s ∪ s⁻¹)), p x ⋯

Tactic:
intro h

Goal state after:
G : Type u_2
inst✝ : Group G
s : Set G
p : (x : G) → x ∈ closure s → Prop
one : p 1 ⋯
x : G
mul_left : ∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ Submonoid.closure (s ∪ s⁻¹)), p y ⋯ → p (x * y) ⋯
inv_mul_cancel : ∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ Submonoid.closure (s ∪ s⁻¹)), p y ⋯ → p (x⁻¹ * y) ⋯
h : x ∈ Submonoid.closure (s ∪ s⁻¹)
⊢ p x ⋯
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_3
inst✝ : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
e : ι ≃ κ
hst : ∀ (i : ι), i ∈ s ↔ e i ∈ t
hfg : ∀ i ∈ s, f i = g (e i)
⊢ ∏ i ∈ s, f i = ∏ i ∈ t, g i

Tactic:
refine prod_nbij' e e.symm ?_ ?_ ?_ ?_ hfg <;> simp [hst]

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f : α → β
comm : (↑s).Pairwise (Commute on f)
p : β → Prop
hom : ∀ (a b : β), p a → p b → p (a * b)
unit : p 1
base : ∀ x ∈ s, p (f x)
b : β
hb : b ∈ Multiset.map f s.val
⊢ ?m.28

Tactic:
simpa using hb

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

Goal state before:
pp: α : Type u
L L' : List (α × Bool)
h' : [] = L'
⊢ ¬Step L' L

Tactic:
intro h

Goal state after:
α : Type u
L L' : List (α × Bool)
h' : [] = L'
h : Step L' L
⊢ False
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
L₁ L₂ : List (α × Bool)
p : α × Bool
LL₁ : List (α × Bool)
eq₁ : p :: L₁ = LL₁
LL₂ : List (α × Bool)
eq₂ : p :: L₂ = LL₂
⊢ Red LL₁ LL₂ → Red L₁ L₂

Tactic:
intro h

Goal state after:
α : Type u
L₁ L₂ : List (α × Bool)
p : α × Bool
LL₁ : List (α × Bool)
eq₁ : p :: L₁ = LL₁
LL₂ : List (α × Bool)
eq₂ : p :: L₂ = LL₂
h : Red LL₁ LL₂
⊢ Red L₁ L₂
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
L L₁ L₂ L₁₂ : List (α × Bool)
eq : L₁ ++ L₂ = L₁₂
⊢ Red L L₁₂ → ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂

Tactic:
intro h

Goal state after:
α : Type u
L L₁ L₂ L₁₂ : List (α × Bool)
eq : L₁ ++ L₂ = L₁₂
h : Red L L₁₂
⊢ ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq κ
s : Finset ι
t : Finset κ
g : ι → κ
f : ι → M
⊢ ∏ j ∈ t, ∏ i ∈ s with g i = j, f i = ∏ i ∈ s with g i ∈ t, f i

Tactic:
rw [← prod_disjiUnion, disjiUnion_filter_eq]

Goal state after:
case h
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq κ
s : Finset ι
t : Finset κ
g : ι → κ
f : ι → M
⊢ (↑t).PairwiseDisjoint fun j ↦ {i ∈ s | g i = j}
Module: Mathlib.GroupTheory.Congruence.Hom

Goal state before:
pp: case mp
M : Type u_1
N : Type u_2
P : Type u_3
F : Type ?u.18
inst✝⁴ : Mul M
inst✝³ : Mul N
inst✝² : Mul P
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
c : Con M
s t : { d // c ≤ d }
⊢ { toFun := fun d ↦ mapOfSurjective c.mkMulHom ⋯ ⋯, invFun := fun d ↦ ⟨comap toQuotient ⋯ d, ⋯⟩, left_inv := ⋯,
          right_inv := ⋯ }
        s ≤
      { toFun := fun d ↦ mapOfSurjective c.mkMulHom ⋯ ⋯, invFun := fun d ↦ ⟨comap toQuotient ⋯ d, ⋯⟩, left_inv := ⋯,
          right_inv := ⋯ }
        t →
    s ≤ t

Tactic:
intro h

Goal state after:
case mp
M : Type u_1
N : Type u_2
P : Type u_3
F : Type ?u.18
inst✝⁴ : Mul M
inst✝³ : Mul N
inst✝² : Mul P
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
c : Con M
s t : { d // c ≤ d }
h :
  { toFun := fun d ↦ mapOfSurjective c.mkMulHom ⋯ ⋯, invFun := fun d ↦ ⟨comap toQuotient ⋯ d, ⋯⟩, left_inv := ⋯,
        right_inv := ⋯ }
      s ≤
    { toFun := fun d ↦ mapOfSurjective c.mkMulHom ⋯ ⋯, invFun := fun d ↦ ⟨comap toQuotient ⋯ d, ⋯⟩, left_inv := ⋯,
        right_inv := ⋯ }
      t
⊢ s ≤ t
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case nil
α : Type u
L2 : List (α × Bool)
x : α
b : Bool
⊢ sizeOf L2 < 1 + sizeOf (x, b) + sizeOf ((x, !b) :: L2)

Tactic:
cons.sizeOf_spec

Goal state after:
case nil
α : Type u
L2 : List (α × Bool)
x : α
b : Bool
⊢ sizeOf L2 < 1 + sizeOf (x, b) + (1 + sizeOf (x, !b) + sizeOf L2)
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 ι
hs : ∀ a ∈ s₁, a ∉ s₂ → f a = 1
⊢ ∏ a ∈ s₁ ∪ s₂, f a = ∏ a ∈ s₂, f a

Tactic:
union_comm,

Goal state after:
ι : Type u_1
M : Type u_4
s₁ s₂ : Finset ι
inst✝¹ : CommMonoid M
f : ι → M
inst✝ : DecidableEq ι
hs : ∀ a ∈ s₁, a ∉ s₂ → f a = 1
⊢ ∏ a ∈ s₂ ∪ s₁, f a = ∏ a ∈ s₂, f a
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case refine_1
G : Type u_3
inst✝ : Group G
x✝ : FG G
S : Finset G
hS : Subgroup.closure ↑S = ⊤
⊢ Function.Surjective ⇑(FreeGroup.lift Subtype.val)

Tactic:
rwa [← MonoidHom.range_eq_top, ← FreeGroup.closure_eq_range]

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a : ι
hp : ∏ x ∈ s, f x = 1
h1 : ∀ x ∈ s, x ≠ a → f x = 1
x : ι
hx : x ∈ s
⊢ f x = 1

Tactic:
by_cases h : x = a

Goal state after:
case pos
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a : ι
hp : ∏ x ∈ s, f x = 1
h1 : ∀ x ∈ s, x ≠ a → f x = 1
x : ι
hx : x ∈ s
h : x = a
⊢ f x = 1

case neg
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a : ι
hp : ∏ x ∈ s, f x = 1
h1 : ∀ x ∈ s, x ≠ a → f x = 1
x : ι
hx : x ∈ s
h : ¬x = a
⊢ f x = 1
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
x : α
⊢ of x ≠ 0

Tactic:
intro h

Goal state after:
α : Type u
x : α
h : of x = 0
⊢ False
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
inst✝ : Mul α
x y : α
⊢ of x * of y = of (x * y)

Tactic:
mul_def,

Goal state after:
α : Type u
inst✝ : Mul α
x y : α
⊢ (lift fun x₂ ↦ (lift fun x₁ ↦ of (x₁ * x₂)) (of x)) (of y) = of (x * y)
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
inst✝² : Group G
H₁ H₂ : Subgroup G
inst✝¹ : H₁.Normal
inst✝ : H₂.Normal
h : Disjoint H₁ H₂
⊢ ⁅H₁, H₂⁆ ≤ ⊥

Tactic:
commutator_le_inf,

Goal state after:
G : Type u_1
inst✝² : Group G
H₁ H₂ : Subgroup G
inst✝¹ : H₁.Normal
inst✝ : H₂.Normal
h : Disjoint H₁ H₂
⊢ H₁ ⊓ H₂ ≤ ⊥
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
x : FreeAbelianGroup α
⊢ 1 * x = x

Tactic:
mul_def,

Goal state after:
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
x : FreeAbelianGroup α
⊢ (lift fun x₂ ↦ (lift fun x₁ ↦ of (x₁ * x₂)) 1) x = x
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
x : FreeAbelianGroup α
⊢ x * 1 = x

Tactic:
mul_def,

Goal state after:
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
x : FreeAbelianGroup α
⊢ (lift fun x₂ ↦ (lift fun x₁ ↦ of (x₁ * x₂)) x) 1 = x