mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a b : α
ane0 : a ≠ 0
c : α
hc : ¬IsUnit c
b_eq : b = a * c
h✝ : ¬b = 0
cne0 : c ≠ 0
x : α
h : x ∈ Classical.choose ⋯
⊢ a ≠ 0

pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a b : α
ane0 : a ≠ 0
c : α
hc : ¬IsUnit c
b_eq : b = a * c
h✝ : ¬b = 0
cne0 : c ≠ 0
x : α
h : x ∈ Classical.choose ⋯
⊢ c ≠ 0

Tactic:
<;>

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a b : α
ane0 : a ≠ 0
c : α
hc : ¬IsUnit c
b_eq : b = a * c
h✝ : ¬b = 0
cne0 : c ≠ 0
x : α
h : x ∈ Classical.choose ⋯
⊢ a ≠ 0

α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a b : α
ane0 : a ≠ 0
c : α
hc : ¬IsUnit c
b_eq : b = a * c
h✝ : ¬b = 0
cne0 : c ≠ 0
x : α
h : x ∈ Classical.choose ⋯
⊢ c ≠ 0
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ (∀ x ∈ p.support, p.coeff x = 0) → p = 0

pp: case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ p = 0 → ∀ x ∈ p.support, p.coeff x = 0

Tactic:
<;>

Goal state after:
case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ (∀ x ∈ p.support, p.coeff x = 0) → p = 0

case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ p = 0 → ∀ x ∈ p.support, p.coeff x = 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case h₁
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a b : α
ane0 : a ≠ 0
c : α
hc : ¬IsUnit c
b_eq : b = a * c
h : ¬b = 0
cne0 : c ≠ 0
⊢ (Classical.choose ⋯).prod ~ᵤ a

pp: case h₂
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a b : α
ane0 : a ≠ 0
c : α
hc : ¬IsUnit c
b_eq : b = a * c
h : ¬b = 0
cne0 : c ≠ 0
⊢ (Classical.choose ⋯).prod ~ᵤ c

Tactic:
<;>

Goal state after:
case h₁
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a b : α
ane0 : a ≠ 0
c : α
hc : ¬IsUnit c
b_eq : b = a * c
h : ¬b = 0
cne0 : c ≠ 0
⊢ (Classical.choose ⋯).prod ~ᵤ a

case h₂
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a b : α
ane0 : a ≠ 0
c : α
hc : ¬IsUnit c
b_eq : b = a * c
h : ¬b = 0
cne0 : c ≠ 0
⊢ (Classical.choose ⋯).prod ~ᵤ c
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a b : α
ane0 : a ≠ 0
c : α
hc : ¬IsUnit c
b_eq : b = a * c
h : ¬b = 0
cne0 : c ≠ 0
⊢ a ≠ 0

pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a b : α
ane0 : a ≠ 0
c : α
hc : ¬IsUnit c
b_eq : b = a * c
h : ¬b = 0
cne0 : c ≠ 0
⊢ c ≠ 0

Tactic:
<;>

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a b : α
ane0 : a ≠ 0
c : α
hc : ¬IsUnit c
b_eq : b = a * c
h : ¬b = 0
cne0 : c ≠ 0
⊢ a ≠ 0

α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a b : α
ane0 : a ≠ 0
c : α
hc : ¬IsUnit c
b_eq : b = a * c
h : ¬b = 0
cne0 : c ≠ 0
⊢ c ≠ 0
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
a : R
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p ≠ C a
⊢ (fun x ↦ eval x p) ⁻¹' {a} = (p - C a).rootSet R

Tactic:
by
  ext; simp [mem_rootSet_of_ne (sub_ne_zero.mpr hp), sub_eq_zero]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: T : Type w
inst✝³ : CommRing T
p : T[X]
hp : p.Monic
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
a : S
⊢ a ∈ p.rootSet S ↔ (aeval a) p = 0

Tactic:
simp [Polynomial.mem_rootSet', (hp.map (algebraMap T S)).ne_zero]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: T : Type w
inst✝⁶ : CommRing T
p : T[X]
S : Type u_1
S' : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Algebra T S
inst✝² : CommRing S'
inst✝¹ : IsDomain S'
inst✝ : Algebra T S'
hp : map (algebraMap T S') p = 0 → map (algebraMap T S) p = 0
f : S →ₐ[T] S'
x : S
hx : map (algebraMap T S) p ≠ 0 ∧ (aeval x) p = 0
⊢ map (algebraMap T S') p ≠ 0 ∧ 0 = 0

Tactic:
exact ⟨mt hp hx.1, rfl⟩

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case zero.inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q✝ : R[X]
a✝ : Nontrivial R
q : R[X]
⊢ Associated (0 * q).content (content 0 * q.content)

pp: case zero.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p✝ q : R[X]
a✝ : Nontrivial R
p : R[X]
⊢ Associated (p * 0).content (p.content * content 0)

Tactic:
<;>

Goal state after:
case zero.inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q✝ : R[X]
a✝ : Nontrivial R
q : R[X]
⊢ Associated (0 * q).content (content 0 * q.content)

case zero.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p✝ q : R[X]
a✝ : Nontrivial R
p : R[X]
⊢ Associated (p * 0).content (p.content * content 0)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case top
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
q : WithTop (Multiset { a // Irreducible a })
h : prod ⊤ = prod q
⊢ ⊤ = q

pp: case coe
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
q : WithTop (Multiset { a // Irreducible a })
a✝ : Multiset { a // Irreducible a }
h : prod ↑a✝ = prod q
⊢ ↑a✝ = q

Tactic:
<;>

Goal state after:
case top
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
q : WithTop (Multiset { a // Irreducible a })
h : prod ⊤ = prod q
⊢ ⊤ = q

case coe
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
q : WithTop (Multiset { a // Irreducible a })
a✝ : Multiset { a // Irreducible a }
h : prod ↑a✝ = prod q
⊢ ↑a✝ = q
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : NormalizationMonoid R
a✝ : R[X]
u : R[X]ˣ
h : a✝ ≠ 0
⊢ ↑{ val := C ↑(normUnit (a✝ * ↑u).leadingCoeff), inv := C ↑(normUnit (a✝ * ↑u).leadingCoeff)⁻¹, val_inv := ⋯,
        inv_val := ⋯ } =
    ↑(u⁻¹ *
        { val := C ↑(normUnit a✝.leadingCoeff), inv := C ↑(normUnit a✝.leadingCoeff)⁻¹, val_inv := ⋯, inv_val := ⋯ })

Tactic:
dsimp only [Units.val_mul]
    obtain ⟨_, ⟨w, rfl⟩, h2⟩ := isUnit_iff.1 ⟨u, rfl⟩
    rw [leadingCoeff_mul, ← h2, leadingCoeff_C, normUnit_mul_units _ (leadingCoeff_ne_zero.2 h),
      Units.eq_inv_mul_iff_mul_eq, Units.val_mul, C_mul, ← mul_assoc, ← h2, ← C_mul]
    simp

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a✝¹ a✝ : Multiset { a // Irreducible a }
h : prod ↑a✝¹ = prod ↑a✝
⊢ ∀ a ∈ Multiset.map Subtype.val a✝¹, Irreducible a

pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a✝¹ a✝ : Multiset { a // Irreducible a }
h : prod ↑a✝¹ = prod ↑a✝
⊢ ∀ a ∈ Multiset.map Subtype.val a✝, Irreducible a

Tactic:
<;>

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a✝¹ a✝ : Multiset { a // Irreducible a }
h : prod ↑a✝¹ = prod ↑a✝
⊢ ∀ a ∈ Multiset.map Subtype.val a✝¹, Irreducible a

α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a✝¹ a✝ : Multiset { a // Irreducible a }
h : prod ↑a✝¹ = prod ↑a✝
⊢ ∀ a ∈ Multiset.map Subtype.val a✝, Irreducible a
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : NormalizationMonoid R
⊢ X = normalize X

Tactic:
by
  simp only [normalize_apply, normUnit_X, Units.val_one, mul_one]

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : Associates α
hm : p ∈ a.factors
ha0 : a ≠ 0
a0 : α
nza : a0 ≠ 0
ha' : Associates.mk a0 = a
⊢ p ∣ a

Tactic:
rw [← Associates.factors_prod a]

Goal state after:
case inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : Associates α
hm : p ∈ a.factors
ha0 : a ≠ 0
a0 : α
nza : a0 ≠ 0
ha' : Associates.mk a0 = a
⊢ p ∣ a.factors.prod
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
hd : p ∣ a
⊢ Associates.mk p ∈ (Associates.mk a).factors

Tactic:
factors_mk _ ha0

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
hd : p ∣ a
⊢ Associates.mk p ∈ ↑(factors' a)
Module: Mathlib.RingTheory.Polynomial.UniqueFactorization

Goal state before:
pp: F : Type u_1
inst✝ : Field F
f : F[X]
hu : ¬IsUnit f
⊢ ∃ g, g.Monic ∧ Irreducible g ∧ g ∣ f

Tactic:
by_cases hf : f = 0
  · exact ⟨X, monic_X, irreducible_X, hf ▸ dvd_zero X⟩
  obtain ⟨g, hi, hf⟩ := WfDvdMonoid.exists_irreducible_factor hu hf
  have ha : Associated g (g * C g.leadingCoeff⁻¹) := associated_mul_unit_right _ _ <|
    isUnit_C.2 (leadingCoeff_ne_zero.2 hi.ne_zero).isUnit.inv
  exact ⟨_, monic_mul_leadingCoeff_inv hi.ne_zero, ha.irreducible hi, ha.dvd_iff_dvd_left.1 hf⟩

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case h
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : DecidableEq (Associates α)
p : Associates α
h₂ : Irreducible p
k : ℕ
m : α
hm : m ≠ 0
h₁ : Associates.mk m ≠ 0
this : Nontrivial α
⊢ m ≠ 0

pp: case h
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : DecidableEq (Associates α)
p : Associates α
h₂ : Irreducible p
k : ℕ
m : α
hm : m ≠ 0
h₁ : Associates.mk m ≠ 0
this : Nontrivial α
⊢ m ≠ 0

Tactic:
<;>

Goal state after:
case h
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : DecidableEq (Associates α)
p : Associates α
h₂ : Irreducible p
k : ℕ
m : α
hm : m ≠ 0
h₁ : Associates.mk m ≠ 0
this : Nontrivial α
⊢ m ≠ 0

case h
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : DecidableEq (Associates α)
p : Associates α
h₂ : Irreducible p
k : ℕ
m : α
hm : m ≠ 0
h₁ : Associates.mk m ≠ 0
this : Nontrivial α
⊢ m ≠ 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
m p : Associates α
h0 : m ≠ 0
hp : Irreducible p
h : 0 < p.count m.factors
⊢ p ≤ m

Tactic:
← pow_one p

Goal state after:
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
m p : Associates α
h0 : m ≠ 0
hp : Irreducible p
h : 0 < p.count m.factors
⊢ p ^ 1 ≤ m
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case pos.inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
this : DecidableEq R := Classical.decEq R
p q r : R[X]
rprim : r.IsPrimitive
hr : ∀ (s : R[X]), p.primPart ∣ s ∧ q.primPart ∣ s ↔ r ∣ s
s : R[X]
hs : ¬s = 0
hpq : p = 0
⊢ p ∣ s ∧ q ∣ s ↔ C (lcm p.content q.content) * r ∣ s

pp: case pos.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
this : DecidableEq R := Classical.decEq R
p q r : R[X]
rprim : r.IsPrimitive
hr : ∀ (s : R[X]), p.primPart ∣ s ∧ q.primPart ∣ s ↔ r ∣ s
s : R[X]
hs : ¬s = 0
hpq : q = 0
⊢ p ∣ s ∧ q ∣ s ↔ C (lcm p.content q.content) * r ∣ s

Tactic:
<;>

Goal state after:
case pos.inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
this : DecidableEq R := Classical.decEq R
p q r : R[X]
rprim : r.IsPrimitive
hr : ∀ (s : R[X]), p.primPart ∣ s ∧ q.primPart ∣ s ↔ r ∣ s
s : R[X]
hs : ¬s = 0
hpq : p = 0
⊢ p ∣ s ∧ q ∣ s ↔ C (lcm p.content q.content) * r ∣ s

case pos.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
this : DecidableEq R := Classical.decEq R
p q r : R[X]
rprim : r.IsPrimitive
hr : ∀ (s : R[X]), p.primPart ∣ s ∧ q.primPart ∣ s ↔ r ∣ s
s : R[X]
hs : ¬s = 0
hpq : q = 0
⊢ p ∣ s ∧ q ∣ s ↔ C (lcm p.content q.content) * r ∣ s
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: case neg
R : Type u
inst✝¹ : Field R
inst✝ : DecidableEq R
a : R[X]
ha : ¬a = 0
⊢ a * C 1 = a

pp: case neg
R : Type u
inst✝¹ : Field R
inst✝ : DecidableEq R
a : R[X]
ha : ¬a = 0
⊢ a.leadingCoeff ≠ 0

pp: case neg.h0
R : Type u
inst✝¹ : Field R
inst✝ : DecidableEq R
a : R[X]
ha : ¬a = 0
⊢ a.leadingCoeff ≠ 0

pp: case neg
R : Type u
inst✝¹ : Field R
inst✝ : DecidableEq R
a : R[X]
ha : ¬a = 0
⊢ a ≠ 0

Tactic:
<;>

Goal state after:
case neg
R : Type u
inst✝¹ : Field R
inst✝ : DecidableEq R
a : R[X]
ha : ¬a = 0
⊢ a * C 1 = a

case neg
R : Type u
inst✝¹ : Field R
inst✝ : DecidableEq R
a : R[X]
ha : ¬a = 0
⊢ a.leadingCoeff ≠ 0

case neg.h0
R : Type u
inst✝¹ : Field R
inst✝ : DecidableEq R
a : R[X]
ha : ¬a = 0
⊢ a.leadingCoeff ≠ 0

case neg
R : Type u
inst✝¹ : Field R
inst✝ : DecidableEq R
a : R[X]
ha : ¬a = 0
⊢ a ≠ 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : Associates α
ha : a ≠ 0
hb : b ≠ 0
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
k : ℕ
a✝ : Nontrivial α
hk0 : ¬k = 0
p : Associates α
hp : Irreducible p
h : a * b = 0
h✝ : a = 0
⊢ False

pp: case inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : Associates α
ha : a ≠ 0
hb : b ≠ 0
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
k : ℕ
a✝ : Nontrivial α
hk0 : ¬k = 0
p : Associates α
hp : Irreducible p
h : a * b = 0
h✝ : b = 0
⊢ False

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : Associates α
ha : a ≠ 0
hb : b ≠ 0
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
k : ℕ
a✝ : Nontrivial α
hk0 : ¬k = 0
p : Associates α
hp : Irreducible p
h : a * b = 0
h✝ : a = 0
⊢ False

case inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : Associates α
ha : a ≠ 0
hb : b ≠ 0
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
k : ℕ
a✝ : Nontrivial α
hk0 : ¬k = 0
p : Associates α
hp : Irreducible p
h : a * b = 0
h✝ : b = 0
⊢ False
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝² : DivisionRing A
inst✝¹ : Field R
inst✝ : Algebra R A
n : ℚ
⊢ IsAlgebraic R ↑n

Tactic:
rw [← map_ratCast (algebraMap R A)]

Goal state after:
R : Type u
A : Type v
inst✝² : DivisionRing A
inst✝¹ : Field R
inst✝ : Algebra R A
n : ℚ
⊢ IsAlgebraic R ((algebraMap R A) ↑n)
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: case refine_1
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : ↥A
p : K[X]
⊢ 0 ≠ 0 → (aeval x) 0 = 0 → (↑x)⁻¹ ∈ A

pp: case refine_2
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : ↥A
p : K[X]
⊢ ∀ (p : K[X]) (a : K),
    p.coeff 0 = 0 → a ≠ 0 → (p ≠ 0 → (aeval x) p = 0 → (↑x)⁻¹ ∈ A) → p + C a ≠ 0 → (aeval x) (p + C a) = 0 → (↑x)⁻¹ ∈ A

pp: case refine_3
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : ↥A
p : K[X]
⊢ ∀ (p : K[X]), p ≠ 0 → (p ≠ 0 → (aeval x) p = 0 → (↑x)⁻¹ ∈ A) → p * X ≠ 0 → (aeval x) (p * X) = 0 → (↑x)⁻¹ ∈ A

Tactic:
· intro h
    contradiction

Goal state after:
case refine_2
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : ↥A
p : K[X]
⊢ ∀ (p : K[X]) (a : K),
    p.coeff 0 = 0 → a ≠ 0 → (p ≠ 0 → (aeval x) p = 0 → (↑x)⁻¹ ∈ A) → p + C a ≠ 0 → (aeval x) (p + C a) = 0 → (↑x)⁻¹ ∈ A

case refine_3
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : ↥A
p : K[X]
⊢ ∀ (p : K[X]), p ≠ 0 → (p ≠ 0 → (aeval x) p = 0 → (↑x)⁻¹ ∈ A) → p * X ≠ 0 → (aeval x) (p * X) = 0 → (↑x)⁻¹ ∈ A
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: ι✝ : Type u_1
inst✝¹ : Preorder ι✝
F₁ : ι✝ → Type u_2
F₂ : ι✝ → Type u_3
F✝ : ι✝ → Type u_4
X✝ : ι✝ → Type u_5
f✝ : ⦃i j : ι✝⦄ → i ≤ j → F✝ j → F✝ i
i✝ j : ι✝
h✝ : i✝ ≤ j
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst✝ : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
equiv : (j : ↑(Iio i)) → F ↑j ≃ piLT X ↑j
nat : IsNatEquiv f equiv
t : ↑(limit piLTProj i)
x✝¹ x✝ : ↑(Iio i)
h : ↑x✝¹ ≤ ↑x✝
⊢ piLTProj h ((equiv ⟨↑x✝, ?hj⟩) ((fun l ↦ (equiv l).symm (↑t l)) x✝)) = piLTProj h (↑t x✝)

pp: case hj
ι✝ : Type u_1
inst✝¹ : Preorder ι✝
F₁ : ι✝ → Type u_2
F₂ : ι✝ → Type u_3
F✝ : ι✝ → Type u_4
X✝ : ι✝ → Type u_5
f✝ : ⦃i j : ι✝⦄ → i ≤ j → F✝ j → F✝ i
i✝ j : ι✝
h✝ : i✝ ≤ j
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst✝ : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
equiv : (j : ↑(Iio i)) → F ↑j ≃ piLT X ↑j
nat : IsNatEquiv f equiv
t : ↑(limit piLTProj i)
x✝¹ x✝ : ↑(Iio i)
h : ↑x✝¹ ≤ ↑x✝
⊢ ↑x✝ ∈ Iio i

Tactic:
<;>

Goal state after:
ι✝ : Type u_1
inst✝¹ : Preorder ι✝
F₁ : ι✝ → Type u_2
F₂ : ι✝ → Type u_3
F✝ : ι✝ → Type u_4
X✝ : ι✝ → Type u_5
f✝ : ⦃i j : ι✝⦄ → i ≤ j → F✝ j → F✝ i
i✝ j : ι✝
h✝ : i✝ ≤ j
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst✝ : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
equiv : (j : ↑(Iio i)) → F ↑j ≃ piLT X ↑j
nat : IsNatEquiv f equiv
t : ↑(limit piLTProj i)
x✝¹ x✝ : ↑(Iio i)
h : ↑x✝¹ ≤ ↑x✝
⊢ piLTProj h ((equiv ⟨↑x✝, ?hj⟩) ((fun l ↦ (equiv l).symm (↑t l)) x✝)) = piLTProj h (↑t x✝)

case hj
ι✝ : Type u_1
inst✝¹ : Preorder ι✝
F₁ : ι✝ → Type u_2
F₂ : ι✝ → Type u_3
F✝ : ι✝ → Type u_4
X✝ : ι✝ → Type u_5
f✝ : ⦃i j : ι✝⦄ → i ≤ j → F✝ j → F✝ i
i✝ j : ι✝
h✝ : i✝ ≤ j
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst✝ : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
equiv : (j : ↑(Iio i)) → F ↑j ≃ piLT X ↑j
nat : IsNatEquiv f equiv
t : ↑(limit piLTProj i)
x✝¹ x✝ : ↑(Iio i)
h : ↑x✝¹ ≤ ↑x✝
⊢ ↑x✝ ∈ Iio i
Module: Mathlib.RingTheory.MvPolynomial.Basic

Goal state before:
pp: case pos
σ : Type u
R : Type v
inst✝ : CommSemiring R
s : Set (σ →₀ ℕ)
m : σ →₀ ℕ
r : R
h✝ : r = 0
⊢ (monomial m) r ∈ restrictSupport R s ↔ m ∈ s ∨ r = 0

pp: case neg
σ : Type u
R : Type v
inst✝ : CommSemiring R
s : Set (σ →₀ ℕ)
m : σ →₀ ℕ
r : R
h✝ : ¬r = 0
⊢ (monomial m) r ∈ restrictSupport R s ↔ m ∈ s ∨ r = 0

Tactic:
<;>

Goal state after:
case pos
σ : Type u
R : Type v
inst✝ : CommSemiring R
s : Set (σ →₀ ℕ)
m : σ →₀ ℕ
r : R
h✝ : r = 0
⊢ (monomial m) r ∈ restrictSupport R s ↔ m ∈ s ∨ r = 0

case neg
σ : Type u
R : Type v
inst✝ : CommSemiring R
s : Set (σ →₀ ℕ)
m : σ →₀ ℕ
r : R
h✝ : ¬r = 0
⊢ (monomial m) r ∈ restrictSupport R s ↔ m ∈ s ∨ r = 0
Module: Mathlib.RingTheory.Finiteness.Small

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P Q : Submodule R M
smallP : Small.{u, u_2} ↥P
smallQ : Small.{u, u_2} ↥Q
⊢ Small.{u, u_2} ↥(P ⊔ Q)

Tactic:
rw [Submodule.sup_eq_range]
  exact small_range _

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Basic

Goal state before:
pp: case zero
σ : Type u
R : Type v
inst✝ : CommSemiring R
s : Set (σ →₀ ℕ)
⊢ restrictSupport R (0 • s) = restrictSupport R s ^ 0

pp: case succ
σ : Type u
R : Type v
inst✝ : CommSemiring R
s : Set (σ →₀ ℕ)
n✝ : ℕ
a✝ : restrictSupport R (n✝ • s) = restrictSupport R s ^ n✝
⊢ restrictSupport R ((n✝ + 1) • s) = restrictSupport R s ^ (n✝ + 1)

Tactic:
<;>

Goal state after:
case zero
σ : Type u
R : Type v
inst✝ : CommSemiring R
s : Set (σ →₀ ℕ)
⊢ restrictSupport R (0 • s) = restrictSupport R s ^ 0

case succ
σ : Type u
R : Type v
inst✝ : CommSemiring R
s : Set (σ →₀ ℕ)
n✝ : ℕ
a✝ : restrictSupport R (n✝ • s) = restrictSupport R s ^ n✝
⊢ restrictSupport R ((n✝ + 1) • s) = restrictSupport R s ^ (n✝ + 1)
Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness

Goal state before:
pp: case h.hi
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x : M ⊗[R] N
S : M →₀ N
h : x = S.sum fun m n ↦ m ⊗ₜ[R] n
⊢ ∀ a ∈ S.support, (a, S a) ∈ S.graph

pp: case h.hj
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x : M ⊗[R] N
S : M →₀ N
h : x = S.sum fun m n ↦ m ⊗ₜ[R] n
⊢ ∀ a ∈ S.graph, a.1 ∈ S.support

pp: case h.left_neg
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x : M ⊗[R] N
S : M →₀ N
h : x = S.sum fun m n ↦ m ⊗ₜ[R] n
⊢ ∀ a ∈ S.support, (a, S a).1 = a

pp: case h.right_neg
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x : M ⊗[R] N
S : M →₀ N
h : x = S.sum fun m n ↦ m ⊗ₜ[R] n
⊢ ∀ a ∈ S.graph, (a.1, S a.1) = a

pp: case h.h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x : M ⊗[R] N
S : M →₀ N
h : x = S.sum fun m n ↦ m ⊗ₜ[R] n
⊢ ∀ a ∈ S.support, a ⊗ₜ[R] S a = (a, S a).1 ⊗ₜ[R] (a, S a).2

Tactic:
<;>

Goal state after:
case h.hi
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x : M ⊗[R] N
S : M →₀ N
h : x = S.sum fun m n ↦ m ⊗ₜ[R] n
⊢ ∀ a ∈ S.support, (a, S a) ∈ S.graph

case h.hj
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x : M ⊗[R] N
S : M →₀ N
h : x = S.sum fun m n ↦ m ⊗ₜ[R] n
⊢ ∀ a ∈ S.graph, a.1 ∈ S.support

case h.left_neg
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x : M ⊗[R] N
S : M →₀ N
h : x = S.sum fun m n ↦ m ⊗ₜ[R] n
⊢ ∀ a ∈ S.support, (a, S a).1 = a

case h.right_neg
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x : M ⊗[R] N
S : M →₀ N
h : x = S.sum fun m n ↦ m ⊗ₜ[R] n
⊢ ∀ a ∈ S.graph, (a.1, S a.1) = a

case h.h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x : M ⊗[R] N
S : M →₀ N
h : x = S.sum fun m n ↦ m ⊗ₜ[R] n
⊢ ∀ a ∈ S.support, a ⊗ₜ[R] S a = (a, S a).1 ⊗ₜ[R] (a, S a).2
Module: Mathlib.RingTheory.Nilpotent.Defs

Goal state before:
pp: case left
R : Type u_1
inst✝¹ : MonoidWithZero R
inst✝ : Nontrivial R
⊢ 0 ^ (0 + 1) = 0

pp: case right
R : Type u_1
inst✝¹ : MonoidWithZero R
inst✝ : Nontrivial R
⊢ 0 ^ 0 ≠ 0

Tactic:
<;>

Goal state after:
case left
R : Type u_1
inst✝¹ : MonoidWithZero R
inst✝ : Nontrivial R
⊢ 0 ^ (0 + 1) = 0

case right
R : Type u_1
inst✝¹ : MonoidWithZero R
inst✝ : Nontrivial R
⊢ 0 ^ 0 ≠ 0