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

Goal state before:
pp: case neg
α : 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)
j : ι
hj : ¬p j
⊢ ⨆ (h : p j), f ⟨j, h⟩ ≤ sSup ∅

Tactic:
exact (ciSup_neg hj).le

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : ConditionallyCompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set α
hne : s.Nonempty
hbdd : BddAbove s
⊢ l (sSup s) = sSup (l '' s)

Tactic:
gc.l_csSup hne hbdd,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : ConditionallyCompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set α
hne : s.Nonempty
hbdd : BddAbove s
⊢ ⨆ x, l ↑x = sSup (l '' s)
Module: Mathlib.Order.Cover

Goal state before:
pp: case mp
ι : Type u_3
α : ι → Type u_4
inst✝² : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst✝¹ : Nonempty ι
inst✝ : DecidableEq ι
⊢ (∃ i, a i ⩿ b i ∧ ∀ (j : ι), j ≠ i → a j = b j) → ∃ i x, a i ⩿ x ∧ b = Function.update a i x

pp: case mpr
ι : Type u_3
α : ι → Type u_4
inst✝² : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst✝¹ : Nonempty ι
inst✝ : DecidableEq ι
⊢ (∃ i x, a i ⩿ x ∧ b = Function.update a i x) → ∃ i, a i ⩿ b i ∧ ∀ (j : ι), j ≠ i → a j = b j

Tactic:
· rintro ⟨i, hi, h⟩
    exact ⟨i, b i, hi, by simpa [Function.eq_update_iff, eq_comm] using h⟩

Goal state after:
case mpr
ι : Type u_3
α : ι → Type u_4
inst✝² : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst✝¹ : Nonempty ι
inst✝ : DecidableEq ι
⊢ (∃ i x, a i ⩿ x ∧ b = Function.update a i x) → ∃ i, a i ⩿ b i ∧ ∀ (j : ι), j ≠ i → a j = b j
Module: Mathlib.Order.Cover

Goal state before:
pp: case mp
ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst✝ : DecidableEq ι
⊢ (∃ i, a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → a j = b j) → ∃ i x, a i ⋖ x ∧ b = Function.update a i x

pp: case mpr
ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst✝ : DecidableEq ι
⊢ (∃ i x, a i ⋖ x ∧ b = Function.update a i x) → ∃ i, a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → a j = b j

Tactic:
· rintro ⟨i, hi, h⟩
    exact ⟨i, b i, hi, by simpa [Function.eq_update_iff, eq_comm] using h⟩

Goal state after:
case mpr
ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst✝ : DecidableEq ι
⊢ (∃ i x, a i ⋖ x ∧ b = Function.update a i x) → ∃ i, a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → a j = b j
Module: Mathlib.Data.Finset.Sigma

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
i : ι
a : α i
b : β i
x : γ i
⊢ ⟨i, x⟩ ∈ sigmaLift f ⟨i, a⟩ ⟨i, b⟩ ↔ x ∈ f a b

Tactic:
rw [sigmaLift, dif_pos rfl, mem_map]
  refine ⟨?_, fun hx => ⟨_, hx, rfl⟩⟩
  rintro ⟨x, hx, _, rfl⟩
  exact hx

Goal state after:
Module: Mathlib.Order.Minimal

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

Tactic:
simp [f.le_iff_le]

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
β : Type u_3
a : α
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
f : α ↪o β
ha : a ∈ s
⊢ ∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)

Tactic:
simp [f.le_iff_le]

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
f : α ↪o β
⊢ ∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)

Tactic:
simp [f.le_iff_le]

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
P : α → Prop
⊢ ∀ ⦃x y : α⦄, ?m.25 x → ?m.25 y → (f x ≤ f y ↔ x ≤ y)

Tactic:
simp [f.le_iff_le]

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

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

Tactic:
rw [Nat.sInf_def h] at hm

Goal state after:
case inr
s : Set ℕ
m : ℕ
h : s.Nonempty
hm : m < Nat.find h
⊢ m ∉ s
Module: Mathlib.Order.Lattice.Nat

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

Tactic:
rintro ⟨H, H'⟩

Goal state after:
case mpr
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : k + 1 ∈ s
H' : k ∉ s
⊢ sInf s = k + 1
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_2
inst✝¹ : Preorder α
inst✝ : Nonempty α
wfl : WellFoundedLT α
wfg : WellFoundedGT α
next : ⦃a : α⦄ → ¬IsMax a → α
hnext : ∀ ⦃a : α⦄ (h : ¬IsMax a), a ⋖ next h
hα : Set.univ.Nonempty
a : ℕ → α := fun t ↦ Nat.rec (⋯.min Set.univ hα) (fun _n a ↦ if ha : IsMax a then a else next ha) t
cov : ∀ (n : ℕ), ¬IsMax (a n) → a n ⋖ a (n + 1)
⊢ ∃ n, IsMax (a n) ∧ ∀ i < n, a i ⋖ a (i + 1)

Tactic:
have H : ∃ n, IsMax (a n) := by
    by_contra!
    exact (RelEmbedding.natGT a fun n ↦ (cov n (this n)).1).not_wellFounded wfg.wf

Goal state after:
α : Type u_2
inst✝¹ : Preorder α
inst✝ : Nonempty α
wfl : WellFoundedLT α
wfg : WellFoundedGT α
next : ⦃a : α⦄ → ¬IsMax a → α
hnext : ∀ ⦃a : α⦄ (h : ¬IsMax a), a ⋖ next h
hα : Set.univ.Nonempty
a : ℕ → α := fun t ↦ Nat.rec (⋯.min Set.univ hα) (fun _n a ↦ if ha : IsMax a then a else next ha) t
cov : ∀ (n : ℕ), ¬IsMax (a n) → a n ⋖ a (n + 1)
H : ∃ n, IsMax (a n)
⊢ ∃ n, IsMax (a n) ∧ ∀ i < n, a i ⋖ a (i + 1)
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
⊢ MulAut.conj h • H = H

Tactic:
refine le_antisymm ?_ ?_
  · exact (conj_smul_le_of_le (le_refl H) ⟨h, hh⟩)
  · rw [subset_pointwise_smul_iff, ← map_inv]
    exact conj_smul_le_of_le (le_refl H) ⟨h⁻¹, H.inv_mem hh⟩

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

Goal state before:
pp: case cons
α : Type u_3
β : Type u_6
inst✝ : CommMonoid β
f : α → β
a : α
s : Finset α
ha : a ∉ s
IH : s.noncommProd f ⋯ = s.prod f
⊢ (cons a s ha).noncommProd f ⋯ = (cons a s ha).prod f

Tactic:
simp [IH]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c d : Con M
x : M → M → Prop
iseqv✝¹ : Equivalence x
mul'✝¹ :
  ∀ {w x_1 y z : M},
    { r := x, iseqv := iseqv✝¹ } w x_1 →
      { r := x, iseqv := iseqv✝¹ } y z → { r := x, iseqv := iseqv✝¹ } (w * y) (x_1 * z)
y : M → M → Prop
iseqv✝ : Equivalence y
mul'✝ :
  ∀ {w x y_1 z : M},
    { r := y, iseqv := iseqv✝ } w x → { r := y, iseqv := iseqv✝ } y_1 z → { r := y, iseqv := iseqv✝ } (w * y_1) (x * z)
h :
  (fun c ↦ ⇑c.toSetoid) { r := x, iseqv := iseqv✝¹, mul' := mul'✝¹ } =
    (fun c ↦ ⇑c.toSetoid) { r := y, iseqv := iseqv✝, mul' := mul'✝ }
this : x = y
⊢ { r := x, iseqv := iseqv✝¹, mul' := mul'✝¹ } = { r := y, iseqv := iseqv✝, mul' := mul'✝ }

Tactic:
subst x

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c d : Con M
y : M → M → Prop
iseqv✝¹ : Equivalence y
mul'✝¹ :
  ∀ {w x y_1 z : M},
    { r := y, iseqv := iseqv✝¹ } w x →
      { r := y, iseqv := iseqv✝¹ } y_1 z → { r := y, iseqv := iseqv✝¹ } (w * y_1) (x * z)
iseqv✝ : Equivalence y
mul'✝ :
  ∀ {w x y_1 z : M},
    { r := y, iseqv := iseqv✝ } w x → { r := y, iseqv := iseqv✝ } y_1 z → { r := y, iseqv := iseqv✝ } (w * y_1) (x * z)
h :
  (fun c ↦ ⇑c.toSetoid) { r := y, iseqv := iseqv✝, mul' := mul'✝ } =
    (fun c ↦ ⇑c.toSetoid) { r := y, iseqv := iseqv✝¹, mul' := mul'✝¹ }
⊢ { r := y, iseqv := iseqv✝, mul' := mul'✝ } = { r := y, iseqv := iseqv✝¹, mul' := mul'✝¹ }
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
f : ι → M
a : ι
h₀ : ∀ b ∈ s, b ≠ a → f b = 1
⊢ ∏ x ∈ s, f x = if a ∈ s then f a else 1

Tactic:
by_cases h : a ∈ s
  · simp [Finset.prod_eq_single_of_mem a h h₀, h]
  · replace h₀ : ∀ b ∈ s, f b = 1 := by grind
    simp +contextual [h₀]

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 ?_ ?_ ?_ ?_ <;> simp +instances +contextual [instMonad]

Goal state after:
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 ?_ ?_ ?_ ?_ <;> simp +instances +contextual [instMonad]

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

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
f : ℕ → M
n : ℕ
⊢ ∏ k ∈ range (n + 1 + 1), f k = (∏ k ∈ range (n + 1), f k) * f (n + 1)

Tactic:
prod_range_succ

Goal state after:
M : Type u_4
inst✝ : CommMonoid M
f : ℕ → M
n : ℕ
⊢ (∏ x ∈ range (n + 1), f x) * f (n + 1) = (∏ k ∈ range (n + 1), f k) * f (n + 1)
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case add
α : Type u
G : Type u_1
inst✝ : AddCommGroup G
f g : α → G
x y : FreeAbelianGroup α
hx : (lift (f + g)) x = (lift f) x + (lift g) x
hy : (lift (f + g)) y = (lift f) y + (lift g) y
⊢ (lift (f + g)) (x + y) = (lift f) (x + y) + (lift g) (x + y)

Tactic:
simp only [(lift _).map_add, hx, hy, add_add_add_comm]

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝ : DecidableEq M
s✝ : Finset ι
t : ι → Finset M
this : DecidableEq ι
a : ι
s : Finset ι
has : a ∉ s
ih : #(s.biUnion t) ≤ ∑ a ∈ s, #(t a)
⊢ #((insert a s).biUnion t) ≤ #(t a) + #(s.biUnion t)

Tactic:
rw [biUnion_insert]; exact card_union_le ..

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
p : ι → Prop
f : ι → M
inst✝ : DecidablePred p
s : Finset ι := {x | p x}.toFinset
⊢ (∏ i, f ↑i) * ∏ i, f ↑i = ∏ i, f i

Tactic:
rw [← Finset.prod_subtype s, ← Finset.prod_subtype sᶜ]

Goal state after:
M : Type u_4
ι : Type u_7
inst✝² : Fintype ι
inst✝¹ : CommMonoid M
p : ι → Prop
f : ι → M
inst✝ : DecidablePred p
s : Finset ι := {x | p x}.toFinset
⊢ (∏ a ∈ s, f a) * ∏ a ∈ sᶜ, f a = ∏ i, f i

case h
M : Type u_4
ι : Type u_7
inst✝² : Fintype ι
inst✝¹ : CommMonoid M
p : ι → Prop
f : ι → M
inst✝ : DecidablePred p
s : Finset ι := {x | p x}.toFinset
⊢ ∀ (x : ι), x ∈ sᶜ ↔ ¬p x

case h
M : Type u_4
ι : Type u_7
inst✝² : Fintype ι
inst✝¹ : CommMonoid M
p : ι → Prop
f : ι → M
inst✝ : DecidablePred p
s : Finset ι := {x | p x}.toFinset
⊢ ∀ (x : ι), x ∈ s ↔ p x
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ H ≤ normalizer ↑K ↔ ⁅H, K⁆ ≤ K

Tactic:
refine le_normalizer_iff.trans ⟨fun hH ↦ ?_, fun hH h hh k hk ↦ ?_⟩
  · exact commutator_le.mpr fun h hh k hk ↦ mul_mem (hH h hh k hk) (inv_mem hk)
  · exact (mul_mem_cancel_right <| inv_mem hk).mp <| hH <| commutator_mem_commutator hh hk

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case of.of
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : CommMonoid α
s t : α
⊢ of s * of t = of t * of s

Tactic:
dsimp only [(· * ·), Mul.mul]
        iterate 4 rw [lift_apply_of]
        congr 1
        exact mul_comm _ _

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
b : Con (M × ↥S)
H : b ∈ {c | ∀ (y : ↥S), c 1 (↑y, y)}
x✝² x✝¹ : M × ↥S
p : M
q : ↥S
x : M
y : ↥S
x✝ : (r' S) (p, q) (x, y)
t : ↥S
ht : ↑t * (↑y * p) = ↑t * (↑q * x)
⊢ (↑t * (↑y * p), t * (y * q)) = (↑t * (↑q * x), t * (q * y))

Tactic:
ht,

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
b : Con (M × ↥S)
H : b ∈ {c | ∀ (y : ↥S), c 1 (↑y, y)}
x✝² x✝¹ : M × ↥S
p : M
q : ↥S
x : M
y : ↥S
x✝ : (r' S) (p, q) (x, y)
t : ↥S
ht : ↑t * (↑y * p) = ↑t * (↑q * x)
⊢ (↑t * (↑q * x), t * (y * q)) = (↑t * (↑q * x), t * (q * y))
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: 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
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
H : ∀ (v : P), ∃ x, v * g ↑x.2 = g x.1
v : P
x : M × ↥S
hx : v * g ↑x.2 = g x.1
⊢ g x.1 = v * g ↑x.2

Tactic:
← hx

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
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
H : ∀ (v : P), ∃ x, v * g ↑x.2 = g x.1
v : P
x : M × ↥S
hx : v * g ↑x.2 = g x.1
⊢ v * g ↑x.2 = v * g ↑x.2
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
p : Sort u
x : Localization S
f : M → ↥S → p
H : ∀ {a c : M} {b d : ↥S}, (r S) (a, b) (c, d) → f a b = f c d
a✝ c✝ : M
b✝ d✝ : ↥S
h : (r S) (a✝, b✝) (c✝, d✝)
⊢ ⋯ ▸ f a✝ b✝ = f c✝ d✝

Tactic:
by simpa only [eq_rec_constant] using H h

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:
OreLocalization.expand' _ _ (s₄' * 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
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)) = r₂' • r₂ • r₁ /ₒ (s₂' * s)
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

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
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
A : Type u_5
inst✝¹ : CommMonoid A
U : Submonoid A
R : Type u_6
inst✝ : CommMonoid R
j : U.LocalizationMap R
l : P →* A
hl : ∀ (w : ↥T), l ↑w ∈ U
z : N
⊢ j (l (k.sec ((f.map hy k) z)).1) *
      ↑((IsUnit.liftRight ((j.toMonoidHom.comp l).domRestrict T) ⋯) (k.sec ((f.map hy k) z)).2)⁻¹ =
    j (l (g (f.sec z).1)) * ↑((IsUnit.liftRight ((j.toMonoidHom.comp (l.comp g)).domRestrict S) ⋯) (f.sec z).2)⁻¹

Tactic:
rw [mul_inv_left, ← mul_assoc, mul_inv_right]

Goal state after:
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
A : Type u_5
inst✝¹ : CommMonoid A
U : Submonoid A
R : Type u_6
inst✝ : CommMonoid R
j : U.LocalizationMap R
l : P →* A
hl : ∀ (w : ↥T), l ↑w ∈ U
z : N
⊢ j (l (k.sec ((f.map hy k) z)).1) * (j.toMonoidHom.comp (l.comp g)) ↑(f.sec z).2 =
    (j.toMonoidHom.comp l) ↑(k.sec ((f.map hy k) z)).2 * j (l (g (f.sec z).1))
Module: Mathlib.GroupTheory.OreLocalization.Basic

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

Tactic:
have : (s₄' * r₃') * (s₁' * s) ∈ S := by
      rw [← mul_assoc, mul_assoc _ r₃', ← h₃, ← mul_assoc, ← mul_assoc, mul_assoc]
      exact mul_mem (s₄' * s₃' * s₂').2 hs

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

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
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
T : Submonoid P
Q : Type u_4
inst✝ : CommMonoid Q
k : P ≃* M
H : Submonoid.map k.toMonoidHom T = S
H' : comap k.toMonoidHom S = T
z : N
x : M × ↥S
hx : z * f ↑x.2 = f x.1
v : P
hv : k v = x.1
w : P
hw : k w = ↑x.2
⊢ z * f.toMonoidHom (k.toMonoidHom w) = f.toMonoidHom (k.toMonoidHom v)

Tactic:
MulEquiv.toMonoidHom_eq_coe,

Goal state after:
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
hg : ∀ (y : ↥S), IsUnit (g ↑y)
T : Submonoid P
Q : Type u_4
inst✝ : CommMonoid Q
k : P ≃* M
H : Submonoid.map k.toMonoidHom T = S
H' : comap k.toMonoidHom S = T
z : N
x : M × ↥S
hx : z * f ↑x.2 = f x.1
v : P
hv : k v = x.1
w : P
hw : k w = ↑x.2
⊢ z * f.toMonoidHom (↑k w) = f.toMonoidHom (↑k v)
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

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
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
T : Submonoid P
Q : Type u_4
inst✝ : CommMonoid Q
k : P ≃* M
H : Submonoid.map k.toMonoidHom T = S
H' : comap k.toMonoidHom S = T
x y : P
⊢ f.toMonoidHom (k.toMonoidHom x) = f.toMonoidHom (k.toMonoidHom y) → ∃ c, ↑c * x = ↑c * y

Tactic:
MulEquiv.toMonoidHom_eq_coe,

Goal state after:
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
hg : ∀ (y : ↥S), IsUnit (g ↑y)
T : Submonoid P
Q : Type u_4
inst✝ : CommMonoid Q
k : P ≃* M
H : Submonoid.map k.toMonoidHom T = S
H' : comap k.toMonoidHom S = T
x y : P
⊢ f.toMonoidHom (↑k x) = f.toMonoidHom (↑k y) → ∃ c, ↑c * x = ↑c * y
Module: Mathlib.Algebra.Order.Sub.WithTop

Goal state before:
pp: α : Type u_1
inst✝¹ : Sub α
inst✝ : Bot α
a b : WithTop α
⊢ a - b ≠ ⊤ ↔ a ≠ ⊤ ∨ b = ⊤

Tactic:
simp [or_iff_not_imp_left]

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_assoc 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
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
x : WithTop α
n✝ n : ℕ
a : WithTop α
⊢ (match a, n + 1 with
    | Option.some a, n => ↑(a ^ n)
    | none, 0 => 1
    | none, _n.succ => ⊤) =
    (match a, n with
      | Option.some a, n => ↑(a ^ n)
      | none, 0 => 1
      | none, _n.succ => ⊤) *
      a

Tactic:
cases n <;> cases a

Goal state after:
case zero.top
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
x : WithTop α
n : ℕ
⊢ (match ⊤, 0 + 1 with
    | Option.some a, n => ↑(a ^ n)
    | none, 0 => 1
    | none, _n.succ => ⊤) =
    (match ⊤, 0 with
      | Option.some a, n => ↑(a ^ n)
      | none, 0 => 1
      | none, _n.succ => ⊤) *
      ⊤

case zero.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
x : WithTop α
n : ℕ
a✝ : α
⊢ (match ↑a✝, 0 + 1 with
    | Option.some a, n => ↑(a ^ n)
    | none, 0 => 1
    | none, _n.succ => ⊤) =
    (match ↑a✝, 0 with
      | Option.some a, n => ↑(a ^ n)
      | none, 0 => 1
      | none, _n.succ => ⊤) *
      ↑a✝

case succ.top
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
x : WithTop α
n n✝ : ℕ
⊢ (match ⊤, n✝ + 1 + 1 with
    | Option.some a, n => ↑(a ^ n)
    | none, 0 => 1
    | none, _n.succ => ⊤) =
    (match ⊤, n✝ + 1 with
      | Option.some a, n => ↑(a ^ n)
      | none, 0 => 1
      | none, _n.succ => ⊤) *
      ⊤

case succ.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
x : WithTop α
n n✝ : ℕ
a✝ : α
⊢ (match ↑a✝, n✝ + 1 + 1 with
    | Option.some a, n => ↑(a ^ n)
    | none, 0 => 1
    | none, _n.succ => ⊤) =
    (match ↑a✝, n✝ + 1 with
      | Option.some a, n => ↑(a ^ n)
      | none, 0 => 1
      | none, _n.succ => ⊤) *
      ↑a✝
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
R' : Type u_2
M : Type u_3
X : Type u_4
inst✝¹² : Monoid M
S : Submonoid M
inst✝¹¹ : OreSet S
inst✝¹⁰ : MulAction M X
inst✝⁹ : SMul R X
inst✝⁸ : SMul R M
inst✝⁷ : IsScalarTower R M M
inst✝⁶ : IsScalarTower R M X
inst✝⁵ : SMul R' X
inst✝⁴ : SMul R' M
inst✝³ : IsScalarTower R' M M
inst✝² : IsScalarTower R' M X
inst✝¹ : SMul R R'
inst✝ : IsScalarTower R R' M
r : R
m : OreLocalization S M
x : OreLocalization S X
⊢ ((r • 1 /ₒ 1) • m) • x = (r • 1 /ₒ 1 * m) • x

Tactic:
smul_eq_mul

Goal state after:
R : Type u_1
R' : Type u_2
M : Type u_3
X : Type u_4
inst✝¹² : Monoid M
S : Submonoid M
inst✝¹¹ : OreSet S
inst✝¹⁰ : MulAction M X
inst✝⁹ : SMul R X
inst✝⁸ : SMul R M
inst✝⁷ : IsScalarTower R M M
inst✝⁶ : IsScalarTower R M X
inst✝⁵ : SMul R' X
inst✝⁴ : SMul R' M
inst✝³ : IsScalarTower R' M M
inst✝² : IsScalarTower R' M X
inst✝¹ : SMul R R'
inst✝ : IsScalarTower R R' M
r : R
m : OreLocalization S M
x : OreLocalization S X
⊢ (r • 1 /ₒ 1 * m) • x = (r • 1 /ₒ 1 * m) • x
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
a : α
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
⊢ ¬IsSuccPrelimit a ↔ ∃ b, ¬IsMax b ∧ succ b = a

Tactic:
rw [not_isSuccPrelimit_iff]
  refine exists_congr fun b ↦ ⟨fun hba ↦ ⟨hba.lt.not_isMax, hba.succ_eq⟩, ?_⟩
  rintro ⟨h, rfl⟩
  exact covBy_succ_of_not_isMax h

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

Goal state before:
pp: α : Type u_1
b : α
motive : α → Sort u_2
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
isMin : (a : α) → IsMin a → motive a
succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a)
isSuccLimit : (a : α) → IsSuccLimit a → ((b : α) → b < a → motive b) → motive a
hb : ¬IsMax b
⊢ limitRecOn (Order.succ b) isMin succ isSuccLimit = succ b hb (limitRecOn b isMin succ isSuccLimit)

Tactic:
rw [limitRecOn, prelimitRecOn_succ_of_not_isMax]; rfl

Goal state after: