mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.GroupWithZero.Divisibility

Goal state before:
pp: case inl
α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
n : α
hn : IsPrimal n
hm : IsPrimal 0
⊢ IsPrimal (0 * n)

pp: case inr
α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
m n : α
hm : IsPrimal m
hn : IsPrimal n
h0 : m ≠ 0
⊢ IsPrimal (m * n)

Tactic:
·

Goal state after:
case inl
α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
n : α
hn : IsPrimal n
hm : IsPrimal 0
⊢ IsPrimal (0 * n)
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
⊢ a ^ n ∣ a ^ m → n ≤ m

pp: case mpr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
⊢ n ≤ m → a ^ n ∣ a ^ m

Tactic:
·

Goal state after:
case mp
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
⊢ a ^ n ∣ a ^ m → n ≤ m
Module: Mathlib.Algebra.GroupWithZero.Divisibility

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

Tactic:
·

Goal state after:
case mpr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
⊢ n ≤ m → a ^ n ∣ a ^ m
Module: Mathlib.Algebra.GroupWithZero.Divisibility

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : GroupWithZero α
m n : α
x✝ : m ∣ n
hm : m = 0
a : α
ha : n = m * a
⊢ n = 0

pp: case refine_2
α : Type u_1
inst✝ : GroupWithZero α
m n : α
h : m = 0 → n = 0
⊢ m ∣ n

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
inst✝ : GroupWithZero α
m n : α
x✝ : m ∣ n
hm : m = 0
a : α
ha : n = m * a
⊢ n = 0
Module: Mathlib.Algebra.GroupWithZero.Divisibility

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : GroupWithZero α
m n : α
h : m = 0 → n = 0
⊢ m ∣ n

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
inst✝ : GroupWithZero α
m n : α
h : m = 0 → n = 0
⊢ m ∣ n
Module: Mathlib.Algebra.GroupWithZero.Divisibility

Goal state before:
pp: case refine_2.inl
α : Type u_1
inst✝ : GroupWithZero α
m : α
h : m = 0 → 0 = 0
⊢ 0 = m * (m⁻¹ * 0)

pp: case refine_2.inr
α : Type u_1
inst✝ : GroupWithZero α
m n : α
h : m = 0 → n = 0
hn : n ≠ 0
⊢ n = m * (m⁻¹ * n)

Tactic:
·

Goal state after:
case refine_2.inl
α : Type u_1
inst✝ : GroupWithZero α
m : α
h : m = 0 → 0 = 0
⊢ 0 = m * (m⁻¹ * 0)
Module: Mathlib.Algebra.GroupWithZero.Divisibility

Goal state before:
pp: case refine_2.inr
α : Type u_1
inst✝ : GroupWithZero α
m n : α
h : m = 0 → n = 0
hn : n ≠ 0
⊢ n = m * (m⁻¹ * n)

Tactic:
·

Goal state after:
case refine_2.inr
α : Type u_1
inst✝ : GroupWithZero α
m n : α
h : m = 0 → n = 0
hn : n ≠ 0
⊢ n = m * (m⁻¹ * n)
Module: Mathlib.Data.PNat.Defs

Goal state before:
pp: case succ
m k : ℕ+
n : ℕ
⊢ ↑(k.modDivAux (n + 1) (↑m / ↑k)).fst = if n + 1 = 0 then ↑k else n + 1

Tactic:
rw [if_neg n.succ_ne_zero]

Goal state after:
case succ
m k : ℕ+
n : ℕ
⊢ ↑(k.modDivAux (n + 1) (↑m / ↑k)).fst = n + 1
Module: Mathlib.Data.PNat.Defs

Goal state before:
pp: case succ
m k : ℕ+
n : ℕ
⊢ (k.modDivAux (n + 1) (↑m / ↑k)).snd = if n + 1 = 0 then ↑m / ↑k - 1 else ↑m / ↑k

Tactic:
rw [if_neg n.succ_ne_zero]

Goal state after:
case succ
m k : ℕ+
n : ℕ
⊢ (k.modDivAux (n + 1) (↑m / ↑k)).snd = ↑m / ↑k
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: case pos
a b : ℤ
b0 : b = 0
⊢ ↑(a /. b).den ∣ b

pp: case neg
a b : ℤ
b0 : ¬b = 0
⊢ ↑(a /. b).den ∣ b

Tactic:
·

Goal state after:
case pos
a b : ℤ
b0 : b = 0
⊢ ↑(a /. b).den ∣ b
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: case inl
q : ℚ
d : ℤ
hd : d ≠ 0
qdf : q = 0 /. d
⊢ ∃ c, 0 = c * q.num ∧ d = c * ↑q.den

pp: case inr
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
⊢ ∃ c, n = c * q.num ∧ d = c * ↑q.den

Tactic:
·

Goal state after:
case inl
q : ℚ
d : ℤ
hd : d ≠ 0
qdf : q = 0 /. d
⊢ ∃ c, 0 = c * q.num ∧ d = c * ↑q.den
Module: Mathlib.Data.Rat.Lemmas

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

pp: case refine_2
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
⊢ q.num /. ↑q.den = n /. d

Tactic:
·

Goal state after:
case refine_1
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
⊢ ↑q.den ≠ 0
Module: Mathlib.Data.Rat.Cast.CharZero

Goal state before:
pp: α : Type u_3
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
h : ↑{ num := n₁, den := d₁, den_nz := d₁0, reduced := c₁ } = ↑{ num := n₂, den := d₂, den_nz := d₂0, reduced := c₂ }
⊢ { num := n₁, den := d₁, den_nz := d₁0, reduced := c₁ } = { num := n₂, den := d₂, den_nz := d₂0, reduced := c₂ }

Tactic:
have d₁a : (d₁ : α) ≠ 0 := Nat.cast_ne_zero.2 d₁0

Goal state after:
α : Type u_3
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
h : ↑{ num := n₁, den := d₁, den_nz := d₁0, reduced := c₁ } = ↑{ num := n₂, den := d₂, den_nz := d₂0, reduced := c₂ }
d₁a : ↑d₁ ≠ 0
⊢ { num := n₁, den := d₁, den_nz := d₁0, reduced := c₁ } = { num := n₂, den := d₂, den_nz := d₂0, reduced := c₂ }
Module: Mathlib.Data.Rat.Lemmas

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

Tactic:
·

Goal state after:
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: case inr.refine_1
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
this : q.num * d = n * ↑q.den
hqdn : q.num ∣ n
⊢ n = n / q.num * q.num

pp: case inr.refine_2
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
this : q.num * d = n * ↑q.den
hqdn : q.num ∣ n
⊢ d = n / q.num * ↑q.den

Tactic:
·

Goal state after:
case inr.refine_1
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
this : q.num * d = n * ↑q.den
hqdn : q.num ∣ n
⊢ n = n / q.num * q.num
Module: Mathlib.Data.Rat.Lemmas

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

Tactic:
·

Goal state after:
case inr.refine_2
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
this : q.num * d = n * ↑q.den
hqdn : q.num ∣ n
⊢ d = n / q.num * ↑q.den
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: case a
q : ℚ
n : ℤ
⊢ (q + ↑n).den ∣ q.den

pp: case a
q : ℚ
n : ℤ
⊢ q.den ∣ (q + ↑n).den

Tactic:
·

Goal state after:
case a
q : ℚ
n : ℤ
⊢ (q + ↑n).den ∣ q.den
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: case a
q : ℚ
n : ℤ
⊢ q.den ∣ (q + ↑n).den

Tactic:
·

Goal state after:
case a
q : ℚ
n : ℤ
⊢ q.den ∣ (q + ↑n).den
Module: Mathlib.Data.Rat.Lemmas

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

pp: case mpr
q : ℚ
⊢ IsSquare q.num ∧ IsSquare q.den → IsSquare q

Tactic:
·

Goal state after:
case mp
q : ℚ
⊢ IsSquare q → IsSquare q.num ∧ IsSquare q.den
Module: Mathlib.Data.Rat.Lemmas

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

Tactic:
·

Goal state after:
case mpr
q : ℚ
⊢ IsSquare q.num ∧ IsSquare q.den → IsSquare q
Module: Mathlib.Data.Rat.Cast.CharZero

Goal state before:
pp: α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
p q : ℚ≥0
hpq : ↑p.num * ↑q.den = ↑q.num * ↑p.den
⊢ ↑p.num * ↑q.den = ↑q.num * ↑p.den

pp: case hb
α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
p q : ℚ≥0
hpq : ↑p.num * ↑q.den = ↑q.num * ↑p.den
⊢ ↑p.den ≠ 0

pp: case hd
α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
p q : ℚ≥0
hpq : ↑p.num * ↑q.den = ↑q.num * ↑p.den
⊢ ↑q.den ≠ 0

pp: case hbd
α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
p q : ℚ≥0
hpq : ↑p.num / ↑p.den = ↑q.num / ↑q.den
⊢ Commute ↑p.den ↑q.den

pp: case hb
α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
p q : ℚ≥0
hpq : ↑p.num / ↑p.den = ↑q.num / ↑q.den
⊢ ↑p.den ≠ 0

pp: case hd
α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
p q : ℚ≥0
hpq : ↑p.num / ↑p.den = ↑q.num / ↑q.den
⊢ ↑q.den ≠ 0

Tactic:
·

Goal state after:
α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
p q : ℚ≥0
hpq : ↑p.num * ↑q.den = ↑q.num * ↑p.den
⊢ ↑p.num * ↑q.den = ↑q.num * ↑p.den
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionSemiring α
a b : ℕ
hb : ↑b ≠ 0
d : ℕ
h : d ≠ 0
n : ℕ
c : (↑n).natAbs.Coprime d
hn : 0 ≤ { num := ↑n, den := d, den_nz := h, reduced := c }
hd : ↑d ≠ 0
hb' : b ≠ 0
e : a * d = n * b
⊢ ↑n * ↑b = ↑a * ↑d

pp: α : Type u_3
inst✝ : DivisionSemiring α
a b : ℕ
hb : ↑b ≠ 0
d : ℕ
h : d ≠ 0
n : ℕ
c : (↑n).natAbs.Coprime d
hn : 0 ≤ { num := ↑n, den := d, den_nz := h, reduced := c }
hd : ↑d ≠ 0
hb' : b ≠ 0
e : a * d = n * b
⊢ Commute ↑d ↑b

Tactic:
·

Goal state after:
α : Type u_3
inst✝ : DivisionSemiring α
a b : ℕ
hb : ↑b ≠ 0
d : ℕ
h : d ≠ 0
n : ℕ
c : (↑n).natAbs.Coprime d
hn : 0 ≤ { num := ↑n, den := d, den_nz := h, reduced := c }
hd : ↑d ≠ 0
hb' : b ≠ 0
e : a * d = n * b
⊢ ↑n * ↑b = ↑a * ↑d
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.num * r.den + q.den * r.num) / ↑(q.den * r.den) = (↑q.num * ↑r.den + ↑q.den * ↑r.num) / (↑q.den * ↑r.den)

pp: case hb
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑(q.den * r.den) ≠ 0

Tactic:
·

Goal state after:
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑(q.num * r.den + q.den * r.num) / ↑(q.den * r.den) = (↑q.num * ↑r.den + ↑q.den * ↑r.num) / (↑q.den * ↑r.den)
Module: Mathlib.Data.Rat.Cast.Defs

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

Tactic:
·

Goal state after:
case hb
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑(q.den * r.den) ≠ 0
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.num * r.num) / ↑(q.den * r.den) = ↑q.num * ↑r.num / (↑q.den * ↑r.den)

pp: case hb
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑(q.den * r.den) ≠ 0

Tactic:
·

Goal state after:
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑(q.num * r.num) / ↑(q.den * r.den) = ↑q.num * ↑r.num / (↑q.den * ↑r.den)
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.num * r.den) / ↑(q.den * r.num) = ↑q.num * ↑r.den / (↑q.den * ↑r.num)

pp: case hb
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.num ≠ 0
⊢ ↑(q.den * r.num) ≠ 0

Tactic:
·

Goal state after:
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.num ≠ 0
⊢ ↑(q.num * r.den) / ↑(q.den * r.num) = ↑q.num * ↑r.den / (↑q.den * ↑r.num)
Module: Mathlib.Data.Rat.Cast.Defs

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

Tactic:
·

Goal state after:
case hb
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.num ≠ 0
⊢ ↑(q.den * r.num) ≠ 0
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
⊢ ↑(a /. b) = ↑a / ↑b

Tactic:
have b0' : b ≠ 0 := by
    refine mt ?_ b0
    simp +contextual

Goal state after:
α : Type u_3
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
⊢ ↑(a /. b) = ↑a / ↑b
Module: Mathlib.Data.Rat.Cast.Defs

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

pp: case hb
α : Type u_3
inst✝ : DivisionRing α
q r : ℚ
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑(q.den * r.den) ≠ 0

Tactic:
·

Goal state after:
α : Type u_3
inst✝ : DivisionRing α
q r : ℚ
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑(q.num * ↑r.den + ↑q.den * r.num) / ↑(q.den * r.den) = (↑q.num * ↑r.den + ↑q.den * ↑r.num) / (↑q.den * ↑r.den)
Module: Mathlib.Data.Rat.Cast.Defs

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

Tactic:
·

Goal state after:
case hb
α : Type u_3
inst✝ : DivisionRing α
q r : ℚ
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑(q.den * r.den) ≠ 0
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.num * q.num) / ↑(p.den * q.den) = ↑p.num * ↑q.num / (↑p.den * ↑q.den)

pp: case hb
α : Type u_3
inst✝ : DivisionRing α
p q : ℚ
hp : ↑p.den ≠ 0
hq : ↑q.den ≠ 0
⊢ ↑(p.den * q.den) ≠ 0

Tactic:
·

Goal state after:
α : Type u_3
inst✝ : DivisionRing α
p q : ℚ
hp : ↑p.den ≠ 0
hq : ↑q.den ≠ 0
⊢ ↑(p.num * q.num) / ↑(p.den * q.den) = ↑p.num * ↑q.num / (↑p.den * ↑q.den)
Module: Mathlib.Data.Rat.Cast.Defs

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

Tactic:
·

Goal state after:
case hb
α : Type u_3
inst✝ : DivisionRing α
p q : ℚ
hp : ↑p.den ≠ 0
hq : ↑q.den ≠ 0
⊢ ↑(p.den * q.den) ≠ 0
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: case left
a b c d : ℤ
hb0 : 0 < b
hd0 : 0 < d
h1 : a.natAbs.Coprime b.natAbs
h2 : c.natAbs.Coprime d.natAbs
h : ↑a / ↑b = ↑c / ↑d
⊢ a = c

pp: case right
a b c d : ℤ
hb0 : 0 < b
hd0 : 0 < d
h1 : a.natAbs.Coprime b.natAbs
h2 : c.natAbs.Coprime d.natAbs
h : ↑a / ↑b = ↑c / ↑d
⊢ b = d

Tactic:
·

Goal state after:
case left
a b c d : ℤ
hb0 : 0 < b
hd0 : 0 < d
h1 : a.natAbs.Coprime b.natAbs
h2 : c.natAbs.Coprime d.natAbs
h : ↑a / ↑b = ↑c / ↑d
⊢ a = c
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: case right
a b c d : ℤ
hb0 : 0 < b
hd0 : 0 < d
h1 : a.natAbs.Coprime b.natAbs
h2 : c.natAbs.Coprime d.natAbs
h : ↑a / ↑b = ↑c / ↑d
⊢ b = d

Tactic:
·

Goal state after:
case right
a b c d : ℤ
hb0 : 0 < b
hd0 : 0 < d
h1 : a.natAbs.Coprime b.natAbs
h2 : c.natAbs.Coprime d.natAbs
h : ↑a / ↑b = ↑c / ↑d
⊢ b = d
Module: Mathlib.Data.Rat.Cast.Defs

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

pp: case b0
α : Type u_3
inst✝ : DivisionRing α
p q : ℚ
hp : ↑p.den ≠ 0
hq : ↑q.num ≠ 0
⊢ ↑(↑p.den * q.num) ≠ 0

Tactic:
·

Goal state after:
α : Type u_3
inst✝ : DivisionRing α
p q : ℚ
hp : ↑p.den ≠ 0
hq : ↑q.num ≠ 0
⊢ ↑(p.num * ↑q.den) / ↑(↑p.den * q.num) = ↑p.num * ↑q.den / (↑p.den * ↑q.num)
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: case pos
n : ℤ
hn : n = 0
⊢ ↑(n / n) = ↑n / ↑n

pp: case neg
n : ℤ
hn : ¬n = 0
⊢ ↑(n / n) = ↑n / ↑n

Tactic:
·

Goal state after:
case pos
n : ℤ
hn : n = 0
⊢ ↑(n / n) = ↑n / ↑n
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: case neg
n : ℤ
hn : ¬n = 0
⊢ ↑(n / n) = ↑n / ↑n

Tactic:
·

Goal state after:
case neg
n : ℤ
hn : ¬n = 0
⊢ ↑(n / n) = ↑n / ↑n
Module: Mathlib.Data.Rat.Cast.Defs

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

Tactic:
·

Goal state after:
case b0
α : Type u_3
inst✝ : DivisionRing α
p q : ℚ
hp : ↑p.den ≠ 0
hq : ↑q.num ≠ 0
⊢ ↑(↑p.den * q.num) ≠ 0
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: case mp
m n : ℤ
hn : ↑n ≠ 0
⊢ (↑m / ↑n).den = 1 → n ∣ m

pp: case mpr
m n : ℤ
hn : ↑n ≠ 0
⊢ n ∣ m → (↑m / ↑n).den = 1

Tactic:
·

Goal state after:
case mp
m n : ℤ
hn : ↑n ≠ 0
⊢ (↑m / ↑n).den = 1 → n ∣ m
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: case mpr
m n : ℤ
hn : ↑n ≠ 0
⊢ n ∣ m → (↑m / ↑n).den = 1

Tactic:
·

Goal state after:
case mpr
m n : ℤ
hn : ↑n ≠ 0
⊢ n ∣ m → (↑m / ↑n).den = 1
Module: Mathlib.Tactic.CancelDenoms.Core

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : 0 < ad
hbd : 0 < bd
hgcd : 0 < gcd
⊢ 0 < ad * bd

pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : 0 < ad
hbd : 0 < bd
hgcd : 0 < gcd
⊢ 0 < 1 / gcd

Tactic:
·

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : 0 < ad
hbd : 0 < bd
hgcd : 0 < gcd
⊢ 0 < ad * bd
Module: Mathlib.Tactic.CancelDenoms.Core

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : 0 < ad
hbd : 0 < bd
hgcd : 0 < gcd
⊢ 0 < 1 / gcd

Tactic:
·

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : 0 < ad
hbd : 0 < bd
hgcd : 0 < gcd
⊢ 0 < 1 / gcd
Module: Mathlib.Algebra.Order.Ring.Canonical

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

pp: case inr
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
this : MulPosStrictMono R
hc : 0 < c
⊢ a * c < b * d

Tactic:
·

Goal state after:
case inl
R : Type u
inst✝³ : CommSemiring R
inst✝² : PartialOrder R
inst✝¹ : CanonicallyOrderedAdd R
inst✝ : PosMulStrictMono R
a b d : R
hab : a < b
this : MulPosStrictMono R
hcd : 0 < d
⊢ a * 0 < b * d
Module: Mathlib.Algebra.Order.Ring.Canonical

Goal state before:
pp: case inr
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
this : MulPosStrictMono R
hc : 0 < c
⊢ a * c < b * d

Tactic:
·

Goal state after:
case inr
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
this : MulPosStrictMono R
hc : 0 < c
⊢ a * c < b * d
Module: Mathlib.Algebra.Order.Ring.Canonical

Goal state before:
pp: case inl
R : Type u
inst✝⁵ : NonUnitalNonAssocSemiring R
inst✝⁴ : PartialOrder R
inst✝³ : CanonicallyOrderedAdd R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
a b c : R
h : AddLECancellable (a * c)
hbc : b ≤ c
⊢ a * (b - c) = a * b - a * c

pp: case inr
R : Type u
inst✝⁵ : NonUnitalNonAssocSemiring R
inst✝⁴ : PartialOrder R
inst✝³ : CanonicallyOrderedAdd R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
a b c : R
h : AddLECancellable (a * c)
hcb : c ≤ b
⊢ a * (b - c) = a * b - a * c

Tactic:
·

Goal state after:
case inl
R : Type u
inst✝⁵ : NonUnitalNonAssocSemiring R
inst✝⁴ : PartialOrder R
inst✝³ : CanonicallyOrderedAdd R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
a b c : R
h : AddLECancellable (a * c)
hbc : b ≤ c
⊢ a * (b - c) = a * b - a * c
Module: Mathlib.Algebra.Order.Ring.Canonical

Goal state before:
pp: case inr
R : Type u
inst✝⁵ : NonUnitalNonAssocSemiring R
inst✝⁴ : PartialOrder R
inst✝³ : CanonicallyOrderedAdd R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
a b c : R
h : AddLECancellable (a * c)
hcb : c ≤ b
⊢ a * (b - c) = a * b - a * c

Tactic:
·

Goal state after:
case inr
R : Type u
inst✝⁵ : NonUnitalNonAssocSemiring R
inst✝⁴ : PartialOrder R
inst✝³ : CanonicallyOrderedAdd R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
a b c : R
h : AddLECancellable (a * c)
hcb : c ≤ b
⊢ a * (b - c) = a * b - a * c
Module: Mathlib.Algebra.Order.Ring.Canonical

Goal state before:
pp: case inl
R : Type u
inst✝⁶ : NonUnitalNonAssocSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : CanonicallyOrderedAdd R
inst✝³ : Sub R
inst✝² : OrderedSub R
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : MulRightMono R
a b c : R
h : AddLECancellable (b * c)
hab : a ≤ b
⊢ (a - b) * c = a * c - b * c

pp: case inr
R : Type u
inst✝⁶ : NonUnitalNonAssocSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : CanonicallyOrderedAdd R
inst✝³ : Sub R
inst✝² : OrderedSub R
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : MulRightMono R
a b c : R
h : AddLECancellable (b * c)
hba : b ≤ a
⊢ (a - b) * c = a * c - b * c

Tactic:
·

Goal state after:
case inl
R : Type u
inst✝⁶ : NonUnitalNonAssocSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : CanonicallyOrderedAdd R
inst✝³ : Sub R
inst✝² : OrderedSub R
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : MulRightMono R
a b c : R
h : AddLECancellable (b * c)
hab : a ≤ b
⊢ (a - b) * c = a * c - b * c
Module: Mathlib.Algebra.Order.Ring.Canonical

Goal state before:
pp: case inr
R : Type u
inst✝⁶ : NonUnitalNonAssocSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : CanonicallyOrderedAdd R
inst✝³ : Sub R
inst✝² : OrderedSub R
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : MulRightMono R
a b c : R
h : AddLECancellable (b * c)
hba : b ≤ a
⊢ (a - b) * c = a * c - b * c

Tactic:
·

Goal state after:
case inr
R : Type u
inst✝⁶ : NonUnitalNonAssocSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : CanonicallyOrderedAdd R
inst✝³ : Sub R
inst✝² : OrderedSub R
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : MulRightMono R
a b c : R
h : AddLECancellable (b * c)
hba : b ≤ a
⊢ (a - b) * c = a * c - b * c
Module: Mathlib.Order.CompleteLattice.Defs

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
i : CompleteLinearOrder α
a b : α
h : a ≤ b
⊢ min a b = a

pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
i : CompleteLinearOrder α
a b : α
h : ¬a ≤ b
⊢ min a b = b

Tactic:
·

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
i : CompleteLinearOrder α
a b : α
h : a ≤ b
⊢ min a b = a
Module: Mathlib.Order.CompleteLattice.Defs

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
i : CompleteLinearOrder α
a b : α
h : ¬a ≤ b
⊢ min a b = b

Tactic:
·

Goal state after:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
i : CompleteLinearOrder α
a b : α
h : ¬a ≤ b
⊢ min a b = b
Module: Mathlib.Order.CompleteLattice.Lemmas

Goal state before:
pp: case a
α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ ∀ i ≥ n, u i ≤ ⨆ i, u (i + n)

pp: case a
α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ ∀ (i : ℕ), u (i + n) ≤ ⨆ i, ⨆ (_ : i ≥ n), u i

Tactic:
·

Goal state after:
case a
α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ ∀ i ≥ n, u i ≤ ⨆ i, u (i + n)
Module: Mathlib.Order.CompleteLattice.Defs

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
i : CompleteLinearOrder α
a b : α
h : a ≤ b
⊢ max a b = b

pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
i : CompleteLinearOrder α
a b : α
h : ¬a ≤ b
⊢ max a b = a

Tactic:
·

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
i : CompleteLinearOrder α
a b : α
h : a ≤ b
⊢ max a b = b
Module: Mathlib.Order.CompleteLattice.Lemmas

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

Tactic:
·

Goal state after:
case a
α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ ∀ (i : ℕ), u (i + n) ≤ ⨆ i, ⨆ (_ : i ≥ n), u i