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 β
f : α ↪o β
t : Set β
ht : t ⊆ range ⇑f
⊢ Minimal (fun x ↦ x ∈ t) (f x) ↔ Minimal (fun x ↦ f x ∈ t) x

Tactic:
rw [← f.minimal_apply_mem_inter_range_iff, inter_eq_self_of_subset_left ht]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b : α
⊢ Icc a b = 0 ↔ ¬a ≤ b

Tactic:
rw [Icc, Finset.val_eq_zero, Finset.Icc_eq_empty_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : Preorder β
inst✝² : Fintype α
inst✝¹ : DecidableLT α
inst✝ : DecidableLE α
a b x : α
⊢ x ∈ (Set.Ioc a b).toFinset ↔ a < x ∧ x ≤ b

Tactic:
simp only [Set.mem_toFinset, Set.mem_Ioc]

Goal state after:
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: case neg
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : bad.Finite
m : ℕ
hm : ∀ (n : ℕ), m ≤ n → n ∉ bad
h : ∀ (n : ℕ), ∃ n', n < n' ∧ r (f (n + m)) (f (n' + m))
⊢ ∃ g, (∀ (n : ℕ), r (f (g n)) (f (g (n + 1)))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))

Tactic:
let g' : ℕ → ℕ := @Nat.rec (fun _ => ℕ) m fun n gn => Nat.find (h gn)

Goal state after:
case neg
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : bad.Finite
m : ℕ
hm : ∀ (n : ℕ), m ≤ n → n ∉ bad
h : ∀ (n : ℕ), ∃ n', n < n' ∧ r (f (n + m)) (f (n' + m))
g' : ℕ → ℕ := Nat.rec m fun n gn ↦ Nat.find ⋯
⊢ ∃ g, (∀ (n : ℕ), r (f (g n)) (f (g (n + 1)))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ WellFoundedGT α ↔ ∀ (a : ℕ →o α), ∃ n, ∀ (m : ℕ), n ≤ m → ¬a n < a m

Tactic:
by
  refine ⟨fun h a => ?_, fun h => ?_⟩
  · obtain ⟨x, ⟨n, rfl⟩, H⟩ := h.wf.has_min _ (Set.range_nonempty a)
    exact ⟨n, fun m _ => H _ (Set.mem_range_self _)⟩
  · rw [WellFoundedGT, isWellFounded_iff, RelEmbedding.wellFounded_iff_isEmpty]
    refine ⟨fun a => ?_⟩
    obtain ⟨n, hn⟩ := h (a.swap : _ →r _).toOrderHom
    exact hn n.succ n.lt_succ_self.le ((RelEmbedding.map_rel_iff _).2 n.lt_succ_self)

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: case mpr
α : Type u_1
r : α → α → Prop
inst✝ : IsPreorder α r
h : ∀ (f : ℕ → α), ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))
f : ℕ → α
g : ℕ ↪o ℕ
gmon : ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))
⊢ ∃ m n, m < n ∧ r (f m) (f n)

Tactic:
exact ⟨_, _, g.strictMono Nat.zero_lt_one, gmon _ _ (Nat.zero_le 1)⟩

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

Goal state before:
pp: α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h₁ : a₁ ≤ b₁
⊢ Icc a₁ b₁ ⊆ Icc a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂

Tactic:
by
  rw [← coe_subset, coe_Icc, coe_Icc, Set.Icc_subset_Icc_iff h₁]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
a : α
⊢ Iio a ⊆ Iic a

Tactic:
by
  simpa [← coe_subset] using Set.Iio_subset_Iic_self

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

Goal state before:
pp: M : Type u_3
N : Type u_1
F : Type u_2
inst✝³ : EquivLike F M N
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : MulEquivClass F M N
e : F
x : M
hx : x ∈ Set.center M
⊢ e x ∈ Set.center N

Tactic:
let e := MulEquivClass.toMulEquiv e
  change e x ∈ Set.center N
  constructor <;>
  (intros; apply e.symm.injective; simp only
    [map_mul, e.symm_apply_apply, (hx.comm _).eq, (isMulCentral_iff _).mp hx, ← hx.right_comm])

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

Goal state before:
pp: M : Type u_1
c : M
inst✝ : Mul M
h : IsMulCentral c
a b : M
⊢ a * b * c = a * c * b

Tactic:
simp only [h.right_assoc, h.mid_assoc, (h.comm _).eq]

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
x : G
⊢ closure {x⁻¹} = closure {x}

Tactic:
by
  rw [← Set.inv_singleton, closure_inv]

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

Goal state before:
pp: case mem
G : Type u_2
inst✝ : Group G
ι : Sort u_5
S : ι → Subgroup G
C : G → Prop
x✝ : G
mem : ∀ (i : ι), ∀ x ∈ S i, C x
one : C 1
mul : ∀ (x y : G), C x → C y → C (x * y)
x : G
hx : x ∈ ⋃ i, ↑(S i)
i : ι
hi : x ∈ ↑(S i)
⊢ C x

Tactic:
exact mem _ _ hi

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : A ≤ C
⊢ ↑A * ↑(B ⊓ C) = ↑A * ↑B ∩ ↑C

Tactic:
ext
  simp only [coe_inf, Set.mem_mul, Set.mem_inter_iff]
  constructor
  · rintro ⟨y, hy, z, ⟨hzB, hzC⟩, rfl⟩
    refine ⟨?_, mul_mem (h hy) hzC⟩
    exact ⟨y, hy, z, hzB, rfl⟩
  rintro ⟨⟨y, hy, z, hz, rfl⟩, hyz⟩
  refine ⟨y, hy, z, ⟨hz, ?_⟩, rfl⟩
  suffices y⁻¹ * (y * z) ∈ C by simpa
  exact mul_mem (inv_mem (h hy)) hyz

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

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

Tactic:
exact ⟨g, hg, rfl⟩

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

Goal state before:
pp: α : Type u_3
inst✝¹ : Monoid α
inst✝ : DecidableEq α
s : Multiset α
a : α
h : a ∈ s
comm : {x | x ∈ s}.Pairwise Commute
comm' : ∀ x ∈ {x | x ∈ s.erase a}, ∀ x_1 ∈ {x | x ∈ s.erase a}, x ≠ x_1 → Commute x x_1
this : ∀ b ∈ s.erase a, Commute a b
⊢ a * (s.erase a).noncommProd comm' = s.noncommProd comm

Tactic:
mul_noncommProd_erase s h comm comm'

Goal state after:
α : Type u_3
inst✝¹ : Monoid α
inst✝ : DecidableEq α
s : Multiset α
a : α
h : a ∈ s
comm : {x | x ∈ s}.Pairwise Commute
comm' : ∀ x ∈ {x | x ∈ s.erase a}, ∀ x_1 ∈ {x | x ∈ s.erase a}, x ≠ x_1 → Commute x x_1
this : ∀ b ∈ s.erase a, Commute a b
⊢ s.noncommProd comm = s.noncommProd comm
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
⊢ ∀ {w x y z : M}, ⊤ w x → ⊤ y z → ⊤ (w * y) (x * z)

Tactic:
by tauto

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

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

Tactic:
cases b <;> exact Step.not

Goal state after:
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.disjiUnion t hs, f x = ∏ x ∈ s, ∏ i ∈ t x, f i

Tactic:
prod_disjiUnion

Goal state after:
ι : 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
⊢ ∏ i ∈ s, ∏ x ∈ t i, f x = ∏ x ∈ s, ∏ i ∈ t x, f i
Module: Mathlib.GroupTheory.Coset.Defs

Goal state before:
pp: α : Type u_1
inst✝ : Group α
N : Subgroup α
s : Set α
x : α
⊢ (∃ x_1 ∈ s, x_1⁻¹ * x ∈ N) ↔ ∃ x_1 ∈ N, x * x_1 ∈ s

Tactic:
exact
    ⟨fun ⟨y, hs, hN⟩ => ⟨_, N.inv_mem hN, by simpa using hs⟩, fun ⟨z, hz, hxz⟩ =>
      ⟨x * z, hxz, by simpa using hz⟩⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
N : Subgroup α
s : Set α
⊢ mk ⁻¹' mk '' s = ⋃ x, (fun x_1 ↦ x_1 * ↑x) '' s

Tactic:
rw [preimage_image_mk, iUnion_congr_of_surjective (·⁻¹) inv_surjective]
  exact fun x ↦ image_mul_right'

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

Goal state before:
pp: case calc_2
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
i : (a : ι) → a ∈ s → f a ≠ 1 → κ
hi : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ ∈ t
i_inj :
  ∀ (a₁ : ι) (h₁₁ : a₁ ∈ s) (h₁₂ : f a₁ ≠ 1) (a₂ : ι) (h₂₁ : a₂ ∈ s) (h₂₂ : f a₂ ≠ 1),
    i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂
i_surj : ∀ b ∈ t, g b ≠ 1 → ∃ a, ∃ (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ = b
h : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), f a = g (i a h₁ h₂)
⊢ ∀ (a₁ : ι) (ha₁ : a₁ ∈ {x ∈ s | f x ≠ 1}) (a₂ : ι) (ha₂ : a₂ ∈ {x ∈ s | f x ≠ 1}), i a₁ ⋯ ⋯ = i a₂ ⋯ ⋯ → a₁ = a₂

Tactic:
solve_by_elim

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

Goal state before:
pp: case calc_4
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
i : (a : ι) → a ∈ s → f a ≠ 1 → κ
hi : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ ∈ t
i_inj :
  ∀ (a₁ : ι) (h₁₁ : a₁ ∈ s) (h₁₂ : f a₁ ≠ 1) (a₂ : ι) (h₂₁ : a₂ ∈ s) (h₂₂ : f a₂ ≠ 1),
    i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂
i_surj : ∀ b ∈ t, g b ≠ 1 → ∃ a, ∃ (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ = b
h : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), f a = g (i a h₁ h₂)
⊢ ∀ (a : ι) (ha : a ∈ {x ∈ s | f x ≠ 1}), f a = g (i a ⋯ ⋯)

Tactic:
solve_by_elim

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

Goal state before:
pp: case succ
M : Type u_4
inst✝ : CommMonoid M
u : ℕ → M
N : ℕ
hu : ∀ n ≥ N, u n = 1
m : ℕ
hm : ∏ k ∈ range (N + m), u k = ∏ k ∈ range N, u k
⊢ ∏ k ∈ range (N + (m + 1)), u k = ∏ k ∈ range N, u k

Tactic:
| succ m hm =>

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

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

Tactic:
| succ m hm =>

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : N.Normal
s : Set G
⊢ mk ⁻¹' mk '' s = ↑N * s

Tactic:
by
  ext a
  constructor
  · rintro ⟨b, hb, h⟩
    refine ⟨a / b, (QuotientGroup.eq_one_iff _).1 ?_, b, hb, div_mul_cancel _ _⟩
    simp only [h, QuotientGroup.mk_div, div_self']
  · rintro ⟨a, ha, b, hb, rfl⟩
    refine ⟨b, hb, ?_⟩
    simpa only [QuotientGroup.mk_mul, right_eq_mul, QuotientGroup.eq_one_iff]

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✝ : Semigroup α
x : FreeAbelianGroup α
L3 L2 : α
⊢ x * of L2 * of L3 = x * (of L2 * of L3)

Tactic:
| of L2 =>

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case of
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
f : α →* R
x : FreeAbelianGroup α
L2 : α
⊢ (lift ⇑f) (x * of L2) = (lift ⇑f) x * (lift ⇑f) (of L2)

Tactic:
| of L2 =>

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

Goal state before:
pp: case refine_2.refine_1
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : X
s₃ u : ↥S
v : R
hur₁ : ↑u • r₂ = v • r₁
hs₁u : ↑u * ↑s₂ = v * ↑s₁
u' : ↥S
v' : R
hur₂ : ↑u' • r₃ = v' • r₂
hs₂u : ↑u' * ↑s₃ = v' * ↑s₂
r' : R
s' : ↥S
h : ↑s' * v' = r' * ↑u
⊢ ↑s' • ↑u' • r₃ = r' • v • r₁

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

Tactic:
· rw [hur₂, smul_smul, h, mul_smul, hur₁]

Goal state after:
case refine_2.refine_2
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : X
s₃ u : ↥S
v : R
hur₁ : ↑u • r₂ = v • r₁
hs₁u : ↑u * ↑s₂ = v * ↑s₁
u' : ↥S
v' : R
hur₂ : ↑u' • r₃ = v' • r₂
hs₂u : ↑u' * ↑s₃ = v' * ↑s₂
r' : R
s' : ↥S
h : ↑s' * v' = r' * ↑u
⊢ ↑s' * (↑u' * ↑s₃) = r' * (v * ↑s₁)
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 * (f x⁻¹ * g x) ≤ f x * (g x⁻¹ * g x)

Tactic:
gcongr

Goal state after:
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)
x y : N
⊢ g (f.sec (x * y)).1 * g ↑(f.sec y).2 * g ↑(f.sec x).2 = g (f.sec y).1 * g ↑(f.sec (x * y)).2 * g (f.sec x).1

Tactic:
repeat rw [← g.map_mul]

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)
x y : N
⊢ g ((f.sec (x * y)).1 * ↑(f.sec y).2 * ↑(f.sec x).2) = g ((f.sec y).1 * ↑(f.sec (x * y)).2 * (f.sec x).1)
Module: Mathlib.Algebra.Order.Hom.MonoidWithZero

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
H : Type u_7
inst✝³ : Group G
inst✝² : PartialOrder G
inst✝¹ : Group H
inst✝ : PartialOrder H
x✝ : WithZero G ≃*o WithZero H
x : WithZero G
⊢ ((fun e ↦ { toMulEquiv := MulEquiv.withZero e.toMulEquiv, map_le_map_iff' := ⋯ })
        ((fun e ↦ { toMulEquiv := MulEquiv.withZero.symm ↑e, map_le_map_iff' := ⋯ }) x✝))
      x =
    x✝ x

Tactic:
cases x <;> simp

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
a₁ b₁ : M
a₂ b₂ : ↥S
H : b₁ * ↑a₂ = a₁ * ↑b₂
⊢ ↑a₂ * b₁ = ↑b₂ * a₁

Tactic:
by simpa only [mul_comm] using H

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

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosStrictMono α
a : α
c✝ : WithTop α
b c : α
h₀ : 0 < a
hbc : b < c
⊢ b * a < c * a

Tactic:
gcongr

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

Goal state before:
pp: case c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
φ : OreLocalization S R →* T
huniv : ∀ (r : R), φ (numeratorHom r) = f r
r : R
s : ↥S
⊢ ↑(fS s)⁻¹ * (f ↑s * φ (r /ₒ s)) = ↑(fS s)⁻¹ * φ (r /ₒ 1)

Tactic:
← huniv,

Goal state after:
case c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
φ : OreLocalization S R →* T
huniv : ∀ (r : R), φ (numeratorHom r) = f r
r : R
s : ↥S
⊢ ↑(fS s)⁻¹ * (φ (numeratorHom ↑s) * φ (r /ₒ s)) = ↑(fS s)⁻¹ * φ (r /ₒ 1)
Module: Mathlib.Algebra.Order.Ring.WithTop

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

Tactic:
rcases eq_or_ne x 0 with rfl | x0'

Goal state after:
case inl
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulMono α
a b : WithBot α
h : a ≤ b
x0 : 0 ≤ 0
⊢ 0 * a ≤ 0 * b

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

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

Tactic:
rcases eq_or_ne x 0 with rfl | x0'

Goal state after:
case inl
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosMono α
a b : WithBot α
h : a ≤ b
x0 : 0 ≤ 0
⊢ a * 0 ≤ b * 0

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

Goal state before:
pp: case coe.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosStrictMono α
x a✝¹ a✝ : α
h : a✝ < a✝¹
x0 : 0 < x
⊢ a✝ * x < a✝¹ * x

Tactic:
gcongr

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

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

Tactic:
rcases eq_or_ne x 0 with rfl | x0'

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

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

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

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:
· simp at h

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

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

Tactic:
rcases eq_or_ne x 0 with rfl | x0'

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

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

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

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:
· simp at h

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a : α
ha : ¬IsMax a
⊢ Iic a ⊆ Iio (succ a)

Tactic:
gcongr

Goal state after:
case _a
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a : α
ha : ¬IsMax a
⊢ a < succ a
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
hb : ¬IsMax b
⊢ Icc a b ⊆ Ico a (succ b)

Tactic:
gcongr

Goal state after:
case h
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
hb : ¬IsMax b
⊢ b < succ b
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
hb : ¬IsMax b
⊢ Ioc a b ⊆ Ioo a (succ b)

Tactic:
gcongr

Goal state after:
case h
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
hb : ¬IsMax b
⊢ b < succ b
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
⊢ b ≤ succ a ∧ a ≤ b ↔ b = a ∨ b = succ a

Tactic:
by
  rw [and_comm]
  exact le_and_le_succ_iff

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

Goal state before:
pp: α : Type u_1
b : α
motive : α → Sort u_2
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
succ : (a : α) → ¬IsMax a → motive (Order.succ a)
isSuccPrelimit : (a : α) → IsSuccPrelimit a → motive a
hb : ¬IsMax b
hb' : ¬IsSuccPrelimit (Order.succ b)
H : ¬IsMax (Classical.choose ⋯) ∧ Order.succ (Classical.choose ⋯) = Order.succ b
⊢ (if hb : IsSuccPrelimit (Order.succ b) then isSuccPrelimit (Order.succ b) hb
    else cast ⋯ (succ (Classical.choose ⋯) ⋯)) =
    succ b hb

Tactic:
dif_neg hb',

Goal state after:
α : Type u_1
b : α
motive : α → Sort u_2
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
succ : (a : α) → ¬IsMax a → motive (Order.succ a)
isSuccPrelimit : (a : α) → IsSuccPrelimit a → motive a
hb : ¬IsMax b
hb' : ¬IsSuccPrelimit (Order.succ b)
H : ¬IsMax (Classical.choose ⋯) ∧ Order.succ (Classical.choose ⋯) = Order.succ b
⊢ cast ⋯ (succ (Classical.choose ⋯) ⋯) = succ b hb
Module: Mathlib.Data.Nat.SuccPred

Goal state before:
pp: case succ
m n a n✝ : ℕ
h : a < n✝ + 1
⊢ a ≤ (n✝ + 1).pred

Tactic:
· exact le_of_succ_le_succ h

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

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : SuccOrder α
⊢ sInf (Ioi ⊤) ≤ ⊤

Tactic:
exact le_top

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

Goal state before:
pp: case none
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : (a : α) → Decidable (succ a = a)
⊢ none ≤
    match none with
    | none => ⊤
    | Option.some a => if succ a = a then ⊤ else ↑(succ a)

Tactic:
exact le_top

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : (a : α) → Decidable (succ a = a)
a : α
h✝ : succ a = a
⊢ Option.some a ≤ ⊤

Tactic:
exact le_top

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

Goal state before:
pp: case top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : (a : α) → Decidable (succ a = a)
a : WithTop α
h : a < ⊤
⊢ (match a with
    | none => ⊤
    | Option.some a => if succ a = a then ⊤ else ↑(succ a)) ≤
    ⊤

Tactic:
exact le_top

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

Goal state before:
pp: a b c d m n x : ℕ∞
⊢ SuccOrder.succ x = x + 1

Tactic:
cases x <;> simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
X : Type u_3
Y : Type u_4
inst✝² : Preorder X
inst✝¹ : Preorder Y
inst✝ : SuccOrder X
f : X ≃o Y
a✝ b✝ : Y
h : a✝ < b✝
⊢ succ (f.symm a✝) ≤ EquivLike.inv f b✝

Tactic:
exact succ_le_of_lt (by simp [h])

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

Goal state before:
pp: m : ℕ
n : WithTop ℕ∞
h : ↑m < ⊤
⊢ ↑(m + 1) ≤ ⊤

Tactic:
exact le_top

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

Goal state before:
pp: ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝¹ : (j : ι) → Decidable (j ∈ s)
inst✝ : DecidableEq ι
i : ι
v : π i
⊢ update (s.piecewise f g) i v = s.piecewise (update f i v) (update g i v)

Tactic:
ext j
  rcases em (j = i) with (rfl | hj) <;> by_cases hs : j ∈ s <;> simp [*]

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Finset ι
f : ↥s → M
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ ∏ i ∈ s.attach, f i = ∏ i, if h : i ∈ s then f ⟨i, h⟩ else 1

Tactic:
rw [Finset.prod_dite, Finset.univ_eq_attach, Finset.prod_const_one, mul_one]
  congr
  · simp
  · ext; simp
  · apply Function.hfunext <;> simp +contextual [Subtype.heq_iff_coe_eq]

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

Goal state before:
pp: α : Type u_1
n : ℕ
a : α
⊢ ↑(replicate n a) = Multiset.replicate n a

Tactic:
by
  rw [val_eq_coe, coe_replicate]

Goal state after: