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

Goal state before:
pp: case equal
L : Language
L' : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : L'.Structure M
k : ℕ
ft : (n : ℕ) → L.Term (α ⊕ Fin n) → L'.Term (β ⊕ Fin (k + n))
fr : (n : ℕ) → L.Relations n → L'.Relations n
n : ℕ
v : {n : ℕ} → (Fin (k + n) → M) → α → M
v' : β → M
h1 :
  ∀ (n : ℕ) (t : L.Term (α ⊕ Fin n)) (xs' : Fin (k + n) → M),
    realize (Sum.elim v' xs') (ft n t) = realize (Sum.elim (v xs') (xs' ∘ natAdd k)) t
h2 : ∀ (n : ℕ) (R : L.Relations n) (x : Fin n → M), RelMap (fr n R) x = RelMap R x
hv : ∀ (n : ℕ) (xs : Fin (k + n) → M) (x : M), v (snoc xs x) = v xs
n✝ : ℕ
t₁✝ t₂✝ : L.Term (α ⊕ Fin n✝)
xs : Fin (k + n✝) → M
⊢ (mapTermRel ft fr (fun x ↦ castLE ⋯) (equal t₁✝ t₂✝)).Realize v' xs ↔ (equal t₁✝ t₂✝).Realize (v xs) (xs ∘ natAdd k)

Tactic:
simp [mapTermRel, Realize, h1]

Goal state after:
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: L : Language
α : Type u'
l : List (L.Term α)
t : L.Term α
⊢ ∀ (l : List (α ⊕ (i : ℕ) × L.Functions i)), listDecode (t.listEncode ++ l) = t :: listDecode l

Tactic:
l

Goal state after:
L : Language
α : Type u'
l✝ : List (L.Term α)
t : L.Term α
l : List (α ⊕ (i : ℕ) × L.Functions i)
⊢ listDecode (t.listEncode ++ l) = t :: listDecode l
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
n : ℕ
φ : L.BoundedFormula α n
tf : α → L.Term β
v : β → M
xs : Fin n → M
⊢ ∀ (n : ℕ) (R : L.Relations n) (x : Fin n → M), RelMap (id R) x = RelMap R x

Tactic:
by simp

Goal state after:
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
f : M ↪ₑ[L] N
α : Type u_5
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin n → M
h :
  (φ.restrictFreeVar id).Realize ((↑f ∘ v) ∘ Subtype.val) (↑f ∘ xs) ↔
    (φ.restrictFreeVar id).Realize
      (((Sum.elim (v ∘ Subtype.val) xs ∘ ⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n)).symm) ∘
          ⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n))) ∘
        Sum.inl)
      (((Sum.elim (v ∘ Subtype.val) xs ∘ ⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n)).symm) ∘
          ⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n))) ∘
        Sum.inr)
⊢ ∀ (a : ↥φ.freeVarFinset), (v ∘ Subtype.val) (id a) = v ↑a

Tactic:
by simp

Goal state after:
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
f : M ↪ₑ[L] N
α : Type u_5
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin n → M
⊢ φ.Realize (⇑f ∘ v) (⇑f ∘ xs) ↔ φ.Realize v xs

Tactic:
rw [← BoundedFormula.realize_restrictFreeVar' Set.Subset.rfl, Set.inclusion_eq_id]
    have h :=
      f.map_formula' ((φ.restrictFreeVar id).toFormula.relabel (Fintype.equivFin _))
        (Sum.elim (v ∘ (↑)) xs ∘ (Fintype.equivFin _).symm)
    simp only [Formula.realize_relabel, BoundedFormula.realize_toFormula] at h
    rw [← Function.comp_assoc _ _ (Fintype.equivFin _).symm,
      Function.comp_assoc _ (Fintype.equivFin _).symm (Fintype.equivFin _),
      _root_.Equiv.symm_comp_self, Function.comp_id, Function.comp_assoc, Sum.elim_comp_inl,
      Function.comp_assoc _ _ Sum.inr, Sum.elim_comp_inr, ← Function.comp_assoc] at h
    refine h.trans ?_
    rw [Function.comp_assoc _ _ (Fintype.equivFin _), _root_.Equiv.symm_comp_self,
      Function.comp_id, Sum.elim_comp_inl, Sum.elim_comp_inr (v ∘ Subtype.val) xs,
      BoundedFormula.realize_restrictFreeVar v (by simp)]

Goal state after:
Module: Mathlib.ModelTheory.ElementaryMaps

Goal state before:
pp: 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
f✝ : M ↪ₑ[L] N
x✝ : ℕ
f : L.Functions x✝
x : Fin x✝ → M
⊢ f✝ (funMap f x) = funMap f (⇑f✝ ∘ x)

Tactic:
by simp

Goal state after:
Module: Mathlib.ModelTheory.ElementaryMaps

Goal state before:
pp: 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
f : M ↪ₑ[L] N
x✝ : ℕ
R : L.Relations x✝
x : Fin x✝ → M
⊢ RelMap R (⇑f ∘ x) ↔ RelMap R x

Tactic:
by simp

Goal state after:
Module: Mathlib.ModelTheory.ElementaryMaps

Goal state before:
pp: 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
f : M ↪ₑ[L] N
x✝ : ℕ
R : L.Relations x✝
x : Fin x✝ → M
⊢ RelMap R x → RelMap R (⇑f ∘ x)

Tactic:
by simp

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
inst✝ : DecidableEq α
n : ℕ
φ : L.BoundedFormula α n
s : Set α
h : ↑φ.freeVarFinset ⊆ s
v : α → M
xs : Fin n → M
⊢ ∀ (a : ↥φ.freeVarFinset), (v ∘ Subtype.val) (Set.inclusion h a) = v ↑a

Tactic:
by simp

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
v : α → M
k : ℕ
R : L.Relations k
ts : Fin k → L.Term α
⊢ (RelMap R fun i ↦ Term.realize (Sum.elim v default) (Term.relabel Sum.inl (ts i))) ↔
    RelMap R fun i ↦ Term.realize v (ts i)

Tactic:
by simp

Goal state after:
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
P : Type u_2
inst✝ : L.Structure P
S : L.Substructure P
⊢ ∀ (x : P), x ∈ comap (Hom.id L P) S ↔ x ∈ S

Tactic:
by simp

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
φ : L.Sentence
⊢ M ⊨ {φ} ↔ M ⊨ φ

Tactic:
by simp

Goal state after:
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
m : ↥⊤
⊢ (fun m ↦ ⟨m, ⋯⟩) (⊤.subtype m) = m

Tactic:
by simp

Goal state after:
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
f✝ : M ↪[L] N
s : L.Substructure M
n : ℕ
f : L.Functions n
x : Fin n → ↥s
⊢ (codRestrict (Substructure.map f✝.toHom s) (f✝.domRestrict s) ⋯) (funMap f x) =
    funMap f (⇑(codRestrict (Substructure.map f✝.toHom s) (f✝.domRestrict s) ⋯) ∘ x)

Tactic:
by simp

Goal state after:
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
f : M ↪[L] N
s : L.Substructure M
n : ℕ
R : L.Relations n
x : Fin n → ↥s
⊢ RelMap R (⇑(codRestrict (Substructure.map f.toHom s) (f.domRestrict s) ⋯) ∘ x) ↔ RelMap R x

Tactic:
by simp

Goal state after:
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
f✝ : M ↪[L] N
n : ℕ
f : L.Functions n
x : Fin n → M
⊢ (codRestrict f✝.toHom.range f✝ ⋯) (funMap f x) = funMap f (⇑(codRestrict f✝.toHom.range f✝ ⋯) ∘ x)

Tactic:
by simp

Goal state after:
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
f : M ↪[L] N
n : ℕ
R : L.Relations n
x : Fin n → M
⊢ RelMap R (⇑(codRestrict f.toHom.range f ⋯) ∘ x) ↔ RelMap R x

Tactic:
by simp

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case all
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)
⊢ (relabel (Sum.elim (Sum.inl ∘ Sum.inl) (Sum.map Sum.inr id ∘ ⇑finSumFinEquiv.symm)) f✝.toFormula).Realize v
      (snoc default a) ↔
    f✝.toFormula.Realize (Sum.elim (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a))

Tactic:
realize_relabel,

Goal state after:
case all
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)
⊢ Realize f✝.toFormula
      (Sum.elim v (snoc default a ∘ castAdd 0) ∘
        Sum.elim (Sum.inl ∘ Sum.inl) (Sum.map Sum.inr id ∘ ⇑finSumFinEquiv.symm))
      (snoc default a ∘ natAdd 1) ↔
    f✝.toFormula.Realize (Sum.elim (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a))
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
φ : L.Formula (↑A ⊕ α)
A0 : Finset M := Finset.image Subtype.val (BoundedFormula.freeVarFinset φ).toLeft
x✝ : α → M
⊢ ∀ (a : ↥(BoundedFormula.freeVarFinset φ)),
    Sum.elim Subtype.val x✝
        (Sum.rec (motive := fun x ↦ x ∈ BoundedFormula.freeVarFinset φ → ↥A0 ⊕ α) (fun val hx ↦ Sum.inl ⟨↑val, ⋯⟩)
          (fun val x ↦ Sum.inr val) ↑a ⋯) =
      Sum.elim Subtype.val x✝ ↑a

Tactic:
by simp

Goal state after:
Module: Mathlib.ModelTheory.ElementarySubstructures

Goal state before:
pp: L : Language
M : Type u_1
inst✝ : L.Structure M
S : L.ElementarySubstructure M
D : Set M
x : M
hx : x ∈ D
φ : L[[↑↑S]].Formula (Fin 1)
hφ : {x | x 0 ∈ D} = ofPred φ.Realize
hφx : φ.Realize ![x]
ψ : L[[↑↑S]].Sentence := iExs (Fin 1) (relabel Sum.inr φ)
hψM : M ⊨ ψ
v' : Fin 1 → ↥S
hv' : φ.Realize v'
⊢ ↑(v' 0) ∈ ↑S

Tactic:
by simp

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case all.mpr
L : Language
M : Type w
N : Type u_1
inst✝³ : L.Structure M
inst✝² : L.Structure N
α : Type u'
n : ℕ
F : Type u_4
inst✝¹ : EquivLike F M N
inst✝ : L.StrongHomClass F M N
g : F
v : α → M
n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ {xs : Fin (n✝ + 1) → M}, f✝.Realize (⇑g ∘ v) (⇑g ∘ xs) ↔ f✝.Realize v xs
xs : Fin n✝ → M
⊢ (∀ (x : M), f✝.Realize v (snoc xs x)) → ∀ (x : N), f✝.Realize (⇑g ∘ v) (snoc (⇑g ∘ xs) x)

Tactic:
intro h a
      have h' := h (EquivLike.inv g a)
      rw [← ih3, Fin.comp_snoc, EquivLike.apply_inv_apply g] at h'
      exact h'

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.{w, max v u} (max ℵ₀ L.card) ≤ lift.{max u v, w} #↑(⇑Equiv.ulift '' s')

Tactic:
· rw [lift_max, lift_aleph0, max_le_iff, aleph0_le_lift, and_comm, ← lift_le.{w'},
        lift_lift, lift_lift, ← aleph0_le_lift, h]
      refine ⟨?_, h1⟩
      rw [← lift_lift.{w', w}]
      refine _root_.trans (lift_le.{w}.2 h3) ?_
      rw [lift_lift, ← lift_lift.{w, max u v}, ← hs', ← h, lift_lift]

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 : (i : ι) × ↥(monoms i) → R
i : ι
⊢ ∀ (a : κ →₀ ℕ),
    a ∈ {m ∈ monoms i | ∃ (hm : m ∈ monoms i), p ⟨i, ⟨m, hm⟩⟩ ≠ 0} ↔
      (if hm : a ∈ monoms i then p ⟨i, ⟨a, hm⟩⟩ else 0) ≠ 0

Tactic:
by simp

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
M : Type w'
inst✝ : L.Structure M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h3 : lift.{w', w} κ ≤ lift.{w, w'} #M
⊢ lift.{w, w'} #↑∅ ≤ lift.{w', w} κ

Tactic:
by simp

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
φ : L.Sentence
this : DecidableEq L.Sentence := Classical.decEq L.Sentence
h : ∀ (T0 : Finset L.Sentence), ↑T0 ⊆ T → (↑T0 ∪ {Formula.not φ}).IsSatisfiable
T0 : Finset L.Sentence
hT0 : ↑T0 ⊆ T ∪ {Formula.not φ}
⊢ ↑T0 ⊆ ↑(T0.erase (Formula.not φ)) ∪ {Formula.not φ}

Tactic:
by simp

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: ⊢ lift.{0, 0} Language.empty.card ≤ lift.{0, 0} ℵ₀

Tactic:
by simp

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

Goal state before:
pp: R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : MulAction R X
hc : ∀ (s s' : ↥S), Commute s s'
h✝ : Infinite X
key : ∀ (x : X) (s s' : ↥S), s • x = s' • x → Commute s s' → x /ₒ s = x /ₒ s'
i : X × ↥S → OreLocalization S X := fun x ↦ x.1 /ₒ x.2
hsurj : Surjective i
hi : RightInverse (surjInv hsurj) i
j : OreLocalization S X → X × X := (fun x ↦ (x.1, x.2 • x.1)) ∘ surjInv hsurj
this✝ : Injective j
this : #(OreLocalization S X) ≤ lift.{u, v} #X * lift.{u, v} #X
⊢ ℵ₀ ≤ lift.{u, v} #X

Tactic:
by simp

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

Goal state before:
pp: n : ℕ
⊢ ↑n ≠ 0 ↔ n ≠ 0

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
ι : Type u_2
s : Multiset ι
f : ι → R
h : ∀ x ∈ s, f x ≠ 0
⊢ logDeriv (Multiset.map f s).prod = (Multiset.map (fun x ↦ logDeriv (f x)) s).sum

Tactic:
induction s using Multiset.induction_on

Goal state after:
case empty
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
ι : Type u_2
f : ι → R
h : ∀ x ∈ 0, f x ≠ 0
⊢ logDeriv (Multiset.map f 0).prod = (Multiset.map (fun x ↦ logDeriv (f x)) 0).sum

case cons
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
ι : Type u_2
f : ι → R
a✝¹ : ι
s✝ : Multiset ι
a✝ : (∀ x ∈ s✝, f x ≠ 0) → logDeriv (Multiset.map f s✝).prod = (Multiset.map (fun x ↦ logDeriv (f x)) s✝).sum
h : ∀ x ∈ a✝¹ ::ₘ s✝, f x ≠ 0
⊢ logDeriv (Multiset.map f (a✝¹ ::ₘ s✝)).prod = (Multiset.map (fun x ↦ logDeriv (f x)) (a✝¹ ::ₘ s✝)).sum
Module: Mathlib.FieldTheory.Finite.Polynomial

Goal state before:
pp: σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : MvPolynomial σ (ZMod p)
⊢ (frobenius (MvPolynomial σ (ZMod p)) p) f = (expand p) f

Tactic:
apply induction_on f
  · intro a; rw [expand_C, frobenius_def, ← C_pow, ZMod.pow_card]
  · simp only [map_add]; intro _ _ hf hg; rw [hf, hg]
  · simp only [expand_X, map_mul]
    intro _ _ hf; rw [hf, frobenius_def]

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

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

Tactic:
simp only [coe_deriv, hc, algebraMap.coe_zero]
        apply hc₀

Goal state after:
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
ih : (y : (Module.rank F E).ord.ToType) → y < i → (Module.rank F E).ord.ToType
s : Set E := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : Module.rank F ↥(adjoin F s) = Module.rank F ↥⊤
⊢ (#(Module.rank F E).ord.ToType).ord = Ordinal.type fun x1 x2 ↦ x1 < x2

Tactic:
by simp

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.ExtendRight

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
F : IntermediateField K L
M : Type u_3
inst✝⁷ : Field M
inst✝⁶ : Algebra K M
inst✝⁵ : Algebra L M
inst✝⁴ : IsScalarTower K L M
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra S ↥F
inst✝¹ : Algebra S M
inst✝ : IsScalarTower S (↥F) M
s : S
⊢ (algebraMap (↥F) L) ((algebraMap S ↥F) s) ∈ ↑F.toSubsemiring

Tactic:
by simp

Goal state after:
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
h : Function.Injective ⇑(frobenius R p)
x : R
⊢ (∃ n, x ^ p ^ n = 0) → x = 0

Tactic:
exact fun ⟨n, _⟩ ↦ h.iterate n (by rwa [← coe_iterateFrobenius, map_zero])

Goal state after:
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝² : CommSemiring K
inst✝¹ : CommSemiring L
inst✝ : CommSemiring M
i : K →+* L
j : K →+* M
f : L →+* M
p : ℕ
x : K
⊢ (RingHom.id K) x = x ^ p ^ 0

Tactic:
by simp

Goal state after:
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing K
inst✝⁵ : CommRing L
inst✝⁴ : CommRing M
i : K →+* L
j : K →+* M
p : ℕ
inst✝³ : ExpChar M p
inst✝² : ExpChar K p
inst✝¹ : PerfectRing M p
inst✝ : IsPRadical i p
x : L
n : ℕ
y : K
n' : ℕ := (Classical.choose ⋯).1
h' : i (Classical.choose ⋯).2 = x ^ p ^ n'
h : (x ^ p ^ n) ^ p ^ n' = i y ^ p ^ n'
⊢ (iterateFrobeniusEquiv M p n').symm (j (Classical.choose ⋯).2) = (iterateFrobeniusEquiv M p n).symm (j y)

Tactic:
rw [← pow_mul, mul_comm, pow_mul, ← h', ← map_pow, ← map_pow, ← sub_eq_zero, ← map_sub,
    ← RingHom.mem_ker] at h

Goal state after:
K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing K
inst✝⁵ : CommRing L
inst✝⁴ : CommRing M
i : K →+* L
j : K →+* M
p : ℕ
inst✝³ : ExpChar M p
inst✝² : ExpChar K p
inst✝¹ : PerfectRing M p
inst✝ : IsPRadical i p
x : L
n : ℕ
y : K
n' : ℕ := (Classical.choose ⋯).1
h' : i (Classical.choose ⋯).2 = x ^ p ^ n'
h : (Classical.choose ⋯).2 ^ p ^ n - y ^ p ^ n' ∈ RingHom.ker i
⊢ (iterateFrobeniusEquiv M p n').symm (j (Classical.choose ⋯).2) = (iterateFrobeniusEquiv M p n).symm (j y)
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
L : (FiniteGaloisIntermediateField k K)ᵒᵖ
⊢ ↑((algEquivToLimit k K) (limitToAlgEquiv g)) L = ↑g L

Tactic:
change (limitToAlgEquiv g).restrictNormal _ = _

Goal state after:
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
L : (FiniteGaloisIntermediateField k K)ᵒᵖ
⊢ (limitToAlgEquiv g).restrictNormal ↥(unop L).toIntermediateField = ↑g L
Module: Mathlib.FieldTheory.PerfectClosure

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

Tactic:
simp [Nat.cast_succ, ih, one_def]

Goal state after:
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic

Goal state before:
pp: A : ProfiniteGrp.{u}
a : ↑A.toProfinite.toTop
⊢ (Hom.hom (𝟙 A)) a = a

Tactic:
by simp

Goal state after:
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : CommRing K
inst✝¹⁰ : CommRing L
inst✝⁹ : CommRing M
inst✝⁸ : CommRing N
i : K →+* L
j : K →+* M
g : L →+* N
p : ℕ
inst✝⁷ : ExpChar M p
inst✝⁶ : ExpChar K p
inst✝⁵ : PerfectRing M p
inst✝⁴ : IsPRadical i p
inst✝³ : ExpChar L p
inst✝² : ExpChar N p
inst✝¹ : IsPRadical g p
inst✝ : IsPRadical (g.comp i) p
⊢ ((lift g (lift i j p) p).comp g).comp i = (lift (g.comp i) j p).comp (g.comp i)

Tactic:
lift_comp

Goal state after:
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: case mk.mk
K : Type u
inst✝⁵ : CommRing K
p : ℕ
inst✝⁴ : Fact (Nat.Prime p)
inst✝³ : CharP K p
L : Type v
inst✝² : CommSemiring L
inst✝¹ : CharP L p
inst✝ : PerfectRing L p
f : K →+* L
x✝ : PerfectClosure K p
n : ℕ
x : K
y✝ : PerfectClosure K p
m : ℕ
y : K
⊢ (Quot.mk (R K p) (n, x) + Quot.mk (R K p) (m, y)).liftOn (fun x ↦ (⇑(frobeniusEquiv L p).symm)^[x.1] (f x.2)) ⋯ =
    liftOn (Quot.mk (R K p) (n, x)) (fun x ↦ (⇑(frobeniusEquiv L p).symm)^[x.1] (f x.2)) ⋯ +
      liftOn (Quot.mk (R K p) (m, y)) (fun x ↦ (⇑(frobeniusEquiv L p).symm)^[x.1] (f x.2)) ⋯

Tactic:
simp only [quot_mk_eq_mk, liftOn_mk, f.map_iterate_frobenius, mk_add_mk, map_add,
          iterate_map_add]

Goal state after:
case mk.mk
K : Type u
inst✝⁵ : CommRing K
p : ℕ
inst✝⁴ : Fact (Nat.Prime p)
inst✝³ : CharP K p
L : Type v
inst✝² : CommSemiring L
inst✝¹ : CharP L p
inst✝ : PerfectRing L p
f : K →+* L
x✝ : PerfectClosure K p
n : ℕ
x : K
y✝ : PerfectClosure K p
m : ℕ
y : K
⊢ (⇑(frobeniusEquiv L p).symm)^[n + m] ((⇑(frobenius L p))^[m] (f x)) +
      (⇑(frobeniusEquiv L p).symm)^[n + m] ((⇑(frobenius L p))^[n] (f y)) =
    (⇑(frobeniusEquiv L p).symm)^[n] (f x) + (⇑(frobeniusEquiv L p).symm)^[m] (f y)
Module: Mathlib.FieldTheory.Laurent

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
r : R
inst✝ : IsDomain R
⊢ (laurent r) X = X + C r

Tactic:
by
  rw [← algebraMap_X, laurent_algebraMap, taylor_X, map_add, algebraMap_C]

Goal state after:
Module: Mathlib.FieldTheory.JacobsonNoether

Goal state before:
pp: D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
H : k ≠ ⊤
p : ℕ
hp : ExpChar D p
insep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
a : D
ha : a ∉ k
ha₀ : a ≠ 0
b : D
hb1 : ((ad (↥k) D) a) b ≠ 0
m : ℕ
hm2 : ∀ (n : ℕ), p ^ m ≤ n → (⇑((ad (↥k) D) a))^[n] = 0
h_exist : ∃ n, 0 < n ∧ (⇑((ad (↥k) D) a))^[n + 1] b = 0
t : ℕ := Nat.find h_exist - 1
ht : t = Nat.find h_exist - 1
h_pos : t ≤ 0
h_find : Nat.find h_exist = 1
⊢ (⇑((ad (↥k) D) a))^[Nat.find h_exist] b ≠ 0

Tactic:
rwa [h_find]

Goal state after:
Module: Mathlib.FieldTheory.JacobsonNoether

Goal state before:
pp: D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
H : k ≠ ⊤
p : ℕ
hp : ExpChar D p
insep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
a : D
ha : a ∉ k
ha₀ : a ≠ 0
b : D
hb1 : ((ad (↥k) D) a) b ≠ 0
m : ℕ
hm2 : ∀ (n : ℕ), p ^ m ≤ n → (⇑((ad (↥k) D) a))^[n] = 0
h_exist : ∃ n, 0 < n ∧ (⇑((ad (↥k) D) a))^[n + 1] b = 0
⊢ ∃ n, 0 < n ∧ (⇑((ad (↥k) D) a))^[n] b ≠ 0 ∧ (⇑((ad (↥k) D) a))^[n + 1] b = 0

Tactic:
classical
    refine ⟨Nat.find h_exist, ⟨(Nat.find_spec h_exist).1, ?_, (Nat.find_spec h_exist).2⟩⟩
    set t := (Nat.find h_exist - 1 : ℕ) with ht
    by_cases! h_pos : 0 < t
    · convert! (ne_eq _ _) ▸ not_and.mp (Nat.find_min h_exist (m := t) (by lia)) h_pos
      lia
    · suffices h_find : Nat.find h_exist = 1 by
        rwa [h_find]
      rw [Nat.le_zero, ht, Nat.sub_eq_zero_iff_le] at h_pos
      linarith [(Nat.find_spec h_exist).1]

Goal state after:
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
inst✝ : DecidablePred FiniteIndex
D : Subgroup G := ⨅ k ∈ {i ∈ s | (H i).FiniteIndex}, H k
⊢ ∀ i ∈ {i ∈ s | (H i).FiniteIndex}, (H i).FiniteIndex

Tactic:
by simp

Goal state after:
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
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
⊢ #↑↑A + #↑↑B = max #↥A #↥B

Tactic:
by simp

Goal state after: