mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
inst✝³ : Fintype K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Finite L
this✝ : Fintype L
m : ℕ
lt : m < Module.finrank K L
pos : 0 < m
eq : frobeniusAlgHom K L ^ m = 1
x : L
x✝ : x ∈ univ.val
this : (fun x ↦ x ^ q ^ m) x - x = 0
⊢ X ^ q ^ m - X ≠ 0 ∧ x ^ q ^ m - x = 0

Tactic:
refine ⟨fun h ↦ ?_, this⟩

Goal state after:
K : Type u_1
inst✝⁴ : Field K
inst✝³ : Fintype K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Finite L
this✝ : Fintype L
m : ℕ
lt : m < Module.finrank K L
pos : 0 < m
eq : frobeniusAlgHom K L ^ m = 1
x : L
x✝ : x ∈ univ.val
this : (fun x ↦ x ^ q ^ m) x - x = 0
h : X ^ q ^ m - X = 0
⊢ False
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case succ
p a m : ℕ
hm : (1 + p * a) ^ p ^ m ≡ 1 [MOD p ^ m]
⊢ (1 + p * a) ^ p ^ (m + 1) ≡ 1 [MOD p ^ (m + 1)]

Tactic:
rw [Nat.ModEq.comm, add_comm, Nat.modEq_iff_dvd' (Nat.one_le_pow' _ _)] at hm
    obtain ⟨d, hd⟩ := hm
    rw [tsub_eq_iff_eq_add_of_le (Nat.one_le_pow' _ _), add_comm] at hd
    rw [pow_succ, pow_mul, hd, add_pow, Finset.sum_range_succ', pow_zero, one_mul, one_pow,
      one_mul, Nat.choose_zero_right, Nat.cast_one]
    refine Nat.ModEq.add_right 1 (Nat.modEq_zero_iff_dvd.mpr ?_)
    simp_rw [one_pow, mul_one, pow_succ', mul_assoc, ← Finset.mul_sum]
    refine mul_dvd_mul_left (p ^ m) (dvd_mul_of_dvd_right (Finset.dvd_sum fun k hk ↦ ?_) d)
    cases m
    · rw [pow_zero, pow_one, one_mul, add_comm, add_left_inj] at hd
      cases k <;> simp [← hd, mul_assoc, pow_succ']
    · cases k <;> simp [mul_assoc, pow_succ']

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

Goal state before:
pp: F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
⊢ ringChar F = 2 ↔ Fintype.card F % 2 = 0

Tactic:
rcases FiniteField.card F (ringChar F) with ⟨n, hp, h⟩

Goal state after:
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
n : ℕ+
hp : Nat.Prime (ringChar F)
h : Fintype.card F = ringChar F ^ ↑n
⊢ ringChar F = 2 ↔ Fintype.card F % 2 = 0
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
hf : (Polynomial.map (algebraMap R F) (minpoly R pb.gen)).Splits
this✝ : Nontrivial R
this : (minpoly R pb.gen).Monic
⊢ (algebraMap R F) (-1) ^ (minpoly R pb.gen).natDegree *
      ((-1) ^ (minpoly R pb.gen).natDegree * (Polynomial.map (algebraMap R F) (minpoly R pb.gen)).roots.prod) =
    ((minpoly R pb.gen).aroots F).prod

Tactic:
← mul_assoc,

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
hf : (Polynomial.map (algebraMap R F) (minpoly R pb.gen)).Splits
this✝ : Nontrivial R
this : (minpoly R pb.gen).Monic
⊢ (algebraMap R F) (-1) ^ (minpoly R pb.gen).natDegree * (-1) ^ (minpoly R pb.gen).natDegree *
      (Polynomial.map (algebraMap R F) (minpoly R pb.gen)).roots.prod =
    ((minpoly R pb.gen).aroots F).prod
Module: Mathlib.RingTheory.Norm.Basic

Goal state before:
pp: case mp.refine_2
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : Ring S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : Free R S
inst✝ : Module.Finite R S
x : S
b : Basis (Free.ChooseBasisIndex R S) R S := Free.chooseBasis R S
decEq : DecidableEq (Free.ChooseBasisIndex R S) := Classical.decEq (Free.ChooseBasisIndex R S)
v : Free.ChooseBasisIndex R S → R
v_ne : v ≠ 0
hv : ⇑(b.repr (x * ∑ i, v i • b i)) = 0
⊢ ∑ i, v i • b i ≠ 0

Tactic:
contrapose v_ne with sum_eq

Goal state after:
case mp.refine_2
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : Ring S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : Free R S
inst✝ : Module.Finite R S
x : S
b : Basis (Free.ChooseBasisIndex R S) R S := Free.chooseBasis R S
decEq : DecidableEq (Free.ChooseBasisIndex R S) := Classical.decEq (Free.ChooseBasisIndex R S)
v : Free.ChooseBasisIndex R S → R
hv : ⇑(b.repr (x * ∑ i, v i • b i)) = 0
sum_eq : ∑ i, v i • b i = 0
⊢ v = 0
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 = ∏ σ, σ pb.gen

Tactic:
rw [@Fintype.prod_equiv (S →ₐ[R] F) _ _ (PowerBasis.AlgHom.fintype pb) _ _ pb.liftEquiv'
    (fun σ => σ pb.gen) (fun x => x) ?_]

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 = ∏ x, ↑x

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 : S →ₐ[R] F), x pb.gen = ↑(pb.liftEquiv' x)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative

Goal state before:
pp: case neg.refine_2
α : 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 : α),
    p ∈ normalizedFactors a ∨ p ∈ normalizedFactors b →
      ∀ (q : α), q ∈ normalizedFactors a ∨ q ∈ normalizedFactors b → p ∣ q → p = q

Tactic:
· rintro p (hp | hp) q (hq | hq) hdvd <;>
      rw [← normalize_normalized_factor _ hp, ← normalize_normalized_factor _ hq] <;>
      exact
        normalize_eq_normalize hdvd
          ((prime_of_normalized_factor _ hp).irreducible.dvd_symm
            (prime_of_normalized_factor _ hq).irreducible hdvd)

Goal state after:
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDedekindDomain S
inst✝ : Free ℤ S
I J : Ideal S
⊢ cardQuot (I * J) = cardQuot I * cardQuot J

Tactic:
rw [cardQuot_mul]

Goal state after:
Module: Mathlib.GroupTheory.Submonoid.Inverses

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
S : Submonoid M
x y : M
z : ↥S
h₁ : y * ↑z = 1
h₂ : x * y = 1
⊢ x * (y * ↑z) = ↑z

Tactic:
← mul_assoc,

Goal state after:
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
x y : M
z : ↥S
h₁ : y * ↑z = 1
h₂ : x * y = 1
⊢ x * y * ↑z = ↑z
Module: Mathlib.RingTheory.Localization.InvSubmonoid

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
⊢ Submodule.span R ↑(invSubmonoid M S) = ⊤

Tactic:
rw [eq_top_iff]
  rintro x -
  rcases IsLocalization.surj'' M x with ⟨r, m, rfl⟩
  exact Submodule.smul_mem _ _ (Submodule.subset_span (toInvSubmonoid M S m).prop)

Goal state after:
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: case mp
X : Type u_1
inst✝ : TopologicalSpace X
H : ∀ {Z : Set X}, IsClosed[inst✝] Z → closure[inst✝] (Z ∩ closedPoints X) = Z
Z : Set X
hZ : Z ≠ ∅
⊢ IsClosed[inst✝] (closure[inst✝] Z \ Z) → Z ∩ closedPoints X ≠ ∅

Tactic:
hZ'

Goal state after:
case mp
X : Type u_1
inst✝ : TopologicalSpace X
H : ∀ {Z : Set X}, IsClosed[inst✝] Z → closure[inst✝] (Z ∩ closedPoints X) = Z
Z : Set X
hZ : Z ≠ ∅
hZ' : IsClosed[inst✝] (closure[inst✝] Z \ Z)
⊢ Z ∩ closedPoints X ≠ ∅
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: X : Type u_2
Y : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : JacobsonSpace Y
hf : IsOpenEmbedding f
Z : Set X
hZ : Z.Nonempty
⊢ IsLocallyClosed Z → (Z ∩ f ⁻¹' closedPoints Y).Nonempty

Tactic:
hZ'

Goal state after:
X : Type u_2
Y : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : JacobsonSpace Y
hf : IsOpenEmbedding f
Z : Set X
hZ : Z.Nonempty
hZ' : IsLocallyClosed Z
⊢ (Z ∩ f ⁻¹' closedPoints Y).Nonempty
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: X : Type u_2
Y : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : JacobsonSpace Y
hf : IsClosedEmbedding f
Z : Set X
hZ : Z.Nonempty
⊢ IsLocallyClosed Z → (Z ∩ f ⁻¹' closedPoints Y).Nonempty

Tactic:
hZ'

Goal state after:
X : Type u_2
Y : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : JacobsonSpace Y
hf : IsClosedEmbedding f
Z : Set X
hZ : Z.Nonempty
hZ' : IsLocallyClosed Z
⊢ (Z ∩ f ⁻¹' closedPoints Y).Nonempty
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_1
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), JacobsonSpace ↥(U i)
Z : Set X
hZ : Z.Nonempty
⊢ IsLocallyClosed Z → (Z ∩ closedPoints X).Nonempty

Tactic:
hZ'

Goal state after:
X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_1
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), JacobsonSpace ↥(U i)
Z : Set X
hZ : Z.Nonempty
hZ' : IsLocallyClosed Z
⊢ (Z ∩ closedPoints X).Nonempty
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDedekindDomain S
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
n : ℕ
inst✝ : CharZero S
⊢ Nat.card { I // absNorm I ≤ n } = Nat.card { I // absNorm ↑I ≤ n } + 1

Tactic:
by
  classical
  have : Finite {I : Ideal S // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n} :=
    (finite_setOfPred_absNorm_le n).subset fun _ ⟨_, h⟩ ↦ h
  have : Finite {I : Ideal S // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n} :=
    (finite_setOfPred_absNorm_le n).subset fun _ ⟨_, h⟩ ↦ h
  rw [Nat.card_congr (Equiv.subtypeSubtypeEquivSubtypeInter (fun I ↦ I ∈ (Ideal S)⁰)
    (fun I ↦ absNorm I ≤ n))]
  let e : {I : Ideal S // absNorm I ≤ n} ≃ {I : Ideal S // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n} ⊕
      {I : Ideal S // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n} := by
    refine (Equiv.subtypeEquivRight ?_).trans (subtypeOrEquiv _ _ ?_)
    · intro _
      simp_rw [← or_and_right, em, true_and]
    · exact Pi.disjoint_iff.mpr fun I ↦ Prop.disjoint_iff.mpr (by tauto)
  simp_rw [Nat.card_congr e, Nat.card_sum, add_right_inj]
  conv_lhs =>
    enter [1, 1, I]
    rw [← absNorm_ne_zero_iff_mem_nonZeroDivisors, ne_eq, not_not, and_iff_left_iff_imp.mpr
      (fun h ↦ by rw [h]; exact Nat.zero_le n), absNorm_eq_zero_iff]
  rw [Nat.card_unique]

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
S₁ : Type u_1
inst✝¹ : CommRing S₁
inst✝ : Algebra R S₁
e : S ≃ₐ[R] S₁
P : Ideal S₁
n : ℕ
⊢ n ∈ {n | map f p ≤ comap e P ^ n} ↔ n ∈ {n | map (algebraMap R S₁) p ≤ P ^ n}

Tactic:
simp only [Set.mem_ofPred_eq, Ideal.map_le_iff_le_comap]

Goal state after:
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal R
S₁ : Type u_1
inst✝¹ : CommRing S₁
inst✝ : Algebra R S₁
e : S ≃ₐ[R] S₁
P : Ideal S₁
n : ℕ
⊢ p ≤ comap f (comap e P ^ n) ↔ p ≤ comap (algebraMap R S₁) (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
S₁ : Type u_1
inst✝³ : CommRing S₁
inst✝² : Algebra R S₁
E : Type u_2
inst✝¹ : EquivLike E S S₁
inst✝ : AlgEquivClass E R S S₁
P : Ideal S
e : E
⊢ p.ramificationIdx' (map e P) = p.ramificationIdx' P

Tactic:
show P.map e = _ from P.map_comap_of_equiv (RingEquivClass.toRingEquiv e : S ≃+* S₁)

Goal state after:
R : Type u
inst✝⁶ : CommRing R
S : Type v
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
p : Ideal R
S₁ : Type u_1
inst✝³ : CommRing S₁
inst✝² : Algebra R S₁
E : Type u_2
inst✝¹ : EquivLike E S S₁
inst✝ : AlgEquivClass E R S S₁
P : Ideal S
e : E
⊢ p.ramificationIdx' (comap (↑e).symm P) = p.ramificationIdx' 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
p : Ideal R
S₁ : Type u_1
inst✝³ : CommRing S₁
inst✝² : Algebra R S₁
E : Type u_2
inst✝¹ : EquivLike E S S₁
inst✝ : AlgEquivClass E R S S₁
P : Ideal S
e : E
⊢ p.ramificationIdx' (comap (↑e).symm P) = p.ramificationIdx' P

Tactic:
exact p.ramificationIdx'_comap_eq (AlgEquivClass.toAlgEquiv e).symm P

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

Goal state before:
pp: case mp
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I.FG
e : IsIdempotentElem I
r : R
hr : r ∈ I
hr' : ∀ n ∈ I, r * n = n
x : R
hx : x ∈ I
⊢ r * x ∈ R ∙ r

Tactic:
exact Ideal.mem_span_singleton'.mpr ⟨_, mul_comm _ _⟩

Goal state after:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Instances

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 A
inst✝⁸ : Algebra A B
inst✝⁷ : Algebra R B
inst✝⁶ : IsScalarTower R A B
p : Ideal A
q : Ideal B
inst✝⁵ : q.LiesOver p
inst✝⁴ : p.IsPrime
inst✝³ : q.IsPrime
inst✝² : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝¹ : Localization.AtPrime.IsLiesOverAlgebra p q
inst✝ : Algebra.IsIntegral A B
this✝³ : Algebra.IsIntegral (A ⧸ p) (B ⧸ q)
this✝² : Algebra (A ⧸ p) q.ResidueField :=
  ((algebraMap (B ⧸ q) q.ResidueField).comp (algebraMap (A ⧸ p) (B ⧸ q))).toAlgebra
this✝¹ : IsScalarTower (A ⧸ p) (B ⧸ q) q.ResidueField
this✝ : Algebra.IsAlgebraic (A ⧸ p) q.ResidueField
this : IsScalarTower (A ⧸ p) p.ResidueField q.ResidueField
⊢ Algebra.IsAlgebraic p.ResidueField q.ResidueField

Tactic:
refine .extendScalars (Ideal.injective_algebraMap_quotient_residueField p)

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

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
inst✝² : FormallyUnramified R A
e : A ≃ₐ[R] B
C : Type u_3
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[R] C
e' : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂
⊢ f₁.comp (AlgHom.id R B) = f₂.comp (AlgHom.id R B)

Tactic:
← e.comp_symm,

Goal state after:
R : Type u_1
inst✝⁷ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
inst✝² : FormallyUnramified R A
e : A ≃ₐ[R] B
C : Type u_3
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[R] C
e' : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂
⊢ f₁.comp ((↑e).comp ↑e.symm) = f₂.comp ((↑e).comp ↑e.symm)
Module: Mathlib.RingTheory.Unramified.Finite

Goal state before:
pp: case mp.refine_1
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : EssFiniteType R S
this : ∀ (t : S ⊗[R] S), (TensorProduct.lmul' R) t = 1 ↔ 1 - t ∈ KaehlerDifferential.ideal R S
e : S ⊗[R] S
he₁ : IsIdempotentElem e
he₂ : Ideal.span (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) = Ideal.span {e}
s : S
x : S ⊗[R] S
hx : 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1 = e * x
⊢ (1 - e) * (e * x) = 0

Tactic:
← mul_assoc,

Goal state after:
case mp.refine_1
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : EssFiniteType R S
this : ∀ (t : S ⊗[R] S), (TensorProduct.lmul' R) t = 1 ↔ 1 - t ∈ KaehlerDifferential.ideal R S
e : S ⊗[R] S
he₁ : IsIdempotentElem e
he₂ : Ideal.span (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) = Ideal.span {e}
s : S
x : S ⊗[R] S
hx : 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1 = e * x
⊢ (1 - e) * e * x = 0
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
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : FormallyUnramified R S
inst✝ : EssFiniteType R S
r : S
m : M
⊢ (((TensorProduct.AlgebraTensorModule.mapBilinear R S S S S S M) LinearMap.id).flip (elem R S) ∘ₗ
          (lsmul R R M).toLinearMap.flip).toFun
      (r • m) =
    (RingHom.id S) r •
      (((TensorProduct.AlgebraTensorModule.mapBilinear R S S S S S M) LinearMap.id).flip (elem R S) ∘ₗ
            (lsmul R R M).toLinearMap.flip).toFun
        m

Tactic:
simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, LinearMap.coe_comp, Function.comp_apply,
      LinearMap.flip_apply, TensorProduct.AlgebraTensorModule.mapBilinear_apply, RingHom.id_apply]
    trans (TensorProduct.AlgebraTensorModule.map (LinearMap.id (R := S) (M := S))
      ((LinearMap.flip (AlgHom.toLinearMap (lsmul R R M))) m)) ((1 ⊗ₜ r) * elem R S)
    · induction elem R S using TensorProduct.induction_on
      · simp
      · simp [smul_comm r]
      · simp only [map_add, mul_add, *]
    · have := one_tmul_sub_tmul_one_mul_elem (R := R) r
      rw [sub_mul, sub_eq_zero] at this
      rw [this]
      induction elem R S using TensorProduct.induction_on
      · simp
      · simp [TensorProduct.smul_tmul']
      · simp only [map_add, smul_add, mul_add, *]

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

Goal state before:
pp: case mp
R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
P : Extension R A
inst✝ : FormallySmooth R P.Ring
e : P.ker.Cotangent ≃ₗ[P.Ring] P.Cotangent := ⋯
⊢ (∃ l, l ∘ₗ kerCotangentToTensor R P.Ring A = LinearMap.id) → ∃ l, l ∘ₗ P.cotangentComplex = LinearMap.id

pp: case mpr
R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
P : Extension R A
inst✝ : FormallySmooth R P.Ring
e : P.ker.Cotangent ≃ₗ[P.Ring] P.Cotangent := ⋯
⊢ (∃ l, l ∘ₗ P.cotangentComplex = LinearMap.id) → ∃ l, l ∘ₗ kerCotangentToTensor R P.Ring A = LinearMap.id

Tactic:
· intro ⟨l, hl⟩
    exact ⟨(e.comp l).extendScalarsOfSurjective P.algebraMap_surjective,
      LinearMap.ext (DFunLike.congr_fun hl : _)⟩

Goal state after:
case mpr
R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
P : Extension R A
inst✝ : FormallySmooth R P.Ring
e : P.ker.Cotangent ≃ₗ[P.Ring] P.Cotangent := ⋯
⊢ (∃ l, l ∘ₗ P.cotangentComplex = LinearMap.id) → ∃ l, l ∘ₗ kerCotangentToTensor R P.Ring A = LinearMap.id
Module: Mathlib.RingTheory.Etale.Kaehler

Goal state before:
pp: case zero
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
P : Extension R S
Q : Extension R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
H : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
⊢ (tensorCotangentInvFun f halg H) ((LinearMap.liftBaseChange T (Cotangent.map f)) 0) = 0

Tactic:
simp only [map_zero]

Goal state after:
Module: Mathlib.RingTheory.Etale.Kaehler

Goal state before:
pp: case zero
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
P : Extension R S
Q : Extension R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
H : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
⊢ (LinearMap.liftBaseChange T (Cotangent.map f))
      ((tensorCotangentInvFun f halg H) (Cotangent.mk ((LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) 0))) =
    Cotangent.mk ((LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) 0)

Tactic:
simp only [map_zero]

Goal state after:
Module: Mathlib.RingTheory.Etale.Kaehler

Goal state before:
pp: case left
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
P : Extension R S
Q : Extension R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
inst✝ : Module.Flat S T
H₁ : f.toRingHom.FormallyEtale
H₂ : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
x : T ⊗[S] P.H1Cotangent
hx : (LinearMap.liftBaseChange T (H1Cotangent.map f)) x = 0
⊢ (tensorCotangent f halg H₂) ((LinearMap.lTensor T h1Cotangentι) x) =
    (tensorCotangent f halg H₂) ((LinearMap.lTensor T h1Cotangentι) 0)

Tactic:
simp only [map_zero]

Goal state after:
case left
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
P : Extension R S
Q : Extension R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
inst✝ : Module.Flat S T
H₁ : f.toRingHom.FormallyEtale
H₂ : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
x : T ⊗[S] P.H1Cotangent
hx : (LinearMap.liftBaseChange T (H1Cotangent.map f)) x = 0
⊢ (tensorCotangent f halg H₂) ((LinearMap.lTensor T h1Cotangentι) x) = 0
Module: Mathlib.RingTheory.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 R T
inst✝⁷ : Algebra S T
inst✝⁶ : IsScalarTower R S T
q : Ideal S
r : Ideal T
inst✝⁵ : q.IsPrime
inst✝⁴ : r.IsPrime
inst✝³ : r.LiesOver q
inst✝² : Algebra (Localization.AtPrime q) (Localization.AtPrime r)
inst✝¹ : Localization.AtPrime.IsLiesOverAlgebra q r
inst✝ : Module.Flat (Localization.AtPrime q) (Localization.AtPrime r)
this : q.LiesOver (under R r)
⊢ r.ramificationIdx R = q.ramificationIdx R * r.ramificationIdx S

Tactic:
let f := (Ideal.quotientEquivAlgOfEq (Localization.AtPrime r)
    (by rw [map_map, ← IsScalarTower.algebraMap_eq])).trans
      (Algebra.TensorProduct.quotIdealMapEquivTensorQuot (Localization.AtPrime r)
        ((r.under R).map (algebraMap R (Localization.AtPrime q))))

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
q : Ideal S
r : Ideal T
inst✝⁵ : q.IsPrime
inst✝⁴ : r.IsPrime
inst✝³ : r.LiesOver q
inst✝² : Algebra (Localization.AtPrime q) (Localization.AtPrime r)
inst✝¹ : Localization.AtPrime.IsLiesOverAlgebra q r
inst✝ : Module.Flat (Localization.AtPrime q) (Localization.AtPrime r)
this : q.LiesOver (under R r)
f : (Localization.AtPrime r ⧸ map (algebraMap R (Localization.AtPrime r)) (under R r)) ≃ₐ[Localization.AtPrime r]
  TensorProduct (Localization.AtPrime q) (Localization.AtPrime r)
    (Localization.AtPrime q ⧸ map (algebraMap R (Localization.AtPrime q)) (under R r)) :=
  (quotientEquivAlgOfEq (Localization.AtPrime r) ⋯).trans
    (Algebra.TensorProduct.quotIdealMapEquivTensorQuot (Localization.AtPrime r)
      (map (algebraMap R (Localization.AtPrime q)) (under R r)))
⊢ r.ramificationIdx R = q.ramificationIdx R * r.ramificationIdx S
Module: Mathlib.RingTheory.RamificationInertia.Basic

Goal state before:
pp: R : Type u_1
inst✝¹¹ : CommRing R
p : Ideal R
inst✝¹⁰ : p.IsPrime
S : Type u_2
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : IsDomain R
inst✝⁶ : IsDomain S
inst✝⁵ : Module.Finite R S
inst✝⁴ : Module.Flat R S
inst✝³ : Fintype ↑(p.primesOver S)
G : Type u_3
inst✝² : Group G
inst✝¹ : MulSemiringAction G S
inst✝ : IsGaloisGroup G R S
⊢ ∑ q, (↑q).ramificationIdx R * (↑q).inertiaDeg R = Nat.card G

Tactic:
by
  let := IsGaloisGroup.finite G R S
  rw [sum_ramification_inertia_eq_finrank, IsGaloisGroup.card_eq_finrank' G R S]

Goal state after: