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

Goal state before:
pp: α : Type u_1
⊢ ∀ (x : ring.Symbols),
    x ∈
      { val := ↑[Sum.inl ⟨2, add⟩, Sum.inl ⟨2, mul⟩, Sum.inl ⟨1, neg⟩, Sum.inl ⟨0, zero⟩, Sum.inl ⟨0, one⟩],
        nodup := instFintypeSymbolsRing._proof_1 }

Tactic:
intro x

Goal state after:
α : Type u_1
x : ring.Symbols
⊢ x ∈
    { val := ↑[Sum.inl ⟨2, add⟩, Sum.inl ⟨2, mul⟩, Sum.inl ⟨1, neg⟩, Sum.inl ⟨0, zero⟩, Sum.inl ⟨0, one⟩],
      nodup := instFintypeSymbolsRing._proof_1 }
Module: Mathlib.ModelTheory.Algebra.Ring.Basic

Goal state before:
pp: α : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : NonAssocRing R
inst✝² : NonAssocRing S
inst✝¹ : CompatibleRing R
inst✝ : CompatibleRing S
f : R ≃[ring] S
⊢ ∀ (x y : R), f.toFun (x * y) = f.toFun x * f.toFun y

Tactic:
intro x

Goal state after:
α : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : NonAssocRing R
inst✝² : NonAssocRing S
inst✝¹ : CompatibleRing R
inst✝ : CompatibleRing S
f : R ≃[ring] S
x : R
⊢ ∀ (y : R), f.toFun (x * y) = f.toFun x * f.toFun y
Module: Mathlib.ModelTheory.Algebra.Ring.Basic

Goal state before:
pp: α : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : NonAssocRing R
inst✝² : NonAssocRing S
inst✝¹ : CompatibleRing R
inst✝ : CompatibleRing S
f : R ≃[ring] S
⊢ ∀ (x y : R), f.toFun (x + y) = f.toFun x + f.toFun y

Tactic:
intro x

Goal state after:
α : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : NonAssocRing R
inst✝² : NonAssocRing S
inst✝¹ : CompatibleRing R
inst✝ : CompatibleRing S
f : R ≃[ring] S
x : R
⊢ ∀ (y : R), f.toFun (x + y) = f.toFun x + f.toFun y
Module: Mathlib.ModelTheory.Algebra.Field.Basic

Goal state before:
pp: case negAddCancel
K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
⊢ toProp K negAddCancel

Tactic:
| negAddCancel =>

Goal state after:
Module: Mathlib.ModelTheory.Ultraproducts

Goal state before:
pp: α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → L.Structure (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
n✝ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (β ⊕ Fin n✝)
v : Fin n✝ → (a : α) → M a
h2 : ∀ (a : α), (Sum.elim (fun i ↦ x i a) fun i ↦ v i a) = fun i ↦ Sum.elim x v i a
| RelMap R✝ fun i ↦ Term.realize (Quotient.mk' ∘ Sum.elim x v) (ts✝ i)

Tactic:
2,

Goal state after:
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → L.Structure (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
n✝ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (β ⊕ Fin n✝)
v : Fin n✝ → (a : α) → M a
h2 : ∀ (a : α), (Sum.elim (fun i ↦ x i a) fun i ↦ v i a) = fun i ↦ Sum.elim x v i a
| fun i ↦ Term.realize (Quotient.mk' ∘ Sum.elim x v) (ts✝ i)
Module: Mathlib.ModelTheory.ElementaryMaps

Goal state before:
pp: L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
φ : M ↪ₑ[L] N
⊢ Function.Injective ⇑φ

Tactic:
intro x

Goal state after:
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
φ : M ↪ₑ[L] N
x : M
⊢ ∀ ⦃a₂ : M⦄, φ x = φ a₂ → x = a₂
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: case succ
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
n✝ : ℕ
f : L.Functions (n✝ + 1)
⊢ ClosedUnder f ∅

Tactic:
intro x

Goal state after:
case succ
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
n✝ : ℕ
f : L.Functions (n✝ + 1)
x : Fin (n✝ + 1) → M
⊢ (∀ (i : Fin (n✝ + 1)), x i ∈ ∅) → funMap f x ∈ ∅
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
φ : L.Formula α
⊢ M ⊨ equivSentence φ ↔ φ.Realize fun a ↦ ↑(L.con a)

Tactic:
rw [← realize_equivSentence_symm_con M (equivSentence φ), _root_.Equiv.symm_apply_apply]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
T : L.Theory
φ : L.Sentence
⊢ M ⊨ insert φ T ↔ M ⊨ φ ∧ M ⊨ T

Tactic:
Set.insert_eq,

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
T : L.Theory
φ : L.Sentence
⊢ M ⊨ {φ} ∪ T ↔ M ⊨ φ ∧ M ⊨ T
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case succ.mpr
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n✝ : ℕ
v : α → M
n : ℕ
ih : ∀ {φ : L.BoundedFormula α n}, φ.exs.Realize v ↔ ∃ xs, φ.Realize v xs
φ : L.BoundedFormula α (n + 1)
⊢ (∃ xs, φ.Realize v xs) → ∃ xs a, φ.Realize v (snoc xs a)

Tactic:
rintro ⟨xs, h⟩

Goal state after:
case succ.mpr
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n✝ : ℕ
v : α → M
n : ℕ
ih : ∀ {φ : L.BoundedFormula α n}, φ.exs.Realize v ↔ ∃ xs, φ.Realize v xs
φ : L.BoundedFormula α (n + 1)
xs : Fin (n + 1) → M
h : φ.Realize v xs
⊢ ∃ xs a, φ.Realize v (snoc xs a)
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case refine_2
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
e : β ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯
⊢ ∀ (a : Fin (Classical.choose ⋯) → M),
    (Realize φ (fun x ↦ Sum.elim (fun x ↦ v x) (fun x ↦ a (Fin.cast ⋯ ((Classical.choice ⋯) x))) x) fun x ↦
        a (natAdd (Classical.choose ⋯) x)) ↔
      φ.Realize fun a_1 ↦
        Sum.elim v ({ toFun := fun v ↦ v ∘ ⇑e, invFun := fun v ↦ v ∘ ⇑e.symm, left_inv := ⋯, right_inv := ⋯ } a) a_1

Tactic:
intro x

Goal state after:
case refine_2
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
e : β ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯
x : Fin (Classical.choose ⋯) → M
⊢ (Realize φ (fun x_1 ↦ Sum.elim (fun x ↦ v x) (fun x_2 ↦ x (Fin.cast ⋯ ((Classical.choice ⋯) x_2))) x_1) fun x_1 ↦
      x (natAdd (Classical.choose ⋯) x_1)) ↔
    φ.Realize fun a ↦
      Sum.elim v ({ toFun := fun v ↦ v ∘ ⇑e, invFun := fun v ↦ v ∘ ⇑e.symm, left_inv := ⋯, right_inv := ⋯ } x) a
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
N : Type u_1
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M →[L] N
⊢ Set.range ⇑f = Set.univ ↔ Function.Surjective ⇑f

Tactic:
Set.range_eq_univ

Goal state after:
L : Language
M : Type w
N : Type u_1
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M →[L] N
⊢ Function.Surjective ⇑f ↔ Function.Surjective ⇑f
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case refine_2
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
e : γ ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯
⊢ ∀ (a : Fin (Classical.choose ⋯) → M),
    (Realize φ (fun x ↦ Sum.elim (fun x ↦ v x) (fun x ↦ a (Fin.cast ⋯ ((Classical.choice ⋯) x))) x) fun x ↦
        a (natAdd (Classical.choose ⋯) x)) ↔
      φ.Realize
        (Sum.elim v ({ toFun := fun v ↦ v ∘ ⇑e, invFun := fun v ↦ v ∘ ⇑e.symm, left_inv := ⋯, right_inv := ⋯ } a))

Tactic:
intro x

Goal state after:
case refine_2
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
e : γ ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯
x : Fin (Classical.choose ⋯) → M
⊢ (Realize φ (fun x_1 ↦ Sum.elim (fun x ↦ v x) (fun x_2 ↦ x (Fin.cast ⋯ ((Classical.choice ⋯) x_2))) x_1) fun x_1 ↦
      x (natAdd (Classical.choose ⋯) x_1)) ↔
    φ.Realize (Sum.elim v ({ toFun := fun v ↦ v ∘ ⇑e, invFun := fun v ↦ v ∘ ⇑e.symm, left_inv := ⋯, right_inv := ⋯ } x))
Module: Mathlib.ModelTheory.ElementarySubstructures

Goal state before:
pp: L : Language
M : Type u_1
inst✝ : L.Structure M
A : Set M
hA : MeetsDefinable A
⊢ range (Term.realize Subtype.val) ⊆ A

Tactic:
intro x

Goal state after:
L : Language
M : Type u_1
inst✝ : L.Structure M
A : Set M
hA : MeetsDefinable A
x : M
⊢ x ∈ range (Term.realize Subtype.val) → x ∈ A
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
f g : Set (α → M)
hf : A.Definable L f
hg : A.Definable L g
⊢ A.Definable L (f ∪ g)

Tactic:
rcases hf with ⟨φ, hφ⟩
  rcases hg with ⟨θ, hθ⟩
  refine ⟨φ ⊔ θ, ?_⟩
  ext
  rw [hφ, hθ, mem_ofPred_eq, Formula.realize_sup, mem_union, mem_ofPred_eq, mem_ofPred_eq]

Goal state after:
Module: Mathlib.ModelTheory.Skolem

Goal state before:
pp: L : Language
| (sum fun i ↦ lift.{max u v, u} #(L.Functions i)) + sum fun i ↦ lift.{u, max u v} #(L.BoundedFormula Empty (i + 1))

Tactic:
2,

Goal state after:
L : Language
| sum fun i ↦ lift.{u, max u v} #(L.BoundedFormula Empty (i + 1))
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: L : Language
α : Type u'
inst✝¹ : Countable α
inst✝ : Countable L.Symbols
⊢ #(constantsOn α).Symbols ≤ ℵ₀

Tactic:
change (constantsOn α).card ≤ ℵ₀

Goal state after:
L : Language
α : Type u'
inst✝¹ : Countable α
inst✝ : Countable L.Symbols
⊢ (constantsOn α).card ≤ ℵ₀
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case refine_1
L : Language
M : Type w
inst✝ : L.Structure M
n : ℕ
⊢ (∃ xs,
      ∀ (φ : L.BoundedFormula Empty n) (x x_1 : Fin n),
        (decide ¬x = x_1) = true → ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → φ.Realize default xs) →
    Nonempty (Fin n ↪ M)

Tactic:
rintro ⟨xs, h⟩

Goal state after:
case refine_1
L : Language
M : Type w
inst✝ : L.Structure M
n : ℕ
xs : Fin n → M
h :
  ∀ (φ : L.BoundedFormula Empty n) (x x_1 : Fin n),
    (decide ¬x = x_1) = true → ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → φ.Realize default xs
⊢ Nonempty (Fin n ↪ M)
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case refine_1
L : Language
M : Type w
inst✝ : L.Structure M
n : ℕ
xs : Fin n → M
h :
  ∀ (φ : L.BoundedFormula Empty n) (x x_1 : Fin n),
    (decide ¬x = x_1) = true → ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → φ.Realize default xs
i j : Fin n
ij : xs i = xs j
⊢ i = j

Tactic:
contrapose! ij

Goal state after:
case refine_1
L : Language
M : Type w
inst✝ : L.Structure M
n : ℕ
xs : Fin n → M
h :
  ∀ (φ : L.BoundedFormula Empty n) (x x_1 : Fin n),
    (decide ¬x = x_1) = true → ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → φ.Realize default xs
i j : Fin n
ij : i ≠ j
⊢ xs i ≠ xs j
Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CompatibleRing K
p : ℕ
inst✝¹ : CharP K p
inst✝ : IsAlgClosed K
⊢ K ⊨ Theory.ACF p

Tactic:
by
  refine Theory.model_union_iff.2 ⟨inferInstance, ?_⟩
  simp only [Theory.model_iff, Set.mem_image,
    forall_exists_index, and_imp]
  rintro _ n hn0 rfl
  simp only [realize_genericMonicPolyHasRoot]
  rintro ⟨p, _, rfl⟩
  exact IsAlgClosed.exists_root p (ne_of_gt
    (natDegree_pos_iff_degree_pos.1 hn0))

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.FreeCommRing

Goal state before:
pp: ι : Type u_1
κ : Type u_2
R : Type u_3
inst✝² : DecidableEq κ
inst✝¹ : CommRing R
inst✝ : DecidableEq R
monoms : ι → Finset (κ →₀ ℕ)
p : { p // ∀ (i : ι), (p i).support ⊆ monoms i }
i : ι
m : κ →₀ ℕ
hm : m ∉ monoms i
⊢ 0 = (↑p i).coeff m

Tactic:
have : m ∉ (p.1 i).support := fun h => hm (p.2 i h)

Goal state after:
ι : Type u_1
κ : Type u_2
R : Type u_3
inst✝² : DecidableEq κ
inst✝¹ : CommRing R
inst✝ : DecidableEq R
monoms : ι → Finset (κ →₀ ℕ)
p : { p // ∀ (i : ι), (p i).support ⊆ monoms i }
i : ι
m : κ →₀ ℕ
hm : m ∉ monoms i
this : m ∉ (↑p i).support
⊢ 0 = (↑p i).coeff m
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: case inl
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
hφ : T ⊨ᵇ φ
⊢ M ⊨ φ ↔ T ⊨ᵇ φ

Tactic:
exact iff_of_true (hφ.realize_sentence M) hφ

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
h : T.IsComplete
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
φ : L.BoundedFormula Empty 0
⊢ T ⊨ᵇ φ ↔ M ⊨ φ

Tactic:
refine ⟨fun h_models => h_models.realize_sentence M, fun h_realize => ?_⟩

Goal state after:
L : Language
T : L.Theory
h : T.IsComplete
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
φ : L.BoundedFormula Empty 0
h_realize : M ⊨ φ
⊢ T ⊨ᵇ φ
Module: Mathlib.FieldTheory.AxGrothendieck

Goal state before:
pp: ι : Type u_1
K : Type u_2
R : Type u_3
inst✝⁴ : Field K
inst✝³ : Finite K
inst✝² : CommRing R
inst✝¹ : Finite ι
inst✝ : Algebra K R
alg : Algebra.IsAlgebraic K R
ps : ι → MvPolynomial ι R
S : Set (ι → R)
hm : Set.MapsTo (fun v i ↦ (eval v) (ps i)) S S
hinj : Set.InjOn (fun v i ↦ (eval v) (ps i)) S
is_int : ∀ (x : R), IsIntegral K x
v : ι → R
hvS : v ∈ S
val✝ : Fintype ι
s : Finset R := (univ.biUnion fun i ↦ image (fun x ↦ coeff x (ps i)) (ps i).support) ∪ image v univ
hv : ∀ (i : ι), v i ∈ Algebra.adjoin K ↑s
hs₁ : ∀ (i : ι), ∀ k ∈ (ps i).support, coeff k (ps i) ∈ Algebra.adjoin K ↑s
this✝ : IsNoetherian K ↥(Algebra.adjoin K ↑s)
this : Finite ↥(Algebra.adjoin K ↑s)
S' : Set (ι → ↥(Algebra.adjoin K ↑s)) := (fun v ↦ Subtype.val ∘ v) ⁻¹' S
res : ↑S' → ↑S' := fun x ↦ ⟨fun i ↦ ⟨(eval fun j ↦ ↑(↑x j)) (ps i), ⋯⟩, ⋯⟩
⊢ Function.Injective res

Tactic:
intro x

Goal state after:
ι : Type u_1
K : Type u_2
R : Type u_3
inst✝⁴ : Field K
inst✝³ : Finite K
inst✝² : CommRing R
inst✝¹ : Finite ι
inst✝ : Algebra K R
alg : Algebra.IsAlgebraic K R
ps : ι → MvPolynomial ι R
S : Set (ι → R)
hm : Set.MapsTo (fun v i ↦ (eval v) (ps i)) S S
hinj : Set.InjOn (fun v i ↦ (eval v) (ps i)) S
is_int : ∀ (x : R), IsIntegral K x
v : ι → R
hvS : v ∈ S
val✝ : Fintype ι
s : Finset R := (univ.biUnion fun i ↦ image (fun x ↦ coeff x (ps i)) (ps i).support) ∪ image v univ
hv : ∀ (i : ι), v i ∈ Algebra.adjoin K ↑s
hs₁ : ∀ (i : ι), ∀ k ∈ (ps i).support, coeff k (ps i) ∈ Algebra.adjoin K ↑s
this✝ : IsNoetherian K ↥(Algebra.adjoin K ↑s)
this : Finite ↥(Algebra.adjoin K ↑s)
S' : Set (ι → ↥(Algebra.adjoin K ↑s)) := (fun v ↦ Subtype.val ∘ v) ⁻¹' S
res : ↑S' → ↑S' := fun x ↦ ⟨fun i ↦ ⟨(eval fun j ↦ ↑(↑x j)) (ps i), ⋯⟩, ⋯⟩
x : ↑S'
⊢ ∀ ⦃a₂ : ↑S'⦄, res x = res a₂ → x = a₂
Module: Mathlib.FieldTheory.Differential.Basic

Goal state before:
pp: R : Type u_1
inst✝⁶ : Field R
inst✝⁵ : Differential R
a✝ b : R
F : Type u_2
inst✝⁴ : Field F
inst✝³ : Differential F
inst✝² : CharZero F
p : F[X]
inst✝¹ : Fact (Irreducible p)
inst✝ : Fact p.Monic
a : F
⊢ ((algebraMap F (AdjoinRoot p)) a)′ = (algebraMap F (AdjoinRoot p)) a′

Tactic:
change (Derivation.liftOfSurjective _ _) ((AdjoinRoot.mk p).toIntAlgHom (C a)) = _
    rw [Derivation.liftOfSurjective_apply, implicitDeriv_C]
    rfl

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

Goal state before:
pp: k : Type u_1
inst✝⁴ : Field k
inst✝³ : Finite k
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP k p
n : ℕ
inst✝ : NeZero n
g : Gal(Extension k p n/k)
this : Fintype k := Fintype.ofFinite k
⊢ ∃ i < n, frob k p n ^ i = g

Tactic:
obtain ⟨⟨i, hi⟩, rfl⟩ := (FiniteField.bijective_frobeniusAlgEquivOfAlgebraic_pow k
    (Extension k p n)).2 g

Goal state after:
k : Type u_1
inst✝⁴ : Field k
inst✝³ : Finite k
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP k p
n : ℕ
inst✝ : NeZero n
this : Fintype k := Fintype.ofFinite k
i : ℕ
hi : i < Module.finrank k (Extension k p n)
⊢ ∃ i_1 < n, frob k p n ^ i_1 = (fun n_1 ↦ frobeniusAlgEquivOfAlgebraic k (Extension k p n) ^ ↑n_1) ⟨i, hi⟩
Module: Mathlib.FieldTheory.Differential.Basic

Goal state before:
pp: case hf
R : Type u_1
inst✝⁹ : Field R
inst✝⁸ : Differential R
a✝ b : R
F : Type u_2
inst✝⁷ : Field F
inst✝⁶ : Differential F
inst✝⁵ : CharZero F
K : Type u_3
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Differential K
inst✝¹ : DifferentialAlgebra F K
B : IntermediateField F K
inst✝ : FiniteDimensional F ↥B
a : ↥B
⊢ Function.Injective ⇑B.val

Tactic:
exact Subtype.val_injective

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

Goal state before:
pp: case a
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′
| fun x ↦ ↑(c x) * logDeriv ↑(u x)

Tactic:
intro x

Goal state after:
case a
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′
x : ι
| ↑(c x) * logDeriv ↑(u x)
Module: Mathlib.Topology.Separation.Connected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
h : TotallyDisconnectedSpace X
⊢ ∀ (x : X), IsClosed[inst✝] {x}

Tactic:
intro x

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
h : TotallyDisconnectedSpace X
x : X
⊢ IsClosed[inst✝] {x}
Module: Mathlib.FieldTheory.Differential.Liouville

Goal state before:
pp: case refine_1
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
inst✝² : FiniteDimensional F K
inst✝¹ : IsGalois F K
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → K
v : K
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
this : CharZero K
c₀ : ι → F := fun i ↦ c i / ↑(Fintype.card Gal(K/F))
u₁ : ι → K := fun i ↦ ∏ x, x (u i)
ffb : fixedField ⊤ = ⊥
u₀ : ι → F
hu₀ : ∀ (i : ι), (algebraMap F K) (u₀ i) = u₁ i
v₁ : K := (∑ x, x v) / ↑(Fintype.card Gal(K/F))
v₀ : F
hv₀ : (algebraMap F K) v₀ = v₁
⊢ ∀ (x : ι), (c₀ x)′ = 0

Tactic:
intro x

Goal state after:
case refine_1
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
inst✝² : FiniteDimensional F K
inst✝¹ : IsGalois F K
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → K
v : K
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
this : CharZero K
c₀ : ι → F := fun i ↦ c i / ↑(Fintype.card Gal(K/F))
u₁ : ι → K := fun i ↦ ∏ x, x (u i)
ffb : fixedField ⊤ = ⊥
u₀ : ι → F
hu₀ : ∀ (i : ι), (algebraMap F K) (u₀ i) = u₁ i
v₁ : K := (∑ x, x v) / ↑(Fintype.card Gal(K/F))
v₀ : F
hv₀ : (algebraMap F K) v₀ = v₁
x : ι
⊢ (c₀ x)′ = 0
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
inst✝² : FiniteDimensional F K
inst✝¹ : IsGalois F K
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → K
v : K
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
this : CharZero K
ffb : fixedField ⊤ = ⊥
| (algebraMap F K) a * ↑(Fintype.card Gal(K/F)) = ∑ x, ↑(c x) * logDeriv (∏ x_1, x_1 (u x)) + ∑ x, (x v)′

Tactic:
2,

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
inst✝² : FiniteDimensional F K
inst✝¹ : IsGalois F K
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → K
v : K
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
this : CharZero K
ffb : fixedField ⊤ = ⊥
| ∑ x, ↑(c x) * logDeriv (∏ x_1, x_1 (u x)) + ∑ x, (x v)′
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
inst✝² : FiniteDimensional F K
inst✝¹ : IsGalois F K
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → K
v : K
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
this : CharZero K
ffb : fixedField ⊤ = ⊥
| ∑ x, ↑(c x) * logDeriv (∏ x_1, x_1 (u x))

Tactic:
2,

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
inst✝² : FiniteDimensional F K
inst✝¹ : IsGalois F K
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → K
v : K
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
this : CharZero K
ffb : fixedField ⊤ = ⊥
| fun x ↦ ↑(c x) * logDeriv (∏ x_1, x_1 (u x))
Module: Mathlib.FieldTheory.CardinalEmb

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

Tactic:
simp_rw [adjoin_image_leastExt, eq_top_iff, ← adjoin_basis_eq_top, adjoin_le_iff]

Goal state after:
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
⊢ range ⇑b ⊆ ↑(⨆ i, adjoin F (⇑b '' Iio (φ i)))
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 : (Module.rank F E).ord.ToType
⊢ adjoin F (⇑b ∘ φ '' Iio (i⁺)) = IntermediateField.restrictScalars F (↥(adjoin F (⇑b ∘ φ '' Iio i)))⟮b (φ i)⟯

Tactic:
rw [Iio_succ, ← Iio_insert, image_insert_eq, ← union_singleton, adjoin_adjoin_left]

Goal state after:
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 : (Module.rank F E).ord.ToType
⊢ adjoin F (⇑b ∘ φ '' Iio i ∪ {(⇑b ∘ φ) i}) = adjoin F (⇑b ∘ φ '' Iio i ∪ {b (φ i)})
Module: Mathlib.FieldTheory.Galois.Profinite

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

Tactic:
intro x

Goal state after:
case h.left
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : Normal k ↥L
N : Set Gal(↥L/k)
L' : IntermediateField k ↥L
left✝ : FiniteDimensional k ↥L'
hO : ↑L'.fixingSubgroup ⊆ N
this : Module.Finite k ↥(IntermediateField.lift L')
x : Gal(K/k)
⊢ x ∈ ↑(IntermediateField.lift L').fixingSubgroup → x ∈ ⇑(AlgEquiv.restrictNormalHom ↥L) ⁻¹' N
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: case mp
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y z : ℕ
H : (⇑(frobenius K p))^[(0, ↑y).1 + z] (0, ↑x).2 = (⇑(frobenius K p))^[(0, ↑x).1 + z] (0, ↑y).2
⊢ ↑x = ↑y

Tactic:
simpa only [zero_add, iterate_fixed (map_natCast _ _)] using H

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
⊢ ∀ (x : ℕ), ↑x = 0 ↔ p ∣ x

Tactic:
intro x

Goal state after:
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : ℕ
⊢ ↑x = 0 ↔ p ∣ x