mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Vector.Mem

Goal state before:
pp: α : Type u_1
β : Type u_2
n : ℕ
b : β
v : Vector α (n + 1)
f : α → β
⊢ b ∈ (map f v).toList ↔ f v.head = b ∨ ∃ a, a ∈ v.tail.toList ∧ f a = b

Tactic:
by
  rw [mem_succ_iff, head_map, tail_map, mem_map_iff, @eq_comm _ b]

Goal state after:
Module: Mathlib.Data.Sum.Interval

Goal state before:
pp: case refine_4.inr.inr
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f₁ : α₁ → β₁ → Finset γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
val✝¹ : α₂
val✝ : β₂
h :
  (∀ (a₁ : α₁) (b₁ : β₁), inr val✝¹ = inl a₁ → inr val✝ = inl b₁ → f₁ a₁ b₁ = ∅) ∧
    (∀ (a₁ : α₁) (b₂ : β₂), inr val✝¹ = inl a₁ → inr val✝ = inr b₂ → g₁ a₁ b₂ = ∅ ∧ g₂ a₁ b₂ = ∅) ∧
      ∀ (a₂ : α₂) (b₂ : β₂), inr val✝¹ = inr a₂ → inr val✝ = inr b₂ → f₂ a₂ b₂ = ∅
⊢ sumLexLift f₁ f₂ g₁ g₂ (inr val✝¹) (inr val✝) = ∅

Tactic:
· exact map_eq_empty.2 (h.2.2 _ _ rfl rfl)

Goal state after:
Module: Mathlib.MeasureTheory.Measure.ContinuousPreimage

Goal state before:

Tactic:
μ ((f a ⁻¹' s) ∆ (g ⁻¹' s))
        ≤ μ ((f a ⁻¹' s) ∆ (f a ⁻¹' U)) + μ ((f a ⁻¹' U) ∆ (g ⁻¹' U))
          + μ ((g ⁻¹' U) ∆ (g ⁻¹' s)) := by
        refine (measure_symmDiff_le _ (g ⁻¹' U) _).trans ?_
        gcongr
        apply measure_symmDiff_le
      _ ≤ ε / 3 + ε / 3 + ε / 3 := by
        gcongr
        · rwa [← preimage_symmDiff, hfa.measure_preimage (hs.symmDiff hmU), symmDiff_comm]
        · rwa [← preimage_symmDiff, hg.measure_preimage (hmU.symmDiff hs)]
      _ = ε := by simp

Goal state after:
Module: Mathlib.Dynamics.Ergodic.Conservative

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
k : ℕ
⊢ ∀ᵐ (a : α) ∂μ, f^[k] a ∈ s → ∃ᶠ (n : ℕ) in atTop, f^[n] a ∈ s

Tactic:
refine (hf.ae_mem_imp_frequently_image_mem
    (hs.preimage <| hf.toQuasiMeasurePreserving.iterate k)).mono fun x hx hk => ?_

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
k : ℕ
x : α
hx : x ∈ f^[k] ⁻¹' s → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ f^[k] ⁻¹' s
hk : f^[k] x ∈ s
⊢ ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s
Module: Mathlib.Dynamics.Flow

Goal state before:
pp: τ : Type u_1
α : Type u_2
inst✝² : TopologicalSpace τ
inst✝¹ : TopologicalSpace α
inst✝ : AddZero τ
f₁ : τ → α → α
cont'✝¹ : Continuous (uncurry f₁)
map_add'✝¹ : ∀ (t₁ t₂ : τ) (x : α), f₁ (t₁ + t₂) x = f₁ t₁ (f₁ t₂ x)
map_zero'✝¹ : ∀ (x : α), f₁ 0 x = x
f₂ : τ → α → α
cont'✝ : Continuous (uncurry f₂)
map_add'✝ : ∀ (t₁ t₂ : τ) (x : α), f₂ (t₁ + t₂) x = f₂ t₁ (f₂ t₂ x)
map_zero'✝ : ∀ (x : α), f₂ 0 x = x
h :
  ∀ (t : τ) (x : α),
    { toFun := f₁, cont' := cont'✝¹, map_add' := map_add'✝¹, map_zero' := map_zero'✝¹ }.toFun t x =
      { toFun := f₂, cont' := cont'✝, map_add' := map_add'✝, map_zero' := map_zero'✝ }.toFun t x
⊢ f₁ = f₂

Tactic:
funext

Goal state after:
τ : Type u_1
α : Type u_2
inst✝² : TopologicalSpace τ
inst✝¹ : TopologicalSpace α
inst✝ : AddZero τ
f₁ : τ → α → α
cont'✝¹ : Continuous (uncurry f₁)
map_add'✝¹ : ∀ (t₁ t₂ : τ) (x : α), f₁ (t₁ + t₂) x = f₁ t₁ (f₁ t₂ x)
map_zero'✝¹ : ∀ (x : α), f₁ 0 x = x
f₂ : τ → α → α
cont'✝ : Continuous (uncurry f₂)
map_add'✝ : ∀ (t₁ t₂ : τ) (x : α), f₂ (t₁ + t₂) x = f₂ t₁ (f₂ t₂ x)
map_zero'✝ : ∀ (x : α), f₂ 0 x = x
h :
  ∀ (t : τ) (x : α),
    { toFun := f₁, cont' := cont'✝¹, map_add' := map_add'✝¹, map_zero' := map_zero'✝¹ }.toFun t x =
      { toFun := f₂, cont' := cont'✝, map_add' := map_add'✝, map_zero' := map_zero'✝ }.toFun t x
x✝¹ : τ
x✝ : α
⊢ f₁ x✝¹ x✝ = f₂ x✝¹ x✝
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
pp: X : Type u_1
T : X → X
U : SetRel X X
n : ℕ
s : Finset X
⊢ IsDynNetIn T ∅ U n ↑s → ↑s.card = ⊥

Tactic:
s_net

Goal state after:
X : Type u_1
T : X → X
U : SetRel X X
n : ℕ
s : Finset X
s_net : IsDynNetIn T ∅ U n ↑s
⊢ ↑s.card = ⊥
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
x : α
hx : μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)) x = μ.rnDeriv ν x
⊢ (μ.rnDeriv ν)⁻¹ x = (μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)))⁻¹ x

Tactic:
simp only [Pi.inv_apply, inv_inj]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
x : α
hx : μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)) x = μ.rnDeriv ν x
⊢ μ.rnDeriv ν x = μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)) x
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 := ⋯
U : Set (X × X)
V : Set (Y × Y)
V_uni : V ∈ 𝓤 Y
V_sub : Prod.map φ φ ⁻¹' V ⊆ U
W : Set (Y × Y)
W_uni : W ∈ 𝓤 Y
W_symm : SetRel.IsSymm W
W_V : W ○ W ⊆ V
⊢ (fun U ↦ coverEntropyEntourage S F U) (Prod.map φ φ ⁻¹' (W ○ W)) ≤ coverEntropy T (φ '' F)

Tactic:
apply (le_coverEntropyEntourage_image h F).trans

Goal state after:
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 := ⋯
U : Set (X × X)
V : Set (Y × Y)
V_uni : V ∈ 𝓤 Y
V_sub : Prod.map φ φ ⁻¹' V ⊆ U
W : Set (Y × Y)
W_uni : W ∈ 𝓤 Y
W_symm : SetRel.IsSymm W
W_V : W ○ W ⊆ V
⊢ coverEntropyEntourage T (φ '' F) W ≤ coverEntropy T (φ '' F)
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:
funext_iff.not,

Goal state after:
case h'
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
⊢ ¬∀ (x : ℕ), ↑(netMaxcard T F U x) = 0 x
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
⊢ ¬(fun n ↦ ↑(coverMincard T F U n)) = 0

Tactic:
funext_iff.not,

Goal state after:
case h'
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
⊢ ¬∀ (x : ℕ), ↑(coverMincard T F U x) = 0 x
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
⊢ (fun x ↦ (map f (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν) (f x)) =ᵐ[ν]
    (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv ν

Tactic:
Measure.map_add _ _ hf.measurable

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
⊢ (fun x ↦ (map f (μ.singularPart ν) + map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν) (f x)) =ᵐ[ν]
    (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
Module: Mathlib.FieldTheory.IsAlgClosed.Classification

Goal state before:
pp: K : Type u
L : Type v
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : IsAlgClosed K
inst✝³ : IsAlgClosed L
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
⊢ Nonempty (K ≃+* L)

Tactic:
by
  let : Algebra (ZMod p) K := ZMod.algebra _ _
  let : Algebra (ZMod p) L := ZMod.algebra _ _
  obtain ⟨s, hs⟩ := exists_isTranscendenceBasis (ZMod p) K
  obtain ⟨t, ht⟩ := exists_isTranscendenceBasis (ZMod p) L
  have hL : ℵ₀ < #L := by
    rwa [← aleph0_lt_lift.{v, u}, ← lift_mk_eq'.2 hKL, aleph0_lt_lift]
  have : Cardinal.lift.{v} #s = Cardinal.lift.{u} #t := by
    rw [← lift_injective (cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt _
        hs (le_of_lt (lt_aleph0_of_finite _)) hK),
      ← lift_injective (cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt _
        ht (le_of_lt (lt_aleph0_of_finite _)) hL)]
    exact Cardinal.lift_mk_eq'.2 hKL
  obtain ⟨e⟩ := Cardinal.lift_mk_eq'.1 this
  exact ⟨equivOfTranscendenceBasis _ _ e hs ht⟩

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case refine_1
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
n : ℕ
hn : n ≠ 0
p : F[X]
h1 : p ≠ 0
h2 : (aeval (x ^ n)) p = 0
h : p.leadingCoeff * 1 ^ p.natDegree = 0
⊢ p.leadingCoeff = 0

pp: case refine_1
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
n : ℕ
hn : n ≠ 0
p : F[X]
h1 : p ≠ 0
h2 : (aeval (x ^ n)) p = 0
h : (p.comp (X ^ n)).leadingCoeff = 0
⊢ (X ^ n).natDegree ≠ 0

Tactic:
one_pow,

Goal state after:
case refine_1
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
n : ℕ
hn : n ≠ 0
p : F[X]
h1 : p ≠ 0
h2 : (aeval (x ^ n)) p = 0
h : p.leadingCoeff * 1 = 0
⊢ p.leadingCoeff = 0

case refine_1
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
n : ℕ
hn : n ≠ 0
p : F[X]
h1 : p ≠ 0
h2 : (aeval (x ^ n)) p = 0
h : (p.comp (X ^ n)).leadingCoeff = 0
⊢ (X ^ n).natDegree ≠ 0
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case func
L : Language
α : Type u'
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term α
ih : ∀ (a : Fin l✝), (LHom.id L).onTerm (_ts✝ a) = id (_ts✝ a)
⊢ (LHom.id L).onTerm (func _f✝ _ts✝) = id (func _f✝ _ts✝)

Tactic:
simp_rw [onTerm, ih]; rfl

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case func
L : Language
L' : Language
α : Type u'
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term α
ih : ∀ (a : Fin l✝), (φ.comp ψ).onTerm (_ts✝ a) = (φ.onTerm ∘ ψ.onTerm) (_ts✝ a)
⊢ (φ.comp ψ).onTerm (func _f✝ _ts✝) = (φ.onTerm ∘ ψ.onTerm) (func _f✝ _ts✝)

Tactic:
simp_rw [onTerm, ih]; rfl

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
φ : L ≃ᴸ L'
⊢ Function.LeftInverse φ.invLHom.onTerm φ.toLHom.onTerm

Tactic:
rw [Function.leftInverse_iff_comp, ← LHom.comp_onTerm, φ.left_inv, LHom.id_onTerm]

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:
exact add_assoc

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
n : ℕ
φ : L.Formula (Fin n)
v : Empty → M
x : Fin n → M
⊢ (BoundedFormula.relabel Sum.inr φ).Realize v x ↔ φ.Realize x

Tactic:
rw [BoundedFormula.realize_relabel, Formula.Realize, Sum.elim_comp_inr, Fin.castAdd_zero,
    cast_refl, Function.comp_id,
    Subsingleton.elim (x ∘ (natAdd n : Fin 0 → Fin n)) default]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case succ.mp
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n✝ : ℕ
v : α → M
n : ℕ
ih : ∀ {φ : L.BoundedFormula α n}, φ.exs.Realize v ↔ ∃ xs, φ.Realize v xs
φ : L.BoundedFormula α (n + 1)
xs : Fin n → M
x : M
h : φ.Realize v (snoc xs x)
⊢ ∃ xs, φ.Realize v xs

Tactic:
exact ⟨_, h⟩

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case all
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ (v : α ⊕ Fin (n✝ + 1) → M), f✝.toFormula.Realize v ↔ f✝.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
v : α ⊕ Fin n✝ → M
a : M
h :
  f✝.toFormula.Realize (Sum.elim (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)) ↔ f✝.Realize (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)
⊢ (relabel (Sum.elim (Sum.inl ∘ Sum.inl) (Sum.map Sum.inr id ∘ ⇑finSumFinEquiv.symm)) f✝.toFormula).Realize v
      (snoc default a) ↔
    f✝.Realize (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)

Tactic:
← h,

Goal state after:
case all
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ (v : α ⊕ Fin (n✝ + 1) → M), f✝.toFormula.Realize v ↔ f✝.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
v : α ⊕ Fin n✝ → M
a : M
h :
  f✝.toFormula.Realize (Sum.elim (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)) ↔ f✝.Realize (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)
⊢ (relabel (Sum.elim (Sum.inl ∘ Sum.inl) (Sum.map Sum.inr id ∘ ⇑finSumFinEquiv.symm)) f✝.toFormula).Realize v
      (snoc default a) ↔
    f✝.toFormula.Realize (Sum.elim (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a))
Module: Mathlib.ModelTheory.Skolem

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
κ : Cardinal.{w'}
h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ
h4 : lift.{w, w'} κ ≤ lift.{w', w} #M
s' : Set (ULift.{w', w} M)
h2 : lift.{w', w} #↑s ≤ #↑s'
h1 : ℵ₀ ≤ #↑s'
hs' : #↑s' = lift.{w, w'} κ
this : Nonempty M
h : lift.{w', w} #↑(⇑Equiv.ulift '' s') = #↑s'
⊢ lift.{w', w} #↥((closure (L.sum L.skolem₁)).toFun (s ∪ ⇑Equiv.ulift '' s')) = #↑s'

Tactic:
← h,

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
κ : Cardinal.{w'}
h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ
h4 : lift.{w, w'} κ ≤ lift.{w', w} #M
s' : Set (ULift.{w', w} M)
h2 : lift.{w', w} #↑s ≤ #↑s'
h1 : ℵ₀ ≤ #↑s'
hs' : #↑s' = lift.{w, w'} κ
this : Nonempty M
h : lift.{w', w} #↑(⇑Equiv.ulift '' s') = #↑s'
⊢ lift.{w', w} #↥((closure (L.sum L.skolem₁)).toFun (s ∪ ⇑Equiv.ulift '' s')) = lift.{w', w} #↑(⇑Equiv.ulift '' s')
Module: Mathlib.ModelTheory.Skolem

Goal state before:
pp: case refine_2
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
κ : Cardinal.{w'}
h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ
h4 : lift.{w, w'} κ ≤ lift.{w', w} #M
s' : Set (ULift.{w', w} M)
h2 : lift.{w', w} #↑s ≤ #↑s'
h1 : ℵ₀ ≤ #↑s'
hs' : #↑s' = lift.{w, w'} κ
this : Nonempty M
h : lift.{w', w} #↑(⇑Equiv.ulift '' s') = #↑s'
⊢ lift.{max u v, max w w'} #↑s' ≤ lift.{max (max u v) w', w} #↑(⇑Equiv.ulift '' s')

Tactic:
← h,

Goal state after:
case refine_2
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
κ : Cardinal.{w'}
h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ
h4 : lift.{w, w'} κ ≤ lift.{w', w} #M
s' : Set (ULift.{w', w} M)
h2 : lift.{w', w} #↑s ≤ #↑s'
h1 : ℵ₀ ≤ #↑s'
hs' : #↑s' = lift.{w, w'} κ
this : Nonempty M
h : lift.{w', w} #↑(⇑Equiv.ulift '' s') = #↑s'
⊢ lift.{max u v, max w w'} (lift.{w', w} #↑(⇑Equiv.ulift '' s')) ≤ lift.{max (max u v) w', w} #↑(⇑Equiv.ulift '' s')
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
h : ∃ M, Infinite ↑M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
⊢ ∃ N, #↑N = κ

Tactic:
by
  cases h with
  | intro M MI =>
    obtain ⟨N, hN, rfl⟩ := exists_elementarilyEquivalent_card_eq L M κ h1 h2
    have : Nonempty N := hN.nonempty
    exact ⟨hN.theory_model.bundled, rfl⟩

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

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

Tactic:
simp only [Finset.coe_union, Finset.coe_singleton]

Goal state after:
L : Language
T : L.Theory
φ : L.Sentence
this : DecidableEq L.Sentence := Classical.decEq L.Sentence
h : ∀ (T0 : Finset L.Sentence), ↑T0 ⊆ T ∪ {Formula.not φ} → IsSatisfiable ↑T0
T0 : Finset L.Sentence
hT0 : ↑T0 ⊆ T
⊢ ↑T0 ∪ {Formula.not φ} ⊆ T ∪ {Formula.not φ}
Module: Mathlib.SetTheory.Cardinal.Divisibility

Goal state before:
pp: case inr
a : Cardinal.{u}
h : IsUnit a
ha : a ≠ 0
⊢ a = 1

Tactic:
rw [isUnit_iff_forall_dvd] at h

Goal state after:
case inr
a : Cardinal.{u}
h : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
⊢ a = 1
Module: Mathlib.FieldTheory.Finite.Extension

Goal state before:
pp: k : Type u_1
inst✝⁶ : Field k
inst✝⁵ : Finite k
p : ℕ
inst✝⁴ : Fact (Nat.Prime p)
inst✝³ : CharP k p
n : ℕ
inst✝² : NeZero n
l : Type u_2
inst✝¹ : Field l
inst✝ : Algebra k l
h : Module.finrank k l = n
this✝¹ : Module.Finite k l
this✝ : Finite l
this : Fintype l
⊢ IsSplittingField k l (X ^ Nat.card k ^ n - X)

Tactic:
← h,

Goal state after:
k : Type u_1
inst✝⁶ : Field k
inst✝⁵ : Finite k
p : ℕ
inst✝⁴ : Fact (Nat.Prime p)
inst✝³ : CharP k p
n : ℕ
inst✝² : NeZero n
l : Type u_2
inst✝¹ : Field l
inst✝ : Algebra k l
h : Module.finrank k l = n
this✝¹ : Module.Finite k l
this✝ : Finite l
this : Fintype l
⊢ IsSplittingField k l (X ^ Nat.card k ^ Module.finrank k l - X)
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: case neg.inr
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
x : R
hp✝ : ¬1 < p
x✝ : ∃ n, x ^ p ^ n = 0
n : ℕ
h : x ^ 1 ^ n = 0
hp : p = 1
⊢ x = 0

Tactic:
one_pow,

Goal state after:
case neg.inr
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
x : R
hp✝ : ¬1 < p
x✝ : ∃ n, x ^ p ^ n = 0
n : ℕ
h : x ^ 1 = 0
hp : p = 1
⊢ x = 0
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing K
inst✝⁷ : CommRing L
inst✝⁶ : CommRing M
inst✝⁵ : CommRing N
i : K →+* L
j : K →+* M
k : K →+* N
f : L →+* M
g : L →+* N
p : ℕ
inst✝⁴ : ExpChar M p
inst✝³ : ExpChar K p
inst✝² : PerfectRing M p
inst✝¹ : IsPRadical i p
inst✝ : ExpChar L p
⊢ i 1 = 1 ^ p ^ 0

Tactic:
one_pow,

Goal state after:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing K
inst✝⁷ : CommRing L
inst✝⁶ : CommRing M
inst✝⁵ : CommRing N
i : K →+* L
j : K →+* M
k : K →+* N
f : L →+* M
g : L →+* N
p : ℕ
inst✝⁴ : ExpChar M p
inst✝³ : ExpChar K p
inst✝² : PerfectRing M p
inst✝¹ : IsPRadical i p
inst✝ : ExpChar L p
⊢ i 1 = 1
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✝¹ : PerfectClosure K p
x : ℕ × K
x✝ : IsNilpotent (mk K p x)
n : ℕ
h : mk K p x ^ n = 0
⊢ mk K p x = 0

Tactic:
by
    replace h : mk K p x ^ p ^ n = 0 := by
      rw [← Nat.sub_add_cancel ((n.lt_pow_self (Fact.out : p.Prime).one_lt).le),
        pow_add, h, mul_zero]
    simp only [zero_def, mk_pow, mk_eq_iff, zero_add, ← coe_iterateFrobenius, map_zero] at h ⊢
    obtain ⟨m, h⟩ := h
    exact ⟨n + m, by simpa only [iterateFrobenius_def, pow_add, pow_mul] using h⟩

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

Goal state before:
pp: case inr
R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
hx : IsSquare x
n : ℕ
hk : -↑n ≠ 0
⊢ ∃ r, x = r ^ (-↑n)

Tactic:
rcases exists_eq_pow_of_isSquare hx (by simpa using hk) with ⟨r, hr⟩

Goal state after:
case inr
R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
hx : IsSquare x
n : ℕ
hk : -↑n ≠ 0
r : R
hr : x = r ^ n
⊢ ∃ r, x = r ^ (-↑n)
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
x : K
⊢ (⇑(frobenius (PerfectClosure K p) p))^[n] (mk K p (n, x)) = (of K p) x

Tactic:
induction n with
  | zero => rfl
  | succ n ih => rw [iterate_succ_apply, ← ih, frobenius_mk, mk_succ_pow]

Goal state after:
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
c : Set G
x : G
hj' : ↑(g j) = ↑x
hi' : ↑(g i) = ↑x
hx : x ∈ c
⊢ x ∈ ⊥

Tactic:
← Subtype.mk.injEq (p := (· ∈ (s : Set ι))) i hi j hj

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, hi⟩ = ⟨j, hj⟩
c : Set G
x : G
hj' : ↑(g j) = ↑x
hi' : ↑(g i) = ↑x
hx : x ∈ c
⊢ x ∈ ⊥
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:
simp_rw [laurent_div, taylor_taylor]

Goal state after:
Module: Mathlib.FieldTheory.JacobsonNoether

Goal state before:
pp: D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
H : k ≠ ⊤
p : ℕ
hp : ExpChar D p
insep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
a : D
ha : a ∉ k
ha₀ : a ≠ 0
b : D
hb1 : ((ad (↥k) D) a) b ≠ 0
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 := ⋯ }
hc : a * c = c * a
d : D := c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b
hd_def : d = c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b
hc' : c⁻¹ * a = a * c⁻¹
c_eq : a * (⇑((ad (↥k) D) a))^[n - 1] b - (⇑((ad (↥k) D) a))^[n - 1] b * a = c
eq1 : c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b - c⁻¹ * (⇑((ad (↥k) D) a))^[n - 1] b * a = 1
r : ℕ
hr : d ^ p ^ r ∈ k
deq : d ^ p ^ r = 1 ^ p ^ r + (a⁻¹ * d * a) ^ p ^ r
⊢ False

Tactic:
one_pow,

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 := ⋯ }
hc : a * c = c * a
d : D := c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b
hd_def : d = c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b
hc' : c⁻¹ * a = a * c⁻¹
c_eq : a * (⇑((ad (↥k) D) a))^[n - 1] b - (⇑((ad (↥k) D) a))^[n - 1] b * a = c
eq1 : c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b - c⁻¹ * (⇑((ad (↥k) D) a))^[n - 1] b * a = 1
r : ℕ
hr : d ^ p ^ r ∈ k
deq : d ^ p ^ r = 1 + (a⁻¹ * d * a) ^ p ^ r
⊢ False
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)
α : L
hα : α ^ n = (algebraMap K L) a
⊢ adjoin K (⇑↑(adjoinRootXPowSubCEquiv hζ H hα).symm '' {α}) = ⊤

Tactic:
Set.image_singleton,

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)
α : L
hα : α ^ n = (algebraMap K L) a
⊢ K [↑(adjoinRootXPowSubCEquiv hζ H hα).symm α] = ⊤
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: case refine_1
K : Type u
inst✝⁵ : Field K
L : Type u_1
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
inst✝¹ : IsGalois K L
inst✝ : IsCyclic Gal(L/K)
ζ : K
hζ : IsPrimitiveRoot ζ (finrank K L)
σ : Gal(L/K)
hσ : Function.Surjective fun x ↦ σ ^ x
hσ'✝ : orderOf σ = Nat.card Gal(L/K)
this : (minpoly K σ.toLinearMap).IsRoot ζ
v : L
hv : End.HasEigenvector σ.toLinearMap ζ v
hv' : ∀ (n : ℕ), (σ ^ n) v = ζ ^ n • v
n : ℕ
hσ' : σ ^ n ∈ OrderDual.ofDual ⊥
⊢ 1 ^ n • v ^ finrank K L = v ^ finrank K L

Tactic:
one_pow,

Goal state after:
case refine_1
K : Type u
inst✝⁵ : Field K
L : Type u_1
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
inst✝¹ : IsGalois K L
inst✝ : IsCyclic Gal(L/K)
ζ : K
hζ : IsPrimitiveRoot ζ (finrank K L)
σ : Gal(L/K)
hσ : Function.Surjective fun x ↦ σ ^ x
hσ'✝ : orderOf σ = Nat.card Gal(L/K)
this : (minpoly K σ.toLinearMap).IsRoot ζ
v : L
hv : End.HasEigenvector σ.toLinearMap ζ v
hv' : ∀ (n : ℕ), (σ ^ n) v = ζ ^ n • v
n : ℕ
hσ' : σ ^ n ∈ OrderDual.ofDual ⊥
⊢ 1 • v ^ finrank K L = v ^ finrank K L
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: K : Type u
inst✝³ : Field K
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
a : K
α : L
ha : α ^ finrank K L = (algebraMap K L) a
hα : K⟮α⟯ = ⊤
this : X ^ finrank K L - C a = minpoly K α
⊢ Irreducible (X ^ finrank K L - C a)

Tactic:
exact this ▸ minpoly.irreducible (IsIntegral.of_finite K α)

Goal state after: