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

Goal state before:
pp: case refine_5
α : Type u_1
M : Matroid α
ι : Type u_2
C₀ : Set α
hC₀ : M.IsCircuit C₀
x : ι → α
C : ι → Set α
z : α
hC : ∀ (i : ι), M.IsCircuit (C i)
h_mem_C₀ : ∀ (i : ι), x i ∈ C₀
h_mem : ∀ (i : ι), x i ∈ C i
h_unique : ∀ ⦃i i' : ι⦄, x i ∈ C i' → i = i'
hzC₀ : z ∈ C₀
hzC : ∀ (i : ι), z ∉ C i
C' : Set α
hC'ss : C' ⊆ C₀ \ range x ∪ ⋃ i, C i \ {x i}
hC' : M.IsCircuit C'
hzC' : z ∈ C'
i j : ι
he : x j ∈ C i \ {x i}
⊢ False

Tactic:
obtain rfl : j = i := h_unique he.1

Goal state after:
case refine_5
α : Type u_1
M : Matroid α
ι : Type u_2
C₀ : Set α
hC₀ : M.IsCircuit C₀
x : ι → α
C : ι → Set α
z : α
hC : ∀ (i : ι), M.IsCircuit (C i)
h_mem_C₀ : ∀ (i : ι), x i ∈ C₀
h_mem : ∀ (i : ι), x i ∈ C i
h_unique : ∀ ⦃i i' : ι⦄, x i ∈ C i' → i = i'
hzC₀ : z ∈ C₀
hzC : ∀ (i : ι), z ∉ C i
C' : Set α
hC'ss : C' ⊆ C₀ \ range x ∪ ⋃ i, C i \ {x i}
hC' : M.IsCircuit C'
hzC' : z ∈ C'
j : ι
he : x j ∈ C j \ {x j}
⊢ False
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
C : Set α
hC : M.IsCircuit C
⊢ M.eRk C + 1 = C.encard

Tactic:
obtain ⟨I, hI⟩ := M.exists_isBasis C

Goal state after:
α : Type u_1
M : Matroid α
C : Set α
hC : M.IsCircuit C
I : Set α
hI : M.IsBasis I C
⊢ M.eRk C + 1 = C.encard
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.loops = M₂.loops
hc : M₁.coloops = M₂.coloops
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.loops ∪ M₁.coloops) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
⊢ M₁.Indep I ↔ M₂.Indep I

Tactic:
← sdiff_coloops_indep_iff,

Goal state after:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.loops = M₂.loops
hc : M₁.coloops = M₂.coloops
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.loops ∪ M₁.coloops) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
⊢ M₁.Indep (I \ M₁.coloops) ↔ M₂.Indep I
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: case inr
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.loops = M₂.loops
hc : M₁.coloops = M₂.coloops
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.loops ∪ M₁.coloops) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
hndj : ¬Disjoint I M₁.loops
e : α
heI : e ∈ I
hel : M₂.IsLoop e
⊢ ¬M₂.Indep (I \ M₁.coloops)

Tactic:
rw [hc]

Goal state after:
case inr
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.loops = M₂.loops
hc : M₁.coloops = M₂.coloops
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.loops ∪ M₁.coloops) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
hndj : ¬Disjoint I M₁.loops
e : α
heI : e ∈ I
hel : M₂.IsLoop e
⊢ ¬M₂.Indep (I \ M₂.coloops)
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
this : (∃ x ∈ M.E, M.IsLoop x) ↔ ∃ x, M.IsCircuit x ∧ x.Subsingleton
⊢ (∀ e ∈ M.E, ¬M.IsLoop e) ↔ ∀ (C : Set α), M.IsCircuit C → C.Nontrivial

Tactic:
contrapose!

Goal state after:
α : Type u_1
M : Matroid α
this : (∃ x ∈ M.E, M.IsLoop x) ↔ ∃ x, M.IsCircuit x ∧ x.Subsingleton
⊢ (∃ e ∈ M.E, M.IsLoop e) ↔ ∃ C, M.IsCircuit C ∧ C.Subsingleton
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 ι
ind : AlgebraicIndependent R fun i ↦ x ↑i
H :
  ∀ (t : Set ι),
    t.Finite → (AlgebraicIndependent R fun i ↦ x ↑i) → ∀ i ∉ s, i ∉ t → Transcendental (↥(adjoin R (x '' t))) (x i)
⊢ AlgebraicIndependent R x

Tactic:
classical
  refine algebraicIndependent_of_finite_type fun t hfin ↦ ?_
  suffices AlgebraicIndependent R fun i : ↥(t ∩ s ∪ t \ s) ↦ x i from
    this.comp (Equiv.setCongr (t.inter_union_sdiff s).symm) (Equiv.injective _)
  refine hfin.sdiff.induction_on_subset _ (ind.comp (inclusion <| by simp) (inclusion_injective _))
    fun {a u} ha hu ha' h ↦ ?_
  have : a ∉ t ∩ s ∪ u := (·.elim (ha.2 ·.2) ha')
  convert!
    (((image_eq_range .. ▸ h.option_iff_transcendental <| x a).2 <|
              H _ (hfin.subset (union_subset inter_subset_left <| hu.trans sdiff_subset)) h a ha.2
                this).comp
          _ (subtypeInsertEquivOption this).injective).comp
      (Equiv.setCongr union_insert) (Equiv.injective _) with
    x
  by_cases h : ↑x = a <;> simp [h, Set.subtypeInsertEquivOption]

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:
convert! ← iff_adjoin_image _; apply compl_compl

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

Goal state before:
pp: ι : 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✝³ : Nontrivial R
inst✝² : NoZeroDivisors S
inst✝¹ : Algebra.IsAlgebraic S A
inst✝ : FaithfulSMul S A
x : ι → S
hx : IsTranscendenceBasis R x
f : S →ₐ[R] A := IsScalarTower.toAlgHom R S A
Rx : Subalgebra R S := adjoin R (range x)
e : ↥Rx ≃ₐ[R] ↥(Subalgebra.map f Rx) := Rx.equivMapOfInjective f ⋯
this✝¹ : Algebra ↥Rx ↥(Subalgebra.map f Rx) := e.toRingEquiv.toRingHom.toAlgebra
this✝ : IsScalarTower (↥Rx) (↥(Subalgebra.map f Rx)) A
this : Algebra.IsAlgebraic (↥Rx) S
⊢ Algebra.IsAlgebraic (↥(Subalgebra.map f Rx)) A

Tactic:
have : Algebra.IsAlgebraic Rx A := .trans _ S _

Goal state after:
ι : 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✝³ : Nontrivial R
inst✝² : NoZeroDivisors S
inst✝¹ : Algebra.IsAlgebraic S A
inst✝ : FaithfulSMul S A
x : ι → S
hx : IsTranscendenceBasis R x
f : S →ₐ[R] A := IsScalarTower.toAlgHom R S A
Rx : Subalgebra R S := adjoin R (range x)
e : ↥Rx ≃ₐ[R] ↥(Subalgebra.map f Rx) := Rx.equivMapOfInjective f ⋯
this✝² : Algebra ↥Rx ↥(Subalgebra.map f Rx) := e.toRingEquiv.toRingHom.toAlgebra
this✝¹ : IsScalarTower (↥Rx) (↥(Subalgebra.map f Rx)) A
this✝ : Algebra.IsAlgebraic (↥Rx) S
this : Algebra.IsAlgebraic (↥Rx) A
⊢ Algebra.IsAlgebraic (↥(Subalgebra.map f Rx)) A
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : Subsingleton A
s t : Set A
this : Subsingleton R
⊢ Maximal (fun A_1 ↦ AlgebraicIndepOn R _root_.id A_1 ∧ A_1 ⊆ t) s ∧ t ⊆ (matroid R A).E ↔ s = t

Tactic:
of_subsingleton,

Goal state after:
R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : Subsingleton A
s t : Set A
this : Subsingleton R
⊢ Maximal (fun A_1 ↦ True ∧ A_1 ⊆ t) s ∧ t ⊆ (matroid R A).E ↔ s = t
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors A
ι : Type w
x : ι → A
hx : IsTranscendenceBasis R x
⊢ lift.{w, w} #ι = trdeg R A

Tactic:
lift_cardinalMk_eq_trdeg hx,

Goal state after:
R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors A
ι : Type w
x : ι → A
hx : IsTranscendenceBasis R x
⊢ lift.{w, w} (trdeg R A) = trdeg R A
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
f : F[X]
h : f.natDegree ≠ 0
⊢ f.natSepDegree ≠ 0

Tactic:
by
  rw [natSepDegree, ne_eq, Finset.card_eq_zero, ← ne_eq, ← Finset.nonempty_iff_ne_empty]
  use rootOfSplits (SplittingField.splits f) (degree_ne_of_natDegree_ne (by rwa [natDegree_map]))
  classical
  rw [Multiset.mem_toFinset, mem_aroots]
  exact ⟨ne_of_apply_ne _ h, by simp only [← eval_map_algebraMap, eval_rootOfSplits]⟩

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝¹ : Field F
f g : F[X]
q : ℕ
inst✝ : ExpChar F q
h1 : g.Separable
m : ℕ
h2 : (expand F (q ^ m)) g = f
⊢ f.natSepDegree = g.natDegree

Tactic:
← h2,

Goal state after:
F : Type u
inst✝¹ : Field F
f g : F[X]
q : ℕ
inst✝ : ExpChar F q
h1 : g.Separable
m : ℕ
h2 : (expand F (q ^ m)) g = f
⊢ ((expand F (q ^ m)) g).natSepDegree = g.natDegree
Module: Mathlib.FieldTheory.Galois.Basic

Goal state before:
pp: K : Type u_3
L : Type u_4
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
E : IntermediateField K L
inst✝ : Normal K ↥E
⊢ (restrictNormalHom ↥E).ker = E.fixingSubgroup

Tactic:
by
  simp only [Subgroup.ext_iff, MonoidHom.mem_ker, AlgEquiv.ext_iff, one_apply, Subtype.ext_iff,
    restrictNormalHom_apply, Subtype.forall, mem_fixingSubgroup_iff, implies_true]

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

Goal state before:
pp: case hmul
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_3
inst✝² : IsTopologicalRing R
inst✝¹ : TopologicalSpace M
inst✝ : IsTopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : (𝓝 0).HasBasis p b
hsmul : ∀ {i : ι}, p i → ∃ V ∈ 𝓝 0, ∃ j, p j ∧ V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ j, p j ∧ MapsTo (fun x ↦ x₀ • x) (b j) (b i)
hsmul_right : ∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
⊢ Tendsto (fun p ↦ p.1 • p.2) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0)

Tactic:
rw [h.tendsto_right_iff]

Goal state after:
case hmul
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_3
inst✝² : IsTopologicalRing R
inst✝¹ : TopologicalSpace M
inst✝ : IsTopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : (𝓝 0).HasBasis p b
hsmul : ∀ {i : ι}, p i → ∃ V ∈ 𝓝 0, ∃ j, p j ∧ V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ j, p j ∧ MapsTo (fun x ↦ x₀ • x) (b j) (b i)
hsmul_right : ∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
⊢ ∀ (i : ι), p i → ∀ᶠ (x : R × M) in 𝓝 0 ×ˢ 𝓝 0, x.1 • x.2 ∈ b i
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: case hmulleft
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_3
inst✝² : IsTopologicalRing R
inst✝¹ : TopologicalSpace M
inst✝ : IsTopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : (𝓝 0).HasBasis p b
hsmul : ∀ {i : ι}, p i → ∃ V ∈ 𝓝 0, ∃ j, p j ∧ V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ j, p j ∧ MapsTo (fun x ↦ x₀ • x) (b j) (b i)
hsmul_right : ∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
m₀ : M
⊢ Tendsto (fun a ↦ a • m₀) (𝓝 0) (𝓝 0)

Tactic:
rw [h.tendsto_right_iff]

Goal state after:
case hmulleft
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_3
inst✝² : IsTopologicalRing R
inst✝¹ : TopologicalSpace M
inst✝ : IsTopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : (𝓝 0).HasBasis p b
hsmul : ∀ {i : ι}, p i → ∃ V ∈ 𝓝 0, ∃ j, p j ∧ V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ j, p j ∧ MapsTo (fun x ↦ x₀ • x) (b j) (b i)
hsmul_right : ∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
m₀ : M
⊢ ∀ (i : ι), p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: case hmulright
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_3
inst✝² : IsTopologicalRing R
inst✝¹ : TopologicalSpace M
inst✝ : IsTopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : (𝓝 0).HasBasis p b
hsmul : ∀ {i : ι}, p i → ∃ V ∈ 𝓝 0, ∃ j, p j ∧ V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ j, p j ∧ MapsTo (fun x ↦ x₀ • x) (b j) (b i)
hsmul_right : ∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
x₀ : R
⊢ Tendsto (fun m ↦ x₀ • m) (𝓝 0) (𝓝 0)

Tactic:
rw [h.tendsto_right_iff]

Goal state after:
case hmulright
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_3
inst✝² : IsTopologicalRing R
inst✝¹ : TopologicalSpace M
inst✝ : IsTopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : (𝓝 0).HasBasis p b
hsmul : ∀ {i : ι}, p i → ∃ V ∈ 𝓝 0, ∃ j, p j ∧ V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ j, p j ∧ MapsTo (fun x ↦ x₀ • x) (b j) (b i)
hsmul_right : ∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
x₀ : R
⊢ ∀ (i : ι), p i → ∀ᶠ (x : M) in 𝓝 0, x₀ • x ∈ b i
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
⊢ ∃ U, IsClopen U ∧ σ ∈ U ∧ τ ∈ Uᶜ

Tactic:
let E := IntermediateField.adjoin K ({x} : Set L)

Goal state after:
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⟯
⊢ ∃ U, IsClopen U ∧ σ ∈ U ∧ τ ∈ Uᶜ
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
L : IntermediateField k K
inst✝ : IsGalois k K
h : L.fixingSubgroup.Normal
g : (x : K) → Subgroup Gal(↥(adjoin k {x}).toIntermediateField/k) :=
  fun x ↦ Subgroup.map (restrictNormalHom ↥(adjoin k {x}).toIntermediateField) L.fixingSubgroup
⊢ IsGalois k ↥L

Tactic:
let f (x : L) : IntermediateField k K := IntermediateField.lift <|
      IntermediateField.fixedField <| g x.1

Goal state after:
case refine_1
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
h : L.fixingSubgroup.Normal
g : (x : K) → Subgroup Gal(↥(adjoin k {x}).toIntermediateField/k) :=
  fun x ↦ Subgroup.map (restrictNormalHom ↥(adjoin k {x}).toIntermediateField) L.fixingSubgroup
f : ↥L → IntermediateField k K := fun x ↦ IntermediateField.lift (IntermediateField.fixedField (g ↑x))
⊢ IsGalois k ↥L
Module: Mathlib.RingTheory.Trace.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
ι : Type w
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι R S
i j : ι
⊢ (LinearMap.BilinForm.toMatrix b) (traceForm R S) i j = (trace R S) (b i * b j)

Tactic:
LinearMap.BilinForm.toMatrix_apply,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
ι : Type w
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι R S
i j : ι
⊢ ((traceForm R S) (b i)) (b j) = (trace R S) (b i * b j)
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
⊢ (X ^ q ^ m - C y).natDegree = q ^ m

Tactic:
natDegree_sub_C,

Goal state after:
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
⊢ (X ^ q ^ m).natDegree = q ^ m
Module: Mathlib.RingTheory.DedekindDomain.IntegralClosure

Goal state before:
pp: case refine_2
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
z : L
m : ↥A⁰
hm : IsIntegral A (m • z)
x : C
hx : (algebraMap C L) x = m • z
⊢ z * (algebraMap C L) ↑(x, ⟨(algebraMap A C) ↑m, ⋯⟩).2 = (algebraMap C L) (x, ⟨(algebraMap A C) ↑m, ⋯⟩).1

Tactic:
rw [Subtype.coe_mk, ← IsScalarTower.algebraMap_apply, hx, mul_comm, Submonoid.smul_def,
      smul_def]

Goal state after:
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)
⊢ Function.Injective ⇑(algebraMap A L)

Tactic:
IsScalarTower.algebraMap_eq A K L

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)
⊢ Function.Injective ⇑((algebraMap K L).comp (algebraMap A K))
Module: Mathlib.NumberTheory.NumberField.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
x : 𝓞 K
P : Polynomial ℤ
hPm : P.Monic
hP : Polynomial.eval₂ (algebraMap ℤ K) ((algebraMap (𝓞 K) K) x) P = 0
⊢ Polynomial.eval₂ (algebraMap ℤ (𝓞 K)) x P = 0

Tactic:
IsScalarTower.algebraMap_eq (S := 𝓞 K),

Goal state after:
K : Type u_1
inst✝ : Field K
x : 𝓞 K
P : Polynomial ℤ
hPm : P.Monic
hP : Polynomial.eval₂ ((algebraMap (𝓞 K) K).comp (algebraMap ℤ (𝓞 K))) ((algebraMap (𝓞 K) K) x) P = 0
⊢ Polynomial.eval₂ (algebraMap ℤ (𝓞 K)) x P = 0
Module: Mathlib.RingTheory.IsGaloisGroup.Basic

Goal state before:
pp: G : Type u_1
inst✝⁹ : Group G
H : Subgroup G
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁸ : CommSemiring A
inst✝⁷ : Semiring C
inst✝⁶ : Algebra A C
inst✝⁵ : MulSemiringAction G C
N : Subgroup G
inst✝⁴ : CommSemiring B
inst✝³ : Algebra B C
inst✝² : FaithfulSMul B C
inst✝¹ : IsGaloisGroup (↥N) B C
inst✝ : N.Normal
this : MulSemiringAction G B := ⋯
q : G ⧸ N
x : B
g₁ g₂ : G
h : (QuotientGroup.leftRel N) g₁ g₂
⊢ (algebraMap B C) (g₁ • x) = (algebraMap B C) (g₂ • x)

Tactic:
algebraMap.smul',

Goal state after:
G : Type u_1
inst✝⁹ : Group G
H : Subgroup G
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁸ : CommSemiring A
inst✝⁷ : Semiring C
inst✝⁶ : Algebra A C
inst✝⁵ : MulSemiringAction G C
N : Subgroup G
inst✝⁴ : CommSemiring B
inst✝³ : Algebra B C
inst✝² : FaithfulSMul B C
inst✝¹ : IsGaloisGroup (↥N) B C
inst✝ : N.Normal
this : MulSemiringAction G B := mulSemiringActionOfNormal G B C N
q : G ⧸ N
x : B
g₁ g₂ : G
h : (QuotientGroup.leftRel N) g₁ g₂
⊢ g₁ • (algebraMap B C) x = (algebraMap B C) (g₂ • x)
Module: Mathlib.RingTheory.IsGaloisGroup.Basic

Goal state before:
pp: G : Type u_1
inst✝⁹ : Group G
H : Subgroup G
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁸ : CommSemiring A
inst✝⁷ : Semiring C
inst✝⁶ : Algebra A C
inst✝⁵ : MulSemiringAction G C
N : Subgroup G
inst✝⁴ : CommSemiring B
inst✝³ : Algebra B C
inst✝² : FaithfulSMul B C
inst✝¹ : IsGaloisGroup (↥N) B C
inst✝ : N.Normal
this : MulSemiringAction G B := mulSemiringActionOfNormal G B C N
q : G ⧸ N
x : B
g₁ g₂ : G
h : (QuotientGroup.leftRel N) g₁ g₂
⊢ g₁ • (algebraMap B C) x = (algebraMap B C) (g₂ • x)

Tactic:
algebraMap.smul',

Goal state after:
G : Type u_1
inst✝⁹ : Group G
H : Subgroup G
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁸ : CommSemiring A
inst✝⁷ : Semiring C
inst✝⁶ : Algebra A C
inst✝⁵ : MulSemiringAction G C
N : Subgroup G
inst✝⁴ : CommSemiring B
inst✝³ : Algebra B C
inst✝² : FaithfulSMul B C
inst✝¹ : IsGaloisGroup (↥N) B C
inst✝ : N.Normal
this : MulSemiringAction G B := mulSemiringActionOfNormal G B C N
q : G ⧸ N
x : B
g₁ g₂ : G
h : (QuotientGroup.leftRel N) g₁ g₂
⊢ g₁ • (algebraMap B C) x = g₂ • (algebraMap B C) x
Module: Mathlib.RingTheory.IsGaloisGroup.Basic

Goal state before:
pp: G : Type u_1
inst✝⁹ : Group G
B : Type u_3
C : Type u_4
inst✝⁸ : Semiring C
inst✝⁷ : MulSemiringAction G C
N : Subgroup G
inst✝⁶ : CommSemiring B
inst✝⁵ : Algebra B C
inst✝⁴ : FaithfulSMul B C
inst✝³ : MulSemiringAction G B
inst✝² : SMulDistribClass G B C
inst✝¹ : IsGaloisGroup (↥N) B C
inst✝ : N.Normal
g : G
b : B
this : MulSemiringAction G B := mulSemiringActionOfNormal G B C N
⊢ (algebraMap B C) (g • b) = (algebraMap B C) (g • b)

Tactic:
algebraMap.smul',

Goal state after:
G : Type u_1
inst✝⁹ : Group G
B : Type u_3
C : Type u_4
inst✝⁸ : Semiring C
inst✝⁷ : MulSemiringAction G C
N : Subgroup G
inst✝⁶ : CommSemiring B
inst✝⁵ : Algebra B C
inst✝⁴ : FaithfulSMul B C
inst✝³ : MulSemiringAction G B
inst✝² : SMulDistribClass G B C
inst✝¹ : IsGaloisGroup (↥N) B C
inst✝ : N.Normal
g : G
b : B
this : MulSemiringAction G B := mulSemiringActionOfNormal G B C N
⊢ g • (algebraMap B C) b = (algebraMap B C) (g • b)
Module: Mathlib.RingTheory.Invariant.Basic

Goal state before:
pp: B : Type u_2
inst✝⁴ : CommRing B
G : Type u_3
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : MulSemiringAction G B
Q : Ideal B
inst✝ : Q.IsPrime
val✝ : Fintype G
P : Ideal B := {g | g • Q ≠ Q}.inf fun g ↦ g • Q
h1 : ¬P ≤ Q
⊢ ∃ a b,
    (∀ (g : G), g • a = a) ∧
      a ∉ Q ∧ ∀ (g : G), (algebraMap B (B ⧸ Q)) (g • b) = (algebraMap B (B ⧸ Q)) (if g • Q = Q then a else 0)

Tactic:
obtain ⟨b, hbP, hbQ⟩ := SetLike.not_le_iff_exists.mp h1

Goal state after:
B : Type u_2
inst✝⁴ : CommRing B
G : Type u_3
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : MulSemiringAction G B
Q : Ideal B
inst✝ : Q.IsPrime
val✝ : Fintype G
P : Ideal B := {g | g • Q ≠ Q}.inf fun g ↦ g • Q
h1 : ¬P ≤ Q
b : B
hbP : b ∈ P
hbQ : b ∉ Q
⊢ ∃ a b,
    (∀ (g : G), g • a = a) ∧
      a ∉ Q ∧ ∀ (g : G), (algebraMap B (B ⧸ Q)) (g • b) = (algebraMap B (B ⧸ Q)) (if g • Q = Q then a else 0)
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
L : Type u_5
inst✝⁶ : Field L
F : Type u_6
inst✝⁵ : Field F
inst✝⁴ : Algebra R L
inst✝³ : Algebra L F
inst✝² : Algebra R F
inst✝¹ : IsScalarTower R L F
inst✝ : FiniteDimensional L F
x : F
hx : IsIntegral R x
⊢ IsIntegral R ((trace L F) x)

Tactic:
by
  have hx' : IsIntegral L x := hx.tower_top
  rw [← isIntegral_algebraMap_iff (algebraMap L (AlgebraicClosure F)).injective, trace_eq_sum_roots]
  · refine (IsIntegral.multiset_sum ?_).nsmul _
    intro y hy
    rw [mem_roots_map (minpoly.ne_zero hx')] at hy
    use minpoly R x, minpoly.monic hx
    rw [← aeval_def] at hy ⊢
    exact minpoly.aeval_of_isScalarTower R x y hy
  · apply IsAlgClosed.splits

Goal state after: