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

Goal state before:
pp: case func.succ.inl
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
v : β → M
n✝ : ℕ
ts : Fin (n✝ + 1) → L[[α]].Term β
ih : ∀ (a : Fin (n✝ + 1)), realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (ts a).constantsToVars = realize v (ts a)
val✝ : L.Functions (n✝ + 1)
⊢ realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (func (Sum.inl val✝) ts).constantsToVars =
    realize v (func (Sum.inl val✝) ts)

Tactic:
simp only [realize, ih, constantsOn, constantsOnFunc, constantsToVars]

Goal state after:
case func.succ.inl
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
v : β → M
n✝ : ℕ
ts : Fin (n✝ + 1) → L[[α]].Term β
ih : ∀ (a : Fin (n✝ + 1)), realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (ts a).constantsToVars = realize v (ts a)
val✝ : L.Functions (n✝ + 1)
⊢ (funMap val✝ fun i ↦ realize v (ts i)) = funMap (Sum.inl val✝) fun i ↦ realize v (ts i)
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case refine_1
L : Language
α : Type u'
⊢ lift.{max u u', 0} ℵ₀ * ⨆ i, #(L.Term (α ⊕ Fin i)) ≤ max ℵ₀ #(α ⊕ (i : ℕ) × L.Functions i)

Tactic:
lift_aleph0,

Goal state after:
case refine_1
L : Language
α : Type u'
⊢ ℵ₀ * ⨆ i, #(L.Term (α ⊕ Fin i)) ≤ max ℵ₀ #(α ⊕ (i : ℕ) × L.Functions 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
x : M
⊢ ∀ ⦃a₂ : M⦄, φ x = φ a₂ → x = a₂

Tactic:
y

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 y : M
⊢ φ x = φ y → x = y
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: case mk.mk
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
carrier✝¹ : Set M
fun_mem✝¹ : ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f carrier✝¹
carrier✝ : Set M
fun_mem✝ : ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f carrier✝
h : ↑{ carrier := carrier✝¹, fun_mem := fun_mem✝¹ } = ↑{ carrier := carrier✝, fun_mem := fun_mem✝ }
⊢ { carrier := carrier✝¹, fun_mem := fun_mem✝¹ } = { carrier := carrier✝, fun_mem := fun_mem✝ }

Tactic:
congr

Goal state after:
Module: Mathlib.ModelTheory.ElementaryMaps

Goal state before:
pp: case refine_1
L : Language
M : Type u_1
N✝ : Type u_2
P : Type u_3
Q : Type u_4
inst✝⁷ : L.Structure M
inst✝⁶ : L.Structure N✝
inst✝⁵ : L.Structure P
inst✝⁴ : L.Structure Q
N : Type u_5
inst✝³ : L.Structure N
inst✝² : L[[M]].Structure N
inst✝¹ : (L.lhomWithConstants M).IsExpansionOn N
inst✝ : N ⊨ L.elementaryDiagram M
n : ℕ
φ : L.Formula (Fin n)
x : Fin n → M
⊢ BoundedFormula.Realize φ (fun x_1 ↦ ↑(Sum.inr (x x_1))) default ↔
    BoundedFormula.Realize φ (fun a ↦ Term.realize default (Constants.term (Sum.inr (x a)))) default

Tactic:
Term.realize_constants

Goal state after:
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
ι : Sort u_3
S : ι → L.Substructure M
⊢ ⨆ i, S i = (closure L).toFun (⋃ i, ↑(S i))

Tactic:
simp_rw [closure_iUnion, closure_eq]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
φ : L.Formula α
x : α → M
y : Fin 0 → M
⊢ BoundedFormula.Realize φ x y = BoundedFormula.Realize φ x default

Tactic:
congr

Goal state after:
case e__xs
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
φ : L.Formula α
x : α → M
y : Fin 0 → M
⊢ y = default
Module: Mathlib.ModelTheory.ElementaryMaps

Goal state before:
pp: case refine_3
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✝ l✝ : ℕ
R : L.Relations l✝
ts : Fin l✝ → L.Term (Empty ⊕ Fin n✝)
xs : Fin n✝ → M
⊢ (RelMap R fun i ↦ (⇑f ∘ Term.realize (Sum.elim default xs)) (ts i)) ↔
    RelMap R fun i ↦ (Term.realize (Sum.elim default xs) ∘ ts) i

Tactic:
← Function.comp_apply (f := (f : M → N) ∘ Term.realize (Sum.elim default xs))

Goal state after:
case refine_3
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✝ l✝ : ℕ
R : L.Relations l✝
ts : Fin l✝ → L.Term (Empty ⊕ Fin n✝)
xs : Fin n✝ → M
⊢ (RelMap R fun i ↦ ((⇑f ∘ Term.realize (Sum.elim default xs)) ∘ ts) i) ↔
    RelMap R fun i ↦ (Term.realize (Sum.elim default xs) ∘ ts) i
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 ⋯
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)
      default

Tactic:
congr

Goal state after:
case e__xs
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
⊢ (fun x_1 ↦ x (natAdd (Classical.choose ⋯) x_1)) = default
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
v' : Fin 0 → M
⊢ Realize (Formula.iAlls β φ) v v' = (Formula.iAlls β φ).Realize v

Tactic:
congr

Goal state after:
case e__xs
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
v' : Fin 0 → M
⊢ v' = default
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 ⋯
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))
      default

Tactic:
congr

Goal state after:
case e__xs
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
⊢ (fun x_1 ↦ x (natAdd (Classical.choose ⋯) x_1)) = default
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
v' : Fin 0 → M
⊢ Realize (Formula.iExs γ φ) v v' = (Formula.iExs γ φ).Realize v

Tactic:
congr

Goal state after:
case e__xs
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
v' : Fin 0 → M
⊢ v' = default
Module: Mathlib.ModelTheory.ElementarySubstructures

Goal state before:
pp: L : Language
M : Type u_1
inst✝ : L.Structure M
x✝² x✝¹ : L.ElementarySubstructure M
s : Set M
hs1 : ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f s
hs2 : { carrier := s, fun_mem := hs1 }.IsElementary
t : Set M
ht1 : ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f t
isElementary'✝ : { carrier := t, fun_mem := ht1 }.IsElementary
x✝ :
  (fun x ↦ ↑↑x) { toSubstructure := { carrier := s, fun_mem := hs1 }, isElementary' := hs2 } =
    (fun x ↦ ↑↑x) { toSubstructure := { carrier := t, fun_mem := ht1 }, isElementary' := isElementary'✝ }
⊢ { toSubstructure := { carrier := s, fun_mem := hs1 }, isElementary' := hs2 } =
    { toSubstructure := { carrier := t, fun_mem := ht1 }, isElementary' := isElementary'✝ }

Tactic:
congr

Goal state after:
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: L : Language
α : Type u'
⊢ max (lift.{max (max u u') v, max (max u u') v} #((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ))
      (lift.{max (max u u') v, max (max u u') v} ℵ₀) ≤
    lift.{max (max u u') v, max (max u u') v} (max ℵ₀ (lift.{max u v, u'} #α + lift.{u', max u v} L.card))

Tactic:
lift_aleph0,

Goal state after:
L : Language
α : Type u'
⊢ max (lift.{max (max u u') v, max (max u u') v} #((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)) ℵ₀ ≤
    lift.{max (max u u') v, max (max u u') v} (max ℵ₀ (lift.{max u v, u'} #α + lift.{u', max u v} L.card))
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: L : Language
α : Type u'
⊢ max (lift.{max (max u u') v, max (max u u') v} #((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)) ℵ₀ ≤
    max (lift.{max (max u u') v, max (max u u') v} ℵ₀)
      (lift.{max (max u u') v, max (max u u') v} (lift.{max u v, u'} #α + lift.{u', max u v} L.card))

Tactic:
lift_aleph0,

Goal state after:
L : Language
α : Type u'
⊢ max (lift.{max (max u u') v, max (max u u') v} #((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)) ℵ₀ ≤
    max ℵ₀ (lift.{max (max u u') v, max (max u u') v} (lift.{max u v, u'} #α + lift.{u', max u v} L.card))
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:
enter [2, 1, i]

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

Goal state before:
pp: L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
v' : Fin 0 → M
⊢ Realize (Formula.iExsUnique γ φ) v v' = (Formula.iExsUnique γ φ).Realize v

Tactic:
congr

Goal state after:
case e__xs
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
v' : Fin 0 → M
⊢ v' = default
Module: Mathlib.ModelTheory.Encoding

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

Tactic:
refine mk_le_aleph0_iff.mp ?_

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

Goal state before:
pp: case intro.intro.mpr.refine_2
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 β
h :
  A.Definable L
    ((fun g ↦ g ∘ rangeSplitting f) ⁻¹'
      (fun g ↦ g ∘ Sum.inl) ''
        (fun g ↦ g ∘ ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ''
          (fun g ↦ g ∘ ⇑(Equiv.Set.sumCompl (range f))) '' s)
h' : A.Definable L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
y : β → M
ys : y ∈ s
a : α
⊢ (y ∘ f) a = (y ∘ f) (rangeSplitting f (rangeFactorization f a))

Tactic:
Function.comp_apply,

Goal state after:
case intro.intro.mpr.refine_2
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 β
h :
  A.Definable L
    ((fun g ↦ g ∘ rangeSplitting f) ⁻¹'
      (fun g ↦ g ∘ Sum.inl) ''
        (fun g ↦ g ∘ ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ''
          (fun g ↦ g ∘ ⇑(Equiv.Set.sumCompl (range f))) '' s)
h' : A.Definable L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
y : β → M
ys : y ∈ s
a : α
⊢ y (f a) = (y ∘ f) (rangeSplitting f (rangeFactorization f a))
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: case intro.intro.mpr.refine_2
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 β
h :
  A.Definable L
    ((fun g ↦ g ∘ rangeSplitting f) ⁻¹'
      (fun g ↦ g ∘ Sum.inl) ''
        (fun g ↦ g ∘ ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ''
          (fun g ↦ g ∘ ⇑(Equiv.Set.sumCompl (range f))) '' s)
h' : A.Definable L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
y : β → M
ys : y ∈ s
a : α
⊢ y (f a) = (y ∘ f) (rangeSplitting f (rangeFactorization f a))

Tactic:
Function.comp_apply,

Goal state after:
case intro.intro.mpr.refine_2
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 β
h :
  A.Definable L
    ((fun g ↦ g ∘ rangeSplitting f) ⁻¹'
      (fun g ↦ g ∘ Sum.inl) ''
        (fun g ↦ g ∘ ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ''
          (fun g ↦ g ∘ ⇑(Equiv.Set.sumCompl (range f))) '' s)
h' : A.Definable L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
y : β → M
ys : y ∈ s
a : α
⊢ y (f a) = y (f (rangeSplitting f (rangeFactorization f a)))
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'
⊢ max (lift.{w, max u v} ℵ₀) (lift.{w, max u v} L.card) ≤ lift.{max u v, w} #↑(⇑Equiv.ulift '' s')

Tactic:
lift_aleph0,

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'
⊢ max ℵ₀ (lift.{w, max u v} L.card) ≤ lift.{max u v, w} #↑(⇑Equiv.ulift '' s')
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), ⋯⟩, ⋯⟩
x : ↑S'
⊢ ∀ ⦃a₂ : ↑S'⦄, res x = res a₂ → x = a₂

Tactic:
y

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 y : ↑S'
⊢ res x = res y → x = y
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′
| ∑ x, ↑(c x) * logDeriv ↑(u x) + (↑v)′

Tactic:
congr

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)

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′
| (↑v)′
Module: Mathlib.Topology.Separation.Connected

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : ConnectedSpace X
inst✝¹ : Nontrivial X
inst✝ : T1Space X
x : X
contra : ¬(𝓝[≠] x).NeBot
⊢ False

Tactic:
not_neBot,

Goal state after:
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : ConnectedSpace X
inst✝¹ : Nontrivial X
inst✝ : T1Space X
x : X
contra : 𝓝[≠] x = ⊥
⊢ False
Module: Mathlib.FieldTheory.Galois.NormalBasis

Goal state before:
pp: case e'_4
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Finite L
this✝ : Finite K
this : Fintype K
x : L
hx :
  Ideal.span {X ^ finrank K L - 1} =
    (toSpanSingleton K[X] (AEval' (frobeniusAlgHom K L).toLinearMap)
        ((AEval'.of (frobeniusAlgHom K L).toLinearMap) x)).ker
e_1✝ : Fin (X ^ finrank K L - C 1).natDegree = Fin (AdjoinRoot.powerBasis ⋯).dim
i : Fin (X ^ finrank K L - C 1).natDegree
⊢ ((fun σ ↦ σ x) ∘ ⇑(Equiv.ofBijective (fun n ↦ frobeniusAlgEquivOfAlgebraic K L ^ ↑n) ⋯) ∘ ⇑(finCongr ⋯)) i =
    (⇑(↑(AEval'.of (frobeniusAlgHom K L).toLinearMap).symm ∘ₗ
            ↑K
              (liftQ (Ideal.span {X ^ finrank K L - 1})
                (toSpanSingleton K[X] (AEval' (frobeniusAlgHom K L).toLinearMap)
                  ((AEval'.of (frobeniusAlgHom K L).toLinearMap) x))
                ⋯)) ∘
        ⇑(AdjoinRoot.powerBasis ⋯).basis)
      i

Tactic:
Function.comp_apply,

Goal state after:
case e'_4
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Finite L
this✝ : Finite K
this : Fintype K
x : L
hx :
  Ideal.span {X ^ finrank K L - 1} =
    (toSpanSingleton K[X] (AEval' (frobeniusAlgHom K L).toLinearMap)
        ((AEval'.of (frobeniusAlgHom K L).toLinearMap) x)).ker
e_1✝ : Fin (X ^ finrank K L - C 1).natDegree = Fin (AdjoinRoot.powerBasis ⋯).dim
i : Fin (X ^ finrank K L - C 1).natDegree
⊢ ((Equiv.ofBijective (fun n ↦ frobeniusAlgEquivOfAlgebraic K L ^ ↑n) ⋯) ((finCongr ⋯) i)) x =
    (↑(AEval'.of (frobeniusAlgHom K L).toLinearMap).symm ∘ₗ
        ↑K
          (liftQ (Ideal.span {X ^ finrank K L - 1})
            (toSpanSingleton K[X] (AEval' (frobeniusAlgHom K L).toLinearMap)
              ((AEval'.of (frobeniusAlgHom K L).toLinearMap) x))
            ⋯))
      ((AdjoinRoot.powerBasis ⋯).basis i)
Module: Mathlib.FieldTheory.Galois.Profinite

Goal state before:
pp: case mk.mk
k : Type u_3
K : Type u_4
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
g : ↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop
L : IntermediateField k K
finiteDimensional✝¹ : FiniteDimensional k ↥L
isGalois✝¹ : IsGalois k ↥L
x : ↥{ toIntermediateField := L, finiteDimensional := finiteDimensional✝¹, isGalois := isGalois✝¹ }.toIntermediateField
L' : IntermediateField k K
finiteDimensional✝ : FiniteDimensional k ↥L'
isGalois✝ : IsGalois k ↥L'
h :
  { toIntermediateField := L, finiteDimensional := finiteDimensional✝¹, isGalois := isGalois✝¹ } ≤
    { toIntermediateField := L', finiteDimensional := finiteDimensional✝, isGalois := isGalois✝ }
this✝ : Algebra ↥L ↥L' := (Subsemiring.inclusion h).toAlgebra
this : IsScalarTower k ↥L ↥L' := IsScalarTower.of_algebraMap_eq (congrFun rfl)
⊢ (algebraMap (↥L') K)
      ((algebraMap ↥L ↥L')
        ((((proj { toIntermediateField := L', finiteDimensional := finiteDimensional✝, isGalois := isGalois✝ })
                g).restrictNormal
            ↥L)
          x)) =
    ↑(((proj { toIntermediateField := L', finiteDimensional := finiteDimensional✝, isGalois := isGalois✝ }) g) ⟨↑x, ⋯⟩)

Tactic:
rw [AlgEquiv.restrictNormal_commutes (proj (mk L') g) L]

Goal state after:
case mk.mk
k : Type u_3
K : Type u_4
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
g : ↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop
L : IntermediateField k K
finiteDimensional✝¹ : FiniteDimensional k ↥L
isGalois✝¹ : IsGalois k ↥L
x : ↥{ toIntermediateField := L, finiteDimensional := finiteDimensional✝¹, isGalois := isGalois✝¹ }.toIntermediateField
L' : IntermediateField k K
finiteDimensional✝ : FiniteDimensional k ↥L'
isGalois✝ : IsGalois k ↥L'
h :
  { toIntermediateField := L, finiteDimensional := finiteDimensional✝¹, isGalois := isGalois✝¹ } ≤
    { toIntermediateField := L', finiteDimensional := finiteDimensional✝, isGalois := isGalois✝ }
this✝ : Algebra ↥L ↥L' := (Subsemiring.inclusion h).toAlgebra
this : IsScalarTower k ↥L ↥L' := IsScalarTower.of_algebraMap_eq (congrFun rfl)
⊢ (algebraMap (↥L') K)
      (((proj { toIntermediateField := L', finiteDimensional := finiteDimensional✝, isGalois := isGalois✝ }) g)
        ((algebraMap ↥L
            ↥{ toIntermediateField := L', finiteDimensional := finiteDimensional✝,
                  isGalois := isGalois✝ }.toIntermediateField)
          x)) =
    ↑(((proj { toIntermediateField := L', finiteDimensional := finiteDimensional✝, isGalois := isGalois✝ }) g) ⟨↑x, ⋯⟩)
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: case zero
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : ℕ × K
⊢ mk K p x ^ 0 = mk K p (x.1, x.2 ^ 0)

Tactic:
rw [pow_zero, pow_zero, one_def, mk_eq_iff]

Goal state after:
case zero
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : ℕ × K
⊢ ∃ z, (⇑(frobenius K p))^[(x.1, 1).1 + z] (0, 1).2 = (⇑(frobenius K p))^[(0, 1).1 + z] (x.1, 1).2
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ ProfiniteGrp.{max v u}
i j : J
f : i ⟶ j
⊢ { hom' := { toFun := fun x ↦ ↑x j, map_one' := ⋯, map_mul' := ⋯, continuous_toFun := ⋯ } } =
    { hom' := { toFun := fun x ↦ ↑x i, map_one' := ⋯, map_mul' := ⋯, continuous_toFun := ⋯ } } ≫ F.map f

Tactic:
congr

Goal state after:
J : Type v
inst✝ : SmallCategory J
F : J ⥤ ProfiniteGrp.{max v u}
i j : J
f : i ⟶ j
⊢ (fun x ↦ ↑x j) = fun x ↦
    (F.map f).hom'.toMonoidHom
      ({ hom' := { toFun := fun x ↦ ↑x i, map_one' := ⋯, map_mul' := ⋯, continuous_toFun := ⋯ } }.hom'.toMonoidHom x)