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

Goal state before:
pp: case refine_2
F : Type u_1
K : Type u_2
inst✝⁹ : Field F
inst✝⁸ : Field K
inst✝⁷ : Differential F
inst✝⁶ : Differential K
inst✝⁵ : Algebra F K
inst✝⁴ : DifferentialAlgebra F K
inst✝³ : CharZero F
inst✝² : FiniteDimensional F K
inst✝¹ : IsGalois F K
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → K
v : K
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
this : CharZero K
ffb : fixedField ⊤ = ⊥
⊢ (algebraMap F K) a * ↑(Fintype.card Gal(K/F)) = ∑ x, ↑(c x) * logDeriv (∏ x_1, x_1 (u x)) + ∑ x, (x v)′

Tactic:
conv =>
        enter [2, 1, 2, i, 2]
        equals ∑ x : K ≃ₐ[F] K, logDeriv (x (u i)) =>
          by_cases h : u i = 0 <;>
          simp [logDeriv_prod, h]

Goal state after:
case refine_2
F : Type u_1
K : Type u_2
inst✝⁹ : Field F
inst✝⁸ : Field K
inst✝⁷ : Differential F
inst✝⁶ : Differential K
inst✝⁵ : Algebra F K
inst✝⁴ : DifferentialAlgebra F K
inst✝³ : CharZero F
inst✝² : FiniteDimensional F K
inst✝¹ : IsGalois F K
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → K
v : K
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
this : CharZero K
ffb : fixedField ⊤ = ⊥
⊢ (algebraMap F K) a * ↑(Fintype.card Gal(K/F)) = ∑ i, ↑(c i) * ∑ x, logDeriv (x (u i)) + ∑ x, (x v)′
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
x : R
hp✝ : ¬1 < p
x✝ : ∃ n, x ^ p ^ n = 0
n : ℕ
h : x ^ p ^ n = 0
hp : p = 0
hn : ¬n = 0
⊢ x = 0

Tactic:
hp,

Goal state after:
case neg
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
x : R
hp✝ : ¬1 < p
x✝ : ∃ n, x ^ p ^ n = 0
n : ℕ
h : x ^ 0 ^ n = 0
hp : p = 0
hn : ¬n = 0
⊢ x = 0
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: case neg.inr
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
x : R
hp✝ : ¬1 < p
x✝ : ∃ n, x ^ p ^ n = 0
n : ℕ
h : x ^ p ^ n = 0
hp : p = 1
⊢ x = 0

Tactic:
hp,

Goal state after:
case neg.inr
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
x : R
hp✝ : ¬1 < p
x✝ : ∃ n, x ^ p ^ n = 0
n : ℕ
h : x ^ 1 ^ n = 0
hp : p = 1
⊢ x = 0
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: case mp.trans
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x✝ y✝ x y z : ℕ × K
H1 : Relation.EqvGen (R K p) x y
H2 : Relation.EqvGen (R K p) y z
ih1 : ∃ z, (⇑(frobenius K p))^[y.1 + z] x.2 = (⇑(frobenius K p))^[x.1 + z] y.2
ih2 : ∃ z_1, (⇑(frobenius K p))^[z.1 + z_1] y.2 = (⇑(frobenius K p))^[y.1 + z_1] z.2
⊢ ∃ z_1, (⇑(frobenius K p))^[z.1 + z_1] x.2 = (⇑(frobenius K p))^[x.1 + z_1] z.2

Tactic:
obtain ⟨z1, ih1⟩ := ih1

Goal state after:
case mp.trans
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x✝ y✝ x y z : ℕ × K
H1 : Relation.EqvGen (R K p) x y
H2 : Relation.EqvGen (R K p) y z
ih2 : ∃ z_1, (⇑(frobenius K p))^[z.1 + z_1] y.2 = (⇑(frobenius K p))^[y.1 + z_1] z.2
z1 : ℕ
ih1 : (⇑(frobenius K p))^[y.1 + z1] x.2 = (⇑(frobenius K p))^[x.1 + z1] y.2
⊢ ∃ z_1, (⇑(frobenius K p))^[z.1 + z_1] x.2 = (⇑(frobenius K p))^[x.1 + z_1] z.2
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁷ : CommRing K
inst✝⁶ : CommRing L
inst✝⁵ : CommRing M
i : K →+* L
j : K →+* M
p : ℕ
inst✝⁴ : ExpChar M p
inst✝³ : ExpChar K p
inst✝² : PerfectRing M p
inst✝¹ : IsPRadical i p
inst✝ : ExpChar L p
x : K
⊢ (lift i j p) (i x) = j x

Tactic:
rw [lift_apply i j p _ 0 x (by rw [pow_zero, pow_one]), iterateFrobeniusEquiv_zero]

Goal state after:
K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁷ : CommRing K
inst✝⁶ : CommRing L
inst✝⁵ : CommRing M
i : K →+* L
j : K →+* M
p : ℕ
inst✝⁴ : ExpChar M p
inst✝³ : ExpChar K p
inst✝² : PerfectRing M p
inst✝¹ : IsPRadical i p
inst✝ : ExpChar L p
x : K
⊢ (RingEquiv.refl M).symm (j x) = j x
Module: Mathlib.GroupTheory.CosetCover

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

Tactic:
hind,

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

Goal state before:
pp: case inl
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✝ : Finite F
⊢ ∃ ω, ⊤ ≤ M ω

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:
· have ⟨α, hα⟩ := exists_primitive_element_of_finite_bot F FS
      have ⟨ω, hω⟩ := Set.mem_iUnion.mp (this ▸ Set.mem_univ α)
      exact ⟨ω, show ⊤ ≤ K₀.comap ω by rwa [← hα, adjoin_simple_le_iff]⟩

Goal state after:
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 ω
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: case ind
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq (Subgroup G)
n : ℕ
ih :
  ∀ m < n,
    ∀ {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι},
      ⋃ i ∈ s, g i • ↑(H i) = Set.univ →
        ∀ j ∈ s,
          ⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H i) ≠ Set.univ →
            m = (Finset.image H s).card → ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
j : ι
hj : j ∈ s
hcovers' : ⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H i) ≠ Set.univ
hn : n = (Finset.image H s).card
x : G
hx : ∀ i ∈ s, H i = H j → ↑(g i) ≠ ↑x
⊢ ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex

Tactic:
replace hx : ∀ (y : G), y • (H j : Set G) ⊆
        ⋃ i ∈ s.filter (H · ≠ H j), (y * x⁻¹ * g i) • (H i : Set G) := by
      intro y z hz
      simp_rw [Finset.mem_filter, Set.mem_iUnion]
      have ⟨i, hi, hmem⟩ : ∃ i ∈ s, x * (y⁻¹ * z) ∈ g i • (H i : Set G) := by
        simpa using Set.eq_univ_iff_forall.mp hcovers (x * (y⁻¹ * z))
      rw [mem_leftCoset_iff, SetLike.mem_coe, ← QuotientGroup.eq] at hmem
      refine ⟨i, ⟨hi, fun hij => hx i hi hij ?_⟩, ?_⟩
      · rwa [hmem, eq_comm, QuotientGroup.eq, hij, inv_mul_cancel_left,
          ← SetLike.mem_coe, ← mem_leftCoset_iff]
      · simpa [mem_leftCoset_iff, SetLike.mem_coe, QuotientGroup.eq, mul_assoc] using hmem

Goal state after:
case ind
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq (Subgroup G)
n : ℕ
ih :
  ∀ m < n,
    ∀ {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι},
      ⋃ i ∈ s, g i • ↑(H i) = Set.univ →
        ∀ j ∈ s,
          ⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H i) ≠ Set.univ →
            m = (Finset.image H s).card → ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
j : ι
hj : j ∈ s
hcovers' : ⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H i) ≠ Set.univ
hn : n = (Finset.image H s).card
x : G
hx : ∀ (y : G), y • ↑(H j) ⊆ ⋃ i ∈ {x ∈ s | H x ≠ H j}, (y * x⁻¹ * g i) • ↑(H i)
⊢ ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
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
⊢ a * d - d * a = a

Tactic:
nth_rw 3 [← mul_one a]

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
⊢ a * d - d * a = a * 1
Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality

Goal state before:
pp: case h₂
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A B : IntermediateField F E
hA : Algebra.Transcendental F ↥A
hB : Algebra.Transcendental F ↥B
this✝¹ : Algebra.Transcendental F ↥(A ⊔ B)
this✝ : Infinite ↥A
this : Infinite ↥B
⊢ #↑(↑A ∪ ↑B) ≤ max #↥A #↥B

Tactic:
exact (mk_union_le _ _).trans_eq (by simp)

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
⊢ Function.LeftInverse (AdjoinRootXPowSubCEquivToRootsOfUnity hζ H) (↑(autAdjoinRootXPowSubC n a)).toFun

Tactic:
by
    intro η
    have := Fact.mk H
    have : IsDomain K[n√a] := inferInstance
    let : Algebra K K[n√a] := inferInstance
    apply (rootsOfUnityEquivOfPrimitiveRoots (algebraMap K K[n√a]).injective hζ).injective
    ext
    simp only [AdjoinRoot.algebraMap_eq, OneHom.toFun_eq_coe, MonoidHom.toOneHom_coe,
      autAdjoinRootXPowSubC_root, Algebra.smul_def, MulEquiv.apply_symm_apply,
      rootsOfUnity.val_mkOfPowEq_coe, val_rootsOfUnityEquivOfPrimitiveRoots_apply_coe,
      AdjoinRootXPowSubCEquivToRootsOfUnity]
    split_ifs with h
    · obtain rfl := not_imp_not.mp (fun hn ↦ ne_zero_of_irreducible_X_pow_sub_C' hn H) h
      have : (η : Kˣ) = 1 := (pow_one _).symm.trans η.prop
      simp only [this, Units.val_one, map_one]
    · exact mul_div_cancel_right₀ _ (root_X_pow_sub_C_ne_zero' (NeZero.pos n) h)

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)
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ n - C a)
⊢ Module.finrank K L = n

Tactic:
have := Polynomial.IsSplittingField.finiteDimensional L (X ^ n - C a)

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)
this : FiniteDimensional K L
⊢ Module.finrank K L = n
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 y H

Goal state after:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x y : ConjRootClass K L
H : x.carrier = y.carrier
⊢ x = y
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
c : ConjRootClass K L
x✝ : L
⊢ x✝ ∈ (-c).carrier ↔ x✝ ∈ -c.carrier

Tactic:
simp [mem_carrier, ← mk_neg, neg_eq_iff_eq_neg]

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

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

Tactic:
induction c
  induction d
  simp [isConjRoot_def]

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Semiring T
inst✝ : Algebra R T
x : S
y : T
⊢ (_root_.TensorProduct.map includeLeft.toLinearMap.rangeRestrict includeRight.toLinearMap.rangeRestrict)
      (↑⟨x ⊗ₜ[R] 1, ⋯⟩ * ↑⟨1 ⊗ₜ[R] y, ⋯⟩) =
    ⟨x ⊗ₜ[R] 1, ⋯⟩ ⊗ₜ[R] ⟨1 ⊗ₜ[R] y, ⋯⟩

Tactic:
rw [tmul_mul_tmul, mul_one, one_mul, _root_.TensorProduct.map_tmul]

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Semiring T
inst✝ : Algebra R T
x : S
y : T
⊢ includeLeft.toLinearMap.rangeRestrict x ⊗ₜ[R] includeRight.toLinearMap.rangeRestrict y =
    ⟨x ⊗ₜ[R] 1, ⋯⟩ ⊗ₜ[R] ⟨1 ⊗ₜ[R] y, ⋯⟩
Module: Mathlib.FieldTheory.PurelyInseparable.Exponent

Goal state before:
pp: F : Type u_1
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 b : L
inj : Function.Injective ⇑(algebraMap K L)
this : ExpChar L p
⊢ (a + b) ^ p ^ n = a ^ p ^ n + b ^ p ^ n

Tactic:
add_pow_expChar_pow a b

Goal state after:
F : Type u_1
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 b : L
inj : Function.Injective ⇑(algebraMap K L)
this : ExpChar L p
⊢ a ^ p ^ n + b ^ p ^ n = a ^ p ^ n + b ^ 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
S : Set E
inst✝¹ : Algebra.IsSeparable F ↥(adjoin F S)
q : ℕ
inst✝ : ExpChar F q
n : ℕ
M : IntermediateField F E := adjoin F ((fun x ↦ x ^ q ^ n) '' S)
⊢ adjoin F S = M

Tactic:
have := expChar_of_injective_algebraMap (algebraMap F M).injective q

Goal state after:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
S : Set E
inst✝¹ : Algebra.IsSeparable F ↥(adjoin F S)
q : ℕ
inst✝ : ExpChar F q
n : ℕ
M : IntermediateField F E := adjoin F ((fun x ↦ x ^ q ^ n) '' S)
this : ExpChar (↥M) q
⊢ adjoin F S = M
Module: Mathlib.Geometry.Convex.Cone.Face.Basic

Goal state before:
pp: case h
R : Type u_1
M : Type u_2
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
inst✝³ : IsOrderedRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
C F : PointedCone R M
ι : Type u_4
inst✝ : Fintype ι
f : ι → M
c : ι → R
hF : F.IsFaceOf C
hsC : ∀ (i : ι), f i ∈ C
hc : ∀ (i : ι), 0 ≤ c i
hs : ∑ i, c i • f i ∈ F
i : ι
hci : 0 < c i
⊢ i ∉ Finset.univ → c i • f i = 0

Tactic:
· simp

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

Goal state before:
pp: case e'_3
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
⊢ LinearMap.id x = 1 • x

Tactic:
· 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 : P
⊢ nndist p ↑((orthogonalProjection s) p) = Metric.infNndist p ↑s

Tactic:
← NNReal.coe_inj

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
⊢ ↑(nndist p ↑((orthogonalProjection s) p)) = ↑(Metric.infNndist p ↑s)
Module: Mathlib.Geometry.Euclidean.Altitude

Goal state before:
pp: case mpr.refine_2
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}.toFinset = 1

pp: case mpr.refine_2
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
⊢ LinearIndepOn ℝ id {p -ᵥ s.points i}

Tactic:
· simp

Goal state after:
case mpr.refine_2
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
⊢ LinearIndepOn ℝ id {p -ᵥ s.points i}
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 x (-y) + o.oangle (-y) x = 0

Tactic:
oangle_rev,

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

Goal state before:
pp: case mpr
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : ‖x‖ = ‖y‖
⊢ (o.rotation (o.oangle x y)) x = y

Tactic:
rw [o.eq_iff_oangle_eq_zero_of_norm_eq] <;> simp [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 x y = 0 ↔ o.oangle y x = 0

Tactic:
oangle_rev,

Goal state after:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ -o.oangle y x = 0 ↔ o.oangle y x = 0
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 x y = ↑π ↔ o.oangle y x = ↑π

Tactic:
oangle_rev,

Goal state after:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ -o.oangle y x = ↑π ↔ o.oangle y x = ↑π
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
hkj' : s.points k ∈ Set.range (s.faceOpposite j).points
⊢ j ∉ {i}

Tactic:
simpa using hij.symm

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

Goal state before:
pp: case h.«0»
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
f : V ≃ₗᵢ[ℝ] V
hd : 0 < LinearMap.det ↑f.toLinearEquiv
this : Nontrivial V
x : V
hx : x ≠ 0
⊢ ↑(o.rotation (o.oangle x (f x))).toLinearEquiv ((o.basisRightAngleRotation x hx) ((fun i ↦ i) ⟨0, ⋯⟩)) =
    ↑f.toLinearEquiv ((o.basisRightAngleRotation x hx) ((fun i ↦ i) ⟨0, ⋯⟩))

pp: case h.«1»
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
f : V ≃ₗᵢ[ℝ] V
hd : 0 < LinearMap.det ↑f.toLinearEquiv
this : Nontrivial V
x : V
hx : x ≠ 0
⊢ ↑(o.rotation (o.oangle x (f x))).toLinearEquiv ((o.basisRightAngleRotation x hx) ((fun i ↦ i) ⟨1, ⋯⟩)) =
    ↑f.toLinearEquiv ((o.basisRightAngleRotation x hx) ((fun i ↦ i) ⟨1, ⋯⟩))

Tactic:
· simp

Goal state after:
case h.«1»
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
f : V ≃ₗᵢ[ℝ] V
hd : 0 < LinearMap.det ↑f.toLinearEquiv
this : Nontrivial V
x : V
hx : x ≠ 0
⊢ ↑(o.rotation (o.oangle x (f x))).toLinearEquiv ((o.basisRightAngleRotation x hx) ((fun i ↦ i) ⟨1, ⋯⟩)) =
    ↑f.toLinearEquiv ((o.basisRightAngleRotation x hx) ((fun i ↦ i) ⟨1, ⋯⟩))
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

Goal state before:
pp: case refine_2.inl
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
y : V
⊢ SameRay ℝ 0 y ∨ 0 ≠ 0 ∧ y ≠ 0 ∧ SameRay ℝ 0 (-y)

pp: case refine_2.inr
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
r : ℝ
⊢ SameRay ℝ x (r • x) ∨ x ≠ 0 ∧ r • x ≠ 0 ∧ SameRay ℝ x (-(r • x))

Tactic:
· simp

Goal state after:
case refine_2.inr
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
r : ℝ
⊢ SameRay ℝ x (r • x) ∨ x ≠ 0 ∧ r • x ≠ 0 ∧ SameRay ℝ x (-(r • x))
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
⊢ |⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫| < |s.height i * s.height j|

Tactic:
nth_rw 2 [abs_eq_self.2]

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
⊢ |⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫| < s.height i * s.height j

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
⊢ 0 ≤ s.height i * s.height j