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

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : LinearOrder G₀
a : G₀
inst✝ : PosMulMono G₀
this : PosMulReflectLT G₀
⊢ a⁻¹ < 0 ↔ a < 0

Tactic:
simp only [← not_le, inv_nonneg]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
g : s ↪r t
⊢ ∀ {a b : α}, t ((f.trans g.toEmbedding) a) ((f.trans g.toEmbedding) b) ↔ r a b

Tactic:
by simp [f.map_rel_iff, g.map_rel_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ≃r s
a b : β
⊢ r (f.symm a) (f.symm b) ↔ s a b

Tactic:
← f.map_rel_iff,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ≃r s
a b : β
⊢ s (f (f.symm a)) (f (f.symm b)) ↔ s a b
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow

Goal state before:
pp: M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulLeftMono M
a : M
n : ℕ
h : a < 1
hn : n ≠ 0
⊢ a ^ n < 1

Tactic:
rcases Nat.exists_eq_succ_of_ne_zero hn with ⟨k, rfl⟩
  rw [pow_succ']
  exact mul_lt_one_of_lt_of_le h (pow_le_one_of_le h.le _)

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

Goal state before:
pp: case inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
n : ℕ
a : G
ha : 1 ≤ a
⊢ |a ^ n|ₘ = |a|ₘ ^ n

Tactic:
· rw [mabs_of_one_le ha, mabs_of_one_le (one_le_pow_of_one_le' ha n)]

Goal state after:
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: case inl
α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a : α
h : 1 ≤ a
⊢ |a|ₘ⁻¹ ≤ a

pp: case inr
α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a : α
h : a ≤ 1
⊢ |a|ₘ⁻¹ ≤ a

Tactic:
· simpa [mabs_of_one_le h] using (inv_le_one'.2 h).trans h

Goal state after:
case inr
α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a : α
h : a ≤ 1
⊢ |a|ₘ⁻¹ ≤ a
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: k n : ℕ
hk : n.gcd k < k
⊢ ∃ m, m < k ∧ n * m % k = n.gcd k

Tactic:
have hk' := Int.ofNat_ne_zero.2 (Nat.zero_lt_of_lt hk).ne'
  have key := congr(($(gcd_eq_gcd_ab n k) % k).toNat)
  rw [Int.add_mul_emod_self_left, ← Int.natCast_mod, Int.toNat_natCast, mod_eq_of_lt hk] at key
  refine ⟨(n.gcdA k % k).toNat, ?_, (Int.ofNat_inj.1 ?_).trans key.symm⟩
  · rw [Int.toNat_lt (Int.emod_nonneg _ hk')]
    exact Int.emod_lt _ hk'
  rw [Int.natCast_mod, Int.natCast_mul, Int.toNat_of_nonneg (Int.emod_nonneg _ hk'),
    Int.toNat_of_nonneg (Int.emod_nonneg _ hk'), Int.mul_emod, Int.emod_emod, ← Int.mul_emod]

Goal state after:
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: a b : ℤ
ha : a ≠ 0
⊢ IsLeast {n | 0 < n ∧ ∃ x y, ↑n = a * x + b * y} (a.gcd b)

Tactic:
by
  simp_rw [← gcd_dvd_iff]
  constructor
  · simpa [and_true, dvd_refl, Set.mem_ofPred_eq] using gcd_pos_of_ne_zero_left b ha
  · simp only [lowerBounds, and_imp, Set.mem_ofPred_eq]
    exact fun n hn_pos hn => Nat.le_of_dvd hn_pos hn

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
a b : R
ha : 0 ≤ a
x✝ : ℕ
⊢ x✝ ∈ Nat.cast ⁻¹' Ioo a b ↔ x✝ ∈ Ioo ⌊a⌋₊ ⌈b⌉₊

Tactic:
simp [floor_lt, lt_ceil, ha]

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : FloorSemiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : ExistsAddOfLE R
a : R
n : ℕ
⊢ ⌈a - ↑n⌉₊ = ⌈a⌉₊ - n

Tactic:
obtain han | hna := le_total a n

Goal state after:
case inl
R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : FloorSemiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : ExistsAddOfLE R
a : R
n : ℕ
han : a ≤ ↑n
⊢ ⌈a - ↑n⌉₊ = ⌈a⌉₊ - n

case inr
R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : FloorSemiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : ExistsAddOfLE R
a : R
n : ℕ
hna : ↑n ≤ a
⊢ ⌈a - ↑n⌉₊ = ⌈a⌉₊ - n
Module: Mathlib.Algebra.Ring.Invertible

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
x y : AddUnits R
⊢ x.neg * ↑y = ↑x * ↑(-y)

Tactic:
← val_neg_mulRight

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
x y : AddUnits R
⊢ ↑(-x.mulRight ↑y) = ↑x * ↑(-y)
Module: Mathlib.Algebra.Group.Int.Units

Goal state before:
pp: a b c d : ℤ
ha : IsUnit a
hb : IsUnit b
hc : IsUnit c
hd : IsUnit d
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c

Tactic:
rw [isUnit_iff] at ha hb hc hd

Goal state after:
a b c d : ℤ
ha : a = 1 ∨ a = -1
hb : b = 1 ∨ b = -1
hc : c = 1 ∨ c = -1
hd : d = 1 ∨ d = -1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
Module: Mathlib.Data.Set.Monotone

Goal state before:
pp: case inl
α : Type u_4
β : Type u_5
inst✝¹ : PartialOrder α
inst✝ : LinearOrder β
φ : β → α
ψ : α → β
t : Set β
s : Set α
hφ : MonotoneOn φ t
φψs : RightInvOn ψ φ s
ψts : MapsTo ψ s t
x : α
xs : x ∈ s
y : α
ys : y ∈ s
l : x ≤ y
ψxy : ψ x ≤ ψ y
⊢ ψ x ≤ ψ y

pp: case inr
α : Type u_4
β : Type u_5
inst✝¹ : PartialOrder α
inst✝ : LinearOrder β
φ : β → α
ψ : α → β
t : Set β
s : Set α
hφ : MonotoneOn φ t
φψs : RightInvOn ψ φ s
ψts : MapsTo ψ s t
x : α
xs : x ∈ s
y : α
ys : y ∈ s
l : x ≤ y
ψyx : ψ y ≤ ψ x
⊢ ψ x ≤ ψ y

Tactic:
· exact ψxy

Goal state after:
case inr
α : Type u_4
β : Type u_5
inst✝¹ : PartialOrder α
inst✝ : LinearOrder β
φ : β → α
ψ : α → β
t : Set β
s : Set α
hφ : MonotoneOn φ t
φψs : RightInvOn ψ φ s
ψts : MapsTo ψ s t
x : α
xs : x ∈ s
y : α
ys : y ∈ s
l : x ≤ y
ψyx : ψ y ≤ ψ x
⊢ ψ x ≤ ψ y
Module: Mathlib.Data.Set.Monotone

Goal state before:
pp: case inr
α : Type u_4
β : Type u_5
inst✝¹ : PartialOrder α
inst✝ : LinearOrder β
φ : β → α
ψ : α → β
t : Set β
s : Set α
hφ : MonotoneOn φ t
φψs : RightInvOn ψ φ s
ψts : MapsTo ψ s t
x : α
xs : x ∈ s
y : α
ys : y ∈ s
l : x ≤ y
ψyx : ψ y ≤ ψ x
this : y ≤ φ (ψ x)
⊢ ψ x ≤ ψ y

Tactic:
φψs.eq xs

Goal state after:
case inr
α : Type u_4
β : Type u_5
inst✝¹ : PartialOrder α
inst✝ : LinearOrder β
φ : β → α
ψ : α → β
t : Set β
s : Set α
hφ : MonotoneOn φ t
φψs : RightInvOn ψ φ s
ψts : MapsTo ψ s t
x : α
xs : x ∈ s
y : α
ys : y ∈ s
l : x ≤ y
ψyx : ψ y ≤ ψ x
this : y ≤ x
⊢ ψ x ≤ ψ y
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
⊢ a ^ 2 < 1 ↔ |a| < 1

Tactic:
simpa only [one_pow, abs_one] using sq_lt_sq (a := a) (b := 1)

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
g : β → α → γ
h_comm : ∀ (a : α) (b : β), f a b = g b a
⊢ image2 (fun a b ↦ f b a) t s = image2 g t s

Tactic:
h_comm

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

Goal state before:
pp: case refine_2
α : Type u
π : α → Type u_1
inst✝ : (a : α) → Preorder (π a)
s : Set ((a : α) → π a)
f : (a : α) → π a
H : ∀ (a : α), IsLUB (eval a '' s) (f a)
⊢ f ∈ upperBounds s

pp: case refine_3
α : Type u
π : α → Type u_1
inst✝ : (a : α) → Preorder (π a)
s : Set ((a : α) → π a)
f : (a : α) → π a
H : ∀ (a : α), IsLUB (eval a '' s) (f a)
⊢ f ∈ lowerBounds (upperBounds s)

Tactic:
· exact fun g hg a => (H a).1 (mem_image_of_mem _ hg)

Goal state after:
case refine_3
α : Type u
π : α → Type u_1
inst✝ : (a : α) → Preorder (π a)
s : Set ((a : α) → π a)
f : (a : α) → π a
H : ∀ (a : α), IsLUB (eval a '' s) (f a)
⊢ f ∈ lowerBounds (upperBounds s)
Module: Mathlib.Order.WellFounded

Goal state before:
pp: case refine_3
α : Type u_1
r : α → α → Prop
h : ∀ (s : Set α), s.Nonempty → ∃ m, m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m ∧ (m = x ∨ r m x)
a b : α
⊢ ¬r a b → ¬r b a → a = b

Tactic:
grind [h {a, b} <| by simp]

Goal state after:
Module: Mathlib.Order.WellFounded

Goal state before:
pp: β : 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
a✝ a : β
IH : ∀ (y : β), y < a → f y = g y
⊢ f a = g a

Tactic:
obtain ⟨b, hb⟩ := hfg ▸ mem_range_self a

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
a✝ a : β
IH : ∀ (y : β), y < a → f y = g y
b : β
hb : g b = f a
⊢ f a = g a
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
t : Set β
hs : s.Nonempty
ht : t.Nonempty
x✝ : α × β
⊢ x✝ ∈ upperBounds (s ×ˢ t) ↔ x✝ ∈ upperBounds s ×ˢ upperBounds t

Tactic:
rw [← nonempty_coe_sort] at hs ht

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
t : Set β
hs : Nonempty ↑s
ht : Nonempty ↑t
x✝ : α × β
⊢ x✝ ∈ upperBounds (s ×ˢ t) ↔ x✝ ∈ upperBounds s ×ˢ upperBounds t
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: case mpr
α : Type u_1
a : List α
⊢ Forall₂ (fun x1 x2 ↦ x1 = x2) a a

Tactic:
exact forall₂_refl _

Goal state after:
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 ∧ ∀ {a : α} {b : β}, (a, b) ∈ l₁.zip l₂ → R a b
⊢ Forall₂ R l₁ l₂

Tactic:
obtain ⟨h₁, h₂⟩ := h

Goal state after:
α : 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₂
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: case mpr.slnil
α : Type u_1
β : Type u_2
R : α → β → Prop
l₂ l : List β
l₁ : List α
⊢ Forall₂ R l₁ [] → SublistForall₂ R l₁ []

Tactic:
hl1

Goal state after:
case mpr.slnil
α : Type u_1
β : Type u_2
R : α → β → Prop
l₂ l : List β
l₁ : List α
hl1 : Forall₂ R l₁ []
⊢ SublistForall₂ R l₁ []
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: case mpr.cons
α : Type u_1
β : Type u_2
R : α → β → Prop
l₂ l l₁✝ l₂✝ : List β
a✝¹ : β
a✝ : l₁✝ <+ l₂✝
ih : ∀ {l₁ : List α}, Forall₂ R l₁ l₁✝ → SublistForall₂ R l₁ l₂✝
l₁ : List α
⊢ Forall₂ R l₁ l₁✝ → SublistForall₂ R l₁ (a✝¹ :: l₂✝)

Tactic:
hl1

Goal state after:
case mpr.cons
α : Type u_1
β : Type u_2
R : α → β → Prop
l₂ l l₁✝ l₂✝ : List β
a✝¹ : β
a✝ : l₁✝ <+ l₂✝
ih : ∀ {l₁ : List α}, Forall₂ R l₁ l₁✝ → SublistForall₂ R l₁ l₂✝
l₁ : List α
hl1 : Forall₂ R l₁ l₁✝
⊢ SublistForall₂ R l₁ (a✝¹ :: l₂✝)
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: case mpr.cons_cons
α : Type u_1
β : Type u_2
R : α → β → Prop
l₂ l l₁✝ l₂✝ : List β
a✝¹ : β
a✝ : l₁✝ <+ l₂✝
ih : ∀ {l₁ : List α}, Forall₂ R l₁ l₁✝ → SublistForall₂ R l₁ l₂✝
l₁ : List α
⊢ Forall₂ R l₁ (a✝¹ :: l₁✝) → SublistForall₂ R l₁ (a✝¹ :: l₂✝)

Tactic:
hl1

Goal state after:
case mpr.cons_cons
α : Type u_1
β : Type u_2
R : α → β → Prop
l₂ l l₁✝ l₂✝ : List β
a✝¹ : β
a✝ : l₁✝ <+ l₂✝
ih : ∀ {l₁ : List α}, Forall₂ R l₁ l₁✝ → SublistForall₂ R l₁ l₂✝
l₁ : List α
hl1 : Forall₂ R l₁ (a✝¹ :: l₁✝)
⊢ SublistForall₂ R l₁ (a✝¹ :: l₂✝)
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: case cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst✝ : IsTrans α Rₐ
head✝ : α
tail✝ : List α
ih : ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b tail✝ → SublistForall₂ Rₐ a tail✝
a : List α
h1 : SublistForall₂ Rₐ a []
⊢ SublistForall₂ Rₐ a (head✝ :: tail✝)

Tactic:
cases h1
        exact SublistForall₂.nil

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:
exact perm_append_comm.append_right _

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
x : M
xs : List M
i : ℕ
a : M
⊢ ((x :: xs).set (i + 1) a).prod =
    ((take (i + 1) (x :: xs)).prod * if i + 1 < (x :: xs).length then a else 1) * (drop (i + 1 + 1) (x :: xs)).prod

Tactic:
by simp [set, prod_set xs i a, mul_assoc]

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

Goal state before:
pp: case refine_2
α : Type u
l₁ l₂ : List α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
hl : l₁ <+: l₂
a : α
h : idxOf a l₂ < l₁.length
this : idxOf a l₁ ≤ idxOf a l₂
⊢ a ∈ l₁

Tactic:
grind [List.idxOf_lt_length_iff]

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

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

Tactic:
have h : ((·⁻¹) ∘ fun k ↦ f (k + 1) / f k) = fun k ↦ f k / f (k + 1) := by ext; apply inv_div

Goal state after:
G : Type u_7
inst✝ : CommGroup G
n : ℕ
f : ℕ → G
h : ((fun x ↦ x⁻¹) ∘ fun k ↦ f (k + 1) / f k) = fun k ↦ f k / f (k + 1)
⊢ (map (fun k ↦ f (k + 1) / f k) (range n)).prod = f n / f 0
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: q a✝ b c : ℚ
C : ℚ → Sort u_1
a : ℚ
div : (n : ℤ) → (d : ℕ) → d ≠ 0 → n.natAbs.Coprime d → C (↑n / ↑d)
n : ℤ
d : ℕ
nz : d ≠ 0
red : n.natAbs.Coprime d
⊢ C { num := n, den := d, den_nz := nz, reduced := red }

Tactic:
rw [Rat.mk_eq_divInt, Rat.divInt_eq_div]; exact div n d nz red

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

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
u : αˣ
h : a ∣ b
⊢ a * ↑u * ↑u⁻¹ = a

Tactic:
by rw [mul_assoc, u.mul_inv, mul_one]

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

Goal state before:
pp: a b c : ℕ
h1 : a.pow b = c
⊢ a.pow (2 * b + 1) = c.mul (c.mul a)

Tactic:
simp [two_mul, pow_add, mul_assoc, ← h1]

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

Goal state before:
pp: a : ℤ
ha0 : 0 < a
⊢ ↑(↑a)⁻¹.den = a

Tactic:
simp only [den_inv, num_intCast]

Goal state after:
a : ℤ
ha0 : 0 < a
⊢ ↑(if a = 0 then 1 else a.natAbs) = a
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: a : ℤ
ha0 : 0 < a
⊢ ↑(↑a)⁻¹.den = a

Tactic:
by
  simp only [den_inv, num_intCast]
  grind

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

Goal state before:
pp: a✝¹ b✝¹ c : ℕ
a✝ b✝ : Q(ℕ)
depth : ℕ
a b₀ c₀ b : Q(ℕ)
p : Q(Prop)
hp : «$p» =Q («$a».pow «$b₀» = «$c₀»)
b' : ℕ := Expr.natLit! b
d : ℕ := depth >>> 1
hi : Q(ℕ)
⊢ «$p» =Q («$a».pow «$b₀» = «$c₀»)

Tactic:
exact hp

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

Goal state before:
pp: R : Type u
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : LE R
inst✝ : CanonicallyOrderedAdd R
⊢ MulLeftMono R

Tactic:
by
  refine ⟨fun a b c h => ?_⟩
  rcases exists_add_of_le h with ⟨c, rfl⟩
  rw [mul_add]
  apply self_le_add_right

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

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

Tactic:
obtain (hab | hba) := total_of (· ≤ ·) a b

Goal state after:
case inl
R : Type u
inst✝⁶ : NonUnitalNonAssocSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : CanonicallyOrderedAdd R
inst✝³ : Sub R
inst✝² : OrderedSub R
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : MulRightMono R
a b c : R
h : AddLECancellable (b * c)
hab : a ≤ b
⊢ (a - b) * c = a * c - b * c

case inr
R : Type u
inst✝⁶ : NonUnitalNonAssocSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : CanonicallyOrderedAdd R
inst✝³ : Sub R
inst✝² : OrderedSub R
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : MulRightMono R
a b c : R
h : AddLECancellable (b * c)
hba : b ≤ a
⊢ (a - b) * c = a * c - b * c
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 → α
hf : ∀ (i : ι) (hi : p i), u (l (f i hi)) = f i hi
⊢ l (⨅ i, ⨅ (hi : p i), f i hi) = ⨅ i, ⨅ (hi : p i), l (f i hi)

Tactic:
rw [iInf_subtype', iInf_subtype']

Goal state after:
α : Type u
β : Type v
l : α → β
u : β → α
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
gi : GaloisInsertion l u
ι : Sort x
p : ι → Prop
f : (i : ι) → p i → α
hf : ∀ (i : ι) (hi : p i), u (l (f i hi)) = f i hi
⊢ l (⨅ x, f ↑x ⋯) = ⨅ x, l (f ↑x ⋯)
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
e : α ≃ β
inst✝ : CompleteLattice β
⊢ CompleteLattice α

Tactic:
by
  let top := e.top
  let bot := e.bot
  let supSet := e.supSet
  let infSet := e.infSet
  let lattice := e.lattice
  apply e.injective.completeLattice <;> intros <;> first | rfl | exact e.apply_symm_apply _

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

Goal state before:
pp: ι : Type u_4
s : Set ι
⊢ s.PairwiseDisjoint singleton

Tactic:
intro; grind

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteBooleanAlgebra β
⊢ CompleteBooleanAlgebra α

Tactic:
let completeLattice := e.completeLattice
  let booleanAlgebra := e.booleanAlgebra
  apply e.injective.completeBooleanAlgebra <;> intros <;> first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set ↑s
h_bdd : BddAbove t
c : ↑s
hct : c ∈ t
⊢ sSup (Subtype.val '' t) ∈ s

Tactic:
obtain ⟨B, hB⟩ : ∃ B, B ∈ upperBounds t := h_bdd

Goal state after:
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set ↑s
c : ↑s
hct : c ∈ t
B : ↑s
hB : B ∈ upperBounds t
⊢ sSup (Subtype.val '' t) ∈ s
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
⊢ a⁺ᵐ ⊓ a⁻ᵐ = 1

Tactic:
by
  rw [← mul_left_inj a⁻ᵐ⁻¹, inf_mul, one_mul, mul_inv_cancel, ← div_eq_mul_inv,
    oneLePart_div_leOnePart, leOnePart_eq_inv_inf_one, inv_inv]

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

Goal state before:
pp: n k : ℕ
⊢ (n + 1) ^ (k + 2) < (n + 1).ascFactorial (k + 2)

Tactic:
rw [Nat.pow_succ, ascFactorial, Nat.mul_comm]
  exact Nat.mul_lt_mul_of_lt_of_le' (Nat.lt_add_of_pos_right k.succ_pos)
    (pow_succ_le_ascFactorial n.succ _) (Nat.pow_pos n.succ_pos)

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

Goal state before:
pp: a b : ℕ+
⊢ ↑(a - b) = if b < a then ↑a - ↑b else 1

Tactic:
change (toPNat' _ : ℕ) = ite _ _ _

Goal state after:
a b : ℕ+
⊢ ↑(↑a - ↑b).toPNat' = if b < a then ↑a - ↑b else 1
Module: Mathlib.Algebra.Order.Round

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

Tactic:
by
  rw [sub_eq_add_neg]
  norm_cast
  rw [round_add_intCast, sub_eq_add_neg]

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

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
⊢ |x - ↑(if 2 * fract x < 1 then ⌊x⌋ else ⌈x⌉)| = min (fract x) (1 - fract x)

Tactic:
min_def_lt,

Goal state after:
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
⊢ |x - ↑(if 2 * fract x < 1 then ⌊x⌋ else ⌈x⌉)| = if fract x < 1 - fract x then fract x else 1 - fract x
Module: Mathlib.Data.PNat.Basic

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

Tactic:
by
  rw [mul_comm]
  exact div_add_mod _ _

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

Goal state before:
pp: m k : ℕ+
h : k ∣ m
⊢ ↑k * ↑(m.divExact k) = ↑m

Tactic:
change (k : ℕ) * (div m k).succ = m

Goal state after:
m k : ℕ+
h : k ∣ m
⊢ ↑k * (m.div k).succ = ↑m
Module: Mathlib.Algebra.Order.Ring.Pow

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a : R
Hsq : 0 ≤ a ^ 2
Hsq' : 0 ≤ (1 + a) ^ 2
H : 0 ≤ 2 + a
n : ℕ
⊢ 1 + ↑n * a ≤ (1 + a) ^ n

Tactic:
simpa using (Commute.one_left a).pow_add_mul_le_add_pow_of_sq_nonneg zero_le_one Hsq Hsq'
    (by simpa using H) n

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 : 0 < n
hy : R (f (l + n • a)) (f y)
⊢ R (f (l + 1 • a)) (f y)

Tactic:
rw [← Int.add_one_le_iff, zero_add] at hn

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)
hn : 1 ≤ n
hy : R (f (l + n • a)) (f y)
⊢ R (f (l + 1 • a)) (f y)
Module: Mathlib.Data.List.Perm.Subperm

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

Tactic:
obtain ⟨x, ⟨sublistₓ, mapₓ⟩⟩ := sublist_map_iff.mp sublist

Goal state after:
α : Type u_2
β : Type u_3
l₁ l₂ : List α
f : α → β
hf : Function.Injective f
w : List β
perm : w ~ map f l₁
sublist : w <+ map f l₂
x : List α
sublistₓ : x <+ l₂
mapₓ : w = map f x
⊢ l₁ <+~ l₂
Module: Mathlib.Data.List.Count

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
l : List α
f : α → β
hf : Function.Injective f
x : α
⊢ countP (fun x_1 ↦ (fun x_2 ↦ x_2 == f x) (f x_1)) l = countP (fun x_1 ↦ x_1 == x) l

Tactic:
simp only [hf.beq_eq]

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

Goal state before:
pp: α : Type u_1
a b : α
⊢ {a, b}.card = 2

Tactic:
insert_eq_cons,

Goal state after:
α : Type u_1
a b : α
⊢ (a ::ₘ {b}).card = 2
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case cons.inl
α : 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 = x
⊢ ∃ b, b ∈ y ::ₘ t ∧ r a b

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:
· exact ⟨y, mem_cons_self _ _, ha.symm ▸ hxy⟩

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, b ∈ y ::ₘ t ∧ r a b
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: α : Type u_1
l₁ : List α
inst✝ : DecidableEq α
a : α
⊢ l₁.bagInter [a] = if a ∈ l₁ then [a] else []

Tactic:
induction l₁

Goal state after:
case nil
α : Type u_1
l₁ : List α
inst✝ : DecidableEq α
a : α
⊢ [].bagInter [a] = if a ∈ [] then [a] else []

case cons
α : Type u_1
l₁ : List α
inst✝ : DecidableEq α
a head✝ : α
tail✝ : List α
tail_ih✝ : tail✝.bagInter [a] = if a ∈ tail✝ then [a] else []
⊢ (head✝ :: tail✝).bagInter [a] = if a ∈ head✝ :: tail✝ then [a] else []