mathlib-initiative/mathlib-tactics huggingface dataset:
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⁻¹
c_eq : a * (⇑((ad (↥k) D) a))^[n - 1] b - (⇑((ad (↥k) D) a))^[n - 1] b * a = c
eq1 : c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b - c⁻¹ * (⇑((ad (↥k) D) a))^[n - 1] b * a = 1
deq : a⁻¹ * a * d - a⁻¹ * (d * a) = a⁻¹ * a
⊢ False

Tactic:
inv_mul_cancel₀ ha₀,

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⁻¹
c_eq : a * (⇑((ad (↥k) D) a))^[n - 1] b - (⇑((ad (↥k) D) a))^[n - 1] b * a = c
eq1 : c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b - c⁻¹ * (⇑((ad (↥k) D) a))^[n - 1] b * a = 1
deq : 1 * d - a⁻¹ * (d * a) = 1
⊢ False
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⁻¹
c_eq : a * (⇑((ad (↥k) D) a))^[n - 1] b - (⇑((ad (↥k) D) a))^[n - 1] b * a = c
eq1 : c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b - c⁻¹ * (⇑((ad (↥k) D) a))^[n - 1] b * a = 1
r : ℕ
hr : d ^ p ^ r ∈ k
deq : d ^ p ^ r = 1 + d ^ p ^ r * (a⁻¹ * a)
⊢ False

Tactic:
inv_mul_cancel₀ ha₀,

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⁻¹
c_eq : a * (⇑((ad (↥k) D) a))^[n - 1] b - (⇑((ad (↥k) D) a))^[n - 1] b * a = c
eq1 : c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b - c⁻¹ * (⇑((ad (↥k) D) a))^[n - 1] b * a = 1
r : ℕ
hr : d ^ p ^ r ∈ k
deq : d ^ p ^ r = 1 + d ^ p ^ r * 1
⊢ False
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: case pos
K : Type u
inst✝¹ : Field K
a : K
h : a = 0
hζ : (primitiveRoots 1 K).Nonempty
H : Irreducible (X ^ 1 - C a)
inst✝ : NeZero 1
__spread✝⁻⁰ : ↥(rootsOfUnity 1 K) →* Gal(K[1√a]/K) := autAdjoinRootXPowSubC 1 a
e : Gal(K[1√a]/K)
this✝ : Fact (Irreducible (X ^ 1 - C a))
this : Algebra K K[1√a] := inferInstance
⊢ (of (X ^ 1 - C a)) a = e ((of (X ^ 1 - C a)) a)

Tactic:
← AdjoinRoot.algebraMap_eq,

Goal state after:
case pos
K : Type u
inst✝¹ : Field K
a : K
h : a = 0
hζ : (primitiveRoots 1 K).Nonempty
H : Irreducible (X ^ 1 - C a)
inst✝ : NeZero 1
__spread✝⁻⁰ : ↥(rootsOfUnity 1 K) →* Gal(K[1√a]/K) := autAdjoinRootXPowSubC 1 a
e : Gal(K[1√a]/K)
this✝ : Fact (Irreducible (X ^ 1 - C a))
this : Algebra K K[1√a] := inferInstance
⊢ (algebraMap K K[1√a]) a = e ((algebraMap K K[1√a]) a)
Module: Mathlib.RingTheory.TensorProduct.Nontrivial

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
ha : Function.Injective ⇑(algebraMap R A)
hb : Function.Injective ⇑(algebraMap R B)
inst✝¹ : IsDomain A
inst✝ : IsDomain B
this✝ : IsDomain R
FR : Type u_1 := FractionRing R
FA : Type u_2 := FractionRing A
FB : Type u_3 := FractionRing B
fa : FR →ₐ[R] FA := IsFractionRing.liftAlgHom ⋯
fb : FR →ₐ[R] FB := IsFractionRing.liftAlgHom ⋯
algInst✝¹ : Algebra FR FA := fa.toAlgebra
algInst✝ : Algebra FR FB := fb.toAlgebra
this : CompatibleSMul FR R FA FB := CompatibleSMul.isScalarTower
⊢ Nontrivial (A ⊗[R] B)

Tactic:
exact Algebra.TensorProduct.mapOfCompatibleSMul FR R R FA FB |>.comp
    (Algebra.TensorProduct.map (IsScalarTower.toAlgHom R A FA) (IsScalarTower.toAlgHom R B FB))
    |>.toRingHom.domain_nontrivial

Goal state after:
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
⊢ ∑ x ∈ Finset.univ.sigma fun x ↦ Finset.univ, ↑(if K x = D then 1 else 0) =
    ∑ x ∈ s.attach, (↑(H ↑x).index)⁻¹ * ↑D.index

Tactic:
Finset.sum_sigma,

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
⊢ ∑ a, ∑ s_1, ↑(if K ⟨a, s_1⟩ = D then 1 else 0) = ∑ x ∈ s.attach, (↑(H ↑x).index)⁻¹ * ↑D.index
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
hζ : (primitiveRoots n K).Nonempty
H : Irreducible (X ^ n - C a)
hα : α ^ n = (algebraMap K L) a
this✝ : Fact (Irreducible (X ^ n - C a))
this : IsSplittingField K K[n√a] (X ^ n - C a) := isSplittingField_AdjoinRoot_X_pow_sub_C hζ H
⊢ Algebra.adjoin K ((X ^ n - C a).rootSet K[n√a]) = ⊤

pp: case hf
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
hζ : (primitiveRoots n K).Nonempty
H : Irreducible (X ^ n - C a)
hα : α ^ n = (algebraMap K L) a
this✝ : Fact (Irreducible (X ^ n - C a))
this : IsSplittingField K K[n√a] (X ^ n - C a) := isSplittingField_AdjoinRoot_X_pow_sub_C hζ H
⊢ (Polynomial.map (algebraMap K K[n√a]) (X ^ n - C a)).Splits

Tactic:
IsSplittingField.adjoin_rootSet

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
hζ : (primitiveRoots n K).Nonempty
H : Irreducible (X ^ n - C a)
hα : α ^ n = (algebraMap K L) a
this✝ : Fact (Irreducible (X ^ n - C a))
this : IsSplittingField K K[n√a] (X ^ n - C a) := isSplittingField_AdjoinRoot_X_pow_sub_C hζ H
⊢ ⊤ = ⊤

case hf
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
hζ : (primitiveRoots n K).Nonempty
H : Irreducible (X ^ n - C a)
hα : α ^ n = (algebraMap K L) a
this✝ : Fact (Irreducible (X ^ n - C a))
this : IsSplittingField K K[n√a] (X ^ n - C a) := isSplittingField_AdjoinRoot_X_pow_sub_C hζ H
⊢ (Polynomial.map (algebraMap K K[n√a]) (X ^ n - C a)).Splits
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
⊢ K⟮v⟯ = ⊤

Tactic:
apply IsGalois.intermediateFieldEquivSubgroup.injective

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
⊢ IsGalois.intermediateFieldEquivSubgroup K⟮v⟯ = IsGalois.intermediateFieldEquivSubgroup ⊤
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
h : ∀ i ∈ s, (H i).FiniteIndex → s.card < (H i).index
hs : s.Nonempty
hs' : 0 < s.card
i : ι
hi : i ∈ s
⊢ (↑(H i).index)⁻¹ < (↑s.card)⁻¹

Tactic:
by
    cases eq_or_ne (H i).index 0 with
    | inl hindex =>
      rwa [hindex, Nat.cast_zero, inv_zero, inv_pos, Nat.cast_pos]
    | inr hindex =>
      exact inv_strictAnti₀ (by exact_mod_cast hs') (by exact_mod_cast h i hi ⟨hindex⟩)

Goal state after:
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : ι → Submodule R M
s : Finset ι
hcovers : ⋃ i ∈ s, ↑(p i) = Set.univ
⊢ ⋃ i ∈ s, 0 +ᵥ ↑(p i).toAddSubgroup = Set.univ

Tactic:
by
    simpa only [zero_vadd] using! hcovers

Goal state after:
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 : K
⊢ (iterateFrobenius K L p hn) ((algebraMap K L) a) = a ^ p ^ n

Tactic:
by
  apply (algebraMap K L).injective
  rw [map_pow, algebraMap_iterateFrobenius K p hn]

Goal state after:
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
x : E
⊢ F⟮x⟯ ≤ perfectClosure F E ↔ (minpoly F x).natSepDegree = 1

Tactic:
adjoin_simple_le_iff,

Goal state after:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
⊢ x ∈ perfectClosure F E ↔ (minpoly F x).natSepDegree = 1
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 : ℕ
hF : ExpChar F q
x : E
⊢ F⟮x⟯ ≤ perfectClosure F E ↔ ∃ n, x ^ q ^ n ∈ (algebraMap F E).range

Tactic:
adjoin_simple_le_iff,

Goal state after:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
⊢ x ∈ perfectClosure F E ↔ ∃ n, x ^ q ^ n ∈ (algebraMap F E).range
Module: Mathlib.FieldTheory.RatFunc.Degree

Goal state before:
pp: K : Type u
inst✝ : Field K
x y : K⟮X⟯
hx : x ≠ 0
hy : y ≠ 0
⊢ (x * y).num.natDegree + (x.denom * y.denom).natDegree = x.num.natDegree + y.num.natDegree + (x * y).denom.natDegree

Tactic:
←
    Polynomial.natDegree_mul (RatFunc.num_ne_zero (mul_ne_zero hx hy))
      (mul_ne_zero x.denom_ne_zero y.denom_ne_zero),

Goal state after:
K : Type u
inst✝ : Field K
x y : K⟮X⟯
hx : x ≠ 0
hy : y ≠ 0
⊢ ((x * y).num * (x.denom * y.denom)).natDegree = x.num.natDegree + y.num.natDegree + (x * y).denom.natDegree
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

Goal state before:
pp: K : Type u_1
inst✝⁹ : Field K
f : K⟮X⟯
A : Type u_2
inst✝⁸ : CommRing A
inst✝⁷ : Algebra K A
inst✝⁶ : Algebra (↥K[f]) A
B : Type u_3
inst✝⁵ : CommRing B
inst✝⁴ : Algebra K B
inst✝³ : Algebra (↥K[f]) B
inst✝² : Algebra A B
inst✝¹ : IsScalarTower K A B
inst✝ : IsScalarTower (↥K[f]) A B
⊢ Polynomial.map (algebraMap A B) (f.minpolyX A) = f.minpolyX B

Tactic:
by
  simp [minpolyX, Polynomial.map_map, ← IsScalarTower.algebraMap_eq,
    ← IsScalarTower.algebraMap_apply]

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

Goal state before:
pp: case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F⟮X⟯
x y : F⟮X⟯
hx : ¬x = 0
hy : y = 0
⊢ (if x * 0 = 0 then 0 else exp (x * 0).intDegree) =
    (if x = 0 then 0 else exp x.intDegree) * if 0 = 0 then 0 else exp (intDegree 0)

Tactic:
mul_zero,

Goal state after:
case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F⟮X⟯
x y : F⟮X⟯
hx : ¬x = 0
hy : y = 0
⊢ (if 0 = 0 then 0 else exp (intDegree 0)) =
    (if x = 0 then 0 else exp x.intDegree) * if 0 = 0 then 0 else exp (intDegree 0)
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
⊢ (comap f A).relfinrank (comap f B) = A.relfinrank (B ⊓ f.fieldRange)

Tactic:
by
  simpa using! congr(toNat $(lift_relrank_comap_comap_eq_lift_relrank_inf A B f))

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

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F⟮X⟯
p : F[X]
hp : p ≠ 0
⊢ inftyValuationDef F ((algebraMap F[X] F⟮X⟯) p) = exp ↑p.natDegree

Tactic:
rw [inftyValuationDef, if_neg (by simpa), RatFunc.intDegree_polynomial]

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 ≠ ⊥
⊢ (Φ E).coeff (generatorIndex h) ≠ 0

Tactic:
apply_fun algebraMap K[X] K⟮X⟯
  rw [map_zero, Φ_coeff_generatorIndex h]
  exact mul_ne_zero_iff.mpr ⟨algebraMap_ne_zero (num_ne_zero (c_ne_zero h)), generator_ne_zero h⟩

Goal state after:
Module: Mathlib.FieldTheory.Relrank

Goal state before:
pp: F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
L : Type w
inst✝¹ : Field L
inst✝ : Algebra F L
A B : IntermediateField F E
f : L →ₐ[F] E
⊢ (comap f A).relfinrank (comap f B) = A.relfinrank (B ⊓ f.fieldRange)

Tactic:
by
  simpa using! congr(toNat $(lift_relrank_comap_comap_eq_lift_relrank_inf A B f))

Goal state after:
Module: Mathlib.FieldTheory.Relrank

Goal state before:
pp: F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A : IntermediateField F E
⊢ ⊥.relrank A = Module.rank F ↥A

Tactic:
← rank_bot_mul_relrank (show ⊥ ≤ A from bot_le),

Goal state after:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A : IntermediateField F E
⊢ ⊥.relrank A = Module.rank F ↥⊥ * ⊥.relrank A
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
inst✝¹ : Nonempty ↥s
inst✝ : s.direction.HasOrthogonalProjection
p : P
⊢ ↑((orthogonalProjection s) p) ∈ mk' p s.directionᗮ

Tactic:
mem_mk',

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
inst✝¹ : Nonempty ↥s
inst✝ : s.direction.HasOrthogonalProjection
p : P
⊢ ↑((orthogonalProjection s) p) -ᵥ p ∈ s.directionᗮ
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
inst✝¹ : Nonempty ↥s
inst✝ : s.direction.HasOrthogonalProjection
p q : P
hqs : q ∈ s
hpq : p -ᵥ q ∈ s.directionᗮ
⊢ q ∈ mk' p s.directionᗮ

Tactic:
mem_mk',

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
inst✝¹ : Nonempty ↥s
inst✝ : s.direction.HasOrthogonalProjection
p q : P
hqs : q ∈ s
hpq : p -ᵥ q ∈ s.directionᗮ
⊢ q -ᵥ p ∈ s.directionᗮ
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
inst✝¹ : Nonempty ↥s
inst✝ : s.direction.HasOrthogonalProjection
p₁ p₂ p₃ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
⊢ dist p₁ p₃ = dist p₂ p₃ ↔ dist p₁ ↑((orthogonalProjection s) p₃) = dist p₂ ↑((orthogonalProjection s) p₃)

Tactic:
by
  rw [← mul_self_inj_of_nonneg dist_nonneg dist_nonneg, ←
    mul_self_inj_of_nonneg dist_nonneg dist_nonneg,
    dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq p₃ hp₁,
    dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq p₃ hp₂]
  simp

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 : AffineSubspace 𝕜 P
inst✝¹ : Nonempty ↥s
inst✝ : s.direction.HasOrthogonalProjection
p x : P
hx : x ∈ s
⊢ (reflection s) p = s.direction.reflection (p -ᵥ x) +ᵥ x

Tactic:
reflection_apply,

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
inst✝¹ : Nonempty ↥s
inst✝ : s.direction.HasOrthogonalProjection
p x : P
hx : x ∈ s
⊢ s.direction.reflection (p -ᵥ ↑(Classical.arbitrary ↥s)) +ᵥ ↑(Classical.arbitrary ↥s) =
    s.direction.reflection (p -ᵥ x) +ᵥ x
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
inst✝¹ : Nonempty ↥s
inst✝ : s.direction.HasOrthogonalProjection
p : P
⊢ (reflection s) p = (↑((orthogonalProjection s) p) -ᵥ p) +ᵥ ↑((orthogonalProjection s) p)

Tactic:
reflection_apply,

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
inst✝¹ : Nonempty ↥s
inst✝ : s.direction.HasOrthogonalProjection
p : P
⊢ s.direction.reflection (p -ᵥ ↑(Classical.arbitrary ↥s)) +ᵥ ↑(Classical.arbitrary ↥s) =
    (↑((orthogonalProjection s) p) -ᵥ p) +ᵥ ↑((orthogonalProjection s) p)
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
inst✝¹ : Nonempty ↥s
inst✝ : s.direction.HasOrthogonalProjection
p : P
⊢ (reflection s) p = p ↔ p ∈ s

Tactic:
reflection_apply,

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
inst✝¹ : Nonempty ↥s
inst✝ : s.direction.HasOrthogonalProjection
p : P
⊢ s.direction.reflection (p -ᵥ ↑(Classical.arbitrary ↥s)) +ᵥ ↑(Classical.arbitrary ↥s) = p ↔ p ∈ s
Module: Mathlib.Geometry.Euclidean.Altitude

Goal state before:
pp: case mpr.refine_1
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)
p : P
hne : p ≠ s.points i
h : p -ᵥ s.points i ∈ (s.altitude i).direction
⊢ ℝ ∙ (p -ᵥ s.points i) ≤ (s.altitude i).direction

Tactic:
rw [Submodule.span_le]
      simpa using h

Goal state after:
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
⊢ o.oangle y x = -o.oangle x y

Tactic:
by
  simp only [oangle, o.kahler_swap y x, Complex.arg_conj_coe_angle]

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
inst✝ : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
r : ℝ
hr : r ≠ 0
h : s.points j -ᵥ s.altitudeFoot j = r • (s.points i -ᵥ s.altitudeFoot i)
k : Fin (n + 1)
hki : k ≠ i
hkj : k ≠ j
⊢ s.points k ∈ Set.range (s.faceOpposite i).points

Tactic:
rw [range_faceOpposite_points]

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 : ℕ
s : Simplex ℝ P n
inst✝ : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
r : ℝ
hr : r ≠ 0
h : s.points j -ᵥ s.altitudeFoot j = r • (s.points i -ᵥ s.altitudeFoot i)
k : Fin (n + 1)
hki : k ≠ i
hkj : k ≠ j
⊢ s.points k ∈ s.points '' {i}ᶜ
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
inst✝ : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
r : ℝ
hr : r ≠ 0
h : s.points j -ᵥ s.altitudeFoot j = r • (s.points i -ᵥ s.altitudeFoot i)
k : Fin (n + 1)
hki : k ≠ i
hkj : k ≠ j
hki' : s.points k ∈ Set.range (s.faceOpposite i).points
⊢ s.points k ∈ Set.range (s.faceOpposite j).points

Tactic:
rw [range_faceOpposite_points]

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 : ℕ
s : Simplex ℝ P n
inst✝ : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
r : ℝ
hr : r ≠ 0
h : s.points j -ᵥ s.altitudeFoot j = r • (s.points i -ᵥ s.altitudeFoot i)
k : Fin (n + 1)
hki : k ≠ i
hkj : k ≠ j
hki' : s.points k ∈ Set.range (s.faceOpposite i).points
⊢ s.points k ∈ s.points '' {j}ᶜ