mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Ring.InjSurj

Goal state before:
pp: R : Type u_1
S✝ : Type u_2
f✝ : S✝ → R
hf✝ : Injective f✝
inst✝²⁰ : Add S✝
inst✝¹⁹ : Mul S✝
inst✝¹⁸ : Zero S✝
inst✝¹⁷ : One S✝
inst✝¹⁶ : Neg S✝
inst✝¹⁵ : Sub S✝
inst✝¹⁴ : SMul ℕ S✝
inst✝¹³ : SMul ℤ S✝
inst✝¹² : Pow S✝ ℕ
inst✝¹¹ : NatCast S✝
inst✝¹⁰ : IntCast S✝
S : Type ?u.36
inst✝⁹ : Zero S
inst✝⁸ : One S
inst✝⁷ : Add S
inst✝⁶ : SMul ℕ S
inst✝⁵ : Neg S
inst✝⁴ : Sub S
inst✝³ : SMul ℤ S
inst✝² : NatCast S
inst✝¹ : IntCast S
inst✝ : AddGroupWithOne R
f : S → R
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
neg : ∀ (x : S), f (-x) = -f x
sub : ∀ (x y : S), f (x - y) = f x - f y
nsmul : ∀ (n : ℕ) (x : S), f (n • x) = n • f x
zsmul : ∀ (n : ℤ) (x : S), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f ↑n = ↑n
intCast : ∀ (n : ℤ), f ↑n = ↑n
n : ℕ
⊢ f ↑(Int.negSucc n) = f (-↑(n + 1))

Tactic:
by rw [intCast, neg, natCast, Int.cast_negSucc]

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

Goal state before:
pp: α : Type u_2
inst✝ : Semiring α
a : α
n : ℕ
ha : Odd a
⊢ Odd (a ^ n)

Tactic:
by
  induction n with
  | zero => simp [pow_zero]
  | succ n hrec => rw [pow_succ]; exact hrec.mul ha

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

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

Tactic:
by
  rw [div_eq_mul_inv, div_eq_mul_inv, ← mul_le_mul_iff_left a⁻¹, inv_mul_cancel_left,
    inv_mul_cancel_left, inv_le_inv_iff]

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

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulRightMono α
a b : α
⊢ cmp (a / b) 1 = cmp a b

Tactic:
by rw [← cmp_mul_right' _ _ b, one_mul, div_mul_cancel]

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

Goal state before:
pp: α : Type u_1
s : Grind.CommRing α
n : ℕ
⊢ -(↑n + 1) = -↑(n + 1)

Tactic:
Grind.Semiring.natCast_succ

Goal state after:
α : Type u_1
s : Grind.CommRing α
n : ℕ
⊢ -(↑n + 1) = -(↑n + 1)
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝³ : MonoidWithZero M₀
inst✝² : Preorder M₀
a : M₀
inst✝¹ : ZeroLEOneClass M₀
inst✝ : PosMulMono M₀
ha : 1 < a
n : ℕ
x✝ : n + 1 ≠ 0
⊢ 1 < a * a ^ n

Tactic:
exact one_lt_mul_of_lt_of_le ha (one_le_pow₀ ha.le)

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

Goal state before:
pp: case inl
R : Type u
inst✝³ : Semiring R
inst✝² : LinearOrder R
a b : R
inst✝¹ : MulPosStrictMono R
inst✝ : PosMulStrictMono R
hab : 0 ≤ a * b
ab : 0 ≤ a → b < 0
nab : a ≤ 0 → 0 < b
ha : 0 < a
⊢ a * b < 0

pp: case inr.inl
R : Type u
inst✝³ : Semiring R
inst✝² : LinearOrder R
b : R
inst✝¹ : MulPosStrictMono R
inst✝ : PosMulStrictMono R
hab : 0 ≤ 0 * b
ab : 0 ≤ 0 → b < 0
nab : 0 ≤ 0 → 0 < b
⊢ 0 * b < 0

pp: case inr.inr
R : Type u
inst✝³ : Semiring R
inst✝² : LinearOrder R
a b : R
inst✝¹ : MulPosStrictMono R
inst✝ : PosMulStrictMono R
hab : 0 ≤ a * b
ab : 0 ≤ a → b < 0
nab : a ≤ 0 → 0 < b
ha : a < 0
⊢ a * b < 0

Tactic:
· exact mul_neg_of_pos_of_neg ha (ab ha.le)

Goal state after:
case inr.inl
R : Type u
inst✝³ : Semiring R
inst✝² : LinearOrder R
b : R
inst✝¹ : MulPosStrictMono R
inst✝ : PosMulStrictMono R
hab : 0 ≤ 0 * b
ab : 0 ≤ 0 → b < 0
nab : 0 ≤ 0 → 0 < b
⊢ 0 * b < 0

case inr.inr
R : Type u
inst✝³ : Semiring R
inst✝² : LinearOrder R
a b : R
inst✝¹ : MulPosStrictMono R
inst✝ : PosMulStrictMono R
hab : 0 ≤ a * b
ab : 0 ≤ a → b < 0
nab : a ≤ 0 → 0 < b
ha : a < 0
⊢ a * b < 0
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 g : r →r s
h : (fun o ↦ o.toFun) f = (fun o ↦ o.toFun) g
⊢ f = g

Tactic:
cases f
    cases g
    congr

Goal state after:
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:
by 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
inst✝ : MulLeftMono M
a b : M
hab : a ^ 2 ≤ b * a
n : ℕ
x✝ : n + 2 ≠ 0
⊢ b ^ n * a ^ 2 ≤ b ^ n * (b * a)

Tactic:
grw [hab]

Goal state after:
Module: Mathlib.Data.Nat.Cast.Order.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : AddMonoidWithOne α
inst✝² : PartialOrder α
inst✝¹ : AddLeftMono α
inst✝ : ZeroLEOneClass α
n : ℕ
⊢ ↑n ≤ ↑(n + 1)

Tactic:
rw [Nat.cast_succ]; exact le_add_of_nonneg_right zero_le_one

Goal state after:
Module: Mathlib.Data.Nat.Cast.Order.Basic

Goal state before:
pp: R : Type u_2
S : Type u_3
F : Type u_4
inst✝⁴ : NonAssocSemiring R
inst✝³ : NonAssocSemiring S
inst✝² : FunLike F R S
n : ℕ
inst✝¹ : NeZero ↑n
inst✝ : RingHomClass F R S
f : F
hf : Function.Injective ⇑f
h : ↑n = 0
⊢ f ↑n = f 0

Tactic:
by simpa only [map_natCast, map_zero f]

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

Goal state before:
pp: n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : (p + 1).pred * (q + 1).pred ≤ n
a_n b_n : ℤ
eq : ↑n = ↑(p + 1) * a_n + ↑(q + 1) * b_n
a : ℤ := a_n % ↑q.succ
b : ℤ := b_n + a_n / ↑q.succ * ↑p.succ
⊢ a_n * ↑p.succ + b_n * ↑q.succ = ↑n

Tactic:
eq,

Goal state after:
n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : (p + 1).pred * (q + 1).pred ≤ n
a_n b_n : ℤ
eq : ↑n = ↑(p + 1) * a_n + ↑(q + 1) * b_n
a : ℤ := a_n % ↑q.succ
b : ℤ := b_n + a_n / ↑q.succ * ↑p.succ
⊢ a_n * ↑p.succ + b_n * ↑q.succ = ↑(p + 1) * a_n + ↑(q + 1) * b_n
Module: Mathlib.Data.Int.GCD

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

Tactic:
simp only [hab, Int.ofNat_zero, Int.natCast_succ, zero_add] at this

Goal state after:
a b c : ℤ
habc : a ∣ b * c
hab : a.gcd c = 1
this : 1 = a * a.gcdA c + c * a.gcdB c
⊢ a ∣ b
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
⊢ 0 < a - b ↔ b < a ∨ b = ⊤

Tactic:
obtain rfl | hb := eq_or_ne b ⊤
  · simp
  · simp [← sub_self_eq_zero_of_ne_top hb, hb]

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

Goal state before:
pp: case coe.coe.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddLeftMono α
a✝² a✝¹ a✝ : α
⊢ a✝¹ ≤ a✝ → a✝² + a✝¹ ≤ a✝² + a✝

Tactic:
simpa using fun _ ↦ by gcongr

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

Goal state before:
pp: case coe.coe.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddRightMono α
a✝² a✝¹ a✝ : α
⊢ a✝¹ ≤ a✝ → a✝¹ + a✝² ≤ a✝ + a✝²

Tactic:
simpa using fun _ ↦ by gcongr

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✝ : AddRightReflectLE α
hz : z ≠ ⊤
⊢ x + z ≤ y + z → x ≤ y

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

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

Goal state before:
pp: case coe.coe
α : Type u
inst✝² : Add α
inst✝¹ : LT α
inst✝ : AddLeftStrictMono α
x a✝¹ a✝ : α
⊢ a✝¹ < a✝ → x + a✝¹ < x + a✝

Tactic:
simpa using fun _ ↦ by gcongr

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

Goal state before:
pp: case coe.coe
α : Type u
inst✝² : Add α
inst✝¹ : LT α
inst✝ : AddRightStrictMono α
z a✝¹ a✝ : α
⊢ a✝¹ < a✝ → a✝¹ + z < a✝ + z

Tactic:
simpa using fun _ ↦ by gcongr

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

Goal state before:
pp: α : Type u
inst✝² : Add α
x y z : WithTop α
inst✝¹ : LT α
inst✝ : AddRightStrictMono α
hz : z ≠ ⊤
⊢ x < y → x + z < y + z

Tactic:
by
  lift z to α using hz; cases x <;> cases y <;> simp [← coe_add]; simpa using fun _ ↦ by gcongr

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

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

Tactic:
· rw [max_eq_left h, tsub_add_cancel_of_le h]

Goal state after:
Module: Mathlib.Data.Nat.Cast.Order.Ring

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
m n : ℕ
⊢ -↑m = ↑n ↔ m = 0 ∧ n = 0

Tactic:
by
  simp [neg_eq_iff_add_eq_zero, ← cast_add]

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

Goal state before:
pp: case coe.coe.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithBot α
a b : α
inst✝¹ : LE α
inst✝ : AddLeftMono α
a✝² a✝¹ a✝ : α
⊢ a✝¹ ≤ a✝ → a✝² + a✝¹ ≤ a✝² + a✝

Tactic:
simpa using fun _ ↦ by gcongr

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

Goal state before:
pp: case coe.coe.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithBot α
a b : α
inst✝¹ : LE α
inst✝ : AddRightMono α
a✝² a✝¹ a✝ : α
⊢ a✝¹ ≤ a✝ → a✝¹ + a✝² ≤ a✝ + a✝²

Tactic:
simpa using fun _ ↦ by gcongr

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✝ : AddRightReflectLE α
hz : z ≠ ⊥
⊢ x + z ≤ y + z → x ≤ y

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

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

Goal state before:
pp: α : Type u
inst✝² : Add α
x y z : WithBot α
inst✝¹ : LT α
inst✝ : AddRightStrictMono α
hz : z ≠ ⊥
⊢ x < y → x + z < y + z

Tactic:
by
  lift z to α using hz; cases x <;> cases y <;> simp [← coe_add]; simpa using fun _ ↦ by gcongr

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
a : α
n : ℕ
⊢ (fun a ↦ ⌈a⌉.toNat) a ≤ n ↔ a ≤ ↑n

Tactic:
rw [Int.toNat_le, Int.ceil_le, Int.cast_natCast]

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 : R
n : ℕ
hn : n ≠ 0
⊢ ⌈a⌉₊ = n ↔ ¬⌈a⌉₊ ≤ n - 1 ∧ ⌈a⌉₊ ≤ n

Tactic:
not_le,

Goal state after:
R : Type u_1
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
a : R
n : ℕ
hn : n ≠ 0
⊢ ⌈a⌉₊ = n ↔ n - 1 < ⌈a⌉₊ ∧ ⌈a⌉₊ ≤ n
Module: Mathlib.Algebra.GroupWithZero.Units.Lemmas

Goal state before:
pp: case pos
G₀ : Type u_3
G₀' : Type u_5
F : Type u_6
inst✝³ : GroupWithZero G₀
inst✝² : GroupWithZero G₀'
inst✝¹ : FunLike F G₀ G₀'
inst✝ : MonoidWithZeroHomClass F G₀ G₀'
f : F
a : G₀
h : a = 0
⊢ f a⁻¹ = (f a)⁻¹

pp: case neg
G₀ : Type u_3
G₀' : Type u_5
F : Type u_6
inst✝³ : GroupWithZero G₀
inst✝² : GroupWithZero G₀'
inst✝¹ : FunLike F G₀ G₀'
inst✝ : MonoidWithZeroHomClass F G₀ G₀'
f : F
a : G₀
h : ¬a = 0
⊢ f a⁻¹ = (f a)⁻¹

Tactic:
· simp [h, map_zero f]

Goal state after:
case neg
G₀ : Type u_3
G₀' : Type u_5
F : Type u_6
inst✝³ : GroupWithZero G₀
inst✝² : GroupWithZero G₀'
inst✝¹ : FunLike F G₀ G₀'
inst✝ : MonoidWithZeroHomClass F G₀ G₀'
f : F
a : G₀
h : ¬a = 0
⊢ f a⁻¹ = (f a)⁻¹
Module: Mathlib.Algebra.Ring.Divisibility.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Semigroup α
inst✝² : Semigroup β
F : Type u_3
inst✝¹ : EquivLike F α β
inst✝ : MulEquivClass F α β
f : F
a c : α
⊢ f a ∣ f c ↔ a ∣ (↑f).symm (f c)

Tactic:
simp [map_dvd_iff]

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

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
a b c : K
⊢ a / c - b / c = (a - b) / c

Tactic:
rw [sub_eq_add_neg, ← neg_div, ← add_div, sub_eq_add_neg]

Goal state after:
Module: Mathlib.Order.WellFounded

Goal state before:
pp: α : Type u_1
r : α → α → Prop
wf : WellFounded r
inst✝ : Nonempty α
⊢ ¬Relator.RightTotal r

Tactic:
by
  intro h
  obtain ⟨a, -, ha⟩ := wf.has_min Set.univ Set.univ_nonempty
  obtain ⟨b, hba⟩ := h a
  specialize ha b (Set.mem_univ b)
  contradiction

Goal state after:
Module: Mathlib.Order.Hom.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : Preorder β
f g : α ≃o β
⊢ range ⇑f.toOrderEmbedding = range ⇑g.toOrderEmbedding

Tactic:
coe_toOrderEmbedding,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : Preorder β
f g : α ≃o β
⊢ range ⇑f = range ⇑g.toOrderEmbedding
Module: Mathlib.Order.Hom.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : Preorder β
f g : α ≃o β
⊢ range ⇑f = range ⇑g.toOrderEmbedding

Tactic:
coe_toOrderEmbedding,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : Preorder β
f g : α ≃o β
⊢ range ⇑f = range ⇑g
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Set α
a b : α
h : IsLUB s a
⊢ (∃ x, ∃ (_ : x ∈ s), ¬x ≤ b) ↔ ∃ c ∈ s, ¬c ≤ b

Tactic:
not_le,

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
s : Set α
a b : α
h : IsLUB s a
⊢ (∃ x, ∃ (_ : x ∈ s), b < x) ↔ ∃ c ∈ s, b < c
Module: Mathlib.Tactic.Positivity.Core

Goal state before:
pp: A : Type u_1
e : A
n d : ℕ
inst✝¹ : Semiring A
inst✝ : LinearOrder A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (n = 0) = true
⊢ 0 ≤ e

Tactic:
eq,

Goal state after:
A : Type u_1
e : A
n d : ℕ
inst✝¹ : Semiring A
inst✝ : LinearOrder A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (n = 0) = true
⊢ 0 ≤ ↑n * ⅟↑d
Module: Mathlib.Tactic.Positivity.Core

Goal state before:
pp: A : Type u_1
e : A
n : ℤ
d : ℕ
inst✝¹ : Ring A
inst✝ : LinearOrder A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (n = 0) = true
⊢ 0 ≤ e

Tactic:
eq,

Goal state after:
A : Type u_1
e : A
n : ℤ
d : ℕ
inst✝¹ : Ring A
inst✝ : LinearOrder A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (n = 0) = true
⊢ 0 ≤ ↑n * ⅟↑d
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: α : 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
⊢ IsNNRat (↑na * ⅟↑da + ↑nb * ⅟↑db) nc dc

Tactic:
have : Invertible (↑(da * db) : α) := by simpa using invertibleMul (da:α) db

Goal state after:
α : 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)
⊢ IsNNRat (↑na * ⅟↑da + ↑nb * ⅟↑db) nc dc
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 * ↑db + nb * ↑da = ↑k * nc
h₂ : da * db = k * dc
⊢ IsRat (↑na * ⅟↑da + ↑nb * ⅟↑db) nc dc

Tactic:
have : Invertible (↑(da * db) : α) := by simpa using invertibleMul (da:α) db

Goal state after:
α : 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)
⊢ IsRat (↑na * ⅟↑da + ↑nb * ⅟↑db) nc dc
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
na nb nc da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁ : na * nb = k * nc
h₂ : da * db = k * dc
⊢ IsNNRat (↑na * ⅟↑da * (↑nb * ⅟↑db)) nc dc

Tactic:
have : Invertible (↑(da * db) : α) := by simpa using invertibleMul (da:α) db

Goal state after:
α : Type u_1
inst✝ : Semiring α
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)
⊢ IsNNRat (↑na * ⅟↑da * (↑nb * ⅟↑db)) nc dc
Module: Mathlib.Data.List.Defs

Goal state before:
pp: α : Type u_1
t : α
ts is : List α
⊢ Prod.Lex (fun a₁ a₂ ↦ a₁ < a₂) (fun a₁ a₂ ↦ a₁ < a₂) (ts.length + (t :: is).length, ts.length)
    ((t :: ts).length + is.length, (t :: ts).length)

pp: α : Type u_1
t : α
ts is : List α
⊢ Prod.Lex (fun a₁ a₂ ↦ a₁ < a₂) (fun a₁ a₂ ↦ a₁ < a₂) (is.length + [].length, is.length)
    ((t :: ts).length + is.length, (t :: ts).length)

Tactic:
decreasing_by all_goals (simp_wf; grind)

Goal state after:
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
⊢ IsRat (↑na * ⅟↑da * (↑nb * ⅟↑db)) nc dc

Tactic:
have : Invertible (↑(da * db) : α) := by simpa using invertibleMul (da:α) db

Goal state after:
α : 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)
⊢ IsRat (↑na * ⅟↑da * (↑nb * ⅟↑db)) nc dc
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 / c < b / c ↔ b < a

Tactic:
by
  rw [div_lt_iff_of_neg hc, div_mul_cancel₀ _ hc.ne]

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 : ∀ (x : M), x ∈ z :: l → Commute y x
⊢ Commute y (z :: l).prod

Tactic:
rw [List.forall_mem_cons] at h

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.Tactic.FieldSimp.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
n : ℤ
⊢ zpow' 1 n = 1

Tactic:
by
  simp [zpow']

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

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
a : α
⊢ zpow' a 1 = a

Tactic:
by
  simp [zpow']

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

Goal state before:
pp: M : Type u_1
inst✝ : Semiring M
x₁ x₂ X₁ X₂ Y y a : M
h₁ : x₁ = a * X₁
h₂ : x₂ = a * X₂
H_atom : X₁ + X₂ = Y
hy : a * Y = y
⊢ x₁ + x₂ = y

Tactic:
subst h₁ h₂ H_atom hy
  simp [mul_add]

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

Goal state before:
pp: M : Type u_1
inst✝¹ : MonoidWithZero M
inst✝ : IsLeftCancelMulZero M
f₁ f₂ L : M
HL : L ≠ 0
⊢ (L * f₁ = L * f₂) = (f₁ = f₂)

Tactic:
rw [mul_right_inj' HL]

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
h : Injective f
x : α
xs : List α
y : α
ys : List α
hxy : f x = f y
hxys : map f xs = map f ys
⊢ y :: xs = y :: ys

Tactic:
h.list_map hxys

Goal state after:
α : Type u
β : Type v
f : α → β
h : Injective f
x : α
xs : List α
y : α
ys : List α
hxy : f x = f y
hxys : map f xs = map f ys
⊢ y :: ys = y :: ys
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: 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₁
⊢ { num := n₁, den := d₁, den_nz := hd₁, reduced := hnd₁ } * { num := n₂, den := d₂, den_nz := hd₂, reduced := hnd₂ } =
    { num := n₁ * n₂, den := d₁ * d₂, den_nz := ⋯, reduced := ⋯ }

Tactic:
by
  rw [mul_def]; simp [mk_eq_normalize]

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
x y : α
H : IsRelPrime x y
hy : IsPrimal y
w : α
H2 : y ∣ x * w
⊢ x * y ∣ x * w

Tactic:
exact mul_dvd_mul_left x (H.symm.dvd_of_dvd_mul_left_of_isPrimal H2 hy)

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

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
h : a ^ n ∣ a ^ m
⊢ n ≤ m

Tactic:
rw [← not_lt]

Goal state after:
case mp
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
h : a ^ n ∣ a ^ m
⊢ ¬m < n
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q₁ q₂ : ℚ
⊢ q₁.den.gcd q₂.den ∣ (q₁.num * ↑q₂.den + q₂.num * ↑q₁.den).natAbs ∧
    q₁.den.gcd q₂.den ∣ q₁.den.gcd q₂.den * q₁.den.lcm q₂.den

Tactic:
refine ⟨?_, dvd_mul_right _ _⟩

Goal state after:
q₁ q₂ : ℚ
⊢ q₁.den.gcd q₂.den ∣ (q₁.num * ↑q₂.den + q₂.num * ↑q₁.den).natAbs
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q r : ℚ
s : ℚ := q.num * r.num /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * r.num = c * (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den
a✝ : ¬c = 0
⊢ ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den * (q * r).num =
    (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num * ↑(q * r).den

Tactic:
have h : _ = s := divInt_mul_divInt q.num r.num

Goal state after:
q r : ℚ
s : ℚ := q.num * r.num /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * r.num = c * (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den
a✝ : ¬c = 0
h : q.num /. ↑q.den * (r.num /. ↑r.den) = s
⊢ ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den * (q * r).num =
    (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num * ↑(q * r).den
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
p q : ℚ
hp : ↑p.den ≠ 0
hq : ↑q.den ≠ 0
⊢ ↑(p * q) = ↑p * ↑q

Tactic:
rw [mul_eq_mkRat, cast_mkRat_of_ne_zero, cast_def, cast_def,
    (Nat.commute_cast _ _).div_mul_div_comm (Int.commute_cast _ _)]
  · push_cast
    rfl
  · push_cast
    exact mul_ne_zero hp hq

Goal state after:
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 ^ b' * Int.ofNat a ^ b' * -Int.ofNat a = -Int.ofNat (a.pow b' * (a.pow b' * a))

Tactic:
simp [mul_comm, mul_left_comm]

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

Goal state before:
pp: R : Type u
inst✝³ : CommSemiring R
inst✝² : PartialOrder R
inst✝¹ : CanonicallyOrderedAdd R
inst✝ : PosMulStrictMono R
a b c d : R
hab : a < b
hcd : c < d
⊢ a * c < b * d

Tactic:
have := posMulStrictMono_iff_mulPosStrictMono.1 ‹_›
  obtain rfl | hc := eq_zero_or_pos c
  · rw [mul_zero]
    exact mul_pos hab.pos hcd
  · exact mul_lt_mul_of_pos' hab hcd hc hab.pos

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

Goal state before:
pp: ⊢ range succ = {i | 0 < i}

Tactic:
ext (_ | i)

Goal state after:
case zero
⊢ 0 ∈ range succ ↔ 0 ∈ {i | 0 < i}

case succ
i : ℕ
⊢ i + 1 ∈ range succ ↔ i + 1 ∈ {i | 0 < i}
Module: Mathlib.Order.CompleteLattice.Defs

Goal state before:
pp: α : Type u_1
inst✝ : CompleteSemilatticeSup α
s : Set α
a : α
⊢ sSup s = a → IsLUB s a

Tactic:
by rintro rfl; exact isLUB_sSup _

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

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ ⨆ i, ⨆ (_ : i ≥ n), u i = ⨆ i, u (i + n)

Tactic:
apply le_antisymm <;> simp only [iSup_le_iff]
  · refine fun i hi => le_sSup ⟨i - n, ?_⟩
    dsimp only
    rw [Nat.sub_add_cancel hi]
  · exact fun i => le_sSup ⟨i + n, iSup_pos (Nat.le_add_left _ _)⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
s : Set α
h_sup : sSup s = ⊥
hne : s.Nonempty
⊢ s = {⊥}

Tactic:
rw [Set.eq_singleton_iff_nonempty_unique_mem]

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
s : Set α
h_sup : sSup s = ⊥
hne : s.Nonempty
⊢ s.Nonempty ∧ ∀ x ∈ s, x = ⊥
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
ι : Sort u_5
C : ι → Set α
f : (x : ι) → β → ↑(C x)
hf : ∀ (x : ι), Surjective (f x)
x : α
⊢ (∃ i, x ∈ C i) → ∃ i, x ∈ range fun x ↦ ↑(f x i)

Tactic:
· rintro ⟨i, hx⟩
    obtain ⟨y, hy⟩ := hf i ⟨x, hx⟩
    exact ⟨y, i, congr_arg Subtype.val hy⟩

Goal state after: