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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a b : α
hf : MonotoneOn f s
ha : a ∈ s
hb : b ∈ s
⊢ f (max a b) = max (f a) (f b)

Tactic:
rcases le_total a b with h | h <;>
    simp only [max_eq_right, max_eq_left, hf ha hb, hf hb ha, h]

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

Goal state before:
pp: α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hc : AddLECancellable c
h : a - c < b
⊢ a < b + c

Tactic:
by
  rw [lt_iff_le_and_ne, ← tsub_le_iff_right]
  refine ⟨h.le, ?_⟩
  rintro rfl
  simp [hc] at h

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

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulLeftMono α
a b : α
⊢ b * 1 ≤ b * (b⁻¹ * a) ↔ b ≤ a

Tactic:
mul_one,

Goal state after:
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulLeftMono α
a b : α
⊢ b ≤ b * (b⁻¹ * a) ↔ b ≤ a
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulLeftStrictMono α
a b : α
⊢ b * 1 < b * (b⁻¹ * a) ↔ b < a

Tactic:
mul_one,

Goal state after:
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulLeftStrictMono α
a b : α
⊢ b < b * (b⁻¹ * a) ↔ b < a
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulLeftMono α
a b : α
⊢ a / b ≤ a ↔ 1 ≤ b

Tactic:
simp [div_eq_mul_inv]

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

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulLeftMono α
a b : α
⊢ a ≤ a / b ↔ b ≤ 1

Tactic:
simp [div_eq_mul_inv]

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

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulLeftStrictMono α
a b : α
⊢ a / b < a ↔ 1 < b

Tactic:
simp [div_eq_mul_inv]

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

Goal state before:
pp: α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c d : α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightMono α
h : a * b ≤ c * d
⊢ min a b ≤ max c d

Tactic:
simp_rw [min_le_iff, le_max_iff]; contrapose! h; exact mul_lt_mul_of_le_of_lt h.1.1.le h.2.2

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

Goal state before:
pp: α : Type u_1
inst✝² : MulOneClass α
inst✝¹ : LE α
inst✝ : MulRightReflectLE α
a b : α
h : b ≤ a * b
⊢ 1 * b ≤ a * b

Tactic:
by simpa only [one_mul]

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

Goal state before:
pp: α : Type u_1
inst✝² : MulOneClass α
inst✝¹ : LE α
inst✝ : MulRightReflectLE α
a b : α
h : a * b ≤ b
⊢ a * b ≤ 1 * b

Tactic:
by simpa only [one_mul]

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

Goal state before:
pp: α : Type u_1
inst✝² : MulOneClass α
inst✝¹ : LT α
inst✝ : MulRightReflectLT α
a b : α
h : b < a * b
⊢ 1 * b < a * b

Tactic:
by simpa only [one_mul]

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

Goal state before:
pp: α : Type u_1
inst✝² : MulOneClass α
inst✝¹ : LT α
inst✝ : MulRightReflectLT α
a b : α
h : a * b < b
⊢ a * b < 1 * b

Tactic:
by simpa only [one_mul]

Goal state after:
Module: Mathlib.Algebra.Ring.GrindInstances

Goal state before:
pp: α : Type u_1
s : Semiring α
n : ℕ
⊢ OfNat.ofNat (n + 2 + 1) = OfNat.ofNat (n + 2) + 1

Tactic:
change Nat.cast (n + 2 + 1) = Nat.cast (n + 2) + 1
      rw [← AddMonoidWithOne.natCast_succ]

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

Goal state before:
pp: case inl
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a c : G₀
hc : 0 ≤ c
hb : 0 ≤ 0
h : a ≤ 0 * c
⊢ 0⁻¹ * a ≤ c

pp: case inr
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c : G₀
hb✝ : 0 ≤ b
hc : 0 ≤ c
h : a ≤ b * c
hb : 0 < b
⊢ b⁻¹ * a ≤ c

Tactic:
· simp [hc]

Goal state after:
case inr
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c : G₀
hb✝ : 0 ≤ b
hc : 0 ≤ c
h : a ≤ b * c
hb : 0 < b
⊢ b⁻¹ * a ≤ c
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝² : Semiring R
inst✝¹ : LinearOrder R
b c : R
inst✝ : MulPosStrictMono R
h : 0 < c
⊢ 0 ≤ b * c ↔ 0 ≤ b

Tactic:
by
  simpa using (mul_le_mul_iff_left₀ h : 0 * c ≤ b * c ↔ 0 ≤ b)

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

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : ZeroLEOneClass G₀
ha : 1 < a
⊢ StrictMono fun n ↦ a ^ n

Tactic:
by
  refine strictMono_int_of_lt_succ fun n ↦ ?_
  rw [zpow_add_one₀ (zero_lt_one.trans ha).ne']
  exact lt_mul_of_one_lt_right (zpow_pos (zero_lt_one.trans ha) _) ha

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

Goal state before:
pp: case inl
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a c : G₀
hc : 0 ≤ c
hb : 0 ≤ 0
h : a ≤ c * 0
⊢ a * 0⁻¹ ≤ c

pp: case inr
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hb✝ : 0 ≤ b
hc : 0 ≤ c
h : a ≤ c * b
hb : 0 < b
⊢ a * b⁻¹ ≤ c

Tactic:
· simp [hc]

Goal state after:
case inr
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hb✝ : 0 ≤ b
hc : 0 ≤ c
h : a ≤ c * b
hb : 0 < b
⊢ a * b⁻¹ ≤ c
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LE α
inst✝² : LE β
inst✝¹ : EquivLike F α β
inst✝ : OrderIsoClass F α β
f : F
a : α
b : β
⊢ EquivLike.inv f b ≤ a ↔ b ≤ f a

Tactic:
convert! (map_le_map_iff f).symm
  exact (EquivLike.right_inv f _).symm

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

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
ha : 1 ≤ a ^ 2
⊢ a ^ 2 ⊓ 1 * a ⊓ (a ⊓ 1) * 1 = a ⊓ 1

Tactic:
mul_one,

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
ha : 1 ≤ a ^ 2
⊢ a ^ 2 ⊓ 1 * a ⊓ (a ⊓ 1) = a ⊓ 1
Module: Mathlib.Algebra.Order.Group.Abs

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b c : G
⊢ c⁻¹ < a / b ∧ a / b < c ↔ a / b < c ∧ b / a < c

Tactic:
inv_lt_div_iff_lt_mul',

Goal state after:
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b c : G
⊢ b < a * c ∧ a / b < c ↔ a / b < c ∧ b / a < c
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: α : Type u_1
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b : α
⊢ max a b / min a b = |a / b|ₘ

Tactic:
by
  rcases le_total a b with ab | ba
  · rw [max_eq_right ab, min_eq_left ab, mabs_of_le_one, inv_div]
    rwa [div_le_one']
  · rw [max_eq_left ba, min_eq_right ba, mabs_of_one_le]
    rwa [one_le_div']

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

Goal state before:
pp: s : ℕ
⊢ (xgcd 0 s).1 = 0

Tactic:
xgcd,

Goal state after:
s : ℕ
⊢ (xgcdAux 0 1 0 s 0 1).2.1 = 0
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: s : ℕ
⊢ (xgcd 0 s).2 = 1

Tactic:
xgcd,

Goal state after:
s : ℕ
⊢ (xgcdAux 0 1 0 s 0 1).2.2 = 1
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: x y : ℕ
⊢ x.xgcdAux 1 0 y 0 1 = (x.gcd y, x.xgcd y)

Tactic:
xgcd,

Goal state after:
x y : ℕ
⊢ x.xgcdAux 1 0 y 0 1 = (x.gcd y, (x.xgcdAux 1 0 y 0 1).2)
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: a b c : ℤ
habc : a ∣ b * c
hab : a.gcd c = 1
this✝ : 1 = a * a.gcdA c + c * a.gcdB c
this : b * a * a.gcdA c + b * c * a.gcdB c = b
⊢ a ∣ b * a * a.gcdA c + b * c * a.gcdB c

Tactic:
exact Int.dvd_add (dvd_mul_of_dvd_left (dvd_mul_left a b)) (dvd_mul_of_dvd_left habc)

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : AddCommGroupWithOne R
inst✝³ : PartialOrder R
inst✝² : AddLeftMono R
inst✝¹ : ZeroLEOneClass R
inst✝ : NeZero 1
n : ℤ
⊢ ↑n ≤ 0 ↔ n ≤ 0

Tactic:
rw [← cast_zero, cast_le]

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

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

Tactic:
mul_invOf_cancel_right

Goal state after:
α : Type u
inst✝¹ : Monoid α
a b c : α
inst✝ : Invertible c
⊢ a = b * ⅟c ↔ a = b * ⅟c
Module: Mathlib.Algebra.Group.Invertible.Basic

Goal state before:
pp: α : Type u
inst✝² : Monoid α
a b : α
inst✝¹ : Invertible a
inst✝ : Invertible (a * b)
⊢ 1 * a = a * 1

Tactic:
mul_one,

Goal state after:
α : Type u
inst✝² : Monoid α
a b : α
inst✝¹ : Invertible a
inst✝ : Invertible (a * b)
⊢ 1 * a = a
Module: Mathlib.Algebra.Group.Invertible.Basic

Goal state before:
pp: α : Type u
inst✝² : Monoid α
a b : α
inst✝¹ : Invertible (a * b)
inst✝ : Invertible b
⊢ b * 1 = 1 * b

Tactic:
mul_one,

Goal state after:
α : Type u
inst✝² : Monoid α
a b : α
inst✝¹ : Invertible (a * b)
inst✝ : Invertible b
⊢ b = 1 * b
Module: Mathlib.Algebra.Ring.Invertible

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : Invertible 2
⊢ 2 * 1 - 1 = 1

Tactic:
mul_one,

Goal state after:
R : Type u_1
inst✝¹ : Ring R
inst✝ : Invertible 2
⊢ 2 - 1 = 1
Module: Mathlib.Algebra.Ring.Invertible

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
a b : R
inst✝¹ : Invertible a
inst✝ : Invertible b
⊢ ⅟a + ⅟b = ⅟b + ⅟a * 1

Tactic:
mul_one,

Goal state after:
R : Type u_1
inst✝² : Semiring R
a b : R
inst✝¹ : Invertible a
inst✝ : Invertible b
⊢ ⅟a + ⅟b = ⅟b + ⅟a
Module: Mathlib.Algebra.Ring.Invertible

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
a b : R
h : IsUnit a ↔ IsUnit b
⊢ a⁻¹ʳ + b⁻¹ʳ = a⁻¹ʳ * (a + b) * b⁻¹ʳ

Tactic:
by
  by_cases ha : IsUnit a
  · have hb := h.mp ha
    obtain ⟨ia⟩ := ha.nonempty_invertible
    obtain ⟨ib⟩ := hb.nonempty_invertible
    simp_rw [inverse_invertible, invOf_add_invOf]
  · have hb := h.not.mp ha
    simp [inverse_non_unit, ha, hb]

Goal state after:
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) * ((a + b) * 1) = a * (a * 1) + b * (b * 1) + (a * b + b * a)

Tactic:
mul_one,

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 * a + b * b + (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 * (a * 1) + b * (b * 1) + (a * a + b * b) = 2 * (a * (a * 1) + b * (b * 1))

Tactic:
mul_one,

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

Goal state before:
pp: K : Type u_1
inst✝ : DivisionSemiring K
a b : K
hab : Commute a b
ha : a ≠ 0
hb : b ≠ 0
⊢ (b + a * 1) / (a * b) = (a + b) / (a * b)

Tactic:
mul_one,

Goal state after:
K : Type u_1
inst✝ : DivisionSemiring K
a b : K
hab : Commute a b
ha : a ≠ 0
hb : b ≠ 0
⊢ (b + a) / (a * b) = (a + b) / (a * b)
Module: Mathlib.Algebra.Group.Int.Units

Goal state before:
pp: u v : ℤ
h : u * v = 1
⊢ u = 1 ∧ v = 1 ∨ u = -1 ∧ v = -1

Tactic:
by
  have h' : v * u = 1 := mul_comm u v ▸ h
  obtain rfl | rfl := eq_one_or_neg_one_of_mul_eq_one h <;>
      obtain rfl | rfl := eq_one_or_neg_one_of_mul_eq_one h' <;> tauto

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

Goal state before:
pp: u v : ℤ
h : u * v = -1
⊢ u = 1 ∧ v = -1 ∨ u = -1 ∧ v = 1

Tactic:
by
  obtain rfl | rfl := isUnit_eq_one_or (IsUnit.mul_iff.mp (Int.isUnit_iff.mpr (Or.inr h))).1
  · exact Or.inl ⟨rfl, one_mul v ▸ h⟩
  · simpa [Int.neg_mul] using h

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

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : NeZero 2
a : K
⊢ a - a / 2 = a / 2

Tactic:
by rw [sub_eq_iff_eq_add, add_halves]

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 t' : Set β
a : α
ha : a ∈ s
b : β
hb : b ∈ t
h : ¬f a b ∈ image2 f s t'
⊢ f a b ∈ image2 f s (t \ t')

Tactic:
exact ⟨_, ha, _, ⟨hb, fun hb' ↦ h ⟨_, ha, _, hb', rfl⟩⟩, rfl⟩

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
a : α
s : Set α
hf : StrictAnti f
⊢ IsGreatest (f '' s) (f a) ↔ IsLeast s a

Tactic:
simp [IsLeast, IsGreatest, hf.injective.eq_iff, hf.mem_upperBounds_image]

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

Goal state before:
pp: α✝¹ : Sort u
β✝ : Sort v
γ : Sort w
α✝ : Type u_1
β : Type u_2
α : Type u
s t : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ t \ s ∪ s ∩ t = t

Tactic:
rw [union_comm, inter_comm, inter_union_sdiff]

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s s' : Set α
a b : α
h : (s ∩ s').Nonempty
ha : a ∈ lowerBounds s
hb : b ∈ upperBounds s'
x : α
hx : x ∈ s
hx' : x ∈ s'
⊢ a ≤ b

Tactic:
exact le_trans (ha hx) (hb hx')

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:
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:
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:
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:
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:
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:
simp [div_eq_mul_inv]

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

Goal state before:
pp: α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a : α
inst✝ : IsStrictOrderedRing α
⊢ a / 2 ≤ a ↔ 0 ≤ a

Tactic:
div_le_iff₀ (zero_lt_two' α),

Goal state after:
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a : α
inst✝ : IsStrictOrderedRing α
⊢ a ≤ a * 2 ↔ 0 ≤ a
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
f : α → α → α
a b : α
na nb nc : ℤ
da db dc k : ℕ
⊢ f = HAdd.hAdd →
    IsRat a na da →
      IsRat b nb db → (na.mul ↑db).add (nb.mul ↑da) = (↑k).mul nc → da.mul db = k.mul dc → IsRat (f a b) nc dc

Tactic:
rintro rfl ⟨_, rfl⟩ ⟨_, rfl⟩ (h₁ : na * db + nb * da = k * nc) (h₂ : da * db = k * dc)
  have : Invertible (↑(da * db) : α) := by simpa using invertibleMul (da:α) db
  have := invertibleOfMul' (α := α) h₂
  use this
  have H := (Nat.cast_commute (α := α) da db).invOf_left.invOf_right.right_comm
  have h₁ := congr_arg (↑· * (⅟↑da * ⅟↑db : α)) h₁
  simp only [Int.cast_add, Int.cast_mul, Int.cast_natCast, ← mul_assoc,
    add_mul, mul_invOf_cancel_right] at h₁
  have h₂ := congr_arg (↑nc * ↑· * (⅟↑da * ⅟↑db * ⅟↑dc : α)) h₂
  simp only [H, mul_invOf_cancel_right', Nat.cast_mul, ← mul_assoc] at h₁ h₂
  rw [h₁, h₂, Nat.cast_commute]
  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 c : α
hc : c < 0
⊢ a ≤ b / - -c ↔ b ≤ a * - -c

Tactic:
mul_neg,

Goal state after:
α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b c : α
hc : c < 0
⊢ a ≤ b / - -c ↔ b ≤ -(a * -c)
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b c : α
hc : c < 0
⊢ a < b / - -c ↔ b < a * - -c

Tactic:
mul_neg,

Goal state after:
α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b c : α
hc : c < 0
⊢ a < b / - -c ↔ b < -(a * -c)
Module: Mathlib.Data.List.TakeDrop

Goal state before:
pp: α : Type u
p : α → Bool
a : α
l l₂ : List α
⊢ loop p (a :: l) l₂ = (l₂.reverse ++ takeWhile p (a :: l), dropWhile p (a :: l))

Tactic:
cases hp : p a <;> simp [hp, span.loop, span.loop_eq_take_drop, takeWhile, dropWhile]

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

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

Tactic:
by
  rcases lt_trichotomy b 0 with (hb | rfl | hb)
  · simp [hb, hb.not_gt, hb.ne, div_le_one_of_neg]
  · simp [zero_le_one]
  · simp [hb, hb.not_gt, div_le_one, hb.ne.symm]

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

Goal state before:
pp: α : Type u
n : ℕ
x : α
l₁ l₂ : List α
⊢ (fun l ↦ l.insertIdx n x) l₁ = (fun l ↦ l.insertIdx n x) l₂ → l₁ = l₂

Tactic:
hl

Goal state after:
α : Type u
n : ℕ
x : α
l₁ l₂ : List α
hl : (fun l ↦ l.insertIdx n x) l₁ = (fun l ↦ l.insertIdx n x) l₂
⊢ l₁ = l₂
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: case mp.cons
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
a : α
b : β
l1 : List α
l2 : List β
rab : R a b
a✝ : SublistForall₂ R l1 l2
ih : ∃ l, Forall₂ R l1 l ∧ l <+ l2
⊢ ∃ l, Forall₂ R (a :: l1) l ∧ l <+ b :: l2

Tactic:
obtain ⟨l, hl1, hl2⟩ := ih
      exact ⟨b :: l, Forall₂.cons rab hl1, hl2.cons_cons b⟩

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

Goal state before:
pp: case inr
α : Type u_1
l₁ l₂ : List α
m n : ℕ
h : l₁[m]? = l₂[n]?
hm : m ≥ l₁.length
⊢ l₁.eraseIdx m ~ l₂.eraseIdx n ↔ l₁ ~ l₂

Tactic:
rw [getElem?_eq_none hm, eq_comm, getElem?_eq_none_iff] at h

Goal state after:
case inr
α : Type u_1
l₁ l₂ : List α
m n : ℕ
h : l₂.length ≤ n
hm : m ≥ l₁.length
⊢ l₁.eraseIdx m ~ l₂.eraseIdx n ↔ l₁ ~ l₂
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
m n : ℕ
h : l₁[m]? = l₂[n]?
x✝ : m < l₁.length ∨ m ≥ l₁.length
⊢ l₁.eraseIdx m ~ l₂.eraseIdx n ↔ l₁ ~ l₂

Tactic:
cases Nat.lt_or_ge m l₁.length with

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

Goal state before:
pp: case mpr
α : Type u
hα : Subsingleton α
l1 l2 : List α
⊢ l1.length = l2.length → l1 = l2

Tactic:
hl

Goal state after:
case mpr
α : Type u
hα : Subsingleton α
l1 l2 : List α
hl : l1.length = l2.length
⊢ l1 = l2
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
l : List α
p : α → Prop
⊢ (∀ (x : α), x ∈ l → p x) ↔ ∀ (i : ℕ) (x : i < l.length), p l[i]

Tactic:
simp [mem_iff_getElem, @forall_comm α]

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

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
l l' : List M
h : l.length = l'.length
⊢ (zipWith (fun x1 x2 ↦ x1 * x2) l l').prod * 1 * 1 = (zipWith (fun x1 x2 ↦ x1 * x2) l l').prod

Tactic:
mul_one,

Goal state after:
M : Type u_4
inst✝ : CommMonoid M
l l' : List M
h : l.length = l'.length
⊢ (zipWith (fun x1 x2 ↦ x1 * x2) l l').prod * 1 = (zipWith (fun x1 x2 ↦ x1 * x2) l l').prod
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

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

Tactic:
mul_one,

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

Goal state before:
pp: n₁ d₁ n₂ d₂ : ℤ
⊢ n₁ /. d₁ / (n₂ /. d₂) = n₁ * d₂ /. (d₁ * n₂)

Tactic:
div_def,

Goal state after:
n₁ d₁ n₂ d₂ : ℤ
⊢ n₁ /. d₁ * (n₂ /. d₂)⁻¹ = n₁ * d₂ /. (d₁ * n₂)
Module: Mathlib.Algebra.Ring.Rat

Goal state before:
pp: n : ℕ
⊢ ↑↑(n + 1) = ↑↑n + 1

Tactic:
simp only [intCast_eq_divInt, divInt_add_divInt _ _ Int.one_ne_zero Int.one_ne_zero,
      ← divInt_one_one, Int.natCast_add, Int.natCast_one, mul_one]

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

Goal state before:
pp: a b c d : ℤ
b0 : 0 < b
d0 : 0 < d
⊢ a /. b ≤ c /. d ↔ a * d ≤ c * b

Tactic:
by
  rw [Rat.le_iff_sub_nonneg, ← Int.sub_nonneg]
  simp [sub_eq_add_neg, ne_of_gt b0, ne_of_gt d0, Int.mul_pos d0 b0]

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

Goal state before:
pp: case inl
α : Type u_1
inst✝ : CommMonoid α
x : α
⊢ x ∣ x ^ 0 ↔ 0 ≠ 0 ∨ IsUnit x

Tactic:
simp [isUnit_iff_dvd_one]

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

Goal state before:
pp: α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑(q + r) = ↑q + ↑r

Tactic:
rw [add_def, cast_divNat_of_ne_zero, cast_def, cast_def, mul_comm _ q.den,
    (Nat.commute_cast _ _).div_add_div (Nat.commute_cast _ _) hq hr]
  · push_cast
    rfl
  · push_cast
    exact mul_ne_zero hq hr

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

Goal state before:
pp: α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑(q * r) = ↑q * ↑r

Tactic:
rw [mul_def, cast_divNat_of_ne_zero, cast_def, cast_def,
    (Nat.commute_cast _ _).div_mul_div_comm (Nat.commute_cast _ _)]
  · push_cast
    rfl
  · push_cast
    exact mul_ne_zero hq hr

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

Goal state before:
pp: α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.num ≠ 0
⊢ ↑(q / r) = ↑q / ↑r

Tactic:
div_def,

Goal state after:
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.num ≠ 0
⊢ ↑(divNat (q.num * r.den) (q.den * r.num)) = ↑q / ↑r
Module: Mathlib.Tactic.NormNum.Pow

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

Tactic:
Int.negOfNat_eq,

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

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

Tactic:
Int.negOfNat_eq,

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

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

Tactic:
Int.negOfNat_eq,

Goal state after:
a b c b' c' : ℕ
h1 : a.pow b' = c'
hb : 2 * b' + 1 = b
hc : c' * (c' * a) = c
⊢ (-Int.ofNat a).pow (2 * b' + 1) = -Int.ofNat c
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a₁ a₂ b₁ b₂ c₁ c₂ : R
x✝¹ : a₁ + b₁ = c₁
x✝ : a₂ + b₂ = c₂
⊢ a₁ + a₂ + (b₁ + b₂) = c₁ + c₂

Tactic:
by
  subst_vars; simp [add_assoc, add_left_comm]

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_2
inst✝ : Semifield R
a b : R
⊢ a / b = a * b⁻¹

Tactic:
simp [div_eq_mul_inv]

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

Goal state before:
pp: α : Type u_1
f : Bool → α
⊢ range f = {f false, f true}

Tactic:
by grind [cases Bool]

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

Goal state before:
pp: b : Bool
⊢ {b}ᶜ = {!b}

Tactic:
by grind [cases Bool]

Goal state after: