mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
q r : ℚ
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(q.den * r.den) = ↑q.num / ↑q.den + ↑r.num / ↑r.den

pp: case hb
α : Type u_3
inst✝ : DivisionRing α
q r : ℚ
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑(q.den * r.den) ≠ 0

Tactic:
mul_comm r.num,

Goal state after:
α : Type u_3
inst✝ : DivisionRing α
q r : ℚ
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑(q.num * ↑r.den + ↑q.den * r.num) / ↑(q.den * r.den) = ↑q.num / ↑q.den + ↑r.num / ↑r.den

case hb
α : Type u_3
inst✝ : DivisionRing α
q r : ℚ
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑(q.den * r.den) ≠ 0
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a₂ c₂ : R
ea₁ b c₁ : ℕ
xa₁ : R
x✝¹ : ea₁ * b = c₁
x✝ : a₂ ^ b = c₂
⊢ (xa₁ ^ ea₁ * a₂) ^ b = xa₁ ^ c₁ * c₂

Tactic:
subst_vars; simp [_root_.mul_pow, pow_mul]

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

Goal state before:
pp: R : Type u
inst✝⁶ : NonAssocSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : CanonicallyOrderedAdd R
inst✝³ : Sub R
inst✝² : OrderedSub R
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : AddLeftReflectLE R
a b : R
⊢ a * (b - 1) = a * b - a

Tactic:
mul_tsub,

Goal state after:
R : Type u
inst✝⁶ : NonAssocSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : CanonicallyOrderedAdd R
inst✝³ : Sub R
inst✝² : OrderedSub R
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : AddLeftReflectLE R
a b : R
⊢ a * b - a * 1 = a * b - a
Module: Mathlib.Algebra.Order.Ring.Canonical

Goal state before:
pp: R : Type u
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : CanonicallyOrderedAdd R
inst✝³ : Sub R
inst✝² : OrderedSub R
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : AddLeftReflectLE R
a b : R
⊢ a * a - b * b = (a + b) * (a - b)

Tactic:
mul_tsub,

Goal state after:
R : Type u
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : CanonicallyOrderedAdd R
inst✝³ : Sub R
inst✝² : OrderedSub R
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : AddLeftReflectLE R
a b : R
⊢ a * a - b * b = (a + b) * a - (a + b) * b
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_2
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : SMul R α
r : R
a b t c : α
x✝² : a = b
x✝¹ : ∀ (x : α), r • x = t * x
x✝ : t * b = c
⊢ r • a = c

Tactic:
by
  subst_vars
  simp [*]

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

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
b : α
hs : s.Nonempty
hb : ∀ a ∈ s, a ≤ b
⊢ sSup s ≤ b

Tactic:
exact csSup_le hs hb

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

Goal state before:
pp: α : Type u_1
inst✝² : DivisionRing α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
num den : ℕ
ra : IsNNRat a num den
⊢ IsNNRat |a| num den

Tactic:
obtain ⟨ha1, rfl⟩ := ra
  refine ⟨ha1, abs_of_nonneg ?_⟩
  apply mul_nonneg
  · exact Nat.cast_nonneg' num
  · simp only [invOf_eq_inv, inv_nonneg, Nat.cast_nonneg]

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

Goal state before:
pp: K : Type u_5
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
m : ℚ
n : ℤ
⊢ ↑m ≤ ↑n ↔ ↑m ≤ ↑↑n

Tactic:
cast_intCast

Goal state after:
K : Type u_5
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
m : ℚ
n : ℤ
⊢ ↑m ≤ ↑n ↔ ↑m ≤ ↑n
Module: Mathlib.Data.Rat.Cast.Order

Goal state before:
pp: K : Type u_5
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
m : ℤ
n : ℚ
⊢ ↑m ≤ ↑n ↔ ↑↑m ≤ ↑n

Tactic:
cast_intCast

Goal state after:
K : Type u_5
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
m : ℤ
n : ℚ
⊢ ↑m ≤ ↑n ↔ ↑m ≤ ↑n
Module: Mathlib.Data.Rat.Cast.Order

Goal state before:
pp: K : Type u_5
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
m : ℚ
n : ℤ
⊢ ↑m < ↑n ↔ ↑m < ↑↑n

Tactic:
cast_intCast

Goal state after:
K : Type u_5
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
m : ℚ
n : ℤ
⊢ ↑m < ↑n ↔ ↑m < ↑n
Module: Mathlib.Data.Rat.Cast.Order

Goal state before:
pp: K : Type u_5
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
m : ℤ
n : ℚ
⊢ ↑m < ↑n ↔ ↑↑m < ↑n

Tactic:
cast_intCast

Goal state after:
K : Type u_5
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
m : ℤ
n : ℚ
⊢ ↑m < ↑n ↔ ↑m < ↑n
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✝¹.mul db ≤ num✝.mul da) = true
h✝ : ↑(num✝¹.mul db) ≤ ↑(num✝.mul da)
ha : 0 ≤ ⅟↑da
hb : 0 ≤ ⅟↑db
h : ⅟↑db * (↑(num✝¹.mul db) * ⅟↑da) ≤ ⅟↑db * (↑(num✝.mul da) * ⅟↑da)
⊢ ↑num✝¹ * ⅟↑da ≤ ↑num✝ * ⅟↑db

Tactic:
rw [← mul_assoc, Nat.commute_cast] at h

Goal state after:
α : Type u_1
inst✝² : Semiring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
num✝¹ num✝ da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h✝¹ : decide (num✝¹.mul db ≤ num✝.mul da) = true
h✝ : ↑(num✝¹.mul db) ≤ ↑(num✝.mul da)
ha : 0 ≤ ⅟↑da
hb : 0 ≤ ⅟↑db
h : ↑(num✝¹.mul db) * ⅟↑db * ⅟↑da ≤ ⅟↑db * (↑(num✝.mul da) * ⅟↑da)
⊢ ↑num✝¹ * ⅟↑da ≤ ↑num✝ * ⅟↑db
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
h✝ : ↑(num✝¹ * db) < ↑(num✝ * da)
ha : 0 < ⅟↑da
hb : 0 < ⅟↑db
h : ⅟↑db * (↑(num✝¹ * db) * ⅟↑da) < ⅟↑db * (↑(num✝ * da) * ⅟↑da)
⊢ ↑num✝¹ * ⅟↑da < ↑num✝ * ⅟↑db

Tactic:
rw [← mul_assoc, Nat.commute_cast] at h

Goal state after:
α : 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
h✝ : ↑(num✝¹ * db) < ↑(num✝ * da)
ha : 0 < ⅟↑da
hb : 0 < ⅟↑db
h : ↑(num✝¹ * db) * ⅟↑db * ⅟↑da < ⅟↑db * (↑(num✝ * da) * ⅟↑da)
⊢ ↑num✝¹ * ⅟↑da < ↑num✝ * ⅟↑db
Module: Mathlib.Algebra.Order.Group.PosPart

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

Tactic:
by
  simp [oneLePart, leOnePart]

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

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

Tactic:
simp at hn

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
  rw [sq, ← mul_div_div_cancel, oneLePart_mul_leOnePart, oneLePart_div_leOnePart]

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 rw [descFactorial_zero, Nat.mul_one, Nat.sub_zero]

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

Goal state before:
pp: ⊢ ascFactorial = ascFactorialBinary

Tactic:
ext n k

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

Goal state before:
pp: ⊢ descFactorial = descFactorialBinary

Tactic:
ext n k

Goal state after:
n k : ℕ
⊢ n.descFactorial k = n.descFactorialBinary k
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: case pos
a b : ℕ+
h : b < a
⊢ ↑a - ↑b ≤ ↑a

pp: case neg
a b : ℕ+
h : ¬b < a
⊢ 1 ≤ ↑a

Tactic:
· exact Nat.sub_le a b

Goal state after:
case neg
a b : ℕ+
h : ¬b < a
⊢ 1 ≤ ↑a
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: m k : ℕ+
⊢ ↑(m.mod k) + m.div k * ↑k = ↑m

Tactic:
rw [mul_comm]
  exact mod_add_div _ _

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

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝⁴ : CommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective fun x ↦ a ^ x
hlt : 1 < a
⊢ False

Tactic:
· rcases exists_between hlt with ⟨b, hb, hba⟩
    rcases ha b with ⟨k, rfl⟩
    suffices 0 < k ∧ k < 1 by lia
    simp_rw [← zpow_lt_zpow_iff_right hlt]
    simp_all

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

Goal state before:
pp: K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
x y : K
inst✝ : ExistsAddOfLE K
hx : 0 < x
hy : y < 1
⊢ ∃ n, y ^ n < x

Tactic:
by_cases! y_pos : y ≤ 0

Goal state after:
case pos
K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
x y : K
inst✝ : ExistsAddOfLE K
hx : 0 < x
hy : y < 1
y_pos : y ≤ 0
⊢ ∃ n, y ^ n < x

case neg
K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
x y : K
inst✝ : ExistsAddOfLE K
hx : 0 < x
hy : y < 1
y_pos : 0 < y
⊢ ∃ n, y ^ n < x
Module: Mathlib.Algebra.Torsor.Defs

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

Tactic:
rw [mul_smul, sdiv_smul, sdiv_smul, sdiv_smul]

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

Goal state before:
pp: K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
n : ℕ
hn : n ≠ 0
x y : K
h : x < y
hy : 0 < y
δ : K
δ_pos : δ > 0
cont : ∀ (q r : K), |r| ≤ max 1 y → |q - r| ≤ δ → |q ^ n - r ^ n| < y - max x 0
⊢ ∃ m, y ≤ (↑m * δ) ^ n

Tactic:
have ⟨m, hm⟩ := exists_nat_ge (y / δ + 1 / δ)

Goal state after:
K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
n : ℕ
hn : n ≠ 0
x y : K
h : x < y
hy : 0 < y
δ : K
δ_pos : δ > 0
cont : ∀ (q r : K), |r| ≤ max 1 y → |q - r| ≤ δ → |q ^ n - r ^ n| < y - max x 0
m : ℕ
hm : y / δ + 1 / δ ≤ ↑m
⊢ ∃ m, y ≤ (↑m * δ) ^ n
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: α : Type u_1
s t : Multiset α
a : α
hs : ¬a ∈ s
⊢ a ∈ t ∧ s ≤ t → a ::ₘ s ≤ t

Tactic:
rintro ⟨h₁, h₂⟩

Goal state after:
α : Type u_1
s t : Multiset α
a : α
hs : ¬a ∈ s
h₁ : a ∈ t
h₂ : s ≤ t
⊢ a ::ₘ s ≤ t
Module: Mathlib.Data.Multiset.Replicate

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
n : ℕ
_l : List α
⊢ n ≤ count a (Quot.mk (⇑(isSetoid α)) _l) ↔ replicate n a ≤ Quot.mk (⇑(isSetoid α)) _l

Tactic:
by
    simp only [quot_mk_to_coe'', coe_count]
    exact replicate_sublist_iff.symm.trans replicate_le_coe.symm

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

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

Tactic:
by
    convert! List.count_erase_of_ne ab (l := l) <;> rw [← coe_count] <;> simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
t : Multiset α
a : α
s : Multiset α
ih : 0 - s = 0
⊢ 0 - a ::ₘ s = 0

Tactic:
simp [ih]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Inhabited α
l✝ : List α
a : α
l : List α
⊢ (a :: l).dedup.headI = if (a :: l).headI ∈ (a :: l).tail then (a :: l).tail.dedup.headI else (a :: l).headI

Tactic:
by_cases ha : a ∈ l <;> simp [ha, List.dedup_cons_of_mem]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Inhabited α
l✝ : List α
a : α
l : List α
⊢ (a :: l).dedup.tail = if (a :: l).headI ∈ (a :: l).tail then (a :: l).tail.dedup.tail else (a :: l).tail.dedup

Tactic:
by_cases ha : a ∈ l <;> simp [ha, List.dedup_cons_of_mem]

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

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

Tactic:
induction l with grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
ih : ∀ {l₂ : List α}, tail✝.bagInter l₂ <+ tail✝ ∩ l₂
l₂ : List α
h✝ : head✝ ∈ l₂
⊢ head✝ ∈ l₂

Tactic:
by assumption

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a : α
x✝ : a ∈ s ∧ a ∈ t
h₁ : a ∈ s
h₂ : a ∈ t
⊢ a ∈ s ∩ t

Tactic:
rw [← cons_erase h₁, cons_inter_of_pos _ h₂]; apply mem_cons_self

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ s ∩ (t ∪ s) = s

Tactic:
rw [inter_comm, union_inter_cancel_right]

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

Goal state before:
pp: α : Type u_1
p : α → Prop
s : Finset { x // p x }
a : α
h : a ∈ map (Embedding.subtype fun x ↦ p x) s
⊢ p a

Tactic:
by
  rcases mem_map.1 h with ⟨x, _, rfl⟩
  exact x.2

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
l : List α
P : α → Prop
inst✝ : DecidablePred P
h : l.Nodup
⊢ #(Finset.filter P l.toFinset) = countP (fun b ↦ decide (P b)) l

Tactic:
l.countP_eq_length_filter,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
l : List α
P : α → Prop
inst✝ : DecidablePred P
h : l.Nodup
⊢ #(Finset.filter P l.toFinset) = (List.filter (fun b ↦ decide (P b)) l).length
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ last n
⊢ i.castPred hi ≤ j ↔ i ≤ j.castSucc

Tactic:
rw [← castSucc_le_castSucc_iff, castSucc_castPred]

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

Goal state before:
pp: n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ last n
⊢ j ≤ i.castPred hi ↔ j.castSucc ≤ i

Tactic:
rw [← castSucc_le_castSucc_iff, castSucc_castPred]

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

Goal state before:
pp: case neg
n : ℕ
inst✝ : NeZero n
i : Fin (n + 1)
hi : ¬i = 0
⊢ predAbove 0 i = i.pred hi

Tactic:
· rw [predAbove_zero_of_ne_zero hi]

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: m n : ℕ
α : Fin (n + 1) → Sort u
x✝ : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α i.succ
i : Fin n
y : α i.succ
z : α 0
motive : ((i : Fin n.succ) → α i) → Sort v
cons : (x₀ : α 0) → (x : (i : Fin n) → α i.succ) → motive (Fin.cons x₀ x)
x : (i : Fin n.succ) → α i
⊢ motive (Fin.cons (x 0) (tail x)) = motive x

Tactic:
by rw [cons_self_tail]

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

Goal state before:
pp: case inr
α : Type u_1
p : (s : Finset α) → s.Nonempty → Prop
h₀ : ∀ (a : α), p {a} ⋯
h₁ : ∀ ⦃s : Finset α⦄ (hs : s.Nontrivial), (∀ (t : Finset α) (ht : t.Nonempty), t ⊂ s → p t ht) → p s ⋯
s : Finset α
hs✝ : s.Nonempty
hs : s.Nontrivial
⊢ p s hs✝

Tactic:
· refine h₁ hs fun t ht hts ↦ ?_
      have := card_lt_card hts
      exact ht.strong_induction h₀ h₁

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case succ.cast
n : ℕ
β : Sort u_2
a : β
q : Fin n → β
b : β
j : Fin n
⊢ cons a (snoc q b) j.castSucc.succ = snoc (cons a q) b j.castSucc.succ

Tactic:
rw [cons_succ]

Goal state after:
case succ.cast
n : ℕ
β : Sort u_2
a : β
q : Fin n → β
b : β
j : Fin n
⊢ snoc q b j.castSucc = snoc (cons a q) b j.castSucc.succ
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case refine_2
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
h : Injective (snoc x x₀)
⊢ ¬x₀ ∈ Set.range x

Tactic:
· rintro ⟨i, hi⟩
    rw [← @snoc_last n (fun i ↦ α) x₀ x, ← @snoc_castSucc n (fun i ↦ α) x₀ x i,
      h.eq_iff] at hi
    exact ne_last_of_lt i.castSucc_lt_last hi

Goal state after:
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝ : DecidableEq β
f : α → β
s : Set α
t : Finset β
hfs : SurjOn f s ↑t
u : Set α
hus : u ⊆ s
hf : InjOn f u
himg : f '' u = ↑t
⊢ (f '' u).Finite

Tactic:
simp [himg]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
l : List α
f g : α → List β
h : ∀ (a : α), a ∈ l → f a <+ g a
⊢ flatMap f l <+ flatMap g l

Tactic:
induction l with grind

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case inr.inr
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : ↑j ≠ ↑k
h : ↑j < ↑k
⊢ j.contractNth op g k = g (j.succAbove k)

Tactic:
rwa [j.succAbove_of_le_castSucc, contractNth_apply_of_gt]

Goal state after:
case inr.inr.h
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : ↑j ≠ ↑k
h : ↑j < ↑k
⊢ j ≤ k.castSucc
Module: Mathlib.Data.Finset.Fold

Goal state before:
pp: case insert
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha✝ : Std.Associative op
f : α → β
b : β
s✝ : Finset α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∧ r x z
c : β
a : α
s : Finset α
ha : a ∉ s
IH : r c (fold op b f s) ↔ r c b ∧ ∀ x ∈ s, r c (f x)
⊢ r c (fold op b f (insert a s)) ↔ r c b ∧ ∀ x ∈ insert a s, r c (f x)

Tactic:
rw [Finset.fold_insert ha, hr, IH, ← and_assoc, @and_comm (r c (f a)), and_assoc]
      simp

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
inst✝ : Std.Symm R
hl : Pairwise R l
this : Std.Symm fun x y ↦ x ≠ y → R x y
⊢ ∀ ⦃a : α⦄, a ∈ l → ∀ ⦃b : α⦄, b ∈ l → a ≠ b → R a b

Tactic:
apply Pairwise.forall_of_forall

Goal state after:
case H₁
α : Type u_1
R : α → α → Prop
l : List α
inst✝ : Std.Symm R
hl : Pairwise R l
this : Std.Symm fun x y ↦ x ≠ y → R x y
⊢ ∀ (x : α), x ∈ l → x ≠ x → R x x

case H₂
α : Type u_1
R : α → α → Prop
l : List α
inst✝ : Std.Symm R
hl : Pairwise R l
this : Std.Symm fun x y ↦ x ≠ y → R x y
⊢ Pairwise (fun x y ↦ x ≠ y → R x y) l
Module: Mathlib.Data.List.Pairwise

Goal state before:
pp: α : Type u_1
R : α → α → Prop
a : α
inst✝¹ : Inhabited α
inst✝ : Std.Refl R
head✝ : α
tail✝ : List α
h : Pairwise R (head✝ :: tail✝)
a✝ : Mem a tail✝
⊢ a ∈ tail✝

Tactic:
by assumption

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

Goal state before:
pp: case inr
α : Type u
l : List α
n : ℕ
hl : 0 < l.length
⊢ l.rotate n = drop (n % l.length) l ++ take (n % l.length) l

Tactic:
rw [← rotate_eq_drop_append_take (n.mod_lt hl).le, rotate_mod]

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

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
l₁ l₂ : List M
h : l₁ <+ l₂
⊢ l₁.prod ∣ l₂.prod

Tactic:
obtain ⟨l, hl⟩ := h.exists_perm_append
  rw [hl.prod_eq, prod_append]
  exact dvd_mul_right _ _

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

Goal state before:
pp: case cons
α : Type u_1
β : Type v
f : α → β
a✝ : Multiset α
s✝ : Multiset (Multiset α)
ih : map f s✝.join = (map (map f) s✝).join
⊢ map f (a✝ ::ₘ s✝).join = (map (map f) (a✝ ::ₘ s✝)).join

Tactic:
simp [ih]

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

Goal state before:
pp: case cons
α : Type u_1
inst✝ : CommMonoid α
a✝ : Multiset α
s✝ : Multiset (Multiset α)
ih : s✝.join.prod = (map prod s✝).prod
⊢ (a✝ ::ₘ s✝).join.prod = (map prod (a✝ ::ₘ s✝)).prod

Tactic:
simp [ih]

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

Goal state before:
pp: case cons
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a✝ : Multiset α
s✝ : Multiset (Multiset α)
ih : filter p s✝.join = (map (filter p) s✝).join
⊢ filter p (a✝ ::ₘ s✝).join = (map (filter p) (a✝ ::ₘ s✝)).join

Tactic:
simp [ih]

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

Goal state before:
pp: case cons
α : Type u_1
β : Type v
f : α → Option β
a✝ : Multiset α
s✝ : Multiset (Multiset α)
ih : filterMap f s✝.join = (map (filterMap f) s✝).join
⊢ filterMap f (a✝ ::ₘ s✝).join = (map (filterMap f) (a✝ ::ₘ s✝)).join

Tactic:
simp [ih]

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

Goal state before:
pp: α : Type u
l : List α
n : ℕ
⊢ l.reverse ~r (l.rotate n).reverse

Tactic:
exact ⟨_, (reverse_rotate _ _).symm⟩

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

Goal state before:
pp: ι : Type u_2
κ : Type u_3
M : Type u_5
inst✝ : CommMonoid M
m✝ : Multiset ι
n : Multiset κ
f : ι → κ → M
a : ι
m : Multiset ι
ih : (map (fun a ↦ (map (fun b ↦ f a b) n).prod) m).prod = (map (fun b ↦ (map (fun a ↦ f a b) m).prod) n).prod
⊢ (map (fun a ↦ (map (fun b ↦ f a b) n).prod) (a ::ₘ m)).prod =
    (map (fun b ↦ (map (fun a ↦ f a b) (a ::ₘ m)).prod) n).prod

Tactic:
simp [ih]

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

Goal state before:
pp: α : Type u
l l' : List α
⊢ l.reverse ~r l' ↔ l ~r l'.reverse

Tactic:
by
  constructor <;>
    · intro h
      simpa using h.reverse

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

Goal state before:
pp: α : Type u_1
β : Type v
b : β
s : Multiset α
t : Multiset β
⊢ s ×ˢ (b ::ₘ t) = map (fun a ↦ (a, b)) s + s ×ˢ t

Tactic:
by
  simp [SProd.sprod, product]

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

Goal state before:
pp: α : Type u_1
β : Type v
s t : Multiset α
u : Multiset β
⊢ (s + t) ×ˢ u = s ×ˢ u + t ×ˢ u

Tactic:
by
  simp [SProd.sprod, product]

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

Goal state before:
pp: m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
⊢ (m * (p + 1) + (p + 1)).choose (p + 1) * (m * (p + 1))! * (p + 1)! = (m * (p + 1) + (p + 1))!

Tactic:
rw [add_choose_mul_factorial_mul_factorial]

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

Goal state before:
pp: m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
⊢ (m * (p + 1) + p)! * ((p + 1) * (m + 1)) = (m * (p + 1) + p).choose p * (m * (p + 1))! * p ! * ((p + 1) * (m + 1))

Tactic:
rw [add_choose_mul_factorial_mul_factorial]

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

Goal state before:
pp: case zero
k : ℕ
⊢ ascFactorial 0 k = k ! * (0 + k - 1).choose k

Tactic:
cases k

Goal state after:
case zero.zero
⊢ ascFactorial 0 0 = 0! * (0 + 0 - 1).choose 0

case zero.succ
n✝ : ℕ
⊢ ascFactorial 0 (n✝ + 1) = (n✝ + 1)! * (0 + (n✝ + 1) - 1).choose (n✝ + 1)
Module: Mathlib.Data.Nat.Choose.Basic

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

Tactic:
apply Nat.mul_left_cancel k.factorial_pos
  rw [← ascFactorial_eq_factorial_mul_choose]
  exact (Nat.mul_div_cancel' <| factorial_dvd_ascFactorial _ _).symm

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

Goal state before:
pp: case inr
r n : ℕ
b : n < r
⊢ n.choose r ≤ n.choose (n / 2)

Tactic:
rw [choose_eq_zero_of_lt b]
    apply zero_le

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

Goal state before:
pp: a c : ℕ
⊢ a.choose c ≤ a.succ.choose c

Tactic:
by
  cases c <;> grind

Goal state after:
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: case refine_2.inr
α : Type u_1
β : Type u_2
s : Set α
t : Set β
h : t.Infinite ∧ s.Nonempty
⊢ (s ×ˢ t).Infinite

Tactic:
· exact h.1.prod_right h.2

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

Goal state before:
pp: E : Type u_4
F : Type u_5
G : Type u_6
inst✝³ : Monoid E
inst✝² : Monoid F
inst✝¹ : MulAction F G
inst✝ : IsPretransitive F G
f : E →* F
hf : Surjective ⇑f
x✝ : MulAction E G := compHom G f
x y : G
⊢ ∃ g, g • x = y

Tactic:
obtain ⟨m, rfl⟩ : ∃ m : F, m • x = y := exists_smul_eq F x y

Goal state after:
E : Type u_4
F : Type u_5
G : Type u_6
inst✝³ : Monoid E
inst✝² : Monoid F
inst✝¹ : MulAction F G
inst✝ : IsPretransitive F G
f : E →* F
hf : Surjective ⇑f
x✝ : MulAction E G := compHom G f
x : G
m : F
⊢ ∃ g, g • x = m • x
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
inst✝ : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ i, s i)
inhabited_h : Inhabited ι
y : β
x : ι → α
hx : ∀ (i : ι), x i ∈ s i
hy : ∀ (i : ι), f (x i) = y
i : ι
this : x default = x i
⊢ x i ∈ s i

Tactic:
apply hx

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : Mul α
inst✝ : IsRightCancelMul α
s t : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a ≠ b
c : α
hc : c ∈ t
⊢ (s * t).Nontrivial

Tactic:
exact ⟨a * c, mul_mem_mul ha hc, b * c, mul_mem_mul hb hc, by simpa⟩

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

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
p₁ p₂ : Submonoid M
⊢ (∀ ⦃x : M⦄, x ∈ p₁ ⊓ p₂ → x ∈ ⊥) ↔ ∀ {x : M}, x ∈ p₁ → x ∈ p₂ → x = 1

Tactic:
mem_inf,

Goal state after:
M : Type u_1
inst✝ : MulOneClass M
p₁ p₂ : Submonoid M
⊢ (∀ ⦃x : M⦄, x ∈ p₁ ∧ x ∈ p₂ → x ∈ ⊥) ↔ ∀ {x : M}, x ∈ p₁ → x ∈ p₂ → x = 1