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

Goal state before:
pp: R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : OrzechProperty R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module.Finite R M
N : Type w
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
i f : N →ₗ[R] M
n : ℕ
g : (Fin n → R) →ₗ[R] M
hg : Surjective ⇑g
this✝² : Small.{u, v} M
this✝¹ : AddCommMonoid (Shrink.{u, v} M) := (equivShrink M).symm.addCommMonoid
this✝ : Module R (Shrink.{u, v} M) := Equiv.module R (equivShrink M).symm
j : Shrink.{u, v} M ≃ₗ[R] M := Equiv.linearEquiv R (equivShrink M).symm
this : Module.Finite R (Shrink.{u, v} M)
i' : N →ₗ[R] Shrink.{u, v} M := ↑j.symm ∘ₗ i
hi : Injective ⇑i'
f' : ↥i'.range →ₗ[R] Shrink.{u, v} M := ↑j.symm ∘ₗ f ∘ₗ ↑(LinearEquiv.ofInjective i' hi).symm
hf : Surjective ⇑f'
⊢ Injective ⇑f

Tactic:
simpa using

Goal state after:
R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : OrzechProperty R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module.Finite R M
N : Type w
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
i f : N →ₗ[R] M
n : ℕ
g : (Fin n → R) →ₗ[R] M
hg : Surjective ⇑g
this✝² : Small.{u, v} M
this✝¹ : AddCommMonoid (Shrink.{u, v} M) := (equivShrink M).symm.addCommMonoid
this✝ : Module R (Shrink.{u, v} M) := Equiv.module R (equivShrink M).symm
j : Shrink.{u, v} M ≃ₗ[R] M := Equiv.linearEquiv R (equivShrink M).symm
this : Module.Finite R (Shrink.{u, v} M)
i' : N →ₗ[R] Shrink.{u, v} M := ↑j.symm ∘ₗ i
hi : Injective ⇑i'
f' : ↥i'.range →ₗ[R] Shrink.{u, v} M := ↑j.symm ∘ₗ f ∘ₗ ↑(LinearEquiv.ofInjective i' hi).symm
hf : Surjective ⇑f'
⊢ Injective ⇑f
Module: Mathlib.RingTheory.Noetherian.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁸ : Ring R
inst✝⁷ : Ring S
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup P
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module S P
ι : Type u_6
inst✝ : Finite ι
⊢ ∀ {M : ι → Type u_7} [inst : (i : ι) → AddCommGroup (M i)] [inst_1 : (i : ι) → Module R (M i)]
    [∀ (i : ι), IsNoetherian R (M i)], IsNoetherian R ((i : ι) → M i)

Tactic:
apply Finite.induction_empty_option _ _ _ ι
  · exact fun e h ↦ isNoetherian_of_linearEquiv (LinearEquiv.piCongrLeft R _ e)
  · infer_instance
  · exact fun ih ↦ isNoetherian_of_linearEquiv (LinearEquiv.piOptionEquivProd R).symm

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
f : M × N →ₗ[R] M
i : Injective ⇑f
x y : N
h : Injective ⇑(LinearMap.fst R M N)
⊢ x = y

Tactic:
simpa using

Goal state after:
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
f : M × N →ₗ[R] M
i : Injective ⇑f
x y : N
h : Injective ⇑(LinearMap.fst R M N)
⊢ x = y
Module: Mathlib.RingTheory.Noetherian.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹⁰ : Ring R
inst✝⁹ : Ring S
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : AddCommGroup P
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module S P
ι : Type u_6
inst✝² : Finite ι
α✝ : Type u_6
inst✝¹ : Fintype α✝
ih : ∀ {M : α✝ → Submodule R N} [∀ (i : α✝), IsNoetherian R ↥(M i)], IsNoetherian R ↥(⨆ i, M i)
M✝ : Option α✝ → Submodule R N
inst✝ : ∀ (i : Option α✝), IsNoetherian R ↥(M✝ i)
⊢ IsNoetherian R ↥(⨆ i, M✝ i)

Tactic:
rw [iSup_option]

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹⁰ : Ring R
inst✝⁹ : Ring S
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : AddCommGroup P
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module S P
ι : Type u_6
inst✝² : Finite ι
α✝ : Type u_6
inst✝¹ : Fintype α✝
ih : ∀ {M : α✝ → Submodule R N} [∀ (i : α✝), IsNoetherian R ↥(M i)], IsNoetherian R ↥(⨆ i, M i)
M✝ : Option α✝ → Submodule R N
inst✝ : ∀ (i : Option α✝), IsNoetherian R ↥(M✝ i)
⊢ IsNoetherian R ↥(M✝ none ⊔ ⨆ b, M✝ (some b))
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
⊢ IsNoetherian R N ↔ IsNoetherian R ↥S ∧ IsNoetherian R (N ⧸ S)

Tactic:
by
  refine ⟨fun _ ↦ ⟨inferInstance, inferInstance⟩, fun ⟨_, _⟩ ↦ ?_⟩
  apply isNoetherian_of_range_eq_ker S.subtype S.mkQ
  rw [Submodule.ker_mkQ, Submodule.range_subtype]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint ((partialSups f) n) (f (n + 1))
n : ℕ
w : ∀ (m : ℕ), n ≤ m → (partialSups f) n = (partialSups f) m
m : ℕ
p : n ≤ m
⊢ (partialSups f) m ⊔ f (m + 1) = (partialSups f) m

Tactic:
simpa using

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint ((partialSups f) n) (f (n + 1))
n : ℕ
w : ∀ (m : ℕ), n ≤ m → (partialSups f) n = (partialSups f) m
m : ℕ
p : n ≤ m
⊢ (partialSups f) m ⊔ f (m + 1) = (partialSups f) m
Module: Mathlib.RingTheory.Noetherian.Basic

Goal state before:
pp: case h
R : Type u
inst✝⁴ : CommRing R
inst✝³ : Small.{v, u} R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
m : ℕ
f' : (Fin m → R) →ₗ[R] M
hf' : Surjective ⇑f'
f : (Fin m →₀ Shrink.{v, u} R) →ₗ[R] M := ⋯
⊢ Surjective ⇑f

Tactic:
simpa using

Goal state after:
case h
R : Type u
inst✝⁴ : CommRing R
inst✝³ : Small.{v, u} R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
m : ℕ
f' : (Fin m → R) →ₗ[R] M
hf' : Surjective ⇑f'
f : (Fin m →₀ Shrink.{v, u} R) →ₗ[R] M :=
  f' ∘ₗ ↑(Finsupp.mapRange.linearEquiv (Shrink.linearEquiv R R) ≪≫ₗ Finsupp.linearEquivFunOnFinite R R (Fin m))
⊢ Surjective ⇑f'
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: M : Type u_1
inst✝ : AddCommGroup M
a i : M
⊢ i ∈ (ℤ ∙ a).toAddSubgroup ↔ i ∈ AddSubgroup.zmultiples a

Tactic:
simp [Submodule.mem_span_singleton, AddSubgroup.mem_zmultiples_iff]

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

Goal state before:
pp: case inl
ι : Type u_4
R : ι → Type u_5
inst✝ : (i : ι) → Semiring (R i)
J : Ideal ((i : ι) → R i)
x : (i : ι) → R i
hxJ : x ∈ J
j : ι
I : Ideal (R j)
h : I.IsMaximal
le : comap (Pi.evalRingHom R j) I ≤ J
hxI : x ∉ comap (Pi.evalRingHom R j) I
r y : R j
hy : y ∈ I
eq : r * (Pi.evalRingHom R j) x + y = 1
⊢ 1 j = (update 0 j r * x + update 1 j y) j

Tactic:
simpa using

Goal state after:
case inl
ι : Type u_4
R : ι → Type u_5
inst✝ : (i : ι) → Semiring (R i)
J : Ideal ((i : ι) → R i)
x : (i : ι) → R i
hxJ : x ∈ J
j : ι
I : Ideal (R j)
h : I.IsMaximal
le : comap (Pi.evalRingHom R j) I ≤ J
hxI : x ∉ comap (Pi.evalRingHom R j) I
r y : R j
hy : y ∈ I
eq : r * (Pi.evalRingHom R j) x + y = 1
⊢ r * x j + y = 1
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
a : R
a0 : ¬a = 0
⊢ 0 / a = 0

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : EuclideanDomain R
a : R
a0 : ¬a = 0
⊢ 0 / a = 0
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
a : R
a0 : a ≠ 0
⊢ a / a = 1

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : EuclideanDomain R
a : R
a0 : a ≠ 0
⊢ a / a = 1
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
h : gcd a b = 0
⊢ a = 0 ∧ b = 0

Tactic:
simpa using

Goal state after:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
h : gcd a b = 0
⊢ a = 0 ∧ b = 0
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b c x✝¹ : R
x✝ : c ∣ 0
H : c ∣ x✝¹
⊢ c ∣ gcd 0 x✝¹

Tactic:
simpa using

Goal state after:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b c x✝¹ : R
x✝ : c ∣ 0
H : c ∣ x✝¹
⊢ c ∣ x✝¹
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case mp
R : Type u
S : Type v
inst✝³ : Semiring R
inst✝² : Semiring S
E : Type u_4
inst✝¹ : EquivLike E R S
inst✝ : RingEquivClass E R S
e : E
I : Ideal R
y : S
⊢ y ∈ map e I → ∃ x ∈ I, e x = y

Tactic:
intro h
    simp_rw [show map e I = _ from map_comap_of_equiv (RingEquivClass.toRingEquiv e : R ≃+* S)] at h
    exact ⟨(EquivLike.toEquiv e).symm y, h, (EquivLike.toEquiv e).apply_symm_apply y⟩

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

Goal state before:
pp: R : Type u
S : Type v
F : Type u_1
inst✝⁴ : Semiring R
inst✝³ : Semiring S
inst✝² : FunLike F R S
f : F
I✝ J : Ideal R
K✝ L : Ideal S
G : Type u_2
inst✝¹ : FunLike G S R
inst✝ : RingHomClass F R S
ι : Sort u_3
hf : Function.Bijective ⇑f
I : Ideal R
K x✝¹ x✝ : Ideal S
h :
  { toFun := comap f, invFun := map f, left_inv := ⋯, right_inv := ⋯ } x✝¹ ≤
    { toFun := comap f, invFun := map f, left_inv := ⋯, right_inv := ⋯ } x✝
this :
  map f ({ toFun := comap f, invFun := map f, left_inv := ⋯, right_inv := ⋯ } x✝¹) ≤
    map f ({ toFun := comap f, invFun := map f, left_inv := ⋯, right_inv := ⋯ } x✝)
⊢ x✝¹ ≤ x✝

Tactic:
simpa using

Goal state after:
R : Type u
S : Type v
F : Type u_1
inst✝⁴ : Semiring R
inst✝³ : Semiring S
inst✝² : FunLike F R S
f : F
I✝ J : Ideal R
K✝ L : Ideal S
G : Type u_2
inst✝¹ : FunLike G S R
inst✝ : RingHomClass F R S
ι : Sort u_3
hf : Function.Bijective ⇑f
I : Ideal R
K x✝¹ x✝ : Ideal S
h :
  { toFun := comap f, invFun := map f, left_inv := ⋯, right_inv := ⋯ } x✝¹ ≤
    { toFun := comap f, invFun := map f, left_inv := ⋯, right_inv := ⋯ } x✝
this :
  map f ({ toFun := comap f, invFun := map f, left_inv := ⋯, right_inv := ⋯ } x✝¹) ≤
    map f ({ toFun := comap f, invFun := map f, left_inv := ⋯, right_inv := ⋯ } x✝)
⊢ x✝¹ ≤ x✝
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case refine_1
R : Type u
S : Type v
F : Type u_1
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
I : Ideal S
φ : Ideal S ↪o Ideal R := ⋯
J : Ideal S
K : Ideal R
h : φ J < K
⊢ ¬map f K ≤ map f (φ J)

Tactic:
simpa using

Goal state after:
case refine_1
R : Type u
S : Type v
F : Type u_1
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
I : Ideal S
φ : Ideal S ↪o Ideal R := orderEmbeddingOfSurjective f hf
J : Ideal S
K : Ideal R
h : φ J < K
⊢ ¬K ≤ comap f J
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
N : Submodule R M
⊢ span R ({r} • ↑N) = r • N

Tactic:
simpa using

Goal state after:
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
N : Submodule R M
⊢ span R (r • ↑N) = r • N
Module: Mathlib.RingTheory.Ideal.Maps

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

Tactic:
simpa using

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

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

Tactic:
simpa using

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

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

Tactic:
simpa using

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

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
x y z : R
h1 : z ≠ 0
h2 : z ∣ y
⊢ (x * z + y) / z = x + y / z

Tactic:
mul_comm x z

Goal state after:
R : Type u
inst✝ : EuclideanDomain R
x y z : R
h1 : z ≠ 0
h2 : z ∣ y
⊢ (z * x + y) / z = x + y / z
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
x y z : R
h1 : z ≠ 0
h2 : z ∣ y
⊢ (x * z - y) / z = x - y / z

Tactic:
mul_comm x z

Goal state after:
R : Type u
inst✝ : EuclideanDomain R
x y z : R
h1 : z ≠ 0
h2 : z ∣ y
⊢ (z * x - y) / z = x - y / z
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 b : S
hb : b ≠ 0
⊢ e b ≠ 0

Tactic:
simpa using

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : EuclideanDomain R
inst✝ : CommRing S
e : S ≃+* R
a b : S
hb : b ≠ 0
⊢ ¬b = 0
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
r : R
⊢ r ∈ (span R s).annihilator ↔ ∀ (n : ↑s), r • ↑n = 0

Tactic:
rw [Submodule.mem_annihilator]
  constructor
  · intro h n
    exact h _ (Submodule.subset_span n.prop)
  · intro h n hn
    refine Submodule.span_induction ?_ ?_ ?_ ?_ hn
    · intro x hx
      exact h ⟨x, hx⟩
    · exact smul_zero _
    · intro x y _ _ hx hy
      rw [smul_add, hx, hy, zero_add]
    · intro a x _ hx
      rw [smul_comm, hx, smul_zero]

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

Tactic:
simpa using

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
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
j : Ideal S
hj : j ∈ map f '' A
y : S
hy : y ∈ map f (sInf A)
x : R
hx : x ∈ sInf A ∧ f x = y
⊢ y ∈ j

Tactic:
obtain ⟨J, hJ⟩ := (Set.mem_image _ _ _).mp hj

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
j : Ideal S
hj : j ∈ map f '' A
y : S
hy : y ∈ map f (sInf A)
x : R
hx : x ∈ sInf A ∧ f x = y
J : Ideal R
hJ : J ∈ A ∧ map f J = j
⊢ y ∈ j
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: 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
y : S
hy : y ∈ sInf (map f '' A)
x : R
hx : f x = y
⊢ ∀ I ∈ A, y ∈ map f I

Tactic:
simpa using

Goal state after:
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
y : S
hy : y ∈ sInf (map f '' A)
x : R
hx : f x = y
⊢ ∀ I ∈ A, y ∈ map f 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
A : Set (Ideal R)
f : F
hf : Function.Surjective ⇑f
h : ∀ J ∈ A, RingHom.ker f ≤ J
x : R
J : Submodule R R
hJ : J ∈ A
x' : R
hx' : x' ∈ J
hy : f x' ∈ sInf (map f '' A)
hx : f x = f x'
this✝ : ∀ I ∈ A, f x' ∈ map f I
this : x - x' ∈ J
⊢ x ∈ J

Tactic:
simpa using

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
x : R
J : Submodule R R
hJ : J ∈ A
x' : R
hx' : x' ∈ J
hy : f x' ∈ sInf (map f '' A)
hx : f x = f x'
this✝ : ∀ I ∈ A, f x' ∈ map f I
this : x - x' ∈ J
⊢ x ∈ J
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)

Tactic:
simpa using

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 (s.gcd * t.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) = ⊤

Tactic:
simpa using

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

Tactic:
rw [h, top_pow]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
I : Ideal R
n m : ℕ
hnI : I ^ n = 0
hmn : n ≤ m
x : R
hx : x ∈ I
⊢ x ^ m = 0

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : Semiring R
I : Ideal R
n m : ℕ
hnI : I ^ n = 0
hmn : n ≤ m
x : R
hx : x ∈ I
⊢ x ^ m = 0
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case hI
R : Type u
inst✝¹ : CommSemiring R
ι : Type u_2
inst✝ : Fintype ι
I : ι → R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
⊢ Set.univ.Pairwise (Function.onFun IsCoprime I)

Tactic:
Set.pairwise_univ

Goal state after:
case hI
R : Type u
inst✝¹ : CommSemiring R
ι : Type u_2
inst✝ : Fintype ι
I : ι → R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
⊢ Pairwise (Function.onFun IsCoprime I)
Module: Mathlib.Algebra.GCDMonoid.Finset

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

Tactic:
simpa using

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

Goal state before:
pp: case right
A : Type u_1
B : Type u_2
inst✝¹ : Ring A
inst✝ : Ring B
f : A →+* B
surj : Function.Surjective ⇑f
I : Ideal B
J : Ideal A
eq : comap f I = RingHom.ker f ⊔ J
x : B
x' : A
hx : x' ∈ RingHom.ker f ⊔ J
hx' : f x' = x
y : A
hy : y ∈ RingHom.ker f
z : A
hz : z ∈ J
hyz : y + z = x'
⊢ f z = x

Tactic:
simpa using

Goal state after:
case right
A : Type u_1
B : Type u_2
inst✝¹ : Ring A
inst✝ : Ring B
f : A →+* B
surj : Function.Surjective ⇑f
I : Ideal B
J : Ideal A
eq : comap f I = RingHom.ker f ⊔ J
x : B
x' : A
hx : x' ∈ RingHom.ker f ⊔ J
hx' : f x' = x
y : A
hy : y ∈ RingHom.ker f
z : A
hz : z ∈ J
hyz : y + z = x'
⊢ y ∈ RingHom.ker f
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
x : B
hx : x ∈ I
y : A
mem : y ∈ J
hy : f y = x
⊢ x ∈ map f J

Tactic:
simpa using

Goal state after:
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
x : B
hx : x ∈ I
y : A
mem : y ∈ J
hy : f y = x
⊢ f y ∈ map f J
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a b : α
h : normalize b = b
⊢ gcd a b = b ↔ b ∣ a

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a b : α
h : normalize b = b
⊢ gcd b a = b ↔ b ∣ a
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
⊢ a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a

Tactic:
simp_rw [← UniqueFactorizationMonoid.irreducible_iff_prime]
  apply WfDvdMonoid.exists_factors a

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
hf : factors a = 0
⊢ False

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
hf : factors a = 0
⊢ False
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

Goal state after:
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsPrime
s : Multiset R
⊢ s.prod ∈ I ↔ ∃ p ∈ s, p ∈ I
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a b : α
h : normalize b = b
⊢ lcm a b = b ↔ a ∣ b

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a b : α
h : normalize b = b
⊢ lcm a b = b ↔ a ∣ b
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case pos
R : Type u
inst✝ : CommSemiring R
I P : Ideal R
hP : P.IsPrime
n : ℕ
h : I ^ n ≤ P
hn : n = 0
⊢ I ≤ P

pp: case neg
R : Type u
inst✝ : CommSemiring R
I P : Ideal R
hP : P.IsPrime
n : ℕ
h : I ^ n ≤ P
hn : ¬n = 0
⊢ I ≤ P

Tactic:
· rw [hn, pow_zero, one_eq_top] at h
    exact fun ⦃_⦄ _ ↦ h Submodule.mem_top

Goal state after:
case neg
R : Type u
inst✝ : CommSemiring R
I P : Ideal R
hP : P.IsPrime
n : ℕ
h : I ^ n ≤ P
hn : ¬n = 0
⊢ I ≤ P
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : DecidableEq α
f : Associates α →* α
hinv : Function.RightInverse (⇑f) Associates.mk
a b : α
ha : a ≠ 0
hb : b ≠ 0
this : a * b * ↑(Classical.choose ⋯) = a * ↑(Classical.choose ⋯) * (b * ↑(Classical.choose ⋯))
⊢ a * b * ↑(Classical.choose ⋯) = a * b * (↑(Classical.choose ⋯) * ↑(Classical.choose ⋯))

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : DecidableEq α
f : Associates α →* α
hinv : Function.RightInverse (⇑f) Associates.mk
a b : α
ha : a ≠ 0
hb : b ≠ 0
this : a * b * ↑(Classical.choose ⋯) = a * ↑(Classical.choose ⋯) * (b * ↑(Classical.choose ⋯))
⊢ a * (b * ↑(Classical.choose ⋯)) = a * (b * (↑(Classical.choose ⋯) * ↑(Classical.choose ⋯)))