mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : ⋃ i ∈ ∅, g i • ↑H = Set.univ
hind : H.index = s.card
h : s = ∅
⊢ False

Tactic:
← Finset.set_biUnion_coe,

Goal state after:
G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : ⋃ x ∈ ↑∅, g x • ↑H = Set.univ
hind : H.index = s.card
h : s = ∅
⊢ False
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: G : Type u_1
inst✝ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
hcovers : ⋃ i ∈ ∅, g i • ↑(H i) = Set.univ
⊢ False

Tactic:
← Finset.set_biUnion_coe,

Goal state after:
G : Type u_1
inst✝ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
hcovers : ⋃ x ∈ ↑∅, g x • ↑(H x) = Set.univ
⊢ False
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: case one
K : Type u
inst✝ : Field K
hn : Odd 1
a : K
ha : ∀ (p : ℕ), Nat.Prime p → p ∣ 1 → ∀ (b : K), b ^ p ≠ a
⊢ Irreducible (X ^ 1 - C a)

Tactic:
| one =>

Goal state after:
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: case pos
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
inst✝ : DecidablePred FiniteIndex
D : Subgroup G := ⨅ k ∈ {i ∈ s | (H i).FiniteIndex}, H k
hD : D.FiniteIndex
hD_le : ∀ {i : ι}, i ∈ s → (H i).FiniteIndex → D ≤ H i
t : (i : ι) → i ∈ s → (H i).FiniteIndex → Finset ↥(H i)
ht :
  ∀ (i : ι) (hi : i ∈ s) (hfi : (H i).FiniteIndex),
    IsComplement ↑(t i hi hfi) ↑(D.subgroupOf (H i)) ∧ ⋃ g ∈ t i hi hfi, ↑g • ↑D = ↑(H i)
κ : Type (max u_2 u_1) := (i : ↥s) × ↥(if h : (H ↑i).FiniteIndex then t ↑i ⋯ h else {1})
f : κ → G := fun k ↦ g ↑k.fst * ↑↑k.snd
K : κ → Subgroup G := fun k ↦ if (H ↑k.fst).FiniteIndex then D else H ↑k.fst
k : κ
hkfi : (H ↑k.fst).FiniteIndex
hk : K k = D
hcovers' : ⋃ i ∈ {x | K x = D}, f i • ↑D = Set.univ
hHD : ∀ (i : ι), ¬(H i).FiniteIndex → H i ≠ D
i : ↥s
x✝ : i ∈ s.attach
hfi : (H ↑i).FiniteIndex
⊢ ∑ s_1, ↑(if K ⟨i, s_1⟩ = D then 1 else 0) = ↑(D.relIndex (H ↑i)) * ↑(H ↑i).index * (↑(H ↑i).index)⁻¹

Tactic:
mul_inv_cancel_right₀ (Nat.cast_ne_zero.mpr hfi.index_ne_zero)

Goal state after:
case pos
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
inst✝ : DecidablePred FiniteIndex
D : Subgroup G := ⨅ k ∈ {i ∈ s | (H i).FiniteIndex}, H k
hD : D.FiniteIndex
hD_le : ∀ {i : ι}, i ∈ s → (H i).FiniteIndex → D ≤ H i
t : (i : ι) → i ∈ s → (H i).FiniteIndex → Finset ↥(H i)
ht :
  ∀ (i : ι) (hi : i ∈ s) (hfi : (H i).FiniteIndex),
    IsComplement ↑(t i hi hfi) ↑(D.subgroupOf (H i)) ∧ ⋃ g ∈ t i hi hfi, ↑g • ↑D = ↑(H i)
κ : Type (max u_2 u_1) := (i : ↥s) × ↥(if h : (H ↑i).FiniteIndex then t ↑i ⋯ h else {1})
f : κ → G := fun k ↦ g ↑k.fst * ↑↑k.snd
K : κ → Subgroup G := fun k ↦ if (H ↑k.fst).FiniteIndex then D else H ↑k.fst
k : κ
hkfi : (H ↑k.fst).FiniteIndex
hk : K k = D
hcovers' : ⋃ i ∈ {x | K x = D}, f i • ↑D = Set.univ
hHD : ∀ (i : ι), ¬(H i).FiniteIndex → H i ≠ D
i : ↥s
x✝ : i ∈ s.attach
hfi : (H ↑i).FiniteIndex
⊢ ∑ s_1, ↑(if K ⟨i, s_1⟩ = D then 1 else 0) = ↑(D.relIndex (H ↑i))
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: K : Type u
inst✝³ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ n - C a)
α : L
hα : α ^ n = (algebraMap K L) a
⊢ (AlgEquiv.ofBijective (liftAlgHom (X ^ n - C a) (Algebra.ofId K L) α ⋯) ⋯) (root (X ^ n - C a)) = α

Tactic:
AlgEquiv.coe_ofBijective,

Goal state after:
K : Type u
inst✝³ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ n - C a)
α : L
hα : α ^ n = (algebraMap K L) a
⊢ (liftAlgHom (X ^ n - C a) (Algebra.ofId K L) α ⋯) (root (X ^ n - C a)) = α
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: case refine_2
K : Type u
inst✝⁵ : Field K
L : Type u_1
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
inst✝¹ : IsGalois K L
inst✝ : IsCyclic Gal(L/K)
ζ : K
hζ : IsPrimitiveRoot ζ (finrank K L)
σ : Gal(L/K)
hσ : Function.Surjective fun x ↦ σ ^ x
hσ' : orderOf σ = Nat.card Gal(L/K)
this : (minpoly K σ.toLinearMap).IsRoot ζ
v : L
hv : End.HasEigenvector σ.toLinearMap ζ v
hv' : ∀ (n : ℕ), (σ ^ n) v = ζ ^ n • v
σ' : Gal(L/K)
⊢ σ' ∈ IsGalois.intermediateFieldEquivSubgroup K⟮v⟯ → σ' ∈ ⊤

Tactic:
hσ'

Goal state after:
case refine_2
K : Type u
inst✝⁵ : Field K
L : Type u_1
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
inst✝¹ : IsGalois K L
inst✝ : IsCyclic Gal(L/K)
ζ : K
hζ : IsPrimitiveRoot ζ (finrank K L)
σ : Gal(L/K)
hσ : Function.Surjective fun x ↦ σ ^ x
hσ'✝ : orderOf σ = Nat.card Gal(L/K)
this : (minpoly K σ.toLinearMap).IsRoot ζ
v : L
hv : End.HasEigenvector σ.toLinearMap ζ v
hv' : ∀ (n : ℕ), (σ ^ n) v = ζ ^ n • v
σ' : Gal(L/K)
hσ' : σ' ∈ IsGalois.intermediateFieldEquivSubgroup K⟮v⟯
⊢ σ' ∈ ⊤
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: case inr
G : Type u_1
inst✝ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
h : ∀ i ∈ s, (H i).FiniteIndex → s.card < (H i).index
hs : s.Nonempty
hs' : 0 < s.card
i : ι
hi : i ∈ s
hindex : (H i).index ≠ 0
⊢ (↑(H i).index)⁻¹ < (↑s.card)⁻¹

Tactic:
exact inv_strictAnti₀ (by exact_mod_cast hs') (by exact_mod_cast h i hi ⟨hindex⟩)

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

Goal state before:
pp: K : Type u_1
L : Type u_2
S : Type u_3
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Field S
inst✝³ : Algebra K L
inst✝² : Algebra K S
inst✝¹ : Algebra L S
inst✝ : IsScalarTower K L S
c : ConjRootClass K L
⊢ - -c = c

Tactic:
induction c

Goal state after:
case h
K : Type u_1
L : Type u_2
S : Type u_3
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Field S
inst✝³ : Algebra K L
inst✝² : Algebra K S
inst✝¹ : Algebra L S
inst✝ : IsScalarTower K L S
x✝ : L
⊢ - -mk K x✝ = mk K x✝
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
c d : ConjRootClass K L
⊢ c.minpoly = d.minpoly ↔ c = d

Tactic:
induction c

Goal state after:
case h
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
d : ConjRootClass K L
x✝ : L
⊢ (mk K x✝).minpoly = d.minpoly ↔ mk K x✝ = d
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
n : Normal K L
c : ConjRootClass K L
⊢ (map (algebraMap K L) c.minpoly).Splits

Tactic:
induction c

Goal state after:
case h
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
n : Normal K L
x✝ : L
⊢ (map (algebraMap K L) (mk K x✝).minpoly).Splits
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsAlgebraic K L
c : ConjRootClass K L
⊢ c.minpoly.Monic

Tactic:
induction c

Goal state after:
case h
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsAlgebraic K L
x✝ : L
⊢ (mk K x✝).minpoly.Monic
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsAlgebraic K L
c : ConjRootClass K L
⊢ Irreducible c.minpoly

Tactic:
induction c

Goal state after:
case h
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsAlgebraic K L
x✝ : L
⊢ Irreducible (mk K x✝).minpoly
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsAlgebraic K L
x : L
c : ConjRootClass K L
⊢ (aeval x) c.minpoly = 0 ↔ mk K x = c

Tactic:
induction c

Goal state after:
case h
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsAlgebraic K L
x x✝ : L
⊢ (aeval x) (mk K x✝).minpoly = 0 ↔ mk K x = mk K x✝
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsSeparable K L
c : ConjRootClass K L
⊢ c.minpoly.Separable

Tactic:
induction c

Goal state after:
case h
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsSeparable K L
x✝ : L
⊢ (mk K x✝).minpoly.Separable
Module: Mathlib.FieldTheory.NormalizedTrace

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : CharZero F
inst✝ : Algebra.IsIntegral F K
a b : K
E : IntermediateField F K := F⟮a⟯ ⊔ F⟮b⟯
this✝ : FiniteDimensional F ↥F⟮a⟯
this : FiniteDimensional F ↥F⟮b⟯
ha : a ∈ E
hb : b ∈ E
hab : a + b ∈ E
⊢ normalizedTraceAux F K (a + b) = normalizedTraceAux F K a + normalizedTraceAux F K b

Tactic:
let a' : E := ⟨a, ha⟩

Goal state after:
F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : CharZero F
inst✝ : Algebra.IsIntegral F K
a b : K
E : IntermediateField F K := F⟮a⟯ ⊔ F⟮b⟯
this✝ : FiniteDimensional F ↥F⟮a⟯
this : FiniteDimensional F ↥F⟮b⟯
ha : a ∈ E
hb : b ∈ E
hab : a + b ∈ E
a' : ↥E := ⟨a, ha⟩
⊢ normalizedTraceAux F K (a + b) = normalizedTraceAux F K a + normalizedTraceAux F K b
Module: Mathlib.FieldTheory.NormalizedTrace

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : CharZero F
inst✝ : Algebra.IsIntegral F K
a b : K
E : IntermediateField F K := F⟮a⟯ ⊔ F⟮b⟯
this✝ : FiniteDimensional F ↥F⟮a⟯
this : FiniteDimensional F ↥F⟮b⟯
ha : a ∈ E
hb : b ∈ E
hab : a + b ∈ E
a' : ↥E := ⟨a, ha⟩
⊢ normalizedTraceAux F K (a + b) = normalizedTraceAux F K a + normalizedTraceAux F K b

Tactic:
let b' : E := ⟨b, hb⟩

Goal state after:
F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : CharZero F
inst✝ : Algebra.IsIntegral F K
a b : K
E : IntermediateField F K := F⟮a⟯ ⊔ F⟮b⟯
this✝ : FiniteDimensional F ↥F⟮a⟯
this : FiniteDimensional F ↥F⟮b⟯
ha : a ∈ E
hb : b ∈ E
hab : a + b ∈ E
a' : ↥E := ⟨a, ha⟩
b' : ↥E := ⟨b, hb⟩
⊢ normalizedTraceAux F K (a + b) = normalizedTraceAux F K a + normalizedTraceAux F K b
Module: Mathlib.FieldTheory.NormalizedTrace

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : CharZero F
inst✝ : Algebra.IsIntegral F K
m : F
a : K
E : IntermediateField F K := F⟮a⟯
this : FiniteDimensional F ↥F⟮a⟯
ha : a ∈ E
hma : m • a ∈ E
⊢ normalizedTraceAux F K (m • a) = m • normalizedTraceAux F K a

Tactic:
let a' : E := ⟨a, ha⟩

Goal state after:
F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : CharZero F
inst✝ : Algebra.IsIntegral F K
m : F
a : K
E : IntermediateField F K := F⟮a⟯
this : FiniteDimensional F ↥F⟮a⟯
ha : a ∈ E
hma : m • a ∈ E
a' : ↥E := ⟨a, ha⟩
⊢ normalizedTraceAux F K (m • a) = m • normalizedTraceAux F K a
Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure

Goal state before:
pp: F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
L : IntermediateField F E
h : ∀ (x : ↥L), ∃ n, x ^ ringExpChar F ^ n ∈ (algebraMap F ↥L).range
x : E
hx : x ∈ L
⊢ x ∈ perfectClosure F E

Tactic:
obtain ⟨n, y, hy⟩ := h ⟨x, hx⟩

Goal state after:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
L : IntermediateField F E
h : ∀ (x : ↥L), ∃ n, x ^ ringExpChar F ^ n ∈ (algebraMap F ↥L).range
x : E
hx : x ∈ L
n : ℕ
y : F
hy : (algebraMap F ↥L) y = ⟨x, hx⟩ ^ ringExpChar F ^ n
⊢ x ∈ perfectClosure F E
Module: Mathlib.FieldTheory.LinearDisjoint

Goal state before:
pp: F : Type u
inst✝⁶ : Field F
A : Type v
inst✝⁵ : Field A
B : Type w
inst✝⁴ : Field B
inst✝³ : Algebra F A
inst✝² : Algebra F B
H : IsField (A ⊗[F] B)
K : Type u_1
inst✝¹ : Field K
inst✝ : Algebra F K
fa : A →ₐ[F] K
fb : B →ₐ[F] K
⊢ fa.fieldRange.LinearDisjoint ↥fb.fieldRange

Tactic:
linearDisjoint_iff'

Goal state after:
F : Type u
inst✝⁶ : Field F
A : Type v
inst✝⁵ : Field A
B : Type w
inst✝⁴ : Field B
inst✝³ : Algebra F A
inst✝² : Algebra F B
H : IsField (A ⊗[F] B)
K : Type u_1
inst✝¹ : Field K
inst✝ : Algebra F K
fa : A →ₐ[F] K
fb : B →ₐ[F] K
⊢ fa.fieldRange.LinearDisjoint fb.fieldRange.toSubalgebra
Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure

Goal state before:
pp: case refine_1
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
S : Set E
inst✝¹ : Algebra.IsSeparable F ↥(adjoin F S)
q : ℕ
inst✝ : ExpChar F q
n : ℕ
M : IntermediateField F E := adjoin F ((fun x ↦ x ^ q ^ n) '' S)
this : ExpChar (↥M) q
x : E
hx : x ∈ S
⊢ x ∈ ↑M

Tactic:
have : Algebra.IsSeparable M M⟮x⟯ :=
      (isSeparable_adjoin_simple_iff_isSeparable M E).2 <|
        ((isSeparable_adjoin_iff_isSeparable F E).1 inferInstance x hx).tower_top M
    have : IsPurelyInseparable M M⟮x⟯ :=
      (isPurelyInseparable_adjoin_simple_iff_pow_mem M E q).2
        ⟨n, ⟨x ^ q ^ n, subset_adjoin F _ ⟨x, hx, rfl⟩⟩, rfl⟩
    have hx' := mem_adjoin_simple_self M x
    rw [M⟮x⟯.eq_bot_of_isPurelyInseparable_of_isSeparable, mem_bot] at hx'
    obtain ⟨y, rfl⟩ := hx'
    exact y.2

Goal state after:
Module: Mathlib.FieldTheory.LinearDisjoint

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
A B : IntermediateField F E
inst✝ : FiniteDimensional F E
h₁ : A.LinearDisjoint ↥B
h₂ : A ⊔ B = ⊤
x : ↥B
⊢ (Algebra.trace (↥A) E) ((algebraMap (↥B) E) x) = (algebraMap F ↥A) ((Algebra.trace F ↥B) x)

Tactic:
linearDisjoint_iff'

Goal state after:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
A B : IntermediateField F E
inst✝ : FiniteDimensional F E
h₁ : A.LinearDisjoint B.toSubalgebra
h₂ : A ⊔ B = ⊤
x : ↥B
⊢ (Algebra.trace (↥A) E) ((algebraMap (↥B) E) x) = (algebraMap F ↥A) ((Algebra.trace F ↥B) x)
Module: Mathlib.FieldTheory.LinearDisjoint

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
A B : IntermediateField F E
inst✝ : FiniteDimensional F E
h₁ : A.LinearDisjoint ↥B
h₂ : A ⊔ B = ⊤
x : ↥B
⊢ (Algebra.norm ↥A) ((algebraMap (↥B) E) x) = (algebraMap F ↥A) ((Algebra.norm F) x)

Tactic:
linearDisjoint_iff'

Goal state after:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
A B : IntermediateField F E
inst✝ : FiniteDimensional F E
h₁ : A.LinearDisjoint B.toSubalgebra
h₂ : A ⊔ B = ⊤
x : ↥B
⊢ (Algebra.norm ↥A) ((algebraMap (↥B) E) x) = (algebraMap F ↥A) ((Algebra.norm F) x)
Module: Mathlib.FieldTheory.PurelyInseparable.Tower

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
S : IntermediateField F K
inst✝¹ : Algebra.IsAlgebraic F ↥S
inst✝ : IsPurelyInseparable F E
this : Algebra.IsAlgebraic F ↥(adjoin F ↑S)
⊢ sepDegree E ↥(adjoin E ↑S) = sepDegree F ↥S

Tactic:
have := sepDegree_adjoin_eq_of_isAlgebraic_of_isPurelyInseparable (F := F) E (S : Set K)

Goal state after:
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
S : IntermediateField F K
inst✝¹ : Algebra.IsAlgebraic F ↥S
inst✝ : IsPurelyInseparable F E
this✝ : Algebra.IsAlgebraic F ↥(adjoin F ↑S)
this : sepDegree E ↥(adjoin E ↑S) = sepDegree F ↥(adjoin F ↑S)
⊢ sepDegree E ↥(adjoin E ↑S) = sepDegree F ↥S
Module: Mathlib.FieldTheory.Relrank

Goal state before:
pp: E : Type v
inst✝¹ : Field E
L : Type w
inst✝ : Field L
A B : Subfield E
f : L →+* E
⊢ lift.{w, v} ((A ⊓ f.fieldRange).relrank (B ⊓ f.fieldRange)) = lift.{w, v} (A.relrank (B ⊓ f.fieldRange))

Tactic:
congr 1

Goal state after:
E : Type v
inst✝¹ : Field E
L : Type w
inst✝ : Field L
A B : Subfield E
f : L →+* E
⊢ (A ⊓ f.fieldRange).relrank (B ⊓ f.fieldRange) = A.relrank (B ⊓ f.fieldRange)
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: case neg
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : ¬E = ⊥
⊢ generator E ∈ E

Tactic:
rw [generator_eq_coeff h]
    exact SetLike.coe_mem _

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
⊢ Bivariate.swap (θ E) = -θ E

Tactic:
rw [map_sub, map_mul, map_mul, Bivariate.swap_C, Bivariate.swap_map_C, Bivariate.swap_C,
    Bivariate.swap_map_C]

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
⊢ Polynomial.map Polynomial.C (g E) * Polynomial.C (f E) - Polynomial.map Polynomial.C (f E) * Polynomial.C (g E) = -θ E
Module: Mathlib.Geometry.Convex.Cone.Face.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : DivisionRing R
inst✝³ : LinearOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
C : PointedCone R M
x✝ y✝ : M
xc : x✝ ∈ C
yc : y✝ ∈ C
⊢ x✝ + y✝ ∈ ↑C.lineal → x✝ ∈ ↑C.lineal

Tactic:
xyf

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : DivisionRing R
inst✝³ : LinearOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
C : PointedCone R M
x✝ y✝ : M
xc : x✝ ∈ C
yc : y✝ ∈ C
xyf : x✝ + y✝ ∈ ↑C.lineal
⊢ x✝ ∈ ↑C.lineal
Module: Mathlib.Geometry.Convex.Cone.Face.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : DivisionRing R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsOrderedRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
C₁ : PointedCone R M
C₂ : PointedCone R N
F : PointedCone R (M × N)
hF : F.IsFaceOf (prod C₁ C₂)
⊢ (map (LinearMap.fst R M N) F).IsFaceOf C₁

Tactic:
constructor
  · intro x hx
    simp only [mem_map, LinearMap.fst_apply, Prod.exists, exists_and_right, exists_eq_right] at hx
    exact (Set.mem_prod.mp <| hF.le hx.choose_spec).1
  · simp only [mem_map, LinearMap.fst_apply, Prod.exists, exists_and_right, exists_eq_right,
      forall_exists_index]
    intro x y a hx hy ha z h
    refine ⟨0, hF.mem_of_smul_add_mem (x := (x, 0)) (y := (y, z)) ?_ ?_ ha (by simpa)⟩
    · exact mem_prod.mp ⟨hx, zero_mem C₂⟩
    · exact mem_prod.mp ⟨hy, (hF.le h).2⟩

Goal state after:
Module: Mathlib.Geometry.Convex.Cone.Face.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : DivisionRing R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsOrderedRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
C₁ : PointedCone R M
C₂ : PointedCone R N
F : PointedCone R (M × N)
hF : F.IsFaceOf (prod C₁ C₂)
⊢ (map (LinearMap.snd R M N) F).IsFaceOf C₂

Tactic:
have := hF.map _ (LinearEquiv.prodComm R M N).injective

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : DivisionRing R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsOrderedRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
C₁ : PointedCone R M
C₂ : PointedCone R N
F : PointedCone R (M × N)
hF : F.IsFaceOf (prod C₁ C₂)
this : (map (↑(LinearEquiv.prodComm R M N)) F).IsFaceOf (map (↑(LinearEquiv.prodComm R M N)) (prod C₁ C₂))
⊢ (map (LinearMap.snd R M N) F).IsFaceOf C₂
Module: Mathlib.Geometry.Diffeology.Basic

Goal state before:
pp: X : Type u_1
d : DiffeologicalSpace X
t : TopologicalSpace X
h : dTopology = t
⊢ ∀ {u : Set X}, TopologicalSpace.IsOpen u ↔ ∀ {n : ℕ}, ∀ p ∈ plots n, IsOpen (p ⁻¹' u)

Tactic:
by intro _; rw [← d.isOpen_iff_preimages_plots, ← h]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Altitude

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
i : Fin (n + 1)
⊢ (s.restrict S hS).altitude i = comap S.subtype (s.altitude i)

Tactic:
by
  have := Nonempty.map (AffineSubspace.inclusion hS) inferInstance
  rw [← s.map_altitude_restrict S hS, comap_map_eq_of_injective S.subtype_injective]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Altitude

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
h :
  finrank ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) +
      finrank ℝ ↥((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)) =
    finrank ℝ ↥(vectorSpan ℝ (Set.range s.points))
hn : n - 1 + 1 = n
⊢ n + 1 - 1 = n

Tactic:
add_tsub_cancel_right

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
h :
  finrank ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) +
      finrank ℝ ↥((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)) =
    finrank ℝ ↥(vectorSpan ℝ (Set.range s.points))
hn : n - 1 + 1 = n
⊢ n = n
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

Goal state before:
pp: V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
hr : r < 0
⊢ o.oangle (r • x) y = o.oangle (-x) y

Tactic:
← neg_neg r,

Goal state after:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
hr : r < 0
⊢ o.oangle (- -r • x) y = o.oangle (-x) y
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

Goal state before:
pp: V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
hr : r < 0
⊢ o.oangle x (r • y) = o.oangle x (-y)

Tactic:
← neg_neg r,

Goal state after:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
hr : r < 0
⊢ o.oangle x (- -r • y) = o.oangle x (-y)
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
x : P × P × P
hx12 : x.1 ≠ x.2.1
hx32 : x.2.2 ≠ x.2.1
f : P × P × P → V × V := fun y ↦ (y.1 -ᵥ y.2.1, y.2.2 -ᵥ y.2.1)
hf1 : (f x).1 ≠ 0
hf2 : (f x).2 ≠ 0
⊢ ContinuousAt f x

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation

Goal state before:
pp: V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
f : V ≃ₗᵢ[ℝ] ℂ
hf : (map (Fin 2) f.toLinearEquiv) o = Complex.orientation
x : V
⊢ f ((o.rotation θ) x) = (Complex.orientation.rotation θ) (f x)

Tactic:
← hf,

Goal state after:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
f : V ≃ₗᵢ[ℝ] ℂ
hf : (map (Fin 2) f.toLinearEquiv) o = Complex.orientation
x : V
⊢ f ((o.rotation θ) x) = (((map (Fin 2) f.toLinearEquiv) o).rotation θ) (f x)