mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Mul α
s : Set α
a b : α
⊢ s * {a, b} = s <• a ∪ s <• b

Tactic:
rw [insert_eq, mul_union, mul_singleton, mul_singleton]; rfl

Goal state after:
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: case mpr
α : Type u_2
inst✝ : Group α
s t : Set α
x : αᵐᵒᵖ
a b : α
H : a⁻¹ * b = unop x
ha : a ∈ s
hb : b ∈ t
this : op (a⁻¹ * b) = x
⊢ (x • s ∩ t).Nonempty

Tactic:
exact ⟨b, mem_inter (mem_smul_set.mpr ⟨a, ha, by simp [← this]⟩) hb⟩

Goal state after:
Module: Mathlib.Algebra.FreeMonoid.Basic

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
f : α → β
⊢ Function.Surjective ⇑(map f) → Function.Surjective f

Tactic:
intro fs

Goal state after:
case mp
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective ⇑(map f)
⊢ Function.Surjective f
Module: Mathlib.Algebra.FreeMonoid.Basic

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
f : α → β
⊢ Function.Surjective f → Function.Surjective ⇑(map f)

Tactic:
intro fs

Goal state after:
case mpr
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective f
⊢ Function.Surjective ⇑(map f)
Module: Mathlib.Data.Sigma.Lex

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
a b : (i : ι) × α i
⊢ Lex r s a b ↔ r a.fst b.fst ∨ ∃ h, s b.fst (h ▸ a.snd) b.snd

Tactic:
constructor
  · rintro (⟨a, b, hij⟩ | ⟨a, b, hab⟩)
    · exact Or.inl hij
    · exact Or.inr ⟨rfl, hab⟩
  · obtain ⟨i, a⟩ := a
    dsimp only
    rintro (h | ⟨rfl, h⟩)
    · exact Lex.left _ _ h
    · exact Lex.right _ _ h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : LE β
t c : Lex (α × β)
h : t ≤ c
x✝ : t.1 < c.1 ∨ t.1 = c.1 ∧ t.2 ≤ c.2
⊢ (ofLex t).1 ≤ (ofLex c).1

Tactic:
cases toLex_le_toLex.mp h with

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 α
a : α
b : β
c : α
h : a < c
⊢ toLex (a, b) < toLex (c, b)

Tactic:
simpa [lt_iff]

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 β
a : α
b c : β
h : b < c
⊢ toLex (a, b) < toLex (a, c)

Tactic:
simpa [lt_iff]

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ toFunAux (ofNat s 0) = 0

Tactic:
rw [toFunAux_eq, card_eq_zero, eq_empty_iff_forall_notMem]

Goal state after:
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ ∀ (x : ℕ), x ∉ {y ∈ range ↑(ofNat s 0) | y ∈ s}
Module: Mathlib.Data.Finset.Option

Goal state before:
pp: α : Type u_1
s : Finset α
p : Option α → Prop
⊢ (∀ a ∈ insertNone s, p a) ↔ p none ∧ ∀ a ∈ s, p (some a)

Tactic:
by simp [Option.forall]

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

Goal state before:
pp: P : Type u → Prop
of_equiv : ∀ {α β : Type u} (a : α ≃ β), P α → P β
h_empty : P PEmpty.{u + 1}
h_option : ∀ {α : Type u} [Fintype α], P α → P (Option α)
α : Type u
inst✝ : Finite α
⊢ P α

Tactic:
cases nonempty_fintype α
  refine Fintype.induction_empty_option ?_ ?_ ?_ α
  exacts [fun α β _ => of_equiv, h_empty, @h_option]

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

Goal state before:
pp: case cons
α : Type u_2
ι : Type u_5
inst✝ : LinearOrder α
s✝ : Finset ι
H : s✝.Nonempty
f : ι → α
c : ι
s : Finset ι
hcs : c ∉ s
hs : s.Nonempty
ih : ∃ i ∈ s, s.sup' hs f = f i
⊢ ∃ i ∈ cons c s hcs, (cons c s hcs).sup' ⋯ f = f i

Tactic:
rcases ih with ⟨b, hb, h'⟩
    rw [sup'_cons hs, h']
    cases le_total (f b) (f c) with
    | inl h => exact ⟨c, mem_cons.2 (Or.inl rfl), sup_eq_left.2 h⟩
    | inr h => exact ⟨b, mem_cons.2 (Or.inr hb), sup_eq_right.2 h⟩

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

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

Tactic:
rw [h.csSup_eq_max']

Goal state after:
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Finset α
h : s.Nonempty
⊢ s.max' h ∈ s
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
ι : Sort u_1
inst✝ : Subsingleton ι
s : ι → Set α
⊢ (∀ (i : PLift ι), (s i.down).Finite) ∧ {i | (s i.down).Nonempty}.Finite ↔ ∀ (i : ι), (s i).Finite

Tactic:
simp [PLift.forall, Finite.of_subsingleton]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)
h : ∀ ⦃i : ι⦄ ⦃a : α i⦄ ⦃b : β i⦄, f a b ⊆ g a b
a : (i : ι) × α i
b : (i : ι) × β i
⊢ sigmaLift f a b ⊆ sigmaLift g a b

Tactic:
rintro x hx
  rw [mem_sigmaLift] at hx ⊢
  obtain ⟨ha, hb, hx⟩ := hx
  exact ⟨ha, hb, h hx⟩

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a : α
⊢ (Finset.Ico a a).val = 0

Tactic:
Finset.Ico_self,

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a : α
⊢ ∅.val = 0
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
⊢ sInf s = k + 1 ↔ k + 1 ∈ s ∧ k ∉ s

Tactic:
classical
  constructor
  · intro H
    rw [eq_Ici_of_nonempty_of_upward_closed (nonempty_of_sInf_eq_succ _) hs, H, mem_Ici, mem_Ici]
    · exact ⟨le_rfl, k.not_succ_le_self⟩
    · exact k
    · assumption
  · rintro ⟨H, H'⟩
    rw [sInf_def (⟨_, H⟩ : s.Nonempty), find_eq_iff]
    exact ⟨H, fun n hnk hns ↦ H' <| hs n k (Nat.lt_succ_iff.mp hnk) hns⟩

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

Goal state before:
pp: case inr.mpr.inl.refine_2
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ n % a + a * (n / a) + a ≤ n + a

Tactic:
hn

Goal state after:
case inr.mpr.inl.refine_2
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ n + a ≤ n + a
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: case succ
n✝ : ℕ
⊢ image (fun j ↦ n✝ + 1 - 1 - j) (range (n✝ + 1)) = range (n✝ + 1)

Tactic:
Finset.range_eq_Ico,

Goal state after:
case succ
n✝ : ℕ
⊢ image (fun j ↦ n✝ + 1 - 1 - j) (Ico 0 (n✝ + 1)) = Ico 0 (n✝ + 1)
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a b : ℕ
⊢ range (a + b) = range a ∪ map (addLeftEmbedding a) (range b)

Tactic:
Finset.range_eq_Ico,

Goal state after:
a b : ℕ
⊢ Ico 0 (a + b) = Ico 0 a ∪ map (addLeftEmbedding a) (Ico 0 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
⊢ map (Embedding.subtype p) (Ico a b) = Ico ↑a ↑b

Tactic:
subtype_Ico_eq

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
⊢ map (Embedding.subtype p) (Finset.subtype p (Ico ↑a ↑b)) = Ico ↑a ↑b
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
s : Set α
h : s.IsPWO
⊢ s.IsWF

Tactic:
simpa only [← lt_iff_le_not_ge] using! h.wellFoundedOn

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case inr
α : 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 ≠ []
⊢ False

Tactic:
obtain ⟨g, hg⟩ := h.exists_monotone_subseq fun n => hf1.1 n _ (List.head!_mem_self (hnil n))

Goal state after:
case inr
α : 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!
⊢ False
Module: Mathlib.GroupTheory.Submonoid.Centralizer

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
s : Set M
⊢ ↑(centralizer s.centralizer.centralizer) = ↑(centralizer s)

Tactic:
simp only [coe_centralizer, Set.centralizer_centralizer_centralizer]

Goal state after:
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
inst✝ : DivisionMonoid M
a : M
ha : a ∈ center M
g✝ : M
⊢ g✝ * a⁻¹ = a⁻¹ * g✝

Tactic:
← inv_inj,

Goal state after:
M : Type u_1
inst✝ : DivisionMonoid M
a : M
ha : a ∈ center M
g✝ : M
⊢ (g✝ * a⁻¹)⁻¹ = (a⁻¹ * g✝)⁻¹
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
s : Finset M
⊢ s.val.prod = s.prod id

Tactic:
by
  rw [Finset.prod, Multiset.map_id]

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
Hs : Set (Subgroup G)
h : ∀ H ∈ Hs, H.Normal
⊢ (sSup Hs).Normal

Tactic:
rw [sSup_eq_iSup]
  exact biSup_normal Hs id h

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
P H : Subgroup G
hP : P ≤ H
h : ↥H
g : G
hg : g ∈ ↑P
⊢ ((MulDistribMulAction.toMonoidEnd (MulAut G) G) (MulAut.conj ↑h)) g ∈ H

Tactic:
exact H.mul_mem (H.mul_mem h.2 (hP hg)) (H.inv_mem h.2)

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H : Subgroup G
h : G
hh : h ∈ H
⊢ {h} * ↑H = ↑H

Tactic:
by
  simp [preimage, mul_mem_cancel_left (inv_mem hh)]

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

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

Tactic:
hn

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

Goal state before:
pp: case convert_8.h
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ ∀ x_1 ∈ univ.erase i, Pi.mulSingle x_1 (x x_1) i = 1

Tactic:
· simpa using fun _ a ↦ Pi.mulSingle_eq_of_ne (a ·.symm) _

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

Goal state before:
pp: ι : Type u_2
γ : Type u_5
inst✝³ : Monoid γ
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
f g : ((i : ι) → M i) →* γ
h : ∀ (i : ι) (x : M i), f (Pi.mulSingle i x) = g (Pi.mulSingle i x)
⊢ f = g

Tactic:
by
  cases nonempty_fintype ι
  ext x
  rw [← noncommProd_mulSingle x, univ.map_noncommProd, univ.map_noncommProd]
  congr 1 with i; exact h i (x i)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : Setoid α
s : Setoid β
q : Quotient r × Quotient s
⊢ (fun q ↦ q.liftOn' (fun xy ↦ (Quotient.mk'' xy.1, Quotient.mk'' xy.2)) ⋯)
      ((fun x ↦
          match x with
          | (x, y) => Quotient.map₂ Prod.mk ⋯ x y)
        q) =
    q

Tactic:
by
    rcases q with ⟨qa, qb⟩
    induction qa, qb using Quotient.inductionOn₂'
    rfl

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

Goal state before:
pp: α : Type u
L : List (α × Bool)
x : α
b : Bool
h : Red ((x, b) :: L) []
h₁ : Red ((x, !b) :: (x, b) :: L) [(x, !b)]
⊢ Red L [(x, !b)]

Tactic:
have h₂ : Red ((x, not b) :: (x, b) :: L) L := ReflTransGen.single Step.cons_not_rev

Goal state after:
α : Type u
L : List (α × Bool)
x : α
b : Bool
h : Red ((x, b) :: L) []
h₁ : Red ((x, !b) :: (x, b) :: L) [(x, !b)]
h₂ : Red ((x, !b) :: (x, b) :: L) L
⊢ Red L [(x, !b)]
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
f : ι → M
inst✝ : DecidableEq ι
s : Finset κ
t : κ → Finset ι
hs : (↑s).PairwiseDisjoint t
⊢ ∏ x ∈ s.biUnion t, f x = ∏ x ∈ s, ∏ i ∈ t x, f i

Tactic:
rw [← disjiUnion_eq_biUnion _ _ hs, prod_disjiUnion]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Group β
f : α → β
s : Subgroup β
H : Set.range f ⊆ ↑s
w✝ : FreeGroup α
L : List (α × Bool)
x✝ : α × Bool
tl : List (α × Bool)
ih : (lift f) (Quot.mk Red.Step tl) ∈ s
x : α
b : Bool
⊢ (lift f) (Quot.mk Red.Step ((x, false) :: tl)) ∈ s

Tactic:
simpa using s.mul_mem (s.inv_mem <| H ⟨x, rfl⟩) ih

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
P : Submonoid M
Q : Submonoid N
hP : P.FG
hQ : Q.FG
⊢ (P.prod Q).FG

Tactic:
classical
  obtain ⟨bM, hbM⟩ := hP
  obtain ⟨bN, hbN⟩ := hQ
  refine ⟨bM ×ˢ singleton 1 ∪ singleton 1 ×ˢ bN, ?_⟩
  push_cast
  simp [closure_union, hbM, hbN]

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
M' : Type u_3
inst✝ : Monoid M'
P : Submonoid M
h : P.FG
e : M →* M'
⊢ (Submonoid.map e P).FG

Tactic:
obtain ⟨s, rfl⟩ := h

Goal state after:
M : Type u_1
inst✝¹ : Monoid M
M' : Type u_3
inst✝ : Monoid M'
e : M →* M'
s : Finset M
⊢ (Submonoid.map e (closure ↑s)).FG
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
inst✝ : DecidableEq ι
s : Multiset ι
⊢ ∑ a ∈ s.toFinset, count a s = s.card

Tactic:
by
  simpa using (Finset.sum_multiset_map_count s (fun _ => (1 : ℕ))).symm

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β : Type v
γ : Type w
T : Type u_2
inst✝ : Unique T
n : ℤ
⊢ n • 1 = n

Tactic:
exact zsmul_one n

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

Goal state before:
pp: case refine_1
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
a b c : M × ↥S
t₁ : ↥S
ht₁ : ↑t₁ * (↑b.2 * a.1) = ↑t₁ * (↑a.2 * b.1)
t₂ : ↥S
ht₂ : ↑t₂ * (↑c.2 * b.1) = ↑t₂ * (↑b.2 * c.1)
⊢ ∃ c_1, ↑c_1 * (↑c.2 * a.1) = ↑c_1 * (↑a.2 * c.1)

Tactic:
use t₂ * t₁ * b.2

Goal state after:
case h
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
a b c : M × ↥S
t₁ : ↥S
ht₁ : ↑t₁ * (↑b.2 * a.1) = ↑t₁ * (↑a.2 * b.1)
t₂ : ↥S
ht₂ : ↑t₂ * (↑c.2 * b.1) = ↑t₂ * (↑b.2 * c.1)
⊢ ↑(t₂ * t₁ * b.2) * (↑c.2 * a.1) = ↑(t₂ * t₁ * b.2) * (↑a.2 * c.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_2
inst✝ : MulAction R X
r₁ : R
r₂ : X
s₁ s₂ u : ↥S
v : R
huv : ↑u * r₁ = v * ↑s₂
v₀ : R := oreNum r₁ s₂
u₀ : ↥S := oreDenom r₁ s₂
h₀ : ↑u₀ * r₁ = v₀ * ↑s₂
r₃ : R
s₃ : ↥S
h₃ : ↑s₃ * ↑u₀ = r₃ * ↑u
⊢ r₃ * v * ↑s₂ = r₃ * (↑u * r₁)

Tactic:
by rw [mul_assoc, ← huv]

Goal state after:
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 : M →* N
h : ∀ (y : ↥S), IsUnit (f ↑y)
x₁ x₂ : M
y₁ y₂ : ↥S
⊢ f x₁ * f ↑y₂ = f ↑y₁ * f x₂ ↔ f (x₁ * ↑y₂) = f (x₂ * ↑y₁)

Tactic:
mul_comm x₂,

Goal state after:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : M →* N
h : ∀ (y : ↥S), IsUnit (f ↑y)
x₁ x₂ : M
y₁ y₂ : ↥S
⊢ f x₁ * f ↑y₂ = f ↑y₁ * f x₂ ↔ f (x₁ * ↑y₂) = f (↑y₁ * x₂)
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 y : M
c : ↥S
h : f (↑c * x) = f (↑c * y)
⊢ f x = f y

Tactic:
rw [map_mul, map_mul] at h
  let ⟨u, hu⟩ := f.map_units c
  rw [← hu] at h
  exact (Units.mul_right_inj u).1 h

Goal state after:
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 x₁ = f (x₂ * ↑y₁) * ↑((IsUnit.liftRight (f.toMonoidHom.domRestrict S) ⋯) y₂)⁻¹

Tactic:
mul_comm x₂,

Goal state after:
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 x₁ = f (↑y₁ * x₂) * ↑((IsUnit.liftRight (f.toMonoidHom.domRestrict S) ⋯) y₂)⁻¹
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 * (↑(fS s * (fS s)⁻¹) * f r))

Tactic:
rw [Units.val_mul, mul_assoc, ← mul_assoc _ (fS s : T), ← this, ← mul_assoc]

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⟩)⁻¹ * ↑(fS ⟨t * ↑s, ht⟩) * (↑(fS s)⁻¹ * f r)
Module: Mathlib.Algebra.Ring.Equiv

Goal state before:
pp: α : Type u_2
β : Type u_3
R : Type u_7
inst✝ : NonUnitalNonAssocSemiring R
e : α ≃ β
⊢ (piCongrLeft' (fun x ↦ R) e).symm = piCongrLeft' (fun i ↦ R) e.symm

Tactic:
by
  simp only [piCongrLeft', RingEquiv.symm, MulEquiv.symm, Equiv.piCongrLeft'_symm]

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

Goal state before:
pp: case top
α : Type u_1
β : Type u_2
inst✝⁴ : Add α
inst✝³ : LE α
inst✝² : OrderBot α
inst✝¹ : Sub α
inst✝ : OrderedSub α
x z : WithTop α
⊢ x - ⊤ ≤ z ↔ x ≤ z + ⊤

Tactic:
cases z <;> simp

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
⊢ (∀ ⦃a₁ a₂ : M⦄, (∃ c, ↑c * a₁ = ↑c * a₂) → a₁ = a₂) ↔ ∀ ⦃x : M⦄, x ∈ S → ∀ ⦃a₁ a₂ : M⦄, x * a₁ = x * a₂ → a₁ = a₂

Tactic:
exists_imp,

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : CommMonoid N
f : S.LocalizationMap N
⊢ (∀ ⦃a₁ a₂ : M⦄ (x : ↥S), ↑x * a₁ = ↑x * a₂ → a₁ = a₂) ↔ ∀ ⦃x : M⦄, x ∈ S → ∀ ⦃a₁ a₂ : M⦄, x * a₁ = x * a₂ → a₁ = a₂
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝⁶ : DecidableEq α
R : Type u_2
S : Type u_3
inst✝⁵ : MulZeroOneClass R
inst✝⁴ : DecidableEq R
inst✝³ : Nontrivial R
inst✝² : MulZeroOneClass S
inst✝¹ : DecidableEq S
inst✝ : Nontrivial S
f : R →*₀ S
hf : Function.Injective ⇑f
x y : WithTop R
this : ∀ (z : WithTop R), map (⇑f) z = 0 ↔ z = 0
hx : x ≠ 0
hy : y ≠ 0
⊢ map (⇑f) (x * y) = map (⇑f) x * map (⇑f) y

Tactic:
cases x with | top => simp [hy, this] | coe x => ?_

Goal state after:
case inr.inr.coe
α : Type u_1
inst✝⁶ : DecidableEq α
R : Type u_2
S : Type u_3
inst✝⁵ : MulZeroOneClass R
inst✝⁴ : DecidableEq R
inst✝³ : Nontrivial R
inst✝² : MulZeroOneClass S
inst✝¹ : DecidableEq S
inst✝ : Nontrivial S
f : R →*₀ S
hf : Function.Injective ⇑f
y : WithTop R
this : ∀ (z : WithTop R), map (⇑f) z = 0 ↔ z = 0
hy : y ≠ 0
x : R
hx : ↑x ≠ 0
⊢ map (⇑f) (↑x * y) = map ⇑f ↑x * map (⇑f) y
Module: Mathlib.Algebra.Order.Ring.WithTop

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

Tactic:
lift x to α

Goal state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulMono α
x : WithBot α
x0 : 0 ≤ x
a b : WithBot α
h : a ≤ b
x0' : x ≠ 0
⊢ x ≠ ⊥

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

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

Tactic:
lift x to α

Goal state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosMono α
x : WithBot α
x0 : 0 ≤ x
a b : WithBot α
h : a ≤ b
x0' : x ≠ 0
⊢ x ≠ ⊥

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

Goal state before:
pp: case inr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLT α
x : WithBot α
x0 : 0 ≤ x
a b : WithBot α
h : x * a < x * b
x0' : x ≠ 0
⊢ a < b

Tactic:
lift x to α

Goal state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLT α
x : WithBot α
x0 : 0 ≤ x
a b : WithBot α
h : x * a < x * b
x0' : x ≠ 0
⊢ x ≠ ⊥

case inr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLT α
a b : WithBot α
x : α
x0 : 0 ≤ ↑x
h : ↑x * a < ↑x * b
x0' : ↑x ≠ 0
⊢ a < b
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case inr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLT α
x : WithBot α
x0 : 0 ≤ x
a b : WithBot α
h : a * x < b * x
x0' : x ≠ 0
⊢ a < b

Tactic:
lift x to α

Goal state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLT α
x : WithBot α
x0 : 0 ≤ x
a b : WithBot α
h : a * x < b * x
x0' : x ≠ 0
⊢ x ≠ ⊥

case inr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLT α
a b : WithBot α
x : α
x0 : 0 ≤ ↑x
h : a * ↑x < b * ↑x
x0' : ↑x ≠ 0
⊢ a < b
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
a : α
inst✝ : LinearOrder α
⊢ IsLUB (Iio a) a ↔ IsSuccPrelimit a

Tactic:
refine ⟨fun ha b hb ↦ ?_, IsSuccPrelimit.isLUB_Iio⟩

Goal state after:
α : Type u_1
a : α
inst✝ : LinearOrder α
ha : IsLUB (Iio a) a
b : α
hb : b ⋖ a
⊢ False
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: case inr.inl
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
h : WellFoundedLT α
inst✝ : PredOrder α
a b✝ b : α
ih : ∀ y < b, a ≤ y → ∃ n, pred^[n] y = a
hab : a < b
hb : pred b = b
⊢ ∃ n, pred^[n] b = a

pp: case inr.inr
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
h : WellFoundedLT α
inst✝ : PredOrder α
a b✝ b : α
ih : ∀ y < b, a ≤ y → ∃ n, pred^[n] y = a
hab : a < b
hb : pred b < b
⊢ ∃ n, pred^[n] b = a

Tactic:
· cases (min_of_le_pred hb.ge).not_lt hab

Goal state after:
case inr.inr
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
h : WellFoundedLT α
inst✝ : PredOrder α
a b✝ b : α
ih : ∀ y < b, a ≤ y → ∃ n, pred^[n] y = a
hab : a < b
hb : pred b < b
⊢ ∃ n, pred^[n] b = a
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 : m ∈ upperBounds S → n ∈ S → m ∉ S → ∃ x, IsGreatest S x
hm : succ m ∈ upperBounds S
⊢ n ∈ S → succ m ∉ S → ∃ x, IsGreatest S x

Tactic:
hn

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 : m ∈ upperBounds S → n ∈ S → m ∉ S → ∃ x, IsGreatest S x
hm : succ m ∈ upperBounds S
hn : n ∈ S
⊢ succ m ∉ S → ∃ x, IsGreatest S x