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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
⊢ M.IsColoop e ↔ e ∉ M.closure (M.E \ {e})

Tactic:
rw [isColoop_iff_sdiff_closure, not_iff_not]

Goal state after:
α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
⊢ M.closure (M.E \ {e}) = M.E ↔ e ∈ M.closure (M.E \ {e})
Module: Mathlib.RingTheory.Algebraic.MvPolynomial

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommRing R
i : σ
s : Set σ
h : i ∉ s
f : R[X]
g : MvPolynomial (↑s) R[X] →ₐ[R] MvPolynomial (↑s) R[X] := ⋯
hf : Function.Injective ⇑g
u : (MvPolynomial (↑s) R)[X] →ₐ[R] MvPolynomial σ R := ⋯
v : (MvPolynomial (↑s) R)[X] →ₐ[R] MvPolynomial σ R := ⋯
⊢ Function.Injective
    (⇑(supportedEquivMvPolynomial (insert i s)).symm ∘
      ⇑(renameEquiv R (Set.subtypeInsertEquivOption h).symm) ∘
        ⇑(optionEquivRight R ↑s).symm ∘ ⇑g ∘ ⇑(optionEquivRight R ↑s) ∘ ⇑(optionEquivLeft R ↑s).symm)

Tactic:
simp only [EquivLike.comp_injective]

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommRing R
i : σ
s : Set σ
h : i ∉ s
f : R[X]
g : MvPolynomial (↑s) R[X] →ₐ[R] MvPolynomial (↑s) R[X] := mapAlgHom (Polynomial.aeval f)
hf : Function.Injective ⇑g
u : (MvPolynomial (↑s) R)[X] →ₐ[R] MvPolynomial σ R :=
  (((supported R (insert i s)).val.comp
            ↑(((optionEquivRight R ↑s).symm.trans (renameEquiv R (Set.subtypeInsertEquivOption h).symm)).trans
                (supportedEquivMvPolynomial (insert i s)).symm)).comp
        g).comp
    ↑((optionEquivLeft R ↑s).symm.trans (optionEquivRight R ↑s))
v : (MvPolynomial (↑s) R)[X] →ₐ[R] MvPolynomial σ R :=
  (AlgHom.restrictScalars R (Polynomial.aeval ((Polynomial.aeval (X i)) f))).comp
    ↑(Polynomial.mapAlgEquiv (supportedEquivMvPolynomial s).symm)
⊢ Function.Injective (⇑g ∘ ⇑(optionEquivRight R ↑s) ∘ ⇑(optionEquivLeft R ↑s).symm)
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
hf : InjOn f M.E
⊢ (M.map f hf).InvariantCardinalRank

Tactic:
refine ⟨fun I J X hI hJ ↦ ?_⟩
  obtain ⟨I, X, hIX, rfl, rfl⟩ := map_isBasis_iff'.1 hI
  obtain ⟨J, X', hJX, rfl, h'⟩ := map_isBasis_iff'.1 hJ
  obtain rfl : X = X' := by
    rwa [InjOn.image_eq_image_iff hf hIX.subset_ground hJX.subset_ground] at h'
  have hcard := hIX.cardinalMk_sdiff_comm hJX
  rwa [← lift_inj.{u, v},
    ← mk_image_eq_of_injOn_lift _ _ (hf.mono ((hIX.indep.sdiff _).subset_ground)),
    ← mk_image_eq_of_injOn_lift _ _ (hf.mono ((hJX.indep.sdiff _).subset_ground)),
    lift_inj, (hf.mono hIX.indep.subset_ground).image_sdiff,
    (hf.mono hJX.indep.subset_ground).image_sdiff, inter_comm,
    hf.image_inter hJX.indep.subset_ground hIX.indep.subset_ground,
    sdiff_inter_self_eq_sdiff, sdiff_self_inter] at hcard

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
I : Set α
ι : Type u_4
hI : M.Indep I
X : ι → Set α
A : Set ι
hA : A.Nonempty
h : ∀ i ∈ A, M.IsBasis (X i ∩ I) (X i)
⊢ ⋂ i ∈ A, X i ⊆ M.closure ((⋂ i ∈ A, X i) ∩ I)

Tactic:
← biInter_inter hA,

Goal state after:
α : Type u_2
M : Matroid α
I : Set α
ι : Type u_4
hI : M.Indep I
X : ι → Set α
A : Set ι
hA : A.Nonempty
h : ∀ i ∈ A, M.IsBasis (X i ∩ I) (X i)
⊢ ⋂ i ∈ A, X i ⊆ M.closure (⋂ i ∈ A, X i ∩ I)
Module: Mathlib.RingTheory.AlgebraicIndependent.Basic

Goal state before:
pp: ι : Type u
R : Type u_2
A : Type v
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Subsingleton R
x : ι → A
this : Subsingleton A
h : IsTranscendenceBasis R x
⊢ Nonempty ι

Tactic:
by_contra! hι

Goal state after:
ι : Type u
R : Type u_2
A : Type v
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Subsingleton R
x : ι → A
this : Subsingleton A
h : IsTranscendenceBasis R x
hι : IsEmpty ι
⊢ False
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
hx : AlgebraicIndependent R x
inst✝ : Nontrivial A
s : Set ι
i : ι
⊢ Transcendental (↥(adjoin R (x '' s))) (x i) ↔ Disjoint s {i}

Tactic:
convert! ← hx.adjoin_iff_disjoint (t := { i })

Goal state after:
case e'_1
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
hx : AlgebraicIndependent R x
inst✝ : Nontrivial A
s : Set ι
i : ι
⊢ (AlgebraicIndependent ↥(adjoin R (x '' s)) fun i_1 ↦ x ↑i_1) ↔ Transcendental (↥(adjoin R (x '' s))) (x i)
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: case refine_2
ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
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✝ : NoZeroDivisors A
x : ι → S
y : ι' → A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis S y
h✝ : Nontrivial R
Rx : Subalgebra R S := adjoin R (range x)
Rxy : Subalgebra (↥Rx) A := adjoin (↥Rx) (range y)
this✝³ : Nontrivial S
this✝² : Nontrivial A
Sy : Subalgebra S A := adjoin S (range y)
this✝¹ : Algebra.IsAlgebraic (↥Sy) A
x✝² : Algebra ↥Rxy ↥Sy := (Subalgebra.inclusion ⋯).toAlgebra
this✝ : IsScalarTower (↥Rxy) (↥Sy) A
this : IsScalarTower ↥Rx ↥Rxy ↥Sy
x✝¹ : ↥Sy
a : A
ha : a ∈ Sy
x✝ : S
⊢ Injective ⇑(algebraMap ↥Rx ↥Rxy)

pp: case refine_3
ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
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✝ : NoZeroDivisors A
x : ι → S
y : ι' → A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis S y
h✝ : Nontrivial R
Rx : Subalgebra R S := adjoin R (range x)
Rxy : Subalgebra (↥Rx) A := adjoin (↥Rx) (range y)
this✝³ : Nontrivial S
this✝² : Nontrivial A
Sy : Subalgebra S A := adjoin S (range y)
this✝¹ : Algebra.IsAlgebraic (↥Sy) A
x✝² : Algebra ↥Rxy ↥Sy := (Subalgebra.inclusion ⋯).toAlgebra
this✝ : IsScalarTower (↥Rxy) (↥Sy) A
this : IsScalarTower ↥Rx ↥Rxy ↥Sy
x✝¹ : ↥Sy
a : A
ha : a ∈ Sy
x✝ : S
⊢ IsAlgebraic ↥Rx ⟨(algebraMap S A) x✝, ⋯⟩

Tactic:
· exact fun _ _ ↦ (Subtype.ext <| hy.1.algebraMap_injective <| Subtype.ext_iff.mp ·)

Goal state after:
case refine_3
ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
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✝ : NoZeroDivisors A
x : ι → S
y : ι' → A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis S y
h✝ : Nontrivial R
Rx : Subalgebra R S := adjoin R (range x)
Rxy : Subalgebra (↥Rx) A := adjoin (↥Rx) (range y)
this✝³ : Nontrivial S
this✝² : Nontrivial A
Sy : Subalgebra S A := adjoin S (range y)
this✝¹ : Algebra.IsAlgebraic (↥Sy) A
x✝² : Algebra ↥Rxy ↥Sy := (Subalgebra.inclusion ⋯).toAlgebra
this✝ : IsScalarTower (↥Rxy) (↥Sy) A
this : IsScalarTower ↥Rx ↥Rxy ↥Sy
x✝¹ : ↥Sy
a : A
ha : a ∈ Sy
x✝ : S
⊢ IsAlgebraic ↥Rx ⟨(algebraMap S A) x✝, ⋯⟩
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: ι : Type u
F : Type u_2
E : Type u_3
x : ι → E
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hx : IsTranscendenceBasis F x
S : Set E := range x
this✝¹ : Algebra.IsAlgebraic (↥(adjoin F S)) E
this✝ : Algebra ↥(adjoin F S) ↥(IntermediateField.adjoin F S) := (Subalgebra.inclusion ⋯).toAlgebra
this : IsScalarTower (↥(adjoin F S)) (↥(IntermediateField.adjoin F S)) E
⊢ Algebra.IsAlgebraic (↥(IntermediateField.adjoin F S)) E

Tactic:
exact Algebra.IsAlgebraic.extendScalars (R := adjoin F S) (Subalgebra.inclusion_injective _)

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

Goal state before:
pp: case refine_2
R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : IsDomain A
s : Set A
S : Subalgebra (↥(adjoin R s)) A := algebraicClosure (↥(adjoin R s)) A
⊢ (∃ S, ↑S = s ∧ ∀ (a : A), IsAlgebraic (↥S) a → a ∈ s) → ↑S = s

Tactic:
rintro ⟨s, rfl, hs⟩

Goal state after:
case refine_2
R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : IsDomain A
s : Subalgebra R A
S : Subalgebra (↥(adjoin R ↑s)) A := algebraicClosure (↥(adjoin R ↑s)) A
hs : ∀ (a : A), IsAlgebraic (↥s) a → a ∈ ↑s
⊢ ↑S = ↑s
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
inst✝¹ : IsGalois F E
inst✝ : Finite Gal(E/F)
H : ¬FiniteDimensional F E
K : IntermediateField F E
h₁ : FiniteDimensional F ↥K
h₂ : Nat.card Gal(E/F) < finrank F ↥K
K' : IntermediateField F E := normalClosure F (↥K) E
⊢ False

Tactic:
have : IsGalois F K' := ⟨⟩

Goal state after:
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : IsGalois F E
inst✝ : Finite Gal(E/F)
H : ¬FiniteDimensional F E
K : IntermediateField F E
h₁ : FiniteDimensional F ↥K
h₂ : Nat.card Gal(E/F) < finrank F ↥K
K' : IntermediateField F E := normalClosure F (↥K) E
this : IsGalois F ↥K'
⊢ False
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ finSepDegree F E ∣ finrank F E

Tactic:
by_cases hfd : FiniteDimensional F E
  · rw [← finSepDegree_top F, ← finrank_top F E]
    refine induction_on_adjoin (fun K : IntermediateField F E ↦ finSepDegree F K ∣ finrank F K)
      (by simp_rw [finSepDegree_bot, IntermediateField.finrank_bot, one_dvd]) (fun L x h ↦ ?_) ⊤
    have hdvd := mul_dvd_mul h <| finSepDegree_adjoin_simple_dvd_finrank L E x
    set M := L⟮x⟯
    rwa [finSepDegree_mul_finSepDegree_of_isAlgebraic F L M,
      Module.finrank_mul_finrank F L M] at hdvd
  rw [finrank_of_infinite_dimensional hfd]
  exact dvd_zero _

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

Goal state before:
pp: case refine_2
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
this :
  map (algebraMap K g.SplittingField) g ∈ lifts (algebraMap (↥(integralClosure R g.SplittingField)) g.SplittingField)
⊢ g ∈ lifts (algebraMap (↥(integralClosure R K)) K)

Tactic:
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

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

Goal state before:
pp: case h.left
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
⊢ σ • ↑(adjoin k {y}).fixingSubgroup ⊆ (↑L.fixingSubgroup)ᶜ

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:
· intro f hf
      rcases (Set.mem_smul_set.mp hf) with ⟨g, hg, eq⟩
      simp only [Set.mem_compl_iff, SetLike.mem_coe, ← eq]
      apply (mem_fixingSubgroup_iff Gal(K/k)).not.mpr
      push Not
      use y
      simp only [yL, smul_eq_mul, AlgEquiv.smul_def, AlgEquiv.mul_apply, ne_eq, true_and]
      have : g y = y := (mem_fixingSubgroup_iff Gal(K/k)).mp hg y <|
        adjoin_simple_le_iff.mp le_rfl
      simpa only [this, ne_eq, AlgEquiv.smul_def] using! ne

Goal state after:
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
Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed

Goal state before:
pp: case h
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain S
inst✝ : IsTorsionFree R S
s : S
p : R[X]
hp : (Polynomial.aeval s) p = 0
h₀ : p ≠ 0
pmin : ∀ (q : R[X]), q.Monic → (Polynomial.aeval s) q = 0 → p.degree ≤ q.degree
hInt : IsIntegral R s
q : R[X]
hMul : p = minpoly R s * q
⊢ q.degree ≤ 0

Tactic:
apply WithBot.le_of_add_le_add_left <| Polynomial.degree_ne_bot.mpr <| minpoly.ne_zero hInt

Goal state after:
case h
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain S
inst✝ : IsTorsionFree R S
s : S
p : R[X]
hp : (Polynomial.aeval s) p = 0
h₀ : p ≠ 0
pmin : ∀ (q : R[X]), q.Monic → (Polynomial.aeval s) q = 0 → p.degree ≤ q.degree
hInt : IsIntegral R s
q : R[X]
hMul : p = minpoly R s * q
⊢ (minpoly R s).degree + q.degree ≤ (minpoly R s).degree + 0
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
inst✝ : Algebra.IsAlgebraic F E
⊢ #(Emb F ↥(separableClosure F E)) = Cardinal.lift.{v, v} #(Emb F ↥(separableClosure F E)) * Cardinal.lift.{v, v} 1

Tactic:
lift_one,

Goal state after:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
⊢ #(Emb F ↥(separableClosure F E)) = Cardinal.lift.{v, v} #(Emb F ↥(separableClosure F E)) * 1
Module: Mathlib.RingTheory.DedekindDomain.IntegralClosure

Goal state before:
pp: 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
inst✝⁴ : Algebra K L
inst✝³ : Algebra A L
inst✝² : IsScalarTower A K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsDomain A
this : DecidableEq L := Classical.decEq L
s' : Finset L := IsNoetherian.finsetBasisIndex K L
bs' : Basis (↥(IsNoetherian.finsetBasisIndex K L)) K L := IsNoetherian.finsetBasis K L
y : A
hy : y ≠ 0
his' : ∀ x ∈ Finset.image (⇑bs') Finset.univ, IsIntegral A (y • x)
⊢ ∃ s b, ∀ (x : ↥s), IsIntegral A (b x)

Tactic:
have hy' : algebraMap A L y ≠ 0 := by
    refine mt ((injective_iff_map_eq_zero (algebraMap A L)).mp ?_ _) hy
    rw [IsScalarTower.algebraMap_eq A K L]
    exact (algebraMap K L).injective.comp (IsFractionRing.injective A K)

Goal state after:
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
inst✝⁴ : Algebra K L
inst✝³ : Algebra A L
inst✝² : IsScalarTower A K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsDomain A
this : DecidableEq L := Classical.decEq L
s' : Finset L := IsNoetherian.finsetBasisIndex K L
bs' : Basis (↥(IsNoetherian.finsetBasisIndex K L)) K L := IsNoetherian.finsetBasis K L
y : A
hy : y ≠ 0
his' : ∀ x ∈ Finset.image (⇑bs') Finset.univ, IsIntegral A (y • x)
hy' : (algebraMap A L) y ≠ 0
⊢ ∃ s b, ∀ (x : ↥s), IsIntegral A (b x)
Module: Mathlib.RingTheory.Invariant.Basic

Goal state before:
pp: B : Type u_2
G : Type u_3
inst✝³ : CommRing B
inst✝² : Group G
inst✝¹ : MulSemiringAction G B
inst✝ : Fintype G
b : B
⊢ b - b = 0

Tactic:
sub_self

Goal state after:
B : Type u_2
G : Type u_3
inst✝³ : CommRing B
inst✝² : Group G
inst✝¹ : MulSemiringAction G B
inst✝ : Fintype G
b : B
⊢ 0 = 0
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 Q : Ideal B
hP : P.IsPrime
hQ : Q.IsPrime
hPQ : Ideal.under A P = Ideal.under A Q
b : B
hb : b ∈ ↑Q
a : A
ha : (algebraMap A B) a = ∏ g, g • b
⊢ a ∈ Ideal.under A Q

Tactic:
Q.mem_comap,

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
hP : P.IsPrime
hQ : Q.IsPrime
hPQ : Ideal.under A P = Ideal.under A Q
b : B
hb : b ∈ ↑Q
a : A
ha : (algebraMap A B) a = ∏ g, g • b
⊢ (algebraMap A B) a ∈ Q
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case h1
n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
⊢ ↑y - ↑y = 0

Tactic:
sub_self

Goal state after:
case h1
n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
⊢ 0 = 0
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: K : Type u_1
inst✝³ : Ring K
inst✝² : NoZeroDivisors K
inst✝¹ : Nontrivial K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
n : ℕ := Fintype.card ↥G
nzero : ↑(Fintype.card ↥G) = 0
p : ℕ
char_p : CharP K p
hd : p ∣ n
pprime : Nat.Prime p
fact_pprime : Fact (Nat.Prime p)
x : ↥G
hx : orderOf x = p
u : K := ↑↑x
hu : orderOf u = p
⊢ 1 - 1 = 0

pp: case h
K : Type u_1
inst✝³ : Ring K
inst✝² : NoZeroDivisors K
inst✝¹ : Nontrivial K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
n : ℕ := Fintype.card ↥G
nzero : ↑(Fintype.card ↥G) = 0
p : ℕ
char_p : CharP K p
hd : p ∣ n
pprime : Nat.Prime p
fact_pprime : Fact (Nat.Prime p)
x : ↥G
hx : orderOf x = p
u : K := ↑↑x
hu : orderOf u = p
⊢ Commute u 1

Tactic:
sub_self

Goal state after:
K : Type u_1
inst✝³ : Ring K
inst✝² : NoZeroDivisors K
inst✝¹ : Nontrivial K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
n : ℕ := Fintype.card ↥G
nzero : ↑(Fintype.card ↥G) = 0
p : ℕ
char_p : CharP K p
hd : p ∣ n
pprime : Nat.Prime p
fact_pprime : Fact (Nat.Prime p)
x : ↥G
hx : orderOf x = p
u : K := ↑↑x
hu : orderOf u = p
⊢ 0 = 0

case h
K : Type u_1
inst✝³ : Ring K
inst✝² : NoZeroDivisors K
inst✝¹ : Nontrivial K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
n : ℕ := Fintype.card ↥G
nzero : ↑(Fintype.card ↥G) = 0
p : ℕ
char_p : CharP K p
hd : p ∣ n
pprime : Nat.Prime p
fact_pprime : Fact (Nat.Prime p)
x : ↥G
hx : orderOf x = p
u : K := ↑↑x
hu : orderOf u = p
⊢ Commute u 1
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: K : Type u_1
inst✝² : Ring K
inst✝¹ : NoZeroDivisors K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
a : ↥G
ha : a ≠ 1
a_mul_emb : ↥G ↪ ↥G := mulLeftEmbedding a
h_unchanged : map a_mul_emb univ = univ
h_sum_map : ∑ x, ↑↑x = ↑↑a * ∑ x, ↑↑x
⊢ ∑ x, ↑↑x - ∑ x, ↑↑x = 0

Tactic:
sub_self

Goal state after:
K : Type u_1
inst✝² : Ring K
inst✝¹ : NoZeroDivisors K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
a : ↥G
ha : a ≠ 1
a_mul_emb : ↥G ↪ ↥G := mulLeftEmbedding a
h_unchanged : map a_mul_emb univ = univ
h_sum_map : ∑ x, ↑↑x = ↑↑a * ∑ x, ↑↑x
⊢ 0 = 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
h_multiset_map_sum :
  (Multiset.map (fun x ↦ ↑↑x ^ k) univ.val).sum = (Multiset.map (fun x ↦ ↑↑x ^ k) univ.val).sum * ↑↑a ^ k
⊢ (Multiset.map (fun x ↦ ↑↑x ^ k) univ.val).sum - (Multiset.map (fun i ↦ ↑↑i ^ k) univ.val).sum = 0

Tactic:
sub_self

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) univ.val).sum * ↑↑a ^ k
⊢ 0 = 0
Module: Mathlib.RingTheory.Int.Basic

Goal state before:
pp: a : ℤ
⊢ Ideal.span {↑a.natAbs} = Ideal.span {a}

Tactic:
rw [Ideal.span_singleton_eq_span_singleton]
  exact (associated_natAbs _).symm

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

Goal state before:
pp: K : Type u_1
R : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Fintype K
inst✝³ : CommRing R
inst✝² : Algebra K R
p : ℕ
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
p' : ℕ
left✝ : CharP K p'
n : ℕ+
hp : Nat.Prime p'
card_eq : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
card_eq

Goal state after:
K : Type u_1
R : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Fintype K
inst✝³ : CommRing R
inst✝² : Algebra K R
p : ℕ
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
p' : ℕ
left✝ : CharP K p'
n : ℕ+
hp : Nat.Prime p'
card_eq : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Function.Bijective fun x ↦ x ^ p' ^ ↑n
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: K : Type u_1
R : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Fintype K
inst✝³ : CommRing R
inst✝² : Algebra K R
p : ℕ
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
p' : ℕ
left✝ : CharP K p'
n : ℕ+
hp : Nat.Prime p'
card_eq : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Function.Bijective fun x ↦ x ^ p' ^ ↑n

Tactic:
have : ExpChar K p' := ExpChar.prime hp

Goal state after:
K : Type u_1
R : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Fintype K
inst✝³ : CommRing R
inst✝² : Algebra K R
p : ℕ
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
p' : ℕ
left✝ : CharP K p'
n : ℕ+
hp : Nat.Prime p'
card_eq : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : ExpChar K p'
⊢ Function.Bijective fun x ↦ x ^ p' ^ ↑n
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: p x y : ℕ
hp : Nat.Prime p
h : p - 1 ∣ x - y
hxy : y ≤ x
hy : 0 < y
n : ℤ
⊢ n ^ x ≡ n ^ y [ZMOD ↑p]

Tactic:
rw [← Nat.mul_div_eq_iff_dvd] at h
  by_cases hn : n ≡ 0 [ZMOD p]
  · grw [hn, zero_pow (hy.trans_le hxy).ne', zero_pow hy.ne']
  · rw [Int.modEq_zero_iff_dvd, ← (Nat.prime_iff_prime_int.mp hp).coprime_iff_not_dvd] at hn
    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 succ.zero
p a d k : ℕ
hk : k ∈ range p
hd : (1 + p * a) ^ p ^ 0 = p ^ 0 * d + 1
⊢ p ∣ (p ^ 0 * d) ^ k * ↑(p.choose (k + 1))

Tactic:
rw [pow_zero, pow_one, one_mul, add_comm, add_left_inj] at hd
      cases k <;> simp [← hd, mul_assoc, pow_succ']

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

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

Tactic:
a

Goal state after: