mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.FreeGroup.Basic

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

Tactic:
exact List.recOn L s.one_mem fun ⟨x, b⟩ tl ih ↦
    Bool.recOn b (by simpa using s.mul_mem (s.inv_mem <| H ⟨x, rfl⟩) ih)
      (by simpa using s.mul_mem (H ⟨x, rfl⟩) ih)

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

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x : ℤ
i : ℕ
ih : (of 1 ^ i).sum = ↑i
⊢ (fun x ↦ ((map fun x ↦ 1) x).sum) ((fun x ↦ of () ^ x) (-↑i - 1)) = -↑i - 1

Tactic:
simp [zpow_add, ih, sub_eq_add_neg]

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Set ι
inst✝ : DecidablePred fun x ↦ x ∈ s
f : ι → M
g : ↑s → M
w : ∀ (x : ι) (hx : x ∈ s), f x = g ⟨x, hx⟩
w' : ∀ x ∉ s, f x = 1
⊢ ∏ a, f ↑a = ∏ i, g i

pp: ι : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Set ι
inst✝ : DecidablePred fun x ↦ x ∈ s
f : ι → M
g : ↑s → M
w : ∀ (x : ι) (hx : x ∈ s), f x = g ⟨x, hx⟩
w' : ∀ x ∉ s, f x = 1
⊢ Fintype { x // x ∈ s }

Tactic:
congr! with ⟨x, h⟩

Goal state after:
case a
ι : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Set ι
inst✝ : DecidablePred fun x ↦ x ∈ s
f : ι → M
g : ↑s → M
w : ∀ (x : ι) (hx : x ∈ s), f x = g ⟨x, hx⟩
w' : ∀ x ∉ s, f x = 1
x : ι
h : x ∈ s
a✝ : ⟨x, h⟩ ∈ univ
⊢ f ↑⟨x, h⟩ = g ⟨x, h⟩
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 = (∏ x ∈ range n, f (x + 1)) * f (n + 1) * f 0

Tactic:
mul_right_comm,

Goal state after:
M : Type u_4
inst✝ : CommMonoid M
f : ℕ → M
n : ℕ
⊢ ∏ k ∈ range (n + 1 + 1), f k = (∏ x ∈ range n, f (x + 1)) * f 0 * f (n + 1)
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
    exact ⟨s.image e, by rw [Finset.coe_image, MonoidHom.map_mclosure]⟩

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
e : M →* M'
he : Function.Injective ⇑e
h : (Submonoid.map e P).FG
⊢ P.FG

Tactic:
obtain ⟨s, hs⟩ := h
  use s.preimage e he.injOn
  apply Submonoid.map_injective_of_injective he
  rw [← hs, MonoidHom.map_mclosure e, Finset.coe_preimage]
  congr
  rw [Set.image_preimage_eq_iff, ← MonoidHom.coe_mrange e, ← Submonoid.closure_le, hs,
      MonoidHom.mrange_eq_map e]
  exact Submonoid.monotone_map le_top

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case refine_2
M : Type u_1
inst✝ : Monoid M
⊢ (∃ S, ∃ (_ : S.Finite), ∃ φ, Function.Surjective ⇑φ) → FG M

Tactic:
· rintro ⟨S, hfin : Finite S, φ, hφ⟩
    refine fg_iff.mpr ⟨φ '' Set.range FreeMonoid.of, ?_, Set.toFinite _⟩
    simp [← MonoidHom.map_mclosure, hφ, FreeMonoid.closure_range_of, ← MonoidHom.mrange_eq_map]

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝² : Monoid M
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H
s : Finset G
⊢ Subgroup.closure ↑(s.preimage Subtype.val ⋯) = ⊤

Tactic:
rw [Finset.coe_preimage, ← Subgroup.coe_subtype, Subgroup.closure_preimage_eq_top]

Goal state after:
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 : f a = 1
⊢ ∏ x ∈ s.erase a, f x = ∏ x ∈ s, f x

Tactic:
← sdiff_singleton_eq_erase

Goal state after:
ι : Type u_1
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
f : ι → M
a : ι
h : f a = 1
⊢ ∏ x ∈ s \ {a}, f x = ∏ x ∈ s, f x
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: G : Type u_3
inst✝ : CommGroup G
f : ℕ → G
n : ℕ
⊢ f n = f 0 * ∏ i ∈ range n, f (i + 1) / f i

Tactic:
by
  rw [prod_range_div, mul_div_cancel]

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case of.of.zero
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
L3 L2 : α
⊢ 0 * of L2 * of L3 = 0 * (of L2 * of L3)

Tactic:
simp only [zero_mul]

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case of.of.of
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
L3 L2 L1 : α
⊢ of L1 * of L2 * of L3 = of L1 * (of L2 * of L3)

Tactic:
of_mul_of,

Goal state after:
case of.of.of
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
L3 L2 L1 : α
⊢ of (L1 * L2) * of L3 = of L1 * (of L2 * of L3)
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case of.of.of
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
L3 L2 L1 : α
⊢ of (L1 * L2) * of L3 = of L1 * (of L2 * of L3)

Tactic:
of_mul_of,

Goal state after:
case of.of.of
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
L3 L2 L1 : α
⊢ of (L1 * L2 * L3) = of L1 * (of L2 * of L3)
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case of.of.of
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
L3 L2 L1 : α
⊢ of (L1 * L2 * L3) = of L1 * (of L2 * of L3)

Tactic:
of_mul_of,

Goal state after:
case of.of.of
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
L3 L2 L1 : α
⊢ of (L1 * L2 * L3) = of L1 * of (L2 * L3)
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case of.of.of
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
L3 L2 L1 : α
⊢ of (L1 * L2 * L3) = of L1 * of (L2 * L3)

Tactic:
of_mul_of,

Goal state after:
case of.of.of
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
L3 L2 L1 : α
⊢ of (L1 * L2 * L3) = of (L1 * (L2 * L3))
Module: Mathlib.GroupTheory.FreeAbelianGroup

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

Tactic:
of_mul_of,

Goal state after:
case of.of
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
f : α →* R
L2 L1 : α
⊢ (lift ⇑f) (of (L1 * L2)) = (lift ⇑f) (of L1) * (lift ⇑f) (of L2)
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 : X
s : ↥S
r' : X
s' u : ↥S
v : R
hru : u • r' = v • r
hsu : ↑u * ↑s' = v * ↑s
r₂ : R
s₂ : ↥S
h₁ : ↑s₂ * ↑s = r₂ * ↑s'
r₃ : R
s₃ : ↥S
h₂ : ↑s₃ * r₂ = r₃ * ↑u
⊢ r₃ * v * ↑s = ↑s₃ * (↑s₂ * ↑s)

Tactic:
h₁,

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 : X
s : ↥S
r' : X
s' u : ↥S
v : R
hru : u • r' = v • r
hsu : ↑u * ↑s' = v * ↑s
r₂ : R
s₂ : ↥S
h₁ : ↑s₂ * ↑s = r₂ * ↑s'
r₃ : R
s₃ : ↥S
h₂ : ↑s₃ * r₂ = r₃ * ↑u
⊢ r₃ * v * ↑s = ↑s₃ * (r₂ * ↑s')
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x y : M × ↥S
u : M
hu : u ∈ S
v : M
e₁ : u * y.1 = v * x.1
e₂ : u * ↑y.2 = v * ↑x.2
⊢ v * ↑x.2 * x.1 = u * (↑x.2 * y.1)

Tactic:
mul_right_comm,

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x y : M × ↥S
u : M
hu : u ∈ S
v : M
e₁ : u * y.1 = v * x.1
e₂ : u * ↑y.2 = v * ↑x.2
⊢ v * x.1 * ↑x.2 = u * (↑x.2 * y.1)
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: case mpr
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 : M), f x = f y ↔ g x = g y) → Injective ⇑(f.lift hg)

Tactic:
intro H z w h

Goal state after:
case mpr
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 : ∀ (x y : M), f x = f y ↔ g x = g y
z w : N
h : (f.lift hg) z = (f.lift hg) w
⊢ z = w
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) * (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))

Tactic:
change j _ * j (l (g _)) = j (l _) * _

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 (l (g ↑(f.sec z).2)) = j (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: 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₁'
⊢ r₃' * (↑s₁' * r₁) = r₃' * r₁' * ↑s₂

Tactic:
h₁,

Goal state after:
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₁'
⊢ r₃' * (r₁' * ↑s₂) = r₃' * r₁' * ↑s₂
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₂ : ↥S
⊢ (r₁ /ₒ s₁) • (r₂ /ₒ s₂) = oreNum r₁ s₂ • r₂ /ₒ (oreDenom r₁ s₂ * s₁)

Tactic:
by
  with_unfolding_all 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
r₁ r₂ : R
s₁ s₂ : ↥S
⊢ r₁ /ₒ s₁ * (r₂ /ₒ s₂) = oreNum r₁ s₂ * r₂ /ₒ (oreDenom r₁ s₂ * s₁)

Tactic:
by
  with_unfolding_all 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
inst✝ : One X
⊢ 1 = 1 /ₒ 1

Tactic:
by
  with_unfolding_all rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Add α
inst✝³ : LE α
inst✝² : OrderBot α
inst✝¹ : Sub α
inst✝ : OrderedSub α
⊢ OrderedSub (WithTop α)

Tactic:
by
  constructor
  rintro x y z
  cases y
  · cases z <;> simp
  cases x
  · simp
  cases z
  · simp
  norm_cast
  exact tsub_le_iff_right

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

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
a : α
⊢ 1 * ↑a = ↑a

Tactic:
rw [← coe_one, ← coe_mul, one_mul]

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

Goal state before:
pp: case inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : SemigroupWithZero α
inst✝ : NoZeroDivisors α
b c : WithTop α
⊢ 0 * b * c = 0 * (b * c)

Tactic:
simp only [zero_mul]

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✝¹ : Zero X
inst✝ : MulAction R X
⊢ 0 = 0 /ₒ 1

Tactic:
by
  with_unfolding_all rfl

Goal state after:
Module: Mathlib.Order.Iterate

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
f : α → α
x : α
hf : Monotone f
hx : x ≤ f x
n : ℕ
⊢ f^[n] x ≤ f^[n + 1] x

Tactic:
by
    rw [iterate_succ_apply]
    exact hf.iterate n hx

Goal state after:
Module: Mathlib.Order.Iterate

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
f : α → α
x : α
hf : StrictMono f
hx : x < f x
n : ℕ
⊢ f^[n] x < f^[n + 1] x

Tactic:
by
    rw [iterate_succ_apply]
    exact hf.iterate n hx

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

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

Tactic:
simp only [← coe_mul, coe_lt_coe] at *

Goal state after:
case coe.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulStrictMono α
x : α
x0 : 0 < ↑x
a✝¹ a✝ : α
h : a✝ < a✝¹
⊢ x * a✝ < x * a✝¹
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 : α
x0 : 0 < ↑x
a✝¹ a✝ : α
h : ↑a✝ < ↑a✝¹
⊢ ↑a✝ * ↑x < ↑a✝¹ * ↑x

Tactic:
simp only [← coe_mul, coe_lt_coe] at *

Goal state after:
case coe.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosStrictMono α
x : α
x0 : 0 < ↑x
a✝¹ a✝ : α
h : a✝ < a✝¹
⊢ a✝ * x < a✝¹ * x
Module: Mathlib.Algebra.Order.Ring.WithTop

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

Tactic:
simp only [← coe_mul, coe_lt_coe] at *

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

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

Tactic:
simp only [← coe_mul, coe_lt_coe] at *

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

Goal state before:
pp: α : Type u_2
inst✝³ : Nontrivial α
inst✝² : LinearOrder α
inst✝¹ : OrderBot α
inst✝ : SuccOrder α
a : WithBot α
⊢ a.succ = ⊥ ↔ a = ⊥

Tactic:
cases a
  · simp
  · simpa [WithBot.succ_coe, WithBot.coe_ne_bot, iff_false] using Order.succ_ne_bot _

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

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
hb : ¬IsMax b
⊢ b < succ b

Tactic:
exact lt_succ_of_not_isMax hb

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✝¹ : PartialOrder β
inst✝ : SuccOrder β
f : α ≃o β
a : α
h : IsMax a
⊢ f a = succ (f a)

Tactic:
(f.isMax_apply.2 h).succ_eq

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : SuccOrder α
inst✝¹ : PartialOrder β
inst✝ : SuccOrder β
f : α ≃o β
a : α
h : IsMax a
⊢ f a = f a
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
b : α
motive : α → Sort u_2
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
isMin : (a : α) → IsMin a → motive a
succ : (a : α) → ¬IsMax a → motive (Order.succ a)
isSuccLimit : (a : α) → IsSuccLimit a → motive a
hb : IsMin b
⊢ (if h : IsMin b then isMin b h else isSuccLimit b ⋯) = isMin b hb

Tactic:
dif_pos hb

Goal state after:
α : Type u_1
b : α
motive : α → Sort u_2
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
isMin : (a : α) → IsMin a → motive a
succ : (a : α) → ¬IsMax a → motive (Order.succ a)
isSuccLimit : (a : α) → IsSuccLimit a → motive a
hb : IsMin b
⊢ isMin b hb = isMin b hb
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
b : α
motive : α → Sort u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a)
isSuccPrelimit : (a : α) → IsSuccPrelimit a → ((b : α) → b < a → motive b) → motive a
hb : IsSuccPrelimit b
⊢ (if h : IsSuccPrelimit b then
      isSuccPrelimit b h fun y x ↦
        ⋯.fix
          (fun a IH ↦
            if h : IsSuccPrelimit a then isSuccPrelimit a h IH
            else cast ⋯ (succ (Classical.choose ⋯) ⋯ (IH (Classical.choose ⋯) ⋯)))
          y
    else
      cast ⋯
        (succ (Classical.choose ⋯) ⋯
          ((fun y x ↦
              ⋯.fix
                (fun a IH ↦
                  if h : IsSuccPrelimit a then isSuccPrelimit a h IH
                  else cast ⋯ (succ (Classical.choose ⋯) ⋯ (IH (Classical.choose ⋯) ⋯)))
                y)
            (Classical.choose ⋯) ⋯))) =
    isSuccPrelimit b hb fun x x_1 ↦ prelimitRecOn x succ isSuccPrelimit

Tactic:
dif_pos hb

Goal state after:
α : Type u_1
b : α
motive : α → Sort u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a)
isSuccPrelimit : (a : α) → IsSuccPrelimit a → ((b : α) → b < a → motive b) → motive a
hb : IsSuccPrelimit b
⊢ (isSuccPrelimit b hb fun y x ↦
      ⋯.fix
        (fun a IH ↦
          if h : IsSuccPrelimit a then isSuccPrelimit a h IH
          else cast ⋯ (succ (Classical.choose ⋯) ⋯ (IH (Classical.choose ⋯) ⋯)))
        y) =
    isSuccPrelimit b hb fun x x_1 ↦ prelimitRecOn x succ isSuccPrelimit
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
b : α
motive : α → Sort u_2
inst✝² : PartialOrder α
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 : IsMin b
⊢ (if h : IsMin b then isMin b h
    else
      isSuccLimit b ⋯ fun x x_1 ↦
        prelimitRecOn x succ fun a ha IH ↦ if h : IsMin a then isMin a h else isSuccLimit a ⋯ IH) =
    isMin b hb

Tactic:
dif_pos hb

Goal state after:
α : Type u_1
b : α
motive : α → Sort u_2
inst✝² : PartialOrder α
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 : IsMin b
⊢ isMin b hb = isMin b hb
Module: Mathlib.Data.Nat.SuccPred

Goal state before:
pp: m n a : ℕ
ha : a ≤ a.pred
⊢ IsMin a

Tactic:
cases a
    · exact isMin_bot
    · exact (not_succ_le_self _ ha).elim

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

Goal state before:
pp: α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
i : α
n : ℕ
hn : ¬IsMax (succ^[n] i) → pred^[n + 1] (succ^[n + 1] i) = i
hin : ¬IsMax (succ^[n + 1] i)
⊢ succ^[n] i ≤ succ^[n.succ] i

Tactic:
Function.iterate_succ'

Goal state after:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
i : α
n : ℕ
hn : ¬IsMax (succ^[n] i) → pred^[n + 1] (succ^[n + 1] i) = i
hin : ¬IsMax (succ^[n + 1] i)
⊢ succ^[n] i ≤ (succ ∘ succ^[n]) i
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case succ
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
i : α
n : ℕ
hn : ¬IsMax (succ^[n - 1] i) → pred^[n] (succ^[n] i) = i
hin : ¬IsMax (succ^[n] i)
h_not_max : ¬IsMax (succ^[n - 1] i)
⊢ (pred^[n] ∘ pred) (succ^[n + 1] i) = i

Tactic:
Function.iterate_succ'

Goal state after:
case succ
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
i : α
n : ℕ
hn : ¬IsMax (succ^[n - 1] i) → pred^[n] (succ^[n] i) = i
hin : ¬IsMax (succ^[n] i)
h_not_max : ¬IsMax (succ^[n - 1] i)
⊢ (pred^[n] ∘ pred) ((succ ∘ succ^[n]) i) = i
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : OrderTop α
inst✝ : PredOrder α
a b : WithTop α
h : a < b
⊢ a ≤
    match b with
    | none => ↑⊤
    | Option.some a => ↑(pred a)

Tactic:
cases a
    · exact (le_top.not_gt h).elim
    cases b
    · exact coe_le_coe.2 le_top
    exact coe_le_coe.2 (le_pred_of_lt <| coe_lt_coe.1 h)

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

Goal state before:
pp: case top.coe
a✝ : ℕ
⊢ (⊤ * ↑a✝).toNat = ⊤.toNat * (↑a✝).toNat

pp: case coe.top
a✝ : ℕ
⊢ (↑a✝ * ⊤).toNat = (↑a✝).toNat * ⊤.toNat

pp: case coe.coe
a✝¹ a✝ : ℕ
⊢ (↑a✝¹ * ↑a✝).toNat = (↑a✝¹).toNat * (↑a✝).toNat

Tactic:
· rename_i b; cases b <;> simp

Goal state after:
case coe.top
a✝ : ℕ
⊢ (↑a✝ * ⊤).toNat = (↑a✝).toNat * ⊤.toNat

case coe.coe
a✝¹ a✝ : ℕ
⊢ (↑a✝¹ * ↑a✝).toNat = (↑a✝¹).toNat * (↑a✝).toNat
Module: Mathlib.Control.Applicative

Goal state before:
pp: F : Type u → Type v
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
α β : Type u
f : α → β
⊢ (fun x ↦ pure f <*> x) = fun x ↦ f <$> x

Tactic:
simp [functor_norm]

Goal state after:
Module: Mathlib.Control.Traversable.Basic

Goal state before:
pp: F : Type u → Type v
inst✝² : Applicative F
G : Type u → Type w
inst✝¹ : Applicative G
H : Type u → Type s
inst✝ : Applicative H
η' : ApplicativeTransformation G H
η : ApplicativeTransformation F G
α✝ : Type u
x : α✝
⊢ (fun {α} ↦ η'.app α) ((fun {α} ↦ η.app α) (pure x)) = pure x

Tactic:
simp [functor_norm]

Goal state after:
Module: Mathlib.Control.Traversable.Basic

Goal state before:
pp: F : Type u → Type v
inst✝² : Applicative F
G : Type u → Type w
inst✝¹ : Applicative G
H : Type u → Type s
inst✝ : Applicative H
η' : ApplicativeTransformation G H
η : ApplicativeTransformation F G
α✝ β✝ : Type u
x : F (α✝ → β✝)
y : F α✝
⊢ (fun {α} ↦ η'.app α) ((fun {α} ↦ η.app α) (x <*> y)) =
    (fun {α} ↦ η'.app α) ((fun {α} ↦ η.app α) x) <*> (fun {α} ↦ η'.app α) ((fun {α} ↦ η.app α) y)

Tactic:
simp [functor_norm]

Goal state after:
Module: Mathlib.Control.Applicative

Goal state before:
pp: F : Type u → Type w
G : Type v → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β : Type v
f : Comp F G (α → β)
x : α
⊢ (f <*> pure x).run = ((fun g ↦ g x) <$> f).run

Tactic:
simp [functor_norm]

Goal state after:
Module: Mathlib.Control.Applicative

Goal state before:
pp: F : Type u → Type w
G : Type v → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β : Type v
f : α → β
x : Comp F G α
⊢ (pure f <*> x).run = (f <$> x).run

Tactic:
simp [functor_norm]

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

Goal state before:
pp: α : Type u_1
n : ℕ
p : Sym α n → Prop
⊢ (∀ (s : Sym α n), p s) ↔ ∀ (s : Multiset α) (hs : s.card = n), p (mk s hs)

Tactic:
simp [Sym]

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

Goal state before:
pp: α : Type u_1
n : ℕ
p : Sym α n → Prop
⊢ (∃ s, p s) ↔ ∃ s, ∃ (hs : s.card = n), p (mk s hs)

Tactic:
simp [Sym]

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

Goal state before:
pp: α : Type u_1
n : ℕ
v : Vector α (n + 1)
⊢ v.reverse.head = v.last

Tactic:
rw [← get_zero, last_def, get_eq_get_toList, get_eq_get_toList]
  simp_rw [toList_reverse]
  simp

Goal state after: