mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: X : Type u_6
Y : Type u_7
F : Type u_8
inst✝³ : Preorder X
inst✝² : Preorder Y
inst✝¹ : EquivLike F X Y
inst✝ : OrderIsoClass F X Y
f : F
⊢ DenselyOrdered X ↔ DenselyOrdered Y

Tactic:
constructor
  · intro H
    refine ⟨fun a b h ↦ ?_⟩
    obtain ⟨c, hc⟩ := exists_between ((map_inv_lt_map_inv_iff f).mpr h)
    exact ⟨f c, by simpa using hc⟩
  · intro H
    refine ⟨fun a b h ↦ ?_⟩
    obtain ⟨c, hc⟩ := exists_between ((map_lt_map_iff f).mpr h)
    exact ⟨EquivLike.inv f c, by simpa using hc⟩

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

Goal state before:
pp: case inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
n : ℕ
a : G
ha : 1 ≤ a
⊢ |a ^ n|ₘ = a ^ n

Tactic:
mabs_of_one_le (one_le_pow_of_one_le' ha n)

Goal state after:
case inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
n : ℕ
a : G
ha : 1 ≤ a
⊢ a ^ n = a ^ n
Module: Mathlib.Algebra.Order.Group.Abs

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b n : G
one_le_a : 1 ≤ a
a_lt_n : a < n
one_le_b : 1 ≤ b
b_lt_n : b < n
⊢ a / b < n ∧ b / a < n

Tactic:
div_lt_iff_lt_mul,

Goal state after:
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b n : G
one_le_a : 1 ≤ a
a_lt_n : a < n
one_le_b : 1 ≤ b
b_lt_n : b < n
⊢ a < n * b ∧ b / a < n
Module: Mathlib.Algebra.Order.Group.Abs

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b c : G
hab : a ≤ b
hbc : b ≤ c
⊢ b ≤ max |a|ₘ |c|ₘ

Tactic:
by simp [hbc.trans (le_mabs_self c)]

Goal state after:
Module: Mathlib.Data.Nat.Cast.Order.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : AddMonoidWithOne α
inst✝² : PartialOrder α
inst✝¹ : AddLeftMono α
inst✝ : ZeroLEOneClass α
n : ℕ
⊢ ↑n ≤ ↑(n + 1)

Tactic:
Nat.cast_succ

Goal state after:
α : Type u_1
inst✝³ : AddMonoidWithOne α
inst✝² : PartialOrder α
inst✝¹ : AddLeftMono α
inst✝ : ZeroLEOneClass α
n : ℕ
⊢ ↑n ≤ ↑n + 1
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
inst✝ : Mul α
x y : WithZero α
hxy : x * y ≠ 0
⊢ unzero hxy = unzero ⋯ * unzero ⋯

Tactic:
simp only [← coe_inj, coe_mul, coe_unzero]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Group α
inst✝ : Group β
e : WithZero α ≃* WithZero β
⊢ LeftInverse (fun x ↦ unzero ⋯) fun x ↦ unzero ⋯

Tactic:
intro; simp

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Group α
inst✝ : Group β
e : WithZero α ≃* WithZero β
⊢ RightInverse (fun x ↦ unzero ⋯) fun x ↦ unzero ⋯

Tactic:
intro; simp

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrderedCommMonoidWithZero α
a b : α
n✝ n : ℕ
hn : n ≠ 0
⊢ Function.Injective fun a ↦ a ^ n

Tactic:
simpa using (pow_left_strictMonoOn₀ (M₀ := α) hn).injOn

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: case refine_3
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
x✝ : Nontrivial αˣ ∧ DenselyOrdered αˣ
H₁ : Nontrivial αˣ
H₂ : DenselyOrdered αˣ
⊢ DenselyOrdered α

Tactic:
· refine ⟨fun x y h ↦ ?_⟩
    lift y to αˣ using (ne_zero_of_lt h).isUnit
    obtain rfl | hx := eq_zero_or_pos x
    · obtain ⟨z, hz⟩ := exists_one_lt' (α := αˣ)
      exact ⟨(y * z⁻¹ : αˣ), by simp, Units.val_lt_val.mpr <| by simp [hz]⟩
    · lift x to αˣ using hx.ne'.isUnit
      obtain ⟨z, hz, hz'⟩ := H₂.dense x y (Units.val_lt_val.mpr h)
      exact ⟨z, by simp [hz, hz']⟩

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

Goal state before:
pp: case h
F : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type ?u.6
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedRing α
inst✝ : Nontrivial α
bounded : ∀ (x : α), ∃ n, x ≤ ↑n
below : ∀ (x : α), ∃ n, ↑n ≤ x
x : α
n : ℕ
hn : x ≤ ↑n
⊢ x ≤ ↑↑n

Tactic:
exact_mod_cast hn

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

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
inst✝ : IsStrictOrderedRing R
ha : a ≤ 0
⊢ a = 0 → ⌊a⌋₊ = 0

Tactic:
by
    rintro rfl
    exact floor_zero

Goal state after:
Module: Mathlib.Algebra.Ring.Invertible

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
a b : R
inst✝² : Invertible a
inst✝¹ : Invertible b
inst✝ : Invertible (a + b)
⊢ 1 = 1 + (1 + ⅟b * a) + ⅟a * b ↔ 1 = 1 + 1 + ⅟b * a + ⅟a * b

Tactic:
← add_assoc

Goal state after:
R : Type u_1
inst✝³ : Ring R
a b : R
inst✝² : Invertible a
inst✝¹ : Invertible b
inst✝ : Invertible (a + b)
⊢ 1 = 1 + 1 + ⅟b * a + ⅟a * b ↔ 1 = 1 + 1 + ⅟b * a + ⅟a * b
Module: Mathlib.Algebra.Order.Ring.Basic

Goal state before:
pp: R : Type u_3
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x y : R
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
ih : k + 1 ≠ 0 → x ^ (k + 1) + y ^ (k + 1) ≤ (x + y) ^ (k + 1)
hn : k + 1 + 1 ≠ 0
n : ℕ := k.succ
h1 : 0 ≤ x * y ^ n + y * x ^ n
h2 : 0 ≤ x + y
⊢ x * x ^ n + y * y ^ n + x * y ^ n + y * x ^ n = x * x ^ n + (y * y ^ n + x * y ^ n) + y * x ^ n

Tactic:
← add_assoc

Goal state after:
R : Type u_3
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x y : R
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
ih : k + 1 ≠ 0 → x ^ (k + 1) + y ^ (k + 1) ≤ (x + y) ^ (k + 1)
hn : k + 1 + 1 ≠ 0
n : ℕ := k.succ
h1 : 0 ≤ x * y ^ n + y * x ^ n
h2 : 0 ≤ x + y
⊢ x * x ^ n + y * y ^ n + x * y ^ n + y * x ^ n = x * x ^ n + y * y ^ n + x * y ^ n + y * x ^ n
Module: Mathlib.Algebra.Group.Int.Units

Goal state before:
pp: u : ℤ
⊢ IsUnit u ↔ u = 1 ∨ u = -1

Tactic:
refine ⟨fun h ↦ isUnit_eq_one_or h, fun h ↦ ?_⟩
  rcases h with (rfl | rfl)
  · exact isUnit_one
  · exact ⟨⟨-1, -1, by decide, by decide⟩, rfl⟩

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

Goal state before:
pp: case succ
α : Type u_1
inst✝² : CommRing α
inst✝¹ : LinearOrder α
a b : α
inst✝ : IsOrderedRing α
n : ℕ
⊢ |a - b| * |geomSum a b n| ≤ |a - b| * (↑(n + 1) * max |a| |b| ^ n)

Tactic:
Nat.cast_succ

Goal state after:
case succ
α : Type u_1
inst✝² : CommRing α
inst✝¹ : LinearOrder α
a b : α
inst✝ : IsOrderedRing α
n : ℕ
⊢ |a - b| * |geomSum a b n| ≤ |a - b| * ((↑n + 1) * max |a| |b| ^ n)
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : R
n : ℕ
hn : n ≠ 0
hne : Even n ∧ ¬Odd n
⊢ a ^ n = b ^ n ↔ a = b ∨ a = -b ∧ Even n

Tactic:
by simp only [*, and_true, ← abs_eq_abs,
    ← pow_left_inj₀ (abs_nonneg a) (abs_nonneg b) hn, hne.1.pow_abs]

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

Goal state before:
pp: α : Type u_1
inst✝ : GeneralizedHeytingAlgebra α
a b : α
⊢ IsGreatest {w | w ⊓ a ≤ b} (a ⇨ b)

Tactic:
by
  simp [IsGreatest, mem_upperBounds]

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

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b : α
ha : a < 0
hb : b < 0
⊢ a ≤ 1 / b ↔ b ≤ 1 / a

Tactic:
by
  simpa using le_inv_of_neg ha hb

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

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
⊢ 0 < a / b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

Tactic:
by
  simp only [division_def, mul_pos_iff, inv_pos, inv_lt_zero]

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

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
B ε : α
hε : 0 < ε
n : ℕ
⊢ ∃ δ > 0, ∀ (q r : α), |r| ≤ B → |q - r| ≤ δ → |q ^ n - r ^ n| < ε

Tactic:
by
  wlog! B_pos : 0 < B generalizing B
  · have ⟨δ, δ_pos, cont⟩ := this 1 zero_lt_one
    exact ⟨δ, δ_pos, fun q r hr ↦ cont q r (hr.trans (B_pos.trans zero_le_one))⟩
  have pos : 0 < 1 + ↑n * (B + 1) ^ (n - 1) := zero_lt_one.trans_le <| le_add_of_nonneg_right <|
    mul_nonneg n.cast_nonneg <| (pow_pos (B_pos.trans <| lt_add_of_pos_right _ zero_lt_one) _).le
  refine ⟨min 1 (ε / (1 + n * (B + 1) ^ (n - 1))), lt_min zero_lt_one (div_pos hε pos),
    fun q r hr hqr ↦ (abs_pow_sub_pow_le ..).trans_lt ?_⟩
  rw [le_inf_iff, le_div_iff₀ pos, mul_one_add, ← mul_assoc] at hqr
  obtain h | h := (abs_nonneg (q - r)).eq_or_lt
  · simpa only [← h, zero_mul] using hε
  refine (lt_of_le_of_lt ?_ <| lt_add_of_pos_left _ h).trans_le hqr.2
  gcongr
  · exact mul_nonneg (abs_nonneg _) n.cast_nonneg
  · exact (abs_nonneg _).trans le_sup_left
  refine max_le ?_ (hr.trans <| le_add_of_nonneg_right zero_le_one)
  exact add_sub_cancel r q ▸ (abs_add_le ..).trans (add_le_add hr hqr.1)

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

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → β
l₁ : List α
l₂ : List γ
⊢ (∃ l, Forall₂ (fun a c ↦ R a (f c)) l₁ l ∧ l <+ l₂) → ∃ l, Forall₂ R l₁ l ∧ l <+ map f l₂

Tactic:
rintro ⟨l1, h1, h2⟩
    use l1.map f
    simp [h1, h2.map]

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

Goal state before:
pp: M : Type u_4
N : Type u_5
inst✝³ : Monoid M
inst✝² : Monoid N
l : List M
F : Type u_8
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
f : F
⊢ foldr (fun x y ↦ f x * y) (f 1) l = f (foldr (fun x1 x2 ↦ x1 * x2) 1 l)

Tactic:
exact l.foldr_hom f (fun x y => (map_mul f x y).symm)

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
a : α
n : ℤ
⊢ zpow' a n = 0 ↔ a = 0

Tactic:
obtain rfl | hn := eq_or_ne n 0
  · simp [zpow']
  · simp [zpow', zpow_eq_zero_iff hn]
    tauto

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: case hn
α : Type u_1
inst✝ : GroupWithZero α
a : α
n : ℕ
hn : n ≠ 0
⊢ ↑n ≠ 0

Tactic:
exact_mod_cast hn

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

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
x y : α
hx : x ∈ l
h : idxOf x l = idxOf y l
⊢ x = y

Tactic:
rw [← getElem_idxOf (idxOf_lt_length_iff.mpr hx)]

Goal state after:
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
x y : α
hx : x ∈ l
h : idxOf x l = idxOf y l
⊢ l[idxOf x l] = y
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
β : Type v
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : β → α → m β
b : β
l : List α
h :
  ∀ (mb : m β),
    (do
        let b ← mb
        foldlM f b l) =
      foldl
        (fun mb a ↦ do
          let b ← mb
          f b a)
        mb l
⊢ foldlM f b l =
    foldl
      (fun mb a ↦ do
        let b ← mb
        f b a)
      (pure b) l

Tactic:
simp [← h (pure b)]

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

Goal state before:
pp: α : Type u
p : α → Prop
ys✝ : List α
head✝ : α
tail✝ : List α
⊢ Forall p (head✝ :: tail✝ ++ ys✝) ↔ Forall p (head✝ :: tail✝) ∧ Forall p ys✝

Tactic:
simp [forall_append, and_assoc]

Goal state after:
Module: Mathlib.Algebra.Field.Rat

Goal state before:
pp: q : ℚ≥0
⊢ ↑q = ↑q.num / ↑q.den

Tactic:
rw [← NNRat.den_coe, ← Int.cast_natCast q.num, ← NNRat.num_coe]; exact (num_div_den _).symm

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

Goal state before:
pp: q : ℚ≥0
⊢ ↑q * ↑↑(↑q).den = ↑↑q.num

Tactic:
← num_coe

Goal state after:
q : ℚ≥0
⊢ ↑q * ↑↑(↑q).den = ↑(↑q).num
Module: Mathlib.Algebra.Divisibility.Units

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
u : αˣ
x✝ : a ∣ b * ↑u
c : α
eq : b * ↑u = a * c
⊢ b = a * c * ↑u⁻¹

Tactic:
← eq,

Goal state after:
α : Type u_1
inst✝ : Monoid α
a b : α
u : αˣ
x✝ : a ∣ b * ↑u
c : α
eq : b * ↑u = a * c
⊢ b = b * ↑u * ↑u⁻¹
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: case pos
a b : ℤ
b0 : b = 0
⊢ ↑(a /. b).den ∣ b

Tactic:
simp [b0]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
s : Set β
f : β → α
⊢ IsLUB (f '' s) (⨆ x ∈ s, f x)

Tactic:
by
  simpa only [range_comp, Subtype.range_coe, iSup_subtype'] using!
    @isLUB_iSup α s _ (f ∘ fun x => (x : β))

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

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
ι : Sort u_8
κ : ι → Sort u_9
f : (i : ι) ×' κ i → α
c : α
⊢ ⨆ ij, f ij ≤ c ↔ ⨆ i, ⨆ j, f ⟨i, j⟩ ≤ c

Tactic:
simp only [iSup_le_iff, PSigma.forall]

Goal state after:
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : Lattice α
a b : α
h : a ≤ b
⊢ [[a, b]] = Icc a b

Tactic:
by rw [uIcc, inf_eq_left.2 h, sup_eq_right.2 h]

Goal state after:
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ b < a ∧ a ≤ c ∨ c < a ∧ a ≤ b → a < b ∧ b ≤ c ∨ c < b ∧ b ≤ a → a = b

Tactic:
rintro (⟨_, _⟩ | ⟨_, _⟩) (⟨_, _⟩ | ⟨_, _⟩) <;> apply le_antisymm <;>
    first | assumption | exact le_of_lt ‹_› | exact le_trans ‹_› (le_of_lt ‹_›)

Goal state after:
Module: Mathlib.Order.Interval.Set.OrdConnected

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
he : (range ⇑e).OrdConnected
x y : α
⊢ ⇑e '' Ioo x y = Ioo (e x) (e y)

Tactic:
← e.preimage_Ioo,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
he : (range ⇑e).OrdConnected
x y : α
⊢ ⇑e '' ⇑e ⁻¹' Ioo (e x) (e y) = Ioo (e x) (e y)
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s t : Set α
⊢ IsAntichain r (s ∪ t) ↔ IsAntichain r s ∧ IsAntichain r t ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → rᶜ a b ∧ rᶜ b a

Tactic:
IsAntichain,

Goal state after:
α : Type u_1
r : α → α → Prop
s t : Set α
⊢ (s ∪ t).Pairwise rᶜ ↔ IsAntichain r s ∧ IsAntichain r t ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → rᶜ a b ∧ rᶜ b a
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s t : Set α
⊢ (s ∪ t).Pairwise rᶜ ↔ IsAntichain r s ∧ IsAntichain r t ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → rᶜ a b ∧ rᶜ b a

Tactic:
IsAntichain,

Goal state after:
α : Type u_1
r : α → α → Prop
s t : Set α
⊢ (s ∪ t).Pairwise rᶜ ↔ s.Pairwise rᶜ ∧ IsAntichain r t ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → rᶜ a b ∧ rᶜ b a
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s t : Set α
⊢ (s ∪ t).Pairwise rᶜ ↔ s.Pairwise rᶜ ∧ IsAntichain r t ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → rᶜ a b ∧ rᶜ b a

Tactic:
IsAntichain,

Goal state after:
α : Type u_1
r : α → α → Prop
s t : Set α
⊢ (s ∪ t).Pairwise rᶜ ↔ s.Pairwise rᶜ ∧ t.Pairwise rᶜ ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → rᶜ a b ∧ rᶜ b a
Module: Mathlib.Algebra.Order.Ring.InjSurj

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : Semiring S
inst✝ : PartialOrder S
f : S → R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
mul : ∀ (x y : S), f (x * y) = f x * f y
le : ∀ {x y : S}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : S}, f x < f y ↔ x < y
a : S
ha : 0 < a
b c : S
hbc : b < c
⊢ b * a < c * a

Tactic:
by
    rw [← lt, mul, mul]; refine mul_lt_mul_of_pos_right (lt.2 hbc) ?_; rwa [← zero, lt]

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

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

Tactic:
Nat.mul_left_comm

Goal state after:
n k : ℕ
⊢ (n + 1) * ((n - k) * n.descFactorial k) = (n + 1) * ((n - k) * n.descFactorial k)
Module: Mathlib.Data.Nat.Factorial.Basic

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

Tactic:
Nat.add_sub_cancel

Goal state after:
n k : ℕ
⊢ n * n.succ.ascFactorial k = n * n.succ.ascFactorial k
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: case neg
k m n : ℕ
hkm : k ≤ m
hmn : ¬m ≤ n
⊢ (n - k).descFactorial (m - k) * n.descFactorial k = n.descFactorial m

Tactic:
rw [descFactorial_eq_zero_iff_lt.mpr (show n < m by lia)]
    by_cases hkn : k ≤ n
    · rw [descFactorial_eq_zero_iff_lt.mpr (show n - k < m - k by lia), Nat.zero_mul]
    · rw [descFactorial_eq_zero_iff_lt.mpr (show n < k by lia), Nat.mul_zero]

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

Goal state before:
pp: a b : ℕ+
⊢ ↑(a - b) = if b < a then ↑a - ↑b else 1

Tactic:
by
  change (toPNat' _ : ℕ) = ite _ _ _
  split_ifs with h
  · exact toPNat'_coe (tsub_pos_of_lt h)
  · rw [tsub_eq_zero_iff_le.mpr (le_of_not_gt h : (a : ℕ) ≤ b)]
    rfl

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
⊢ q.num / ↑q.den = n / ↑d

Tactic:
n_eq_c_mul_num,

Goal state after:
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
⊢ q.num / ↑q.den = c * q.num / ↑d
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
a : G
ha : 1 < a
b c : G
⊢ ∃! x, b * a ^ (Equiv.neg ℤ) x ∈ Ico c (c * a)

Tactic:
by
    simpa only [Equiv.neg_apply, mem_Ico, zpow_neg, ← div_eq_mul_inv, le_div_iff_mul_le, one_mul,
      mul_comm c, div_lt_iff_lt_mul, mul_assoc] using existsUnique_zpow_near_of_one_lt' ha (b / c)

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
  simpa [sub_eq_add_neg] using map_add_zsmul f x (-n)

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

Goal state before:
pp: α : Type u_5
β : Type u_6
inst✝¹ : Group α
inst✝ : MulAction α β
⊢ IsCancelSMul α β ↔ ∀ (g : α) (x : β), g • x = x → g = 1

Tactic:
refine ⟨fun H _ _ ↦ IsCancelSMul.eq_one_of_smul, fun H ↦ ⟨fun g h x ↦ ?_⟩⟩

Goal state after:
α : Type u_5
β : Type u_6
inst✝¹ : Group α
inst✝ : MulAction α β
H : ∀ (g : α) (x : β), g • x = x → g = 1
g h : α
x : β
⊢ g • x = h • x → g = h
Module: Mathlib.Algebra.Torsor.Basic

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
p₁ p₂ p : P
h : p₁ /ₛ p = p₂ /ₛ p
⊢ p₁ = p₂

Tactic:
← div_eq_one,

Goal state after:
G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
p₁ p₂ p : P
h : (p₁ /ₛ p) / (p₂ /ₛ p) = 1
⊢ p₁ = p₂
Module: Mathlib.Data.Multiset.Count

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

Tactic:
simp [List.countP_eq_length]

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

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
x : α
t : Multiset α
ih : ∀ {s u : Multiset α}, Rel r s t → Rel r t u → Rel r s u
s u : Multiset α
r1 : Rel r s (x ::ₘ t)
r2 : Rel r (x ::ₘ t) u
⊢ Rel r s u

Tactic:
| cons x t ih =>

Goal state after:
Module: Mathlib.Data.List.Perm.Lattice

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : n ≤ xs.length
n' : ℕ := xs.length - n
h₀ : n = xs.length - n'
⊢ List.drop n xs ~ ys ∩ List.drop n xs

Tactic:
have h₁ : xs.drop n = (xs.reverse.take n').reverse := by
      rw [take_reverse, h₀, reverse_reverse]

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : n ≤ xs.length
n' : ℕ := xs.length - n
h₀ : n = xs.length - n'
h₁ : List.drop n xs = (List.take n' xs.reverse).reverse
⊢ List.drop n xs ~ ys ∩ List.drop n xs
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
finj : Injective f
s t : Multiset α
l₁ l₂ : List α
⊢ List.map f (l₁.diff l₂) ++ List.map f l₂ = (List.map f l₁).diff (List.map f l₂) ++ List.map f l₂

Tactic:
List.map_diff finj

Goal state after:
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
finj : Injective f
s t : Multiset α
l₁ l₂ : List α
⊢ (List.map f l₁).diff (List.map f l₂) ++ List.map f l₂ = (List.map f l₁).diff (List.map f l₂) ++ List.map f l₂
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
⊢ filter p (a ::ₘ s) = (if p a then {a} else 0) + filter p s

Tactic:
by
  split_ifs with h
  · rw [filter_cons_of_pos _ h, singleton_add]
  · rw [filter_cons_of_neg _ h, Multiset.zero_add]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
⊢ t ∪ u + s = s + t ∪ (s + u)

Tactic:
union_add_distrib,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
⊢ t + s ∪ (u + s) = s + t ∪ (s + u)
Module: Mathlib.Data.Finset.Disjoint

Goal state before:
pp: α : Type u_2
a b : α
⊢ Disjoint {a} {b} ↔ a ≠ b

Tactic:
disjoint_singleton_left,

Goal state after:
α : Type u_2
a b : α
⊢ a ∉ {b} ↔ a ≠ b
Module: Mathlib.Data.Finset.Filter

Goal state before:
pp: α : Type u_1
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
s : Finset α
⊢ Disjoint (filter (fun x ↦ p x ∧ ¬q x) s) (filter (fun x ↦ q x ∧ ¬p x) s)

Tactic:
intro _ htp htq

Goal state after:
α : Type u_1
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
s x✝ : Finset α
htp : x✝ ⊆ filter (fun x ↦ p x ∧ ¬q x) s
htq : x✝ ⊆ filter (fun x ↦ q x ∧ ¬p x) s
⊢ x✝ ⊆ ⊥
Module: Mathlib.Data.Finset.Lattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
h : a ∈ s
⊢ {a} ∩ s = {a}

Tactic:
singleton_inter_of_mem h

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
h : a ∈ s
⊢ {a} = {a}
Module: Mathlib.Data.Finset.BooleanAlgebra

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : Nontrivial α
a : α
⊢ {a} ≠ univ

Tactic:
apply SetLike.coe_ne_coe.1

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : Nontrivial α
a : α
⊢ ↑{a} ≠ ↑univ
Module: Mathlib.Data.Fintype.Sets

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Fintype ↑s
t : Finset α
⊢ s.toFinset ⊂ t ↔ s ⊂ ↑t

Tactic:
by
  rw [← Finset.coe_ssubset, coe_toFinset]

Goal state after:
Module: Mathlib.Data.Fintype.Sets

Goal state before:
pp: α : Type u_1
t : Set α
s : Finset α
inst✝ : Fintype ↑t
⊢ s ⊂ t.toFinset ↔ ↑s ⊂ t

Tactic:
by
  rw [← Finset.coe_ssubset, coe_toFinset]

Goal state after:
Module: Mathlib.Data.Fintype.Sets

Goal state before:
pp: α : Type u_1
s t : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑t
⊢ Disjoint s.toFinset t.toFinset ↔ Disjoint s t

Tactic:
simp only [← disjoint_coe, coe_toFinset]

Goal state after:
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
p i : Fin (n + 1)
h : p ≤ i
hp : p ≠ 0
⊢ (p.pred hp).predAbove i = i.pred ⋯

Tactic:
rw [predAbove_of_succ_le _ _ (succ_pred _ _ ▸ h)]

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

Goal state before:
pp: α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
n : ℕ
⊢ P (f n)

Tactic:
induction n using Nat.strong_induction_on with | _ n IH

Goal state after:
case h
α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
n : ℕ
IH : ∀ m < n, P (f m)
⊢ P (f n)
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inl
n : ℕ
p : Fin n
i : Fin (n + 1)
h✝ : i ≠ p.castSucc
h : i < p.castSucc
⊢ p.castSucc.succAbove (i.castPred ⋯) = i

Tactic:
succAbove_castPred_of_lt _ _ h

Goal state after:
case inl
n : ℕ
p : Fin n
i : Fin (n + 1)
h✝ : i ≠ p.castSucc
h : i < p.castSucc
⊢ i = i