mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ℕ
⊢ (1 + X • M.map ⇑C).det.coeff k = ∑ s ∈ powersetCard k univ, (M.submatrix Subtype.val Subtype.val).det

Tactic:
by
  simp only [det]
  let D := (detRowAlternating : (n → R[X]) [⋀^n]→ₗ[R[X]] R[X])
  rw [add_comm]
  change (D (fun i => ((X : R[X]) • M.map C) i + (1 : Matrix n n R[X]) i)).coeff k = _
  conv_lhs => rw [show (fun i ↦ ((X : R[X]) • M.map C) i + (1 : Matrix n n R[X]) i) =
      (fun i => ((X : R[X]) • M.map C) i) + (fun i => (1 : Matrix n n R[X]) i) from rfl]
  conv_lhs => rw [D.map_add_univ]
  have h_map : ∀ s : Finset n,
        (s.piecewise (fun i ↦ (M.map C) i)
          (fun i ↦ (1 : Matrix n n R[X]) i) : Matrix n n R[X]) =
        Matrix.map (s.piecewise M (1 : Matrix n n R)) C := by
      intro s; ext i j
      simp only [Finset.piecewise, Matrix.map_apply]
      split_ifs with h <;> simp [Matrix.one_apply]
  have h_det : ∀ s : Finset n,
      D (s.piecewise (fun i ↦ (M.map C) i)
        (fun i ↦ (1 : Matrix n n R[X]) i)) =
      C (det (s.piecewise M (1 : Matrix n n R))) := by
    intro s; change det _ = _
    rw [h_map]; exact (RingHom.map_det C _).symm
  calc (∑ s : Finset n, D (Finset.piecewise s (fun i ↦ ((X : R[X]) • M.map C) i)
            (fun i ↦ (1 : Matrix n n R[X]) i))).coeff k
      _ = (∑ s : Finset n, (X : R[X]) ^ s.card •
            D (s.piecewise (fun i ↦ (M.map C) i)
              (fun i ↦ (1 : Matrix n n R[X]) i))).coeff k := by
        congr 2 with s
        have h_smul : s.piecewise (fun i ↦ ((X : R[X]) • M.map C) i)
            (fun i ↦ (1 : Matrix n n R[X]) i) =
            fun i => (if i ∈ s then (X : R[X]) else 1) •
              s.piecewise (fun i ↦ (M.map C) i) (fun i ↦ (1 : Matrix n n R[X]) i) i := by
          funext i j
          simp only [piecewise, Pi.smul_apply, smul_eq_mul, ite_mul, one_mul]
          split_ifs <;> rfl
        rw [h_smul, D.map_smul_univ]
        congr 1
        simp only [Finset.prod_ite_mem, Finset.univ_inter, Finset.prod_const]
      _ = ∑ s : Finset n, ((X : R[X]) ^ s.card •
            D (Finset.piecewise s (fun i ↦ (M.map C) i)
              (fun i ↦ (1 : Matrix n n R[X]) i))).coeff k := by
        simp only [Polynomial.finsetSum_coeff]
      _ = _ := by
        simp_rw [h_det, smul_eq_mul, mul_comm (X ^ _) (C _)]
        simp_rw [C_mul_X_pow_eq_monomial, coeff_monomial]
        rw [← Finset.sum_filter]
        have h_set : Finset.univ.filter (fun s : Finset n => s.card = k) =
            Finset.univ.powersetCard k := by
          ext s; simp [Finset.mem_powersetCard]
        rw [h_set]
        exact Finset.sum_congr rfl fun s _ => det_piecewise_one_eq_submatrix_det M s

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

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommSemiring R
p q : R[X]
r : R
inst✝ : NoZeroDivisors R
hp : ¬p = 0
⊢ (p * q).scaleRoots r = p.scaleRoots r * q.scaleRoots r

Tactic:
by_cases hq : q = 0

Goal state after:
case pos
R : Type u_1
inst✝¹ : CommSemiring R
p q : R[X]
r : R
inst✝ : NoZeroDivisors R
hp : ¬p = 0
hq : q = 0
⊢ (p * q).scaleRoots r = p.scaleRoots r * q.scaleRoots r

case neg
R : Type u_1
inst✝¹ : CommSemiring R
p q : R[X]
r : R
inst✝ : NoZeroDivisors R
hp : ¬p = 0
hq : ¬q = 0
⊢ (p * q).scaleRoots r = p.scaleRoots r * q.scaleRoots r
Module: Mathlib.RingTheory.TensorProduct.MvPolynomial

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
σ : Type u_1
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
i✝ : σ
⊢ ((AlgHom.restrictScalars R ↑(algebraTensorAlgEquiv R A).symm).comp (mapAlgHom (Algebra.ofId R A))) (X i✝) =
    Algebra.TensorProduct.includeRight (X i✝)

Tactic:
simp [mapAlgHom, algebraTensorAlgEquiv, X, monomial]

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

Goal state before:
pp: case inl
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
hp : p.Splits
r : R
h✝ : Subsingleton R
⊢ (p.scaleRoots r).Splits

Tactic:
Subsingleton.elim (p.scaleRoots r) p

Goal state after:
case inl
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
hp : p.Splits
r : R
h✝ : Subsingleton R
⊢ p.Splits
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: case inl
R : Type u_1
inst✝ : CommRing R
p : R[X]
r a : R
hr : IsLeftRegular r
h✝ : Subsingleton R
⊢ rootMultiplicity (r * a) (p.scaleRoots r) = rootMultiplicity a p

Tactic:
simp [Subsingleton.elim p 0]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf✝ : f.Splits
hf0 : ¬f.leadingCoeff = 0
m : Multiset R
hm : f = C f.leadingCoeff * (Multiset.map (fun x ↦ X - C x) m).prod
hf : f.roots = m
⊢ f = C f.leadingCoeff * (Multiset.map (fun x ↦ X - C x) f.roots).prod

Tactic:
by rwa [hf]

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra R B
inst✝⁷ : Algebra A B
inst✝⁶ : IsIntegralClosure A R B
S : Type u_4
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : Algebra S B
inst✝² : IsScalarTower R S B
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
isIntegral : Algebra.IsIntegral R S
⊢ mk' A ((algebraMap S B) 0) ⋯ = 0

Tactic:
simp only [map_zero, mk'_zero]

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

Goal state before:
pp: R : Type u_1
inst✝ : Field R
f : R[X]
a b : R
hg : (C a * X + C b).natDegree = 1
hf : (f.comp (C a * X + C b)).Splits
ha : a ≠ 0
⊢ f = f.comp X

Tactic:
comp_X

Goal state after:
R : Type u_1
inst✝ : Field R
f : R[X]
a b : R
hg : (C a * X + C b).natDegree = 1
hf : (f.comp (C a * X + C b)).Splits
ha : a ≠ 0
⊢ f = f
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
g : R →+* R ⧸ Ideal.comap f I := Ideal.Quotient.mk (Ideal.comap f I)
this : (Ideal.quotientMap I f ⋯).comp g = (Ideal.Quotient.mk I).comp f
⊢ (Ideal.quotientMap I f ⋯).IsIntegral ↔ ((Ideal.Quotient.mk I).comp f).IsIntegral

Tactic:
refine ⟨fun h => ?_, fun h => RingHom.IsIntegral.tower_top g _ (this ▸ h)⟩

Goal state after:
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
g : R →+* R ⧸ Ideal.comap f I := Ideal.Quotient.mk (Ideal.comap f I)
this : (Ideal.quotientMap I f ⋯).comp g = (Ideal.Quotient.mk I).comp f
h : (Ideal.quotientMap I f ⋯).IsIntegral
⊢ ((Ideal.Quotient.mk I).comp f).IsIntegral
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝ : Field R
f : R[X]
x : R
h₁ : f.natDegree = 2
h₂ : eval x f = 0
h : (f /ₘ (X - C x)).natDegree = 1
⊢ ((X - C x) * (f /ₘ (X - C x))).Splits

Tactic:
splits_mul (X_sub_C_ne_zero x) (by aesop)

Goal state after:
R : Type u_1
inst✝ : Field R
f : R[X]
x : R
h₁ : f.natDegree = 2
h₂ : eval x f = 0
h : (f /ₘ (X - C x)).natDegree = 1
⊢ (X - C x).Splits ∧ (f /ₘ (X - C x)).Splits
Module: Mathlib.RingTheory.Ideal.GoingUp

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : Ideal R[X]
⊢ comap (mapRingHom (Quotient.mk (comap C P))) ⊥ ≤ P

Tactic:
refine fun p hp =>
    polynomial_mem_ideal_of_coeff_mem_ideal P p fun n => Ideal.Quotient.eq_zero_iff_mem.mp ?_

Goal state after:
R : Type u_1
inst✝ : CommRing R
P : Ideal R[X]
p : R[X]
hp : p ∈ comap (mapRingHom (Quotient.mk (comap C P))) ⊥
n : ℕ
⊢ (Quotient.mk (comap C P)) (p.coeff n) = 0
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: R : Type u_5
S : Type u_6
Sₘ : Type u_7
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing Sₘ
inst✝⁴ : Algebra R S
inst✝³ : Algebra S Sₘ
inst✝² : Algebra R Sₘ
inst✝¹ : IsScalarTower R S Sₘ
r : S
hr : IsIntegral R r
inst✝ : Away r Sₘ
x : S
a : ↥(Submonoid.powers r)
hx : IsIntegral R (mk' Sₘ x a)
⊢ ∃ n, IsIntegral R (r ^ n * x)

Tactic:
by
  refine IsLocalization.Away.exists_isIntegral_mul_of_isIntegral_algebraMap (Sₘ := Sₘ) hr ?_
  obtain ⟨_, ⟨n, rfl⟩⟩ := a
  convert! (hr.pow n).algebraMap.mul hx
  exact (mk'_spec'_mk ..).symm

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

Goal state before:
pp: case pos
R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
hz : IsAlgebraic R z
inj : Function.Injective ⇑(algebraMap R A)
⊢ ∃ y, y ≠ 0 ∧ IsIntegral R (y • z)

Tactic:
have ⟨p, p_ne_zero, px⟩ := hz

Goal state after:
case pos
R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
hz : IsAlgebraic R z
inj : Function.Injective ⇑(algebraMap R A)
p : R[X]
p_ne_zero : p ≠ 0
px : (aeval z) p = 0
⊢ ∃ y, y ≠ 0 ∧ IsIntegral R (y • z)
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: case mpr.refine_1
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
P : Ideal S
inst✝ : P.IsPrime
H : ∀ (s : S), ∃ x r, ∃ c ∉ P, f r ∉ P ∧ c * f r * s = c * f x
y✝ : Localization.AtPrime P
x✝ : S × ↥P.primeCompl
y t : S
h : t ∈ P.primeCompl
yx ys : R
yc : S
hyc : yc ∉ P
hy : f ys ∉ P
ey : yc * f ys * y = yc * f yx
tx ts : R
yt : S
hyt : yt ∉ P
ht : f ts ∉ P
et : yt * f ts * t = yt * f tx
⊢ tx ∈ (Ideal.comap f P).primeCompl

pp: case mpr.refine_2
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
P : Ideal S
inst✝ : P.IsPrime
H : ∀ (s : S), ∃ x r, ∃ c ∉ P, f r ∉ P ∧ c * f r * s = c * f x
y✝ : Localization.AtPrime P
x✝ : S × ↥P.primeCompl
y t : S
h : t ∈ P.primeCompl
yx ys : R
yc : S
hyc : yc ∉ P
hy : f ys ∉ P
ey : yc * f ys * y = yc * f yx
tx ts : R
yt : S
hyt : yt ∉ P
ht : f ts ∉ P
et : yt * f ts * t = yt * f tx
⊢ (Localization.localRingHom (Ideal.comap f P) P f ⋯) (Localization.mk (yx * ts) ⟨ys * tx, ⋯⟩) =
    Localization.mk y ⟨t, h⟩

Tactic:
· exact fun H ↦ mul_mem (P.primeCompl.mul_mem hyt ht) h (et ▸ Ideal.mul_mem_left _ yt H)

Goal state after:
case mpr.refine_2
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
P : Ideal S
inst✝ : P.IsPrime
H : ∀ (s : S), ∃ x r, ∃ c ∉ P, f r ∉ P ∧ c * f r * s = c * f x
y✝ : Localization.AtPrime P
x✝ : S × ↥P.primeCompl
y t : S
h : t ∈ P.primeCompl
yx ys : R
yc : S
hyc : yc ∉ P
hy : f ys ∉ P
ey : yc * f ys * y = yc * f yx
tx ts : R
yt : S
hyt : yt ∉ P
ht : f ts ∉ P
et : yt * f ts * t = yt * f tx
⊢ (Localization.localRingHom (Ideal.comap f P) P f ⋯) (Localization.mk (yx * ts) ⟨ys * tx, ⋯⟩) =
    Localization.mk y ⟨t, h⟩
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: case mp
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun q ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
this : map (algebraMap R (Localization.AtPrime p)) p ≤ (map (algebraMap R (Localization.AtPrime p)) I).radical
n : ℕ
a : ↥I
b : ↥p.primeCompl
hn : (algebraMap R (Localization.AtPrime p)) (x ^ n * ↑(a, b).2) = (algebraMap R (Localization.AtPrime p)) ↑(a, b).1
⊢ ∃ y ∉ I.radical, x * y ∈ I.radical

Tactic:
IsLocalization.eq_iff_exists p.primeCompl

Goal state after:
case mp
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun q ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
this : map (algebraMap R (Localization.AtPrime p)) p ≤ (map (algebraMap R (Localization.AtPrime p)) I).radical
n : ℕ
a : ↥I
b : ↥p.primeCompl
hn : ∃ c, ↑c * (x ^ n * ↑(a, b).2) = ↑c * ↑(a, b).1
⊢ ∃ y ∉ I.radical, x * y ∈ I.radical
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a✝ b✝ : α
⊢ le a✝ (sup a✝ b✝)

Tactic:
simp [eq_le, eq_sup]

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a✝ b✝ : α
⊢ le b✝ (sup a✝ b✝)

Tactic:
simp [eq_le, eq_sup]

Goal state after:
Module: Mathlib.Topology.Compactness.Bases

Goal state before:
pp: case mpr
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
⊢ (∃ s, s.Finite ∧ U = ⋃ i ∈ s, b i) → IsCompact U ∧ IsOpen U

Tactic:
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.Order.Copy

Goal state before:
pp: α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
⊢ ∀ (a b c : α), le a b → le a c → le a (inf b c)

Tactic:
by intro _ _ _ hac hbc; simp_rw [eq_le] at hac hbc ⊢; simp [eq_inf, hac, hbc]

Goal state after:
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
ι : Sort u_5
s : ι → Opens α
⊢ ↑(⨆ i, s i) = ⋃ i, ↑(s i)

Tactic:
simp [iSup]

Goal state after:
Module: Mathlib.Topology.LocallyClosed

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ coborder s = (frontier s)ᶜ ↔ IsOpen[inst✝] s

Tactic:
simp_rw [coborder_eq_union_frontier_compl, union_eq_right, subset_compl_iff_disjoint_left,
    disjoint_frontier_iff_isOpen]

Goal state after:
Module: Mathlib.Topology.Spectral.Prespectral

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PrespectralSpace X
Z U₁ U₂ : Set X
hU₁ : ∀ a ∈ U₁, ∃ t ∈ {U | IsOpen[inst✝¹] U ∧ IsCompact U}, a ∈ t ∧ t ⊆ U₁
hU₂ : ∀ a ∈ U₂, ∃ t ∈ {U | IsOpen[inst✝¹] U ∧ IsCompact U}, a ∈ t ∧ t ⊆ U₂
hU₁Z : (Z ∩ U₁).Nonempty
hU₂Z : (Z ∩ U₂).Nonempty
hU₁₂ : Z ∩ (U₁ ∩ U₂) ⊆ ∅
x₁ : X
hx₁ : x₁ ∈ U₁ ∧ x₁ ∈ Z ∧ x₁ ∉ U₂
x₂ : X
hx₂ : x₂ ∈ U₂ ∧ x₂ ∈ Z ∧ x₂ ∉ U₁
W₁ : Set X
hW₁ : W₁ ∈ {U | IsOpen[inst✝¹] U ∧ IsCompact U} ∧ x₁ ∈ W₁ ∧ W₁ ⊆ U₁
W₂ : Set X
hW₂ : W₂ ∈ {U | IsOpen[inst✝¹] U ∧ IsCompact U} ∧ x₂ ∈ W₂ ∧ W₂ ⊆ U₂
⊢ IsCompact W₂ᶜᶜ

Tactic:
by simp [hW₂.1.2]

Goal state after:
Module: Mathlib.RingTheory.RingHom.FaithfullyFlat

Goal state before:
pp: ⊢ IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ FaithfullyFlat

Tactic:
refine .mk respectsIso (fun R S T _ _ _ _ _ _ ↦ show (algebraMap _ _).FaithfullyFlat from ?_)
  rw [faithfullyFlat_algebraMap_iff] at *
  infer_instance

Goal state after:
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
hR : IsField R
f : R →+* S
this✝ : Algebra R S := f.toAlgebra
this : Field R := hR.toField
⊢ f.Flat

Tactic:
rw [← f.algebraMap_toAlgebra, RingHom.flat_algebraMap_iff]

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
hR : IsField R
f : R →+* S
this✝ : Algebra R S := f.toAlgebra
this : Field R := hR.toField
⊢ Module.Flat R S
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra S A
inst✝⁸ : IsScalarTower R S A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R B
inst✝⁵ : CommRing C
inst✝⁴ : Algebra R C
inst✝³ : Algebra S C
inst✝² : IsScalarTower R S C
inst✝¹ : CommRing D
inst✝ : Algebra R D
f : A →ₐ[S] C
g : B →ₐ[R] D
hf : f.Flat
hg : g.Flat
heq :
  Algebra.TensorProduct.map f g =
    (Algebra.TensorProduct.map f (AlgHom.id R D)).comp (Algebra.TensorProduct.map (AlgHom.id S A) g)
this :
  AlgHom.restrictScalars R (Algebra.TensorProduct.map f (AlgHom.id R D)) =
    (↑(Algebra.TensorProduct.comm R D C)).comp
      ((Algebra.TensorProduct.lTensor D (AlgHom.restrictScalars R f)).comp ↑(Algebra.TensorProduct.comm R A D))
⊢ (↑((Algebra.TensorProduct.lTensor D (AlgHom.restrictScalars R f)).comp ↑(Algebra.TensorProduct.comm R A D))).Flat

Tactic:
change RingHom.Flat (RingHom.comp (Algebra.TensorProduct.lTensor D
      (AlgHom.restrictScalars R f)).toRingHom _)

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra S A
inst✝⁸ : IsScalarTower R S A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R B
inst✝⁵ : CommRing C
inst✝⁴ : Algebra R C
inst✝³ : Algebra S C
inst✝² : IsScalarTower R S C
inst✝¹ : CommRing D
inst✝ : Algebra R D
f : A →ₐ[S] C
g : B →ₐ[R] D
hf : f.Flat
hg : g.Flat
heq :
  Algebra.TensorProduct.map f g =
    (Algebra.TensorProduct.map f (AlgHom.id R D)).comp (Algebra.TensorProduct.map (AlgHom.id S A) g)
this :
  AlgHom.restrictScalars R (Algebra.TensorProduct.map f (AlgHom.id R D)) =
    (↑(Algebra.TensorProduct.comm R D C)).comp
      ((Algebra.TensorProduct.lTensor D (AlgHom.restrictScalars R f)).comp ↑(Algebra.TensorProduct.comm R A D))
⊢ ((Algebra.TensorProduct.lTensor D (AlgHom.restrictScalars R f)).comp ↑↑(Algebra.TensorProduct.comm R A D)).Flat
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x y : PrimeSpectrum R
⊢ x ≤ y ↔ y ∈ closure {x}

Tactic:
← asIdeal_le_asIdeal,

Goal state after:
R : Type u
inst✝ : CommSemiring R
x y : PrimeSpectrum R
⊢ x.asIdeal ≤ y.asIdeal ↔ y ∈ closure {x}
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
x y : PrimeSpectrum R
h : x ≤ y
a : R
ha : a ∈ y.asIdeal.primeCompl
⊢ IsUnit ((algebraMap R (Localization.AtPrime x.asIdeal)) ↑⟨a, ha⟩)

Tactic:
← asIdeal_le_asIdeal,

Goal state after:
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
x y : PrimeSpectrum R
h : x.asIdeal ≤ y.asIdeal
a : R
ha : a ∈ y.asIdeal.primeCompl
⊢ IsUnit ((algebraMap R (Localization.AtPrime x.asIdeal)) ↑⟨a, ha⟩)
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ IsCompact s ∧ IsOpen s ↔ ∃ t, (zeroLocus ↑t)ᶜ = s

Tactic:
rw [isCompact_open_iff_eq_finite_iUnion_of_isTopologicalBasis _
    isTopologicalBasis_basic_opens isCompact_basicOpen]

Goal state after:
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ (∃ s_1, s_1.Finite ∧ s = ⋃ i ∈ s_1, ↑(basicOpen i)) ↔ ∃ t, (zeroLocus ↑t)ᶜ = s
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_3
inst✝ : MulAction G α
this : Finite α
hpα : Nat.card ↑(fixedPoints G α) = 0
⊢ p ∣ Nat.card α

Tactic:
← Nat.modEq_zero_iff_dvd,

Goal state after:
p : ℕ
G : Type u_1
inst✝¹ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_3
inst✝ : MulAction G α
this : Finite α
hpα : Nat.card ↑(fixedPoints G α) = 0
⊢ Nat.card α ≡ 0 [MOD p]
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Group G
n : ℤ
⊢ ↑(Monoid.exponent G) ∣ n ↔ ∀ (g : G), g ^ n = 1

Tactic:
simp_rw [Int.natCast_dvd, Monoid.exponent_dvd_iff_forall_pow_eq_one, pow_natAbs_eq_one]

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case refine_1
ι : Type u_1
inst✝¹ : Fintype ι
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
m : (i : ι) → M i
i : ι
⊢ (m i ^ univ.lcm fun x ↦ exponent (M x)) = 1

Tactic:
← orderOf_dvd_iff_pow_eq_one

Goal state after:
case refine_1
ι : Type u_1
inst✝¹ : Fintype ι
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
m : (i : ι) → M i
i : ι
⊢ orderOf (m i) ∣ univ.lcm fun x ↦ exponent (M x)
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case refine_1.fst
M₁ : Type u_1
M₂ : Type u_2
inst✝¹ : Monoid M₁
inst✝ : Monoid M₂
g : M₁ × M₂
⊢ g.1 ^ GCDMonoid.lcm (exponent M₁) (exponent M₂) = 1

Tactic:
← orderOf_dvd_iff_pow_eq_one

Goal state after:
case refine_1.fst
M₁ : Type u_1
M₂ : Type u_2
inst✝¹ : Monoid M₁
inst✝ : Monoid M₂
g : M₁ × M₂
⊢ orderOf g.1 ∣ GCDMonoid.lcm (exponent M₁) (exponent M₂)
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case refine_1.snd
M₁ : Type u_1
M₂ : Type u_2
inst✝¹ : Monoid M₁
inst✝ : Monoid M₂
g : M₁ × M₂
⊢ g.2 ^ GCDMonoid.lcm (exponent M₁) (exponent M₂) = 1

Tactic:
← orderOf_dvd_iff_pow_eq_one

Goal state after:
case refine_1.snd
M₁ : Type u_1
M₂ : Type u_2
inst✝¹ : Monoid M₁
inst✝ : Monoid M₂
g : M₁ × M₂
⊢ orderOf g.2 ∣ GCDMonoid.lcm (exponent M₁) (exponent M₂)
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h : IsClosedMap (comap (mapRingHom f))
algInst✝ : Algebra R S := f.toAlgebra
a✝¹ : Nontrivial R
a✝ : Nontrivial S
r : S
p : S[X] := C r * X - 1
⊢ 1 ∈ Ideal.span {X} ⊔ Ideal.comap (mapRingHom f) (Ideal.span {p})

Tactic:
have H := h _ (isClosed_zeroLocus {p})

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h : IsClosedMap (comap (mapRingHom f))
algInst✝ : Algebra R S := f.toAlgebra
a✝¹ : Nontrivial R
a✝ : Nontrivial S
r : S
p : S[X] := C r * X - 1
H : IsClosed (comap (mapRingHom f) '' zeroLocus {p})
⊢ 1 ∈ Ideal.span {X} ⊔ Ideal.comap (mapRingHom f) (Ideal.span {p})
Module: Mathlib.GroupTheory.Rank

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : Nontrivial G
inst✝ : FG G
⊢ ¬rank G = 0

Tactic:
rank_eq_zero_iff,

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : Nontrivial G
inst✝ : FG G
⊢ ¬Subsingleton G
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
inst✝ : CommMonoid G
p : ℕ
hp : Fact (Nat.Prime p)
g : ↥(primaryComponent G p)
⊢ ∃ n, orderOf g = p ^ n

Tactic:
rw [← orderOf_submonoid, ← mem_primaryComponent_iff_orderOf]
  exact g.property

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
G : Type u_2
G' : Type u_3
a : α
p : ℕ
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : Fact (Nat.Prime p)
hG : Nat.card G = p
hH : Nat.card G' = p
⊢ G ≃* G'

Tactic:
have hGcyc := isCyclic_of_prime_card hG

Goal state after:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
p : ℕ
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : Fact (Nat.Prime p)
hG : Nat.card G = p
hH : Nat.card G' = p
hGcyc : IsCyclic G
⊢ G ≃* G'
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: case refine_2.left
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
hn : ∀ {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G), (↑P).Normal
this✝ : Fintype G
ps : Finset ℕ := ⋯
P : (p : ℕ) → Sylow p G := ⋯
this : (p : ℕ) → Fintype ↥↑(P p)
hcomm : _root_.Pairwise fun p₁ p₂ ↦ ∀ (x y : G), x ∈ P ↑p₁ → y ∈ P ↑p₂ → Commute x y
⊢ Injective ⇑(noncommPiCoprod hcomm)

Tactic:
apply Subgroup.injective_noncommPiCoprod_of_iSupIndep

Goal state after:
case refine_2.left
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
hn : ∀ {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G), (↑P).Normal
this✝ : Fintype G
ps : Finset ℕ := ⋯
P : (p : ℕ) → Sylow p G := ⋯
this : (p : ℕ) → Fintype ↥↑(P p)
hcomm : _root_.Pairwise fun p₁ p₂ ↦ ∀ (x y : G), x ∈ P ↑p₁ → y ∈ P ↑p₂ → Commute x y
⊢ iSupIndep fun i ↦ ↑(P ↑i)
Module: Mathlib.RingTheory.SimpleModule.Basic

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
N : Submodule R M
⊢ sSup {m | IsSimpleModule R ↥m ∧ m ≤ N} = N

Tactic:
simpa only [isSimpleModule_iff_isAtom] using sSup_atoms_le_eq _

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

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p q : Submodule R M
x✝¹ : IsSemisimpleModule R ↥p
x✝ : IsSemisimpleModule R ↥q
⊢ IsSemisimpleModule R ↥(p ⊔ q)

Tactic:
let f : Bool → Submodule R M := Bool.rec q p
  rw [show p ⊔ q = ⨆ i ∈ Set.univ, f i by rw [iSup_univ, iSup_bool_eq]]
  exact isSemisimpleModule_biSup_of_isSemisimpleModule_submodule
    (by rintro (_ | _) _ <;> assumption)

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : R
⊢ (∀ ⦃x : M⦄, a • x = 0) ↔ a ∈ annihilator R M

Tactic:
mem_annihilator

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : R
⊢ (∀ ⦃x : M⦄, a • x = 0) ↔ ∀ (m : M), a • m = 0