mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monad.Comonadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : HasCoreflexiveEqualizers C
inst✝¹ : F.ReflectsIsomorphisms
inst✝ : PreservesLimitOfIsCoreflexivePair F
this : ∀ (X : adj.toComonad.Coalgebra), IsIso ((comparisonAdjunction adj).counit.app X)
Y : C
⊢ IsIso ((comparisonAdjunction adj).unit.app Y)

Tactic:
rw [comparisonAdjunction_unit_app]

Goal state after:
C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : HasCoreflexiveEqualizers C
inst✝¹ : F.ReflectsIsomorphisms
inst✝ : PreservesLimitOfIsCoreflexivePair F
this : ∀ (X : adj.toComonad.Coalgebra), IsIso ((comparisonAdjunction adj).counit.app X)
Y : C
⊢ IsIso (limit.lift (parallelPair (G.map (F.map (adj.unit.app Y))) (adj.unit.app (G.obj (F.obj Y)))) (unitFork adj Y))
Module: Mathlib.CategoryTheory.Monad.Limits

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
R : D ⥤ C
inst✝ : Coreflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := ⋯
c : Cocone (F ⋙ R)
h : IsColimit c
this✝ : HasColimit (F ⋙ R)
this : HasColimit F
⊢ R.obj (colimit.cocone F).1 ≅ c.pt

Tactic:
letI := comonadicCreatesColimits.{v, v} R

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
R : D ⥤ C
inst✝ : Coreflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := empty D
c : Cocone (F ⋙ R)
h : IsColimit c
this✝¹ : HasColimit (F ⋙ R)
this✝ : HasColimit F
this : CreatesColimitsOfSize.{v, v, v₂, v₁, u₂, u₁} R := comonadicCreatesColimits R
⊢ R.obj (colimit.cocone F).1 ≅ c.pt
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ⟶ G.obj zero
e₁ : F.obj one ⟶ G.obj one
h₁ : F.map left ≫ e₀ = e₁ ≫ G.map left
h₂ : F.map right ≫ e₀ = e₁ ≫ G.map right
h₃ : F.map reflexion ≫ e₁ = e₀ ≫ G.map reflexion
D : Type u₂
inst✝ : Category.{v₂, u₂} D
H : C ⥤ D
⊢ (F ⋙ H).map left ≫ H.map e₀ = H.map e₁ ≫ (G ⋙ H).map left

Tactic:
by simp only [Functor.comp_obj, Functor.comp_map, ← Functor.map_comp, h₁]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
I J : Ideal S
p : Ideal R
P : Ideal S
inst✝ : Algebra R S
x : R
⊢ (algebraMap R (S ⧸ map (algebraMap R S) p)) x = (algebraMap (R ⧸ p) (S ⧸ map (algebraMap R S) p)) ((mk p) x)

Tactic:
Quotient.algebraMap_quotient_map_quotient,

Goal state after:
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
I J : Ideal S
p : Ideal R
P : Ideal S
inst✝ : Algebra R S
x : R
⊢ (algebraMap R (S ⧸ map (algebraMap R S) p)) x = (mk (map (algebraMap R S) p)) ((algebraMap R S) x)
Module: Mathlib.RingTheory.Ideal.IsPrimary

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
hi : I.radical.IsMaximal
x y : R
hxy : x * y ∈ I
h : I + span {y} = ⊤
⊢ x ∈ I ∨ y ∈ I.radical

Tactic:
rw [← span_singleton_le_iff_mem, ← mul_top (span {x}), ← h, mul_add,
        span_singleton_mul_span_singleton, add_le_iff, span_singleton_le_iff_mem]
      exact Or.inl ⟨mul_le_right, hxy⟩

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
hi : I.radical.IsMaximal
x y : R
hxy : x * y ∈ I
h : ¬I + span {y} = ⊤
⊢ x ∈ I ∨ y ∈ I.radical

Tactic:
· obtain ⟨m, hm, hy⟩ := exists_le_maximal (I + span {y}) h
      rw [add_le_iff, span_singleton_le_iff_mem, ← hm.isPrime.radical_le_iff] at hy
      exact Or.inr (hi.eq_of_le hm.ne_top hy.1 ▸ hy.2)

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
hp : I.IsPrime
hd : Disjoint ↑M ↑I
⊢ (Ideal.map (algebraMap R S) I).IsPrime

Tactic:
rw [isPrime_iff_isPrime_disjoint M S, under_map_of_isPrime_disjoint M S hp hd]
  exact ⟨hp, hd⟩

Goal state after:
Module: Mathlib.Algebra.Ring.Regular

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
h : ∀ (x y z : α), x * y = 1 → x * z = 1 → y = z
x y : α
eq : x * y = 1
⊢ 0 + 1 = 1

Tactic:
zero_add

Goal state after:
α : Type u_1
inst✝ : Ring α
h : ∀ (x y z : α), x * y = 1 → x * z = 1 → y = z
x y : α
eq : x * y = 1
⊢ 1 = 1
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
h : EssFiniteType R T
⊢ EssFiniteType S T

Tactic:
by
  rw [essFiniteType_iff] at h ⊢
  obtain ⟨σ, hσ⟩ := h
  use σ
  intro x
  obtain ⟨y, hy₁, hy₂, hy₃⟩ := hσ x
  simp_rw [← Algebra.adjoin_adjoin_of_tower R (S := S) (σ : Set T)]
  exact ⟨y, Algebra.subset_adjoin hy₁, hy₂, Algebra.subset_adjoin hy₃⟩

Goal state after:
Module: Mathlib.Algebra.Ring.Regular

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
h : ∀ (x y z : α), x * z = 1 → y * z = 1 → x = y
x y : α
eq : x * y = 1
⊢ 0 + 1 = 1

Tactic:
zero_add

Goal state after:
α : Type u_1
inst✝ : Ring α
h : ∀ (x y z : α), x * z = 1 → y * z = 1 → x = y
x y : α
eq : x * y = 1
⊢ 1 = 1
Module: Mathlib.RingTheory.LocalProperties.Basic

Goal state before:
pp: R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPc : StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ P
hPp : LocalizationPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
hPl : HoldsForLocalization fun {R S} [CommRing R] [CommRing S] ↦ P
M : Submonoid R
T : Submonoid S
R' : Type u
inst✝⁵ : CommRing R'
inst✝⁴ : Algebra R R'
inst✝³ : IsLocalization M R'
S' : Type u
inst✝² : CommRing S'
inst✝¹ : Algebra S S'
inst✝ : IsLocalization T S'
f : R →+* S
hy : M ≤ Submonoid.comap f T
hf : P f
⊢ Submonoid.map f M ≤ T

Tactic:
simpa [Submonoid.map_le_iff_le_comap]

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

Goal state before:
pp: m : Type u_1
R : Type u_3
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing R
s : m × m → R
⊢ (MvPolynomial.eval s) (mvPolynomialX m m R).det = (of fun i j ↦ s (i, j)).det

Tactic:
by
  rw [(MvPolynomial.eval s).map_det]
  congr 1
  ext i j
  simp [mvPolynomialX]

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

Goal state before:
pp: α : Type u_1
m : Type u_3
R : Type v
M N : Matrix m m R
b : m → α
inst✝¹ : LT α
inst✝ : AddZeroClass R
hM : M.BlockTriangular b
hN : N.BlockTriangular b
i j : m
h : b j < b i
⊢ 0 + 0 = 0

Tactic:
zero_add

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

Goal state before:
pp: m : Type u_3
R : Type v
M : Matrix m m R
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : LinearOrder m
h : M.IsUpperTriangular
this : DecidableEq R
⊢ ∏ a ∈ image id univ, (M.toSquareBlock id a).det = ∏ i, M i i

Tactic:
image_id,

Goal state after:
m : Type u_3
R : Type v
M : Matrix m m R
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : LinearOrder m
h : M.IsUpperTriangular
this : DecidableEq R
⊢ ∏ x, (M.toSquareBlock id x).det = ∏ i, M i i
Module: Mathlib.RingTheory.MatrixPolynomialAlgebra

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
k : ℕ
x : R
⊢ matPolyEquiv (single i j ((monomial k) x)) = (monomial k) (single i j x)

Tactic:
simp only [matPolyEquiv, AlgEquiv.trans_apply, matrixEquivTensor_apply_single]

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
k : ℕ
x : R
⊢ (polyEquivTensor R (Matrix n n R)).symm
      ((Algebra.TensorProduct.comm R R[X] (Matrix n n R)) ((monomial k) x ⊗ₜ[R] single i j 1)) =
    (monomial k) (single i j x)
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: n : Type u_1
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n 𝕜
⊢ ∃ L L' D, (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D

Tactic:
have e : n ≃ Fin (Fintype.card n) := Fintype.equivOfCardEq (by simp)

Goal state after:
n : Type u_1
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n 𝕜
e : n ≃ Fin (Fintype.card n)
⊢ ∃ L L' D, (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
Module: Mathlib.RingTheory.Polynomial.Nilpotent

Goal state before:
pp: R : Type u_1
r : R
inst✝ : Semiring R
n : ℕ
hnil : IsNilpotent r
⊢ IsNilpotent (C r * X ^ n)

Tactic:
by
  refine Commute.isNilpotent_mul_right (commute_X_pow _ _).symm ?_
  obtain ⟨m, hm⟩ := hnil
  refine ⟨m, ?_⟩
  rw [← C_pow, hm, C_0]

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

Goal state before:
pp: case refine_2.succ
R : Type u_1
inst✝ : CommRing R
P p : R[X]
r : R
hp₀ : p.coeff 0 = 0
x✝ : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (p.coeff i)
hpr : IsNilpotent (p + C r)
hr : IsNilpotent (C r)
i : ℕ
⊢ IsNilpotent ((p + C r).coeff (i + 1))

Tactic:
simp only [coeff_add, coeff_C_succ, add_zero]

Goal state after:
case refine_2.succ
R : Type u_1
inst✝ : CommRing R
P p : R[X]
r : R
hp₀ : p.coeff 0 = 0
x✝ : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (p.coeff i)
hpr : IsNilpotent (p + C r)
hr : IsNilpotent (C r)
i : ℕ
⊢ IsNilpotent (p.coeff (i + 1))
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
i j : n
⊢ (M.charmatrix i j).natDegree ≤ if i = j then 1 else 0

Tactic:
split_ifs with h <;> simp [h, natDegree_X_le]

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

Goal state before:
pp: R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h : p.FG
s : Set M
hs₁ : #↑s = p.spanRank
hs₂ : span R s = p
this : p.spanRank = ↑p.spanFinrank
⊢ toENat #↑s = ↑(toNat p.spanRank)

Tactic:
hs₁,

Goal state after:
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h : p.FG
s : Set M
hs₁ : #↑s = p.spanRank
hs₂ : span R s = p
this : p.spanRank = ↑p.spanFinrank
⊢ toENat p.spanRank = ↑(toNat p.spanRank)
Module: Mathlib.Algebra.Polynomial.Lifts

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
n : ℕ
⊢ (mapRingHom f) (X ^ n) = X ^ n

Tactic:
by
    simp only [coe_mapRingHom, map_pow, map_X]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
D : (n → R[X]) [⋀^n]→ₗ[R[X]] R[X] := detRowAlternating
⊢ (detRowAlternating (X • M.map ⇑C + 1)).coeff k =
    ∑ x ∈ powersetCard k univ, detRowAlternating (M.submatrix Subtype.val Subtype.val)

Tactic:
change (D (fun i => ((X : R[X]) • M.map C) i + (1 : Matrix n n R[X]) i)).coeff k = _

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
D : (n → R[X]) [⋀^n]→ₗ[R[X]] R[X] := detRowAlternating
⊢ (D fun i ↦ (X • M.map ⇑C) i + 1 i).coeff k =
    ∑ x ∈ powersetCard k univ, detRowAlternating (M.submatrix Subtype.val Subtype.val)
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
h3 : k ≤ k + l
⊢ ↑(i - l)! / (↑k ! * ↑(i - l - k)!) * (↑i ! / (↑l ! * ↑(i - l)!)) = ↑((k + l).choose k) * ↑(i.choose (k + l))

Tactic:
cast_choose ℚ h3,

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
h3 : k ≤ k + l
⊢ ↑(i - l)! / (↑k ! * ↑(i - l - k)!) * (↑i ! / (↑l ! * ↑(i - l)!)) =
    ↑(k + l)! / (↑k ! * ↑(k + l - k)!) * ↑(i.choose (k + l))
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k : ℕ
D : ℕ → R[X] →+ R[X] := fun k ↦ (hasseDeriv k).toAddMonoidHom
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
aux :
  ∀ x ∈ antidiagonal k,
    (monomial (m - x.1 + (n - x.2))) (↑(m.choose x.1) * r * (↑(n.choose x.2) * s)) =
      (monomial (m + n - k)) (↑(m.choose x.1) * ↑(n.choose x.2) * (r * s))
⊢ (monomial (m + n - k)) (↑((m + n).choose k) * (r * s)) =
    ∑ x ∈ antidiagonal k, (monomial (m - x.1 + (n - x.2))) (↑(m.choose x.1) * r * (↑(n.choose x.2) * s))

Tactic:
Finset.sum_congr rfl aux

Goal state after:
R : Type u_1
inst✝ : Semiring R
k : ℕ
D : ℕ → R[X] →+ R[X] := fun k ↦ (hasseDeriv k).toAddMonoidHom
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
aux :
  ∀ x ∈ antidiagonal k,
    (monomial (m - x.1 + (n - x.2))) (↑(m.choose x.1) * r * (↑(n.choose x.2) * s)) =
      (monomial (m + n - k)) (↑(m.choose x.1) * ↑(n.choose x.2) * (r * s))
⊢ (monomial (m + n - k)) (↑((m + n).choose k) * (r * s)) =
    ∑ x ∈ antidiagonal k, (monomial (m + n - k)) (↑(m.choose x.1) * ↑(n.choose x.2) * (r * s))
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: R : Type u_1
A : Type u_3
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : NoZeroDivisors R
alg : Algebra.IsAlgebraic R A
s : Finset A
this : Nontrivial R
r : A → R
hr : ∀ (x : A), r x ≠ 0
int : ∀ (x : A), IsIntegral R (r x • x)
x✝ : A
h : x✝ ∈ s
⊢ IsIntegral R ((∏ x ∈ s.erase x✝, r x) • r x✝ • x✝)

Tactic:
exact (int _).smul _

Goal state after:
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
a✝ : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun x ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun i r ↦ X ^ i * reflect N r
this : ∀ (i : ℕ), (aeval t) (reflect N (q.coeff i)) = t ^ N * (aeval s) (q.coeff i)
⊢ eval₂ (algebraMap R S) t q' = 0

Tactic:
trans t ^ N * q.sum (t ^ · * φ.toRingHom ·)
    · simp [φ, q', Polynomial.sum, ← aeval_def, this, mul_left_comm _ (t ^ N), ← Finset.mul_sum]
    · simp_rw [mul_comm (t ^ _), ← eval₂_eq_sum, hqt, zero_mul]

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: case hgt
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
M : Submodule R R
hgt : ∀ J > M, ∃ Z, (Multiset.map asIdeal Z).prod ≤ J
⊢ ∃ Z, (Multiset.map asIdeal Z).prod ≤ M

Tactic:
| hgt M hgt =>

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: case hgt
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
M : Submodule A A
hgt : ∀ J > M, J ≠ ⊥ → ∃ Z, (Multiset.map asIdeal Z).prod ≤ J ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
h_nzI : M ≠ ⊥
⊢ ∃ Z, (Multiset.map asIdeal Z).prod ≤ M ∧ (Multiset.map asIdeal Z).prod ≠ ⊥

Tactic:
| hgt M hgt =>

Goal state after:
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Module.FaithfullyFlat A B
I : Ideal A
⊢ Function.Injective (⇑(↑A ↑↑(quotIdealMapEquivTensorQuot B I).symm) ∘ ⇑((TensorProduct.mk A B (A ⧸ I)) 1))

Tactic:
← LinearEquiv.restrictScalars_toLinearMap

Goal state after:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Module.FaithfullyFlat A B
I : Ideal A
⊢ Function.Injective
    (⇑↑(LinearEquiv.restrictScalars A ↑(quotIdealMapEquivTensorQuot B I).symm) ∘ ⇑((TensorProduct.mk A B (A ⧸ I)) 1))
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: ι : Type u_3
R : ι → Type u_2
inst✝² : (i : ι) → CommSemiring (R i)
inst✝¹ : Infinite ι
inst✝ : ∀ (i : ι), Nontrivial (R i)
⊢ ∀ (c : (i : ι) → R i) {x : (i : ι) → R i},
    x ∈ (AddMonoidHom.mrange DFinsupp.coeFnAddMonoidHom).carrier →
      c • x ∈ (AddMonoidHom.mrange DFinsupp.coeFnAddMonoidHom).carrier

Tactic:
by
      rintro r _ ⟨x, rfl⟩
      refine ⟨.mk x.support fun i ↦ r i * x i, funext fun i ↦ show dite _ _ _ = _ from ?_⟩
      simp_rw +instances [DFinsupp.coeFnAddMonoidHom]
      refine dite_eq_left_iff.mpr fun h ↦ ?_
      rw [DFinsupp.notMem_support_iff.mp h, mul_zero]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b c : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
⊢ (↑a).2 * (↑b).2 + (0 + (↑a).2 * (↑b).1 * (↑c).2) = (↑a).2 * (↑b).2 + (↑a).2 * (↑b).1 * (↑c).2

Tactic:
zero_add

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b c : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
⊢ (↑((a ⊔ b) ⊓ (a ⊔ c))).2 = (↑(a ⊔ b ⊓ c)).2

Tactic:
simp_rw +instances [(· ⊔ ·), (· ⊓ ·), (·ᶜ), SemilatticeSup.sup, add_mul, mul_add,
      mul_mul_mul_comm _ b.1.1, (IsIdempotentElem.of_mul_add a.2.1 a.2.2).2.eq, ← mul_assoc, a.2.1,
      zero_mul, zero_add]

Goal state after:
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: case refine_2
R : Type u_1
inst✝³ : CommSemiring R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
q : Ideal R
hqp : q.IsPrime
inst✝ : IsLocalization.AtPrime A q
I : Ideal R
hIq : q ∈ I.minimalPrimes
this✝ : IsLocalRing A
J : Ideal A
hJ : J ∈ Ideal.under R ⁻¹' I.minimalPrimes
this : ¬J = ⊤
⊢ Ideal.under R J ≤ q

Tactic:
← ne_eq,

Goal state after:
case refine_2
R : Type u_1
inst✝³ : CommSemiring R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
q : Ideal R
hqp : q.IsPrime
inst✝ : IsLocalization.AtPrime A q
I : Ideal R
hIq : q ∈ I.minimalPrimes
this✝ : IsLocalRing A
J : Ideal A
hJ : J ∈ Ideal.under R ⁻¹' I.minimalPrimes
this : J ≠ ⊤
⊢ Ideal.under R J ≤ q
Module: Mathlib.Topology.Compactness.Bases

Goal state before:
pp: X : Type u_1
ι : Type u_2
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
U : Set X
⊢ IsCompact U ∧ IsOpen U ↔ ∃ s, s.Finite ∧ U = ⋃ i ∈ s, b i

Tactic:
constructor
  · exact fun ⟨h₁, h₂⟩ ↦ eq_finite_iUnion_of_isTopologicalBasis_of_isCompact_open _ hb U h₁ h₂
  · rintro ⟨s, hs, rfl⟩
    constructor
    · exact hs.isCompact_biUnion fun i _ => hb' i
    · exact isOpen_biUnion fun i _ => hb.isOpen (Set.mem_range_self _)

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: ι : Type u_5
R : ι → Type u_4
inst✝² : (i : ι) → CommSemiring (R i)
inst✝¹ : ∀ (i : ι), Nontrivial (R i)
inst✝ : Infinite ι
surj : Function.Surjective ⇑(toPiLocalization ((i : ι) → R i))
⊢ Function.Surjective ⇑(MaximalSpectrum.toPiLocalization ((i : ι) → R i))

Tactic:
by
    rw [← AlgHom.coe_toRingHom, ← piLocalizationToMaximal_comp_toPiLocalization]
    exact (piLocalizationToMaximal_surjective _).comp surj

Goal state after:
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
hf : ∀ (i : ι), GeneralizingMap ((U i).carrier.restrictPreimage f)
x : α
y : β
h✝ : (fun x1 x2 ↦ x1 ⤳ x2) y (f x)
i : ι
hx : f x ∈ U i
h : ⟨y, ⋯⟩ ⤳ (U i).carrier.restrictPreimage f ⟨x, hx⟩
a : ↑(f ⁻¹' (U i).carrier)
ha : a ⤳ ⟨x, hx⟩
heq : (U i).carrier.restrictPreimage f a = ⟨y, ⋯⟩
⊢ (fun x1 x2 ↦ x1 ⤳ x2) (↑a) x

Tactic:
rwa [subtype_specializes_iff] at ha

Goal state after:
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens α
hU : IsOpenCover U
hf : ∀ (i : ι), IsOpenMap (f ∘ Subtype.val)
V : Set α
hV : IsOpen[inst✝¹] V
⊢ f '' V = ⋃ i, f ∘ Subtype.val '' Subtype.val ⁻¹' V

Tactic:
Set.image_comp,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens α
hU : IsOpenCover U
hf : ∀ (i : ι), IsOpenMap (f ∘ Subtype.val)
V : Set α
hV : IsOpen[inst✝¹] V
⊢ f '' V = ⋃ i, f '' Subtype.val '' Subtype.val ⁻¹' V
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: case inl
α✝ : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α✝
inst✝ : TopologicalSpace β
α : Type u_3
s : Set (CofiniteTopology α)
f : Ultrafilter (CofiniteTopology α)
hs : s ∈ ↑f
hf : ↑f ≤ Filter.cofinite
⊢ ∃ x ∈ s, ↑f ≤ pure x ∨ ↑f ≤ Filter.cofinite

pp: case inr
α✝ : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α✝
inst✝ : TopologicalSpace β
α : Type u_3
s : Set (CofiniteTopology α)
a : CofiniteTopology α
hs : s ∈ ↑(pure a)
⊢ ∃ x ∈ s, ↑(pure a) ≤ pure x ∨ ↑(pure a) ≤ Filter.cofinite

Tactic:
· rcases Filter.nonempty_of_mem hs with ⟨a, ha⟩
    exact ⟨a, ha, Or.inr hf⟩

Goal state after:
case inr
α✝ : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α✝
inst✝ : TopologicalSpace β
α : Type u_3
s : Set (CofiniteTopology α)
a : CofiniteTopology α
hs : s ∈ ↑(pure a)
⊢ ∃ x ∈ s, ↑(pure a) ≤ pure x ∨ ↑(pure a) ≤ Filter.cofinite
Module: Mathlib.Topology.Constructible

Goal state before:
pp: case sdiff
X : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
P : (s : Set X) → IsConstructible s → Prop
inst✝¹ : QuasiSeparatedSpace X
ι : Type u_4
inst✝ : Nonempty ι
b : ι → Set X
basis : IsTopologicalBasis (range b)
isCompact_basis : ∀ (i : ι), IsCompact (b i)
sdiff : ∀ (i : ι) (s : Set ι) (hs : s.Finite), P (b i \ ⋃ j ∈ s, b j) ⋯
union : ∀ (s : Set X) (hs : IsConstructible s) (t : Set X) (ht : IsConstructible t), P s hs → P t ht → P (s ∪ t) ⋯
s✝ : Set X
this : ∀ (U : Set X), IsCompact U ∧ IsOpen[inst✝³] U ↔ ∃ s, s.Finite ∧ U = ⋃ i ∈ s, b i
s : Set ι
hs : s.Finite
hU : ⋃ i ∈ s, b i ∈ {U | IsOpen[inst✝³] U ∧ IsRetrocompact U}
t : Set ι
ht : t.Finite
hV : ⋃ i ∈ t, b i ∈ {U | IsOpen[inst✝³] U ∧ IsRetrocompact U}
⊢ P (⋃ i ∈ s, b i \ ⋃ i ∈ t, b i) ⋯

Tactic:
induction s, hs using Set.Finite.induction_on with

Goal state after:
Module: Mathlib.RingTheory.Derivation.ToSquareZero

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
inst✝¹ : Algebra A B
hI✝ : I ^ 2 = ⊥
inst✝ : IsScalarTower R A B
hI : I ^ 2 = ⊥
f : Derivation R A ↥I
⊢ 0 + 1 = 1

Tactic:
zero_add

Goal state after:
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
inst✝¹ : Algebra A B
hI✝ : I ^ 2 = ⊥
inst✝ : IsScalarTower R A B
hI : I ^ 2 = ⊥
f : Derivation R A ↥I
⊢ 1 = 1
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.Flat
⊢ GeneralizingMap (comap f)

Tactic:
algebraize [f]
  change GeneralizingMap (comap (algebraMap R S))
  rw [← Algebra.HasGoingDown.iff_generalizingMap_primeSpectrumComap]
  infer_instance

Goal state after:
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case pos
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
le : b.factorization p ≤ a.factorization p
⊢ p ^ (a.lcm b).factorization p ∣ p ^ a.factorization p

Tactic:
rw [factorization_lcm ha hb]; apply pow_dvd_pow; exact sup_le le_rfl le

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ IsPreirreducible (zeroLocus ↑I) ↔
    ∀ (x y : Ideal R),
      zeroLocus ↑I ⊆ zeroLocus ↑x ∪ zeroLocus ↑y → zeroLocus ↑I ⊆ zeroLocus ↑x ∨ zeroLocus ↑I ⊆ zeroLocus ↑y

Tactic:
simp_rw [isPreirreducible_iff_isClosed_union_isClosed, isClosed_iff_zeroLocus_ideal]

Goal state after:
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ (∀ (z₁ z₂ : Set (PrimeSpectrum R)),
      (∃ I, z₁ = zeroLocus ↑I) →
        (∃ I, z₂ = zeroLocus ↑I) → zeroLocus ↑I ⊆ z₁ ∪ z₂ → zeroLocus ↑I ⊆ z₁ ∨ zeroLocus ↑I ⊆ z₂) ↔
    ∀ (x y : Ideal R),
      zeroLocus ↑I ⊆ zeroLocus ↑x ∪ zeroLocus ↑y → zeroLocus ↑I ⊆ zeroLocus ↑x ∨ zeroLocus ↑I ⊆ zeroLocus ↑y