mathlib-initiative/mathlib-tactics huggingface dataset:
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:
by
  rw [← map_inv_eq_map, inv_mul', inv_inv, div_eq_mul_inv]

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

Goal state before:
pp: case zero
⊢ 2 ^ 0 * 0! ≤ (2 * 0)!

Tactic:
simp

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

Goal state before:
pp: case case1
n✝ : ℕ
⊢ n✝.ascFactorial 0 = 1

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Rat.Cast.Lemmas

Goal state before:
pp: case zero
α : Type u_1
inst✝ : DivisionRing α
⊢ ↑(↑0)⁻¹ = (↑0)⁻¹

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Rat.Cast.Lemmas

Goal state before:
pp: case inl
K : Type u_1
inst✝ : DivisionSemiring K
q : ℚ≥0
hq : ↑q.num ≠ 0
n : ℕ
⊢ ↑(q ^ ↑n) = ↑q ^ ↑n

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
⊢ (if ↑2 * fract x < 1 then ⌊x⌋ + ⌊fract x⌋ else ⌈↑⌊x⌋ + fract x⌉) = (2 * ⌊x⌋ + ⌊↑2 * fract x⌋ + 1) / 2

Tactic:
ceil_intCast_add,

Goal state after:
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
⊢ (if ↑2 * fract x < 1 then ⌊x⌋ + ⌊fract x⌋ else ⌊x⌋ + ⌈fract x⌉) = (2 * ⌊x⌋ + ⌊↑2 * fract x⌋ + 1) / 2
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: case pos.e_a
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
h : 2 * fract x < 1
⊢ 0 = (0 + 1) / 2

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: case pos.e_a.hb
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
h : 2 * fract x < 1
⊢ 0 ≤ fract x

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: case h
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
h : 2 * fract x < 1
⊢ 1 ≤ 2

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: case neg.e_a
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
H : ⌊2 * fract x⌋ = 1
h : fract x ≤ 0
⊢ 2 * 0 < 1

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: n : ℕ
property✝ : 0 < n + 2
x✝ : ⟨n + 2, property✝⟩ ≠ 1
⊢ 0 < n + 1

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: case inl
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
hx : fract x < 1 - fract x
⊢ |x - ↑(if fract x < 1 - fract x then ⌊x⌋ else ⌈x⌉)| = if fract x < 1 - fract x then fract x else 1 - fract x

Tactic:
if_pos hx,

Goal state after:
case inl
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
hx : fract x < 1 - fract x
⊢ |x - ↑⌊x⌋| = if fract x < 1 - fract x then fract x else 1 - fract x
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: case inl
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
hx : fract x < 1 - fract x
⊢ |x - ↑⌊x⌋| = if fract x < 1 - fract x then fract x else 1 - fract x

Tactic:
if_pos hx,

Goal state after:
case inl
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
hx : fract x < 1 - fract x
⊢ |x - ↑⌊x⌋| = fract x
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: case pos
m k : ℕ+
h : ↑m % ↑k = 0
hm : ↑k * (↑m / ↑k) > 0
⊢ ↑k ≤ ↑k * (↑m / ↑k) ∧ ↑k ≤ ↑k

Tactic:
simp

Goal state after:
case pos
m k : ℕ+
h : ↑m % ↑k = 0
hm : ↑k * (↑m / ↑k) > 0
⊢ 1 ≤ ↑m / ↑k
Module: Mathlib.Tactic.Ring.RingNF

Goal state before:
pp: R : Type u_2
inst✝ : Ring R
a b : R
⊢ a * -b = -(a * b)

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.Ring.RingNF

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
⊢ Nat.rawCast 0 = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.Ring.RingNF

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
⊢ Nat.rawCast 1 = 1

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.Ring.RingNF

Goal state before:
pp: n : ℕ
R : Type u_2
inst✝ : Ring R
⊢ (Int.negOfNat n).rawCast = -n.rawCast

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.Ring.RingNF

Goal state before:
pp: n d : ℕ
R : Type u_2
inst✝ : DivisionSemiring R
⊢ NNRat.rawCast n d = n.rawCast / d.rawCast

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.Ring.RingNF

Goal state before:
pp: n d : ℕ
R : Type u_2
inst✝ : DivisionRing R
⊢ Rat.rawCast (Int.negOfNat n) d = (Int.negOfNat n).rawCast / d.rawCast

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: case inl
α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
m : ℕ
⊢ |↑m / ↑0 - ↑(round (↑m / ↑0))| = ↑(min (m % 0) (0 - m % 0)) / ↑0

Tactic:
simp

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

Goal state before:
pp: case inl
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a : k
hn : 0 ≤ 0
⊢ ⌊a / ↑0⌋ = ⌊a⌋ / 0

Tactic:
simp

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

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
m : ℤ
⊢ a + ↑m - ↑⌊a + ↑m⌋ = fract a

Tactic:
simp

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

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
m : ℕ
⊢ a + ↑m - ↑⌊a + ↑m⌋ = fract a

Tactic:
simp

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

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
m : ℤ
⊢ a - ↑m - ↑⌊a - ↑m⌋ = fract a

Tactic:
simp

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

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
n : ℕ
⊢ a - ↑n - ↑⌊a - ↑n⌋ = fract a

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b : R
Hcomm : Commute a b
ha : 0 ≤ a
Hsq : 0 ≤ b ^ 2
Hsq' : 0 ≤ (a + b) ^ 2
H : 0 ≤ 2 * a + b
⊢ a ^ 0 + ↑0 * a ^ (0 - 1) * b ≤ (a + b) ^ 0

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b : R
Hcomm : Commute a b
ha : 0 ≤ a
Hsq : 0 ≤ b ^ 2
Hsq' : 0 ≤ (a + b) ^ 2
H : 0 ≤ 2 * a + b
⊢ a ^ 1 + ↑1 * a ^ (1 - 1) * b ≤ (a + b) ^ 1

Tactic:
simp

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

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
h : fract a = b
⊢ 0 ≤ fract a ∧ fract a < 1 ∧ ∃ z, a - fract a = ↑z

Tactic:
exact ⟨fract_nonneg _, fract_lt_one _, ⟨⌊a⌋, sub_sub_cancel _ _⟩⟩

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

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
⊢ a - a = ↑0

Tactic:
simp

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

Goal state before:
pp: case h
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
⊢ fract a * ↑0 - fract (a * ↑0) = ↑0

Tactic:
simp

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

Goal state before:
pp: case inl
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
m : ℕ
⊢ fract (↑m / ↑0) = ↑(m % 0) / ↑0

Tactic:
simp

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

Goal state before:
pp: case inl
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
m : ℤ
⊢ fract (↑m / ↑0) = ↑(m % ↑0) / ↑0

Tactic:
simp

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

Goal state before:
pp: k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
q : ℤ := ⌈↑m₀ / ↑n⌉
m₁ : ℤ := q * ↑n - ↑m₀
hm₁ : 0 ≤ m₁
⊢ fract (↑(-↑m₀) / ↑n) = fract (-↑m₀ / ↑n)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: case inl
n : ℤ
⊢ (↑n / ↑0).num / ↑(↑n / ↑0).den = n / ↑0

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : ℚ
⊢ ↑(x + 1 / 2) = ↑x + 1 / 2

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: R : Type u_3
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
m : ℕ
⊢ ⌊↑m⌋ = ↑m

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: R : Type u_3
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
m : ℤ
⊢ ⌊↑m⌋ = ↑m

Tactic:
simp

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

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
n : ℕ
⊢ ↑n = ↑↑n

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: R : Type u_3
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
m : ℕ
⊢ ⌈↑m⌉ = ↑m

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: R : Type u_3
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
m : ℤ
⊢ ⌈↑m⌉ = ↑m

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
inst✝² : AddMonoidWithOne G
inst✝¹ : AddMonoidWithOne H
inst✝ : AddConstMapClass F G H 1 1
f : F
x : G
n : ℕ
⊢ f (x + ↑n) = f x + ↑n

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
inst✝² : AddMonoidWithOne G
inst✝¹ : AddMonoidWithOne H
inst✝ : AddConstMapClass F G H 1 1
f : F
n : ℕ
⊢ f ↑n = f 0 + ↑n

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
inst✝² : AddCommMonoidWithOne G
inst✝¹ : AddMonoidWithOne H
inst✝ : AddConstMapClass F G H 1 1
f : F
n : ℕ
x : G
⊢ f (↑n + x) = f x + ↑n

Tactic:
simp

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

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
ha : fract a ≠ 0
⊢ a < ↑(⌊a⌋ + 1)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
m : ℕ
⊢ fract ↑m = ↑0

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
m : ℤ
⊢ fract ↑m = ↑0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
a : G
b : H
inst✝² : AddGroup G
inst✝¹ : AddGroup H
inst✝ : AddConstMapClass F G H a b
f : F
x : G
n : ℕ
⊢ f (x + ↑n • a) = f x + ↑n • b

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: R : Type u_3
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
m : ℕ
⊢ round ↑m = ↑m

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: R : Type u_3
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
m : ℤ
⊢ round ↑m = ↑m

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
inst✝² : AddGroupWithOne G
inst✝¹ : AddGroupWithOne H
inst✝ : AddConstMapClass F G H 1 1
f : F
x : G
n : ℤ
⊢ f (x + ↑n) = f x + ↑n

Tactic:
simp

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

Goal state before:
pp: R : Type u_3
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
x : R
⊢ ∃ fl, ∀ (z : ℤ), z ≤ fl ↔ ↑z ≤ x

Tactic:
by
  apply exists_floor'
  · obtain ⟨n, hn⟩ := exists_int_lt x
    exact ⟨n, hn.le⟩
  · obtain ⟨n, hn⟩ := exists_int_gt x
    exact ⟨n, hn.le⟩

Goal state after:
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
inst✝² : AddGroupWithOne G
inst✝¹ : AddGroupWithOne H
inst✝ : AddConstMapClass F G H 1 1
f : F
x : G
n : ℤ
⊢ f (x - ↑n) = f x - ↑n

Tactic:
simp

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

Goal state before:

Tactic:
b * a < b * (⌊a⌋ + 1) := by gcongr; apply lt_floor_add_one
    _ ≤ ⌊a⌋ := by
      rwa [_root_.mul_add_one, ← le_sub_iff_add_le', ← one_sub_mul, ← div_le_iff₀' (by linarith),
        ← ceil_le, le_floor]

Goal state after:
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
inst✝² : AddCommGroupWithOne G
inst✝¹ : AddGroupWithOne H
inst✝ : AddConstMapClass F G H 1 1
f : F
n : ℤ
x : G
⊢ f (↑n + x) = f x + ↑n

Tactic:
simp

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

Goal state before:
pp: case inl
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
ha : 1 ≤ 1
⊢ ⌈↑⌈(1 - 1)⁻¹⌉ / 1⌉ = ⌈(1 - 1)⁻¹⌉

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: F : Type u_1
G : Type u_2
H : Type u_3
inst✝⁷ : FunLike F G H
a : G
b : H
inst✝⁶ : AddCommGroup G
inst✝⁵ : LinearOrder G
inst✝⁴ : IsOrderedAddMonoid G
inst✝³ : Archimedean G
inst✝² : AddGroup H
inst✝¹ : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst✝ : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R (f x) (f y)
x y : G
hxy : (fun x1 x2 ↦ x1 < x2) x y
hR : Covariant H H (fun x y ↦ y + x) R
ha' : 0 ≤ a
⊢ R (f x) (f y)

Tactic:
wlog hx : x ∈ Ico l (l + a) generalizing x y

Goal state after:
case inr
F : Type u_1
G : Type u_2
H : Type u_3
inst✝⁷ : FunLike F G H
a : G
b : H
inst✝⁶ : AddCommGroup G
inst✝⁵ : LinearOrder G
inst✝⁴ : IsOrderedAddMonoid G
inst✝³ : Archimedean G
inst✝² : AddGroup H
inst✝¹ : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst✝ : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R (f x) (f y)
x y : G
hxy : (fun x1 x2 ↦ x1 < x2) x y
hR : Covariant H H (fun x y ↦ y + x) R
ha' : 0 ≤ a
this : ∀ (x y : G), x < y → x ∈ Ico l (l + a) → R (f x) (f y)
hx : x ∉ Ico l (l + a)
⊢ R (f x) (f y)

F : Type u_1
G : Type u_2
H : Type u_3
inst✝⁷ : FunLike F G H
a : G
b : H
inst✝⁶ : AddCommGroup G
inst✝⁵ : LinearOrder G
inst✝⁴ : IsOrderedAddMonoid G
inst✝³ : Archimedean G
inst✝² : AddGroup H
inst✝¹ : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst✝ : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R (f x) (f y)
hR : Covariant H H (fun x y ↦ y + x) R
ha' : 0 ≤ a
x y : G
hxy : x < y
hx : x ∈ Ico l (l + a)
⊢ R (f x) (f y)
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: q : ℚ
this : ↑q.num < ↑q.num + (1 - fract q) * ↑q.den
⊢ q * ↑q.den + (1 - fract q) * ↑q.den = ↑q.num + (1 - fract q) * ↑q.den

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑q.num.natAbs = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * ↑q⁻¹.den < ↑q⁻¹.den
coprime_q_denom_q_num : q.den.Coprime q.num.natAbs
⊢ (↑q.den).natAbs = q.den

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Torsor.Defs

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝¹ : Group G
inst✝ : Torsor G P
p p' : P
⊢ (fun x ↦ x⁻¹ • p) ((fun x ↦ p /ₛ x) p') = p'

Tactic:
simp

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

Goal state before:
pp: case neg
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsStrictOrderedRing R
a : R
ha : -1 < a
h : a < 0
⊢ 0 < a + 1

Tactic:
exact neg_lt_iff_pos_add.mp ha

Goal state after:
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝² : Add G
inst✝¹ : Add H
a : G
b : H
K : Type u_3
inst✝ : Add K
c : K
g : H →+c[b, c] K
f : G →+c[a, b] H
⊢ ∀ (x : G), (⇑g ∘ ⇑f) (x + a) = (⇑g ∘ ⇑f) x + c

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : AddCommGroup G
inst✝ : AddCommGroup H
a : G
b : H
x✝¹ : G →+c[a, b] H
x✝ : G
⊢ ((fun f ↦ { toFun := fun x ↦ -f (-x), map_add_const' := ⋯ })
        ((fun f ↦ { toFun := fun x ↦ -f (-x), map_add_const' := ⋯ }) x✝¹))
      x✝ =
    x✝¹ x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Multiset.Defs

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
m : Multiset α
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
l : List α
⊢ (∀ (a : α), a ∈ l → p a) ↔ ∀ (a : α), a ∈ ⟦l⟧ → p a

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Multiset.Defs

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
m : Multiset α
p : α → Prop
inst✝ : DecidablePred p
l : List α
⊢ (∃ a, a ∈ l ∧ p a) ↔ ∃ x, x ∈ ⟦l⟧ ∧ p x

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Multiset.Defs

Goal state before:
pp: α : Type u_1
r : α → α → Prop
l : List α
⊢ ∀ (a : List α), ↑l = ↑a ∧ List.Pairwise r a ↔ l ~ a ∧ List.Pairwise r a

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
s₁ s₂ : Finset α
⊢ ↑s₁ ⊂ ↑s₂ ↔ s₁ ⊂ s₂

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
p : α → Prop
_hp : (a : α) → Decidable (p a)
⊢ (∃ a x, p a) ↔ ∃ a, a ∈ s ∧ p a

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Multiset.Count

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
_l : List α
⊢ 0 < countP p (Quot.mk (⇑(isSetoid α)) _l) ↔ ∃ a, a ∈ Quot.mk (⇑(isSetoid α)) _l ∧ p a

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Torsor.Basic

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝¹ : CommGroup G
inst✝ : Torsor G P
p₁ p₂ p₃ : P
⊢ (p₁ /ₛ p₂) * ((p₃ /ₛ p₁) / (p₃ /ₛ p₂)) = 1

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Torsor.Basic

Goal state before:
pp: G : Type u_3
P : Type u_4
inst✝ : AddGroup G
T : AddTorsor G P
x y : P
⊢ -(x -ᵥ (pointReflection x) y) = -(y -ᵥ x)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
inst✝ : IsEmpty α
⊢ ∀ (a : Multiset α), a = 0

Tactic:
rintro ⟨_ | ⟨a, l⟩⟩

Goal state after:
case mk.nil
α : Type u_1
β : Type v
γ : Type u_2
inst✝ : IsEmpty α
a✝ : Multiset α
⊢ Quot.mk ⇑(isSetoid α) [] = 0

case mk.cons
α : Type u_1
β : Type v
γ : Type u_2
inst✝ : IsEmpty α
a✝ : Multiset α
a : α
l : List α
⊢ Quot.mk (⇑(isSetoid α)) (a :: l) = 0
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case mk.mk
α : Type u_1
a : α
s✝ : Multiset α
l₁ : List α
t✝ : Multiset α
l₂ : List α
⊢ a ::ₘ Quot.mk (⇑(isSetoid α)) l₁ = a ::ₘ Quot.mk (⇑(isSetoid α)) l₂ ↔
    Quot.mk (⇑(isSetoid α)) l₁ = Quot.mk (⇑(isSetoid α)) l₂

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: α : Type u_1
s : Multiset α
l✝ : List α
hl : Quot.mk (⇑(isSetoid α)) l✝ ≠ 0
a : α
l : List α
x✝ : Quot.mk (⇑(isSetoid α)) (a :: l) ≠ 0
⊢ a ∈ Quot.mk (⇑(isSetoid α)) (a :: l)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case refine_2
α : Type u_1
a : α
⊢ 0 ⊂ {a}

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Multiset.Replicate

Goal state before:
pp: case e'_3.h₁
α : Type u_1
inst✝ : DecidableEq α
a b : α
n : ℕ
⊢ b = a ↔ (b == a) = true

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: α : Type u_1
β : Type v
r : α → β → Prop
b : Multiset β
⊢ (0 = 0 ∧ b = 0 ∨ ∃ a b_1 as bs, r a b_1 ∧ Rel r as bs ∧ 0 = a ::ₘ as ∧ b = b_1 ::ₘ bs) ↔ b = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: α : Type u_1
β : Type v
r : α → β → Prop
a : Multiset α
⊢ (a = 0 ∧ 0 = 0 ∨ ∃ a_1 b as bs, r a_1 b ∧ Rel r as bs ∧ a = a_1 ::ₘ as ∧ 0 = b ::ₘ bs) ↔ a = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: case nil
α : Type u
x : α
h : [].Nodup
⊢ [] ≠ [x] ↔ [] = [] ∨ ∃ y, y ∈ [] ∧ y ≠ x

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Set.List

Goal state before:
pp: α : Type u_1
inst✝ : Inhabited α
l : List α
⊢ (range fun n ↦ l.getD n default) = insert default {x | x ∈ l}

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: case neg.inl
α : Type u
x hd : α
hl : [] ≠ [x] ↔ [] = [] ∨ ∃ y, y ∈ [] ∧ y ≠ x
h : [hd].Nodup
⊢ [hd] ≠ [x] ↔ [hd] = [] ∨ ∃ y, y ∈ [hd] ∧ y ≠ x

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case zero
α : Type u_1
β : Type v
r : α → β → Prop
s : Multiset α
t : Multiset β
⊢ ∀ {a : α}, a ∈ 0 → ∃ b, b ∈ 0 ∧ r a b

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: case e'_2
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
l : List α
⊢ count a (erase ⟦l⟧ a) = count a ↑(l.erase a)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: case e'_3
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
l : List α
⊢ count a ⟦l⟧ = count a ↑l

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: case e'_2
α : Type u_1
inst✝ : DecidableEq α
a b : α
ab : a ≠ b
s : Multiset α
l : List α
⊢ count a (erase ⟦l⟧ b) = count a ↑(l.erase b)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: case e'_3
α : Type u_1
inst✝ : DecidableEq α
a b : α
ab : a ≠ b
s : Multiset α
l : List α
⊢ count a ⟦l⟧ = count a ↑l

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a : α
⊢ count a (s + t - t) = count a s

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: case nil
α : Type u
β : Type v
f : α → β
d : (map f []).Nodup
⊢ ∀ ⦃x : α⦄, x ∈ [] → ∀ ⦃y : α⦄, y ∈ [] → f x = f y → x = y

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: α : Type u_1
β : Type v
r : α → β → Prop
as₀ as₁ : Multiset α
⊢ ∀ {bs : Multiset β}, Rel r (0 + as₁) bs ↔ ∃ bs₀ bs₁, Rel r 0 bs₀ ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: α : Type u_1
β : Type v
r : α → β → Prop
as₀ as₁ : Multiset α
a : α
s : Multiset α
ih : ∀ {bs : Multiset β}, Rel r (s + as₁) bs ↔ ∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
b : β
hab : r a b
bs₀ bs₁ : Multiset β
h₀ : Rel r s bs₀
h₁ : Rel r as₁ bs₁
⊢ b ::ₘ (bs₀ + bs₁) = b ::ₘ bs₀ + bs₁

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: α : Type u
l : List α
u : α
⊢ (l.concat u).reverse.Nodup ↔ ¬u ∈ l ∧ l.Nodup

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: case nil
α : Type u
h : [][0]? = [].getLast?
⊢ [].reverse.tail.Nodup ↔ [].tail.Nodup

Tactic:
simp

Goal state after: