mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.ModelTheory.Algebra.Ring.Basic

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝ : ring.Structure R
⊢ ∀ (x : Fin 2 → R), funMap mulFunc x = x 0 * x 1

Tactic:
simp only [Fin.forall_fin_succ_pi, Fin.cons_zero, Fin.forall_fin_zero_pi]
      intros; rfl

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

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝ : ring.Structure R
⊢ ∀ (x : Fin 1 → R), funMap negFunc x = -x 0

Tactic:
simp only [Fin.forall_fin_succ_pi, Fin.cons_zero, Fin.forall_fin_zero_pi]
      intros; rfl

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case func
L : Language
α : Type u'
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term α
_ts_ih✝ : ∀ (a : Fin l✝), ((_ts✝ a).substFunc fun {n} ↦ Functions.term) = _ts✝ a
⊢ ((func _f✝ _ts✝).substFunc fun {n} ↦ Functions.term) = func _f✝ _ts✝

Tactic:
· simp only [substFunc, Functions.term, subst, ‹∀ _, _›]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case var.inl
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
γ : Type u_4
xs : β ⊕ γ → M
xs' : α → M
val✝ : α
f : ↥(var (Sum.inl val✝)).varFinsetLeft → β
hxs' : ∀ (a : ↥(var (Sum.inl val✝)).varFinsetLeft), xs (Sum.inl (f a)) = xs' ↑a
⊢ realize xs ((var (Sum.inl val✝)).restrictVarLeft f) = realize (Sum.elim xs' (xs ∘ Sum.inr)) (var (Sum.inl val✝))

Tactic:
simp [restrictVarLeft, hxs']

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case var.inr
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
γ : Type u_4
xs : β ⊕ γ → M
xs' : α → M
val✝ : γ
f : ↥(var (Sum.inr val✝)).varFinsetLeft → β
hxs' : ∀ (a : ↥(var (Sum.inr val✝)).varFinsetLeft), xs (Sum.inl (f a)) = xs' ↑a
⊢ realize xs ((var (Sum.inr val✝)).restrictVarLeft f) = realize (Sum.elim xs' (xs ∘ Sum.inr)) (var (Sum.inr val✝))

Tactic:
simp [restrictVarLeft, hxs']

Goal state after:
Module: Mathlib.ModelTheory.ElementaryMaps

Goal state before:
pp: L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪ₑ[L] N
T : L.Theory
⊢ M ⊨ T ↔ N ⊨ T

Tactic:
by
  simp only [Theory.model_iff, f.map_sentence]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Divisibility

Goal state before:
pp: case inr
a : Cardinal.{u}
h : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
t : Cardinal.{u}
ht : a = 1 ∧ t = 1
⊢ a = 1

Tactic:
exact ht.1

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Divisibility

Goal state before:
pp: case inr
a : ℕ
h : ↑a < ℵ₀
⊢ Prime ↑a ↔ ℵ₀ ≤ ↑a ∨ ∃ p, ↑a = ↑p ∧ Nat.Prime p

Tactic:
simp [not_le.mpr h]

Goal state after:
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
inst✝ : FinTrdeg K L
ι : Type u_3
x : ι → L
hx : IsTranscendenceBasis K x
⊢ Finite ι

Tactic:
rw [← Cardinal.mk_lt_aleph0_iff, ← Cardinal.lift_lt_aleph0,
    hx.lift_cardinalMk_eq_trdeg, Cardinal.lift_lt_aleph0]
  exact trdeg_lt_aleph0 K L

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

Goal state before:
pp: k : Type u_1
inst✝⁶ : Field k
inst✝⁵ : Finite k
p : ℕ
inst✝⁴ : Fact (Nat.Prime p)
inst✝³ : CharP k p
l : Type u_2
inst✝² : Field l
inst✝¹ : Algebra k l
inst✝ : Finite l
g : Gal(l/k)
n : ℕ := Module.finrank k l
⊢ ∃ i, ∀ (x : l), g x = x ^ Nat.card k ^ i

Tactic:
have : NeZero n := NeZero.of_pos Module.finrank_pos

Goal state after:
k : Type u_1
inst✝⁶ : Field k
inst✝⁵ : Finite k
p : ℕ
inst✝⁴ : Fact (Nat.Prime p)
inst✝³ : CharP k p
l : Type u_2
inst✝² : Field l
inst✝¹ : Algebra k l
inst✝ : Finite l
g : Gal(l/k)
n : ℕ := Module.finrank k l
this : NeZero n
⊢ ∃ i, ∀ (x : l), g x = x ^ Nat.card k ^ i
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
h0 : M.det = 0
⊢ False

Tactic:
by
    simpa [hc] using! congr(($h0).eval c)

Goal state after:
Module: Mathlib.FieldTheory.CardinalEmb

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
⊢ ⨆ i, adjoin F (⇑b ∘ φ '' Iio i) = ⊤

Tactic:
simp_rw [adjoin_image_leastExt, eq_top_iff, ← adjoin_basis_eq_top, adjoin_le_iff]
  rintro _ ⟨i, rfl⟩
  refine le_iSup (α := IntermediateField F E) _ (i⁺) (subset_adjoin _ _ ⟨i, ?_, rfl⟩)
  exact (lt_succ i).trans_le strictMono_leastExt.le_apply

Goal state after:
Module: Mathlib.FieldTheory.CardinalEmb

Goal state before:
pp: case coe
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
a✝ : (Module.rank F E).ord.ToType
hi : IsSuccPrelimit ↑a✝
⊢ ⨆ j, filtration ↑j = filtration ↑a✝

Tactic:
refine (iSup_le fun j ↦ filtration.monotone (mem_Iio.1 j.2).le).antisymm (adjoin_le_iff.2 ?_)

Goal state after:
case coe
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
a✝ : (Module.rank F E).ord.ToType
hi : IsSuccPrelimit ↑a✝
⊢ ⇑b ∘ φ '' Iio a✝ ⊆ ↑(⨆ j, filtration ↑j)
Module: Mathlib.FieldTheory.Galois.Profinite

Goal state before:
pp: case h.right
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : Normal k ↥L
N : Set Gal(↥L/k)
L' : IntermediateField k ↥L
left✝ : FiniteDimensional k ↥L'
hO : ↑L'.fixingSubgroup ⊆ N
this : Module.Finite k ↥(IntermediateField.lift L')
⊢ IsOpen ↑(IntermediateField.lift L').fixingSubgroup ∧ 1 ∈ ↑(IntermediateField.lift L').fixingSubgroup

Tactic:
· exact ⟨IntermediateField.fixingSubgroup_isOpen (IntermediateField.lift L'), congrFun rfl⟩

Goal state after:
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring K
inst✝³ : CommSemiring L
inst✝² : CommSemiring M
i : K →+* L
f : L →+* M
p : ℕ
inst✝¹ : IsPRadical i p
inst✝ : IsPRadical f p
x : K
h : x ∈ RingHom.ker (f.comp i)
⊢ x ∈ pNilradical K p

Tactic:
rw [RingHom.mem_ker, RingHom.comp_apply, ← RingHom.mem_ker] at h
    simpa only [← Ideal.mem_comap, comap_pNilradical] using ker_le f p h

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

Goal state before:
pp: case inr
R : Type u
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
isSquare_of_nonneg : ∀ {x : R}, 0 ≤ x → IsSquare x
exists_isRoot_of_odd_natDegree : ∀ {f : R[X]}, Odd f.natDegree → ∃ x, f.IsRoot x
x : R
pos : 0 ≤ x
⊢ IsSquare x ∨ IsSquare (-x)

Tactic:
· exact .inl <| isSquare_of_nonneg pos

Goal state after:
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: case pos
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
inst✝ : DecidablePred FiniteIndex
hcovers : ⋃ i ∈ {i ∈ s | (H i).FiniteIndex} ∪ {a ∈ s | ¬(H a).FiniteIndex}, g i • ↑(H i) = Set.univ
D : Subgroup G := ⨅ k ∈ {i ∈ s | (H i).FiniteIndex}, H k
hD : D.FiniteIndex
hD_le : ∀ {i : ι}, i ∈ s → (H i).FiniteIndex → D ≤ H i
t : (i : ι) → i ∈ s → (H i).FiniteIndex → Finset ↥(H i)
ht :
  ∀ (i : ι) (hi : i ∈ s) (hfi : (H i).FiniteIndex),
    IsComplement ↑(t i hi hfi) ↑(D.subgroupOf (H i)) ∧ ⋃ g ∈ t i hi hfi, ↑g • ↑D = ↑(H i)
κ : Type (max u_2 u_1) := (i : ↥s) × ↥(if h : (H ↑i).FiniteIndex then t ↑i ⋯ h else {1})
f : κ → G := fun k ↦ g ↑k.fst * ↑↑k.snd
K : κ → Subgroup G := fun k ↦ if (H ↑k.fst).FiniteIndex then D else H ↑k.fst
i : ι
hfi : (H i).FiniteIndex
⊢ ⋃ (hx : i ∈ s), ⋃ a, ⋃ (_ : ⟨⟨i, hx⟩, a⟩ ∈ {a | ¬(H ↑a.fst).FiniteIndex}), f ⟨⟨i, hx⟩, a⟩ • ↑(K ⟨⟨i, hx⟩, a⟩) =
    ⋃ (_ : i ∈ {a ∈ s | ¬(H a).FiniteIndex}), g i • ↑(H i)

Tactic:
simp [Set.iUnion_subtype, f, K, hfi]

Goal state after:
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: case neg
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
inst✝ : DecidablePred FiniteIndex
hcovers : ⋃ i ∈ {i ∈ s | (H i).FiniteIndex} ∪ {a ∈ s | ¬(H a).FiniteIndex}, g i • ↑(H i) = Set.univ
D : Subgroup G := ⨅ k ∈ {i ∈ s | (H i).FiniteIndex}, H k
hD : D.FiniteIndex
hD_le : ∀ {i : ι}, i ∈ s → (H i).FiniteIndex → D ≤ H i
t : (i : ι) → i ∈ s → (H i).FiniteIndex → Finset ↥(H i)
ht :
  ∀ (i : ι) (hi : i ∈ s) (hfi : (H i).FiniteIndex),
    IsComplement ↑(t i hi hfi) ↑(D.subgroupOf (H i)) ∧ ⋃ g ∈ t i hi hfi, ↑g • ↑D = ↑(H i)
κ : Type (max u_2 u_1) := (i : ↥s) × ↥(if h : (H ↑i).FiniteIndex then t ↑i ⋯ h else {1})
f : κ → G := fun k ↦ g ↑k.fst * ↑↑k.snd
K : κ → Subgroup G := fun k ↦ if (H ↑k.fst).FiniteIndex then D else H ↑k.fst
i : ι
hfi : ¬(H i).FiniteIndex
⊢ ⋃ (hx : i ∈ s), ⋃ a, ⋃ (_ : ⟨⟨i, hx⟩, a⟩ ∈ {a | ¬(H ↑a.fst).FiniteIndex}), f ⟨⟨i, hx⟩, a⟩ • ↑(K ⟨⟨i, hx⟩, a⟩) =
    ⋃ (_ : i ∈ {a ∈ s | ¬(H a).FiniteIndex}), g i • ↑(H i)

Tactic:
simp [Set.iUnion_subtype, f, K, hfi]

Goal state after:
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
inst✝ : Flat R ↥A
ι : Type u_1
b : ι → ↥B
hb : LinearIndependent R b
⊢ LinearIndependent (↥A) (⇑B.val ∘ b)

Tactic:
by
  have h := Submodule.LinearDisjoint.linearIndependent_right_of_flat H hb
  rwa [mulRightMap_ker_eq_bot_iff_linearIndependent] at h

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
x y : ConjRootClass K L
⊢ (∃ a ∈ x.carrier, ∃ b ∈ y.carrier, a + b = 0) ↔ x = -y

Tactic:
simp_rw [mem_carrier]

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
⊢ (∃ a, mk K a = x ∧ ∃ b, mk K b = y ∧ a + b = 0) ↔ x = -y
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
K : Type w
inst✝¹ : Field K
inst✝ : Algebra F K
i : E →ₐ[F] K
⊢ comap i (perfectClosure F K) = perfectClosure F E

Tactic:
by
  ext x
  exact map_mem_perfectClosure_iff i

Goal state after:
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✝ : FiniteDimensional F E
h₁ : A.LinearDisjoint ↥B
h₂ : A ⊔ B = ⊤
x : ↥B
⊢ (Algebra.trace (↥A) E) ((algebraMap (↥B) E) x) = (algebraMap F ↥A) ((Algebra.trace F ↥B) x)

Tactic:
rw [linearDisjoint_iff'] at 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✝ : FiniteDimensional F E
h₁ : A.LinearDisjoint B.toSubalgebra
h₂ : A ⊔ B = ⊤
x : ↥B
⊢ (Algebra.trace (↥A) E) ((algebraMap (↥B) E) x) = (algebraMap F ↥A) ((Algebra.trace F ↥B) x)
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✝ : FiniteDimensional F E
h₁ : A.LinearDisjoint ↥B
h₂ : A ⊔ B = ⊤
x : ↥B
⊢ (Algebra.norm ↥A) ((algebraMap (↥B) E) x) = (algebraMap F ↥A) ((Algebra.norm F) x)

Tactic:
rw [linearDisjoint_iff'] at 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✝ : FiniteDimensional F E
h₁ : A.LinearDisjoint B.toSubalgebra
h₂ : A ⊔ B = ⊤
x : ↥B
⊢ (Algebra.norm ↥A) ((algebraMap (↥B) E) x) = (algebraMap F ↥A) ((Algebra.norm F) x)
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

Goal state before:
pp: K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ¬∃ c, f = C c
f_ne_zero : f ≠ 0
H : f⁻¹ = C (f.denom.coeff f.num.natDegree) / C f.num.leadingCoeff
⊢ False

Tactic:
← inv_inj,

Goal state after:
K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ¬∃ c, f = C c
f_ne_zero : f ≠ 0
H : f⁻¹⁻¹ = (C (f.denom.coeff f.num.natDegree) / C f.num.leadingCoeff)⁻¹
⊢ 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
inst✝ : IsPurelyInseparable F E
⊢ Cardinal.lift.{w, v} (Module.rank F E) * Cardinal.lift.{v, w} (insepDegree E K) =
    Cardinal.lift.{v, w} (insepDegree F K)

Tactic:
by
  have h := (separableClosure F K).linearDisjoint_of_isPurelyInseparable_of_isSeparable E
    |>.lift_rank_right_mul_lift_adjoin_rank_eq_of_isAlgebraic_left
  rwa [separableClosure.adjoin_eq_of_isAlgebraic] at h

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
e : K[X] ≃ₐ[K] ↥K[f] := Polynomial.algEquivOfTranscendental K f ⋯
φ : K[X][X] :=
  Polynomial.map (algebraMap K K[X]) f.num - Polynomial.C Polynomial.X * Polynomial.map (algebraMap K K[X]) f.denom
⊢ (mapEquiv e.toRingEquiv) φ = f.minpolyX ↥K[f]

Tactic:
simp only [algebraMap_eq, map_sub, mapEquiv_apply,
      AlgEquiv.toRingEquiv_toRingHom, algEquivOfTranscendental_coe, Polynomial.map_map, map_mul,
      map_C, RingHom.coe_coe, aeval_X, e, φ]

Goal state after:
K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ¬∃ c, f = C c
e : K[X] ≃ₐ[K] ↥K[f] := Polynomial.algEquivOfTranscendental K f ⋯
φ : K[X][X] :=
  Polynomial.map (algebraMap K K[X]) f.num - Polynomial.C Polynomial.X * Polynomial.map (algebraMap K K[X]) f.denom
⊢ Polynomial.map ((↑(aeval ⟨f, ⋯⟩)).comp Polynomial.C) f.num -
      Polynomial.C ⟨f, ⋯⟩ * Polynomial.map ((↑(aeval ⟨f, ⋯⟩)).comp Polynomial.C) f.denom =
    f.minpolyX ↥K[f]
Module: Mathlib.FieldTheory.Relrank

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

Tactic:
relrank_mul_relrank inf_le_right inf_le_right

Goal state after:
E : Type v
inst✝ : Field E
A B C : Subfield E
⊢ (A ⊓ (B ⊓ C)).relrank C = (A ⊓ (B ⊓ C)).relrank C
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
this : (Bivariate.swap (Q₁ h)).natDegree + (Bivariate.swap (Φ E)).natDegree = (Bivariate.swap (θ E)).natDegree
h₁ : (Bivariate.swap (θ E)).natDegree ≤ m E
⊢ (Bivariate.swap (Q₁ h)).natDegree = 0

Tactic:
grind [m_le_swap_Φ_natDegree h]

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)))
⊢ (generator E).num.natDegree = 0 ∧ (generator E).denom.natDegree = 0

Tactic:
have isCoprime := IsCoprime.map (generator E).isCoprime_num_denom <|
    Polynomial.mapRingHom (algebraMap K F)

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)
⊢ (generator E).num.natDegree = 0 ∧ (generator E).denom.natDegree = 0
Module: Mathlib.Geometry.Euclidean.Projection

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace 𝕜 V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst✝¹ : Nonempty ↥s
inst✝ : s.direction.HasOrthogonalProjection
p q : P
hqs : q ∈ s
hpq : p -ᵥ q ∈ s.directionᗮ
hq : q ∈ mk' p s.directionᗮ
this : q ∈ {↑((orthogonalProjection s) p)}
⊢ ↑((orthogonalProjection s) p) = q

Tactic:
simpa [eq_comm] using this

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

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
n : ℕ
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
hc : #{i}ᶜ = n - 1 + 1
⊢ n = n - 1 + 1

Tactic:
hn

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
hc : #{i}ᶜ = n - 1 + 1
⊢ n = n
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation

Goal state before:
pp: V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
⊢ (o.rotation θ).symm = o.rotation (-θ)

Tactic:
by
  ext; simp [o.rotation_apply, o.rotation_symm_apply, sub_eq_add_neg]

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

Goal state before:
pp: case refine_2.inr.inr.inl.inl
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 : Wbtw ℝ p₂ p₁ p₃
⊢ Collinear ℝ {p₁, p₂, p₃}

Tactic:
rw [Set.insert_comm]

Goal state after:
case refine_2.inr.inr.inl.inl
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 : Wbtw ℝ p₂ p₁ p₃
⊢ Collinear ℝ {p₂, p₁, p₃}
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₅ p₆ : P
h₂ : p₂ ∉ line[ℝ, p₁, p₃]
h₄ : p₄ ∈ line[ℝ, p₁, p₃]
h₆ : p₆ ∈ line[ℝ, p₁, p₃]
h₁₂₄₅ : line[ℝ, p₁, p₂] ∥ line[ℝ, p₄, p₅]
h₃₂₆₅ : line[ℝ, p₃, p₂] ∥ line[ℝ, p₆, p₅]
hd : line[ℝ, p₆, p₄].direction ≤ line[ℝ, p₃, p₁].direction
r : ℝ
hr : r ≠ 0
h₅₄ : p₄ -ᵥ p₅ = r • (p₁ -ᵥ p₂)
h₆₅ : p₆ -ᵥ p₅ = r • (p₃ -ᵥ p₂)
⊢ o.oangle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = o.oangle (p₄ -ᵥ p₅) (p₆ -ᵥ p₅)

Tactic:
rw [h₅₄, 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₄ p₅ p₆ : P
h₂ : p₂ ∉ line[ℝ, p₁, p₃]
h₄ : p₄ ∈ line[ℝ, p₁, p₃]
h₆ : p₆ ∈ line[ℝ, p₁, p₃]
h₁₂₄₅ : line[ℝ, p₁, p₂] ∥ line[ℝ, p₄, p₅]
h₃₂₆₅ : line[ℝ, p₃, p₂] ∥ line[ℝ, p₆, p₅]
hd : line[ℝ, p₆, p₄].direction ≤ line[ℝ, p₃, p₁].direction
r : ℝ
hr : r ≠ 0
h₅₄ : p₄ -ᵥ p₅ = r • (p₁ -ᵥ p₂)
h₆₅ : p₆ -ᵥ p₅ = r • (p₃ -ᵥ p₂)
⊢ o.oangle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = o.oangle (r • (p₁ -ᵥ p₂)) (r • (p₃ -ᵥ p₂))
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ : P
h : InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = π / 2
⊢ ∠ p₂ p₃ p₁ = Real.arccos (dist p₃ p₂ / dist p₁ p₃)

Tactic:
← inner_eq_zero_iff_angle_eq_pi_div_two,

Goal state after:
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₂⟫ = 0
⊢ ∠ p₂ p₃ p₁ = Real.arccos (dist p₃ p₂ / dist p₁ p₃)
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ : P
h : InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = π / 2
h0 : p₁ ≠ p₂ ∨ p₃ ≠ p₂
⊢ ∠ p₂ p₃ p₁ = Real.arcsin (dist p₁ p₂ / dist p₁ p₃)

Tactic:
← inner_eq_zero_iff_angle_eq_pi_div_two,

Goal state after:
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₂⟫ = 0
h0 : p₁ ≠ p₂ ∨ p₃ ≠ p₂
⊢ ∠ p₂ p₃ p₁ = Real.arcsin (dist p₁ p₂ / dist p₁ p₃)
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ : P
h : InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = π / 2
h0 : p₃ ≠ p₂
⊢ ∠ p₂ p₃ p₁ = Real.arctan (dist p₁ p₂ / dist p₃ p₂)

Tactic:
← inner_eq_zero_iff_angle_eq_pi_div_two,

Goal state after:
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₂⟫ = 0
h0 : p₃ ≠ p₂
⊢ ∠ p₂ p₃ p₁ = Real.arctan (dist p₁ p₂ / dist p₃ p₂)
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ : P
h : InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = π / 2
h0 : p₁ ≠ p₂ ∨ p₃ = p₂
⊢ 0 < ∠ p₂ p₃ p₁

Tactic:
← inner_eq_zero_iff_angle_eq_pi_div_two,

Goal state after:
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₂⟫ = 0
h0 : p₁ ≠ p₂ ∨ p₃ = p₂
⊢ 0 < ∠ p₂ p₃ p₁
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ : P
h : InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = π / 2
⊢ ∠ p₂ p₃ p₁ ≤ π / 2

Tactic:
← inner_eq_zero_iff_angle_eq_pi_div_two,

Goal state after:
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₂⟫ = 0
⊢ ∠ p₂ p₃ p₁ ≤ π / 2
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ : P
h : InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = π / 2
h0 : p₃ ≠ p₂
⊢ ∠ p₂ p₃ p₁ < π / 2

Tactic:
← inner_eq_zero_iff_angle_eq_pi_div_two,

Goal state after:
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₂⟫ = 0
h0 : p₃ ≠ p₂
⊢ ∠ p₂ p₃ p₁ < π / 2