mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Invertible.Basic

Goal state before:
pp: α : Type u
R : Type u_1
S : Type u_2
F : Type u_3
inst✝⁴ : MulOneClass R
inst✝³ : MulOneClass S
inst✝² : FunLike F R S
inst✝¹ : MonoidHomClass F R S
f : F
r : R
inst✝ : Invertible r
⊢ f r * f ⅟r = 1

Tactic:
rw [← map_mul, mul_invOf_self, map_one]

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

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsOrderedRing R
inst✝ : ExistsAddOfLE R
a : R
k : ℕ
⊢ 0 ≤ a ^ (k + k)

Tactic:
pow_add

Goal state after:
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsOrderedRing R
inst✝ : ExistsAddOfLE R
a : R
k : ℕ
⊢ 0 ≤ a ^ k * a ^ k
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n : ℕ
a : α
h : n ≠ 0
⊢ |a ^ n| = 1 ↔ |a| = 1

Tactic:
convert! pow_left_inj₀ (abs_nonneg a) zero_le_one h
  exacts [(pow_abs _ _).symm, (one_pow _).symm]

Goal state after:
Module: Mathlib.Order.Antisymmetrization

Goal state before:
pp: α : Type u_1
β : Type u_2
a b c d : α
inst✝¹ : Preorder α
inst✝ : Preorder β
⊢ RightInverse (uncurry (Quotient.lift₂ (fun a b ↦ ⟦(a, b)⟧) ⋯)) (Quotient.lift (fun ab ↦ (⟦ab.1⟧, ⟦ab.2⟧)) ⋯)

Tactic:
rintro ⟨⟨_⟩, ⟨_⟩⟩

Goal state after:
case mk.mk
α : Type u_1
β : Type u_2
a b c d : α
inst✝¹ : Preorder α
inst✝ : Preorder β
fst✝ : Antisymmetrization α fun x1 x2 ↦ x1 ≤ x2
snd✝ : Antisymmetrization β fun x1 x2 ↦ x1 ≤ x2
a✝¹ : α
a✝ : β
⊢ Quotient.lift (fun ab ↦ (⟦ab.1⟧, ⟦ab.2⟧)) ⋯
      (uncurry (Quotient.lift₂ (fun a b ↦ ⟦(a, b)⟧) ⋯)
        (Quot.mk (⇑(AntisymmRel.setoid α fun x1 x2 ↦ x1 ≤ x2)) a✝¹,
          Quot.mk (⇑(AntisymmRel.setoid β fun x1 x2 ↦ x1 ≤ x2)) a✝)) =
    (Quot.mk (⇑(AntisymmRel.setoid α fun x1 x2 ↦ x1 ≤ x2)) a✝¹,
      Quot.mk (⇑(AntisymmRel.setoid β fun x1 x2 ↦ x1 ≤ x2)) a✝)
Module: Mathlib.Order.Bounds.Image

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Preorder β
f g : α → β
h : ∀ (a : α), f a ≤ g a
hbdd : BddAbove (range g)
⊢ BddAbove (range f)

Tactic:
obtain ⟨C, hC⟩ := hbdd

Goal state after:
α : Type u
β : Type v
inst✝ : Preorder β
f g : α → β
h : ∀ (a : α), f a ≤ g a
C : β
hC : C ∈ upperBounds (range g)
⊢ BddAbove (range f)
Module: Mathlib.Order.WellFounded

Goal state before:
pp: β : Type u_2
γ : Type u_3
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : WellFoundedLT β
⊢ InjOn range {f | StrictMono f}

Tactic:
intro f hf g hg hfg

Goal state after:
β : Type u_2
γ : Type u_3
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : WellFoundedLT β
f : β → γ
hf : f ∈ {f | StrictMono f}
g : β → γ
hg : g ∈ {f | StrictMono f}
hfg : range f = range g
⊢ f = g
Module: Mathlib.Order.WellFounded

Goal state before:
pp: β : Type u_2
inst✝¹ : LinearOrder β
inst✝ : WellFoundedLT β
f : β → β
hf : StrictMono f
H : ∃ i, f i < id i
m : β
hm : m ∈ {i | f i < i}
hm' : ∀ (x : β), x ∈ {i | f i < i} → ¬x < m
⊢ False

Tactic:
exact hm' _ (hf hm) hm

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : b ∈ s
⊢ s ∈ {Icc a b, Ico a b, Ioc a b, Ioo a b}

Tactic:
refine Or.inr <| Or.inr <| Or.inl <| Subset.antisymm ?_ ?_
    · rw [← Icc_sdiff_left]
      exact subset_sdiff_singleton hc ha
    · rwa [← Ioc_sdiff_right, sdiff_singleton_subset_iff, insert_eq_of_mem hb] at ho

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

Goal state before:
pp: ι : Sort u_4
α : Type u_5
inst✝ : SemilatticeSup α
f g : ι → α
hf : BddAbove (range f)
hg : BddAbove (range g)
af : α
haf : af ∈ upperBounds (range f)
⊢ BddAbove (range fun x ↦ f x ⊔ g x)

Tactic:
have ⟨ag, hag⟩ := hg

Goal state after:
ι : Sort u_4
α : Type u_5
inst✝ : SemilatticeSup α
f g : ι → α
hf : BddAbove (range f)
hg : BddAbove (range g)
af : α
haf : af ∈ upperBounds (range f)
ag : α
hag : ag ∈ upperBounds (range g)
⊢ BddAbove (range fun x ↦ f x ⊔ g x)
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ upperBounds ∅ = univ

Tactic:
simp only [upperBounds, eq_univ_iff_forall, mem_ofPred_eq, forall_mem_empty, forall_true_iff]

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

Goal state before:
pp: α : Type u
n d : ℕ
inst✝ : DivisionSemiring α
inv : Invertible ↑d
⊢ ↑n * ⅟↑d = NNRat.rawCast n d

Tactic:
by simp [div_eq_mul_inv]

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

Goal state before:
pp: α : Type u
n : ℤ
d : ℕ
inst✝ : DivisionRing α
inv : Invertible ↑d
⊢ ↑n * ⅟↑d = Rat.rawCast n d

Tactic:
by simp [div_eq_mul_inv]

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionRing α
n d : ℕ
inv✝ : Invertible ↑d
⊢ ↑(Int.negOfNat n) * ⅟↑d = -(↑n / ↑d)

Tactic:
by simp [div_eq_mul_inv]

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionSemiring α
n d : ℕ
inv✝ : Invertible ↑d
⊢ ↑n * ⅟↑d = ↑n / ↑d

Tactic:
by simp [div_eq_mul_inv]

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionSemiring α
n d : ℕ
h : ↑d ≠ 0
this : Invertible ↑d
⊢ NNRat.rawCast n d = ↑n * ⅟↑d

Tactic:
by simp [div_eq_mul_inv]

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionRing α
n : ℤ
d : ℕ
h : ↑d ≠ 0
this : Invertible ↑d
⊢ Rat.rawCast n d = ↑n * ⅟↑d

Tactic:
by simp [div_eq_mul_inv]

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

Goal state before:
pp: case inr
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
b : α
inst✝ : IsStrictOrderedRing α
s : Set α
hs : IsGLB s b
ha : 0 ≤ 0
⊢ IsGLB ((fun b ↦ 0 * b) '' s) (0 * b)

Tactic:
simp_rw [zero_mul]
    rw [hs.nonempty.image_const]
    exact isGLB_singleton

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 c : α
hc : a * b < c
hb : b ≤ 0
⊢ ∃ a' > a, a' * b < c

pp: case inr
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
hc : a * b < c
hb : 0 < b
⊢ ∃ a' > a, a' * b < c

Tactic:
· obtain ⟨a', ha'⟩ := exists_gt a
    exact ⟨a', ha', hc.trans_le' (antitone_mul_right hb ha'.le)⟩

Goal state after:
case inr
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
hc : a * b < c
hb : 0 < b
⊢ ∃ a' > a, a' * b < c
Module: Mathlib.Data.List.InsertIdx

Goal state before:
pp: α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
l : List α
a : α
n : ℕ
hl : ∀ (x : α), x ∈ l → p x
ha : p a
⊢ (pmap f l hl).insertIdx n (f a ha) = pmap f (l.insertIdx n a) ⋯

Tactic:
induction n generalizing l with
  | zero => cases l <;> simp
  | succ n ihn => cases l <;> simp_all

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

Goal state before:
pp: α : Type u
l : List α
x : α
n k : ℕ
hn : k < n
hk : k < l.length
hk' : k < (l.insertIdx n x).length
⊢ (l.insertIdx n x).get ⟨k, hk'⟩ = l.get ⟨k, hk⟩

Tactic:
simp_all [getElem_insertIdx_of_lt]

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

Goal state before:
pp: M : Type u_1
inst✝ : DivInvOneMonoid M
l l_n n : M
h : l = l_n / 1
hn : l_n = n
⊢ n / 1 = n

Tactic:
div_one

Goal state after:
M : Type u_1
inst✝ : DivInvOneMonoid M
l l_n n : M
h : l = l_n / 1
hn : l_n = n
⊢ n = n
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: a b : ℤ
b0 : b ≠ 0
⊢ a /. b = 0 ↔ a = 0

Tactic:
by
  rw [← zero_divInt b, divInt_eq_divInt_iff b0 b0, Int.zero_mul, Int.mul_eq_zero, or_iff_left b0]

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

Goal state before:
pp: q a b c : ℚ
x✝¹ : ℕ
x✝ : ℚ
⊢ Int.negSucc x✝¹ • x✝ = -(↑x✝¹.succ • x✝)

Tactic:
simp_rw [HSMul.hSMul, SMul.smul]
    rw [Int.negSucc_eq, Rat.intCast_neg, Rat.neg_mul]; rfl

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

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
f : α → β
finj : Injective f
a : α
l : List α
⊢ map f (l.erase a) = (map f l).erase (f a)

Tactic:
by
  have : (a == ·) = (f a == f ·) := by ext b; simp [finj.eq_iff]
  rw [erase_eq_eraseP, erase_eq_eraseP, eraseP_map, this]; rfl

Goal state after:
Module: Mathlib.Algebra.Divisibility.Units

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
a b : α
u : αˣ
⊢ a ∣ ↑u * b ↔ a ∣ b

Tactic:
apply Units.dvd_mul_left

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

Goal state before:
pp: m k : ℕ+
⊢ ↑(m.mod k) = if ↑m % ↑k = 0 then ↑k else ↑m % ↑k

Tactic:
dsimp [mod, modDiv]

Goal state after:
m k : ℕ+
⊢ ↑(k.modDivAux (↑m % ↑k) (↑m / ↑k)).fst = if ↑m % ↑k = 0 then ↑k else ↑m % ↑k
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
n : ℤ
⊢ ↑n / 1 = ↑n

Tactic:
div_one

Goal state after:
α : Type u_3
inst✝ : DivisionRing α
n : ℤ
⊢ ↑n = ↑n
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: case left
a b c d : ℤ
hb0 : 0 < b
hd0 : 0 < d
h1 : a.natAbs.Coprime b.natAbs
h2 : c.natAbs.Coprime d.natAbs
h : ↑a / ↑b = ↑c / ↑d
⊢ a = c

Tactic:
← num_div_eq_of_coprime hb0 h1,

Goal state after:
case left
a b c d : ℤ
hb0 : 0 < b
hd0 : 0 < d
h1 : a.natAbs.Coprime b.natAbs
h2 : c.natAbs.Coprime d.natAbs
h : ↑a / ↑b = ↑c / ↑d
⊢ (↑a / ↑b).num = c
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: case mp
m n : ℤ
hn : ↑n ≠ 0
⊢ (↑m / ↑n).den = 1 → n ∣ m

Tactic:
rw [Rat.den_eq_one_iff, eq_div_iff hn]
    exact mod_cast (Dvd.intro_left _)

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

Goal state before:
pp: a : ℕ
inst✝ : a.AtLeastTwo
⊢ (OfNat.ofNat a)⁻¹.num = 1

Tactic:
by
  -- This proof is quite unpleasant: golf / find better simp lemmas?
  have : 2 ≤ a := Nat.AtLeastTwo.prop
  simp only [num_inv, num_ofNat, den_ofNat, Nat.cast_one, mul_one, Int.sign_eq_one_iff_pos,
    gt_iff_lt]
  change 0 < (a : ℤ)
  lia

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set α
b : β
⊢ b ∈ upperBounds (l '' s) ↔ b ∈ u ⁻¹' upperBounds s

Tactic:
by simp [upperBounds, gc _ _]

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

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
s : Set α
⊢ sSup s = ⊥ ↔ s = ∅ ∨ s = {⊥}

Tactic:
by
  rw [sSup_eq_bot, ← subset_singleton_iff_eq, subset_singleton_iff]

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

Goal state before:
pp: case mpr
α : Type u_12
β : Type u_13
C : Set (Set α)
f : (s : ↑C) → β → ↑↑s
hf : ∀ (s : ↑C), Surjective (f s)
x : α
⊢ x ∈ ⋃₀ C → x ∈ ⋃ y, range fun s ↦ ↑(f s y)

Tactic:
rintro ⟨s, hs, hx⟩

Goal state after:
case mpr
α : Type u_12
β : Type u_13
C : Set (Set α)
f : (s : ↑C) → β → ↑↑s
hf : ∀ (s : ↑C), Surjective (f s)
x : α
s : Set α
hs : s ∈ C
hx : x ∈ s
⊢ x ∈ ⋃ y, range fun s ↦ ↑(f s y)
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
ι : Sort u_5
inst✝ : Preorder α
f : ι → α
⊢ (⋂ i, Iic (f i)).Nonempty ↔ BddBelow (range f)

Tactic:
by
  have : (⋂ (i : ι), Iic (f i)) = lowerBounds (range f) := by
    ext c; simp [lowerBounds]
  simp [this, BddBelow]

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

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s t : Set α
⊢ sSup (s ∪ t) ≤ max (sSup s) (sSup t)

Tactic:
rcases s.eq_empty_or_nonempty with (rfl | hs)
  · simp
  rcases t.eq_empty_or_nonempty with (rfl | ht)
  · simp
  by_cases BddAbove (s ∪ t) <;>
    grind [csSup_union, bddAbove_union, csSup_of_not_bddAbove]

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

Goal state before:
pp: case inr
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : s.Nonempty
⊢ IsLUB s (sSup s)

Tactic:
exact isLUB_sSup' hs

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
s t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : s ⊆ t
h : ∀ y ∈ t, ∃ x ∈ s, x ≤ y
⊢ sInf (f '' s) = sInf (f '' t)

Tactic:
by
  obtain rfl | hs := Set.eq_empty_or_nonempty s
  · obtain rfl : t = ∅ := by simpa [Set.eq_empty_iff_forall_notMem] using h
    rfl
  refine le_antisymm ?_ (by gcongr; exacts [ht, hs.image f])
  refine le_csInf ((hs.mono hst).image f) ?_
  simp only [mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
  intro a ha
  obtain ⟨x, hxs, hxa⟩ := h a ha
  exact csInf_le_of_le (ht.mono (image_mono hst)) ⟨x, hxs, rfl⟩ (hf (hst hxs) ha hxa)

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

Goal state before:
pp: α : Type u_1
s : Set α
r : α → α → Prop
⊢ (Pairwise fun x y ↦ r ↑x ↑y) ↔ s.Pairwise r

Tactic:
simp only [Pairwise, Set.Pairwise, SetCoe.forall, Ne, Subtype.ext_iff]

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
h : b ≤ a
⊢ uIoo a b = Ioo b a

Tactic:
by
  rw [uIoo, inf_eq_right.2 h, sup_eq_left.2 h]

Goal state after:
Module: Mathlib.Order.Antichain

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

Tactic:
rw [IsAntichain, IsAntichain, IsAntichain, pairwise_union]

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

Goal state before:
pp: case inl
α : Type u_1
inst✝³ : Nontrivial α
inst✝² : AddGroup α
inst✝¹ : LinearOrder α
inst✝ : AddLeftMono α
a : α
ha : a ≠ 0
lt : a < 0
⊢ Nontrivial { x // 0 ≤ x }

Tactic:
exact ⟨0, ⟨-a, neg_nonneg.mpr lt.le⟩, Subtype.coe_ne_coe.mp (neg_ne_zero.mpr ha).symm⟩

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

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
q : ℚ≥0
ha : 0 ≤ a
⊢ 0 ≤ q • a

Tactic:
rw [NNRat.smul_def]; exact mul_nonneg q.cast_nonneg ha

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

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
q : ℚ≥0
a : α
ha : 0 ≤ a
⊢ 0 ≤ q • a

Tactic:
rw [NNRat.smul_def]; exact mul_nonneg q.cast_nonneg ha

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:
by
  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.Nat.Factorial.Basic

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

Tactic:
descFactorial_eq_zero_iff_lt.mpr (show n < k by lia),

Goal state after:
case neg
k m n : ℕ
hkm : k ≤ m
hmn : ¬m ≤ n
hkn : ¬k ≤ n
⊢ (n - k).descFactorial (m - k) * 0 = 0
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
⊢ (2 * n)! ≤ (2 * n) ^ n * n !

Tactic:
rw [Nat.two_mul, ← factorial_mul_ascFactorial, Nat.mul_comm]
  exact Nat.mul_le_mul_right _ (ascFactorial_le_pow_add _ _)

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

Goal state before:
pp: p : ℕ+ → Sort u_1
a : ℕ+
hz : p 1
hi : (n : ℕ+) → ((m : ℕ+) → m ≤ n → p m) → p (n + 1)
⊢ (k : ℕ+) → ((m : ℕ+) → m < k → p m) → p k

Tactic:
rintro ⟨k, kprop⟩ hk

Goal state after:
p : ℕ+ → Sort u_1
a : ℕ+
hz : p 1
hi : (n : ℕ+) → ((m : ℕ+) → m ≤ n → p m) → p (n + 1)
k : ℕ
kprop : 0 < k
hk : (m : ℕ+) → m < ⟨k, kprop⟩ → p m
⊢ p ⟨k, kprop⟩
Module: Mathlib.Tactic.Ring.PNat

Goal state before:
pp: n : ℕ+
n' k : ℕ
h1 : CSLiftVal n n'
⊢ n' ^ k = CSLift.lift (n ^ k)

Tactic:
simp [h1.1, CSLift.lift]

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

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

Tactic:
rw [round_eq x, show x - 1 / 2 = x + 1 / 2 - 1 by linarith]

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

Goal state before:
pp: R : Type u_4
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
x k : R
hk : 1 < k
⊢ (∃ n, k * x = k * ↑n + 1) → k * x = k * ↑⌊x⌋ + 1

Tactic:
rintro ⟨n, hn⟩

Goal state after:
R : Type u_4
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
x k : R
hk : 1 < k
n : ℤ
hn : k * x = k * ↑n + 1
⊢ k * x = k * ↑⌊x⌋ + 1
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
m : ℤ
n : ℕ
⊢ fract (↑m / ↑n) = ↑(m % ↑n) / ↑n

Tactic:
by
  rcases n.eq_zero_or_pos with (rfl | hn)
  · simp
  replace hn : 0 < (n : k) := by norm_cast
  have : ∀ {l : ℤ}, 0 ≤ l → fract ((l : k) / n) = ↑(l % n) / n := by
    intro l hl
    obtain ⟨l₀, rfl | rfl⟩ := l.eq_nat_or_neg
    · rw [cast_natCast, ← natCast_mod, cast_natCast, fract_div_natCast_eq_div_natCast_mod]
    · rw [Right.nonneg_neg_iff, natCast_nonpos_iff] at hl
      simp [hl]
  obtain ⟨m₀, rfl | rfl⟩ := m.eq_nat_or_neg
  · exact this (natCast_nonneg m₀)
  let q := ⌈↑m₀ / (n : k)⌉
  let m₁ := q * ↑n - (↑m₀ : ℤ)
  have hm₁ : 0 ≤ m₁ := by
    simpa [m₁, ← @cast_le k, ← div_le_iff₀ hn] using FloorRing.gc_ceil_coe.le_u_l _
  calc
    fract ((Int.cast (-(m₀ : ℤ)) : k) / (n : k))
      = fract (-(m₀ : k) / n) := by simp
    _ = fract ((m₁ : k) / n) := ?_
    _ = Int.cast (m₁ % (n : ℤ)) / Nat.cast n := this hm₁
    _ = Int.cast (-(↑m₀ : ℤ) % ↑n) / Nat.cast n := ?_
  · rw [← fract_intCast_add q, ← mul_div_cancel_right₀ (q : k) hn.ne', ← add_div, ← sub_eq_add_neg]
    simp [m₁]
  · congr 2
    simp only [m₁]
    rw [sub_eq_add_neg, add_comm (q * ↑n), add_mul_emod_self_right]

Goal state after:
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:
rw [q_eq]
    exact mod_cast @Rat.exists_eq_mul_div_num_and_eq_mul_div_den n d (mod_cast hd.ne')

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

Goal state before:
pp: n : ℤ
d : ℕ
⊢ ⌈↑n / ↑d⌉ = -(-n / ↑d)

Tactic:
conv_lhs => rw [← neg_neg ⌈_⌉, ← floor_neg]
  rw [← neg_div, ← Int.cast_neg, floor_intCast_div_natCast]

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
a : R
inst✝ : IsOrderedRing R
ha : fract a ≠ 0
⊢ ↑⌈a⌉ = a + 1 - fract a

Tactic:
rw [(or_iff_right ha).mp (fract_eq_zero_or_add_one_sub_ceil a)]

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
a : R
inst✝ : IsOrderedRing R
ha : fract a ≠ 0
⊢ ↑⌈a⌉ = a + 1 - (a + 1 - ↑⌈a⌉)
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
ha : fract a ≠ 0
⊢ ↑⌈a⌉ - a = 1 - fract a

Tactic:
rw [(or_iff_right ha).mp (fract_eq_zero_or_add_one_sub_ceil a)]

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
a : R
inst✝ : IsOrderedRing R
ha : fract a ≠ 0
⊢ ↑⌈a⌉ - a = 1 - (a + 1 - ↑⌈a⌉)
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)
⊢ R (f x) (f y)

Tactic:
rcases existsUnique_sub_zsmul_mem_Ioc ha y l with ⟨n, hny, -⟩

Goal state after:
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)
⊢ R (f x) (f y)
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 : 1 < b
hba : ↑⌈(b - 1)⁻¹⌉ / b < a
⊢ ↑⌈a⌉ < b * a

Tactic:
by
  obtain hab | hba := le_total a (b - 1)⁻¹
  · calc
      ⌈a⌉ ≤ (⌈(b - 1)⁻¹⌉ : k) := by gcongr
      _ < b * a := by rwa [← div_lt_iff₀']; positivity
  · rw [← sub_pos] at hb
    calc
      ⌈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.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsStrictOrderedRing R
a : R
ha : -1 < a
⊢ ↑⌈a⌉₊ < a + 1

Tactic:
by
  by_cases! h : 0 ≤ a
  · exact ceil_lt_add_one h
  · rw [ceil_eq_zero.mpr h.le, cast_zero]
    exact neg_lt_iff_pos_add.mp ha

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

Goal state before:
pp: G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
α : Type u_5
inst✝⁴ : Group G
inst✝³ : Monoid M
inst✝² : MulAction G M
inst✝¹ : SMulCommClass G M M
inst✝ : IsScalarTower G M M
g : G
m : Mˣ
⊢ g • ↑m * g⁻¹ • ↑m⁻¹ = 1

Tactic:
rw [smul_mul_smul_comm, Units.mul_inv, mul_inv_cancel, one_smul]

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

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
p : α → Prop
f : (a : α) → p a → β
s : Multiset α
l₁ l₂ : List α
pp : l₁ ~ l₂
H₂ : ∀ (a : α), a ∈ l₂ → p a
H₁ : ∀ (a : α), a ∈ l₁ → p a
s₂ : Multiset α
e : ↑l₁ = s₂
H✝ : ∀ (a : α), a ∈ s₂ → p a
⊢ Eq.ndrec (motive := fun s ↦ (∀ (a : α), a ∈ s → p a) → Multiset β) (fun x ↦ ↑(List.pmap f l₁ H₁)) e H✝ =
    ↑(List.pmap f l₁ H₁)

Tactic:
subst e

Goal state after:
α : Type u_1
β : Type v
γ : Type u_2
p : α → Prop
f : (a : α) → p a → β
s : Multiset α
l₁ l₂ : List α
pp : l₁ ~ l₂
H₂ : ∀ (a : α), a ∈ l₂ → p a
H₁ : ∀ (a : α), a ∈ l₁ → p a
H✝ : ∀ (a : α), a ∈ ↑l₁ → p a
⊢ Eq.ndrec (motive := fun s ↦ (∀ (a : α), a ∈ s → p a) → Multiset β) (fun x ↦ ↑(List.pmap f l₁ H₁)) ⋯ H✝ =
    ↑(List.pmap f l₁ H₁)
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: case mpr
α : Type u_1
β : Type v
f : α → β
s : Multiset α
b : β
⊢ (∃ a, s = {a} ∧ f a = b) → map f s = {b}

Tactic:
rintro ⟨a, rfl, rfl⟩
    simp

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

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
r : α → β → Prop
s : Multiset α
t : Multiset γ
f : γ → β
⊢ Rel r s (map f t) ↔ Rel (fun a b ↦ r a (f b)) s t

Tactic:
rw [← rel_flip, rel_map_left, ← rel_flip]

Goal state after:
α : Type u_1
β : Type v
γ : Type u_2
r : α → β → Prop
s : Multiset α
t : Multiset γ
f : γ → β
⊢ Rel (flip fun a b ↦ flip r (f a) b) s t ↔ Rel (fun a b ↦ r a (f b)) s t
Module: Mathlib.Data.List.Perm.Lattice

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
IH : ∀ {t₁ t₂ : List α}, t₁ ~ t₂ → l.bagInter t₁ = l.bagInter t₂
t₁ t₂ : List α
p : t₁ ~ t₂
h : a ∈ t₁
⊢ (a :: l).bagInter t₁ = (a :: l).bagInter t₂

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
IH : ∀ {t₁ t₂ : List α}, t₁ ~ t₂ → l.bagInter t₁ = l.bagInter t₂
t₁ t₂ : List α
p : t₁ ~ t₂
h : ¬a ∈ t₁
⊢ (a :: l).bagInter t₁ = (a :: l).bagInter t₂

Tactic:
· simp [h, p.subset h, IH (p.erase _)]

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
IH : ∀ {t₁ t₂ : List α}, t₁ ~ t₂ → l.bagInter t₁ = l.bagInter t₂
t₁ t₂ : List α
p : t₁ ~ t₂
h : ¬a ∈ t₁
⊢ (a :: l).bagInter t₁ = (a :: l).bagInter t₂