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

Goal state before:
pp: α : Type u_1
β : Type u_2
s s' : Finset α
t t' : Finset β
⊢ Disjoint ↑(s ×ˢ t) ↑(s' ×ˢ t') ↔ Disjoint ↑s ↑s' ∨ Disjoint ↑t ↑t'

Tactic:
coe_product,

Goal state after:
α : Type u_1
β : Type u_2
s s' : Finset α
t t' : Finset β
⊢ Disjoint (↑s ×ˢ ↑t) (↑s' ×ˢ ↑t') ↔ Disjoint ↑s ↑s' ∨ Disjoint ↑t ↑t'
Module: Mathlib.Algebra.Group.Pointwise.Set.Finite

Goal state before:
pp: case zero
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Monoid α
s t : Set α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ DecidablePred fun x ↦ x ∈ s ^ 0

Tactic:
simp only [pow_zero, mem_one]

Goal state after:
case zero
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Monoid α
s t : Set α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ DecidablePred fun x ↦ x = 1
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: case mp.inl
α : Type u_2
inst✝ : Monoid α
s : Set α
n : ℕ
hs : s.Nonempty
⊢ (s ^ n).Nonempty

pp: case mp.inr
α : Type u_2
inst✝ : Monoid α
s : Set α
⊢ (s ^ 0).Nonempty

Tactic:
· exact hs.pow

Goal state after:
case mp.inr
α : Type u_2
inst✝ : Monoid α
s : Set α
⊢ (s ^ 0).Nonempty
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: case mpr
α : Type u_2
inst✝ : DivisionMonoid α
n : ℤ
hn : n ≠ 0
⊢ ∅ ^ n = ∅

Tactic:
exact empty_zpow hn

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
K : Subgroup G
f : G →* N
⊢ (f.domRestrict K).range = map f K

Tactic:
SetLike.ext_iff,

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
K : Subgroup G
f : G →* N
⊢ ∀ (x : N), x ∈ (f.domRestrict K).range ↔ x ∈ map f K
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝ : Group G
ι : Sort u_2
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun x1 x2 ↦ x1 ≤ x2) K
x : G
⊢ iSup K = ⨆ i, ⨆ (_ : True), K i.down

Tactic:
simp [iSup_plift_down]

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

Goal state before:
pp: case hK
G : Type u_1
inst✝ : Group G
ι : Sort u_2
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun x1 x2 ↦ x1 ≤ x2) K
x : G
this : iSup K = ⨆ i, ⨆ (_ : True), K i.down
⊢ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) ((fun i ↦ K i.down) '' univ)

Tactic:
Set.image_univ,

Goal state after:
case hK
G : Type u_1
inst✝ : Group G
ι : Sort u_2
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun x1 x2 ↦ x1 ≤ x2) K
x : G
this : iSup K = ⨆ i, ⨆ (_ : True), K i.down
⊢ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (range fun i ↦ K i.down)
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
ι : Sort u_2
inst✝ : Nonempty ι
S : ι → Subgroup G
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
a : G
i : ι
ha : a ∈ S i
b : G
j : ι
hb : b ∈ S j
k : ι
hik : S i ≤ S k
hjk : S j ≤ S k
⊢ a * b = b * a

Tactic:
exact setLike_mul_comm (hik ha) (hjk hb)

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
P : Subgroup ↥H → Prop
⊢ (∀ (H' : Subgroup ↥H), P H') ↔ ∀ H' ≤ H, P (H'.subgroupOf H)

Tactic:
by
  simp [(MapSubtype.orderIso H).forall_congr_left]

Goal state after:
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: n : ℕ
h : 2 ≤ n
⊢ decodeSum n = none

Tactic:
have : 1 ≤ n / 2 := by
    rw [Nat.le_div_iff_mul_le]
    exacts [h, by decide]

Goal state after:
n : ℕ
h : 2 ≤ n
this : 1 ≤ n / 2
⊢ decodeSum n = none
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Encodable β
n : ℕ
⊢ Option.map (⇑(Equiv.sigmaEquivProd α β))
      ((decode (unpair n).1).bind fun a ↦ Option.map (Sigma.mk a) (decode (unpair n).2)) =
    (decode (unpair n).1).bind fun a ↦ Option.map (Prod.mk a) (decode (unpair n).2)

Tactic:
cases (decode n.unpair.1 : Option α)

Goal state after:
case none
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Encodable β
n : ℕ
⊢ Option.map (⇑(Equiv.sigmaEquivProd α β)) (none.bind fun a ↦ Option.map (Sigma.mk a) (decode (unpair n).2)) =
    none.bind fun a ↦ Option.map (Prod.mk a) (decode (unpair n).2)

case some
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Encodable β
n : ℕ
val✝ : α
⊢ Option.map (⇑(Equiv.sigmaEquivProd α β)) ((some val✝).bind fun a ↦ Option.map (Sigma.mk a) (decode (unpair n).2)) =
    (some val✝).bind fun a ↦ Option.map (Prod.mk a) (decode (unpair n).2)
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case cons
M : Type u_3
N : Type u_4
inst✝² : AddZeroClass M
inst✝¹ : Zero N
inst✝ : LinearOrder N
f : M → N
h0 : f 0 ≤ 0
hadd : ∀ (x y : M), f (x + y) ≤ max (f x) (f y)
hd : M
tl : List M
IH : f tl.sum ≤ foldr max 0 (map f tl)
⊢ f (hd :: tl).sum ≤ foldr max 0 (map f (hd :: tl))

Tactic:
simp only [List.sum_cons, List.foldr_map, List.foldr] at IH ⊢

Goal state after:
case cons
M : Type u_3
N : Type u_4
inst✝² : AddZeroClass M
inst✝¹ : Zero N
inst✝ : LinearOrder N
f : M → N
h0 : f 0 ≤ 0
hadd : ∀ (x y : M), f (x + y) ≤ max (f x) (f y)
hd : M
tl : List M
IH : f tl.sum ≤ foldr (fun x y ↦ max (f x) y) 0 tl
⊢ f (hd + tl.sum) ≤ max (f hd) (foldr (fun x y ↦ max (f x) y) 0 tl)
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 : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
a : M
i : ι
ha : a ∈ S i
b : M
j : ι
hb : b ∈ S j
k : ι
hik : S i ≤ S k
hjk : S j ≤ S k
⊢ a * b = b * a

Tactic:
exact setLike_mul_comm (hik ha) (hjk hb)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMaxOrder α
a : α
b : β
c : α
h : a < c
⊢ ∃ b_1, toLex (a, b) < b_1

Tactic:
use toLex (c, b)

Goal state after:
case h
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMaxOrder α
a : α
b : β
c : α
h : a < c
⊢ toLex (a, b) < toLex (c, b)
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ Subtype.val '' Set.univ = s

Tactic:
Set.image_univ,

Goal state after:
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ Set.range Subtype.val = s
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: α : Type u_1
⊢ powerset 0 = {0}

Tactic:
exact powerset_zero

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

Goal state before:
pp: α : Type u
a : α
l : List α
⊢ sublistsLen (a :: l).length (a :: l) = [a :: l]

Tactic:
by
    simp only [length, sublistsLen_succ_cons, sublistsLen_length, map,
      sublistsLen_of_length_lt (lt_succ_self _), nil_append]

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

Goal state before:
pp: α : Type u_1
s : Finset (Option α)
h : none ∈ s
⊢ #(s.erase none) = #s - 1

Tactic:
card_erase_of_mem h

Goal state after:
α : Type u_1
s : Finset (Option α)
h : none ∈ s
⊢ #s - 1 = #s - 1
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
s : Set α
hs : s.Finite
ι : Type u_1
t : ι → Set α
h : s ⊆ ⋃ i, t i
this : Finite ↑s
⊢ ∃ I, I.Finite ∧ s ⊆ ⋃ i ∈ I, t i

Tactic:
choose f hf using show ∀ x : s, ∃ i, x.1 ∈ t i by simpa [subset_def] using h

Goal state after:
α : Type u
s : Set α
hs : s.Finite
ι : Type u_1
t : ι → Set α
h : s ⊆ ⋃ i, t i
this : Finite ↑s
f : ↑s → ι
hf : ∀ (x : ↑s), ↑x ∈ t (f x)
⊢ ∃ I, I.Finite ∧ s ⊆ ⋃ i ∈ I, t i
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
s : Set ι
f : ι → ι'
g : ι' → α
hf : BddAbove (range fun i ↦ g (f ↑i))
hg' : sSup ∅ ≤ ⨆ i, g (f ↑i)
hs : s.Nonempty
hg : BddAbove (range fun i ↦ g ↑i)
this : Nonempty ↑s
i : ι
h : i ∈ s
⊢ ∃ t, g ↑t = g (f ↑⟨i, h⟩)

Tactic:
have : f i ∈ f '' s := Set.mem_image_of_mem _ h

Goal state after:
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
s : Set ι
f : ι → ι'
g : ι' → α
hf : BddAbove (range fun i ↦ g (f ↑i))
hg' : sSup ∅ ≤ ⨆ i, g (f ↑i)
hs : s.Nonempty
hg : BddAbove (range fun i ↦ g ↑i)
this✝ : Nonempty ↑s
i : ι
h : i ∈ s
this : f i ∈ f '' s
⊢ ∃ t, g ↑t = g (f ↑⟨i, h⟩)
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ⩿ b
⊢ Ioc a b ⊆ {b}

Tactic:
rw [← Icc_sdiff_left, h.Icc_eq, sdiff_singleton_subset_iff]

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : Ioo a b = {c}
⊢ a ⋖ c ∧ c ⋖ b

Tactic:
by
    simp_rw [Set.ext_iff, mem_Ioo, mem_singleton_iff] at h
    have ⟨hac, hcb⟩ := (h c).mpr rfl
    exact ⟨⟨hac, fun d had hdc ↦ hdc.ne ((h d).mp ⟨had, hdc.trans hcb⟩)⟩,
      ⟨hcb, fun d hcd hdb ↦ hcd.ne ((h d).mp ⟨hac.trans hcd, hdb⟩).symm⟩⟩

Goal state after:
Module: Mathlib.Order.Preorder.Finite

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

Tactic:
| singleton i =>

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
x : α
inst✝ : LE α
⊢ ¬Minimal (fun x ↦ False) x

Tactic:
simp [Minimal]

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
P Q : α → Prop
x : α
inst✝ : LE α
hPQ : ∀ ⦃x : α⦄, P x → Q x
⊢ Minimal (fun x ↦ P x) x → Q x

Tactic:
exact fun h ↦ hPQ h.prop

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b : α
⊢ Ico a b = 0 ↔ ¬a < b

Tactic:
by
  rw [Ico, Finset.val_eq_zero, Finset.Ico_eq_empty_iff]

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

Goal state before:
pp: ι : Sort u_1
inst✝ : IsEmpty ι
f : ι → ℕ
⊢ sInf ∅ = 0

Tactic:
sInf_empty

Goal state after:
ι : Sort u_1
inst✝ : IsEmpty ι
f : ι → ℕ
⊢ 0 = 0
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: s : Set ℕ
m : ℕ
hm : m ∈ s
⊢ sInf s ≤ m

Tactic:
rw [Nat.sInf_def ⟨m, hm⟩]

Goal state after:
s : Set ℕ
m : ℕ
hm : m ∈ s
⊢ Nat.find ⋯ ≤ m
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : OrderTop α
a✝ x✝ a x : α
⊢ x ∈ Icc a ⊤ ↔ a ≤ x

Tactic:
rw [mem_Icc, and_iff_left le_top]

Goal state after:
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 : β
h : Injective fun x ↦ x • b
⊢ stabilizer G (a • b) = stabilizer G a

Tactic:
refine (le_stabilizer_smul_left _ _).antisymm' fun a ha ↦ ?_

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 : β
h : Injective fun x ↦ x • b
a : G
ha : a ∈ stabilizer G (a✝ • b)
⊢ a ∈ stabilizer G a✝
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case inr.refine_1
α : Type u_2
r : α → α → Prop
inst✝ : IsPreorder α r
s : Set α
h : s.PartiallyWellOrderedOn r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ x ∈ l, x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (f (g m)).head! (f (g n)).head!
⊢ (f (g 0)).length - 1 < (f (g 0)).length

Tactic:
← Nat.pred_eq_sub_one

Goal state after:
case inr.refine_1
α : Type u_2
r : α → α → Prop
inst✝ : IsPreorder α r
s : Set α
h : s.PartiallyWellOrderedOn r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ x ∈ l, x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (f (g m)).head! (f (g n)).head!
⊢ (f (g 0)).length.pred < (f (g 0)).length
Module: Mathlib.GroupTheory.Submonoid.Center

Goal state before:
pp: M : Type u_3
N : Type u_1
F : Type u_2
inst✝³ : EquivLike F M N
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : MulEquivClass F M N
e : F
x : M
hx : x ∈ Set.center M
⊢ e x ∈ Set.center N

Tactic:
let e := MulEquivClass.toMulEquiv e

Goal state after:
M : Type u_3
N : Type u_1
F : Type u_2
inst✝³ : EquivLike F M N
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : MulEquivClass F M N
e✝ : F
x : M
hx : x ∈ Set.center M
e : M ≃* N := ↑e✝
⊢ e✝ x ∈ Set.center N
Module: Mathlib.Algebra.Group.Center

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

Tactic:
by
  rw [_root_.Semigroup.mem_center_iff]
  intro _
  rw [← Units.val_inj, Units.val_mul, Units.val_mul, ha.comm]

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

Goal state before:
pp: α : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Group G
H : Subgroup G
hH : H.Normal
K : Subgroup ↥H
h : K.Characteristic
a : G
ha : a ∈ map H.subtype K
b : G
⊢ b * a * b⁻¹ ∈ map H.subtype K

Tactic:
obtain ⟨a, ha, rfl⟩ := ha

Goal state after:
α : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Group G
H : Subgroup G
hH : H.Normal
K : Subgroup ↥H
h : K.Characteristic
b : G
a : ↥H
ha : a ∈ ↑K
⊢ b * H.subtype a * b⁻¹ ∈ map H.subtype K
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: case h
α : Type u_3
inst✝ : Monoid α
y : α
a✝ : List α
comm : {x | x ∈ ⟦a✝⟧}.Pairwise Commute
h : ∀ x ∈ ⟦a✝⟧, Commute y x
⊢ Commute y a✝.prod

Tactic:
exact Commute.list_prod_right _ _ h

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
N : Type u_4
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
r : M → N → Prop
f : ι → M
g : ι → N
s : Finset ι
h₁ : r 1 1
h₂ : ∀ (a : ι) (b : M) (c : N), r b c → r (f a * b) (g a * c)
⊢ r (∏ x ∈ s, f x) (∏ x ∈ s, g x)

Tactic:
delta Finset.prod

Goal state after:
ι : Type u_1
M : Type u_3
N : Type u_4
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
r : M → N → Prop
f : ι → M
g : ι → N
s : Finset ι
h₁ : r 1 1
h₂ : ∀ (a : ι) (b : M) (c : N), r b c → r (f a * b) (g a * c)
⊢ r (Multiset.map (fun x ↦ f x) s.val).prod (Multiset.map (fun x ↦ g x) s.val).prod
Module: Mathlib.Data.Setoid.Basic

Goal state before:
pp: case trans.inl.inl
α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
hf : ker f ≤ r
i✝¹ i✝ x✝ y✝ z✝ : β
a✝¹ : Relation.EqvGen (Relation.Map (⇑r) f f) x✝ y✝
a✝ : Relation.EqvGen (Relation.Map (⇑r) f f) y✝ z✝
ih1 : Relation.Map (⇑r) f f x✝ y✝
ih2 : Relation.Map (⇑r) f f y✝ z✝
⊢ (Relation.Map (⇑r) f f ⊔ fun x1 x2 ↦ x1 = x2) x✝ z✝

Tactic:
exact .inl <| r.iseqv.isTrans.map hf |>.trans _ _ _ ih1 ih2

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ (∃ a, x⁻¹ * y = ↑a⁻¹) ↔ x⁻¹ * y ∈ s

Tactic:
by simp [exists_inv_mem_iff_exists_mem]

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ (∃ a, y * x⁻¹ = ↑a⁻¹) ↔ y * x⁻¹ ∈ s

Tactic:
by simp [exists_inv_mem_iff_exists_mem]

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

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f✝ : α → β
x y : FreeGroup α
f : α → β
⊢ ∀ (a b : FreeGroup α), Quot.lift (Lift.aux f) ⋯ (a * b) = Quot.lift (Lift.aux f) ⋯ a * Quot.lift (Lift.aux f) ⋯ b

Tactic:
rintro ⟨L₁⟩ ⟨L₂⟩

Goal state after:
case mk.mk
α : Type u
L L₁✝ L₂✝ L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f✝ : α → β
x y : FreeGroup α
f : α → β
a✝ : FreeGroup α
L₁ : List (α × Bool)
b✝ : FreeGroup α
L₂ : List (α × Bool)
⊢ Quot.lift (Lift.aux f) ⋯ (Quot.mk Red.Step L₁ * Quot.mk Red.Step L₂) =
    Quot.lift (Lift.aux f) ⋯ (Quot.mk Red.Step L₁) * Quot.lift (Lift.aux f) ⋯ (Quot.mk Red.Step L₂)
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
f : α → β
x y : FreeGroup α
⊢ ∀ (a b : FreeGroup α),
    Quot.map (List.map fun x ↦ (f x.1, x.2)) ⋯ (a * b) =
      Quot.map (List.map fun x ↦ (f x.1, x.2)) ⋯ a * Quot.map (List.map fun x ↦ (f x.1, x.2)) ⋯ b

Tactic:
rintro ⟨L₁⟩ ⟨L₂⟩

Goal state after:
case mk.mk
α : Type u
L L₁✝ L₂✝ L₃ L₄ : List (α × Bool)
β : Type v
f : α → β
x y a✝ : FreeGroup α
L₁ : List (α × Bool)
b✝ : FreeGroup α
L₂ : List (α × Bool)
⊢ Quot.map (List.map fun x ↦ (f x.1, x.2)) ⋯ (Quot.mk Red.Step L₁ * Quot.mk Red.Step L₂) =
    Quot.map (List.map fun x ↦ (f x.1, x.2)) ⋯ (Quot.mk Red.Step L₁) *
      Quot.map (List.map fun x ↦ (f x.1, x.2)) ⋯ (Quot.mk Red.Step L₂)
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
β : Type v
f : α → β
hf : Function.Surjective f
⊢ Subgroup.closure (of '' Set.univ) = ⊤

Tactic:
Set.image_univ,

Goal state after:
α : Type u
β : Type v
f : α → β
hf : Function.Surjective f
⊢ Subgroup.closure (Set.range of) = ⊤
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : Unique α
x✝¹ x✝ : FreeGroup α
⊢ (⇑Multiplicative.ofAdd ∘ ⇑equivIntOfUnique) (x✝¹ * x✝) =
    (⇑Multiplicative.ofAdd ∘ ⇑equivIntOfUnique) x✝¹ * (⇑Multiplicative.ofAdd ∘ ⇑equivIntOfUnique) x✝

Tactic:
by simp [equivIntOfUnique]

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

Goal state before:
pp: case succ
M : Type u_4
inst✝ : CommMonoid M
f s : ℕ → M
base : s 0 = 1
k : ℕ
hk : (∀ k_1 < k, s (k_1 + 1) = s k_1 * f k_1) → ∏ k ∈ range k, f k = s k
step : ∀ k_1 < k + 1, s (k_1 + 1) = s k_1 * f k_1
⊢ (∏ x ∈ range k, f x) * f k = s (k + 1)

Tactic:
step _ (Nat.lt_succ_self _),

Goal state after:
case succ
M : Type u_4
inst✝ : CommMonoid M
f s : ℕ → M
base : s 0 = 1
k : ℕ
hk : (∀ k_1 < k, s (k_1 + 1) = s k_1 * f k_1) → ∏ k ∈ range k, f k = s k
step : ∀ k_1 < k + 1, s (k_1 + 1) = s k_1 * f k_1
⊢ (∏ x ∈ range k, f x) * f k = s k * f k
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: case e_f
M : Type u_4
κ : Type u_6
ι : Type u_7
inst✝³ : Fintype ι
inst✝² : Fintype κ
inst✝¹ : CommMonoid M
inst✝ : DecidableEq κ
g : ι → κ
f : ι → M
j : κ
⊢ ∏ i, f ↑i = ∏ i with g i = j, f i

Tactic:
exact (prod_subtype _ (by simp) _).symm

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case pure.pure
α : Type u
G : Type u_1
β α✝ β✝ : Type u
p : α✝
q : β✝
⊢ pure (p, q) = (fun a ↦ (a, q)) <$> pure p

Tactic:
map_pure

Goal state after:
case pure.pure
α : Type u
G : Type u_1
β α✝ β✝ : Type u
p : α✝
q : β✝
⊢ pure (p, q) = pure (p, q)
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ ⁅centralizer ↑(commutator G), ⁅⊤, centralizer ↑(commutator G)⁆⁆ = ⊥

Tactic:
Subgroup.commutator_eq_bot_iff_le_centralizer

Goal state after:
G : Type u_1
inst✝ : Group G
⊢ centralizer ↑(commutator G) ≤ centralizer ↑⁅⊤, centralizer ↑(commutator G)⁆
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x y : M × ↥S
u : M
hu : u ∈ S
e : u * (↑y.2 * x.1) = u * (↑x.2 * y.1)
⊢ u * (↑x.2 * y.1) = u * (↑y.2 * x.1)

Tactic:
← e

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x y : M × ↥S
u : M
hu : u ∈ S
e : u * (↑y.2 * x.1) = u * (↑x.2 * y.1)
⊢ u * (↑y.2 * x.1) = u * (↑y.2 * x.1)
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.10
inst✝ : MulAction R X
r : R
s : ↥S
r₁ : X
r₂ : R
s' : ↥S
hs : r₂ * ↑s' ∈ S
r₁' : R
s₁' : ↥S
h₁ : ↑s₁' * r = r₁' * ↑s'
r₂' : R
s₂' : ↥S
h₂ : ↑s₂' * r = r₂' * ↑⟨r₂ * ↑s', hs⟩
r₃' : R
s₃' : ↥S
h₃ : ↑s₃' * ↑s₁' = r₃' * ↑s₂'
this : ↑s₃' * r₁' * ↑s' = r₃' * r₂' * r₂ * ↑s'
⊢ r₁' • r₁ /ₒ (s₁' * s) = r₂' • r₂ • r₁ /ₒ (s₂' * s)

Tactic:
rcases ore_right_cancel _ _ _ this with ⟨s₄', h₄⟩

Goal state after:
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
r : R
s : ↥S
r₁ : X
r₂ : R
s' : ↥S
hs : r₂ * ↑s' ∈ S
r₁' : R
s₁' : ↥S
h₁ : ↑s₁' * r = r₁' * ↑s'
r₂' : R
s₂' : ↥S
h₂ : ↑s₂' * r = r₂' * ↑⟨r₂ * ↑s', hs⟩
r₃' : R
s₃' : ↥S
h₃ : ↑s₃' * ↑s₁' = r₃' * ↑s₂'
this : ↑s₃' * r₁' * ↑s' = r₃' * r₂' * r₂ * ↑s'
s₄' : ↥S
h₄ : ↑s₄' * (↑s₃' * r₁') = ↑s₄' * (r₃' * r₂' * r₂)
⊢ r₁' • r₁ /ₒ (s₁' * s) = r₂' • r₂ • r₁ /ₒ (s₂' * s)
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
y : OreLocalization S R
r₁ r₂ : R
s : ↥S
hs : r₂ * ↑s ∈ S
x : X
s₂ : ↥S
r₁' : R
s₁' : ↥S
h₁ : ↑s₁' * r₁ = r₁' * ↑s₂
r₂' : R
s₂' : ↥S
h₂ : ↑s₂' * (r₂ * r₁) = r₂' * ↑s₂
r₃' : R
s₃' : ↥S
h₃ : ↑s₃' * (↑s₂' * r₂) = r₃' * ↑s₁'
this : ↑s₃' * r₂' * ↑s₂ = r₃' * r₁' * ↑s₂
⊢ r₁' • x /ₒ (s₁' * s) = r₂' • x /ₒ (s₂' * ⟨r₂ * ↑s, hs⟩)

Tactic:
rcases ore_right_cancel _ _ _ this with ⟨s₄', h₄⟩

Goal state after:
case c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
y : OreLocalization S R
r₁ r₂ : R
s : ↥S
hs : r₂ * ↑s ∈ S
x : X
s₂ : ↥S
r₁' : R
s₁' : ↥S
h₁ : ↑s₁' * r₁ = r₁' * ↑s₂
r₂' : R
s₂' : ↥S
h₂ : ↑s₂' * (r₂ * r₁) = r₂' * ↑s₂
r₃' : R
s₃' : ↥S
h₃ : ↑s₃' * (↑s₂' * r₂) = r₃' * ↑s₁'
this : ↑s₃' * r₂' * ↑s₂ = r₃' * r₁' * ↑s₂
s₄' : ↥S
h₄ : ↑s₄' * (↑s₃' * r₂') = ↑s₄' * (r₃' * r₁')
⊢ r₁' • x /ₒ (s₁' * s) = r₂' • x /ₒ (s₂' * ⟨r₂ * ↑s, hs⟩)
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 t : ↥S
⊢ (r₁ * ↑s /ₒ t) • (r₂ /ₒ s) = r₁ • r₂ /ₒ t

Tactic:
simp [oreDiv_smul_char (r₁ * s) r₂ t s r₁ 1 (by simp)]

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

Goal state before:
pp: M : Type u_1
G : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommGroup G
S : Submonoid M
f : M → G
hf : Injective f
surj : ∀ (g : G), ∃ x, ∃ y ∈ S, g = f x / f y
g : G
x y : M
hy : y ∈ S
eq : g = f x / f y
⊢ g * f ↑(x, ⟨y, hy⟩).2 = f (x, ⟨y, hy⟩).1

Tactic:
simp [eq]

Goal state after:
Module: Mathlib.Order.Iterate

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
n : ℕ
hn : 0 < n
⊢ f^[n] x < g^[n] x ↔ f x < g x

Tactic:
rcases lt_trichotomy (f x) (g x) with (H | H | H)
  · simp only [*, iterate_pos_lt_of_map_lt]
  · simp only [*, h.iterate_eq_of_map_eq, lt_irrefl]
  · simp only [lt_asymm H, lt_asymm (h.symm.iterate_pos_lt_of_map_lt' hg hf H hn)]

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

Goal state before:
pp: case inr
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α
n m : ℕ
this :
  ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] [IsSuccArchimedean α] {r : α} (n m : ℕ),
    n ≤ m → succ^[n] r ≤ succ^[m] r ∨ succ^[m] r ≤ succ^[n] r
h : ¬n ≤ m
⊢ succ^[n] r ≤ succ^[m] r ∨ succ^[m] r ≤ succ^[n] r

Tactic:
rw [Or.comm]
    apply this
    exact Nat.le_of_not_ge h

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

Goal state before:
pp: α : Type u_1
a : α
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
h : ¬IsSuccPrelimit a
⊢ a ∈ range succ

Tactic:
obtain ⟨b, hb⟩ := not_isSuccPrelimit_iff_succ_eq.1 h
  exact ⟨b, hb.2⟩

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

Goal state before:
pp: α : Type u_1
b : α
motive : α → Sort u_2
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
succ : (a : α) → ¬IsMax a → motive (Order.succ a)
isSuccPrelimit : (a : α) → IsSuccPrelimit a → motive a
hb : ¬IsMax b
hb' : ¬IsSuccPrelimit (Order.succ b)
H : ¬IsMax (Classical.choose ⋯) ∧ Order.succ (Classical.choose ⋯) = Order.succ b
⊢ isSuccPrelimitRecOn (Order.succ b) succ isSuccPrelimit = succ b hb

Tactic:
rw [isSuccPrelimitRecOn, dif_neg hb', cast_eq_iff_heq]

Goal state after:
α : Type u_1
b : α
motive : α → Sort u_2
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
succ : (a : α) → ¬IsMax a → motive (Order.succ a)
isSuccPrelimit : (a : α) → IsSuccPrelimit a → motive a
hb : ¬IsMax b
hb' : ¬IsSuccPrelimit (Order.succ b)
H : ¬IsMax (Classical.choose ⋯) ∧ Order.succ (Classical.choose ⋯) = Order.succ b
⊢ succ (Classical.choose ⋯) ⋯ ≍ succ b hb