mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Subgroup.Defs

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : H.Normal
a b : G
h : a * b ∈ H
⊢ b * a ∈ H

Tactic:
have : a⁻¹ * (a * b) * a⁻¹⁻¹ ∈ H := nH.conj_mem (a * b) h a⁻¹
  simpa

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
i j : PLift ι
⊢ ∃ x, K i.down ≤ K x ∧ K j.down ≤ K x

Tactic:
refine (hK i.down j.down).imp ?_

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
i j : PLift ι
⊢ ∀ (a : ι),
    (fun x1 x2 ↦ x1 ≤ x2) (K i.down) (K a) ∧ (fun x1 x2 ↦ x1 ≤ x2) (K j.down) (K a) → K i.down ≤ K a ∧ K j.down ≤ K a
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H K : Subgroup G
hH : f.ker ≤ H
hK : f.ker ≤ K
hf : comap f (map f H) = comap f (map f K)
⊢ H = K

Tactic:
rwa [comap_map_eq, comap_map_eq, sup_of_le_left hH, sup_of_le_left hK] at hf

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

Goal state before:
pp: ι : Type u_4
M : ι → Type u_5
inst✝ : (i : ι) → MulOneClass (M i)
S : (i : ι) → Submonoid (M i)
⊢ pi Set.univ S = ⊥ ↔ ∀ (i : ι), S i = ⊥

Tactic:
simp_rw [SetLike.ext'_iff]
  exact Set.univ_pi_eq_singleton_iff

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: n : ℕ
⊢ n.succ.bodd = !n.bodd

Tactic:
by
  simp only [bodd]
  cases mod_two_eq_zero_or_one n with | _ h => simp [h, add_mod]

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: ⊢ bits 0 = []

Tactic:
by simp [Nat.bits]

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: case bit
b✝ : Bool
n✝ : ℕ
h : n✝ = 0 → b✝ = true
a✝ : n✝.bodd = n✝.bits.headI
⊢ (bit b✝ n✝).bodd = (bit b✝ n✝).bits.headI

Tactic:
simp [bodd_bit, bits_append_bit _ _ h]

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

Goal state before:
pp: α : Type u_1
inst✝ : Encodable α
n : ℕ
a : α
⊢ a ∈ decode₂ α n ↔ a ∈ decode n ∧ encode a = n

Tactic:
simp [decode₂, Option.bind_eq_some_iff]

Goal state after:
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: case inr
m n : ℕ
h : n ≤ m
⊢ m * m + n ≤ m * m + (m + n)

Tactic:
Nat.add_le_add_iff_left

Goal state after:
case inr
m n : ℕ
h : n ≤ m
⊢ n ≤ m + n
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: η : Type u_7
f : η → Type u_8
inst✝ : (i : η) → Group (f i)
H : (i : η) → Subgroup (f i)
⊢ pi univ H = ⊥ ↔ ∀ (i : η), H i = ⊥

Tactic:
simp_rw [SetLike.ext'_iff]
  exact Set.univ_pi_eq_singleton_iff

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

Goal state before:
pp: case right.left
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : Std.Asymm r
inst✝ : ∀ (i : ι), Std.Antisymm (s i)
i✝ : ι
a b : α i✝
hab : s i✝ a b
hji : r i✝ i✝
⊢ ⟨i✝, a⟩ = ⟨i✝, b⟩

pp: case right.right
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : Std.Asymm r
inst✝ : ∀ (i : ι), Std.Antisymm (s i)
i✝ : ι
a b : α i✝
hab : s i✝ a b
hba : s i✝ b a
⊢ ⟨i✝, a⟩ = ⟨i✝, b⟩

Tactic:
· exact (irrefl _ hji).elim

Goal state after:
case right.right
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : Std.Asymm r
inst✝ : ∀ (i : ι), Std.Antisymm (s i)
i✝ : ι
a b : α i✝
hab : s i✝ a b
hba : s i✝ b a
⊢ ⟨i✝, a⟩ = ⟨i✝, b⟩
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
S T : Submonoid M
⊢ ∀ {x : M}, x ∈ S → x ∈ S ⊔ T

Tactic:
rw [← SetLike.le_def]
  exact le_sup_left

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

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : NoMinOrder β
inst✝ : DenselyOrdered β
x y : α × β
h : x.1 < y.1
v : β
hv : v < y.2
⊢ toLex x < toLex (y.1, v) ∧ toLex (y.1, v) < toLex y

Tactic:
simp [Prod.Lex.toLex_lt_toLex, h, hv]

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

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : NoMaxOrder β
inst✝ : DenselyOrdered β
x y : α × β
h : x.1 < y.1
v : β
hv : x.2 < v
⊢ toLex x < toLex (x.1, v) ∧ toLex (x.1, v) < toLex y

Tactic:
simp [Prod.Lex.toLex_lt_toLex, h, hv]

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

Goal state before:
pp: ⊢ AddSubmonoid.closure {1} = ⊤

Tactic:
ext
  simp [AddSubmonoid.mem_closure_singleton]

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
n : ℕ
h₁ : ↑(ofNat s n) ∉ {x ∈ range ↑(ofNat s n) | x ∈ s}
h₂ : {x ∈ range ↑(succ (ofNat s n)) | x ∈ s} = insert (↑(ofNat s n)) ({x ∈ range ↑(ofNat s n) | x ∈ s})
ih : #({y ∈ range ↑(ofNat s n) | y ∈ s}) = n
⊢ #({y ∈ range ↑(succ (ofNat s n)) | y ∈ s}) = n + 1

Tactic:
conv =>
      rhs
      rw [← ih, ← card_insert_of_notMem h₁, ← h₂]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Lattice α
inst✝¹ : Lattice β
inst✝ : Lattice γ
g : LatticeHom β γ
f₁ f₂ : LatticeHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
rw [← LatticeHom.comp_apply, h, LatticeHom.comp_apply]

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

Goal state before:
pp: α : Type u_2
S : Multiset α
⊢ ((range (S.card + 1)).bind fun k ↦ powersetCard k S) = S.powerset

Tactic:
by
  induction S using Quotient.inductionOn
  simp_rw [quot_mk_to_coe, powerset_coe', powersetCard_coe, ← coe_range, coe_bind,
    ← List.map_flatMap, coe_card]
  exact coe_eq_coe.mpr ((List.range_bind_sublistsLen_perm _).map _)

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

Goal state before:
pp: case mpr
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
y : Finset α
hyt : y ⊆ t \ s
hyn : #y = n - #s
⊢ (y ∪ s ⊆ t ∧ #(y ∪ s) = n) ∧ s ⊆ y ∪ s

Tactic:
refine ⟨⟨union_subset (hyt.trans sdiff_subset) hst, ?_⟩, subset_union_right⟩

Goal state after:
case mpr
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
y : Finset α
hyt : y ⊆ t \ s
hyn : #y = n - #s
⊢ #(y ∪ s) = n
Module: Mathlib.Data.Set.Pairwise.Lattice

Goal state before:
pp: α : Type u_5
ι : Type u_6
s : Set ι
f : ι → Set α
h : s.PairwiseDisjoint f
x : (i : ↑s) × ↑(f ↑i)
⊢ ↑((biUnionEqSigmaOfDisjoint h).symm x) = ↑x.snd

Tactic:
by
  rfl

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:
Finset.sup_insert (b := a) (s := s) (f := f)

Goal state after:
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
⊢ max (f a) (s.sup f) ∈ f '' ↑(insert a s)
Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed

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

Tactic:
rw [iSup_of_empty']

Goal state after:
Module: Mathlib.Order.Hom.WithTopBot

Goal state before:
pp: α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : DecidablePred fun x ↦ x = ⊤
a : α
h : a ≠ ⊤
⊢ subtypeOrderIso.symm a = ↑⟨a, h⟩

Tactic:
by
  rw [OrderIso.symm_apply_eq]
  rfl

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Multiset ι
f : ι → α
h : ∃ x ∈ s, sSup ∅ ≤ f x
⊢ ⨆ x ∈ s, f x ∈ map f s

Tactic:
by
  classical
  simpa using s.toFinset.ciSup_mem_image f (by simpa using h)

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝¹ : ConditionallyCompleteLinearOrder α
a : α
inst✝ : Nonempty ι
f : ι → α
hb : BddBelow (range f)
⊢ iInf f < a ↔ ∃ i, f i < a

Tactic:
simpa only [mem_range, exists_exists_eq_and] using! csInf_lt_iff hb (range_nonempty _)

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
x y : α × β
⊢ x ⩿ y ↔ x.1 ⩿ y.1 ∧ x.2 = y.2 ∨ x.2 ⩿ y.2 ∧ x.1 = y.1

Tactic:
cases x
  cases y
  exact mk_wcovBy_mk_iff

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
x y : α × β
⊢ x ⋖ y ↔ x.1 ⋖ y.1 ∧ x.2 = y.2 ∨ x.2 ⋖ y.2 ∧ x.1 = y.1

Tactic:
by
  cases x
  cases y
  exact mk_covBy_mk_iff

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
inst✝ : Nonempty ι
i : ι
hab : a i ⩿ b i
h : ∀ (j : ι), j ≠ i → AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)
c : (i : ι) → α i
hac✝ : a < c
hcb : c < b
hac : a ≤ c
j : ι
hj : a j < c j
⊢ a i < c i

Tactic:
exact (eq_or_ne j i).elim (· ▸ hj) fun hj' ↦
      ((lt_of_antisymmRel_of_lt (h j hj').symm hj).not_ge (hcb.le j)).elim

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: case mp
ι : Type u_3
α : ι → Type u_4
inst✝ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : a ⋖ b
⊢ ∃ i, a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)

Tactic:
obtain ⟨j, hj⟩ := (Pi.lt_def.1 h.1).2

Goal state after:
case mp
ι : Type u_3
α : ι → Type u_4
inst✝ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : a ⋖ b
j : ι
hj : a j < b j
⊢ ∃ i, a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)
Module: Mathlib.Order.Cover

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst✝ : Nonempty ι
h : a ⩿ b
⊢ ∃ i, ∀ (j : ι), j ≠ i → a j = b j

Tactic:
by
  obtain ⟨i, hi⟩ := exists_forall_antisymmRel_of_wcovBy h
  exact ⟨i, fun j hj ↦ AntisymmRel.eq (hi _ hj)⟩

Goal state after:
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : WellFoundedGT α
a : ℕ →o α
m : ℕ
hm : m ≤ monotonicSequenceLimitIndex a
⊢ a m ≤ monotonicSequenceLimit a

Tactic:
exact a.monotone hm

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrderTop α
a x : Subtype p
⊢ x ∈ Finset.subtype p (Ioi ↑a) ↔ a < x

Tactic:
simp_rw [Finset.mem_subtype, mem_Ioi, Subtype.coe_lt_coe]

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

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a₁ a₂ : α
⊢ a₁ ∈ orbit G a₂ ↔ a₂ ∈ orbit G a₁

Tactic:
simp_rw [← orbit_eq_iff, eq_comm]

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
s : Set α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a : α
ha : a ∈ lowerBounds s
f : (fun x1 x2 ↦ x1 > x2) ↪r fun x1 x2 ↦ x1 < x2
hf : ∀ (n : ℕ), f n ∈ s
⊢ (range ⇑f).Finite

Tactic:
exact (finite_Icc a <| f 0).subset <| range_subset_iff.2 <| fun n =>
    ⟨ha <| hf _,
      antitone_iff_forall_lt.2 (fun a b hab => (f.map_rel_iff.2 hab).le) <| Nat.zero_le _⟩

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case mp
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
⊢ (∃ x, IsBadSeq r s x) → ∃ f, IsBadSeq r s f ∧ ∀ (n : ℕ), IsMinBadSeq r rk s n f

Tactic:
apply exists_min_bad_of_exists_bad

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ (center G).Characteristic

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

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

Goal state before:
pp: G : Type u_4
inst✝ : Group G
H : Subgroup G
g h : ↥H
⊢ ↑(toConjAct g • h) = toConjAct ↑g • ↑h

Tactic:
by
  rfl

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

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
inst✝ : Monoid M
c : Con M
u : c.Quotientˣ
f : (x y : M) → c (x * y) 1 → c (y * x) 1 → α
Hf :
  ∀ (x y : M) (hxy : c (x * y) 1) (hyx : c (y * x) 1) (x' y' : M) (hxy' : c (x' * y') 1) (hyx' : c (y' * x') 1),
    c x x' → c y y' → f x y hxy hyx = f x' y' hxy' hyx'
⊢ α

Tactic:
refine
    Con.hrecOn₂ (cN := c) (φ := fun x y => x * y = 1 → y * x = 1 → α) (u : c.Quotient)
      (↑u⁻¹ : c.Quotient)
      (fun (x y : M) (hxy : (x * y : c.Quotient) = 1) (hyx : (y * x : c.Quotient) = 1) =>
        f x y (c.eq.1 hxy) (c.eq.1 hyx))
      (fun x y x' y' hx hy => ?_) u.3 u.4

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
inst✝ : Monoid M
c : Con M
u : c.Quotientˣ
f : (x y : M) → c (x * y) 1 → c (y * x) 1 → α
Hf :
  ∀ (x y : M) (hxy : c (x * y) 1) (hyx : c (y * x) 1) (x' y' : M) (hxy' : c (x' * y') 1) (hyx' : c (y' * x') 1),
    c x x' → c y y' → f x y hxy hyx = f x' y' hxy' hyx'
x y x' y' : M
hx : c x x'
hy : c y y'
⊢ (fun hxy hyx ↦ f x y ⋯ ⋯) ≍ fun hxy hyx ↦ f x' y' ⋯ ⋯
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
x3 : α
b3 : Bool
x4 : α
b4 : Bool
tl x✝⁵ x✝⁴ : List (α × Bool)
x✝³ : α
x✝² : Bool
x✝¹ : α
x✝ : Bool
H : (x3, b3) :: (x4, b4) :: tl ++ (x✝³, x✝²) :: (x✝³, !x✝²) :: x✝⁵ = [] ++ (x✝¹, x✝) :: (x✝¹, !x✝) :: x✝⁴
⊢ (x3, b3) :: (x4, b4) :: tl ++ x✝⁵ = [] ++ x✝⁴ ∨
    ∃ L₅, Step ((x3, b3) :: (x4, b4) :: tl ++ x✝⁵) L₅ ∧ Step ([] ++ x✝⁴) L₅

Tactic:
by
    injections; subst_vars; right; simpa using ⟨_, Red.Step.cons_not, Red.Step.not⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
a b : α
⊢ (rightRel s) a b → (leftRel s) a⁻¹ b⁻¹

Tactic:
by
      rw [leftRel_apply, rightRel_apply]
      exact fun h => (congr_arg (· ∈ s) (by simp)).mp (s.inv_mem h)

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
a b : α
⊢ (leftRel s) a b → (rightRel s) a⁻¹ b⁻¹

Tactic:
by
      rw [leftRel_apply, rightRel_apply]
      exact fun h => (congr_arg (· ∈ s) (by simp)).mp (s.inv_mem h)

Goal state after:
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₂⟩; simp

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

Goal state before:
pp: α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
x✝¹ : FreeGroup Unit
L : List (Unit × Bool)
x✝ : Unit × Bool
tl : List (Unit × Bool)
ih : of () ^ (List.map ((fun x ↦ bif x.2 then x.1 else -x.1) ∘ fun x ↦ (1, x.2)) tl).sum = mk tl
b : Bool
⊢ of () ^ (List.map ((fun x ↦ bif x.2 then x.1 else -x.1) ∘ fun x ↦ (1, x.2)) ((PUnit.unit, b) :: tl)).sum =
    mk ((PUnit.unit, b) :: tl)

Tactic:
cases b <;> simp [zpow_add, ih]

Goal state after:
case false
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
x✝¹ : FreeGroup Unit
L : List (Unit × Bool)
x✝ : Unit × Bool
tl : List (Unit × Bool)
ih : of () ^ (List.map ((fun x ↦ bif x.2 then x.1 else -x.1) ∘ fun x ↦ (1, x.2)) tl).sum = mk tl
⊢ (of ())⁻¹ * mk tl = mk ((PUnit.unit, false) :: tl)

case true
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
x✝¹ : FreeGroup Unit
L : List (Unit × Bool)
x✝ : Unit × Bool
tl : List (Unit × Bool)
ih : of () ^ (List.map ((fun x ↦ bif x.2 then x.1 else -x.1) ∘ fun x ↦ (1, x.2)) tl).sum = mk tl
⊢ of () * mk tl = mk ((PUnit.unit, true) :: tl)
Module: Mathlib.GroupTheory.QuotientGroup.Defs

Goal state before:
pp: G : Type u_1
inst✝ : Group G
c : Con G
x y : G
h : c x y
⊢ c (x⁻¹ * y) 1

Tactic:
by simpa using c.mul (c.refl x⁻¹) (c.symm h)

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
b₁ b₂ : M
a : ι
ha : a ∈ s
h : f a * b₁ = f a * b₂
⊢ (∏ a ∈ insert a (s.erase a), f a) * b₁ = (∏ a ∈ insert a (s.erase a), f a) * b₂

Tactic:
simp only [mem_erase, ne_eq, not_true_eq_false, false_and, not_false_eq_true, prod_insert]

Goal state after:
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
b₁ b₂ : M
a : ι
ha : a ∈ s
h : f a * b₁ = f a * b₂
⊢ (f a * ∏ a ∈ s.erase a, f a) * b₁ = (f a * ∏ a ∈ s.erase a, f a) * b₂
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: M : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : PartialOrder M
inst✝⁴ : Sub M
inst✝³ : OrderedSub M
inst✝² : AddLeftMono M
inst✝¹ : AddLeftReflectLE M
inst✝ : ExistsAddOfLE M
f : ℕ → M
h : Monotone f
n : ℕ
⊢ f 0 = 0 + f 0

Tactic:
rw [zero_add]

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

Goal state before:
pp: M : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : PartialOrder M
inst✝⁴ : Sub M
inst✝³ : OrderedSub M
inst✝² : AddLeftMono M
inst✝¹ : AddLeftReflectLE M
inst✝ : ExistsAddOfLE M
f : ℕ → M
h : Monotone f
n : ℕ
⊢ ∀ k < n, f (k + 1) - f 0 = f k - f 0 + (f (k + 1) - f k)

Tactic:
intro n _
    have h₁ : f n ≤ f (n + 1) := h (Nat.le_succ _)
    have h₂ : f 0 ≤ f n := h (Nat.zero_le _)
    rw [tsub_add_eq_add_tsub h₂, add_tsub_cancel_of_le h₁]

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
s : Finset ι
f : ι → M
h : ∀ (i : ι), f i ≠ 1 → i ∈ s
⊢ ∀ x ∈ univ, x ∉ s → f x = 1

Tactic:
simpa [not_imp_comm (a := _ ∈ s)]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ map H.subtype (_root_.commutator ↥H) = ⁅H, H⁆

Tactic:
rw [_root_.commutator_def, map_commutator, ← MonoidHom.range_eq_map, H.range_subtype]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Type u_4
inst✝ : Group H
f : G →* H
⊢ map f ⁅⊤, ⊤⁆ = ⁅f.range, f.range⁆

Tactic:
Subgroup.map_commutator

Goal state after:
G : Type u_1
inst✝¹ : Group G
H : Type u_4
inst✝ : Group H
f : G →* H
⊢ ⁅map f ⊤, map f ⊤⁆ = ⁅f.range, f.range⁆
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case refine_1.refine_1
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
r : X
s : ↥S
r' : X
s' u : ↥S
v : R
hru : u • r' = v • r
hsu : ↑u * ↑s' = v * ↑s
r₂ : R
s₂ : ↥S
h₁ : ↑s₂ * ↑s = r₂ * ↑s'
r₃ : R
s₃ : ↥S
h₂ : ↑s₃ * r₂ = r₃ * ↑u
this : r₃ * v * ↑s = ↑s₃ * ↑s₂ * ↑s
w : ↥S
hw : ↑w * (r₃ * v) = ↑w * (↑s₃ * ↑s₂)
⊢ (↑w * (r₃ * v)) • r = (↑w * (r₃ * ↑u)) • r'

pp: case refine_1.refine_2
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
r : X
s : ↥S
r' : X
s' u : ↥S
v : R
hru : u • r' = v • r
hsu : ↑u * ↑s' = v * ↑s
r₂ : R
s₂ : ↥S
h₁ : ↑s₂ * ↑s = r₂ * ↑s'
r₃ : R
s₃ : ↥S
h₂ : ↑s₃ * r₂ = r₃ * ↑u
this : r₃ * v * ↑s = ↑s₃ * ↑s₂ * ↑s
w : ↥S
hw : ↑w * (r₃ * v) = ↑w * (↑s₃ * ↑s₂)
⊢ ↑w * (r₃ * v) * ↑s = ↑w * (r₃ * ↑u) * ↑s'

Tactic:
· simp only [mul_smul, hru, ← Submonoid.smul_def]

Goal state after:
case refine_1.refine_2
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
r : X
s : ↥S
r' : X
s' u : ↥S
v : R
hru : u • r' = v • r
hsu : ↑u * ↑s' = v * ↑s
r₂ : R
s₂ : ↥S
h₁ : ↑s₂ * ↑s = r₂ * ↑s'
r₃ : R
s₃ : ↥S
h₂ : ↑s₃ * r₂ = r₃ * ↑u
this : r₃ * v * ↑s = ↑s₃ * ↑s₂ * ↑s
w : ↥S
hw : ↑w * (r₃ * v) = ↑w * (↑s₃ * ↑s₂)
⊢ ↑w * (r₃ * v) * ↑s = ↑w * (r₃ * ↑u) * ↑s'
Module: Mathlib.Algebra.Order.Hom.MonoidWithZero

Goal state before:
pp: α : Type u_2
β : Type u_3
hα : Preorder α
hα' : MulZeroOneClass α
hβ : Preorder β
hβ' : MulZeroOneClass β
f : α →*₀o β
⊢ f.toMonoidWithZeroHom = MonoidWithZeroHom.ofClass f

Tactic:
by
  rfl

Goal state after:
Module: Mathlib.Algebra.Order.Hom.MonoidWithZero

Goal state before:
pp: α : Type u_2
β : Type u_3
hα : Preorder α
hα' : MulZeroOneClass α
hβ : Preorder β
hβ' : MulZeroOneClass β
f : α →*₀ β
hf : Monotone ⇑f
⊢ MonoidWithZeroHom.ofClass { toMonoidWithZeroHom := f, monotone' := hf } = f

Tactic:
by
  rfl

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.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₂)
this : ↑s₄' * r₃' * (↑s₂' * ↑s) ∈ S
⊢ r₁' • r₁ /ₒ (s₁' * s) = r₂' • r₂ • r₁ /ₒ (s₂' * s)

Tactic:
rw [OreLocalization.expand' _ _ (s₄' * s₃'), OreLocalization.expand _ (s₂' * s) _ this]

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₂)
this : ↑s₄' * r₃' * (↑s₂' * ↑s) ∈ S
⊢ (s₄' * s₃') • r₁' • r₁ /ₒ (s₄' * s₃' * (s₁' * s)) = (↑s₄' * r₃') • r₂' • r₂ • r₁ /ₒ ⟨↑s₄' * r₃' * ↑(s₂' * s), this⟩
Module: Mathlib.Algebra.Order.Hom.Ring

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁸ : Mul α
inst✝⁷ : Add α
inst✝⁶ : LE α
inst✝⁵ : Mul β
inst✝⁴ : Add β
inst✝³ : LE β
inst✝² : Mul γ
inst✝¹ : Add γ
inst✝ : LE γ
f g : α ≃+*o β
h₁ : f.toFun = g.toFun
h₂ : f.invFun = g.invFun
⊢ f = g

Tactic:
by
    obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := f
    obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := g
    congr

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

Goal state before:
pp: α : Type u_2
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : LE α
x : α
⊢ (OrderRingIso.refl α) x = x

Tactic:
by
  rfl

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.10
inst✝¹ : MulAction R X
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
x : OreLocalization S R
r t : R
s : ↥S
ht : t * ↑s ∈ S
this : ↑(fS ⟨t * ↑s, ht⟩) = f t * ↑(fS s)
| ↑(fS ⟨t * ↑s, ht⟩)⁻¹ * (f t * (1 * f r))

Tactic:
← Units.val_one,

Goal state after:
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type ?u.10
inst✝¹ : MulAction R X
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
x : OreLocalization S R
r t : R
s : ↥S
ht : t * ↑s ∈ S
this : ↑(fS ⟨t * ↑s, ht⟩) = f t * ↑(fS s)
| ↑(fS ⟨t * ↑s, ht⟩)⁻¹ * (f t * (↑1 * f r))
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
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
x : OreLocalization S R
r t : R
s : ↥S
ht : t * ↑s ∈ S
this : ↑(fS ⟨t * ↑s, ht⟩) = f t * ↑(fS s)
| ↑(fS ⟨t * ↑s, ht⟩)⁻¹ * f (t * r)

Tactic:
rw [map_mul, ← one_mul (f r), ← Units.val_one, ← mul_inv_cancel (fS s)]

Goal state after:
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type ?u.10
inst✝¹ : MulAction R X
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
x : OreLocalization S R
r t : R
s : ↥S
ht : t * ↑s ∈ S
this : ↑(fS ⟨t * ↑s, ht⟩) = f t * ↑(fS s)
| ↑(fS ⟨t * ↑s, ht⟩)⁻¹ * (f t * (↑(fS s * (fS s)⁻¹) * f r))