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

Goal state before:
pp: α : Type u_1
σ : α → Type u_4
s✝ : Multiset α
a : α
s : Multiset α
IH : ∀ (t u : (a : α) → Multiset (σ a)), (s.sigma fun a ↦ t a + u a) = s.sigma t + s.sigma u
t u : (a : α) → Multiset (σ a)
⊢ ((a ::ₘ s).sigma fun a ↦ t a + u a) = (a ::ₘ s).sigma t + (a ::ₘ s).sigma u

Tactic:
by
    rw [cons_sigma, IH]
    simp [add_comm, add_left_comm, add_assoc]

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

Goal state before:
pp: n : ℕ
⊢ n.choose 1 = n

Tactic:
by induction n <;> simp [*, choose, Nat.add_comm]

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

Goal state before:
pp: α : Type u_1
s : Finset α
x : α × α
⊢ x ∈ s.diag ↔ x.1 ∈ s ∧ x.1 = x.2

Tactic:
by
  aesop (add simp diag)

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
m✝ : Multiset α
t : (a : α) → Multiset (β a)
a a' : α
m : Multiset α
n : Multiset ((a : α) → a ∈ m → β a)
eq : ¬a = a'
⊢ ((t a).bind fun b ↦ map (Pi.cons (a' ::ₘ m) a b) ((t a').bind fun b ↦ map (Pi.cons m a' b) n)) ≍
    (t a').bind fun b ↦ map (Pi.cons (a ::ₘ m) a' b) ((t a).bind fun b ↦ map (Pi.cons m a b) n)

Tactic:
· simp only [map_bind, map_map, comp_apply, bind_bind (t a') (t a)]
        apply bind_hcongr
        · rw [cons_swap a a']
        intro b _
        apply bind_hcongr
        · rw [cons_swap a a']
        intro b' _
        apply map_hcongr
        · rw [cons_swap a a']
        intro f _
        exact Pi.cons_swap eq

Goal state after:
Module: Mathlib.Algebra.Group.Action.Hom

Goal state before:
pp: E : Type u_4
F : Type u_5
G : Type u_6
inst✝³ : Monoid E
inst✝² : Monoid F
inst✝¹ : MulAction F G
inst✝ : IsPretransitive F G
f : E →* F
hf : Surjective ⇑f
⊢ IsPretransitive E G

Tactic:
let _ : MulAction E G := MulAction.compHom _ f

Goal state after:
E : Type u_4
F : Type u_5
G : Type u_6
inst✝³ : Monoid E
inst✝² : Monoid F
inst✝¹ : MulAction F G
inst✝ : IsPretransitive F G
f : E →* F
hf : Surjective ⇑f
x✝ : MulAction E G := compHom G f
⊢ IsPretransitive E G
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : DivisionMonoid α
s✝ t✝ : Set α
n : ℤ
s t : Set α
⊢ (s * t)⁻¹ = t⁻¹ * s⁻¹

Tactic:
simp_rw [← image_inv_eq_inv]
      exact image_image2_antidistrib mul_inv_rev

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Group α
a b : α
⊢ (fun x ↦ a * x) ⁻¹' {b} = {a⁻¹ * b}

Tactic:
by
  rw [← image_mul_left', image_singleton]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
k : Set G
p : (x y : G) → x ∈ closure k → y ∈ closure k → Prop
mem : ∀ (x y : G) (hx : x ∈ k) (hy : y ∈ k), p x y ⋯ ⋯
one_left : ∀ (x : G) (hx : x ∈ closure k), p 1 x ⋯ hx
one_right : ∀ (x : G) (hx : x ∈ closure k), p x 1 hx ⋯
mul_left :
  ∀ (x y z : G) (hx : x ∈ closure k) (hy : y ∈ closure k) (hz : z ∈ closure k),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (y z x : G) (hy : y ∈ closure k) (hz : z ∈ closure k) (hx : x ∈ closure k),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
inv_left : ∀ (x y : G) (hx : x ∈ closure k) (hy : y ∈ closure k), p x y hx hy → p x⁻¹ y ⋯ hy
inv_right : ∀ (x y : G) (hx : x ∈ closure k) (hy : y ∈ closure k), p x y hx hy → p x y⁻¹ hx ⋯
x y : G
hx : x ∈ closure k
hy : y ∈ closure k
⊢ p 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₂
    | inv _ _ h => exact inv_left _ _ _ _ h
  | one => exact one_right x hx
  | mul _ _ _ _ h₁ h₂ => exact mul_right _ _ _ _ _ hx h₁ h₂
  | inv _ _ h => exact inv_right _ _ _ _ h

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
N : Type u_5
inst✝¹ : Group N
P : Type u_8
inst✝ : MulOneClass P
g : N →* P
iso : G ≃* N
⊢ (g.comp ↑iso).ker = map (↑iso.symm) g.ker

Tactic:
by
  rw [← comap_ker, comap_equiv_eq_map_symm]

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

Goal state before:
pp: case mpr
N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
hH : map (inl M N) s ≤ u
hK : map (inr M N) t ≤ u
x1 : M
x2 : N
h1 : (x1, x2).1 ∈ ↑s
h2 : (x1, x2).2 ∈ ↑t
h1' : (inl M N) x1 ∈ u
⊢ (x1, x2) ∈ u

Tactic:
have h2' : inr M N x2 ∈ u := by
      apply hK
      simpa using h2

Goal state after:
case mpr
N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
hH : map (inl M N) s ≤ u
hK : map (inr M N) t ≤ u
x1 : M
x2 : N
h1 : (x1, x2).1 ∈ ↑s
h2 : (x1, x2).2 ∈ ↑t
h1' : (inl M N) x1 ∈ u
h2' : (inr M N) x2 ∈ u
⊢ (x1, x2) ∈ u
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
g : N →* P
f : M →* N
⊢ map g (mrange f) = mrange (g.comp f)

Tactic:
simpa only [mrange_eq_map] using (⊤ : Submonoid M).map_map g f

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

Goal state before:
pp: M✝ : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M✝
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M✝
M : Type u_4
inst✝ : Monoid M
x y : Mˣ
⊢ ⟨↑(x * y), ⋯⟩ = ⟨↑x, ⋯⟩ * ⟨↑y, ⋯⟩

Tactic:
Units.val_mul

Goal state after:
M✝ : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M✝
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M✝
M : Type u_4
inst✝ : Monoid M
x y : Mˣ
⊢ ⟨↑x * ↑y, ⋯⟩ = ⟨↑x, ⋯⟩ * ⟨↑y, ⋯⟩
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: case inl
m n : ℕ
h : m < n
⊢ max m n ^ 2 + min m n ≤ if m < n then n * n + m else m * m + m + n

Tactic:
if_pos h,

Goal state after:
case inl
m n : ℕ
h : m < n
⊢ max m n ^ 2 + min m n ≤ n * n + m
Module: Mathlib.Algebra.FreeMonoid.Basic

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
head✝ : M
xs : List M
⊢ prodAux (head✝ :: xs) = (head✝ :: xs).prod

Tactic:
simp [prodAux, List.prod_eq_foldl]

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

Goal state before:
pp: M : Type u_1
inst✝¹ : MulOneClass M
ι : Sort u_4
inst✝ : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : M
⊢ x ∈ ⨆ i, S i ↔ ∃ i, x ∈ S i

Tactic:
by
  refine ⟨?_, fun ⟨i, hi⟩ ↦ le_iSup S i hi⟩
  suffices x ∈ closure (⋃ i, (S i : Set M)) → ∃ i, x ∈ S i by
    simpa only [closure_iUnion, closure_eq (S _)] using this
  refine fun hx ↦ closure_induction (by simp) (by simp) ?_ hx
  rintro x y _ _ ⟨i, hi⟩ ⟨j, hj⟩
  obtain ⟨k, hik, hjk⟩ := hS i j
  exact ⟨k, mul_mem (hik hi) (hjk hj)⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : NoMaxOrder β
inst✝ : DenselyOrdered β
x y : Lex (α × β)
h : x < y
⊢ ∃ a, x < a ∧ a < y

Tactic:
cases x with | h x
    cases y with | h y
    simp only [Prod.Lex.toLex_lt_toLex] at h
    rcases h with (h | h)
    · obtain ⟨v, hv⟩ := exists_gt x.2
      use toLex (x.1, v)
      simp [Prod.Lex.toLex_lt_toLex, h, hv]
    · obtain ⟨v, htv, hvu⟩ := DenselyOrdered.dense x.2 y.2 h.2
      use toLex (x.1, v)
      simp [Prod.Lex.toLex_lt_toLex, h.1, htv, hvu]

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

Goal state before:
pp: A : Type u_2
inst✝ : AddMonoid A
⊢ closure {0} = ⊥

Tactic:
simp [eq_bot_iff_forall, mem_closure_singleton, nsmul_zero]

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

Goal state before:
pp: α : Type u
a : α
r₁ r₂ : List (List α)
⊢ sublists'Aux a r₁ r₂ = (Array.foldl (fun r l ↦ r.push (a :: l)) r₂.toArray r₁.toArray).toList

Tactic:
sublists'Aux,

Goal state after:
α : Type u
a : α
r₁ r₂ : List (List α)
⊢ foldl (fun r l ↦ r ++ [a :: l]) r₂ r₁ = (Array.foldl (fun r l ↦ r.push (a :: l)) r₂.toArray r₁.toArray).toList
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : Monotone f
s : Finset α
h : (image f s).Nonempty
⊢ s.inf' ⋯ (id ∘ f) = f (s.inf' ⋯ id)

Tactic:
exact .symm <| apply_inf'_eq_inf'_comp _ _ fun _ _ ↦ hf.map_min

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

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

Tactic:
simp [sublists'Aux]

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₂ = sublists'Aux a r₁ r₂ ++ [a :: l]

Tactic:
sublists'Aux,

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 α)
⊢ foldl (fun r l ↦ r ++ [a :: l]) r₂ (r₁ ++ [l]) = sublists'Aux a r₁ r₂ ++ [a :: l]
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 α)
⊢ foldl (fun r l ↦ r ++ [a :: l]) (foldl (fun r l ↦ r ++ [a :: l]) r₂ r₁ ++ [a :: l]) [] =
    sublists'Aux a r₁ r₂ ++ [a :: l]

Tactic:
simp [sublists'Aux]

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

Goal state before:
pp: case H.inl
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : DecidableEq α
motive : Finset α → Prop
empty : motive ∅
insert : ∀ (a : α) (s : Finset α), (∀ x ∈ s, x < a) → motive s → motive (Insert.insert a s)
ih : ∀ s ∈ ∅, motive (∅.erase s)
⊢ motive ∅

pp: case H.inr
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : DecidableEq α
motive : Finset α → Prop
empty : motive ∅
insert : ∀ (a : α) (s : Finset α), (∀ x ∈ s, x < a) → motive s → motive (Insert.insert a s)
s : Finset α
ih : ∀ s_1 ∈ s, motive (s.erase s_1)
hne : s.Nonempty
⊢ motive s

Tactic:
· exact empty

Goal state after:
case H.inr
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : DecidableEq α
motive : Finset α → Prop
empty : motive ∅
insert : ∀ (a : α) (s : Finset α), (∀ x ∈ s, x < a) → motive s → motive (Insert.insert a s)
s : Finset α
ih : ∀ s_1 ∈ s, motive (s.erase s_1)
hne : s.Nonempty
⊢ motive s
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: α : Type u_1
l : List α
x : Multiset α × Multiset α
h : ∃ a, a ∈ l.sublists.revzip ∧ Prod.map ofList ofList a = x
⊢ x.1 + x.2 = ↑l

Tactic:
simp only [Prod.map_apply, Prod.exists] at h

Goal state after:
α : Type u_1
l : List α
x : Multiset α × Multiset α
h : ∃ a b, (a, b) ∈ l.sublists.revzip ∧ (↑a, ↑b) = x
⊢ x.1 + x.2 = ↑l
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: α : Type u_1
l : List α
x : Multiset α × Multiset α
h : ∃ a, a ∈ l.sublists'.revzip ∧ Prod.map ofList ofList a = x
⊢ x.1 + x.2 = ↑l

Tactic:
simp only [Prod.map_apply, Prod.exists] at h

Goal state after:
α : Type u_1
l : List α
x : Multiset α × Multiset α
h : ∃ a b, (a, b) ∈ l.sublists'.revzip ∧ (↑a, ↑b) = x
⊢ x.1 + x.2 = ↑l
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
⊢ (s.sup fun x ↦ ⊥) = ⊥

Tactic:
by
  obtain rfl | hs := s.eq_empty_or_nonempty
  · exact sup_empty
  · exact sup_const hs _

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

pp: case inl.refine_2
α : 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, j') ≤ (fun i' ↦ ⨆ i ∈ s, f (i, i')) (i, j').2

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

Goal state after:
case inl.refine_2
α : 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, j') ≤ (fun i' ↦ ⨆ i ∈ s, f (i, i')) (i, j').2
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
h : s.Nonempty
⊢ ∅ ⊂ s

Tactic:
ssubset_iff_subset_ne

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
h : s.Nonempty
⊢ ∅ ⊆ s ∧ ∅ ≠ s
Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed

Goal state before:
pp: case inr
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompletePartialOrderSup α
f g : ι → α
hdf : Directed (fun x1 x2 ↦ x1 ≤ x2) f
hdg : Directed (fun x1 x2 ↦ x1 ≤ x2) g
B : BddAbove (range g)
H : ∀ (x : ι), f x ≤ g x
h✝ : Nonempty ι
⊢ iSup f ≤ iSup g

Tactic:
exact hdf.ciSup_le fun x ↦ hdg.le_ciSup_of_le B x (H x)

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

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

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

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ some ⁻¹' Iio ⊤ = univ

Tactic:
by
  rw [← range_coe, preimage_range]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CompleteLattice β
inst✝ : DecidableEq α
x : α
t : Finset α
f : α → β
s : β
hx : x ∉ t
⊢ ⨆ i ∈ insert x t, update f x s i = s ⊔ ⨆ i ∈ t, f i

Tactic:
Finset.iSup_insert

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : CompleteLattice β
inst✝ : DecidableEq α
x : α
t : Finset α
f : α → β
s : β
hx : x ∉ t
⊢ update f x s x ⊔ ⨆ x_1 ∈ t, update f x s x_1 = s ⊔ ⨆ i ∈ t, f i
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ (Finset.Ico a b \ Finset.Ico a c).val = (Finset.Ico (max a c) b).val

Tactic:
Finset.Ico_sdiff_Ico_left

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ (Finset.Ico (max a c) b).val = (Finset.Ico (max a c) b).val
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a : ℕ
h : 0 < a
⊢ Ico (a - 1) a = {a - 1}

Tactic:
by
  ext x
  rw [mem_Ico, mem_singleton]
  lia

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀_finset_Icc h₀_finset_Ico h₀_finset_Ioc h₀_finset_Ioo : α → α → Finset α
h₀_finset_mem_Icc : ∀ (a b x : α), x ∈ h₀_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₀_finset_mem_Ico : ∀ (a b x : α), x ∈ h₀_finset_Ico a b ↔ a ≤ x ∧ x < b
h₀_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₀_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₀_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₀_finset_Ioo a b ↔ a < x ∧ x < b
h₁_finset_Icc h₁_finset_Ico h₁_finset_Ioc h₁_finset_Ioo : α → α → Finset α
h₁_finset_mem_Icc : ∀ (a b x : α), x ∈ h₁_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₁_finset_mem_Ico : ∀ (a b x : α), x ∈ h₁_finset_Ico a b ↔ a ≤ x ∧ x < b
h₁_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₁_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₁_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₁_finset_Ioo a b ↔ a < x ∧ x < b
⊢ { finsetIcc := h₀_finset_Icc, finsetIco := h₀_finset_Ico, finsetIoc := h₀_finset_Ioc, finsetIoo := h₀_finset_Ioo,
      finset_mem_Icc := h₀_finset_mem_Icc, finset_mem_Ico := h₀_finset_mem_Ico, finset_mem_Ioc := h₀_finset_mem_Ioc,
      finset_mem_Ioo := h₀_finset_mem_Ioo } =
    { finsetIcc := h₁_finset_Icc, finsetIco := h₁_finset_Ico, finsetIoc := h₁_finset_Ioc, finsetIoo := h₁_finset_Ioo,
      finset_mem_Icc := h₁_finset_mem_Icc, finset_mem_Ico := h₁_finset_mem_Ico, finset_mem_Ioc := h₁_finset_mem_Ioc,
      finset_mem_Ioo := h₁_finset_mem_Ioo }

Tactic:
have hIcc : h₀_finset_Icc = h₁_finset_Icc := by
      ext a b x
      rw [h₀_finset_mem_Icc, h₁_finset_mem_Icc]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀_finset_Icc h₀_finset_Ico h₀_finset_Ioc h₀_finset_Ioo : α → α → Finset α
h₀_finset_mem_Icc : ∀ (a b x : α), x ∈ h₀_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₀_finset_mem_Ico : ∀ (a b x : α), x ∈ h₀_finset_Ico a b ↔ a ≤ x ∧ x < b
h₀_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₀_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₀_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₀_finset_Ioo a b ↔ a < x ∧ x < b
h₁_finset_Icc h₁_finset_Ico h₁_finset_Ioc h₁_finset_Ioo : α → α → Finset α
h₁_finset_mem_Icc : ∀ (a b x : α), x ∈ h₁_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₁_finset_mem_Ico : ∀ (a b x : α), x ∈ h₁_finset_Ico a b ↔ a ≤ x ∧ x < b
h₁_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₁_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₁_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₁_finset_Ioo a b ↔ a < x ∧ x < b
hIcc : h₀_finset_Icc = h₁_finset_Icc
⊢ { finsetIcc := h₀_finset_Icc, finsetIco := h₀_finset_Ico, finsetIoc := h₀_finset_Ioc, finsetIoo := h₀_finset_Ioo,
      finset_mem_Icc := h₀_finset_mem_Icc, finset_mem_Ico := h₀_finset_mem_Ico, finset_mem_Ioc := h₀_finset_mem_Ioc,
      finset_mem_Ioo := h₀_finset_mem_Ioo } =
    { finsetIcc := h₁_finset_Icc, finsetIco := h₁_finset_Ico, finsetIoc := h₁_finset_Ioc, finsetIoo := h₁_finset_Ioo,
      finset_mem_Icc := h₁_finset_mem_Icc, finset_mem_Ico := h₁_finset_mem_Ico, finset_mem_Ioc := h₁_finset_mem_Ioc,
      finset_mem_Ioo := h₁_finset_mem_Ioo }
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder β
f : α ↪o β
a b x : α
⊢ x ∈ (Ico (f a) (f b)).preimage ⇑f ⋯ ↔ a ≤ x ∧ x < b

Tactic:
rw [mem_preimage, mem_Ico, f.le_iff_le, f.lt_iff_lt]

Goal state after:
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: case inr
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : ℕ → α
g : ℕ ↪o ℕ
hnr : ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))
⊢ ∃ g, (∀ (m n : ℕ), m < n → r (f (g m)) (f (g n))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))

Tactic:
· exact ⟨g, Or.intro_right _ hnr⟩

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
inst✝ : LocallyFiniteOrder α
a b x : Subtype p
⊢ ↑a ≤ ↑x ∧ ↑x ≤ ↑b ↔ a ≤ x ∧ x ≤ b

Tactic:
Subtype.coe_le_coe

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
inst✝ : LocallyFiniteOrderTop α
a x : Subtype p
⊢ ↑a ≤ ↑x ↔ a ≤ x

Tactic:
Subtype.coe_le_coe

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

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderTop α
h : a ≤ b
⊢ Ioi b ⊆ Ioi a

Tactic:
by
  simpa [← coe_subset] using Set.Ioi_subset_Ioi h

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

Goal state before:
pp: M : Type u
α : Type v
inst✝² : Monoid M
inst✝¹ : Group α
inst✝ : MulDistribMulAction M α
x✝¹ : α
ha : x✝¹ ∈ (submonoid M α).carrier
x✝ : M
⊢ x✝ • x✝¹⁻¹ = x✝¹⁻¹

Tactic:
by rw [smul_inv', ha]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x ≤ y
⊢ TransGen (fun x1 x2 ↦ x1 ⩿ x2) x y

Tactic:
by
  -- We proceed by well-founded induction on the cardinality of `Icc x y`.
  -- It's impossible for the cardinality to be zero since `x ≤ y`
  have : #(Ico x y) < #(Icc x y) := card_lt_card <|
    ⟨Ico_subset_Icc_self, not_subset.mpr ⟨y, ⟨right_mem_Icc.mpr hxy, right_notMem_Ico⟩⟩⟩
  by_cases hxy' : y ≤ x
  -- If `y ≤ x`, then `x ⩿ y`
  · exact .single <| wcovBy_of_le_of_le hxy hxy'
  /- and if `¬ y ≤ x`, then `x < y`, not because it is a linear order, but because `x ≤ y`
  already. In that case, since `z` is maximal in `Ico x y`, then `z ⩿ y` and we can use the
  induction hypothesis to show that `Relation.TransGen (· ⩿ ·) x z`. -/
  · obtain ⟨z, hxz, hz⟩ :=
      (Set.finite_Ico x y).exists_le_maximal <| Set.left_mem_Ico.2 <| hxy.lt_of_not_ge hxy'
    have z_card := calc
      #(Icc x z) ≤ #(Ico x y) := card_le_card <| Icc_subset_Ico_right hz.1.2
      _          < #(Icc x y) := this
    have h₁ := transGen_wcovBy_of_le hz.1.1
    have h₂ : z ⩿ y :=
      ⟨hz.1.2.le, fun c hzc hcy ↦ hzc.not_ge <| hz.2 ⟨hz.1.1.trans hzc.le, hcy⟩ hzc.le⟩
    exact .tail h₁ h₂

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

Goal state before:
pp: case pos
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x < y
z : α
hxz✝ : x ≤ z
hz : Maximal (fun x_1 ↦ x_1 ∈ Set.Ico x y) z
z_card : #(Ico x z) < #(Ico x y)
hzy : z ⋖ y
hxz : x < z
⊢ TransGen (fun x1 x2 ↦ x1 ⋖ x2) x y

pp: case neg
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x < y
z : α
hxz✝ : x ≤ z
hz : Maximal (fun x_1 ↦ x_1 ∈ Set.Ico x y) z
z_card : #(Ico x z) < #(Ico x y)
hzy : z ⋖ y
hxz : ¬x < z
⊢ TransGen (fun x1 x2 ↦ x1 ⋖ x2) x y

Tactic:
· exact .tail (transGen_covBy_of_lt hxz) hzy

Goal state after:
case neg
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x < y
z : α
hxz✝ : x ≤ z
hz : Maximal (fun x_1 ↦ x_1 ∈ Set.Ico x y) z
z_card : #(Ico x z) < #(Ico x y)
hzy : z ⋖ y
hxz : ¬x < z
⊢ TransGen (fun x1 x2 ↦ x1 ⋖ x2) x y
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
⊢ f a < f b

Tactic:
have := Relation.TransGen.lift f h a b

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 : TransGen CovBy a b ≤ (TransGen 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_2
β : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MulAction G β
inst✝¹ : SMul α β
inst✝ : IsScalarTower G α β
a : α
b : β
⊢ ∀ ⦃x : G⦄, x • a = a → (x • a) • b = a • b

Tactic:
rintro a h

Goal state after:
G : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MulAction G β
inst✝¹ : SMul α β
inst✝ : IsScalarTower G α β
a✝ : α
b : β
a : G
h : a • a✝ = a✝
⊢ (a • a✝) • b = a✝ • b
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: α : Type u_2
β : Type u_3
G' : Type u_4
inst✝³ : Group G'
inst✝² : SMul α β
inst✝¹ : MulAction G' β
inst✝ : SMulCommClass G' α β
a : α
b : β
⊢ ∀ ⦃x : G'⦄, x • b = b → a • x • b = a • b

Tactic:
rintro a h

Goal state after:
α : Type u_2
β : Type u_3
G' : Type u_4
inst✝³ : Group G'
inst✝² : SMul α β
inst✝¹ : MulAction G' β
inst✝ : SMulCommClass G' α β
a✝ : α
b : β
a : G'
h : a • b = b
⊢ a✝ • a • b = a✝ • b
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)
h : G
⊢ h * g = g * h

Tactic:
rw [← ϕ.injective.eq_iff, map_mul, map_mul]

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: G : Type u_1
inst✝ : Group G
⊢ (center G).Characteristic

Tactic:
refine characteristic_iff_comap_le.mpr fun ϕ g hg => ?_
  rw [mem_center_iff]
  intro h
  rw [← ϕ.injective.eq_iff, map_mul, map_mul]
  exact (hg.comm (ϕ h)).symm

Goal state after: