mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
β : Type v
f✝ : α → β
M✝ : Matroid α
I✝ J✝ B B' X✝ Y : Set α
M : Matroid β
inst✝ : M.InvariantCardinalRank
f : α → β
I J X : Set α
hI✝ : (M.comap f).IsBasis I X
hJ✝ : (M.comap f).IsBasis J X
hI : M.IsBasis (f '' I) (f '' X)
hfI : InjOn f I
hIX : I ⊆ X
hJ : M.IsBasis (f '' J) (f '' X)
hfJ : InjOn f J
hJX : J ⊆ X
⊢ #↑(f '' I \ f '' J) + #↑((f '' J ∩ f '' I) \ f '' (I ∩ J)) = #↑(f '' J \ f '' (J ∩ I))

pp: α : Type u
β : Type v
f✝ : α → β
M✝ : Matroid α
I✝ J✝ B B' X✝ Y : Set α
M : Matroid β
inst✝ : M.InvariantCardinalRank
f : α → β
I J X : Set α
hI✝ : (M.comap f).IsBasis I X
hJ✝ : (M.comap f).IsBasis J X
hI : M.IsBasis (f '' I) (f '' X)
hfI : InjOn f I
hIX : I ⊆ X
hJ : M.IsBasis (f '' J) (f '' X)
hfJ : InjOn f J
hJX : J ⊆ X
⊢ Disjoint (f '' I \ f '' J) ((f '' J ∩ f '' I) \ f '' (I ∩ J))

Tactic:
hI.cardinalMk_sdiff_comm hJ,

Goal state after:
α : Type u
β : Type v
f✝ : α → β
M✝ : Matroid α
I✝ J✝ B B' X✝ Y : Set α
M : Matroid β
inst✝ : M.InvariantCardinalRank
f : α → β
I J X : Set α
hI✝ : (M.comap f).IsBasis I X
hJ✝ : (M.comap f).IsBasis J X
hI : M.IsBasis (f '' I) (f '' X)
hfI : InjOn f I
hIX : I ⊆ X
hJ : M.IsBasis (f '' J) (f '' X)
hfJ : InjOn f J
hJX : J ⊆ X
⊢ #↑(f '' J \ f '' I) + #↑((f '' J ∩ f '' I) \ f '' (I ∩ J)) = #↑(f '' J \ f '' (J ∩ I))

α : Type u
β : Type v
f✝ : α → β
M✝ : Matroid α
I✝ J✝ B B' X✝ Y : Set α
M : Matroid β
inst✝ : M.InvariantCardinalRank
f : α → β
I J X : Set α
hI✝ : (M.comap f).IsBasis I X
hJ✝ : (M.comap f).IsBasis J X
hI : M.IsBasis (f '' I) (f '' X)
hfI : InjOn f I
hIX : I ⊆ X
hJ : M.IsBasis (f '' J) (f '' X)
hfJ : InjOn f J
hJX : J ⊆ X
⊢ Disjoint (f '' I \ f '' J) ((f '' J ∩ f '' I) \ f '' (I ∩ J))
Module: Mathlib.RingTheory.AlgebraicIndependent.Basic

Goal state before:
pp: ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
⊢ Injective ⇑(algebraMap R A)

Tactic:
by
  simpa [Function.comp_def] using
    (Injective.of_comp_iff (algebraicIndependent_iff_injective_aeval.1 hx) MvPolynomial.C).2
      (MvPolynomial.C_injective _ _)

Goal state after:
Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental

Goal state before:
pp: ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set ι
⊢ AlgebraicIndependent R x ↔ (AlgebraicIndependent R fun i ↦ x ↑i) ∧ AlgebraicIndepOn (↥(adjoin R (x '' s))) x sᶜ

Tactic:
show x '' s = range fun i : s ↦ x i by ext; simp

Goal state after:
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set ι
⊢ AlgebraicIndependent R x ↔
    (AlgebraicIndependent R fun i ↦ x ↑i) ∧ AlgebraicIndepOn (↥(adjoin R (range fun i ↦ x ↑i))) x sᶜ
Module: Mathlib.RingTheory.AlgebraicIndependent.Basic

Goal state before:
pp: R : Type u_2
A : Type v
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
ι : Type u_3
ι' : Type u_4
s : Set ι
f : ι → ι'
g : ι' → A
hs : AlgebraicIndependent R fun x ↦ g (f ↑x)
⊢ AlgebraicIndependent R fun x ↦ g ↑x

Tactic:
by
  nontriviality R
  have : InjOn f s := injOn_iff_injective.2 hs.injective.of_comp
  exact (algebraicIndependent_equiv' (Equiv.Set.imageOfInjOn f s this) rfl).1 hs

Goal state after:
Module: Mathlib.FieldTheory.AlgebraicClosure

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
K : Type u_3
inst✝¹ : Field K
inst✝ : Algebra F K
i : E →ₐ[F] K
⊢ comap i (algebraicClosure F K) = algebraicClosure F E

Tactic:
by
  ext x
  exact map_mem_algebraicClosure_iff i

Goal state after:
Module: Mathlib.FieldTheory.AlgebraicClosure

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra E K
inst✝ : IsScalarTower F E K
h : algebraicClosure E K = ⊥
x : K
hx : x ∈ algebraicClosure F K
⊢ x ∈ IntermediateField.map (IsScalarTower.toAlgHom F E K) (algebraicClosure F E)

Tactic:
obtain ⟨y, rfl⟩ := mem_bot.1 <| h ▸ mem_algebraicClosure_iff'.2
    (IsIntegral.tower_top <| mem_algebraicClosure_iff'.1 hx)

Goal state after:
F : Type u_1
E : Type u_2
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra E K
inst✝ : IsScalarTower F E K
h : algebraicClosure E K = ⊥
y : E
hx : (algebraMap E K) y ∈ algebraicClosure F K
⊢ (algebraMap E K) y ∈ IntermediateField.map (IsScalarTower.toAlgHom F E K) (algebraicClosure F E)
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
x : ι → A
y : ι' → A
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : FaithfulSMul R A
inst✝ : NoZeroDivisors A
I B : Set A
I_ind : AlgebraicIndepOn R _root_.id I
h : ¬Maximal (AlgebraicIndepOn R _root_.id) I
B_base : Maximal (AlgebraicIndepOn R _root_.id) B
⊢ ∃ x ∈ B \ I, AlgebraicIndepOn R _root_.id (insert x I)

Tactic:
contrapose! h
    rw [← isTranscendenceBasis_iff_maximal] at B_base ⊢
    cases subsingleton_or_nontrivial R
    · rw [isTranscendenceBasis_iff_of_subsingleton] at B_base ⊢
      by_contra this
      have ⟨b, hb⟩ := B_base
      exact h b ⟨hb, fun hbI ↦ this ⟨b, hbI⟩⟩ .of_subsingleton
    apply I_ind.isTranscendenceBasis_iff_isAlgebraic.mpr
    replace B_base := B_base.isAlgebraic
    simp_rw +instances [id_eq]
    rw [Subtype.range_val] at B_base ⊢
    refine ⟨fun a ↦ (B_base.1 a).adjoin_of_forall_isAlgebraic fun x hx ↦ ?_⟩
    contrapose! h
    exact ⟨x, hx, I_ind.insert <| by rwa [image_id]⟩

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case neg
F : Type u
inst✝ : Field F
f g : F[X]
h : ¬f * g = 0
⊢ (∀ (a : AlgebraicClosure F), f ≠ 0 ∧ (aeval a) f = 0 → ∀ (b : AlgebraicClosure F), g ≠ 0 ∧ (aeval b) g = 0 → a ≠ b) ↔
    f = 0 ∧ g = 0 ∨ IsCoprime f g

Tactic:
rw [mul_eq_zero, not_or] at h

Goal state after:
case neg
F : Type u
inst✝ : Field F
f g : F[X]
h : ¬f = 0 ∧ ¬g = 0
⊢ (∀ (a : AlgebraicClosure F), f ≠ 0 ∧ (aeval a) f = 0 → ∀ (b : AlgebraicClosure F), g ≠ 0 ∧ (aeval b) g = 0 → a ≠ b) ↔
    f = 0 ∧ g = 0 ∨ IsCoprime f g
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: G : Type u
inst✝ : Group G
B : GroupFilterBasis G
x₀ : G
⊢ (𝓝 x₀).HasBasis (fun V ↦ V ∈ B) fun V ↦ (fun y ↦ x₀ * y) '' V

Tactic:
by
  rw [B.nhds_eq]
  apply B.hasBasis

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✝ : FiniteDimensional K L
⊢ DiscreteTopology Gal(L/K)

Tactic:
by
  rw [discreteTopology_iff_isOpen_singleton_one]
  change IsOpen ((⊥ : Subgroup Gal(L/K)) : Set Gal(L/K))
  rw [← IntermediateField.fixingSubgroup_top]
  exact IntermediateField.fixingSubgroup_isOpen ⊤

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
f : R[X]
hf : f.Monic
g : K[X]
hg : g.Monic
hd : g ∣ map (algebraMap R K) f
⊢ g ∈ lifts (algebraMap (↥(integralClosure R K)) K)

Tactic:
have := (SplittingField.splits g).mem_lift_of_roots_mem_range (hg.map _)
    (algebraMap (integralClosure R g.SplittingField) g.SplittingField)
     fun a ha =>
      (SetLike.ext_iff.mp (integralClosure R g.SplittingField).range_algebraMap _).mpr <|
        roots_mem_integralClosure hf ?_
  · rw [lifts_iff_coeff_lifts, ← RingHom.coe_range, Subalgebra.range_algebraMap] at this
    refine (lifts_iff_coeff_lifts _).2 fun n => ?_
    rw [← RingHom.coe_range, Subalgebra.range_algebraMap]
    obtain ⟨p, hp, he⟩ := SetLike.mem_coe.mp (this n); use p, hp
    rw [IsScalarTower.algebraMap_eq R K, coeff_map, ← eval₂_map, eval₂_at_apply] at he
    rw [eval₂_eq_eval_map]; apply (injective_iff_map_eq_zero _).1 _ _ he
    apply RingHom.injective
  rw [aroots_def, IsScalarTower.algebraMap_eq R K _, ← map_map]
  refine Multiset.mem_of_le (roots.le_of_dvd ((hf.map _).map _).ne_zero ?_) ha
  exact map_dvd (algebraMap K g.SplittingField) hd

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

Goal state before:
pp: case h.right
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
σ : Gal(K/k)
h : σ ∈ (↑L.fixingSubgroup)ᶜ
y : K
yL : y ∈ ↑L
ne : y ∉ fun a ↦ σ • a = a
⊢ IsOpen (σ • ↑(adjoin k {y}).fixingSubgroup) ∧ σ ∈ σ • ↑(adjoin k {y}).fixingSubgroup

Tactic:
simp only [(IntermediateField.fixingSubgroup_isOpen (adjoin k {y}).1).smul σ, true_and]
      use 1
      simp only [SetLike.mem_coe, smul_eq_mul, mul_one, and_true, Subgroup.one_mem]

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearForm.DualLattice

Goal state before:
pp: case a
R : Type u_4
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
ι : Type u_1
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
hB : B.Nondegenerate
b : Basis ι S M
val✝ : Fintype ι
⊢ Submodule.span R (Set.range ⇑(B.dualBasis hB b)) ≤ B.dualSubmodule (Submodule.span R (Set.range ⇑b))

Tactic:
rw [Submodule.span_le]
    rintro _ ⟨i, rfl⟩ y hy
    obtain ⟨f, rfl⟩ := (Submodule.mem_span_range_iff_exists_fun _).mp hy
    simp only [map_sum]
    apply sum_mem
    rintro j -
    rw [← IsScalarTower.algebraMap_smul S (f j), map_smul]
    simp_rw [apply_dualBasis_left]
    rw [smul_eq_mul, mul_ite, mul_one, mul_zero, ← (algebraMap R S).map_zero, ← apply_ite]
    exact Submodule.mem_one.mpr ⟨_, rfl⟩

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
x : K
hx : ∀ f ∈ L.fixingSubgroup, f x = x
mem : x ∈ (adjoin ↥L {x}).toIntermediateField
this : IntermediateField.fixedField ⊤ = ⊥
⊢ ⟨x, mem⟩ ∈ ⊥

Tactic:
rw [← this, IntermediateField.mem_fixedField_iff]

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
x : K
hx : ∀ f ∈ L.fixingSubgroup, f x = x
mem : x ∈ (adjoin ↥L {x}).toIntermediateField
this : IntermediateField.fixedField ⊤ = ⊥
⊢ ∀ f ∈ ⊤, f ⟨x, mem⟩ = ⟨x, mem⟩
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
hinj : Function.Injective ⇑φ
f : R[X]
hf : f.IsPrimitive
h_irr : Irreducible (map φ f)
⊢ Irreducible f

Tactic:
refine
    ⟨fun h => h_irr.not_isUnit (IsUnit.map (mapRingHom φ) h), fun a b h =>
      (h_irr.isUnit_or_isUnit <| by rw [h, Polynomial.map_mul]).imp ?_ ?_⟩
  all_goals apply ((isPrimitive_of_dvd hf _).isUnit_iff_isUnit_map_of_injective hinj).mpr
  exacts [Dvd.intro _ h.symm, Dvd.intro_left _ h.symm]

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

Goal state before:
pp: F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Ring E
inst✝² : IsDomain E
inst✝¹ : Algebra F E
q : ℕ
inst✝ : ExpChar F q
⊢ (∀ (x : E), IsIntegral F x ∧ (IsSeparable F x → x ∈ (algebraMap F E).range)) ↔
    ∀ (x : E), ∃ n, x ^ q ^ n ∈ (algebraMap F E).range

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

Goal state after:
case refine_1
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Ring E
inst✝² : IsDomain E
inst✝¹ : Algebra F E
q : ℕ
inst✝ : ExpChar F q
h : ∀ (x : E), IsIntegral F x ∧ (IsSeparable F x → x ∈ (algebraMap F E).range)
x : E
⊢ ∃ n, x ^ q ^ n ∈ (algebraMap F E).range

case refine_2
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Ring E
inst✝² : IsDomain E
inst✝¹ : Algebra F E
q : ℕ
inst✝ : ExpChar F q
h : ∀ (x : E), ∃ n, x ^ q ^ n ∈ (algebraMap F E).range
x : E
⊢ IsIntegral F x ∧ (IsSeparable F x → x ∈ (algebraMap F E).range)
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
K : Type w
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra E K
inst✝ : IsScalarTower F E K
q : ℕ
h✝¹ : ∀ (x : K), ∃ n, x ^ q ^ n ∈ (algebraMap F K).range
h✝ : ExpChar F q
this : ExpChar E q
x : K
n : ℕ
y : F
h : (algebraMap F K) y = x ^ q ^ n
⊢ ∃ n, x ^ q ^ n ∈ (algebraMap E K).range

Tactic:
exact ⟨n, (algebraMap F E) y, h.symm ▸ (IsScalarTower.algebraMap_apply F E K y).symm⟩

Goal state after:
Module: Mathlib.RingTheory.Trace.Defs

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✝³ : Free R S
inst✝² : Free R T
inst✝¹ : Module.Finite R S
inst✝ : Module.Finite R T
x : S × T
f : S × T →ₗ[R] End R S × End R T := (lmul R S).toLinearMap.prodMap (lmul R T).toLinearMap
⊢ (trace R (S × T)) x = (trace R S) x.1 + (trace R T) x.2

Tactic:
have : (lmul R (S × T)).toLinearMap = (prodMapLinear R S T S T R).comp f :=
    LinearMap.ext₂ Prod.mul_def

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✝³ : Free R S
inst✝² : Free R T
inst✝¹ : Module.Finite R S
inst✝ : Module.Finite R T
x : S × T
f : S × T →ₗ[R] End R S × End R T := (lmul R S).toLinearMap.prodMap (lmul R T).toLinearMap
this : (lmul R (S × T)).toLinearMap = prodMapLinear R S T S T R ∘ₗ f
⊢ (trace R (S × T)) x = (trace R S) x.1 + (trace R T) x.2
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: case inl
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
p : R[X]
hp : p.IsPrimitive
hi : Irreducible p
a b : K[X]
hab : map (algebraMap R K) p = a * b
c : R
c0 : c ≠ 0
hc : map (algebraMap R K) (integerNormalization R⁰ a) = C ((algebraMap R K) c) * a
d : R
d0 : d ≠ 0
hd : map (algebraMap R K) (integerNormalization R⁰ b) = C ((algebraMap R K) d) * b
hcd0 : ¬C (c * d) = 0
this : NormalizedGCDMonoid R
u : Rˣ
h1 : C (c * d) * (C ↑u * (integerNormalization R⁰ b).primPart * (integerNormalization R⁰ a).primPart) = C (c * d) * p
hu : c * d * ↑u = (integerNormalization R⁰ a).content * (integerNormalization R⁰ b).content
h0 : a ≠ 0 ∧ b ≠ 0
h : IsUnit (C ↑u * (integerNormalization R⁰ b).primPart)
⊢ IsUnit a ∨ IsUnit b

Tactic:
right
    apply
      isUnit_or_eq_zero_of_isUnit_integerNormalization_primPart h0.2
        (isUnit_of_mul_isUnit_right h)

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

Goal state before:
pp: A : Type u_1
B : Type u_2
G : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A B
inst✝⁴ : Group G
inst✝³ : MulSemiringAction G B
inst✝² : IsInvariant A B G
inst✝¹ : Finite G
inst✝ : SMulCommClass G A B
P✝ Q : Ideal B
hP : P✝.IsPrime
hQ : Q.IsPrime
hPQ : Ideal.under A P✝ = Ideal.under A Q
val✝ : Fintype G
P : Ideal B
⊢ ∀ (Q : Ideal B) [P.IsPrime] [Q.IsPrime], Ideal.under A P = Ideal.under A Q → ∃ g ∈ ⊤, Q ≤ g • P

Tactic:
Q

Goal state after:
A : Type u_1
B : Type u_2
G : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A B
inst✝⁴ : Group G
inst✝³ : MulSemiringAction G B
inst✝² : IsInvariant A B G
inst✝¹ : Finite G
inst✝ : SMulCommClass G A B
P✝ Q✝ : Ideal B
hP : P✝.IsPrime
hQ : Q✝.IsPrime
hPQ : Ideal.under A P✝ = Ideal.under A Q✝
val✝ : Fintype G
P Q : Ideal B
⊢ ∀ [P.IsPrime] [Q.IsPrime], Ideal.under A P = Ideal.under A Q → ∃ g ∈ ⊤, Q ≤ g • P
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
E : Type u_7
inst✝¹ : Field E
inst✝ : Algebra K E
pb : PowerBasis K L
hE : (Polynomial.map (algebraMap K E) (minpoly K pb.gen)).Splits
hfx : IsSeparable K pb.gen
this✝ : DecidableEq E := Classical.decEq E
this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
⊢ (algebraMap K E) ((Algebra.trace K L) pb.gen) = ∑ σ, σ pb.gen

Tactic:
pb.trace_gen_eq_sum_roots hE,

Goal state after:
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
E : Type u_7
inst✝¹ : Field E
inst✝ : Algebra K E
pb : PowerBasis K L
hE : (Polynomial.map (algebraMap K E) (minpoly K pb.gen)).Splits
hfx : IsSeparable K pb.gen
this✝ : DecidableEq E := Classical.decEq E
this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
⊢ ((minpoly K pb.gen).aroots E).sum = ∑ σ, σ pb.gen
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)
⊢ 0 < (-g).degree

Tactic:
rw [degree_neg, hg2]; decide

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
this : ¬∀ ⦃a : R⦄, (∃ a_1 ∈ univ, eval a_1 f = a) → ¬∃ a_2 ∈ univ, eval a_2 (-g) = a
⊢ ∃ a b, eval a f + eval b g = 0

Tactic:
push Not at this

Goal state after:
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
this : ∃ a, (∃ a_1 ∈ univ, eval a_1 f = a) ∧ ∃ a_1 ∈ univ, eval a_1 (-g) = a
⊢ ∃ a b, eval a f + eval b g = 0
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: K : Type u_1
inst✝² : CommRing K
inst✝¹ : NoZeroDivisors K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card ↥G
a✝ : Nontrivial K
this : IsDomain K
a : ↥G
ha : a ^ k ≠ 1
h_multiset_map : Multiset.map (fun x ↦ ↑↑x ^ k) univ.val = Multiset.map (fun x ↦ ↑↑x ^ k * ↑↑a ^ k) univ.val
⊢ (Multiset.map (fun x ↦ ↑↑x ^ k) univ.val).sum = 0

Tactic:
have h_multiset_map_sum : (Multiset.map (fun x : G => ((x : Kˣ) : K) ^ k) Finset.univ.val).sum =
    (Multiset.map (fun x : G => ((x : Kˣ) : K) ^ k * ((a : Kˣ) : K) ^ k) Finset.univ.val).sum := by
    rw [h_multiset_map]

Goal state after:
K : Type u_1
inst✝² : CommRing K
inst✝¹ : NoZeroDivisors K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card ↥G
a✝ : Nontrivial K
this : IsDomain K
a : ↥G
ha : a ^ k ≠ 1
h_multiset_map : Multiset.map (fun x ↦ ↑↑x ^ k) univ.val = Multiset.map (fun x ↦ ↑↑x ^ k * ↑↑a ^ k) univ.val
h_multiset_map_sum :
  (Multiset.map (fun x ↦ ↑↑x ^ k) univ.val).sum = (Multiset.map (fun x ↦ ↑↑x ^ k * ↑↑a ^ k) univ.val).sum
⊢ (Multiset.map (fun x ↦ ↑↑x ^ k) univ.val).sum = 0
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
φ : Kˣ →* K := { toFun := fun x ↦ ↑x ^ i, map_one' := ⋯, map_mul' := ⋯ }
this : Decidable (φ = 1)
⊢ (∀ (x : Kˣ), x ^ i = 1) ↔ φ = 1

Tactic:
DFunLike.ext_iff

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
φ : Kˣ →* K := { toFun := fun x ↦ ↑x ^ i, map_one' := ⋯, map_mul' := ⋯ }
this : Decidable (φ = 1)
⊢ (∀ (x : Kˣ), x ^ i = 1) ↔ ∀ (x : Kˣ), φ x = 1 x
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: p : ℕ
hp : Nat.Prime p
n : ℤ
hpn : IsCoprime n ↑p
this : Fact (Nat.Prime p)
⊢ ¬↑n = 0

Tactic:
rw [CharP.intCast_eq_zero_iff _ p, ← (Nat.prime_iff_prime_int.mp hp).coprime_iff_not_dvd]

Goal state after:
p : ℕ
hp : Nat.Prime p
n : ℤ
hpn : IsCoprime n ↑p
this : Fact (Nat.Prime p)
⊢ IsCoprime (↑p) n
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✝¹ : IsFractionRing (A ⧸ P) K
inst✝ : IsFractionRing (B ⧸ Q) L
f : Gal(L/K)
val✝ : Fintype G
this✝ : P.IsPrime
this : Algebra.IsIntegral A B
x y b : B ⧸ Q
a : A ⧸ P
ha : (algebraMap (A ⧸ P) L) a ≠ 0
hy : (algebraMap (B ⧸ Q) L) y ≠ 0
h : (algebraMap (B ⧸ Q) L) x / (algebraMap (B ⧸ Q) L) y = (algebraMap (B ⧸ Q) L) b / (algebraMap (A ⧸ P) L) a
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    ((IsFractionRing.stabilizerHom G P Q K L) g) ((algebraMap (B ⧸ Q) L) b) /
        (algebraMap K L) ((algebraMap (A ⧸ P) K) a) =
      (algebraMap (B ⧸ Q) L) b / (algebraMap K L) ((algebraMap (A ⧸ P) K) a)
⊢ f ((algebraMap (B ⧸ Q) L) b) / (algebraMap K L) ((algebraMap (A ⧸ P) K) a) =
    (algebraMap (B ⧸ Q) L) b / (algebraMap K L) ((algebraMap (A ⧸ P) K) a)

Tactic:
simp only [← algebraMap_apply, div_left_inj' ha] at hx ⊢

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✝¹⁵ : 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✝¹ : IsFractionRing (A ⧸ P) K
inst✝ : IsFractionRing (B ⧸ Q) L
f : Gal(L/K)
val✝ : Fintype G
this✝ : P.IsPrime
this : Algebra.IsIntegral A B
x y b : B ⧸ Q
a : A ⧸ P
ha : (algebraMap (A ⧸ P) L) a ≠ 0
hy : (algebraMap (B ⧸ Q) L) y ≠ 0
h : (algebraMap (B ⧸ Q) L) x / (algebraMap (B ⧸ Q) L) y = (algebraMap (B ⧸ Q) L) b / (algebraMap (A ⧸ P) L) a
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    ((IsFractionRing.stabilizerHom G P Q K L) g) ((algebraMap (B ⧸ Q) L) b) = (algebraMap (B ⧸ Q) L) b
⊢ f ((algebraMap (B ⧸ Q) L) b) = (algebraMap (B ⧸ Q) L) b
Module: Mathlib.LinearAlgebra.Quotient.Pi

Goal state before:
pp: ι : 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
x : (i : ι) → Ms i
⊢ ((piQuotientLift p q f hf) fun i ↦ Quotient.mk (x i)) = Quotient.mk (((lsum R Ms R) f) x)

Tactic:
by
  rw [piQuotientLift, lsum_apply, sum_apply, ← mkQ_apply, lsum_apply, sum_apply, _root_.map_sum]
  simp only [coe_proj, mapQ_apply, mkQ_apply, comp_apply]

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

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Free ℤ R
inst✝¹ : Module.Finite ℤ R
p : ℤ
P : Ideal R
inst✝ : P.LiesOver (span {p})
hp : Prime p
⊢ absNorm P = p.natAbs ^ (span {p}).inertiaDeg' P

Tactic:
by
  simpa using absNorm_eq_pow_inertiaDeg'_of_liesOver P (span {p})
    (by rwa [span_singleton_prime hp.ne_zero]) (by simpa using hp.ne_zero)

Goal state after: