mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
s : Set α
hs : MeasurableSet s
⊢ (∫⁻ (a : α) in s, μ.rnDeriv ν a ∂ν).toReal = ((ν.withDensity (μ.rnDeriv ν)) s).toReal

Tactic:
rw [ENNReal.toReal_eq_toReal_iff, ← withDensity_apply _ hs]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
s : Set α
hs : MeasurableSet s
⊢ (ν.withDensity (μ.rnDeriv ν)) s = (ν.withDensity (μ.rnDeriv ν)) s ∨
    (ν.withDensity (μ.rnDeriv ν)) s = 0 ∧ (ν.withDensity (μ.rnDeriv ν)) s = ∞ ∨
      (ν.withDensity (μ.rnDeriv ν)) s = ∞ ∧ (ν.withDensity (μ.rnDeriv ν)) s = 0
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: X : Type u_1
T : X → X
U : SetRel X X
F : Set X
n : ℕ
inst✝ : U.IsSymm
s : Finset X
h' : ↑(#s) = coverMincard T F U n
x : X
x_s : x ∈ s
ball_empt : F ∩ ball x (dynEntourage T U n) = ∅
y : X
y_F : y ∈ F
z : X
z_s : z ∈ s
hz : (y, z) ∈ dynEntourage T U n
⊢ ∃ y_1, (y_1 ∈ s ∧ ¬y_1 = x) ∧ (y, y_1) ∈ dynEntourage T U n

Tactic:
refine ⟨z, ⟨z_s, fun z_x ↦ notMem_empty y ?_⟩, hz⟩

Goal state after:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
n : ℕ
inst✝ : U.IsSymm
s : Finset X
h' : ↑(#s) = coverMincard T F U n
x : X
x_s : x ∈ s
ball_empt : F ∩ ball x (dynEntourage T U n) = ∅
y : X
y_F : y ∈ F
z : X
z_s : z ∈ s
hz : (y, z) ∈ dynEntourage T U n
z_x : z = x
⊢ y ∈ ∅
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case pos
F : Type u_1
inst✝ : Field F
n : ℕ
hn : n = 0
⊢ Group.IsSolvable (X ^ n - 1).Gal

Tactic:
rw [hn, pow_zero, sub_self]

Goal state after:
case pos
F : Type u_1
inst✝ : Field F
n : ℕ
hn : n = 0
⊢ Group.IsSolvable (Gal 0)
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case pos
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : (map i (X ^ n - C a)).Splits
ha' : i a ≠ 0
hn : n = 0
⊢ (map i (X ^ n - 1)).Splits

pp: case neg
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : (map i (X ^ n - C a)).Splits
ha' : i a ≠ 0
hn : ¬n = 0
⊢ (map i (X ^ n - 1)).Splits

Tactic:
· simp [hn]

Goal state after:
case neg
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : (map i (X ^ n - C a)).Splits
ha' : i a ≠ 0
hn : ¬n = 0
⊢ (map i (X ^ n - 1)).Splits
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case neg.hq
F : Type u_1
inst✝ : Field F
n : ℕ
x : F
hx : ¬x = 0
key : (X ^ n - map (algebraMap F (X ^ n - 1).SplittingField) 1).Splits
⊢ (X ^ n - 1).Splits

Tactic:
Polynomial.map_one

Goal state after:
case neg.hq
F : Type u_1
inst✝ : Field F
n : ℕ
x : F
hx : ¬x = 0
key : (X ^ n - 1).Splits
⊢ (X ^ n - 1).Splits
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case var
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
x : γ ⊕ α
⊢ (var x).varsToConstants.constantsToVars = var x

Tactic:
| var x =>

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

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

Tactic:
| addAssoc =>

Goal state after:
Module: Mathlib.ModelTheory.Ultraproducts

Goal state before:
pp: case refine_1
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝ : (a : α) → L.Structure (M a)
n : ℕ
r : L.Relations n
x y : Fin n → (a : α) → M a
xy : x ≈ y
hx : RelMap r x
⊢ RelMap r y

Tactic:
refine mem_of_superset (inter_mem hx (iInter_mem.2 xy)) ?_

Goal state after:
case refine_1
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝ : (a : α) → L.Structure (M a)
n : ℕ
r : L.Relations n
x y : Fin n → (a : α) → M a
xy : x ≈ y
hx : RelMap r x
⊢ {x_1 | (fun a ↦ RelMap r fun i ↦ x i a) x_1} ∩ ⋂ i, {x_1 | (fun a ↦ x i a = y i a) x_1} ⊆
    {x | (fun a ↦ RelMap r fun i ↦ y i a) x}
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:
induction t generalizing l with
  | var => rw [listEncode, singleton_append, listDecode]
  | @func n f ts ih =>
    rw [listEncode, cons_append, listDecode]
    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]
    simp only [h, length_append, length_map, length_finRange, le_add_iff_nonneg_right,
      _root_.zero_le, ↓reduceDIte, getElem_fin, cons.injEq, func.injEq, heq_eq_eq, true_and]
    refine ⟨funext (fun i => ?_), ?_⟩
    · simp only [length_map, length_finRange, is_lt, getElem_append_left, getElem_map,
      getElem_finRange, cast_mk, Fin.eta]
    · simp only [length_map, length_finRange, drop_left']

Goal state after:
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
p : M → Prop
x : M
s : Set M
hs : (closure L).toFun s = ⊤
Hs : ∀ x ∈ s, p x
Hfun : ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f (ofPred p)
⊢ p x

Tactic:
by
  have : ∀ x ∈ closure L s, p x := fun x hx => closure_induction hx Hs fun {n} => Hfun
  simpa [hs] using this x

Goal state after:
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 : (α → M) → M
p : (α → M) → Prop
g : (α → M) → M
inst✝ : DecidablePred p
hp : A.Definable L (ofPred p)
hf : DefinableFun L A f
hg : DefinableFun L A g
⊢ DefinableFun L A fun v ↦ if p v then f v else g v

Tactic:
by
  let P : Set (Option α → M) := {w | p (w ∘ some)}
  have hP : A.Definable L P := hp.preimage_comp some
  simp only [DefinableFun]
  convert! (hP.inter hf).union (hP.compl.inter hg)
  ext w
  by_cases h : p (w ∘ some) <;> simp [tupleGraph, P, h]

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: case inr
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 ⊨ φ
hT : T ⊨ᵇ Formula.not φ
this : M ⊨ ∼φ
⊢ T ⊨ᵇ φ

Tactic:
Sentence.realize_not

Goal state after:
case inr
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 ⊨ φ
hT : T ⊨ᵇ Formula.not φ
this : ¬M ⊨ φ
⊢ T ⊨ᵇ φ
Module: Mathlib.RingTheory.Nullstellensatz

Goal state before:
pp: k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Field K
inst✝² : Algebra k K
σ : Type u_3
inst✝¹ : IsAlgClosed K
inst✝ : Finite σ
I J : Ideal (MvPolynomial σ k)
hJI : I ≤ J
hJ : J.IsMaximal
x : σ → K
hx : J = vanishingIdeal k {x}
y : σ → K
hy : y ∈ {x}
p : MvPolynomial σ k
hp : p ∈ I
⊢ (aeval y) p = 0

Tactic:
← mem_vanishingIdeal_singleton_iff,

Goal state after:
k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Field K
inst✝² : Algebra k K
σ : Type u_3
inst✝¹ : IsAlgClosed K
inst✝ : Finite σ
I J : Ideal (MvPolynomial σ k)
hJI : I ≤ J
hJ : J.IsMaximal
x : σ → K
hx : J = vanishingIdeal k {x}
y : σ → K
hy : y ∈ {x}
p : MvPolynomial σ k
hp : p ∈ I
⊢ p ∈ vanishingIdeal k {y}
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
⊢ ∀ (x : F[X]),
    (AdjoinRoot.mk p).toIntAlgHom x = 0 →
      (AdjoinRoot.mk p).toIntAlgHom
          ((implicitDeriv
              ((AdjoinRoot.modByMonicHom ⋯)
                (-(aeval (AdjoinRoot.root p)) (mapCoeffs p) / (aeval (AdjoinRoot.root p)) (derivative p))))
            x) =
        0

Tactic:
by
      rintro x hx
      simp_all only [RingHom.toIntAlgHom_apply, AdjoinRoot.mk_eq_zero]
      obtain ⟨q, rfl⟩ := hx
      simp only [Derivation.leibniz, smul_eq_mul]
      apply dvd_add (dvd_mul_right ..)
      apply dvd_mul_of_dvd_right
      rw [← AdjoinRoot.mk_eq_zero]
      unfold implicitDeriv
      simp only [AdjoinRoot.aeval_eq, Derivation.coe_add, Derivation.coe_smul, Pi.add_apply,
        Pi.smul_apply, Derivation.restrictScalars_apply, derivative'_apply, smul_eq_mul, map_add,
        map_mul, AdjoinRoot.mk_leftInverse Fact.out _]
      rw [div_mul_cancel₀, add_neg_cancel]
      simp only [ne_eq, AdjoinRoot.mk_eq_zero]
      have : 0 < p.natDegree := Irreducible.natDegree_pos (Fact.out)
      apply not_dvd_of_natDegree_lt
      · intro nh
        simp_all
      apply natDegree_derivative_lt
      exact Nat.ne_zero_of_lt this

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

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

Tactic:
ne

Goal state after:
case refine_1
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
n b : σ
a✝ : b ∈ Finset.univ
ne : b ≠ n
⊢ (Fintype.card K - 1) * Multiset.count n {b} = 0
Module: Mathlib.FieldTheory.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
R : Type u_4
S : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra S ↥F
inst✝⁵ : Algebra S M
inst✝⁴ : IsScalarTower S (↥F) M
inst✝³ : Algebra R ↥F
inst✝² : Algebra R M
inst✝¹ : IsScalarTower R (↥F) M
inst✝ : IsIntegralClosure S R ↥F
⊢ IsIntegralClosure S R ↥(F.extendRight M)

Tactic:
refine .of_algEquiv S (F.extendRightEquiv' M R) fun x ↦ ?_

Goal state after:
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
R : Type u_4
S : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra S ↥F
inst✝⁵ : Algebra S M
inst✝⁴ : IsScalarTower S (↥F) M
inst✝³ : Algebra R ↥F
inst✝² : Algebra R M
inst✝¹ : IsScalarTower R (↥F) M
inst✝ : IsIntegralClosure S R ↥F
x : S
⊢ (algebraMap S ↥(F.extendRight M)) x = (F.extendRightEquiv' M R) ((algebraMap S ↥F) 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 : WithTop (Module.rank F E).ord.ToType
hi : IsSuccPrelimit i
f : ↑(limit (embFunctor F E) i)
j : ↑(Iio i)
this : Nonempty ↑(Iio i)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
dif_pos this

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 : WithTop (Module.rank F E).ord.ToType
hi : IsSuccPrelimit i
f : ↑(limit (embFunctor F E) i)
j : ↑(Iio i)
this : Nonempty ↑(Iio i)
⊢ embFunctor F E ⋯ (Subalgebra.iSupLift (fun x ↦ (filtration ↑x).toSubalgebra) ⋯ ↑f ⋯ (filtration i).toSubalgebra ⋯) =
    ↑f j
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
σ : Gal(K/k)
L₁ L₂ : (FiniteGaloisIntermediateField k K)ᵒᵖ
π : L₁ ⟶ L₂
⊢ (Hom.hom ((asProfiniteGaloisGroupFunctor k K).map π))
      ((fun L ↦ (AlgEquiv.restrictNormalHom ↥(unop L).toIntermediateField) σ) L₁) =
    (fun L ↦ (AlgEquiv.restrictNormalHom ↥(unop L).toIntermediateField) σ) L₂

Tactic:
algebraize [Subsemiring.inclusion π.1.le]

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
σ : Gal(K/k)
L₁ L₂ : (FiniteGaloisIntermediateField k K)ᵒᵖ
π : L₁ ⟶ L₂
algInst✝ : Algebra ↥(unop L₂).toSubsemiring ↥(unop L₁).toSubsemiring := (Subsemiring.inclusion ⋯).toAlgebra
⊢ (Hom.hom ((asProfiniteGaloisGroupFunctor k K).map π))
      ((fun L ↦ (AlgEquiv.restrictNormalHom ↥(unop L).toIntermediateField) σ) L₁) =
    (fun L ↦ (AlgEquiv.restrictNormalHom ↥(unop L).toIntermediateField) σ) L₂
Module: Mathlib.FieldTheory.CardinalEmb

Goal state before:
pp: case neg
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
h : ¬ℵ₀ ≤ Module.rank F E
⊢ #(Emb F E) = Module.rank F E

Tactic:
rw [not_le, ← IsNoetherian.iff_rank_lt_aleph0] at h

Goal state after:
case neg
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
h : IsNoetherian F E
⊢ #(Emb F E) = Module.rank F E
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)
⊢ ↑(((proj { toIntermediateField := L, finiteDimensional := finiteDimensional✝¹, isGalois := isGalois✝¹ }) g) x) =
    ↑(((proj { toIntermediateField := L', finiteDimensional := finiteDimensional✝, isGalois := isGalois✝ }) g) ⟨↑x, ⋯⟩)

Tactic:
rw [← finGaloisGroupFunctor_map_proj_eq_proj g h.hom]

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)
⊢ ↑(((ConcreteCategory.hom ((finGaloisGroupFunctor k K).map h.hom.op))
          ((proj { toIntermediateField := L', finiteDimensional := finiteDimensional✝, isGalois := isGalois✝ }) g))
        x) =
    ↑(((proj { toIntermediateField := L', finiteDimensional := finiteDimensional✝, isGalois := isGalois✝ }) g) ⟨↑x, ⋯⟩)
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 : ℕ × K
H : mk K p x = mk K p y
⊢ ∃ z, (⇑(frobenius K p))^[y.1 + z] x.2 = (⇑(frobenius K p))^[x.1 + z] y.2

Tactic:
replace H := Quot.eqvGen_exact H

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

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ ProfiniteGrp.{max v u}
cone : Limits.Cone F
m : cone.pt ⟶ (limitCone F).pt
h : ∀ (j : J), m ≫ (limitCone F).π.app j = cone.π.app j
⊢ m =
    ofHom
      (let __src :=
        TopCat.Hom.hom
          ((Profinite.limitConeIsLimit (F ⋙ forget₂ ProfiniteGrp.{max u v} Profinite)).lift
              ((forget₂ ProfiniteGrp.{max u v} Profinite).mapCone cone)).hom;
      { toFun := __src.toFun, map_one' := ⋯, map_mul' := ⋯, continuous_toFun := ⋯ })

Tactic:
by
    apply (forget₂ ProfiniteGrp Profinite).map_injective
    simpa using! (Profinite.limitConeIsLimit (F ⋙ (forget₂ ProfiniteGrp Profinite))).uniq
      ((forget₂ ProfiniteGrp Profinite).mapCone cone) ((forget₂ ProfiniteGrp Profinite).map m)
      (fun j ↦ congrArg (forget₂ ProfiniteGrp Profinite).map (h j))

Goal state after:
Module: Mathlib.FieldTheory.JacobsonNoether

Goal state before:
pp: D : Type u_1
inst✝² : DivisionRing D
inst✝¹ : Algebra.IsAlgebraic (↥k) D
p : ℕ
inst✝ : ExpChar D p
a : D
ha : a ∉ k
hinsep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
⊢ ∃ n, 1 ≤ n ∧ a ^ p ^ n ∈ k

Tactic:
by
  obtain ⟨n, hn⟩ := exists_pow_mem_center_of_inseparable p a hinsep
  have nzero : n ≠ 0 := by
    rintro rfl
    rw [pow_zero, pow_one] at hn
    exact ha hn
  exact ⟨n, ⟨Nat.one_le_iff_ne_zero.mpr nzero, hn⟩⟩

Goal state after:
Module: Mathlib.FieldTheory.JacobsonNoether

Goal state before:
pp: D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
p : ℕ
hchar : ExpChar D p
a : D
ha : a ∉ k
hinsep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
m : ℕ
hm : 1 ≤ m ∧ a ^ p ^ m ∈ k
n : ℕ
hn : p ^ m ≤ n
x : D
⊢ ((mulLeft (↥k) a - mulRight (↥k) a) ^ p ^ m) x = 0 x

Tactic:
sub_pow_expChar_pow_of_commute p m (commute_mulLeft_right a a),

Goal state after:
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
p : ℕ
hchar : ExpChar D p
a : D
ha : a ∉ k
hinsep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
m : ℕ
hm : 1 ≤ m ∧ a ^ p ^ m ∈ k
n : ℕ
hn : p ^ m ≤ n
x : D
⊢ (mulLeft (↥k) a ^ p ^ m - mulRight (↥k) a ^ p ^ m) x = 0 x
Module: Mathlib.FieldTheory.JacobsonNoether

Goal state before:
pp: D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
p : ℕ
hchar : ExpChar D p
a : D
ha : a ∉ k
hinsep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
m : ℕ
hm : 1 ≤ m ∧ a ^ p ^ m ∈ k
n : ℕ
hn : p ^ m ≤ n
inter : (⇑((ad (↥k) D) a))^[p ^ m] = 0
⊢ (⇑((ad (↥k) D) a))^[n - p ^ m] ∘ 0 = 0

Tactic:
Pi.comp_zero,

Goal state after:
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
p : ℕ
hchar : ExpChar D p
a : D
ha : a ∉ k
hinsep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
m : ℕ
hm : 1 ≤ m ∧ a ^ p ^ m ∈ k
n : ℕ
hn : p ^ m ≤ n
inter : (⇑((ad (↥k) D) a))^[p ^ m] = 0
⊢ Function.const D ((⇑((ad (↥k) D) a))^[n - p ^ m] 0) = 0
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
n : ℕ
hn : 0 < n
c : D := (⇑((ad (↥k) D) a))^[n] b
hb : c ≠ 0 ∧ (⇑((ad (↥k) D) a))^[n + 1] b = 0
hc_def : c = (⇑((ad (↥k) D) a))^[n] b
x✝ : Invertible c := { invOf := c⁻¹, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }
⊢ ((ad (↥k) D) a) c = 0

Tactic:
← Function.iterate_succ_apply' (ad k D a) n b,

Goal state after:
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
n : ℕ
hn : 0 < n
c : D := (⇑((ad (↥k) D) a))^[n] b
hb : c ≠ 0 ∧ (⇑((ad (↥k) D) a))^[n + 1] b = 0
hc_def : c = (⇑((ad (↥k) D) a))^[n] b
x✝ : Invertible c := { invOf := c⁻¹, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }
⊢ (⇑((ad (↥k) D) a))^[n.succ] b = 0
Module: Mathlib.FieldTheory.Relrank

Goal state before:
pp: E : Type v
inst✝ : Field E
A B : Subfield E
⊢ A.relrank B = 1 ↔ B ≤ A

Tactic:
relrank,

Goal state after:
E : Type v
inst✝ : Field E
A B : Subfield E
⊢ Module.rank ↥(A ⊓ B) ↥(extendScalars ⋯) = 1 ↔ B ≤ A
Module: Mathlib.FieldTheory.Relrank

Goal state before:
pp: E : Type v
inst✝ : Field E
A B C : Subfield E
h : B ≤ C
⊢ A.relfinrank B * B.relfinrank C = (A ⊓ B).relfinrank C

Tactic:
by
  simpa using! congr(toNat $(relrank_mul_relrank_eq_inf_relrank A h))

Goal state after:
Module: Mathlib.FieldTheory.Relrank

Goal state before:
pp: E : Type v
inst✝ : Field E
A B C : Subfield E
h : A ≤ B
⊢ A.relfinrank (B ⊓ C) * B.relfinrank C = A.relfinrank C

Tactic:
by
  simpa using! congr(toNat $(relrank_inf_mul_relrank_of_le C h))

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
x✝ : ℕ
| Bivariate.swap ((monomial x✝) ((Φ E).coeff x✝))

Tactic:
Bivariate.swap_monomial,

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
x✝ : ℕ
| Polynomial.map Polynomial.C ((Φ E).coeff x✝) * Polynomial.C (Polynomial.X ^ x✝)
Module: Mathlib.FieldTheory.Relrank

Goal state before:
pp: F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A B C : IntermediateField F E
h : B ≤ C
⊢ A.relfinrank B * B.relfinrank C = (A ⊓ B).relfinrank C

Tactic:
by
  simpa using! congr(toNat $(relrank_mul_relrank_eq_inf_relrank A h))

Goal state after:
Module: Mathlib.FieldTheory.Relrank

Goal state before:
pp: F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A B C : IntermediateField F E
h : A ≤ B
⊢ A.relfinrank (B ⊓ C) * B.relfinrank C = A.relfinrank C

Tactic:
by
  simpa using! congr(toNat $(relrank_inf_mul_relrank_of_le C h))

Goal state after:
Module: Mathlib.Geometry.Euclidean.Projection

Goal state before:
pp: case mpr
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace 𝕜 V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst✝¹ : Nonempty ↥s
inst✝ : s.direction.HasOrthogonalProjection
p q : P
⊢ q ∈ s ∧ p -ᵥ q ∈ s.directionᗮ → ↑((orthogonalProjection s) p) = q

Tactic:
rintro ⟨hqs, hpq⟩

Goal state after:
case mpr
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace 𝕜 V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst✝¹ : Nonempty ↥s
inst✝ : s.direction.HasOrthogonalProjection
p q : P
hqs : q ∈ s
hpq : p -ᵥ q ∈ s.directionᗮ
⊢ ↑((orthogonalProjection s) p) = q
Module: Mathlib.Geometry.Euclidean.Altitude

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
h :
  finrank ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) +
      finrank ℝ ↥((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)) =
    finrank ℝ ↥(vectorSpan ℝ (Set.range s.points))
hn : n - 1 + 1 = n
⊢ #{i}ᶜ = n - 1 + 1

Tactic:
rw [card_compl, card_singleton, Fintype.card_fin, hn, add_tsub_cancel_right]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
v₁ v₂ v₃ : V
⊢ ∠ (-v₁) (-v₂) (-v₃) = ∠ v₁ v₂ v₃

Tactic:
simpa only [zero_sub] using angle_const_sub 0 v₁ v₂ v₃

Goal state after: