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
⊢ ∀ (a a_1 : R), funMap mulFunc (Fin.cons a (Fin.cons a_1 finZeroElim)) = a * Fin.cons a (Fin.cons a_1 finZeroElim) 1

Tactic:
intros

Goal state after:
α : Type u_1
R : Type u_2
inst✝ : ring.Structure R
a✝¹ a✝ : R
⊢ funMap mulFunc (Fin.cons a✝¹ (Fin.cons a✝ finZeroElim)) = a✝¹ * Fin.cons a✝¹ (Fin.cons a✝ finZeroElim) 1
Module: Mathlib.ModelTheory.Algebra.Ring.Basic

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝ : ring.Structure R
⊢ ∀ (a : R), funMap negFunc (Fin.cons a finZeroElim) = -a

Tactic:
intros

Goal state after:
α : Type u_1
R : Type u_2
inst✝ : ring.Structure R
a✝ : R
⊢ funMap negFunc (Fin.cons a✝ finZeroElim) = -a✝
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case func.zero.inl
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
_ts✝ : Fin 0 → L[[γ]].Term α
ih : ∀ (a : Fin 0), (_ts✝ a).constantsToVars.varsToConstants = _ts✝ a
val✝ : L.Functions 0
⊢ (func (Sum.inl val✝) _ts✝).constantsToVars.varsToConstants = func (Sum.inl val✝) _ts✝

Tactic:
simp [constantsToVars, varsToConstants, ih]

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case func.succ.inl
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n✝ : ℕ
_ts✝ : Fin (n✝ + 1) → L[[γ]].Term α
ih : ∀ (a : Fin (n✝ + 1)), (_ts✝ a).constantsToVars.varsToConstants = _ts✝ a
val✝ : L.Functions (n✝ + 1)
⊢ (func (Sum.inl val✝) _ts✝).constantsToVars.varsToConstants = func (Sum.inl val✝) _ts✝

Tactic:
simp [constantsToVars, varsToConstants, ih]

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case falsum
L : Language
α : Type u'
k n✝ : ℕ
⊢ ∀ {m n : ℕ} (km : n✝ ≤ m) (mn : m ≤ n), castLE mn (castLE km falsum) = castLE ⋯ falsum

Tactic:
intros

Goal state after:
case falsum
L : Language
α : Type u'
k n✝¹ m✝ n✝ : ℕ
km✝ : n✝¹ ≤ m✝
mn✝ : m✝ ≤ n✝
⊢ castLE mn✝ (castLE km✝ falsum) = castLE ⋯ falsum
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case rel
L : Language
α : Type u'
k n✝ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (α ⊕ Fin n✝)
⊢ ∀ {m n : ℕ} (km : n✝ ≤ m) (mn : m ≤ n), castLE mn (castLE km (rel R✝ ts✝)) = castLE ⋯ (rel R✝ ts✝)

Tactic:
intros

Goal state after:
case rel
L : Language
α : Type u'
k n✝¹ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (α ⊕ Fin n✝¹)
m✝ n✝ : ℕ
km✝ : n✝¹ ≤ m✝
mn✝ : m✝ ≤ n✝
⊢ castLE mn✝ (castLE km✝ (rel R✝ ts✝)) = castLE ⋯ (rel R✝ ts✝)
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case all
L : Language
α : Type u'
k n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ {m n : ℕ} (km : n✝ + 1 ≤ m) (mn : m ≤ n), castLE mn (castLE km f✝) = castLE ⋯ f✝
⊢ ∀ {m n : ℕ} (km : n✝ ≤ m) (mn : m ≤ n), castLE mn (castLE km f✝.all) = castLE ⋯ f✝.all

Tactic:
intros

Goal state after:
case all
L : Language
α : Type u'
k n✝¹ : ℕ
f✝ : L.BoundedFormula α (n✝¹ + 1)
ih3 : ∀ {m n : ℕ} (km : n✝¹ + 1 ≤ m) (mn : m ≤ n), castLE mn (castLE km f✝) = castLE ⋯ f✝
m✝ n✝ : ℕ
km✝ : n✝¹ ≤ m✝
mn✝ : m✝ ≤ n✝
⊢ castLE mn✝ (castLE km✝ f✝.all) = castLE ⋯ f✝.all
Module: Mathlib.ModelTheory.Algebra.Field.CharP

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
⊢ CharZero K ↔ CharP K 0

Tactic:
exact ⟨fun _ => CharP.ofCharZero _, fun _ => CharP.charP_to_charZero K⟩

Goal state after:
Module: Mathlib.ModelTheory.ElementaryMaps

Goal state before:
pp: case refine_2
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    φ.Realize default (Fin.snoc (⇑f ∘ x) a) → ∃ b, φ.Realize default (Fin.snoc (⇑f ∘ x) (f b))
n : ℕ
φ : L.BoundedFormula Empty n
⊢ ∀ {n : ℕ} (t₁ t₂ : L.Term (Empty ⊕ Fin n)) (xs : Fin n → M),
    (BoundedFormula.equal t₁ t₂).Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ (BoundedFormula.equal t₁ t₂).Realize default xs

Tactic:
intros

Goal state after:
case refine_2
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    φ.Realize default (Fin.snoc (⇑f ∘ x) a) → ∃ b, φ.Realize default (Fin.snoc (⇑f ∘ x) (f b))
n : ℕ
φ : L.BoundedFormula Empty n
n✝ : ℕ
t₁✝ t₂✝ : L.Term (Empty ⊕ Fin n✝)
xs✝ : Fin n✝ → M
⊢ (BoundedFormula.equal t₁✝ t₂✝).Realize (⇑f ∘ default) (⇑f ∘ xs✝) ↔ (BoundedFormula.equal t₁✝ t₂✝).Realize default xs✝
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝³ : L.Structure M
inst✝² : L.Structure N
inst✝¹ : L.Structure P
S : L.Substructure M
s : Set M
inst✝ : IsEmpty L.Constants
x : M
⊢ x ∉ ⊥

Tactic:
have h : (∅ : Set M) ∈ (closure L).closed := by
    rw [mem_closed_iff]
    intro n f
    cases n
    · exact isEmptyElim f
    · intro x hx
      simp only [mem_empty_iff_false, forall_const] at hx

Goal state after:
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝³ : L.Structure M
inst✝² : L.Structure N
inst✝¹ : L.Structure P
S : L.Substructure M
s : Set M
inst✝ : IsEmpty L.Constants
x : M
h : ∅ ∈ (closure L).closed
⊢ x ∉ ⊥
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
φ : L.BoundedFormula (↑A ⊕ α) 0
x✝ : α → M
⊢ ∀ (n : ℕ) (t : L.Term ((↑A ⊕ α) ⊕ Fin n)) (xs : Fin n → M),
    Term.realize (Sum.elim x✝ xs) (((fun x ↦ Term.constantsVarsEquivLeft) n).symm t) =
      Term.realize (Sum.elim (Sum.elim Subtype.val x✝) xs) t

Tactic:
intros

Goal state after:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
φ : L.BoundedFormula (↑A ⊕ α) 0
x✝ : α → M
n✝ : ℕ
t✝ : L.Term ((↑A ⊕ α) ⊕ Fin n✝)
xs✝ : Fin n✝ → M
⊢ Term.realize (Sum.elim x✝ xs✝) (((fun x ↦ Term.constantsVarsEquivLeft) n✝).symm t✝) =
    Term.realize (Sum.elim (Sum.elim Subtype.val x✝) xs✝) t✝
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case all.e__v.inr.refine_1
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ (v : α ⊕ Fin (n✝ + 1) → M), f✝.toFormula.Realize v ↔ f✝.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
v : α ⊕ Fin n✝ → M
a : M
h :
  f✝.toFormula.Realize (Sum.elim (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)) ↔ f✝.Realize (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)
x : Fin (n✝ + 1)
⊢ Sum.elim v (fun x ↦ snoc default a (castAdd 0 x))
      (Sum.elim (fun x ↦ Sum.inl (Sum.inl x)) (fun x ↦ Sum.map Sum.inr id (finSumFinEquiv.symm x))
        (Sum.inr (last n✝))) =
    Sum.elim (fun x ↦ v (Sum.inl x)) (snoc (fun x ↦ v (Sum.inr x)) a) (Sum.inr (last n✝))

pp: case all.e__v.inr.refine_2
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ (v : α ⊕ Fin (n✝ + 1) → M), f✝.toFormula.Realize v ↔ f✝.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
v : α ⊕ Fin n✝ → M
a : M
h :
  f✝.toFormula.Realize (Sum.elim (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)) ↔ f✝.Realize (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)
x : Fin (n✝ + 1)
⊢ ∀ (i : Fin n✝),
    Sum.elim v (fun x ↦ snoc default a (castAdd 0 x))
        (Sum.elim (fun x ↦ Sum.inl (Sum.inl x)) (fun x ↦ Sum.map Sum.inr id (finSumFinEquiv.symm x))
          (Sum.inr i.castSucc)) =
      Sum.elim (fun x ↦ v (Sum.inl x)) (snoc (fun x ↦ v (Sum.inr x)) a) (Sum.inr i.castSucc)

Tactic:
· simp [Fin.snoc]

Goal state after:
case all.e__v.inr.refine_2
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ (v : α ⊕ Fin (n✝ + 1) → M), f✝.toFormula.Realize v ↔ f✝.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
v : α ⊕ Fin n✝ → M
a : M
h :
  f✝.toFormula.Realize (Sum.elim (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)) ↔ f✝.Realize (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)
x : Fin (n✝ + 1)
⊢ ∀ (i : Fin n✝),
    Sum.elim v (fun x ↦ snoc default a (castAdd 0 x))
        (Sum.elim (fun x ↦ Sum.inl (Sum.inl x)) (fun x ↦ Sum.map Sum.inr id (finSumFinEquiv.symm x))
          (Sum.inr i.castSucc)) =
      Sum.elim (fun x ↦ v (Sum.inl x)) (snoc (fun x ↦ v (Sum.inr x)) a) (Sum.inr i.castSucc)
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
n : ℕ
inst✝ : Finite β
f : β → L.BoundedFormula α n
v : α → M
v' : Fin n → M
⊢ (iInf f).Realize v v' ↔ ∀ (b : β), (f b).Realize v v'

Tactic:
simp only [iInf, realize_foldr_inf, List.mem_map, Finset.mem_toList, Finset.mem_univ, true_and,
    forall_exists_index, forall_apply_eq_imp_iff]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case mp
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : DecidableEq α
inst✝ : Nonempty M
φ : L.Formula α
⊢ (∃ v, M ⊨ equivSentence φ) → M ⊨ φ.exClosure

Tactic:
rintro ⟨v, hv⟩

Goal state after:
case mp
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : DecidableEq α
inst✝ : Nonempty M
φ : L.Formula α
v : α → M
hv : M ⊨ equivSentence φ
⊢ M ⊨ φ.exClosure
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
r : L.Relations 2
⊢ M ⊨ r.symmetric ↔ Std.Symm fun x y ↦ RelMap r ![x, y]

Tactic:
symm_def

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
r : L.Relations 2
⊢ M ⊨ r.symmetric ↔ ∀ ⦃a b : M⦄, RelMap r ![a, b] → RelMap r ![b, a]
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type u_1
L : Language
inst✝¹ : L.Structure M
A : Set M
α : Type u_4
β : Type u_5
inst✝ : Finite β
F : (α → M) → β → M
hF : DefinableMap L A F
S : Set (β → M)
hS : A.Definable L S
h_graph : A.Definable L {w | ∀ (i : β), F (w ∘ Sum.inl) i = w (Sum.inr i)}
h_cyl : A.Definable L {w | w ∘ Sum.inr ∈ S}
v : α → M
⊢ v ∈ F ⁻¹' S ↔ v ∈ {v | ∃ u, Sum.elim v u ∈ {w | ∀ (i : β), F (w ∘ Sum.inl) i = w (Sum.inr i)} ∩ {w | w ∘ Sum.inr ∈ S}}

Tactic:
simp [← funext_iff]

Goal state after:
Module: Mathlib.ModelTheory.Skolem

Goal state before:
pp: case refine_2
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') = #↑s'
⊢ lift.{max w w', max u v} L.card ≤ lift.{max (max u v) w', w} #↑(⇑Equiv.ulift '' s')

Tactic:
← lift_lift.{w', w}

Goal state after:
case refine_2
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') = #↑s'
⊢ lift.{w, max w' u v} (lift.{w', max u v} L.card) ≤ lift.{max (max u v) w', w} #↑(⇑Equiv.ulift '' s')
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: case inr
L : Language
M : Type w'
inst✝¹ : L.Structure M
inst✝ : Infinite M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
N : Bundled L.Structure
hNκ : #↑N = κ
MN : Nonempty (M ↪ₑ[L] ↑N)
⊢ ∃ N, (M ≅[L] ↑N) ∧ #↑N = κ

Tactic:
exact ⟨N, MN.some.elementarilyEquivalent, hNκ⟩

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

Goal state before:
pp: a : Cardinal.{u}
ha : ℵ₀ ≤ a
⊢ ¬Irreducible a

Tactic:
rw [irreducible_iff, not_and_or]
  refine Or.inr fun h => ?_
  simpa [mul_aleph0_eq ha, isUnit_iff, (one_lt_aleph0.trans_le ha).ne', one_lt_aleph0.ne'] using
    @h a ℵ₀

Goal state after:
Module: Mathlib.FieldTheory.AxGrothendieck

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝¹ : Finite α
inst✝ : Finite ι
p : ℕ
hp : Nat.Prime p
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
this✝ : Fact (Nat.Prime p)
this : CompatibleRing (AlgebraicClosure (ZMod p)) := compatibleRingOfRing (AlgebraicClosure (ZMod p))
⊢ Theory.ACF p ⊨ᵇ genericPolyMapSurjOnOfInjOn φ mons

Tactic:
rw [← (ACF_isComplete (Or.inl hp)).realize_sentence_iff _
    (AlgebraicClosure (ZMod p)), realize_genericPolyMapSurjOnOfInjOn]

Goal state after:
ι : Type u_1
α : Type u_2
inst✝¹ : Finite α
inst✝ : Finite ι
p : ℕ
hp : Nat.Prime p
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
this✝ : Fact (Nat.Prime p)
this : CompatibleRing (AlgebraicClosure (ZMod p)) := compatibleRingOfRing (AlgebraicClosure (ZMod p))
⊢ ∀ (v : α → AlgebraicClosure (ZMod p)) (p_1 : { p_1 // ∀ (i : ι), (p_1 i).support ⊆ mons i }),
    have f := fun v i ↦ (eval v) (↑p_1 i);
    have S := {x | φ.Realize (Sum.elim v x)};
    Set.MapsTo f S S → Set.InjOn f S → Set.SurjOn f S S
Module: Mathlib.FieldTheory.AxGrothendieck

Goal state before:
pp: K : Type u_1
ι : Type u_2
inst✝³ : Field K
inst✝² : IsAlgClosed K
inst✝¹ : Finite ι
inst✝ : CompatibleRing K
c✝ : Set K
S : Set (ι → K)
ps : ι → MvPolynomial ι K
this : Fintype ι := Fintype.ofFinite ι
p : ℕ := ringChar K
c : Finset K
left✝ : ↑c ⊆ c✝
hS : (↑c).Definable ring S
⊢ Set.MapsTo (fun v i ↦ (eval v) (ps i)) S S →
    Set.InjOn (fun v i ↦ (eval v) (ps i)) S → Set.SurjOn (fun v i ↦ (eval v) (ps i)) S S

Tactic:
rw [Set.definable_iff_exists_formula_sum] at hS

Goal state after:
K : Type u_1
ι : Type u_2
inst✝³ : Field K
inst✝² : IsAlgClosed K
inst✝¹ : Finite ι
inst✝ : CompatibleRing K
c✝ : Set K
S : Set (ι → K)
ps : ι → MvPolynomial ι K
this : Fintype ι := Fintype.ofFinite ι
p : ℕ := ringChar K
c : Finset K
left✝ : ↑c ⊆ c✝
hS : ∃ φ, S = {v | φ.Realize (Sum.elim Subtype.val v)}
⊢ Set.MapsTo (fun v i ↦ (eval v) (ps i)) S S →
    Set.InjOn (fun v i ↦ (eval v) (ps i)) S → Set.SurjOn (fun v i ↦ (eval v) (ps i)) S S
Module: Mathlib.FieldTheory.AxGrothendieck

Goal state before:
pp: K : Type u_1
ι : Type u_2
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : Finite ι
I : Ideal (MvPolynomial ι K)
p : ι → MvPolynomial ι K
this : CompatibleRing K := compatibleRingOfRing K
⊢ let S := zeroLocus K I;
  Set.MapsTo (fun v i ↦ (eval v) (p i)) S S →
    Set.InjOn (fun v i ↦ (eval v) (p i)) S → Set.SurjOn (fun v i ↦ (eval v) (p i)) S S

Tactic:
intro S

Goal state after:
K : Type u_1
ι : Type u_2
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : Finite ι
I : Ideal (MvPolynomial ι K)
p : ι → MvPolynomial ι K
this : CompatibleRing K := compatibleRingOfRing K
S : Set (ι → K) := zeroLocus K I
⊢ Set.MapsTo (fun v i ↦ (eval v) (p i)) S S →
    Set.InjOn (fun v i ↦ (eval v) (p i)) S → Set.SurjOn (fun v i ↦ (eval v) (p i)) S S
Module: Mathlib.FieldTheory.Finite.Polynomial

Goal state before:
pp: case refine_1
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
n : σ
⊢ ∀ b ∈ Finset.univ, b ≠ n → (Fintype.card K - 1) * Multiset.count n {b} = 0

Tactic:
intro b _ ne

Goal state after:
case refine_1
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
n b : σ
a✝ : b ∈ Finset.univ
ne : b ≠ n
⊢ (Fintype.card K - 1) * Multiset.count n {b} = 0
Module: Mathlib.FieldTheory.CardinalEmb

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
rank_inf : ℵ₀ ≤ sepDegree F E
⊢ #(Emb F E) = 2 ^ sepDegree F E

Tactic:
rw [← cardinal_separableClosure, cardinal_eq_two_pow_rank rank_inf]

Goal state after:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
rank_inf : ℵ₀ ≤ sepDegree F E
⊢ 2 ^ Module.rank F ↥(separableClosure F E) = 2 ^ sepDegree F E
Module: Mathlib.FieldTheory.PerfectClosure

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

Tactic:
by
  cases x <;> simp [natCast K p 0]

Goal state after:
Module: Mathlib.RingTheory.Algebraic.LinearIndependent

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
H : ∀ (p : F[X]), (aeval x) p = 0 → p = 0
s : Finset F
m : F → F
i : F
hi : i ∈ s
hnz : ∀ (a : F), x - (algebraMap F E) a ≠ 0
b : E := ∏ j ∈ s, (x - (algebraMap F E) j)
h1 : ∀ i ∈ s, m i • (b * (x - (algebraMap F E) i)⁻¹) = m i • ∏ j ∈ s.erase i, (x - (algebraMap F E) j)
hm : b * ∑ i ∈ s, m i • (x - (algebraMap F E) i)⁻¹ = b * 0
⊢ m i = 0

Tactic:
simp_rw [mul_zero, Finset.mul_sum, mul_smul_comm, Finset.sum_congr rfl h1] at hm

Goal state after:
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
H : ∀ (p : F[X]), (aeval x) p = 0 → p = 0
s : Finset F
m : F → F
i : F
hi : i ∈ s
hnz : ∀ (a : F), x - (algebraMap F E) a ≠ 0
b : E := ∏ j ∈ s, (x - (algebraMap F E) j)
h1 : ∀ i ∈ s, m i • (b * (x - (algebraMap F E) i)⁻¹) = m i • ∏ j ∈ s.erase i, (x - (algebraMap F E) j)
hm : ∑ x_1 ∈ s, m x_1 • ∏ j ∈ s.erase x_1, (x - (algebraMap F E) j) = 0
⊢ m i = 0
Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.Transcendental F E
ι : Type v
x : ι → E
hx : IsTranscendenceBasis F x
⊢ Module.rank F E = #E

Tactic:
have := hx.nonempty_iff_transcendental.2 ‹_›

Goal state after:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.Transcendental F E
ι : Type v
x : ι → E
hx : IsTranscendenceBasis F x
this : Nonempty ι
⊢ Module.rank F E = #E
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: case splits'
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⟮α⟯ = ⊤
⊢ (X ^ finrank K L - C ((algebraMap K L) a)).Splits

Tactic:
have ⟨_, hζ⟩ := hK

Goal state after:
case splits'
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⟮α⟯ = ⊤
w✝ : K
hζ : w✝ ∈ primitiveRoots (finrank K L) K
⊢ (X ^ finrank K L - C ((algebraMap K L) a)).Splits
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: case refine_2
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)⁻¹
⊢ ↑D.index ≤ ↑{x | K x = D}.card * ((↑D.index)⁻¹ * ↑D.index)

Tactic:
inv_mul_cancel₀ (Nat.cast_ne_zero.mpr hD.index_ne_zero),

Goal state after:
case refine_2
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)⁻¹
⊢ ↑D.index ≤ ↑{x | K x = D}.card * 1
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
ι : Type u_1
a : Basis ι R ↥A
H : LinearIndependent (↥B.op) (MulOpposite.op ∘ ⇑A.val ∘ ⇑a)
⊢ A.LinearDisjoint B

Tactic:
← mulLeftMap_ker_eq_bot_iff_linearIndependent_op

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
A B : Subalgebra R S
ι : Type u_1
a : Basis ι R ↥A
H : (Submodule.mulLeftMap (toSubmodule B) ⇑a).ker = ⊥
⊢ A.LinearDisjoint B
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).toFinset.val).prod

Tactic:
Multiset.toFinset_val

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 = (Multiset.map (fun x ↦ X - C x) (c.minpoly.aroots L).dedup).prod
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
K : Type u_1
inst✝⁶ : Field K
inst✝⁵ : Algebra F K
inst✝⁴ : Algebra L K
inst✝³ : IsScalarTower F L K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : IsScalarTower L E K
⊢ (IntermediateField.map (IsScalarTower.toAlgHom F E K) A).LinearDisjoint L

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 : 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 (IsScalarTower.toAlgHom F L E).range
K : Type u_1
inst✝⁶ : Field K
inst✝⁵ : Algebra F K
inst✝⁴ : Algebra L K
inst✝³ : IsScalarTower F L K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : IsScalarTower L E K
⊢ (IntermediateField.map (IsScalarTower.toAlgHom F E K) A).LinearDisjoint (IsScalarTower.toAlgHom F L K).range
Module: Mathlib.FieldTheory.LinearDisjoint

Goal state before:
pp: F : Type u
E : Type v
inst✝²⁰ : Field F
inst✝¹⁹ : Field E
inst✝¹⁸ : Algebra F E
L : Type w
inst✝¹⁷ : Field L
inst✝¹⁶ : Algebra F L
inst✝¹⁵ : Algebra L E
inst✝¹⁴ : IsScalarTower F L E
L' : Type u_1
inst✝¹³ : Field L'
inst✝¹² : Algebra F L'
inst✝¹¹ : Algebra L' E
inst✝¹⁰ : IsScalarTower F L' E
H : (IsScalarTower.toAlgHom F L E).fieldRange.LinearDisjoint L'
K : Type u_2
inst✝⁹ : Field K
inst✝⁸ : Algebra F K
inst✝⁷ : Algebra L K
inst✝⁶ : IsScalarTower F L K
inst✝⁵ : Algebra L' K
inst✝⁴ : IsScalarTower F L' K
inst✝³ : Algebra E K
inst✝² : IsScalarTower F E K
inst✝¹ : IsScalarTower L E K
inst✝ : IsScalarTower L' E K
⊢ (IsScalarTower.toAlgHom F L K).fieldRange.LinearDisjoint L'

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