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

Goal state before:
pp: α : Type u_1
M : Matroid α
I X Y : Set α
hIX : M.IsBasis I X
hIY : M.IsBasis I Y
⊢ M.IsBasis I (X ∪ Y)

Tactic:
convert! hIX.union_isBasis_union hIY _

Goal state after:
α : Type u_1
M : Matroid α
I X Y : Set α
hIX : M.IsBasis I X
hIY : M.IsBasis I Y
⊢ I = I ∪ I

α : Type u_1
M : Matroid α
I X Y : Set α
hIX : M.IsBasis I X
hIY : M.IsBasis I Y
⊢ M.Indep (I ∪ I)
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
I E R : Set α
⊢ uniqueBaseOn I E ↾ R = uniqueBaseOn (I ∩ R ∩ E) R

Tactic:
simp_rw [ext_iff_indep, restrict_ground_eq, uniqueBaseOn_ground, true_and,
    restrict_indep_iff, uniqueBaseOn_indep_iff', subset_inter_iff]
  tauto

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

Goal state before:
pp: α : Type u_1
E : Set α
IsBase : Set α → Prop
exists_finite_base : ∃ B, IsBase B ∧ B.Finite
isBase_exchange : ExchangeProperty IsBase
subset_ground : ∀ (B : Set α), IsBase B → B ⊆ E
⊢ ∃ B, IsBase B

Tactic:
obtain ⟨B, h⟩ := exists_finite_base

Goal state after:
α : Type u_1
E : Set α
IsBase : Set α → Prop
isBase_exchange : ExchangeProperty IsBase
subset_ground : ∀ (B : Set α), IsBase B → B ⊆ E
B : Set α
h : IsBase B ∧ B.Finite
⊢ ∃ B, IsBase B
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
C I : Set α
hC : M.IsCircuit C
⊢ M.IsBasis I C ↔ ∃ e ∈ C \ I, C = insert e I

Tactic:
rw [hC.isBasis_iff_eq_sdiff_singleton]
  refine ⟨fun ⟨e, he, hI⟩ ↦ ⟨e, ⟨he, fun heI ↦ (hI.subset heI).2 rfl⟩, ?_⟩,
    fun ⟨e, he, hC⟩ ↦ ⟨e, he.1, ?_⟩⟩
  · rw [hI, insert_sdiff_singleton, insert_eq_of_mem he]
  rw [hC, insert_sdiff_self_of_notMem he.2]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
C : Set α
hC : M.IsCircuit C
h : 1 < C.encard
he : e ∈ C
⊢ M.IsNonloop e

Tactic:
refine isNonloop_of_not_isLoop (hC.subset_ground he) (fun hlp ↦ ?_)
  rw [hlp.eq_of_isCircuit_mem hC he, encard_singleton] at h
  exact h.ne rfl

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
hX : M.Dep X
I : Set α
hI : M.IsBasis I X
e : α
heX : e ∈ X
heI : e ∉ I
⊢ ∃ C ⊆ X, M.IsCircuit C

Tactic:
exact ⟨M.fundCircuit e I, (M.fundCircuit_subset_insert e I).trans (insert_subset heX hI.subset),
    hI.indep.fundCircuit_isCircuit (hI.subset_closure heX) heI⟩

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

Goal state before:
pp: α : Type u_1
M : Matroid α
C : Set α
hC : M.IsCircuit C
e : α
he : e ∈ C
⊢ M.closure (C \ {e}) = M.closure C

Tactic:
by rw [(hC.sdiff_singleton_isBasis he).closure_eq_closure]

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

Goal state before:
pp: α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ ⦃C : Set α⦄, C ⊆ M₁.E → (M₁.IsCircuit C ↔ M₂.IsCircuit C)
h' : ∀ {C : Set α}, M₁.IsCircuit C ↔ M₂.IsCircuit C
I : Set α
hI : I ⊆ M₁.E
⊢ M₁.Indep I ↔ M₂.Indep I

Tactic:
indep_iff_forall_subset_not_isCircuit hI,

Goal state after:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ ⦃C : Set α⦄, C ⊆ M₁.E → (M₁.IsCircuit C ↔ M₂.IsCircuit C)
h' : ∀ {C : Set α}, M₁.IsCircuit C ↔ M₂.IsCircuit C
I : Set α
hI : I ⊆ M₁.E
⊢ (∀ C ⊆ I, ¬M₁.IsCircuit C) ↔ M₂.Indep I
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
C₀ : Set α
hC₀ : M.IsCircuit C₀
X : Set α
S : Set (Set α)
z : α
hCS : ∀ C ∈ S, M.IsCircuit C
hXC₀ : X ⊆ C₀
hzC₀ : z ∈ C₀
hz : ∀ C ∈ S, z ∉ C
C : α → Set α
hC : (∀ x ∈ X, C x ∈ S) ∧ ∀ x ∈ X, C x ∩ X = {x}
e : α
heX : e ∈ X
⊢ {e} ⊆ C e

Tactic:
by simp [← hC.2 e heX]

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

Goal state before:
pp: case inr
α : Type u_1
M : Matroid α
e : α
B : Set α
hB : M.IsBase B
he : e ∈ B
h : ∀ x ∈ M.E \ B, e ∉ M.fundCircuit x B
x : α
hxE : x ∈ M.E
hne : x ≠ e
hx : x ∉ B
⊢ x ∈ M.closure (B \ {e})

Tactic:
have h_cct := (hB.fundCircuit_isCircuit hxE hx).mem_closure_sdiff_singleton_of_mem
      (M.mem_fundCircuit x B)

Goal state after:
case inr
α : Type u_1
M : Matroid α
e : α
B : Set α
hB : M.IsBase B
he : e ∈ B
h : ∀ x ∈ M.E \ B, e ∉ M.fundCircuit x B
x : α
hxE : x ∈ M.E
hne : x ≠ e
hx : x ∉ B
h_cct : x ∈ M.closure (M.fundCircuit x B \ {x})
⊢ x ∈ M.closure (B \ {e})
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
heI : e ∉ I
⊢ e ∈ M.closure I ↔ e ∈ M.closure I ∧ e ∉ I

Tactic:
and_iff_left heI

Goal state after:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
heI : e ∉ I
⊢ e ∈ M.closure I ↔ e ∈ M.closure I
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
heI : e ∉ I
he : e ∈ M.E
⊢ M.Indep (insert e I) ∧ e ∉ I ↔ M.Indep (insert e I)

Tactic:
and_iff_left heI

Goal state after:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
heI : e ∉ I
he : e ∈ M.E
⊢ M.Indep (insert e I) ↔ M.Indep (insert e I)
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
β : Type v
M : Matroid β
f : α → β
X : Set α
I : Set β
hIX : M.IsBasis' I (f '' X)
⊢ ∃ I₀ ⊆ X, f '' I₀ = I ∧ InjOn f I₀

Tactic:
obtain ⟨I₀, hI₀ss, hbij⟩ := exists_subset_bijOn (f ⁻¹' I ∩ X) f
    refine ⟨I₀, hI₀ss.trans inter_subset_right, ?_, hbij.injOn⟩
    rw [hbij.image_eq, image_preimage_inter, inter_eq_self_of_subset_left hIX.subset]

Goal state after:
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]
hf : Function.Injective ⇑(Polynomial.aeval f)
g : MvPolynomial (↑s) R[X] →ₐ[R] MvPolynomial (↑s) R[X] := mapAlgHom (Polynomial.aeval f)
⊢ Function.Injective ⇑(Polynomial.aeval ((Polynomial.aeval (X i)) f))

Tactic:
replace hf : Function.Injective g := MvPolynomial.map_injective _ hf

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
⊢ Function.Injective ⇑(Polynomial.aeval ((Polynomial.aeval (X i)) f))
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
aux : ∀ {N : Matroid α} {B' : Set α}, N.IsBase B' → ∀ {e f : α}, e ∈ N.fundCocircuit f B' → f ∈ N.fundCircuit e B'
h : f ∈ M.fundCircuit e B
⊢ f ∈ M✶.fundCocircuit e (M.E \ B)

Tactic:
simpa [fundCocircuit, inter_eq_self_of_subset_right hB.subset_ground]

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
M : Matroid α
X : Set α
⊢ toENat (M.cRk X) = M.eRk X

Tactic:
by
  rw [cRk, toENat_cRank_eq, eRk]

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

Goal state before:
pp: case inl
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
hfI : e ∈ M.closure I
he : e ∈ M.closure (insert e I \ {e})
⊢ M.Indep (insert e I \ {e})

pp: case inr
α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep I
hfI : f ∈ M.closure I
he : e ∈ M.closure (insert f I \ {e})
heI : e ∈ I
⊢ M.Indep (insert f I \ {e})

Tactic:
· exact hI.subset (by simp)

Goal state after:
case inr
α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep I
hfI : f ∈ M.closure I
he : e ∈ M.closure (insert f I \ {e})
heI : e ∈ I
⊢ M.Indep (insert f I \ {e})
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
f : ι → Polynomial R
hf : ∀ (i : ι), Transcendental R (f i)
x✝ : ι
⊢ (Polynomial.aeval (x x✝)) (f x✝) = (aeval x) ((Polynomial.aeval (X x✝)) (f x✝))

Tactic:
rw [← AlgHom.comp_apply]

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
hx : AlgebraicIndependent R x
f : ι → Polynomial R
hf : ∀ (i : ι), Transcendental R (f i)
x✝ : ι
⊢ (Polynomial.aeval (x x✝)) (f x✝) = ((aeval x).comp (Polynomial.aeval (X x✝))) (f x✝)
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
X : Set α
hK : X ⊆ M.E
⊢ M.Coindep X ↔ M.closure (M.E \ X) = M.E

Tactic:
by
  rw [coindep_iff_compl_spanning, spanning_iff_closure_eq]

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

Goal state before:
pp: case refine_2
ι : 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
a : A
⊢ ∀ (i : Option ι),
    (Polynomial.aeval a) (hx.mvPolynomialOptionEquivPolynomialAdjoin (X i)) = (aeval fun o ↦ o.elim a x) (X i)

Tactic:
· rintro (⟨⟩ | ⟨i⟩)
    · rw [hx.mvPolynomialOptionEquivPolynomialAdjoin_X_none, aeval_X, Polynomial.aeval_X,
        Option.elim]
    · rw [hx.mvPolynomialOptionEquivPolynomialAdjoin_X_some, Polynomial.aeval_C,
        hx.algebraMap_aevalEquiv, aeval_X, aeval_X, Option.elim]

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

Goal state before:
pp: ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
i : AlgebraicIndependent R x
⊢ IsTranscendenceBasis R x ↔
    ∀ (κ : Type w) (w : κ → A), AlgebraicIndependent R w → ∀ (j : ι → κ), w ∘ j = x → Surjective j

Tactic:
fconstructor
  · rintro p κ w i' j rfl
    have p := p.2 (range w) i'.coe_range (range_comp_subset_range _ _)
    rw [range_comp, ← @image_univ _ _ w] at p
    exact range_eq_univ.mp (image_injective.mpr i'.injective p)
  · intro p
    use i
    intro w i' h
    specialize p w ((↑) : w → A) i' (fun i => ⟨x i, range_subset_iff.mp h i⟩) (by ext; simp)
    have q := congr_arg (fun s => ((↑) : w → A) '' s) p.range_eq
    rw [← image_univ, image_image] at q
    simpa using q

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
x✝ : Gal(E/F)
⊢ x✝ ∈ ⊤.fixingSubgroup ↔ x✝ ∈ ⊥

Tactic:
simp [DFunLike.ext_iff]

Goal state after:
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : TopologicalSpace R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : ModuleFilterBasis R M
inst✝ : DiscreteTopology R
⊢ ∀ (x₀ : R) {U : Set M},
    U ∈
        (have this := default;
          this).sets →
      ∃
        V ∈
          (have this := default;
            this).sets,
        V ⊆ (fun x ↦ x₀ • x) ⁻¹' U

Tactic:
by
        rintro x₀ U (h : U ∈ {{(0 : M)}})
        rw [mem_singleton_iff] at h
        use {0}, rfl
        simp [h]

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
⊢ TotallySeparatedSpace Gal(L/K)

Tactic:
by
  rw [totallySeparatedSpace_iff_exists_isClopen]
  intro σ τ h_diff
  have hστ : σ⁻¹ * τ ≠ 1 := by rwa [Ne, inv_mul_eq_one]
  rcases DFunLike.exists_ne hστ with ⟨x, hx : (σ⁻¹ * τ) x ≠ x⟩
  let E := IntermediateField.adjoin K ({x} : Set L)
  have := IntermediateField.adjoin.finiteDimensional
    (Algebra.IsIntegral.isIntegral (R := K) x)
  refine ⟨σ • E.fixingSubgroup,
    ⟨E.fixingSubgroup_isClosed.leftCoset σ, E.fixingSubgroup_isOpen.leftCoset σ⟩,
    ⟨1, E.fixingSubgroup.one_mem', mul_one σ⟩, ?_⟩
  simp only [Set.mem_compl_iff, mem_leftCoset_iff, SetLike.mem_coe,
    IntermediateField.mem_fixingSubgroup_iff, not_forall]
  exact ⟨x, IntermediateField.mem_adjoin_simple_self K x, hx⟩

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

Goal state before:
pp: case mp
F : Type u_1
E : Type u_2
E' : Type u_3
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Field E'
inst✝⁴ : Algebra F E
inst✝³ : Algebra F E'
inst✝² : Algebra E E'
inst✝¹ : IsScalarTower F E E'
L : IntermediateField F E
inst✝ : Normal F E
f : Gal(E'/F)
h : ∀ x ∈ map (IsScalarTower.toAlgHom F E E') L, f x = x
x : E
hx : x ∈ L
⊢ f ((algebraMap E E') x) = (algebraMap E E') x

Tactic:
exact h _ ⟨x, hx, rfl⟩

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed

Goal state before:
pp: case refine_1
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]
hmo : P.Monic
hP : (Polynomial.aeval s) P = 0
Pmin : ∀ (Q : R[X]), Q.Monic → (Polynomial.aeval s) Q = 0 → P.degree ≤ Q.degree
hs : IsIntegral R s
hnz : ¬minpoly R s - P = 0
⊢ (minpoly R s).degree = P.degree

Tactic:
exact le_antisymm (min R s hmo hP) (Pmin (minpoly R s) (monic hs) (aeval R s))

Goal state after:
Module: Mathlib.FieldTheory.IsSepClosed

Goal state before:
pp: k : Type u
inst✝⁴ : Field k
K : Type v
inst✝³ : Field K
inst✝² : IsSepClosed k
inst✝¹ : Algebra k K
inst✝ : Algebra.IsSeparable k K
x : K
hq : (minpoly k x).leadingCoeff = 1
hsep : IsSeparable k x
h : (minpoly k x).degree = 1
this : (aeval x) (minpoly k x) = 0
⊢ (algebraMap k K) (-(minpoly k x).coeff 0) = x

Tactic:
rw [eq_X_add_C_of_degree_eq_one h, hq, C_1, one_mul, aeval_add, aeval_X, aeval_C,
    add_eq_zero_iff_eq_neg] at this

Goal state after:
k : Type u
inst✝⁴ : Field k
K : Type v
inst✝³ : Field K
inst✝² : IsSepClosed k
inst✝¹ : Algebra k K
inst✝ : Algebra.IsSeparable k K
x : K
hq : (minpoly k x).leadingCoeff = 1
hsep : IsSeparable k x
h : (minpoly k x).degree = 1
this : x = -(algebraMap k K) ((minpoly k x).coeff 0)
⊢ (algebraMap k K) (-(minpoly k x).coeff 0) = x
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✝
q✝ : ℕ
inst✝⁸ : ExpChar F✝ q✝
inst✝⁷ : IsPurelyInseparable F✝ E✝
inst✝⁶ : FiniteDimensional F✝ E✝
E : Type v
inst✝⁵ : Field E
q d : ℕ
IH :
  ∀ m < d,
    ∀ (F : Type v) [inst : Field F] [inst_1 : Algebra F E] [ExpChar F q] [IsPurelyInseparable F E]
      [FiniteDimensional F E], finrank F E = m → ∃ n, m = q ^ n
F : Type v
inst✝⁴ : Field F
inst✝³ : Algebra F E
inst✝² : ExpChar F q
inst✝¹ : IsPurelyInseparable F E
inst✝ : FiniteDimensional F E
hd : finrank F E = d
h : ¬⊥ = ⊤
x : E
hx : x ∉ ⊥
m : ℕ
y : F
e : minpoly F x = X ^ q ^ m - C y
this : finrank F ↥F⟮x⟯ = q ^ m
H : q ^ m ≤ 1
⊢ 1 ≤ finrank F ↥F⟮x⟯

Tactic:
exact Nat.one_le_iff_ne_zero.mpr Module.finrank_pos.ne'

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

Goal state before:
pp: G : Type u_1
A : Type u_2
B : Type u_4
inst✝⁷ : Group G
inst✝⁶ : CommSemiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra A B
inst✝³ : MulSemiringAction G B
hG : IsGaloisGroup G A B
B' : Type u_5
inst✝² : Semiring B'
inst✝¹ : Algebra A B'
inst✝ : MulSemiringAction G B'
e : B ≃ₐ[A] B'
he : ∀ (g : G) (x : B), e (g • x) = g • e x
g : G
a : A
b' x' : B'
⊢ e.symm (g • x') = g • e.symm x'

Tactic:
apply e.injective

Goal state after:
G : Type u_1
A : Type u_2
B : Type u_4
inst✝⁷ : Group G
inst✝⁶ : CommSemiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra A B
inst✝³ : MulSemiringAction G B
hG : IsGaloisGroup G A B
B' : Type u_5
inst✝² : Semiring B'
inst✝¹ : Algebra A B'
inst✝ : MulSemiringAction G B'
e : B ≃ₐ[A] B'
he : ∀ (g : G) (x : B), e (g • x) = g • e x
g : G
a : A
b' x' : B'
⊢ e (e.symm (g • x')) = e (g • e.symm x')
Module: Mathlib.RingTheory.IsGaloisGroup.Defs

Goal state before:
pp: G : Type u_1
A : Type u_2
B : Type u_4
inst✝⁷ : Group G
inst✝⁶ : CommSemiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra A B
inst✝³ : MulSemiringAction G B
hG : IsGaloisGroup G A B
B' : Type u_5
inst✝² : Semiring B'
inst✝¹ : Algebra A B'
inst✝ : MulSemiringAction G B'
e : B ≃ₐ[A] B'
he : ∀ (g : G) (x : B), e (g • x) = g • e x
x' : B'
hx' : ∀ (g : G), g • x' = x'
g : G
⊢ g • e.symm x' = e.symm x'

Tactic:
apply e.injective

Goal state after:
G : Type u_1
A : Type u_2
B : Type u_4
inst✝⁷ : Group G
inst✝⁶ : CommSemiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra A B
inst✝³ : MulSemiringAction G B
hG : IsGaloisGroup G A B
B' : Type u_5
inst✝² : Semiring B'
inst✝¹ : Algebra A B'
inst✝ : MulSemiringAction G B'
e : B ≃ₐ[A] B'
he : ∀ (g : G) (x : B), e (g • x) = g • e x
x' : B'
hx' : ∀ (g : G), g • x' = x'
g : G
⊢ e (g • e.symm x') = e (e.symm x')
Module: Mathlib.RingTheory.IsGaloisGroup.Defs

Goal state before:
pp: G : Type u_1
A : Type u_2
A' : Type u_3
B : Type u_4
inst✝⁶ : Group G
inst✝⁵ : CommSemiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra A B
inst✝² : MulSemiringAction G B
hG : IsGaloisGroup G A B
inst✝¹ : CommSemiring A'
inst✝ : Algebra A' B
e : A →+* A'
he : ∀ (a : A), (algebraMap A' B) (e a) = (algebraMap A B) a
he' : Function.Surjective ⇑e
b : B
h : ∀ (g : G), g • b = b
⊢ ∃ a, (algebraMap A' B) a = b

Tactic:
obtain ⟨a, ha⟩ := hG.isInvariant.isInvariant b h

Goal state after:
G : Type u_1
A : Type u_2
A' : Type u_3
B : Type u_4
inst✝⁶ : Group G
inst✝⁵ : CommSemiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra A B
inst✝² : MulSemiringAction G B
hG : IsGaloisGroup G A B
inst✝¹ : CommSemiring A'
inst✝ : Algebra A' B
e : A →+* A'
he : ∀ (a : A), (algebraMap A' B) (e a) = (algebraMap A B) a
he' : Function.Surjective ⇑e
b : B
h : ∀ (g : G), g • b = b
a : A
ha : (algebraMap A B) a = b
⊢ ∃ a, (algebraMap A' B) a = b
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: x✝ : NeZero 0
x : ZMod 0
⊢ x.valMinAbs = if x.val ≤ 0 / 2 then ↑x.val else ↑x.val - ↑0

Tactic:
cases NeZero.ne 0 rfl

Goal state after:
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:
· rw [← Int.cast_natCast, Int.ofNat_natAbs_of_nonpos this, Int.cast_neg, Int.cast_sub,
      Int.cast_natCast, Int.cast_natCast, natCast_self, sub_zero, natCast_zmod_val]

Goal state after:
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:
rw [pb.trace_gen_eq_sum_roots hE, Fintype.sum_equiv pb.liftEquiv', Finset.sum_mem_multiset,
    Finset.sum_eq_multiset_sum, Multiset.toFinset_val, Multiset.dedup_eq_self.mpr _,
    Multiset.map_id]

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).Nodup

case f
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 := ⋯
this : Fintype (L →ₐ[K] E) := ⋯
⊢ { x // x ∈ (minpoly K pb.gen).aroots E } → E

case hfg
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
⊢ ∀ (x : { x // x ∈ (minpoly K pb.gen).aroots E }), ?f✝ x = _root_.id ↑x

case h
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
⊢ ∀ (x : L →ₐ[K] E), x pb.gen = ?f✝ (pb.liftEquiv' x)
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: case neg
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : ¬Algebra.IsSeparable K L
p : ℕ
hp : ExpChar K p
this : p ≠ 0
x : L
h₀ : FiniteDimensional K L
hx : ¬IsSeparable K x
g : K[X]
hg₁ : g.Separable
m : ℕ
hg₂ : (expand K (p ^ m)) g = minpoly K x
⊢ ↑(finrank (↥K⟮x⟯) L) * -(minpoly K x).nextCoeff = 0 x

Tactic:
cases m with
    | zero =>
      obtain rfl : g = minpoly K x := by simpa using hg₂
      cases hx hg₁
    | succ n =>
      rw [nextCoeff, if_neg, ← hg₂, coeff_expand (by positivity),
        if_neg, neg_zero, mul_zero, LinearMap.zero_apply]
      · rw [natDegree_expand]
        intro h
        have := Nat.dvd_sub (dvd_mul_left (p ^ (n + 1)) g.natDegree) h
        rw [tsub_tsub_cancel_of_le, Nat.dvd_one] at this
        · obtain rfl : g = minpoly K x := by simpa [this] using hg₂
          cases hx hg₁
        · rw [Nat.one_le_iff_ne_zero]
          have : g.natDegree ≠ 0 := fun e ↦ by
            have := congr(natDegree $hg₂)
            rw [natDegree_expand, e, zero_mul] at this
            exact (minpoly.natDegree_pos (IsIntegral.isIntegral x)).ne this
          positivity
      · exact (minpoly.natDegree_pos (IsIntegral.isIntegral x)).ne'

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

Goal state before:
pp: G : Type u_1
K : Type u_3
L : Type u_4
inst✝⁵ : Group G
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : MulSemiringAction G L
F : IntermediateField K L
hGKL : IsGaloisGroup G K L
inst✝ : Finite G
⊢ FixedPoints.intermediateField ↥(fixingSubgroup G ↑F) = F

Tactic:
by
  rw [← ofDual_intermediateFieldEquivSubgroup_apply, ← intermediateFieldEquivSubgroup_symm_apply,
    OrderIso.symm_apply_apply]

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

Goal state before:
pp: case inr
m : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ 2 * m ^ 2
hpp : p ∣ (m ^ 2).natAbs
⊢ p ∣ m.natAbs

Tactic:
rw [sq, Int.natAbs_mul] at hpp

Goal state after:
case inr
m : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ 2 * m ^ 2
hpp : p ∣ m.natAbs * m.natAbs
⊢ p ∣ m.natAbs
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:
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:
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: case e'_3
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' : IsLocallyClosed Z
i : ι
x : X
hx : x ∈ Z
hx' : x ∈ ↑(U i)
y : ↥(U i)
hy : y ∈ Subtype.val ⁻¹' Z
hy' : y ∈ closedPoints ↥(U i)
j : ι
h : ↑y ∉ U j
⊢ Subtype.val ⁻¹' {↑y} = ∅

Tactic:
Set.eq_empty_iff_forall_notMem

Goal state after:
case e'_3
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' : IsLocallyClosed Z
i : ι
x : X
hx : x ∈ Z
hx' : x ∈ ↑(U i)
y : ↥(U i)
hy : y ∈ Subtype.val ⁻¹' Z
hy' : y ∈ closedPoints ↥(U i)
j : ι
h : ↑y ∉ U j
⊢ ∀ (x : ↥(U j)), x ∉ Subtype.val ⁻¹' {↑y}
Module: Mathlib.RingTheory.LocalRing.Length

Goal state before:
pp: A : Type u_1
B : Type u_2
M : Type u_3
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : IsLocalRing A
inst✝⁶ : IsLocalRing B
inst✝⁵ : Algebra A B
inst✝⁴ : IsLocalHom (algebraMap A B)
inst✝³ : AddCommGroup M
inst✝² : Module A M
inst✝¹ : Module B M
inst✝ : IsScalarTower A B M
h : IsFiniteLength B M
s : CompositionSeries (Submodule B M)
hs_bot : RelSeries.head s = ⊥
hs_top : RelSeries.last s = ⊤
this : ∀ (k : Fin (s.length + 1)), length A ↥(s.toFun k) = ↑↑k * length (ResidueField A) (ResidueField B)
⊢ length A M = ↑s.length * length (ResidueField A) (ResidueField B)

Tactic:
by
      rw [← Fin.val_last s.length, ← this, ← RelSeries.last, hs_top]
      exact length_top.symm

Goal state after: