mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Set.Pairwise.Lattice

Goal state before:
pp: α : Type u_1
ι : Type u_2
f : ι → Set α
s : Set ι
y : α
h_disjoint : s.PairwiseDisjoint f
hy : y ∈ ⋃ i ∈ s, f i
⊢ ∃! i, i ∈ s ∧ y ∈ f i

Tactic:
refine existsUnique_of_exists_of_unique ?ex ?unique

Goal state after:
case ex
α : Type u_1
ι : Type u_2
f : ι → Set α
s : Set ι
y : α
h_disjoint : s.PairwiseDisjoint f
hy : y ∈ ⋃ i ∈ s, f i
⊢ ∃ x ∈ s, y ∈ f x

case unique
α : Type u_1
ι : Type u_2
f : ι → Set α
s : Set ι
y : α
h_disjoint : s.PairwiseDisjoint f
hy : y ∈ ⋃ i ∈ s, f i
⊢ ∀ (y₁ y₂ : ι), y₁ ∈ s ∧ y ∈ f y₁ → y₂ ∈ s ∧ y ∈ f y₂ → y₁ = y₂
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: ι : Type u_5
α : Type u_7
inst✝² : LinearOrder α
inst✝¹ : BoundedOrder α
inst✝ : Nontrivial α
s : Finset ι
f : ι → α
⊢ s.sup f = ⊤ ↔ ∃ b ∈ s, f b = ⊤

Tactic:
simp only [← top_le_iff]
  exact Finset.le_sup_iff bot_lt_top

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : ConditionallyCompletePartialOrderSup α
inst✝ : Preorder β
f : β → α
a : β
hf : Monotone f
⊢ ⨆ x, f ↑x = f a

Tactic:
have hd : Directed (· ≤ ·) (fun x : Iic a ↦ f x) := fun x y ↦ ⟨⟨a, le_refl a⟩, ⟨hf x.2, hf y.2⟩⟩
  have H : BddAbove (range fun x : Iic a ↦ f x) := ⟨f a, fun _ ↦ by aesop⟩
  apply (hd.le_ciSup H (⟨a, le_refl a⟩ : Iic a)).antisymm'
  rw [hd.ciSup_le_iff H]
  rintro ⟨a, h⟩
  exact hf h

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
hf : BddAbove (range f)
h✝ : Nonempty β
⊢ ⨆ p, f p = ⨆ b, ⨆ c, f (b, c)

Tactic:
rcases isEmpty_or_nonempty γ

Goal state after:
case inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
hf : BddAbove (range f)
h✝¹ : Nonempty β
h✝ : IsEmpty γ
⊢ ⨆ p, f p = ⨆ b, ⨆ c, f (b, c)

case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
hf : BddAbove (range f)
h✝¹ : Nonempty β
h✝ : Nonempty γ
⊢ ⨆ p, f p = ⨆ b, ⨆ c, f (b, c)
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case inr
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
gt : iSup f < sSup ∅
i : ι
hi : ¬p i
this : Nonempty ι
bdd : BddAbove (range f)
⊢ ⨆ i, ⨆ (h : p i), f ⟨i, h⟩ = max (iSup f) (sSup ∅)

Tactic:
max_eq_right gt.le

Goal state after:
case inr
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
gt : iSup f < sSup ∅
i : ι
hi : ¬p i
this : Nonempty ι
bdd : BddAbove (range f)
⊢ ⨆ i, ⨆ (h : p i), f ⟨i, h⟩ = sSup ∅
Module: Mathlib.Order.CompleteLattice.Finset

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
P : Finset α → Prop
s : Finset α
hP : ∀ ⦃s t : Finset α⦄, P t → s ⊆ t → P s
⊢ Maximal P s ↔ P s ∧ ∀ x ∉ s, ¬P (insert x s)

Tactic:
by
  simp only [Maximal, and_congr_right_iff]
  exact fun _ ↦ ⟨fun h x hxs hx ↦ hxs <| h hx (subset_insert _ _) (mem_insert_self x s),
    fun h t ht hst x hxt ↦ by_contra fun hxs ↦ h x hxs (hP ht (insert_subset hxt hst))⟩

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: case top
α : Type u_1
inst✝ : Preorder α
⊢ ⊤ ⋖ ⊤ ↔ ∃ b, IsMax b ∧ ⊤ = ↑b

Tactic:
| top =>

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
b x : α
⊢ x ∈ Iic b ↔ x ≤ b

Tactic:
by rw [Iic, ← Finset.mem_def, Finset.mem_Iic]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h : ∀ (a b : α), (Set.Icc a b).Finite
a b x : α
⊢ x ∈ ⋯.toFinset ↔ a ≤ x ∧ x ≤ b

Tactic:
Set.Finite.mem_toFinset,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h : ∀ (a b : α), (Set.Icc a b).Finite
a b x : α
⊢ x ∈ Set.Icc a b ↔ a ≤ x ∧ x ≤ b
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: case inl
n : ℕ
⊢ image (fun x ↦ x % 0) (Ico n (n + 0)) = range 0

Tactic:
rw [range_zero, add_zero, Ico_self, image_empty]

Goal state after:
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: case inl.zero
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : ℕ → α
g : ℕ ↪o ℕ
hr : ∀ (n : ℕ), r (f (g n)) (f (g (n + 1)))
m : ℕ
mn : m < m.succ + 0
⊢ r (f (g m)) (f (g (m.succ + 0)))

Tactic:
apply hr

Goal state after:
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_2
inst✝ : PartialOrder α
wfl : WellFoundedLT α
wfg : WellFoundedGT α
x y : α
h : x ≤ y
⊢ ∃ a, a 0 = x ∧ ∃ n, a n = y ∧ ∀ i < n, a i ⋖ a (i + 1)

Tactic:
let S := Set.Icc x y
  let hS : BoundedOrder S :=
    { top := ⟨y, h, le_rfl⟩, le_top x := x.2.2, bot := ⟨x, le_rfl, h⟩, bot_le x := x.2.1 }
  obtain ⟨a, h₁, n, h₂, e⟩ := exists_covBy_seq_of_wellFoundedLT_wellFoundedGT S
  simp only [isMin_iff_eq_bot, Subtype.ext_iff, isMax_iff_eq_top] at h₁ h₂
  exact ⟨Subtype.val ∘ a, h₁, n, h₂, fun i hi ↦ ⟨(e i hi).1, fun c hc h ↦ (e i hi).2
    (c := ⟨c, (a i).2.1.trans hc.le, h.le.trans (a _).2.2⟩) hc h⟩⟩

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: α : Type u_3
β : Type u_4
r : α → α → Prop
s : β → β → Prop
h : WellQuasiOrdered r
f : r →r s
hf : Function.Surjective ⇑f
seq : ℕ → β
w✝¹ w✝ : ℕ
hle : w✝¹ < w✝
hr : r ((Function.surjInv hf ∘ seq) w✝¹) ((Function.surjInv hf ∘ seq) w✝)
⊢ ∃ m n, m < n ∧ s (seq m) (seq n)

Tactic:
exact ⟨_, _, hle, by simpa [Function.surjInv_eq] using f.map_rel hr⟩

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case mpr
α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s : Set α
⊢ (∃ x, ∀ (n : ℕ), x n ∈ s) → Nonempty ((fun x1 x2 ↦ x1 > x2) ↪r fun a b ↦ r a b ∧ a ∈ s ∧ b ∈ s)

Tactic:
· rintro ⟨⟨f, hf⟩, hfs : ∀ n, f n ∈ s⟩
    refine ⟨⟨f, ?_⟩⟩
    simpa only [hfs, and_true] using @hf

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
y : α
F : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : Preorder M
inst✝³ : Preorder N
inst✝² : EquivLike F M N
inst✝¹ : OrderIsoClass F M N
f : F
inst✝ : LocallyFiniteOrder N
⊢ ∀ (a b x : M), x ∈ map { toFun := EquivLike.inv f, inj' := ⋯ } (finsetIco (f a) (f b)) ↔ a ≤ x ∧ x < b

Tactic:
simp [finset_mem_Ico, EquivLike.inv_apply_eq, map_lt_map_iff]

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

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

Tactic:
by
  classical rw [cons_eq_insert, Ioo_insert_right h]

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
g : G
⊢ centralizer {g} = comap toConjAct.toMonoidHom (stabilizer (ConjAct G) g)

Tactic:
ext k

Goal state after:
G : Type u_3
inst✝ : Group G
g k : G
⊢ k ∈ centralizer {g} ↔ k ∈ comap toConjAct.toMonoidHom (stabilizer (ConjAct G) g)
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝² : Group G
inst✝¹ : AddGroup A
s : Set G
ι : Sort u_5
H : ι → Subgroup G
inst✝ : ∀ (i : ι), (H i).Normal
⊢ ⊤ ≤ ⨅ i, normalizer ↑(H i)

Tactic:
simp [normalizer_eq_top]

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

Goal state before:
pp: case h
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
l : List M
comm : {x | x ∈ ⟦l⟧}.Pairwise Commute
h : ∀ x ∈ ⟦l⟧, x ∈ S
⊢ l.prod ∈ S

Tactic:
exact Submonoid.list_prod_mem _ h

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

Goal state before:
pp: case hbc.hab
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f g : α → β
comm_ff : (↑s).Pairwise (Commute on f)
comm_gg : (↑s).Pairwise (Commute on g)
comm_gf : (↑s).Pairwise fun x y ↦ Commute (g x) (f y)
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
h : x ≠ y
⊢ Commute (g x) (f y)

Tactic:
exact comm_gf hx hy h

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:
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
r : α → α → Prop
⊢ Subsingleton (Quot r) ↔ Relation.EqvGen r = ⊤

Tactic:
by
  simp only [_root_.subsingleton_iff, _root_.eq_top_iff, Pi.le_def, Pi.top_apply]
  refine Quot.mk_surjective.forall.trans (forall_congr' fun a => ?_)
  refine Quot.mk_surjective.forall.trans (forall_congr' fun b => ?_)
  rw [Quot.eq]
  simp

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

Goal state before:
pp: case false
α : Type u
L₁ L₂ : List (α × Bool)
x : α
⊢ Step (L₁ ++ (x, !false) :: (x, false) :: L₂) (L₁ ++ L₂)

Tactic:
exact Step.not

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

Goal state before:
pp: case true
α : Type u
L₁ L₂ : List (α × Bool)
x : α
⊢ Step (L₁ ++ (x, !true) :: (x, true) :: L₂) (L₁ ++ L₂)

Tactic:
exact Step.not

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

Goal state before:
pp: case head.inr
α : Type u
LL₁ c✝ L₂ : List (α × Bool)
a : α
b : Bool
h : ReflTransGen Step c✝ ((a, b) :: L₂)
ih : ∀ {L₁ L₂_1 : List (α × Bool)}, (a, b) :: L₁ = c✝ → (a, b) :: L₂_1 = (a, b) :: L₂ → Red L₁ L₂_1
⊢ Red ((a, !b) :: c✝) L₂

Tactic:
exact (cons_cons h).tail Step.cons_not_rev

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

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
F : Type ?u.18
inst✝⁴ : Mul M
inst✝³ : Mul N
inst✝² : Mul P
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
c : Con M
f : F
h : ker f ≤ c
hf : Surjective ⇑f
w✝ x✝ y✝ z✝ : N
h₁ : (c.mapOfSurjective (⇑f) h hf) w✝ x✝
h₂ : (c.mapOfSurjective (⇑f) h hf) y✝ z✝
⊢ (c.mapOfSurjective (⇑f) h hf) (w✝ * y✝) (x✝ * z✝)

Tactic:
by
    rcases h₁ with ⟨a, b, h1, rfl, rfl⟩
    rcases h₂ with ⟨p, q, h2, rfl, rfl⟩
    exact ⟨a * p, b * q, c.mul h1 h2, map_mul f _ _, map_mul f _ _⟩

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
c : Con M
f : N →* M
x y : N
⊢ c (f x) (f y) ↔ c.mk' (f x) = c.mk' (f y)

Tactic:
rw [← c.eq]; rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
g : α
⊢ Quotient.out ↑g = g * ↑⟨g⁻¹ * Quotient.out ↑g, ⋯⟩

Tactic:
by rw [mul_inv_cancel_left]

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

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α✝ β✝ γ✝ : Type u
x : FreeGroup α✝
⊢ ∀ (f : α✝ → FreeGroup β✝) (g : β✝ → FreeGroup γ✝), x >>= f >>= g = x >>= fun x ↦ f x >>= g

Tactic:
refine FreeGroup.induction_on x ?_ ?_ ?_ ?_

Goal state after:
case refine_1
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α✝ β✝ γ✝ : Type u
x : FreeGroup α✝
⊢ ∀ (f : α✝ → FreeGroup β✝) (g : β✝ → FreeGroup γ✝), 1 >>= f >>= g = 1 >>= fun x ↦ f x >>= g

case refine_2
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α✝ β✝ γ✝ : Type u
x : FreeGroup α✝
⊢ ∀ (x : α✝) (f : α✝ → FreeGroup β✝) (g : β✝ → FreeGroup γ✝), of x >>= f >>= g = of x >>= fun x ↦ f x >>= g

case refine_3
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α✝ β✝ γ✝ : Type u
x : FreeGroup α✝
⊢ ∀ (x : α✝),
    (∀ (f : α✝ → FreeGroup β✝) (g : β✝ → FreeGroup γ✝), of x >>= f >>= g = of x >>= fun x ↦ f x >>= g) →
      ∀ (f : α✝ → FreeGroup β✝) (g : β✝ → FreeGroup γ✝), (of x)⁻¹ >>= f >>= g = (of x)⁻¹ >>= fun x ↦ f x >>= g

case refine_4
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α✝ β✝ γ✝ : Type u
x : FreeGroup α✝
⊢ ∀ (x y : FreeGroup α✝),
    (∀ (f : α✝ → FreeGroup β✝) (g : β✝ → FreeGroup γ✝), x >>= f >>= g = x >>= fun x ↦ f x >>= g) →
      (∀ (f : α✝ → FreeGroup β✝) (g : β✝ → FreeGroup γ✝), y >>= f >>= g = y >>= fun x ↦ f x >>= g) →
        ∀ (f : α✝ → FreeGroup β✝) (g : β✝ → FreeGroup γ✝), x * y >>= f >>= g = x * y >>= fun x ↦ f x >>= g
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α✝ β✝ : Type u
f : α✝ → β✝
x : FreeGroup α✝
⊢ (do
      let y ← x
      pure (f y)) =
    f <$> x

Tactic:
refine FreeGroup.induction_on x ?_ ?_ ?_ ?_

Goal state after:
case refine_1
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α✝ β✝ : Type u
f : α✝ → β✝
x : FreeGroup α✝
⊢ (do
      let y ← 1
      pure (f y)) =
    f <$> 1

case refine_2
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α✝ β✝ : Type u
f : α✝ → β✝
x : FreeGroup α✝
⊢ ∀ (x : α✝),
    (do
        let y ← of x
        pure (f y)) =
      f <$> of x

case refine_3
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α✝ β✝ : Type u
f : α✝ → β✝
x : FreeGroup α✝
⊢ ∀ (x : α✝),
    (do
          let y ← of x
          pure (f y)) =
        f <$> of x →
      (do
          let y ← (of x)⁻¹
          pure (f y)) =
        f <$> (of x)⁻¹

case refine_4
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α✝ β✝ : Type u
f : α✝ → β✝
x : FreeGroup α✝
⊢ ∀ (x y : FreeGroup α✝),
    (do
          let y ← x
          pure (f y)) =
        f <$> x →
      (do
            let y ← y
            pure (f y)) =
          f <$> y →
        (do
            let y ← x * y
            pure (f y)) =
          f <$> (x * y)
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case h
M : Type u_1
inst✝¹ : Monoid M
M' : Type u_3
inst✝ : Monoid M'
P : Submonoid M
e : M →* M'
he : Function.Injective ⇑e
s : Finset M'
hs : closure ↑s = Submonoid.map e P
⊢ Submonoid.map e (closure ↑(s.preimage ⇑e ⋯)) = Submonoid.map e P

Tactic:
rw [← hs, MonoidHom.map_mclosure e, Finset.coe_preimage]

Goal state after:
case h
M : Type u_1
inst✝¹ : Monoid M
M' : Type u_3
inst✝ : Monoid M'
P : Submonoid M
e : M →* M'
he : Function.Injective ⇑e
s : Finset M'
hs : closure ↑s = Submonoid.map e P
⊢ closure (⇑e '' ⇑e ⁻¹' ↑s) = closure ↑s
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
x : α
h : of x = 0
f : FreeAbelianGroup α →+ ℤ := lift 1
⊢ False

Tactic:
have hfx : f (of x) = 1 := lift_apply_of _ _

Goal state after:
α : Type u
x : α
h : of x = 0
f : FreeAbelianGroup α →+ ℤ := lift 1
hfx : f (of x) = 1
⊢ False
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✝ n : ℕ
a✝ : n < n✝
h₁ : f n ≤ f (n + 1)
h₂ : f 0 ≤ f n
⊢ f (n + 1) - f 0 = f n - f 0 + (f (n + 1) - f n)

Tactic:
rw [tsub_add_eq_add_tsub h₂, add_tsub_cancel_of_le h₁]

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
z : FreeAbelianGroup T
⊢ (fun n ↦ n • of default) ((lift fun x ↦ 1) 0) = 0

Tactic:
by simp only [zero_smul, map_zero]

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
P : Type u_3
inst✝ : CommMonoid P
⊢ Con (M × ↥S)

Tactic:
by
  -- note we multiply by `c` on the left so that we can later generalize to `•`
  refine
    { r := fun a b : M × S ↦ ∃ c : S, ↑c * (↑b.2 * a.1) = c * (a.2 * b.1)
      iseqv := ⟨fun a ↦ ⟨1, rfl⟩, fun ⟨c, hc⟩ ↦ ⟨c, hc.symm⟩, ?_⟩
      mul' := ?_ }
  · rintro a b c ⟨t₁, ht₁⟩ ⟨t₂, ht₂⟩
    use t₂ * t₁ * b.2
    simp only [Submonoid.coe_mul]
    calc
      (t₂ * t₁ * b.2 : M) * (c.2 * a.1) = t₂ * c.2 * (t₁ * (b.2 * a.1)) := by ac_rfl
      _ = t₁ * a.2 * (t₂ * (c.2 * b.1)) := by rw [ht₁]; ac_rfl
      _ = t₂ * t₁ * b.2 * (a.2 * c.1) := by rw [ht₂]; ac_rfl
  · rintro a b c d ⟨t₁, ht₁⟩ ⟨t₂, ht₂⟩
    use t₂ * t₁
    calc
      (t₂ * t₁ : M) * (b.2 * d.2 * (a.1 * c.1)) = t₂ * (d.2 * c.1) * (t₁ * (b.2 * a.1)) := by ac_rfl
      _ = (t₂ * t₁ : M) * (a.2 * c.2 * (b.1 * d.1)) := by rw [ht₁, ht₂]; ac_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_2
inst✝ : MulAction R X
r₁ : R
r₂ : X
s₁ s₂ u : ↥S
v : R
huv : ↑u * r₁ = v * ↑s₂
⊢ smul' r₁ s₁ r₂ s₂ = v • r₂ /ₒ (u * s₁)

Tactic:
simp only [smul']
  have h₀ := ore_eq r₁ s₂; set v₀ := oreNum r₁ s₂; set u₀ := oreDenom r₁ s₂
  rcases oreCondition (u₀ : R) u with ⟨r₃, s₃, h₃⟩
  have :=
    calc
      r₃ * v * s₂ = r₃ * (u * r₁) := by rw [mul_assoc, ← huv]
      _ = s₃ * (u₀ * r₁) := by rw [← mul_assoc, ← mul_assoc, h₃]
      _ = s₃ * v₀ * s₂ := by rw [mul_assoc, h₀]
  rcases ore_right_cancel _ _ _ this with ⟨s₄, hs₄⟩
  symm; rw [oreDiv_eq_iff]
  use s₄ * s₃
  use s₄ * r₃
  simp only [Submonoid.coe_mul, Submonoid.smul_def]
  constructor
  · rw [smul_smul, mul_assoc (c := v₀), ← hs₄]
    simp only [smul_smul, mul_assoc]
  · rw [← mul_assoc (b := (u₀ : R)), mul_assoc (c := (u₀ : R)), h₃]
    simp only [mul_assoc]

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 : M
y : ↥S
z : N
H : z * f ↑y = f x
⊢ z = f.mk' x y

Tactic:
rwa [mk', mul_inv_right]

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_2
inst✝ : MulAction R X
p : R
r : X
s : ↥S
⊢ (p /ₒ s) • (r /ₒ 1) = p • r /ₒ s

Tactic:
by
  simp [oreDiv_smul_char p r s 1 p 1 (by simp)]

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

Goal state before:
pp: case inr.inr.top
α : 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
hx : ⊤ ≠ 0
⊢ map (⇑f) (⊤ * y) = map ⇑f ⊤ * map (⇑f) y

Tactic:
| top =>

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

Goal state before:
pp: case inr.inr.coe.top
α : 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
this : ∀ (z : WithTop R), map (⇑f) z = 0 ↔ z = 0
x : R
hx : ↑x ≠ 0
hy : ⊤ ≠ 0
⊢ map (⇑f) (↑x * ⊤) = map ⇑f ↑x * map ⇑f ⊤

Tactic:
| top =>

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

Goal state before:
pp: case inr.inr.inr.top
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : SemigroupWithZero α
inst✝ : NoZeroDivisors α
b c : WithTop α
hb : b ≠ 0
hc : c ≠ 0
ha : ⊤ ≠ 0
⊢ ⊤ * b * c = ⊤ * (b * c)

Tactic:
| top =>

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

Goal state before:
pp: case inr.inr.inr.coe.top
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : SemigroupWithZero α
inst✝ : NoZeroDivisors α
c : WithTop α
hc : c ≠ 0
a : α
ha : ↑a ≠ 0
hb : ⊤ ≠ 0
⊢ ↑a * ⊤ * c = ↑a * (⊤ * c)

Tactic:
| top =>

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

Goal state before:
pp: case inr.inr.inr.coe.coe.top
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : SemigroupWithZero α
inst✝ : NoZeroDivisors α
a : α
ha : ↑a ≠ 0
b : α
hb : ↑b ≠ 0
hc : ⊤ ≠ 0
⊢ ↑a * ↑b * ⊤ = ↑a * (↑b * ⊤)

Tactic:
| top =>

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

Goal state before:
pp: case top
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
a b : WithTop α
⊢ ⊤ * (a + b) = ⊤ * a + ⊤ * b

Tactic:
| top =>

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

Goal state before:
pp: case top
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
a b : WithTop α
⊢ (a + b) * ⊤ = a * ⊤ + b * ⊤

Tactic:
| top =>

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

Goal state before:
pp: case top
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
⊢ IsSuccPrelimit ⊤ ↔ ⊤ = ⊤ ∨ ∃ y, ⊤ = ↑y ∧ IsSuccPrelimit y

Tactic:
| top =>

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

Goal state before:
pp: case top
α : Type u_1
inst✝² : Preorder α
inst✝¹ : Nonempty α
inst✝ : NoMaxOrder α
⊢ IsSuccLimit ⊤ ↔ ⊤ = ⊤ ∨ ∃ y, ⊤ = ↑y ∧ IsSuccLimit y

Tactic:
| top =>

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

Goal state before:
pp: case top
α : Type u_1
inst✝ : Preorder α
⊢ IsPredPrelimit ⊤ ↔ ⊤ = ⊤ ∨ ∃ y, ⊤ = ↑y ∧ IsPredLimit y

Tactic:
| top =>

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

Goal state before:
pp: case neg
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m : X
hm : m ∈ upperBounds S
n : X
hn : n ∈ S
hm' : m ∉ S
hn' : n ≤ m
⊢ ∃ x, IsGreatest S x

Tactic:
revert hn hm hm'

Goal state after:
case neg
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m n : X
hn' : n ≤ m
⊢ m ∈ upperBounds S → n ∈ S → m ∉ S → ∃ x, IsGreatest S x
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: case succ
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddMonoidWithOne α
inst✝ : SuccAddOrder α
x : α
n : ℕ
IH : succ^[n] x = x + ↑n
⊢ x + ↑n + 1 = x + (↑n + 1)

Tactic:
add_assoc

Goal state after:
case succ
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddMonoidWithOne α
inst✝ : SuccAddOrder α
x : α
n : ℕ
IH : succ^[n] x = x + ↑n
⊢ x + (↑n + 1) = x + (↑n + 1)
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case top
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
hα : Nonempty α
a✝ : PredOrder (WithTop α)
h : pred ⊤ = ⊤
⊢ False

Tactic:
| top =>

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
hα : Nonempty α
a✝ : PredOrder (WithTop α)
x✝ : WithTop α
h : pred ⊤ = x✝
⊢ False

Tactic:
cases h : pred (⊤ : WithTop α) with

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

Goal state before:
pp: case inr.inr.top
a b c d m n : ℕ∞
α : Type u_1
S : Type u_2
inst✝² : MulZeroOneClass S
inst✝¹ : DecidableEq S
inst✝ : Nontrivial S
f : ℕ →*₀ S
hf : Injective ⇑f
y : ℕ∞
this : ∀ (z : ℕ∞), map (⇑f) z = 0 ↔ z = 0
hy : y ≠ 0
hx : ⊤ ≠ 0
⊢ map (⇑f) (⊤ * y) = map ⇑f ⊤ * map (⇑f) y

Tactic:
| top =>

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

Goal state before:
pp: case inr.inr.coe.top
a b c d m n : ℕ∞
α : Type u_1
S : Type u_2
inst✝² : MulZeroOneClass S
inst✝¹ : DecidableEq S
inst✝ : Nontrivial S
f : ℕ →*₀ S
hf : Injective ⇑f
this : ∀ (z : ℕ∞), map (⇑f) z = 0 ↔ z = 0
x : ℕ
hx : ↑x ≠ 0
hy : ⊤ ≠ 0
⊢ map (⇑f) (↑x * ⊤) = map ⇑f ↑x * map ⇑f ⊤

Tactic:
| top =>

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Fintype α
u : Finset (α ⊕ β)
⊢ u.toLeft = univ ↔ map Function.Embedding.inl univ ⊆ u

Tactic:
by
  simp [map_inl_subset_iff_subset_toLeft]

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

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : Sym α n
⊢ ↑(filterNe a m).snd + ↑(replicate (↑(filterNe a m).fst) a) = ↑m

Tactic:
filterNe,

Goal state after:
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : Sym α n
⊢ ↑⟨⟨count a ↑m, ⋯⟩, ⟨filter (fun x ↦ a ≠ x) ↑m, ⋯⟩⟩.snd +
      ↑(replicate (↑⟨⟨count a ↑m, ⋯⟩, ⟨filter (fun x ↦ a ≠ x) ↑m, ⋯⟩⟩.fst) a) =
    ↑m
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : a ∉ m.snd
⊢ ↑(filterNe a (fill a m.fst m.snd)).snd = ↑m.snd

Tactic:
filterNe,

Goal state after:
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : a ∉ m.snd
⊢ ↑⟨⟨count a ↑(fill a m.fst m.snd), ⋯⟩, ⟨filter (fun x ↦ a ≠ x) ↑(fill a m.fst m.snd), ⋯⟩⟩.snd = ↑m.snd