mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed

Goal state before:
pp: case inl
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
x✝ : CompatibleRing (AlgebraicClosure (ZMod p)) := compatibleRingOfRing (AlgebraicClosure (ZMod p))
⊢ (Theory.ACF p).IsSatisfiable

Tactic:
exact ⟨⟨AlgebraicClosure (ZMod p)⟩⟩

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

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

Tactic:
have : Fact p.Prime := ⟨hp⟩
    let _ := compatibleRingOfRing (AlgebraicClosure (ZMod p))
    exact ⟨⟨AlgebraicClosure (ZMod p)⟩⟩

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
ι : Type u_1
T : ι → L.Theory
h : ∀ (s : Finset ι), IsSatisfiable (⋃ i ∈ s, T i)
s : Finset L.Sentence
hs : ↑s ⊆ ⋃ t, ⋃ i ∈ t, T i
⊢ IsSatisfiable ↑s

Tactic:
obtain ⟨t, ht⟩ := Directed.exists_mem_subset_of_finset_subset_biUnion (by
    exact Monotone.directed_le fun t1 t2 (h : ∀ ⦃x⦄, x ∈ t1 → x ∈ t2) =>
      Set.iUnion_mono fun _ => Set.iUnion_mono' fun h1 => ⟨h h1, refl _⟩) hs

Goal state after:
L : Language
ι : Type u_1
T : ι → L.Theory
h : ∀ (s : Finset ι), IsSatisfiable (⋃ i ∈ s, T i)
s : Finset L.Sentence
hs : ↑s ⊆ ⋃ t, ⋃ i ∈ t, T i
t : Finset ι
ht : ↑s ⊆ ⋃ i ∈ t, T i
⊢ IsSatisfiable ↑s
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: case refine_1
L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α n
h : T ⊨ᵇ φ.toFormula
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
⊢ φ.Realize v xs

Tactic:
have h' : φ.toFormula.Realize (Sum.elim v xs) := h.realize_formula M
    simp only [BoundedFormula.realize_toFormula, Sum.elim_comp_inl, Sum.elim_comp_inr] at h'
    exact h'

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

Goal state before:
pp: case inr
a : Cardinal.{u}
h : IsUnit a
ha : a ≠ 0
⊢ a = 1

Tactic:
isUnit_iff_forall_dvd

Goal state after:
case inr
a : Cardinal.{u}
h : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
⊢ a = 1
Module: Mathlib.FieldTheory.Differential.Basic

Goal state before:
pp: case cons
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
ι : Type u_2
f : ι → R
a✝¹ : ι
s✝ : Multiset ι
a✝ : (∀ x ∈ s✝, f x ≠ 0) → logDeriv (Multiset.map f s✝).prod = (Multiset.map (fun x ↦ logDeriv (f x)) s✝).sum
h : ∀ x ∈ a✝¹ ::ₘ s✝, f x ≠ 0
⊢ logDeriv (Multiset.map f (a✝¹ ::ₘ s✝)).prod = (Multiset.map (fun x ↦ logDeriv (f x)) (a✝¹ ::ₘ s✝)).sum

Tactic:
· rename_i h₂
    simp only [Multiset.map_cons, Multiset.sum_cons, Multiset.prod_cons]
    rw [← h₂]
    · apply logDeriv_mul
      · simp [h]
      · simp_all
    · simp_all

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

Goal state before:
pp: case ha
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : Field K
a b : σ → K
h : a ≠ b
i : σ
hi : a i ≠ b i
⊢ ¬a i - b i = 0

Tactic:
sub_eq_zero

Goal state after:
case ha
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : Field K
a b : σ → K
h : a ≠ b
i : σ
hi : a i ≠ b i
⊢ ¬a i = b i
Module: Mathlib.FieldTheory.CardinalEmb

Goal state before:
pp: case inr
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 j : (Module.rank F E).ord.ToType
h : i < j
least : ∀ (i : (Module.rank F E).ord.ToType), IsLeast {k | b k ∉ adjoin F (⇑b ∘ φ '' Iio i)} (φ i)
this : φ j ≤ φ i
lt : φ j < φ i
⊢ False

Tactic:
refine ((least i).2 <| mt (adjoin.mono _ _ _ (image_mono ?_) ·) (least j).1).not_gt lt
    exact fun k (hk : k < i) ↦ hk.trans h

Goal state after:
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : ExpChar R p
x y : R
⊢ (∃ n, x ^ p ^ n - y ^ p ^ n = 0) ↔ ∃ n, x ^ p ^ n = y ^ p ^ n

Tactic:
sub_eq_zero

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

Goal state before:
pp: k : Type u_3
K : Type u_4
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
L : (FiniteGaloisIntermediateField k K)ᵒᵖ
⊢ Continuous fun a ↦ (Subtype.val ∘ ⇑(algEquivToLimit k K)) a L

Tactic:
convert! restrictNormalHom_continuous L.unop.1

Goal state after:
case e'_4
k : Type u_3
K : Type u_4
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
L : (FiniteGaloisIntermediateField k K)ᵒᵖ
e_2✝ : ↑((asProfiniteGaloisGroupFunctor k K).obj L).toProfinite.toTop = Gal(↥(unop L).toIntermediateField/k)
⊢ ((asProfiniteGaloisGroupFunctor k K).obj L).toProfinite.toTop.str = krullTopology k ↥(unop L).toIntermediateField
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
n' : ℕ := (Classical.choose ⋯).1
h' : i (Classical.choose ⋯).2 = x ^ p ^ n'
h✝ : (Classical.choose ⋯).2 ^ p ^ n - y ^ p ^ n' ∈ RingHom.ker i
m : ℕ
h : ((Classical.choose ⋯).2 ^ p ^ n - y ^ p ^ n') ^ p ^ m = 0
⊢ j (((Classical.choose ⋯).2 ^ p ^ n) ^ p ^ m - (y ^ p ^ n') ^ p ^ m) = 0

Tactic:
← sub_pow_expChar_pow,

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
n' : ℕ := (Classical.choose ⋯).1
h' : i (Classical.choose ⋯).2 = x ^ p ^ n'
h✝ : (Classical.choose ⋯).2 ^ p ^ n - y ^ p ^ n' ∈ RingHom.ker i
m : ℕ
h : ((Classical.choose ⋯).2 ^ p ^ n - y ^ p ^ n') ^ p ^ m = 0
⊢ j (((Classical.choose ⋯).2 ^ p ^ n - y ^ p ^ n') ^ p ^ m) = 0
Module: Mathlib.FieldTheory.IsRealClosed.Basic

Goal state before:
pp: case inl
R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
hx : IsSquare x
n : ℕ
hk : ↑n ≠ 0
⊢ ∃ r, x = r ^ ↑n

Tactic:
simpa using exists_eq_pow_of_isSquare hx (by simpa using hk)

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
e : Gal(K[n√a]/K)
this✝ : Fact (Irreducible (X ^ n - C a))
this : Algebra K K[n√a] := ⋯
⊢ ↑((↑(autAdjoinRootXPowSubC n a)).toFun (AdjoinRootXPowSubCEquivToRootsOfUnity hζ H e)) = ↑e

Tactic:
apply AdjoinRoot.algHom_ext

Goal state after:
K : Type u
inst✝¹ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
inst✝ : NeZero n
e : Gal(K[n√a]/K)
this✝ : Fact (Irreducible (X ^ n - C a))
this : Algebra K K[n√a] := ⋯
⊢ ↑((↑(autAdjoinRootXPowSubC n a)).toFun (AdjoinRootXPowSubCEquivToRootsOfUnity hζ H e)) (root (X ^ n - C a)) =
    ↑e (root (X ^ n - C a))
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: case splits'
K : Type u
inst✝ : Field K
n : ℕ
hζ✝ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
this✝ : Fact (Irreducible (X ^ n - C a))
this : Algebra K K[n√a] := inferInstance
w✝ : K
hζ : IsPrimitiveRoot w✝ n
⊢ (X ^ n - C ((algebraMap K K[n√a]) a)).Splits

Tactic:
exact X_pow_sub_C_splits_of_isPrimitiveRoot (hζ.map_of_injective (algebraMap K _).injective)
      (root_X_pow_sub_C_pow n a)

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)
α : L
hα✝ : α ^ n = (algebraMap K L) a
hζ : (primitiveRoots n K).Nonempty
H : Irreducible (X ^ n - C a)
hα : α ^ n = (algebraMap K L) a
⊢ Function.Bijective ⇑(liftAlgHom (X ^ n - C a) (Algebra.ofId K L) α ⋯)

Tactic:
have := Fact.mk H
    let := isSplittingField_AdjoinRoot_X_pow_sub_C hζ H
    refine ⟨(liftAlgHom (X ^ n - C a) _ α _).injective, ?_⟩
    rw [← AlgHom.range_eq_top, ← IsSplittingField.adjoin_rootSet _ (X ^ n - C a),
      eq_comm, Splits.adjoin_rootSet_eq_range, IsSplittingField.adjoin_rootSet]
    exact IsSplittingField.splits _ _

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 ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
inst✝ : DecidablePred FiniteIndex
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
k : κ
hkfi : (H ↑k.fst).FiniteIndex
hk : K k = D
hcovers' : ⋃ i ∈ {x | K x = D}, f i • ↑D = Set.univ
hHD : ∀ (i : ι), ¬(H i).FiniteIndex → H i ≠ D
i : ↥s
x✝ : i ∈ s.attach
hfi : ¬(H ↑i).FiniteIndex
⊢ ∑ s_1, ↑(if K ⟨i, s_1⟩ = D then 1 else 0) = 0 * ↑D.index

Tactic:
zero_mul

Goal state after:
case neg
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
inst✝ : DecidablePred FiniteIndex
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
k : κ
hkfi : (H ↑k.fst).FiniteIndex
hk : K k = D
hcovers' : ⋃ i ∈ {x | K x = D}, f i • ↑D = Set.univ
hHD : ∀ (i : ι), ¬(H i).FiniteIndex → H i ≠ D
i : ↥s
x✝ : i ∈ s.attach
hfi : ¬(H ↑i).FiniteIndex
⊢ ∑ s_1, ↑(if K ⟨i, s_1⟩ = D then 1 else 0) = 0
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: case refine_3
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
inst✝ : DecidablePred FiniteIndex
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
k : κ
hkfi : (H ↑k.fst).FiniteIndex
hk : K k = D
hcovers' : ⋃ i ∈ {x | K x = D}, f i • ↑D = Set.univ
hHD : ∀ (i : ι), ¬(H i).FiniteIndex → H i ≠ D
hdensity : ∑ i ∈ s, (↑(H i).index)⁻¹ = ↑{x | K x = D}.card * (↑D.index)⁻¹
⊢ {x | K x = D}.card = D.index → (↑({i ∈ s | (H i).FiniteIndex})).PairwiseDisjoint fun i ↦ g i • ↑(H i)

Tactic:
Finset.coe_filter

Goal state after:
case refine_3
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
inst✝ : DecidablePred FiniteIndex
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
k : κ
hkfi : (H ↑k.fst).FiniteIndex
hk : K k = D
hcovers' : ⋃ i ∈ {x | K x = D}, f i • ↑D = Set.univ
hHD : ∀ (i : ι), ¬(H i).FiniteIndex → H i ≠ D
hdensity : ∑ i ∈ s, (↑(H i).index)⁻¹ = ↑{x | K x = D}.card * (↑D.index)⁻¹
⊢ {x | K x = D}.card = D.index → {x | x ∈ s ∧ (H x).FiniteIndex}.PairwiseDisjoint fun i ↦ g i • ↑(H i)
Module: Mathlib.RingTheory.LinearDisjoint

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

Tactic:
exact Submodule.LinearDisjoint.one_right _

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✝ : L
⊢ x✝ = 0 ↔ x✝ ∈ {0}

Tactic:
Set.mem_singleton_iff

Goal state after:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x✝ : L
⊢ x✝ = 0 ↔ x✝ = 0
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
⊢ iterateFrobeniusAux K L p n (a + b) = iterateFrobeniusAux K L p n a + iterateFrobeniusAux K L p n b

Tactic:
by
    have inj := (algebraMap K L).injective
    have : ExpChar L p := expChar_of_injective_ringHom inj p
    apply inj
    rw [(algebraMap K L).map_add,
      algebraMap_iterateFrobeniusAux K p hn a,
      algebraMap_iterateFrobeniusAux K p hn b,
      algebraMap_iterateFrobeniusAux K p hn (a + b),
      add_pow_expChar_pow a b]

Goal state after:
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
q : ℕ
hF : ExpChar F q
S : Set E
⊢ (∀ x ∈ S, x ∈ ↑(perfectClosure F E)) ↔ ∀ x ∈ S, x ∈ perfectClosure F E

Tactic:
SetLike.mem_coe

Goal state after:
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
q n : ℕ
hF : ExpChar F q
ι : Type u_1
v : ι → E
hsep : ∀ (i : ι), IsSeparable F (v i)
h : LinearIndependent F v
⊢ LinearIndependent F fun x ↦ v x ^ q ^ n

Tactic:
by
  let E' := adjoin F (Set.range v)
  have : Algebra.IsSeparable F E' := (isSeparable_adjoin_iff_isSeparable F _).2 <| by
    rintro _ ⟨y, rfl⟩; exact hsep y
  let v' (i : ι) : E' := ⟨v i, subset_adjoin F _ ⟨i, rfl⟩⟩
  have h' : LinearIndependent F v' := h.of_comp E'.val.toLinearMap
  exact (h'.map_pow_expChar_pow_of_isSeparable q n).map'
    E'.val.toLinearMap (LinearMap.ker_eq_bot_of_injective E'.val.injective)

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

Tactic:
rw [sepDegree, sepDegree, separableClosure.eq_restrictScalars_of_isSeparable 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.IsSeparable F E
⊢ Cardinal.lift.{w, v} (Module.rank F E) * Cardinal.lift.{v, w} (Module.rank E ↥(separableClosure E K)) =
    Cardinal.lift.{v, w} (Module.rank F ↥(restrictScalars F (separableClosure E K)))
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

Goal state before:
pp: case pos
K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ∃ c, f = C c
⊢ (f.minpolyX ↥K⟮f⟯).natDegree = max f.num.natDegree f.denom.natDegree

pp: case neg
K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ¬∃ c, f = C c
⊢ (f.minpolyX ↥K⟮f⟯).natDegree = max f.num.natDegree f.denom.natDegree

Tactic:
· obtain ⟨c, rfl⟩ := hf
    simp

Goal state after:
case neg
K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ¬∃ c, f = C c
⊢ (f.minpolyX ↥K⟮f⟯).natDegree = max f.num.natDegree f.denom.natDegree
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
⊢ sepDegree F K = sepDegree E K

Tactic:
by
  convert! sepDegree_eq_of_isPurelyInseparable_of_isSeparable F E (separableClosure E K)
  have : IsScalarTower F (separableClosure E K) K := IsScalarTower.of_algebraMap_eq (congrFun rfl)
  rw [sepDegree, ← separableClosure.map_eq_of_separableClosure_eq_bot F
    (separableClosure.separableClosure_eq_bot E K)]
  exact (separableClosure F (separableClosure E K)).equivMap
    (IsScalarTower.toAlgHom F (separableClosure E K) K) |>.symm.toLinearEquiv.rank_eq

Goal state after:
Module: Mathlib.FieldTheory.Relrank

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

Tactic:
relrank_eq_rank_of_le h

Goal state after:
E : Type v
inst✝ : Field E
A B : Subfield E
h : A ≤ B
⊢ Module.rank ↥A ↥(extendScalars h) * Module.rank (↥B) E = Module.rank (↥A) E
Module: Mathlib.FieldTheory.RatFunc.Valuation

Goal state before:
pp: case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F⟮X⟯
x y : F⟮X⟯
hx : x = 0
⊢ 0 = 0 * if y = 0 then 0 else exp y.intDegree

Tactic:
zero_mul

Goal state after:
case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F⟮X⟯
x y : F⟮X⟯
hx : x = 0
⊢ 0 = 0
Module: Mathlib.FieldTheory.Relrank

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
h : A ≤ B
⊢ Module.rank F ↥A * A.relrank B = Module.rank F ↥B

Tactic:
relrank_eq_rank_of_le 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
h : A ≤ B
⊢ Module.rank F ↥A * Module.rank ↥A ↥(extendScalars h) = Module.rank F ↥B
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)
⊢ Associated ((Polynomial.mapRingHom (algebraMap K F)) (f E)) ((Polynomial.mapRingHom (algebraMap K F)) (g E))

Tactic:
← associated_mul_isUnit_left_iff isUnit₂,

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)
⊢ Associated ((Polynomial.mapRingHom (algebraMap K F)) (f E) * Polynomial.C ((aeval α) (g E)))
    ((Polynomial.mapRingHom (algebraMap K F)) (g E))
Module: Mathlib.Geometry.Euclidean.Altitude

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
i : Fin (n + 1)
⊢ (s.altitude i).direction = (vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)

Tactic:
altitude_def,

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
i : Fin (n + 1)
⊢ (mk' (s.points i) (affineSpan ℝ (s.points '' {i}ᶜ)).directionᗮ ⊓ affineSpan ℝ (Set.range s.points)).direction =
    (vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)
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
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
i : Fin (n + 1)
⊢ AffineSubspace.map S.subtype ((s.restrict S hS).altitude i) = s.altitude i

Tactic:
rw [eq_comm]
  convert! (s.restrict S hS).altitude_map S.subtypeₐᵢ i

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

Goal state before:
pp: case mp
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
⊢ vectorSpan ℝ {p, s.points i} = (s.altitude i).direction →
    p ≠ s.points i ∧
      p -ᵥ s.points i ∈ vectorSpan ℝ (Set.range s.points) ∧ p -ᵥ s.points i ∈ (vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ

Tactic:
intro h
    constructor
    · intro heq
      rw [heq, Set.pair_eq_singleton, vectorSpan_singleton] at h
      have hd : finrank ℝ (s.altitude i).direction = 0 := by rw [← h, finrank_bot]
      simp at hd
    · rw [← Submodule.mem_inf, _root_.inf_comm, ← direction_altitude, ← h]
      exact
        vsub_mem_vectorSpan ℝ (Set.mem_insert _ _) (Set.mem_insert_of_mem _ (Set.mem_singleton _))

Goal state after:
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)
⊢ s.points j -ᵥ s.altitudeFoot j ∈ ↑(vectorSpan ℝ (Set.range s.points))ᗮ

Tactic:
SetLike.mem_coe

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)
⊢ s.points j -ᵥ s.altitudeFoot j ∈ (vectorSpan ℝ (Set.range s.points))ᗮ
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

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
h : o.oangle x y - ↑π = 0
⊢ o.oangle x y = ↑π

Tactic:
sub_eq_zero

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
h : o.oangle x y = ↑π
⊢ o.oangle x y = ↑π
Module: Mathlib.Geometry.Euclidean.Altitude

Goal state before:
pp: case inl.refine_1
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 : Fin (n + 1)
⊢ -(s.height i * s.height i) < 0

Tactic:
rw [neg_lt_zero]
      positivity

Goal state after:
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
⊢ ‖p₁ -ᵥ p₃‖ * ‖p₁ -ᵥ p₃‖ = ‖p₁ -ᵥ p₂‖ * ‖p₁ -ᵥ p₂‖ + dist p₂ p₃ * dist p₂ p₃ ↔ ∠ p₁ p₂ p₃ = π / 2

Tactic:
dist_eq_norm_vsub V p₂ p₃,

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
⊢ ‖p₁ -ᵥ p₃‖ * ‖p₁ -ᵥ p₃‖ = ‖p₁ -ᵥ p₂‖ * ‖p₁ -ᵥ p₂‖ + ‖p₂ -ᵥ p₃‖ * ‖p₂ -ᵥ p₃‖ ↔ ∠ p₁ p₂ p₃ = π / 2