mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Set.Pairwise.Lattice

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

Tactic:
simp only [Set.Pairwise, mem_iUnion, exists_prop, forall_exists_index, and_imp]

Goal state after:
α : Type u_1
s : Set (Set α)
hd : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) s
r : α → α → Prop
h : ∀ a ∈ s, a.Pairwise r
⊢ ∀ ⦃x : α⦄, ∀ x_1 ∈ s, x ∈ x_1 → ∀ ⦃y : α⦄, ∀ x_2 ∈ s, y ∈ x_2 → x ≠ y → r x y
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ ↑s.powerset = SetLike.coe ⁻¹' 𝒫 ↑s

Tactic:
by
  ext
  simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset (Option α)
⊢ eraseNone s = s.biUnion Option.toFinset

Tactic:
by
  ext
  simp

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ eraseNone (map Embedding.some s) = s

Tactic:
by
  ext
  simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq (Option α)
inst✝ : DecidableEq α
s t : Finset (Option α)
⊢ eraseNone (s ∪ t) = eraseNone s ∪ eraseNone t

Tactic:
by
  ext
  simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq (Option α)
inst✝ : DecidableEq α
s t : Finset (Option α)
⊢ eraseNone (s ∩ t) = eraseNone s ∩ eraseNone t

Tactic:
by
  ext
  simp

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

Goal state before:
pp: α : Type u_1
⊢ eraseNone ∅ = ∅

Tactic:
by
  ext
  simp

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

Goal state before:
pp: α : Type u_1
⊢ eraseNone {none} = ∅

Tactic:
by
  ext
  simp

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ eraseNone (insertNone s) = s

Tactic:
by
  ext
  simp

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

Goal state before:
pp: case unique
α : Type u_1
ι : Type u_2
f : ι → Set α
s : Set ι
y : α
h_disjoint : s.PairwiseDisjoint f
hy : y ∈ ⋃ i ∈ s, f i
⊢ ∀ (y₁ y₂ : ι), y₁ ∈ s ∧ y ∈ f y₁ → y₂ ∈ s ∧ y ∈ f y₂ → y₁ = y₂

Tactic:
rintro i j ⟨his, hi⟩ ⟨hjs, hj⟩
    exact h_disjoint.elim his hjs <| not_disjoint_iff.mpr ⟨y, ⟨hi, hj⟩⟩

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

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

Tactic:
induction hs using Finset.Nonempty.cons_induction with

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

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

Tactic:
induction hs using Finset.Nonempty.cons_induction with

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

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

Tactic:
induction hs using Finset.Nonempty.cons_induction with

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, sSup ∅ ≤ f x
h' : (image f s).Nonempty
⊢ ⨆ i ∈ s, f i = (image f s).max' h'

Tactic:
rw [iSup, ← h'.csSup_eq_max', coe_image]
  refine csSup_eq_csSup_of_forall_exists_le ?_ ?_
  · simp only [ciSup_eq_ite, dite_eq_ite, Set.mem_range, Set.mem_image, mem_coe,
      exists_exists_and_eq_and, forall_exists_index, forall_apply_eq_imp_iff]
    intro i
    split_ifs
    · exact ⟨_, by assumption, le_rfl⟩
    · assumption
  · simp only [Set.mem_image, mem_coe, ciSup_eq_ite, dite_eq_ite, Set.mem_range,
      exists_exists_eq_and, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
    intro i hi
    refine ⟨i, ?_⟩
    simp [hi]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : DecidableEq ι
f : ι → α
s t : Finset ι
this : ∀ (st : Finset ι), BddAbove (Set.range fun x ↦ ⨆ (_ : x ∈ st), f x)
⊢ ⨆ x ∈ s ∪ t, f x = max (⨆ x ∈ s, f x) (⨆ x ∈ t, f x)

Tactic:
simp [ciSup_or', ciSup_sup_eq, this]

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

Goal state before:
pp: case refine_2
α : Type u_2
ι : Type u_5
inst✝ : CompleteLattice α
s : ι → α
⊢ ⨆ t, ⨆ i ∈ t, s i ≤ ⨆ i, s i

Tactic:
· exact iSup_le fun t => iSup_le fun b => iSup_le fun _ => le_iSup _ _

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

Goal state before:
pp: ι : Type u_5
s : Set ι
⊢ ⋃ s', Subtype.val '' ↑s' = s

Tactic:
by
  ext x
  simp only [Set.mem_iUnion, Set.mem_image, SetLike.mem_coe, Subtype.exists,
    exists_and_right, exists_eq_right]
  exact ⟨fun ⟨_, hx, _⟩ ↦ hx, fun hx ↦ ⟨{⟨x, hx⟩}, hx, by simp⟩⟩

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
⊢ a ≤ c ∧ c ≤ b ↔ c = a ∨ c = b

Tactic:
refine ⟨fun h2 => h.eq_or_eq h2.1 h2.2, ?_⟩

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
⊢ c = a ∨ c = b → a ≤ c ∧ c ≤ b
Module: Mathlib.Order.Preorder.Finite

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

Tactic:
induction hs using Finset.Nonempty.cons_induction with

Goal state after:
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: case pos
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : Infinite ↑bad
m n : ℕ
mn : m < n
h : (Nat.orderEmbeddingOfSet bad) m ∈ Set.range ⇑(Nat.orderEmbeddingOfSet bad)
⊢ ¬r (f ((Nat.orderEmbeddingOfSet bad) m)) (f ((Nat.orderEmbeddingOfSet bad) n))

Tactic:
Nat.orderEmbeddingOfSet_range bad

Goal state after:
case pos
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : Infinite ↑bad
m n : ℕ
mn : m < n
h : (Nat.orderEmbeddingOfSet bad) m ∈ bad
⊢ ¬r (f ((Nat.orderEmbeddingOfSet bad) m)) (f ((Nat.orderEmbeddingOfSet bad) n))
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : Preorder β
inst✝² : LocallyFiniteOrder α
inst✝¹ : LocallyFiniteOrder β
inst✝ : DecidableLE (α × β)
a b x : α × β
⊢ x ∈ Icc a.1 b.1 ×ˢ Icc a.2 b.2 ↔ a ≤ x ∧ x ≤ b

Tactic:
by
    rw [mem_product, mem_Icc, mem_Icc, and_and_and_comm, le_def, le_def]

Goal state after:
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: case inr
α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
a✝ : Infinite α
f : ℕ → α
hStrictAnti : StrictAnti f
⊢ False

Tactic:
· exact not_strictAnti_of_wellFoundedLT f hStrictAnti

Goal state after:
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_2
inst✝¹ : Preorder α
inst✝ : Nonempty α
wfl : WellFoundedLT α
wfg : WellFoundedGT α
next : ⦃a : α⦄ → ¬IsMax a → α
hnext : ∀ ⦃a : α⦄ (h : ¬IsMax a), a ⋖ next h
hα : Set.univ.Nonempty
a : ℕ → α := fun t ↦ Nat.rec (⋯.min Set.univ hα) (fun _n a ↦ if ha : IsMax a then a else next ha) t
cov : ∀ (n : ℕ), ¬IsMax (a n) → a n ⋖ a (n + 1)
H : ∃ n, IsMax (a n)
⊢ ∃ n, IsMax (a n) ∧ ∀ i < n, a i ⋖ a (i + 1)

Tactic:
exact ⟨_, wellFounded_lt.min_mem _ H, fun i h ↦ cov _ (wellFounded_lt.not_lt_min _ · h)⟩

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

Goal state before:
pp: P : ℕ → Prop
base : ∃ n, ∀ m > n, P m
step : ∀ (n : ℕ), (∀ m > n, P m) → P n
n : ℕ
⊢ ∀ (n : ℕ), (∀ m ≥ n + 1, P m) → ∀ m ≥ n, P m

Tactic:
intro n ih m hm

Goal state after:
P : ℕ → Prop
base : ∃ n, ∀ m > n, P m
step : ∀ (n : ℕ), (∀ m > n, P m) → P n
n✝ n : ℕ
ih : ∀ m ≥ n + 1, P m
m : ℕ
hm : m ≥ n
⊢ P m
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DistribLattice α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ a ∈ [[b, c]] → b ∈ [[a, c]] → a = b

Tactic:
simp_rw [mem_uIcc]

Goal state after:
α : Type u_2
inst✝¹ : DistribLattice α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ b ⊓ c ≤ a ∧ a ≤ b ⊔ c → a ⊓ c ≤ b ∧ b ≤ a ⊔ c → a = b
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DistribLattice α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ b ∈ [[a, c]] → c ∈ [[a, b]] → b = c

Tactic:
simp_rw [mem_uIcc]

Goal state after:
α : Type u_2
inst✝¹ : DistribLattice α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ a ⊓ c ≤ b ∧ b ≤ a ⊔ c → a ⊓ b ≤ c ∧ c ≤ a ⊔ b → b = c
Module: Mathlib.GroupTheory.Subgroup.Center

Goal state before:
pp: G : Type u_2
inst✝ : CommGroup G
⊢ center G = ⊤

Tactic:
rw [eq_top_iff']
  intro x
  rw [Subgroup.mem_center_iff]
  intro y
  exact mul_comm y x

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
⊢ Set.BijOn ConjClasses.mk (↑(Subgroup.center G)) (noncenter G)ᶜ

Tactic:
by
  refine ⟨fun g hg ↦ ?_, fun x hx y _ H ↦ ?_, ?_⟩
  · simp only [mem_noncenter, Set.compl_def, Set.mem_ofPred, Set.not_nontrivial_iff]
    intro x hx y hy
    simp only [mem_carrier_iff_mk_eq, mk_eq_mk_iff_isConj] at hx hy
    rw [hx.eq_of_right_mem_center hg, hy.eq_of_right_mem_center hg]
  · rw [mk_eq_mk_iff_isConj] at H
    exact H.eq_of_left_mem_center hx
  · rintro ⟨g⟩ hg
    refine ⟨g, ?_, rfl⟩
    simp only [mem_noncenter, Set.compl_def, Set.mem_ofPred, Set.not_nontrivial_iff] at hg
    rw [SetLike.mem_coe, Subgroup.mem_center_iff]
    intro h
    rw [← mul_inv_eq_iff_eq_mul]
    refine hg ?_ mem_carrier_mk
    rw [mem_carrier_iff_mk_eq]
    apply mk_eq_mk_iff_isConj.mpr
    rw [isConj_comm, isConj_iff]
    exact ⟨h, rfl⟩

Goal state after:
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
x✝ : Mˣ
ha : x✝ ∈ Units.val ⁻¹' center M
g✝ : Mˣ
⊢ g✝ * x✝ = x✝ * g✝

Tactic:
rw [← Units.val_inj, Units.val_mul, Units.val_mul, ha.comm]

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

Goal state before:
pp: case refine_2
G : Type u_2
inst✝ : Group G
ι : Sort u_5
S : ι → Subgroup G
C : (x : G) → x ∈ ⨆ i, S i → Prop
hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x ⋯
h1 : C 1 ⋯
hmul : ∀ (x y : G) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯
x : G
hx : x ∈ ⨆ i, S i
⊢ ∃ (h : 1 ∈ ⨆ i, S i), C 1 h

Tactic:
exact ⟨_, h1⟩

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

Goal state before:
pp: case refine_3
G : Type u_2
inst✝ : Group G
ι : Sort u_5
S : ι → Subgroup G
C : (x : G) → x ∈ ⨆ i, S i → Prop
hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x ⋯
h1 : C 1 ⋯
hmul : ∀ (x y : G) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯
x✝ : G
hx : x✝ ∈ ⨆ i, S i
x y : G
⊢ (∃ (h : x ∈ ⨆ i, S i), C x h) → (∃ (h : y ∈ ⨆ i, S i), C y h) → ∃ (h : x * y ∈ ⨆ i, S i), C (x * y) h

Tactic:
rintro ⟨_, Cx⟩ ⟨_, Cy⟩

Goal state after:
case refine_3
G : Type u_2
inst✝ : Group G
ι : Sort u_5
S : ι → Subgroup G
C : (x : G) → x ∈ ⨆ i, S i → Prop
hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x ⋯
h1 : C 1 ⋯
hmul : ∀ (x y : G) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯
x✝ : G
hx : x✝ ∈ ⨆ i, S i
x y : G
w✝¹ : x ∈ ⨆ i, S i
Cx : C x w✝¹
w✝ : y ∈ ⨆ i, S i
Cy : C y w✝
⊢ ∃ (h : x * y ∈ ⨆ i, S i), C (x * y) h
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: case h.cons
α : Type u_3
inst✝ : Monoid α
a hd : α
tl : List α
IH : {x | x ∈ a ::ₘ ⟦tl⟧}.Pairwise Commute → a * tl.prod = tl.prod * a
comm : {x | x ∈ a ::ₘ ⟦hd :: tl⟧}.Pairwise Commute
⊢ a * hd * tl.prod = hd * a * tl.prod

Tactic:
congr 1
      apply comm.of_refl <;> simp

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

Goal state before:
pp: case mul.refine_2
G : Type u_2
inst✝ : Group G
H N : Subgroup G
hLE : H ≤ normalizer ↑N
x✝ x : G
hx : x ∈ ↑H
y : G
hy : y ∈ ↑N
hx✝ : (fun x1 x2 ↦ x1 * x2) x y ∈ closure (↑H * ↑N)
x' : G
hx' : x' ∈ ↑H
y' : G
hy' : y' ∈ ↑N
hy✝ : (fun x1 x2 ↦ x1 * x2) x' y' ∈ closure (↑H * ↑N)
⊢ (fun x1 x2 ↦ x1 * x2) (x * x') (x'⁻¹ * y * x' * y') = (fun x1 x2 ↦ x1 * x2) x y * (fun x1 x2 ↦ x1 * x2) x' y'

Tactic:
· simp only [mul_assoc, mul_inv_cancel_left]

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
S : Submonoid M
ι : Type u_4
t : Finset ι
f : ι → M
comm : (↑t).Pairwise (Function.onFun Commute f)
h : ∀ c ∈ t, f c ∈ S
⊢ t.noncommProd f comm ∈ S

Tactic:
apply multiset_noncommProd_mem
  intro y
  rw [Multiset.mem_map]
  rintro ⟨x, ⟨hx, rfl⟩⟩
  exact h x hx

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

Goal state before:
pp: case convert_4
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ ∀ x_1 ∈ insert i (univ.erase i),
    (Pi.evalMonoidHom M i) ((MonoidHom.mulSingle M x_1) (x x_1)) = Pi.mulSingle x_1 (x x_1) i

Tactic:
intro j _

Goal state after:
case convert_4
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i j : ι
a✝ : j ∈ insert i (univ.erase i)
⊢ (Pi.evalMonoidHom M i) ((MonoidHom.mulSingle M j) (x j)) = Pi.mulSingle j (x j) i
Module: Mathlib.GroupTheory.Congruence.Defs

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

Tactic:
by cases c; congr!

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
s : Finset ι
a : ι
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
h : a ∉ s
f : ι → M
⊢ (insert a s).prod f = f a * ∏ x ∈ s, f x

Tactic:
Finset.prod_insert h

Goal state after:
ι : Type u_1
M : Type u_4
s : Finset ι
a : ι
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
h : a ∉ s
f : ι → M
⊢ f a * ∏ x ∈ s, f x = f a * ∏ x ∈ s, f x
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
L : List (α × Bool)
x : α
b : Bool
h : Red ((x, b) :: L) []
h₁✝ : Red ((x, !b) :: (x, b) :: L) [(x, !b)]
h₂✝ : Red ((x, !b) :: (x, b) :: L) L
L' : List (α × Bool)
h₁ : Red [(x, !b)] L'
h₂ : Red L L'
⊢ Red L [(x, !b)]

Tactic:
rw [singleton_iff] at h₁

Goal state after:
α : Type u
L : List (α × Bool)
x : α
b : Bool
h : Red ((x, b) :: L) []
h₁✝ : Red ((x, !b) :: (x, b) :: L) [(x, !b)]
h₂✝ : Red ((x, !b) :: (x, b) :: L) L
L' : List (α × Bool)
h₁ : L' = [(x, !b)]
h₂ : Red L L'
⊢ Red L [(x, !b)]
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
L₁ L₂ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
H1 : (x1, b1) ≠ (x2, b2)
H2 : Red ((x1, b1) :: L₁) ((x2, b2) :: L₂)
⊢ Red L₁ ((x1, !b1) :: (x2, b2) :: L₂)

Tactic:
have : Red ((x1, b1) :: L₁) ([(x2, b2)] ++ L₂) := H2

Goal state after:
α : Type u
L₁ L₂ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
H1 : (x1, b1) ≠ (x2, b2)
H2 : Red ((x1, b1) :: L₁) ((x2, b2) :: L₂)
this : Red ((x1, b1) :: L₁) ([(x2, b2)] ++ L₂)
⊢ Red L₁ ((x1, !b1) :: (x2, b2) :: L₂)
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case cons
α : Type u
L2 : List (α × Bool)
x : α
b : Bool
hd : α × Bool
tl : List (α × Bool)
ih : sizeOf (tl ++ L2) < sizeOf (tl ++ (x, b) :: (x, !b) :: L2)
⊢ sizeOf (hd :: (tl ++ L2)) < sizeOf (hd :: (tl ++ (x, b) :: (x, !b) :: L2))

Tactic:
exact Nat.add_lt_add_left ih _

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
b a : α
hb : b ∈ s
⊢ ↑(a * b) = ↑a

Tactic:
by
  rwa [QuotientGroup.eq, mul_inv_rev, inv_mul_cancel_right, s.inv_mem_iff]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g₁ g₂ : G
⊢ ⁅g₁, g₂⁆⁻¹ = ⁅g₂, g₁⁆

Tactic:
by
  simp_rw [commutatorElement_def, mul_inv_rev, inv_inv, mul_assoc]

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

Goal state before:
pp: M : Type u_4
ι : Type u_7
inst✝² : Fintype ι
inst✝¹ : CommMonoid M
p : ι → Prop
f : ι → M
inst✝ : DecidablePred p
s : Finset ι := {x | p x}.toFinset
⊢ (∏ a ∈ s, f a) * ∏ a ∈ sᶜ, f a = ∏ i, f i

pp: case h
M : Type u_4
ι : Type u_7
inst✝² : Fintype ι
inst✝¹ : CommMonoid M
p : ι → Prop
f : ι → M
inst✝ : DecidablePred p
s : Finset ι := {x | p x}.toFinset
⊢ ∀ (x : ι), x ∈ sᶜ ↔ ¬p x

pp: case h
M : Type u_4
ι : Type u_7
inst✝² : Fintype ι
inst✝¹ : CommMonoid M
p : ι → Prop
f : ι → M
inst✝ : DecidablePred p
s : Finset ι := {x | p x}.toFinset
⊢ ∀ (x : ι), x ∈ s ↔ p x

Tactic:
· exact Finset.prod_mul_prod_compl _ _

Goal state after:
case h
M : Type u_4
ι : Type u_7
inst✝² : Fintype ι
inst✝¹ : CommMonoid M
p : ι → Prop
f : ι → M
inst✝ : DecidablePred p
s : Finset ι := {x | p x}.toFinset
⊢ ∀ (x : ι), x ∈ sᶜ ↔ ¬p x

case h
M : Type u_4
ι : Type u_7
inst✝² : Fintype ι
inst✝¹ : CommMonoid M
p : ι → Prop
f : ι → M
inst✝ : DecidablePred p
s : Finset ι := {x | p x}.toFinset
⊢ ∀ (x : ι), x ∈ s ↔ p x
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ commutator G = closure (commutatorSet G)

Tactic:
simp [commutator, Subgroup.commutator_def, commutatorSet]

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

Goal state before:
pp: R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
r₂ : X
s₁ s₂ : ↥S
r' : R
s' : ↥S
huv : ↑s' * r₁ = r' * ↑s₂
⊢ (r₁ /ₒ s₁) • (r₂ /ₒ s₂) = r' • r₂ /ₒ (s' * s₁)

Tactic:
by
  with_unfolding_all exact smul'_char r₁ r₂ s₁ s₂ s' r' huv

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ : ↥S
r' : R
s' : ↥S
huv : ↑s' * r₁ = r' * ↑s₂
⊢ r₁ /ₒ s₁ * (r₂ /ₒ s₂) = r' * r₂ /ₒ (s' * s₁)

Tactic:
by
  with_unfolding_all exact smul'_char r₁ r₂ s₁ s₂ s' r' huv

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

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x₁ x₂ : M
y₁ y₂ : ↥S
⊢ f.mk' (x₁ * x₂) (y₁ * y₂) = f.mk' x₁ y₁ * f.mk' x₂ y₂

Tactic:
by
  refine (mul_inv_left f.map_units _ _ _).2 ?_
  simp only [map_mul, coe_mul, toMonoidHom_apply, mk', IsUnit.liftRight, Units.liftRight,
    MonoidHom.domRestrict_apply, MonoidHom.coe_mk, OneHom.coe_mk]
  rw [mul_mul_mul_comm (f x₁), mul_left_comm, mul_mul_mul_comm (f y₁)]
  simp

Goal state after:
Module: Mathlib.Algebra.Ring.Equiv

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
e : R ≃+* S
⊢ e.toNonUnitalRingHom.comp e.symm.toNonUnitalRingHom = NonUnitalRingHom.id S

Tactic:
by
  ext
  simp

Goal state after:
Module: Mathlib.Algebra.Ring.Equiv

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
e : R ≃+* S
⊢ e.symm.toNonUnitalRingHom.comp e.toNonUnitalRingHom = NonUnitalRingHom.id R

Tactic:
by
  ext
  simp

Goal state after:
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : CommMonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
a b : WithTop α
⊢ (if a = 0 ∨ b = 0 then 0 else map₂ (fun x1 x2 ↦ x1 * x2) a b) =
    if b = 0 ∨ a = 0 then 0 else map₂ (fun x1 x2 ↦ x1 * x2) b a

Tactic:
exact if_congr or_comm rfl (Option.map₂_comm mul_comm)

Goal state after:
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: case neg.refine_2
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m✝ n : X
hn' : n ≤ m✝
m : X
hmn✝ : n ≤ m
IH : m ∈ upperBounds S → n ∈ S → m ∉ S → ∃ x, IsGreatest S x
hm : succ m ∈ upperBounds S
hn : n ∈ S
⊢ succ m ∉ S → ∃ x, IsGreatest S x

Tactic:
hm'

Goal state after:
case neg.refine_2
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m✝ n : X
hn' : n ≤ m✝
m : X
hmn✝ : n ≤ m
IH : m ∈ upperBounds S → n ∈ S → m ∉ S → ∃ x, IsGreatest S x
hm : succ m ∈ upperBounds S
hn : n ∈ S
hm' : succ m ∉ S
⊢ ∃ x, IsGreatest S x
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: case pos
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m✝ n : X
hn' : n ≤ m✝
m : X
hmn✝ : n ≤ m
IH : (∀ x ∈ S, x ≤ m) → n ∈ S → m ∉ S → ∃ x, IsGreatest S x
hn : n ∈ S
hm' : succ m ∉ S
hm : ∀ x ∈ S, x ≤ m
hmS : m ∈ S
⊢ ∃ x, IsGreatest S x

pp: case neg
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m✝ n : X
hn' : n ≤ m✝
m : X
hmn✝ : n ≤ m
IH : (∀ x ∈ S, x ≤ m) → n ∈ S → m ∉ S → ∃ x, IsGreatest S x
hn : n ∈ S
hm' : succ m ∉ S
hm : ∀ x ∈ S, x ≤ m
hmS : m ∉ S
⊢ ∃ x, IsGreatest S x

Tactic:
· exact ⟨m, hmS, hm⟩

Goal state after:
case neg
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m✝ n : X
hn' : n ≤ m✝
m : X
hmn✝ : n ≤ m
IH : (∀ x ∈ S, x ≤ m) → n ∈ S → m ∉ S → ∃ x, IsGreatest S x
hn : n ∈ S
hm' : succ m ∉ S
hm : ∀ x ∈ S, x ≤ m
hmS : m ∉ S
⊢ ∃ x, IsGreatest S x
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: case h.succ
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PredOrder α
inst✝¹ : IsPredArchimedean α
s : Set α
inst✝ : s.OrdConnected
x✝¹ x✝ : ↑s
b : α
hb : b ∈ s
n : ℕ
hi : ∀ (c : α) (hc : c ∈ s), b ≤ c → pred^[n] c = b → pred^[n] ⟨c, hc⟩ = ⟨b, hb⟩
c : α
hc : c ∈ s
hbc : b ≤ c
hn : pred^[n + 1] c = b
⊢ pred^[n + 1] ⟨c, hc⟩ = ⟨b, hb⟩

Tactic:
simp_all only [Function.iterate_succ, Function.comp_apply]
      change Order.pred^[n] (dite ..) = _
      split_ifs with h
      · dsimp only at h ⊢
        apply hi _ _ _ hn
        · rw [← hn]
          apply Order.pred_iterate_le
      · have : Order.pred (⟨c, hc⟩ : s) = ⟨c, hc⟩ := by
          change dite .. = _
          simp [h]
        rw [Function.iterate_fixed]
        · simp only [Order.pred_eq_iff_isMin] at this
          apply (this.eq_of_le _).symm
          exact hbc
        · exact this

Goal state after:
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMax a → f a ≤ f (succ a)
⊢ ∀ (a : α), ¬IsMax a → a ∈ Set.univ → succ a ∈ Set.univ → f a ≤ f (succ a)

Tactic:
by simpa using hf

Goal state after:
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMax a → f (succ a) ≤ f a
⊢ ∀ (a : α), ¬IsMax a → a ∈ Set.univ → succ a ∈ Set.univ → f (succ a) ≤ f a

Tactic:
by simpa using hf

Goal state after:
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMax a → f a < f (succ a)
⊢ ∀ (a : α), ¬IsMax a → a ∈ Set.univ → succ a ∈ Set.univ → f a < f (succ a)

Tactic:
by simpa using hf

Goal state after:
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMax a → f (succ a) < f a
⊢ ∀ (a : α), ¬IsMax a → a ∈ Set.univ → succ a ∈ Set.univ → f (succ a) < f a

Tactic:
by simpa using hf

Goal state after:
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMin a → f (pred a) ≤ f a
⊢ ∀ (a : α), ¬IsMin a → a ∈ Set.univ → pred a ∈ Set.univ → f (pred a) ≤ f a

Tactic:
by simpa using hf

Goal state after:
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMin a → f a ≤ f (pred a)
⊢ ∀ (a : α), ¬IsMin a → a ∈ Set.univ → pred a ∈ Set.univ → f a ≤ f (pred a)

Tactic:
by simpa using hf

Goal state after: