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

Goal state before:
pp: case refine_2.inl
α : Type u_1
inst✝ : Preorder α
s t : Set α
hs : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
hts : IsCofinalFor t s
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
x' : α
hx' : x' ∈ s
hxx' : x ≤ x'
⊢ ∃ z ∈ s ∪ t, (fun x1 x2 ↦ x1 ≤ x2) x z ∧ (fun x1 x2 ↦ x1 ≤ x2) y z

Tactic:
obtain ⟨y', hy', hyy'⟩ := hts.union_right hy

Goal state after:
case refine_2.inl
α : Type u_1
inst✝ : Preorder α
s t : Set α
hs : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
hts : IsCofinalFor t s
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
x' : α
hx' : x' ∈ s
hxx' : x ≤ x'
y' : α
hy' : y' ∈ s
hyy' : y ≤ y'
⊢ ∃ z ∈ s ∪ t, (fun x1 x2 ↦ x1 ≤ x2) x z ∧ (fun x1 x2 ↦ x1 ≤ x2) y z
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b c d : α
h : a ≤ b
heq : Icc a b = Icc c d
⊢ a = c ∧ b = d

Tactic:
have h' : c ≤ d := by
    by_contra contra; rw [Icc_eq_empty_iff.mpr contra, Icc_eq_empty_iff] at heq; contradiction

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a b c d : α
h : a ≤ b
heq : Icc a b = Icc c d
h' : c ≤ d
⊢ a = c ∧ b = d
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
⊢ AntitoneOn (fun x ↦ x⁻¹) (Set.Iio 0)

Tactic:
by
  convert! sub_inv_antitoneOn_Iio (α := α)
  exact (sub_zero _).symm

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

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

pp: case inr.inl
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
⊢ 1 < a / 0 ↔ 0 < 0 ∧ 0 < a ∨ 0 < 0 ∧ a < 0

pp: case inr.inr
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
hb : 0 < b
⊢ 1 < a / b ↔ 0 < b ∧ b < a ∨ b < 0 ∧ a < b

Tactic:
· simp [hb, hb.not_gt, one_lt_div_of_neg]

Goal state after:
case inr.inl
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
⊢ 1 < a / 0 ↔ 0 < 0 ∧ 0 < a ∨ 0 < 0 ∧ a < 0

case inr.inr
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
hb : 0 < b
⊢ 1 < a / b ↔ 0 < b ∧ b < a ∨ b < 0 ∧ a < b
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
h₁ : l₁.length = l₂.length
h₂ : ∀ {a : α} {b : β}, (a, b) ∈ l₁.zip l₂ → R a b
⊢ Forall₂ R l₁ l₂

Tactic:
induction l₁ generalizing l₂ with
    | nil =>
      cases length_eq_zero_iff.1 h₁.symm
      constructor
    | cons a l₁ IH =>
      rcases l₂ with - | ⟨b, l₂⟩
      · simp at h₁
      · simp only [length_cons, succ.injEq] at h₁
        exact Forall₂.cons (h₂ <| by simp [zip])
          (IH h₁ fun h => h₂ <| by
            simp only [zip, zipWith, mem_cons, Prod.mk.injEq]; right
            simpa [zip] using h)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
p : α → Bool
q : β → Bool
hpq : (R ⇒ fun x1 x2 ↦ x1 ↔ x2) (fun x ↦ p x = true) fun x ↦ q x = true
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
⊢ Forall₂ R (filter p (a :: as)) (filter q (b :: bs))

Tactic:
dsimp [LiftFun] at hpq

Goal state after:
α : Type u_1
β : Type u_2
R : α → β → Prop
p : α → Bool
q : β → Bool
hpq : ∀ ⦃a : α⦄ ⦃b : β⦄, R a b → (p a = true ↔ q b = true)
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
⊢ Forall₂ R (filter p (a :: as)) (filter q (b :: bs))
Module: Mathlib.Data.List.Perm.Basic

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

Tactic:
by
  rw [rel_congr_left (perm_insertIdx _ _ hm), rel_congr_right (perm_insertIdx _ _ hn), perm_cons]

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

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

Tactic:
| cons _ _ r =>

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : GroupWithZero α
a : α
m n : ℤ
ha : a = 0
⊢ zpow' a (m + n) = zpow' a m * zpow' a n

pp: case neg
α : Type u_1
inst✝ : GroupWithZero α
a : α
m n : ℤ
ha : ¬a = 0
⊢ zpow' a (m + n) = zpow' a m * zpow' a n

Tactic:
· simp [zpow', ha]
    by_cases hn : n = 0
    · simp +contextual [hn, zero_zpow]
    · simp +contextual [hn, zero_zpow]

Goal state after:
case neg
α : Type u_1
inst✝ : GroupWithZero α
a : α
m n : ℤ
ha : ¬a = 0
⊢ zpow' a (m + n) = zpow' a m * zpow' a n
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: l : List ℤ
n : ℤ
⊢ l.prod % n = (map (fun x ↦ x % n) l).prod % n

Tactic:
induction l <;> simp [Int.mul_emod, *]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat

Goal state before:
pp: a b c d : ℤ
b_pos : 0 < b
d_pos : 0 < d
⊢ ↑a / ↑b < ↑c / ↑d ↔ a * d < c * b

Tactic:
simp only [lt_iff_le_not_ge]

Goal state after:
a b c d : ℤ
b_pos : 0 < b
d_pos : 0 < d
⊢ ↑a / ↑b ≤ ↑c / ↑d ∧ ¬↑c / ↑d ≤ ↑a / ↑b ↔ a * d ≤ c * b ∧ ¬c * b ≤ a * d
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: p q : ℚ≥0
⊢ p ≤ q ↔ p.num * q.den ≤ q.num * p.den

Tactic:
← NNRat.coe_le_coe,

Goal state after:
p q : ℚ≥0
⊢ ↑p ≤ ↑q ↔ p.num * q.den ≤ q.num * p.den
Module: Mathlib.Algebra.GroupWithZero.Divisibility

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
m n : α
⊢ m ∣ n ↔ m = 0 → n = 0

Tactic:
refine ⟨fun ⟨a, ha⟩ hm => ?_, fun h => ?_⟩
  · simp [hm, ha]
  · refine ⟨m⁻¹ * n, ?_⟩
    obtain rfl | hn := eq_or_ne n 0
    · simp
    · rw [mul_inv_cancel_left₀ (mt h hn)]

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

Goal state before:
pp: α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
q : ℚ≥0
⊢ ↑q = ↑0 ↔ q = 0

Tactic:
cast_inj

Goal state after:
α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
q : ℚ≥0
⊢ q = 0 ↔ q = 0
Module: Mathlib.Tactic.NormNum.Inv

Goal state before:
pp: n✝¹ num✝ n✝ denom✝ : ℕ
inv✝ : Invertible ↑denom✝
h : ↑n✝¹ / ↑n✝ = ↑num✝ * ⅟↑denom✝
⊢ IsNNRat (NNRat.divNat ↑n✝¹ ↑n✝) num✝ denom✝

Tactic:
rw [NNRat.divNat_eq_div]; exact ⟨_, h⟩

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

Goal state before:
pp: a b c b' c' : ℕ
h1 : a.pow b' = c'
hb : 2 * b' = b
hc : c' * c' = c
⊢ Int.ofNat a ^ b' * Int.ofNat a ^ b' = Int.ofNat c

Tactic:
← hc,

Goal state after:
a b c b' c' : ℕ
h1 : a.pow b' = c'
hb : 2 * b' = b
hc : c' * c' = c
⊢ Int.ofNat a ^ b' * Int.ofNat a ^ b' = Int.ofNat (c' * c')
Module: Mathlib.Tactic.NormNum.Pow

Goal state before:
pp: a b c b' c' : ℕ
h1 : a.pow b' = c'
hb : 2 * b' + 1 = b
hc : c' * (c' * a) = c
⊢ Int.ofNat a ^ b' * Int.ofNat a ^ b' * -Int.ofNat a = -Int.ofNat c

Tactic:
← hc,

Goal state after:
a b c b' c' : ℕ
h1 : a.pow b' = c'
hb : 2 * b' + 1 = b
hc : c' * (c' * a) = c
⊢ Int.ofNat a ^ b' * Int.ofNat a ^ b' * -Int.ofNat a = -Int.ofNat (c' * (c' * a))
Module: Mathlib.Data.Tree.Basic

Goal state before:
pp: α : Type u
x : BinaryTree α
⊢ x.numLeaves = x.numNodes + 1

Tactic:
induction x <;> simp [*, Nat.add_comm, Nat.add_assoc, Nat.add_left_comm]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
l : α → β
u : β → α
gc : GaloisConnection l u
a : β
b : α
⊢ (u aᶜ)ᶜ ≤ b ↔ l bᶜ ≤ aᶜ

Tactic:
gc,

Goal state after:
α : Type u
β : Type v
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
l : α → β
u : β → α
gc : GaloisConnection l u
a : β
b : α
⊢ (u aᶜ)ᶜ ≤ b ↔ bᶜ ≤ u aᶜ
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
minAx : MinimalAxioms α
a : α
s : Set α
⊢ (⨆ i,
      ⨅ j,
        match i, j with
        | { down := true }, j => a
        | { down := false }, j => ↑j) =
    a ⊔ sInf s

Tactic:
by simp [sInf_eq_iInf', iInf_unique, iSup_bool_eq]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
t : α → Set β
s₁ s₂ : Set α
⊢ s₁ ⊆ s₂ ∪ s₁ \ s₂

Tactic:
union_sdiff_self

Goal state after:
α : Type u_1
β : Type u_2
t : α → Set β
s₁ s₂ : Set α
⊢ s₁ ⊆ s₂ ∪ s₁
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case inl
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
t : Set α
h₁ : BddAbove t
h₂ : ∅ ⊆ t
⊢ sSup ∅ ≤ sSup t

pp: case inr
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s t : Set α
h₁ : BddAbove t
h₂ : s ⊆ t
h : s.Nonempty
⊢ sSup s ≤ sSup t

Tactic:
· rw [csSup_empty]
    exact bot_le

Goal state after:
case inr
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s t : Set α
h₁ : BddAbove t
h₂ : s ⊆ t
h : s.Nonempty
⊢ sSup s ≤ sSup t
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case pos.some.refine_1
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove ((fun a ↦ ↑a) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
⊢ ((fun a ↦ ↑a) ⁻¹' s).Nonempty

Tactic:
rcases hs with ⟨⟨⟩ | b, hb⟩
        · exact absurd hb h₁
        · exact ⟨b, hb⟩

Goal state after:
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

pp: case inr
α : 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 : j < i
⊢ ∃ 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:
case inr
α : 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 : j < i
⊢ ∃ i, i ∈ s ∧ ∃ j, j ∈ s ∧ i < j ∧ ∃ x, x ∈ f i ∩ f j
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
inst✝ : Std.Trichotomous r
h : IsAntichain r s
⊢ s.Subsingleton

Tactic:
rintro a ha b hb

Goal state after:
α : Type u_1
r : α → α → Prop
s : Set α
inst✝ : Std.Trichotomous r
h : IsAntichain r s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ a = b
Module: Mathlib.Order.Interval.Set.OrdConnected

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Set α
x : α
hx : x ∈ s
⊢ s.OrdConnected ↔ ∀ ⦃y : α⦄, y ∈ s → [[y, x]] ⊆ s

Tactic:
by
  simp_rw [ordConnected_iff_uIcc_subset_left hx, uIcc_comm]

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

Goal state before:
pp: k : ℕ
⊢ (0 + (k + 1)) * ascFactorial 0 (k + 1) = 0

Tactic:
zero_ascFactorial k,

Goal state after:
k : ℕ
⊢ (0 + (k + 1)) * 0 = 0
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: a b : ℕ+
h : a < b
⊢ ↑(a + (b - a)) = ↑b

Tactic:
add_coe,

Goal state after:
a b : ℕ+
h : a < b
⊢ ↑a + ↑(b - a) = ↑b
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: case inr
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
hx : 1 - fract x ≤ fract x
this : 0 < fract x
⊢ |x - ↑(if fract x < 1 - fract x then ⌊x⌋ else ⌈x⌉)| = if fract x < 1 - fract x then fract x else 1 - fract x

Tactic:
rw [if_neg (not_lt.mpr hx), if_neg (not_lt.mpr hx), abs_sub_comm, ceil_sub_self_eq this.ne.symm,
      abs_one_sub_fract]

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

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
⊢ fract x ≤ |x - ↑z| ∨ 1 - fract x ≤ |x - ↑z|

Tactic:
rcases le_or_gt (z : α) x with (hx | hx)

Goal state after:
case inl
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : ↑z ≤ x
⊢ fract x ≤ |x - ↑z| ∨ 1 - fract x ≤ |x - ↑z|

case inr
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : x < ↑z
⊢ fract x ≤ |x - ↑z| ∨ 1 - fract x ≤ |x - ↑z|
Module: Mathlib.Algebra.Order.Round

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

Tactic:
round_eq x

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

Goal state before:
pp: case inr.inr.calc_2.e_a
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
q : ℤ := ⌈↑m₀ / ↑n⌉
m₁ : ℤ := q * ↑n - ↑m₀
hm₁ : 0 ≤ m₁
⊢ (-↑m₀ + q * ↑n) % ↑n = -↑m₀ % ↑n

Tactic:
add_mul_emod_self_right

Goal state after:
case inr.inr.calc_2.e_a
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
q : ℤ := ⌈↑m₀ / ↑n⌉
m₁ : ℤ := q * ↑n - ↑m₀
hm₁ : 0 ≤ m₁
⊢ -↑m₀ % ↑n = -↑m₀ % ↑n
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: n : ℤ
d : ℕ
hd : 0 < d
q : ℚ := ↑n / ↑d
q_eq : q = ↑n / ↑d
⊢ ∃ c, n = c * q.num ∧ ↑d = c * ↑q.den

Tactic:
q_eq

Goal state after:
n : ℤ
d : ℕ
hd : 0 < d
q : ℚ := ↑n / ↑d
q_eq : q = ↑n / ↑d
⊢ ∃ c, n = c * (↑n / ↑d).num ∧ ↑d = c * ↑(↑n / ↑d).den
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
r : α
n d : ℕ
⊢ IsRat r (negOfNat n) d → IsRat (fract r) (-↑n % ↑d) d

Tactic:
rintro ⟨inv, rfl⟩
  refine ⟨inv, ?_⟩
  simp only [invOf_eq_inv, ← div_eq_mul_inv, fract_div_intCast_eq_div_intCast_mod,
    negOfNat_eq, ofNat_eq_natCast]

Goal state after:
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
b : H
inst✝² : AddGroupWithOne G
inst✝¹ : AddGroup H
inst✝ : AddConstMapClass F G H 1 b
f : F
x : G
n : ℕ
⊢ f (x - ↑n) = f x - n • b

Tactic:
by
  simpa using map_sub_nsmul f x n

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

Goal state before:
pp: k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a b : k
hb : 0 < b - 1
hba✝ : ↑⌈(b - 1)⁻¹⌉ / b < a
hba : (b - 1)⁻¹ ≤ a
⊢ a + 1 = a + (b - 1) * (b - 1)⁻¹

Tactic:
rw [mul_inv_cancel₀]; positivity

Goal state after:
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: F : Type u_1
G : Type u_2
H : Type u_3
inst✝⁷ : FunLike F G H
a : G
b : H
inst✝⁶ : AddCommGroup G
inst✝⁵ : LinearOrder G
inst✝⁴ : IsOrderedAddMonoid G
inst✝³ : Archimedean G
inst✝² : AddGroup H
inst✝¹ : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst✝ : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R (f x) (f y)
hR : Covariant H H (fun x y ↦ y + x) R
ha' : 0 ≤ a
x y : G
hxy : x < y
hx : x ∈ Ico l (l + a)
n : ℤ
hny : y - n • a ∈ Ioc l (l + a)
hn : 1 ≤ n
hy : R (f (l + n • a)) (f y)
⊢ R (f (l + 1 • a)) (f y)

Tactic:
rcases hn.eq_or_lt with rfl | hn

Goal state after:
case inl
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)
hny : y - 1 • a ∈ Ioc l (l + a)
hn : 1 ≤ 1
hy : R (f (l + 1 • a)) (f y)
⊢ R (f (l + 1 • a)) (f y)

case inr
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
⊢ R (f (l + 1 • a)) (f y)
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) = 0 ↔ ∀ (a : α), a ∈ Quot.mk (⇑(isSetoid α)) _l → ¬p a

Tactic:
by simp [List.countP_eq_zero]

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

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

Tactic:
apply Iff.intro (fun h ↦ ⟨subset_of_le h (mem_cons_self a s), le_trans (le_cons_self s a) h⟩)

Goal state after:
α : Type u_1
s t : Multiset α
a : α
hs : ¬a ∈ s
⊢ a ∈ t ∧ s ≤ t → a ::ₘ s ≤ t
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a b : α
h : a ∈ s
⊢ (b ::ₘ s).erase a = b ::ₘ s.erase a

Tactic:
rcases eq_or_ne a b with rfl | hab
  · simp [cons_erase h]
  · exact s.erase_cons_tail hab.symm

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

Goal state before:
pp: case cons.inr
α : Type u_1
β : Type v
r : α → β → Prop
s✝ : Multiset α
t✝ : Multiset β
x : α
y : β
s : Multiset α
t : Multiset β
hxy : r x y
a✝ : Rel r s t
ih : ∀ {a : α}, a ∈ s → ∃ b, b ∈ t ∧ r a b
a : α
ha✝ : a ∈ x ::ₘ s
ha : a ∈ s
⊢ ∃ b, b ∈ y ::ₘ t ∧ r a b

Tactic:
rcases ih ha with ⟨b, hbt, hab⟩

Goal state after:
case cons.inr
α : Type u_1
β : Type v
r : α → β → Prop
s✝ : Multiset α
t✝ : Multiset β
x : α
y : β
s : Multiset α
t : Multiset β
hxy : r x y
a✝ : Rel r s t
ih : ∀ {a : α}, a ∈ s → ∃ b, b ∈ t ∧ r a b
a : α
ha✝ : a ∈ x ::ₘ s
ha : a ∈ s
b : β
hbt : b ∈ t
hab : r a b
⊢ ∃ b, b ∈ y ::ₘ t ∧ r a b
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: case cons
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l₁ : List α
ih : ∀ {l₂ : List α}, l₂.Nodup → (l₁ ∪ l₂).Nodup
l₂ : List α
h : l₂.Nodup
⊢ (a :: l₁ ∪ l₂).Nodup

Tactic:
exact (ih h).insert

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

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

Tactic:
by
  induction l₁ with | nil => rfl | cons a l₁ IH => ?_
  simp only [cons_union] at *
  rw [← IH, cons_append]
  by_cases h : a ∈ dedup (l₁ ++ l₂)
  · rw [dedup_cons_of_mem' h, insert_of_mem h]
  · rw [dedup_cons_of_notMem' h, insert_of_not_mem h]

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

Goal state before:
pp: α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Set.InjOn f {x | x ∈ s}
x : α
H : x ∈ s
⊢ count (f x) (map f s) = count x s

Tactic:
suffices (filter (fun a : α => f x = f a) s).count x = card (filter (fun a : α => f x = f a) s) by
    rw [count, countP_map, ← this]
    exact count_filter_of_pos <| rfl
  · rw [eq_replicate_card.2 fun b hb => (hf H (mem_filter.1 hb).left _).symm]
    · simp
    · simp only [mem_filter, and_imp, @eq_comm _ (f x), imp_self, implies_true]

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

Goal state before:
pp: case pos
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Injective f
x : α
H : x ∈ s
⊢ count (f x) (map f s) = count x s

Tactic:
exact count_map_eq_count f _ hf.injOn _ H

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

Goal state before:
pp: α : Type u_1
β : Type v
f : α → β
r : β → β → Prop
m : Multiset α
h : {a | a ∈ m}.Pairwise fun a₁ a₂ ↦ r (f a₁) (f a₂)
b₁ : β
h₁ : b₁ ∈ {b | b ∈ map f m}
b₂ : β
h₂ : b₂ ∈ {b | b ∈ map f m}
hn : b₁ ≠ b₂
⊢ r b₁ b₂

Tactic:
obtain ⟨⟨a₁, H₁, rfl⟩, a₂, H₂, rfl⟩ := Multiset.mem_map.1 h₁, Multiset.mem_map.1 h₂
    exact h H₁ H₂ (mt (congr_arg f) hn)

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

Goal state before:
pp: α : Type u_1
s✝ : List α
a : α
t : List α
mi : s✝ <+: a :: t
b : α
s r : List α
hr : b :: s ++ r = a :: t
ba : b ≍ a
st : s ++ r ≍ t
⊢ ∃ l, l ∈ t.inits ∧ a :: l = b :: s

Tactic:
rw [eq_of_heq ba]; exact ⟨_, (mem_inits _ _).2 ⟨_, eq_of_heq st⟩, rfl⟩

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

Goal state before:
pp: α : Type u_1
a : α
s : Finset α
⊢ s.toList = [a] ↔ s = {a}

Tactic:
rw [toList, Multiset.toList_eq_singleton_iff, val_eq_singleton_iff]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f : ℕ → α
a : α
n : ℕ
hn : 0 < n
h : ∀ (i : ℕ), f (i % n) = f i
⊢ a ∈ Set.range f ↔ a ∈ image (fun i ↦ f i) (range n)

Tactic:
constructor
  · rintro ⟨i, hi⟩
    simp only [mem_image, mem_range]
    exact ⟨i % n, Nat.mod_lt i hn, (rfl.congr hi).mp (h i)⟩
  · rintro h
    simp only [mem_image, Set.mem_range, mem_range] at *
    rcases h with ⟨i, _, ha⟩
    exact ⟨i, ha⟩

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Finset α
a : α
ha : p a
⊢ ⟨a, ha⟩ ∈ Finset.subtype p s ↔ ↑⟨a, ha⟩ ∈ s

Tactic:
simp [Finset.subtype, ha]

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

Goal state before:
pp: α : Type u_1
s : Finset α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
a : α
⊢ a ∈ s ↔ a ∈ image (fun i ↦ f ↑i ⋯) (range n).attach

Tactic:
suffices _ : a ∈ s ↔ ∃ (i : _) (hi : i ∈ range n), f i (mem_range.1 hi) = a by
      simpa only [mem_image, mem_attach, true_and, Subtype.exists]

Goal state after:
α : Type u_1
s : Finset α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
a : α
⊢ a ∈ s ↔ ∃ i, ∃ (hi : i ∈ range n), f i ⋯ = a
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:
Fin.add_def

Goal state after:
n : ℕ
u v : Fin n
⊢ ↑↑⟨(↑u + ↑v) % n, ⋯⟩ = if ↑u + ↑v < n then ↑↑u + ↑↑v else ↑↑u + ↑↑v - ↑n
Module: Mathlib.Order.Fin.Basic

Goal state before:
pp: case h.refine_1
m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
h : ∀ (m_1 : ℕ), m_1 < i → ∀ (hi : m_1 < n), ↑(e ⟨m_1, hi⟩) = m_1
hi : i < n
j : ℕ
hj : j < ↑(e ⟨i, hi⟩)
⊢ j < i

pp: case h.refine_2
m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
h : ∀ (m_1 : ℕ), m_1 < i → ∀ (hi : m_1 < n), ↑(e ⟨m_1, hi⟩) = m_1
hi : i < n
j : ℕ
hj : j < i
⊢ j < ↑(e ⟨i, hi⟩)

Tactic:
· have := e.symm.lt_symm_apply.1 (mk_lt_of_lt_val hj)
    specialize h _ this (e.symm _).is_lt
    simp only [Fin.eta, OrderIso.apply_symm_apply] at h
    rwa [h]

Goal state after:
case h.refine_2
m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
h : ∀ (m_1 : ℕ), m_1 < i → ∀ (hi : m_1 < n), ↑(e ⟨m_1, hi⟩) = m_1
hi : i < n
j : ℕ
hj : j < i
⊢ j < ↑(e ⟨i, hi⟩)
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n m : ℕ
i : Fin n
⊢ (castAdd m i).succ = if h : i.succ = last n then natAdd n 0 else castAdd (m + 1) ⟨↑i + 1, ⋯⟩

Tactic:
by
  split_ifs with h
  exacts [Fin.ext (congr_arg Fin.val h :), rfl]

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

Goal state before:
pp: n : ℕ
σ : Perm (Fin n)
⊢ map (⇑σ) (finRange n) ~ finRange n

Tactic:
perm_ext_iff_of_nodup ((nodup_finRange n).map σ.injective) <| nodup_finRange n

Goal state after:
n : ℕ
σ : Perm (Fin n)
⊢ ∀ (a : Fin n), a ∈ map (⇑σ) (finRange n) ↔ a ∈ finRange n