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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
⊢ ∀ (x : R × S), x ∈ ⊤.prod ⊤ ↔ x ∈ ⊤

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M N : Submodule R A
m n : A
I J : Submodule R A
a✝ b✝ : A
ha : a✝ ∈ {x | ∀ y ∈ J, x * y ∈ I}
hb : b✝ ∈ {x | ∀ y ∈ J, x * y ∈ I}
y : A
hy : y ∈ J
⊢ (a✝ + b✝) * y ∈ I

Tactic:
add_mul

Goal state after:
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M N : Submodule R A
m n : A
I J : Submodule R A
a✝ b✝ : A
ha : a✝ ∈ {x | ∀ y ∈ J, x * y ∈ I}
hb : b✝ ∈ {x | ∀ y ∈ J, x * y ∈ I}
y : A
hy : y ∈ J
⊢ a✝ * y + b✝ * y ∈ I
Module: Mathlib.RingTheory.Ideal.Prod

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I✝ : Ideal R
J✝ : Ideal S
x✝ : Ideal R × Ideal S
I : Ideal R
J : Ideal S
⊢ (fun I ↦ (map (RingHom.fst R S) I, map (RingHom.snd R S) I)) ((fun I ↦ I.1.prod I.2) (I, J)) = (I, J)

Tactic:
by simp

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
J : Ideal S
x✝¹ : 1 ∉ I ∧ 1 ∉ J
x✝ : 1 ∉ I.prod J
hI : 1 ∉ I
hJ : 1 ∉ J
⊢ (0, 1) * (1, 0) ∈ I.prod J

Tactic:
by simp

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

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : Semiring R
inst✝² : Semiring S
I✝ : Ideal R
J : Ideal S
inst✝¹ : IsPrincipalIdealRing R
inst✝ : IsPrincipalIdealRing S
I : Ideal (R × S)
⊢ {generator (Ideal.map (RingHom.fst R S) I)}.Nonempty

Tactic:
by simp

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

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : Semiring R
inst✝² : Semiring S
I✝ : Ideal R
J : Ideal S
inst✝¹ : IsPrincipalIdealRing R
inst✝ : IsPrincipalIdealRing S
I : Ideal (R × S)
⊢ {generator (Ideal.map (RingHom.snd R S) I)}.Nonempty

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.Noetherian.Orzech

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type w
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsNoetherian R M
i f : N →ₗ[R] M
hi : Injective ⇑i
hf : Surjective ⇑f
this : IsNoetherian R N
⊢ Submodule.map f ⊥ ≤ Submodule.map i ⊥

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
N : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
S : Submodule R N
x✝ : IsNoetherian R ↥S ∧ IsNoetherian R (N ⧸ S)
left✝ : IsNoetherian R ↥S
right✝ : IsNoetherian R (N ⧸ S)
⊢ S.subtype.range = S.mkQ.ker

Tactic:
rw [Submodule.ker_mkQ, Submodule.range_subtype]

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

Goal state before:
pp: ι : Type u_2
inst✝ : Finite ι
⊢ ∀ {α β : Type u_2} (a : α ≃ β),
    (∀ {R : α → Type u_1} [inst : (i : α) → Semiring (R i)] [∀ (i : α), IsNoetherianRing (R i)],
        IsNoetherianRing ((i : α) → R i)) →
      ∀ {R : β → Type u_1} [inst : (i : β) → Semiring (R i)] [∀ (i : β), IsNoetherianRing (R i)],
        IsNoetherianRing ((i : β) → R i)

pp: ι : Type u_2
inst✝ : Finite ι
⊢ ∀ {R : PEmpty.{u_2 + 1} → Type u_1} [inst : (i : PEmpty.{u_2 + 1}) → Semiring (R i)]
    [∀ (i : PEmpty.{u_2 + 1}), IsNoetherianRing (R i)], IsNoetherianRing ((i : PEmpty.{u_2 + 1}) → R i)

pp: ι : Type u_2
inst✝ : Finite ι
⊢ ∀ {α : Type u_2} [Fintype α],
    (∀ {R : α → Type u_1} [inst : (i : α) → Semiring (R i)] [∀ (i : α), IsNoetherianRing (R i)],
        IsNoetherianRing ((i : α) → R i)) →
      ∀ {R : Option α → Type u_1} [inst : (i : Option α) → Semiring (R i)] [∀ (i : Option α), IsNoetherianRing (R i)],
        IsNoetherianRing ((i : Option α) → R i)

Tactic:
· exact fun e h ↦ isNoetherianRing_of_ringEquiv _ (.piCongrLeft _ e)

Goal state after:
ι : Type u_2
inst✝ : Finite ι
⊢ ∀ {R : PEmpty.{u_2 + 1} → Type u_1} [inst : (i : PEmpty.{u_2 + 1}) → Semiring (R i)]
    [∀ (i : PEmpty.{u_2 + 1}), IsNoetherianRing (R i)], IsNoetherianRing ((i : PEmpty.{u_2 + 1}) → R i)

ι : Type u_2
inst✝ : Finite ι
⊢ ∀ {α : Type u_2} [Fintype α],
    (∀ {R : α → Type u_1} [inst : (i : α) → Semiring (R i)] [∀ (i : α), IsNoetherianRing (R i)],
        IsNoetherianRing ((i : α) → R i)) →
      ∀ {R : Option α → Type u_1} [inst : (i : Option α) → Semiring (R i)] [∀ (i : Option α), IsNoetherianRing (R i)],
        IsNoetherianRing ((i : Option α) → R i)
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective ⇑f
p : Submodule R M'
hp : p ≤ f.range
I : Ideal R
⊢ I • comap f p ≤ comap f (I • p)

Tactic:
by simp

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

Goal state before:
pp: ι : Type u_4
R : ι → Type u_5
inst✝ : (i : ι) → Semiring (R i)
I : (i : ι) → Ideal (R i)
i : ι
r : R i
hr : r ∈ I i
⊢ (Pi.evalRingHom R i) (Pi.single i r) = r

Tactic:
by simp

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
I : Ideal R
⊢ I * ⊥ = ⊥

Tactic:
by simp

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
I : Ideal R
⊢ ⊥ * I = ⊥

Tactic:
by simp

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

Goal state before:
pp: case mp
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
⊢ lcm x y = 0 → x = 0 ∨ y = 0

Tactic:
intro hxy

Goal state after:
case mp
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : lcm x y = 0
⊢ x = 0 ∨ y = 0
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : EuclideanDomain R
inst✝ : CommRing S
e : S ≃+* R
a : S
⊢ e.symm (e a / e 0) = 0

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
a : α
⊢ lcm 0 ∣ a ↔ ∀ (b : α), b ∈ 0 → b ∣ a

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
⊢ normalize (lcm 0) = lcm 0

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s✝ : Multiset α
a : α
s : Multiset α
x✝ : normalize s.lcm = s.lcm
⊢ normalize (a ::ₘ s).lcm = (a ::ₘ s).lcm

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s : Multiset α
⊢ (dedup 0).lcm = lcm 0

Tactic:
by simp

Goal state after:
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 ⊔ ⨅ i ∈ ∅, J i = ⊤

Tactic:
by simp

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

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

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
⊢ normalize (gcd 0) = gcd 0

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s✝ : Multiset α
a : α
s : Multiset α
x✝ : normalize s.gcd = s.gcd
⊢ normalize (a ::ₘ s).gcd = (a ::ₘ s).gcd

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s : Multiset α
⊢ (dedup 0).gcd = gcd 0

Tactic:
by simp

Goal state after:
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:
rw [sup_comm, h i hi]

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ (s₁.ndunion s₂).gcd = GCDMonoid.gcd s₁.gcd s₂.gcd

Tactic:
rw [← gcd_dedup, dedup_ext.2, gcd_dedup, gcd_add]

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ ∀ (a : α), a ∈ s₁.ndunion s₂ ↔ a ∈ s₁ + s₂
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ (s₁ ∪ s₂).gcd = GCDMonoid.gcd s₁.gcd s₂.gcd

Tactic:
rw [← gcd_dedup, dedup_ext.2, gcd_dedup, gcd_add]

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ ∀ (a : α), a ∈ s₁ ∪ s₂ ↔ a ∈ s₁ + s₂
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Surjective ⇑f
⊢ map f I = map f J ↔ I ⊔ RingHom.ker f = J ⊔ RingHom.ker f

Tactic:
← (comap_injective_of_surjective f hf).eq_iff,

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Surjective ⇑f
⊢ comap f (map f I) = comap f (map f J) ↔ I ⊔ RingHom.ker f = J ⊔ RingHom.ker f
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
a : β
s : Finset β
x✝ : a ∉ s
ih : (s ∪ s₂).lcm f = GCDMonoid.lcm (s.lcm f) (s₂.lcm f)
⊢ (insert a s ∪ s₂).lcm f = GCDMonoid.lcm ((insert a s).lcm f) (s₂.lcm f)

Tactic:
insert_union,

Goal state after:
α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
a : β
s : Finset β
x✝ : a ∉ s
ih : (s ∪ s₂).lcm f = GCDMonoid.lcm (s.lcm f) (s₂.lcm f)
⊢ (insert a (s ∪ s₂)).lcm f = GCDMonoid.lcm ((insert a s).lcm f) (s₂.lcm f)
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
a : β
s : Finset β
x✝ : a ∉ s
ih : (s ∪ s₂).gcd f = GCDMonoid.gcd (s.gcd f) (s₂.gcd f)
⊢ (insert a s ∪ s₂).gcd f = GCDMonoid.gcd ((insert a s).gcd f) (s₂.gcd f)

Tactic:
insert_union,

Goal state after:
α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
a : β
s : Finset β
x✝ : a ∉ s
ih : (s ∪ s₂).gcd f = GCDMonoid.gcd (s.gcd f) (s₂.gcd f)
⊢ (insert a (s ∪ s₂)).gcd f = GCDMonoid.gcd ((insert a s).gcd f) (s₂.gcd f)
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
m : Multiset R
⊢ (Multiset.map (fun x ↦ span {x}) 0).prod = span {Multiset.prod 0}

Tactic:
by simp

Goal state after:
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
⊢ {x ∈ s | f x ≠ 0}.gcd f = {x ∈ s | f x ≠ 0}.gcd f

Tactic:
by simp

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

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

Tactic:
t

Goal state after:
case refine_2
β : Type u_3
α : Type u_5
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
b : β
t : Finset β
⊢ b ∉ t →
    (t.gcd fun x ↦ a * f x) = normalize a * t.gcd f →
      ((insert b t).gcd fun x ↦ a * f x) = normalize a * (insert b t).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 (∅.gcd fun x ↦ a * f x) (a * ∅.gcd f)

Tactic:
by simp

Goal state after:
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:
rw [sup_comm, h i hi]

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
surj : Function.Surjective ⇑f
I : Ideal B
J : Ideal A
eq : comap f I = RingHom.ker f ⊔ J
⊢ I = map f J

Tactic:
by
  refine le_antisymm (fun x hx ↦ ?_)
    (Ideal.map_le_iff_le_comap.mpr (le_of_le_of_eq le_sup_right eq.symm))
  rcases Ideal.exists_of_comap_eq_ker_sup _ surj eq hx with ⟨y, mem, hy⟩
  simpa [← hy] using Ideal.mem_map_of_mem _ mem

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

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
inst✝¹ : MonoidWithZero α
inst✝ : IsLeftCancelMulZero α
⊢ (if 1 = 1 then 1 else Quotient.out 1) = 1

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MonoidWithZero α
inst✝ : NormalizationMonoid α
a : Associates α
⊢ ∀ (a : α), Associates.out ⟦a⟧ = 0 ↔ ⟦a⟧ = 0

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a : α
⊢ Associated (gcd 1 a) 1

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a : α
⊢ Associated (gcd a 1) 1

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoidWithZero α
n : α
a✝ : GCDMonoid α
H : 0 ∣ 0 * n
⊢ 0 = 0 * n

Tactic:
by simp

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

Goal state before:
pp: case neg.inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
h✝ : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
⊢ ∃ d, Associated (d ^ k) a

Tactic:
have hc : c ∣ a * b := by
    rw [h]
    exact dvd_pow_self _ hk.ne'

Goal state after:
case neg.inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
h✝ : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
hc : c ∣ a * b
⊢ ∃ d, Associated (d ^ k) a
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
f : Multiset α
hi : ∀ b ∈ f, Irreducible b
u : αˣ
hn0 : f.prod * ↑u ≠ 0
hnu : ¬IsUnit (f.prod * ↑u)
b : α
h : b ∈ f
a : α
ha : a ∈ b * ↑u ::ₘ f.erase b
⊢ Irreducible a

Tactic:
obtain rfl | ha := Multiset.mem_cons.1 ha

Goal state after:
case refine_1.inl
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
f : Multiset α
hi : ∀ b ∈ f, Irreducible b
u : αˣ
hn0 : f.prod * ↑u ≠ 0
hnu : ¬IsUnit (f.prod * ↑u)
b : α
h : b ∈ f
ha : b * ↑u ∈ b * ↑u ::ₘ f.erase b
⊢ Irreducible (b * ↑u)

case refine_1.inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
f : Multiset α
hi : ∀ b ∈ f, Irreducible b
u : αˣ
hn0 : f.prod * ↑u ≠ 0
hnu : ¬IsUnit (f.prod * ↑u)
b : α
h : b ∈ f
a : α
ha✝ : a ∈ b * ↑u ::ₘ f.erase b
ha : a ∈ f.erase b
⊢ Irreducible a
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R
x✝ : 1 ≠ 0
⊢ (I ^ 1).radical = I.radical

Tactic:
by simp

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsPrime
s : Multiset R
⊢ s.prod ∈ I ↔ ∃ p ∈ s, p ∈ I

Tactic:
simpa using (hI.multiset_prod_map_le (span {·}))

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
h✝ : ¬(a = 0 ∨ b = 0)
h1 : ¬a = 0
h2 : ¬b = 0
h : gcd a b ≠ 0
⊢ gcd a b * lcm a b ∣ gcd a b * c ↔ a ∣ c ∧ b ∣ c

Tactic:
(gcd_mul_lcm a b).dvd_iff_dvd_left,

Goal state after:
case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
h✝ : ¬(a = 0 ∨ b = 0)
h1 : ¬a = 0
h2 : ¬b = 0
h : gcd a b ≠ 0
⊢ a * b ∣ gcd a b * c ↔ a ∣ c ∧ b ∣ c
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
m n : α
⊢ m ∣ m * n

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
m n : α
⊢ n ∣ m * n

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : DecidableEq α
gcd : α → α → α
gcd_dvd_left : ∀ (a b : α), gcd a b ∣ a
gcd_dvd_right : ∀ (a b : α), gcd a b ∣ b
dvd_gcd : ∀ {a b c : α}, a ∣ c → a ∣ b → a ∣ gcd c b
a : α
⊢ (if a = 0 then 0 else Classical.choose ⋯) = 0

Tactic:
split_ifs with a0
      · rfl
      have h := (Classical.choose_spec ((gcd_dvd_left a 0).trans (Dvd.intro 0 rfl))).symm
      have a0' : gcd a 0 ≠ 0 := by
        contrapose a0
        rw [← associated_zero_iff_eq_zero, ← a0]
        exact associated_of_dvd_dvd (dvd_gcd (dvd_refl a) (dvd_zero a)) (gcd_dvd_left _ _)
      apply Or.resolve_left (mul_eq_zero.1 _) a0'
      rw [h, mul_zero]

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ⊥ = R ∙ 0

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
M : Type v
inst✝¹ : Ring R
inst✝ : IsBezout R
x y : R
⊢ Ideal.span ↑{x, y} = Ideal.span {x, y}

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
x y : R
inst✝ : IsPrincipal (Ideal.span {x, y})
⊢ x ∈ {x, y}

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
x y : R
inst✝ : IsPrincipal (Ideal.span {x, y})
⊢ y ∈ {x, y}

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
G₀ : Type u_2
inst✝¹ : CommGroupWithZero G₀
inst✝ : DecidableEq G₀
u : G₀ˣ
⊢ (if h : ↑u = 0 then 1 else (Units.mk0 (↑u) h)⁻¹) = u⁻¹

Tactic:
by simp

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Defs

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
eₘ : m ≃ l
eₙ : n ≃ o
M : Matrix m n α
⊢ (fun M ↦ M.submatrix ⇑eₘ ⇑eₙ) ((fun M ↦ M.submatrix ⇑eₘ.symm ⇑eₙ.symm) M) = M

Tactic:
by simp

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Defs

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
eₘ : m ≃ l
eₙ : n ≃ o
M : Matrix l o α
⊢ (fun M ↦ M.submatrix ⇑eₘ.symm ⇑eₙ.symm) ((fun M ↦ M.submatrix ⇑eₘ ⇑eₙ) M) = M

Tactic:
by simp

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : StrongRankCondition R
inst✝⁴ : Ring S
inst✝³ : IsDomain S
inst✝² : Algebra R S
n : Type u_4
m : Type u_5
inst✝¹ : Fintype n
inst✝ : Fintype m
b : Basis n R S
I : Ideal S
hI : I ≠ ⊥
c : Basis m R ↥I
a : ↥I
ha : a ≠ 0
hb : ∀ (g : n → R), ∑ i, g i • b i = 0 → ∀ (i : n), g i = 0
g : n → R
hg : ∑ i, g i • b i = 0 ∨ a = 0
⊢ ∑ i, g i • b i = 0

Tactic:
exact hg.resolve_right ha

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : StrongRankCondition R
⊢ Module.rank R R = ↑1

Tactic:
by simp

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

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : I.IsMaximal
x : R
hx : x ∉ I
y i : R
hmem : i ∈ I
hi : y * x + i = 1
⊢ 0 * x + i ^ 0 = 1

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ∀ (b : Submodule R M), 1 • b = b

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.AlgebraTower

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
ι : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : AddCommMonoid M
inst✝³ : Algebra R A
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
b : Basis ι R M
h : Function.Bijective ⇑(algebraMap R A)
c : R
x : M
⊢ (RingEquiv.ofBijective (algebraMap R A) h) c • x = c • x

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Order.Group.Finset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
⊢ s.toFinset = {a} ↔ s.card ≠ 0 ∧ s = s.card • {a}

Tactic:
by
  refine ⟨fun H ↦ ⟨fun h ↦ ?_, ext' fun x ↦ ?_⟩, fun H ↦ ?_⟩
  · rw [card_eq_zero.1 h, toFinset_zero] at H
    exact Finset.empty_ne_singleton _ H
  · rw [count_nsmul, count_singleton]
    by_cases hx : x = a
    · simp_rw [hx, ite_true, mul_one, count_eq_card]
      intro y hy
      rw [← mem_toFinset, H, Finset.mem_singleton] at hy
      exact hy.symm
    have hx' : x ∉ s := fun h' ↦ hx <| by rwa [← mem_toFinset, H, Finset.mem_singleton] at h'
    simp_rw [count_eq_zero_of_notMem hx', hx, ite_false, Nat.mul_zero]
  simpa only [toFinset_nsmul _ _ H.1, toFinset_singleton] using congr($(H.2).toFinset)

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Finsupp

Goal state before:
pp: α β : Type u
inst✝¹ : Fintype α
inst✝ : Zero β
⊢ #(α →₀ β) = #β ^ Fintype.card α

Tactic:
by simp

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Finsupp

Goal state before:
pp: α β : Type u
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ #(α →₀ β) = max #α #β

Tactic:
by simp

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Finsupp

Goal state before:
pp: α β : Type u
inst✝² : Nonempty α
inst✝¹ : Zero β
inst✝ : Infinite β
⊢ #(α →₀ β) = max #α #β

Tactic:
by simp

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Finsupp

Goal state before:
pp: α : Type u
inst✝ : Nonempty α
⊢ #(α →₀ ℕ) = max #α ℵ₀

Tactic:
by simp

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Finsupp

Goal state before:
pp: α : Type u
inst✝ : IsEmpty α
⊢ #(α →₀ ℕ) = 1

Tactic:
by simp

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Finsupp

Goal state before:
pp: α : Type u
inst✝ : Infinite α
⊢ #(Multiset α) = #α

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Set.UnionLift

Goal state before:
pp: α : Type u_1
ι : Sort u_3
β : Sort u_2
S : ι → Set α
f : (i : ι) → ↑(S i) → β
hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩
T : Set α
hT : T ⊆ iUnion S
i : ι
x : α
hx✝ : x ∈ T
hx : ↑⟨x, hx✝⟩ ∈ S i
⊢ iUnionLift S f hf T hT ⟨x, hx✝⟩ = f i ⟨↑⟨x, hx✝⟩, hx⟩

Tactic:
exact hf _ _ _ _ _

Goal state after:
Module: Mathlib.Data.Finsupp.Multiset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f : α →₀ ℕ
a : α
⊢ Multiset.count a (f.sum fun a n ↦ n • {a}) = f.sum fun x n ↦ Multiset.count a (n • {x})

Tactic:
exact map_sum (Multiset.countAddMonoidHom a) _ f.support

Goal state after: