mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : DivInvMonoid α
a : α
⊢ a⁺ᵐ ≤ 1 ↔ a ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : DivInvMonoid α
a : α
⊢ a⁻ᵐ ≤ 1 ↔ a⁻¹ ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : DivInvMonoid α
a : α
ha : 1 < a
⊢ 1 < a⁺ᵐ

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.NormNum.Ineq

Goal state before:
pp: α : Type u_1
inst✝² : Semiring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
num✝¹ num✝ da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h : decide (num✝¹ * db < num✝ * da) = true
⊢ ↑num✝¹ * ⅟↑da < ↑num✝ * ⅟↑db

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : DivInvMonoid α
a b : α
⊢ (a ⊔ b)⁺ᵐ = a⁺ᵐ ⊔ b⁺ᵐ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : Group α
⊢ 1⁻ᵐ = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : Group α
a : α
⊢ a⁻¹⁻ᵐ = a⁺ᵐ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : Group α
a : α
inst✝ : MulLeftMono α
⊢ a⁻ᵐ = a⁻¹ ↔ a ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
N : Type u_4
inst✝¹ : One M
inst✝ : One N
f : ι → M
g : ι → N
x : ι
⊢ (x ∈ mulSupport fun x ↦ (f x, g x)) ↔ x ∈ mulSupport f ∪ mulSupport g

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : Group α
a : α
inst✝ : MulLeftMono α
⊢ a⁻ᵐ = 1 ↔ 1 ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : Group α
a : α
inst✝ : MulLeftMono α
⊢ a⁻ᵐ ≤ 1 ↔ 1 ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : Group α
a : α
inst✝ : MulLeftMono α
ha : a < 1
⊢ 1 < a⁻ᵐ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
N : Type u_4
inst✝¹ : One M
inst✝ : One N
f : ι → M × N
⊢ mulSupport f = (mulSupport fun x ↦ (f x).1) ∪ mulSupport fun x ↦ (f x).2

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : Group α
inst✝ : MulLeftMono α
a : α
⊢ a⁺ᵐ / a⁻ᵐ = a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : Group α
inst✝ : MulLeftMono α
a : α
⊢ a⁻ᵐ / a⁺ᵐ = a⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_3
inst✝ : One M
f : ι × κ → M
i : ι
j : κ
hj : j ∈ mulSupport fun j ↦ f (i, j)
⊢ (i, j) ∈ mulSupport f ∧ (i, j).2 = j

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_3
inst✝ : One M
f : ι × κ → M
⊢ mulSupport (curry f) = Prod.fst '' mulSupport f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : Group α
inst✝ : MulLeftMono α
⊢ Injective fun a ↦ (a⁺ᵐ, a⁻ᵐ)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_3
inst✝ : One M
f : ι → M
s : Set κ
g : κ → ι
⊢ g '' s ∩ mulSupport f = g '' (s ∩ mulSupport (f ∘ g))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : One M
i : ι
⊢ mulSupport (mulSingle i 1) = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : One M
i : ι
a : M
h : a ≠ 1
x : ι
hx : x ∈ {i}
⊢ x ∈ mulSupport (mulSingle i a)

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.NormNum.Ineq

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
num✝¹ num✝ : ℤ
da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h : decide (num✝¹.mul (Int.ofNat db) ≤ num✝.mul (Int.ofNat da)) = true
⊢ ↑num✝¹ * ⅟↑da ≤ ↑num✝ * ⅟↑db

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
⊢ a⁻ᵐ = (a ⊓ 1)⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.NormNum.Ineq

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
num✝¹ num✝ : ℤ
da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h✝ : decide (num✝¹ * ↑db < num✝ * ↑da) = true
h : (fun x ↦ ↑x) (num✝¹ * ↑db) < (fun x ↦ ↑x) (num✝ * ↑da)
⊢ ↑num✝¹ * ⅟↑da < ↑num✝ * ⅟↑db

Tactic:
have ha : 0 < ⅟(da : α) := pos_invOf_of_invertible_cast da

Goal state after:
α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
num✝¹ num✝ : ℤ
da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h✝ : decide (num✝¹ * ↑db < num✝ * ↑da) = true
h : (fun x ↦ ↑x) (num✝¹ * ↑db) < (fun x ↦ ↑x) (num✝ * ↑da)
ha : 0 < ⅟↑da
⊢ ↑num✝¹ * ⅟↑da < ↑num✝ * ⅟↑db
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : One M
i : ι
a : M
inst✝ : DecidableEq M
⊢ mulSupport (mulSingle i a) = if a = 1 then ∅ else {i}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : One M
i : ι
a : M
⊢ (mulSupport (mulSingle i a)).Subsingleton

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : One M
i j : ι
a b : M
ha : a ≠ 1
hb : b ≠ 1
⊢ Disjoint (mulSupport (mulSingle i a)) (mulSupport (mulSingle j b)) ↔ i ≠ j

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
⊢ a⁺ᵐ * a⁻ᵐ = |a|ₘ

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Cast.Field

Goal state before:
pp: R : Type u_2
inst✝ : DivisionRing R
n : ℕ
⊢ ↑(-↑n) = -↑n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Cast.Field

Goal state before:
pp: α : Type u_1
inst✝ : DivisionRing α
n : ℤ
hn : ↑n ≠ 0
k : ℤ
⊢ n ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Cast.Field

Goal state before:
pp: α : Type u_1
inst✝ : DivisionRing α
m n : ℤ
n_dvd : n ∣ m
hn : ↑n ≠ 0
⊢ ↑(m / n) = ↑m / ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
⊢ a⁻ᵐ * a⁺ᵐ = |a|ₘ

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.NormNum.Ineq

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
num✝¹ num✝ : ℤ
da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h : decide (num✝¹ * ↑db < num✝ * ↑da) = true
⊢ ↑num✝¹ * ⅟↑da < ↑num✝ * ⅟↑db

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.NormNum.Ineq

Goal state before:
pp: $u✝ «$u» : Level
«$α» : Type u
«$lα» : LE «$α»
«$a» «$b» : «$α»
«$e» : Prop
«$ra» : AddMonoidWithOne «$α»
«$na» : ℕ
«$pa» : IsNat «$a» «$na»
«$rb» : AddMonoidWithOne «$α»
«$nb» : ℕ
«$pb» : IsNat «$b» «$nb»
$fst✝¹ : Semiring «$α»
$fst✝ : PartialOrder «$α»
«$_i» : IsOrderedRing «$α»
⊢ AddMonoidWithOne «$α»

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
⊢ a⁺ᵐ ⊓ a⁻ᵐ = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b : α
⊢ (a ⊓ b)⁻ᵐ = a⁻ᵐ ⊔ b⁻ᵐ

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.NormNum.Ineq

Goal state before:
pp: $u✝ «$u» : Level
«$α» : Type u
«$lα» : LE «$α»
«$a» «$b» : «$α»
«$e» : Prop
«$na» : ℕ
«$rb» : AddMonoidWithOne «$α»
«$nb» : ℕ
«$pb» : IsNat «$b» «$nb»
$fst✝¹ : Semiring «$α»
$fst✝ : PartialOrder «$α»
«$_i» : IsOrderedRing «$α»
«$ra» : AddMonoidWithOne «$α» := inferInstance
«$pa» : IsNat «$a» «$na»
⊢ AddMonoidWithOne «$α»

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ a ⊔ b = b * (a / b)⁺ᵐ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ a ⊓ b = a / (a / b)⁺ᵐ

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: m n : ℕ
h : m ≤ n
⊢ m ! ∣ n !

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.NormNum.Ineq

Goal state before:
pp: $u✝ «$u» : Level
«$α» : Type u
«$lα» : LT «$α»
«$a» «$b» : «$α»
«$e» : Prop
«$ra» : AddMonoidWithOne «$α»
«$na» : ℕ
«$pa» : IsNat «$a» «$na»
«$rb» : AddMonoidWithOne «$α»
«$nb» : ℕ
«$pb» : IsNat «$b» «$nb»
$fst✝¹ : Semiring «$α»
$fst✝ : PartialOrder «$α»
«$_i» : IsOrderedRing «$α»
⊢ AddMonoidWithOne «$α»

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: m : ℕ
⊢ m ! * (m + 1) ^ 0 ≤ (m + 0)!

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.NormNum.Ineq

Goal state before:
pp: $u✝ «$u» : Level
«$α» : Type u
«$lα» : LT «$α»
«$a» «$b» : «$α»
«$e» : Prop
«$na» : ℕ
«$rb» : AddMonoidWithOne «$α»
«$nb» : ℕ
«$pb» : IsNat «$b» «$nb»
$fst✝¹ : Semiring «$α»
$fst✝ : PartialOrder «$α»
«$_i» : IsOrderedRing «$α»
«$ra» : AddMonoidWithOne «$α» := inferInstance
«$pa» : IsNat «$a» «$na»
⊢ AddMonoidWithOne «$α»

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.CharZero

Goal state before:
pp: k : Type u_3
inst✝¹ : DivisionRing k
inst✝ : CharZero k
m n : ℤ
n_dvd : n ∣ m
⊢ ↑(m / n) = ↑m / ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: m n : ℕ
⊢ m ! * (m + 1) ^ (n + 1) ≤ (m + (n + 1))!

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.CharZero

Goal state before:
pp: k : Type u_3
inst✝¹ : DivisionRing k
inst✝ : CharZero k
m n : ℕ
n_dvd : n ∣ m
⊢ ↑(↑m / ↑n) = ↑m / ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ a ≤ b ↔ a⁺ᵐ ≤ b⁺ᵐ ∧ b⁻ᵐ ≤ a⁻ᵐ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a : α
⊢ |a|ₘ * a = a⁺ᵐ ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: m n : ℕ
hn : 0 < n
h : n < m
⊢ ∀ {n : ℕ}, 0 < n → n ! < (n + 1)!

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a : α
⊢ a * |a|ₘ = a⁺ᵐ ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a : α
⊢ |a|ₘ / a = a⁻ᵐ ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: m n : ℕ
hn : 0 < n
⊢ n ! < m ! ↔ n < m

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a : α
⊢ a / |a|ₘ = (a⁻ᵐ ^ 2)⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : Group α
a b : α
⊢ (a ⊓ b)⁺ᵐ = a⁺ᵐ ⊓ b⁺ᵐ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝³ : DistribLattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b : α
⊢ (a ⊔ b)⁻ᵐ = a⁻ᵐ ⊓ b⁻ᵐ

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
⊢ n ! = 1 ↔ n ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Group α
a : α
⊢ a⁺ᵐ = if 1 ≤ a then a else 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Group α
a : α
⊢ a⁺ᵐ = if 1 < a then a else 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Group α
a : α
ha : 1 < a⁺ᵐ
⊢ a⁺ᵐ = a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : Group α
a : α
inst✝ : MulLeftMono α
⊢ a⁻ᵐ = if a ≤ 1 then a⁻¹ else 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : Group α
a : α
inst✝ : MulLeftMono α
⊢ a⁻ᵐ = if a < 1 then a⁻¹ else 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
inst✝² : Group α
a b : α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
⊢ a⁻¹ < b ∧ 1 < b ↔ b⁻¹ < a ∧ 1 < b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: m n : ℕ
hn : 1 < n
⊢ n ! = m ! ↔ n = m

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: m n : ℕ
h : 1 < n ∨ 1 < m
⊢ n ! = m ! ↔ n = m

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
hi : 3 ≤ n
⊢ 0 < n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
hi : 3 ≤ n
⊢ n < n !

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: i n : ℕ
hi : 2 ≤ i
⊢ i + (n + 1)! < (i + n + 1)!

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: i n : ℕ
hi : 2 ≤ i
hn : 1 ≤ n
⊢ i + n ! < (i + n)!

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: i n : ℕ
⊢ i + (n + 1)! ≤ (i + (n + 1))!

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: i n : ℕ
n1 : 1 ≤ n
⊢ i + n ! ≤ (i + n)!

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n m : ℕ
hnm : n ≤ m
⊢ n ! * (n + 1) ^ (m - n) ≤ m !

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n m : ℕ
hnm : n ≤ m
⊢ n ! * n ^ (m - n) ≤ m !

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
⊢ (n + 1) * (n + 1) ^ n = (n + 1) ^ (n + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: ⊢ ascFactorial 0 (succ 0) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: k : ℕ
⊢ ascFactorial 0 (k + 1).succ = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: k : ℕ
⊢ ascFactorial 1 (k + 1) = (k + 1)!

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
⊢ n * n.succ.ascFactorial 0 = (n + 0) * n.ascFactorial 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
⊢ n * n.succ.ascFactorial (k + 1) = (n + (k + 1)) * n.ascFactorial (k + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
⊢ n ! * (n + 1).ascFactorial 0 = (n + 0)!

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
⊢ n ! * (n + 1).ascFactorial (k + 1) = (n + (k + 1))!

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
h : 0 < n
⊢ (n - 1)! * n.ascFactorial k = (n + k - 1)!

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: case succ
l k n' : ℕ
⊢ (n' + l)! * (n' + l + 1).ascFactorial k = (n' + (l + k))!

Tactic:
factorial_mul_ascFactorial,

Goal state after:
case succ
l k n' : ℕ
⊢ (n' + l + k)! = (n' + (l + k))!
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n l k : ℕ
⊢ n.ascFactorial l * (n + l).ascFactorial k = n.ascFactorial (l + k)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
⊢ (n - k) * (n - k + 1).ascFactorial k = (n - k).ascFactorial (k + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n m : ℕ
h : n ≤ m
k : ℕ
ih : n.ascFactorial k ≤ m.ascFactorial k
⊢ n + k ≤ m + k

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: k n m : ℕ
h : n ≤ m
⊢ n.ascFactorial k ≤ m.ascFactorial k

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
⊢ n ^ 0 ≤ n.ascFactorial 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
⊢ n ^ (k + 1) ≤ n.ascFactorial (k + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
⊢ (n + 1) ^ (k + 2) < (n + 1).ascFactorial (k + 2)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
⊢ 2 ≤ 0 → (n + 1) ^ 0 < (n + 1).ascFactorial 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
⊢ 2 ≤ 1 → (n + 1) ^ 1 < (n + 1).ascFactorial 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
⊢ (n + 1).ascFactorial 0 ≤ (n + 0) ^ 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
⊢ (n + 1).ascFactorial (k + 1) ≤ (n + (k + 1)) ^ (k + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
⊢ n.ascFactorial 0 ≤ 0! * n ^ 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k j : ℕ
⊢ n.ascFactorial (j + 1) ≤ (j + 1)! * n ^ (j + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
⊢ 2 ≤ 0 → (n + 1).ascFactorial 0 < (n + 0) ^ 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
⊢ 2 ≤ 1 → (n + 1).ascFactorial 1 < (n + 1) ^ 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
x✝ : 2 ≤ k + 2
⊢ (n + 1).ascFactorial (k + 2) < (n + (k + 2)) ^ (k + 2)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: k : ℕ
⊢ descFactorial 0 (k + 1) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
⊢ n.descFactorial 1 = n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
⊢ (n + 1).descFactorial (0 + 1) = (n + 1) * n.descFactorial 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
⊢ (n + 1).descFactorial (k.succ + 1) = (n + 1) * n.descFactorial k.succ

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
⊢ (n + 1 - 0) * (n + 1).descFactorial 0 = (n + 1) * n.descFactorial 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
⊢ (n + 1 - (k + 1)) * (n + 1).descFactorial (k + 1) = (n + 1) * n.descFactorial (k + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: ⊢ descFactorial 0 0 = 0!

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Hom.Basic

Goal state before:
pp: F : Type u_2
α : Type u_3
β : Type u_4
inst✝⁴ : FunLike F α β
inst✝³ : Group α
inst✝² : CommMagma β
inst✝¹ : LE β
inst✝ : SubmultiplicativeHomClass F α β
f : F
a b : α
⊢ f a ≤ f b * f (a / b)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
⊢ n.succ.descFactorial n.succ = n.succ !

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
⊢ n.descFactorial 0 = 0 ↔ n < 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Hom.Basic

Goal state before:
pp: F : Type u_2
α : Type u_3
β : Type u_4
inst✝⁴ : FunLike F α β
inst✝³ : Group α
inst✝² : AddCommMagma β
inst✝¹ : LE β
inst✝ : MulLEAddHomClass F α β
f : F
a b : α
⊢ f a ≤ f b + f (a / b)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Hom.Basic

Goal state before:
pp: F : Type u_2
α : Type u_3
β : Type u_4
inst✝⁴ : FunLike F α β
inst✝³ : Group α
inst✝² : Mul β
inst✝¹ : LE β
inst✝ : SubmultiplicativeHomClass F α β
f : F
a b c : α
⊢ f (a / c) ≤ f (a / b) * f (b / c)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
⊢ n.descFactorial k.succ = 0 ↔ n < k.succ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Hom.Basic

Goal state before:
pp: F : Type u_2
α : Type u_3
β : Type u_4
inst✝⁴ : FunLike F α β
inst✝³ : Group α
inst✝² : Add β
inst✝¹ : LE β
inst✝ : MulLEAddHomClass F α β
f : F
a b c : α
⊢ f (a / c) ≤ f (a / b) + f (b / c)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
⊢ 0 < n.descFactorial k ↔ k ≤ n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
⊢ (n + 0).descFactorial 0 = (n + 1).ascFactorial 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
⊢ (n + k.succ).descFactorial k.succ = (n + 1).ascFactorial k.succ

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
⊢ (n + 0 - 1).descFactorial 0 = n.ascFactorial 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Hom.Basic

Goal state before:
pp: F : Type u_2
α : Type u_3
β : Type u_4
inst✝⁴ : FunLike F α β
inst✝³ : Group α
inst✝² : AddCommMonoid β
inst✝¹ : PartialOrder β
inst✝ : GroupSeminormClass F α β
f : F
x y : α
⊢ f (x / y) ≤ f x + f y

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
⊢ (n + k.succ - 1).descFactorial k.succ = n.ascFactorial k.succ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Hom.Basic

Goal state before:
pp: F : Type u_2
α : Type u_3
β : Type u_4
inst✝⁴ : FunLike F α β
inst✝³ : Group α
inst✝² : AddCommMonoid β
inst✝¹ : PartialOrder β
inst✝ : GroupSeminormClass F α β
f : F
x y : α
⊢ f (x / y) = f (y / x)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
x✝ : 0 ≤ n
⊢ (n - 0)! * n.descFactorial 0 = n !

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: k : ℕ
h : k.succ ≤ 0
⊢ (0 - k.succ)! * descFactorial 0 k.succ = 0!

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Hom.Basic

Goal state before:
pp: F : Type u_2
β : Type u_4
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
f : F
α : Type u_7
inst✝² : FunLike F α β
inst✝¹ : CommGroup α
inst✝ : GroupSeminormClass F α β
x y : α
⊢ f (x⁻¹ * y)⁻¹ = f (x * y⁻¹)

Tactic:
inv_mul',

Goal state after:
F : Type u_2
β : Type u_4
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
f : F
α : Type u_7
inst✝² : FunLike F α β
inst✝¹ : CommGroup α
inst✝ : GroupSeminormClass F α β
x y : α
⊢ f (x⁻¹⁻¹ / y) = f (x * y⁻¹)