mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.FreeModule.Finite.Quotient

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : Finite ι
N : Submodule R M
b : Basis ι R M
h : finrank R ↥N = finrank R M
⊢ (M ⧸ N) ≃ₗ[R] (i : ι) → R ⧸ Ideal.span {smithNormalFormCoeffs b h i}

Tactic:
haveI := Fintype.ofFinite ι
  -- Choose `e : M ≃ₗ N` and a basis `b'` for `M` that turns the map
  -- `f := ((Submodule.subtype N).comp e` into a diagonal matrix:
  -- there is an `a : ι → ℤ` such that `f (b' i) = a i • b' i`.
  let a := smithNormalFormCoeffs b h
  let b' := smithNormalFormTopBasis b h
  let ab := smithNormalFormBotBasis b h
  have ab_eq := smithNormalFormBotBasis_def b h
  have mem_I_iff : ∀ x, x ∈ N ↔ ∀ i, a i ∣ b'.repr x i := by
    intro x
    simp_rw [ab.mem_submodule_iff', ab, ab_eq]
    have : ∀ (c : ι → R) (i), b'.repr (∑ j : ι, c j • a j • b' j) i = a i * c i := by
      intro c i
      simp only [← mul_smul, b'.repr_sum_self, mul_comm]
    constructor
    · rintro ⟨c, rfl⟩ i
      exact ⟨c i, this c i⟩
    · rintro ha
      choose c hc using ha
      exact ⟨c, b'.ext_elem fun i => Eq.trans (hc i) (this c i).symm⟩
  -- Now we map everything through the linear equiv `M ≃ₗ (ι → R)`,
  -- which maps `N` to `N' := Π i, a i ℤ`.
  let N' : Submodule R (ι → R) := Submodule.pi Set.univ fun i => span R ({a i} : Set R)
  have : Submodule.map (b'.equivFun : M →ₗ[R] ι → R) N = N' := by
    ext x
    simp only [N', Submodule.mem_map, Submodule.mem_pi, mem_span_singleton, Set.mem_univ,
      mem_I_iff, smul_eq_mul, forall_true_left, LinearEquiv.coe_coe,
      Basis.equivFun_apply, mul_comm _ (a _), eq_comm (b := (x _))]
    constructor
    · rintro ⟨y, hy, rfl⟩ i
      exact hy i
    · rintro hdvd
      refine ⟨∑ i, x i • b' i, fun i => ?_, ?_⟩ <;> rw [b'.repr_sum_self]
      · exact hdvd i
  refine (Submodule.Quotient.equiv N N' b'.equivFun this).trans (re₂₃ := inferInstance)
    (re₃₂ := inferInstance) ?_
  classical
  exact Submodule.quotientPi (show _ → Submodule R R from fun i => span R ({a i} : Set R))

Goal state after:
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case mpr
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hn : (fun x ↦ g ^ x) n = a
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
⊢ a ^ (Fintype.card F / 2) = 1 → IsSquare a

Tactic:
· subst a; intro h
    rw [← Nat.card_eq_fintype_card] at hodd h
    have key : 2 * (Nat.card F / 2) ∣ n * (Nat.card F / 2) := by
      rw [← pow_mul] at h
      rw [hodd, ← Nat.card_units, ← orderOf_eq_card_of_forall_mem_zpowers hg]
      apply orderOf_dvd_of_pow_eq_one h
    have : 0 < Nat.card F / 2 := Nat.div_pos Finite.one_lt_card (by simp)
    obtain ⟨m, rfl⟩ := Nat.dvd_of_mul_dvd_mul_right this key
    refine ⟨g ^ m, ?_⟩
    dsimp
    rw [mul_comm, pow_mul, pow_two]

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

Goal state before:
pp: G : Type u_1
A : Type u_2
B : Type u_3
K : Type u_4
L : Type u_5
inst✝¹⁸ : Group G
inst✝¹⁷ : CommRing A
inst✝¹⁶ : CommRing B
inst✝¹⁵ : Algebra A B
inst✝¹⁴ : Field K
inst✝¹³ : Field L
inst✝¹² : Algebra K L
inst✝¹¹ : Algebra A K
inst✝¹⁰ : Algebra B L
inst✝⁹ : Algebra A L
inst✝⁸ : IsFractionRing A K
inst✝⁷ : IsFractionRing B L
inst✝⁶ : IsScalarTower A K L
inst✝⁵ : IsScalarTower A B L
inst✝⁴ : MulSemiringAction G B
inst✝³ : MulSemiringAction G L
inst✝² : SMulDistribClass G B L
hAB : Algebra.IsInvariant A B G
inst✝¹ : SMulCommClass G A B
inst✝ : Algebra.IsIntegral A B
hc : ∀ (a : A), (algebraMap K L) ((algebraMap A K) a) = (algebraMap B L) ((algebraMap A B) a)
this✝ : Nontrivial A
this : Nontrivial B
x y : B
hy : y ∈ nonZeroDivisors B
h : ∀ (g : G), g • ((algebraMap B L) x / (algebraMap B L) y) = (algebraMap B L) x / (algebraMap B L) y
hy' : (algebraMap B L) y ≠ 0
b : B
a : A
hb : x * (algebraMap A B) a = b * y
ha : (algebraMap B L) ((algebraMap A B) a) ≠ 0
⊢ (algebraMap B L) (x * (algebraMap A B) a) = (algebraMap B L) b * (algebraMap B L) y

Tactic:
hb,

Goal state after:
G : Type u_1
A : Type u_2
B : Type u_3
K : Type u_4
L : Type u_5
inst✝¹⁸ : Group G
inst✝¹⁷ : CommRing A
inst✝¹⁶ : CommRing B
inst✝¹⁵ : Algebra A B
inst✝¹⁴ : Field K
inst✝¹³ : Field L
inst✝¹² : Algebra K L
inst✝¹¹ : Algebra A K
inst✝¹⁰ : Algebra B L
inst✝⁹ : Algebra A L
inst✝⁸ : IsFractionRing A K
inst✝⁷ : IsFractionRing B L
inst✝⁶ : IsScalarTower A K L
inst✝⁵ : IsScalarTower A B L
inst✝⁴ : MulSemiringAction G B
inst✝³ : MulSemiringAction G L
inst✝² : SMulDistribClass G B L
hAB : Algebra.IsInvariant A B G
inst✝¹ : SMulCommClass G A B
inst✝ : Algebra.IsIntegral A B
hc : ∀ (a : A), (algebraMap K L) ((algebraMap A K) a) = (algebraMap B L) ((algebraMap A B) a)
this✝ : Nontrivial A
this : Nontrivial B
x y : B
hy : y ∈ nonZeroDivisors B
h : ∀ (g : G), g • ((algebraMap B L) x / (algebraMap B L) y) = (algebraMap B L) x / (algebraMap B L) y
hy' : (algebraMap B L) y ≠ 0
b : B
a : A
hb : x * (algebraMap A B) a = b * y
ha : (algebraMap B L) ((algebraMap A B) a) ≠ 0
⊢ (algebraMap B L) (b * y) = (algebraMap B L) b * (algebraMap B L) y
Module: Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient

Goal state before:
pp: case calc_1
M : Type u_1
inst✝⁴ : AddCommGroup M
inst✝³ : Free ℤ M
inst✝² : Module.Finite ℤ M
N : Submodule ℤ M
E : Type u_2
inst✝¹ : EquivLike E M ↥N
inst✝ : AddEquivClass E M ↥N
e : E
b : Basis (Free.ChooseBasisIndex ℤ M) ℤ M := Free.chooseBasis ℤ M
h : finrank ℤ ↥N = finrank ℤ M
a : Free.ChooseBasisIndex ℤ M → ℤ := smithNormalFormCoeffs b h
b' : Basis (Free.ChooseBasisIndex ℤ M) ℤ M := smithNormalFormTopBasis b h
ab : Basis (Free.ChooseBasisIndex ℤ M) ℤ ↥N := smithNormalFormBotBasis b h
ab_eq :
  ∀ (i : Free.ChooseBasisIndex ℤ M),
    ↑((smithNormalFormBotBasis b h) i) = smithNormalFormCoeffs b h i • (smithNormalFormTopBasis b h) i
e' : M ≃ₗ[ℤ] ↥N := b'.equiv ab (Equiv.refl (Free.ChooseBasisIndex ℤ M))
f : M →ₗ[ℤ] M := N.subtype ∘ₗ ↑e'
f_apply : ∀ (x : M), f x = ↑((b'.equiv ab (Equiv.refl (Free.ChooseBasisIndex ℤ M))) x) := fun x ↦ rfl
ha : ∀ (i : Free.ChooseBasisIndex ℤ M), f (b' i) = a i • b' i
⊢ ((LinearMap.toMatrix b' b') f).det.natAbs = (Matrix.diagonal a).det.natAbs

Tactic:
congr 2; ext i j
    rw [LinearMap.toMatrix_apply, ha, map_smul, Basis.repr_self, Finsupp.smul_single,
      smul_eq_mul, mul_one]
    by_cases h : i = j
    · rw [h, Matrix.diagonal_apply_eq, Finsupp.single_eq_same]
    · rw [Matrix.diagonal_apply_ne _ h, Finsupp.single_eq_of_ne h]

Goal state after:
Module: Mathlib.RingTheory.Jacobson.Artinian

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra.FiniteType R A
inst✝ : IsArtinianRing R
⊢ Module.Finite R A ↔ Ring.KrullDimLE 0 A

Tactic:
have : IsNoetherianRing A := Algebra.FiniteType.isNoetherianRing R A
  rw [finite_iff_isArtinianRing, isArtinianRing_iff_isNoetherianRing_krullDimLE_zero,
    and_iff_right this]

Goal state after:
Module: Mathlib.RingTheory.Jacobson.Artinian

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra.FiniteType R A
inst✝ : IsArtinianRing R
⊢ Module.Finite R A ↔ Ring.KrullDimLE 0 A

Tactic:
by
  have : IsNoetherianRing A := Algebra.FiniteType.isNoetherianRing R A
  rw [finite_iff_isArtinianRing, isArtinianRing_iff_isNoetherianRing_krullDimLE_zero,
    and_iff_right this]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsJacobsonRing R
s : Set (PrimeSpectrum R)
hs : IsOpen s
hs' : s.Nonempty
I : Ideal R
hI' : sᶜ = zeroLocus ↑I
this : ∀ (x : PrimeSpectrum R), x.asIdeal.IsMaximal → ↑I ⊆ ↑x.asIdeal
⊢ zeroLocus ↑I = Set.univ

Tactic:
← zeroLocus_bot,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsJacobsonRing R
s : Set (PrimeSpectrum R)
hs : IsOpen s
hs' : s.Nonempty
I : Ideal R
hI' : sᶜ = zeroLocus ↑I
this : ∀ (x : PrimeSpectrum R), x.asIdeal.IsMaximal → ↑I ⊆ ↑x.asIdeal
⊢ zeroLocus ↑I = zeroLocus ↑⊥
Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
H : JacobsonSpace (PrimeSpectrum R)
I : Ideal R
hI : I.IsRadical
| I

Tactic:
rw [← hI.radical]

Goal state after:
R : Type u_1
inst✝ : CommRing R
H : JacobsonSpace (PrimeSpectrum R)
I : Ideal R
hI : I.IsRadical
| I.radical
Module: Mathlib.RingTheory.HopkinsLevitzki

Goal state before:
pp: M : Type u
inst✝⁴ : AddCommGroup M
R : Type u_3
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : IsArtinian R M
s : Set M
fin : Finite ↑s
span : ⨆ i, R ∙ ↑i = ⊤
i : M
e : (I : Ideal R) → R ⧸ I →ₛₗ[Ideal.Quotient.mk I] R ⧸ I := fun I ↦ { toAddHom := AddHom.id (R ⧸ I), map_smul' := ⋯ }
⊢ IsArtinian R (R ⧸ (LinearMap.toSpanSingleton R M i).ker)

Tactic:
(LinearMap.quotKerEquivRange _).isArtinian_iff

Goal state after:
M : Type u
inst✝⁴ : AddCommGroup M
R : Type u_3
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : IsArtinian R M
s : Set M
fin : Finite ↑s
span : ⨆ i, R ∙ ↑i = ⊤
i : M
e : (I : Ideal R) → R ⧸ I →ₛₗ[Ideal.Quotient.mk I] R ⧸ I := fun I ↦ { toAddHom := AddHom.id (R ⧸ I), map_smul' := ⋯ }
⊢ IsArtinian R ↥(LinearMap.toSpanSingleton R M i).range
Module: Mathlib.RingTheory.LocalRing.Length

Goal state before:
pp: A : Type u_1
B : Type u_2
M : Type u_3
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : IsLocalRing A
inst✝⁶ : IsLocalRing B
inst✝⁵ : Algebra A B
inst✝⁴ : IsLocalHom (algebraMap A B)
inst✝³ : AddCommGroup M
inst✝² : Module A M
inst✝¹ : Module B M
inst✝ : IsScalarTower A B M
p q : Submodule B M
h : p ⋖ q
f : ↥p →ₗ[B] ↥q := inclusion ⋯
key : IsSimpleModule B (↥q ⧸ f.range)
m : Ideal B
hm : m.IsMaximal
e : (↥q ⧸ f.range) ≃ₗ[B] B ⧸ maximalIdeal B
g : ↥q →ₗ[B] ResidueField B := ↑e ∘ₗ f.range.mkQ
⊢ length A ↥q = length A ↥p + length (ResidueField A) (ResidueField B)

Tactic:
have : Function.Injective f := inclusion_injective _

Goal state after:
A : Type u_1
B : Type u_2
M : Type u_3
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : IsLocalRing A
inst✝⁶ : IsLocalRing B
inst✝⁵ : Algebra A B
inst✝⁴ : IsLocalHom (algebraMap A B)
inst✝³ : AddCommGroup M
inst✝² : Module A M
inst✝¹ : Module B M
inst✝ : IsScalarTower A B M
p q : Submodule B M
h : p ⋖ q
f : ↥p →ₗ[B] ↥q := inclusion ⋯
key : IsSimpleModule B (↥q ⧸ f.range)
m : Ideal B
hm : m.IsMaximal
e : (↥q ⧸ f.range) ≃ₗ[B] B ⧸ maximalIdeal B
g : ↥q →ₗ[B] ResidueField B := ↑e ∘ₗ f.range.mkQ
this : Function.Injective ⇑f
⊢ length A ↥q = length A ↥p + length (ResidueField A) (ResidueField B)
Module: Mathlib.RingTheory.LocalRing.Length

Goal state before:
pp: A : Type u_1
B : Type u_2
M : Type u_3
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : IsLocalRing A
inst✝⁵ : IsLocalRing B
inst✝⁴ : Algebra A B
inst✝³ : IsLocalHom (algebraMap A B)
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Flat A B
p q : Submodule A M
h : p ⋖ q
f : ↥p →ₗ[A] ↥q := inclusion ⋯
key : IsSimpleModule A (↥q ⧸ f.range)
hm : (maximalIdeal A).IsMaximal
e : (↥q ⧸ f.range) ≃ₗ[A] A ⧸ maximalIdeal A
g : ↥q →ₗ[A] A ⧸ maximalIdeal A := ↑e ∘ₗ f.range.mkQ
⊢ length B (B ⊗[A] ↥q) = length B (B ⊗[A] ↥p) + length B (B ⧸ Ideal.map (algebraMap A B) (maximalIdeal A))

Tactic:
have : Function.Injective f := inclusion_injective _

Goal state after:
A : Type u_1
B : Type u_2
M : Type u_3
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : IsLocalRing A
inst✝⁵ : IsLocalRing B
inst✝⁴ : Algebra A B
inst✝³ : IsLocalHom (algebraMap A B)
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Flat A B
p q : Submodule A M
h : p ⋖ q
f : ↥p →ₗ[A] ↥q := inclusion ⋯
key : IsSimpleModule A (↥q ⧸ f.range)
hm : (maximalIdeal A).IsMaximal
e : (↥q ⧸ f.range) ≃ₗ[A] A ⧸ maximalIdeal A
g : ↥q →ₗ[A] A ⧸ maximalIdeal A := ↑e ∘ₗ f.range.mkQ
this : Function.Injective ⇑f
⊢ length B (B ⊗[A] ↥q) = length B (B ⊗[A] ↥p) + length B (B ⧸ Ideal.map (algebraMap A B) (maximalIdeal A))
Module: Mathlib.RingTheory.RamificationInertia.Inertia

Goal state before:
pp: case pos
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
q : Ideal S
G : Type u_4
inst✝² : Group G
inst✝¹ : MulSemiringAction G S
inst✝ : SMulCommClass G R S
g : G
hq : q.IsPrime
⊢ (g • q).inertiaDeg R = q.inertiaDeg R

Tactic:
let p := q.under R
    let f₀ := MulSemiringAction.toAlgAut G R S g
    let := Localization.AtPrime.algebraOfLiesOver p q
    let := Localization.AtPrime.algebraOfLiesOver p (g • q)
    rw [inertiaDeg_eq p q, inertiaDeg_eq p (g • q)]
    let e₂ := Ideal.residueFieldAlgEquiv' p (g • q) q f₀.symm (comap_symm f₀.toRingEquiv).symm
    exact e₂.toLinearEquiv.finrank_eq

Goal state after:
Module: Mathlib.NumberTheory.RamificationInertia.Ramification

Goal state before:
pp: case succ
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : Ideal R
P : Ideal S
n : ℕ
hgt : ¬map f p ≤ P ^ (n + 1)
⊢ p.ramificationIdx' P < n + 1

Tactic:
Nat.lt_succ_iff

Goal state after:
case succ
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : Ideal R
P : Ideal S
n : ℕ
hgt : ¬map f p ≤ P ^ (n + 1)
⊢ p.ramificationIdx' P ≤ n
Module: Mathlib.NumberTheory.RamificationInertia.Ramification

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
S : Type v
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
p : Ideal R
P : Ideal S
T : Type u_2
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Ideal T
hp : p = comap f P
h : p.ramificationIdx' Q ≠ 0
⊢ P.ramificationIdx' Q ≤ p.ramificationIdx' Q

Tactic:
simp_rw [ramificationIdx', Ne] at *
  refine csSup_le_csSup' (h.imp_symm Nat.sSup_of_not_bddAbove) fun n hn ↦ ?_
  simp_rw [hp, IsScalarTower.algebraMap_eq R S T, ← map_map, map_le_iff_le_comap]
  exact comap_mono <| by rwa [← map_le_iff_le_comap]

Goal state after:
Module: Mathlib.NumberTheory.RamificationInertia.Ramification

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
S : Type v
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
p : Ideal R
P : Ideal S
T : Type u_2
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Ideal T
hp : p = comap f P
h : p.ramificationIdx' Q ≠ 0
⊢ P.ramificationIdx' Q ≤ p.ramificationIdx' Q

Tactic:
by
  simp_rw [ramificationIdx', Ne] at *
  refine csSup_le_csSup' (h.imp_symm Nat.sSup_of_not_bddAbove) fun n hn ↦ ?_
  simp_rw [hp, IsScalarTower.algebraMap_eq R S T, ← map_map, map_le_iff_le_comap]
  exact comap_mono <| by rwa [← map_le_iff_le_comap]

Goal state after:
Module: Mathlib.NumberTheory.RamificationInertia.Ramification

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
P : Ideal S
inst✝ : IsDedekindDomain S
hp0 : map f p ≠ ⊥
hP : P.IsPrime
le : map f p ≤ P
hP0 : P ≠ ⊥
hPirr : Irreducible P
P' : Ideal S
hP' : P' ∈ normalizedFactors (map f p)
P'_eq : Associated P P'
⊢ P ∈ normalizedFactors (map f p)

Tactic:
associated_iff_eq.mp P'_eq

Goal state after:
R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
P : Ideal S
inst✝ : IsDedekindDomain S
hp0 : map f p ≠ ⊥
hP : P.IsPrime
le : map f p ≤ P
hP0 : P ≠ ⊥
hPirr : Irreducible P
P' : Ideal S
hP' : P' ∈ normalizedFactors (map f p)
P'_eq : Associated P P'
⊢ P' ∈ normalizedFactors (map f p)
Module: Mathlib.NumberTheory.RamificationInertia.Ramification

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsDedekindDomain S
p : Ideal R
P : Ideal S
inst✝ : P.IsPrime
hp : P ≠ ⊥
hpP : map f p ≤ P
Sₚ : Type v := Localization.AtPrime P
H₁ : ¬map f p ≤ P * P
a : Ideal S
ha : map f p = P * a
ha' : ¬a ≤ P
⊢ map (algebraMap S (Localization.AtPrime P)) (P * a) = maximalIdeal (Localization.AtPrime P)

Tactic:
Ideal.map_mul,

Goal state after:
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsDedekindDomain S
p : Ideal R
P : Ideal S
inst✝ : P.IsPrime
hp : P ≠ ⊥
hpP : map f p ≤ P
Sₚ : Type v := Localization.AtPrime P
H₁ : ¬map f p ≤ P * P
a : Ideal S
ha : map f p = P * a
ha' : ¬a ≤ P
⊢ map (algebraMap S (Localization.AtPrime P)) P * map (algebraMap S (Localization.AtPrime P)) a =
    maximalIdeal (Localization.AtPrime P)
Module: Mathlib.NumberTheory.RamificationInertia.Ramification

Goal state before:
pp: case h₃
R : Type u
inst✝⁶ : CommRing R
S : Type v
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDedekindDomain S
inst✝² : IsDedekindDomain R
inst✝¹ : FaithfulSMul R S
v : Ideal R
w : Ideal S
hv : Irreducible v
hw : Irreducible w
hw_bot : w ≠ ⊥
inst✝ : w.LiesOver v
I p : Ideal R
hI : I ≠ 0
hp : Prime p
IH : I ≠ ⊥ → emultiplicity w (map f I) = ↑(v.ramificationIdx' w) * emultiplicity v I
h : p * I ≠ ⊥
⊢ emultiplicity w (map f (p * I)) = ↑(v.ramificationIdx' w) * emultiplicity v (p * I)

Tactic:
Ideal.map_mul,

Goal state after:
case h₃
R : Type u
inst✝⁶ : CommRing R
S : Type v
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDedekindDomain S
inst✝² : IsDedekindDomain R
inst✝¹ : FaithfulSMul R S
v : Ideal R
w : Ideal S
hv : Irreducible v
hw : Irreducible w
hw_bot : w ≠ ⊥
inst✝ : w.LiesOver v
I p : Ideal R
hI : I ≠ 0
hp : Prime p
IH : I ≠ ⊥ → emultiplicity w (map f I) = ↑(v.ramificationIdx' w) * emultiplicity v I
h : p * I ≠ ⊥
⊢ emultiplicity w (map f p * map f I) = ↑(v.ramificationIdx' w) * emultiplicity v (p * I)
Module: Mathlib.NumberTheory.RamificationInertia.Ramification

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 S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
inst✝¹ : IsDedekindDomain S
inst✝ : IsDedekindDomain T
p : Ideal R
P : Ideal S
Q : Ideal T
hpm : P.IsPrime
hqm : Q.IsPrime
hg0 : map (algebraMap S T) P ≠ ⊥
hfg : map (algebraMap R T) p ≠ ⊥
hg : map (algebraMap S T) P ≤ Q
hf0 : map f p ≠ ⊥
hp0 : P ≠ ⊥
hq0 : Q ≠ ⊥
this : P.IsMaximal := Ring.DimensionLEOne.maximalOfPrime hp0 hpm
I : Ideal S
hcp✝ : P ⊔ I = ⊤
heq : map f p = P ^ Multiset.count P (normalizedFactors (map f p)) * I
hcp : ⊤ = map (algebraMap S T) P ⊔ map (algebraMap S T) I
hntq : ¬⊤ ≤ Q
⊢ Multiset.count Q (normalizedFactors (map (algebraMap S T) (P ^ Multiset.count P (normalizedFactors (map f p)) * I))) =
    Multiset.count P (normalizedFactors (map f p)) * Multiset.count Q (normalizedFactors (map (algebraMap S T) P))

Tactic:
Ideal.map_mul,

Goal state after:
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 S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
inst✝¹ : IsDedekindDomain S
inst✝ : IsDedekindDomain T
p : Ideal R
P : Ideal S
Q : Ideal T
hpm : P.IsPrime
hqm : Q.IsPrime
hg0 : map (algebraMap S T) P ≠ ⊥
hfg : map (algebraMap R T) p ≠ ⊥
hg : map (algebraMap S T) P ≤ Q
hf0 : map f p ≠ ⊥
hp0 : P ≠ ⊥
hq0 : Q ≠ ⊥
this : P.IsMaximal := Ring.DimensionLEOne.maximalOfPrime hp0 hpm
I : Ideal S
hcp✝ : P ⊔ I = ⊤
heq : map f p = P ^ Multiset.count P (normalizedFactors (map f p)) * I
hcp : ⊤ = map (algebraMap S T) P ⊔ map (algebraMap S T) I
hntq : ¬⊤ ≤ Q
⊢ Multiset.count Q
      (normalizedFactors
        (map (algebraMap S T) (P ^ Multiset.count P (normalizedFactors (map f p))) * map (algebraMap S T) I)) =
    Multiset.count P (normalizedFactors (map f p)) * Multiset.count Q (normalizedFactors (map (algebraMap S T) P))
Module: Mathlib.RingTheory.Unramified.Finite

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
I : Type u_4
inst✝ : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : I → I →₀ R := fun i ↦ b.repr (b i * x)
⊢ ∑ i ∈ f.support, ∑ x ∈ (a i).support, ((a i) x • f i) ⊗ₜ[R] b x =
    ∑ k ∈ f.support.biUnion fun i ↦ ((fun i ↦ b.repr (b i * x)) i).support,
      (b.repr (f.sum fun i y ↦ ((fun i ↦ b.repr (b i * x)) i) k • y)).sum fun j c ↦ c • b j ⊗ₜ[R] b k

Tactic:
have h₁ : ∀ k,
    (Finsupp.sum (Finsupp.sum f fun i y ↦ a i k • b.repr y) fun j z ↦ z • b j ⊗ₜ[R] b k) =
      (f.sum fun i y ↦ (b.repr y).sum fun j z ↦ a i k • z • b j ⊗ₜ[R] b k) := by
    intro i
    rw [Finsupp.sum_sum_index]
    · congr
      ext j s
      rw [Finsupp.sum_smul_index]
      · simp only [mul_smul, Finsupp.sum, ← Finset.smul_sum]
      intro; simp only [zero_smul]
    · intro; simp only [zero_smul]
    · intros; simp only [add_smul]

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
I : Type u_4
inst✝ : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : I → I →₀ R := fun i ↦ b.repr (b i * x)
h₁ :
  ∀ (k : I),
    ((f.sum fun i y ↦ (a i) k • b.repr y).sum fun j z ↦ z • b j ⊗ₜ[R] b k) =
      f.sum fun i y ↦ (b.repr y).sum fun j z ↦ (a i) k • z • b j ⊗ₜ[R] b k
⊢ ∑ i ∈ f.support, ∑ x ∈ (a i).support, ((a i) x • f i) ⊗ₜ[R] b x =
    ∑ k ∈ f.support.biUnion fun i ↦ ((fun i ↦ b.repr (b i * x)) i).support,
      (b.repr (f.sum fun i y ↦ ((fun i ↦ b.repr (b i * x)) i) k • y)).sum fun j c ↦ c • b j ⊗ₜ[R] b k
Module: Mathlib.RingTheory.Unramified.Finite

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
I : Type u_4
inst✝ : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : I → I →₀ R := fun i ↦ b.repr (b i * x)
h₁ :
  ∀ (k : I),
    ((f.sum fun i y ↦ (a i) k • b.repr y).sum fun j z ↦ z • b j ⊗ₜ[R] b k) =
      f.sum fun i y ↦ (b.repr y).sum fun j z ↦ (a i) k • z • b j ⊗ₜ[R] b k
h₂ : ∀ (x : S), ∑ a ∈ (b.repr x).support, (b.repr x) a • b a = x
⊢ ∑ i ∈ f.support, ∑ x ∈ (a i).support, ((a i) x • f i) ⊗ₜ[R] b x =
    ∑ k ∈ f.support.biUnion fun i ↦ ((fun i ↦ b.repr (b i * x)) i).support,
      (b.repr (f.sum fun i y ↦ ((fun i ↦ b.repr (b i * x)) i) k • y)).sum fun j c ↦ c • b j ⊗ₜ[R] b k

Tactic:
simp only [a] at h₁

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
I : Type u_4
inst✝ : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : I → I →₀ R := fun i ↦ b.repr (b i * x)
h₁ :
  ∀ (k : I),
    ((f.sum fun i y ↦ (b.repr (b i * x)) k • b.repr y).sum fun j z ↦ z • b j ⊗ₜ[R] b k) =
      f.sum fun i y ↦ (b.repr y).sum fun j z ↦ (b.repr (b i * x)) k • z • b j ⊗ₜ[R] b k
h₂ : ∀ (x : S), ∑ a ∈ (b.repr x).support, (b.repr x) a • b a = x
⊢ ∑ i ∈ f.support, ∑ x ∈ (a i).support, ((a i) x • f i) ⊗ₜ[R] b x =
    ∑ k ∈ f.support.biUnion fun i ↦ ((fun i ↦ b.repr (b i * x)) i).support,
      (b.repr (f.sum fun i y ↦ ((fun i ↦ b.repr (b i * x)) i) k • y)).sum fun j c ↦ c • b j ⊗ₜ[R] b k
Module: Mathlib.RingTheory.QuasiFinite.Basic

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
inst✝² : Algebra.IsIntegral R S
inst✝¹ : FiniteType R T
s : S
inst✝ : IsLocalization.Away s T
A : Subalgebra R S := R[s]
sA : ↥A := ⟨s, ⋯⟩
f : Localization.Away sA →+* T := IsLocalization.Away.lift sA ⋯
⊢ QuasiFinite R T

Tactic:
let := f.toAlgebra

Goal state after:
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
inst✝² : Algebra.IsIntegral R S
inst✝¹ : FiniteType R T
s : S
inst✝ : IsLocalization.Away s T
A : Subalgebra R S := R[s]
sA : ↥A := ⟨s, ⋯⟩
f : Localization.Away sA →+* T := IsLocalization.Away.lift sA ⋯
this : Algebra (Localization.Away sA) T := f.toAlgebra
⊢ QuasiFinite R T