mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
S : WSeq (WSeq α)
⊢ Computation.IsBisimulation fun c1 c2 ↦ c1 = c2 ∨ ∃ S, c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux

Tactic:
intro c1 c2 h

Goal state after:
α : Type u
S : WSeq (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ S, c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux
⊢ BisimO (fun c1 c2 ↦ c1 = c2 ∨ ∃ S, c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux) c1.destruct
    c2.destruct
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: α : Type u
β : Type v
f : α → β
S : WSeq (Computation α)
⊢ IsBisimulation fun c1 c2 ↦
    ∃ l S, c1 = map f (corec parallel.aux1 (l, S)) ∧ c2 = corec parallel.aux1 (List.map (map f) l, WSeq.map (map f) S)

Tactic:
intro c1 c2 h

Goal state after:
α : Type u
β : Type v
f : α → β
S : WSeq (Computation α)
c1 c2 : Computation β
h : ∃ l S, c1 = map f (corec parallel.aux1 (l, S)) ∧ c2 = corec parallel.aux1 (List.map (map f) l, WSeq.map (map f) S)
⊢ BisimO
    (fun c1 c2 ↦
      ∃ l S,
        c1 = map f (corec parallel.aux1 (l, S)) ∧ c2 = corec parallel.aux1 (List.map (map f) l, WSeq.map (map f) S))
    c1.destruct c2.destruct
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
SS : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
⊢ ∀ {ca cb : Computation (Option (α × WSeq α))},
    (∃ s S SS,
        ca = (s.append (S.append SS.join).join).destruct ∧
          cb = (s.append (S.join.append (map join SS).join)).destruct) →
      LiftRelAux
        (LiftRelO Eq fun s1 s2 ↦
          ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join))
        (fun c1 c2 ↦
          ∃ s S SS,
            c1 = (s.append (S.append SS.join).join).destruct ∧
              c2 = (s.append (S.join.append (map join SS).join)).destruct)
        ca.destruct cb.destruct

Tactic:
intro c1 c2 h

Goal state after:
α : Type u
SS : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h✝ : ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
c1 c2 : Computation (Option (α × WSeq α))
h :
  ∃ s S SS,
    c1 = (s.append (S.append SS.join).join).destruct ∧ c2 = (s.append (S.join.append (map join SS).join)).destruct
⊢ LiftRelAux
    (LiftRelO Eq fun s1 s2 ↦
      ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join))
    (fun c1 c2 ↦
      ∃ s S SS,
        c1 = (s.append (S.append SS.join).join).destruct ∧ c2 = (s.append (S.join.append (map join SS).join)).destruct)
    c1.destruct c2.destruct
Module: Mathlib.Data.Vector.Zip

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
x : Vector α n
y : Vector β n
⊢ (zipWith f x y).tail = zipWith f x.tail y.tail

Tactic:
ext
  simp [get_tail]

Goal state after:
Module: Mathlib.Data.Vector3

Goal state before:
pp: α : Type u_1
n : ℕ
a b : α
v : Vector3 α n
i : Fin2 (n + 1)
j : Fin2 (n + 1 + 1)
⊢ insert a (b :: v) i.fs j = (b :: insert a v i) j

Tactic:
by
    refine j.cases' (by simp [insert, insertPerm]) fun j => ?_
    simp only [insert, insertPerm, succ_eq_add_one, cons_fs]
    refine Fin2.cases' ?_ ?_ (insertPerm i j) <;> simp

Goal state after:
Module: Mathlib.Data.Vector3

Goal state before:
pp: α : Type u_1
n✝ : ℕ
p : α → Prop
v✝ : Vector3 α n✝
n : ℕ
a : α
v : Vector3 α n
IH : VectorAllP p v ↔ ∀ (i : Fin2 n), p (v i)
x✝ : p a ∧ ∀ (i : Fin2 n), p (v i)
i : Fin2 (n + 1)
pa : p a
h : ∀ (i : Fin2 n), p (v i)
⊢ p ((a :: v) i)

Tactic:
refine i.cases' ?_ ?_
          exacts [pa, h]

Goal state after:
Module: Mathlib.Dynamics.SymbolicDynamics.Basic

Goal state before:
pp: A : Type u_3
G : Type u_4
inst✝¹ : Inhabited A
inst✝ : Monoid G
p : Pattern A G
x : G → A
g h : G
⊢ p.mulOccursInAt (mulShift g x) h ↔ p.mulOccursInAt x (g * h)

Tactic:
simp only [Pattern.mulOccursInAt, mulShift_apply, mul_assoc]

Goal state after:
Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage

Goal state before:
pp: X : Type u_1
T : X → X
U : SetRel X X
inst✝ : UniformSpace X
h : Continuous[inst✝.toTopologicalSpace, inst✝.toTopologicalSpace] T
U_uni : U ∈ 𝓤 X
n : ℕ
x : X
⊢ ⋂ i, ball x ((map T T)^[↑i] ⁻¹' U) ∈ 𝓝 x

Tactic:
Filter.iInter_mem,

Goal state after:
X : Type u_1
T : X → X
U : SetRel X X
inst✝ : UniformSpace X
h : Continuous[inst✝.toTopologicalSpace, inst✝.toTopologicalSpace] T
U_uni : U ∈ 𝓤 X
n : ℕ
x : X
⊢ ∀ (i : ↑(Ico 0 n)), ball x ((map T T)^[↑i] ⁻¹' U) ∈ 𝓝 x
Module: Mathlib.Dynamics.SymbolicDynamics.Basic

Goal state before:
pp: A : Type u_1
inst✝⁴ : TopologicalSpace A
inst✝³ : Inhabited A
G : Type u_2
inst✝² : Monoid G
inst✝¹ : IsLeftCancelMul G
inst✝ : DiscreteTopology A
F : Set (Pattern A G)
h_eq : {x | ∀ p ∈ F, ∀ (v : G), ¬p.mulOccursInAt x v} = ⋂ p ∈ F, ⋂ v, {x | ¬p.mulOccursInAt x v}
p : Pattern A G
hp : p ∈ F
v : G
⊢ IsClosed[Pi.topologicalSpace] {x | ¬p.mulOccursInAt x v}

Tactic:
have : {x | ¬ p.mulOccursInAt x v} = {x | p.mulOccursInAt x v}ᶜ := by ext; simp

Goal state after:
A : Type u_1
inst✝⁴ : TopologicalSpace A
inst✝³ : Inhabited A
G : Type u_2
inst✝² : Monoid G
inst✝¹ : IsLeftCancelMul G
inst✝ : DiscreteTopology A
F : Set (Pattern A G)
h_eq : {x | ∀ p ∈ F, ∀ (v : G), ¬p.mulOccursInAt x v} = ⋂ p ∈ F, ⋂ v, {x | ¬p.mulOccursInAt x v}
p : Pattern A G
hp : p ∈ F
v : G
this : {x | ¬p.mulOccursInAt x v} = {x | p.mulOccursInAt x v}ᶜ
⊢ IsClosed[Pi.topologicalSpace] {x | ¬p.mulOccursInAt x v}
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
pp: X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
⊢ netMaxcard T F U n < ⊤ ↔ ∃ s, IsDynNetIn T F U n ↑s ∧ ↑s.card = netMaxcard T F U n

Tactic:
apply Iff.intro <;> intro h

Goal state after:
case mp
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : netMaxcard T F U n < ⊤
⊢ ∃ s, IsDynNetIn T F U n ↑s ∧ ↑s.card = netMaxcard T F U n

case mpr
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : ∃ s, IsDynNetIn T F U n ↑s ∧ ↑s.card = netMaxcard T F U n
⊢ netMaxcard T F U n < ⊤
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
pp: X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
⊢ netMaxcard T F U n = 0 ↔ F = ∅

Tactic:
by
  refine ⟨fun h ↦ ?_, fun h ↦ by rw [h, netMaxcard_empty]⟩
  rw [eq_empty_iff_forall_notMem]
  intro x x_F
  have key := isDynNetIn_singleton T U n x_F
  rw [← Finset.coe_singleton] at key
  replace key := key.card_le_netMaxcard
  rw [Finset.card_singleton, Nat.cast_one, h] at key
  exact key.not_gt zero_lt_one

Goal state after:
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
pp: X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
⊢ netMaxcard T F U n = ⊤ ↔ ∀ (k : ℕ), ∃ s, IsDynNetIn T F U n ↑s ∧ k ≤ s.card

Tactic:
apply Iff.intro <;> intro h

Goal state after:
case mp
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : netMaxcard T F U n = ⊤
⊢ ∀ (k : ℕ), ∃ s, IsDynNetIn T F U n ↑s ∧ k ≤ s.card

case mpr
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : ∀ (k : ℕ), ∃ s, IsDynNetIn T F U n ↑s ∧ k ≤ s.card
⊢ netMaxcard T F U n = ⊤
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: case inr.inl
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
F_inv : MapsTo T F F
inst✝ : U.IsSymm
m : ℕ
F_nonempty : F.Nonempty
⊢ coverMincard T F (U ○ U) (m * 0) ≤ coverMincard T F U m ^ 0

Tactic:
rw [mul_zero, coverMincard_zero T F_nonempty (U ○ U), pow_zero]

Goal state after:
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
pp: case h'
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
⊢ (fun n ↦ ↑(netMaxcard T F U n)) ≠ 0

Tactic:
rw [ne_eq, funext_iff.not, not_forall]
    use 0
    rw [netMaxcard_zero T h U, Pi.zero_apply, ENat.toENNReal_one]
    exact one_ne_zero

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hμν : μ ≤ ν
inst✝ : SigmaFinite ν
⊢ μ.rnDeriv ν ≤ᵐ[ν] 1

Tactic:
refine ae_le_of_forall_setLIntegral_le_of_sigmaFinite (μ.measurable_rnDeriv ν) fun s _ _ ↦ ?_

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hμν : μ ≤ ν
inst✝ : SigmaFinite ν
s : Set α
x✝¹ : MeasurableSet s
x✝ : ν s < ∞
⊢ ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν ≤ ∫⁻ (x : α) in s, 1 x ∂ν
Module: Mathlib.Dynamics.TopologicalEntropy.Subset

Goal state before:
pp: X : Type u_1
T : X → X
F s : Set X
U V : SetRel X X
n : ℕ
inst✝ : UniformSpace X
h : Continuous T
V_uni : V ∈ 𝓤 X
s_cover : IsDynCoverOf T F U n s
W : SetRel X X
W_V : id W ⊆ V
W_uni : W ∈ 𝓤 X
W_symm : W.IsSymm
⊢ IsDynCoverOf T (_root_.closure F) (V ○ U) n s

Tactic:
refine IsDynCoverOf.of_entourage_subset (SetRel.comp_subset_comp_left W_V) fun x hx ↦ ?_

Goal state after:
X : Type u_1
T : X → X
F s : Set X
U V : SetRel X X
n : ℕ
inst✝ : UniformSpace X
h : Continuous T
V_uni : V ∈ 𝓤 X
s_cover : IsDynCoverOf T F U n s
W : SetRel X X
W_V : id W ⊆ V
W_uni : W ∈ 𝓤 X
W_symm : W.IsSymm
x : X
hx : x ∈ _root_.closure F
⊢ ∃ y ∈ s, (x, y) ∈ dynEntourage T (id W ○ U) n
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃[L] N
⊢ f.symm.comp f = refl L M

Tactic:
by
  ext; rw [comp_apply, symm_apply_apply, refl_apply]

Goal state after:
Module: Mathlib.ModelTheory.Algebra.Ring.Basic

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝⁵ : Add R
inst✝⁴ : Mul R
inst✝³ : Neg R
inst✝² : One R
inst✝¹ : Zero R
inst✝ : CompatibleRing R
x : ring.Term α
v : α → R
⊢ Term.realize v (-x) = -Term.realize v x

Tactic:
by
  simp [neg_def, funMap_neg]

Goal state after:
Module: Mathlib.ModelTheory.Syntax

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

Tactic:
· obtain - | f := f
        · simp [constantsToVars, varsToConstants, ih]
        · exact isEmptyElim f

Goal state after:
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case func
L : Language
α : Type u'
l✝ : List (L.Term α)
n : ℕ
f : L.Functions n
ts : Fin n → L.Term α
ih : ∀ (a : Fin n) (l : List (α ⊕ (i : ℕ) × L.Functions i)), listDecode ((ts a).listEncode ++ l) = ts a :: listDecode l
l : List (α ⊕ (i : ℕ) × L.Functions i)
⊢ (if h : n ≤ (listDecode (flatMap (fun i ↦ (ts i).listEncode) (finRange n) ++ l)).length then
      (func f fun i ↦ (listDecode (flatMap (fun i ↦ (ts i).listEncode) (finRange n) ++ l))[i]) ::
        drop n (listDecode (flatMap (fun i ↦ (ts i).listEncode) (finRange n) ++ l))
    else []) =
    func f ts :: listDecode l

Tactic:
have h : listDecode (((finRange n).flatMap fun i : Fin n => (ts i).listEncode) ++ l) =
        (finRange n).map ts ++ listDecode l := by
      induction finRange n with
      | nil => rfl
      | cons i l' l'ih => rw [flatMap_cons, List.append_assoc, ih, map_cons, l'ih, cons_append]

Goal state after:
case func
L : Language
α : Type u'
l✝ : List (L.Term α)
n : ℕ
f : L.Functions n
ts : Fin n → L.Term α
ih : ∀ (a : Fin n) (l : List (α ⊕ (i : ℕ) × L.Functions i)), listDecode ((ts a).listEncode ++ l) = ts a :: listDecode l
l : List (α ⊕ (i : ℕ) × L.Functions i)
h : listDecode (flatMap (fun i ↦ (ts i).listEncode) (finRange n) ++ l) = List.map ts (finRange n) ++ listDecode l
⊢ (if h : n ≤ (listDecode (flatMap (fun i ↦ (ts i).listEncode) (finRange n) ++ l)).length then
      (func f fun i ↦ (listDecode (flatMap (fun i ↦ (ts i).listEncode) (finRange n) ++ l))[i]) ::
        drop n (listDecode (flatMap (fun i ↦ (ts i).listEncode) (finRange n) ++ l))
    else []) =
    func f ts :: listDecode l
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
n : ℕ
φ : L.BoundedFormula α n
f : ↥φ.freeVarFinset → β
v : β → M
xs : Fin n → M
v' : α → M
hv' : ∀ (a : ↥φ.freeVarFinset), v (f a) = v' ↑a
⊢ (φ.restrictFreeVar f).Realize v xs ↔ φ.Realize v' xs

Tactic:
by
  induction φ with
  | falsum => rfl
  | equal =>
    simp only [Realize, restrictFreeVar]
    rw [realize_restrictVarLeft v' (by simp [hv']), realize_restrictVarLeft v' (by simp [hv'])]
    simp
  | rel =>
    simp only [Realize, restrictFreeVar]
    congr!
    rw [realize_restrictVarLeft v' (by simp [hv'])]
    simp
  | imp _ _ ih1 ih2 =>
    simp only [Realize, restrictFreeVar]
    rw [ih1, ih2] <;> simp [hv']
  | all _ ih3 =>
    simp only [restrictFreeVar, Realize]
    refine forall_congr' (fun _ => ?_)
    rw [ih3]; simp [hv']

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type u_1
L : Language
inst✝ : L.Structure M
α : Type u_2
f : (α → M) → M
⊢ DefinableFun L ∅ f ↔ ∃ φ, tupleGraph f = ofPred φ.Realize

Tactic:
by
  simp [DefinableFun, Set.empty_definable_iff]

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
h : T.IsFinitelySatisfiable
M : Finset ↑T → Type (max u v) := fun T0 ↦ ↑(Nonempty.some ⋯)
M' : Type (max u v) := (↑(Ultrafilter.of Filter.atTop)).Product M
φ : L.Sentence
hφ : φ ∈ T
s : Finset ↑T
h' : {⟨φ, hφ⟩} ⊆ s
⊢ φ ∈ ↑(Finset.map (Function.Embedding.subtype fun x ↦ x ∈ T) s)

Tactic:
simp only [Finset.coe_map, Function.Embedding.coe_subtype, Set.mem_image, Finset.mem_coe,
        Subtype.exists, exists_and_right, exists_eq_right]

Goal state after:
L : Language
T : L.Theory
h : T.IsFinitelySatisfiable
M : Finset ↑T → Type (max u v) := fun T0 ↦ ↑(Nonempty.some ⋯)
M' : Type (max u v) := (↑(Ultrafilter.of Filter.atTop)).Product M
φ : L.Sentence
hφ : φ ∈ T
s : Finset ↑T
h' : {⟨φ, hφ⟩} ⊆ s
⊢ ∃ (x : φ ∈ T), ⟨φ, ⋯⟩ ∈ s
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type u_1
L : Language
inst✝ : L.Structure M
α : Type u_2
A : Set M
f g : (α → M) → M
hf : DefinableFun L A f
hg : DefinableFun L A g
hF : DefinableMap L A fun v ↦ ![f v, g v]
⊢ A.Definable L {v | f v = g v}

Tactic:
exact (Definable.diagonal L A).preimage_map hF

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

Goal state before:
pp: p✝ : ℕ
K : Type u_2
inst✝¹ : Field K
inst✝ : CompatibleRing K
h : K ⊨ Theory.ACF p✝
p : K[X]
hpm : p.Monic
hpi : Irreducible p
⊢ genericMonicPolyHasRoot '' {n | 0 < n} ⊆ Theory.ACF p✝

Tactic:
simp [Theory.ACF]

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

Goal state before:
pp: case inr
x✝ : CompatibleRing (AlgebraicClosure ℚ) := compatibleRingOfRing (AlgebraicClosure ℚ)
⊢ (Theory.ACF 0).IsSatisfiable

Tactic:
exact ⟨⟨AlgebraicClosure ℚ⟩⟩

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

Goal state before:
pp: case neg
a : ℕ
h : ¬ℵ₀ ≤ ↑a
p : Cardinal.{u_1}
k : ℕ
hp : Prime p
hk : 0 < k
hpk : p ^ k = ↑a
key : p ^ 1 ≤ ↑a
⊢ ∃ n, ↑a = ↑n ∧ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n

Tactic:
power_one

Goal state after:
case neg
a : ℕ
h : ¬ℵ₀ ≤ ↑a
p : Cardinal.{u_1}
k : ℕ
hp : Prime p
hk : 0 < k
hpk : p ^ k = ↑a
key : p ≤ ↑a
⊢ ∃ n, ↑a = ↑n ∧ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
Module: Mathlib.FieldTheory.FinTrdeg

Goal state before:
pp: case mp
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E : IntermediateField K L
alg : Algebra.IsAlgebraic (↥E) L
S₀ : Subalgebra K ↥E
M : Submonoid ↥S₀
fin : Algebra.FiniteType K ↥S₀
islocal : IsLocalization M ↥E
⊢ Algebra.trdeg K ↥S₀ + Algebra.trdeg ↥S₀ ↥E < Cardinal.aleph0

Tactic:
trdeg_eq_zero_iff.2 islocal.isAlgebraic,

Goal state after:
case mp
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E : IntermediateField K L
alg : Algebra.IsAlgebraic (↥E) L
S₀ : Subalgebra K ↥E
M : Submonoid ↥S₀
fin : Algebra.FiniteType K ↥S₀
islocal : IsLocalization M ↥E
⊢ Algebra.trdeg K ↥S₀ + 0 < Cardinal.aleph0
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
a : ↥(F.extendRight M)
⊢ (algebraMap (↥F) M) ((F.extendRightEquiv M).symm a) = ↑a

Tactic:
by
  rw [← algebraMap_extendRightEquiv, AlgEquiv.apply_symm_apply, algebraMap_apply]

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
inst✝ : Algebra.IsAlgebraic F E
⊢ #(Emb F E) = (fun c ↦ if ℵ₀ ≤ c then 2 ^ c else c) (sepDegree F E)

Tactic:
by
  rw [← cardinal_separableClosure, cardinal_eq_of_isSeparable]; rfl

Goal state after:
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring K
inst✝³ : CommSemiring L
inst✝² : CommSemiring M
i : K →+* L
f : L →+* M
p : ℕ
inst✝¹ : IsPRadical i p
inst✝ : IsPRadical f p
x : K
h : x ∈ RingHom.ker (f.comp i)
⊢ x ∈ pNilradical K p

Tactic:
RingHom.mem_ker,

Goal state after:
K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring K
inst✝³ : CommSemiring L
inst✝² : CommSemiring M
i : K →+* L
f : L →+* M
p : ℕ
inst✝¹ : IsPRadical i p
inst✝ : IsPRadical f p
x : K
h : (f.comp i) x = 0
⊢ x ∈ pNilradical K p
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
e f g : PerfectClosure K p
x✝² : ℕ × K
m : ℕ
x : K
x✝¹ : ℕ × K
n : ℕ
y : K
x✝ : ℕ × K
s : ℕ
z : K
⊢ (⇑(frobenius K p))^[m]
      ((⇑(frobenius K p))^[n + s] x * (⇑(frobenius K p))^[m] ((⇑(frobenius K p))^[n] z + (⇑(frobenius K p))^[s] y)) =
    (⇑(frobenius K p))^[m + n] ((⇑(frobenius K p))^[s] x * (⇑(frobenius K p))^[m] z) +
      (⇑(frobenius K p))^[m + s] ((⇑(frobenius K p))^[n] x * (⇑(frobenius K p))^[m] y)

Tactic:
simp only [iterate_map_mul, iterate_map_add, ← iterate_add_apply,
              mul_add, add_comm, add_left_comm]

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

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

Tactic:
by
    simp only [toAlgEquivAux_eq_liftNormal g _ ⊥ (algebraMap_mem _ x), AlgEquiv.commutes]

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 ↔ ↑x = 0

Tactic:
rw [← Nat.cast_zero, natCast_eq_iff, Nat.cast_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✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : K
h : x ∈ RingHom.ker (of K p)
⊢ x ∈ pNilradical K p

Tactic:
RingHom.mem_ker,

Goal state after:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : K
h : (of K p) x = 0
⊢ x ∈ pNilradical K p
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
⊢ (⇑(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)

Tactic:
have := LeftInverse.iterate (frobeniusEquiv_symm_apply_frobenius L p)

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
this : ∀ (n : ℕ), LeftInverse (⇑(frobeniusEquiv L p).symm)^[n] (⇑(frobenius L p))^[n]
⊢ (⇑(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.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
⊢ (⇑(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)

Tactic:
have := LeftInverse.iterate (frobeniusEquiv_symm_apply_frobenius L p)

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
this : ∀ (n : ℕ), LeftInverse (⇑(frobeniusEquiv L p).symm)^[n] (⇑(frobenius L p))^[n]
⊢ (⇑(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.GroupTheory.CosetCover

Goal state before:
pp: G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : ⋃ i ∈ s, g i • ↑H = Set.univ
hind : H.index = s.card
this✝ : Fintype (G ⧸ H)
this : Function.Bijective fun x ↦ ↑(g ↑x)
i : ι
hi : i ∈ ↑s
j : ι
hj : j ∈ ↑s
h' : i ≠ j
⊢ Function.onFun Disjoint (fun x ↦ g x • ↑H) i j

Tactic:
c

Goal state after:
G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : ⋃ i ∈ s, g i • ↑H = Set.univ
hind : H.index = s.card
this✝ : Fintype (G ⧸ H)
this : Function.Bijective fun x ↦ ↑(g ↑x)
i : ι
hi : i ∈ ↑s
j : ι
hj : j ∈ ↑s
h' : i ≠ j
c : Set G
⊢ c ⊆ (fun x ↦ g x • ↑H) i → c ⊆ (fun x ↦ g x • ↑H) j → c ⊆ ⊥
Module: Mathlib.FieldTheory.Laurent

Goal state before:
pp: case f
R : Type u
inst✝¹ : CommRing R
r s : R
f : R⟮X⟯
inst✝ : IsDomain R
p✝ q✝ : R[X]
x✝ : q✝ ≠ 0
⊢ (laurent r) ((laurent s) ((algebraMap R[X] R⟮X⟯) p✝ / (algebraMap R[X] R⟮X⟯) q✝)) =
    (laurent (r + s)) ((algebraMap R[X] R⟮X⟯) p✝ / (algebraMap R[X] R⟮X⟯) q✝)

Tactic:
laurent_div,

Goal state after:
case f
R : Type u
inst✝¹ : CommRing R
r s : R
f : R⟮X⟯
inst✝ : IsDomain R
p✝ q✝ : R[X]
x✝ : q✝ ≠ 0
⊢ (algebraMap R[X] R⟮X⟯) ((taylor r) ((taylor s) p✝)) / (algebraMap R[X] R⟮X⟯) ((taylor r) ((taylor s) q✝)) =
    (algebraMap R[X] R⟮X⟯) ((taylor (r + s)) p✝) / (algebraMap R[X] R⟮X⟯) ((taylor (r + s)) q✝)
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: case splits'
K : Type u
inst✝ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
this✝ : Fact (Irreducible (X ^ n - C a))
this : Algebra K K[n√a] := inferInstance
⊢ (Polynomial.map (algebraMap K K[n√a]) X ^ n - C ((algebraMap K K[n√a]) a)).Splits

Tactic:
Polynomial.map_X

Goal state after:
case splits'
K : Type u
inst✝ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
this✝ : Fact (Irreducible (X ^ n - C a))
this : Algebra K K[n√a] := inferInstance
⊢ (X ^ n - C ((algebraMap K K[n√a]) a)).Splits