mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
⊢ s.gcd = 0 → ∀ (x : α), x ∈ s → x = 0

pp: case mpr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
⊢ (∀ (x : α), x ∈ s → x = 0) → s.gcd = 0

Tactic:
·

Goal state after:
case mp
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
⊢ s.gcd = 0 → ∀ (x : α), x ∈ s → x = 0
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: case mpr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
⊢ (∀ (x : α), x ∈ s → x = 0) → s.gcd = 0

Tactic:
·

Goal state after:
case mpr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
⊢ (∀ (x : α), x ∈ s → x = 0) → s.gcd = 0
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: case mpr.refine_1
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
⊢ (∀ (x : α), x ∈ 0 → x = 0) → gcd 0 = 0

pp: case mpr.refine_2
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
⊢ ∀ (a : α) (s : Multiset α),
    ((∀ (x : α), x ∈ s → x = 0) → s.gcd = 0) → (∀ (x : α), x ∈ a ::ₘ s → x = 0) → (a ::ₘ s).gcd = 0

Tactic:
·

Goal state after:
case mpr.refine_1
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
⊢ (∀ (x : α), x ∈ 0 → x = 0) → gcd 0 = 0
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
⊢ s.gcd = 0 ↔ ∀ (x : α), x ∈ s → x = 0

Tactic:
by
  constructor
  · intro h x hx
    apply eq_zero_of_zero_dvd
    rw [← h]
    apply gcd_dvd hx
  · refine s.induction_on ?_ ?_
    · simp
    intro a s sgcd h
    simp [h a (mem_cons_self a s), sgcd fun x hx ↦ h x (mem_cons_of_mem hx)]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ⇑f
h : ∀ J ∈ A, RingHom.ker f ≤ J
⊢ ∀ b ∈ map f '' A, map f (sInf A) ≤ b

pp: case refine_2
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ⇑f
h : ∀ J ∈ A, RingHom.ker f ≤ J
⊢ sInf (map f '' A) ≤ map f (sInf A)

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ⇑f
h : ∀ J ∈ A, RingHom.ker f ≤ J
⊢ ∀ b ∈ map f '' A, map f (sInf A) ≤ b
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: case refine_1
α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizedGCDMonoid α
a : α
s : Multiset α
⊢ (map (fun x ↦ a * x) 0).gcd = normalize a * gcd 0

pp: case refine_2
α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizedGCDMonoid α
a : α
s✝ : Multiset α
b : α
s : Multiset α
ih : (map (fun x ↦ a * x) s).gcd = normalize a * s.gcd
⊢ (map (fun x ↦ a * x) (b ::ₘ s)).gcd = normalize a * (b ::ₘ s).gcd

Tactic:
·

Goal state after:
case refine_1
α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizedGCDMonoid α
a : α
s : Multiset α
⊢ (map (fun x ↦ a * x) 0).gcd = normalize a * gcd 0
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: case refine_2
α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizedGCDMonoid α
a : α
s✝ : Multiset α
b : α
s : Multiset α
ih : (map (fun x ↦ a * x) s).gcd = normalize a * s.gcd
⊢ (map (fun x ↦ a * x) (b ::ₘ s)).gcd = normalize a * (b ::ₘ s).gcd

Tactic:
·

Goal state after:
case refine_2
α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizedGCDMonoid α
a : α
s✝ : Multiset α
b : α
s : Multiset α
ih : (map (fun x ↦ a * x) s).gcd = normalize a * s.gcd
⊢ (map (fun x ↦ a * x) (b ::ₘ s)).gcd = normalize a * (b ::ₘ s).gcd
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ⇑f
h : ∀ J ∈ A, RingHom.ker f ≤ J
⊢ sInf (map f '' A) ≤ map f (sInf A)

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ⇑f
h : ∀ J ∈ A, RingHom.ker f ≤ J
⊢ sInf (map f '' A) ≤ map f (sInf A)
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a : α
s : Multiset α
⊢ Associated (map (fun x ↦ a * x) 0).gcd (a * gcd 0)

pp: case refine_2
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a : α
s✝ : Multiset α
b : α
s : Multiset α
ih : Associated (map (fun x ↦ a * x) s).gcd (a * s.gcd)
⊢ Associated (map (fun x ↦ a * x) (b ::ₘ s)).gcd (a * (b ::ₘ s).gcd)

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a : α
s : Multiset α
⊢ Associated (map (fun x ↦ a * x) 0).gcd (a * gcd 0)
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a : α
s✝ : Multiset α
b : α
s : Multiset α
ih : Associated (map (fun x ↦ a * x) s).gcd (a * s.gcd)
⊢ Associated (map (fun x ↦ a * x) (b ::ₘ s)).gcd (a * (b ::ₘ s).gcd)

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a : α
s✝ : Multiset α
b : α
s : Multiset α
ih : Associated (map (fun x ↦ a * x) s).gcd (a * s.gcd)
⊢ Associated (map (fun x ↦ a * x) (b ::ₘ s)).gcd (a * (b ::ₘ s).gcd)
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : s.dedup.gcd = s.gcd
h : ¬a ∈ s
⊢ (a ::ₘ s).dedup.gcd = (a ::ₘ s).gcd

pp: case pos
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : s.dedup.gcd = s.gcd
h : a ∈ s
⊢ (a ::ₘ s).dedup.gcd = (a ::ₘ s).gcd

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : s.dedup.gcd = s.gcd
h : ¬a ∈ s
⊢ (a ::ₘ s).dedup.gcd = (a ::ₘ s).gcd
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
I : Ideal R
H : I.IsPrime
hk : RingHom.ker f ≤ I
h : map f I = ⊤
⊢ ⊤ ≤ I

pp: case refine_2
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
I : Ideal R
H : I.IsPrime
hk : RingHom.ker f ≤ I
x y : S
⊢ x * y ∈ map f I → x ∈ map f I ∨ y ∈ map f I

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
I : Ideal R
H : I.IsPrime
hk : RingHom.ker f ≤ I
h : map f I = ⊤
⊢ ⊤ ≤ I
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
I : Ideal R
H : I.IsPrime
hk : RingHom.ker f ≤ I
x y : S
⊢ x * y ∈ map f I → x ∈ map f I ∨ y ∈ map f I

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
I : Ideal R
H : I.IsPrime
hk : RingHom.ker f ≤ I
x y : S
⊢ x * y ∈ map f I → x ∈ map f I ∨ y ∈ map f I
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s t : Multiset α
hs : ∃ x, x ∈ s ∧ x ≠ 0
ht : s = map (fun x ↦ s.gcd * x) t
⊢ Associated (s.gcd * 1) (s.gcd * t.gcd)

pp: case refine_2
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s t : Multiset α
hs : ∃ x, x ∈ s ∧ x ≠ 0
ht : s = map (fun x ↦ s.gcd * x) t
⊢ s.gcd ≠ 0

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s t : Multiset α
hs : ∃ x, x ∈ s ∧ x ≠ 0
ht : s = map (fun x ↦ s.gcd * x) t
⊢ Associated (s.gcd * 1) (s.gcd * t.gcd)
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∀ (x : α), x ∈ s → x = 0
⊢ ∃ t, s = map (fun x ↦ s.gcd * x) t ∧ t.gcd = 1

pp: case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∃ x, x ∈ s ∧ x ≠ 0
⊢ ∃ t, s = map (fun x ↦ s.gcd * x) t ∧ t.gcd = 1

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∀ (x : α), x ∈ s → x = 0
⊢ ∃ t, s = map (fun x ↦ s.gcd * x) t ∧ t.gcd = 1
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case succ.inl
R : Type u
inst✝¹ : Semiring R
I J : Ideal R
inst✝ : J.IsTwoSided
h : I ⊔ J = ⊤
ih : I ⊔ J ^ 0 = ⊤
⊢ I ⊔ J ^ (0 + 1) = ⊤

pp: case succ.inr
R : Type u
inst✝¹ : Semiring R
I J : Ideal R
inst✝ : J.IsTwoSided
h : I ⊔ J = ⊤
n : ℕ
ih : I ⊔ J ^ n = ⊤
hn : n ≠ 0
⊢ I ⊔ J ^ (n + 1) = ⊤

Tactic:
·

Goal state after:
case succ.inl
R : Type u
inst✝¹ : Semiring R
I J : Ideal R
inst✝ : J.IsTwoSided
h : I ⊔ J = ⊤
ih : I ⊔ J ^ 0 = ⊤
⊢ I ⊔ J ^ (0 + 1) = ⊤
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∃ x, x ∈ s ∧ x ≠ 0
⊢ ∃ t, s = map (fun x ↦ s.gcd * x) t ∧ t.gcd = 1

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∃ x, x ∈ s ∧ x ≠ 0
⊢ ∃ t, s = map (fun x ↦ s.gcd * x) t ∧ t.gcd = 1
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 ⋯)

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 ⋯)
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
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_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.RingTheory.Ideal.Operations

Goal state before:
pp: case inl
R : Type u
inst✝ : Semiring R
I : Ideal R
n : ℕ
h : I = ⊤
⊢ I ^ n = ⊤

pp: case inr
R : Type u
inst✝ : Semiring R
I : Ideal R
n : ℕ
h : n = 0
⊢ I ^ n = ⊤

Tactic:
·

Goal state after:
case inl
R : Type u
inst✝ : Semiring R
I : Ideal R
n : ℕ
h : I = ⊤
⊢ I ^ n = ⊤
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case inr
R : Type u
inst✝ : Semiring R
I : Ideal R
n : ℕ
h : n = 0
⊢ I ^ n = ⊤

Tactic:
·

Goal state after:
case inr
R : Type u
inst✝ : Semiring R
I : Ideal R
n : ℕ
h : n = 0
⊢ I ^ n = ⊤
Module: Mathlib.Algebra.GCDMonoid.Nat

Goal state before:
pp: case inl
h : 0 ≤ 0
⊢ normalize 0 = -0

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

Tactic:
·

Goal state after:
case inl
h : 0 ≤ 0
⊢ normalize 0 = -0
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case succ.zero
R : Type u
inst✝ : Semiring R
ih : 0 ≠ 0 → ↑0 = ⊤
hn : 0 + 1 ≠ 0
⊢ ↑(0 + 1) = ⊤

pp: case succ.succ
R : Type u
inst✝ : Semiring R
n : ℕ
ih : n + 1 ≠ 0 → ↑(n + 1) = ⊤
hn : n + 1 + 1 ≠ 0
⊢ ↑(n + 1 + 1) = ⊤

Tactic:
·

Goal state after:
case succ.zero
R : Type u
inst✝ : Semiring R
ih : 0 ≠ 0 → ↑0 = ⊤
hn : 0 + 1 ≠ 0
⊢ ↑(0 + 1) = ⊤
Module: Mathlib.Algebra.GCDMonoid.Nat

Goal state before:
pp: case inr
z : ℤ
h✝ : z ≤ 0
h : z < 0
⊢ normalize z = -z

Tactic:
·

Goal state after:
case inr
z : ℤ
h✝ : z ≤ 0
h : z < 0
⊢ normalize z = -z
Module: Mathlib.Algebra.GCDMonoid.Nat

Goal state before:
pp: case pos
z : ℤ
hz : normalize z = z
h : 0 ≤ z
⊢ 0 ≤ z

pp: case neg
z : ℤ
hz : normalize z = z
h : z < 0
⊢ 0 ≤ z

Tactic:
·

Goal state after:
case pos
z : ℤ
hz : normalize z = z
h : 0 ≤ z
⊢ 0 ≤ z
Module: Mathlib.Algebra.GCDMonoid.Nat

Goal state before:
pp: case neg
z : ℤ
hz : normalize z = z
h : z < 0
⊢ 0 ≤ z

Tactic:
·

Goal state after:
case neg
z : ℤ
hz : normalize z = z
h : z < 0
⊢ 0 ≤ z
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case mp
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal R
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsPrime}, RingHom.ker f ≤ J
j : Ideal S
⊢ j ∈ {J | map f I ≤ J ∧ J.IsPrime} → j ∈ map f '' {J | I ≤ J ∧ J.IsPrime}

pp: case mpr
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal R
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsPrime}, RingHom.ker f ≤ J
j : Ideal S
⊢ j ∈ map f '' {J | I ≤ J ∧ J.IsPrime} → j ∈ {J | map f I ≤ J ∧ J.IsPrime}

Tactic:
·

Goal state after:
case mp
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal R
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsPrime}, RingHom.ker f ≤ J
j : Ideal S
⊢ j ∈ {J | map f I ≤ J ∧ J.IsPrime} → j ∈ map f '' {J | I ≤ J ∧ J.IsPrime}
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case refine_1
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
s : Finset ι
I : ι → Ideal R
x : ι → R
⊢ (∀ i ∈ ∅, x i ∈ I i) → ∏ i ∈ ∅, x i ∈ ∏ i ∈ ∅, I i

pp: case refine_2
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
s : Finset ι
I : ι → Ideal R
x : ι → R
⊢ ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      ((∀ i ∈ s, x i ∈ I i) → ∏ i ∈ s, x i ∈ ∏ i ∈ s, I i) →
        (∀ i ∈ insert a s, x i ∈ I i) → ∏ i ∈ insert a s, x i ∈ ∏ i ∈ insert a s, I i

Tactic:
·

Goal state after:
case refine_1
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
s : Finset ι
I : ι → Ideal R
x : ι → R
⊢ (∀ i ∈ ∅, x i ∈ I i) → ∏ i ∈ ∅, x i ∈ ∏ i ∈ ∅, I i
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case refine_2
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
s : Finset ι
I : ι → Ideal R
x : ι → R
⊢ ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      ((∀ i ∈ s, x i ∈ I i) → ∏ i ∈ s, x i ∈ ∏ i ∈ s, I i) →
        (∀ i ∈ insert a s, x i ∈ I i) → ∏ i ∈ insert a s, x i ∈ ∏ i ∈ insert a s, I i

Tactic:
·

Goal state after:
case refine_2
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
s : Finset ι
I : ι → Ideal R
x : ι → R
⊢ ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      ((∀ i ∈ s, x i ∈ I i) → ∏ i ∈ s, x i ∈ ∏ i ∈ s, I i) →
        (∀ i ∈ insert a s, x i ∈ I i) → ∏ i ∈ insert a s, x i ∈ ∏ i ∈ insert a s, I i
Module: Mathlib.Algebra.GCDMonoid.Nat

Goal state before:
pp: case inl
a : ℤ
h : a = ↑a.natAbs
⊢ ∃ u x, ↑a.natAbs = u * a

pp: case inr
a : ℤ
h : a = -↑a.natAbs
⊢ ∃ u x, ↑a.natAbs = u * a

Tactic:
·

Goal state after:
case inl
a : ℤ
h : a = ↑a.natAbs
⊢ ∃ u x, ↑a.natAbs = u * a
Module: Mathlib.Algebra.GCDMonoid.Nat

Goal state before:
pp: case inr
a : ℤ
h : a = -↑a.natAbs
⊢ ∃ u x, ↑a.natAbs = u * a

Tactic:
·

Goal state after:
case inr
a : ℤ
h : a = -↑a.natAbs
⊢ ∃ u x, ↑a.natAbs = u * a
Module: Mathlib.Algebra.GCDMonoid.Nat

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

pp: case refine_2
n : ℕ
⊢ (fun x ↦ x.out.natAbs) ((fun x ↦ Associates.mk ↑x) n) = n

Tactic:
·

Goal state after:
case refine_1
⊢ Function.LeftInverse (fun x ↦ Associates.mk ↑x) fun x ↦ x.out.natAbs
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case mpr
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal R
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsPrime}, RingHom.ker f ≤ J
j : Ideal S
⊢ j ∈ map f '' {J | I ≤ J ∧ J.IsPrime} → j ∈ {J | map f I ≤ J ∧ J.IsPrime}

Tactic:
·

Goal state after:
case mpr
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal R
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsPrime}, RingHom.ker f ≤ J
j : Ideal S
⊢ j ∈ map f '' {J | I ≤ J ∧ J.IsPrime} → j ∈ {J | map f I ≤ J ∧ J.IsPrime}
Module: Mathlib.Algebra.GCDMonoid.Nat

Goal state before:
pp: case refine_2
n : ℕ
⊢ (fun x ↦ x.out.natAbs) ((fun x ↦ Associates.mk ↑x) n) = n

Tactic:
·

Goal state after:
case refine_2
n : ℕ
⊢ (fun x ↦ x.out.natAbs) ((fun x ↦ Associates.mk ↑x) n) = n
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✝ : DecidableEq β
b : β
h : b ∈ s
⊢ (insert b s).lcm f = GCDMonoid.lcm (f b) (s.lcm f)

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

Goal state after:
case pos
α : 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)
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case pos
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
n m i : ℕ
hi : i ∈ Finset.range (n + m + 1)
hn : n ≤ i
⊢ I ^ i * J ^ (n + m - i) * ↑((n + m).choose i) ≤ I ^ n + J ^ m

pp: case neg
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
n m i : ℕ
hi : i ∈ Finset.range (n + m + 1)
hn : ¬n ≤ i
⊢ I ^ i * J ^ (n + m - i) * ↑((n + m).choose i) ≤ I ^ n + J ^ m

Tactic:
·

Goal state after:
case pos
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
n m i : ℕ
hi : i ∈ Finset.range (n + m + 1)
hn : n ≤ i
⊢ I ^ i * J ^ (n + m - i) * ↑((n + m).choose i) ≤ I ^ n + J ^ m
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case neg
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
n m i : ℕ
hi : i ∈ Finset.range (n + m + 1)
hn : ¬n ≤ i
⊢ I ^ i * J ^ (n + m - i) * ↑((n + m).choose i) ≤ I ^ n + J ^ m

Tactic:
·

Goal state after:
case neg
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
n m i : ℕ
hi : i ∈ Finset.range (n + m + 1)
hn : ¬n ≤ i
⊢ I ^ i * J ^ (n + m - i) * ↑((n + m).choose i) ≤ I ^ n + J ^ m
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✝ : DecidableEq β
b : β
h : b ∈ s
⊢ (insert b s).gcd f = GCDMonoid.gcd (f b) (s.gcd f)

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

Goal state after:
case pos
α : 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)
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case mp
R : Type u_2
inst✝ : CommSemiring R
x y : R
⊢ (∃ y_1 ∈ span {x}, ∃ z ∈ span {y}, y_1 + z = 1) → IsCoprime x y

pp: case mpr
R : Type u_2
inst✝ : CommSemiring R
x y : R
⊢ IsCoprime x y → ∃ y_1 ∈ span {x}, ∃ z ∈ span {y}, y_1 + z = 1

Tactic:
·

Goal state after:
case mp
R : Type u_2
inst✝ : CommSemiring R
x y : R
⊢ (∃ y_1 ∈ span {x}, ∃ z ∈ span {y}, y_1 + z = 1) → IsCoprime x y
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidablePred fun x ↦ f x = 0
⊢ s.gcd f = ({x ∈ s | f x = 0} ∪ {x ∈ s | f x ≠ 0}).gcd f

pp: α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidablePred fun x ↦ f x = 0
⊢ ({x ∈ s | f x = 0} ∪ {x ∈ s | f x ≠ 0}).gcd f = {x ∈ s | f x ≠ 0}.gcd f

Tactic:
·

Goal state after:
α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidablePred fun x ↦ f x = 0
⊢ s.gcd f = ({x ∈ s | f x = 0} ∪ {x ∈ s | f x ≠ 0}).gcd f
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case mpr
R : Type u_2
inst✝ : CommSemiring R
x y : R
⊢ IsCoprime x y → ∃ y_1 ∈ span {x}, ∃ z ∈ span {y}, y_1 + z = 1

Tactic:
·

Goal state after:
case mpr
R : Type u_2
inst✝ : CommSemiring R
x y : R
⊢ IsCoprime x y → ∃ y_1 ∈ span {x}, ∃ z ∈ span {y}, y_1 + z = 1
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: case refine_1
α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidablePred fun x ↦ f x = 0
⊢ α

pp: case refine_2
α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidablePred fun x ↦ f x = 0
⊢ GCDMonoid.gcd ({x ∈ s | f x = 0}.gcd f) ({x ∈ s | f x ≠ 0}.gcd f) = GCDMonoid.gcd 0 ?refine_1

pp: case refine_3
α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidablePred fun x ↦ f x = 0
⊢ GCDMonoid.gcd 0 ?refine_1 = {x ∈ s | f x ≠ 0}.gcd f

Tactic:
·

Goal state after:
case refine_1
α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidablePred fun x ↦ f x = 0
⊢ α
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case refine_1
R : Type u
inst✝ : CommSemiring R
s : Multiset (Ideal R)
⊢ Multiset.prod 0 ≤ Multiset.inf 0

pp: case refine_2
R : Type u
inst✝ : CommSemiring R
s : Multiset (Ideal R)
⊢ ∀ (a : Ideal R) (s : Multiset (Ideal R)), s.prod ≤ s.inf → (a ::ₘ s).prod ≤ (a ::ₘ s).inf

Tactic:
·

Goal state after:
case refine_1
R : Type u
inst✝ : CommSemiring R
s : Multiset (Ideal R)
⊢ Multiset.prod 0 ≤ Multiset.inf 0
Module: Mathlib.Algebra.GCDMonoid.Finset

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

pp: case refine_3
α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidablePred fun x ↦ f x = 0
⊢ GCDMonoid.gcd 0 ({x ∈ s | f x ≠ 0}.gcd f) = {x ∈ s | f x ≠ 0}.gcd f

Tactic:
·

Goal state after:
case refine_2
α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidablePred fun x ↦ f x = 0
⊢ GCDMonoid.gcd ({x ∈ s | f x = 0}.gcd f) ({x ∈ s | f x ≠ 0}.gcd f) = GCDMonoid.gcd 0 ({x ∈ s | f x ≠ 0}.gcd f)