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

Goal state before:
pp: case mp
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
⊢ A.Definable L s → ∃ A0, ↑A0 ⊆ A ∧ (↑A0).Definable L s

pp: case mpr
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
⊢ (∃ A0, ↑A0 ⊆ A ∧ (↑A0).Definable L s) → A.Definable L s

Tactic:
· simp only [definable_iff_exists_formula_sum]
    rintro ⟨φ, rfl⟩
    let A0 := (φ.freeVarFinset.toLeft).image Subtype.val
    refine ⟨A0, by simp [A0], (φ.restrictFreeVar <| fun x => Sum.casesOn x.1
        (fun x hx => Sum.inl ⟨x, by simp [A0, hx]⟩) (fun x _ => Sum.inr x) x.2), ?_⟩
    ext
    simp only [Formula.Realize, mem_ofPred_eq, Finset.coe_sort_coe]
    exact iff_comm.1 <| BoundedFormula.realize_restrictFreeVar _ (by simp)

Goal state after:
case mpr
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
⊢ (∃ A0, ↑A0 ⊆ A ∧ (↑A0).Definable L s) → A.Definable L s
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: case inl
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
hφ : T ⊨ᵇ φ
⊢ ↑(Nonempty.some ⋯) ⊨ φ

Tactic:
exact models_sentence_iff.1 hφ _

Goal state after:
Module: Mathlib.GroupTheory.OreLocalization.Cardinality

Goal state before:
pp: case inl
R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : MulAction R X
hc : ∀ (s s' : ↥S), Commute s s'
h✝ : Finite X
⊢ #(OreLocalization S X) ≤ lift.{u, v} #X

Tactic:
have := lift_mk_le_lift_mk_of_surjective (oreDiv_one_surjective_of_finite_right S X)
    rwa [lift_umax.{v, u}, lift_id'] at this

Goal state after:
Module: Mathlib.FieldTheory.FinTrdeg

Goal state before:
pp: case mp
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E : IntermediateField K L
fg : E.FG
alg : Algebra.IsAlgebraic (↥E) L
⊢ Algebra.trdeg K L < Cardinal.aleph0

Tactic:
← trdeg_add_eq K E,

Goal state after:
case mp
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E : IntermediateField K L
fg : E.FG
alg : Algebra.IsAlgebraic (↥E) L
⊢ Algebra.trdeg K ↥E + Algebra.trdeg (↥E) L < Cardinal.aleph0
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 ι
h₂ : (∀ 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 (f a✝ * (Multiset.map f s✝).prod) = logDeriv (f a✝) + logDeriv (Multiset.map f s✝).prod

Tactic:
apply logDeriv_mul
      · simp [h]
      · simp_all

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

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝¹² : Field F
inst✝¹¹ : Field K
inst✝¹⁰ : Differential F
inst✝⁹ : Differential K
inst✝⁸ : Algebra F K
inst✝⁷ : DifferentialAlgebra F K
A : Type u_3
inst✝⁶ : Field A
inst✝⁵ : Algebra K A
inst✝⁴ : Algebra F A
inst✝³ : Differential A
inst✝² : IsScalarTower F K A
inst✝¹ : ContainConstants F K
inst1 : IsLiouville F K
inst2 : IsLiouville K A
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → A
v : A
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
⊢ ∃ ι₀ x c₀, ∃ (_ : ∀ (x : ι₀), (c₀ x)′ = 0), ∃ u₀ v₀, a = ∑ x, c₀ x * logDeriv (u₀ x) + v₀′

Tactic:
by
    obtain ⟨ι₀, _, c₀, hc₀, u₀, v₀, h₀⟩ := inst2.isLiouville (a : K) ι
        ((↑) ∘ c)
        (fun _ ↦ by simp only [Function.comp_apply, ← coe_deriv, coe_eq_zero_iff, hc])
        ((↑) ∘ u) v (by simpa only [Function.comp_apply, ← IsScalarTower.algebraMap_apply])
    have hc (x : ι₀) := mem_range_of_deriv_eq_zero F (hc₀ x)
    choose c₀ hc using hc
    apply inst1.isLiouville a ι₀ c₀ _ u₀ v₀
    · rw [h₀]
      simp [hc]
    · intro
      apply_fun ((↑) : F → K)
      · simp only [coe_deriv, hc, algebraMap.coe_zero]
        apply hc₀
      · apply FaithfulSMul.algebraMap_injective

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

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁸ : Field F
inst✝⁷ : Field K
inst✝⁶ : Differential F
inst✝⁵ : Differential K
inst✝⁴ : Algebra F K
inst✝³ : DifferentialAlgebra F K
inst✝² : CharZero F
B : IntermediateField F K
inst✝¹ : FiniteDimensional F ↥B
inst : IsLiouville F K
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → ↥B
v : ↥B
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
⊢ ↑a = ∑ x, ↑(c x) * logDeriv ((⇑B.val ∘ u) x) + (B.val v)′

Tactic:
dsimp only [coe_val, Function.comp_apply]

Goal state after:
F : Type u_1
K : Type u_2
inst✝⁸ : Field F
inst✝⁷ : Field K
inst✝⁶ : Differential F
inst✝⁵ : Differential K
inst✝⁴ : Algebra F K
inst✝³ : DifferentialAlgebra F K
inst✝² : CharZero F
B : IntermediateField F K
inst✝¹ : FiniteDimensional F ↥B
inst : IsLiouville F K
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → ↥B
v : ↥B
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
⊢ ↑a = ∑ x, ↑(c x) * logDeriv ↑(u x) + (↑v)′
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 j : (Module.rank F E).ord.ToType
h : i < j
⊢ φ i < φ j

Tactic:
have least := isLeast_leastExt (F := F) (E := E)
  by_contra!
  obtain eq | lt := this.eq_or_lt
  · exact (least j).1 (subset_adjoin _ _ ⟨i, h, congr_arg b eq.symm⟩)
  · 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.Galois.Profinite

Goal state before:
pp: k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
L : FiniteGaloisIntermediateField k K
fix1 : Set
  ((L : (FiniteGaloisIntermediateField k K)ᵒᵖ) → ↑((asProfiniteGaloisGroupFunctor k K).obj L).toProfinite.toTop) :=
  {f | f (op L) = 1}
x : ↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop
⊢ x ∈ ⇑(mulEquivToLimit k K) '' ↑L.fixingSubgroup ↔ x ∈ Subtype.val ⁻¹' fix1

Tactic:
obtain ⟨σ, rfl⟩ := (mulEquivToLimit k K).surjective x

Goal state after:
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
L : FiniteGaloisIntermediateField k K
fix1 : Set
  ((L : (FiniteGaloisIntermediateField k K)ᵒᵖ) → ↑((asProfiniteGaloisGroupFunctor k K).obj L).toProfinite.toTop) :=
  {f | f (op L) = 1}
σ : Gal(K/k)
⊢ (mulEquivToLimit k K) σ ∈ ⇑(mulEquivToLimit k K) '' ↑L.fixingSubgroup ↔ (mulEquivToLimit k K) σ ∈ Subtype.val ⁻¹' fix1
Module: Mathlib.FieldTheory.JacobsonNoether

Goal state before:
pp: case neg
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
h_exist : ∃ n, 0 < n ∧ (⇑((ad (↥k) D) a))^[n + 1] b = 0
t : ℕ := Nat.find h_exist - 1
ht : t = Nat.find h_exist - 1
h_pos : t ≤ 0
⊢ Nat.find h_exist = 1

Tactic:
rw [Nat.le_zero, ht, Nat.sub_eq_zero_iff_le] at h_pos

Goal state after:
case neg
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
h_exist : ∃ n, 0 < n ∧ (⇑((ad (↥k) D) a))^[n + 1] b = 0
t : ℕ := Nat.find h_exist - 1
ht : t = Nat.find h_exist - 1
h_pos : Nat.find h_exist ≤ 1
⊢ Nat.find h_exist = 1
Module: Mathlib.RingTheory.MvPolynomial

Goal state before:
pp: σ : Type u
K : Type v
inst✝ : Field K
I : Ideal (MvPolynomial σ K)
hI : I ≠ ⊤
x : K
hx : C x ∈ I
hx0 : ¬x = 0
this : C 1 ∈ I
⊢ 1 ∈ I

Tactic:
MvPolynomial.C_1

Goal state after:
σ : Type u
K : Type v
inst✝ : Field K
I : Ideal (MvPolynomial σ K)
hI : I ≠ ⊤
x : K
hx : C x ∈ I
hx0 : ¬x = 0
this : 1 ∈ I
⊢ 1 ∈ I
Module: Mathlib.FieldTheory.JacobsonNoether

Goal state before:
pp: L : Type u_2
D : Type u_3
inst✝⁴ : Field L
inst✝³ : DivisionRing D
inst✝² : Algebra L D
inst✝¹ : Algebra.IsAlgebraic L D
inst✝ : IsCentral L D
hneq : ⊥ ≠ ⊤
hcenter : Subalgebra.center L D = ⊥
ntrivial : k ≠ ⊤
φ : ↥⊥ ≃ₐ[L] ↥(Subalgebra.center L D) := ⊥.equivOfEq (Subalgebra.center L D) ⋯
equiv : L ≃+* ↥k := ((botEquiv L D).symm.trans φ).toRingEquiv
x✝⁴ : Algebra L ↥k := equiv.toRingHom.toAlgebra
x✝³ : Algebra (↥k) L := equiv.symm.toRingHom.toAlgebra
x✝² : IsScalarTower L (↥k) D
x✝¹ : IsScalarTower (↥k) L D
x✝ : Algebra.IsAlgebraic (↥k) D
⊢ ∃ x ∉ ⊥, IsSeparable L x

Tactic:
obtain ⟨x, hxd, hx⟩ := exists_separable_and_not_isCentral D ntrivial

Goal state after:
L : Type u_2
D : Type u_3
inst✝⁴ : Field L
inst✝³ : DivisionRing D
inst✝² : Algebra L D
inst✝¹ : Algebra.IsAlgebraic L D
inst✝ : IsCentral L D
hneq : ⊥ ≠ ⊤
hcenter : Subalgebra.center L D = ⊥
ntrivial : k ≠ ⊤
φ : ↥⊥ ≃ₐ[L] ↥(Subalgebra.center L D) := ⊥.equivOfEq (Subalgebra.center L D) ⋯
equiv : L ≃+* ↥k := ((botEquiv L D).symm.trans φ).toRingEquiv
x✝⁴ : Algebra L ↥k := equiv.toRingHom.toAlgebra
x✝³ : Algebra (↥k) L := equiv.symm.toRingHom.toAlgebra
x✝² : IsScalarTower L (↥k) D
x✝¹ : IsScalarTower (↥k) L D
x✝ : Algebra.IsAlgebraic (↥k) D
x : D
hxd : x ∉ k
hx : IsSeparable (↥k) x
⊢ ∃ x ∉ ⊥, IsSeparable L x
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
⊢ (adjoinRootXPowSubCEquiv hζ H hα) ((adjoinRootXPowSubCEquiv hζ H hα).symm α) =
    (adjoinRootXPowSubCEquiv hζ H hα) (root (X ^ n - C a))

Tactic:
rw [(adjoinRootXPowSubCEquiv hζ H hα).apply_symm_apply, adjoinRootXPowSubCEquiv_root]

Goal state after:
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: 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
⊢ ⋃ k ∈ {i ∈ s | (H i).FiniteIndex}, g k • ↑(H k) = Set.univ ∧
    1 ≤ ∑ i ∈ s, (↑(H i).index)⁻¹ ∧
      (∑ i ∈ s, (↑(H i).index)⁻¹ = 1 → (↑({i ∈ s | (H i).FiniteIndex})).PairwiseDisjoint fun i ↦ g i • ↑(H i))

Tactic:
have hdensity : ∑ i ∈ s, ((H i).index : ℚ)⁻¹ =
      (Finset.univ.filter (K · = D)).card * (D.index : ℚ)⁻¹ := by
    rw [eq_mul_inv_iff_mul_eq₀ (Nat.cast_ne_zero.mpr hD.index_ne_zero), Finset.sum_mul,
      ← Finset.sum_attach, eq_comm, Finset.card_filter, Nat.cast_sum, ← Finset.univ_sigma_univ,
      Finset.sum_sigma, Finset.sum_coe_sort_eq_attach]
    refine Finset.sum_congr rfl fun i _ => ?_
    by_cases hfi : (H i).FiniteIndex
    · rw [← relIndex_mul_index (hD_le i.2 hfi), Nat.cast_mul, mul_comm,
        mul_inv_cancel_right₀ (Nat.cast_ne_zero.mpr hfi.index_ne_zero)]
      simpa [K, hfi] using! (ht i.1 i.2 hfi).1.card_left
    · rw [of_not_not (FiniteIndex.mk.mt hfi), Nat.cast_zero, inv_zero, zero_mul]
      simpa [K, hfi] using! hHD i hfi

Goal state after:
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)⁻¹
⊢ ⋃ k ∈ {i ∈ s | (H i).FiniteIndex}, g k • ↑(H k) = Set.univ ∧
    1 ≤ ∑ i ∈ s, (↑(H i).index)⁻¹ ∧
      (∑ i ∈ s, (↑(H i).index)⁻¹ = 1 → (↑({i ∈ s | (H i).FiniteIndex})).PairwiseDisjoint fun i ↦ g i • ↑(H i))
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 = (Multiset.map (fun x ↦ X - C x) (c.minpoly.aroots L).dedup).prod

Tactic:
rw [Multiset.dedup_eq_self.mpr (nodup_roots c.separable_minpoly.map),
    prod_multiset_X_sub_C_of_monic_of_roots_card_eq (c.monic_minpoly.map _)]

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).roots.card = (map (algebraMap K L) c.minpoly).natDegree
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
⊢ (algebraMap K L) (iterateFrobeniusAux K L p n (a * b)) =
    (algebraMap K L) (iterateFrobeniusAux K L p n a * iterateFrobeniusAux K L p n b)

Tactic:
rw [(algebraMap K L).map_mul,
      algebraMap_iterateFrobeniusAux K p hn a,
      algebraMap_iterateFrobeniusAux K p hn b,
      algebraMap_iterateFrobeniusAux K p hn (a * b),
      mul_pow]

Goal state after:
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
inst✝¹ : Free R ↥A
inst✝ : Free R ↥B
⊢ finrank R ↥(A ⊔ B) = finrank R ↥A * finrank R ↥B

Tactic:
simpa only [map_mul] using! congr(Cardinal.toNat $(H.rank_sup_of_free))

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✝² : IsGalois F ↥A
inst✝¹ : FiniteDimensional F ↥A
inst✝ : FiniteDimensional F ↥B
h : A ⊓ B = ⊥
C : IntermediateField F E := A ⊔ B
A' : IntermediateField F ↥C := restrict ⋯
B' : IntermediateField F ↥C := restrict ⋯
hA : IntermediateField.map C.val A' = A
hB : IntermediateField.map C.val B' = B
h₁ : A' ⊔ B' = ⊤
h₂ : A' ⊓ B' = ⊥
⊢ A'.LinearDisjoint ↥B'

Tactic:
have : IsGalois F A' := IsGalois.of_algEquiv <| restrictAlgEquiv ..

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 ↥A
inst✝ : FiniteDimensional F ↥B
h : A ⊓ B = ⊥
C : IntermediateField F E := A ⊔ B
A' : IntermediateField F ↥C := restrict ⋯
B' : IntermediateField F ↥C := restrict ⋯
hA : IntermediateField.map C.val A' = A
hB : IntermediateField.map C.val B' = B
h₁ : A' ⊔ B' = ⊤
h₂ : A' ⊓ B' = ⊥
this : IsGalois F ↥A'
⊢ A'.LinearDisjoint ↥B'
Module: Mathlib.FieldTheory.RatFunc.Degree

Goal state before:
pp: K : Type u
inst✝ : Field K
x : K⟮X⟯
hx : x ≠ 0
s : K[X]
hs : s ≠ 0
⊢ x.num * s * x.denom = x.num * (s * x.denom)

Tactic:
rw [mul_assoc]

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
S : Set K
inst✝¹ : IsPurelyInseparable F E
M : IntermediateField F K := adjoin F S
inst✝ : Algebra.IsAlgebraic F ↥M
L : IntermediateField E K := adjoin E S
E' : IntermediateField F K := (IsScalarTower.toAlgHom F E K).fieldRange
j : E ≃ₐ[F] ↥E' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F E K)
⊢ M ≤ restrictScalars F (adjoin (↥E') S)

Tactic:
restrictScalars_adjoin

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
S : Set K
inst✝¹ : IsPurelyInseparable F E
M : IntermediateField F K := adjoin F S
inst✝ : Algebra.IsAlgebraic F ↥M
L : IntermediateField E K := adjoin E S
E' : IntermediateField F K := (IsScalarTower.toAlgHom F E K).fieldRange
j : E ≃ₐ[F] ↥E' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F E K)
⊢ M ≤ adjoin F (↑E' ∪ S)
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
S : Set K
inst✝¹ : IsPurelyInseparable F E
M : IntermediateField F K := adjoin F S
inst✝ : Algebra.IsAlgebraic F ↥M
L : IntermediateField E K := adjoin E S
E' : IntermediateField F K := (IsScalarTower.toAlgHom F E K).fieldRange
j : E ≃ₐ[F] ↥E' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F E K)
hi : M ≤ restrictScalars F L
i : ↥M →+* ↥L := Subsemiring.inclusion hi
this✝² : Algebra ↥M ↥L := i.toAlgebra
this✝¹ : SMul ↥M ↥L := this✝².toSMul
this✝ : IsScalarTower F ↥M ↥L
q : ℕ
h✝ : ExpChar F q
this : extendScalars hi = adjoin ↥M ↑E'
⊢ IsPurelyInseparable ↥M ↥(adjoin ↥M ↑E')

Tactic:
isPurelyInseparable_adjoin_iff_pow_mem _ _ q

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
S : Set K
inst✝¹ : IsPurelyInseparable F E
M : IntermediateField F K := adjoin F S
inst✝ : Algebra.IsAlgebraic F ↥M
L : IntermediateField E K := adjoin E S
E' : IntermediateField F K := (IsScalarTower.toAlgHom F E K).fieldRange
j : E ≃ₐ[F] ↥E' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F E K)
hi : M ≤ restrictScalars F L
i : ↥M →+* ↥L := Subsemiring.inclusion hi
this✝² : Algebra ↥M ↥L := i.toAlgebra
this✝¹ : SMul ↥M ↥L := this✝².toSMul
this✝ : IsScalarTower F ↥M ↥L
q : ℕ
h✝ : ExpChar F q
this : extendScalars hi = adjoin ↥M ↑E'
⊢ ∀ x ∈ ↑E', ∃ n, x ^ q ^ n ∈ (algebraMap (↥M) K).range
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
φ_map : (mapEquiv e.toRingEquiv) φ = f.minpolyX ↥K[f]
⊢ Irreducible φ

Tactic:
have : φ = Bivariate.swap
      (Polynomial.C f.num - Polynomial.X * Polynomial.C f.denom) := by
    simp only [X_mul_C, Bivariate.swap_apply, aevalAeval, aevalAevalEquiv, Equiv.coe_fn_mk,
      AlgHom.coe_comp, AlgHom.coe_restrictScalars', coe_aeval_eq_eval, Function.comp_apply,
      aeval_sub, aeval_C, algebraMap_def, coe_mapRingHom, map_mul, aeval_X, eval_sub,
      eval_map_algebraMap, Polynomial.eval_mul, Polynomial.eval_C]
    rw [mul_comm]
    rfl

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
φ_map : (mapEquiv e.toRingEquiv) φ = f.minpolyX ↥K[f]
this : φ = Bivariate.swap (Polynomial.C f.num - Polynomial.X * Polynomial.C f.denom)
⊢ Irreducible φ
Module: Mathlib.FieldTheory.Relrank

Goal state before:
pp: E : Type v
inst✝¹ : Field E
A B : Subfield E
L : Type v
inst✝ : Field L
f : E →+* L
⊢ (map f A).relrank (map f B) = A.relrank B

Tactic:
by
  simpa only [lift_id] using lift_relrank_map_map A B f

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 ≠ ⊥
⊢ (Φ E).coeff (φ E).natDegree = (c E).num

Tactic:
by
  apply algebraMap_injective
  rw [Φ_coeff_φ_natDegree h]
  conv_lhs => rw [← num_div_denom (c E), c_denom h, map_one, div_one]

Goal state after:
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
L : Type v
inst✝¹ : Field L
inst✝ : Algebra F L
f : E →ₐ[F] L
⊢ (map f A).relrank (map f B) = A.relrank B

Tactic:
by
  simpa only [lift_id] using lift_relrank_map_map A B f

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

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsOrderedRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
C F : PointedCone R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Function.Injective ⇑f
sub : map f F ≤ map f C
hF : ∀ {x y : N} {a : R}, x ∈ map f C → y ∈ map f C → 0 < a → a • x + y ∈ map f F → x ∈ map f F
x : M
xf : x ∈ F
⊢ x ∈ C

Tactic:
obtain ⟨y, yC, hy⟩ := mem_map.mp <| sub (mem_map_of_mem xf)

Goal state after:
case refine_1
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsOrderedRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
C F : PointedCone R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Function.Injective ⇑f
sub : map f F ≤ map f C
hF : ∀ {x y : N} {a : R}, x ∈ map f C → y ∈ map f C → 0 < a → a • x + y ∈ map f F → x ∈ map f F
x : M
xf : x ∈ F
y : M
yC : y ∈ C
hy : f y = (↑{ c // 0 ≤ c } f) x
⊢ x ∈ C
Module: Mathlib.Geometry.Euclidean.Projection

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace 𝕜 V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst✝¹ : Nonempty ↥s
inst✝ : s.direction.HasOrthogonalProjection
p₁ p₂ p₃ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
⊢ dist p₁ ↑((orthogonalProjection s) p₃) * dist p₁ ↑((orthogonalProjection s) p₃) +
        dist p₃ ↑((orthogonalProjection s) p₃) * dist p₃ ↑((orthogonalProjection s) p₃) =
      dist p₂ p₃ * dist p₂ p₃ ↔
    dist p₁ ↑((orthogonalProjection s) p₃) * dist p₁ ↑((orthogonalProjection s) p₃) =
      dist p₂ ↑((orthogonalProjection s) p₃) * dist p₂ ↑((orthogonalProjection s) p₃)

Tactic:
dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq p₃ hp₂

Goal state after:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace 𝕜 V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst✝¹ : Nonempty ↥s
inst✝ : s.direction.HasOrthogonalProjection
p₁ p₂ p₃ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
⊢ dist p₁ ↑((orthogonalProjection s) p₃) * dist p₁ ↑((orthogonalProjection s) p₃) +
        dist p₃ ↑((orthogonalProjection s) p₃) * dist p₃ ↑((orthogonalProjection s) p₃) =
      dist p₂ ↑((orthogonalProjection s) p₃) * dist p₂ ↑((orthogonalProjection s) p₃) +
        dist p₃ ↑((orthogonalProjection s) p₃) * dist p₃ ↑((orthogonalProjection s) p₃) ↔
    dist p₁ ↑((orthogonalProjection s) p₃) * dist p₁ ↑((orthogonalProjection s) p₃) =
      dist p₂ ↑((orthogonalProjection s) p₃) * dist p₂ ↑((orthogonalProjection s) p₃)