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
⊢ liftAux i j p (x1 * x2) = (iterateFrobeniusEquiv M p n1).symm (j y1) * (iterateFrobeniusEquiv M p n2).symm (j y2)

Tactic:
liftAux_apply i j p (x1 * x2) (n1 + n2) (y1 ^ p ^ n2 * y2 ^ p ^ n1) (by rw [map_mul,
        map_pow, map_pow, h1, h2, ← pow_mul, ← pow_add, ← pow_mul, ← pow_add,
        add_comm n2, mul_pow]),

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
⊢ (iterateFrobeniusEquiv M p (n1 + n2)).symm (j (y1 ^ p ^ n2 * y2 ^ p ^ n1)) =
    (iterateFrobeniusEquiv M p n1).symm (j y1) * (iterateFrobeniusEquiv M p n2).symm (j y2)
Module: Mathlib.FieldTheory.Isaacs

Goal state before:
pp: case inr
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (x : E), ∃ y, (aeval y) (minpoly F x) = 0
S : Finset E
p : K[X] := ∏ x ∈ S, Polynomial.map (algebraMap F K) (minpoly F x)
K' : Type u_3 := p.SplittingField
splits : ∀ s ∈ S, (Polynomial.map (algebraMap F K') (minpoly F s)).Splits
K₀ : IntermediateField F K' := restrictScalars F ⊥
FS : IntermediateField F E := adjoin F ↑S
Ω : Type (max u_2 u_3) := ↥FS →ₐ[F] K'
this✝ : FiniteDimensional F ↥(adjoin F ↑S)
M : Ω → Submodule F ↥FS := fun ω ↦ Subalgebra.toSubmodule (comap ω K₀).toSubalgebra
this : ⋃ ω, ↑(M ω) = Set.univ
h✝ : Infinite F
⊢ ∃ ω, ⊤ ≤ M ω

Tactic:
· simp_rw [top_le_iff, Subspace.exists_eq_top_of_iUnion_eq_univ this]

Goal state after:
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)
ε η : ↥(rootsOfUnity n K)
⊢ (liftAlgHom (X ^ n - C a) (Algebra.ofId K K[n√a]) (↑↑(ε * η) • root (X ^ n - C a)) ⋯) (root (X ^ n - C a)) =
    (liftAlgHom (X ^ n - C a) (Algebra.ofId K K[n√a]) (↑↑ε • root (X ^ n - C a)) ⋯ *
        liftAlgHom (X ^ n - C a) (Algebra.ofId K K[n√a]) (↑↑η • root (X ^ n - C a)) ⋯)
      (root (X ^ n - C a))

Tactic:
by simp [mul_smul, smul_comm ((ε : Kˣ) : K)]

Goal state after:
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)
inst✝ : NeZero n
η : ↥(rootsOfUnity n K)
⊢ AdjoinRootXPowSubCEquivToRootsOfUnity hζ H ((↑(autAdjoinRootXPowSubC n a)).toFun η) = η

Tactic:
have := Fact.mk H

Goal state after:
K : Type u
inst✝¹ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
inst✝ : NeZero n
η : ↥(rootsOfUnity n K)
this : Fact (Irreducible (X ^ n - C a))
⊢ AdjoinRootXPowSubCEquivToRootsOfUnity hζ H ((↑(autAdjoinRootXPowSubC n a)).toFun η) = η
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)
inst✝ : NeZero n
e : K[n√a] ≃ₐ[K] K[n√a]
⊢ (↑(autAdjoinRootXPowSubC n a)).toFun (AdjoinRootXPowSubCEquivToRootsOfUnity hζ H e) = e

Tactic:
have := Fact.mk H

Goal state after:
K : Type u
inst✝¹ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
inst✝ : NeZero n
e : Gal(K[n√a]/K)
this : Fact (Irreducible (X ^ n - C a))
⊢ (↑(autAdjoinRootXPowSubC n a)).toFun (AdjoinRootXPowSubCEquivToRootsOfUnity hζ H e) = e
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)
inst✝ : NeZero n
σ : K[n√a] ≃ₐ[K] K[n√a]
⊢ ↑((autAdjoinRootXPowSubCEquiv hζ H).symm σ) • root (X ^ n - C a) = σ (root (X ^ n - C a))

Tactic:
have := Fact.mk H

Goal state after:
K : Type u
inst✝¹ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
inst✝ : NeZero n
σ : Gal(K[n√a]/K)
this : Fact (Irreducible (X ^ n - C a))
⊢ ↑((autAdjoinRootXPowSubCEquiv hζ H).symm σ) • root (X ^ n - C a) = σ (root (X ^ n - C a))
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)
⊢ IsSplittingField K K[n√a] (X ^ n - C a)

Tactic:
have := Fact.mk H

Goal state after:
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))
⊢ IsSplittingField K K[n√a] (X ^ n - C a)
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
⊢ Function.Bijective ⇑(liftAlgHom (X ^ n - C a) (Algebra.ofId K L) α ⋯)

Tactic:
have := Fact.mk H

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))
⊢ Function.Bijective ⇑(liftAlgHom (X ^ n - C a) (Algebra.ofId K L) α ⋯)
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
B : Subalgebra R S
⊢ (toSubmodule ⊥).LinearDisjoint (toSubmodule B)

Tactic:
Algebra.toSubmodule_bot

Goal state after:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
B : Subalgebra R S
⊢ Submodule.LinearDisjoint 1 (toSubmodule B)
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
A : Subalgebra R S
⊢ (toSubmodule A).LinearDisjoint (toSubmodule ⊥)

Tactic:
Algebra.toSubmodule_bot

Goal state after:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
A : Subalgebra R S
⊢ (toSubmodule A).LinearDisjoint 1
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
H : A.LinearDisjoint B
H' : A ⊔ B = ⊤
inst✝¹ : Free R ↥B
inst✝ : Module.Finite R ↥B
x : ↥B
⊢ (Algebra.trace (↥A) S) ((algebraMap (↥B) S) x) = (algebraMap R ↥A) ((Algebra.trace R ↥B) x)

Tactic:
Algebra.trace_eq_matrix_trace (Module.Free.chooseBasis R B),

Goal state after:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
H' : A ⊔ B = ⊤
inst✝¹ : Free R ↥B
inst✝ : Module.Finite R ↥B
x : ↥B
⊢ (Algebra.trace (↥A) S) ((algebraMap (↥B) S) x) =
    (algebraMap R ↥A) ((Algebra.leftMulMatrix (Free.chooseBasis R ↥B)) x).trace
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
x y : ↥(toSubmodule A) ⊗[R] ↥(toSubmodule B)
hxy : ((toSubmodule A).mulMap (toSubmodule B)) x = ((toSubmodule A).mulMap (toSubmodule B)) y
M' : Submodule R S
hM : M' ≤ toSubmodule A
hf : Module.Finite R ↥M'
h : {x, y} ⊆ ↑(LinearMap.rTensor (↥(toSubmodule B)) (Submodule.inclusion hM)).range
s : Finset S
hs : Submodule.span R ↑s = M'
hs' : ↑s ⊆ ↑A
A' : Subalgebra R S := Algebra.adjoin R ↑s
hf' : Module.Finite R ↥A'
hA : toSubmodule A' ≤ toSubmodule A
x✝ : ↥(toSubmodule A) ⊗[R] ↥(toSubmodule B)
hx : x✝ ∈ {x, y}
⊢ M' ≤ toSubmodule A'

Tactic:
rw [← hs, Submodule.span_le]

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 y : ↥(toSubmodule A) ⊗[R] ↥(toSubmodule B)
hxy : ((toSubmodule A).mulMap (toSubmodule B)) x = ((toSubmodule A).mulMap (toSubmodule B)) y
M' : Submodule R S
hM : M' ≤ toSubmodule A
hf : Module.Finite R ↥M'
h : {x, y} ⊆ ↑(LinearMap.rTensor (↥(toSubmodule B)) (Submodule.inclusion hM)).range
s : Finset S
hs : Submodule.span R ↑s = M'
hs' : ↑s ⊆ ↑A
A' : Subalgebra R S := Algebra.adjoin R ↑s
hf' : Module.Finite R ↥A'
hA : toSubmodule A' ≤ toSubmodule A
x✝ : ↥(toSubmodule A) ⊗[R] ↥(toSubmodule B)
hx : x✝ ∈ {x, y}
⊢ ↑s ⊆ ↑(toSubmodule A')
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
inst✝ : Algebra.IsSeparable E K
h : Module.rank F ↥(separableClosure F K) = Module.rank E ↥(adjoin E ↑(separableClosure F K))
⊢ sepDegree F K = Module.rank E K

Tactic:
rwa [separableClosure.adjoin_eq_of_isAlgebraic_of_isSeparable K, rank_top'] at h

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
S : Set K
inst✝¹ : IsPurelyInseparable F E
M : IntermediateField F K := adjoin F S
inst✝ : Algebra.IsAlgebraic F ↥M
L : IntermediateField E K := adjoin E S
E' : IntermediateField F K := (IsScalarTower.toAlgHom F E K).fieldRange
j : E ≃ₐ[F] ↥E' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F E K)
hi : M ≤ restrictScalars F L
i : ↥M →+* ↥L := Subsemiring.inclusion hi
this✝¹ : Algebra ↥M ↥L := i.toAlgebra
this✝ : SMul ↥M ↥L := this✝¹.toSMul
this : IsScalarTower F ↥M ↥L
q : ℕ
h✝ : ExpChar F q
| restrictScalars F (adjoin (↥(adjoin F ↑E')) S)

Tactic:
adjoin_adjoin_comm

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 : Set K
inst✝¹ : IsPurelyInseparable F E
M : IntermediateField F K := adjoin F S
inst✝ : Algebra.IsAlgebraic F ↥M
L : IntermediateField E K := adjoin E S
E' : IntermediateField F K := (IsScalarTower.toAlgHom F E K).fieldRange
j : E ≃ₐ[F] ↥E' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F E K)
hi : M ≤ restrictScalars F L
i : ↥M →+* ↥L := Subsemiring.inclusion hi
this✝¹ : Algebra ↥M ↥L := i.toAlgebra
this✝ : SMul ↥M ↥L := this✝¹.toSMul
this : IsScalarTower F ↥M ↥L
q : ℕ
h✝ : ExpChar F q
| restrictScalars F (adjoin ↥(adjoin F S) ↑E')
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

Goal state before:
pp: K : Type u_1
inst✝ : Field K
f : K⟮X⟯
⊢ (f.minpolyX ↥K⟮f⟯).natDegree = max f.num.natDegree f.denom.natDegree

Tactic:
by
  by_cases hf : ∃ c, f = C c
  · obtain ⟨c, rfl⟩ := hf
    simp
  apply le_antisymm
  · have : (f.minpolyX K⟮f⟯).natDegree ≤ _ := natDegree_sub_le _ _
    rw [natDegree_map, natDegree_C_mul fun H ↦ hf ⟨0, by simpa [map_zero] using congr($(H).val)⟩,
      natDegree_map] at this
    exact this
  · exact max_le (natDegree_num_le_natDegree_minpolyX f hf) <| le_natDegree_of_ne_zero
      fun H ↦ hf (f.eq_C_of_minpolyX_coeff_eq_zero congr($(H).val))

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ¬∃ c, f = C c
H : IsAlgebraic K f
this : Algebra.IsAlgebraic K ↥K⟮f⟯
⊢ False

Tactic:
have tr : Algebra.Transcendental K K⟮X⟯ := by infer_instance

Goal state after:
K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ¬∃ c, f = C c
H : IsAlgebraic K f
this : Algebra.IsAlgebraic K ↥K⟮f⟯
tr : Algebra.Transcendental K K⟮X⟯
⊢ False
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 : Set K
inst✝¹ : IsPurelyInseparable F E
M : IntermediateField F K := adjoin F S
inst✝ : Algebra.IsAlgebraic F ↥M
L : IntermediateField E K := adjoin E S
E' : IntermediateField F K := (IsScalarTower.toAlgHom F E K).fieldRange
j : E ≃ₐ[F] ↥E' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F E K)
hi : M ≤ restrictScalars F L
i : ↥M →+* ↥L := Subsemiring.inclusion hi
this✝² : Algebra ↥M ↥L := i.toAlgebra
this✝¹ : SMul ↥M ↥L := this✝².toSMul
this✝ : IsScalarTower F ↥M ↥L
q : ℕ
h✝ : ExpChar F q
this : extendScalars hi = adjoin ↥M ↑E'
x : K
y : E
hy : (IsScalarTower.toAlgHom F E K).toRingHom y = x
n : ℕ
z : F
hz : (algebraMap F E) z = y ^ q ^ n
⊢ (algebraMap E K) y ^ q ^ n = ↑(IsScalarTower.toAlgHom F E K) y ^ q ^ n

Tactic:
IsScalarTower.coe_toAlgHom

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 : Set K
inst✝¹ : IsPurelyInseparable F E
M : IntermediateField F K := adjoin F S
inst✝ : Algebra.IsAlgebraic F ↥M
L : IntermediateField E K := adjoin E S
E' : IntermediateField F K := (IsScalarTower.toAlgHom F E K).fieldRange
j : E ≃ₐ[F] ↥E' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F E K)
hi : M ≤ restrictScalars F L
i : ↥M →+* ↥L := Subsemiring.inclusion hi
this✝² : Algebra ↥M ↥L := i.toAlgebra
this✝¹ : SMul ↥M ↥L := this✝².toSMul
this✝ : IsScalarTower F ↥M ↥L
q : ℕ
h✝ : ExpChar F q
this : extendScalars hi = adjoin ↥M ↑E'
x : K
y : E
hy : (IsScalarTower.toAlgHom F E K).toRingHom y = x
n : ℕ
z : F
hz : (algebraMap F E) z = y ^ q ^ n
⊢ (algebraMap E K) y ^ q ^ n = (algebraMap E K) y ^ q ^ n
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

Goal state before:
pp: K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ¬∃ c, f = C c
this : UniqueFactorizationMonoid ↥K[f]
⊢ (f.minpolyX ↥K[f]).IsPrimitive

Tactic:
apply (f.irreducible_minpolyX' hf).isPrimitive
    intro H
    have := natDegree_map_le (f := algebraMap K[f] K⟮f⟯) (p := f.minpolyX K[f])
    rw [f.minpolyX_map K[f] K⟮f⟯, H, nonpos_iff_eq_zero, f.natDegree_minpolyX,
      Nat.max_eq_zero_iff, ← f.eq_C_iff] at this
    exact hf this

Goal state after:
Module: Mathlib.FieldTheory.Relrank

Goal state before:
pp: E : Type v
inst✝ : Field E
A : Subfield E
⊢ A.relrank ⊤ = Module.rank (↥A) E

Tactic:
by
  rw [relrank_eq_rank_of_le (show A ≤ ⊤ from le_top), extendScalars_top,
    IntermediateField.topEquiv.toLinearEquiv.rank_eq]

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 ≠ ⊥
⊢ Polynomial.C ((algebraMap K[X] K⟮X⟯) (Φ' E).content)⁻¹ * Polynomial.C ((algebraMap K[X] K⟮X⟯) (Φ' E).content) *
      Polynomial.map (algebraMap K[X] K⟮X⟯) (Φ' E).primPart =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (Φ E)

Tactic:
← C_mul,

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ Polynomial.C (((algebraMap K[X] K⟮X⟯) (Φ' E).content)⁻¹ * (algebraMap K[X] K⟮X⟯) (Φ' E).content) *
      Polynomial.map (algebraMap K[X] K⟮X⟯) (Φ' E).primPart =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (Φ E)
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
⊢ Fintype.card (Fin (n + 1)) - #{i} = n - 1 + 1

Tactic:
card_singleton,

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
⊢ Fintype.card (Fin (n + 1)) - 1 = n - 1 + 1
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)
p : P
⊢ line[ℝ, p, s.points i].direction = (s.altitude i).direction ↔
    p ≠ s.points i ∧
      p ∈ affineSpan ℝ (Set.range s.points) ∧ p -ᵥ s.points i ∈ (affineSpan ℝ (s.points '' {i}ᶜ)).directionᗮ

Tactic:
← vsub_right_mem_direction_iff_mem (mem_affineSpan ℝ (Set.mem_range_self i)) p,

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)
p : P
⊢ line[ℝ, p, s.points i].direction = (s.altitude i).direction ↔
    p ≠ s.points i ∧
      p -ᵥ s.points i ∈ (affineSpan ℝ (Set.range s.points)).direction ∧
        p -ᵥ s.points i ∈ (affineSpan ℝ (s.points '' {i}ᶜ)).directionᗮ
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 z : V
h : ℝ ∙ y = ℝ ∙ z
⊢ 2 • o.oangle x y = 2 • o.oangle x z

Tactic:
by
  rw [Submodule.span_singleton_eq_span_singleton] at h
  rcases h with ⟨r, rfl⟩
  exact (o.two_zsmul_oangle_smul_right_of_ne_zero _ _ (Units.ne_zero _)).symm

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

Goal state before:
pp: case a.refine_2.refine_2
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)
hk : ∃ k, k ≠ i ∧ k ≠ j
hs :
  vectorSpan ℝ (Set.range s.points) =
    vectorSpan ℝ (Set.range (s.faceOpposite i).points) ⊔ vectorSpan ℝ (Set.range (s.faceOpposite j).points)
⊢ s.points j -ᵥ s.altitudeFoot j ∈ (vectorSpan ℝ (Set.range (s.faceOpposite j).points))ᗮ

Tactic:
rw [← direction_affineSpan]

Goal state after:
case a.refine_2.refine_2
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)
hk : ∃ k, k ≠ i ∧ k ≠ j
hs :
  vectorSpan ℝ (Set.range s.points) =
    vectorSpan ℝ (Set.range (s.faceOpposite i).points) ⊔ vectorSpan ℝ (Set.range (s.faceOpposite j).points)
⊢ s.points j -ᵥ s.altitudeFoot j ∈ (affineSpan ℝ (Set.range (s.faceOpposite j).points)).directionᗮ
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
hp₁p₂ : p₁ ≠ p₂
this : dist p₁ p₂ = dist p₁ (midpoint ℝ p₁ p₂) + dist (midpoint ℝ p₁ p₂) p₂
⊢ ∠ p₁ (midpoint ℝ p₁ p₂) p₂ = π

Tactic:
by
    rwa [← dist_eq_add_dist_iff_angle_eq_pi (by simpa) (by simpa), dist_comm p₂]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle

Goal state before:
pp: case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : ¬x = 0
⊢ Real.tan (Real.arctan (‖y‖ / ‖x‖)) = ‖y‖ / ‖x‖

Tactic:
Real.tan_arctan

Goal state after:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : ¬x = 0
⊢ ‖y‖ / ‖x‖ = ‖y‖ / ‖x‖
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
⊢ Real.sin (angle x (x + y)) * ‖x + y‖ = ‖y‖

Tactic:
by
  by_cases h0 : x = 0 ∧ y = 0; · simp [h0]
  rw [not_and_or] at h0
  rw [sin_angle_add_of_inner_eq_zero h h0, div_mul_cancel₀]
  rw [← mul_self_ne_zero, norm_add_sq_eq_norm_sq_add_norm_sq_real h]
  refine (ne_of_lt ?_).symm
  rcases h0 with (h0 | h0)
  · exact Left.add_pos_of_pos_of_nonneg (mul_self_pos.2 (norm_ne_zero_iff.2 h0)) (mul_self_nonneg _)
  · exact Left.add_pos_of_nonneg_of_pos (mul_self_nonneg _) (mul_self_pos.2 (norm_ne_zero_iff.2 h0))

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

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
⊢ Real.tan (Real.arctan r) = r

Tactic:
Real.tan_arctan

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
⊢ r = r
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
⊢ Real.tan (Real.arctan r⁻¹) = r⁻¹

Tactic:
Real.tan_arctan

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
⊢ r⁻¹ = r⁻¹
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

Goal state before:
pp: case neg
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r₁ r₂ r₃ r₄ : ℝ
hr₁ : ¬r₁ = 0
⊢ SignType.sign (-r₃ / r₁ * r₂ + r₄) * SignType.sign r₁ * (o.oangle x y).sign =
    SignType.sign (r₁ * r₄ - r₂ * r₃) * (o.oangle x y).sign

Tactic:
← sign_mul,

Goal state after:
case neg
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r₁ r₂ r₃ r₄ : ℝ
hr₁ : ¬r₁ = 0
⊢ SignType.sign ((-r₃ / r₁ * r₂ + r₄) * r₁) * (o.oangle x y).sign =
    SignType.sign (r₁ * r₄ - r₂ * r₃) * (o.oangle x y).sign
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle

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
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : (∡ p₂ p₃ p₁).sign = 1
⊢ Real.sin (∠ p₂ p₃ p₁) * dist p₁ p₃ = dist p₁ p₂

Tactic:
sin_angle_mul_dist_of_angle_eq_pi_div_two (angle_eq_pi_div_two_of_oangle_eq_pi_div_two h)

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : (∡ p₂ p₃ p₁).sign = 1
⊢ dist p₁ p₂ = dist p₁ p₂
Module: Mathlib.Geometry.Euclidean.SignedDist

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 : V
p q r : P
⊢ ((signedDist v) p) q - ((signedDist v) p) r = ((signedDist v) r) q

Tactic:
sub_eq_iff_eq_add',

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
v : V
p q r : P
⊢ ((signedDist v) p) q = ((signedDist v) p) r + ((signedDist v) r) q