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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → (∀ z ∈ s, z ∉ Set.Ioo x y) → ∃ z ∈ t, x < z ∧ z < y
⊢ #s ≤ #t + 1

Tactic:
replace h : ∀ᵉ (x ∈ s) (y ∈ s), x < y → ∃ z ∈ t, x < z ∧ z < y := by
    intro x hx y hy hxy
    rcases exists_next_right ⟨y, hy, hxy⟩ with ⟨a, has, hxa, ha⟩
    rcases h x hx a has hxa fun z hzs hz => hz.2.not_ge <| ha _ hzs hz.1 with ⟨b, hbt, hxb, hba⟩
    exact ⟨b, hbt, hxb, hba.trans_le <| ha _ hy hxy⟩
  set f : α → WithTop α := fun x => (t.filter fun y => x < y).min
  have f_mono : StrictMonoOn f s := by
    intro x hx y hy hxy
    rcases h x hx y hy hxy with ⟨a, hat, hxa, hay⟩
    calc
      f x ≤ a := min_le (mem_filter.2 ⟨hat, by simpa⟩)
      _ < f y :=
        (Finset.lt_inf_iff <| WithTop.coe_lt_top a).2 fun b hb =>
          WithTop.coe_lt_coe.2 <| hay.trans (by simpa using (mem_filter.1 hb).2)
  calc
    s.card = (s.image f).card := (card_image_of_injOn f_mono.injOn).symm
    _ ≤ (insert ⊤ (t.image (↑)) : Finset (WithTop α)).card :=
      card_mono <| image_subset_iff.2 fun x _ =>
          insert_subset_insert _ (image_subset_image <| filter_subset _ _)
            (min_mem_insert_top_image_coe _)
    _ ≤ t.card + 1 := (card_insert_le _ _).trans (Nat.add_le_add_right card_image_le _)

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

Goal state before:
pp: α : Type u
n : ℕ
a : α
l : List α
⊢ sublistsLen (n + 1) (a :: l) = sublistsLen (n + 1) l ++ map (cons a) (sublistsLen n l)

Tactic:
by
  rw [sublistsLen, sublistsLenAux, sublistsLenAux_eq, sublistsLenAux_eq, map_id,
      append_nil]; rfl

Goal state after:
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
⊢ ∀ ⦃x : α⦄, ∀ x_1 ∈ s, x ∈ x_1 → ∀ ⦃y : α⦄, ∀ x_2 ∈ s, y ∈ x_2 → x ≠ y → r x y

Tactic:
intro x S hS hx y T hT hy hne

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 : α
S : Set α
hS : S ∈ s
hx : x ∈ S
y : α
T : Set α
hT : T ∈ s
hy : y ∈ T
hne : x ≠ y
⊢ r x y
Module: Mathlib.Data.Fintype.Option

Goal state before:
pp: P : (α : Type u) → [Fintype α] → Prop
of_equiv : ∀ (α β : Type u) [inst : Fintype β] (e : α ≃ β), P α → P β
h_empty : P PEmpty.{u + 1}
h_option : ∀ (α : Type u) [inst : Fintype α], P α → P (Option α)
α : Type u
h_fintype : Fintype α
f_empty : ∀ (i : Fintype PEmpty.{u + 1}), P PEmpty.{u + 1} := fun i ↦ ?m.44
⊢ ∀ {α : Type u} [Fintype α] [DecidableEq α], (∀ (h : Fintype α), P α) → ∀ (h : Fintype (Option α)), P (Option α)

Tactic:
by
      rintro α hα - Pα hα'
      convert! h_option α (Pα _)

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

Goal state before:
pp: case insert
α : 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
⊢ (insert a s).sup f ∈ f '' ↑(insert a s)

Tactic:
rw [Finset.sup_insert (b := a) (s := s) (f := f)]
    cases s.eq_empty_or_nonempty with
    | inl hs => simp [hs]
    | inr hs =>
      simp only [Finset.coe_insert]
      rcases le_total (f a) (s.sup f) with (ha | ha)
      · rw [sup_eq_right.mpr ha]
        exact Set.image_mono (Set.subset_insert a s) (h hs)
      · rw [sup_eq_left.mpr ha]
        apply Set.mem_image_of_mem _ (Set.mem_insert a ↑s)

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

Goal state before:
pp: case inr
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompletePartialOrderSup α
p : ι → Prop
f : (i : ι) → p i → α
hp : ∀ (i : ι), ¬p i
h✝ : Nonempty ι
this : ∀ (i : ι), IsEmpty (p i)
⊢ ⨆ i, ⨆ (h : p i), f i h = sSup ∅

Tactic:
simp only [iSup_of_empty', ciSup_const]

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

Goal state before:
pp: α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Finset α
h : s.Nonempty
⊢ sSup ↑s ∈ s

Tactic:
by
  rw [h.csSup_eq_max']
  exact s.max'_mem _

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

Goal state before:
pp: ι : Type u_5
s : Set ι
hs : s.Nonempty
α : Type u_6
inst✝ : CompleteLattice α
f : ι → α
⊢ ↑(⨆ i ∈ s, f i) = ⨆ i ∈ s, ↑(f i)

Tactic:
rcases hs with ⟨j, hj⟩

Goal state after:
ι : Type u_5
s : Set ι
α : Type u_6
inst✝ : CompleteLattice α
f : ι → α
j : ι
hj : j ∈ s
⊢ ↑(⨆ i ∈ s, f i) = ⨆ i ∈ s, ↑(f i)
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case pos
ι : Type u_5
s : Set ι
α : Type u_6
inst✝ : CompleteLattice α
f : ι → α
j : ι
hj : j ∈ s
this : Nonempty ι
i : ι
h : i ∈ s
⊢ ↑(⨆ (_ : i ∈ s), f i) ≤ ⨆ i ∈ s, ↑(f i)

pp: case neg
ι : Type u_5
s : Set ι
α : Type u_6
inst✝ : CompleteLattice α
f : ι → α
j : ι
hj : j ∈ s
this : Nonempty ι
i : ι
h : i ∉ s
⊢ ↑(⨆ (_ : i ∈ s), f i) ≤ ⨆ i ∈ s, ↑(f i)

Tactic:
· simpa only [iSup_pos h] using by apply le_biSup _ h

Goal state after:
case neg
ι : Type u_5
s : Set ι
α : Type u_6
inst✝ : CompleteLattice α
f : ι → α
j : ι
hj : j ∈ s
this : Nonempty ι
i : ι
h : i ∉ s
⊢ ↑(⨆ (_ : i ∈ s), f i) ≤ ⨆ i ∈ s, ↑(f i)
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case inr
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
f g : ι → α
Hf : BddAbove (range f)
Hg : BddAbove (range g)
h✝ : Nonempty ι
this : BddAbove (range fun x ↦ f x ⊔ g x)
⊢ iSup f ⊔ iSup g ≤ ⨆ x, f x ⊔ g x

Tactic:
exact sup_le (ciSup_mono this fun _ ↦ le_sup_left) (ciSup_mono this fun _ ↦ le_sup_right)

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
⊢ some '' some ⁻¹' Ioi ↑a = Ioo ↑a ⊤

Tactic:
image_preimage_eq_inter_range,

Goal state after:
α : Type u_1
inst✝ : Preorder α
a : α
⊢ Ioi ↑a ∩ range some = Ioo ↑a ⊤
Module: Mathlib.Order.Interval.Set.WithBotTop

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
⊢ some '' some ⁻¹' Ici ↑a = Ico ↑a ⊤

Tactic:
image_preimage_eq_inter_range,

Goal state after:
α : Type u_1
inst✝ : Preorder α
a : α
⊢ Ici ↑a ∩ range some = Ico ↑a ⊤
Module: Mathlib.Order.Interval.Set.WithBotTop

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

Tactic:
image_preimage_eq_inter_range,

Goal state after:
α : Type u_1
inst✝ : Preorder α
a : α
⊢ Iio ↑a ∩ range some = Iio ↑a
Module: Mathlib.Order.Interval.Set.WithBotTop

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

Tactic:
image_preimage_eq_inter_range,

Goal state after:
α : Type u_1
inst✝ : Preorder α
a : α
⊢ Iic ↑a ∩ range some = Iic ↑a
Module: Mathlib.Order.Interval.Set.WithBotTop

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ some '' some ⁻¹' Icc ↑a ↑b = Icc ↑a ↑b

Tactic:
image_preimage_eq_inter_range,

Goal state after:
α : Type u_1
inst✝ : Preorder α
a b : α
⊢ Icc ↑a ↑b ∩ range some = Icc ↑a ↑b
Module: Mathlib.Order.Interval.Set.WithBotTop

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ some '' some ⁻¹' Ico ↑a ↑b = Ico ↑a ↑b

Tactic:
image_preimage_eq_inter_range,

Goal state after:
α : Type u_1
inst✝ : Preorder α
a b : α
⊢ Ico ↑a ↑b ∩ range some = Ico ↑a ↑b
Module: Mathlib.Order.Interval.Set.WithBotTop

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ some '' some ⁻¹' Ioc ↑a ↑b = Ioc ↑a ↑b

Tactic:
image_preimage_eq_inter_range,

Goal state after:
α : Type u_1
inst✝ : Preorder α
a b : α
⊢ Ioc ↑a ↑b ∩ range some = Ioc ↑a ↑b
Module: Mathlib.Order.Interval.Set.WithBotTop

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ some '' some ⁻¹' Ioo ↑a ↑b = Ioo ↑a ↑b

Tactic:
image_preimage_eq_inter_range,

Goal state after:
α : Type u_1
inst✝ : Preorder α
a b : α
⊢ Ioo ↑a ↑b ∩ range some = Ioo ↑a ↑b
Module: Mathlib.Order.Cover

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ a₂ : α
b₁ b₂ : β
⊢ a₁ ⩿ a₂ ∧ b₁ = b₂ ∨ b₁ ⩿ b₂ ∧ a₁ = a₂ → (a₁, b₁) ⩿ (a₂, b₂)

Tactic:
· rintro (⟨h, rfl⟩ | ⟨h, rfl⟩)
    · exact mk_wcovBy_mk_iff_left.2 h
    · exact mk_wcovBy_mk_iff_right.2 h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : Preorder β
inst✝² : Fintype α
inst✝¹ : DecidableLT α
inst✝ : DecidableLE α
a b x : α
⊢ x ∈ (Set.Icc a b).toFinset ↔ a ≤ x ∧ x ≤ b

Tactic:
by simp only [Set.mem_toFinset, Set.mem_Icc]

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, IsMin (a 0) ∧ ∃ n, IsMax (a n) ∧ ∀ i < n, a i ⋖ a (i + 1)

Tactic:
let a : ℕ → α := Nat.rec (wfl.wf.min _ hα) fun _n a ↦ if ha : IsMax a then a else next ha
  refine ⟨a, isMin_iff_forall_not_lt.mpr fun _ ↦ wfl.wf.not_lt_min _ (Set.mem_univ _), ?_⟩
  have cov n (hn : ¬ IsMax (a n)) : a n ⋖ a (n + 1) := by
    change a n ⋖ if ha : IsMax (a n) then a n else _
    rw [dif_neg hn]
    exact hnext hn
  have H : ∃ n, IsMax (a n) := by
    by_contra!
    exact (RelEmbedding.natGT a fun n ↦ (cov n (this n)).1).not_wellFounded wfg.wf
  exact ⟨_, wellFounded_lt.min_mem _ H, fun i h ↦ cov _ (wellFounded_lt.not_lt_min _ · h)⟩

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

Goal state before:
pp: case h
M : Type u_3
inst✝³ : Monoid M
N : Type u_7
inst✝² : CommMonoid N
inst✝¹ : MulAction M N
inst✝ : IsScalarTower M N N
r : M
s : Set N
x✝ x y : N
hx✝¹ : x ∈ closure s
hy✝¹ : y ∈ closure s
hx✝ : ∃ n, r ^ n • x ∈ closure (r • s)
hy✝ : ∃ n, r ^ n • y ∈ closure (r • s)
nx : ℕ
hx : r ^ nx • x ∈ closure (r • s)
ny : ℕ
hy : r ^ ny • y ∈ closure (r • s)
⊢ r ^ ny • y * r ^ nx • x ∈ closure (r • s)

Tactic:
exact mul_mem hy hx

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

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

Tactic:
← Set.inv_subset,

Goal state after:
case a
G : Type u_2
inst✝ : Group G
s : Set G
⊢ s⁻¹⁻¹ ⊆ ↑(closure s)
Module: Mathlib.Algebra.Group.Submonoid.Pointwise

Goal state before:
pp: α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
S✝ : Type u_6
inst✝³ : Monoid M
inst✝² : AddMonoid A
inst✝¹ : Monoid α
inst✝ : MulDistribMulAction α M
S : Submonoid M
⊢ 1 • S = S

Tactic:
change S.map _ = S

Goal state after:
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
S✝ : Type u_6
inst✝³ : Monoid M
inst✝² : AddMonoid A
inst✝¹ : Monoid α
inst✝ : MulDistribMulAction α M
S : Submonoid M
⊢ map ((MulDistribMulAction.toMonoidEnd α M) 1) S = S
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c d : α
⊢ Set.Ico a b ∩ Set.Ico c d = Set.Ico (max a c) (min b d)

Tactic:
Set.Ico_inter_Ico

Goal state after:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c d : α
⊢ Set.Ico (max a c) (min b d) = Set.Ico (max a c) (min b d)
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:
exact (hg.comm (ϕ h)).symm

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

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

Tactic:
rw [List.prod_cons, List.foldr, hl]

Goal state after:
case cons
α : Type u_3
inst✝ : Monoid α
hd : α
tl : List α
hl : {x | x ∈ ↑tl}.Pairwise Commute → List.foldr (fun x1 x2 ↦ x1 * x2) 1 tl = tl.prod
comm : {x | x ∈ ↑(hd :: tl)}.Pairwise Commute
⊢ {x | x ∈ ↑tl}.Pairwise Commute
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: α : Type u_3
inst✝ : Monoid α
s : Multiset α
a : α
comm : {x | x ∈ a ::ₘ s}.Pairwise Commute
⊢ (a ::ₘ s).noncommProd comm = s.noncommProd ⋯ * a

Tactic:
induction s using Quotient.inductionOn with

Goal state after:
case h
α : Type u_3
inst✝ : Monoid α
a : α
s : List α
comm : {x | x ∈ a ::ₘ ⟦s⟧}.Pairwise Commute
⊢ (a ::ₘ ⟦s⟧).noncommProd comm = noncommProd ⟦s⟧ ⋯ * a
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: α : Type u_3
inst✝ : Monoid α
s : Multiset α
comm : {x | x ∈ s}.Pairwise Commute
p : α → Prop
hom : ∀ (a b : α), p a → p b → p (a * b)
unit : p 1
base : ∀ x ∈ s, p x
⊢ p (s.noncommProd comm)

Tactic:
induction s using Quotient.inductionOn with

Goal state after:
case h
α : Type u_3
inst✝ : Monoid α
p : α → Prop
hom : ∀ (a b : α), p a → p b → p (a * b)
unit : p 1
l : List α
comm : {x | x ∈ ⟦l⟧}.Pairwise Commute
base : ∀ x ∈ ⟦l⟧, p x
⊢ p (noncommProd ⟦l⟧ comm)
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: α : Type u_3
inst✝¹ : Monoid α
inst✝ : DecidableEq α
s : Multiset α
a : α
h : a ∈ s
comm : {x | x ∈ s}.Pairwise Commute
comm' : ∀ x ∈ {x | x ∈ s.erase a}, ∀ x_1 ∈ {x | x ∈ s.erase a}, x ≠ x_1 → Commute x x_1
⊢ a * (s.erase a).noncommProd comm' = s.noncommProd comm

Tactic:
induction s using Quotient.inductionOn with

Goal state after:
case h
α : Type u_3
inst✝¹ : Monoid α
inst✝ : DecidableEq α
a : α
l : List α
h : a ∈ ⟦l⟧
comm : {x | x ∈ ⟦l⟧}.Pairwise Commute
comm' : ∀ x ∈ {x | x ∈ erase ⟦l⟧ a}, ∀ x_1 ∈ {x | x ∈ erase ⟦l⟧ a}, x ≠ x_1 → Commute x x_1
⊢ a * (erase ⟦l⟧ a).noncommProd comm' = noncommProd ⟦l⟧ comm
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: α : Type u_1
G : Type u_2
A : Type u_3
S✝ : Type u_4
inst✝³ : Group G
inst✝² : AddGroup A
s : Set G
inst✝¹ : Monoid α
inst✝ : MulDistribMulAction α G
S : Subgroup G
⊢ 1 • S = S

Tactic:
change S.map _ = S

Goal state after:
α : Type u_1
G : Type u_2
A : Type u_3
S✝ : Type u_4
inst✝³ : Group G
inst✝² : AddGroup A
s : Set G
inst✝¹ : Monoid α
inst✝ : MulDistribMulAction α G
S : Subgroup G
⊢ map ((MulDistribMulAction.toMonoidEnd α G) 1) S = S
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H : Subgroup G
h : ∀ (g : G), MulAut.conj g • H = H
n : G
hn : n ∈ H
g : G
⊢ MulAut.conj g⁻¹ • (g * n * g⁻¹) ∈ H

Tactic:
MulAut.smul_def,

Goal state after:
G : Type u_2
inst✝ : Group G
H : Subgroup G
h : ∀ (g : G), MulAut.conj g • H = H
n : G
hn : n ∈ H
g : G
⊢ (MulAut.conj g⁻¹) (g * n * g⁻¹) ∈ H
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: M : Type u_3
inst✝ : AddMonoid M
s : List M
⊢ ofAdd s.sum = (List.map (⇑ofAdd) s).prod

Tactic:
by simp [ofAdd]; rfl

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

Goal state before:
pp: case mul.e_a
M : Type u_1
inst✝ : CommMonoid M
x : M
s : Set M
f : M → ℕ
t : Finset M
hts : ↑t ⊆ s
hf : Function.support f ⊆ ↑t
hx✝ : ∏ a ∈ t, a ^ f a ∈ closure s
g : M → ℕ
u : Finset M
hus : ↑u ⊆ s
hg : Function.support g ⊆ ↑u
hy✝ : ∏ a ∈ u, a ^ g a ∈ closure s
⊢ ∏ x ∈ u, x ^ g x = ∏ x ∈ t ∪ u, x ^ g x

Tactic:
refine Finset.prod_subset Finset.subset_union_right ?_
      simp +contextual [Function.support_subset_iff'.1 hg]

Goal state after:
Module: Mathlib.Data.Setoid.Basic

Goal state before:
pp: α : Type u_1
s : Setoid α
⊢ Subsingleton (Quotient s) ↔ s = ⊤

Tactic:
simp only [_root_.subsingleton_iff, eq_top_iff, Setoid.le_def, Setoid.top_def, Pi.top_apply]
  refine Quotient.mk'_surjective.forall.trans (forall_congr' fun a => ?_)
  refine Quotient.mk'_surjective.forall.trans (forall_congr' fun b => ?_)
  simp_rw [Prop.top_eq_true, true_implies, Quotient.eq']

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

Goal state before:
pp: case mpr.inr
α : Type u
L₂ : List (α × Bool)
a : α
b : Bool
⊢ Step ((a, b) :: (a, !b) :: L₂) L₂

Tactic:
exact Step.cons_not

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
g✝ : Quotient (rightRel s)
g : α
⊢ (rightRel s) ((fun g ↦ g⁻¹) ((fun g ↦ g⁻¹) g)) g

Tactic:
simp only [inv_inv]

Goal state after:
α : Type u_1
inst✝ : Group α
s : Subgroup α
g✝ : Quotient (rightRel s)
g : α
⊢ (rightRel s) g g
Module: Mathlib.GroupTheory.Coset.Defs

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
g✝ : α ⧸ s
g : α
⊢ (leftRel s) ((fun g ↦ g⁻¹) ((fun g ↦ g⁻¹) g)) g

Tactic:
simp only [inv_inv]

Goal state after:
α : Type u_1
inst✝ : Group α
s : Subgroup α
g✝ : α ⧸ s
g : α
⊢ (leftRel s) g g
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

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

Tactic:
mul_prod_erase s f h

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
f : ι → M
inst✝ : DecidableEq ι
s : Finset κ
t : κ → Finset ι
hs : (↑s).Pairwise fun i j ↦ ∀ k ∈ t i ∩ t j, f k = 1
t' : κ → Finset ι := fun k ↦ {i ∈ t k | f i ≠ 1}
this : s.biUnion t' = {i ∈ s.biUnion t | f i ≠ 1}
⊢ (↑s).PairwiseDisjoint t'

Tactic:
intro i hi j hj hij a hai haj k hk

Goal state after:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
f : ι → M
inst✝ : DecidableEq ι
s : Finset κ
t : κ → Finset ι
hs : (↑s).Pairwise fun i j ↦ ∀ k ∈ t i ∩ t j, f k = 1
t' : κ → Finset ι := fun k ↦ {i ∈ t k | f i ≠ 1}
this : s.biUnion t' = {i ∈ s.biUnion t | f i ≠ 1}
i : κ
hi : i ∈ ↑s
j : κ
hj : j ∈ ↑s
hij : i ≠ j
a : Finset ι
hai : a ⊆ t' i
haj : a ⊆ t' j
k : ι
hk : k ∈ a
⊢ k ∈ ⊥
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case of
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
x y : FreeAbelianGroup α
L3 : α
⊢ x * y * of L3 = x * (y * of L3)

Tactic:
induction y using FreeAbelianGroup.induction_on with

Goal state after:
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
f : α →* R
x y : FreeAbelianGroup α
⊢ (lift ⇑f) (x * y) = (lift ⇑f) x * (lift ⇑f) y

Tactic:
induction y using FreeAbelianGroup.induction_on with

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case of
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : CommMonoid α
y : FreeAbelianGroup α
s : α
⊢ of s * y = y * of s

Tactic:
induction y using FreeAbelianGroup.induction_on with

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

Goal state before:
pp: M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝ : CommMonoid Q
k : T.LocalizationMap Q
or : Set.SurjOn ⇑g ↑S ↑T ∨ Injective ⇑k
hg : Injective ⇑g
z w : N
i : N →* Q := f.map hy k
hizw : i z = i w
ifkg : ∀ (a : M), i (f a) = k (g a)
z' w' : M
x : ↥S
hxz : z * f ↑x = f z'
hxw : w * f ↑x = f w'
⊢ i z * i (f ↑x) = i w * i (f ↑x)

Tactic:
hizw

Goal state after:
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝ : CommMonoid Q
k : T.LocalizationMap Q
or : Set.SurjOn ⇑g ↑S ↑T ∨ Injective ⇑k
hg : Injective ⇑g
z w : N
i : N →* Q := f.map hy k
hizw : i z = i w
ifkg : ∀ (a : M), i (f a) = k (g a)
z' w' : M
x : ↥S
hxz : z * f ↑x = f z'
hxw : w * f ↑x = f w'
⊢ i w * i (f ↑x) = i w * i (f ↑x)
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
R' : Type u_2
M : Type u_3
X : Type u_4
inst✝¹² : Monoid M
S : Submonoid M
inst✝¹¹ : OreSet S
inst✝¹⁰ : MulAction M X
inst✝⁹ : SMul R X
inst✝⁸ : SMul R M
inst✝⁷ : IsScalarTower R M M
inst✝⁶ : IsScalarTower R M X
inst✝⁵ : SMul R' X
inst✝⁴ : SMul R' M
inst✝³ : IsScalarTower R' M M
inst✝² : IsScalarTower R' M X
inst✝¹ : SMul R R'
inst✝ : IsScalarTower R R' M
r : R
m : R'
x : OreLocalization S X
⊢ (r • m) • x = r • m • x

Tactic:
by
    rw [← smul_one_oreDiv_one_smul, ← smul_one_oreDiv_one_smul, ← smul_one_oreDiv_one_smul,
      ← mul_smul, mul_div_one]
    simp only [smul_mul_assoc, smul_assoc, one_mul]

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

Goal state before:
pp: case inr.coe.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulMono α
x : α
x0 : 0 ≤ ↑x
x0' : ↑x ≠ 0
a✝¹ a✝ : α
h : ↑a✝¹ ≤ ↑a✝
⊢ ↑x * ↑a✝¹ ≤ ↑x * ↑a✝

Tactic:
simp only [← coe_mul, coe_le_coe] at *

Goal state after:
case inr.coe.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulMono α
x : α
x0 : 0 ≤ ↑x
x0' : ↑x ≠ 0
a✝¹ a✝ : α
h : a✝¹ ≤ a✝
⊢ x * a✝¹ ≤ x * a✝
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case inr.coe.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosMono α
x : α
x0 : 0 ≤ ↑x
x0' : ↑x ≠ 0
a✝¹ a✝ : α
h : ↑a✝¹ ≤ ↑a✝
⊢ ↑a✝¹ * ↑x ≤ ↑a✝ * ↑x

Tactic:
simp only [← coe_mul, coe_le_coe] at *

Goal state after:
case inr.coe.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosMono α
x : α
x0 : 0 ≤ ↑x
x0' : ↑x ≠ 0
a✝¹ a✝ : α
h : a✝¹ ≤ a✝
⊢ a✝¹ * x ≤ a✝ * x
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case coe.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLE α
x : α
x0 : 0 < ↑x
a✝¹ a✝ : α
h : ↑x * ↑a✝¹ ≤ ↑x * ↑a✝
⊢ ↑a✝¹ ≤ ↑a✝

Tactic:
simp only [← coe_mul, coe_le_coe] at *

Goal state after:
case coe.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLE α
x : α
x0 : 0 < ↑x
a✝¹ a✝ : α
h : x * a✝¹ ≤ x * a✝
⊢ a✝¹ ≤ a✝
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case coe.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLE α
x : α
x0 : 0 < ↑x
a✝¹ a✝ : α
h : ↑a✝¹ * ↑x ≤ ↑a✝ * ↑x
⊢ ↑a✝¹ ≤ ↑a✝

Tactic:
simp only [← coe_mul, coe_le_coe] at *

Goal state after:
case coe.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLE α
x : α
x0 : 0 < ↑x
a✝¹ a✝ : α
h : a✝¹ * x ≤ a✝ * x
⊢ a✝¹ ≤ a✝
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
a : α
inst✝³ : Preorder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : NoMaxOrder α
h : IsSuccPrelimit a
⊢ IsMin a

Tactic:
by
  intro b hb
  rcases hb.exists_succ_iterate with ⟨_ | n, rfl⟩
  · exact le_rfl
  · rw [iterate_succ_apply'] at h
    exact (not_isSuccPrelimit_succ _ h).elim

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

Goal state before:
pp: case neg
α : 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] (pred c) = b
h : pred ↑⟨c, hc⟩ ∉ s
this : pred ⟨c, hc⟩ = ⟨c, hc⟩
⊢ ⟨c, hc⟩ = ⟨b, hb⟩

Tactic:
simp only [Order.pred_eq_iff_isMin] at this
          apply (this.eq_of_le _).symm
          exact hbc

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α
inst✝⁴ : Preorder β
inst✝³ : Add α
inst✝² : One α
inst✝¹ : SuccAddOrder α
inst✝ : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
⊢ (∀ (a : α), ¬IsMax a → a ∈ s → a + 1 ∈ s → f a ≤ f (a + 1)) → MonotoneOn f s

Tactic:
by
  simpa [Order.succ_eq_add_one] using monotoneOn_of_le_succ hs (f := f)

Goal state after:
Module: Mathlib.Logic.Small.Defs

Goal state before:
pp: α : Type u_2
β : α → Type u_1
inst✝¹ : Small.{w, u_2} α
inst✝ : ∀ (a : α), Small.{w, u_1} (β a)
a : α
⊢ β a ≃ Shrink.{w, u_1} (β ((equivShrink α).symm ((equivShrink α) a)))

Tactic:
by simpa using equivShrink (β a)

Goal state after: