mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝⁵ : CommRing K
p : ℕ
inst✝⁴ : Fact (Nat.Prime p)
inst✝³ : CharP K p
L : Type v
inst✝² : CommSemiring L
inst✝¹ : CharP L p
inst✝ : PerfectRing L p
f : K →+* L
⊢ ∀ (x y : PerfectClosure K p),
    (x * y).liftOn (fun x ↦ (⇑(frobeniusEquiv L p).symm)^[x.1] (f x.2)) ⋯ =
      x.liftOn (fun x ↦ (⇑(frobeniusEquiv L p).symm)^[x.1] (f x.2)) ⋯ *
        y.liftOn (fun x ↦ (⇑(frobeniusEquiv L p).symm)^[x.1] (f x.2)) ⋯

Tactic:
rintro ⟨n, x⟩ ⟨m, y⟩

Goal state after:
case mk.mk
K : Type u
inst✝⁵ : CommRing K
p : ℕ
inst✝⁴ : Fact (Nat.Prime p)
inst✝³ : CharP K p
L : Type v
inst✝² : CommSemiring L
inst✝¹ : CharP L p
inst✝ : PerfectRing L p
f : K →+* L
x✝ : PerfectClosure K p
n : ℕ
x : K
y✝ : PerfectClosure K p
m : ℕ
y : K
⊢ (Quot.mk (R K p) (n, x) * Quot.mk (R K p) (m, y)).liftOn (fun x ↦ (⇑(frobeniusEquiv L p).symm)^[x.1] (f x.2)) ⋯ =
    liftOn (Quot.mk (R K p) (n, x)) (fun x ↦ (⇑(frobeniusEquiv L p).symm)^[x.1] (f x.2)) ⋯ *
      liftOn (Quot.mk (R K p) (m, y)) (fun x ↦ (⇑(frobeniusEquiv L p).symm)^[x.1] (f x.2)) ⋯
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝⁵ : CommRing K
p : ℕ
inst✝⁴ : Fact (Nat.Prime p)
inst✝³ : CharP K p
L : Type v
inst✝² : CommSemiring L
inst✝¹ : CharP L p
inst✝ : PerfectRing L p
f : K →+* L
⊢ ∀ (x y : PerfectClosure K p),
    (x + y).liftOn (fun x ↦ (⇑(frobeniusEquiv L p).symm)^[x.1] (f x.2)) ⋯ =
      x.liftOn (fun x ↦ (⇑(frobeniusEquiv L p).symm)^[x.1] (f x.2)) ⋯ +
        y.liftOn (fun x ↦ (⇑(frobeniusEquiv L p).symm)^[x.1] (f x.2)) ⋯

Tactic:
rintro ⟨n, x⟩ ⟨m, y⟩

Goal state after:
case mk.mk
K : Type u
inst✝⁵ : CommRing K
p : ℕ
inst✝⁴ : Fact (Nat.Prime p)
inst✝³ : CharP K p
L : Type v
inst✝² : CommSemiring L
inst✝¹ : CharP L p
inst✝ : PerfectRing L p
f : K →+* L
x✝ : PerfectClosure K p
n : ℕ
x : K
y✝ : PerfectClosure K p
m : ℕ
y : K
⊢ (Quot.mk (R K p) (n, x) + Quot.mk (R K p) (m, y)).liftOn (fun x ↦ (⇑(frobeniusEquiv L p).symm)^[x.1] (f x.2)) ⋯ =
    liftOn (Quot.mk (R K p) (n, x)) (fun x ↦ (⇑(frobeniusEquiv L p).symm)^[x.1] (f x.2)) ⋯ +
      liftOn (Quot.mk (R K p) (m, y)) (fun x ↦ (⇑(frobeniusEquiv L p).symm)^[x.1] (f x.2)) ⋯
Module: Mathlib.FieldTheory.Laurent

Goal state before:
pp: R : Type u
inst✝ : CommRing R
r : R
p : R[X]
hp : p ∈ R[X]⁰
⊢ ∀ (x : R[X]), x * (taylor r) p = 0 → x = 0

Tactic:
intro x

Goal state after:
R : Type u
inst✝ : CommRing R
r : R
p : R[X]
hp : p ∈ R[X]⁰
x : R[X]
⊢ x * (taylor r) p = 0 → x = 0
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
inst✝ : DecidablePred FiniteIndex
hcovers : ⋃ i ∈ {i ∈ s | (H i).FiniteIndex} ∪ {a ∈ s | ¬(H a).FiniteIndex}, g i • ↑(H i) = Set.univ
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 ∈ Finset.univ, f k • ↑(K k) = Set.univ

Tactic:
rw [← hcovers, ← Finset.univ.filter_union_filter_not_eq (fun k => (H k.1).FiniteIndex),
      Finset.set_biUnion_union, Finset.set_biUnion_union]

Goal state after:
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
inst✝ : DecidablePred FiniteIndex
hcovers : ⋃ i ∈ {i ∈ s | (H i).FiniteIndex} ∪ {a ∈ s | ¬(H a).FiniteIndex}, g i • ↑(H i) = Set.univ
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
⊢ (⋃ x ∈ {k | (H ↑k.fst).FiniteIndex}, f x • ↑(K x)) ∪ ⋃ x ∈ {a | ¬(H ↑a.fst).FiniteIndex}, f x • ↑(K x) =
    (⋃ x ∈ {i ∈ s | (H i).FiniteIndex}, g x • ↑(H x)) ∪ ⋃ x ∈ {a ∈ s | ¬(H a).FiniteIndex}, g x • ↑(H x)
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)
this✝ : Fact (Irreducible (X ^ n - C a)) := { out := H }
this : Algebra K K[n√a] := inferInstance
hn : 0 < n
⊢ (X ^ n - C a).Separable

Tactic:
by_cases hn' : n = 1

Goal state after:
case pos
K : Type u
inst✝ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
this✝ : Fact (Irreducible (X ^ n - C a)) := { out := H }
this : Algebra K K[n√a] := inferInstance
hn : 0 < n
hn' : n = 1
⊢ (X ^ n - C a).Separable

case neg
K : Type u
inst✝ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
this✝ : Fact (Irreducible (X ^ n - C a)) := { out := H }
this : Algebra K K[n√a] := inferInstance
hn : 0 < n
hn' : ¬n = 1
⊢ (X ^ n - C a).Separable
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: 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
hdensity : ∑ i ∈ s, (↑(H i).index)⁻¹ = ↑{x | K x = D}.card * (↑D.index)⁻¹
h : {x | K x = D}.card = D.index
i✝ : ι
hi✝ : i✝ ∈ s ∧ (H i✝).FiniteIndex
j : ι
hj : j ∈ s ∧ (H j).FiniteIndex
hij : i✝ ≠ j
c : Set G
hi'✝ : c ⊆ (fun i ↦ g i • ↑(H i)) i✝
hj' : c ⊆ (fun i ↦ g i • ↑(H i)) j
x : G
hx : x ∈ c
hdisjoint : (↑{x | K x = D}).PairwiseDisjoint fun x ↦ f x • ↑D
i : ι
hi : i ∈ s ∧ (H i).FiniteIndex
hi' : c ⊆ g i • ⋃ g ∈ t i ⋯ ⋯, ↑g • ↑D
this : ∃ r ∈ t i ⋯ ⋯, x ∈ (g i * ↑r) • ↑D
r : ↥(H i)
hr : r ∈ t i ⋯ ⋯
hxr : x ∈ (g i * ↑r) • ↑D
⊢ K ⟨⟨i, ⋯⟩, ⟨r, ⋯⟩⟩ = D ∧ x ∈ f ⟨⟨i, ⋯⟩, ⟨r, ⋯⟩⟩ • ↑D

Tactic:
simpa [K, f, if_pos hi.2] using! hxr

Goal state after:
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
A B : Subalgebra R S
ι : Type u_1
b : ι → ↥B
i : (ι →₀ ↥A) →ₗ[R] S := (toSubmodule A).mulRightMap b
j : (ι →₀ ↥A) →ₗ[R] S := ↑R (Finsupp.linearCombination (↥A) (⇑B.val ∘ b))
a✝ : ι
x✝ : ↥A
⊢ (i ∘ₗ Finsupp.lsingle a✝) x✝ = (j ∘ₗ Finsupp.lsingle a✝) x✝

Tactic:
simp only [LinearMap.coe_comp, Function.comp_apply, Finsupp.lsingle_apply, coe_val,
    LinearMap.coe_restrictScalars, Finsupp.linearCombination_single, i, j]

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
A B : Subalgebra R S
ι : Type u_1
b : ι → ↥B
i : (ι →₀ ↥A) →ₗ[R] S := (toSubmodule A).mulRightMap b
j : (ι →₀ ↥A) →ₗ[R] S := ↑R (Finsupp.linearCombination (↥A) (⇑B.val ∘ b))
a✝ : ι
x✝ : ↥A
⊢ ((toSubmodule A).mulRightMap b) (Finsupp.single a✝ x✝) = x✝ • ↑(b a✝)
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
⊢ Function.Injective carrier

Tactic:
intro x

Goal state after:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : ConjRootClass K L
⊢ ∀ ⦃a₂ : ConjRootClass K L⦄, x.carrier = a₂.carrier → x = a₂
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
⊢ normalizedTraceAux F K (a + b) = normalizedTraceAux F K a + normalizedTraceAux F K b

Tactic:
have hb : b ∈ E := (le_sup_right : F⟮b⟯ ≤ E) <| mem_adjoin_simple_self F b

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
⊢ normalizedTraceAux F K (a + b) = normalizedTraceAux F K a + normalizedTraceAux F K b
Module: Mathlib.FieldTheory.PurelyInseparable.AdjoinPthRoots

Goal state before:
pp: k : Type u_1
inst✝¹ : Field k
p✝ : ℕ
inst✝ : ExpChar k p✝
p : ℕ
hp : ExpChar k p
⊢ ∀ (x : AdjoinPthRoots k), ∃ n, x ^ p ^ n ∈ (algebraMap k (AdjoinPthRoots k)).range

Tactic:
intro x

Goal state after:
k : Type u_1
inst✝¹ : Field k
p✝ : ℕ
inst✝ : ExpChar k p✝
p : ℕ
hp : ExpChar k p
x : AdjoinPthRoots k
⊢ ∃ n, x ^ p ^ n ∈ (algebraMap k (AdjoinPthRoots k)).range
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
⊢ L ≤ perfectClosure F E

Tactic:
intro x

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
⊢ x ∈ L → x ∈ perfectClosure F E
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 : IntermediateField F E
L : Type w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
H : IsField (↥A ⊗[F] L)
⊢ A.LinearDisjoint L

Tactic:
apply Subalgebra.LinearDisjoint.of_isField

Goal state after:
F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
H : IsField (↥A ⊗[F] L)
⊢ IsField (↥A.toSubalgebra ⊗[F] ↥(IsScalarTower.toAlgHom F L E).range)
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.toSubalgebra

Tactic:
apply Subalgebra.LinearDisjoint.of_isField

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
⊢ IsField (↥fa.fieldRange.toSubalgebra ⊗[F] ↥fb.fieldRange.toSubalgebra)
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 :
  ∀ (K : Type (max v w)) [inst : Field K] [inst_1 : Algebra F K] (fa : A →ₐ[F] K) (fb : B →ₐ[F] K),
    fa.fieldRange.LinearDisjoint ↥fb.fieldRange
M : Ideal (A ⊗[F] B)
hM : M.IsMaximal
K : Type (max v w) := A ⊗[F] B ⧸ M
this : Field K := Ideal.Quotient.field M
⊢ M = ⊥

Tactic:
let i := IsScalarTower.toAlgHom F (A ⊗[F] B) K

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 :
  ∀ (K : Type (max v w)) [inst : Field K] [inst_1 : Algebra F K] (fa : A →ₐ[F] K) (fb : B →ₐ[F] K),
    fa.fieldRange.LinearDisjoint ↥fb.fieldRange
M : Ideal (A ⊗[F] B)
hM : M.IsMaximal
K : Type (max v w) := A ⊗[F] B ⧸ M
this : Field K := Ideal.Quotient.field M
i : A ⊗[F] B →ₐ[F] K := IsScalarTower.toAlgHom F (A ⊗[F] B) K
⊢ M = ⊥
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
A B : Subalgebra R S
inst✝ : Algebra.IsIntegral R ↥A
H : ∀ A' ≤ A, ∀ [Module.Finite R ↥A'], A'.LinearDisjoint B
⊢ Function.Injective ⇑((toSubmodule A).mulMap (toSubmodule B))

Tactic:
intro x

Goal state after:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
A B : Subalgebra R S
inst✝ : Algebra.IsIntegral R ↥A
H : ∀ A' ≤ A, ∀ [Module.Finite R ↥A'], A'.LinearDisjoint B
x : ↥(toSubmodule A) ⊗[R] ↥(toSubmodule B)
⊢ ∀ ⦃a₂ : ↥(toSubmodule A) ⊗[R] ↥(toSubmodule B)⦄,
    ((toSubmodule A).mulMap (toSubmodule B)) x = ((toSubmodule A).mulMap (toSubmodule B)) a₂ → x = 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
q n : ℕ
hF : ExpChar F q
ι : Type u_1
v : ι → E
inst✝ : Algebra.IsSeparable F E
h : Submodule.span F (Set.range v) = ⊤
⊢ Submodule.span F (Set.range fun x ↦ v x ^ q ^ n) = ⊤

Tactic:
rw [← Algebra.top_toSubmodule, ← top_toSubalgebra, ← adjoin_univ,
    adjoin_eq_adjoin_pow_expChar_pow_of_isSeparable' F E _ q n,
    adjoin_toSubalgebra_of_isAlgebraic fun x _ ↦ Algebra.IsAlgebraic.isAlgebraic x,
    Set.image_univ, Algebra.adjoin_eq_span]
  have := (MonoidHom.mrange (powMonoidHom (α := E) (q ^ n))).closure_eq
  simp only [MonoidHom.mrange, powMonoidHom, MonoidHom.coe_mk, OneHom.coe_mk,
    Submonoid.coe_copy] at this
  rw [this]
  refine (Submodule.span_mono <| Set.range_comp_subset_range _ _).antisymm (Submodule.span_le.2 ?_)
  rw [Set.range_comp, ← Set.image_univ]
  have := expChar_of_injective_algebraMap (algebraMap F E).injective q
  apply h ▸ Submodule.image_span_subset_span (LinearMap.iterateFrobenius F E q n) _

Goal state after:
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
inst✝ : IsPurelyInseparable F E
ι : Type u_1
v : ι → K
hsep : ∀ (i : ι), IsSeparable F (v i)
h : LinearIndependent F v
q : ℕ
h✝ : ExpChar F q
this✝ : ExpChar K q
l : ι →₀ E
i : ι
f : ι → ℕ
n : ℕ := l.support.sup f
this : q ^ n ≠ 0
lF : ι → F
hlF : ∀ (i : ι), (algebraMap F E) (lF i) = l i ^ q ^ n
lF₀ : ι →₀ F := Finsupp.onFinset l.support lF ⋯
hl : (∑ a ∈ l.support, l a • v a) ^ q ^ n = 0 ^ q ^ n
⊢ (Finsupp.linearCombination F fun x ↦ v x ^ q ^ n) lF₀ = 0

Tactic:
sum_pow_char_pow,

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
inst✝ : IsPurelyInseparable F E
ι : Type u_1
v : ι → K
hsep : ∀ (i : ι), IsSeparable F (v i)
h : LinearIndependent F v
q : ℕ
h✝ : ExpChar F q
this✝ : ExpChar K q
l : ι →₀ E
i : ι
f : ι → ℕ
n : ℕ := l.support.sup f
this : q ^ n ≠ 0
lF : ι → F
hlF : ∀ (i : ι), (algebraMap F E) (lF i) = l i ^ q ^ n
lF₀ : ι →₀ F := Finsupp.onFinset l.support lF ⋯
hl : ∑ i ∈ l.support, (l i • v i) ^ q ^ n = 0 ^ q ^ n
⊢ (Finsupp.linearCombination F fun x ↦ v x ^ q ^ n) lF₀ = 0
Module: Mathlib.Geometry.Convex.Cone.DualFinite

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsOrderedRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : M →ₗ[R] N →ₗ[R] R
C : PointedCone R N
hC : DualFG p C
⊢ dual p ↑(dual p.flip ↑C) = C

Tactic:
obtain ⟨D, hDualFG, rfl⟩ := exists_fg_dual hC

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsOrderedRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : M →ₗ[R] N →ₗ[R] R
D : PointedCone R M
hDualFG : Submodule.FG D
hC : DualFG p (dual p ↑D)
⊢ dual p ↑(dual p.flip ↑(dual p ↑D)) = dual p ↑D
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ (Φ E).natDegree = (φ E).natDegree

Tactic:
← natDegree_map_eq_of_injective (algebraMap_injective K),

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ (Polynomial.map (algebraMap K[X] K⟮X⟯) (Φ E)).natDegree = (φ E).natDegree
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
this :
  (algebraMap K[X] K⟮X⟯) ((Φ E).coeff (generatorIndex h)) * (algebraMap K[X] K⟮X⟯) (g E) =
    (algebraMap K[X] K⟮X⟯) (c E).num * generator E * (algebraMap K[X] K⟮X⟯) (g E)
| (algebraMap K[X] K⟮X⟯) ((Φ E).coeff (generatorIndex h)) * (algebraMap K[X] K⟮X⟯) (g E) =
    (algebraMap K[X] K⟮X⟯) (c E).num * generator E * (algebraMap K[X] K⟮X⟯) (g E)

Tactic:
2,

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
this :
  (algebraMap K[X] K⟮X⟯) ((Φ E).coeff (generatorIndex h)) * (algebraMap K[X] K⟮X⟯) (g E) =
    (algebraMap K[X] K⟮X⟯) (c E).num * generator E * (algebraMap K[X] K⟮X⟯) (g E)
| (algebraMap K[X] K⟮X⟯) (c E).num * generator E * (algebraMap K[X] K⟮X⟯) (g E)
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
| Polynomial.C ((algebraMap K[X] K⟮X⟯) (g E)) *
      Polynomial.map (((algebraMap (↥E) K⟮X⟯).comp ↑(inclusion ⋯)).comp (algebraMap K ↥K⟮generator E⟯))
        (generator E).num -
    Polynomial.C ((algebraMap K[X] K⟮X⟯) (g E) * ↑⟨generator E, ⋯⟩) *
      Polynomial.map (((algebraMap (↥E) K⟮X⟯).comp ↑(inclusion ⋯)).comp (algebraMap K ↥K⟮generator E⟯))
        (generator E).denom

Tactic:
2,

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
| Polynomial.C ((algebraMap K[X] K⟮X⟯) (g E) * ↑⟨generator E, ⋯⟩) *
    Polynomial.map (((algebraMap (↥E) K⟮X⟯).comp ↑(inclusion ⋯)).comp (algebraMap K ↥K⟮generator E⟯))
      (generator E).denom
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
| Polynomial.C ((algebraMap K[X] K⟮X⟯) (g E) * ↑⟨generator E, ⋯⟩)

Tactic:
2,

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
| (algebraMap K[X] K⟮X⟯) (g E) * ↑⟨generator 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 F : PointedCone R M
hF : F.IsFaceOf C
⊢ F.lineal = C.lineal

Tactic:
ext
  refine ⟨fun ⟨hx, hx'⟩ ↦ ⟨hF.le hx, hF.le hx'⟩, fun ⟨hx, hx'⟩ ↦ ⟨?_, ?_⟩⟩
  · exact hF.mem_of_add_mem_left hx hx' (by simp)
  · exact hF.mem_of_add_mem_left hx' hx (by simp)

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

Goal state before:
pp: case le
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 ≤ C₁

Tactic:
intro x

Goal state after:
case le
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₂)
x : M
⊢ x ∈ map (LinearMap.fst R M N) F → x ∈ C₁
Module: Mathlib.Geometry.Convex.Cone.Face.Basic

Goal state before:
pp: case mem_of_smul_add_mem
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₂)
⊢ ∀ {x y : M} {a : R}, x ∈ C₁ → y ∈ C₁ → 0 < a → ∀ (x_1 : N), (a • x + y, x_1) ∈ F → ∃ x_2, (x, x_2) ∈ F

Tactic:
intro x

Goal state after:
case mem_of_smul_add_mem
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₂)
x : M
⊢ ∀ {y : M} {a : R}, x ∈ C₁ → y ∈ C₁ → 0 < a → ∀ (x_1 : N), (a • x + y, x_1) ∈ F → ∃ x_2, (x, x_2) ∈ F
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ (Φ E).natDegree = (θ E).natDegree

Tactic:
by
  have := congr($(Q₂_mul_Φ h).natDegree)
  rwa [natDegree_mul (Polynomial.map_ne_zero (Q₂_ne_zero h)) (Φ_ne_zero h), natDegree_map,
    Q₂_natDegree h, zero_add] at this

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

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace 𝕜 V
inst✝⁵ : MetricSpace P
inst✝⁴ : NormedAddTorsor V P
s s' : AffineSubspace 𝕜 P
inst✝³ : Nonempty ↥s
inst✝² : Nonempty ↥s'
inst✝¹ : s.direction.HasOrthogonalProjection
inst✝ : s'.direction.HasOrthogonalProjection
h : s = s'
p : P
⊢ ↑((orthogonalProjection s) p) = ↑((orthogonalProjection s') p)

Tactic:
by
  subst h
  rfl

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
V₂ : Type u_3
P₂ : Type u_4
inst✝³ : NormedAddCommGroup V₂
inst✝² : InnerProductSpace ℝ V₂
inst✝¹ : MetricSpace P₂
inst✝ : NormedAddTorsor V₂ P₂
n : ℕ
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
i : Fin (n + 1)
⊢ (s.map f.toAffineMap ⋯).altitude i = AffineSubspace.map f.toAffineMap (s.altitude i)

Tactic:
by
  refine (eq_iff_direction_eq_of_mem (p := f (s.points i)) ?_ ?_).mpr ?_
  · exact (s.map f.toAffineMap f.injective).mem_altitude i
  · exact mem_map_of_mem f.toAffineMap (s.mem_altitude i)
  have hf : Function.Injective f.linear := f.linearIsometry.injective
  rw [map_direction, direction_altitude, direction_altitude, Submodule.map_inf _ hf,
    AffineIsometry.linear_eq_linearIsometry, Submodule.map_orthogonal,
    ← AffineIsometry.linear_eq_linearIsometry, map_points, Set.range_comp,
    Set.image_comp, ← AffineMap.map_vectorSpan, inf_assoc, ← Submodule.map_top,
    ← Submodule.map_inf _ hf, top_inf_eq, ← AffineMap.map_vectorSpan]

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

Goal state before:
pp: V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
⊢ ∀ (x y : V),
    ⟪(θ.cos • LinearMap.id + θ.sin • ↑o.rightAngleRotation.toLinearEquiv) x,
        (θ.cos • LinearMap.id + θ.sin • ↑o.rightAngleRotation.toLinearEquiv) y⟫ =
      ⟪x, y⟫

Tactic:
intro x

Goal state after:
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
x : V
⊢ ∀ (y : V),
    ⟪(θ.cos • LinearMap.id + θ.sin • ↑o.rightAngleRotation.toLinearEquiv) x,
        (θ.cos • LinearMap.id + θ.sin • ↑o.rightAngleRotation.toLinearEquiv) y⟫ =
      ⟪x, y⟫