mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case neg.refine_1
α : Type u_1
inst✝ : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h✝¹ : ¬m = 0
h✝ : ¬n = 0
hb : ¬b = 0
ha : ¬a = 0
⊢ a = (a ^ m.gcdB n * b ^ m.gcdA n) ^ n

Tactic:
refine (pow_one _).symm.trans ?_

Goal state after:
case neg.refine_1
α : Type u_1
inst✝ : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h✝¹ : ¬m = 0
h✝ : ¬n = 0
hb : ¬b = 0
ha : ¬a = 0
⊢ a ^ 1 = (a ^ m.gcdB n * b ^ m.gcdA n) ^ n
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case neg.refine_2
α : Type u_1
inst✝ : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h✝¹ : ¬m = 0
h✝ : ¬n = 0
hb : ¬b = 0
ha : ¬a = 0
⊢ b = (a ^ m.gcdB n * b ^ m.gcdA n) ^ m

Tactic:
refine (pow_one _).symm.trans ?_

Goal state after:
case neg.refine_2
α : Type u_1
inst✝ : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h✝¹ : ¬m = 0
h✝ : ¬n = 0
hb : ¬b = 0
ha : ¬a = 0
⊢ b ^ 1 = (a ^ m.gcdB n * b ^ m.gcdA n) ^ m
Module: Mathlib.Algebra.Order.Monoid.WithTop

Goal state before:
pp: case coe.coe
α : Type u
inst✝² : Add α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedAdd α
a✝¹ : α
hx : ↑a✝¹ ≠ ⊥
a✝ : α
⊢ ↑a✝ ≤ ↑a✝ + ↑a✝¹

Tactic:
← WithBot.coe_add,

Goal state after:
case coe.coe
α : Type u
inst✝² : Add α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedAdd α
a✝¹ : α
hx : ↑a✝¹ ≠ ⊥
a✝ : α
⊢ ↑a✝ ≤ ↑(a✝ + a✝¹)
Module: Mathlib.Algebra.Order.Monoid.WithTop

Goal state before:
pp: case coe.coe
α : Type u
inst✝² : AddCommMagma α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedAdd α
a✝¹ : α
hx : ↑a✝¹ ≠ ⊥
a✝ : α
⊢ ↑a✝ ≤ ↑a✝¹ + ↑a✝

Tactic:
← WithBot.coe_add,

Goal state after:
case coe.coe
α : Type u
inst✝² : AddCommMagma α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedAdd α
a✝¹ : α
hx : ↑a✝¹ ≠ ⊥
a✝ : α
⊢ ↑a✝ ≤ ↑(a✝¹ + a✝)
Module: Mathlib.Algebra.Regular.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
a : R
n : ℕ
rra : IsRightRegular a
⊢ Function.Injective fun x ↦ x * a ^ n

Tactic:
← mul_right_iterate

Goal state after:
R : Type u_1
inst✝ : Monoid R
a : R
n : ℕ
rra : IsRightRegular a
⊢ Function.Injective (fun x ↦ x * a)^[n]
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
⊢ ⊤ ≠ 0

Tactic:
by
  intro h
  obtain ⟨a, ha⟩ := exists_ne (0 : α)
  rw [← zero_add a] at ha
  simp [LinearOrderedAddCommGroupWithTop.top_add', -zero_add, ← h] at ha

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝² : Add α
x y z : WithTop α
inst✝¹ : LE α
inst✝ : AddLeftReflectLE α
hx : x ≠ ⊤
⊢ x + y ≤ x + z → y ≤ z

Tactic:
by
  lift x to α using hx; cases y <;> cases z <;> simp [← coe_add]; simpa using le_of_add_le_add_left

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝² : Add α
x y z : WithBot α
inst✝¹ : LE α
inst✝ : AddLeftReflectLE α
hx : x ≠ ⊥
⊢ x + y ≤ x + z → y ≤ z

Tactic:
by
  lift x to α using hx; cases y <;> cases z <;> simp [← coe_add]; simpa using le_of_add_le_add_left

Goal state after:
Module: Mathlib.Data.Nat.Find

Goal state before:
pp: case pos
P Q : ℕ → Prop
inst✝¹ : DecidablePred P
inst✝ : DecidablePred Q
hPQ : ∀ (n : ℕ), P n → Q n
n : ℕ
hn : findGreatest P n ≤ findGreatest Q n
h : P (n + 1)
⊢ findGreatest P (n + 1) ≤ findGreatest Q (n + 1)

pp: case neg
P Q : ℕ → Prop
inst✝¹ : DecidablePred P
inst✝ : DecidablePred Q
hPQ : ∀ (n : ℕ), P n → Q n
n : ℕ
hn : findGreatest P n ≤ findGreatest Q n
h : ¬P (n + 1)
⊢ findGreatest P (n + 1) ≤ findGreatest Q (n + 1)

Tactic:
· rw [findGreatest_eq h, findGreatest_eq (hPQ _ h)]

Goal state after:
case neg
P Q : ℕ → Prop
inst✝¹ : DecidablePred P
inst✝ : DecidablePred Q
hPQ : ∀ (n : ℕ), P n → Q n
n : ℕ
hn : findGreatest P n ≤ findGreatest Q n
h : ¬P (n + 1)
⊢ findGreatest P (n + 1) ≤ findGreatest Q (n + 1)
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: α : Type u_2
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
a : α
⊢ ↑0 ≤ a ↔ 0 ≤ a

Tactic:
Int.cast_zero

Goal state after:
α : Type u_2
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
a : α
⊢ 0 ≤ a ↔ 0 ≤ a
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: α : Type u_2
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
a : α
⊢ a < ↑0 ↔ a < 0

Tactic:
Int.cast_zero

Goal state after:
α : Type u_2
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
a : α
⊢ a < 0 ↔ a < 0
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: α : Type u_2
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
a : α
ha : 0 ≤ a
⊢ ↑0 ≤ ↑⌈a⌉

Tactic:
Int.cast_zero

Goal state after:
α : Type u_2
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
a : α
ha : 0 ≤ a
⊢ 0 ≤ ↑⌈a⌉
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: α : Type u_2
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
a : α
ha : a ≤ 0
⊢ ↑⌊a⌋ ≤ ↑0

Tactic:
Int.cast_zero

Goal state after:
α : Type u_2
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
a : α
ha : a ≤ 0
⊢ ↑⌊a⌋ ≤ 0
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: case inr
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
a b : R
h : a ≤ b
ha : 0 ≤ a
⊢ ⌊a⌋₊ ≤ ⌊b⌋₊

Tactic:
exact le_floor ((floor_le ha).trans h)

Goal state after:
Module: Mathlib.Order.Directed

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
r₂ : β → β → Prop
d₁ : Set α
d₂ : Set β
h₁ : DirectedOn (fun x1 x2 ↦ r x1 x2) d₁
h₂ : DirectedOn (fun x1 x2 ↦ r₂ x1 x2) d₂
x✝¹ : α × β
hpd : x✝¹ ∈ d₁ ×ˢ d₂
x✝ : α × β
hqd : x✝ ∈ d₁ ×ˢ d₂
⊢ ∃ z ∈ d₁ ×ˢ d₂, (fun p q ↦ r p.1 q.1 ∧ r₂ p.2 q.2) x✝¹ z ∧ (fun p q ↦ r p.1 q.1 ∧ r₂ p.2 q.2) x✝ z

Tactic:
by
  obtain ⟨r₁, hdr₁, hpr₁, hqr₁⟩ := h₁ _ hpd.1 _ hqd.1
  obtain ⟨r₂, hdr₂, hpr₂, hqr₂⟩ := h₂ _ hpd.2 _ hqd.2
  exact ⟨⟨r₁, r₂⟩, ⟨hdr₁, hdr₂⟩, ⟨hpr₁, hpr₂⟩, ⟨hqr₁, hqr₂⟩⟩

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

Goal state before:
pp: case pos
K : Type u_1
L : Type u_2
inst✝ : Field K
a : K
n : ℕ
h : a = 0
⊢ a ^ (↑n + 1) = a ^ ↑n * a

Tactic:
← Int.natCast_add_one,

Goal state after:
case pos
K : Type u_1
L : Type u_2
inst✝ : Field K
a : K
n : ℕ
h : a = 0
⊢ a ^ ↑(n + 1) = a ^ ↑n * a
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
x : α
⊢ |x ^ 2| = x ^ 2

Tactic:
by simpa only [sq] using abs_mul_self x

Goal state after:
Module: Mathlib.Order.Antisymmetrization

Goal state before:
pp: case mk
α : Type u_1
inst✝ : Preorder α
a : α
b✝ : Antisymmetrization α fun x1 x2 ↦ x1 ≤ x2
b : α
h : Quot.mk (⇑(AntisymmRel.setoid α fun x1 x2 ↦ x1 ≤ x2)) b < toAntisymmetrization (fun x1 x2 ↦ x1 ≤ x2) a
⊢ ∃ a',
    (fun x1 x2 ↦ x1 < x2) a' a ∧
      toAntisymmetrization (fun x1 x2 ↦ x1 ≤ x2) a' = Quot.mk (⇑(AntisymmRel.setoid α fun x1 x2 ↦ x1 ≤ x2)) b

Tactic:
exact ⟨b, h, rfl⟩

Goal state after:
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
s : Set β
⊢ ⇑e.symm '' s = ⇑e ⁻¹' s

Tactic:
ext; exact mem_image_iff_of_inverse e.right_inv e.left_inv

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

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a : R
inst✝ : Invertible a
⊢ 0 < a * ⅟a

Tactic:
by simp only [mul_invOf_self, zero_lt_one]

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

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a : α
⊢ Iic a \ (Iic a \ {a}) = {a}

Tactic:
sdiff_sdiff_cancel_left (singleton_subset_iff.2 self_mem_Iic)

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a : α
⊢ {a} = {a}
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ≤ b
⊢ Ioo a b ∪ {a, b} = Icc a b

Tactic:
have : (Icc a b \ {a, b}) ∪ {a, b} = Icc a b := sdiff_union_of_subset fun
    | x, .inl rfl => left_mem_Icc.mpr h
    | x, .inr rfl => right_mem_Icc.mpr h

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ≤ b
this : Icc a b \ {a, b} ∪ {a, b} = Icc a b
⊢ Ioo a b ∪ {a, b} = Icc a b
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: case inl.inr
α : Type u_1
inst✝ : Preorder α
s t : Set α
hn : (s ∪ t).Nonempty
h✝ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (s ∪ t)
h : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
hs : s.Nonempty
⊢ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s ∧ s.Nonempty ∨ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) t ∧ t.Nonempty

Tactic:
exact .inl ⟨h, hs⟩

Goal state after:
Module: Mathlib.Tactic.Positivity.Core

Goal state before:
pp: A : Type u_1
e : A
n : ℕ
inst✝² : Semiring A
inst✝¹ : PartialOrder A
inst✝ : IsOrderedRing A
h : NormNum.IsNat e n
⊢ 0 ≤ ↑n

Tactic:
exact Nat.cast_nonneg n

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 : 0 < a
⊢ AntitoneOn (fun x ↦ x⁻¹) (Set.Icc a b)

Tactic:
by
  convert! sub_inv_antitoneOn_Icc_right ha
  exact (sub_zero _).symm

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 : α
hb : b < 0
h : 1 / a ≤ 1 / b
⊢ b ≤ a

Tactic:
simpa using one_div_le_one_div_of_neg_of_le (one_div b ▸ inv_lt_zero'.2 hb) h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
p : α → Prop
a : α
l : List α
u : List β
⊢ Forall₂ (fun a b ↦ p a ∧ R a b) (a :: l) u ↔ (∀ (a_1 : α), a_1 ∈ a :: l → p a_1) ∧ Forall₂ R (a :: l) u

Tactic:
simp only [forall₂_and_left l, forall₂_cons_left_iff, forall_mem_cons, and_assoc,
      exists_and_left]
    simp only [and_comm, and_assoc, ← exists_and_right]

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

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
ha : 0 ≤ a
hc : 0 ≤ c
h : c < a * b
hb : 0 < b
a' : α
ha' : c / b < a'
a_a' : a' < a
⊢ ∃ a' ∈ Set.Ico 0 a, c < a' * b

Tactic:
exact ⟨a', ⟨(div_nonneg hc hb.le).trans ha'.le, a_a'⟩, (div_lt_iff₀ hb).1 ha'⟩

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

Goal state before:
pp: α : Type u
n : ℕ
x : α
⊢ Injective fun l ↦ l.insertIdx n x

Tactic:
intro l₁ l₂ hl
  simpa using congr($hl |>.eraseIdx n)

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

Goal state before:
pp: α : Type u
inst✝ : Inhabited α
⊢ [].getLastI = [].getLast?.getD default

Tactic:
by simp [getLastI]

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

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
a b c D e f : M
h₁ : a = b
h₂ : b = c
h₃ : c = D * e
h₄ : e = f
⊢ a = D * f

Tactic:
rw [h₁, h₂, h₃, h₄]

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

Goal state before:
pp: G : Type u_7
inst✝ : CommGroup G
a : G
⊢ [a].alternatingProd = a * [].alternatingProd⁻¹

Tactic:
alternatingProd_nil,

Goal state after:
G : Type u_7
inst✝ : CommGroup G
a : G
⊢ [a].alternatingProd = a * 1⁻¹
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: a : ℤ
b : ℕ
⊢ (mkRat a b)⁻¹ = ↑b /. a

Tactic:
by
  rw [mkRat_eq_divInt, inv_divInt]

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

Goal state before:
pp: α : Type u
l : List α
p : α → Bool
⊢ filter p (map (fun a ↦ ↑a) l.attach) = map (fun x ↦ ↑x) (filter p l).attach

Tactic:
attach_map_subtype_val

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s t : List α
hf : Injective f
h : s.Disjoint t
⊢ (map f s).Disjoint (map f t)

Tactic:
rw [← pmap_eq_map (fun _ _ ↦ trivial), ← pmap_eq_map (fun _ _ ↦ trivial)]
  exact disjoint_pmap _ _ (fun _ _ _ _ h' ↦ hf h') h

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

Goal state before:
pp: α : Type u
l₁ l₂ l : List α
p : l₁ ~ l₂
⊢ l₁.Disjoint l ↔ l₂.Disjoint l

Tactic:
simp_rw [List.disjoint_left, p.mem_iff]

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

Goal state before:
pp: p q : ℚ
hp : 0 ≤ p
⊢ (p * q).toNNRat = p.toNNRat * q.toNNRat

Tactic:
rcases le_total 0 q with hq | hq
  · ext; simp [toNNRat, hp, hq, mul_nonneg]
  · have hpq := mul_nonpos_of_nonneg_of_nonpos hp hq
    rw [toNNRat_eq_zero.2 hq, toNNRat_eq_zero.2 hpq, mul_zero]

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

Goal state before:
pp: a b : ℤ
b0 : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a /. b = { num := n, den := d, den_nz := h, reduced := c }
⊢ { num := n, den := d, den_nz := h, reduced := c }.num ∣ a

Tactic:
rw [Rat.mk_eq_divInt, divInt_eq_divInt_iff b0 (mod_cast h)] at e

Goal state after:
a b : ℤ
b0 : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a * ↑d = n * b
⊢ { num := n, den := d, den_nz := h, reduced := c }.num ∣ a
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: case mp
q : ℚ
⊢ IsSquare q → IsSquare q.num ∧ IsSquare q.den

Tactic:
rintro ⟨qr, rfl⟩

Goal state after:
case mp
qr : ℚ
⊢ IsSquare (qr * qr).num ∧ IsSquare (qr * qr).den
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a b₃ c b₁ : R
b₂ : ℕ
x✝ : a * b₃ = c
⊢ a * (b₁ ^ b₂ * b₃) = b₁ ^ b₂ * c

Tactic:
by
  subst_vars; rw [mul_left_comm]

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

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

Tactic:
rw [mul_tsub, mul_one]

Goal state after:
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 (l '' range f) (l (iSup f))

Tactic:
← sSup_range

Goal state after:
α : Type u
β : Type v
ι : Sort x
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
f : ι → α
⊢ IsLUB (l '' range f) (l (sSup (range f)))
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : CompleteLattice α
f : β × γ → α
c : α
⊢ ⨆ x, f x ≤ c ↔ ⨆ i, ⨆ j, f (i, j) ≤ c

Tactic:
by simp only [iSup_le_iff, Prod.forall]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Option β → α
c : α
⊢ ⨆ o, f o ≤ c ↔ f none ⊔ ⨆ b, f (some b) ≤ c

Tactic:
simp only [iSup_le_iff, sup_le_iff, Option.forall]

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

Goal state before:
pp: α : Type u_1
S : Set (Set α)
⊢ ⋂₀ S = (⋃₀ (compl '' S))ᶜ

Tactic:
← compl_compl (⋂₀ S),

Goal state after:
α : Type u_1
S : Set (Set α)
⊢ (⋂₀ S)ᶜᶜ = (⋃₀ (compl '' S))ᶜ
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α✝ : Type u
β✝ : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLinearOrder α✝
α : Type u
β : α → Type u
g : (a : α) → β a → α✝
lhs : α✝ := ⨅ a, ⨆ b, g a b
rhs : α✝ := ⨆ h, ⨅ a, g a (h a)
x : α✝
hr : rhs < x
hl : x < lhs
f : (a : α) → β a
hf : ∀ (a : α), x < g a (f a)
⊢ rhs ≥ x

Tactic:
refine le_trans ?_ (le_iSup _ f)

Goal state after:
α✝ : Type u
β✝ : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLinearOrder α✝
α : Type u
β : α → Type u
g : (a : α) → β a → α✝
lhs : α✝ := ⨅ a, ⨆ b, g a b
rhs : α✝ := ⨆ h, ⨅ a, g a (h a)
x : α✝
hr : rhs < x
hl : x < lhs
f : (a : α) → β a
hf : ∀ (a : α), x < g a (f a)
⊢ x ≤ ⨅ a, g a (f a)
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α✝ : Type u
β✝ : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLinearOrder α✝
α : Type u
β : α → Type u
g : (a : α) → β a → α✝
lhs : α✝ := ⨅ a, ⨆ b, g a b
rhs : α✝ := ⨆ h, ⨅ a, g a (h a)
hrl : rhs < lhs
h : ∀ (x : α✝), x ≤ rhs ∨ lhs ≤ x
f : (a : α) → β a
hf : ∀ (a : α), rhs < g a (f a)
this : ∀ (a : α), lhs ≤ g a (f a)
⊢ lhs ≤ rhs

Tactic:
refine le_trans ?_ (le_iSup _ f)

Goal state after:
α✝ : Type u
β✝ : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLinearOrder α✝
α : Type u
β : α → Type u
g : (a : α) → β a → α✝
lhs : α✝ := ⨅ a, ⨆ b, g a b
rhs : α✝ := ⨆ h, ⨅ a, g a (h a)
hrl : rhs < lhs
h : ∀ (x : α✝), x ≤ rhs ∨ lhs ≤ x
f : (a : α) → β a
hf : ∀ (a : α), rhs < g a (f a)
this : ∀ (a : α), lhs ≤ g a (f a)
⊢ lhs ≤ ⨅ a, g a (f a)
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: α : Type u_2
s : Set α
inst✝² : Preorder α
inst✝¹ : InfSet α
inst✝ : Inhabited ↑s
t : Set ↑s
ht : ¬BddBelow t
⊢ sInf t = default

Tactic:
simp [sInf, ht]

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
a : α
f : ι → ↑(Iic a)
⊢ ↑(sSup (range fun i ↦ f i)) = ⨆ i, ↑(f i)

Tactic:
coe_sSup

Goal state after:
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
a : α
f : ι → ↑(Iic a)
⊢ sSup (Subtype.val '' range fun i ↦ f i) = ⨆ i, ↑(f i)
Module: Mathlib.Tactic.NormNum.Abs

Goal state before:
pp: α : Type u_1
inst✝² : DivisionRing α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
num den : ℕ
ha1 : Invertible ↑den
⊢ IsNNRat |↑(Int.negOfNat num) * ⅟↑den| num den

Tactic:
simp only [Int.cast_negOfNat, neg_mul, abs_neg]

Goal state after:
α : Type u_1
inst✝² : DivisionRing α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
num den : ℕ
ha1 : Invertible ↑den
⊢ IsNNRat |↑num * ⅟↑den| num den
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: m n : ℕ
h : m ≤ n
⊢ m ! ∣ n !

Tactic:
induction h with
  | refl => exact Nat.dvd_refl _
  | step _ ih => exact Nat.dvd_trans ih (Nat.dvd_mul_left _ _)

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

Goal state before:
pp: k : Type u_4
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : FloorRing k
a b : k
ha : a ≠ 0
⊢ fract (b / a) * a + ⌊b / a⌋ • a = b

Tactic:
rw [zsmul_eq_mul, ← add_mul, fract_add_floor, div_mul_cancel₀ b ha]

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

Goal state before:
pp: case inr.refine_1
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ 0 ≤ ↑(m % n) / ↑n

pp: case inr.refine_2
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ ↑(m % n) / ↑n < 1

pp: case inr.refine_3
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ ↑m / ↑n - ↑(m % n) / ↑n = ↑(↑m / ↑n)

Tactic:
· positivity

Goal state after:
case inr.refine_2
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ ↑(m % n) / ↑n < 1

case inr.refine_3
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ ↑m / ↑n - ↑(m % n) / ↑n = ↑(↑m / ↑n)
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case inr
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
m : ℤ
n : ℕ
hn : 0 < ↑n
l₀ : ℕ
hl : 0 ≤ -↑l₀
⊢ fract (↑(-↑l₀) / ↑n) = ↑(-↑l₀ % ↑n) / ↑n

Tactic:
rw [Right.nonneg_neg_iff, natCast_nonpos_iff] at hl
      simp [hl]

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
a b : R
⊢ ⌈a + b⌉ ≤ ⌈a⌉ + ⌈b⌉

Tactic:
by
  rw [ceil_le, Int.cast_add]
  gcongr <;> apply le_ceil

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

Goal state before:
pp: case refine_1
K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
x y : K
inst✝ : ExistsAddOfLE K
xpos : 0 < x
hx : x ≤ 1
ypos : 0 < y
hy : y < 1
n : ℕ
hn : y⁻¹ ^ n ≤ x⁻¹
h'n : x⁻¹ < (y ^ (n + 1))⁻¹
⊢ y ^ (n + 1) < x

Tactic:
inv_lt_inv₀ xpos (pow_pos ypos _)

Goal state after:
case refine_1
K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
x y : K
inst✝ : ExistsAddOfLE K
xpos : 0 < x
hx : x ≤ 1
ypos : 0 < y
hy : y < 1
n : ℕ
hn : y⁻¹ ^ n ≤ x⁻¹
h'n : y ^ (n + 1) < x
⊢ y ^ (n + 1) < x
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 • a)) (f (l + (k + 1) • a))

Tactic:
add_comm k 1,

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)
hn : 1 < n
k : ℤ
⊢ R (f (l + k • a)) (f (l + (1 + k) • 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
ha : 0 ≤ a
⊢ ↑⌈a⌉₊ = ↑⌈a⌉

Tactic:
by
  rw [← Int.natCast_ceil_eq_ceil ha, Int.cast_natCast]

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

Goal state before:
pp: G : Type u_1
G' : Type u_2
P : Type u_3
P' : Type u_4
inst✝³ : Group G
inst✝² : Group G'
inst✝¹ : Torsor G P
inst✝ : Torsor G' P'
s₁ s₂ : Set P
t₁ t₂ : Set P'
⊢ s₁ ×ˢ t₁ /ₛ s₂ ×ˢ t₂ = (s₁ /ₛ s₂) ×ˢ (t₁ /ₛ t₂)

Tactic:
by
  aesop (add norm simp [mem_sdiv, mem_prod])

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

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
inst✝ : IsEmpty α
⊢ ∀ (a : Multiset α), a = 0

Tactic:
rintro ⟨_ | ⟨a, l⟩⟩; exacts [rfl, isEmptyElim a]

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

Goal state before:
pp: α : Type u_1
s : Multiset α
n : ℕ
⊢ s.card = n + 1 ↔ ∃ a t, a ::ₘ t = s ∧ t.card = n

Tactic:
refine ⟨?_, by aesop⟩
  induction s using Multiset.induction generalizing n with aesop

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

Goal state before:
pp: case inl
α : Type u
l : List α
h : ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length), i < j → l[i] ≠ l[j]
i : ℕ
hi : i < l.length
j : ℕ
hj : j < l.length
hg : (fun i ↦ l[↑i]) ⟨i, hi⟩ = (fun i ↦ l[↑i]) ⟨j, hj⟩
hij : i < j
⊢ ⟨i, hi⟩ = ⟨j, hj⟩

pp: case inr.inl
α : Type u
l : List α
h : ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length), i < j → l[i] ≠ l[j]
i : ℕ
hi hj : i < l.length
hg : (fun i ↦ l[↑i]) ⟨i, hi⟩ = (fun i ↦ l[↑i]) ⟨i, hj⟩
⊢ ⟨i, hi⟩ = ⟨i, hj⟩

pp: case inr.inr
α : Type u
l : List α
h : ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length), i < j → l[i] ≠ l[j]
i : ℕ
hi : i < l.length
j : ℕ
hj : j < l.length
hg : (fun i ↦ l[↑i]) ⟨i, hi⟩ = (fun i ↦ l[↑i]) ⟨j, hj⟩
hji : j < i
⊢ ⟨i, hi⟩ = ⟨j, hj⟩

Tactic:
· exact (h i j hi hj hij hg).elim

Goal state after:
case inr.inl
α : Type u
l : List α
h : ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length), i < j → l[i] ≠ l[j]
i : ℕ
hi hj : i < l.length
hg : (fun i ↦ l[↑i]) ⟨i, hi⟩ = (fun i ↦ l[↑i]) ⟨i, hj⟩
⊢ ⟨i, hi⟩ = ⟨i, hj⟩

case inr.inr
α : Type u
l : List α
h : ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length), i < j → l[i] ≠ l[j]
i : ℕ
hi : i < l.length
j : ℕ
hj : j < l.length
hg : (fun i ↦ l[↑i]) ⟨i, hi⟩ = (fun i ↦ l[↑i]) ⟨j, hj⟩
hji : j < i
⊢ ⟨i, hi⟩ = ⟨j, hj⟩
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: α : Type u_1
s t : Multiset α
⊢ s ≤ s + t

Tactic:
simpa using Multiset.add_le_add_left (zero_le t)

Goal state after: