mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Bounds.Image

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set (α × β)
p : α × β
H : IsLUB s p
a : α
ha : a ∈ upperBounds (Prod.fst '' s)
⊢ p.1 ≤ a

Tactic:
suffices h : (a, p.2) ∈ upperBounds s from (H.2 h).1

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set (α × β)
p : α × β
H : IsLUB s p
a : α
ha : a ∈ upperBounds (Prod.fst '' s)
⊢ (a, p.2) ∈ upperBounds s
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: α : Type u_3
β : Type u_4
e : α ≃ β
s : Set α
t : Set β
⊢ ⇑e.symm '' t ⊆ s ↔ t ⊆ ⇑e '' s

Tactic:
rw [image_subset_iff, image_eq_preimage_symm]

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

Goal state before:
pp: α : Type u_1
inst✝ : SemilatticeInf α
a b : α
⊢ Iic a ∩ Iic b = Iic (a ⊓ b)

Tactic:
ext x
  simp [Iic]

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

Goal state before:
pp: α : Type u
l : List α
n : ℕ
h : n < l.length
⊢ take 1 (l[n] :: drop (n + 1) l) = [l.get ⟨n, h⟩]

Tactic:
take,

Goal state after:
α : Type u
l : List α
n : ℕ
h : n < l.length
⊢ l[n] :: take 0 (drop (n + 1) l) = [l.get ⟨n, h⟩]
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
⊢ 1 / a ≤ b ↔ 1 / b ≤ a

Tactic:
simpa using inv_le_of_neg ha hb

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
⊢ 1 / a < b ↔ 1 / b < a

Tactic:
by
  simpa using inv_lt_of_neg ha hb

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
hr : BiUnique R
a : α
b : β
h : R a b
a' : α
as : List α
b' : β
bs : List β
h₁ : R a' b'
h₂ : Forall₂ R as bs
⊢ (fun x1 x2 ↦ x1 ∈ x2) a (a' :: as) ↔ (fun x1 x2 ↦ x1 ∈ x2) b (b' :: bs)

Tactic:
simp only [mem_cons]

Goal state after:
α : Type u_1
β : Type u_2
R : α → β → Prop
hr : BiUnique R
a : α
b : β
h : R a b
a' : α
as : List α
b' : β
bs : List β
h₁ : R a' b'
h₂ : Forall₂ R as bs
⊢ a = a' ∨ a ∈ as ↔ b = b' ∨ b ∈ bs
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
n : ℕ
a : α
⊢ l₁.insertIdx n a ~ l₂.insertIdx n a ↔ l₁ ~ l₂

Tactic:
wlog hle : length l₁ ≤ length l₂ generalizing l₁ l₂
  · rw [perm_comm, this (Nat.le_of_not_ge hle), perm_comm]
  cases Nat.lt_or_ge (length l₁) n with
  | inl hn₁ =>
    rw [insertIdx_of_length_lt hn₁]
    cases Nat.lt_or_ge (length l₂) n with
    | inl hn₂ => rw [insertIdx_of_length_lt hn₂]
    | inr hn₂ =>
      apply iff_of_false
      · intro h
        rw [h.length_eq] at hn₁
        grind
      · grind [Perm.length_eq]
  | inr hn₁ =>
    exact perm_insertIdx_iff_of_le hn₁ (Nat.le_trans hn₁ hle) _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → β → Prop
hr : RightUnique r
a : List α
b : List β
h₁ : Forall₂ r a b
c : List α
d : List β
h₂ : Forall₂ r c d
h : a ~ c
this : (flip (Forall₂ r) ∘r Perm ∘r Forall₂ r) b d
⊢ ((flip (Forall₂ r) ∘r Forall₂ r) ∘r Perm) b d

Tactic:
by
    rwa [← forall₂_comp_perm_eq_perm_comp_forall₂, ← Relation.comp_assoc] at this

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

Goal state before:
pp: case swap'
α : Type u_1
β : Type u_2
f : α → β → β
l₁ l₂ : List α
lcomm : LeftCommutative f
x✝ y✝ : α
l₁✝ l₂✝ : List α
h✝ : l₁✝ ~ l₂✝
r : ∀ (b : β), foldr f b l₁✝ = foldr f b l₂✝
b : β
⊢ foldr f b (y✝ :: x✝ :: l₁✝) = foldr f b (x✝ :: y✝ :: l₂✝)

Tactic:
| swap' _ _ _ r =>

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

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
f g : α → List β
a : α
l : List α
IH : flatMap f l ++ flatMap g l ~ flatMap (fun x ↦ f x ++ g x) l
⊢ flatMap f l ++ g a ++ flatMap g l ~ g a ++ (flatMap f l ++ flatMap g l)

Tactic:
← append_assoc

Goal state after:
case cons
α : Type u_1
β : Type u_2
f g : α → List β
a : α
l : List α
IH : flatMap f l ++ flatMap g l ~ flatMap (fun x ↦ f x ++ g x) l
⊢ flatMap f l ++ g a ++ flatMap g l ~ g a ++ flatMap f l ++ flatMap g l
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: M : Type u_4
inst✝ : LeftCancelMonoid M
L L' : List M
h : L.length = L'.length
h' : ∀ (i : ℕ), i ≤ L.length → (take i L).prod = (take i L').prod
i : ℕ
h₁ : i < L.length
h₂ : i < L'.length
this : (take i L').prod * L[i] = (take i L').prod * L'[i]
⊢ L.get ⟨i, h₁⟩ = L'.get ⟨i, h₂⟩

Tactic:
convert! mul_left_cancel this

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

Goal state before:
pp: G : Type u_7
inst✝ : Group G
n : ℕ
f : ℕ → G
⊢ (map (fun k ↦ f k / f (k + 1)) (range n)).prod = f 0 / f n

Tactic:
by
  induction n with
  | zero => exact (div_self' (f 0)).symm
  | succ n h => simp [range_succ, prod_append, map_append, h]

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

Goal state before:
pp: case succ
m k : ℕ+
n : ℕ
⊢ ↑(k.modDivAux (n + 1) (↑m / ↑k)).fst = if n + 1 = 0 then ↑k else n + 1

Tactic:
rw [if_neg n.succ_ne_zero]
    rfl

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

Goal state before:
pp: case succ
m k : ℕ+
n : ℕ
⊢ (k.modDivAux (n + 1) (↑m / ↑k)).snd = if n + 1 = 0 then ↑m / ↑k - 1 else ↑m / ↑k

Tactic:
rw [if_neg n.succ_ne_zero]
    rfl

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

Goal state before:
pp: q₁ q₂ : ℚ
⊢ q₁.num * q₂.num = (q₁ * q₂).num * ↑((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den))

Tactic:
mul_num

Goal state after:
q₁ q₂ : ℚ
⊢ q₁.num * q₂.num =
    q₁.num * q₂.num / ↑((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)) *
      ↑((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den))
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 + r) = ↑q + ↑r

Tactic:
add_def',

Goal state after:
α : Type u_3
inst✝ : DivisionRing α
q r : ℚ
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑(mkRat (q.num * ↑r.den + r.num * ↑q.den) (q.den * r.den)) = ↑q + ↑r
Module: Mathlib.Order.CompleteLattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
f : Bool → α
⊢ sSup (range fun b ↦ f b) = f true ⊔ f false

Tactic:
Bool.range_eq,

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
f : Bool → α
⊢ sSup {f false, f true} = f true ⊔ f false
Module: Mathlib.Order.GaloisConnection.Basic

Goal state before:
pp: α : Type u
β : Type v
ι : Sort x
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
f : ι → α
⊢ IsLUB (range (l ∘ f)) (l (iSup f))

Tactic:
rw [range_comp, ← sSup_range]; exact gc.isLUB_l_image (isLUB_sSup _)

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a₁ a₂ : α
b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : PartialOrder β
inst✝ : SemilatticeInf α
gi : GaloisInsertion l u
⊢ ∀ (a b c : β), a ≤ b → a ≤ c → a ≤ l (u b ⊓ u c)

Tactic:
exact fun a b c hac hbc =>
        (gi.le_l_u a).trans <|
          gi.gc.monotone_l <| le_inf (gi.gc.monotone_u hac) (gi.gc.monotone_u hbc)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : CompleteLattice α
f : β × γ → α
s : Set β
t : Set γ
⊢ ⨆ i, ⨆ j, ⨆ (_ : i ∈ s), ⨆ (_ : j ∈ t), f (i, j) = ⨆ a ∈ s, ⨆ b ∈ t, f (a, b)

Tactic:
exact iSup_congr fun _ => iSup_comm

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LE α
inst✝ : SupSet α
s : Set α
hs : BddAbove s
⊢ ↑(sSup s) = sSup ((fun a ↦ ↑a) '' s)

Tactic:
change _ = ite _ _ _
  rw [if_neg, preimage_image_eq, if_pos hs]
  · exact Option.some_injective _
  · rintro ⟨x, _, ⟨⟩⟩

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
inst✝ : Frame α
s : Set α
b : α
⊢ sSup s ⊓ b = ⨆ a ∈ s, a ⊓ b

Tactic:
by
  simpa only [inf_comm] using @inf_sSup_eq α _ s b

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
e : α ↪o β
x y : α
⊢ ⇑e ⁻¹' uIcc (e x) (e y) = uIcc x y

Tactic:
cases le_total x y

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
e : α ↪o β
x y : α
h✝ : x ≤ y
⊢ ⇑e ⁻¹' uIcc (e x) (e y) = uIcc x y

case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
e : α ↪o β
x y : α
h✝ : y ≤ x
⊢ ⇑e ⁻¹' uIcc (e x) (e y) = uIcc x y
Module: Mathlib.Order.Interval.Set.OrderEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
e : α ↪o β
x y : α
⊢ ⇑e ⁻¹' uIoc (e x) (e y) = uIoc x y

Tactic:
cases le_total x y

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
e : α ↪o β
x y : α
h✝ : x ≤ y
⊢ ⇑e ⁻¹' uIoc (e x) (e y) = uIoc x y

case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
e : α ↪o β
x y : α
h✝ : y ≤ x
⊢ ⇑e ⁻¹' uIoc (e x) (e y) = uIoc x y
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a : α
⊢ uIoo a a = ∅

Tactic:
simp [uIoo]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
s : Set α
inst✝ : s.OrdConnected
a b : ↑s
⊢ Subtype.val '' [[a, b]] = [[↑a, ↑b]]

Tactic:
simp [uIcc, (Subtype.mono_coe (· ∈ s)).map_inf, (Subtype.mono_coe (· ∈ s)).map_sup]

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: case pos
ι : Sort u_1
α : Type u_2
s : Set α
inst✝¹ : ConditionallyCompleteLattice α
a b : α
inst✝ : Fact (a ≤ b)
S : Set ↑(Icc a b)
hS : S = ∅
⊢ IsLUB S ⟨a, ⋯⟩

Tactic:
subst hS; simp only [isLUB_empty_iff, isBot_iff_eq_bot]; rfl

Goal state after:
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: case neg
ι : Type u_1
κ : Type u_2
N : Type u_4
inst✝ : One N
f : ι → κ
g : ι → N
x : κ
hfg : ¬x ∈ f '' mulSupport g
hf : ¬∃ a, f a = x
⊢ extend f g 1 x = 1

Tactic:
rw [extend_apply' _ _ _ hf]; rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionRing α
m n : ℤ
n_dvd : n ∣ m
hn : ↑n ≠ 0
⊢ ↑(m / n) = ↑m / ↑n

Tactic:
by
  rcases n_dvd with ⟨k, rfl⟩
  have : n ≠ 0 := by rintro rfl; simp at hn
  rw [Int.mul_ediv_cancel_left _ this, mul_comm n, Int.cast_mul, mul_div_cancel_right₀ _ hn]

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

Goal state before:
pp: case step
m n m✝ : ℕ
a✝ : m.le m✝
ih : m ! ∣ m✝!
⊢ m ! ∣ m✝.succ !

Tactic:
exact Nat.dvd_trans ih (Nat.dvd_mul_left _ _)

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

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
y : ℕ
⊢ round (↑y + x) = ↑y + round x

Tactic:
by
  rw [add_comm, round_add_natCast, add_comm]

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
n : ℕ
a : R
⊢ ⌊↑↑n + a⌋ = ↑n + ⌊a⌋

Tactic:
floor_intCast_add

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
n : ℕ
a : R
⊢ ↑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 : 1 < a
⊢ StrictMono fun n ↦ a ^ n

Tactic:
by
  refine strictMono_int_of_lt_succ fun n ↦ ?_
  rw [zpow_add_one]
  exact lt_mul_of_one_lt_right' (a ^ n) ha

Goal state after:
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
⊢ (fun x ↦ x ^ n) a < (fun x ↦ x ^ n) b

Tactic:
rw [← one_lt_div', ← div_zpow]

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
n : ℤ
hn : 0 < n
a b : α
hab : a < b
⊢ 1 < (b / a) ^ n
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case refine_1
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
h : ⌈a⌉ = ⌊a⌋ + 1
ht : a ∈ range Int.cast
h0 : ↑⌊a⌋ = ↑⌈a⌉
⊢ False

Tactic:
rw [h, cast_add, cast_one, left_eq_add] at h0

Goal state after:
case refine_1
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
h : ⌈a⌉ = ⌊a⌋ + 1
ht : a ∈ range Int.cast
h0 : 1 = 0
⊢ False
Module: Mathlib.Algebra.Order.Floor.Ring

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

Tactic:
← self_sub_fract a,

Goal state after:
case inr
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
ha : fract a ≠ 0
⊢ a - fract a < a
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
y_pos : 0 < y
q : ℕ
hq : x⁻¹ < (y ^ q)⁻¹
⊢ y ^ q < x

Tactic:
inv_lt_inv₀ hx (pow_pos y_pos _)

Goal state after:
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
q : ℕ
hq : y ^ q < x
⊢ y ^ q < 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
g : G
⊢ (g • p₂ /ₛ p₂)⁻¹ = (p₂ /ₛ p₁) * ((p₁ /ₛ p₂) / g)

Tactic:
smul_sdiv,

Goal state after:
G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
p₁ p₂ : P
g : G
⊢ g⁻¹ = (p₂ /ₛ p₁) * ((p₁ /ₛ p₂) / g)
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✝ : 1 ≤ n
hy : R (f (l + n • a)) (f y)
hn : 1 < n
k : ℤ
⊢ R (f l + k • b) (f (l + a) + k • b)

Tactic:
refine hR (k • b) (hf _ ?_ _ ?_ ?_)

Goal state after:
case refine_1
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✝ : 1 ≤ n
hy : R (f (l + n • a)) (f y)
hn : 1 < n
k : ℤ
⊢ l ∈ Icc l (l + a)

case refine_2
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✝ : 1 ≤ n
hy : R (f (l + n • a)) (f y)
hn : 1 < n
k : ℤ
⊢ l + a ∈ Icc l (l + a)

case refine_3
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✝ : 1 ≤ n
hy : R (f (l + n • a)) (f y)
hn : 1 < n
k : ℤ
⊢ l < l + a
Module: Mathlib.Data.Multiset.Count

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Prop
inst✝² : IsTrans α r
inst✝¹ : Std.Symm r
x : α
inst✝ : DecidablePred (r x)
y : α
s : Multiset α
ih : ∀ {t : Multiset α}, Rel r s t → countP (r x) s = countP (r x) t
b : α
bs : Multiset α
hb1 : r y b
hb2 : Rel r s bs
h : Rel r (y ::ₘ s) (b ::ₘ bs)
⊢ (countP (r x) bs + if r x y then 1 else 0) = countP (r x) bs + if r x b then 1 else 0

Tactic:
simp only [Nat.add_right_inj]

Goal state after:
case cons
α : Type u_1
r : α → α → Prop
inst✝² : IsTrans α r
inst✝¹ : Std.Symm r
x : α
inst✝ : DecidablePred (r x)
y : α
s : Multiset α
ih : ∀ {t : Multiset α}, Rel r s t → countP (r x) s = countP (r x) t
b : α
bs : Multiset α
hb1 : r y b
hb2 : Rel r s bs
h : Rel r (y ::ₘ s) (b ::ₘ bs)
⊢ (if r x y then 1 else 0) = if r x b then 1 else 0
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: α : Type u
xs : List α
n m : Fin xs.length
h : xs.get n = xs.get m
hne : n ≠ m
⊢ ¬xs.Nodup

Tactic:
rw [nodup_iff_injective_get]
  exact fun hinj => hne (hinj h)

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

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

Tactic:
by
  rw [← hstu, Multiset.add_sub_cancel_right]

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

Goal state before:
pp: case cons
α : Type u
β : Type v
f : α → β
hd : α
tl : List α
ih : (map f tl).Nodup → ∀ ⦃x : α⦄, x ∈ tl → ∀ ⦃y : α⦄, y ∈ tl → f x = f y → x = y
d : (∀ (x : α), x ∈ tl → f x ≠ f hd) ∧ (map f tl).Nodup
⊢ ∀ ⦃x : α⦄, x ∈ hd :: tl → ∀ ⦃y : α⦄, y ∈ hd :: tl → f x = f y → x = y

Tactic:
simp only [mem_cons]

Goal state after:
case cons
α : Type u
β : Type v
f : α → β
hd : α
tl : List α
ih : (map f tl).Nodup → ∀ ⦃x : α⦄, x ∈ tl → ∀ ⦃y : α⦄, y ∈ tl → f x = f y → x = y
d : (∀ (x : α), x ∈ tl → f x ≠ f hd) ∧ (map f tl).Nodup
⊢ ∀ ⦃x : α⦄, x = hd ∨ x ∈ tl → ∀ ⦃y : α⦄, y = hd ∨ y ∈ tl → f x = f y → x = y
Module: Mathlib.Data.Multiset.AddSub

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

Tactic:
rw [← rel_flip, rel_add_left]

Goal state after:
α : Type u_1
β : Type v
r : α → β → Prop
as : Multiset α
bs₀ bs₁ : Multiset β
⊢ (∃ bs₀_1 bs₁_1, Rel (flip r) bs₀ bs₀_1 ∧ Rel (flip r) bs₁ bs₁_1 ∧ as = bs₀_1 + bs₁_1) ↔
    ∃ as₀ as₁, Rel r as₀ bs₀ ∧ Rel r as₁ bs₁ ∧ as = as₀ + as₁
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: α : Type u_1
β : Type v
f : α → β → β
inst✝ : LeftCommutative f
x : β
q : α → Prop
p : β → Prop
s : Multiset α
hpqf : ∀ (a : α) (b : β), q a → p b → p (f a b)
px : p x
q_s : ∀ (a : α), a ∈ s → q a
⊢ p (foldr f x s)

Tactic:
induction s using Multiset.induction with

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : List α
h : t ⊆ s
⊢ (s ++ t).dedup ~ s.dedup

Tactic:
by
  rw [← coe_eq_coe, ← coe_dedup, ← coe_add, Subset.dedup_add_left h, coe_dedup]

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

Goal state before:
pp: α : Type u_1
β : Type v
f : α → β
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
⊢ map f (filter p s) = filterMap (fun a ↦ if p a then some (f a) else none) s

Tactic:
induction s using Multiset.induction with

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

Goal state before:
pp: α : Type u_3
motive : Finset α → Prop
empty : motive ∅
cons : ∀ (a : α) (s : Finset α) (h : a ∉ s), motive s → motive (Finset.cons a s h)
s : Multiset α
nd : s.Nodup
⊢ motive { val := s, nodup := nd }

Tactic:
induction s using Multiset.induction with

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

Goal state before:
pp: case refine_3
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
⊢ ↑(filter (fun x ↦ x ∉ t₁) s) ⊆ t₂ \ t₁

Tactic:
intro x
      simp only [coe_filter, Set.mem_ofPred_eq, and_imp]
      intro hx hx₂
      exact ⟨Or.resolve_left (h hx) hx₂, hx₂⟩

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

Goal state before:
pp: k l : ℕ
inst✝¹ : NeZero k
inst✝ : NeZero l
h : k = l
x : Fin k
⊢ Fin.cast h x = 0 ↔ x = 0

Tactic:
simp [← val_eq_zero_iff]

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

Goal state before:
pp: n : ℕ
i j : Fin (n + 1)
h : i < j
hij : i.predAbove i.succ = j.predAbove i.succ
⊢ i = j

Tactic:
predAbove_succ_self,

Goal state after:
n : ℕ
i j : Fin (n + 1)
h : i < j
hij : i = j.predAbove i.succ
⊢ i = j
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n m : ℕ
i : Fin (m * n)
H₁ : ↑i % n + 1 ≤ n
H₂ : ↑i / n < m
⊢ (m * n - (↑i / n * n + ↑i % n + 1)) % n = ((m - ↑i / n - 1) * n + (n - (↑i % n + 1))) % n

Tactic:
by
      rw [Nat.mul_sub_right_distrib, Nat.one_mul, Nat.sub_add_sub_cancel _ H₁,
        Nat.mul_sub_right_distrib, Nat.sub_sub, Nat.add_assoc]
      exact Nat.le_mul_of_pos_left _ <| Nat.le_sub_of_add_le' H₂

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

Goal state before:
pp: case mpr.refine_2.inl
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
hij : ↑i = ↑j.castSucc
⊢ r (f i) (f j.succ)

Tactic:
obtain rfl := Fin.ext hij

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
hi : i ≠ last (n + 1)
⊢ (last n).predAbove i = i.castPred hi

Tactic:
rw [← exists_castSucc_eq] at hi

Goal state after:
n : ℕ
i : Fin (n + 2)
hi✝ : i ≠ last (n + 1)
hi : ∃ j, j.castSucc = i
⊢ (last n).predAbove i = i.castPred hi✝
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case refine_1
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hv : n = 0
l : Fin m
⊢ u l = u (Fin.cast ⋯ (castAdd n l))

Tactic:
refine congr_arg u (Fin.ext ?_)

Goal state after:
case refine_1
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hv : n = 0
l : Fin m
⊢ ↑l = ↑(Fin.cast ⋯ (castAdd n l))
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: m n : ℕ
α : Sort u_1
f : Fin (m + n) → α
⊢ (append (fun i ↦ f (castAdd n i)) fun i ↦ f (natAdd m i)) = f

Tactic:
by
  unfold append addCases
  simp

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

Goal state before:
pp: α : Type u_4
inst✝ : Fintype α
x : α
h : Fintype.card α = 1
⊢ univ = {x}

Tactic:
symm
  apply eq_of_subset_of_card_le (subset_univ {x})
  simp [h]

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
z : α (last n)
⊢ update (snoc p x) (last n) z = snoc p z

Tactic:
ext j
  cases j using lastCases <;> simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
h : a ∉ s
⊢ fold op b f (insert a s) = op (f a) (fold op b f s)

Tactic:
by
  unfold fold
  rw [insert_val, ndinsert_of_notMem h, Multiset.map_cons, fold_cons_left]

Goal state after: