mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.Galois.Infinite

Goal state before:
pp: k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
h : IsOpen L.fixingSubgroup.carrier
S : Set Gal(K/k)
sub : S ⊆ (↑(IntermediateFieldEquivClosedSubgroup.toFun L)).carrier
gp : Subgroup Gal(K/k)
eq : (fun g ↦ g.carrier) gp = S
M : IntermediateField k K
hM : M ∈ finiteExts k K
eq' : M.fixingSubgroup = gp
⊢ FiniteDimensional k ↥L

Tactic:
rw [← eq, ← eq'] at sub

Goal state after:
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
h : IsOpen L.fixingSubgroup.carrier
S : Set Gal(K/k)
gp : Subgroup Gal(K/k)
eq : (fun g ↦ g.carrier) gp = S
M : IntermediateField k K
sub : (fun g ↦ g.carrier) M.fixingSubgroup ⊆ (↑(IntermediateFieldEquivClosedSubgroup.toFun L)).carrier
hM : M ∈ finiteExts k K
eq' : M.fixingSubgroup = gp
⊢ FiniteDimensional k ↥L
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case mpr
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
x : Kˣ
h : x ^ i = 1
y : Kˣ
hx : ∀ (x_1 : Kˣ), x_1 ∈ Submonoid.powers x
⊢ y ^ i = 1

Tactic:
rcases hx y with ⟨j, rfl⟩

Goal state after:
case mpr
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
x : Kˣ
h : x ^ i = 1
hx : ∀ (x_1 : Kˣ), x_1 ∈ Submonoid.powers x
j : ℕ
⊢ (fun x_1 ↦ x ^ x_1) j ^ i = 1
Module: Mathlib.RingTheory.Int.Basic

Goal state before:
pp: a b c : ℤ
h : a.gcd b = 1
heq : a * b = c ^ 2
⊢ IsUnit (GCDMonoid.gcd a b)

Tactic:
rw [← coe_gcd, h, Int.ofNat_one]

Goal state after:
a b c : ℤ
h : a.gcd b = 1
heq : a * b = c ^ 2
⊢ IsUnit 1
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: K' : Type u_3
inst✝ : Field K'
p : ℕ
hp : 1 < p
⊢ X.degree < ↑p

Tactic:
degree_X

Goal state after:
K' : Type u_3
inst✝ : Field K'
p : ℕ
hp : 1 < p
⊢ 1 < ↑p
Module: Mathlib.RingTheory.Invariant.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹⁸ : CommRing A
inst✝¹⁷ : CommRing B
inst✝¹⁶ : Algebra A B
G : Type u_3
inst✝¹⁵ : Group G
inst✝¹⁴ : Finite G
inst✝¹³ : MulSemiringAction G B
inst✝¹² : SMulCommClass G A B
P : Ideal A
Q : Ideal B
inst✝¹¹ : Q.IsPrime
inst✝¹⁰ : Q.LiesOver P
K : Type u_4
L : Type u_5
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra (A ⧸ P) K
inst✝⁶ : Algebra (B ⧸ Q) L
inst✝⁵ : Algebra (A ⧸ P) L
inst✝⁴ : IsScalarTower (A ⧸ P) (B ⧸ Q) L
inst✝³ : Algebra K L
inst✝² : IsScalarTower (A ⧸ P) K L
inst✝¹ : Algebra.IsInvariant A B G
inst✝ : Module.IsTorsionFree (B ⧸ Q) L
f : Gal(L/K)
b : B ⧸ Q
hx : ∀ (g : ↥(MulAction.stabilizer G Q)), ((Ideal.Quotient.stabilizerHom Q P G) g) b = b
⊢ f ((algebraMap (B ⧸ Q) L) b) = (algebraMap (B ⧸ Q) L) b

Tactic:
cases nonempty_fintype G
  obtain ⟨b₀, rfl⟩ := Ideal.Quotient.mk_surjective b
  rw [← Ideal.Quotient.algebraMap_eq]
  obtain ⟨a, b, ha1, ha2, hb⟩ := fixed_of_fixed1_aux2 G Q b₀ (fun g hg ↦ hx ⟨g, hg⟩)
  obtain ⟨M, key⟩ := (mem_lifts _).mp (Algebra.IsInvariant.charpoly_mem_lifts A B G b)
  replace key := congrArg (map (algebraMap B (B ⧸ Q))) key
  rw [map_map, ← algebraMap_eq, algebraMap_eq A (A ⧸ P) (B ⧸ Q),
      ← map_map, MulSemiringAction.charpoly, Polynomial.map_prod] at key
  have key₀ : ∀ g : G, (X - C (g • b)).map (algebraMap B (B ⧸ Q)) =
      if g • Q = Q then X - C (algebraMap B (B ⧸ Q) (a * b₀)) else X := by
    intro g
    rw [Polynomial.map_sub, map_X, map_C, hb]
    split_ifs
    · rfl
    · rw [map_zero, map_zero, sub_zero]
  simp only [key₀, Finset.prod_ite, Finset.prod_const] at key
  replace key := congrArg (map (algebraMap (B ⧸ Q) L)) key
  rw [map_map, ← algebraMap_eq, algebraMap_eq (A ⧸ P) K L,
      ← map_map, Polynomial.map_mul, Polynomial.map_pow, Polynomial.map_pow, Polynomial.map_sub,
      map_X, map_C] at key
  replace key := fixed_of_fixed1_aux3 key f (Finset.card_ne_zero_of_mem
    (Finset.mem_filter.mpr ⟨Finset.mem_univ 1, one_smul G Q⟩))
  simp only [map_mul] at key
  obtain ⟨a, rfl⟩ := Algebra.IsInvariant.isInvariant (A := A) a ha1
  rwa [← algebraMap_apply A B (B ⧸ Q), algebraMap_apply A (A ⧸ P) (B ⧸ Q),
      ← algebraMap_apply, algebraMap_apply (A ⧸ P) K L, f.commutes, mul_right_inj'] at key
  rwa [← algebraMap_apply, algebraMap_apply (A ⧸ P) (B ⧸ Q) L,
      ← algebraMap_apply A (A ⧸ P) (B ⧸ Q), algebraMap_apply A B (B ⧸ Q),
      Ne, algebraMap_eq_zero_iff, Ideal.Quotient.algebraMap_eq, Ideal.Quotient.eq_zero_iff_mem]

Goal state after:
Module: Mathlib.LinearAlgebra.Quotient.Pi

Goal state before:
pp: case h₀
ι : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
Ms : ι → Type u_3
inst✝⁵ : (i : ι) → AddCommGroup (Ms i)
inst✝⁴ : (i : ι) → Module R (Ms i)
N : Type u_4
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
q : Submodule R N
f : (i : ι) → Ms i →ₗ[R] N
hf : ∀ (i : ι), p i ≤ comap (f i) q
i : ι
x : Ms i ⧸ p i
j : ι
hj : j ≠ i
⊢ ((p j).mapQ q (f j) ⋯) (Pi.single i x j) = 0

Tactic:
rw [Pi.single_eq_of_ne hj, map_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient

Goal state before:
pp: E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Module ℚ E
L₁ L₂ : AddSubgroup E
H : L₁ ≤ L₂
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b₁ b₂ : Basis ι ℚ E
h₁ : L₁ = closure (Set.range ⇑b₁)
h₂ : L₂ = closure (Set.range ⇑b₂)
i✝ j✝ : ι
⊢ (algebraMap ℤ ℚ).mapMatrix
      ((Basis.addSubgroupOfClosure L₂ b₂ h₂).toMatrix fun i ↦ ⟨↑((Basis.addSubgroupOfClosure L₁ b₁ h₁) i), ⋯⟩) i✝ j✝ =
    b₂.toMatrix (⇑b₁) i✝ j✝

Tactic:
simp [Basis.toMatrix_apply]

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

Goal state before:
pp: case h.refine_2
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
s : Finset ↥K⟮x⟯
b : Basis (↥s) K ↥K⟮x⟯
⊢ x ∈ K⟮x⟯.toSubalgebra

Tactic:
· exact IntermediateField.subset_adjoin K _ (Set.mem_singleton x)

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
F : Type u_6
inst✝¹ : Field F
inst✝ : Algebra R F
pb : PowerBasis R S
hE : (Polynomial.map (algebraMap R F) (minpoly R pb.gen)).Splits
hfx : IsSeparable R pb.gen
this : DecidableEq F := Classical.decEq F
⊢ ((minpoly R pb.gen).aroots F).prod = (Multiset.map ?f ((minpoly R pb.gen).aroots F)).prod

pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
F : Type u_6
inst✝¹ : Field F
inst✝ : Algebra R F
pb : PowerBasis R S
hE : (Polynomial.map (algebraMap R F) (minpoly R pb.gen)).Splits
hfx : IsSeparable R pb.gen
this : DecidableEq F := Classical.decEq F
⊢ ((minpoly R pb.gen).aroots F).Nodup

pp: case f
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
F : Type u_6
inst✝¹ : Field F
inst✝ : Algebra R F
pb : PowerBasis R S
hE : (Polynomial.map (algebraMap R F) (minpoly R pb.gen)).Splits
hfx : IsSeparable R pb.gen
this : DecidableEq F := ⋯
⊢ F → F

pp: case hfg
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
F : Type u_6
inst✝¹ : Field F
inst✝ : Algebra R F
pb : PowerBasis R S
hE : (Polynomial.map (algebraMap R F) (minpoly R pb.gen)).Splits
hfx : IsSeparable R pb.gen
this : DecidableEq F := Classical.decEq F
⊢ ∀ (x : { x // x ∈ (minpoly R pb.gen).aroots F }), ↑x = ?f ↑x

Tactic:
Multiset.map_id

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
F : Type u_6
inst✝¹ : Field F
inst✝ : Algebra R F
pb : PowerBasis R S
hE : (Polynomial.map (algebraMap R F) (minpoly R pb.gen)).Splits
hfx : IsSeparable R pb.gen
this : DecidableEq F := Classical.decEq F
⊢ ((minpoly R pb.gen).aroots F).prod = ((minpoly R pb.gen).aroots F).prod

R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
F : Type u_6
inst✝¹ : Field F
inst✝ : Algebra R F
pb : PowerBasis R S
hE : (Polynomial.map (algebraMap R F) (minpoly R pb.gen)).Splits
hfx : IsSeparable R pb.gen
this : DecidableEq F := Classical.decEq F
⊢ ((minpoly R pb.gen).aroots F).Nodup

case hfg
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
F : Type u_6
inst✝¹ : Field F
inst✝ : Algebra R F
pb : PowerBasis R S
hE : (Polynomial.map (algebraMap R F) (minpoly R pb.gen)).Splits
hfx : IsSeparable R pb.gen
this : DecidableEq F := Classical.decEq F
⊢ ∀ (x : { x // x ∈ (minpoly R pb.gen).aroots F }), ↑x = _root_.id ↑x
Module: Mathlib.RingTheory.Norm.Basic

Goal state before:
pp: K : Type u_4
L : Type u_5
F : Type u_6
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Field F
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra K F
E : Type u_7
inst✝⁶ : Field E
inst✝⁵ : Algebra K E
inst✝⁴ : Algebra L F
inst✝³ : IsScalarTower K L F
inst✝² : IsAlgClosed E
inst✝¹ : Algebra.IsSeparable K F
inst✝ : FiniteDimensional K F
pb : PowerBasis K L
this✝² : FiniteDimensional L F
this✝¹ : Algebra.IsSeparable L F
this✝ : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
σ : L →ₐ[K] E
x✝ : σ ∈ Finset.univ
this : Algebra L E := σ.toAlgebra
⊢ ∏ s, ⟨σ, s⟩.fst pb.gen = σ pb.gen ^ finrank L F

Tactic:
simp_rw [Finset.prod_const]

Goal state after:
K : Type u_4
L : Type u_5
F : Type u_6
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Field F
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra K F
E : Type u_7
inst✝⁶ : Field E
inst✝⁵ : Algebra K E
inst✝⁴ : Algebra L F
inst✝³ : IsScalarTower K L F
inst✝² : IsAlgClosed E
inst✝¹ : Algebra.IsSeparable K F
inst✝ : FiniteDimensional K F
pb : PowerBasis K L
this✝² : FiniteDimensional L F
this✝¹ : Algebra.IsSeparable L F
this✝ : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
σ : L →ₐ[K] E
x✝ : σ ∈ Finset.univ
this : Algebra L E := σ.toAlgebra
⊢ σ pb.gen ^ Finset.univ.card = σ pb.gen ^ finrank L F
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative

Goal state before:
pp: case neg.refine_2.inl.inl
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_3
inst✝ : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this✝¹ : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝ : Nontrivial α
this : StrongNormalizationMonoid α := UniqueFactorizationMonoid.strongNormalizationMonoid
p : α
hp : p ∈ normalizedFactors a
q : α
hq : q ∈ normalizedFactors a
hdvd : p ∣ q
⊢ p = q

Tactic:
rw [← normalize_normalized_factor _ hp, ← normalize_normalized_factor _ hq]

Goal state after:
case neg.refine_2.inl.inl
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_3
inst✝ : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this✝¹ : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝ : Nontrivial α
this : StrongNormalizationMonoid α := UniqueFactorizationMonoid.strongNormalizationMonoid
p : α
hp : p ∈ normalizedFactors a
q : α
hq : q ∈ normalizedFactors a
hdvd : p ∣ q
⊢ normalize p = normalize q
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative

Goal state before:
pp: case neg.refine_2.inl.inr
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_3
inst✝ : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this✝¹ : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝ : Nontrivial α
this : StrongNormalizationMonoid α := UniqueFactorizationMonoid.strongNormalizationMonoid
p : α
hp : p ∈ normalizedFactors a
q : α
hq : q ∈ normalizedFactors b
hdvd : p ∣ q
⊢ p = q

Tactic:
rw [← normalize_normalized_factor _ hp, ← normalize_normalized_factor _ hq]

Goal state after:
case neg.refine_2.inl.inr
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_3
inst✝ : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this✝¹ : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝ : Nontrivial α
this : StrongNormalizationMonoid α := UniqueFactorizationMonoid.strongNormalizationMonoid
p : α
hp : p ∈ normalizedFactors a
q : α
hq : q ∈ normalizedFactors b
hdvd : p ∣ q
⊢ normalize p = normalize q
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative

Goal state before:
pp: case neg.refine_2.inr.inl
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_3
inst✝ : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this✝¹ : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝ : Nontrivial α
this : StrongNormalizationMonoid α := UniqueFactorizationMonoid.strongNormalizationMonoid
p : α
hp : p ∈ normalizedFactors b
q : α
hq : q ∈ normalizedFactors a
hdvd : p ∣ q
⊢ p = q

Tactic:
rw [← normalize_normalized_factor _ hp, ← normalize_normalized_factor _ hq]

Goal state after:
case neg.refine_2.inr.inl
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_3
inst✝ : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this✝¹ : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝ : Nontrivial α
this : StrongNormalizationMonoid α := UniqueFactorizationMonoid.strongNormalizationMonoid
p : α
hp : p ∈ normalizedFactors b
q : α
hq : q ∈ normalizedFactors a
hdvd : p ∣ q
⊢ normalize p = normalize q
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative

Goal state before:
pp: case neg.refine_2.inr.inr
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_3
inst✝ : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this✝¹ : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝ : Nontrivial α
this : StrongNormalizationMonoid α := UniqueFactorizationMonoid.strongNormalizationMonoid
p : α
hp : p ∈ normalizedFactors b
q : α
hq : q ∈ normalizedFactors b
hdvd : p ∣ q
⊢ p = q

Tactic:
rw [← normalize_normalized_factor _ hp, ← normalize_normalized_factor _ hq]

Goal state after:
case neg.refine_2.inr.inr
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_3
inst✝ : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this✝¹ : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝ : Nontrivial α
this : StrongNormalizationMonoid α := UniqueFactorizationMonoid.strongNormalizationMonoid
p : α
hp : p ∈ normalizedFactors b
q : α
hq : q ∈ normalizedFactors b
hdvd : p ∣ q
⊢ normalize p = normalize q
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: case neg
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
r : S
hr : ¬r = 0
b : Basis (Free.ChooseBasisIndex ℤ S) ℤ S := Free.chooseBasis ℤ S
⊢ absNorm (span {r}) = (LinearMap.det ((Algebra.lmul ℤ S) r)).natAbs

Tactic:
rw [← natAbs_det_equiv _ (b.equiv (basisSpanSingleton b hr) (Equiv.refl _))]

Goal state after:
case neg
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
r : S
hr : ¬r = 0
b : Basis (Free.ChooseBasisIndex ℤ S) ℤ S := Free.chooseBasis ℤ S
⊢ (LinearMap.det
        (↑ℤ (Submodule.subtype (span {r})) ∘ₗ
          (↑(b.equiv (basisSpanSingleton b hr) (Equiv.refl (Free.ChooseBasisIndex ℤ S)))).toIntLinearMap)).natAbs =
    (LinearMap.det ((Algebra.lmul ℤ S) r)).natAbs
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' := ⋯ }
⊢ IsNoetherian R (R ⧸ (LinearMap.toSpanSingleton R M i).ker)

Tactic:
rw [(e _).isNoetherian_iff_of_bijective Function.bijective_id]

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' := ⋯ }
⊢ IsNoetherian (R ⧸ (LinearMap.toSpanSingleton R M i).ker) (R ⧸ (LinearMap.toSpanSingleton R M i).ker)
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
h : IsFiniteLength B M
s : CompositionSeries (Submodule B M)
hs_bot : RelSeries.head s = ⊥
hs_top : RelSeries.last s = ⊤
this : ∀ (k : Fin (s.length + 1)), length A ↥(s.toFun k) = ↑↑k * length (ResidueField A) (ResidueField B)
⊢ length A M = ↑s.length * length (ResidueField A) (ResidueField B)

Tactic:
← Fin.val_last s.length,

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
h : IsFiniteLength B M
s : CompositionSeries (Submodule B M)
hs_bot : RelSeries.head s = ⊥
hs_top : RelSeries.last s = ⊤
this : ∀ (k : Fin (s.length + 1)), length A ↥(s.toFun k) = ↑↑k * length (ResidueField A) (ResidueField B)
⊢ length A M = ↑↑(Fin.last s.length) * 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
h : IsFiniteLength A M
s : CompositionSeries (Submodule A M)
hs_bot : RelSeries.head s = ⊥
hs_top : RelSeries.last s = ⊤
this :
  ∀ (k : Fin (s.length + 1)),
    length B ↥(Submodule.baseChange B (s.toFun k)) = ↑↑k * length B (B ⧸ Ideal.map (algebraMap A B) (maximalIdeal A))
⊢ length B (B ⊗[A] M) = ↑s.length * length B (B ⧸ Ideal.map (algebraMap A B) (maximalIdeal A))

Tactic:
← Fin.val_last s.length,

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
h : IsFiniteLength A M
s : CompositionSeries (Submodule A M)
hs_bot : RelSeries.head s = ⊥
hs_top : RelSeries.last s = ⊤
this :
  ∀ (k : Fin (s.length + 1)),
    length B ↥(Submodule.baseChange B (s.toFun k)) = ↑↑k * length B (B ⧸ Ideal.map (algebraMap A B) (maximalIdeal A))
⊢ length B (B ⊗[A] M) = ↑↑(Fin.last s.length) * length B (B ⧸ Ideal.map (algebraMap A B) (maximalIdeal A))
Module: Mathlib.NumberTheory.RamificationInertia.Ramification

Goal state before:
pp: case pos
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : Ideal R
P : Ideal S
hp : map f p ≤ P
H : ∀ (n : ℕ), ∃ k, map f p ≤ P ^ k ∧ n < k
k : ℕ
hk : map f p ≤ P ^ k
h2k : 2 < k
⊢ p.ramificationIdx' P ≠ 1 ↔ map f p ≤ P ^ 2

Tactic:
simp [Ideal.ramificationIdx'_eq_zero H, hk.trans (Ideal.pow_le_pow_right h2k.le)]

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

Goal state before:
pp: case pos
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : Ideal R
P : Ideal S
hp : map f p ≤ P
H : ∀ (n : ℕ), ∃ k, map f p ≤ P ^ k ∧ n < k
⊢ p.ramificationIdx' P ≠ 1 ↔ map f p ≤ P ^ 2

Tactic:
obtain ⟨k, hk, h2k⟩ := H 2
    simp [Ideal.ramificationIdx'_eq_zero H, hk.trans (Ideal.pow_le_pow_right h2k.le)]

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

Goal state before:
pp: case mpr.refine_2
R : Type v
inst✝³ : CommRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Small.{w, u} A
H :
  ∀ ⦃B : Type u⦄ [inst : CommRing B] [Small.{w, u} B] [inst_2 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp
h : Nontrivial Ω[A⁄R]
f₁ f₂ : { f // (TensorProduct.lmul' R).kerSquareLift.comp f = AlgHom.id R A }
e : f₁ ≠ f₂
f : Ideal (A ⊗[R] A ⧸ RingHom.ker (TensorProduct.lmul' R).toRingHom ^ 2) :=
  RingHom.ker (TensorProduct.lmul' R).kerSquareLift.toRingHom
⊢ (Ideal.Quotient.mkₐ R (RingHom.ker (TensorProduct.lmul' R).kerSquareLift.toRingHom)).comp ↑f₁ =
    (Ideal.Quotient.mkₐ R (RingHom.ker (TensorProduct.lmul' R).kerSquareLift.toRingHom)).comp ↑f₂

Tactic:
· ext x
      apply RingHom.kerLift_injective (TensorProduct.lmul' R (S := A)).kerSquareLift.toRingHom
      simpa using DFunLike.congr_fun (f₁.2.trans f₂.2.symm) x

Goal state after:
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
inst✝ : EssFiniteType R S
⊢ Subsingleton (KaehlerDifferential.ideal R S).Cotangent ↔
    ∃ t, (∀ (s : S), (1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) * t = 0) ∧ (TensorProduct.lmul' R) t = 1

Tactic:
Ideal.cotangent_subsingleton_iff,

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : EssFiniteType R S
⊢ IsIdempotentElem (KaehlerDifferential.ideal R S) ↔
    ∃ t, (∀ (s : S), (1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) * t = 0) ∧ (TensorProduct.lmul' R) t = 1
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : EssFiniteType R S
inst✝ : FormallyUnramified R S
⊢ ∃ T x x_1, Nonempty (S ⊗[R] S ≃ₐ[S] S × T)

Tactic:
obtain ⟨e, he, hsp⟩ : ∃ e, IsIdempotentElem e ∧ KaehlerDifferential.ideal R S = S ⊗[R] S ∙ e :=
    (Ideal.isIdempotentElem_iff_of_fg _ (KaehlerDifferential.ideal_fg R S)).mp <|
      (Ideal.cotangent_subsingleton_iff _).mp <| inferInstanceAs <| Subsingleton Ω[S⁄R]

Goal state after:
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : EssFiniteType R S
inst✝ : FormallyUnramified R S
e : S ⊗[R] S
he : IsIdempotentElem e
hsp : KaehlerDifferential.ideal R S = S ⊗[R] S ∙ e
⊢ ∃ T x x_1, Nonempty (S ⊗[R] S ≃ₐ[S] S × T)
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: case h1
R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : P.toExtension.Ring
hx : x ∈ P.toExtension.ker
⊢ ((Extension.Cotangent.map ((Q.ofComp P).toExtensionHom.comp (Q.toComp P).toExtensionHom))
        (Extension.Cotangent.mk ⟨x, hx⟩)).val =
    (0 (Extension.Cotangent.mk ⟨x, hx⟩)).val

Tactic:
simp only [map_mk, val_mk, LinearMap.zero_apply, val_zero]

Goal state after:
case h1
R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : P.toExtension.Ring
hx : x ∈ P.toExtension.ker
⊢ Q.toExtension.ker.toCotangent ⟨((Q.ofComp P).toExtensionHom.comp (Q.toComp P).toExtensionHom).toAlgHom x, ⋯⟩ = 0