mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
p : α → Prop
ys✝ : List α
head✝ : α
tail✝ : List α
⊢ Forall p (head✝ :: tail✝ ++ ys✝) ↔ Forall p (head✝ :: tail✝) ∧ Forall p ys✝

Tactic:
by

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

Goal state before:
pp: q a✝ b c : ℚ
C : ℚ → Sort u_1
a : ℚ
div : (n : ℤ) → (d : ℕ) → d ≠ 0 → n.natAbs.Coprime d → C (↑n / ↑d)
n : ℤ
d : ℕ
nz : d ≠ 0
red : n.natAbs.Coprime d
⊢ C { num := n, den := d, den_nz := nz, reduced := red }

Tactic:
by

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

Goal state before:
pp: α : Type u
p : α → Prop
x : α
l : List α
⊢ Forall p (x :: l) ↔ ∀ (x_1 : α), x_1 ∈ x :: l → p x_1

Tactic:
by

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

Goal state before:
pp: α : Type u
p q : α → Prop
h : ∀ (x : α), p x → q x
x : α
l : List α
⊢ Forall p (x :: l) → Forall q (x :: l)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
l : List α
p : β → Prop
f : α → β
⊢ Forall p (map f l) ↔ Forall (p ∘ f) l

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
i : Fin l.attach.length
⊢ ↑(l.attach.get i) = l.get ⟨↑i, ⋯⟩

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: x✝¹ : ℕ
x✝ : ℚ
⊢ x✝ ^ ↑x✝¹.succ = x✝ ^ ↑x✝¹ * x✝

Tactic:
by

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

Goal state before:
pp: a b : ℕ
hab : ↑a = ↑b
⊢ a = b

Tactic:
by

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

Goal state before:
pp: ⊢ CommSemiring ℚ

Tactic:
by

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

Goal state before:
pp: ⊢ Semiring ℚ

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: r : ℚ
⊢ ↑r.num / ↑r.den = r

Tactic:
by

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

Goal state before:
pp: num : ℕ
den : ℤ
n : ℕ
⊢ (↑num /. den) ^ n = ↑num ^ n /. den ^ n

Tactic:
by

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

Goal state before:
pp: num den n : ℕ
⊢ mkRat (↑num) den ^ n = mkRat (↑num ^ n) (den ^ n)

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ ↑n = ↑n /. 1

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
s t : List α
hs : ∀ (a : α), a ∈ s → p a
ht : ∀ (a : α), a ∈ t → p a
hf : ∀ (a a' : α) (ha : p a) (ha' : p a'), f a ha = f a' ha' → a = a'
h : s.Disjoint t
⊢ (pmap f s hs).Disjoint (pmap f t ht)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s t : List α
hf : Injective f
h : s.Disjoint t
⊢ (map f s).Disjoint (map f t)

Tactic:
by

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

Goal state before:
pp: α : Type u
l₁ l₂ l : List α
p : l₁ ~ l₂
⊢ l₁.Disjoint l ↔ l₂.Disjoint l

Tactic:
by

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

Goal state before:
pp: q : ℚ
⊢ q * ↑q.den = ↑q.num

Tactic:
by

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

Goal state before:
pp: α : Type u
l₁ l₂ l : List α
p : l₁ ~ l₂
⊢ l.Disjoint l₁ ↔ l.Disjoint l₂

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
f : α → β
a : α
as : List α
h : a ∈ as
⊢ lookup a (map (fun x ↦ (x, f x)) as) = some (f a)

Tactic:
by

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

Goal state before:
pp: q : ℚ
⊢ ↑q.den * q = ↑q.num

Tactic:
by

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

Goal state before:
pp: a b : ℕ
⊢ range' a b 0 = replicate b a

Tactic:
by

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

Goal state before:
pp: a b s x : ℕ
hx : x ∈ range' a b s
⊢ a ≤ x

Tactic:
by

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

Goal state before:
pp: a : ℤ
ha : 0 ≤ a
b : ℕ
⊢ 0 ≤ mkRat a b

Tactic:
by

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

Goal state before:
pp: m e : ℕ
⊢ ¬false = true

Tactic:
by

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

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

Tactic:
by

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

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

Goal state before:
pp: a : ℤ
b : ℕ
hb : b ≠ 0
⊢ 0 < mkRat a b ↔ 0 < a

Tactic:
by

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

Goal state before:
pp: a : ℤ
b : ℕ
hb : b ≠ 0
⊢ mkRat a b ≤ 0 ↔ a ≤ 0

Tactic:
grind [mkRat_pos_iff]

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

Goal state before:
pp: a : ℤ
b : ℕ
hb : b ≠ 0
⊢ mkRat a b ≤ 0 ↔ a ≤ 0

Tactic:
by

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

Goal state before:
pp: a : ℤ
ha : a ≤ 0
b : ℕ
⊢ mkRat a b ≤ 0

Tactic:
by

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

Goal state before:
pp: a : ℤ
b : ℕ
hb : b ≠ 0
⊢ mkRat a b < 0 ↔ a < 0

Tactic:
by

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

Goal state before:
pp: a : ℚ
⊢ a.num ≤ 0 ↔ a ≤ 0

Tactic:
by

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

Goal state before:
pp: a b c d : ℤ
b_pos : 0 < b
d_pos : 0 < d
⊢ ↑a / ↑b < ↑c / ↑d ↔ a * d < c * b

Tactic:
by

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

Goal state before:
pp: q : ℚ
⊢ q.num ≤ ↑q.den ↔ q ≤ 1

Tactic:
by

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

Goal state before:
pp: q : ℚ
⊢ q.num < ↑q.den ↔ q < 1

Tactic:
by

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

Goal state before:
pp: q : ℚ
⊢ |q| = ↑q.num.natAbs /. ↑q.den

Tactic:
by

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

Goal state before:
pp: q : ℚ
⊢ |q| = { num := |q.num|, den := q.den, den_nz := ⋯, reduced := ⋯ }

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: q : ℚ≥0
⊢ ↑q = ↑q.num / ↑q.den

Tactic:
by

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

Goal state before:
pp: a : ℚ
ha : 0 ≤ a
⊢ 0 ≤ a⁻¹

Tactic:
by

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

Goal state before:
pp: q : ℚ≥0
⊢ q⁻¹ = divNat q.den q.num

Tactic:
by

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

Goal state before:
pp: p q : ℚ≥0
⊢ p / q = divNat (p.num * q.den) (p.den * q.num)

Tactic:
by

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

Goal state before:
pp: a b : ℕ
⊢ divNat a b = ↑a / ↑b

Tactic:
by

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

Goal state before:
pp: q : ℚ≥0
hq : q ≠ 0
⊢ q⁻¹.num = q.den

Tactic:
by

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

Goal state before:
pp: q : ℚ≥0
hq : q ≠ 0
⊢ q⁻¹.den = q.num

Tactic:
by

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

Goal state before:
pp: q : ℚ≥0
⊢ ↑q.num / ↑q.den = q

Tactic:
by

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

Goal state before:
pp: a : ℚ≥0
⊢ a ^ 0 = 1

Tactic:
by

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

Goal state before:
pp: n : ℕ
a : ℚ≥0
⊢ a ^ ↑n.succ = a ^ ↑n * a

Tactic:
by

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

Goal state before:
pp: n : ℕ
a : ℚ≥0
⊢ a ^ Int.negSucc n = (a ^ ↑n.succ)⁻¹

Tactic:
by

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

Goal state before:
pp: ⊢ 0⁻¹ = 0

Tactic:
by

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

Goal state before:
pp: q : ℚ≥0
h : q ≠ 0
⊢ q * q⁻¹ = 1

Tactic:
by

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

Goal state before:
pp: r : ℚ
hr : 0 ≤ r
p q : ℚ
hpq : p ≤ q
⊢ r * p ≤ r * q

Tactic:
by

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

Goal state before:
pp: p q : ℚ≥0
⊢ 1 ≠ 0

Tactic:
by

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

Goal state before:
pp: p q : ℚ≥0
a b : ℕ
hab : ↑a = ↑b
⊢ a = b

Tactic:
by

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

Goal state before:
pp: q : ℚ≥0
n : ℕ
⊢ (q ^ n).num = q.num ^ n

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: q : ℚ≥0
⊢ ↑q = 0 ↔ q = 0

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ ↑(↑n).toNNRat = ↑↑n

Tactic:
by

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

Goal state before:
pp: q : ℚ
⊢ 0 < q.toNNRat ↔ 0 < q

Tactic:
by

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

Goal state before:
pp: q : ℚ
⊢ q.toNNRat = 0 ↔ q ≤ 0

Tactic:
by

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

Goal state before:
pp: p q : ℚ
hp : 0 ≤ p
⊢ q.toNNRat ≤ p.toNNRat ↔ q ≤ p

Tactic:
by

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

Goal state before:
pp: p q : ℚ
⊢ q.toNNRat < p.toNNRat ↔ q < p ∧ 0 < p

Tactic:
by

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

Goal state before:
pp: p q : ℚ
hq : 0 ≤ q
hp : 0 ≤ p
⊢ ↑(q + p).toNNRat = ↑(q.toNNRat + p.toNNRat)

Tactic:
by

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

Goal state before:
pp: p : ℚ
q : ℚ≥0
hp : 0 ≤ p
⊢ q ≤ p.toNNRat ↔ ↑q ≤ p

Tactic:
by

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

Goal state before:
pp: p : ℚ
q : ℚ≥0
hq : 0 < q
hp : p < 0
⊢ q ≤ p.toNNRat ↔ ↑q ≤ p

Tactic:
by

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

Goal state before:
pp: q : ℚ
p : ℚ≥0
hq : 0 ≤ q
⊢ q.toNNRat < p ↔ q < ↑p

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : NNRatCast K
m : ℕ
b : Bool
d : ℕ
⊢ OfScientific.ofScientific m b d = ↑(if b = true then NNRat.divNat m (10 ^ d) else ↑(m * 10 ^ d))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Semiconj.Basic

Goal state before:
pp: G : Type u_1
inst✝ : DivisionMonoid G
a x y : G
⊢ SemiconjBy a⁻¹ x⁻¹ y⁻¹ ↔ SemiconjBy a y x

Tactic:
by

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

Goal state before:
pp: p q : ℚ
hp : 0 ≤ p
⊢ (p * q).toNNRat = p.toNNRat * q.toNNRat

Tactic:
by

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

Goal state before:
pp: q : ℚ≥0
⊢ (↑q).num = ↑q.num

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Semiconj.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a x y : G
⊢ SemiconjBy a⁻¹ y x ↔ SemiconjBy a x y

Tactic:
by

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

Goal state before:
pp: q : ℚ≥0
⊢ q.num ≠ 0 ↔ q ≠ 0

Tactic:
by

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

Goal state before:
pp: q : ℚ≥0
⊢ 0 < q.num ↔ 0 < q

Tactic:
by

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

Goal state before:
pp: q : ℚ≥0
⊢ q.num.Coprime q.den

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Semiconj.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a x y : G
⊢ SemiconjBy a x⁻¹ y⁻¹ ↔ SemiconjBy a x y

Tactic:
by

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

Goal state before:
pp: p q : ℚ≥0
hn : p.num = q.num
hd : p.den = q.den
⊢ p = q

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Semiconj.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a x y : G
h : SemiconjBy a x y
n : ℕ
⊢ SemiconjBy a (x ^ ↑n) (y ^ ↑n)

Tactic:
by

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

Goal state before:
pp: p q : ℚ≥0
⊢ p = q → p.num = q.num ∧ p.den = q.den

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Semiconj.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a x y : G
h : SemiconjBy a x y
n : ℕ
⊢ SemiconjBy a (x ^ Int.negSucc n) (y ^ Int.negSucc n)

Tactic:
by

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

Goal state before:
pp: n₁ n₂ d₁ d₂ : ℕ
h₁ : d₁ ≠ 0
h₂ : d₂ ≠ 0
⊢ divNat n₁ d₁ = divNat n₂ d₂ ↔ n₁ * d₂ = n₂ * d₁

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ divNat n 0 = 0

Tactic:
by

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

Goal state before:
pp: q : ℚ≥0
⊢ ↑(divNat q.num q.den) = ↑q

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Semiconj.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a x y : G
h : SemiconjBy a x y
⊢ x = 1 ↔ y = 1

Tactic:
by

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

Goal state before:
pp: n₁ n₂ d₁ d₂ : ℕ
⊢ divNat n₁ d₁ * divNat n₂ d₂ = divNat (n₁ * n₂) (d₁ * d₂)

Tactic:
by

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

Goal state before:
pp: a : ℕ
ha : a ≠ 0
n d : ℕ
⊢ divNat (a * n) (a * d) = divNat n d

Tactic:
by

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

Goal state before:
pp: a : ℕ
ha : a ≠ 0
n d : ℕ
⊢ divNat (n * a) (d * a) = divNat n d

Tactic:
by

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

Goal state before:
pp: q : ℚ≥0
⊢ q * ↑q.den = ↑q.num

Tactic:
by

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

Goal state before:
pp: q : ℚ≥0
⊢ ↑q.den * q = ↑q.num

Tactic:
by

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

Goal state before:
pp: p q✝ : ℚ≥0
n₁ n₂ d₁ d₂ : ℕ
C : ℚ≥0 → Sort u
q : ℚ≥0
H : (n d : ℕ) → d ≠ 0 → n.Coprime d → C (divNat n d)
⊢ C q

Tactic:
by

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

Goal state before:
pp: q r : ℚ≥0
⊢ q + r = divNat (q.num * r.den + r.num * q.den) (q.den * r.den)

Tactic:
by

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

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

Tactic:
by

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:
by

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:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a : α
u : αˣ
⊢ a = ↑u * (↑u⁻¹ * a)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : SemigroupWithZero α
a : α
h : a = 0
⊢ 0 = 0 * 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : SemigroupWithZero α
a : α
h : a = 0
⊢ 0 ∣ a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : SemigroupWithZero α
a : α
⊢ a * 0 = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MonoidWithZero α
inst✝ : IsLeftCancelMulZero α
a b c : α
ha : a ≠ 0
d : α
⊢ a * c = a * b * d ↔ c = b * d

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
u : αˣ
x✝ : a ∣ b * ↑u
c : α
eq : b * ↑u = a * c
⊢ b = a * (c * ↑u⁻¹)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a b c : α
hc : c ≠ 0
d : α
⊢ b * c = a * c * d ↔ b = a * d

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
u : αˣ
h : a ∣ b
⊢ a * ↑u * ↑u⁻¹ = a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
a b : α
u : αˣ
⊢ a ∣ ↑u * b ↔ a ∣ b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
a b : α
u : αˣ
⊢ ↑u * a ∣ b ↔ a ∣ b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a u : α
hu : IsUnit u
⊢ u ∣ a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoidWithZero α
a b : α
hd : a ∣ b
hnd : ¬b ∣ a
⊢ DvdNotUnit a b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b u : α
hu : IsUnit u
⊢ a ∣ b * u ↔ a ∣ b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
x y : α
inst✝ : Nontrivial α
h : IsRelPrime x y
⊢ x = 0 → y ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Commute.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Semigroup G
a b c : G
h : SemiconjBy a b c
j : G
⊢ (fun x ↦ a * x) ((fun x ↦ b * x) j) = (fun x ↦ c * x) ((fun x ↦ a * x) j)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b u : α
hu : IsUnit u
⊢ a * u ∣ b ↔ a ∣ b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
a b u : α
hu : IsUnit u
⊢ a ∣ u * b ↔ a ∣ b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Commute.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Semigroup G
a b c : G
h : SemiconjBy a b c
j : G
⊢ (fun x ↦ x * a) ((fun x ↦ x * c) j) = (fun x ↦ x * b) ((fun x ↦ x * a) j)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
a b u : α
hu : IsUnit u
⊢ u * a ∣ b ↔ a ∣ b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : MonoidWithZero α
x y : α
nonzero : ¬(x = 0 ∧ y = 0)
H : ∀ (z : α), ¬IsUnit z → z ≠ 0 → z ∣ x → ¬z ∣ y
⊢ IsRelPrime x y

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
x y : α
x✝ : x ∣ y ∧ ¬y ∣ x
d : α
hd : y = x * d
hyx : ¬y ∣ x
hx0 : x = 0
⊢ False

Tactic:
simp [hx0] at hyx

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
x y : α
x✝ : x ∣ y ∧ ¬y ∣ x
d : α
hd : y = x * d
hyx : ¬y ∣ x
hx0 : x = 0
⊢ False

Tactic:
by

Goal state after:
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

Goal state after:
Module: Mathlib.Algebra.Group.Commute.Basic

Goal state before:
pp: G : Type u_1
inst✝ : DivisionMonoid G
a b c d : G
hbd : Commute b d
hbc : Commute b⁻¹ c
⊢ a / b * (c / d) = a * c / (b * d)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
x y : α
x✝¹ : x ∣ y ∧ ¬y ∣ x
d : α
hd : y = x * d
hyx : ¬y ∣ x
x✝ : d ∣ 1
e : α
he : 1 = d * e
⊢ x = y * e

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
x y z : α
H : IsRelPrime x (y * z)
⊢ IsRelPrime x y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Commute.Basic

Goal state before:
pp: G : Type u_1
inst✝ : DivisionMonoid G
a b c d : G
hbc : Commute b c
hbd : Commute b⁻¹ d
hcd : Commute c⁻¹ d
⊢ a / b / (c / d) = a / c / (b / d)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
x y z : α
h : IsRelPrime y z
dvd : x ∣ y
⊢ IsRelPrime x z

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Commute.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a b : G
h : Commute a b
⊢ a⁻¹ * b * a = b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
x y z : α
hu : IsUnit x
⊢ IsRelPrime y (x * z) ↔ IsRelPrime y z

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Commute.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a b : G
h : Commute a b
⊢ a⁻¹ * (b * a) = b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
x y z : α
hu : IsUnit x
⊢ IsRelPrime (x * y) (x * z) ↔ IsRelPrime y z

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
x y z : α
hu : IsUnit x
⊢ IsRelPrime (y * x) z ↔ IsRelPrime y z

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
x y : α
x✝¹ : DvdNotUnit x y
hx0 : x ≠ 0
d : α
hdu : ¬IsUnit d
hdx : y = x * d
x✝ : y ∣ x
e : α
he : x = y * e
⊢ x * 1 = x * (d * e)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : MonoidWithZero α
p q : α
h₁ : q ≠ 0
h₂ : p ∣ q
⊢ p ≠ 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
x y z : α
hu : IsUnit x
⊢ IsRelPrime y (z * x) ↔ IsRelPrime y z

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
x y z : α
hu : IsUnit x
⊢ IsRelPrime (y * x) (z * x) ↔ IsRelPrime y z

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
x y z : α
H1 : IsRelPrime x z
H2 : x ∣ y * z
h : IsPrimal x
⊢ x ∣ y

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoid α
x y z : α
inst✝ : DecompositionMonoid α
H1 : IsRelPrime x z
H2 : IsRelPrime y z
x✝ : α
h : x✝ ∣ x * y
hz : x✝ ∣ z
⊢ IsUnit x✝

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoid α
x y z : α
inst✝ : DecompositionMonoid α
H1 : IsRelPrime x y
H2 : IsRelPrime x z
⊢ IsRelPrime x (y * z)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
a b : α
inst✝ : Subsingleton αˣ
⊢ a ∣ b → b ∣ a → a = b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
h : a ^ n ∣ a ^ m
hmn : m < n
⊢ a ^ m * a ∣ a ^ m * 1

Tactic:
by

Goal state after: