mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: case inr.inr.refine_1
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
m : ℕ
F_inv : MapsTo T F F
inst✝ : U.IsSymm
n : ℕ
s : Finset X
h : IsDynCoverOf T F U m ↑s
x✝ : Nonempty X
s_nemp : s.Nonempty
x : X
x_F : x ∈ F
m_pos : m > 0
dyncover : (Fin n → ↥s) → X
h_dyncover :
  ∀ (t : Fin n → ↥s),
    ⋂ k, T^[m * ↑k] ⁻¹' ball (↑(t k)) (dynEntourage T U m) ⊆ ball (dyncover t) (dynEntourage T (U ○ U) (m * n))
sn : Set X := range dyncover
⊢ IsDynCoverOf T F (U ○ U) (m * n) ↑sn.toFinset

Tactic:
have _ : Nonempty s := Finset.Nonempty.coe_sort s_nemp

Goal state after:
case inr.inr.refine_1
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
m : ℕ
F_inv : MapsTo T F F
inst✝ : U.IsSymm
n : ℕ
s : Finset X
h : IsDynCoverOf T F U m ↑s
x✝¹ : Nonempty X
s_nemp : s.Nonempty
x : X
x_F : x ∈ F
m_pos : m > 0
dyncover : (Fin n → ↥s) → X
h_dyncover :
  ∀ (t : Fin n → ↥s),
    ⋂ k, T^[m * ↑k] ⁻¹' ball (↑(t k)) (dynEntourage T U m) ⊆ ball (dyncover t) (dynEntourage T (U ○ U) (m * n))
sn : Set X := range dyncover
x✝ : Nonempty ↥s
⊢ IsDynCoverOf T F (U ○ U) (m * n) ↑sn.toFinset
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᵐ[ν + ν']
    (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')
h₂ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᵐ[ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
h₃ : (μ.singularPart ν').rnDeriv (ν + ν') =ᵐ[ν] (μ.singularPart ν').rnDeriv ν
h₄ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᵐ[ν] 0
⊢ (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᵐ[ν] 0

Tactic:
rw [rnDeriv_eq_zero]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᵐ[ν + ν']
    (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')
h₂ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᵐ[ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
h₃ : (μ.singularPart ν').rnDeriv (ν + ν') =ᵐ[ν] (μ.singularPart ν').rnDeriv ν
h₄ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᵐ[ν] 0
⊢ ν'.withDensity (μ.rnDeriv ν') ⟂ₘ ν
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
⊢ coverMincard T F U 0 = 1

Tactic:
apply le_antisymm _ ((one_le_coverMincard_iff T F U 0).2 h)

Goal state after:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
⊢ coverMincard T F U 0 ≤ 1
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.toHom.comp f.toHom = Hom.id L M

Tactic:
by
  rw [← comp_toHom, symm_comp_self, refl_toHom]

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
v : α → R
⊢ Term.realize v 1 = 1

Tactic:
simp [one_def, funMap_one, constantMap]

Goal state after:
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
x : M
⊢ x ∈ (closure L).toFun s ↔ ∃ t, Term.realize Subtype.val t = x

Tactic:
rw [← SetLike.mem_coe, coe_closure_eq_range_term_realize, mem_range]

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝² : L.Structure M
α : Type u₁
s : Set (α → M)
L' : Language
inst✝¹ : L'.Structure M
h : A.Definable L s
φ : L →ᴸ L'
inst✝ : φ.IsExpansionOn M
⊢ A.Definable L' s

Tactic:
by
  obtain ⟨ψ, rfl⟩ := h
  refine ⟨(φ.addConstants A).onFormula ψ, ?_⟩
  ext x
  simp only [mem_ofPred_eq, LHom.realize_onFormula]

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
⊢ (∀' f✝).toFormula.Realize v ↔ (∀' f✝).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)

Tactic:
rw [toFormula, Formula.Realize, realize_all, realize_all]
    refine forall_congr' fun a => ?_
    have h := ih3 (Sum.elim (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a))
    simp only [Sum.elim_comp_inl, Sum.elim_comp_inr] at h
    rw [← h, realize_relabel, Formula.Realize, iff_iff_eq]
    simp only [Function.comp_def]
    congr with x
    · rcases x with _ | x
      · simp
      · refine Fin.lastCases ?_ ?_ x
        · simp [Fin.snoc]
        · simp only [castSucc, Sum.elim_inr,
            finSumFinEquiv_symm_apply_castAdd, Sum.map_inl, Sum.elim_inl]
          rw [← castSucc]
          simp
    · exact Fin.elim0 x

Goal state after:
Module: Mathlib.ModelTheory.ElementarySubstructures

Goal state before:
pp: case e'_7
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' :
  (BoundedFormula.constantsVarsEquiv φ).Realize (⇑S.subtype ∘ Sum.elim (fun a ↦ ↑(L.con a)) v') (⇑S.subtype ∘ default)
i : ↑↑S ⊕ Fin 1
⊢ Sum.elim (fun a ↦ ↑(L.con a)) (Subtype.val ∘ v') i = (⇑S.subtype ∘ Sum.elim (fun a ↦ ↑(L.con a)) v') i

Tactic:
cases i <;> rfl

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: case mpr
L : Language
T : L.Theory
hsat : T.IsSatisfiable
h : ∀ (M N : T.ModelType), ↑M ≅[L] ↑N
φ : L.Sentence
⊢ T ⊨ᵇ φ ∨ T ⊨ᵇ Formula.not φ

Tactic:
obtain ⟨M⟩ := hsat

Goal state after:
case mpr
L : Language
T : L.Theory
h : ∀ (M N : T.ModelType), ↑M ≅[L] ↑N
φ : L.Sentence
M : T.ModelType
⊢ T ⊨ᵇ φ ∨ T ⊨ᵇ Formula.not φ
Module: Mathlib.FieldTheory.FinTrdeg

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
ι : Type u_3
inst✝ : Finite ι
x : ι → L
hx : IsTranscendenceBasis K x
⊢ FinTrdeg K L

Tactic:
rw [finTrdeg_iff_trdeg, ← Cardinal.lift_lt_aleph0,
    ← hx.lift_cardinalMk_eq_trdeg, Cardinal.lift_lt_aleph0]

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
ι : Type u_3
inst✝ : Finite ι
x : ι → L
hx : IsTranscendenceBasis K x
⊢ Cardinal.mk ι < Cardinal.aleph0
Module: Mathlib.FieldTheory.Finite.Polynomial

Goal state before:
pp: σ K : Type u
inst✝ : Fintype K
m : ℕ
⊢ DecidablePred fun x ↦ x ∈ {n | ∀ (i : σ), n i ≤ m}

Tactic:
simp only [Set.mem_ofPred_eq]

Goal state after:
σ K : Type u
inst✝ : Fintype K
m : ℕ
⊢ DecidablePred fun n ↦ ∀ (i : σ), n i ≤ m
Module: Mathlib.FieldTheory.Finite.Polynomial

Goal state before:
pp: σ K : Type u
inst✝ : Fintype K
m : ℕ
⊢ DecidablePred fun x ↦ x ∈ {n | ∀ (i : σ), n i ≤ m}

Tactic:
by
  simp only [Set.mem_ofPred_eq]; infer_instance

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
x1 x2 y : ℕ × K
H : R K p x1 x2
n : ℕ
x : K
⊢ R K p ((n, x).1 + y.1, (⇑(frobenius K p))^[y.1] (n, x).2 * (⇑(frobenius K p))^[(n, x).1] y.2)
    ((n + 1, (frobenius K p) x).1 + y.1,
      (⇑(frobenius K p))^[y.1] (n + 1, (frobenius K p) x).2 * (⇑(frobenius K p))^[(n + 1, (frobenius K p) x).1] y.2)

Tactic:
rw [← iterate_succ_apply, iterate_succ_apply', iterate_succ_apply', ← map_mul,
        Nat.succ_add]

Goal state after:
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x1 x2 y : ℕ × K
H : R K p x1 x2
n : ℕ
x : K
⊢ R K p ((n, x).1 + y.1, (⇑(frobenius K p))^[y.1] (n, x).2 * (⇑(frobenius K p))^[(n, x).1] y.2)
    ((n + y.1).succ, (frobenius K p) ((⇑(frobenius K p))^[y.1] x * (⇑(frobenius K p))^[n] y.2))
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
x : R
hp : 1 < p
⊢ x ∈ pNilradical R p ↔ ∃ n, x ^ p ^ n = 0

Tactic:
pNilradical_eq_nilradical hp

Goal state after:
case pos
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
x : R
hp : 1 < p
⊢ x ∈ nilradical R ↔ ∃ n, x ^ p ^ n = 0
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ ProfiniteGrp.{max v u}
a✝ b✝ : (j : J) → ↑(F.obj j).toProfinite.toTop
hx : a✝ ∈ {x | ∀ ⦃i j : J⦄ (π : i ⟶ j), (Hom.hom (F.map π)) (x i) = x j}
hy : b✝ ∈ {x | ∀ ⦃i j : J⦄ (π : i ⟶ j), (Hom.hom (F.map π)) (x i) = x j}
x✝¹ x✝ : J
π : x✝¹ ⟶ x✝
⊢ (Hom.hom (F.map π)) ((a✝ * b✝) x✝¹) = (a✝ * b✝) x✝

Tactic:
simp only [Pi.mul_apply, map_mul, hx π, hy π]

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
⊢ Bijective fun x ↦ x ^ p

Tactic:
by
    simp_rw [← frobenius_def]
    let f : PerfectClosure K p → PerfectClosure K p := fun e ↦
      liftOn e (fun x => mk K p (x.1 + 1, x.2)) fun x y H =>
      match x, y, H with
      | _, _, R.intro n x => Quot.sound (R.intro _ _)
    refine bijective_iff_has_inverse.mpr ⟨f, fun e ↦ induction_on e fun ⟨n, x⟩ ↦ ?_,
      fun e ↦ induction_on e fun ⟨n, x⟩ ↦ ?_⟩ <;>
      simp only [f, liftOn_mk, frobenius_mk, mk_succ_pow]

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

Goal state before:
pp: R : Type u
inst✝³ : Field R
inst✝² : IsRealClosed R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
h : 0 ≤ x
⊢ IsSquare x

Tactic:
by
    suffices IsSquare (-x) → x = 0 by aesop
    exact fun hc ↦ le_antisymm (nonpos_of_neg_nonneg (IsSquare.nonneg hc)) h

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
⊢ ∃ m, 1 ≤ m ∧ ∀ (n : ℕ), p ^ m ≤ n → (⇑((ad (↥k) D) a))^[n] = 0

Tactic:
refine ⟨m, ⟨hm.1, fun n hn ↦ ?_⟩⟩

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
⊢ (⇑((ad (↥k) D) a))^[n] = 0
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: case inr
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq (Subgroup G)
n : ℕ
ih :
  ∀ m < n,
    ∀ {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι},
      ⋃ i ∈ s, g i • ↑(H i) = Set.univ →
        ∀ j ∈ s,
          ⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H i) ≠ Set.univ →
            m = (Finset.image H s).card → ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
j : ι
hcovers : (⋃ x ∈ {x ∈ s | H x = H j}, g x • ↑(H x)) ∪ ⋃ x ∈ {a ∈ s | ¬H a = H j}, g x • ↑(H x) = Set.univ
hj : j ∈ s
hcovers' : ⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H i) ≠ Set.univ
hn : n = (Finset.image H s).card
x : G
hx : ∀ (y : G), y • ↑(H j) ⊆ ⋃ i ∈ {x ∈ s | H x ≠ H j}, (y * x⁻¹ * g i) • ↑(H i)
κ : Type u_2 := ↥({x ∈ s | H x ≠ H j}) × Option ↥({x ∈ s | H x = H j})
f : κ → G :=
  fun x_1 ↦
    match x_1 with
    | (k₁, some k₂) => g ↑k₂ * x⁻¹ * g ↑k₁
    | (k₁, none) => g ↑k₁
K : κ → Subgroup G := fun k ↦ H ↑k.1
hK' : ∀ (k : κ), K k ∈ (Finset.image H s).erase (H j)
hK : ∀ (k : κ), K k ≠ H j
y : G
hy : y ∈ ⋃ x ∈ {a ∈ s | ¬H a = H j}, g x • ↑(H x)
⊢ ∃ i, ∃ (_ : i ∈ Finset.univ), y ∈ f i • ↑(K i)

Tactic:
have ⟨i, hi, hy⟩ := Set.mem_iUnion₂.mp hy
        exact ⟨⟨⟨i, hi⟩, none⟩, Finset.mem_univ _, hy⟩

Goal state after:
Module: Mathlib.RingTheory.Algebraic.LinearIndependent

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
H : ∀ (p : F[X]), (aeval x) p = 0 → p = 0
s : Finset F
m : F → F
i : F
hi : i ∈ s
hnz : ∀ (a : F), x - (algebraMap F E) a ≠ 0
b : E := ∏ j ∈ s, (x - (algebraMap F E) j)
h1 : ∀ i ∈ s, m i • (b * (x - (algebraMap F E) i)⁻¹) = m i • ∏ j ∈ s.erase i, (x - (algebraMap F E) j)
hm : ∑ x_1 ∈ s, m x_1 • ∏ j ∈ s.erase x_1, (x - (algebraMap F E) j) = 0
p : F[X] := ∑ i ∈ s, C (m i) * ∏ j ∈ s.erase i, (X - C j)
⊢ ∑ x_1 ∈ s, (aeval x) (C (m x_1)) * (aeval x) (∏ j ∈ s.erase x_1, (X - C j)) =
    ∑ x_1 ∈ s, m x_1 • ∏ j ∈ s.erase x_1, (x - (algebraMap F E) j)

Tactic:
map_prod,

Goal state after:
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
H : ∀ (p : F[X]), (aeval x) p = 0 → p = 0
s : Finset F
m : F → F
i : F
hi : i ∈ s
hnz : ∀ (a : F), x - (algebraMap F E) a ≠ 0
b : E := ∏ j ∈ s, (x - (algebraMap F E) j)
h1 : ∀ i ∈ s, m i • (b * (x - (algebraMap F E) i)⁻¹) = m i • ∏ j ∈ s.erase i, (x - (algebraMap F E) j)
hm : ∑ x_1 ∈ s, m x_1 • ∏ j ∈ s.erase x_1, (x - (algebraMap F E) j) = 0
p : F[X] := ∑ i ∈ s, C (m i) * ∏ j ∈ s.erase i, (X - C j)
⊢ ∑ x_1 ∈ s, (aeval x) (C (m x_1)) * ∏ x_2 ∈ s.erase x_1, (aeval x) (X - C x_2) =
    ∑ x_1 ∈ s, m x_1 • ∏ j ∈ s.erase x_1, (x - (algebraMap F E) j)
Module: Mathlib.RingTheory.Algebraic.LinearIndependent

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
H : ∀ (p : F[X]), (aeval x) p = 0 → p = 0
s : Finset F
m : F → F
i : F
hi : i ∈ s
hnz : ∀ (a : F), x - (algebraMap F E) a ≠ 0
b : E := ∏ j ∈ s, (x - (algebraMap F E) j)
h1 : ∀ i ∈ s, m i • (b * (x - (algebraMap F E) i)⁻¹) = m i • ∏ j ∈ s.erase i, (x - (algebraMap F E) j)
p : F[X] := ∑ i ∈ s, C (m i) * ∏ j ∈ s.erase i, (X - C j)
h2 : ∀ j ∈ s.erase i, m j * ∏ x ∈ s.erase j, (i - x) = 0
hm : ∑ x ∈ s, (aeval i) (C (m x)) * (aeval i) (∏ j ∈ s.erase x, (X - C j)) = 0
⊢ m i = 0

Tactic:
map_prod,

Goal state after:
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
H : ∀ (p : F[X]), (aeval x) p = 0 → p = 0
s : Finset F
m : F → F
i : F
hi : i ∈ s
hnz : ∀ (a : F), x - (algebraMap F E) a ≠ 0
b : E := ∏ j ∈ s, (x - (algebraMap F E) j)
h1 : ∀ i ∈ s, m i • (b * (x - (algebraMap F E) i)⁻¹) = m i • ∏ j ∈ s.erase i, (x - (algebraMap F E) j)
p : F[X] := ∑ i ∈ s, C (m i) * ∏ j ∈ s.erase i, (X - C j)
h2 : ∀ j ∈ s.erase i, m j * ∏ x ∈ s.erase j, (i - x) = 0
hm : ∑ x ∈ s, (aeval i) (C (m x)) * ∏ x ∈ s.erase x, (aeval i) (X - C x) = 0
⊢ m i = 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 := ⋯ }
this : ((ad (↥k) D) a) c = 0
⊢ (mulLeft (↥k) a) c - (mulRight (↥k) a) c = 0

Tactic:
rw [← this]

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 := ⋯ }
this : ((ad (↥k) D) a) c = 0
⊢ (mulLeft (↥k) a) c - (mulRight (↥k) a) c = ((ad (↥k) D) a) c
Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality

Goal state before:
pp: case neg
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A B : IntermediateField F E
hA : ¬Algebra.IsAlgebraic F ↥A
hB : ¬Algebra.IsAlgebraic F ↥B
⊢ Module.rank F ↥(A ⊔ B) ≤ Module.rank F ↥A * Module.rank F ↥B

Tactic:
← Algebra.transcendental_iff_not_isAlgebraic

Goal state after:
case neg
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
⊢ Module.rank F ↥(A ⊔ B) ≤ Module.rank F ↥A * Module.rank F ↥B
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: case pos
K : Type u
inst✝¹ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
inst✝ : NeZero n
e : Gal(K[n√a]/K)
this✝ : Fact (Irreducible (X ^ n - C a))
this : Algebra K K[n√a] := inferInstance
h : a = 0
⊢ 1 * root (X ^ n - C a) = e (root (X ^ n - C a))

pp: case neg
K : Type u
inst✝¹ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
inst✝ : NeZero n
e : Gal(K[n√a]/K)
this✝ : Fact (Irreducible (X ^ n - C a))
this : Algebra K K[n√a] := inferInstance
h : ¬a = 0
⊢ e (root (X ^ n - C a)) / root (X ^ n - C a) * root (X ^ n - C a) = e (root (X ^ n - C a))

Tactic:
· obtain rfl := not_imp_not.mp (fun hn ↦ ne_zero_of_irreducible_X_pow_sub_C' hn H) h
      rw [(pow_one _).symm.trans (root_X_pow_sub_C_pow 1 a), one_mul,
        ← AdjoinRoot.algebraMap_eq, AlgEquiv.commutes]

Goal state after:
case neg
K : Type u
inst✝¹ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
inst✝ : NeZero n
e : Gal(K[n√a]/K)
this✝ : Fact (Irreducible (X ^ n - C a))
this : Algebra K K[n√a] := inferInstance
h : ¬a = 0
⊢ e (root (X ^ n - C a)) / root (X ^ n - C a) * root (X ^ n - C a) = e (root (X ^ n - C a))
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: K : Type u
inst✝³ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ n - C a)
this✝ : FiniteDimensional K L
this : IsGalois K L
hn : 0 < n
⊢ Module.finrank K L = n

Tactic:
have : NeZero n := ⟨ne_zero_of_irreducible_X_pow_sub_C H⟩

Goal state after:
K : Type u
inst✝³ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ n - C a)
this✝¹ : FiniteDimensional K L
this✝ : IsGalois K L
hn : 0 < n
this : NeZero n
⊢ Module.finrank K L = n
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: K : Type u
inst✝³ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ n - C a)
⊢ Module.finrank K L = n

Tactic:
by
  have := Polynomial.IsSplittingField.finiteDimensional L (X ^ n - C a)
  have := isGalois_of_isSplittingField_X_pow_sub_C hζ H L
  have hn := Nat.pos_iff_ne_zero.mpr (ne_zero_of_irreducible_X_pow_sub_C H)
  have : NeZero n := ⟨ne_zero_of_irreducible_X_pow_sub_C H⟩
  rw [← IsGalois.card_aut_eq_finrank, Nat.card_congr ((autEquivZmod H L <|
    (mem_primitiveRoots hn).mp hζ.choose_spec).toEquiv.trans Multiplicative.toAdd), Nat.card_zmod]

Goal state after:
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
A B : Subalgebra R S
ι : Type u_1
b : Basis ι R ↥B
H : ((toSubmodule A).mulRightMap ⇑b).ker = ⊥
⊢ A.LinearDisjoint B

Tactic:
exact Submodule.LinearDisjoint.of_basis_right _ _ b H

Goal state after:
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
hf : Flat R ↥A ∨ Flat R ↥B
hc : ∀ (a b : ↥(A ⊓ B)), Commute ↑a ↑b
hinj : Function.Injective ⇑(algebraMap R S)
a✝ : Nontrivial R
this : Module.rank R ↥⊥ = 1
⊢ 1 ≤ Module.rank R ↥(A ⊓ B)

Tactic:
rw [← this]

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
hf : Flat R ↥A ∨ Flat R ↥B
hc : ∀ (a b : ↥(A ⊓ B)), Commute ↑a ↑b
hinj : Function.Injective ⇑(algebraMap R S)
a✝ : Nontrivial R
this : Module.rank R ↥⊥ = 1
⊢ Module.rank R ↥⊥ ≤ Module.rank R ↥(A ⊓ B)
Module: Mathlib.FieldTheory.NormalizedTrace

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Algebra F K
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
f : E →ₐ[F] K
a : E
e : ↥F⟮a⟯ ≃ₐ[F] ↥F⟮f a⟯ := (F⟮a⟯.equivMap f).trans (equivOfEq ⋯)
⊢ (↑(Module.finrank F ↥F⟮f a⟯))⁻¹ • (trace F ↥F⟮f a⟯) (AdjoinSimple.gen F (f a)) =
    (↑(Module.finrank F ↥F⟮a⟯))⁻¹ • (trace F ↥F⟮a⟯) (AdjoinSimple.gen F a)

Tactic:
← LinearEquiv.finrank_eq e.toLinearEquiv

Goal state after:
F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Algebra F K
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
f : E →ₐ[F] K
a : E
e : ↥F⟮a⟯ ≃ₐ[F] ↥F⟮f a⟯ := (F⟮a⟯.equivMap f).trans (equivOfEq ⋯)
⊢ (↑(Module.finrank F ↥F⟮a⟯))⁻¹ • (trace F ↥F⟮f a⟯) (AdjoinSimple.gen F (f a)) =
    (↑(Module.finrank F ↥F⟮a⟯))⁻¹ • (trace F ↥F⟮a⟯) (AdjoinSimple.gen F a)
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
inst✝⁸ : CommRing R
A : Type v
inst✝⁷ : CommRing A
B : Type w
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Flat R A
inst✝² : Flat R B
inst✝¹ : Algebra.Transcendental R A
inst✝ : Algebra.Transcendental R B
H : IsField (A ⊗[R] B)
this : Field (A ⊗[R] B) := H.toField
a : A
hta : Transcendental R a
b : B
htb : Transcendental R b
ha : Function.Injective ⇑(algebraMap R A)
hb : Function.Injective ⇑(algebraMap R B)
⊢ False

Tactic:
let fa : A →ₐ[R] A ⊗[R] B := Algebra.TensorProduct.includeLeft

Goal state after:
R : Type u
inst✝⁸ : CommRing R
A : Type v
inst✝⁷ : CommRing A
B : Type w
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Flat R A
inst✝² : Flat R B
inst✝¹ : Algebra.Transcendental R A
inst✝ : Algebra.Transcendental R B
H : IsField (A ⊗[R] B)
this : Field (A ⊗[R] B) := H.toField
a : A
hta : Transcendental R a
b : B
htb : Transcendental R b
ha : Function.Injective ⇑(algebraMap R A)
hb : Function.Injective ⇑(algebraMap R B)
fa : A →ₐ[R] A ⊗[R] B := Algebra.TensorProduct.includeLeft
⊢ False
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
A : Type v
inst✝⁵ : CommRing A
B : Type w
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Flat R A
inst✝ : Flat R B
H : IsField (A ⊗[R] B)
h : ¬Algebra.IsAlgebraic R A ∧ ¬Algebra.IsAlgebraic R B
⊢ False

Tactic:
← Algebra.transcendental_iff_not_isAlgebraic

Goal state after:
R : Type u
inst✝⁶ : CommRing R
A : Type v
inst✝⁵ : CommRing A
B : Type w
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Flat R A
inst✝ : Flat R B
H : IsField (A ⊗[R] B)
h : Algebra.Transcendental R A ∧ Algebra.Transcendental R B
⊢ False
Module: Mathlib.FieldTheory.PurelyInseparable.Tower

Goal state before:
pp: F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : IsPurelyInseparable F E
ι : Type u_1
v : ι → K
hsep : ∀ (i : ι), IsSeparable F (v i)
h : LinearIndependent F v
q : ℕ
h✝ : ExpChar F q
this : ExpChar K q
l : ι →₀ E
hl : (Finsupp.linearCombination E v) l = 0
i : ι
f : ι → ℕ
hf : ∀ (i : ι), l i ^ q ^ f i ∈ (algebraMap F E).range
n : ℕ := l.support.sup f
⊢ l i = 0 i

Tactic:
have := (expChar_pow_pos F q n).ne'

Goal state after:
F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : IsPurelyInseparable F E
ι : Type u_1
v : ι → K
hsep : ∀ (i : ι), IsSeparable F (v i)
h : LinearIndependent F v
q : ℕ
h✝ : ExpChar F q
this✝ : ExpChar K q
l : ι →₀ E
hl : (Finsupp.linearCombination E v) l = 0
i : ι
f : ι → ℕ
hf : ∀ (i : ι), l i ^ q ^ f i ∈ (algebraMap F E).range
n : ℕ := l.support.sup f
this : q ^ n ≠ 0
⊢ l i = 0 i
Module: Mathlib.FieldTheory.RatFunc.Degree

Goal state before:
pp: K : Type u
inst✝ : Field K
x y : K⟮X⟯
hx : x ≠ 0
hy : y ≠ 0
⊢ (x / y).intDegree = x.intDegree - y.intDegree

Tactic:
by
  rw [div_eq_mul_inv, intDegree_mul, intDegree_inv, ← sub_eq_add_neg] <;> grind

Goal state after: