mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: case inr.inr
ι : Type u
R : Type u_1
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : NoZeroDivisors S
s : Set ι
i j : ι
v : ι → S
hj✝ : j ∈ insert i s
H₁ : IsTranscendenceBasis R fun x ↦ v ↑x
this✝³ : Nontrivial ↥(adjoin R (v '' (insert i s \ {j})))
this✝² : Nontrivial S
this✝¹ : IsDomain S
H₂ : v j ∈ (matroid R S).closure (v '' (insert i s \ {j}))
this✝ : Nontrivial R
inj : InjOn v s
H' : (matroid R S).IsBase (v '' s)
hj : j ∈ s
Hj : v j ∉ (matroid R S).closure (v '' s \ {v j})
hi : i ∉ s
ne : v i ≠ v j
hi' : v i ∉ v '' s
this : InjOn v (insert i s)
⊢ (matroid R S).IsBase (v '' (insert i s \ {j}))

Tactic:
rw [this.image_sdiff_subset (singleton_subset_iff.mpr (.inr hj)), image_singleton,
    image_insert_eq] at H₂ ⊢

Goal state after:
case inr.inr
ι : Type u
R : Type u_1
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : NoZeroDivisors S
s : Set ι
i j : ι
v : ι → S
hj✝ : j ∈ insert i s
H₁ : IsTranscendenceBasis R fun x ↦ v ↑x
this✝³ : Nontrivial ↥(adjoin R (v '' (insert i s \ {j})))
this✝² : Nontrivial S
this✝¹ : IsDomain S
H₂ : v j ∈ (matroid R S).closure (insert (v i) (v '' s) \ {v j})
this✝ : Nontrivial R
inj : InjOn v s
H' : (matroid R S).IsBase (v '' s)
hj : j ∈ s
Hj : v j ∉ (matroid R S).closure (v '' s \ {v j})
hi : i ∉ s
ne : v i ≠ v j
hi' : v i ∉ v '' s
this : InjOn v (insert i s)
⊢ (matroid R S).IsBase (insert (v i) (v '' s) \ {v j})
Module: Mathlib.FieldTheory.Galois.Basic

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
K L : IntermediateField F E
φ : Gal(E/F)
⊢ φ ∈ (K ⊔ L).fixingSubgroup ↔ φ ∈ K.fixingSubgroup ⊓ L.fixingSubgroup

Tactic:
exact ⟨fun h ↦ ⟨fixingSubgroup_antitone le_sup_left h, fixingSubgroup_antitone le_sup_right h⟩,
    by simp [← Subgroup.zpowers_le, ← IntermediateField.le_iff_le]⟩

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

Goal state before:
pp: F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
H : Subgroup Gal(E/F)
inst✝ : FiniteDimensional F E
H_le : H ≤ (fixedField H).fixingSubgroup
⊢ (fixedField H).fixingSubgroup = H

Tactic:
suffices Nat.card H = Nat.card (fixingSubgroup (fixedField H)) by
    exact SetLike.coe_injective (Set.eq_of_inclusion_surjective
      ((Nat.bijective_iff_injective_and_card (Set.inclusion H_le)).mpr
        ⟨Set.inclusion_injective H_le, this⟩).2).symm

Goal state after:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
H : Subgroup Gal(E/F)
inst✝ : FiniteDimensional F E
H_le : H ≤ (fixedField H).fixingSubgroup
⊢ Nat.card ↥H = Nat.card ↥(fixedField H).fixingSubgroup
Module: Mathlib.FieldTheory.Galois.Basic

Goal state before:
pp: F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
K : IntermediateField F E
inst✝ : FiniteDimensional F E
h : IsGalois F E
K_le : K ≤ fixedField K.fixingSubgroup
⊢ finrank (↥K) E = Nat.card Gal(E/↥K)

Tactic:
exact (card_aut_eq_finrank K E).symm

Goal state after:
Module: Mathlib.FieldTheory.KrullTopology

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsIntegral K L
σ τ : Gal(L/K)
h_diff : σ ≠ τ
hστ : σ⁻¹ * τ ≠ 1
x : L
hx : (σ⁻¹ * τ) x ≠ x
E : IntermediateField K L := K⟮x⟯
this : FiniteDimensional K ↥K⟮x⟯
⊢ ∃ x, ∃ (_ : x ∈ E), ¬(σ⁻¹ * τ) x = x

Tactic:
exact ⟨x, IntermediateField.mem_adjoin_simple_self K x, hx⟩

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

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
K L : IntermediateField F E
inst✝ : Normal F ↥K
φ : Gal(E/↥L)
x : ↥K
⊢ ↑(((restrictRestrictAlgEquivMapHom F (↥K) (↥L) E) φ) x) = φ ↑x

Tactic:
by
  simp [restrictRestrictAlgEquivMapHom, AlgEquiv.restrictNormalHom_apply]

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

Goal state before:
pp: F : Type u_1
E' : Type u_3
inst✝³ : Field F
inst✝² : Field E'
inst✝¹ : Algebra F E'
inst✝ : IsGalois F E'
L : IntermediateField F E'
hnfd : FiniteDimensional F ↥L
E : IntermediateField F E' := normalClosure F (↥L) E'
hle : L ≤ E
L' : IntermediateField F ↥E := restrict hle
h : finrank F ↥L' * Nat.card ↥L'.fixingSubgroup = Nat.card Gal(↥E/F)
⊢ finrank F ↥L = L.fixingSubgroup.index

Tactic:
rw [← L'.fixingSubgroup.index_mul_card, Nat.mul_left_inj Finite.card_pos.ne'] at h

Goal state after:
F : Type u_1
E' : Type u_3
inst✝³ : Field F
inst✝² : Field E'
inst✝¹ : Algebra F E'
inst✝ : IsGalois F E'
L : IntermediateField F E'
hnfd : FiniteDimensional F ↥L
E : IntermediateField F E' := normalClosure F (↥L) E'
hle : L ≤ E
L' : IntermediateField F ↥E := restrict hle
h : finrank F ↥L' = L'.fixingSubgroup.index
⊢ finrank F ↥L = L.fixingSubgroup.index
Module: Mathlib.LinearAlgebra.BilinearForm.DualLattice

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Field S
inst✝⁶ : AddCommGroup M
inst✝⁵ : Algebra R S
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
B : BilinForm S M
inst✝¹ : IsDomain R
hB : B.Nondegenerate
inst✝ : IsTorsionFree R S
N : Submodule R M
hN : Submodule.span S ↑N = ⊤
x y : ↥(B.dualSubmodule N)
e : (B.dualSubmoduleToDual N) x = (B.dualSubmoduleToDual N) y
⊢ B ↑x = B ↑y

Tactic:
apply LinearMap.ext_on hN

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Field S
inst✝⁶ : AddCommGroup M
inst✝⁵ : Algebra R S
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
B : BilinForm S M
inst✝¹ : IsDomain R
hB : B.Nondegenerate
inst✝ : IsTorsionFree R S
N : Submodule R M
hN : Submodule.span S ↑N = ⊤
x y : ↥(B.dualSubmodule N)
e : (B.dualSubmoduleToDual N) x = (B.dualSubmoduleToDual N) y
⊢ Set.EqOn ⇑(B ↑x) ⇑(B ↑y) ↑N
Module: Mathlib.FieldTheory.Galois.Infinite

Goal state before:
pp: case refine_1
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
H : Subgroup Gal(K/k)
L : IntermediateField k K
inst✝ : Normal k ↥L
x : K
h : x ∈ ↑(fixedField H ⊓ L)
⊢ x ∈ ↑(lift (fixedField (Subgroup.map (restrictNormalHom ↥L) H)))

Tactic:
have xL := h.out.2
    apply (mem_lift (⟨x, xL⟩ : L)).mpr
    simp only [mem_fixedField_iff, Subgroup.mem_map, forall_exists_index, and_imp,
      forall_apply_eq_imp_iff₂]
    intro σ hσ
    apply Subtype.val_injective
    dsimp only
    nth_rw 2 [← (h.out.1 ⟨σ, hσ⟩)]
    exact AlgEquiv.restrictNormal_commutes σ L ⟨x, xL⟩

Goal state after:
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
⊢ L.fixingSubgroup.Normal ↔ IsGalois k ↥L

Tactic:
by
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · let g (x : K) := L.fixingSubgroup.map (restrictNormalHom (adjoin k {x}))
    let f (x : L) : IntermediateField k K := IntermediateField.lift <|
      IntermediateField.fixedField <| g x.1
    have (x : K) : (g x).Normal :=
      Subgroup.Normal.map h (restrictNormalHom (adjoin k {x})) (restrictNormalHom_surjective K)
    have (l : L) : Normal k (f l) :=
      Normal.of_algEquiv <| IntermediateField.liftAlgEquiv <| IntermediateField.fixedField (g l.1)
    have n : Normal k ↥(⨆ l : L, f l) := IntermediateField.normal_iSup k K f
    have : (⨆ l : L, f l) = L := by
      apply le_antisymm
      · apply iSup_le
        intro l
        simpa only [f, g, ← restrict_fixedField L.fixingSubgroup (adjoin k {l.1}),
          fixedField_fixingSubgroup L] using inf_le_left
      · intro l hl
        apply le_iSup f ⟨l, hl⟩
        simpa only [f, g, ← restrict_fixedField L.fixingSubgroup (adjoin k {l}),
          fixedField_fixingSubgroup L, IntermediateField.mem_inf, hl, true_and]
          using adjoin_simple_le_iff.mp le_rfl
    rw [this] at n
    constructor
  · simpa only [IntermediateFieldEquivClosedSubgroup, RelIso.coe_fn_mk, Equiv.coe_fn_mk,
      ← L.restrictNormalHom_ker] using MonoidHom.normal_ker (restrictNormalHom L)

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.IntegralClosure

Goal state before:
pp: case refine_1
A : Type u_1
K : Type u_2
inst✝¹⁴ : CommRing A
inst✝¹³ : Field K
inst✝¹² : Algebra A K
inst✝¹¹ : IsFractionRing A K
L : Type u_3
inst✝¹⁰ : Field L
C : Type u_4
inst✝⁹ : CommRing C
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A L
inst✝⁶ : IsScalarTower A K L
inst✝⁵ : Algebra C L
inst✝⁴ : IsIntegralClosure C A L
inst✝³ : Algebra A C
inst✝² : IsScalarTower A C L
inst✝¹ : IsDomain A
inst✝ : Algebra.IsAlgebraic K L
this✝¹ : IsDomain C
this✝ : IsTorsionFree A L
this : IsTorsionFree A C
x : A
hx : x ∈ ↑A⁰
⊢ (algebraMap C L) ↑⟨(algebraMap A C) x, ⋯⟩ ≠ 0

Tactic:
map_ne_zero_iff _ (IsIntegralClosure.algebraMap_injective C A L),

Goal state after:
case refine_1
A : Type u_1
K : Type u_2
inst✝¹⁴ : CommRing A
inst✝¹³ : Field K
inst✝¹² : Algebra A K
inst✝¹¹ : IsFractionRing A K
L : Type u_3
inst✝¹⁰ : Field L
C : Type u_4
inst✝⁹ : CommRing C
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A L
inst✝⁶ : IsScalarTower A K L
inst✝⁵ : Algebra C L
inst✝⁴ : IsIntegralClosure C A L
inst✝³ : Algebra A C
inst✝² : IsScalarTower A C L
inst✝¹ : IsDomain A
inst✝ : Algebra.IsAlgebraic K L
this✝¹ : IsDomain C
this✝ : IsTorsionFree A L
this : IsTorsionFree A C
x : A
hx : x ∈ ↑A⁰
⊢ ↑⟨(algebraMap A C) x, ⋯⟩ ≠ 0
Module: Mathlib.RingTheory.IsGaloisGroup.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✝¹⁹ : MulSemiringAction G 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 L
inst✝⁶ : SMulDistribClass G B L
inst✝⁵ : IsDomain A
inst✝⁴ : IsDomain B
inst✝³ : Finite G
inst✝² : IsGaloisGroup G A B
inst✝¹ : Algebra (FractionRing A) (FractionRing B)
inst✝ : IsScalarTower A (FractionRing A) (FractionRing B)
⊢ IsGaloisGroup G (FractionRing A) (FractionRing B)

Tactic:
by
  let := IsFractionRing.mulSemiringAction G B (FractionRing B)
  apply IsGaloisGroup.to_isFractionRing G A B _ _

Goal state after:
Module: Mathlib.Data.Nat.Prime.Int

Goal state before:
pp: p q n : ℕ
hp : Prime p
hq : Prime q
hn : n ≠ 0
m : ℕ
hm : m + 1 ≠ 0
h : p ^ (m + 1) = q ^ n
⊢ p = q ∧ m + 1 = n

Tactic:
obtain ⟨n, rfl⟩ := exists_eq_add_one_of_ne_zero hn

Goal state after:
p q : ℕ
hp : Prime p
hq : Prime q
m : ℕ
hm : m + 1 ≠ 0
n : ℕ
hn : n + 1 ≠ 0
h : p ^ (m + 1) = q ^ (n + 1)
⊢ p = q ∧ m + 1 = n + 1
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case neg
n : ℕ
inst✝ : NeZero n
a : ZMod n
this : ↑a.val - ↑n ≤ 0
h✝ : ¬a.val ≤ n / 2
⊢ ↑↑(↑a.val - ↑n).natAbs = -a

Tactic:
Int.ofNat_natAbs_of_nonpos this,

Goal state after:
case neg
n : ℕ
inst✝ : NeZero n
a : ZMod n
this : ↑a.val - ↑n ≤ 0
h✝ : ¬a.val ≤ n / 2
⊢ ↑(-(↑a.val - ↑n)) = -a
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: R : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : DecidableEq R
inst✝ : Fintype R
p : R[X]
hp : 0 < p.degree
a : R
x✝ : a ∈ image (fun x ↦ eval x p) univ
⊢ {a_1 | eval a_1 p = a} = (p - C a).roots.toFinset

Tactic:
by simp [Finset.ext_iff, ← mem_roots_sub_C hp]

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

Goal state before:
pp: R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype R
f g : R[X]
hf2 : f.degree = 2
hg2 : g.degree = 2
hR : Fintype.card R % 2 = 1
this : DecidableEq R := Classical.decEq R
hd : Disjoint (image (fun x ↦ eval x f) univ) (image (fun x ↦ eval x (-g)) univ)
⊢ f.natDegree * #(image (fun x ↦ eval x f) univ) + (-g).natDegree * #(image (fun x ↦ eval x (-g)) univ) =
    2 * #(image (fun x ↦ eval x f) univ ∪ image (fun x ↦ eval x (-g)) univ)

Tactic:
rw [card_union_of_disjoint hd]
        simp [natDegree_eq_of_degree_eq_some hf2, natDegree_eq_of_degree_eq_some hg2, mul_add]

Goal state after:
Module: Mathlib.FieldTheory.Galois.IsGaloisGroup

Goal state before:
pp: G : Type u_1
inst✝⁸ : Group G
A : Type u_5
B : Type u_6
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
inst✝³ : FaithfulSMul A B
inst✝² : MulSemiringAction G B
inst✝¹ : IsGaloisGroup G A B
inst✝ : Finite G
this✝¹ : IsDomain A
this✝ : Algebra (FractionRing A) (FractionRing B) := FractionRing.liftAlgebra A (FractionRing B)
this : MulSemiringAction G (FractionRing B) := IsFractionRing.mulSemiringAction G B (FractionRing B)
⊢ Nat.card G = finrank A B

Tactic:
rw [IsGaloisGroup.card_eq_finrank G (FractionRing A) (FractionRing B),
    IsFractionRing.finrank_eq A (FractionRing A) B (FractionRing B)]

Goal state after:
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
x : L
⊢ ((aeval (frobeniusAlgHom K L).toLinearMap) (X ^ Module.finrank K L - 1)) x = 0 x

Tactic:
by
      simpa [sub_eq_zero, Module.End.coe_pow, orderOf_frobeniusAlgHom] using!
        congr($(pow_orderOf_eq_one (frobeniusAlgHom K L)) x)

Goal state after:
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✝¹² : MulSemiringAction G B
inst✝¹¹ : SMulCommClass G A B
P : Ideal A
Q : Ideal B
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✝¹ : IsFractionRing (A ⧸ P) K
inst✝ : IsFractionRing (B ⧸ Q) L
⊢ ((fieldEquivOfAlgEquivHom K L).comp (Ideal.Quotient.stabilizerHom Q P G)).ker =
    Ideal.inertia (↥(MulAction.stabilizer G Q)) Q

Tactic:
MonoidHom.ker_comp_of_injective,

Goal state after:
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✝¹² : MulSemiringAction G B
inst✝¹¹ : SMulCommClass G A B
P : Ideal A
Q : Ideal B
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✝¹ : IsFractionRing (A ⧸ P) K
inst✝ : IsFractionRing (B ⧸ Q) L
⊢ (Ideal.Quotient.stabilizerHom Q P G).ker = Ideal.inertia (↥(MulAction.stabilizer G Q)) Q

case hg
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✝¹² : MulSemiringAction G B
inst✝¹¹ : SMulCommClass G A B
P : Ideal A
Q : Ideal B
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✝¹ : IsFractionRing (A ⧸ P) K
inst✝ : IsFractionRing (B ⧸ Q) L
⊢ Function.Injective ⇑(fieldEquivOfAlgEquivHom K L)
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case neg
p x y : ℕ
hp : Nat.Prime p
h : (p - 1) * ((x - y) / (p - 1)) = x - y
hxy : y ≤ x
hy : 0 < y
n : ℤ
hn : IsCoprime (↑p) n
⊢ n ^ x ≡ n ^ y [ZMOD ↑p]

Tactic:
grw [← pow_sub_mul_pow n hxy, ← h, pow_mul, Int.ModEq.pow_card_sub_one_eq_one hp hn.symm,
      one_pow, one_mul]

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

Goal state before:
pp: case inr.inr
n p k : ℕ
inst✝ : Fact (Nat.Prime p)
hn : n = p ^ k
hn0 : n ≠ 0
this : NeZero n
a : ℕ
ha : (orderOf ↑a).Coprime n
ha0 : ↑a ≠ 0
h : ¬IsUnit (↑a - 1)
⊢ ↑a ^ n = 1

Tactic:
← Nat.cast_pow,

Goal state after:
case inr.inr
n p k : ℕ
inst✝ : Fact (Nat.Prime p)
hn : n = p ^ k
hn0 : n ≠ 0
this : NeZero n
a : ℕ
ha : (orderOf ↑a).Coprime n
ha0 : ↑a ≠ 0
h : ¬IsUnit (↑a - 1)
⊢ ↑(a ^ n) = 1
Module: Mathlib.NumberTheory.RamificationInertia.Inertia

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
p : Ideal R
P : Ideal S
I : Ideal T
inst✝³ : p.IsMaximal
inst✝² : P.IsMaximal
inst✝¹ : P.LiesOver p
inst✝ : I.LiesOver P
h₁ : p = under R P
h₂ : P = under S I
h₃ : p = under R I
this : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfLEComap ⋯
⊢ finrank (R ⧸ p) (T ⧸ I) = finrank (R ⧸ p) (S ⧸ P) * finrank (S ⧸ P) (T ⧸ I)

Tactic:
let : Algebra (S ⧸ P) (T ⧸ I) := Ideal.Quotient.algebraQuotientOfLEComap h₂.le

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
p : Ideal R
P : Ideal S
I : Ideal T
inst✝³ : p.IsMaximal
inst✝² : P.IsMaximal
inst✝¹ : P.LiesOver p
inst✝ : I.LiesOver P
h₁ : p = under R P
h₂ : P = under S I
h₃ : p = under R I
this✝ : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfLEComap ⋯
this : Algebra (S ⧸ P) (T ⧸ I) := Quotient.algebraQuotientOfLEComap ⋯
⊢ finrank (R ⧸ p) (T ⧸ I) = finrank (R ⧸ p) (S ⧸ P) * finrank (S ⧸ P) (T ⧸ I)
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDedekindDomain S
P : Ideal S
P_prime : P.IsPrime
hP : P ≠ ⊥
i : ℕ
a b : S
a_notMem : ¬P ^ i * P ∣ span {a}
ab_mem : P ^ i * P ∣ span {a} * span {b}
⊢ P ∣ span {b}

Tactic:
exact (prime_pow_succ_dvd_mul (Ideal.prime_of_isPrime hP P_prime) ab_mem).resolve_left a_notMem

Goal state after:
Module: Mathlib.RingTheory.Finiteness.NilpotentKer

Goal state before:
pp: case succ
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✝ : Module.Finite R T
f : S →ₐ[R] T
hf₁ : Function.Surjective ⇑f
I : Ideal S
hI : RingHom.ker f = I
hf₂ : I ≤ nilradical S
hf₃ : I.FG
this : Module.Finite R (S ⧸ I)
n : ℕ
IH : Module.Finite R (S ⧸ I ^ n)
⊢ Module.Finite R (S ⧸ I ^ (n + 1))

Tactic:
let φ : (S ⧸ I ^ (n + 1)) →ₐ[S] S ⧸ I ^ n :=
      Ideal.Quotient.factorₐ _ (Ideal.pow_le_pow_right n.le_succ)
    have hφ : Function.Surjective φ :=
      Ideal.Quotient.factor_surjective (Ideal.pow_le_pow_right n.le_succ)
    have hφ' : φ.toLinearMap ∘ₗ (I ^ (n + 1)).mkQ = (I ^ n).mkQ := rfl
    refine ⟨Submodule.fg_of_fg_map_of_fg_inf_ker (φ.toLinearMap.restrictScalars R) ?_ ?_⟩
    · simpa [LinearMap.range_eq_top_of_surjective (φ.toLinearMap.restrictScalars R) hφ] using
        Module.Finite.fg_top
    · have : Module.Finite R ((S ⧸ I) ⊗[S] ↑(I ^ n)) := by
        have : Module.Finite S ↑(I ^ n) := .of_fg (.pow hf₃ _)
        exact .trans (S ⧸ I) _
      let ψ : (S ⧸ I) ⊗[S] ↑(I ^ n) →ₗ[S] (S ⧸ I ^ (n + 1)) := by
        refine ?_ ∘ₗ (TensorProduct.quotTensorEquivQuotSMul _ I).toLinearMap
        refine Submodule.liftQ _ ((Submodule.mkQ _).comp (I ^ n).subtype) ?_
        rw [LinearMap.ker_comp, ← Submodule.map_le_map_iff_of_injective (I ^ n).subtype_injective,
          Submodule.map_smul'', Submodule.map_comap_eq]
        simpa [pow_succ'] using Ideal.mul_le_right (I := I) (J := I ^ n)
      convert! Module.Finite.fg_top.map (ψ.restrictScalars R) using 1
      suffices LinearMap.ker φ.toLinearMap = Submodule.map (I ^ (n + 1)).mkQ (I ^ n) by
        simpa [LinearMap.range_restrictScalars, ψ, LinearMap.range_comp, Submodule.range_liftQ]
      apply Submodule.comap_injective_of_surjective (I ^ (n + 1)).mkQ_surjective
      simpa [← LinearMap.ker_comp, hφ'] using Ideal.pow_le_pow_right n.le_succ

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
inst✝ : Module.Finite ℤ S
I : Ideal S
hI : I ≠ ⊥
J : Ideal S
this : (toAddSubgroup I).FiniteIndex
⊢ (toAddSubgroup I).IsFiniteRelIndex (toAddSubgroup J)

Tactic:
exact isFiniteRelIndex_of_finiteIndex

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

Goal state before:
pp: case intro
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDedekindDomain S
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
P : Ideal S
inst✝ : P.IsMaximal
this✝² : IsAddTorsionFree S
this✝¹ : CharZero S
this✝ : Finite (S ⧸ P)
val✝ : Fintype (S ⧸ P)
this : Field (S ⧸ P) := Quotient.field P
p : ℕ
hpR : CharP (S ⧸ P) p
n : ℕ+
hp : Nat.Prime p
e : Fintype.card (S ⧸ P) = p ^ ↑n
hP : absNorm P = p ^ ↑n
⊢ ↑p ^ ↑n ∈ P

Tactic:
← Nat.cast_pow,

Goal state after:
case intro
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDedekindDomain S
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
P : Ideal S
inst✝ : P.IsMaximal
this✝² : IsAddTorsionFree S
this✝¹ : CharZero S
this✝ : Finite (S ⧸ P)
val✝ : Fintype (S ⧸ P)
this : Field (S ⧸ P) := Quotient.field P
p : ℕ
hpR : CharP (S ⧸ P) p
n : ℕ+
hp : Nat.Prime p
e : Fintype.card (S ⧸ P) = p ^ ↑n
hP : absNorm P = p ^ ↑n
⊢ ↑(p ^ ↑n) ∈ P
Module: Mathlib.GroupTheory.Submonoid.Inverses

Goal state before:
pp: M : Type u_1
inst✝ : Group M
S : Submonoid M
x : ↥S.leftInv
⊢ ↑(S.fromLeftInv x) = (↑x)⁻¹

Tactic:
rw [← mul_right_inj (x : M), mul_inv_cancel, mul_fromLeftInv]

Goal state after:
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: case mpr
X : Type u_1
inst✝ : TopologicalSpace X
H : ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ closedPoints X).Nonempty
Z : Set X
hZ : IsClosed[inst✝] Z
H' : ((closure[inst✝] (Z ∩ closedPoints X))ᶜ ∩ Z).Nonempty
⊢ False

Tactic:
have := H _ H' (isClosed_closure.isOpen_compl.isLocallyClosed.inter hZ.isLocallyClosed)

Goal state after:
case mpr
X : Type u_1
inst✝ : TopologicalSpace X
H : ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ closedPoints X).Nonempty
Z : Set X
hZ : IsClosed[inst✝] Z
H' : ((closure[inst✝] (Z ∩ closedPoints X))ᶜ ∩ Z).Nonempty
this : ((closure[inst✝] (Z ∩ closedPoints X))ᶜ ∩ Z ∩ closedPoints X).Nonempty
⊢ False
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: case mp
R : Type v
inst✝⁵ : CommRing R
A : Type u
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Small.{w, u} A
a✝ : FormallyUnramified R A
B✝ : Type w
inst✝¹ : CommRing B✝
inst✝ : Algebra R B✝
I✝ : Ideal B✝
x✝ : I✝ ^ 2 = ⊥
⊢ Function.Injective (Ideal.Quotient.mkₐ R I✝).comp

Tactic:
exact comp_injective _ ‹_›

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

Goal state before:
pp: R : Type v
inst✝⁵ : CommRing R
A : Type u
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type w
inst✝² : CommRing B
inst✝¹ : Algebra R B
I : Ideal B
inst✝ : FormallyUnramified R A
hI : ⨅ i, I ^ i = ⊥
g₁ g₂ : A →ₐ[R] B
H : ∀ (x : A), (Ideal.Quotient.mk I) (g₁ x) = (Ideal.Quotient.mk I) (g₂ x)
this : ∀ (i : ℕ), (Ideal.Quotient.mkₐ R (I ^ i)).comp g₁ = (Ideal.Quotient.mkₐ R (I ^ i)).comp g₂
x : A
i : ℕ
⊢ (Ideal.Quotient.mk (I ^ i)) (g₁ x) = (Ideal.Quotient.mk (I ^ i)) (g₂ x)

Tactic:
exact DFunLike.congr_fun (this i) x

Goal state after: