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

Goal state before:
pp: case inr
X : Type u_1
Y : Type u_2
F : Set X
V : SetRel Y Y
S : X → X
T : Y → Y
φ : X → Y
n : ℕ
h : Semiconj φ S T
inst✝ : V.IsSymm
t : Finset Y
h' : IsDynCoverOf T (φ '' F) V n ↑t
h✝¹ : Nonempty X
s : Finset Y
s_cover : IsDynCoverOf T (φ '' F) V n ↑s
s_card : s.card ≤ t.card
s_inter : ∀ x ∈ s, (ball x (dynEntourage T V n) ∩ φ '' F).Nonempty
g : Y → Y
g_rel : ∀ x ∈ s, g x ∈ ball x (dynEntourage T V n)
g_mem : ∀ x ∈ s, g x ∈ φ '' F
f : Y → X
h✝ : ∀ y ∈ φ '' F, f y ∈ F
φ_f : ∀ y ∈ φ '' F, φ (f y) = y
x : X
hx : x ∈ F
⊢ ∃ a ∈ s, (φ x, φ (f (g a))) ∈ dynEntourage T (V ○ V) n

Tactic:
obtain ⟨y, hy, hxy⟩ := s_cover (Set.mem_image_of_mem _ hx)

Goal state after:
case inr
X : Type u_1
Y : Type u_2
F : Set X
V : SetRel Y Y
S : X → X
T : Y → Y
φ : X → Y
n : ℕ
h : Semiconj φ S T
inst✝ : V.IsSymm
t : Finset Y
h' : IsDynCoverOf T (φ '' F) V n ↑t
h✝¹ : Nonempty X
s : Finset Y
s_cover : IsDynCoverOf T (φ '' F) V n ↑s
s_card : s.card ≤ t.card
s_inter : ∀ x ∈ s, (ball x (dynEntourage T V n) ∩ φ '' F).Nonempty
g : Y → Y
g_rel : ∀ x ∈ s, g x ∈ ball x (dynEntourage T V n)
g_mem : ∀ x ∈ s, g x ∈ φ '' F
f : Y → X
h✝ : ∀ y ∈ φ '' F, f y ∈ F
φ_f : ∀ y ∈ φ '' F, φ (f y) = y
x : X
hx : x ∈ F
y : Y
hy : y ∈ ↑s
hxy : (φ x, y) ∈ dynEntourage T V n
⊢ ∃ a ∈ s, (φ x, φ (f (g a))) ∈ dynEntourage T (V ○ V) n
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
this :
  (μ.rnDeriv ν)⁻¹ =ᵐ[μ] (μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)))⁻¹ ∧
    ν.rnDeriv μ =ᵐ[μ] (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ
⊢ (μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)))⁻¹ =ᵐ[μ] (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ

Tactic:
exact Measure.inv_rnDeriv_aux (absolutelyContinuous_withDensity_rnDeriv hμν)
      (withDensity_absolutelyContinuous _ _)

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

Goal state before:
pp: case a
X : Type u_1
Y : Type u_2
u : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
this : UniformSpace X := UniformSpace.comap φ u
V : Set (Y × Y)
V_uni : V ∈ 𝓤 Y
⊢ ∃ t ∈ 𝓤 Y, Prod.map φ φ ⁻¹' t ⊆ Prod.map φ φ ⁻¹' SetRel.symmetrize V

Tactic:
exact ⟨_, symmetrize_mem_uniformity V_uni, .rfl⟩

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

Goal state before:
pp: X : Type u_1
T : X → X
U : SetRel X X
⊢ netEntropyEntourage T ∅ U = ⊥

Tactic:
netEntropyEntourage,

Goal state after:
X : Type u_1
T : X → X
U : SetRel X X
⊢ (expGrowthSup fun n ↦ ↑(netMaxcard T ∅ U n)) = ⊥
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
⊢ ¬1 = 0

Tactic:
exact one_ne_zero

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

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

Tactic:
exact one_ne_zero

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

Goal state before:
pp: X : Type u_1
T : X → X
F G : Set X
U : SetRel X X
⊢ coverEntropyEntourage T (F ∪ G) U = max (coverEntropyEntourage T F U) (coverEntropyEntourage T G U)

Tactic:
by
  refine le_antisymm ?_ ?_
  · apply le_of_le_of_eq (expGrowthSup_monotone fun n ↦ ?_) expGrowthSup_add
    rw [Pi.add_apply, ← ENat.toENNReal_add]
    exact ENat.toENNReal_mono (coverMincard_union_le T F G U n)
  · exact max_le (coverEntropyEntourage_monotone T U subset_union_left)
      (coverEntropyEntourage_monotone T U subset_union_right)

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite ξ
hμ : μ ≪ ξ
hν : ν ≪ ξ
h1✝ : μ.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ =ᵐ[ξ] μ.rnDeriv ξ
h2✝ : ν.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ =ᵐ[ξ] ν.rnDeriv ξ
h_ac : μ + ν ≪ ξ
a : α
h1 : (μ.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ) a = μ.rnDeriv ξ a
h2 : (ν.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ) a = ν.rnDeriv ξ a
h_lt_top1 : (μ + ν).rnDeriv ξ a < ∞
h_lt_top2 : ν.rnDeriv (μ + ν) a < ∞
h_pos : 0 < (μ + ν).rnDeriv ξ a
⊢ μ.rnDeriv ξ a / ν.rnDeriv ξ a = μ.rnDeriv (μ + ν) a / ν.rnDeriv (μ + ν) a

Tactic:
← h1,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite ξ
hμ : μ ≪ ξ
hν : ν ≪ ξ
h1✝ : μ.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ =ᵐ[ξ] μ.rnDeriv ξ
h2✝ : ν.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ =ᵐ[ξ] ν.rnDeriv ξ
h_ac : μ + ν ≪ ξ
a : α
h1 : (μ.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ) a = μ.rnDeriv ξ a
h2 : (ν.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ) a = ν.rnDeriv ξ a
h_lt_top1 : (μ + ν).rnDeriv ξ a < ∞
h_lt_top2 : ν.rnDeriv (μ + ν) a < ∞
h_pos : 0 < (μ + ν).rnDeriv ξ a
⊢ (μ.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ) a / ν.rnDeriv ξ a = μ.rnDeriv (μ + ν) a / ν.rnDeriv (μ + ν) a
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : L.Structure M
inst✝² : L.Structure N
P : Type u_1
inst✝¹ : L.Structure P
Q : Type u_2
inst✝ : L.Structure Q
f g : M →[L] N
h : f.toFun = g.toFun
⊢ f = g

Tactic:
by cases f; cases g; cases h; rfl

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
L' : Language
α : Type u'
β : Type v'
γ : Type u_1
L'' : Language
ft : (n : ℕ) → L.Term (α ⊕ Fin n) → L'.Term (β ⊕ Fin n)
fr : (n : ℕ) → L.Relations n → L'.Relations n
ft' : (n : ℕ) → L'.Term (β ⊕ Fin n) → L''.Term (γ ⊕ Fin n)
fr' : (n : ℕ) → L'.Relations n → L''.Relations n
n : ℕ
φ : L.BoundedFormula α n
⊢ mapTermRel ft' fr' (fun x ↦ id) (mapTermRel ft fr (fun x ↦ id) φ) =
    mapTermRel (fun x ↦ ft' x ∘ ft x) (fun x ↦ fr' x ∘ fr x) (fun x ↦ id) φ

Tactic:
induction φ with
  | falsum => rfl
  | equal => simp [mapTermRel]
  | rel => simp [mapTermRel]
  | imp _ _ ih1 ih2 => simp [mapTermRel, ih1, ih2]
  | all _ ih3 => simp [mapTermRel, ih3]

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
⊢ mapTermRel (fun x ↦ id) (fun x ↦ id) (fun x ↦ id) φ = φ

Tactic:
induction φ with
  | falsum => rfl
  | equal => simp [mapTermRel]
  | rel => simp [mapTermRel]
  | imp _ _ ih1 ih2 => simp [mapTermRel, ih1, ih2]
  | all _ ih3 => simp [mapTermRel, ih3]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
l : ℕ
v : α → M
xs : Fin l → M
R : L.Relations 2
t₁ t₂ : L.Term (α ⊕ Fin l)
⊢ (R.boundedFormula₂ t₁ t₂).Realize v xs ↔ RelMap R ![realize (Sum.elim v xs) t₁, realize (Sum.elim v xs) t₂]

Tactic:
rw [Relations.boundedFormula₂, realize_rel, iff_eq_eq]

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
l : ℕ
v : α → M
xs : Fin l → M
R : L.Relations 2
t₁ t₂ : L.Term (α ⊕ Fin l)
⊢ (RelMap R fun i ↦ realize (Sum.elim v xs) (![t₁, t₂] i)) =
    RelMap R ![realize (Sum.elim v xs) t₁, realize (Sum.elim v xs) t₂]
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:
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.Substructures

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
S : L.Substructure M
x : M
⊢ (∃ y, ↑y = x) → x ∈ S

Tactic:
rintro ⟨⟨y, hy⟩, rfl⟩

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
S : L.Substructure M
y : M
hy : y ∈ S
⊢ ↑⟨y, hy⟩ ∈ S
Module: Mathlib.ModelTheory.Skolem

Goal state before:
pp: case refine_1
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'
⊢ #↑s + #↑(⇑Equiv.ulift '' s') ≤ #↑(⇑Equiv.ulift '' s')

Tactic:
← lift_le,

Goal state after:
case refine_1
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.{?u.120, w} (#↑s + #↑(⇑Equiv.ulift '' s')) ≤ lift.{?u.120, w} #↑(⇑Equiv.ulift '' s')
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
B : Set M
f : (α → M) → M
h : ∅.TermDefinable L[[↑A]] f
hAB : A ⊆ B
⊢ ∅.TermDefinable L[[↑B]] f

Tactic:
exact h.map_expansion (L.lhomWithConstantsMap (Set.inclusion hAB))

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
M : Type w'
inst✝ : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h2 : lift.{w, w'} #M ≤ lift.{w', w} κ
N0 : (L.elementaryDiagram M).ModelType
hN0 : lift.{max (max u w') v w, w} κ ≤ #↑N0
⊢ ∃ N, Nonempty (M ↪ₑ[L] ↑N) ∧ #↑N = κ

Tactic:
rw [← lift_le.{max u v}, lift_lift, lift_lift] at h2

Goal state after:
L : Language
M : Type w'
inst✝ : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h2 : lift.{max w u v, w'} #M ≤ lift.{max w' u v, w} κ
N0 : (L.elementaryDiagram M).ModelType
hN0 : lift.{max (max u w') v w, w} κ ≤ #↑N0
⊢ ∃ N, Nonempty (M ↪ₑ[L] ↑N) ∧ #↑N = κ
Module: Mathlib.FieldTheory.AxGrothendieck

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝³ : Finite α
K : Type u_3
inst✝² : Field K
inst✝¹ : CompatibleRing K
inst✝ : Finite ι
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
⊢ K ⊨ genericPolyMapSurjOnOfInjOn φ mons ↔
    ∀ (v : α → K) (p : { p // ∀ (i : ι), (p i).support ⊆ mons i }),
      let f := fun v i ↦ (eval v) (↑p i);
      let S := {x | φ.Realize (Sum.elim v x)};
      Set.MapsTo f S S → Set.InjOn f S → Set.SurjOn f S S

Tactic:
have injOnAlt : ∀ {S : Set (ι → K)} (f : (ι → K) → (ι → K)),
      S.InjOn f ↔ ∀ x y, x ∈ S → y ∈ S → f x = f y → x = y := by
    simp [Set.InjOn]; tauto
  simp only [Sentence.Realize, Formula.Realize, genericPolyMapSurjOnOfInjOn, Formula.relabel,
    Function.comp_def, Sum.map, id_eq, Equiv.sumAssoc, Equiv.coe_fn_symm_mk, Sum.elim_inr,
    realize_iAlls, realize_imp, realize_relabel, Fin.natAdd_zero, realize_subst, realize_iInf,
    realize_bdEqual, Term.realize_relabel,
    Equiv.forall_congr_left (Equiv.curry (Fin 2) ι K), Equiv.curry_symm_apply,
    Fin.forall_fin_succ_pi, Fin.forall_fin_zero_pi, realize_iExs, realize_inf, Sum.forall_sum,
    Set.MapsTo, Set.mem_ofPred_eq, injOnAlt, funext_iff, Set.SurjOn, Set.image,
    Set.subset_def, Equiv.forall_congr_left (mvPolynomialSupportLEEquiv mons)]
  simp +singlePass only [← Sum.elim_comp_inl_inr]
  -- was `simp` and very slow (https://github.com/leanprover-community/mathlib4/issues/19751)
  simp only [Function.comp_def, Sum.elim_inl, Sum.elim_inr, Fin.castAdd_zero, Fin.cast_eq_self,
    Nat.add_zero, Term.realize_var, Term.realize_relabel, realize_termOfFreeCommRing,
    lift_genericPolyMap, Nat.reduceAdd, Fin.isValue, Function.uncurry_apply_pair, Fin.cons_zero,
    Fin.cons_one, ↓reduceIte, one_ne_zero]

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

Goal state before:
pp: a : ℕ
h : ¬ℵ₀ ≤ ↑a
p : Cardinal.{u_1}
k : ℕ
hp : Prime p
hk : 0 < k
hpk : p ^ k = ↑a
⊢ p ^ 1 ≤ ↑a

Tactic:
rw [← hpk]

Goal state after:
a : ℕ
h : ¬ℵ₀ ≤ ↑a
p : Cardinal.{u_1}
k : ℕ
hp : Prime p
hk : 0 < k
hpk : p ^ k = ↑a
⊢ p ^ 1 ≤ p ^ k
Module: Mathlib.FieldTheory.Differential.Basic

Goal state before:
pp: F : Type u_2
inst✝⁵ : Field F
inst✝⁴ : Differential F
inst✝³ : CharZero F
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F K
k : K := ⋯.choose
h : F⟮k⟯ = ⊤
⊢ DifferentialAlgebra F K

Tactic:
have : Fact (minpoly F k).Monic := ⟨minpoly.monic (IsAlgebraic.of_finite ..).isIntegral⟩

Goal state after:
F : Type u_2
inst✝⁵ : Field F
inst✝⁴ : Differential F
inst✝³ : CharZero F
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F K
k : K := ⋯.choose
h : F⟮k⟯ = ⊤
this : Fact (minpoly F k).Monic
⊢ DifferentialAlgebra F K
Module: Mathlib.FieldTheory.Finite.Polynomial

Goal state before:
pp: K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : Field K
a b : σ → K
h : a ≠ b
⊢ ∃ i, a i ≠ b i

Tactic:
Ne,

Goal state after:
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : Field K
a b : σ → K
h : ¬a = b
⊢ ∃ i, a i ≠ b i
Module: Mathlib.FieldTheory.Finite.Polynomial

Goal state before:
pp: case ha
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : Field K
a b : σ → K
h : a ≠ b
i : σ
hi : a i ≠ b i
⊢ a i - b i ≠ 0

Tactic:
Ne,

Goal state after:
case ha
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : Field K
a b : σ → K
h : a ≠ b
i : σ
hi : a i ≠ b i
⊢ ¬a i - b i = 0
Module: Mathlib.Topology.Separation.Connected

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : PreconnectedSpace X
inst✝ : DiscreteTopology X
x y : X
hxy : x ≠ y
⊢ False

Tactic:
Ne,

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : PreconnectedSpace X
inst✝ : DiscreteTopology X
x y : X
hxy : ¬x = y
⊢ False
Module: Mathlib.FieldTheory.Differential.Liouville

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁸ : Field F
inst✝⁷ : Field K
inst✝⁶ : Differential F
inst✝⁵ : Differential K
inst✝⁴ : Algebra F K
inst✝³ : DifferentialAlgebra F K
inst✝² : CharZero F
B : IntermediateField F K
inst✝¹ : FiniteDimensional F ↥B
inst : IsLiouville F K
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → ↥B
v : ↥B
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
⊢ ↑a = ∑ x, ↑(c x) * (algebraMap (↥B) K) (logDeriv (u x)) + (algebraMap (↥B) K) v′

Tactic:
simp_rw [IsScalarTower.algebraMap_apply F B K]

Goal state after:
F : Type u_1
K : Type u_2
inst✝⁸ : Field F
inst✝⁷ : Field K
inst✝⁶ : Differential F
inst✝⁵ : Differential K
inst✝⁴ : Algebra F K
inst✝³ : DifferentialAlgebra F K
inst✝² : CharZero F
B : IntermediateField F K
inst✝¹ : FiniteDimensional F ↥B
inst : IsLiouville F K
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → ↥B
v : ↥B
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
⊢ (algebraMap (↥B) K) ((algebraMap F ↥B) a) =
    ∑ x, (algebraMap (↥B) K) ((algebraMap F ↥B) (c x)) * (algebraMap (↥B) K) (logDeriv (u x)) + (algebraMap (↥B) K) v′
Module: Mathlib.FieldTheory.Galois.NormalBasis

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Infinite K
e : Module.Basis (Module.Free.ChooseBasisIndex K L) K L
M : Matrix Gal(L/K) Gal(L/K) (MvPolynomial (Module.Free.ChooseBasisIndex K L) L) :=
  Matrix.of fun i j ↦ ∑ k, i.symm (j (e k)) • MvPolynomial.X k
hq : Submodule.span L (Set.range fun k j ↦ j (e k)) = ⊤
c : Module.Free.ChooseBasisIndex K L → L
hc : (MvPolynomial.eval c) M.det = 1
hM : M.det ≠ 0
h : ∀ (b : Module.Free.ChooseBasisIndex K L → K), (MvPolynomial.eval (⇑(algebraMap K L) ∘ b)) M.det = 0
⊢ False

Tactic:
refine hM (MvPolynomial.funext_set _
      (fun _ ↦ Set.infinite_range_of_injective (algebraMap K L).injective) fun x hx ↦ ?_)

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Infinite K
e : Module.Basis (Module.Free.ChooseBasisIndex K L) K L
M : Matrix Gal(L/K) Gal(L/K) (MvPolynomial (Module.Free.ChooseBasisIndex K L) L) :=
  Matrix.of fun i j ↦ ∑ k, i.symm (j (e k)) • MvPolynomial.X k
hq : Submodule.span L (Set.range fun k j ↦ j (e k)) = ⊤
c : Module.Free.ChooseBasisIndex K L → L
hc : (MvPolynomial.eval c) M.det = 1
hM : M.det ≠ 0
h : ∀ (b : Module.Free.ChooseBasisIndex K L → K), (MvPolynomial.eval (⇑(algebraMap K L) ∘ b)) M.det = 0
x : Module.Free.ChooseBasisIndex K L → L
hx : x ∈ Set.univ.pi fun x ↦ Set.range ⇑(algebraMap K L)
⊢ (MvPolynomial.eval x) M.det = (MvPolynomial.eval x) 0
Module: Mathlib.FieldTheory.IsPerfectClosure

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

Tactic:
by_cases hp : 1 < p
  · rw [pNilradical_eq_nilradical hp]
    refine ⟨fun ⟨n, h⟩ ↦ ⟨n, ?_⟩, fun ⟨n, h⟩ ↦ ⟨p ^ n, h⟩⟩
    rw [← Nat.sub_add_cancel ((n.lt_pow_self hp).le), pow_add, h, mul_zero]
  rw [pNilradical_eq_bot hp, Ideal.mem_bot]
  refine ⟨fun h ↦ ⟨0, by rw [pow_zero, pow_one, h]⟩, fun ⟨n, h⟩ ↦ ?_⟩
  rcases Nat.le_one_iff_eq_zero_or_eq_one.1 (not_lt.1 hp) with hp | hp
  · by_cases hn : n = 0
    · rwa [hn, pow_zero, pow_one] at h
    rw [hp, zero_pow hn, pow_zero] at h
    subsingleton [subsingleton_of_zero_eq_one h.symm]
  rwa [hp, one_pow, pow_one] at h

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

Goal state before:
pp: case h.left
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : Normal k ↥L
N : Set Gal(↥L/k)
L' : IntermediateField k ↥L
left✝ : FiniteDimensional k ↥L'
hO : ↑L'.fixingSubgroup ⊆ N
this : Module.Finite k ↥(IntermediateField.lift L')
⊢ ↑(IntermediateField.lift L').fixingSubgroup ⊆ ⇑(AlgEquiv.restrictNormalHom ↥L) ⁻¹' N

Tactic:
intro x hx
    apply hO
    simp only [SetLike.mem_coe, IntermediateField.mem_fixingSubgroup_iff] at hx ⊢
    intro y hy
    have := AlgEquiv.restrictNormal_commutes x L y
    dsimp at this
    rw [hx y.1 ((IntermediateField.mem_lift y).mpr hy)] at this
    exact SetLike.coe_eq_coe.mp this

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✝ : (Classical.choose ⋯).2 ^ p ^ n - y ^ p ^ n' ∈ RingHom.ker i
m : ℕ
h : ((Classical.choose ⋯).2 ^ p ^ n - y ^ p ^ n') ^ p ^ m = 0
⊢ (iterateFrobeniusEquiv M p (m + n)) (j (Classical.choose ⋯).2) =
    (iterateFrobeniusEquiv M p (m + (n + n'))) ((iterateFrobeniusEquiv M p n).symm (j y))

Tactic:
add_comm n n',

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
m : ℕ
h : ((Classical.choose ⋯).2 ^ p ^ n - y ^ p ^ n') ^ p ^ m = 0
⊢ (iterateFrobeniusEquiv M p (m + n)) (j (Classical.choose ⋯).2) =
    (iterateFrobeniusEquiv M p (m + (n' + n))) ((iterateFrobeniusEquiv M p n).symm (j y))
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: case isFalse
K : Type u
inst✝¹ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
inst✝ : NeZero n
σ : Gal(K[n√a]/K)
this✝¹ : Fact (Irreducible (X ^ n - C a)) := { out := H }
this✝ : IsDomain K[n√a] := inferInstance
this : DecidableEq K := Classical.decEq K
h✝ : ¬a = 0
⊢ (algebraMap K K[n√a]) a ≠ 0

Tactic:
Ne,

Goal state after:
case isFalse
K : Type u
inst✝¹ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
inst✝ : NeZero n
σ : Gal(K[n√a]/K)
this✝¹ : Fact (Irreducible (X ^ n - C a)) := { out := H }
this✝ : IsDomain K[n√a] := inferInstance
this : DecidableEq K := Classical.decEq K
h✝ : ¬a = 0
⊢ ¬(algebraMap K K[n√a]) a = 0
Module: Mathlib.FieldTheory.JacobsonNoether

Goal state before:
pp: case e_6
L : Type u_2
D : Type u_3
inst✝⁴ : Field L
inst✝³ : DivisionRing D
inst✝² : Algebra L D
inst✝¹ : Algebra.IsAlgebraic L D
inst✝ : IsCentral L D
hneq : ⊥ ≠ ⊤
hcenter : Subalgebra.center L D = ⊥
ntrivial : k ≠ ⊤
φ : ↥⊥ ≃ₐ[L] ↥(Subalgebra.center L D) := ⋯
equiv : L ≃+* ↥k := ⋯
x✝² : Algebra L ↥k := ⋯
x✝¹ : Algebra (↥k) L := ⋯
x✝ : IsScalarTower L (↥k) D
x : ↥k
⊢ x = (algebraMap L ↥k) ((algebraMap (↥k) L) x)

Tactic:
exact (equiv.apply_symm_apply x).symm

Goal state after:
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
⊢ (X ^ n - C ((algebraMap K K[n√a]) a)).Splits

Tactic:
have ⟨_, hζ⟩ := hζ

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
w✝ : K
hζ : w✝ ∈ primitiveRoots n K
⊢ (X ^ n - C ((algebraMap K K[n√a]) a)).Splits
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
⊢ normalizedTraceAux F K (f a) = normalizedTraceAux F E a

Tactic:
by
  let e := (F⟮a⟯.equivMap f).trans (equivOfEq <| Set.image_singleton ▸ adjoin_map F {a} f)
  simp_rw [normalizedTraceAux, ← LinearEquiv.finrank_eq e.toLinearEquiv]
  congr
  exact trace_eq_of_algEquiv e <| AdjoinSimple.gen F a

Goal state after:
Module: Mathlib.FieldTheory.LinearDisjoint

Goal state before:
pp: F : Type u
E : Type v
inst✝²⁰ : Field F
inst✝¹⁹ : Field E
inst✝¹⁸ : Algebra F E
L : Type w
inst✝¹⁷ : Field L
inst✝¹⁶ : Algebra F L
inst✝¹⁵ : Algebra L E
inst✝¹⁴ : IsScalarTower F L E
L' : Type u_1
inst✝¹³ : Field L'
inst✝¹² : Algebra F L'
inst✝¹¹ : Algebra L' E
inst✝¹⁰ : IsScalarTower F L' E
H : (IsScalarTower.toAlgHom F L E).fieldRange.LinearDisjoint (IsScalarTower.toAlgHom F L' E).range
K : Type u_2
inst✝⁹ : Field K
inst✝⁸ : Algebra F K
inst✝⁷ : Algebra L K
inst✝⁶ : IsScalarTower F L K
inst✝⁵ : Algebra L' K
inst✝⁴ : IsScalarTower F L' K
inst✝³ : Algebra E K
inst✝² : IsScalarTower F E K
inst✝¹ : IsScalarTower L E K
inst✝ : IsScalarTower L' E K
this :
  ((IsScalarTower.toAlgHom F E K).comp (IsScalarTower.toAlgHom F L E)).range.LinearDisjoint
    ((IsScalarTower.toAlgHom F E K).comp (IsScalarTower.toAlgHom F L' E)).range
⊢ (IsScalarTower.toAlgHom F L K).range.LinearDisjoint (IsScalarTower.toAlgHom F L' K).range

Tactic:
convert! this <;> (ext; exact IsScalarTower.algebraMap_apply _ E K _)

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Semiring T
inst✝ : Algebra R T
⊢ ∀ (x : ↥includeLeft.range) (y : ↥includeRight.range),
    (_root_.TensorProduct.map includeLeft.toLinearMap.rangeRestrict includeRight.toLinearMap.rangeRestrict ∘ₗ
          includeLeft.toLinearMap.range.mulMap includeRight.toLinearMap.range)
        (x ⊗ₜ[R] y) =
      LinearMap.id (x ⊗ₜ[R] y)

Tactic:
rintro ⟨x', x, rfl : x ⊗ₜ 1 = x'⟩ ⟨y', y, rfl : 1 ⊗ₜ y = y'⟩

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Semiring T
inst✝ : Algebra R T
x : S
y : T
⊢ (_root_.TensorProduct.map includeLeft.toLinearMap.rangeRestrict includeRight.toLinearMap.rangeRestrict ∘ₗ
        includeLeft.toLinearMap.range.mulMap includeRight.toLinearMap.range)
      (⟨x ⊗ₜ[R] 1, ⋯⟩ ⊗ₜ[R] ⟨1 ⊗ₜ[R] y, ⋯⟩) =
    LinearMap.id (⟨x ⊗ₜ[R] 1, ⋯⟩ ⊗ₜ[R] ⟨1 ⊗ₜ[R] y, ⋯⟩)