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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
⊢ sigmaLift f a b ≠ ∅ ↔ ∃ (h : a.fst = b.fst), f (⋯ ▸ a.snd) b.snd ≠ ∅

Tactic:
sigmaLift

Goal state after:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
⊢ (if h : a.fst = b.fst then map (Embedding.sigmaMk b.fst) (f (h ▸ a.snd) b.snd) else ∅) ≠ ∅ ↔
    ∃ (h : a.fst = b.fst), f (⋯ ▸ a.snd) b.snd ≠ ∅
Module: Mathlib.Data.Finset.Sigma

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
⊢ sigmaLift f a b = ∅ ↔ ∀ (h : a.fst = b.fst), f (h ▸ a.snd) b.snd = ∅

Tactic:
sigmaLift

Goal state after:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
⊢ (if h : a.fst = b.fst then map (Embedding.sigmaMk b.fst) (f (h ▸ a.snd) b.snd) else ∅) = ∅ ↔
    ∀ (h : a.fst = b.fst), f (h ▸ a.snd) b.snd = ∅
Module: Mathlib.Data.Finset.Sigma

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
⊢ #(sigmaLift f a b) = if h : a.fst = b.fst then #(f (h ▸ a.snd) b.snd) else 0

Tactic:
sigmaLift

Goal state after:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
⊢ #(if h : a.fst = b.fst then map (Embedding.sigmaMk b.fst) (f (h ▸ a.snd) b.snd) else ∅) =
    if h : a.fst = b.fst then #(f (h ▸ a.snd) b.snd) else 0
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝² : LinearOrder α
inst✝¹ : PartialOrder β
inst✝ : Finite α
f g : α ↪o β
h : Set.range ⇑f = Set.range ⇑g
ef : ↑Set.univ ≃o ↑(⇑f '' Set.univ) := StrictMonoOn.orderIso (⇑f) Set.univ ⋯
eg : ↑Set.univ ≃o ↑(⇑g '' Set.univ) := StrictMonoOn.orderIso (⇑g) Set.univ ⋯
i : ↑(⇑f '' Set.univ) ≃o ↑(⇑g '' Set.univ) :=
  let __spread.0 := Equiv.setCongr ⋯;
  { toEquiv := __spread.0, map_rel_iff' := ⋯ }
this : (ef.trans i).trans eg.symm = OrderIso.refl ↑Set.univ
x : α
⊢ f x = g x

Tactic:
simpa only [OrderIso.trans_apply, OrderIso.apply_symm_apply, OrderIso.refl_apply, Subtype.ext_iff]
    using! congr(eg ($this ⟨x, Set.mem_univ x⟩))

Goal state after:
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred fun x ↦ x < c
hcb : c ≤ b
⊢ filter (fun x ↦ x < c) (Ico a b) = Ico a c

Tactic:
by
  rw [Ico, ← Finset.filter_val, Finset.Ico_filter_lt_of_le_right hcb]
  rfl

Goal state after:
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: s : Set ℕ
h : 0 < sInf s
contra : s = ∅
h' : sInf s ≠ 0
⊢ sInf s = 0

Tactic:
Nat.sInf_eq_zero

Goal state after:
s : Set ℕ
h : 0 < sInf s
contra : s = ∅
h' : sInf s ≠ 0
⊢ 0 ∈ s ∨ s = ∅
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a b c : ℕ
h : c ≤ a
x : ℕ
⊢ (∃ a_1, (a ≤ a_1 ∧ a_1 < b) ∧ a_1 - c = x) → a - c ≤ x ∧ x < b - c

Tactic:
rintro ⟨x, hx, rfl⟩

Goal state after:
a b c : ℕ
h : c ≤ a
x : ℕ
hx : a ≤ x ∧ x < b
⊢ a - c ≤ x - c ∧ x - c < b - c
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a b c : ℕ
hac : a ≤ c
x : ℕ
⊢ (∃ a_1, (a ≤ a_1 ∧ a_1 < b) ∧ c - a_1 = x) → c + 1 - b ≤ x ∧ x < c + 1 - a

Tactic:
rintro ⟨x, hx, rfl⟩

Goal state after:
a b c : ℕ
hac : a ≤ c
x : ℕ
hx : a ≤ x ∧ x < b
⊢ c + 1 - b ≤ c - x ∧ c - x < c + 1 - a
Module: Mathlib.Order.WellQuasiOrder

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

Tactic:
refine ⟨g, fun m n hle => ?_⟩

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
x : α
hx : ↑a ≤ x ∧ x < ↑b
⊢ p x

Tactic:
exact hp hx.1 hx.2.le a.prop b.prop

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x✝ : WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s → s.Finite
hwf : WellFoundedLT α
hc : ∀ (s : Set α), IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s → s.Finite
f : ℕ → α
⊢ ∃ m n, m < n ∧ (fun x1 x2 ↦ x1 ≤ x2) (f m) (f n)

Tactic:
obtain ⟨g, h1 | h2⟩ := exists_increasing_or_nonincreasing_subseq (· > ·) f

Goal state after:
case inl
α : Type u_1
inst✝ : Preorder α
x✝ : WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s → s.Finite
hwf : WellFoundedLT α
hc : ∀ (s : Set α), IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s → s.Finite
f : ℕ → α
g : ℕ ↪o ℕ
h1 : ∀ (m n : ℕ), m < n → f (g m) > f (g n)
⊢ ∃ m n, m < n ∧ (fun x1 x2 ↦ x1 ≤ x2) (f m) (f n)

case inr
α : Type u_1
inst✝ : Preorder α
x✝ : WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s → s.Finite
hwf : WellFoundedLT α
hc : ∀ (s : Set α), IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s → s.Finite
f : ℕ → α
g : ℕ ↪o ℕ
h2 : ∀ (m n : ℕ), m < n → ¬f (g m) > f (g n)
⊢ ∃ m n, m < n ∧ (fun x1 x2 ↦ x1 ≤ x2) (f m) (f n)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
⊢ (Icc a b).erase a = Ioc a b

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
⊢ (Icc a b).erase b = Ico a b

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
⊢ (Ico a b).erase a = Ioo a b

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
⊢ (Ioc a b).erase b = Ioo a b

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
⊢ Icc a b \ {a, b} = Ioo a b

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: case inl
α : Type u_3
inst✝² : Nonempty α
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
⊢ ∅.Finite ↔ BddBelow ∅ ∧ BddAbove ∅

pp: case inr
α : Type u_3
s : Set α
inst✝² : Nonempty α
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
hs : s.Nonempty
⊢ s.Finite ↔ BddBelow s ∧ BddAbove s

Tactic:
· simp only [Set.finite_empty, bddBelow_empty, bddAbove_empty, and_self]

Goal state after:
case inr
α : Type u_3
s : Set α
inst✝² : Nonempty α
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
hs : s.Nonempty
⊢ s.Finite ↔ BddBelow s ∧ BddAbove s
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
p : α → Prop
inst✝² : DecidablePred p
y : α
inst✝¹ : DecidableLT α
inst✝ : LocallyFiniteOrder α
a b : { x // x < y }
⊢ b ∈ Finset.subtype (fun x ↦ x < y) (Ioo (↑a) y) ↔ a < b

Tactic:
simp only [Finset.mem_subtype, Finset.mem_Ioo, Subtype.coe_lt_coe, and_iff_left_iff_imp]
    exact fun _ => b.property

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

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

Tactic:
by
  classical rw [cons_eq_insert, Ioc_insert_left h]

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hα : ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ (fun x ↦ (ofLex x).1) '' s) → ∃ g, Monotone (f ∘ ⇑g)
hβ : ∀ (a : α), {y | toLex (a, y) ∈ s}.IsPWO
f : ℕ → Lex (α × β)
hf : ∀ (n : ℕ), f n ∈ s
⊢ ∃ m n, m < n ∧ f m ≤ f n

Tactic:
obtain ⟨g, hg⟩ : ∃ (g : (ℕ ↪o ℕ)), Monotone fun n => (ofLex f (g n)).1 :=
    hα (fun n => (ofLex f n).1) (fun k => mem_image_of_mem (fun x => (ofLex x).1) (hf k))

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hα : ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ (fun x ↦ (ofLex x).1) '' s) → ∃ g, Monotone (f ∘ ⇑g)
hβ : ∀ (a : α), {y | toLex (a, y) ∈ s}.IsPWO
f : ℕ → Lex (α × β)
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
hg : Monotone fun n ↦ (ofLex f (g n)).1
⊢ ∃ m n, m < n ∧ f m ≤ f n
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:
by
  induction s using Quotient.inductionOn with | _ s
  simp only [quot_mk_to_coe, cons_coe, noncommProd_coe, List.prod_cons]
  induction s with
  | nil => simp
  | cons hd tl IH =>
    rw [List.prod_cons, mul_assoc, ← IH, ← mul_assoc, ← mul_assoc]
    · congr 1
      apply comm.of_refl <;> simp
    · intro x hx y hy
      simp only [quot_mk_to_coe, List.mem_cons, mem_coe, cons_coe] at hx hy
      apply comm
      · cases hx <;> simp [*]
      · cases hy <;> simp [*]

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

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 | _ l
   =>  _ 

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.BigOperators.Group.Finset.Defs

Goal state before:
pp: case refine_1
ι : 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)
⊢ ∀ a ∈ s, e a ∈ t

Tactic:
simp [hst]

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

Goal state before:
pp: case refine_2
ι : 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)
⊢ ∀ a ∈ t, e.symm a ∈ s

Tactic:
simp [hst]

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

Goal state before:
pp: case refine_3
ι : 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)
⊢ ∀ a ∈ s, e.symm (e a) = a

Tactic:
simp [hst]

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

Goal state before:
pp: case refine_4
ι : 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)
⊢ ∀ a ∈ t, e (e.symm a) = a

Tactic:
simp [hst]

Goal state after:
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:
cases c; congr!

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

Goal state before:
pp: case mp
α : Type u
L₁ L₂ : List (α × Bool)
a : α
b : Bool
L : List (α × Bool)
hL : (a, b) :: L₁ = L
⊢ Step L L₂ → (∃ L, Step L₁ L ∧ L₂ = (a, b) :: L) ∨ L₁ = (a, !b) :: L₂

Tactic:
rintro @⟨_ | ⟨p, s'⟩, e, a', b'⟩

Goal state after:
case mp.nil
α : Type u
L₁ : List (α × Bool)
a : α
b : Bool
e : List (α × Bool)
a' : α
b' : Bool
hL : (a, b) :: L₁ = [] ++ (a', b') :: (a', !b') :: e
⊢ (∃ L, Step L₁ L ∧ [] ++ e = (a, b) :: L) ∨ L₁ = (a, !b) :: ([] ++ e)

case mp.cons
α : Type u
L₁ : List (α × Bool)
a : α
b : Bool
e : List (α × Bool)
a' : α
b' : Bool
p : α × Bool
s' : List (α × Bool)
hL : (a, b) :: L₁ = p :: s' ++ (a', b') :: (a', !b') :: e
⊢ (∃ L, Step L₁ L ∧ p :: s' ++ e = (a, b) :: L) ∨ L₁ = (a, !b) :: (p :: s' ++ e)
Module: Mathlib.GroupTheory.Coset.Defs

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
⊢ ∀ (a b : α), (rightRel s) a b = (b * a⁻¹ ∈ s)

Tactic:
simp only [eq_iff_iff]
    apply rightRel_apply

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

Goal state before:
pp: G : Type u_1
M : Type u_4
inst✝¹ : Group G
inst✝ : Monoid M
f : G →* M
⊢ QuotientGroup.con f.ker = Con.ker f

Tactic:
ext
  rw [QuotientGroup.con, Con.rel_mk, Setoid.comm', leftRel_apply, Con.ker_rel, MonoidHom.eq_iff]

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

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
f : ℕ → M
n m : ℕ
⊢ ∏ x ∈ range (n + m), f x = (∏ x ∈ range n, f x) * ∏ x ∈ range m, f (n + x)

Tactic:
by
  induction m with
  | zero => simp
  | succ m hm => rw [Nat.add_succ, prod_range_succ, prod_range_succ, hm, mul_assoc]

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
inst✝ : Mul α
x y : α
⊢ (lift fun x₂ ↦ (lift fun x₁ ↦ of (x₁ * x₂)) (of x)) (of y) = of (x * y)

Tactic:
lift_apply_of,

Goal state after:
α : Type u
inst✝ : Mul α
x y : α
⊢ (lift fun x₁ ↦ of (x₁ * y)) (of x) = 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:
h.eq_bot.le

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

Goal state before:
pp: case right
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
f : G →* G'
p : G
hp : p ∈ ↑H₁
q : G
hq : q ∈ ↑H₂
⊢ ⁅f p, f q⁆ ∈ map f ⁅H₁, H₂⁆

Tactic:
rw [← map_commutatorElement]

Goal state after:
case right
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
f : G →* G'
p : G
hp : p ∈ ↑H₁
q : G
hq : q ∈ ↑H₂
⊢ f ⁅p, q⁆ ∈ map f ⁅H₁, H₂⁆
Module: Mathlib.GroupTheory.FreeAbelianGroup

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

Tactic:
lift_apply_of,

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

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

Tactic:
lift_apply_of,

Goal state after:
case of
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
L : α
⊢ of (L * 1) = of L
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₁ r₂ : R
s t : ↥S
h : ↑t * r = ↑t * r'
r₁' : R
t' : ↥S
hr₁ : ↑t' * r₁ = r₁' * ↑t
⊢ ↑t' * (r₁ * r * r₂) = ↑t' * r₁ * r * r₂

Tactic:
simp [← mul_assoc]

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₁ r₂ : R
s t : ↥S
h : ↑t * r = ↑t * r'
r₁' : R
t' : ↥S
hr₁ : ↑t' * r₁ = r₁' * ↑t
⊢ r₁' * ↑t * r * r₂ = r₁' * (↑t * r) * r₂

Tactic:
simp [← mul_assoc]

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₁ r₂ : R
s t : ↥S
h : ↑t * r = ↑t * r'
r₁' : R
t' : ↥S
hr₁ : ↑t' * r₁ = r₁' * ↑t
⊢ r₁' * (↑t * r') * r₂ = r₁' * ↑t * r' * r₂

Tactic:
simp [← mul_assoc]

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₁ r₂ : R
s t : ↥S
h : ↑t * r = ↑t * r'
r₁' : R
t' : ↥S
hr₁ : ↑t' * r₁ = r₁' * ↑t
⊢ ↑t' * r₁ * r' * r₂ = ↑t' * (r₁ * r' * r₂)

Tactic:
simp [← mul_assoc]

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

Goal state before:
pp: case h.left
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₂ u : ↥S
v : R
huv : ↑u * r₁ = v * ↑s₂
v₀ : R := ⋯
u₀ : ↥S := ⋯
h₀ : ↑u₀ * r₁ = v₀ * ↑s₂
r₃ : R
s₃ : ↥S
h₃ : ↑s₃ * ↑u₀ = r₃ * ↑u
this : r₃ * v * ↑s₂ = ↑s₃ * v₀ * ↑s₂
s₄ : ↥S
hs₄ : ↑s₄ * (r₃ * v) = ↑s₄ * (↑s₃ * v₀)
⊢ (↑s₄ * ↑s₃) • v₀ • r₂ = (↑s₄ * r₃) • v • r₂

pp: case h.right
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₂ u : ↥S
v : R
huv : ↑u * r₁ = v * ↑s₂
v₀ : R := ⋯
u₀ : ↥S := ⋯
h₀ : ↑u₀ * r₁ = v₀ * ↑s₂
r₃ : R
s₃ : ↥S
h₃ : ↑s₃ * ↑u₀ = r₃ * ↑u
this : r₃ * v * ↑s₂ = ↑s₃ * v₀ * ↑s₂
s₄ : ↥S
hs₄ : ↑s₄ * (r₃ * v) = ↑s₄ * (↑s₃ * v₀)
⊢ ↑s₄ * ↑s₃ * (↑u₀ * ↑s₁) = ↑s₄ * r₃ * (↑u * ↑s₁)

Tactic:
· rw [smul_smul, mul_assoc (c := v₀), ← hs₄]
    simp only [smul_smul, mul_assoc]

Goal state after:
case h.right
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₂ u : ↥S
v : R
huv : ↑u * r₁ = v * ↑s₂
v₀ : R := ⋯
u₀ : ↥S := ⋯
h₀ : ↑u₀ * r₁ = v₀ * ↑s₂
r₃ : R
s₃ : ↥S
h₃ : ↑s₃ * ↑u₀ = r₃ * ↑u
this : r₃ * v * ↑s₂ = ↑s₃ * v₀ * ↑s₂
s₄ : ↥S
hs₄ : ↑s₄ * (r₃ * v) = ↑s₄ * (↑s₃ * v₀)
⊢ ↑s₄ * ↑s₃ * (↑u₀ * ↑s₁) = ↑s₄ * r₃ * (↑u * ↑s₁)
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
H : f (↑y₂ * x₁) = f (↑y₁ * x₂)
⊢ f.mk' x₁ y₁ = f.mk' x₂ y₂

Tactic:
rw [mk'_eq_iff_eq_mul, mk', mul_assoc, mul_comm _ (f y₁), ← mul_assoc, ← map_mul f, mul_comm x₂,
      ← H, ← mul_comm x₁, map_mul f, mul_inv_right f.map_units, toMonoidHom_apply]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Sub α
inst✝ : Bot α
a : WithTop α
⊢ a - ⊤ = ↑⊥

Tactic:
cases a <;> rfl

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

Goal state before:
pp: case top.top
α : Type u_1
inst✝¹ : Sub α
inst✝ : Bot α
⊢ ⊤ - ⊤ = ⊤ ↔ ⊤ = ⊤ ∧ ⊤ ≠ ⊤

Tactic:
simp only [← coe_sub, coe_ne_top, sub_top, top_sub_coe, false_and, Ne, not_true_eq_false,
      not_false_eq_true, and_false, and_self]

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

Goal state before:
pp: case top.coe
α : Type u_1
inst✝¹ : Sub α
inst✝ : Bot α
a✝ : α
⊢ ⊤ - ↑a✝ = ⊤ ↔ ⊤ = ⊤ ∧ ↑a✝ ≠ ⊤

Tactic:
simp only [← coe_sub, coe_ne_top, sub_top, top_sub_coe, false_and, Ne, not_true_eq_false,
      not_false_eq_true, and_false, and_self]

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

Goal state before:
pp: case coe.top
α : Type u_1
inst✝¹ : Sub α
inst✝ : Bot α
a✝ : α
⊢ ↑a✝ - ⊤ = ⊤ ↔ ↑a✝ = ⊤ ∧ ⊤ ≠ ⊤

Tactic:
simp only [← coe_sub, coe_ne_top, sub_top, top_sub_coe, false_and, Ne, not_true_eq_false,
      not_false_eq_true, and_false, and_self]

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

Goal state before:
pp: case coe.coe
α : Type u_1
inst✝¹ : Sub α
inst✝ : Bot α
a✝¹ a✝ : α
⊢ ↑a✝¹ - ↑a✝ = ⊤ ↔ ↑a✝¹ = ⊤ ∧ ↑a✝ ≠ ⊤

Tactic:
simp only [← coe_sub, coe_ne_top, sub_top, top_sub_coe, false_and, Ne, not_true_eq_false,
      not_false_eq_true, and_false, and_self]

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : CommSemiring α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
a₂ b₂ : WithTop α
this : MulPosStrictMono α
a₁ : α
ha : ↑a₁ < a₂
b₁ : α
hb : ↑b₁ < b₂
⊢ ↑a₁ * ↑b₁ < a₂ * b₂

Tactic:
obtain rfl | ha₂ := eq_or_ne a₂ ⊤

Goal state after:
case inl
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : CommSemiring α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
b₂ : WithTop α
this : MulPosStrictMono α
a₁ b₁ : α
hb : ↑b₁ < b₂
ha : ↑a₁ < ⊤
⊢ ↑a₁ * ↑b₁ < ⊤ * b₂

case inr
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : CommSemiring α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
a₂ b₂ : WithTop α
this : MulPosStrictMono α
a₁ : α
ha : ↑a₁ < a₂
b₁ : α
hb : ↑b₁ < b₂
ha₂ : a₂ ≠ ⊤
⊢ ↑a₁ * ↑b₁ < a₂ * b₂
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
a : α
inst✝¹ : Preorder α
inst✝ : SuccOrder α
h : IsSuccPrelimit (succ a)
⊢ IsMax a

Tactic:
by
  by_contra H
  exact h a (covBy_succ_of_not_isMax H)

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 : (∀ x ∈ S, x ≤ m) → n ∈ S → m ∉ S → ∃ x, IsGreatest S x
hm : ∀ x ∈ S, x ≤ succ m
hn : n ∈ S
hm' : succ m ∉ S
⊢ ∃ x, IsGreatest S x

Tactic:
Order.le_succ_iff_eq_or_le

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 : (∀ x ∈ S, x ≤ m) → n ∈ S → m ∉ S → ∃ x, IsGreatest S x
hn : n ∈ S
hm' : succ m ∉ S
hm : ∀ x ∈ S, x = succ m ∨ x ≤ m
⊢ ∃ x, IsGreatest S x
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : Sub α
inst✝² : One α
inst✝¹ : PredSubOrder α
inst✝ : NoMinOrder α
x : α
⊢ x - 1 ⋖ x

Tactic:
rw [← pred_eq_sub_one]
  exact pred_covBy x

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

Goal state before:
pp: case top
n : ℕ
⊢ (⊤ - ↑n).toNat = ⊤.toNat - (↑n).toNat

Tactic:
top_sub_natCast,

Goal state after:
case top
n : ℕ
⊢ ⊤.toNat = ⊤.toNat - (↑n).toNat
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: a b : ℕ∞
⊢ (a * b).toNat = a.toNat * b.toNat

Tactic:
cases a <;> cases b
  · simp
  · rename_i b; cases b <;> simp
  · rename_i a; cases a <;> simp
  · simp only [toNat_natCast]; rw [← natCast_mul, toNat_natCast]

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)
⊢ StrictAnti f

Tactic:
by
  simpa using strictAntiOn_of_lt_pred Set.ordConnected_univ (by simpa using hf)

Goal state after: