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

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝¹ : L.Structure M
α : Type u₁
β : Type u_1
s : Set (β → M)
h : A.Definable L s
f : α ↪ β
inst✝ : Finite β
⊢ A.Definable L ((fun g ↦ g ∘ ⇑f) '' s)

Tactic:
cases nonempty_fintype β

Goal state after:
case intro
M : Type w
A : Set M
L : Language
inst✝¹ : L.Structure M
α : Type u₁
β : Type u_1
s : Set (β → M)
h : A.Definable L s
f : α ↪ β
inst✝ : Finite β
val✝ : Fintype β
⊢ A.Definable L ((fun g ↦ g ∘ ⇑f) '' s)
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: case intro
M : Type w
A : Set M
L : Language
inst✝² : L.Structure M
α : Type u₁
β : Type u_1
s : Set (β → M)
h : A.Definable L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝ : Fintype α
⊢ A.Definable L ((fun g ↦ g ∘ f) '' s)

Tactic:
cases nonempty_fintype β

Goal state after:
case intro.intro
M : Type w
A : Set M
L : Language
inst✝² : L.Structure M
α : Type u₁
β : Type u_1
s : Set (β → M)
h : A.Definable L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
⊢ A.Definable L ((fun g ↦ g ∘ f) '' s)
Module: Mathlib.ModelTheory.Skolem

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
κ : Cardinal.{w'}
h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ
h4 : lift.{w, w'} κ ≤ lift.{w', w} #M
s' : Set (ULift.{w', w} M)
h2 : lift.{w', w} #↑s ≤ #↑s'
h1 : ℵ₀ ≤ #↑s'
hs' : #↑s' = lift.{w, w'} κ
this : Nonempty M
h : lift.{max w w', w} #↑(⇑Equiv.ulift '' s') = lift.{w, max w w'} #↑s'
⊢ lift.{w', w} #↥((closure (L.sum L.skolem₁)).toFun (s ∪ ⇑Equiv.ulift '' s')).elementarySkolem₁Reduct = #↑s'

Tactic:
lift_umax.{w, w'},

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
κ : Cardinal.{w'}
h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ
h4 : lift.{w, w'} κ ≤ lift.{w', w} #M
s' : Set (ULift.{w', w} M)
h2 : lift.{w', w} #↑s ≤ #↑s'
h1 : ℵ₀ ≤ #↑s'
hs' : #↑s' = lift.{w, w'} κ
this : Nonempty M
h : lift.{w', w} #↑(⇑Equiv.ulift '' s') = lift.{w, max w w'} #↑s'
⊢ lift.{w', w} #↥((closure (L.sum L.skolem₁)).toFun (s ∪ ⇑Equiv.ulift '' s')).elementarySkolem₁Reduct = #↑s'
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝¹ : L.Structure M
α : Type u₁
β : Type u_1
inst✝ : Finite β
S : Set (α ⊕ β → M)
hS : A.Definable L S
⊢ A.Definable L {v | ∀ (u : β → M), Sum.elim v u ∈ S}

Tactic:
obtain ⟨φ, hφ⟩ := hS
  exists φ.iAlls β
  ext v
  simp [hφ]

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

Goal state before:
pp: p✝ : ℕ
K : Type u_2
inst✝¹ : Field K
inst✝ : CompatibleRing K
h✝ : K ⊨ Theory.ACF p✝
p : K[X]
hpm : p.Monic
hpi : Irreducible p
h : ∀ (φ : Language.ring.Sentence), ∀ x ∈ {n | 0 < n}, genericMonicPolyHasRoot x = φ → K ⊨ φ
this : K ⊨ genericMonicPolyHasRoot p.natDegree
⊢ ∃ x, eval x p = 0

Tactic:
rw [realize_genericMonicPolyHasRoot] at this

Goal state after:
p✝ : ℕ
K : Type u_2
inst✝¹ : Field K
inst✝ : CompatibleRing K
h✝ : K ⊨ Theory.ACF p✝
p : K[X]
hpm : p.Monic
hpi : Irreducible p
h : ∀ (φ : Language.ring.Sentence), ∀ x ∈ {n | 0 < n}, genericMonicPolyHasRoot x = φ → K ⊨ φ
this : ∀ (p_1 : { p_1 // p_1.Monic ∧ p_1.natDegree = p.natDegree }), ∃ x, eval x ↑p_1 = 0
⊢ ∃ x, eval x p = 0
Module: Mathlib.RingTheory.Nullstellensatz

Goal state before:
pp: k : Type u_1
K : Type u_2
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
σ : Type u_3
x : σ → K
⊢ (vanishingIdeal K {x}).IsMaximal

Tactic:
convert! RingHom.ker_isMaximal_of_surjective (aeval (R := K) x) ?_

Goal state after:
case e'_3
k : Type u_1
K : Type u_2
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
σ : Type u_3
x : σ → K
e_2✝ : AddMonoidAlgebra.semiring = AddMonoidAlgebra.ring.toSemiring
⊢ vanishingIdeal K {x} = RingHom.ker (aeval x)

k : Type u_1
K : Type u_2
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
σ : Type u_3
x : σ → K
⊢ Function.Surjective ⇑(aeval x)
Module: Mathlib.RingTheory.Nullstellensatz

Goal state before:
pp: k : Type u_1
K : Type u_2
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
σ : Type u_3
I : Ideal (MvPolynomial σ k)
⊢ I.radical ≤ vanishingIdeal k (zeroLocus K I)

Tactic:
by
  intro p hp x hx
  rw [← mem_vanishingIdeal_singleton_iff]
  rw [radical_eq_sInf] at hp
  refine
    (mem_sInf.mp hp)
      ⟨le_trans (le_vanishingIdeal_zeroLocus I)
          (vanishingIdeal_anti_mono fun y hy => hy.symm ▸ hx),
        inferInstance⟩

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

Goal state before:
pp: case inr.inr
k : Type u_1
inst✝ : Field k
f : k[X]
hi : Irreducible f
n : ℕ
h : f ∣ 1 - X
hn : n ≠ 0
h✝ : Infinite k
⊢ f.natDegree ∣ n

Tactic:
← dvd_neg,

Goal state after:
case inr.inr
k : Type u_1
inst✝ : Field k
f : k[X]
hi : Irreducible f
n : ℕ
h : f ∣ -(1 - X)
hn : n ≠ 0
h✝ : Infinite k
⊢ f.natDegree ∣ n
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 ∈ restrictDegree σ K (Fintype.card K - 1)

Tactic:
by
  classical
  rw [mem_restrictDegree_iff_sup, indicator]
  intro n
  refine le_trans (Multiset.count_le_of_le _ <| degrees_indicator _) (le_of_eq ?_)
  simp_rw [← Multiset.coe_countAddMonoidHom, map_sum,
    map_nsmul, Multiset.coe_countAddMonoidHom, nsmul_eq_mul, Nat.cast_id]
  trans
  · refine Finset.sum_eq_single n ?_ ?_
    · intro b _ ne
      simp [ne, eqComm]
    · intro h; exact (h <| Finset.mem_univ _).elim
  · rw [Multiset.count_singleton_self, mul_one]

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

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

Tactic:
obtain ⟨x, rfl⟩ := Set.range_piMap _ ▸ hx

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

Goal state before:
pp: k✝ : Type u_1
K✝ : Type u_2
inst✝⁶ : Field k✝
inst✝⁵ : Field K✝
inst✝⁴ : Algebra k✝ K✝
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
g : ↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop
x y : K
⊢ toAlgEquivAux g (x * y) = toAlgEquivAux g x * toAlgEquivAux g y

Tactic:
by
    have hx : x ∈ (adjoin k {x, y}).1 := subset_adjoin _ _ (Set.mem_insert x {y})
    have hy : y ∈ (adjoin k {x, y}).1 := subset_adjoin _ _ (Set.mem_insert_of_mem x rfl)
    rw [toAlgEquivAux_eq_liftNormal g x (adjoin k {x, y}) hx,
      toAlgEquivAux_eq_liftNormal g y (adjoin k {x, y}) hy,
      toAlgEquivAux_eq_liftNormal g (x * y) (adjoin k {x, y}) (mul_mem hx hy), map_mul]

Goal state after:
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n x : ℕ
⊢ ↑x = mk K p (n, ↑x)

Tactic:
induction n with
  | zero =>
    induction x with
    | zero => simp
    | succ x ih => simp [Nat.cast_succ, ih, one_def]
  | succ n ih =>
    rw [ih]; apply Quot.sound
    suffices R K p (n, (x : K)) (Nat.succ n, frobenius K p (x : K)) by
      rwa [map_natCast] at this
    apply R.intro

Goal state after:
Module: Mathlib.FieldTheory.Isaacs

Goal state before:
pp: F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (x : E), ∃ y, (aeval y) (minpoly F x) = 0
S : Finset E
p : K[X] := ∏ x ∈ S, Polynomial.map (algebraMap F K) (minpoly F x)
K' : Type u_3 := p.SplittingField
splits : ∀ s ∈ S, (Polynomial.map (algebraMap F K') (minpoly F s)).Splits
K₀ : IntermediateField F K' := restrictScalars F ⊥
FS : IntermediateField F E := adjoin F ↑S
Ω : Type (max u_2 u_3) := ↥FS →ₐ[F] K'
this✝ : FiniteDimensional F ↥(adjoin F ↑S)
M : Ω → Submodule F ↥FS := fun ω ↦ Subalgebra.toSubmodule (comap ω K₀).toSubalgebra
this : ⋃ ω, ↑(M ω) = Set.univ
h✝ : Finite F
α : ↥FS
hα : F⟮α⟯ = ⊤
ω : Ω
hω : α ∈ ↑(M ω)
⊢ ⊤ ≤ comap ω K₀

Tactic:
← hα,

Goal state after:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (x : E), ∃ y, (aeval y) (minpoly F x) = 0
S : Finset E
p : K[X] := ∏ x ∈ S, Polynomial.map (algebraMap F K) (minpoly F x)
K' : Type u_3 := p.SplittingField
splits : ∀ s ∈ S, (Polynomial.map (algebraMap F K') (minpoly F s)).Splits
K₀ : IntermediateField F K' := restrictScalars F ⊥
FS : IntermediateField F E := adjoin F ↑S
Ω : Type (max u_2 u_3) := ↥FS →ₐ[F] K'
this✝ : FiniteDimensional F ↥(adjoin F ↑S)
M : Ω → Submodule F ↥FS := fun ω ↦ Subalgebra.toSubmodule (comap ω K₀).toSubalgebra
this : ⋃ ω, ↑(M ω) = Set.univ
h✝ : Finite F
α : ↥FS
hα : F⟮α⟯ = ⊤
ω : Ω
hω : α ∈ ↑(M ω)
⊢ F⟮α⟯ ≤ comap ω K₀
Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality

Goal state before:
pp: case neg
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A B : IntermediateField F E
hA : Algebra.Transcendental F ↥A
hB : Algebra.Transcendental F ↥B
this✝¹ : Algebra.Transcendental F ↥(A ⊔ B)
this✝ : Infinite ↥A
this : Infinite ↥B
⊢ Cardinal.lift.{u, v} #↥(adjoin F (↑A ∪ ↑B)) ≤ Cardinal.lift.{u, v} (max #↥A #↥B)

Tactic:
refine (lift_cardinalMk_adjoin_le _ _).trans ?_

Goal state after:
case neg
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A B : IntermediateField F E
hA : Algebra.Transcendental F ↥A
hB : Algebra.Transcendental F ↥B
this✝¹ : Algebra.Transcendental F ↥(A ⊔ B)
this✝ : Infinite ↥A
this : Infinite ↥B
⊢ max (max (Cardinal.lift.{v, u} #F) (Cardinal.lift.{u, v} #↑(↑A ∪ ↑B))) ℵ₀ ≤ Cardinal.lift.{u, v} (max #↥A #↥B)
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: case refine_1
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⟮α⟯ = ⊤
⊢ (aeval α) (X ^ finrank K L - C a) = 0

Tactic:
simp only [aeval_def, eval₂_sub, eval₂_X_pow, ha, eval₂_C, sub_self]

Goal state after:
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: case adjoin_rootSet'
K : Type u
inst✝³ : Field K
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
a : K
α : L
ha : α ^ finrank K L = (algebraMap K L) a
hα : K⟮α⟯ = ⊤
⊢ ⊤.toSubalgebra ≤ Algebra.adjoin K ((X ^ finrank K L - C a).rootSet L)

Tactic:
← hα,

Goal state after:
case adjoin_rootSet'
K : Type u
inst✝³ : Field K
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
a : K
α : L
ha : α ^ finrank K L = (algebraMap K L) a
hα : K⟮α⟯ = ⊤
⊢ K⟮α⟯.toSubalgebra ≤ Algebra.adjoin K ((X ^ finrank K L - C a).rootSet L)
Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Semiring T
inst✝ : Algebra R T
A : Subalgebra R S
⊢ ∀ (a₁ a₂ : ↥⊥) (b₁ b₂ : ↥A),
    (toSubmodule A).lTensorOne ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) =
      (toSubmodule A).lTensorOne (a₁ ⊗ₜ[R] b₁) * (toSubmodule A).lTensorOne (a₂ ⊗ₜ[R] b₂)

Tactic:
rintro x y a b
    obtain ⟨x', hx⟩ := Algebra.mem_bot.1 x.2
    replace hx : algebraMap R _ x' = x := Subtype.val_injective hx
    obtain ⟨y', hy⟩ := Algebra.mem_bot.1 y.2
    replace hy : algebraMap R _ y' = y := Subtype.val_injective hy
    rw [← hx, ← hy, ← map_mul, (toSubmodule A).lTensorOne_tmul x' a,
      (toSubmodule A).lTensorOne_tmul y' b, (toSubmodule A).lTensorOne_tmul (x' * y') (a * b),
      Algebra.mul_smul_comm, Algebra.smul_mul_assoc, smul_smul, mul_comm x' y']

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 = ⊥
⊢ A.LinearDisjoint ↥B

Tactic:
let C : IntermediateField F E := A ⊔ B
  let A' : IntermediateField F C := A.restrict le_sup_left
  let B' : IntermediateField F C := B.restrict le_sup_right
  have hA : IntermediateField.map C.val A' = A := lift_restrict le_sup_left
  have hB : IntermediateField.map C.val B' = B := lift_restrict le_sup_right
  suffices A'.LinearDisjoint B' from hA ▸ hB ▸ LinearDisjoint.map this C.val
  have h₁ : A' ⊔ B' = ⊤ := by
    rw [← lift_inj, lift_top, lift_sup, lift_restrict le_sup_left, lift_restrict le_sup_right]
  have h₂ : A' ⊓ B' = ⊥ := by
    rw [← lift_inj, lift_bot, lift_inf, lift_restrict le_sup_left, lift_restrict le_sup_right, h]
  have : IsGalois F A' := IsGalois.of_algEquiv <| restrictAlgEquiv ..
  exact of_inf_eq_bot_aux h₁ h₂

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 : IntermediateField F E
L : Type w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
H : A.LinearDisjoint L
halg : Algebra.IsAlgebraic F ↥A ∨ Algebra.IsAlgebraic F L
L' : Subalgebra F E := (IsScalarTower.toAlgHom F L E).range
i : L ≃ₐ[F] ↥L' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)
⊢ Subsemiring.closure (Set.range ⇑(algebraMap L E) ∪ ↑A) = Subsemiring.closure (Set.range ⇑(algebraMap (↥L') E) ∪ ↑A)

Tactic:
congr 2

Goal state after:
case e_a
F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
H : A.LinearDisjoint L
halg : Algebra.IsAlgebraic F ↥A ∨ Algebra.IsAlgebraic F L
L' : Subalgebra F E := (IsScalarTower.toAlgHom F L E).range
i : L ≃ₐ[F] ↥L' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)
⊢ Set.range ⇑(algebraMap L E) = Set.range ⇑(algebraMap (↥L') E)
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 : IntermediateField F E
L : Type w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
H : A.LinearDisjoint L
halg : Algebra.IsAlgebraic F ↥A ∨ Algebra.IsAlgebraic F L
L' : Subalgebra F E := (IsScalarTower.toAlgHom F L E).range
⊢ Subsemiring.closure (↑A ∪ Set.range ⇑(algebraMap L E)) = Subsemiring.closure (Set.range ⇑(algebraMap (↥A) E) ∪ ↑L')

Tactic:
congr 2

Goal state after:
case e_a
F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
H : A.LinearDisjoint L
halg : Algebra.IsAlgebraic F ↥A ∨ Algebra.IsAlgebraic F L
L' : Subalgebra F E := (IsScalarTower.toAlgHom F L E).range
⊢ ↑A = Set.range ⇑(algebraMap (↥A) E)
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
inst✝ : Algebra.IsSeparable F E
h : LinearIndependent F v
⊢ LinearIndependent F fun x ↦ v x ^ q ^ n

Tactic:
classical
  rw [linearIndependent_iff_finset_linearIndependent] at h ⊢
  intro s
  let E' := adjoin F (s.image v : Set E)
  have : FiniteDimensional F E' := finiteDimensional_adjoin
    fun x _ ↦ Algebra.IsIntegral.isIntegral x
  let v' (i : s) : E' := ⟨v i.1, subset_adjoin F _ (Finset.mem_image.2 ⟨i.1, i.2, rfl⟩)⟩
  have h' : LinearIndependent F v' := (h s).of_comp E'.val.toLinearMap
  exact (h'.map_pow_expChar_pow_of_fd_isSeparable q n).map'
    E'.val.toLinearMap (LinearMap.ker_eq_bot_of_injective E'.val.injective)

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

Goal state before:
pp: case neg
K : Type u
inst✝ : Field K
x : K⟮X⟯
hx : ¬x = 0
⊢ (-x).intDegree = x.intDegree

Tactic:
rw [intDegree, intDegree, ← natDegree_neg x.num]
    exact
      natDegree_sub_eq_of_prod_eq (num_ne_zero (neg_ne_zero.mpr hx)) (denom_ne_zero (-x))
        (neg_ne_zero.mpr (num_ne_zero hx)) (denom_ne_zero x) (num_denom_neg x)

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 v
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : IsPurelyInseparable F E
⊢ Module.rank F E * insepDegree E K = insepDegree F K

Tactic:
by
  simpa only [Cardinal.lift_id] using lift_rank_mul_lift_insepDegree_of_isPurelyInseparable F E K

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
⊢ 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]

Tactic:
congr 2

Goal state after:
case e_a.e_f
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
⊢ (↑(aeval ⟨f, ⋯⟩)).comp Polynomial.C = algebraMap K ↥K[f]

case e_a.e_a
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.denom = Polynomial.map (algebraMap K ↥K[f]) f.denom
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 F : PointedCone R M
h : F.IsFaceOf C
x✝ : M
xc : x✝ ∈ ↑C
y✝ : M
yc : y✝ ∈ ↑C
w✝¹ w✝ : R
a0 : 0 < w✝¹
b0 : 0 < w✝
zf : w✝¹ • x✝ + w✝ • y✝ ∈ ↑F
⊢ x✝ ∈ ↑F

Tactic:
exact h.mem_of_smul_add_smul_mem_left xc yc a0 b0 zf

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 F : PointedCone R M
hF : F.IsFaceOf C
x y : M
hx : x ∈ C
hy : y ∈ C
hxy : x + y ∈ F
⊢ x ∈ F

Tactic:
nontriviality R using Module.subsingleton R M

Goal state after:
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 F : PointedCone R M
hF : F.IsFaceOf C
x y : M
hx : x ∈ C
hy : y ∈ C
hxy : x + y ∈ F
a✝ : Nontrivial R
⊢ x ∈ F
Module: Mathlib.Geometry.Convex.Cone.Face.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : DivisionRing R
inst✝³ : LinearOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
C : PointedCone R M
⊢ (↑C.lineal).IsFaceOf C

Tactic:
by
  apply of_mem_of_add_mem_left (lineal_le C)
  intro _ _ xc yc xyf
  simp [neg_add_rev, xc, true_and] at xyf ⊢
  simpa [neg_add_cancel_comm] using add_mem xyf.2 yc

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 ≠ ⊥
⊢ Q₁ h ≠ 0

Tactic:
exact Q₁_ne_zero h

Goal state after:
Module: Mathlib.Geometry.Diffeology.Basic

Goal state before:
pp: X : Type u_1
d : CorePlotsOn X
n : ℕ
p : EuclideanSpace ℝ (Fin n) → X
h✝ :
  ∀ (x : EuclideanSpace ℝ (Fin n)),
    ∃ u,
      IsOpen u ∧
        x ∈ u ∧
          ∀ {m : ℕ} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
            (∀ (x : EuclideanSpace ℝ (Fin m)), f x ∈ u) → ContDiff ℝ ∞ f → p ∘ f ∈ {p | d.isPlot p}
x : EuclideanSpace ℝ (Fin n)
x✝ : x ∈ Set.univ
u : Set (EuclideanSpace ℝ (Fin n))
hu : IsOpen u
hxu : x ∈ u
hu' :
  ∀ {m : ℕ} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
    (∀ (x : EuclideanSpace ℝ (Fin m)), f x ∈ u) → ContDiff ℝ ∞ f → p ∘ f ∈ {p | d.isPlot p}
ε : ℝ
hε : ε > 0
hε' : Metric.ball x ε ⊆ u
h : d.isPlot (p ∘ ↑(OpenPartialHomeomorph.univBall x ε))
h' : d.isPlotOn ⋯ ((p ∘ ↑(OpenPartialHomeomorph.univBall x ε)) ∘ ↑(OpenPartialHomeomorph.univBall x ε).symm)
⊢ Set.EqOn (p ∘ ↑(OpenPartialHomeomorph.univBall x ε) ∘ ↑(OpenPartialHomeomorph.univBall x ε).symm) p (Metric.ball x ε)

Tactic:
← OpenPartialHomeomorph.coe_trans

Goal state after:
X : Type u_1
d : CorePlotsOn X
n : ℕ
p : EuclideanSpace ℝ (Fin n) → X
h✝ :
  ∀ (x : EuclideanSpace ℝ (Fin n)),
    ∃ u,
      IsOpen u ∧
        x ∈ u ∧
          ∀ {m : ℕ} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
            (∀ (x : EuclideanSpace ℝ (Fin m)), f x ∈ u) → ContDiff ℝ ∞ f → p ∘ f ∈ {p | d.isPlot p}
x : EuclideanSpace ℝ (Fin n)
x✝ : x ∈ Set.univ
u : Set (EuclideanSpace ℝ (Fin n))
hu : IsOpen u
hxu : x ∈ u
hu' :
  ∀ {m : ℕ} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
    (∀ (x : EuclideanSpace ℝ (Fin m)), f x ∈ u) → ContDiff ℝ ∞ f → p ∘ f ∈ {p | d.isPlot p}
ε : ℝ
hε : ε > 0
hε' : Metric.ball x ε ⊆ u
h : d.isPlot (p ∘ ↑(OpenPartialHomeomorph.univBall x ε))
h' : d.isPlotOn ⋯ ((p ∘ ↑(OpenPartialHomeomorph.univBall x ε)) ∘ ↑(OpenPartialHomeomorph.univBall x ε).symm)
⊢ Set.EqOn (p ∘ ↑((OpenPartialHomeomorph.univBall x ε).symm.trans (OpenPartialHomeomorph.univBall x ε))) p
    (Metric.ball x ε)
Module: Mathlib.Geometry.Euclidean.Altitude

Goal state before:
pp: case refine_3
V : Type u_1
P : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MetricSpace P
inst✝⁴ : NormedAddTorsor V P
V₂ : Type u_3
P₂ : Type u_4
inst✝³ : NormedAddCommGroup V₂
inst✝² : InnerProductSpace ℝ V₂
inst✝¹ : MetricSpace P₂
inst✝ : NormedAddTorsor V₂ P₂
n : ℕ
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
i : Fin (n + 1)
hf : Function.Injective ⇑f.linear
⊢ ((s.map f.toAffineMap ⋯).altitude i).direction = Submodule.map f.linear (s.altitude i).direction

Tactic:
direction_altitude,

Goal state after:
case refine_3
V : Type u_1
P : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MetricSpace P
inst✝⁴ : NormedAddTorsor V P
V₂ : Type u_3
P₂ : Type u_4
inst✝³ : NormedAddCommGroup V₂
inst✝² : InnerProductSpace ℝ V₂
inst✝¹ : MetricSpace P₂
inst✝ : NormedAddTorsor V₂ P₂
n : ℕ
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
i : Fin (n + 1)
hf : Function.Injective ⇑f.linear
⊢ (vectorSpan ℝ ((s.map f.toAffineMap ⋯).points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range (s.map f.toAffineMap ⋯).points) =
    Submodule.map f.linear (s.altitude i).direction