mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: case intro.intro.mpr
M : Type w
A : Set M
L : Language
inst✝² : L.Structure M
α : Type u₁
β : Type u_1
s : Set (β → M)
h✝ : A.Definable L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  A.Definable L
    ((fun g ↦ g ∘ rangeSplitting f) ⁻¹'
      (fun g ↦ g ∘ Sum.inl) ''
        (fun g ↦ g ∘ ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ''
          (fun g ↦ g ∘ ⇑(Equiv.Set.sumCompl (range f))) '' s)
h' : A.Definable L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
x : α → M
⊢ (∃ x_1 ∈ s, x_1 ∘ f = x) →
    (∃ a ∈ s,
        ((a ∘ ⇑(Equiv.Set.sumCompl (range f))) ∘
              ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ∘
            Sum.inl =
          x ∘ rangeSplitting f) ∧
      ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))

Tactic:
rintro ⟨y, ys, rfl⟩
      refine ⟨⟨y, ys, ?_⟩, fun a => ?_⟩
      · ext
        simp [Set.apply_rangeSplitting f]
      · rw [Function.comp_apply, Function.comp_apply, apply_rangeSplitting f,
          rangeFactorization_coe]

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type u_1
L : Language
inst✝ : L.Structure M
α : Type u_2
A : Set M
f g : (α → M) → M
hf : DefinableFun L A f
hg : DefinableFun L A g
⊢ A.Definable L {v | f v = g v}

Tactic:
by
  have hF : A.DefinableMap L (fun v => ![f v, g v]) := by
    simp [DefinableMap, *]
  exact (Definable.diagonal L A).preimage_map hF

Goal state after:
Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed

Goal state before:
pp: case inl
φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : ↑T0 ⊆ Theory.ACF 0
h✝ : ↑T0 ⊨ᵇ φ
ψ : Language.ring.Sentence
h : ψ ∈ Theory.field ∪ genericMonicPolyHasRoot '' {n | 0 < n}
⊢ Nonempty { s // ∀ q ∉ s, Theory.ACF ↑q ⊨ᵇ ψ }

Tactic:
refine ⟨⟨∅, ?_⟩⟩
      intro q _
      exact Theory.models_sentence_of_mem
        (by rw [Theory.ACF, Theory.fieldOfChar, Set.union_right_comm];
            exact Set.mem_union_left _ h)

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: case mpr
L : Language
T : L.Theory
h : ∀ (M N : T.ModelType), ↑M ≅[L] ↑N
φ : L.Sentence
M : T.ModelType
⊢ T ⊨ᵇ φ ∨ T ⊨ᵇ Formula.not φ

Tactic:
(«tacticBy_cases_:_»
 "by_cases"
 [`hφ ":"]
 (choice (FirstOrder.Language.«term_⊨__1» `M "⊨" `φ) (FirstOrder.Language.«term_⊨_» `M "⊨" `φ)))

Goal state after:
case pos
L : Language
T : L.Theory
h : ∀ (M N : T.ModelType), ↑M ≅[L] ↑N
φ : L.Sentence
M : T.ModelType
hφ : ↑M ⊨ φ
⊢ T ⊨ᵇ φ ∨ T ⊨ᵇ Formula.not φ

case neg
L : Language
T : L.Theory
h : ∀ (M N : T.ModelType), ↑M ≅[L] ↑N
φ : L.Sentence
M : T.ModelType
hφ : ¬↑M ⊨ φ
⊢ T ⊨ᵇ φ ∨ T ⊨ᵇ Formula.not φ
Module: Mathlib.FieldTheory.AxGrothendieck

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝¹ : Finite α
inst✝ : Finite ι
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
⊢ {p | Theory.ACF ↑p ⊨ᵇ genericPolyMapSurjOnOfInjOn φ mons} = Set.univ

Tactic:
rw [Set.eq_univ_iff_forall]

Goal state after:
ι : Type u_1
α : Type u_2
inst✝¹ : Finite α
inst✝ : Finite ι
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
⊢ ∀ (x : Nat.Primes), x ∈ {p | Theory.ACF ↑p ⊨ᵇ genericPolyMapSurjOnOfInjOn φ mons}
Module: Mathlib.FieldTheory.Differential.Basic

Goal state before:
pp: case inj.h0
R : Type u_1
inst✝⁷ : Field R
inst✝⁶ : Differential R
a✝ b : R
F : Type u_2
inst✝⁵ : Field F
inst✝⁴ : Differential F
inst✝³ : CharZero F
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F K
default : { _a // DifferentialAlgebra F K } := ⋯
x✝ : { _a // DifferentialAlgebra F K }
a : Differential K
ha : DifferentialAlgebra F K
x : K
this : 0 < (minpoly F x).natDegree
⊢ derivative (minpoly F x) ≠ 0

pp: case hl
R : Type u_1
inst✝⁷ : Field R
inst✝⁶ : Differential R
a✝ b : R
F : Type u_2
inst✝⁵ : Field F
inst✝⁴ : Differential F
inst✝³ : CharZero F
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F K
default : { _a // DifferentialAlgebra F K } := ⋯
x✝ : { _a // DifferentialAlgebra F K }
a : Differential K
ha : DifferentialAlgebra F K
x : K
this : 0 < (minpoly F x).natDegree
⊢ (derivative (minpoly F x)).natDegree < (minpoly F x).natDegree

Tactic:
· intro nh
      simp_all

Goal state after:
case hl
R : Type u_1
inst✝⁷ : Field R
inst✝⁶ : Differential R
a✝ b : R
F : Type u_2
inst✝⁵ : Field F
inst✝⁴ : Differential F
inst✝³ : CharZero F
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F K
default : { _a // DifferentialAlgebra F K } := ⋯
x✝ : { _a // DifferentialAlgebra F K }
a : Differential K
ha : DifferentialAlgebra F K
x : K
this : 0 < (minpoly F x).natDegree
⊢ (derivative (minpoly F x)).natDegree < (minpoly F x).natDegree
Module: Mathlib.FieldTheory.Finite.Polynomial

Goal state before:
pp: σ K : Type u
inst✝² : Fintype K
inst✝¹ : Field K
inst✝ : Finite σ
p : MvPolynomial σ K
h : ∀ (v : σ → K), (eval v) p = 0
hp : p ∈ restrictDegree σ K (Fintype.card K - 1)
p' : R σ K := ⟨p, hp⟩
this : p' ∈ (evalᵢ σ K).ker
⊢ p' = 0

Tactic:
by rwa [ker_evalₗ, mem_bot] at this

Goal state after:
Module: Mathlib.FieldTheory.Galois.NormalBasis

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Infinite K
e : Module.Basis (Module.Free.ChooseBasisIndex K L) K L
M : Matrix Gal(L/K) Gal(L/K) (MvPolynomial (Module.Free.ChooseBasisIndex K L) L) :=
  Matrix.of fun i j ↦ ∑ k, i.symm (j (e k)) • MvPolynomial.X k
hq : Submodule.span L (Set.range fun k j ↦ j (e k)) = ⊤
c : Module.Free.ChooseBasisIndex K L → L
hc : (MvPolynomial.eval c) M.det = 1
hM : M.det ≠ 0
b : Module.Free.ChooseBasisIndex K L → K
hb : (M.map ⇑(MvPolynomial.eval (⇑(algebraMap K L) ∘ b))).det ≠ 0
a : Gal(L/K) → K
ha : ∑ i, a i • i (∑ k, b k • e k) = 0
⊢ (fun x ↦ (algebraMap K L) (a x)) = fun x ↦ 0

Tactic:
refine Matrix.eq_zero_of_mulVec_eq_zero hb (funext fun i ↦ i.injective ?_)

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Infinite K
e : Module.Basis (Module.Free.ChooseBasisIndex K L) K L
M : Matrix Gal(L/K) Gal(L/K) (MvPolynomial (Module.Free.ChooseBasisIndex K L) L) :=
  Matrix.of fun i j ↦ ∑ k, i.symm (j (e k)) • MvPolynomial.X k
hq : Submodule.span L (Set.range fun k j ↦ j (e k)) = ⊤
c : Module.Free.ChooseBasisIndex K L → L
hc : (MvPolynomial.eval c) M.det = 1
hM : M.det ≠ 0
b : Module.Free.ChooseBasisIndex K L → K
hb : (M.map ⇑(MvPolynomial.eval (⇑(algebraMap K L) ∘ b))).det ≠ 0
a : Gal(L/K) → K
ha : ∑ i, a i • i (∑ k, b k • e k) = 0
i : Gal(L/K)
⊢ i ((M.map ⇑(MvPolynomial.eval (⇑(algebraMap K L) ∘ b))).mulVec (fun x ↦ (algebraMap K L) (a x)) i) = i (0 i)
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : CommSemiring K
inst✝¹ : CommSemiring L
i : K →+* L
p : ℕ
inst✝ : IsPRadical i p
⊢ Ideal.comap i (pNilradical L p) = pNilradical K p

Tactic:
by
  refine le_antisymm (fun x h ↦ mem_pNilradical.2 ?_) (fun x h ↦ ?_)
  · obtain ⟨n, h⟩ := mem_pNilradical.1 <| Ideal.mem_comap.1 h
    obtain ⟨m, h⟩ := mem_pNilradical.1 <| ker_le i p ((map_pow i x _).symm ▸ h)
    exact ⟨n + m, by rwa [pow_add, pow_mul]⟩
  simp only [Ideal.mem_comap, mem_pNilradical] at h ⊢
  obtain ⟨n, h⟩ := h
  exact ⟨n, by simpa only [map_pow, map_zero] using congr(i $h)⟩

Goal state after:
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ ProfiniteGrp.{max v u}
a✝ b✝ : (j : J) → ↑(F.obj j).toProfinite.toTop
hx : a✝ ∈ {x | ∀ ⦃i j : J⦄ (π : i ⟶ j), (Hom.hom (F.map π)) (x i) = x j}
hy : b✝ ∈ {x | ∀ ⦃i j : J⦄ (π : i ⟶ j), (Hom.hom (F.map π)) (x i) = x j}
x✝¹ x✝ : J
π : x✝¹ ⟶ x✝
⊢ (Hom.hom (F.map π)) ((a✝ * b✝) x✝¹) = (a✝ * b✝) x✝

Tactic:
by simp only [Pi.mul_apply, map_mul, hx π, hy π]

Goal state after:
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
n : ℕ
h : (iterateFrobenius K p n) x = 0
⊢ x ∈ pNilradical K p

Tactic:
exact mem_pNilradical.2 ⟨n, h⟩

Goal state after:
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
α : ↥FS
hα : F⟮α⟯ = ⊤
⊢ ∃ ω, ⊤ ≤ M ω

Tactic:
have ⟨ω, hω⟩ := Set.mem_iUnion.mp (this ▸ Set.mem_univ α)

Goal state after:
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
α : ↥FS
hα : F⟮α⟯ = ⊤
ω : Ω
hω : α ∈ ↑(M ω)
⊢ ∃ ω, ⊤ ≤ M ω
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
m : ℕ
hm2 : ∀ (n : ℕ), p ^ m ≤ n → (⇑((ad (↥k) D) a))^[n] = 0
⊢ (⇑((ad (↥k) D) a))^[p ^ m + 1] b = 0

Tactic:
hm2 (p ^ m + 1) (Nat.le_add_right _ _),

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
m : ℕ
hm2 : ∀ (n : ℕ), p ^ m ≤ n → (⇑((ad (↥k) D) a))^[n] = 0
⊢ 0 b = 0
Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
ι : Type w
x : ι → E
inst✝ : Nonempty ι
hx : IsTranscendenceBasis F x
K : IntermediateField F E := IntermediateField.adjoin F (range x)
this : Algebra.IsAlgebraic (↥K) E
⊢ max (max (lift.{max w v, u} #F) (lift.{max u v, w} #ι)) (lift.{v, max u w} ℵ₀) *
      lift.{max u w, v} (Module.rank (↥K) E) =
    max (max (lift.{max v w, u} #F) (lift.{max u v, w} #ι)) ℵ₀

Tactic:
lift_aleph0

Goal state after:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
ι : Type w
x : ι → E
inst✝ : Nonempty ι
hx : IsTranscendenceBasis F x
K : IntermediateField F E := IntermediateField.adjoin F (range x)
this : Algebra.IsAlgebraic (↥K) E
⊢ max (max (lift.{max w v, u} #F) (lift.{max u v, w} #ι)) ℵ₀ * lift.{max u w, v} (Module.rank (↥K) E) =
    max (max (lift.{max v w, u} #F) (lift.{max u v, w} #ι)) ℵ₀
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
⊢ eval₂ (↑(Algebra.ofId K L)) α (X ^ n - C a) = 0

Tactic:
simp [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)
inst✝ : NeZero n
η : ↥(rootsOfUnity n K)
⊢ ((autEquivRootsOfUnity hζ H L).symm η) (rootOfSplitsXPowSubC ⋯ a L) =
    (autEquivRootsOfUnity hζ H L) ((autEquivRootsOfUnity hζ H L).symm η) • rootOfSplitsXPowSubC ⋯ a L

Tactic:
rw [MulEquiv.apply_symm_apply, autEquivRootsOfUnity]

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)
inst✝ : NeZero n
η : ↥(rootsOfUnity n K)
⊢ (((adjoinRootXPowSubCEquiv hζ H ⋯).symm.autCongr.trans (autAdjoinRootXPowSubCEquiv hζ H).symm).symm η)
      (rootOfSplitsXPowSubC ⋯ a L) =
    η • rootOfSplitsXPowSubC ⋯ a L
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
inst✝ : NeZero n
σ : Gal(L/K)
⊢ (autEquivRootsOfUnity hζ H L) σ • α = σ α

Tactic:
by
  have ⟨ζ, hζ'⟩ := hζ
  have hn := NeZero.pos n
  rw [mem_primitiveRoots hn] at hζ'
  rw [← mem_nthRoots hn, (hζ'.map_of_injective (algebraMap K L).injective).nthRoots_eq
    (rootOfSplitsXPowSubC_pow a L)] at hα
  simp only [Multiset.mem_map, Multiset.mem_range] at hα
  obtain ⟨i, _, rfl⟩ := hα
  simp only [← map_pow, ← Algebra.smul_def, map_smul,
    autEquivRootsOfUnity_apply_rootOfSplit hζ H L]
  exact smul_comm _ _ _

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

Goal state before:
pp: case h
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsAlgebraic K L
x✝ : L
⊢ Irreducible (minpoly K x✝)

Tactic:
exact minpoly.irreducible (Algebra.IsIntegral.isIntegral _)

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

Goal state before:
pp: K : Type u
inst✝ : Field K
⊢ intDegree 0 = 0

Tactic:
by
  rw [intDegree, num_zero, natDegree_zero, denom_zero, natDegree_one, sub_self]

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

Goal state before:
pp: F : Type u
E : Type v
inst✝⁸ : Field F
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
K : Type w
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra E K
inst✝² : IsScalarTower F E K
inst✝¹ : IsPurelyInseparable F E
S : IntermediateField F K
inst✝ : Algebra.IsSeparable F ↥S
ι : Set ↥S
b : Module.Basis (↑ι) F ↥S
i : ↑ι
⊢ IsSeparable F ((⇑S.val ∘ ⇑b) i)

Tactic:
simpa only [IsSeparable, minpoly_eq] using! Algebra.IsSeparable.isSeparable F (b i)

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

Goal state before:
pp: F : Type u
E : Type v
inst✝⁸ : Field F
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
K : Type w
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra E K
inst✝² : IsScalarTower F E K
inst✝¹ : IsPurelyInseparable F E
inst✝ : Algebra.IsSeparable E K
⊢ sepDegree F K = Module.rank E K

Tactic:
have h := (separableClosure F K).linearDisjoint_of_isPurelyInseparable_of_isSeparable E
    |>.adjoin_rank_eq_rank_left_of_isAlgebraic_left |>.symm

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
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
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✝ : Algebra.IsAlgebraic F E
h :
  Cardinal.lift.{w, v} (Module.rank (↥(separableClosure F E)) E) * Cardinal.lift.{v, w} (insepDegree E K) =
    Cardinal.lift.{v, w} (insepDegree (↥(separableClosure F E)) K)
⊢ Cardinal.lift.{w, v} (insepDegree F E) * Cardinal.lift.{v, w} (insepDegree E K) =
    Cardinal.lift.{v, w} (insepDegree F K)

Tactic:
← insepDegree_eq_of_isSeparable F (separableClosure F E) K

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✝ : Algebra.IsAlgebraic F E
h :
  Cardinal.lift.{w, v} (Module.rank (↥(separableClosure F E)) E) * Cardinal.lift.{v, w} (insepDegree E K) =
    Cardinal.lift.{v, w} (insepDegree F K)
⊢ Cardinal.lift.{w, v} (insepDegree F E) * Cardinal.lift.{v, w} (insepDegree E K) =
    Cardinal.lift.{v, w} (insepDegree F K)
Module: Mathlib.FieldTheory.Relrank

Goal state before:
pp: E : Type v
inst✝ : Field E
A B C : Subfield E
⊢ A.relrank (B ⊓ C) * B.relrank C = (A ⊓ B).relrank C

Tactic:
rw [← inf_relrank_right A (B ⊓ C), ← inf_relrank_right B C, ← inf_relrank_right (A ⊓ B) C,
    inf_assoc, relrank_mul_relrank inf_le_right inf_le_right]

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 :
  (algebraMap K[X] K⟮X⟯) ((Φ E).coeff (generatorIndex h) * g E) = (algebraMap K[X] K⟮X⟯) ((c E).num * (generator E).num)
⊢ (f E).natDegree ≤ ((Φ E).coeff (generatorIndex h)).natDegree

Tactic:
replace this := congr($(algebraMap_injective K this).natDegree)

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
this : ((Φ E).coeff (generatorIndex h) * g E).natDegree = ((c E).num * (generator E).num).natDegree
⊢ (f E).natDegree ≤ ((Φ E).coeff (generatorIndex h)).natDegree
Module: Mathlib.Geometry.Convex.Hull

Goal state before:
pp: R : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : ConvexSpace R X
inst✝ : ConvexSpace R Y
f : X → Y
hf : IsAffineMap R f
s : Set X
⊢ s ⊆ f ⁻¹' (convexHull R) (f '' s) ∧ (convexHull R) (f '' s) ⊆ f '' (convexHull R) s

Tactic:
← image_subset_iff,

Goal state after:
R : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : ConvexSpace R X
inst✝ : ConvexSpace R Y
f : X → Y
hf : IsAffineMap R f
s : Set X
⊢ f '' s ⊆ (convexHull R) (f '' s) ∧ (convexHull R) (f '' s) ⊆ f '' (convexHull R) s
Module: Mathlib.Geometry.Euclidean.Projection

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

Tactic:
orthogonalProjection_eq_orthogonalProjection_iff_vsub_mem

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₁ s₂ : AffineSubspace 𝕜 P
inst✝³ : Nonempty ↥s₁
inst✝² : Nonempty ↥s₂
inst✝¹ : s₁.direction.HasOrthogonalProjection
inst✝ : s₂.direction.HasOrthogonalProjection
h : s₁ ≤ s₂
p : P
⊢ ↑((orthogonalProjection s₂) p) -ᵥ p ∈ s₁.directionᗮ
Module: Mathlib.Geometry.Euclidean.Altitude

Goal state before:
pp: case mp.right
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
h : vectorSpan ℝ {p, s.points i} = (s.altitude i).direction
⊢ p -ᵥ s.points i ∈ vectorSpan ℝ {p, s.points i}

Tactic:
exact
        vsub_mem_vectorSpan ℝ (Set.mem_insert _ _) (Set.mem_insert_of_mem _ (Set.mem_singleton _))

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 = ↑π ↔ x ≠ 0 ∧ y ≠ 0 ∧ SameRay ℝ x (-y)

Tactic:
rw [← o.oangle_eq_zero_iff_sameRay]
  constructor
  · intro h
    by_cases hx : x = 0; · simp [hx, Real.Angle.pi_ne_zero.symm] at h
    by_cases hy : y = 0; · simp [hy, Real.Angle.pi_ne_zero.symm] at h
    refine ⟨hx, hy, ?_⟩
    rw [o.oangle_neg_right hx hy, h, Real.Angle.coe_pi_add_coe_pi]
  · rintro ⟨hx, hy, h⟩
    rwa [o.oangle_neg_right hx hy, ← Real.Angle.sub_coe_pi_eq_add_coe_pi, sub_eq_zero] at h

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₄ : P
h : ∠ p₂ p₃ p₄ = π
⊢ ∠ p₁ p₂ p₃ = ∠ p₁ p₂ p₄

Tactic:
by
  unfold angle at *
  rcases angle_eq_pi_iff.1 h with ⟨_, ⟨r, ⟨hr, hpr⟩⟩⟩
  rw [eq_comm]
  replace hpr : (-r + 1) • (p₃ -ᵥ p₂) = p₄ -ᵥ p₂ := by
    rw [add_smul, ← neg_vsub_eq_vsub_rev p₂ p₃, smul_neg, neg_smul, ← hpr]
    simp
  replace hr : 0 < -r + 1 := by linarith
  exact angle_smul_right_of_pos p₁ hr hpr

Goal state after:
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.arccos (‖x‖ / ‖x + y‖) ≤ π / 2

Tactic:
Real.arccos_le_pi_div_two

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
⊢ 0 ≤ ‖x‖ / ‖x + y‖
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine

Goal state before:
pp: case neg
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₁ p₂ ((AffineEquiv.pointReflection ℝ p₂) p₃) = π - ∠ p₁ p₂ p₃

Tactic:
rw [eq_sub_iff_add_eq]

Goal state after:
case neg
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₁ p₂ ((AffineEquiv.pointReflection ℝ p₂) p₃) + ∠ p₁ p₂ p₃ = π
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

Goal state before:
pp: case neg.refine_1
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : ¬x = 0
hy : ¬y = 0
h : o.oangle x y = ↑(π / 2) ∨ o.oangle x y = ↑(-π / 2)
⊢ InnerProductGeometry.angle x y = π / 2

Tactic:
rwa [o.angle_eq_abs_oangle_toReal hx hy, Real.Angle.abs_toReal_eq_pi_div_two_iff]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₃' : P
h : Wbtw ℝ p₂ p₃ p₃'
hp₃p₂ : p₃ ≠ p₂
⊢ ∡ p₁ p₂ p₃ = ∡ p₁ p₂ p₃'

Tactic:
rw [oangle_rev, h.oangle_eq_left hp₃p₂, ← oangle_rev]

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 y : V
h : o.oangle x y = ↑(π / 2)
hs : (o.oangle y (y - x)).sign = 1
⊢ (o.oangle y (y - x)).sin * ‖y - x‖ = ‖x‖

Tactic:
rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.sin_coe,
    InnerProductGeometry.sin_angle_sub_mul_norm_of_inner_eq_zero
      (o.inner_rev_eq_zero_of_oangle_eq_pi_div_two h)]

Goal state after: