mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case inl.inl
R : Type u_1
inst✝ : EuclideanDomain R
c : R
⊢ (0 * c / 0) ^ 0 = (0 * c) ^ 0 / 0 ^ 0

pp: case inl.inr
R : Type u_1
inst✝ : EuclideanDomain R
n : ℕ
c : R
hn : n ≠ 0
⊢ (0 * c / 0) ^ n = (0 * c) ^ n / 0 ^ n

Tactic:
<;>

Goal state after:
case inl.inl
R : Type u_1
inst✝ : EuclideanDomain R
c : R
⊢ (0 * c / 0) ^ 0 = (0 * c) ^ 0 / 0 ^ 0

case inl.inr
R : Type u_1
inst✝ : EuclideanDomain R
n : ℕ
c : R
hn : n ≠ 0
⊢ (0 * c / 0) ^ n = (0 * c) ^ n / 0 ^ n
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case mp.refine_3.refine_1
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
ax : ι →₀ R
hax : ∀ (i : ι), ax i ∈ I
ay : ι →₀ R
hay : ∀ (i : ι), ay i ∈ I
⊢ ∀ (a : ι), 0 • f a = 0

pp: case mp.refine_3.refine_2
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
ax : ι →₀ R
hax : ∀ (i : ι), ax i ∈ I
ay : ι →₀ R
hay : ∀ (i : ι), ay i ∈ I
⊢ ∀ (a : ι) (b₁ b₂ : R), (b₁ + b₂) • f a = b₁ • f a + b₂ • f a

Tactic:
<;>

Goal state after:
case mp.refine_3.refine_1
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
ax : ι →₀ R
hax : ∀ (i : ι), ax i ∈ I
ay : ι →₀ R
hay : ∀ (i : ι), ay i ∈ I
⊢ ∀ (a : ι), 0 • f a = 0

case mp.refine_3.refine_2
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
ax : ι →₀ R
hax : ∀ (i : ι), ax i ∈ I
ay : ι →₀ R
hay : ∀ (i : ι), ay i ∈ I
⊢ ∀ (a : ι) (b₁ b₂ : R), (b₁ + b₂) • f a = b₁ • f a + b₂ • f a
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : gcd x y = 0
⊢ x ∣ x * y / 0

Tactic:
div_zero

Goal state after:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : gcd x y = 0
⊢ x ∣ 0
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case mp.refine_3.refine_1
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
ax : ι →₀ R
hax : ∀ (i : ι), ax i ∈ I
ay : ι →₀ R
hay : ∀ (i : ι), ay i ∈ I
a✝ : ι
⊢ 0 • f a✝ = 0

pp: case mp.refine_3.refine_2
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
ax : ι →₀ R
hax : ∀ (i : ι), ax i ∈ I
ay : ι →₀ R
hay : ∀ (i : ι), ay i ∈ I
a✝ : ι
b₁✝ b₂✝ : R
⊢ (b₁✝ + b₂✝) • f a✝ = b₁✝ • f a✝ + b₂✝ • f a✝

Tactic:
<;>

Goal state after:
case mp.refine_3.refine_1
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
ax : ι →₀ R
hax : ∀ (i : ι), ax i ∈ I
ay : ι →₀ R
hay : ∀ (i : ι), ay i ∈ I
a✝ : ι
⊢ 0 • f a✝ = 0

case mp.refine_3.refine_2
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
ax : ι →₀ R
hax : ∀ (i : ι), ax i ∈ I
ay : ι →₀ R
hay : ∀ (i : ι), ay i ∈ I
a✝ : ι
b₁✝ b₂✝ : R
⊢ (b₁✝ + b₂✝) • f a✝ = b₁✝ • f a✝ + b₂✝ • f a✝
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case succ
R : Type u
S : Type v
F : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
K : Ideal S
n : ℕ
n_ih : comap f K ^ n ≤ comap f (K ^ n)
⊢ comap f K ^ (n + 1) ≤ comap f (K ^ (n + 1))

Tactic:
| succ n n_ih =>

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

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : gcd x y = 0
⊢ y ∣ x * y / 0

Tactic:
div_zero

Goal state after:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : gcd x y = 0
⊢ y ∣ 0
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
f : R →+* S
p : Ideal R
inst✝ : p.IsPrime
⊢ comap f (map f p) = p ↔ ∃ q, q.IsPrime ∧ comap f q = p

Tactic:
by
  refine ⟨fun hp ↦ ?_, ?_⟩
  · obtain ⟨q, hq₁, hq₂, hq₃⟩ := Ideal.exists_le_prime_disjoint _ _
      (disjoint_map_primeCompl_iff_comap_le.mpr hp.le)
    exact ⟨q, hq₁, le_antisymm (disjoint_map_primeCompl_iff_comap_le.mp hq₃)
      (map_le_iff_le_comap.mp hq₂)⟩
  · rintro ⟨q, hq, rfl⟩
    simp

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

Goal state before:
pp: case pos
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : gcd x y = 0
⊢ x * y / 0 ∣ z

Tactic:
div_zero

Goal state after:
case pos
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : gcd x y = 0
⊢ 0 ∣ z
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case mp.refine_4
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
c : R
a : ι →₀ R
ha : ∀ (i : ι), a i ∈ I
⊢ (a.sum fun i a ↦ (c * a) • f i) = a.sum fun a b ↦ c • b • f a

pp: case mp.refine_4
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
c : R
a : ι →₀ R
ha : ∀ (i : ι), a i ∈ I
⊢ ∀ (i : ι), 0 • f i = 0

Tactic:
<;>

Goal state after:
case mp.refine_4
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
c : R
a : ι →₀ R
ha : ∀ (i : ι), a i ∈ I
⊢ (a.sum fun i a ↦ (c * a) • f i) = a.sum fun a b ↦ c • b • f a

case mp.refine_4
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
c : R
a : ι →₀ R
ha : ∀ (i : ι), a i ∈ I
⊢ ∀ (i : ι), 0 • f i = 0
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case mp.refine_4
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
c : R
a : ι →₀ R
ha : ∀ (i : ι), a i ∈ I
⊢ (a.sum fun i a ↦ (c * a) • f i) = a.sum fun a b ↦ c • b • f a

pp: case mp.refine_4
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
c : R
a : ι →₀ R
ha : ∀ (i : ι), a i ∈ I
i✝ : ι
⊢ 0 • f i✝ = 0

Tactic:
<;>

Goal state after:
case mp.refine_4
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
c : R
a : ι →₀ R
ha : ∀ (i : ι), a i ∈ I
⊢ (a.sum fun i a ↦ (c * a) • f i) = a.sum fun a b ↦ c • b • f a

case mp.refine_4
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
c : R
a : ι →₀ R
ha : ∀ (i : ι), a i ∈ I
i✝ : ι
⊢ 0 • f i✝ = 0
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_4
inst✝ : Nonempty ι
r : R
⊢ (∀ (m : ι →₀ M), r • m = 0) → ∀ (m : M), r • m = 0

pp: case mpr
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_4
inst✝ : Nonempty ι
r : R
⊢ (∀ (m : M), r • m = 0) → ∀ (m : ι →₀ M), r • m = 0

Tactic:
<;>

Goal state after:
case mp
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_4
inst✝ : Nonempty ι
r : R
⊢ (∀ (m : ι →₀ M), r • m = 0) → ∀ (m : M), r • m = 0

case mpr
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_4
inst✝ : Nonempty ι
r : R
⊢ (∀ (m : M), r • m = 0) → ∀ (m : ι →₀ M), r • m = 0
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case mp
R : Type u_1
inst✝² : Semiring R
ι : Type u_4
M : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
r : R
⊢ (∀ (m : Π₀ (i : ι), M i), r • m = 0) → ∀ (i : ι) (m : M i), r • m = 0

pp: case mpr
R : Type u_1
inst✝² : Semiring R
ι : Type u_4
M : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
r : R
⊢ (∀ (i : ι) (m : M i), r • m = 0) → ∀ (m : Π₀ (i : ι), M i), r • m = 0

Tactic:
<;>

Goal state after:
case mp
R : Type u_1
inst✝² : Semiring R
ι : Type u_4
M : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
r : R
⊢ (∀ (m : Π₀ (i : ι), M i), r • m = 0) → ∀ (i : ι) (m : M i), r • m = 0

case mpr
R : Type u_1
inst✝² : Semiring R
ι : Type u_4
M : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
r : R
⊢ (∀ (i : ι) (m : M i), r • m = 0) → ∀ (m : Π₀ (i : ι), M i), r • m = 0
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case mp
R : Type u_1
inst✝² : Semiring R
ι : Type u_4
M : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
r : R
⊢ (∀ (m : (i : ι) → M i), r • m = 0) → ∀ (i : ι) (m : M i), r • m = 0

pp: case mpr
R : Type u_1
inst✝² : Semiring R
ι : Type u_4
M : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
r : R
⊢ (∀ (i : ι) (m : M i), r • m = 0) → ∀ (m : (i : ι) → M i), r • m = 0

Tactic:
<;>

Goal state after:
case mp
R : Type u_1
inst✝² : Semiring R
ι : Type u_4
M : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
r : R
⊢ (∀ (m : (i : ι) → M i), r • m = 0) → ∀ (i : ι) (m : M i), r • m = 0

case mpr
R : Type u_1
inst✝² : Semiring R
ι : Type u_4
M : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
r : R
⊢ (∀ (i : ι) (m : M i), r • m = 0) → ∀ (m : (i : ι) → M i), r • m = 0
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
a b c : R
ha : a ≠ 0
hcb : c ∣ b
⊢ a * b / (a * c) = b / c

Tactic:
by_cases hc : c = 0

Goal state after:
case pos
R : Type u
inst✝ : EuclideanDomain R
a b c : R
ha : a ≠ 0
hcb : c ∣ b
hc : c = 0
⊢ a * b / (a * c) = b / c

case neg
R : Type u
inst✝ : EuclideanDomain R
a b c : R
ha : a ≠ 0
hcb : c ∣ b
hc : ¬c = 0
⊢ a * b / (a * c) = b / c
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: case neg.refine_1
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∃ x, x ∈ s ∧ x ≠ 0
f : {a : α} → a ∈ s → α
hf : ∀ {a : α} (h : a ∈ s), a = s.gcd * f h
⊢ s = map (fun x ↦ s.gcd * x) (pmap f s ⋯)

pp: case neg.refine_2
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∃ x, x ∈ s ∧ x ≠ 0
f : {a : α} → a ∈ s → α
hf : ∀ {a : α} (h : a ∈ s), a = s.gcd * f h
⊢ s = map (fun x ↦ s.gcd * x) (pmap f s ⋯)

Tactic:
<;>

Goal state after:
case neg.refine_1
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∃ x, x ∈ s ∧ x ≠ 0
f : {a : α} → a ∈ s → α
hf : ∀ {a : α} (h : a ∈ s), a = s.gcd * f h
⊢ s = map (fun x ↦ s.gcd * x) (pmap f s ⋯)

case neg.refine_2
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∃ x, x ∈ s ∧ x ≠ 0
f : {a : α} → a ∈ s → α
hf : ∀ {a : α} (h : a ∈ s), a = s.gcd * f h
⊢ s = map (fun x ↦ s.gcd * x) (pmap f s ⋯)
Module: Mathlib.Algebra.GCDMonoid.Nat

Goal state before:
pp: case inl
a b : ℤ
hna : a ≠ 0
hnb : b ≠ 0
ha : a < 0
⊢ (if 0 ≤ a * b then 1 else -1) = (if 0 ≤ a then 1 else -1) * if 0 ≤ b then 1 else -1

pp: case inr
a b : ℤ
hna : a ≠ 0
hnb : b ≠ 0
ha : 0 < a
⊢ (if 0 ≤ a * b then 1 else -1) = (if 0 ≤ a then 1 else -1) * if 0 ≤ b then 1 else -1

Tactic:
<;>

Goal state after:
case inl
a b : ℤ
hna : a ≠ 0
hnb : b ≠ 0
ha : a < 0
⊢ (if 0 ≤ a * b then 1 else -1) = (if 0 ≤ a then 1 else -1) * if 0 ≤ b then 1 else -1

case inr
a b : ℤ
hna : a ≠ 0
hnb : b ≠ 0
ha : 0 < a
⊢ (if 0 ≤ a * b then 1 else -1) = (if 0 ≤ a then 1 else -1) * if 0 ≤ b then 1 else -1
Module: Mathlib.Algebra.GCDMonoid.Nat

Goal state before:
pp: case inl
a b : ℤ
hna : a ≠ 0
hnb : b ≠ 0
ha : a < 0
⊢ (if 0 ≤ a * b then 1 else -1) = (if 0 ≤ a then 1 else -1) * if 0 ≤ b then 1 else -1

Tactic:
rcases hnb.lt_or_gt with hb | hb

Goal state after:
case inl.inl
a b : ℤ
hna : a ≠ 0
hnb : b ≠ 0
ha : a < 0
hb : b < 0
⊢ (if 0 ≤ a * b then 1 else -1) = (if 0 ≤ a then 1 else -1) * if 0 ≤ b then 1 else -1

case inl.inr
a b : ℤ
hna : a ≠ 0
hnb : b ≠ 0
ha : a < 0
hb : 0 < b
⊢ (if 0 ≤ a * b then 1 else -1) = (if 0 ≤ a then 1 else -1) * if 0 ≤ b then 1 else -1
Module: Mathlib.Algebra.GCDMonoid.Nat

Goal state before:
pp: case inr
a b : ℤ
hna : a ≠ 0
hnb : b ≠ 0
ha : 0 < a
⊢ (if 0 ≤ a * b then 1 else -1) = (if 0 ≤ a then 1 else -1) * if 0 ≤ b then 1 else -1

Tactic:
rcases hnb.lt_or_gt with hb | hb

Goal state after:
case inr.inl
a b : ℤ
hna : a ≠ 0
hnb : b ≠ 0
ha : 0 < a
hb : b < 0
⊢ (if 0 ≤ a * b then 1 else -1) = (if 0 ≤ a then 1 else -1) * if 0 ≤ b then 1 else -1

case inr.inr
a b : ℤ
hna : a ≠ 0
hnb : b ≠ 0
ha : 0 < a
hb : 0 < b
⊢ (if 0 ≤ a * b then 1 else -1) = (if 0 ≤ a then 1 else -1) * if 0 ≤ b then 1 else -1
Module: Mathlib.Algebra.GCDMonoid.Nat

Goal state before:
pp: case inl.inl
a b : ℤ
hna : a ≠ 0
hnb : b ≠ 0
ha : a < 0
hb : b < 0
⊢ (if 0 ≤ a * b then 1 else -1) = (if 0 ≤ a then 1 else -1) * if 0 ≤ b then 1 else -1

pp: case inl.inr
a b : ℤ
hna : a ≠ 0
hnb : b ≠ 0
ha : a < 0
hb : 0 < b
⊢ (if 0 ≤ a * b then 1 else -1) = (if 0 ≤ a then 1 else -1) * if 0 ≤ b then 1 else -1

pp: case inr.inl
a b : ℤ
hna : a ≠ 0
hnb : b ≠ 0
ha : 0 < a
hb : b < 0
⊢ (if 0 ≤ a * b then 1 else -1) = (if 0 ≤ a then 1 else -1) * if 0 ≤ b then 1 else -1

pp: case inr.inr
a b : ℤ
hna : a ≠ 0
hnb : b ≠ 0
ha : 0 < a
hb : 0 < b
⊢ (if 0 ≤ a * b then 1 else -1) = (if 0 ≤ a then 1 else -1) * if 0 ≤ b then 1 else -1

Tactic:
<;>

Goal state after:
case inl.inl
a b : ℤ
hna : a ≠ 0
hnb : b ≠ 0
ha : a < 0
hb : b < 0
⊢ (if 0 ≤ a * b then 1 else -1) = (if 0 ≤ a then 1 else -1) * if 0 ≤ b then 1 else -1

case inl.inr
a b : ℤ
hna : a ≠ 0
hnb : b ≠ 0
ha : a < 0
hb : 0 < b
⊢ (if 0 ≤ a * b then 1 else -1) = (if 0 ≤ a then 1 else -1) * if 0 ≤ b then 1 else -1

case inr.inl
a b : ℤ
hna : a ≠ 0
hnb : b ≠ 0
ha : 0 < a
hb : b < 0
⊢ (if 0 ≤ a * b then 1 else -1) = (if 0 ≤ a then 1 else -1) * if 0 ≤ b then 1 else -1

case inr.inr
a b : ℤ
hna : a ≠ 0
hnb : b ≠ 0
ha : 0 < a
hb : 0 < b
⊢ (if 0 ≤ a * b then 1 else -1) = (if 0 ≤ a then 1 else -1) * if 0 ≤ b then 1 else -1
Module: Mathlib.Algebra.GCDMonoid.Nat

Goal state before:
pp: case inl
z : ℤ
h✝ : 0 ≤ z
⊢ |z| = normalize z

pp: case inr
z : ℤ
h✝ : z ≤ 0
⊢ |z| = normalize z

Tactic:
<;>

Goal state after:
case inl
z : ℤ
h✝ : 0 ≤ z
⊢ |z| = normalize z

case inr
z : ℤ
h✝ : z ≤ 0
⊢ |z| = normalize z
Module: Mathlib.Algebra.GCDMonoid.Nat

Goal state before:
pp: case refine_1
⊢ Function.LeftInverse (fun x ↦ Associates.mk ↑x) fun x ↦ x.out.natAbs

Tactic:
refine Associates.forall_associated.2 fun a ↦ ?_

Goal state after:
case refine_1
a : ℤ
⊢ (fun x ↦ Associates.mk ↑x) ((fun x ↦ x.out.natAbs) (Associates.mk a)) = Associates.mk a
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: case neg
α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidableEq β
b : β
h : b ∉ s
⊢ (insert b s).lcm f = GCDMonoid.lcm (f b) (s.lcm f)

Tactic:
apply fold_insert h

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: case empty
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
f : β → α
inst✝ : DecidableEq β
g : γ → β
⊢ (image g ∅).lcm f = ∅.lcm (f ∘ g)

pp: case insert
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
f : β → α
inst✝ : DecidableEq β
g : γ → β
a✝² : γ
s✝ : Finset γ
a✝¹ : a✝² ∉ s✝
a✝ : (image g s✝).lcm f = s✝.lcm (f ∘ g)
⊢ (image g (insert a✝² s✝)).lcm f = (insert a✝² s✝).lcm (f ∘ g)

Tactic:
<;>

Goal state after:
case empty
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
f : β → α
inst✝ : DecidableEq β
g : γ → β
⊢ (image g ∅).lcm f = ∅.lcm (f ∘ g)

case insert
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
f : β → α
inst✝ : DecidableEq β
g : γ → β
a✝² : γ
s✝ : Finset γ
a✝¹ : a✝² ∉ s✝
a✝ : (image g s✝).lcm f = s✝.lcm (f ∘ g)
⊢ (image g (insert a✝² s✝)).lcm f = (insert a✝² s✝).lcm (f ∘ g)
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x y : R
I J : Ideal R
⊢ span {x} * I ≤ span {y} * J ↔ ∀ zI ∈ I, ∃ zJ ∈ J, x * zI = y * zJ

Tactic:
by
  simp only [span_singleton_mul_le_iff, mem_span_singleton_mul, eq_comm]

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: case neg
α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidableEq β
b : β
h : b ∉ s
⊢ (insert b s).gcd f = GCDMonoid.gcd (f b) (s.gcd f)

Tactic:
apply fold_insert h

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: case empty
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
f : β → α
inst✝ : DecidableEq β
g : γ → β
⊢ (image g ∅).gcd f = ∅.gcd (f ∘ g)

pp: case insert
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
f : β → α
inst✝ : DecidableEq β
g : γ → β
a✝² : γ
s✝ : Finset γ
a✝¹ : a✝² ∉ s✝
a✝ : (image g s✝).gcd f = s✝.gcd (f ∘ g)
⊢ (image g (insert a✝² s✝)).gcd f = (insert a✝² s✝).gcd (f ∘ g)

Tactic:
<;>

Goal state after:
case empty
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
f : β → α
inst✝ : DecidableEq β
g : γ → β
⊢ (image g ∅).gcd f = ∅.gcd (f ∘ g)

case insert
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
f : β → α
inst✝ : DecidableEq β
g : γ → β
a✝² : γ
s✝ : Finset γ
a✝¹ : a✝² ∉ s✝
a✝ : (image g s✝).gcd f = s✝.gcd (f ∘ g)
⊢ (image g (insert a✝² s✝)).gcd f = (insert a✝² s✝).gcd (f ∘ g)
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: case pos
α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s✝ : Finset β
f : β → α
inst✝ : DecidablePred fun x ↦ f x = 0
a : β
s : Finset β
a✝ : a ∉ s
h : {x ∈ s | f x = 0}.gcd f = 0
h1 : f a = 0
⊢ (insert a ({x ∈ s | f x = 0})).gcd f = 0

pp: case neg
α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s✝ : Finset β
f : β → α
inst✝ : DecidablePred fun x ↦ f x = 0
a : β
s : Finset β
a✝ : a ∉ s
h : {x ∈ s | f x = 0}.gcd f = 0
h1 : ¬f a = 0
⊢ {x ∈ s | f x = 0}.gcd f = 0

Tactic:
<;>

Goal state after:
case pos
α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s✝ : Finset β
f : β → α
inst✝ : DecidablePred fun x ↦ f x = 0
a : β
s : Finset β
a✝ : a ∉ s
h : {x ∈ s | f x = 0}.gcd f = 0
h1 : f a = 0
⊢ (insert a ({x ∈ s | f x = 0})).gcd f = 0

case neg
α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s✝ : Finset β
f : β → α
inst✝ : DecidablePred fun x ↦ f x = 0
a : β
s : Finset β
a✝ : a ∉ s
h : {x ∈ s | f x = 0}.gcd f = 0
h1 : ¬f a = 0
⊢ {x ∈ s | f x = 0}.gcd f = 0
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case e'_2
α✝ : Type u_1
α : Type u_2
inst✝¹ : MonoidWithZero α
inst✝ : IsLeftCancelMulZero α
out : Associates α → α
mk_out : ∀ (a : Associates α), Associates.mk (out a) = a
out_one : out 1 = 1
assoc : ∀ (a : α), Associated a (out (Associates.mk a))
this : (p : Prop) → Decidable p := Classical.dec
a✝ : Nontrivial α
⊢ 1 * ↑(Exists.choose ⋯) = ↑(if 1 = 0 then 1 else Exists.choose ⋯)

pp: case e'_3
α✝ : Type u_1
α : Type u_2
inst✝¹ : MonoidWithZero α
inst✝ : IsLeftCancelMulZero α
out : Associates α → α
mk_out : ∀ (a : Associates α), Associates.mk (out a) = a
out_one : out 1 = 1
assoc : ∀ (a : α), Associated a (out (Associates.mk a))
this : (p : Prop) → Decidable p := Classical.dec
a✝ : Nontrivial α
⊢ out (Associates.mk 1) = ↑1

Tactic:
<;>

Goal state after:
case e'_2
α✝ : Type u_1
α : Type u_2
inst✝¹ : MonoidWithZero α
inst✝ : IsLeftCancelMulZero α
out : Associates α → α
mk_out : ∀ (a : Associates α), Associates.mk (out a) = a
out_one : out 1 = 1
assoc : ∀ (a : α), Associated a (out (Associates.mk a))
this : (p : Prop) → Decidable p := Classical.dec
a✝ : Nontrivial α
⊢ 1 * ↑(Exists.choose ⋯) = ↑(if 1 = 0 then 1 else Exists.choose ⋯)

case e'_3
α✝ : Type u_1
α : Type u_2
inst✝¹ : MonoidWithZero α
inst✝ : IsLeftCancelMulZero α
out : Associates α → α
mk_out : ∀ (a : Associates α), Associates.mk (out a) = a
out_one : out 1 = 1
assoc : ∀ (a : α), Associated a (out (Associates.mk a))
this : (p : Prop) → Decidable p := Classical.dec
a✝ : Nontrivial α
⊢ out (Associates.mk 1) = ↑1
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case pos
α✝ : Type u_1
α : Type u_2
inst✝¹ : MonoidWithZero α
inst✝ : IsLeftCancelMulZero α
x✝ : Associates α
h : x✝ = 1
⊢ Associates.mk 1 = x✝

pp: case neg
α✝ : Type u_1
α : Type u_2
inst✝¹ : MonoidWithZero α
inst✝ : IsLeftCancelMulZero α
x✝ : Associates α
h : ¬x✝ = 1
⊢ Associates.mk (Quotient.out x✝) = x✝

Tactic:
<;>

Goal state after:
case pos
α✝ : Type u_1
α : Type u_2
inst✝¹ : MonoidWithZero α
inst✝ : IsLeftCancelMulZero α
x✝ : Associates α
h : x✝ = 1
⊢ Associates.mk 1 = x✝

case neg
α✝ : Type u_1
α : Type u_2
inst✝¹ : MonoidWithZero α
inst✝ : IsLeftCancelMulZero α
x✝ : Associates α
h : ¬x✝ = 1
⊢ Associates.mk (Quotient.out x✝) = x✝
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case e'_2
α : Type u_1
inst✝¹ : MonoidWithZero α
inst✝ : NormalizationMonoid α
u : αˣ
a✝ : Nontrivial α
⊢ normUnit ↑u = normUnit (1 * ↑u)

pp: case e'_3
α : Type u_1
inst✝¹ : MonoidWithZero α
inst✝ : NormalizationMonoid α
u : αˣ
a✝ : Nontrivial α
⊢ u⁻¹ = u⁻¹ * normUnit 1

Tactic:
<;>

Goal state after:
case e'_2
α : Type u_1
inst✝¹ : MonoidWithZero α
inst✝ : NormalizationMonoid α
u : αˣ
a✝ : Nontrivial α
⊢ normUnit ↑u = normUnit (1 * ↑u)

case e'_3
α : Type u_1
inst✝¹ : MonoidWithZero α
inst✝ : NormalizationMonoid α
u : αˣ
a✝ : Nontrivial α
⊢ u⁻¹ = u⁻¹ * normUnit 1
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case a
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
x✝ : a = 0 ∧ b = 0
ha : a = 0
hb : b = 0
⊢ 0 ∣ 0

pp: case a
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
x✝ : a = 0 ∧ b = 0
ha : a = 0
hb : b = 0
⊢ 0 ∣ 0

Tactic:
<;>

Goal state after:
case a
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
x✝ : a = 0 ∧ b = 0
ha : a = 0
hb : b = 0
⊢ 0 ∣ 0

case a
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
x✝ : a = 0 ∧ b = 0
ha : a = 0
hb : b = 0
⊢ 0 ∣ 0
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case a
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
k m n m' n' : α
hm' : m' ∣ m
hn' : n' ∣ n
h : gcd k (m * n) = m' * n'
hm'n' : m' * n' ∣ k
⊢ m' ∣ gcd k m

pp: case a
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
k m n m' n' : α
hm' : m' ∣ m
hn' : n' ∣ n
h : gcd k (m * n) = m' * n'
hm'n' : m' * n' ∣ k
⊢ n' ∣ gcd k n

Tactic:
· have hm'k : m' ∣ k := (dvd_mul_right m' n').trans hm'n'
    exact dvd_gcd hm'k hm'

Goal state after:
case a
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
k m n m' n' : α
hm' : m' ∣ m
hn' : n' ∣ n
h : gcd k (m * n) = m' * n'
hm'n' : m' * n' ∣ k
⊢ n' ∣ gcd k n