mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝¹ : R
x✝ : x✝¹ ∈ ⊤
⊢ x✝¹ • 0 = 0

Tactic:
;

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝¹ : R
x✝ : x✝¹ ∈ ⊤
⊢ x✝¹ • 0 = 0
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
I J K : Ideal R
inst✝ : I.IsTwoSided
h : 1 ∈ I ⊔ J
i : R
hi : i ∈ I ⊔ K
⊢ i ∈ I ⊔ J * K

Tactic:
;

Goal state after:
R : Type u
inst✝¹ : Semiring R
I J K : Ideal R
inst✝ : I.IsTwoSided
h : 1 ∈ I ⊔ J
i : R
hi : i ∈ I ⊔ K
⊢ i ∈ I ⊔ J * K
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
I J K : Ideal R
inst✝ : I.IsTwoSided
i : R
hi : ∃ y ∈ I, ∃ z ∈ K, y + z = i
i1 : R
hi1 : i1 ∈ I
j : R
hj : j ∈ J
h : i1 + j = 1
⊢ ∃ y ∈ I, ∃ z ∈ J * K, y + z = i

Tactic:
;

Goal state after:
R : Type u
inst✝¹ : Semiring R
I J K : Ideal R
inst✝ : I.IsTwoSided
i : R
hi : ∃ y ∈ I, ∃ z ∈ K, y + z = i
i1 : R
hi1 : i1 ∈ I
j : R
hj : j ∈ J
h : i1 + j = 1
⊢ ∃ y ∈ I, ∃ z ∈ J * K, y + z = i
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
I J K : Ideal R
inst✝ : J.IsTwoSided
h : 1 ∈ I ⊔ K
i : R
hi : i ∈ I ⊔ J
⊢ i ∈ I ⊔ J * K

Tactic:
;

Goal state after:
R : Type u
inst✝¹ : Semiring R
I J K : Ideal R
inst✝ : J.IsTwoSided
h : 1 ∈ I ⊔ K
i : R
hi : i ∈ I ⊔ J
⊢ i ∈ I ⊔ J * K
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
I : Ideal R
⊢ (∀ ⦃x : R⦄, x ∈ I → ∀ n ∈ N, x • n = 0) ↔ ∀ r ∈ I, ∀ n ∈ N, r • n ∈ ⊥

Tactic:
;

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
I : Ideal R
⊢ (∀ ⦃x : R⦄, x ∈ I → ∀ n ∈ N, x • n = 0) ↔ ∀ r ∈ I, ∀ n ∈ N, r • n ∈ ⊥
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
I J K : Ideal R
inst✝ : J.IsTwoSided
i : R
hi : ∃ y ∈ I, ∃ z ∈ J, y + z = i
i1 : R
hi1 : i1 ∈ I
k : R
hk : k ∈ K
h : i1 + k = 1
⊢ ∃ y ∈ I, ∃ z ∈ J * K, y + z = i

Tactic:
;

Goal state after:
R : Type u
inst✝¹ : Semiring R
I J K : Ideal R
inst✝ : J.IsTwoSided
i : R
hi : ∃ y ∈ I, ∃ z ∈ J, y + z = i
i1 : R
hi1 : i1 ∈ I
k : R
hk : k ∈ K
h : i1 + k = 1
⊢ ∃ y ∈ I, ∃ z ∈ J * K, y + z = i
Module: Mathlib.Algebra.GCDMonoid.Multiset

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

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

Tactic:
;

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

case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : s.dedup.lcm = s.lcm
h : ¬a ∈ s
⊢ (a ::ₘ s).dedup.lcm = (a ::ₘ s).lcm
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.lcm = s.lcm
h : ¬a ∈ s
⊢ (a ::ₘ s).dedup.lcm = (a ::ₘ s).lcm

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

Tactic:
;

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

case pos
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : s.dedup.lcm = s.lcm
h : a ∈ s
⊢ (a ::ₘ s).dedup.lcm = (a ::ₘ s).lcm
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
x✝ : R
⊢ x✝ ∈ (span R s).annihilator ↔ x✝ ∈ ⨅ g, (toSpanSingleton R M ↑g).ker

Tactic:
;

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
x✝ : R
⊢ x✝ ∈ (span R s).annihilator ↔ x✝ ∈ ⨅ g, (toSpanSingleton R M ↑g).ker
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
I : Ideal R
ι : Type u_1
s : Finset ι
J : ι → Ideal R
inst✝ : ∀ (i : ι), (J i).IsTwoSided
h : ∀ i ∈ s, I ⊔ J i = ⊤
i : ι
t : Finset ι
his : i ∈ s
hts : t ⊆ s
hit : i ∉ t
eq_top : I ⊔ ⨅ i ∈ t, J i = ⊤
⊢ ⊤ ≤ I ⊔ J i ⊓ ⨅ x ∈ t, J x

Tactic:
inf_comm

Goal state after:
R : Type u
inst✝¹ : Semiring R
I : Ideal R
ι : Type u_1
s : Finset ι
J : ι → Ideal R
inst✝ : ∀ (i : ι), (J i).IsTwoSided
h : ∀ i ∈ s, I ⊔ J i = ⊤
i : ι
t : Finset ι
his : i ∈ s
hts : t ⊆ s
hit : i ∉ t
eq_top : I ⊔ ⨅ i ∈ t, J i = ⊤
⊢ ⊤ ≤ I ⊔ (⨅ x ∈ t, J x) ⊓ J i
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
I : Ideal R
ι : Type u_1
s : Finset ι
J : ι → Ideal R
inst✝ : ∀ (i : ι), (J i).IsTwoSided
h : ∀ i ∈ s, J i ⊔ I = ⊤
⊢ ∀ i ∈ s, I ⊔ J i = ⊤

Tactic:
;

Goal state after:
R : Type u
inst✝¹ : Semiring R
I : Ideal R
ι : Type u_1
s : Finset ι
J : ι → Ideal R
inst✝ : ∀ (i : ι), (J i).IsTwoSided
h : ∀ i ∈ s, J i ⊔ I = ⊤
⊢ ∀ i ∈ s, I ⊔ J i = ⊤
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
I : Ideal R
ι : Type u_1
s : Finset ι
J : ι → Ideal R
inst✝ : ∀ (i : ι), (J i).IsTwoSided
h : ∀ i ∈ s, J i ⊔ I = ⊤
i : ι
hi : i ∈ s
⊢ I ⊔ J i = ⊤

Tactic:
;

Goal state after:
R : Type u
inst✝¹ : Semiring R
I : Ideal R
ι : Type u_1
s : Finset ι
J : ι → Ideal R
inst✝ : ∀ (i : ι), (J i).IsTwoSided
h : ∀ i ∈ s, J i ⊔ I = ⊤
i : ι
hi : i ∈ s
⊢ I ⊔ J i = ⊤
Module: Mathlib.Algebra.GCDMonoid.Multiset

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

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

Tactic:
;

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

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.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

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
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) = ⊤

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) = ⊤
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
I J : Ideal R
inst✝ : I.IsTwoSided
n : ℕ
h : I ⊔ J = ⊤
⊢ I ^ n ⊔ J = ⊤

Tactic:
by
  rw [sup_comm, sup_pow_eq_top' (sup_comm I J ▸ h)]

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
w x y z : R
inst✝ : (span {w, x}).IsTwoSided
⊢ span ({w, x} * {y, z}) = span {w * y, w * z, x * y, x * z}

Tactic:
;

Goal state after:
R : Type u
inst✝¹ : Semiring R
w x y z : R
inst✝ : (span {w, x}).IsTwoSided
⊢ span ({w, x} * {y, z}) = span {w * y, w * z, x * y, x * z}
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
w x y z : R
inst✝ : (span {w, x}).IsTwoSided
⊢ {w, x} * {y, z} = {w * y, w * z, x * y, x * z}

Tactic:
;

Goal state after:
R : Type u
inst✝¹ : Semiring R
w x y z : R
inst✝ : (span {w, x}).IsTwoSided
⊢ {w, x} * {y, z} = {w * y, w * z, x * y, x * z}
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
w x y z : R
inst✝ : (span {w, x}).IsTwoSided
r : R
⊢ r ∈ {w, x} * {y, z} ↔ r ∈ {w * y, w * z, x * y, x * z}

Tactic:
;

Goal state after:
R : Type u
inst✝¹ : Semiring R
w x y z : R
inst✝ : (span {w, x}).IsTwoSided
r : R
⊢ r ∈ {w, x} * {y, z} ↔ r ∈ {w * y, w * z, x * y, x * z}
Module: Mathlib.Algebra.GCDMonoid.Nat

Goal state before:
pp: a b : ℕ
⊢ Associated (a * b) (a * b)

Tactic:
;

Goal state after:
a b : ℕ
⊢ Associated (a * b) (a * b)
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) = ⊤

case succ.succ
R : Type u
inst✝ : Semiring R
n : ℕ
ih : n + 1 ≠ 0 → ↑(n + 1) = ⊤
hn : n + 1 + 1 ≠ 0
⊢ ↑(n + 1 + 1) = ⊤
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

Tactic:
rintro ⟨u, hu, v, hv, h1⟩

Goal state after:
case mp
R : Type u_2
inst✝ : CommSemiring R
x y u : R
hu : u ∈ span {x}
v : R
hv : v ∈ span {y}
h1 : u + v = 1
⊢ IsCoprime x y
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
x✝ : R
⊢ x✝ ∈ RingHom.ker (algebraMap R A) ↔ x✝ ∈ ⊥

Tactic:
;

Goal state after:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
x✝ : R
⊢ x✝ ∈ RingHom.ker (algebraMap R A) ↔ x✝ ∈ ⊥
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
ι : Type u_1
inst✝ : CommSemiring R
I : Ideal R
s : Finset ι
J : ι → Ideal R
h : ∀ i ∈ s, J i ⊔ I = ⊤
⊢ ∀ i ∈ s, I ⊔ J i = ⊤

Tactic:
;

Goal state after:
R : Type u
ι : Type u_1
inst✝ : CommSemiring R
I : Ideal R
s : Finset ι
J : ι → Ideal R
h : ∀ i ∈ s, J i ⊔ I = ⊤
⊢ ∀ i ∈ s, I ⊔ J i = ⊤
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: β : Type u_3
α : Type u_5
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
⊢ (s.gcd fun x ↦ a * f x) = normalize a * s.gcd f

Tactic:
;

Goal state after:
β : Type u_3
α : Type u_5
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
⊢ (s.gcd fun x ↦ a * f x) = normalize a * s.gcd f
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
⊢ Associated (s.gcd fun x ↦ a * f x) (a * s.gcd f)

Tactic:
;

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
⊢ Associated (s.gcd fun x ↦ a * f x) (a * s.gcd f)
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
ι : Type u_1
inst✝ : CommSemiring R
I : Ideal R
s : Finset ι
J : ι → Ideal R
h : ∀ i ∈ s, J i ⊔ I = ⊤
i : ι
hi : i ∈ s
⊢ I ⊔ J i = ⊤

Tactic:
;

Goal state after:
R : Type u
ι : Type u_1
inst✝ : CommSemiring R
I : Ideal R
s : Finset ι
J : ι → Ideal R
h : ∀ i ∈ s, J i ⊔ I = ⊤
i : ι
hi : i ∈ s
⊢ I ⊔ J i = ⊤
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I J : Ideal R
⊢ IsCoprime I J ↔ Codisjoint I J

Tactic:
IsCoprime,

Goal state after:
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
⊢ (∃ a b, a * I + b * J = 1) ↔ Codisjoint I J
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α✝ : 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 α
⊢ (if 1 = 0 then 1 else Exists.choose ⋯) = 1

Tactic:
;

Goal state after:
α✝ : 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 α
⊢ (if 1 = 0 then 1 else Exists.choose ⋯) = 1
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α✝ : 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 α
⊢ ↑(if 1 = 0 then 1 else Exists.choose ⋯) = ↑1

Tactic:
;

Goal state after:
α✝ : 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 α
⊢ ↑(if 1 = 0 then 1 else Exists.choose ⋯) = ↑1
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α✝ : Type u_1
α : Type ?u.4
inst✝¹ : CommMonoidWithZero α
normUnit : α → αˣ
normUnit_zero : normUnit 0 = 1
normUnit_one : normUnit 1 = 1
normUnit_mul : ∀ {a b : α}, a ≠ 0 → b ≠ 0 → normUnit (a * b) = normUnit a * normUnit b
normUnit_coe_units : ∀ (u : αˣ), normUnit ↑u = u⁻¹
a : α
u : αˣ
ha : a ≠ 0
inst✝ : Nontrivial α
⊢ normUnit (a * ↑u) = u⁻¹ * normUnit a

Tactic:
;

Goal state after:
α✝ : Type u_1
α : Type ?u.4
inst✝¹ : CommMonoidWithZero α
normUnit : α → αˣ
normUnit_zero : normUnit 0 = 1
normUnit_one : normUnit 1 = 1
normUnit_mul : ∀ {a b : α}, a ≠ 0 → b ≠ 0 → normUnit (a * b) = normUnit a * normUnit b
normUnit_coe_units : ∀ (u : αˣ), normUnit ↑u = u⁻¹
a : α
u : αˣ
ha : a ≠ 0
inst✝ : Nontrivial α
⊢ normUnit (a * ↑u) = u⁻¹ * normUnit a
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : MonoidWithZero α
inst✝ : NormalizationMonoid α
u : αˣ
a✝ : Nontrivial α
⊢ normUnit ↑u = u⁻¹

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : MonoidWithZero α
inst✝ : NormalizationMonoid α
u : αˣ
a✝ : Nontrivial α
⊢ normUnit ↑u = u⁻¹
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : MonoidWithZero α
inst✝ : NormalizationMonoid α
⊢ normalize 0 = 0

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : MonoidWithZero α
inst✝ : NormalizationMonoid α
⊢ normalize 0 = 0
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : MonoidWithZero α
inst✝ : NormalizationMonoid α
u : αˣ
a✝ : Nontrivial α
⊢ normalize 0 = normalize (0 * ↑u)

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : MonoidWithZero α
inst✝ : NormalizationMonoid α
u : αˣ
a✝ : Nontrivial α
⊢ normalize 0 = normalize (0 * ↑u)
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizationMonoid α
y : α
⊢ normalize (0 * y) = normalize 0 * normalize y

pp: case inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizationMonoid α
x y : α
hx : x ≠ 0
⊢ normalize (x * y) = normalize x * normalize y

Tactic:
;

Goal state after:
case inl
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizationMonoid α
y : α
⊢ normalize (0 * y) = normalize 0 * normalize y

case inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizationMonoid α
x y : α
hx : x ≠ 0
⊢ normalize (x * y) = normalize x * normalize y
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizationMonoid α
x : α
hx : x ≠ 0
⊢ normalize (x * 0) = normalize x * normalize 0

pp: case inr.inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ normalize (x * y) = normalize x * normalize y

Tactic:
;

Goal state after:
case inr.inl
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizationMonoid α
x : α
hx : x ≠ 0
⊢ normalize (x * 0) = normalize x * normalize 0

case inr.inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ normalize (x * y) = normalize x * normalize y
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case mp
R : Type u
inst✝ : CommSemiring R
x y a b : R
e : a * x + y * b = 1
⊢ IsCoprime x y

Tactic:
;

Goal state after:
case mp
R : Type u
inst✝ : CommSemiring R
x y a b : R
e : a * x + y * b = 1
⊢ IsCoprime x y
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case mpr
R : Type u
inst✝ : CommSemiring R
x y a b : R
e : a * x + b * y = 1
⊢ ∃ a b, y ∣ b ∧ a * x + b = 1

Tactic:
;

Goal state after:
case mpr
R : Type u
inst✝ : CommSemiring R
x y a b : R
e : a * x + b * y = 1
⊢ ∃ a b, y ∣ b ∧ a * x + b = 1
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizedGCDMonoid α
b c : α
⊢ gcd (0 * b) (0 * c) = normalize 0 * gcd b c

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizedGCDMonoid α
b c : α
⊢ gcd (0 * b) (0 * c) = normalize 0 * gcd b c
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case neg
α : Type u_1
inst✝ : CommMonoidWithZero α
k m n : α
H : k ∣ m * n
a✝ : GCDMonoid α
h0 : ¬gcd k m = 0
a : α
ha : k = gcd k m * a
⊢ ∃ a₁ a₂, a₁ ∣ m ∧ a₂ ∣ n ∧ k = a₁ * a₂

Tactic:
refine ⟨gcd k m, a, gcd_dvd_right _ _, ?_, ha⟩

Goal state after:
case neg
α : Type u_1
inst✝ : CommMonoidWithZero α
k m n : α
H : k ∣ m * n
a✝ : GCDMonoid α
h0 : ¬gcd k m = 0
a : α
ha : k = gcd k m * a
⊢ a ∣ n
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I J : Ideal R
hI : I.IsRadical
hJ : J.IsRadical
⊢ I.radical ⊓ J.radical ≤ I ⊓ J

Tactic:
;

Goal state after:
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
hI : I.IsRadical
hJ : J.IsRadical
⊢ I.radical ⊓ J.radical ≤ I ⊓ J
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case neg.zero
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
hg : ¬gcd a b = 0
⊢ gcd a 1 ∣ 1

Tactic:
;

Goal state after:
case neg.zero
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
hg : ¬gcd a b = 0
⊢ gcd a 1 ∣ 1
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case neg.succ
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
hg : ¬gcd a b = 0
k : ℕ
hk : gcd a (b ^ k) ∣ gcd a b ^ k
⊢ gcd a (b ^ (k + 1)) ∣ gcd a b ^ (k + 1)

Tactic:
rw [pow_succ', pow_succ']
      trans gcd a b * gcd a (b ^ k)
      · exact gcd_mul_dvd_mul_gcd a b (b ^ k)
      · exact (mul_dvd_mul_iff_left hg).mpr hk

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R
r : R
hr : r ∈ sInf {J | I ≤ J ∧ J.IsPrime}
hri : r ∉ I.radical
hIm : I ≤ ⊤
hm : Maximal (fun x ↦ x ∈ {K | r ∉ K.radical}) ⊤
hrm : r ∉ ⊤.radical
this : ∀ x ∉ ⊤, r ∈ (⊤ ⊔ span {x}).radical
⊢ False

Tactic:
;

Goal state after:
R : Type u
inst✝ : CommSemiring R
I : Ideal R
r : R
hr : r ∈ sInf {J | I ≤ J ∧ J.IsPrime}
hri : r ∉ I.radical
hIm : I ≤ ⊤
hm : Maximal (fun x ↦ x ∈ {K | r ∉ K.radical}) ⊤
hrm : r ∉ ⊤.radical
this : ∀ x ∉ ⊤, r ∈ (⊤ ⊔ span {x}).radical
⊢ False
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R
r : R
hr : r ∈ sInf {J | I ≤ J ∧ J.IsPrime}
hri : r ∉ I.radical
hIm : I ≤ ⊤
hm : Maximal (fun x ↦ x ∈ {K | r ∉ K.radical}) ⊤
hrm : r ∉ ⊤
this : ∀ x ∉ ⊤, r ∈ (⊤ ⊔ span {x}).radical
⊢ False

Tactic:
;

Goal state after:
R : Type u
inst✝ : CommSemiring R
I : Ideal R
r : R
hr : r ∈ sInf {J | I ≤ J ∧ J.IsPrime}
hri : r ∉ I.radical
hIm : I ≤ ⊤
hm : Maximal (fun x ↦ x ∈ {K | r ∉ K.radical}) ⊤
hrm : r ∉ ⊤
this : ∀ x ∉ ⊤, r ∈ (⊤ ⊔ span {x}).radical
⊢ False
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
⊢ IsPrimal 0

pp: case inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
ha : a ≠ 0
⊢ IsPrimal a

Tactic:
;

Goal state after:
case inl
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
⊢ IsPrimal 0

case inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
ha : a ≠ 0
⊢ IsPrimal a
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizedGCDMonoid α
b c : α
⊢ lcm (0 * b) (0 * c) = normalize 0 * lcm b c

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizedGCDMonoid α
b c : α
⊢ lcm (0 * b) (0 * c) = normalize 0 * lcm b c
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : Subsingleton αˣ
normUnit✝ : α → αˣ
normUnit_zero✝ : normUnit✝ 0 = 1
normUnit_one✝ : normUnit✝ 1 = 1
normUnit_mul_units✝ : ∀ {a : α} (u : αˣ), a ≠ 0 → normUnit✝ (a * ↑u) = u⁻¹ * normUnit✝ a
⊢ { normUnit := normUnit✝, normUnit_zero := normUnit_zero✝, normUnit_one := normUnit_one✝,
      normUnit_mul_units := normUnit_mul_units✝ } =
    inferInstance

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : Subsingleton αˣ
normUnit✝ : α → αˣ
normUnit_zero✝ : normUnit✝ 0 = 1
normUnit_one✝ : normUnit✝ 1 = 1
normUnit_mul_units✝ : ∀ {a : α} (u : αˣ), a ≠ 0 → normUnit✝ (a * ↑u) = u⁻¹ * normUnit✝ a
⊢ { normUnit := normUnit✝, normUnit_zero := normUnit_zero✝, normUnit_one := normUnit_one✝,
      normUnit_mul_units := normUnit_mul_units✝ } =
    inferInstance