mathlib-initiative/mathlib-tactics huggingface dataset:
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 : G
hab : a ≤ b
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1

Tactic:
obtain ha | ha := le_or_gt 1 a <;> obtain hb | hb := le_or_gt 1 b
  · simp [ha, hb, mabs_of_one_le, one_le_mul ha hb]
  · exact (lt_irrefl (1 : G) <| ha.trans_lt <| hab.trans_lt hb).elim
  swap
  · simp [ha.le, hb.le, mabs_of_le_one, mul_le_one', mul_comm]
  have : (|a * b|ₘ = a⁻¹ * b ↔ b ≤ 1) ↔
    (|a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1) := by
    simp [ha.le, ha.not_ge, hb, mabs_of_le_one, mabs_of_one_le]
  refine this.mp ⟨fun h ↦ ?_, fun h ↦ by simp only [h.antisymm hb, mabs_of_lt_one ha, mul_one]⟩
  obtain ab | ab := le_or_gt (a * b) 1
  · refine (eq_one_of_inv_eq' ?_).le
    rwa [mabs_of_le_one ab, mul_inv_rev, mul_comm, mul_right_inj] at h
  · rw [mabs_of_one_lt ab, mul_left_inj] at h
    rw [eq_one_of_inv_eq' h.symm] at ha
    cases ha.false

Goal state after:
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 : G
⊢ a ≤ |b|ₘ ↔ b ≤ a⁻¹ ∨ a ≤ b

Tactic:
le_mabs,

Goal state after:
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
⊢ a ≤ b ∨ a ≤ b⁻¹ ↔ b ≤ a⁻¹ ∨ a ≤ b
Module: Mathlib.Algebra.Order.Ring.Int

Goal state before:
pp: p q n : ℕ
dvd : p.gcd q ∣ n
le : p.pred * q.pred ≤ n
⊢ ∃ a b, a * p + b * q = n

Tactic:
obtain _ | p := p

Goal state after:
case zero
q n : ℕ
dvd : gcd 0 q ∣ n
le : pred 0 * q.pred ≤ n
⊢ ∃ a b, a * 0 + b * q = n

case succ
q n p : ℕ
dvd : (p + 1).gcd q ∣ n
le : (p + 1).pred * q.pred ≤ n
⊢ ∃ a b, a * (p + 1) + b * q = n
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: a b c : ℤ
habc : a ∣ b * c
hab : a.gcd b = 1
⊢ a ∣ c

Tactic:
rw [mul_comm] at habc
  exact dvd_of_dvd_mul_left_of_gcd_one habc hab

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

Goal state before:
pp: α β γ : Type u
f : α → β → γ
a : Option α
b : Option β
⊢ map₂ f a b = f <$> a <*> b

Tactic:
cases a <;> rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : Option α
⊢ map₂ f a none = none

Tactic:
cases a <;> rfl

Goal state after:
Module: Mathlib.Algebra.Group.WithOne.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : WithOne α
⊢ map₂ f a 1 = 1

Tactic:
cases a <;> rfl

Goal state after:
Module: Mathlib.Algebra.Group.WithOne.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : WithOne α
b : β
⊢ map₂ f a ↑b = map (fun x ↦ f x b) a

Tactic:
cases a <;> rfl

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

Goal state before:
pp: R : Type u_1
inst✝¹ : MulZeroClass R
inst✝ : Nontrivial R
ra : IsRightRegular 0
x y : R
xy : x ≠ y
⊢ False

Tactic:
refine xy (ra ?_)

Goal state after:
R : Type u_1
inst✝¹ : MulZeroClass R
inst✝ : Nontrivial R
ra : IsRightRegular 0
x y : R
xy : x ≠ y
⊢ (fun x ↦ x * 0) x = (fun x ↦ x * 0) y
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a✝ b c a : α
⊢ - -a = a

Tactic:
by
    obtain rfl | ha := eq_or_ne a ⊤
    · simp
    · apply left_neg_eq_right_neg (a := -a) <;> simp [add_comm, add_neg_cancel_of_ne_top, ha]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Group α
inst✝ : Group β
e : WithZero α ≃* WithZero β
x✝ : α
⊢ ∀ (y : α),
    { toFun := fun x ↦ unzero ⋯, invFun := fun x ↦ unzero ⋯, left_inv := ⋯, right_inv := ⋯ }.toFun (x✝ * y) =
      { toFun := fun x ↦ unzero ⋯, invFun := fun x ↦ unzero ⋯, left_inv := ⋯, right_inv := ⋯ }.toFun x✝ *
        { toFun := fun x ↦ unzero ⋯, invFun := fun x ↦ unzero ⋯, left_inv := ⋯, right_inv := ⋯ }.toFun y

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: α : Type u
inst✝¹ : Add α
a : α
inst✝ : LE α
ha : AddLECancellable a
⊢ AddLECancellable ↑a

Tactic:
rintro (_ | b) (_ | c)
  · simp [none_eq_top]
  · simp [none_eq_top]
  · simp [some_eq_coe, ← coe_add, none_eq_top]
  · simpa [none_eq_top, some_eq_coe, ← coe_add] using fun a ↦ ha a

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hbc : AddLECancellable (b - c)
h₁ : b ≤ a
h₂ : c ≤ b
⊢ a = a - b + c + (b - c)

Tactic:
add_assoc,

Goal state after:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hbc : AddLECancellable (b - c)
h₁ : b ≤ a
h₂ : c ≤ b
⊢ a = a - b + (c + (b - c))
Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hb : AddLECancellable b
hd : AddLECancellable d
hba : b ≤ a
hdc : d ≤ c
⊢ a - b + (c - d) = a + c - (b + d)

Tactic:
rw [hb.tsub_add_eq_add_tsub hba, ← hd.add_tsub_assoc_of_le hdc, tsub_tsub, add_comm d]

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hac : AddLECancellable (a - c)
h : c ≤ a
⊢ a + b = b + c + (a - c)

Tactic:
add_assoc,

Goal state after:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hac : AddLECancellable (a - c)
h : c ≤ a
⊢ a + b = b + (c + (a - c))
Module: Mathlib.Algebra.Order.Sub.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
ha : AddLECancellable a
⊢ a - b < a ↔ 0 < a ∧ 0 < b

Tactic:
refine ⟨fun h => ⟨h.pos, pos_of_ne_zero ?_⟩, fun h => ha.tsub_lt_self h.1 h.2⟩

Goal state after:
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
ha : AddLECancellable a
h : a - b < a
⊢ b ≠ 0
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
y : β
v : WithBot α
⊢ ↑y = map f v ↔ ∃ x, v = ↑x ∧ f x = y

Tactic:
cases v <;> simp [eq_comm]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : WithBot α
⊢ map₂ f a ⊥ = ⊥

Tactic:
cases a <;> rfl

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : WithBot α
b : β
⊢ map₂ f a ↑b = map (fun x ↦ f x b) a

Tactic:
cases a <;> rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrderedCommGroupWithZero α
a b c d : α
m n : ℕ
⊢ ∀ ⦃x : (Additive α)ᵒᵈ⦄, x ≠ ⊤ → x + -x = 0

Tactic:
by
    simp
    simp +contextual [bot_eq_zero, Additive.ext_iff, OrderDual.ext_iff, -Additive.toMul_eq_top,
      -ofDual_eq_zero]

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
x✝ : ℕ
⊢ x✝ ∈ Nat.cast ⁻¹' Ici a ↔ x✝ ∈ Ici ⌈a⌉₊

Tactic:
simp [ceil_le]

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
a : R
ha : 0 ≤ a
⊢ -1 ≤ a - ↑⌈a⌉₊

Tactic:
simpa using (ceil_lt_add_one ha).le

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

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

Tactic:
simp [← mul_assoc]

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

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

Tactic:
simp [← mul_assoc]

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

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

Tactic:
simp [← mul_assoc]

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

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

Tactic:
← neg_eq_val_neg,

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
x y : AddUnits R
⊢ x.neg * ↑y = ↑x * ↑(-y)
Module: Mathlib.Algebra.Ring.Invertible

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
a b : R
inst✝² : Invertible a
inst✝¹ : Invertible b
inst✝ : Invertible (a + b)
⊢ -1 + -1 + 1 = ⅟b * a + ⅟a * b ↔ -1 + 0 = ⅟b * a + ⅟a * b

Tactic:
add_assoc,

Goal state after:
R : Type u_1
inst✝³ : Ring R
a b : R
inst✝² : Invertible a
inst✝¹ : Invertible b
inst✝ : Invertible (a + b)
⊢ -1 + (-1 + 1) = ⅟b * a + ⅟a * b ↔ -1 + 0 = ⅟b * a + ⅟a * b
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n : ℕ
a : α
h : n ≠ 0
⊢ |a ^ n| = 1 ↔ |a| = 1

Tactic:
by
  convert! pow_left_inj₀ (abs_nonneg a) zero_le_one h
  exacts [(pow_abs _ _).symm, (one_pow _).symm]

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

Goal state before:
pp: α : Type u
f : α → α
hf : Involutive f
a : α
l : List α
⊢ a ∈ map f l ↔ f a ∈ l

Tactic:
by rw [mem_map, hf.exists_mem_and_apply_eq_iff]

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

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
a : α
n : ℕ
hn : n ≠ 0
⊢ zpow' a ↑n = a ^ n

Tactic:
zpow'_of_ne_zero_right

Goal state after:
α : Type u_1
inst✝ : GroupWithZero α
a : α
n : ℕ
hn : n ≠ 0
⊢ a ^ ↑n = a ^ n

case hn
α : Type u_1
inst✝ : GroupWithZero α
a : α
n : ℕ
hn : n ≠ 0
⊢ ↑n ≠ 0
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:
by
  simp [mem_iff_getElem, @forall_comm α]

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

Goal state before:
pp: α : Type u
l₁ l₂ : List α
⊢ l₁ = l₂ → ∀ (n : ℕ), n < max l₁.length l₂.length → l₁[n]? = l₂[n]?

Tactic:
rintro rfl _ _

Goal state after:
α : Type u
l₁ : List α
n✝ : ℕ
a✝ : n✝ < max l₁.length l₁.length
⊢ l₁[n✝]? = l₁[n✝]?
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: f : ℚ → ℚ → ℚ
f₁ f₂ : ℤ → ℤ → ℤ → ℤ → ℤ
fv :
  ∀ {n₁ : ℤ} {d₁ : ℕ} {h₁ : d₁ ≠ 0} {c₁ : n₁.natAbs.Coprime d₁} {n₂ : ℤ} {d₂ : ℕ} {h₂ : d₂ ≠ 0}
    {c₂ : n₂.natAbs.Coprime d₂},
    f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ } { num := n₂, den := d₂, den_nz := h₂, reduced := c₂ } =
      f₁ n₁ (↑d₁) n₂ ↑d₂ /. f₂ n₁ (↑d₁) n₂ ↑d₂
f0 : ∀ {n₁ d₁ n₂ d₂ : ℤ}, d₁ ≠ 0 → d₂ ≠ 0 → f₂ n₁ d₁ n₂ d₂ ≠ 0
a b c d : ℤ
b0 : b ≠ 0
d0 : d ≠ 0
H : ∀ {n₁ d₁ n₂ d₂ : ℤ}, a * d₁ = n₁ * b → c * d₂ = n₂ * d → f₁ n₁ d₁ n₂ d₂ * f₂ a b c d = f₁ a b c d * f₂ n₁ d₁ n₂ d₂
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
ha : a /. b = n₁ /. ↑d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
hc : c /. d = n₂ /. ↑d₂
d₁0 : ↑d₁ ≠ 0
d₂0 : ↑d₂ ≠ 0
⊢ f₁ n₁ (↑d₁) n₂ ↑d₂ /. f₂ n₁ (↑d₁) n₂ ↑d₂ = f₁ a b c d /. f₂ a b c d

Tactic:
exact (divInt_eq_divInt_iff (f0 d₁0 d₂0) (f0 b0 d0)).2
    (H ((divInt_eq_divInt_iff b0 d₁0).1 ha) ((divInt_eq_divInt_iff d0 d₂0).1 hc))

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

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

Tactic:
by
  rw [← divInt_div_divInt, num_divInt_den, num_divInt_den]

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

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
h : a ∈ l
⊢ (eraseP (fun x ↦ a == x) l).length + 1 = l.length

Tactic:
length_eraseP_add_one h BEq.rfl

Goal state after:
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
h : a ∈ l
⊢ l.length = l.length
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: case pos
x : ℤ
hx : x ≠ 0
n d : ℤ
hd : d = 0
⊢ n /. x * (x /. d) = n /. d

pp: case neg
x : ℤ
hx : x ≠ 0
n d : ℤ
hd : ¬d = 0
⊢ n /. x * (x /. d) = n /. d

Tactic:
· rw [hd]
    simp

Goal state after:
case neg
x : ℤ
hx : x ≠ 0
n d : ℤ
hd : ¬d = 0
⊢ n /. x * (x /. d) = n /. d
Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat

Goal state before:
pp: m : ℕ
s : Bool
e : ℕ
⊢ 0 ≤ Rat.ofScientific m s e

Tactic:
rw [Rat.ofScientific]
  cases s
  · rw [if_neg (by decide)]
    exact num_nonneg.mp <| Int.natCast_nonneg _
  · grind [normalize_eq_mkRat, Rat.mkRat_nonneg]

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

Goal state before:
pp: p q : ℚ≥0
⊢ p ≤ q ↔ p.num * q.den ≤ q.num * p.den

Tactic:
rw [← NNRat.coe_le_coe, Rat.le_iff]

Goal state after:
p q : ℚ≥0
⊢ (↑p).num * ↑(↑q).den ≤ (↑q).num * ↑(↑p).den ↔ p.num * q.den ≤ q.num * p.den
Module: Mathlib.Algebra.Divisibility.Units

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
x : α
x✝ : x ∣ 1
y : α
h : 1 = x * y
⊢ y * x = 1

Tactic:
by rw [h, mul_comm]

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

Goal state before:
pp: case neg
a b : ℤ
b0 : ¬b = 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a * ↑d = n * b
⊢ ↑d ∣ ↑(n * b).natAbs

Tactic:
Int.dvd_natAbs,

Goal state after:
case neg
a b : ℤ
b0 : ¬b = 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a * ↑d = n * b
⊢ ↑d ∣ n * b
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
⊢ q.num * d = n * ↑q.den

Tactic:
refine (divInt_eq_divInt_iff ?_ hd).mp ?_

Goal state after:
case refine_1
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
⊢ ↑q.den ≠ 0

case refine_2
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
⊢ q.num /. ↑q.den = n /. d
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
this : q.num * d = n * ↑q.den
⊢ (n /. d).num ∣ n

Tactic:
exact Rat.num_dvd _ hd

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
a : α
n d : ℕ
⊢ IsNNRat a n.succ d → IsNNRat a⁻¹ d n.succ

Tactic:
rintro ⟨_, rfl⟩

Goal state after:
α : Type u_1
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
n d : ℕ
inv✝ : Invertible ↑d
⊢ IsNNRat (↑n.succ * ⅟↑d)⁻¹ d n.succ
Module: Mathlib.Tactic.NormNum.Inv

Goal state before:
pp: α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
a : α
n d : ℕ
⊢ IsRat a (Int.ofNat n.succ) d → IsRat a⁻¹ (Int.ofNat d) n.succ

Tactic:
rintro ⟨_, rfl⟩

Goal state after:
α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n d : ℕ
inv✝ : Invertible ↑d
⊢ IsRat (↑(Int.ofNat n.succ) * ⅟↑d)⁻¹ (Int.ofNat d) n.succ
Module: Mathlib.Tactic.NormNum.Inv

Goal state before:
pp: α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
a : α
n d : ℕ
⊢ IsRat a (Int.negOfNat n.succ) d → IsRat a⁻¹ (Int.negOfNat d) n.succ

Tactic:
rintro ⟨_, rfl⟩

Goal state after:
α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n d : ℕ
inv✝ : Invertible ↑d
⊢ IsRat (↑(Int.negOfNat n.succ) * ⅟↑d)⁻¹ (Int.negOfNat d) n.succ
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLattice α
minAx : MinimalAxioms α
f : (i : ι) → κ i → α
g : ((i : ι) → κ i) → ι
⊢ ∃ a, ∀ (b : κ a), ∃ f, ∃ (h : a = g f), h ▸ b = f (g f)

Tactic:
by_contra! h
    choose h hh using h
    have := hh _ h rfl
    contradiction

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

Goal state before:
pp: α : Type u_1
ι : Sort u_5
inst✝ : Preorder α
f : ι → α
⊢ (⋂ i, Iic (f i)).Nonempty ↔ BddBelow (range f)

Tactic:
have : (⋂ (i : ι), Iic (f i)) = lowerBounds (range f) := by
    ext c; simp [lowerBounds]
  simp [this, BddBelow]

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
h₁ : a₁ < b₁
⊢ Ioc a₁ b₁ ⊆ Ioc a₂ b₂ ↔ b₁ ≤ b₂ ∧ a₂ ≤ a₁

Tactic:
convert! @Ico_subset_Ico_iff αᵒᵈ _ b₁ b₂ a₁ a₂ h₁ using 2 <;> exact (@Ico_toDual α _ _ _).symm

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

Goal state before:
pp: case neg
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
inst✝ : ConditionallyCompleteLattice α
S : Set (WithTop (WithBot α))
a : WithTop (WithBot α)
haS : a ∈ S
h₁ : ¬S ⊆ {⊤}
⊢ ↑(sInf ((fun a ↦ ↑a) ⁻¹' S)) ≤ a

Tactic:
cases a
        · exact le_top
        · apply WithTop.coe_le_coe.2
          refine csInf_le ?_ haS
          use ⊥
          intro b _
          exact bot_le

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Semiring α
inst✝ : CharZero α
num✝¹ num✝ denom✝¹ denom✝ : ℕ
inv✝¹ : Invertible ↑denom✝¹
inv✝ : Invertible ↑denom✝
h : decide (num✝¹.mul denom✝ = num✝.mul denom✝¹) = false
⊢ ¬↑num✝¹ * ↑denom✝ = ↑num✝ * ↑denom✝¹

Tactic:
exact mod_cast of_decide_eq_false h

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Ring α
inst✝ : CharZero α
num✝¹ num✝ : ℤ
denom✝¹ denom✝ : ℕ
inv✝¹ : Invertible ↑denom✝¹
inv✝ : Invertible ↑denom✝
h : decide (num✝¹.mul (Int.ofNat denom✝) = num✝.mul (Int.ofNat denom✝¹)) = false
⊢ ¬↑num✝¹ * ↑denom✝ = ↑num✝ * ↑denom✝¹

Tactic:
exact mod_cast of_decide_eq_false h

Goal state after:
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : One M
f : ι → M
k : Set ι
h : mulSupport f ⊆ k
⊢ range f = f '' k ∨ range f = insert 1 (f '' k)

Tactic:
have : range f ⊆ insert 1 (f '' k) :=
    (range_subset_insert_image_mulSupport f).trans (insert_subset_insert (image_mono h))

Goal state after:
ι : Type u_1
M : Type u_3
inst✝ : One M
f : ι → M
k : Set ι
h : mulSupport f ⊆ k
this : range f ⊆ insert 1 (f '' k)
⊢ range f = f '' k ∨ range f = insert 1 (f '' k)
Module: Mathlib.Tactic.NormNum.Ineq

Goal state before:
pp: α : Type u_1
inst✝² : Semiring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
num✝¹ num✝ da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h✝¹ : decide (num✝¹ * db < num✝ * da) = true
h✝ : ↑(num✝¹ * db) < ↑(num✝ * da)
ha : 0 < ⅟↑da
hb : 0 < ⅟↑db
h : ↑(num✝¹ * db) * ⅟↑db * ⅟↑da < ⅟↑db * (↑(num✝ * da) * ⅟↑da)
⊢ ↑num✝¹ * ⅟↑da < ↑num✝ * ⅟↑db

Tactic:
simp? at h says simp only [Nat.cast_mul, mul_invOf_cancel_right'] at h

Goal state after:
α : Type u_1
inst✝² : Semiring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
num✝¹ num✝ da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h✝¹ : decide (num✝¹ * db < num✝ * da) = true
h✝ : ↑(num✝¹ * db) < ↑(num✝ * da)
ha : 0 < ⅟↑da
hb : 0 < ⅟↑db
h : ↑num✝¹ * ⅟↑da < ⅟↑db * ↑num✝
⊢ ↑num✝¹ * ⅟↑da < ↑num✝ * ⅟↑db
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
N : Type u_4
inst✝¹ : One M
inst✝ : One N
f : ι → M
g : ι → N
x : ι
⊢ (x ∈ mulSupport fun x ↦ (f x, g x)) ↔ x ∈ mulSupport f ∪ mulSupport g

Tactic:
simp only [mulSupport, not_and_or, mem_union, mem_ofPred_eq, Prod.mk_eq_one, Ne]

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

Goal state before:
pp: case succ
l k n' : ℕ
⊢ (n' + 1).ascFactorial l * (n' + 1 + l).ascFactorial k = (n' + 1).ascFactorial (l + k)

Tactic:
| succ n' =>

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

Goal state before:
pp: case succ
n : ℕ
⊢ 2 ^ (n + 1) * (n + 1)! ≤ (2 * (n + 1))!

Tactic:
rw [Nat.mul_comm, Nat.two_mul]

Goal state after:
case succ
n : ℕ
⊢ (n + 1)! * 2 ^ (n + 1) ≤ (n + 1 + (n + 1))!
Module: Mathlib.Algebra.Order.Round

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

Tactic:
add_assoc,

Goal state after:
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
⊢ (if ↑2 * fract x < 1 then ⌊x⌋ + ⌊fract x⌋ else ⌊x⌋ + ⌈fract x⌉) = (2 * ⌊x⌋ + (⌊↑2 * fract x⌋ + 1)) / 2
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 : R
n : ℕ
⊢ ⌊a - ↑↑n⌋ = ⌊a⌋ - ↑n

Tactic:
floor_sub_intCast

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
n : ℕ
⊢ ⌊a⌋ - ↑n = ⌊a⌋ - ↑n
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
s : Set R
x : R
⊢ fract x ∈ s ↔ ∃ i, x - ↑i ∈ s ∧ x - ↑i ∈ Ico 0 1

Tactic:
refine ⟨fun h => ⟨⌊x⌋, h, fract_nonneg x, fract_lt_one x⟩, ?_⟩

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
s : Set R
x : R
⊢ (∃ i, x - ↑i ∈ s ∧ x - ↑i ∈ Ico 0 1) → fract x ∈ s
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
n d : ℕ
inv : Invertible ↑d
⊢ ⌊↑n / ↑d⌋ = ⌊↑n / ↑d⌋

Tactic:
← floor_cast (α := α),

Goal state after:
α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
n d : ℕ
inv : Invertible ↑d
⊢ ⌊↑n / ↑d⌋ = ⌊↑(↑n / ↑d)⌋
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 : R
z : ℤ
⊢ ⌊-a - ↑z⌋ = ⌊-a⌋ - z

Tactic:
floor_sub_intCast

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
z : ℤ
⊢ ⌊-a⌋ - z = ⌊-a⌋ - z
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
n d : ℕ
inv : Invertible ↑d
⊢ ⌊↑(negOfNat n) / ↑d⌋ = ⌊↑(negOfNat n) / ↑d⌋

Tactic:
← floor_cast (α := α),

Goal state after:
α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
n d : ℕ
inv : Invertible ↑d
⊢ ⌊↑(negOfNat n) / ↑d⌋ = ⌊↑(↑(negOfNat n) / ↑d)⌋
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: n : ℤ
d : ℕ
⊢ n % ↑d = n - ↑d * ⌊↑n / ↑d⌋

Tactic:
rw [Int.emod_def, Rat.floor_intCast_div_natCast]

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

Goal state before:
pp: q : ℚ
this : ↑q.num < ↑q.num + (1 - fract q) * ↑q.den
⊢ (q - fract q + 1) * ↑q.den = ↑q.num + (1 - fract q) * ↑q.den

Tactic:
calc
        (q - fract q + 1) * q.den = (q + (1 - fract q)) * q.den := by ring
        _ = q * q.den + (1 - fract q) * q.den := by rw [add_mul]
        _ = q.num + (1 - fract q) * q.den := by simp

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

Goal state before:
pp: case right
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑q.num.natAbs = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * ↑q⁻¹.den < ↑q⁻¹.den
coprime_q_denom_q_num : (↑q.den).natAbs.Coprime q.num.natAbs
this : (↑q.den).natAbs = q.den
⊢ ↑(↑q.den / ↑q.num).den = ↑q.num.natAbs

Tactic:
rw [q_num_abs_eq_q_num]

Goal state after:
case right
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑q.num.natAbs = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * ↑q⁻¹.den < ↑q⁻¹.den
coprime_q_denom_q_num : (↑q.den).natAbs.Coprime q.num.natAbs
this : (↑q.den).natAbs = q.den
⊢ ↑(↑q.den / ↑q.num).den = q.num
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
x✝ : ℤ
⊢ x✝ ∈ Int.cast ⁻¹' Ici a ↔ x✝ ∈ Ici ⌈a⌉

Tactic:
simp [ceil_le]

Goal state after: