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

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
n : ℕ
⊢ (∃ xs,
      ∀
        φ ∈
          List.map (fun ij ↦ ∼((var ∘ Sum.inr) ij.1 =' (var ∘ Sum.inr) ij.2))
            (List.filter (fun ij ↦ decide (ij.1 ≠ ij.2)) (List.finRange n ×ˢ List.finRange n)),
        φ.Realize default xs) ↔
    Nonempty (Fin n ↪ M)

Tactic:
simp only [Function.comp_apply, List.mem_map, Prod.exists, Ne, List.mem_product,
    List.mem_finRange, forall_exists_index, and_imp, List.mem_filter, true_and]

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
n : ℕ
⊢ (∃ xs,
      ∀ (φ : L.BoundedFormula Empty n) (x x_1 : Fin n),
        (decide ¬x = x_1) = true → ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → φ.Realize default xs) ↔
    Nonempty (Fin n ↪ M)
Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed

Goal state before:
pp: case inl
p : ℕ
hp : Nat.Prime p
⊢ (Theory.ACF p).IsSatisfiable

Tactic:
| inl hp =>

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
f : M → M
⊢ TermDefinable₁ L f ↔ ∃ φ, f = (fun v ↦ Term.realize v φ) ∘ Function.const Unit

Tactic:
by
  refine exists_congr fun φ ↦ ?_
  rw [funext_iff, funext_iff, (Equiv.funUnique Unit M).forall_congr']
  simp only [Equiv.funUnique_symm_apply, uniqueElim_const, Function.comp_apply]
  congr!

Goal state after:
Module: Mathlib.ModelTheory.Algebra.Ring.Definability

Goal state before:
pp: ι : Type u_1
K : Type u_2
inst✝¹ : Field K
inst✝ : CompatibleRing K
S : Finset (MvPolynomial ι K)
p' : ↥S → FreeCommRing ((i : ↥S) × ↥(↑i).support ⊕ ι) := genericPolyMap fun p ↦ (↑p).support
this : DecidableEq ι := Classical.decEq ι
⊢ ∃ φ, zeroLocus K (Ideal.span ↑S) = {v | φ.Realize (Sum.elim Subtype.val v)}

Tactic:
let := Classical.decEq K

Goal state after:
ι : Type u_1
K : Type u_2
inst✝¹ : Field K
inst✝ : CompatibleRing K
S : Finset (MvPolynomial ι K)
p' : ↥S → FreeCommRing ((i : ↥S) × ↥(↑i).support ⊕ ι) := genericPolyMap fun p ↦ (↑p).support
this✝ : DecidableEq ι := Classical.decEq ι
this : DecidableEq K := Classical.decEq K
⊢ ∃ φ, zeroLocus K (Ideal.span ↑S) = {v | φ.Realize (Sum.elim Subtype.val v)}
Module: Mathlib.FieldTheory.Cardinality

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
⊢ Nonempty (Field α) ↔ IsPrimePow ‖α‖

Tactic:
refine ⟨fun ⟨h⟩ => Fintype.isPrimePow_card_of_field, ?_⟩
  rintro ⟨p, n, hp, hn, hα⟩
  have := Fact.mk hp.nat_prime
  have : Fintype (GaloisField p n) := Fintype.ofFinite (GaloisField p n)
  exact ⟨(Fintype.equivOfCardEq
    (((Fintype.card_eq_nat_card).trans (GaloisField.card p n hn.ne')).trans hα)).symm.field⟩

Goal state after:
Module: Mathlib.FieldTheory.Differential.Basic

Goal state before:
pp: case succ.inr
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
a : R
n : ℕ
h2 : logDeriv (a ^ n) = ↑n * logDeriv a
hb : a ≠ 0
⊢ logDeriv (a ^ (n + 1)) = logDeriv (a ^ n) + logDeriv a

Tactic:
pow_succ,

Goal state after:
case succ.inr
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
a : R
n : ℕ
h2 : logDeriv (a ^ n) = ↑n * logDeriv a
hb : a ≠ 0
⊢ logDeriv (a ^ n * a) = logDeriv (a ^ n) + logDeriv a
Module: Mathlib.FieldTheory.FinTrdeg

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
ι : Type u_3
inst✝ : Finite ι
x : ι → L
hx : IsTranscendenceBasis K x
⊢ FinTrdeg K L

Tactic:
by
  rw [finTrdeg_iff_trdeg, ← Cardinal.lift_lt_aleph0,
    ← hx.lift_cardinalMk_eq_trdeg, Cardinal.lift_lt_aleph0]
  exact Cardinal.mk_lt_aleph0

Goal state after:
Module: Mathlib.FieldTheory.Finite.Polynomial

Goal state before:
pp: K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
⊢ (indicator c).degrees ≤ ∑ s, (Fintype.card K - 1) • {s}

Tactic:
rw [indicator]

Goal state after:
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
⊢ (∏ n, (1 - (X n - C (c n)) ^ (Fintype.card K - 1))).degrees ≤ ∑ s, (Fintype.card K - 1) • {s}
Module: Mathlib.FieldTheory.Finite.Valuation

Goal state before:
pp: Fq : Type u_1
A : Type u_2
Γ : Type u_3
inst✝⁴ : Field Fq
inst✝³ : Finite Fq
inst✝² : Ring A
inst✝¹ : Algebra Fq A
inst✝ : LinearOrderedCommMonoidWithZero Γ
v : Valuation A Γ
a : Fq
⊢ v ((algebraMap Fq A) a) ≤ 1

Tactic:
by by_cases a = 0 <;> grind [zero_le]

Goal state after:
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
x : L
n : ℕ
y : K
h : i y = x ^ p ^ n
⊢ liftAux i j p x = (iterateFrobeniusEquiv M p n).symm (j y)

Tactic:
rw [liftAux]

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
x : L
n : ℕ
y : K
h : i y = x ^ p ^ n
⊢ (iterateFrobeniusEquiv M p (Classical.choose ⋯).1).symm (j (Classical.choose ⋯).2) =
    (iterateFrobeniusEquiv M p n).symm (j y)
Module: Mathlib.FieldTheory.PerfectClosure

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

Tactic:
pow_succ,

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

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

Tactic:
pow_succ,

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

Goal state before:
pp: K : Type u
inst✝⁵ : CommRing K
p : ℕ
inst✝⁴ : Fact (Nat.Prime p)
inst✝³ : CharP K p
L : Type v
inst✝² : CommSemiring L
inst✝¹ : CharP L p
inst✝ : PerfectRing L p
f : K →+* L
⊢ ∀ (x y : PerfectClosure K p),
    (x + y).liftOn (fun x ↦ (⇑(frobeniusEquiv L p).symm)^[x.1] (f x.2)) ⋯ =
      x.liftOn (fun x ↦ (⇑(frobeniusEquiv L p).symm)^[x.1] (f x.2)) ⋯ +
        y.liftOn (fun x ↦ (⇑(frobeniusEquiv L p).symm)^[x.1] (f x.2)) ⋯

Tactic:
rintro ⟨n, x⟩ ⟨m, y⟩
        simp only [quot_mk_eq_mk, liftOn_mk, f.map_iterate_frobenius, mk_add_mk, map_add,
          iterate_map_add]
        have := LeftInverse.iterate (frobeniusEquiv_symm_apply_frobenius L p)
        rw [iterate_add_apply, this _ _, add_comm n, iterate_add_apply, this _ _]

Goal state after:
Module: Mathlib.FieldTheory.JacobsonNoether

Goal state before:
pp: D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
p : ℕ
hchar : ExpChar D p
a : D
ha : a ∉ k
hinsep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
m : ℕ
hm : 1 ≤ m ∧ a ^ p ^ m ∈ k
n : ℕ
hn : p ^ m ≤ n
x : D
⊢ (⇑((ad (↥k) D) a))^[p ^ m] x = 0 x

Tactic:
rw [ad_eq_lmul_left_sub_lmul_right, ← Module.End.pow_apply, Pi.sub_apply,
      sub_pow_expChar_pow_of_commute p m (commute_mulLeft_right a a), LinearMap.sub_apply,
      pow_mulLeft, mulLeft_apply, pow_mulRight, mulRight_apply, Pi.zero_apply,
      Subring.mem_center_iff.1 hm.2 x]

Goal state after:
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
p : ℕ
hchar : ExpChar D p
a : D
ha : a ∉ k
hinsep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
m : ℕ
hm : 1 ≤ m ∧ a ^ p ^ m ∈ k
n : ℕ
hn : p ^ m ≤ n
x : D
⊢ a ^ p ^ m * x - a ^ p ^ m * x = 0
Module: Mathlib.FieldTheory.MvRatFunc.Rank

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

Tactic:
refine ((rank_le_card _ _).trans ?_).antisymm ?_

Goal state after:
case refine_1
σ : Type u
F : Type v
inst✝¹ : Field F
inst✝ : Nonempty σ
R : Type (max v u) := MvPolynomial σ F
K : Type (max u v) := FractionRing R
⊢ #(FractionRing (MvPolynomial σ F)) ≤ max (max (lift.{u, v} #F) (lift.{v, u} #σ)) ℵ₀

case refine_2
σ : Type u
F : Type v
inst✝¹ : Field F
inst✝ : Nonempty σ
R : Type (max v u) := MvPolynomial σ F
K : Type (max u v) := FractionRing R
⊢ max (max (lift.{u, v} #F) (lift.{v, u} #σ)) ℵ₀ ≤ Module.rank F (FractionRing (MvPolynomial σ F))
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: K : Type u
inst✝³ : Field K
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
a : K
α : L
ha : α ^ finrank K L = (algebraMap K L) a
hα : K⟮α⟯ = ⊤
⊢ Irreducible (X ^ finrank K L - C a)

Tactic:
have : X ^ (finrank K L) - C a = minpoly K α := by
    refine minpoly.unique _ _ (monic_X_pow_sub_C _ finrank_pos.ne.symm) ?_ ?_
    · simp only [aeval_def, eval₂_sub, eval₂_X_pow, ha, eval₂_C, sub_self]
    · intro q hq hq'
      refine le_trans ?_ (degree_le_of_dvd (minpoly.dvd _ _ hq') hq.ne_zero)
      rw [degree_X_pow_sub_C finrank_pos,
        degree_eq_natDegree (minpoly.ne_zero (IsIntegral.of_finite K α)),
        ← IntermediateField.adjoin.finrank (IsIntegral.of_finite K α), hα, Nat.cast_le]
      exact (finrank_top K L).ge
  exact this ▸ minpoly.irreducible (IsIntegral.of_finite K α)

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
inst✝² : Algebra.IsSeparable K L
inst✝¹ : Normal K L
c : ConjRootClass K L
inst✝ : Fintype ↑c.carrier
⊢ (map (algebraMap K L) c.minpoly).roots.card = (map (algebraMap K L) c.minpoly).natDegree

Tactic:
← splits_iff_card_roots

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Algebra.IsSeparable K L
inst✝¹ : Normal K L
c : ConjRootClass K L
inst✝ : Fintype ↑c.carrier
⊢ (map (algebraMap K L) c.minpoly).Splits
Module: Mathlib.FieldTheory.NormalizedTrace

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : CharZero F
inst✝ : FiniteDimensional F K
a : K
h : ↑(Module.finrank (↥F⟮a⟯) K) ≠ 0
⊢ normalizedTraceAux F K a =
    (trace F ↥F⟮a⟯) (AdjoinSimple.gen F a) * ↑(Module.finrank (↥F⟮a⟯) K) /
      (↑(Module.finrank F ↥F⟮a⟯) * ↑(Module.finrank (↥F⟮a⟯) K))

Tactic:
mul_div_mul_right _ _ h,

Goal state after:
F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : CharZero F
inst✝ : FiniteDimensional F K
a : K
h : ↑(Module.finrank (↥F⟮a⟯) K) ≠ 0
⊢ normalizedTraceAux F K a = (trace F ↥F⟮a⟯) (AdjoinSimple.gen F a) / ↑(Module.finrank F ↥F⟮a⟯)
Module: Mathlib.FieldTheory.LinearDisjoint

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
inst✝¹⁵ : Algebra L E
inst✝¹⁴ : IsScalarTower F L E
L' : Type u_1
inst✝¹³ : Field L'
inst✝¹² : Algebra F L'
inst✝¹¹ : Algebra L' E
inst✝¹⁰ : IsScalarTower F L' E
H : (IsScalarTower.toAlgHom F L E).fieldRange.LinearDisjoint (IsScalarTower.toAlgHom F L' E).range
K : Type u_2
inst✝⁹ : Field K
inst✝⁸ : Algebra F K
inst✝⁷ : Algebra L K
inst✝⁶ : IsScalarTower F L K
inst✝⁵ : Algebra L' K
inst✝⁴ : IsScalarTower F L' K
inst✝³ : Algebra E K
inst✝² : IsScalarTower F E K
inst✝¹ : IsScalarTower L E K
inst✝ : IsScalarTower L' E K
this :
  (Subalgebra.map (IsScalarTower.toAlgHom F E K) (IsScalarTower.toAlgHom F L E).fieldRange.toSubalgebra).LinearDisjoint
    (Subalgebra.map (IsScalarTower.toAlgHom F E K) (IsScalarTower.toAlgHom F L' E).range)
⊢ (IsScalarTower.toAlgHom F L K).fieldRange.LinearDisjoint (IsScalarTower.toAlgHom F L' K).range

Tactic:
simp_rw [AlgHom.fieldRange_toSubalgebra, ← AlgHom.range_comp] at this

Goal state after:
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
inst✝¹⁵ : Algebra L E
inst✝¹⁴ : IsScalarTower F L E
L' : Type u_1
inst✝¹³ : Field L'
inst✝¹² : Algebra F L'
inst✝¹¹ : Algebra L' E
inst✝¹⁰ : IsScalarTower F L' E
H : (IsScalarTower.toAlgHom F L E).fieldRange.LinearDisjoint (IsScalarTower.toAlgHom F L' E).range
K : Type u_2
inst✝⁹ : Field K
inst✝⁸ : Algebra F K
inst✝⁷ : Algebra L K
inst✝⁶ : IsScalarTower F L K
inst✝⁵ : Algebra L' K
inst✝⁴ : IsScalarTower F L' K
inst✝³ : Algebra E K
inst✝² : IsScalarTower F E K
inst✝¹ : IsScalarTower L E K
inst✝ : IsScalarTower L' E K
this :
  ((IsScalarTower.toAlgHom F E K).comp (IsScalarTower.toAlgHom F L E)).range.LinearDisjoint
    ((IsScalarTower.toAlgHom F E K).comp (IsScalarTower.toAlgHom F L' E)).range
⊢ (IsScalarTower.toAlgHom F L K).fieldRange.LinearDisjoint (IsScalarTower.toAlgHom F L' K).range
Module: Mathlib.FieldTheory.LinearDisjoint

Goal state before:
pp: F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
A B : IntermediateField F E
inst✝¹ : IsGalois F ↥A
inst✝ : FiniteDimensional F E
h₁ : A ⊔ B = ⊤
h₂ : A ⊓ B = ⊥
⊢ finrank (↥B) E = finrank F ↥A

Tactic:
have : IsGalois B E := IsGalois.sup_right A B h₁

Goal state after:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
A B : IntermediateField F E
inst✝¹ : IsGalois F ↥A
inst✝ : FiniteDimensional F E
h₁ : A ⊔ B = ⊤
h₂ : A ⊓ B = ⊥
this : IsGalois (↥B) E
⊢ finrank (↥B) E = finrank F ↥A
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

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

Tactic:
rw [ne_eq, ← le_bot_iff, SetLike.not_le_iff_exists] at hE
  obtain ⟨f, hf₁, hf₂⟩ := hE
  exact IsAlgebraic.tower_top_of_subalgebra_le (adjoin_simple_le_iff.mpr hf₁) <|
    f.isAlgebraic_adjoin_simple_X (by rintro ⟨c, rfl⟩; exact hf₂ ⟨c, rfl⟩)

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

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F⟮X⟯
x y : F⟮X⟯
⊢ inftyValuationDef F (x + y) ≤ max (inftyValuationDef F x) (inftyValuationDef F y)

Tactic:
by
  unfold inftyValuationDef
  have := @RatFunc.intDegree_add_le F
  aesop

Goal state after:
Module: Mathlib.Geometry.Convex.Cone.Face.Basic

Goal state before:
pp: 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₁ C₂ F₁ F₂ : PointedCone R M
h₁ : F₁.IsFaceOf C₁
h₂ : F₂.IsFaceOf C₂
⊢ (F₁ ⊓ F₂).IsFaceOf (C₁ ⊓ C₂)

Tactic:
by
  use le_inf_iff.mpr ⟨Set.inter_subset_left.trans h₁.le, Set.inter_subset_right.trans h₂.le⟩
  simp only [mem_inf, and_imp]
  refine fun xc₁ xc₂ yc₁ yc₂ a0 hz₁ hz₂ ↦ ⟨?_, ?_⟩
  · exact h₁.mem_of_smul_add_mem xc₁ yc₁ a0 hz₁
  · exact h₂.mem_of_smul_add_mem xc₂ yc₂ a0 hz₂

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 ≠ ⊥
F : Type u_1 := AlgebraicClosure K
H : ¬(Polynomial.map (algebraMap K F) (Q₂ h)).degree ≤ 0
α : F
hα : (aeval α) (Q₂ h) = 0
eq :
  (Polynomial.mapRingHom (algebraMap K F)) (g E) * Polynomial.C ((aeval α) (f E)) =
    (Polynomial.mapRingHom (algebraMap K F)) (f E) * Polynomial.C ((aeval α) (g E))
isUnit₁ : IsUnit (Polynomial.C ((aeval α) (f E)))
isUnit₂ : IsUnit (Polynomial.C ((aeval α) (g E)))
isCoprime :
  IsCoprime ((Polynomial.mapRingHom (algebraMap K F)) (generator E).num)
    ((Polynomial.mapRingHom (algebraMap K F)) (generator E).denom)
this : Associated ((Polynomial.mapRingHom (algebraMap K F)) (f E)) ((Polynomial.mapRingHom (algebraMap K F)) (g E))
⊢ (generator E).num.natDegree = 0 ∧ (generator E).denom.natDegree = 0

Tactic:
have := isCoprime.isUnit_of_associated this

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
F : Type u_1 := AlgebraicClosure K
H : ¬(Polynomial.map (algebraMap K F) (Q₂ h)).degree ≤ 0
α : F
hα : (aeval α) (Q₂ h) = 0
eq :
  (Polynomial.mapRingHom (algebraMap K F)) (g E) * Polynomial.C ((aeval α) (f E)) =
    (Polynomial.mapRingHom (algebraMap K F)) (f E) * Polynomial.C ((aeval α) (g E))
isUnit₁ : IsUnit (Polynomial.C ((aeval α) (f E)))
isUnit₂ : IsUnit (Polynomial.C ((aeval α) (g E)))
isCoprime :
  IsCoprime ((Polynomial.mapRingHom (algebraMap K F)) (generator E).num)
    ((Polynomial.mapRingHom (algebraMap K F)) (generator E).denom)
this✝ : Associated ((Polynomial.mapRingHom (algebraMap K F)) (f E)) ((Polynomial.mapRingHom (algebraMap K F)) (g E))
this :
  IsUnit ((Polynomial.mapRingHom (algebraMap K F)) (generator E).num) ∧
    IsUnit ((Polynomial.mapRingHom (algebraMap K F)) (generator E).denom)
⊢ (generator E).num.natDegree = 0 ∧ (generator E).denom.natDegree = 0
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation

Goal state before:
pp: case e'_2
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
⊢ ((o.rotationAux θ).toLinearMap ∘ₗ (θ.cos • LinearMap.id - θ.sin • ↑o.rightAngleRotation.toLinearEquiv)) x =
    (θ.cos ^ 2 + θ.sin ^ 2) • x

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 only [o.rightAngleRotation_rightAngleRotation, o.rotationAux_apply,
          Function.comp_apply, id, LinearEquiv.coe_coe, LinearIsometry.coe_toLinearMap,
          LinearIsometryEquiv.coe_toLinearEquiv, map_smul, map_sub, LinearMap.coe_comp,
          LinearMap.id_coe, LinearMap.smul_apply, LinearMap.sub_apply]
        module

Goal state after:
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
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

Goal state before:
pp: case refine_2
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V × V
hx1 : x.1 ≠ 0
hx2 : x.2 ≠ 0
⊢ ContinuousAt (fun y ↦ (o.kahler y.1) y.2) x

Tactic:
exact ((continuous_ofReal.comp continuous_inner).add
    ((continuous_ofReal.comp o.areaForm'.continuous₂).mul continuous_const)).continuousAt

Goal state after:
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
hx : ¬x = 0
⊢ 2 • o.oangle x (-y) = 2 • o.oangle x y

Tactic:
· by_cases hy : y = 0
    · simp [hy]
    · simp [o.oangle_neg_right hx hy]

Goal state after:
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
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
hp : 0 < ‖y‖ / ‖x‖
hye : y = (‖y‖ / ‖x‖) • (o.rotation θ) x
⊢ o.oangle x y = θ

Tactic:
hye,

Goal state after:
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
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
hp : 0 < ‖y‖ / ‖x‖
hye : y = (‖y‖ / ‖x‖) • (o.rotation θ) x
⊢ o.oangle x ((‖y‖ / ‖x‖) • (o.rotation θ) x) = θ
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
⊢ (↑⟪x, y⟫ + (o.areaForm x) y • I).arg = 0 ↔ SameRay ℝ x y

Tactic:
Complex.arg_eq_zero_iff

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
⊢ 0 ≤ (↑⟪x, y⟫ + (o.areaForm x) y • I).re ∧ (↑⟪x, y⟫ + (o.areaForm x) y • I).im = 0 ↔ SameRay ℝ x y
Module: Mathlib.Geometry.Euclidean.Altitude

Goal state before:
pp: case a.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 i).points))ᗮ ⊓ (vectorSpan ℝ (Set.range (s.faceOpposite j).points))ᗮ

Tactic:
Submodule.mem_inf

Goal state after:
case a.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 i).points))ᗮ ∧
    s.points j -ᵥ s.altitudeFoot j ∈ (vectorSpan ℝ (Set.range (s.faceOpposite j).points))ᗮ
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
h0 : x ≠ 0
⊢ angle x (x + y) = Real.arctan (‖y‖ / ‖x‖)

Tactic:
rw [angle_add_eq_arcsin_of_inner_eq_zero h (Or.inl h0), Real.arctan_eq_arcsin, ←
    div_mul_eq_div_div, norm_add_eq_sqrt_iff_real_inner_eq_zero.2 h]

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x ≠ 0
⊢ Real.arcsin (‖y‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)) = Real.arcsin (‖y‖ / (‖x‖ * √(1 + (‖y‖ / ‖x‖) ^ 2)))
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
⊢ AffineIndependent ℝ ![p₁, p₂, p₃] ↔ ¬Collinear ℝ {p₁, p₂, p₃}

Tactic:
affineIndependent_iff_not_collinear_set

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
⊢ ¬Collinear ℝ {p₁, p₂, p₃} ↔ ¬Collinear ℝ {p₁, p₂, p₃}