mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
β : Type u_3
x : α
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
f : α → β
hf : ∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)
hx : Minimal (fun x ↦ x ∈ s) x
y : α
hy : y ∈ s
⊢ f y ≤ f x → x ≤ y

Tactic:
hf hy hx.prop

Goal state after:
α : Type u_2
β : Type u_3
x : α
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
f : α → β
hf : ∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)
hx : Minimal (fun x ↦ x ∈ s) x
y : α
hy : y ∈ s
⊢ y ≤ x → x ≤ y
Module: Mathlib.Order.Minimal

Goal state before:
pp: case e'_3
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
P : α → Prop
x✝¹ x✝ : β
⊢ P (f.symm x✝) ↔ ∃ x₀, P x₀ ∧ f x₀ = x✝

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b c d : α
h : b ≤ c
a✝ : α
hab : a✝ ∈ Ico a b
hbc : a✝ ∈ Ico c d
⊢ False

Tactic:
mem_Ico

Goal state after:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b c d : α
h : b ≤ c
a✝ : α
hab : a ≤ a✝ ∧ a✝ < b
hbc : c ≤ a✝ ∧ a✝ < d
⊢ False
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: case inr
s : Set ℕ
m : ℕ
h : s.Nonempty
hm : m < Nat.find h
⊢ m ∉ s

Tactic:
exact Nat.find_min h hm

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

Goal state before:
pp: a b c : ℕ
h : c ≤ a
x : ℕ
⊢ (∃ a_1 ∈ Ico a b, a_1 - c = x) ↔ x ∈ Ico (a - c) (b - c)

Tactic:
mem_Ico

Goal state after:
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
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: s : Set ℕ
hs : ¬BddBelow s
⊢ sInf s = sInf ∅

Tactic:
simp at hs

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

Goal state before:
pp: a b c : ℕ
hac : a ≤ c
x : ℕ
⊢ (∃ a_1 ∈ Ico a b, c - a_1 = x) ↔ x ∈ Ico (c + 1 - b) (c + 1 - a)

Tactic:
mem_Ico

Goal state after:
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
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a b x : ℕ
⊢ x ∈ Ico a.succ b ↔ x ≠ a ∧ x ∈ Ico a b

Tactic:
mem_Ico

Goal state after:
a b x : ℕ
⊢ a.succ ≤ x ∧ x < b ↔ x ≠ a ∧ a ≤ x ∧ x < b
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a b : ℕ
h : a ≤ b
x : ℕ
⊢ x ∈ Ico a b.succ ↔ x = b ∨ x ∈ Ico a b

Tactic:
mem_Ico

Goal state after:
a b : ℕ
h : a ≤ b
x : ℕ
⊢ a ≤ x ∧ x < b.succ ↔ x = b ∨ a ≤ x ∧ x < b
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 : x ∈ Ico ↑a ↑b
⊢ p x

Tactic:
mem_Ico

Goal state after:
α : 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
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderTop α
inst✝¹ : OrderBot α
inst✝ : Fintype α
⊢ Ici ⊥ = univ

Tactic:
by
  ext a; simp only [mem_Ici, bot_le, mem_univ]

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → α → Prop
r' : β → β → Prop
f : α → β
s : Set α
hs : s.PartiallyWellOrderedOn r
hf : ∀ a₁ ∈ s, ∀ a₂ ∈ s, r a₁ a₂ → r' (f a₁) (f a₂)
⊢ (f '' s).PartiallyWellOrderedOn r'

Tactic:
partiallyWellOrderedOn_iff_exists_lt

Goal state after:
α : Type u_2
β : Type u_3
r : α → α → Prop
r' : β → β → Prop
f : α → β
s : Set α
hs : ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ m n, m < n ∧ r (f m) (f n)
hf : ∀ a₁ ∈ s, ∀ a₂ ∈ s, r a₁ a₂ → r' (f a₁) (f a₂)
⊢ ∀ (f_1 : ℕ → β), (∀ (n : ℕ), f_1 n ∈ f '' s) → ∃ m n, m < n ∧ r' (f_1 m) (f_1 n)
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: case inr.refine_2
α : Type u_1
inst✝ : Preorder α
x✝ : WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s → s.Finite
hwf : WellFoundedLT α
f : ℕ → α
g : ℕ ↪o ℕ
h2 : ∀ (m n : ℕ), m < n → ¬f (g m) > f (g n)
hc : ∀ (m n : ℕ), m < n → ¬f m ≤ f n
m n : ℕ
hf : f (g m) = f (g n)
⊢ m = n

Tactic:
obtain h | rfl | h := lt_trichotomy m n <;>
        (first | rfl | cases (hf ▸ hc _ _ (g.strictMono h)) le_rfl)

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : Std.Refl r
inst✝ : Std.Symm r
⊢ (∀ t ⊆ s, IsAntichain r t → t.Finite) → s.PartiallyWellOrderedOn r

Tactic:
partiallyWellOrderedOn_iff_exists_lt

Goal state after:
α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : Std.Refl r
inst✝ : Std.Symm r
⊢ (∀ t ⊆ s, IsAntichain r t → t.Finite) → ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ m n, m < n ∧ r (f m) (f n)
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
⊢ (WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s → s.Finite) ↔ WellFoundedLT α

Tactic:
and_iff_left_iff_imp

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
⊢ WellFoundedLT α → ∀ (s : Set α), IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s → s.Finite
Module: Mathlib.Order.Interval.Finset.Basic

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

Tactic:
by simp [← coe_inj, h]

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

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

Tactic:
by simp [← coe_inj, h]

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

Goal state before:
pp: M : Type u_3
S : Type u_6
inst✝² : Monoid M
inst✝¹ : SetLike S M
inst✝ : SubmonoidClass S M
n : ℕ
x✝ : n + 2 ≠ 0
H : S
⊢ ↑H ^ (n + 2) = ↑H

Tactic:
by rw [pow_succ, coe_set_pow n.succ_ne_zero, coe_mul_coe]

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

Goal state before:
pp: case zero
M : Type u_3
inst✝ : Monoid M
s : Set M
S : Submonoid M
hs : s ⊆ ↑S
⊢ s ^ 0 ⊆ ↑S

Tactic:
simp [pow_succ, *]

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

Goal state before:
pp: case succ
M : Type u_3
inst✝ : Monoid M
s : Set M
S : Submonoid M
hs : s ⊆ ↑S
n✝ : ℕ
a✝ : s ^ n✝ ⊆ ↑S
⊢ s ^ (n✝ + 1) ⊆ ↑S

Tactic:
simp [pow_succ, *]

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

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

Tactic:
by simp [← coe_inj, h]

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

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

Tactic:
by simp [← coe_inj, h]

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

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

Tactic:
by simp [← coe_inj, h]

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → α → Prop
r' : β → β → Prop
s : Set α
inst✝ : IsPreorder α r
t : Set β
hs : s.PartiallyWellOrderedOn r
ht : t.PartiallyWellOrderedOn r'
⊢ (s ×ˢ t).PartiallyWellOrderedOn fun x y ↦ r x.1 y.1 ∧ r' x.2 y.2

Tactic:
partiallyWellOrderedOn_iff_exists_lt

Goal state after:
α : Type u_2
β : Type u_3
r : α → α → Prop
r' : β → β → Prop
s : Set α
inst✝ : IsPreorder α r
t : Set β
hs : s.PartiallyWellOrderedOn r
ht : t.PartiallyWellOrderedOn r'
⊢ ∀ (f : ℕ → α × β), (∀ (n : ℕ), f n ∈ s ×ˢ t) → ∃ m n, m < n ∧ r (f m).1 (f n).1 ∧ r' (f m).2 (f n).2
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
s : Set α
a : α
hs : s.IsPWO
ha : a ∈ s
⊢ ∃ b ≤ a, Minimal (fun x ↦ x ∈ s) b

Tactic:
by
  let t : Set s := {x | x ≤ a}
  let h : t.Nonempty := ⟨⟨a, ha⟩, le_rfl⟩
  refine ⟨hs.wellFounded.min t h, hs.wellFounded.min_mem t h,
    (hs.wellFounded.min t h).2, fun y hy hle => ?_⟩
  by_contra hnle
  exact hs.wellFounded.not_lt_min t (x := ⟨y, hy⟩) (hle.trans (hs.wellFounded.min_mem t h))
    ⟨hle, hnle⟩

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
s : Set α
hs : s.PartiallyWellOrderedOn r
f : ℕ → α
hf : ∀ (x : ℕ), ∃ y ∈ f ⁻¹' s, x < y
φ : ℕ → ℕ
hφm : StrictMono φ
hφs : ∀ (n : ℕ), φ n ∈ f ⁻¹' s
⊢ ∃ m n, m < n ∧ r (f m) (f n)

Tactic:
partiallyWellOrderedOn_iff_exists_lt

Goal state after:
α : Type u_2
r : α → α → Prop
s : Set α
hs : ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ m n, m < n ∧ r (f m) (f n)
f : ℕ → α
hf : ∀ (x : ℕ), ∃ y ∈ f ⁻¹' s, x < y
φ : ℕ → ℕ
hφm : StrictMono φ
hφs : ∀ (n : ℕ), φ n ∈ f ⁻¹' s
⊢ ∃ m n, m < n ∧ r (f m) (f n)
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
s : Set α
⊢ s.PartiallyWellOrderedOn r ↔ ∀ (f : ℕ → α), ¬IsBadSeq r s f

Tactic:
partiallyWellOrderedOn_iff_exists_lt

Goal state after:
α : Type u_2
r : α → α → Prop
s : Set α
⊢ (∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ m n, m < n ∧ r (f m) (f n)) ↔ ∀ (f : ℕ → α), ¬IsBadSeq r s f
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : Quotient G α
a b : ↑x.orbit
c : α
h : ⟦a⟧ = ⟦b⟧
hb : b ∈ MulAction.orbit ↥H ⟦a⟧.out
⊢ MulAction.orbit (↥H) a = MulAction.orbit ↥H ⟦a⟧.out

Tactic:
rw [orbit_eq_iff, ← orbitRel_apply, ← Quotient.eq'', Quotient.out_eq', @Quotient.mk''_eq_mk]

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

Goal state before:
pp: M : Type u_2
inst✝ : Mul M
x : M
⊢ ((∀ (a : M), Commute (op x) (op a)) ∧
      (∀ (a a_1 : M), a_1 * a * x = a_1 * (a * x)) ∧ ∀ (a a_1 : M), x * (a_1 * a) = x * a_1 * a) ↔
    (∀ (a : M), Commute x a) ∧ (∀ (b c : M), x * (b * c) = x * b * c) ∧ ∀ (a b : M), a * b * x = a * (b * x)

Tactic:
aesop

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α : ((fun x ↦ (ofLex x).1) '' s).IsPWO
hβ : ∀ (a : α), {y | toLex (a, y) ∈ s}.IsPWO
⊢ s.PartiallyWellOrderedOn fun x1 x2 ↦ x1 ≤ x2

Tactic:
partiallyWellOrderedOn_iff_exists_lt

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hα : ((fun x ↦ (ofLex x).1) '' s).IsPWO
hβ : ∀ (a : α), {y | toLex (a, y) ∈ s}.IsPWO
⊢ ∀ (f : ℕ → Lex (α × β)), (∀ (n : ℕ), f n ∈ s) → ∃ m n, m < n ∧ f m ≤ f n
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
a : M
inst✝ : Invertible a
ha : a ∈ center M
⊢ ⅟a ∈ center M

Tactic:
rw [Semigroup.mem_center_iff] at *
  exact (Commute.invOf_right <| ha ·)

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g k : G
⊢ k ∈ centralizer {g} ↔ k * g = g * k

Tactic:
simp only [mem_centralizer_iff, Set.mem_singleton_iff, forall_eq]
  exact eq_comm

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

Goal state before:
pp: case zero
G : Type u_2
inst✝ : Group G
s : Set G
H : Subgroup G
hs : s ⊆ ↑H
⊢ s ^ 0 ⊆ ↑H

Tactic:
simp [pow_succ, *]

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

Goal state before:
pp: case succ
G : Type u_2
inst✝ : Group G
s : Set G
H : Subgroup G
hs : s ⊆ ↑H
n✝ : ℕ
a✝ : s ^ n✝ ⊆ ↑H
⊢ s ^ (n✝ + 1) ⊆ ↑H

Tactic:
simp [pow_succ, *]

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H K : Subgroup G
g : G
hg : map (↑(MulAut.conj g)) H = H ∧ map (↑(MulAut.conj g)) K = K
⊢ map (↑(MulAut.conj g)) H ⊔ map (↑(MulAut.conj g)) K = H ⊔ K

Tactic:
hg.1,

Goal state after:
G : Type u_2
inst✝ : Group G
H K : Subgroup G
g : G
hg : True ∧ map (↑(MulAut.conj g)) K = K
⊢ H ⊔ map (↑(MulAut.conj g)) K = H ⊔ K
Module: Mathlib.Data.Setoid.Basic

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

Tactic:
| symm _ _ _ ih =>

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

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

Tactic:
generalize hL : ((a, b) :: L₁ : List _) = L

Goal state after:
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₂
Module: Mathlib.GroupTheory.Congruence.Defs

Goal state before:
pp: case refine_1
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'
⊢ (↑x * ↑y = 1) = (↑x' * ↑y' = 1)

pp: case refine_2
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'
⊢ ∀ (a : ↑x * ↑y = 1) (a' : ↑x' * ↑y' = 1), a ≍ a' → (fun hyx ↦ f x y ⋯ ⋯) ≍ fun hyx ↦ f x' y' ⋯ ⋯

Tactic:
· rw [c.eq.2 hx, c.eq.2 hy]

Goal state after:
case refine_2
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'
⊢ ∀ (a : ↑x * ↑y = 1) (a' : ↑x' * ↑y' = 1), a ≍ a' → (fun hyx ↦ f x y ⋯ ⋯) ≍ fun hyx ↦ f x' y' ⋯ ⋯
Module: Mathlib.GroupTheory.Congruence.Defs

Goal state before:
pp: case refine_2.refine_1
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'
Hxy : ↑x * ↑y = 1
Hxy' : ↑x' * ↑y' = 1
⊢ (↑y * ↑x = 1) = (↑y' * ↑x' = 1)

pp: case refine_2.refine_2
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'
Hxy : ↑x * ↑y = 1
Hxy' : ↑x' * ↑y' = 1
⊢ ∀ (a : ↑y * ↑x = 1) (a' : ↑y' * ↑x' = 1), a ≍ a' → f x y ⋯ ⋯ ≍ f x' y' ⋯ ⋯

Tactic:
· rw [c.eq.2 hx, c.eq.2 hy]

Goal state after:
case refine_2.refine_2
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'
Hxy : ↑x * ↑y = 1
Hxy' : ↑x' * ↑y' = 1
⊢ ∀ (a : ↑y * ↑x = 1) (a' : ↑y' * ↑x' = 1), a ≍ a' → f x y ⋯ ⋯ ≍ f x' y' ⋯ ⋯
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
L₁ L₂ : List (α × Bool)
p : α × Bool
⊢ Red (p :: L₁) (p :: L₂) → Red L₁ L₂

Tactic:
generalize eq₁ : (p :: L₁ : List _) = LL₁

Goal state after:
α : Type u
L₁ L₂ : List (α × Bool)
p : α × Bool
LL₁ : List (α × Bool)
eq₁ : p :: L₁ = LL₁
⊢ Red LL₁ (p :: L₂) → Red L₁ L₂
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case nil
α : Type u
L₁ L₂ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
H1 : (x1, b1) ≠ (x2, b2)
H2 : Red ((x1, b1) :: L₁) ((x2, b2) :: L₂)
this : Red ((x1, b1) :: L₁) ([(x2, b2)] ++ L₂)
L₄ : List (α × Bool)
eq : (x1, b1) :: L₁ = [] ++ L₄
h₁ : Red [] [(x2, b2)]
h₂ : Red L₄ L₂
⊢ Red L₁ ((x1, !b1) :: (x2, b2) :: L₂)

pp: case cons
α : Type u
L₁ L₂ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
H1 : (x1, b1) ≠ (x2, b2)
H2 : Red ((x1, b1) :: L₁) ((x2, b2) :: L₂)
this : Red ((x1, b1) :: L₁) ([(x2, b2)] ++ L₂)
p : α × Bool
L₃ L₄ : List (α × Bool)
eq : (x1, b1) :: L₁ = p :: L₃ ++ L₄
h₁ : Red (p :: L₃) [(x2, b2)]
h₂ : Red L₄ L₂
⊢ Red L₁ ((x1, !b1) :: (x2, b2) :: L₂)

Tactic:
· simp [nil_iff] at h₁

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

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
⊢ ∀ (a b c : FreeGroup α), a * b * c = a * (b * c)

Tactic:
rintro ⟨L₁⟩ ⟨L₂⟩ ⟨L₃⟩; simp

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

Goal state before:
pp: ι : Type u_5
M : Type u_6
s₁ s₂ : Finset ι
f g : ι → M
inst✝ : CommMonoid M
h₁ : ∀ a ∈ s₁, a ∉ s₂ → f a = 1
h₂ : ∀ a ∈ s₂, a ∉ s₁ → g a = 1
h : ∀ a ∈ s₁, a ∈ s₂ → f a = g a
| ∏ a ∈ s₁, f a

Tactic:
rw [← sdiff_union_inter s₁ s₂, prod_union_eq_right (by simp_all)]

Goal state after:
ι : Type u_5
M : Type u_6
s₁ s₂ : Finset ι
f g : ι → M
inst✝ : CommMonoid M
h₁ : ∀ a ∈ s₁, a ∉ s₂ → f a = 1
h₂ : ∀ a ∈ s₂, a ∉ s₁ → g a = 1
h : ∀ a ∈ s₁, a ∈ s₂ → f a = g a
| ∏ a ∈ s₁ ∩ s₂, f a
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: case neg
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a b : ι
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq ι
h₁ : a ∈ s
h₂ : b ∉ s
⊢ ∏ x ∈ s, f x = f a * f b

Tactic:
hb h₂,

Goal state after:
case neg
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a b : ι
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq ι
h₁ : a ∈ s
h₂ : b ∉ s
⊢ ∏ x ∈ s, f x = f a * 1
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: case neg
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a b : ι
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq ι
h₁ : a ∉ s
h₂ : b ∉ s
⊢ ∏ x ∈ s, f x = 1 * f b

Tactic:
hb h₂,

Goal state after:
case neg
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a b : ι
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq ι
h₁ : a ∉ s
h₂ : b ∉ s
⊢ ∏ x ∈ s, f x = 1 * 1
Module: Mathlib.GroupTheory.QuotientGroup.Defs

Goal state before:
pp: G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : N.Normal
⊢ Subgroup.map (mk' N) N = ⊥

Tactic:
aesop

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M✝ : Type u_1
N : Type u_2
inst✝⁵ : Monoid M✝
G : Type u_3
H : Type u_4
inst✝⁴ : Group G
inst✝³ : AddGroup H
ι : Type u_5
inst✝² : Finite ι
M : ι → Type u_6
inst✝¹ : (i : ι) → Monoid (M i)
inst✝ : ∀ (i : ι), Monoid.FG (M i)
⊢ ⊤.FG

Tactic:
rw [← Submonoid.pi_top Set.univ]

Goal state after:
M✝ : Type u_1
N : Type u_2
inst✝⁵ : Monoid M✝
G : Type u_3
H : Type u_4
inst✝⁴ : Group G
inst✝³ : AddGroup H
ι : Type u_5
inst✝² : Finite ι
M : ι → Type u_6
inst✝¹ : (i : ι) → Monoid (M i)
inst✝ : ∀ (i : ι), Monoid.FG (M i)
⊢ (Submonoid.pi Set.univ fun i ↦ ⊤).FG
Module: Mathlib.Algebra.Order.Hom.Monoid

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁶ : Group α
inst✝⁵ : Monoid β
F : Type u_6
inst✝⁴ : FunLike F α β
inst✝³ : MonoidHomClass F α β
inst✝² : LE β
inst✝¹ : MulRightMono β
inst✝ : MulLeftMono β
f✝ g✝ : F
x✝ : α
f g : F
x : α
hfg : f x⁻¹ ≤ g x⁻¹
⊢ f x * (g x⁻¹ * g x) = f x

Tactic:
by simp [← map_mul]

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

Goal state before:
pp: case inl
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
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'
this : k (g z') = k (g w')
surj : Set.SurjOn ⇑g ↑S ↑T
c : M
hc : c ∈ ↑S
hc' : g c ∈ T
eq : c * z' = c * w'
⊢ ∃ c, ↑c * z' = ↑c * w'

Tactic:
exact ⟨⟨c, hc⟩, eq⟩

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

Goal state before:
pp: case top.top
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
⊢ ⊤ * ⊤ = if ⊤ = 0 ∨ ⊤ = 0 then 0 else map₂ (fun x1 x2 ↦ x1 * x2) ⊤ ⊤

Tactic:
aesop

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

Goal state before:
pp: case top.coe
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝ : α
⊢ ⊤ * ↑a✝ = if ⊤ = 0 ∨ ↑a✝ = 0 then 0 else map₂ (fun x1 x2 ↦ x1 * x2) ⊤ ↑a✝

Tactic:
aesop

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

Goal state before:
pp: case coe.top
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝ : α
⊢ ↑a✝ * ⊤ = if ↑a✝ = 0 ∨ ⊤ = 0 then 0 else map₂ (fun x1 x2 ↦ x1 * x2) ↑a✝ ⊤

Tactic:
aesop

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

Goal state before:
pp: case coe.coe
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝¹ a✝ : α
⊢ ↑a✝¹ * ↑a✝ = if ↑a✝¹ = 0 ∨ ↑a✝ = 0 then 0 else map₂ (fun x1 x2 ↦ x1 * x2) ↑a✝¹ ↑a✝

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithTop α
⊢ (if a = 0 ∨ b = 0 then 0 else map₂ (fun x1 x2 ↦ x1 * x2) a b) = ⊤ ↔ a ≠ 0 ∧ b = ⊤ ∨ a = ⊤ ∧ b ≠ 0

Tactic:
aesop

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

Goal state before:
pp: case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
S' : Type u_6
inst✝⁵ : Mul R
inst✝⁴ : Mul S
inst✝³ : Add R
inst✝² : Add S
inst✝¹ : Mul S'
inst✝ : Add S'
toEquiv✝¹ : R ≃ S
map_mul'✝¹ : ∀ (x y : R), toEquiv✝¹.toFun (x * y) = toEquiv✝¹.toFun x * toEquiv✝¹.toFun y
map_add'✝¹ : ∀ (x y : R), toEquiv✝¹.toFun (x + y) = toEquiv✝¹.toFun x + toEquiv✝¹.toFun y
toEquiv✝ : R ≃ S
map_mul'✝ : ∀ (x y : R), toEquiv✝.toFun (x * y) = toEquiv✝.toFun x * toEquiv✝.toFun y
map_add'✝ : ∀ (x y : R), toEquiv✝.toFun (x + y) = toEquiv✝.toFun x + toEquiv✝.toFun y
h₁ :
  { toEquiv := toEquiv✝¹, map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ }.toFun =
    { toEquiv := toEquiv✝, map_mul' := map_mul'✝, map_add' := map_add'✝ }.toFun
h₂ :
  { toEquiv := toEquiv✝¹, map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ }.invFun =
    { toEquiv := toEquiv✝, map_mul' := map_mul'✝, map_add' := map_add'✝ }.invFun
⊢ toEquiv✝¹ = toEquiv✝

Tactic:
apply Equiv.coe_fn_injective h₁

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : CommMonoid N
f : S.LocalizationMap N
m : M
hm : IsRegular m
n₁ n₂ : N
ms₁ : M × ↥S
eq₁ : n₁ * f ↑ms₁.2 = f ms₁.1
ms₂ : M × ↥S
eq₂ : n₂ * f ↑ms₂.2 = f ms₂.1
eq : f m * (f ms₁.1 * f ↑ms₂.2) = f m * (n₂ * f ↑ms₁.2 * f ↑ms₂.2)
⊢ f ms₁.1 * f ↑ms₂.2 = n₂ * f ↑ms₁.2 * f ↑ms₂.2

Tactic:
mul_right_comm n₂,

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : CommMonoid N
f : S.LocalizationMap N
m : M
hm : IsRegular m
n₁ n₂ : N
ms₁ : M × ↥S
eq₁ : n₁ * f ↑ms₁.2 = f ms₁.1
ms₂ : M × ↥S
eq₂ : n₂ * f ↑ms₂.2 = f ms₂.1
eq : f m * (f ms₁.1 * f ↑ms₂.2) = f m * (n₂ * f ↑ms₂.2 * f ↑ms₁.2)
⊢ f ms₁.1 * f ↑ms₂.2 = n₂ * f ↑ms₂.2 * f ↑ms₁.2