mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Tactic.NormNum.Inv

Goal state before:
pp: α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n d : ℕ
inv✝ : Invertible ↑d
⊢ IsRat (↑(Int.ofNat n.succ) * ⅟↑d)⁻¹ (Int.ofNat d) n.succ

Tactic:
have := invertibleOfNonzero (α := α) (Nat.cast_ne_zero.2 (Nat.succ_ne_zero n))

Goal state after:
α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n d : ℕ
inv✝ : Invertible ↑d
this : Invertible ↑n.succ
⊢ IsRat (↑(Int.ofNat n.succ) * ⅟↑d)⁻¹ (Int.ofNat d) n.succ
Module: Mathlib.Tactic.NormNum.Inv

Goal state before:
pp: α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n d : ℕ
inv✝ : Invertible ↑d
⊢ IsRat (↑(-Int.ofNat n.succ) * ⅟↑d)⁻¹ (-Int.ofNat d) n.succ

Tactic:
have := invertibleOfNonzero (α := α) (Nat.cast_ne_zero.2 (Nat.succ_ne_zero n))

Goal state after:
α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n d : ℕ
inv✝ : Invertible ↑d
this : Invertible ↑n.succ
⊢ IsRat (↑(-Int.ofNat n.succ) * ⅟↑d)⁻¹ (-Int.ofNat d) n.succ
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
⊢ ↑(a /. b) = ↑a / ↑b

Tactic:
have b0' : b ≠ 0 := by
    refine mt ?_ b0
    simp +contextual
  rcases e : a /. b with ⟨n, d, h, c⟩
  have d0 : (d : α) ≠ 0 := by
    intro d0
    have dd := den_dvd a b
    rcases show (d : ℤ) ∣ b by rwa [e] at dd with ⟨k, ke⟩
    have : (b : α) = (d : α) * (k : α) := by rw [ke, Int.cast_mul, Int.cast_natCast]
    rw [d0, zero_mul] at this
    contradiction
  rw [mk_eq_divInt] at e
  have := congr_arg ((↑) : ℤ → α)
    ((divInt_eq_divInt_iff b0' <| ne_of_gt <| Int.natCast_pos.2 h.bot_lt).1 e)
  rw [Int.cast_mul, Int.cast_mul, Int.cast_natCast] at this
  rw [eq_comm, cast_def, div_eq_mul_inv, eq_div_iff_mul_eq d0, mul_assoc, (d.commute_cast _).eq,
    ← mul_assoc, this, mul_assoc, mul_inv_cancel₀ b0, mul_one]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
s : Set α
t : Set β
l : α → β → γ
u₁ : β → γ → α
u₂ : α → γ → β
a₀ : α
b₀ : β
h₁ : ∀ (b : β), GaloisConnection (swap l b) (u₁ b)
h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)
ha₀ : ∀ (b : α), a₀ ≤ b ↔ ∀ x ∈ s, x ≤ b
hb₀ : ∀ (b : β), b₀ ≤ b ↔ ∀ x ∈ t, x ≤ b
⊢ ∀ (b : γ), l a₀ b₀ ≤ b ↔ ∀ x ∈ s, ∀ y ∈ t, l x y ≤ b

Tactic:
(h₂ _).le_iff_le,

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
s : Set α
t : Set β
l : α → β → γ
u₁ : β → γ → α
u₂ : α → γ → β
a₀ : α
b₀ : β
h₁ : ∀ (b : β), GaloisConnection (swap l b) (u₁ b)
h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)
ha₀ : ∀ (b : α), a₀ ≤ b ↔ ∀ x ∈ s, x ≤ b
hb₀ : ∀ (b : β), b₀ ≤ b ↔ ∀ x ∈ t, x ≤ b
⊢ ∀ (b : γ), b₀ ≤ u₂ a₀ b ↔ ∀ x ∈ s, ∀ y ∈ t, y ≤ u₂ x b
Module: Mathlib.Order.GaloisConnection.Basic

Goal state before:
pp: α : Type u
β : Type v
l : α → β
u : β → α
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
gi : GaloisInsertion l u
ι : Sort x
p : ι → Prop
f : (i : ι) → p i → β
⊢ l (⨆ i, ⨆ (hi : p i), u (f i hi)) = ⨆ i, ⨆ (hi : p i), f i hi

Tactic:
by
  simp only [iSup_subtype', gi.l_iSup_u]

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

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
s : Set α
h_sup : sSup s = ⊥
hne : s.Nonempty
⊢ s = {⊥}

Tactic:
rw [Set.eq_singleton_iff_nonempty_unique_mem]
  rw [sSup_eq_bot] at h_sup
  exact ⟨hne, h_sup⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
s_ne : s.Nonempty
hs : ∀ x ∈ s, ∃ y ∈ ∅, x ≤ y
ht : ∀ y ∈ ∅, ∃ x ∈ s, y ≤ x
x : α
xs : x ∈ s
⊢ False

Tactic:
by simpa using hs x xs

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

Goal state before:
pp: case right
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
⊢ sSup s ∈ lowerBounds (upperBounds s)

Tactic:
· change ite _ _ _ ∈ _
    split_ifs with h₁ h₂
    · rintro (⟨⟩ | a) ha
      · exact le_rfl
      · exact False.elim (not_top_le_coe a (ha h₁))
    · rintro (⟨⟩ | b) hb
      · exact le_top
      refine coe_le_coe.2 (csSup_le ?_ ?_)
      · rcases hs with ⟨⟨⟩ | b, hb⟩
        · exact absurd hb h₁
        · exact ⟨b, hb⟩
      · intro a ha
        exact coe_le_coe.1 (hb ha)
    · rintro (⟨⟩ | b) hb
      · exact le_rfl
      · exfalso
        apply h₂
        use b
        intro a ha
        exact coe_le_coe.1 (hb ha)

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

Goal state before:
pp: α : Type u_1
ι : Type u_4
s : Set ι
f : ι → Set α
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
h_ne : i ≠ j
t : Set α
hfi : t ⊆ f i
hfj : t ⊆ f j
ht : t.Nonempty
⊢ ∃ i, i ∈ s ∧ ∃ j, j ∈ s ∧ i ≠ j ∧ ∃ x, x ∈ f i ∩ f j

Tactic:
obtain ⟨x, hx⟩ := ht

Goal state after:
α : Type u_1
ι : Type u_4
s : Set ι
f : ι → Set α
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
h_ne : i ≠ j
t : Set α
hfi : t ⊆ f i
hfj : t ⊆ f j
x : α
hx : x ∈ t
⊢ ∃ i, i ∈ s ∧ ∃ j, j ∈ s ∧ i ≠ j ∧ ∃ x, x ∈ f i ∩ f j
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: case inl
α : Type u_1
ι : Type u_4
s : Set ι
inst✝ : LinearOrder ι
f : ι → Set α
h : ¬s.PairwiseDisjoint f
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hne : i ≠ j
x : α
hx₁ : x ∈ f i
hx₂ : x ∈ f j
h_lt : i < j
⊢ ∃ i, i ∈ s ∧ ∃ j, j ∈ s ∧ i < j ∧ ∃ x, x ∈ f i ∩ f j

Tactic:
exact ⟨i, hi, j, hj, h_lt, x, hx₁, hx₂⟩

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

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

Tactic:
map_inv_eq_map

Goal state after:
F : Type u_2
α : Type u_3
β : Type u_4
inst✝⁴ : FunLike F α β
inst✝³ : Group α
inst✝² : AddCommMonoid β
inst✝¹ : PartialOrder β
inst✝ : GroupSeminormClass F α β
f : F
x y : α
⊢ f (y / x) = f (y / x)
Module: Mathlib.Data.Rat.Cast.Lemmas

Goal state before:
pp: case succ
α : Type u_1
inst✝ : DivisionRing α
n : ℕ
⊢ ↑(↑(n + 1)).sign / ↑(n + 1) = (↑(n + 1))⁻¹

Tactic:
Int.sign_eq_one_of_pos (Int.ofNat_succ_pos n),

Goal state after:
case succ
α : Type u_1
inst✝ : DivisionRing α
n : ℕ
⊢ ↑1 / ↑(n + 1) = (↑(n + 1))⁻¹
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
⊢ |x - ↑(round x)| ≤ 1 / 2

Tactic:
round_eq,

Goal state after:
α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
⊢ |x - ↑⌊x + 1 / 2⌋| ≤ 1 / 2
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁹ : Field α
inst✝⁸ : LinearOrder α
inst✝⁷ : IsStrictOrderedRing α
inst✝⁶ : Field β
inst✝⁵ : LinearOrder β
inst✝⁴ : IsStrictOrderedRing β
inst✝³ : FloorRing α
inst✝² : FloorRing β
inst✝¹ : FunLike F α β
inst✝ : RingHomClass F α β
f : F
hf : StrictMono ⇑f
a : α
⊢ round (f a) = round a

Tactic:
round_eq,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁹ : Field α
inst✝⁸ : LinearOrder α
inst✝⁷ : IsStrictOrderedRing α
inst✝⁶ : Field β
inst✝⁵ : LinearOrder β
inst✝⁴ : IsStrictOrderedRing β
inst✝³ : FloorRing α
inst✝² : FloorRing β
inst✝¹ : FunLike F α β
inst✝ : RingHomClass F α β
f : F
hf : StrictMono ⇑f
a : α
⊢ ⌊f a + 1 / 2⌋ = ⌊a + 1 / 2⌋
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
a : R
inst✝ : IsOrderedRing R
z : ℤ
⊢ z ≤ ⌊-a⌋ ↔ z ≤ -⌈a⌉

Tactic:
le_neg,

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
a : R
inst✝ : IsOrderedRing R
z : ℤ
⊢ z ≤ ⌊-a⌋ ↔ ⌈a⌉ ≤ -z
Module: Mathlib.Data.Rat.Floor

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

Tactic:
round_eq,

Goal state after:
α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : ℚ
this : ↑(x + 1 / 2) = ↑x + 1 / 2
⊢ ⌊↑x + 1 / 2⌋ = round x
Module: Mathlib.Data.Rat.Floor

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

Tactic:
round_eq,

Goal state after:
α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : ℚ
this : ↑(x + 1 / 2) = ↑x + 1 / 2
⊢ ⌊↑x + 1 / 2⌋ = ⌊x + 1 / 2⌋
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
⊢ fract a = 0 ∨ fract a = a + 1 - ↑⌈a⌉

Tactic:
by
  rcases eq_or_ne (fract a) 0 with ha | ha
  · exact Or.inl ha
  right
  suffices (⌈a⌉ : R) = ⌊a⌋ + 1 by
    rw [this, ← self_sub_fract]
    abel
  rw [← Int.cast_one, ← Int.cast_add]
  refine congrArg Int.cast (ceil_eq_iff.mpr ⟨?_, _root_.le_of_lt <| by simp⟩)
  rw [cast_add, cast_one, add_tsub_cancel_right, ← self_sub_fract a, sub_lt_self_iff]
  exact ha.symm.lt_of_le (fract_nonneg a)

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
xpos : 0 < x
hx : x ≤ 1
ypos : 0 < y
hy : y < 1
⊢ ∃ n, y ^ (n + 1) < x ∧ x ≤ y ^ n

Tactic:
rcases exists_nat_pow_near (one_le_inv_iff₀.2 ⟨xpos, hx⟩) (one_lt_inv_iff₀.2 ⟨ypos, hy⟩) with
    ⟨n, hn, h'n⟩
  refine ⟨n, ?_, ?_⟩
  · rwa [inv_pow, inv_lt_inv₀ xpos (pow_pos ypos _)] at h'n
  · rwa [inv_pow, inv_le_inv₀ (pow_pos ypos _) xpos] at hn

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

Goal state before:

Tactic:
⌈a⌉ < a + 1 := ceil_lt_add_one _
      _ = a + (b - 1) * (b - 1)⁻¹ := by rw [mul_inv_cancel₀]; positivity
      _ ≤ a + (b - 1) * a := by gcongr
      _ = b * a := by rw [sub_one_mul, add_sub_cancel]

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
ex : ∃ m, y ≤ (↑m * δ) ^ n
m : ℕ := Nat.find ex
m_pos : 0 < m
q : K := ↑m.pred * δ
qny : q ^ n < y
q1y : |q| < max 1 y
⊢ (↑m * δ) ^ n - (y - max x 0) < (↑m * δ) ^ n - ((↑m * δ) ^ n - q ^ n)

Tactic:
refine sub_lt_sub_left ((le_abs_self _).trans_lt <| cont _ _ q1y.le ?_) _
        rw [← Nat.succ_pred_eq_of_pos m_pos, Nat.cast_succ, ← sub_mul,
          add_sub_cancel_left, one_mul, abs_eq_self.mpr (by positivity)]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
l₁ l₂ : List α
f : α → β
hf : Function.Injective f
l : List α
hl_perm : l ~ l₁
hl_sub : l <+ l₂
⊢ map f l₁ <+~ map f l₂

Tactic:
exact ⟨l.map f, hl_perm.map f, hl_sub.map f⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
d : s.Nodup
h : a ∈ s - t
h' : a ∈ t
⊢ count a (s - t) = 0

Tactic:
rw [count_sub a s t, Nat.sub_eq_zero_iff_le]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
d : s.Nodup
h : a ∈ s - t
h' : a ∈ t
⊢ count a s ≤ count a t
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: α : Type u
β : Type v
l₁ : List α
l₂ : List β
d₁ : l₁.Nodup
d₂ : l₂.Nodup
a₁ a₂ : α
n : a₁ ≠ a₂
x : α × β
h₁ : x ∈ (fun a ↦ map (Prod.mk a) l₂) a₁
h₂ : x ∈ (fun a ↦ map (Prod.mk a) l₂) a₂
⊢ False

Tactic:
rcases mem_map.1 h₁ with ⟨b₁, _, rfl⟩
        rcases mem_map.1 h₂ with ⟨b₂, mb₂, ⟨⟩⟩
        exact n rfl

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

Goal state before:
pp: α : Type u
l₁ : List α
σ : α → Type u_1
l₂ : (a : α) → List (σ a)
d₁ : l₁.Nodup
d₂ : ∀ (a : α), (l₂ a).Nodup
a₁ a₂ : α
n : a₁ ≠ a₂
x : (a : α) × σ a
h₁ : x ∈ (fun a ↦ map (Sigma.mk a) (l₂ a)) a₁
h₂ : x ∈ (fun a ↦ map (Sigma.mk a) (l₂ a)) a₂
⊢ False

Tactic:
rcases mem_map.1 h₁ with ⟨b₁, _, rfl⟩
        rcases mem_map.1 h₂ with ⟨b₂, mb₂, ⟨⟩⟩
        exact n rfl

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

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

Tactic:
simp only [eq_nil_iff_forall_not_mem, mem_inter_iff, not_and]
  rfl

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
t₁ t₂ : List α
h : t₁.Disjoint t₂
x : α
xs : List α
l_ih : xs ∩ (t₁ ++ t₂) ~ xs ∩ t₁ ++ xs ∩ t₂
h₁ : ¬x ∈ t₁
h₂ : x ∈ t₂
⊢ (x :: xs) ∩ (t₁ ++ t₂) ~ (x :: xs) ∩ t₁ ++ (x :: xs) ∩ t₂

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
t₁ t₂ : List α
h : t₁.Disjoint t₂
x : α
xs : List α
l_ih : xs ∩ (t₁ ++ t₂) ~ xs ∩ t₁ ++ xs ∩ t₂
h₁ : ¬x ∈ t₁
h₂ : ¬x ∈ t₂
⊢ (x :: xs) ∩ (t₁ ++ t₂) ~ (x :: xs) ∩ t₁ ++ (x :: xs) ∩ t₂

Tactic:
· simp only [*, inter_cons_of_notMem, false_or, mem_append, inter_cons_of_mem,
        not_false_iff]
      exact perm_cons_append_cons _ l_ih

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
t₁ t₂ : List α
h : t₁.Disjoint t₂
x : α
xs : List α
l_ih : xs ∩ (t₁ ++ t₂) ~ xs ∩ t₁ ++ xs ∩ t₂
h₁ : ¬x ∈ t₁
h₂ : ¬x ∈ t₂
⊢ (x :: xs) ∩ (t₁ ++ t₂) ~ (x :: xs) ∩ t₁ ++ (x :: xs) ∩ t₂
Module: Mathlib.Data.Finset.Range

Goal state before:
pp: n : ℕ
hn : 1 < n
⊢ (Set.Iio n).Nontrivial

Tactic:
exact ⟨0, by grind, 1, hn, Nat.zero_ne_one⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x : α
s : Finset α
⊢ s ∪ {x} = insert x s

Tactic:
Finset.union_comm,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
x : α
s : Finset α
⊢ {x} ∪ s = insert x s
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
p : α → Prop
inst✝¹ : DecidablePred p
f : α ↪ β
s : Finset α
inst✝ : DecidablePred fun x ↦ ∃ a, p a ∧ f a = x
⊢ map f (filter p s) = {b ∈ map f s | ∃ a, p a ∧ f a = b}

Tactic:
by
  simp [filter_map]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
f : α → β
inst✝ : DecidableEq β
y : β
⊢ #({x ∈ s | f x = y}) ≠ 0 ↔ y ∈ image f s

Tactic:
by
  rw [← Nat.pos_iff_ne_zero, card_pos, fiber_nonempty_iff_mem_image]

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

Goal state before:
pp: case neg
n : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
ha : a.castSucc < i
hb : ¬b.castSucc < i
⊢ i.pred ⋯ ≤ i.castPred ⋯

pp: case pos
n : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
ha : ¬a.castSucc < i
hb : b.castSucc < i
⊢ i.castPred ⋯ ≤ i.pred ⋯

pp: case neg
n : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
ha : ¬a.castSucc < i
hb : ¬b.castSucc < i
⊢ i.castPred ⋯ ≤ i.castPred ⋯

Tactic:
· exact pred_le _

Goal state after:
case pos
n : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
ha : ¬a.castSucc < i
hb : b.castSucc < i
⊢ i.castPred ⋯ ≤ i.pred ⋯

case neg
n : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
ha : ¬a.castSucc < i
hb : ¬b.castSucc < i
⊢ i.castPred ⋯ ≤ i.castPred ⋯
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n : ℕ
u v : Fin n
⊢ ↑↑(u + v) = if ↑u + ↑v < n then ↑↑u + ↑↑v else ↑↑u + ↑↑v - ↑n

Tactic:
by
  rw [Fin.add_def]
  split
  · rw [natCast_emod, Int.emod_eq_of_lt] <;> lia
  · rw [natCast_emod, Int.emod_eq_sub_self_emod, Int.emod_eq_of_lt] <;> lia

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

Goal state before:
pp: n a b : ℕ
han : a < n.succ
hbn : b < n.succ
⊢ ↑a ≤ ↑b ↔ a ≤ b

Tactic:
simp [le_iff_val_le_val, -val_fin_le, Nat.mod_eq_of_lt, han, hbn]

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

Goal state before:
pp: case mpr.refine_2
n : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
H : ∀ (i : Fin n), r (f i.castSucc) (f i.succ)
i : Fin (n + 1)
j : Fin n
ihj : (fun x1 x2 ↦ x1 < x2) i j.castSucc → r (f i) (f j.castSucc)
hij : i < j.succ
⊢ r (f i) (f j.succ)

Tactic:
rw [← le_castSucc_iff] at hij

Goal state after:
case mpr.refine_2
n : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
H : ∀ (i : Fin n), r (f i.castSucc) (f i.succ)
i : Fin (n + 1)
j : Fin n
ihj : (fun x1 x2 ↦ x1 < x2) i j.castSucc → r (f i) (f j.castSucc)
hij : i ≤ j.castSucc
⊢ r (f i) (f j.succ)
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
p i : Fin (n + 1)
h : p < i
⊢ p.succAbove (i.pred ⋯) = i

Tactic:
succAbove_of_lt_succ _ _ (succ_pred _ _ ▸ h),

Goal state after:
n : ℕ
p i : Fin (n + 1)
h : p < i
⊢ (i.pred ⋯).succ = i
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ #(s ∪ t) = #s + #t ↔ Disjoint s t

Tactic:
← card_union_add_card_inter

Goal state after:
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ #(s ∪ t) = #(s ∪ t) + #(s ∩ t) ↔ Disjoint s t
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inl
n : ℕ
p : Fin (n + 1)
i : Fin n
H : i.castSucc < p
⊢ p < p.succAbove i ↔ p ≤ i.castSucc

Tactic:
rw [iff_false_right (Fin.not_le.2 H), succAbove_of_castSucc_lt _ _ H]
    exact Fin.not_lt.2 <| Fin.le_of_lt H

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

Goal state before:
pp: k : ℕ
i : Fin k
⊢ idxOf i (finRange k) = ↑i

Tactic:
by
  simpa using (nodup_finRange k).idxOf_getElem i

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

Goal state before:
pp: case pos
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
i : Fin n
y : α i.succ
j : Fin n
h : j = i
⊢ tail (update q i.succ y) j = update (tail q) i y j

Tactic:
rw [h]
    simp [tail]

Goal state after:
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₀)
i : Fin n
hi : x i = snoc x x₀ (last n)
⊢ False

Tactic:
← @snoc_castSucc n (fun i ↦ α) x₀ x i,

Goal state after:
case refine_2
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
h : Injective (snoc x x₀)
i : Fin n
hi : snoc x x₀ i.castSucc = snoc x x₀ (last n)
⊢ False
Module: Mathlib.Data.List.Sort

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l : List α
h : ∀ (b : α), b ∈ l → r a b
x✝ : List α
hi : insertionSort r l = x✝
⊢ orderedInsert r a x✝ = a :: x✝

Tactic:
cases hi : insertionSort r l with

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

Goal state before:
pp: case mpr
α : Type u_1
l : List α
x : α
⊢ (∃ n m x_1, x = l.get n ∧ x = l.get m) →
    ∃ f, ∀ (ix : Fin (replicate 2 x).length), (replicate 2 x).get ix = l.get (f ix)

Tactic:
rintro ⟨n, m, hnm, h, h'⟩

Goal state after:
case mpr
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
⊢ ∃ f, ∀ (ix : Fin (replicate 2 x).length), (replicate 2 x).get ix = l.get (f ix)
Module: Mathlib.Data.List.Sort

Goal state before:
pp: case neg
α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
a b : α
l : List α
h : Pairwise r (b :: l)
h' : ¬r a b
⊢ ∀ (b' : α), b' ∈ List.orderedInsert r a l → r b b'

Tactic:
intro b' bm

Goal state after:
case neg
α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
a b : α
l : List α
h : Pairwise r (b :: l)
h' : ¬r a b
b' : α
bm : b' ∈ List.orderedInsert r a l
⊢ r b b'
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
inst✝ : Infinite α
n : ℕ
⊢ ∃ s, #s = n + 1

Tactic:
by
    classical
    obtain ⟨s, rfl⟩ := exists_card_eq n
    obtain ⟨a, ha⟩ := s.exists_notMem
    exact ⟨insert a s, card_insert_of_notMem ha⟩

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

Goal state before:
pp: case inl
α : Type u_1
R : α → α → Prop
inst✝ : Std.Refl R
l : List α
h : Pairwise R l
a : Fin l.length
hab : a ≤ a
⊢ R (l.get a) (l.get a)

pp: case inr
α : Type u_1
R : α → α → Prop
inst✝ : Std.Refl R
l : List α
h : Pairwise R l
a b : Fin l.length
hab : a ≤ b
hlt : a < b
⊢ R (l.get a) (l.get b)

Tactic:
exacts [refl _, (pairwise_iff_get.1 h) _ _ hlt]

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

Goal state before:
pp: case inr.inr
α : Type u
r : α → α → Prop
inst✝¹ : IsOrderConnected α r
inst✝ : Std.Trichotomous r
a : α
l₁ : List α
b : α
l₂ l₃ : List α
h : Lex r l₁ l₃
ab : r b a
⊢ Lex r (a :: l₁) (b :: l₂) ∨ Lex r (b :: l₂) (a :: l₃)

Tactic:
· exact Or.inr (rel ab)

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

Goal state before:
pp: α : Type u
a : α
l : List α
n m : ℕ
⊢ (l ++ [a]).rotate' (n + m) = (a :: l).rotate' (n + 1 + m)

Tactic:
Nat.add_right_comm,

Goal state after:
α : Type u
a : α
l : List α
n m : ℕ
⊢ (l ++ [a]).rotate' (n + m) = (a :: l).rotate' (n + m + 1)
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
n k : ℕ
hk : k < l.length
⊢ k = (l.length - n % l.length + k + n % l.length) % l.length

Tactic:
Nat.add_right_comm,

Goal state after:
α : Type u
l : List α
n k : ℕ
hk : k < l.length
⊢ k = (l.length - n % l.length + n % l.length + k) % l.length
Module: Mathlib.Data.Nat.Choose.Basic

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

Tactic:
Nat.add_right_comm _ _ (_ * _),

Goal state after:
n k : ℕ
⊢ (n + 1 + 1) * (n + 1).choose (k + 1) = (n + 1) * n.choose k + (n + 1) * n.choose (k + 1) + (n + 1).choose (k + 1)
Module: Mathlib.Data.List.OffDiag

Goal state before:
pp: α : Type u_1
l : List α
this : DecidableEq α := Classical.decEq α
a : α
h : ¬List.count a l ≤ 1
⊢ ¬(List.count a l * List.count a l - if a = a then List.count a l else 0) ≤ 1

Tactic:
rw [Nat.not_le] at h

Goal state after:
α : Type u_1
l : List α
this : DecidableEq α := Classical.decEq α
a : α
h : 1 < List.count a l
⊢ ¬(List.count a l * List.count a l - if a = a then List.count a l else 0) ≤ 1
Module: Mathlib.Data.Fintype.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
s : Finset α
t : Finset β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
⊢ s ×ˢ t = univ ↔ s = univ ∧ t = univ

Tactic:
simp [eq_univ_iff_forall, forall_and]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a✝ : α
r : ⦃a : α⦄ → δ a → δ a → Prop
b₁ b₂ : δ a✝
f₁ f₂ : (a' : α) → a' ∈ m → δ a'
hb : r b₁ b₂
hf : ∀ (a : α) (ha : a ∈ m), r (f₁ a ha) (f₂ a ha)
a : α
ha : a ∈ a✝ ::ₘ m
H : a = a✝
⊢ r (⋯ ▸ b₁) (⋯ ▸ b₂)

Tactic:
cases H

Goal state after:
case pos.refl
α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a : α
r : ⦃a : α⦄ → δ a → δ a → Prop
b₁ b₂ : δ a
f₁ f₂ : (a' : α) → a' ∈ m → δ a'
hb : r b₁ b₂
hf : ∀ (a : α) (ha : a ∈ m), r (f₁ a ha) (f₂ a ha)
ha : a ∈ a ::ₘ m
⊢ r (⋯ ▸ b₁) (⋯ ▸ b₂)
Module: Mathlib.Data.Finset.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ Disjoint ({x ∈ s ×ˢ t | p x.1 ∧ q x.2}) ({x ∈ s ×ˢ t | ¬p x.1 ∧ ¬q x.2})

Tactic:
apply Finset.disjoint_filter_filter'

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ Disjoint (fun x ↦ p x.1 ∧ q x.2) fun x ↦ ¬p x.1 ∧ ¬q x.2
Module: Mathlib.Data.Nat.Choose.Basic

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

pp: case zero.succ
n✝ : ℕ
⊢ ascFactorial 0 (n✝ + 1) = (n✝ + 1)! * (0 + (n✝ + 1) - 1).choose (n✝ + 1)

Tactic:
· rw [ascFactorial_zero, choose_zero_right, factorial_zero, Nat.mul_one]

Goal state after:
case zero.succ
n✝ : ℕ
⊢ ascFactorial 0 (n✝ + 1) = (n✝ + 1)! * (0 + (n✝ + 1) - 1).choose (n✝ + 1)
Module: Mathlib.Algebra.Group.Action.Hom

Goal state before:
pp: M✝ : Type u_1
N : Type u_2
α : Type u_3
inst✝⁵ : Monoid M✝
inst✝⁴ : MulAction M✝ α
R : Type u_4
S : Type u_5
M : Type u_6
inst✝³ : Monoid R
inst✝² : MulAction R M
inst✝¹ : Monoid S
inst✝ : SMul S M
f : R →* S
hf : Surjective ⇑f
hsmul : ∀ (c : R) (x : M), f c • x = c • x
a b : R
x : M
⊢ (f a * f b) • x = f a • f b • x

Tactic:
by simp only [← f.map_mul, hsmul, mul_smul]

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

Goal state before:
pp: M : Type u_3
A : Type u_4
inst✝² : Monoid M
inst✝¹ : SetLike A M
inst✝ : SubmonoidClass A M
S : A
x : M
hx : x ∈ S
n : ℕ
⊢ x ^ n * x ∈ S

Tactic:
exact mul_mem (pow_mem hx n) hx

Goal state after: