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

Goal state before:
pp: F : Type u_6
α : Type u_7
β : Type u_8
inst✝² : LE α
inst✝¹ : LE β
inst✝ : FunLike F α β
⊢ (RelHomClass F (fun x1 x2 ↦ x1 ≤ x2) fun x1 x2 ↦ x1 ≤ x2) = RelHomClass F (fun x1 x2 ↦ x2 ≤ x1) fun x1 x2 ↦ x2 ≤ x1

Tactic:
grind only [RelHomClass]

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

Goal state before:
pp: M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulRightMono M
x : M
hx : 1 ≤ x
n : ℕ
⊢ 1 ≤ x ^ (n + 1)

Tactic:
rw [pow_succ]
    exact Right.one_le_mul (Right.one_le_pow_of_le hx) hx

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

Goal state before:
pp: s t : ℤ
r' : ℕ
s' t' : ℤ
⊢ Nat.strongRec (motive := fun x ↦ ℤ → ℤ → ℕ → ℤ → ℤ → ℕ × ℤ × ℤ)
      (fun n ih s t r' s' t' ↦
        match n, ih with
        | 0, ih => (r', s', t')
        | k.succ, ih =>
          have q := r' / k.succ;
          ih (r' % k.succ) ⋯ (s' - ↑q * s) (t' - ↑q * t) k.succ s t)
      0 s t r' s' t' =
    (r', s', t')

Tactic:
Nat.strongRec_eq

Goal state after:
s t : ℤ
r' : ℕ
s' t' : ℤ
⊢ (match 0, fun m x ↦
      Nat.strongRec (motive := fun x ↦ ℤ → ℤ → ℕ → ℤ → ℤ → ℕ × ℤ × ℤ)
        (fun n ih s t r' s' t' ↦
          match n, ih with
          | 0, ih => (r', s', t')
          | k.succ, ih =>
            have q := r' / k.succ;
            ih (r' % k.succ) ⋯ (s' - ↑q * s) (t' - ↑q * t) k.succ s t)
        m with
    | 0, ih => (r', s', t')
    | k.succ, ih =>
      have q := r' / k.succ;
      ih (r' % k.succ) ⋯ (s' - ↑q * s) (t' - ↑q * t) k.succ s t) =
    (r', s', t')
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: s t : ℤ
r' : ℕ
s' t' : ℤ
r : ℕ
h : 0 < r.succ
⊢ Nat.strongRec (motive := fun x ↦ ℤ → ℤ → ℕ → ℤ → ℤ → ℕ × ℤ × ℤ)
      (fun n ih s t r' s' t' ↦
        match n, ih with
        | 0, ih => (r', s', t')
        | k.succ, ih =>
          have q := r' / k.succ;
          ih (r' % k.succ) ⋯ (s' - ↑q * s) (t' - ↑q * t) k.succ s t)
      r.succ s t r' s' t' =
    (r' % r.succ).xgcdAux (s' - ↑r' / ↑r.succ * s) (t' - ↑r' / ↑r.succ * t) r.succ s t

Tactic:
Nat.strongRec_eq

Goal state after:
s t : ℤ
r' : ℕ
s' t' : ℤ
r : ℕ
h : 0 < r.succ
⊢ (match r.succ, fun m x ↦
      Nat.strongRec (motive := fun x ↦ ℤ → ℤ → ℕ → ℤ → ℤ → ℕ × ℤ × ℤ)
        (fun n ih s t r' s' t' ↦
          match n, ih with
          | 0, ih => (r', s', t')
          | k.succ, ih =>
            have q := r' / k.succ;
            ih (r' % k.succ) ⋯ (s' - ↑q * s) (t' - ↑q * t) k.succ s t)
        m with
    | 0, ih => (r', s', t')
    | k.succ, ih =>
      have q := r' / k.succ;
      ih (r' % k.succ) ⋯ (s' - ↑q * s) (t' - ↑q * t) k.succ s t) =
    (r' % r.succ).xgcdAux (s' - ↑r' / ↑r.succ * s) (t' - ↑r' / ↑r.succ * t) r.succ s t
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: s : ℕ
⊢ (Nat.strongRec (motive := fun x ↦ ℤ → ℤ → ℕ → ℤ → ℤ → ℕ × ℤ × ℤ)
          (fun n ih s t r' s' t' ↦
            match n, ih with
            | 0, ih => (r', s', t')
            | k.succ, ih =>
              have q := r' / k.succ;
              ih (r' % k.succ) ⋯ (s' - ↑q * s) (t' - ↑q * t) k.succ s t)
          0 1 0 s 0 1).2.1 =
    0

Tactic:
Nat.strongRec_eq

Goal state after:
s : ℕ
⊢ (match 0, fun m x ↦
          Nat.strongRec (motive := fun x ↦ ℤ → ℤ → ℕ → ℤ → ℤ → ℕ × ℤ × ℤ)
            (fun n ih s t r' s' t' ↦
              match n, ih with
              | 0, ih => (r', s', t')
              | k.succ, ih =>
                have q := r' / k.succ;
                ih (r' % k.succ) ⋯ (s' - ↑q * s) (t' - ↑q * t) k.succ s t)
            m with
        | 0, ih => (s, 0, 1)
        | k.succ, ih =>
          have q := s / k.succ;
          ih (s % k.succ) ⋯ (0 - ↑q * 1) (1 - ↑q * 0) k.succ 1 0).2.1 =
    0
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: s : ℕ
⊢ (Nat.strongRec (motive := fun x ↦ ℤ → ℤ → ℕ → ℤ → ℤ → ℕ × ℤ × ℤ)
          (fun n ih s t r' s' t' ↦
            match n, ih with
            | 0, ih => (r', s', t')
            | k.succ, ih =>
              have q := r' / k.succ;
              ih (r' % k.succ) ⋯ (s' - ↑q * s) (t' - ↑q * t) k.succ s t)
          0 1 0 s 0 1).2.2 =
    1

Tactic:
Nat.strongRec_eq

Goal state after:
s : ℕ
⊢ (match 0, fun m x ↦
          Nat.strongRec (motive := fun x ↦ ℤ → ℤ → ℕ → ℤ → ℤ → ℕ × ℤ × ℤ)
            (fun n ih s t r' s' t' ↦
              match n, ih with
              | 0, ih => (r', s', t')
              | k.succ, ih =>
                have q := r' / k.succ;
                ih (r' % k.succ) ⋯ (s' - ↑q * s) (t' - ↑q * t) k.succ s t)
            m with
        | 0, ih => (s, 0, 1)
        | k.succ, ih =>
          have q := s / k.succ;
          ih (s % k.succ) ⋯ (0 - ↑q * 1) (1 - ↑q * 0) k.succ 1 0).2.2 =
    1
Module: Mathlib.Algebra.Order.Group.Nat

Goal state before:
pp: case succ
m n : ℕ
ih : ∀ (k : ℕ), m - n ≤ k ↔ m ≤ k + n
k : ℕ
⊢ m - (n + 1) ≤ k ↔ m ≤ k + (n + 1)

Tactic:
simp only [sub_succ, pred_le_iff, ih, succ_add, add_succ]

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs

Goal state before:
pp: case inr
α : Type u
inst✝² : Monoid α
inst✝¹ : LinearOrder α
inst✝ : CanonicallyOrderedMul α
a b c : α
hb : b ≤ a
⊢ min a (b * c) = min a (min a b * min a c)

Tactic:
rcases le_total a c with hc | hc

Goal state after:
case inr.inl
α : Type u
inst✝² : Monoid α
inst✝¹ : LinearOrder α
inst✝ : CanonicallyOrderedMul α
a b c : α
hb : b ≤ a
hc : a ≤ c
⊢ min a (b * c) = min a (min a b * min a c)

case inr.inr
α : Type u
inst✝² : Monoid α
inst✝¹ : LinearOrder α
inst✝ : CanonicallyOrderedMul α
a b c : α
hb : b ≤ a
hc : c ≤ a
⊢ min a (b * c) = min a (min a b * min a c)
Module: Mathlib.Algebra.Group.WithOne.Defs

Goal state before:
pp: α : Type u
d y : α
x : WithOne α
⊢ unoneD d x = y ↔ x = ↑y ∨ x = 1 ∧ y = d

Tactic:
induction x <;> simp [@eq_comm _ d]

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

Goal state before:
pp: case inl
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
h : a ≤ b
⊢ a - b = a - min a b

Tactic:
rw [min_eq_left h, tsub_self, tsub_eq_zero_of_le h]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
d y : α
x : WithBot α
⊢ unbotD d x = y ↔ x = ↑y ∨ x = ⊥ ∧ y = d

Tactic:
induction x <;> simp [@eq_comm _ d]

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

Goal state before:
pp: α : Type u_3
a : WithZero (Multiplicative α)
h : a ≠ 0
b : α
k : a = ↑(ofAdd b)
⊢ toAdd (unzero h) = b

Tactic:
subst k; rfl

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
⊢ ⌊↑0⌋₊ = 0

Tactic:
floor_natCast

Goal state after:
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
⊢ 0 = 0
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
⊢ ⌊↑1⌋₊ = 1

Tactic:
floor_natCast

Goal state after:
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
⊢ 1 = 1
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
⊢ ⌈0⌉₊ = 0

Tactic:
rw [← Nat.cast_zero, ceil_natCast]

Goal state after:
Module: Mathlib.Algebra.Group.Invertible.Defs

Goal state before:
pp: α : Type u
inst✝¹ : Monoid α
a b : α
inst✝ : Invertible a
h : ⅟a = b
⊢ a * b = 1

Tactic:
by rw [← h, mul_invOf_self]

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:
obtain ⟨r₁, hdr₁, hpr₁, hqr₁⟩ := h₁ _ hpd.1 _ hqd.1

Goal state after:
α : 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₂
r₁ : α
hdr₁ : r₁ ∈ d₁
hpr₁ : r x✝¹.1 r₁
hqr₁ : r x✝.1 r₁
⊢ ∃ 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
Module: Mathlib.Algebra.Order.Ring.Basic

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a b : R
inst✝ : ExistsAddOfLE R
⊢ (a + b) ^ 2 = a ^ 2 + b ^ 2 + (a * b + b * a)

Tactic:
pow_succ',

Goal state after:
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a b : R
inst✝ : ExistsAddOfLE R
⊢ (a + b) * ((a + b) * (a + b) ^ 0) = a * (a * a ^ 0) + b * (b * b ^ 0) + (a * b + b * a)
Module: Mathlib.Algebra.Order.Ring.Basic

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a b : R
inst✝ : ExistsAddOfLE R
⊢ a ^ 2 + b ^ 2 + (a * a + b * b) = 2 * (a ^ 2 + b ^ 2)

Tactic:
pow_succ',

Goal state after:
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a b : R
inst✝ : ExistsAddOfLE R
⊢ a * (a * a ^ 0) + b * (b * b ^ 0) + (a * a + b * b) = 2 * (a * (a * a ^ 0) + b * (b * b ^ 0))
Module: Mathlib.Algebra.Order.Ring.Basic

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : a ≤ 0
hb : b ≤ 0
c : R
hac : 0 = a + c
d : R
hbd : 0 = b + d
hd : 0 ≤ d
⊢ c ^ n = b ^ n + (c ^ n + d ^ n)

Tactic:
rw [add_left_comm, hn.pow_add_pow_eq_zero hbd.symm, add_zero]

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

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝¹ : PartialOrder α
inst✝ : LinearOrder β
φ : β → α
ψ : α → β
t : Set β
s : Set α
hφ : MonotoneOn φ t
φψs : RightInvOn ψ φ s
ψts : MapsTo ψ s t
⊢ MonotoneOn ψ s

Tactic:
rintro x xs y ys l
  rcases le_total (ψ x) (ψ y) with (ψxy | ψyx)
  · exact ψxy
  · have := hφ (ψts ys) (ψts xs) ψyx
    rw [φψs.eq ys, φψs.eq xs] at this
    induction le_antisymm l this
    exact le_refl _

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

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
h : a ^ 2 < b ^ 2
hb : 0 ≤ b
⊢ |a| < b

Tactic:
rwa [← abs_of_nonneg hb, ← sq_lt_sq]

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
ε : Type u_9
ε' : Type u_10
s : Set α
t : Set β
u : Set γ
f : δ → γ → ε
g : α → β → δ
f' : α → ε' → ε
g' : β → γ → ε'
h_assoc : ∀ (a : α) (b : β) (c : γ), f (g a b) c = f' a (g' b c)
x✝ : Set ε
⊢ image2 f (image2 g s t) u ⊆ x✝ ↔ image2 f' s (image2 g' t u) ⊆ x✝

Tactic:
by simp only [image2_subset_iff, forall_mem_image2, h_assoc]

Goal state after:
Module: Mathlib.Order.Antisymmetrization

Goal state before:
pp: α : Type u_1
a b : α
inst✝ : Preorder α
⊢ a ≤ b ↔ a < b ∨ AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) a b

Tactic:
lt_iff_le_not_ge,

Goal state after:
α : Type u_1
a b : α
inst✝ : Preorder α
⊢ a ≤ b ↔ a ≤ b ∧ ¬b ≤ a ∨ AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) a b
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
a b : α
inst✝ : DenselyOrdered α
⊢ Ioo a b = ∅ ↔ ¬a < b

Tactic:
contrapose!; exact nonempty_Ioo

Goal state after:
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'
y' : α
hy' : y' ∈ s
hyy' : y ≤ y'
z : α
hz : z ∈ s
hx'z : x' ≤ z
hy'z : y' ≤ z
⊢ ∃ z ∈ s ∪ t, (fun x1 x2 ↦ x1 ≤ x2) x z ∧ (fun x1 x2 ↦ x1 ≤ x2) y z

Tactic:
exact ⟨z, .inl hz, hxx'.trans hx'z, hyy'.trans hy'z⟩

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

Goal state before:
pp: case eq
α : Type u_1
inst✝ : Semiring α
na nb nc da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁✝ : na * db + nb * da = k * nc
h₂✝ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
h₁ : ↑na * ⅟↑da + ↑nb * ⅟↑db = ↑k * ↑nc * ⅟↑db * ⅟↑da
h₂ : ↑nc * ⅟↑dc = ↑nc * ↑k * ↑dc * ⅟↑db * ⅟↑da * ⅟↑dc
⊢ ↑nc * ↑k * ⅟↑db * ⅟↑da = ↑nc * ↑k * ↑dc * ⅟↑db * ⅟↑da * ⅟↑dc

Tactic:
simp only [mul_invOf_cancel_right,
    (Nat.cast_commute (α := α) da dc).invOf_left.invOf_right.right_comm,
    (Nat.cast_commute (α := α) db dc).invOf_left.invOf_right.right_comm]

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

Goal state before:
pp: case cons
M : Type u_2
inst✝¹ : Mul M
inst✝ : One M
l✝ : List M
p : M → Prop
hom : ∀ (a b : M), p a → p b → p (a * b)
unit : p 1
a : M
l : List M
ih : (∀ (x : M), x ∈ l → p x) → p l.prod
base : ∀ (x : M), x ∈ a :: l → p x
⊢ p (a :: l).prod

Tactic:
rw [List.prod_cons]

Goal state after:
case cons
M : Type u_2
inst✝¹ : Mul M
inst✝ : One M
l✝ : List M
p : M → Prop
hom : ∀ (a b : M), p a → p b → p (a * b)
unit : p 1
a : M
l : List M
ih : (∀ (x : M), x ∈ l → p x) → p l.prod
base : ∀ (x : M), x ∈ a :: l → p x
⊢ p (a * l.prod)
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: case eq
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁✝ : na * ↑db + nb * ↑da = ↑k * nc
h₂✝ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
h₁ : ↑na * ⅟↑da + ↑nb * ⅟↑db = ↑k * ↑nc * ⅟↑db * ⅟↑da
h₂ : ↑nc * ⅟↑dc = ↑nc * ↑k * ↑dc * ⅟↑db * ⅟↑da * ⅟↑dc
⊢ ↑nc * ↑k * ⅟↑db * ⅟↑da = ↑nc * ↑k * ↑dc * ⅟↑db * ⅟↑da * ⅟↑dc

Tactic:
simp only [mul_invOf_cancel_right,
    (Nat.cast_commute (α := α) da dc).invOf_left.invOf_right.right_comm,
    (Nat.cast_commute (α := α) db dc).invOf_left.invOf_right.right_comm]

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

Goal state before:
pp: case neg
M : Type u_2
inst✝ : MulOneClass M
l✝ : List M
p : M → Prop
hom : ∀ (a b : M), p a → p b → p (a * b)
a : M
l : List M
ih : l ≠ [] → (∀ (x : M), x ∈ l → p x) → p l.prod
hl : a :: l ≠ []
base : ∀ (x : M), x ∈ a :: l → p x
hl_empty : ¬l = []
⊢ p (a :: l).prod

Tactic:
rw [List.prod_cons]

Goal state after:
case neg
M : Type u_2
inst✝ : MulOneClass M
l✝ : List M
p : M → Prop
hom : ∀ (a b : M), p a → p b → p (a * b)
a : M
l : List M
ih : l ≠ [] → (∀ (x : M), x ∈ l → p x) → p l.prod
hl : a :: l ≠ []
base : ∀ (x : M), x ∈ a :: l → p x
hl_empty : ¬l = []
⊢ p (a * l.prod)
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁✝ : na * nb = ↑k * nc
h₂✝ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
h₁ : ↑na * ↑nb = ↑k * ↑nc
h₂ : ↑nc * ⅟↑dc = ↑nc * ↑k * ↑dc * ⅟↑da * ⅟↑db * ⅟↑dc
⊢ ↑nc * ↑k * ⅟↑da * ⅟↑db = ↑nc * ↑k * ↑dc * ⅟↑da * ⅟↑db * ⅟↑dc

Tactic:
simp only [mul_invOf_cancel_right,
    (Nat.cast_commute (α := α) da dc).invOf_left.invOf_right.right_comm,
    (Nat.cast_commute (α := α) db dc).invOf_left.invOf_right.right_comm]

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

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b : α
ha : a < 0
hb : b < 0
⊢ a⁻¹ ≤ b ↔ b⁻¹ ≤ a

Tactic:
rw [← inv_le_inv_of_neg hb (inv_lt_zero'.2 ha), inv_inv]

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

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b : α
ha : a < 0
hb : b < 0
⊢ a ≤ b⁻¹ ↔ b ≤ a⁻¹

Tactic:
rw [← inv_le_inv_of_neg (inv_lt_zero'.2 hb) ha, inv_inv]

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

Goal state before:
pp: α : Type u
n : ℕ
a : α
l : List α
b : α
hb : b ∈ l.insertIdx n a
⊢ b ∈ a :: l

Tactic:
simpa using eq_or_mem_of_mem_insertIdx hb

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

Goal state before:
pp: case neg
α : Type u
inst✝ : DecidableEq α
a b : α
l : List α
h : a ∈ b :: l
hab : ¬a = b
⊢ a = b ∨ a ≠ b ∧ a ∈ l

Tactic:
exact ((List.mem_cons.1 h).elim Or.inl (fun h => Or.inr ⟨hab, h⟩))

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
a b : α
m n : ℕ
h : a ≠ b
this : l ⊆ [a, b] ↔ ∀ (c : α), c ≠ b → c ≠ a → ¬c ∈ l
⊢ (count a l = count a (replicate m a ++ replicate n b) ∧
      (b ≠ a → count b l = count b (replicate m a ++ replicate n b)) ∧
        ∀ (b_1 : α), b_1 ≠ b → b_1 ≠ a → count b_1 l = count b_1 (replicate m a ++ replicate n b)) ↔
    count a l = m ∧ count b l = n ∧ l ⊆ [a, b]

Tactic:
simp +contextual [count_replicate, h, this, count_eq_zero, Ne.symm]

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

Goal state before:
pp: case cons
M : Type u_4
inst✝ : Monoid M
y z : M
l : List M
IH : (∀ (x : M), x ∈ l → Commute y x) → Commute y l.prod
h : Commute y z ∧ ∀ (x : M), x ∈ l → Commute y x
⊢ Commute y (z :: l).prod

Tactic:
rw [List.prod_cons]

Goal state after:
case cons
M : Type u_4
inst✝ : Monoid M
y z : M
l : List M
IH : (∀ (x : M), x ∈ l → Commute y x) → Commute y l.prod
h : Commute y z ∧ ∀ (x : M), x ∈ l → Commute y x
⊢ Commute y (z * l.prod)
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case cons
α : Type u
β : Type v
f g : α → β → α
hd : β
tl : List β
ih : ∀ (a : α), (∀ (a : α) (b : β), b ∈ tl → f a b = g a b) → foldl f a tl = foldl g a tl
a : α
H : ∀ (a : α) (b : β), b ∈ hd :: tl → f a b = g a b
⊢ foldl f (f a hd) tl = foldl g (g a hd) tl

Tactic:
ih _ fun a b bin => H a b <| mem_cons_of_mem _ bin,

Goal state after:
case cons
α : Type u
β : Type v
f g : α → β → α
hd : β
tl : List β
ih : ∀ (a : α), (∀ (a : α) (b : β), b ∈ tl → f a b = g a b) → foldl f a tl = foldl g a tl
a : α
H : ∀ (a : α) (b : β), b ∈ hd :: tl → f a b = g a b
⊢ foldl g (f a hd) tl = foldl g (g a hd) tl
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: q : ℚ
n₁ n₂ : ℤ
d₁ d₂ : ℕ
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
hnd₁ : n₁.natAbs.Coprime d₁
hnd₂ : n₂.natAbs.Coprime d₂
h₁₂ : n₁.natAbs.Coprime d₂
h₂₁ : n₂.natAbs.Coprime d₁
⊢ (n₁ * n₂).natAbs.Coprime (d₁ * d₂)

Tactic:
rw [Int.natAbs_mul]

Goal state after:
q : ℚ
n₁ n₂ : ℤ
d₁ d₂ : ℕ
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
hnd₁ : n₁.natAbs.Coprime d₁
hnd₂ : n₂.natAbs.Coprime d₂
h₁₂ : n₁.natAbs.Coprime d₂
h₂₁ : n₂.natAbs.Coprime d₁
⊢ (n₁.natAbs * n₂.natAbs).Coprime (d₁ * d₂)
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: q r : ℚ
⊢ q * r = mkRat (q.num * r.num) (q.den * r.den)

Tactic:
by
  rw [mul_def, normalize_eq_mkRat]

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

Goal state before:
pp: q : ℚ
⊢ |q|.num = |q.num|

Tactic:
rw [abs_def']

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

Goal state before:
pp: q : ℚ
⊢ |q|.den = q.den

Tactic:
rw [abs_def']

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

Goal state before:
pp: case pos
K : Type u_1
inst✝ : NNRatCast K
m : ℕ
b : Bool
d : ℕ
h✝ : b = true
⊢ ↑⟨OfScientific.ofScientific m b d, ⋯⟩ = ↑(NNRat.divNat m (10 ^ d))

Tactic:
congr 2
    rw [← Rat.ofScientific_eq_ofScientific, Rat.ofScientific_def, if_pos ‹_›]
    congr

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

Goal state before:
pp: p q : ℚ≥0
h : q ≤ p
⊢ ↑q ≤ ↑p - 0

Tactic:
by rwa [sub_zero]

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

Goal state before:
pp: n : ℤ
q : ℚ
⊢ (↑n + -q).den = q.den

Tactic:
intCast_add_den,

Goal state after:
n : ℤ
q : ℚ
⊢ (-q).den = q.den
Module: Mathlib.Data.Nat.Set

Goal state before:
pp: case e'_4
α : Type u_2
x : α
f : ℕ → α → α
n : ℕ
⊢ rec (f 0 x) (f ∘ succ) n = f n (rec x f n)

Tactic:
induction n with
  | zero => rfl
  | succ n ihn => dsimp at ihn ⊢; rw [ihn]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
ι' : Sort u_5
inst✝ : SupSet α
f : ι → α
g : ι' → α
h : ι → ι'
h1 : Surjective h
h2 : ∀ (x : ι), g (h x) = f x
⊢ ⨆ x, f x = ⨆ y, g y

Tactic:
convert! h1.iSup_comp g
  exact (h2 _).symm

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

Goal state before:
pp: α : Type u_1
inst✝² : CompleteLattice α
ι : Type u_8
inst✝¹ : LT ι
inst✝ : NoMinOrder ι
f : ι → α
⊢ ⨆ i, ⨆ j, ⨆ (_ : j > i), f j = ⨆ i, f i

Tactic:
apply le_antisymm
  · exact iSup_le fun _ ↦ iSup₂_le fun _ _ ↦ le_iSup _ _
  · refine iSup_le fun j ↦ ?_
    obtain ⟨i, jlt⟩ := exists_lt j
    exact le_iSup_of_le i (le_iSup₂_of_le j jlt le_rfl)

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLattice α
minAx : MinimalAxioms α
f : (a : ι) → κ a → α
⊢ ⨅ i, ⨆ j, f i j = ⨅ a, ⨆ b, ↑b

Tactic:
by
      simp_rw [iInf_subtype, iInf_range, iSup_subtype, iSup_range]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case neg
α : Type u
inst✝ : CompletelyDistribLattice α
ι : Type u_1
κ : Type u_2
f : ι → α
h : Pairwise (Disjoint on f)
s : κ → Set ι
j : κ
I : κ → ι
hI : ∀ (a : κ), I a ∈ s a
H : ∃ k, I k ≠ I j
⊢ ⨅ a, f (I a) ≤ ⨆ i, ⨆ (_ : ∀ (i_1 : κ), i ∈ s i_1), f i

Tactic:
rcases H with ⟨k, hk⟩
    calc ⨅ l, f (I l)
    _ ≤ f (I k) ⊓ f (I j) := le_inf (iInf_le _ _) (iInf_le _ _)
    _ = ⊥ := (h hk).eq_bot
    _ ≤ _ := bot_le

Goal state after:
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 β
top : Top α := e.top
bot : Bot α := e.bot
supSet : SupSet α := e.supSet
⊢ CompleteLattice α

Tactic:
let infSet := e.infSet

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
e : α ≃ β
inst✝ : CompleteLattice β
top : Top α := e.top
bot : Bot α := e.bot
supSet : SupSet α := e.supSet
infSet : InfSet α := e.infSet
⊢ CompleteLattice α
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Sort u_4
ι : Type u_5
α : ι → Type u_6
inst✝ : (i : ι) → ConditionallyCompleteLattice (α i)
x✝¹ : Set ((i : ι) → α i)
hn : x✝¹.Nonempty
hb : BddBelow x✝¹
x✝ : ι
⊢ IsGLB (eval x✝ '' x✝¹) (sInf x✝¹ x✝)

Tactic:
by
    rw [sInf_apply_eq_sInf_image]
    exact isGLB_csInf (image_nonempty.mpr hn) ((monotone_eval _).map_bddBelow hb)

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

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set α
a : α
hb : BddAbove s
⊢ a < sSup s ↔ ∃ b ∈ s, a < b

Tactic:
by
  simpa only [not_le, not_forall₂, exists_prop] using (csSup_le_iff' hb).not

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

Goal state before:
pp: β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
⊢ IsGLB s (sInf s)

Tactic:
classical
  constructor
  · change ite _ _ _ ∈ _
    simp only [hs, not_true_eq_false, or_false]
    split_ifs with h
    · intro a ha
      exact top_le_iff.2 (Set.mem_singleton_iff.1 (h ha))
    · rintro (⟨⟩ | a) ha
      · exact le_top
      refine coe_le_coe.2 (csInf_le ?_ ha)
      rcases hs with ⟨⟨⟩ | b, hb⟩
      · exfalso
        apply h
        intro c hc
        rw [mem_singleton_iff, ← top_le_iff]
        exact hb hc
      use b
      intro c hc
      exact coe_le_coe.1 (hb hc)
  · change ite _ _ _ ∈ _
    simp only [hs, not_true_eq_false, or_false]
    split_ifs with h
    · intro _ _
      exact le_top
    · rintro (⟨⟩ | a) ha
      · exfalso
        apply h
        intro b hb
        exact Set.mem_singleton_iff.2 (top_le_iff.1 (ha hb))
      · refine coe_le_coe.2 (le_csInf ?_ ?_)
        · classical
            contrapose! h
            rintro (⟨⟩ | a) ha
            · exact mem_singleton ⊤
            · exact (not_nonempty_iff_eq_empty.2 h ⟨a, ha⟩).elim
        · intro b hb
          rw [← coe_le_coe]
          exact ha hb

Goal state after: