mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: case case3
n k : ℕ
ih₁ : n.ascFactorial ((k + 2) / 2) = n.ascFactorialBinary ((k + 2) / 2)
ih₂ : (n + (k + 2) / 2).ascFactorial ((k + 2 + 1) / 2) = (n + (k + 2) / 2).ascFactorialBinary ((k + 2 + 1) / 2)
⊢ n.ascFactorial k.succ.succ =
    n.ascFactorialBinary ((k + 2) / 2) * (n + (k + 2) / 2).ascFactorialBinary ((k + 2 + 1) / 2)

Tactic:
| case3 n k ih₁ ih₂ =>

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

Goal state before:
pp: case pos
n k : ℕ
h : n < k
⊢ n.descFactorial k = 0

Tactic:
rw [descFactorial_of_lt h]

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:
by simp

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

Goal state before:
pp: case mpr
k m : ℕ+
a : ℕ
h : ↑m = ↑k * a
⊢ k ∣ m

Tactic:
obtain ⟨n, rfl⟩ := Nat.exists_eq_succ_of_ne_zero (n := a) <| by
      rintro rfl
      simp only [mul_zero, ne_zero] at h

Goal state after:
case mpr
k m : ℕ+
n : ℕ
h : ↑m = ↑k * n.succ
⊢ k ∣ m
Module: Mathlib.Tactic.Ring.RingNF

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

Tactic:
by 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:
by 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:
by 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:
by 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:
by 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:
by simp

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

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

Tactic:
by
  rcases n.eq_zero_or_pos with (rfl | hn)
  · simp
  have hn' : 0 < (n : α) := by
    norm_cast
  rw [abs_sub_round_eq_min, Nat.cast_min, ← min_div_div_right hn'.le,
    fract_div_natCast_eq_div_natCast_mod, Nat.cast_sub (m.mod_lt hn).le, sub_div, div_self hn'.ne']

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

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a : α
ha : 1 < a
n : ℤ
⊢ a ^ n < a ^ (n + 1)

Tactic:
rw [zpow_add_one]

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a : α
ha : 1 < a
n : ℤ
⊢ a ^ n < a ^ n * a
Module: Mathlib.Algebra.Order.Group.Basic

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a : α
ha : a < 1
n : ℤ
⊢ a ^ (n + 1) < a ^ n

Tactic:
rw [zpow_add_one]

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a : α
ha : a < 1
n : ℤ
⊢ a ^ n * a < a ^ n
Module: Mathlib.Algebra.Order.Group.Basic

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a : α
ha : 1 ≤ a
n : ℤ
⊢ a ^ n ≤ a ^ (n + 1)

Tactic:
rw [zpow_add_one]

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a : α
ha : 1 ≤ a
n : ℤ
⊢ a ^ n ≤ a ^ n * a
Module: Mathlib.Algebra.Order.Group.Basic

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
n : ℤ
hn : 0 < n
a b : α
hab : a < b
⊢ 1 < (b / a) ^ n

Tactic:
exact one_lt_zpow (one_lt_div'.2 hab) hn

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

Goal state before:
pp: R : Type u_4
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
x k : R
hk : 1 < k
n : ℤ
hn : k * x = k * ↑n + 1
hk0 : 0 < k
⊢ k * ↑n ≤ k * x ∧ x < ↑n + 1

Tactic:
← mul_lt_mul_iff_right₀ hk0,

Goal state after:
R : Type u_4
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
x k : R
hk : 1 < k
n : ℤ
hn : k * x = k * ↑n + 1
hk0 : 0 < k
⊢ k * ↑n ≤ k * x ∧ k * x < k * (↑n + 1)
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
z : ℤ
⊢ ↑z - ↑⌊↑z⌋ = 0

Tactic:
rw [floor_intCast]

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
z : ℤ
⊢ ↑z - ↑z = 0
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:
by 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:
by 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
⊢ a - a = ↑0

Tactic:
by 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:
by simp

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

Goal state before:
pp: case inr
n : ℤ
d : ℕ
hd : 0 < d
q : ℚ := ↑n / ↑d
q_eq : q = ↑n / ↑d
c : ℤ
n_eq_c_mul_num : n = c * q.num
d_eq_c_mul_denom : ↑d = c * ↑q.den
⊢ 0 < c * ↑q.den

Tactic:
rwa [← d_eq_c_mul_denom, Int.natCast_pos]

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

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : ℚ
⊢ round ↑x = round x

Tactic:
have : ((x + 1 / 2 : ℚ) : α) = x + 1 / 2 := by simp
  rw [round_eq, round_eq, ← this, floor_cast]

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:
by 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:
by simp

Goal state after:
Module: Mathlib.Tactic.Positivity.Basic

Goal state before:
pp: a : ℤ
ha : 0 < a
⊢ 0 < a / a

Tactic:
Int.ediv_self ha.ne'

Goal state after:
a : ℤ
ha : 0 < a
⊢ 0 < 1
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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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
b : H
inst✝² : AddGroupWithOne G
inst✝¹ : AddGroup H
inst✝ : AddConstMapClass F G H 1 b
f : F
x : G
n : ℤ
⊢ f (x + ↑n) = f x + n • b

Tactic:
by
  rw [← map_add_zsmul f x n, zsmul_one]

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:
by 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:
by 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✝² : AddCommGroupWithOne G
inst✝¹ : AddGroupWithOne H
inst✝ : AddConstMapClass F G H 1 1
f : F
n : ℤ
x : G
⊢ f (↑n + x) = f x + ↑n

Tactic:
by simp

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

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

Tactic:
add_mul

Goal state after:
q : ℚ
this : ↑q.num < ↑q.num + (1 - fract q) * ↑q.den
⊢ q * ↑q.den + (1 - fract q) * ↑q.den = q * ↑q.den + (1 - fract q) * ↑q.den
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:
by 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)
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)
n : ℤ
hny : y - n • a ∈ Ioc l (l + a)
hn : n < 0
⊢ l + a + n • a = l + (n + 1) • a

Tactic:
rw [add_comm n, add_smul, one_smul, add_assoc]

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

Goal state before:
pp: case inl
K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
inst✝ : ExistsAddOfLE K
a b c : K
h : a < b * c
hb₀ : 0 < b
hc₀ : 0 < c
hc₁ : c < 1
ha : a ≤ 0
⊢ ∃ n, a < c ^ n ∧ c ^ n < b

Tactic:
obtain ⟨n, hn⟩ := exists_pow_lt_of_lt_one hb₀ hc₁

Goal state after:
case inl
K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
inst✝ : ExistsAddOfLE K
a b c : K
h : a < b * c
hb₀ : 0 < b
hc₀ : 0 < c
hc₁ : c < 1
ha : a ≤ 0
n : ℕ
hn : c ^ n < b
⊢ ∃ n, a < c ^ n ∧ c ^ n < b
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: q : ℚ
q_pos : 0 < q
⊢ (fract q⁻¹).num < q.num

Tactic:
have q_num_pos : 0 < q.num := Rat.num_pos.mpr q_pos
  -- we will work with the absolute value of the numerator, which is equal to the numerator
  have q_num_abs_eq_q_num : (q.num.natAbs : ℤ) = q.num := Int.natAbs_of_nonneg q_num_pos.le
  set q_inv : ℚ := q.den / q.num with q_inv_def
  have q_inv_eq : q⁻¹ = q_inv := by rw [q_inv_def, inv_def, divInt_eq_div, Int.cast_natCast]
  suffices (q_inv - ⌊q_inv⌋).num < q.num by rwa [q_inv_eq]
  suffices ((q.den - q.num * ⌊q_inv⌋ : ℚ) / q.num).num < q.num by
    simp only [gt_iff_lt, q_inv]
    field_simp
    simp [q_inv, this]
  suffices (q.den : ℤ) - q.num * ⌊q_inv⌋ < q.num by
    -- use that `q.num` and `q.den` are coprime to show that the numerator stays unreduced
    have : ((q.den - q.num * ⌊q_inv⌋ : ℚ) / q.num).num = q.den - q.num * ⌊q_inv⌋ := by
      suffices ((q.den : ℤ) - q.num * ⌊q_inv⌋).natAbs.Coprime q.num.natAbs from
        mod_cast Rat.num_div_eq_of_coprime q_num_pos this
      have tmp := Nat.coprime_sub_mul_floor_rat_div_of_coprime q.reduced.symm
      simpa only [Nat.cast_natAbs, abs_of_nonneg q_num_pos.le] using! tmp
    rwa [this]
  -- to show the claim, start with the following inequality
  have q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * q⁻¹.den < q⁻¹.den := by
    have : q⁻¹.num < (⌊q⁻¹⌋ + 1) * q⁻¹.den := Rat.num_lt_succ_floor_mul_den q⁻¹
    have : q⁻¹.num < ⌊q⁻¹⌋ * q⁻¹.den + q⁻¹.den := by rwa [right_distrib, one_mul] at this
    rwa [← sub_lt_iff_lt_add'] at this
  -- use that `q.num` and `q.den` are coprime to show that q_inv is the unreduced reciprocal
  -- of `q`
  have : q_inv.num = q.den ∧ q_inv.den = q.num.natAbs := by
    have coprime_q_denom_q_num : q.den.Coprime q.num.natAbs := q.reduced.symm
    have : Int.natAbs q.den = q.den := by simp
    rw [← this] at coprime_q_denom_q_num
    rw [q_inv_def]
    constructor
    · exact mod_cast Rat.num_div_eq_of_coprime q_num_pos coprime_q_denom_q_num
    · suffices (((q.den : ℚ) / q.num).den : ℤ) = q.num.natAbs by exact mod_cast this
      rw [q_num_abs_eq_q_num]
      exact mod_cast Rat.den_div_eq_of_coprime q_num_pos coprime_q_denom_q_num
  rwa [q_inv_eq, this.left, this.right, q_num_abs_eq_q_num, mul_comm] at q_inv_num_denom_ineq

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:
by simp

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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by simp

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

Goal state before:
pp: α : Type u_1
m : Multiset α
a : α
r : α → α → Prop
n : ℕ
h : Rel r (replicate n a) m
x : α
hx : x ∈ m
b : α
hb1 : b ∈ replicate n a
hb2 : flip r x b
⊢ r a x

Tactic:
eq_of_mem_replicate hb1

Goal state after:
α : Type u_1
m : Multiset α
a : α
r : α → α → Prop
n : ℕ
h : Rel r (replicate n a) m
x : α
hx : x ∈ m
b : α
hb1 : b ∈ replicate n a
hb2 : flip r x a
⊢ r a x
Module: Mathlib.Data.Set.List

Goal state before:
pp: α : Type u_1
l : List α
⊢ range l.get = {x | x ∈ l}

Tactic:
by
  ext x
  rw [mem_ofPred_eq, mem_iff_get, mem_range]

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

Goal state before:
pp: case mp
α : Type u_1
β : Type v
r : α → β → Prop
a : α
as : Multiset α
bs : Multiset β
⊢ Rel r (a ::ₘ as) bs → ∃ b bs', r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs'

Tactic:
generalize hm : a ::ₘ as = m
    intro h
    induction h generalizing as with
    | zero => simp at hm
    | @cons a' b as' bs ha'b h ih =>
      rcases cons_eq_cons.1 hm with (⟨rfl, rfl⟩ | ⟨_h, cs, eq₁, eq₂⟩)
      · exact ⟨b, bs, ha'b, h, rfl⟩
      · rcases ih eq₂.symm with ⟨b', bs', h₁, h₂, eq⟩
        exact ⟨b', b ::ₘ bs', h₁, eq₁.symm ▸ Rel.cons ha'b h₂, eq.symm ▸ cons_swap _ _ _⟩

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

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

Tactic:
ext a; simp

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

Goal state before:
pp: case refine_2
α : Type u_1
m2 : Multiset α
r : α → α → Prop
a : α
⊢ ∀ (s : Multiset α),
    (∀ {m1 : Multiset α}, (∀ (a b : α), a ∈ m1 → b ∈ s → r a b) → m1.card = s.card → Rel r m1 s) →
      ∀ {m1 : Multiset α},
        (∀ (a_2 b : α), a_2 ∈ m1 → b ∈ a ::ₘ s → r a_2 b) → m1.card = (a ::ₘ s).card → Rel r m1 (a ::ₘ s)

Tactic:
t

Goal state after:
case refine_2
α : Type u_1
m2 : Multiset α
r : α → α → Prop
a : α
t : Multiset α
⊢ (∀ {m1 : Multiset α}, (∀ (a b : α), a ∈ m1 → b ∈ t → r a b) → m1.card = t.card → Rel r m1 t) →
    ∀ {m1 : Multiset α},
      (∀ (a_2 b : α), a_2 ∈ m1 → b ∈ a ::ₘ t → r a_2 b) → m1.card = (a ::ₘ t).card → Rel r m1 (a ::ₘ t)
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:
by 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:
by 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₁
bs₁ : Multiset β
h₁ : Rel r as₁ bs₁
b : β
bs : Multiset β
hab : r a b
h₀ : Rel r s bs
⊢ b ::ₘ bs + bs₁ = b ::ₘ (bs + bs₁)

Tactic:
by simp

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

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ : List α
x✝ : l₁.Nodup
⊢ l₁.diff [] = List.filter (fun x ↦ decide ¬x ∈ []) l₁

Tactic:
by simp

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

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
n : ℕ
x✝ : [].Nodup
⊢ take n [] = List.filter (fun a ↦ elem a (take n [])) []

Tactic:
by simp

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

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
b : α
l : List α
x✝ : (b :: l).Nodup
⊢ take 0 (b :: l) = List.filter (fun a ↦ elem a (take 0 (b :: l))) (b :: l)

Tactic:
by simp

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

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
b : α
l : List α
n : ℕ
hl : (b :: l).Nodup
⊢ elem b (b :: List.filter (fun a ↦ elem a (take n l)) l) = true

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
x : { x // x ∈ s }
⊢ map val (s.attach.erase x) = s.erase ↑x

Tactic:
rw [Multiset.map_erase _ val_injective, attach_map_val]

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

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
r : α → β → Prop
s : Multiset γ
f : γ → α
⊢ ∀ {t : Multiset β}, Rel r (map f 0) t ↔ Rel (fun a b ↦ r (f a) b) 0 t

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
⊢ (l₁ ++ l₂).dedup = l₁ ∪ l₂.dedup

Tactic:
induction l₁ with

Goal state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : (l₁ ++ l₂).dedup = l₁ ∪ l₂.dedup
⊢ (a :: l₁ ++ l₂).dedup = a :: l₁ ∪ l₂.dedup
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l₂ : List α
⊢ [].bagInter l₂ = [] ↔ [] ∩ l₂ = []

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
s : Multiset α
⊢ s.toList.isEmpty = true ↔ s = 0

Tactic:
by simp

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

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

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
_l : List α
⊢ List.filter (fun b ↦ decide (p b)) _l = _l ↔ ∀ (a : α), a ∈ Quot.mk (⇑(isSetoid α)) _l → p a

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
_l : List α
⊢ List.filter (fun b ↦ decide (p b)) _l = [] ↔ ∀ (a : α), a ∈ Quot.mk (⇑(isSetoid α)) _l → ¬p a

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
s : Multiset α
⊢ filter (fun x ↦ True) s = s

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
s : Multiset α
⊢ filter (fun x ↦ False) s = 0

Tactic:
by simp

Goal state after: