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

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing K
inst✝⁷ : CommRing L
inst✝⁶ : CommRing M
inst✝⁵ : CommRing N
i : K →+* L
j : K →+* M
k : K →+* N
f : L →+* M
g : L →+* N
p : ℕ
inst✝⁴ : ExpChar M p
inst✝³ : ExpChar K p
inst✝² : PerfectRing M p
inst✝¹ : IsPRadical i p
inst✝ : ExpChar L p
x1 x2 : L
n1 : ℕ
y1 : K
h1 : i y1 = x1 ^ p ^ n1
n2 : ℕ
y2 : K
h2 : i y2 = x2 ^ p ^ n2
⊢ (x1 ^ p ^ n1) ^ p ^ n2 * (x2 ^ p ^ n2) ^ p ^ n1 = (x1 * x2) ^ p ^ (n1 + n2)

Tactic:
← pow_mul,

Goal state after:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing K
inst✝⁷ : CommRing L
inst✝⁶ : CommRing M
inst✝⁵ : CommRing N
i : K →+* L
j : K →+* M
k : K →+* N
f : L →+* M
g : L →+* N
p : ℕ
inst✝⁴ : ExpChar M p
inst✝³ : ExpChar K p
inst✝² : PerfectRing M p
inst✝¹ : IsPRadical i p
inst✝ : ExpChar L p
x1 x2 : L
n1 : ℕ
y1 : K
h1 : i y1 = x1 ^ p ^ n1
n2 : ℕ
y2 : K
h2 : i y2 = x2 ^ p ^ n2
⊢ x1 ^ (p ^ n1 * p ^ n2) * (x2 ^ p ^ n2) ^ p ^ n1 = (x1 * x2) ^ p ^ (n1 + n2)
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing K
inst✝⁷ : CommRing L
inst✝⁶ : CommRing M
inst✝⁵ : CommRing N
i : K →+* L
j : K →+* M
k : K →+* N
f : L →+* M
g : L →+* N
p : ℕ
inst✝⁴ : ExpChar M p
inst✝³ : ExpChar K p
inst✝² : PerfectRing M p
inst✝¹ : IsPRadical i p
inst✝ : ExpChar L p
x1 x2 : L
n1 : ℕ
y1 : K
h1 : i y1 = x1 ^ p ^ n1
n2 : ℕ
y2 : K
h2 : i y2 = x2 ^ p ^ n2
⊢ x1 ^ p ^ (n1 + n2) * (x2 ^ p ^ n2) ^ p ^ n1 = (x1 * x2) ^ p ^ (n1 + n2)

Tactic:
← pow_mul,

Goal state after:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing K
inst✝⁷ : CommRing L
inst✝⁶ : CommRing M
inst✝⁵ : CommRing N
i : K →+* L
j : K →+* M
k : K →+* N
f : L →+* M
g : L →+* N
p : ℕ
inst✝⁴ : ExpChar M p
inst✝³ : ExpChar K p
inst✝² : PerfectRing M p
inst✝¹ : IsPRadical i p
inst✝ : ExpChar L p
x1 x2 : L
n1 : ℕ
y1 : K
h1 : i y1 = x1 ^ p ^ n1
n2 : ℕ
y2 : K
h2 : i y2 = x2 ^ p ^ n2
⊢ x1 ^ p ^ (n1 + n2) * x2 ^ (p ^ n2 * p ^ n1) = (x1 * x2) ^ p ^ (n1 + n2)
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : ℕ × K
n : ℕ
ih : mk K p x ^ n = mk K p (x.1, x.2 ^ n)
⊢ ((x.2 ^ n) ^ p ^ x.1) ^ p ^ x.1 * (x.2 ^ p ^ x.1) ^ p ^ x.1 = (x.2 ^ n) ^ p ^ (x.1 + x.1) * x.2 ^ p ^ (x.1 + x.1)

Tactic:
← pow_mul,

Goal state after:
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : ℕ × K
n : ℕ
ih : mk K p x ^ n = mk K p (x.1, x.2 ^ n)
⊢ x.2 ^ (n * p ^ x.1 * p ^ x.1) * x.2 ^ (p ^ x.1 * p ^ x.1) = x.2 ^ (n * p ^ (x.1 + x.1)) * x.2 ^ p ^ (x.1 + x.1)
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing K
inst✝⁷ : CommRing L
inst✝⁶ : CommRing M
inst✝⁵ : CommRing N
i : K →+* L
j : K →+* M
k : K →+* N
f : L →+* M
g : L →+* N
p : ℕ
inst✝⁴ : ExpChar M p
inst✝³ : ExpChar K p
inst✝² : PerfectRing M p
inst✝¹ : IsPRadical i p
inst✝ : ExpChar L p
x1 x2 : L
n1 : ℕ
y1 : K
h1 : i y1 = x1 ^ p ^ n1
n2 : ℕ
y2 : K
h2 : i y2 = x2 ^ p ^ n2
⊢ (x1 ^ p ^ n1) ^ p ^ n2 + (x2 ^ p ^ n2) ^ p ^ n1 = (x1 + x2) ^ p ^ (n1 + n2)

Tactic:
← pow_mul,

Goal state after:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing K
inst✝⁷ : CommRing L
inst✝⁶ : CommRing M
inst✝⁵ : CommRing N
i : K →+* L
j : K →+* M
k : K →+* N
f : L →+* M
g : L →+* N
p : ℕ
inst✝⁴ : ExpChar M p
inst✝³ : ExpChar K p
inst✝² : PerfectRing M p
inst✝¹ : IsPRadical i p
inst✝ : ExpChar L p
x1 x2 : L
n1 : ℕ
y1 : K
h1 : i y1 = x1 ^ p ^ n1
n2 : ℕ
y2 : K
h2 : i y2 = x2 ^ p ^ n2
⊢ x1 ^ (p ^ n1 * p ^ n2) + (x2 ^ p ^ n2) ^ p ^ n1 = (x1 + x2) ^ p ^ (n1 + n2)
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing K
inst✝⁷ : CommRing L
inst✝⁶ : CommRing M
inst✝⁵ : CommRing N
i : K →+* L
j : K →+* M
k : K →+* N
f : L →+* M
g : L →+* N
p : ℕ
inst✝⁴ : ExpChar M p
inst✝³ : ExpChar K p
inst✝² : PerfectRing M p
inst✝¹ : IsPRadical i p
inst✝ : ExpChar L p
x1 x2 : L
n1 : ℕ
y1 : K
h1 : i y1 = x1 ^ p ^ n1
n2 : ℕ
y2 : K
h2 : i y2 = x2 ^ p ^ n2
⊢ x1 ^ p ^ (n1 + n2) + (x2 ^ p ^ n2) ^ p ^ n1 = (x1 + x2) ^ p ^ (n1 + n2)

Tactic:
← pow_mul,

Goal state after:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing K
inst✝⁷ : CommRing L
inst✝⁶ : CommRing M
inst✝⁵ : CommRing N
i : K →+* L
j : K →+* M
k : K →+* N
f : L →+* M
g : L →+* N
p : ℕ
inst✝⁴ : ExpChar M p
inst✝³ : ExpChar K p
inst✝² : PerfectRing M p
inst✝¹ : IsPRadical i p
inst✝ : ExpChar L p
x1 x2 : L
n1 : ℕ
y1 : K
h1 : i y1 = x1 ^ p ^ n1
n2 : ℕ
y2 : K
h2 : i y2 = x2 ^ p ^ n2
⊢ x1 ^ p ^ (n1 + n2) + x2 ^ (p ^ n2 * p ^ n1) = (x1 + x2) ^ p ^ (n1 + n2)
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : K
h : x ∈ RingHom.ker (of K p)
⊢ x ∈ pNilradical K p

Tactic:
by
    rw [RingHom.mem_ker, of_apply, zero_def, mk_eq_iff] at h
    obtain ⟨n, h⟩ := h
    simp_rw [zero_add, ← coe_iterateFrobenius, map_zero] at h
    exact mem_pNilradical.2 ⟨n, h⟩

Goal state after:
Module: Mathlib.FieldTheory.MvRatFunc.Rank

Goal state before:
pp: σ : Type u
F : Type v
inst✝¹ : Field F
inst✝ : Nonempty σ
⊢ Module.rank F (FractionRing (MvPolynomial σ F)) = max (max (lift.{u, v} #F) (lift.{v, u} #σ)) ℵ₀

Tactic:
by
  let R := MvPolynomial σ F
  let K := FractionRing R
  refine ((rank_le_card _ _).trans ?_).antisymm ?_
  · rw [FractionRing.cardinalMk, MvPolynomial.cardinalMk_eq_max_lift]
  have hinj := IsFractionRing.injective R K
  have h1 := (IsScalarTower.toAlgHom F R K).toLinearMap.rank_le_of_injective hinj
  rw [MvPolynomial.rank_eq_lift, mk_finsupp_nat, lift_max, lift_aleph0, max_le_iff] at h1
  obtain ⟨i⟩ := ‹Nonempty σ›
  have hx : Transcendental F (algebraMap R K (MvPolynomial.X i)) :=
    (transcendental_algebraMap_iff hinj).2 (MvPolynomial.transcendental_X F i)
  have h2 := hx.linearIndependent_sub_inv.cardinal_lift_le_rank
  rw [lift_id'.{v, u}, lift_umax.{v, u}] at h2
  exact max_le (max_le h2 h1.1) h1.2

Goal state after:
Module: Mathlib.FieldTheory.JacobsonNoether

Goal state before:
pp: D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
H : k ≠ ⊤
p : ℕ
hp : ExpChar D p
insep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
a : D
ha : a ∉ k
ha₀ : a ≠ 0
b : D
hb1 : ((ad (↥k) D) a) b ≠ 0
n : ℕ
hn : 0 < n
c : D := (⇑((ad (↥k) D) a))^[n] b
hb : c ≠ 0 ∧ (⇑((ad (↥k) D) a))^[n + 1] b = 0
hc_def : c = (⇑((ad (↥k) D) a))^[n] b
x✝ : Invertible c := { invOf := c⁻¹, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }
hc : a * c = c * a
d : D := c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b
hd_def : d = c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b
hc' : c⁻¹ * a = a * c⁻¹
⊢ a * (⇑((ad (↥k) D) a))^[n - Nat.succ 0 + Nat.succ 0 - 1] b -
      (⇑((ad (↥k) D) a))^[n - Nat.succ 0 + Nat.succ 0 - 1] b * a =
    (⇑((ad (↥k) D) a))^[n - Nat.succ 0 + Nat.succ 0] b

Tactic:
Function.iterate_succ_apply' (ad k D a) _ b

Goal state after:
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
H : k ≠ ⊤
p : ℕ
hp : ExpChar D p
insep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
a : D
ha : a ∉ k
ha₀ : a ≠ 0
b : D
hb1 : ((ad (↥k) D) a) b ≠ 0
n : ℕ
hn : 0 < n
c : D := (⇑((ad (↥k) D) a))^[n] b
hb : c ≠ 0 ∧ (⇑((ad (↥k) D) a))^[n + 1] b = 0
hc_def : c = (⇑((ad (↥k) D) a))^[n] b
x✝ : Invertible c := { invOf := c⁻¹, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }
hc : a * c = c * a
d : D := c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b
hd_def : d = c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b
hc' : c⁻¹ * a = a * c⁻¹
⊢ a * (⇑((ad (↥k) D) a))^[n - Nat.succ 0 + Nat.succ 0 - 1] b -
      (⇑((ad (↥k) D) a))^[n - Nat.succ 0 + Nat.succ 0 - 1] b * a =
    ((ad (↥k) D) a) ((⇑((ad (↥k) D) a))^[n - Nat.succ 0] b)
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
⊢ ∑ i ∈ s, (↑(H i).index)⁻¹ * ↑D.index = ↑{x | K x = D}.card

Tactic:
← Finset.sum_attach,

Goal state after:
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
⊢ ∑ x ∈ s.attach, (↑(H ↑x).index)⁻¹ * ↑D.index = ↑{x | K x = D}.card
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
⊢ (adjoinRootXPowSubCEquiv hζ H hα) (root (X ^ n - C a)) = α

Tactic:
by
  rw [adjoinRootXPowSubCEquiv, AlgEquiv.coe_ofBijective, liftAlgHom_root]

Goal state after:
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: K : Type u
inst✝⁴ : Field K
n : ℕ
a : K
L : Type u_1
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : IsSplittingField K L (X ^ n - C a)
inst✝ : NeZero n
⊢ (Polynomial.map (algebraMap K L) (X ^ n - C a)).degree ≠ 0

Tactic:
by simp [degree_X_pow_sub_C (NeZero.pos n), NeZero.ne n]

Goal state after:
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: case refine_1
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
n : ℕ
hσ' : σ ^ n ∈ OrderDual.ofDual ⊥
⊢ (ζ ^ n) ^ finrank K L • v ^ finrank K L = v ^ finrank K L

Tactic:
← pow_mul,

Goal state after:
case refine_1
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
n : ℕ
hσ' : σ ^ n ∈ OrderDual.ofDual ⊥
⊢ ζ ^ (n * finrank K L) • v ^ finrank K L = v ^ finrank K L
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
inst✝ : Fintype ↑c.carrier
⊢ c.minpoly.aroots L = (c.minpoly.aroots L).dedup

Tactic:
c.nodup_aroots_minpoly.dedup

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.Exponent

Goal state before:
pp: case prime
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : IsPurelyInseparable K L
inst✝ : FiniteDimensional K L
p : ℕ
h✝ : ExpChar K p
hp : Nat.Prime p
hchar✝ : CharP K p
e : ℕ := Nat.log (ringExpChar K) (Module.finrank K L)
a : L
h_elemexp_bound : ∀ (a : L), elemExponent K a ≤ e
⊢ (a ^ ringExpChar K ^ elemExponent K a) ^ ringExpChar K ^ (e - elemExponent K a) = a ^ ringExpChar K ^ e

Tactic:
← pow_mul,

Goal state after:
case prime
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : IsPurelyInseparable K L
inst✝ : FiniteDimensional K L
p : ℕ
h✝ : ExpChar K p
hp : Nat.Prime p
hchar✝ : CharP K p
e : ℕ := Nat.log (ringExpChar K) (Module.finrank K L)
a : L
h_elemexp_bound : ∀ (a : L), elemExponent K a ≤ e
⊢ a ^ (ringExpChar K ^ elemExponent K a * ringExpChar K ^ (e - elemExponent K a)) = a ^ ringExpChar K ^ e
Module: Mathlib.FieldTheory.PurelyInseparable.Exponent

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : HasExponent K L
p : ℕ
inst✝ : ExpChar K p
n : ℕ
hn : exponent K L ≤ n
a : L
⊢ (a ^ p ^ elemExponent K a) ^ p ^ (n - elemExponent K a) = a ^ p ^ n

Tactic:
← pow_mul,

Goal state after:
K : Type u_2
L : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : HasExponent K L
p : ℕ
inst✝ : ExpChar K p
n : ℕ
hn : exponent K L ≤ n
a : L
⊢ a ^ (p ^ elemExponent K a * p ^ (n - elemExponent K a)) = a ^ p ^ n
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
K : Type w
inst✝³ : Field K
inst✝² : Algebra F K
p : ℕ
inst✝¹ : ExpChar E p
inst✝ : PerfectRing E p
x : ↥(perfectClosure F E)
this : ExpChar F p
x' : E
hx : x' ^ p = ↑x
n : ℕ
y : F
hy : (algebraMap F E) y = (x' ^ p) ^ p ^ n
⊢ ∃ a, (frobenius (↥(perfectClosure F E)) p) a = x

Tactic:
← pow_mul,

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
p : ℕ
inst✝¹ : ExpChar E p
inst✝ : PerfectRing E p
x : ↥(perfectClosure F E)
this : ExpChar F p
x' : E
hx : x' ^ p = ↑x
n : ℕ
y : F
hy : (algebraMap F E) y = x' ^ (p * p ^ n)
⊢ ∃ a, (frobenius (↥(perfectClosure F E)) p) a = 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
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
hl : (Finsupp.linearCombination E v) l = 0
i✝ : ι
f : ι → ℕ
hf : ∀ (i : ι), l i ^ q ^ f i ∈ (algebraMap F E).range
n : ℕ := l.support.sup f
this : q ^ n ≠ 0
i : ι
hs : i ∈ l.support
⊢ l i ^ q ^ n = (l i ^ q ^ f i) ^ q ^ (n - f i)

Tactic:
← pow_mul,

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
hl : (Finsupp.linearCombination E v) l = 0
i✝ : ι
f : ι → ℕ
hf : ∀ (i : ι), l i ^ q ^ f i ∈ (algebraMap F E).range
n : ℕ := l.support.sup f
this : q ^ n ≠ 0
i : ι
hs : i ∈ l.support
⊢ l i ^ q ^ n = l i ^ (q ^ f i * q ^ (n - f i))
Module: Mathlib.FieldTheory.RatFunc.Degree

Goal state before:
pp: K : Type u
inst✝ : Field K
x : K⟮X⟯
⊢ x⁻¹.intDegree = -x.intDegree

Tactic:
by
  by_cases hx : x = 0 <;> simp [hx, eq_neg_iff_add_eq_zero, ← intDegree_mul (inv_ne_zero hx) hx]

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
hE : ¬E = ⊥
⊢ IsAlgebraic (↥E) X

Tactic:
← le_bot_iff,

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
hE : ¬E ≤ ⊥
⊢ IsAlgebraic (↥E) X
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 (c E) * Polynomial.map (algebraMap (↥E) K⟮X⟯) (φ E) = Polynomial.map (algebraMap K[X] K⟮X⟯) (Φ E)

Tactic:
by
  classical
  rw [map_mul, mul_assoc]
  conv =>
    enter [1, 2]
    rw [← Polynomial.smul_eq_C_mul, algebraMap_smul, ← Φ'_map, eq_C_content_mul_primPart (Φ' E)]
  rw [Polynomial.map_mul, map_C, ← mul_assoc, ← C_mul, inv_mul_cancel₀, map_one, one_mul]
  · rw [ne_eq, FaithfulSMul.algebraMap_eq_zero_iff, content_eq_zero_iff]
    exact Φ'_ne_zero h

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
this : Bivariate.swap (Bivariate.swap (Q₁ h)) = Bivariate.swap (Polynomial.C ((Bivariate.swap (Q₁ h)).coeff 0))
⊢ Polynomial.map Polynomial.C (Q₂ h) = Q₁ h

Tactic:
Bivariate.swap_swap_apply,

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
this : Q₁ h = Bivariate.swap (Polynomial.C ((Bivariate.swap (Q₁ h)).coeff 0))
⊢ Polynomial.map Polynomial.C (Q₂ h) = Q₁ h
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 : AffineSubspace 𝕜 P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
r₁ r₂ : 𝕜
v : V
hv : v ∈ s.directionᗮ
⊢ ‖(r₁ • v +ᵥ p₁) -ᵥ p₂ - r₂ • v‖ * ‖(r₁ • v +ᵥ p₁) -ᵥ p₂ - r₂ • v‖ =
    ‖p₁ -ᵥ p₂ + (r₁ - r₂) • v‖ * ‖p₁ -ᵥ p₂ + (r₁ - r₂) • v‖

Tactic:
vadd_vsub_assoc,

Goal state after:
𝕜 : 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 : AffineSubspace 𝕜 P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
r₁ r₂ : 𝕜
v : V
hv : v ∈ s.directionᗮ
⊢ ‖r₁ • v + (p₁ -ᵥ p₂) - r₂ • v‖ * ‖r₁ • v + (p₁ -ᵥ p₂) - r₂ • v‖ =
    ‖p₁ -ᵥ p₂ + (r₁ - r₂) • v‖ * ‖p₁ -ᵥ p₂ + (r₁ - r₂) • v‖
Module: Mathlib.Geometry.Euclidean.Projection

Goal state before:
pp: case mp
𝕜 : 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
p : P
h :
  ((↑((orthogonalProjection s₁) p) -ᵥ p) +ᵥ ↑((orthogonalProjection s₁) p)) -ᵥ ↑((orthogonalProjection s₂) p) -
      (↑((orthogonalProjection s₂) p) -ᵥ p) =
    0
⊢ ↑((orthogonalProjection s₁) p) = ↑((orthogonalProjection s₂) p)

Tactic:
vadd_vsub_assoc,

Goal state after:
case mp
𝕜 : 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
p : P
h :
  ↑((orthogonalProjection s₁) p) -ᵥ p + (↑((orthogonalProjection s₁) p) -ᵥ ↑((orthogonalProjection s₂) p)) -
      (↑((orthogonalProjection s₂) p) -ᵥ p) =
    0
⊢ ↑((orthogonalProjection s₁) p) = ↑((orthogonalProjection s₂) p)
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)
⊢ s.altitudeFoot i ∈ affineSpan ℝ (Set.range s.points)

Tactic:
refine SetLike.le_def.1 (affineSpan_mono _ ?_) (s.altitudeFoot_mem_affineSpan_faceOpposite _)

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)
⊢ Set.range (s.faceOpposite i).points ⊆ Set.range s.points
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
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π
⊢ dist p₁ p₂ ≠ 0

Tactic:
by_contra heq
  rw [dist_eq_zero] at heq
  rw [heq, angle_self_left] at h
  exact Real.pi_ne_zero (by linarith)

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) = ↑θ.toCircle * f x

Tactic:
rw [← Complex.rotation, ← hf, o.rotation_map, LinearIsometryEquiv.symm_apply_apply]

Goal state after:
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
p₁ p₂ p₃ : P
r : ℝ
hp₂ : (AffineMap.lineMap p₁ p₃) r = p₂
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
hr0' : r ≠ 0
hr1' : r ≠ 1
hr0 : 0 < r
hr1 : r < 1
⊢ p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = - -((1 - r) • (p₃ -ᵥ p₁))

Tactic:
neg_neg,

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
r : ℝ
hp₂ : (AffineMap.lineMap p₁ p₃) r = p₂
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
hr0' : r ≠ 0
hr1' : r ≠ 1
hr0 : 0 < r
hr1 : r < 1
⊢ p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = (1 - r) • (p₃ -ᵥ p₁)
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

Goal state before:
pp: case mpr.inr
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
y : V
hy : y ≠ 0
r : ℝ
hr : 0 ≤ r
h₁ : ‖r • y‖ = ‖y‖
h₂ : SameRay ℝ (r • y) y
this : ‖y‖ ≠ 0
⊢ r • y = y

Tactic:
obtain rfl : r = 1 := by
      apply mul_right_cancel₀ this
      simpa [norm_smul, abs_of_nonneg hr] using h₁

Goal state after:
case mpr.inr
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
y : V
hy : y ≠ 0
this : ‖y‖ ≠ 0
hr : 0 ≤ 1
h₁ : ‖1 • y‖ = ‖y‖
h₂ : SameRay ℝ (1 • y) y
⊢ 1 • y = y
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine

Goal state before:
pp: case refine_1
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
hp₁p₂ : p₁ -ᵥ p₂ ≠ 0
r : ℝ
hr : r < 0
hp₃p₂ : p₃ = r • (p₁ -ᵥ p₂) +ᵥ p₂
⊢ (1 / (1 - r)) • ((r • (p₁ -ᵥ p₂) +ᵥ p₂) -ᵥ p₁) +ᵥ p₁ = p₂

Tactic:
vadd_vsub_assoc,

Goal state after:
case refine_1
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
hp₁p₂ : p₁ -ᵥ p₂ ≠ 0
r : ℝ
hr : r < 0
hp₃p₂ : p₃ = r • (p₁ -ᵥ p₂) +ᵥ p₂
⊢ (1 / (1 - r)) • (r • (p₁ -ᵥ p₂) + (p₂ -ᵥ p₁)) +ᵥ p₁ = p₂
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
p₁ p₃ : P
r : ℝ
hr1 : r ≤ 1
hp₂p₁ : (AffineMap.lineMap p₁ p₃) r ≠ p₁
hr0' : r ≠ 0
hr0 : 0 < r
⊢ p₃ -ᵥ p₁ = r⁻¹ • ((r • (p₃ -ᵥ p₁) +ᵥ p₁) -ᵥ p₁)

Tactic:
vadd_vsub_assoc,

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₃ : P
r : ℝ
hr1 : r ≤ 1
hp₂p₁ : (AffineMap.lineMap p₁ p₃) r ≠ p₁
hr0' : r ≠ 0
hr0 : 0 < r
⊢ p₃ -ᵥ p₁ = r⁻¹ • (r • (p₃ -ᵥ p₁) + (p₁ -ᵥ p₁))