mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Dynamics.Ergodic.Action.Regular

Goal state before:
pp: G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulLeftInvariant
s : Set G
hsm : MeasurableSet s
hs : ∀ (g : G), (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s
this : (∃ᵐ (x : G) ∂μ, x ∈ s) → ∀ᵐ (x : G) ∂μ, x ∈ s
⊢ EventuallyConst s (ae μ)

Tactic:
by
    simp only [eventuallyConst_set, ← not_frequently]
    exact or_not_of_imp this

Goal state after:
Module: Mathlib.Dynamics.Ergodic.Action.Regular

Goal state before:
pp: G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulRightInvariant
s : Set G
hsm : MeasurableSet s
hs : ∀ (g : Gᵐᵒᵖ), (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s
this : (∃ᵐ (x : G) ∂μ, x ∈ s) → ∀ᵐ (x : G) ∂μ, x ∈ s
⊢ EventuallyConst s (ae μ)

Tactic:
by
    simp only [eventuallyConst_set, ← not_frequently]
    exact or_not_of_imp this

Goal state after:
Module: Mathlib.MeasureTheory.Group.AddCircle

Goal state before:
pp: case inl
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : ε ≤ 0
⊢ closedBall x ε =ᵐ[volume] ball x ε

Tactic:
ball_eq_empty.mpr hε,

Goal state after:
case inl
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : ε ≤ 0
⊢ closedBall x ε =ᵐ[volume] ∅
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
hν_ac : ν ≪ ν.withDensity f
this : SigmaFinite (ν.withDensity f)
⊢ μ.singularPart ν ⟂ₘ ν.withDensity f

Tactic:
exact ((mutuallySingular_singularPart μ ν).symm.withDensity).symm

Goal state after:
Module: Mathlib.Dynamics.FixedPoints.Support

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
f g : X → X
hf : ∃ K, IsClosed K ∧ IsCompact K ∧ (fixedPoints f)ᶜ ⊆ K
hg : ∃ K, IsClosed K ∧ IsCompact K ∧ (fixedPoints g)ᶜ ⊆ K
⊢ ∃ K, IsClosed K ∧ IsCompact K ∧ (fixedPoints (f ∘ g))ᶜ ⊆ K

Tactic:
obtain ⟨K, hK₁, hK₂, hf⟩ := hf

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
f g : X → X
hg : ∃ K, IsClosed K ∧ IsCompact K ∧ (fixedPoints g)ᶜ ⊆ K
K : Set X
hK₁ : IsClosed K
hK₂ : IsCompact K
hf : (fixedPoints f)ᶜ ⊆ K
⊢ ∃ K, IsClosed K ∧ IsCompact K ∧ (fixedPoints (f ∘ g))ᶜ ⊆ K
Module: Mathlib.Dynamics.SymbolicDynamics.Basic

Goal state before:
pp: case mp
A : Type u_1
inst✝² : Inhabited A
G : Type u_2
inst✝¹ : Monoid G
inst✝ : IsLeftCancelMul G
p : Pattern A G
g : G
x : G → A
H : x ∈ {x | p.mulOccursInAt x g}
w : G
hw : w ∈ p.support
hu : g * w ∈ Finset.image (fun x ↦ g * x) p.support
hx : x (g * w) = p.config w
⊢ x (g * w) = p.mulShift g (g * w)

Tactic:
simpa [Pattern.mulShift_apply_mul_left_of_mem (p := p) (v := g) (w := w) hw] using hx

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Function.Semiconj φ S T
U : Set (Y × Y)
n k : ℕ
x✝ : k < n
⊢ (map T T)^[k] ∘ map φ φ ⁻¹' U = map φ φ ∘ (map S S)^[k] ⁻¹' U

Tactic:
map_iterate S S k,

Goal state after:
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Function.Semiconj φ S T
U : Set (Y × Y)
n k : ℕ
x✝ : k < n
⊢ (map T T)^[k] ∘ map φ φ ⁻¹' U = map φ φ ∘ map S^[k] S^[k] ⁻¹' U
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
pp: case mp
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : netMaxcard T F U n < ⊤
k : ℕ
k_max : ↑k = ↑(sSup (Finset.card '' {s | IsDynNetIn T F U n ↑s}))
this : netMaxcard T F U n = sSup (WithTop.some '' Finset.card '' {s | IsDynNetIn T F U n ↑s})
h_bdda : BddAbove (Finset.card '' {s | IsDynNetIn T F U n ↑s})
h_nemp : (Finset.card '' {s | IsDynNetIn T F U n ↑s}).Nonempty
key : ∃ x, IsDynNetIn T F U n ↑x ∧ x.card = k
⊢ ∃ s, IsDynNetIn T F U n ↑s ∧ s.card = k

Tactic:
exact key

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

Goal state before:
pp: X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h_fin : coverMincard T F U n < ⊤
k : ℕ
k_min : ↑k = ⨅ x, ↑(#↑x)
this : Nonempty { s // IsDynCoverOf T F U n ↑s }
key : ∃ a, IsDynCoverOf T F U n ↑a ∧ #a = k
⊢ ∃ s, IsDynCoverOf T F U n ↑s ∧ #s = k

Tactic:
exact key

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

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

Tactic:
obtain ⟨s, s_cover, s_coverMincard⟩ := (coverMincard_finite_iff T F U m).1 h

Goal state after:
case inr.inr.inr
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
F_inv : MapsTo T F F
inst✝ : U.IsSymm
m n : ℕ
F_nonempty : F.Nonempty
hn : n ≠ 0
h : coverMincard T F U m < ⊤
s : Finset X
s_cover : IsDynCoverOf T F U m ↑s
s_coverMincard : ↑(#s) = coverMincard T F U m
⊢ coverMincard T F (U ○ U) (m * n) ≤ coverMincard T F U m ^ n
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

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

Tactic:
· obtain ⟨s, s_cover, s_coverMincard⟩ := (coverMincard_finite_iff T F U m).1 h
    obtain ⟨t, t_cover, t_sn⟩ := s_cover.iterate_le_pow F_inv n
    rw [← s_coverMincard]
    exact t_cover.coverMincard_le_card.trans (WithTop.coe_le_coe.2 t_sn)

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

Goal state before:
pp: X : Type u_1
inst✝ : UniformSpace X
ι : Sort u_2
p : ι → Prop
s : ι → SetRel X X
h : (𝓤 X).HasBasis p s
T : X → X
F : Set X
U : SetRel X X
U_uni : U ∈ 𝓤 X
i : ι
h_i : p i
si_U : s i ⊆ U
⊢ (fun U ↦ netEntropyInfEntourage T F U) (s i) ≤ ⨆ i, ⨆ (_ : p i), netEntropyInfEntourage T F (s i)

Tactic:
exact le_iSup₂ (f := fun (i : ι) (_ : p i) ↦ netEntropyInfEntourage T F (s i)) i h_i

Goal state after:
Module: Mathlib.Dynamics.Transitive

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : Monoid M
inst✝ : MulAction M α
h : ContinuousConstSMul M α
h₄ : ∀ {U : Set α}, IsOpen U → U.Nonempty → (∀ (m : M), (fun x ↦ m • x) ⁻¹' U ⊆ U) → Dense U
U✝ : Set α
hU : IsOpen U✝
x✝ : U✝.Nonempty
⊢ ((fun x ↦ 1 • x) ⁻¹' U✝).Nonempty

Tactic:
simpa only [one_smul]

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

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

Tactic:
sub_self

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

Goal state before:
pp: L : Language
L' : Language
M : Type w
inst✝ : L.Structure M
L'' : Language
e'✝ : L' ≃ᴸ L''
e✝ e : L ≃ᴸ L'
e' : L' ≃ᴸ L''
⊢ (e.invLHom.comp e'.invLHom).comp (e'.toLHom.comp e.toLHom) = LHom.id L

Tactic:
LHom.comp_assoc,

Goal state after:
L : Language
L' : Language
M : Type w
inst✝ : L.Structure M
L'' : Language
e'✝ : L' ≃ᴸ L''
e✝ e : L ≃ᴸ L'
e' : L' ≃ᴸ L''
⊢ e.invLHom.comp (e'.invLHom.comp (e'.toLHom.comp e.toLHom)) = LHom.id L
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: L : Language
L' : Language
M : Type w
inst✝ : L.Structure M
L'' : Language
e'✝ : L' ≃ᴸ L''
e✝ e : L ≃ᴸ L'
e' : L' ≃ᴸ L''
⊢ (e'.toLHom.comp e.toLHom).comp (e.invLHom.comp e'.invLHom) = LHom.id L''

Tactic:
LHom.comp_assoc,

Goal state after:
L : Language
L' : Language
M : Type w
inst✝ : L.Structure M
L'' : Language
e'✝ : L' ≃ᴸ L''
e✝ e : L ≃ᴸ L'
e' : L' ≃ᴸ L''
⊢ e'.toLHom.comp (e.toLHom.comp (e.invLHom.comp e'.invLHom)) = LHom.id L''
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.comp f.symm).toEmbedding = Embedding.refl L N

Tactic:
self_comp_symm,

Goal state after:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃[L] N
⊢ (refl L N).toEmbedding = Embedding.refl L N
Module: Mathlib.ModelTheory.Basic

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

Tactic:
self_comp_symm,

Goal state after:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃[L] N
⊢ (refl L N).toHom = Hom.id L N
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: case e'_2
L : Language
M : Type w
N : Type w'
inst✝² : L.Structure M
inst✝¹ : L.Structure N
P : Type u_1
inst✝ : L.Structure P
h : M ≃[L] N
f g : N ≃[L] P
hfg : (fun f ↦ f.comp h) f = (fun f ↦ f.comp h) g
⊢ f = f.comp (h.comp h.symm)

Tactic:
self_comp_symm,

Goal state after:
case e'_2
L : Language
M : Type w
N : Type w'
inst✝² : L.Structure M
inst✝¹ : L.Structure N
P : Type u_1
inst✝ : L.Structure P
h : M ≃[L] N
f g : N ≃[L] P
hfg : (fun f ↦ f.comp h) f = (fun f ↦ f.comp h) g
⊢ f = f.comp (refl L N)
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: case e'_3
L : Language
M : Type w
N : Type w'
inst✝² : L.Structure M
inst✝¹ : L.Structure N
P : Type u_1
inst✝ : L.Structure P
h : M ≃[L] N
f g : N ≃[L] P
hfg : (fun f ↦ f.comp h) f = (fun f ↦ f.comp h) g
⊢ g = g.comp (h.comp h.symm)

Tactic:
self_comp_symm,

Goal state after:
case e'_3
L : Language
M : Type w
N : Type w'
inst✝² : L.Structure M
inst✝¹ : L.Structure N
P : Type u_1
inst✝ : L.Structure P
h : M ≃[L] N
f g : N ≃[L] P
hfg : (fun f ↦ f.comp h) f = (fun f ↦ f.comp h) g
⊢ g = g.comp (refl L N)
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
a : Language.empty.Structure M
⊢ a = default

Tactic:
ext _ f

Goal state after:
case funMap
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
a : Language.empty.Structure M
x✝¹ : ℕ
f : Language.empty.Functions x✝¹
x✝ : Fin x✝¹ → M
⊢ funMap f x✝ = funMap f x✝

case RelMap
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
a : Language.empty.Structure M
x✝¹ : ℕ
f : Language.empty.Relations x✝¹
x✝ : Fin x✝¹ → M
⊢ RelMap f x✝ ↔ RelMap f x✝
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case inr
M : Type w
α : Type u'
β : Type v'
n m : ℕ
g : α → β ⊕ Fin n
v : β → M
xs : Fin (n + m) → M
x : Fin m
⊢ (Sum.elim v xs ∘ relabelAux g m) (Sum.inr x) = Sum.elim (Sum.elim v (xs ∘ castAdd m) ∘ g) (xs ∘ natAdd n) (Sum.inr x)

Tactic:
· simp [BoundedFormula.relabelAux]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
t : L.Term (α ⊕ β)
v : β → M
⊢ realize v t.varsToConstants = realize (Sum.elim (fun a ↦ ↑(L.con a)) v) t

Tactic:
by
  induction t with
  | var ab => rcases ab with a | b <;> simp [Language.con]
  | func f ts ih =>
    simp only [realize, constantsOn, constantsOnFunc, ih, varsToConstants]
    -- Porting note: below lemma does not work with simp for some reason
    rw [withConstants_funMap_sumInl]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case equal
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n✝ : ℕ
t₁✝ t₂✝ : L.Term (α ⊕ Fin n✝)
f : ↥(equal t₁✝ t₂✝).freeVarFinset → β
xs : Fin n✝ → M
hv' : ∀ (a : ↥(equal t₁✝ t₂✝).freeVarFinset), v (f a) = v' ↑a
⊢ realize (Sum.elim v xs) (t₁✝.restrictVarLeft (f ∘ Set.inclusion ⋯)) =
      realize (Sum.elim v xs) (t₂✝.restrictVarLeft (f ∘ Set.inclusion ⋯)) ↔
    realize (Sum.elim v' xs) t₁✝ = realize (Sum.elim v' xs) t₂✝

Tactic:
rw [realize_restrictVarLeft v' (by simp [hv']), realize_restrictVarLeft v' (by simp [hv'])]

Goal state after:
case equal
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n✝ : ℕ
t₁✝ t₂✝ : L.Term (α ⊕ Fin n✝)
f : ↥(equal t₁✝ t₂✝).freeVarFinset → β
xs : Fin n✝ → M
hv' : ∀ (a : ↥(equal t₁✝ t₂✝).freeVarFinset), v (f a) = v' ↑a
⊢ realize (Sum.elim v' (Sum.elim v xs ∘ Sum.inr)) t₁✝ = realize (Sum.elim v' (Sum.elim v xs ∘ Sum.inr)) t₂✝ ↔
    realize (Sum.elim v' xs) t₁✝ = realize (Sum.elim v' xs) t₂✝
Module: Mathlib.ModelTheory.ElementaryMaps

Goal state before:
pp: L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    φ.Realize default (Fin.snoc (⇑f ∘ x) a) → ∃ b, φ.Realize default (Fin.snoc (⇑f ∘ x) (f b))
⊢ ∀ {n : ℕ} (φ : L.Formula (Fin n)) (x : Fin n → M), φ.Realize (⇑f ∘ x) ↔ φ.Realize x

Tactic:
suffices h : ∀ (n : ℕ) (φ : L.BoundedFormula Empty n) (xs : Fin n → M),
      φ.Realize (f ∘ default) (f ∘ xs) ↔ φ.Realize default xs by
    intro n φ x
    exact φ.realize_relabel_sumInr.symm.trans (_root_.trans (h n _ _) φ.realize_relabel_sumInr)

Goal state after:
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    φ.Realize default (Fin.snoc (⇑f ∘ x) a) → ∃ b, φ.Realize default (Fin.snoc (⇑f ∘ x) (f b))
⊢ ∀ (n : ℕ) (φ : L.BoundedFormula Empty n) (xs : Fin n → M), φ.Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ φ.Realize default xs
Module: Mathlib.ModelTheory.ElementarySubstructures

Goal state before:
pp: L : Language
M : Type u_1
inst✝ : L.Structure M
A : Set M
hA : MeetsDefinable A
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
x : Fin n → ↥((closure L).toFun A)
⊢ ∀ (a : M), φ.Realize default (Fin.snoc (Subtype.val ∘ x) a) → ∃ b, φ.Realize default (Fin.snoc (Subtype.val ∘ x) ↑b)

Tactic:
a

Goal state after:
L : Language
M : Type u_1
inst✝ : L.Structure M
A : Set M
hA : MeetsDefinable A
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
x : Fin n → ↥((closure L).toFun A)
a : M
⊢ φ.Realize default (Fin.snoc (Subtype.val ∘ x) a) → ∃ b, φ.Realize default (Fin.snoc (Subtype.val ∘ x) ↑b)
Module: Mathlib.ModelTheory.Skolem

Goal state before:
pp: L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : L.Structure M
S : (L.sum L.skolem₁).Substructure M
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
x : Fin n → ↥(LHom.sumInl.substructureReduct S)
⊢ ∀ (a : M), φ.Realize default (Fin.snoc (Subtype.val ∘ x) a) → ∃ b, φ.Realize default (Fin.snoc (Subtype.val ∘ x) ↑b)

Tactic:
a

Goal state after:
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : L.Structure M
S : (L.sum L.skolem₁).Substructure M
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
x : Fin n → ↥(LHom.sumInl.substructureReduct S)
a : M
⊢ φ.Realize default (Fin.snoc (Subtype.val ∘ x) a) → ∃ b, φ.Realize default (Fin.snoc (Subtype.val ∘ x) ↑b)
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case all.mp
L : Language
M : Type w
N : Type u_1
inst✝³ : L.Structure M
inst✝² : L.Structure N
α : Type u'
n : ℕ
F : Type u_4
inst✝¹ : EquivLike F M N
inst✝ : L.StrongHomClass F M N
g : F
v : α → M
n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ {xs : Fin (n✝ + 1) → M}, f✝.Realize (⇑g ∘ v) (⇑g ∘ xs) ↔ f✝.Realize v xs
xs : Fin n✝ → M
h : ∀ (x : N), f✝.Realize (⇑g ∘ v) (snoc (⇑g ∘ xs) x)
⊢ ∀ (x : M), f✝.Realize v (snoc xs x)

Tactic:
a

Goal state after:
case all.mp
L : Language
M : Type w
N : Type u_1
inst✝³ : L.Structure M
inst✝² : L.Structure N
α : Type u'
n : ℕ
F : Type u_4
inst✝¹ : EquivLike F M N
inst✝ : L.StrongHomClass F M N
g : F
v : α → M
n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ {xs : Fin (n✝ + 1) → M}, f✝.Realize (⇑g ∘ v) (⇑g ∘ xs) ↔ f✝.Realize v xs
xs : Fin n✝ → M
h : ∀ (x : N), f✝.Realize (⇑g ∘ v) (snoc (⇑g ∘ xs) x)
a : M
⊢ f✝.Realize v (snoc xs a)
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case all.mpr
L : Language
M : Type w
N : Type u_1
inst✝³ : L.Structure M
inst✝² : L.Structure N
α : Type u'
n : ℕ
F : Type u_4
inst✝¹ : EquivLike F M N
inst✝ : L.StrongHomClass F M N
g : F
v : α → M
n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ {xs : Fin (n✝ + 1) → M}, f✝.Realize (⇑g ∘ v) (⇑g ∘ xs) ↔ f✝.Realize v xs
xs : Fin n✝ → M
h : ∀ (x : M), f✝.Realize v (snoc xs x)
⊢ ∀ (x : N), f✝.Realize (⇑g ∘ v) (snoc (⇑g ∘ xs) x)

Tactic:
a

Goal state after:
case all.mpr
L : Language
M : Type w
N : Type u_1
inst✝³ : L.Structure M
inst✝² : L.Structure N
α : Type u'
n : ℕ
F : Type u_4
inst✝¹ : EquivLike F M N
inst✝ : L.StrongHomClass F M N
g : F
v : α → M
n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ {xs : Fin (n✝ + 1) → M}, f✝.Realize (⇑g ∘ v) (⇑g ∘ xs) ↔ f✝.Realize v xs
xs : Fin n✝ → M
h : ∀ (x : M), f✝.Realize v (snoc xs x)
a : N
⊢ f✝.Realize (⇑g ∘ v) (snoc (⇑g ∘ xs) 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'
⊢ ℵ₀ ≤ #↑(⇑Equiv.ulift '' s') ∧
    lift.{max u v, w} #↑(s ∪ ⇑Equiv.ulift '' s') + lift.{w, max u v} #((i : ℕ) × (L.sum L.skolem₁).Functions i) ≤
      lift.{max u v, w} #↑(⇑Equiv.ulift '' s')

Tactic:
← aleph0_le_lift.{_, w'},

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} #↑(⇑Equiv.ulift '' s') ∧
    lift.{max u v, w} #↑(s ∪ ⇑Equiv.ulift '' s') + lift.{w, max u v} #((i : ℕ) × (L.sum L.skolem₁).Functions i) ≤
      lift.{max u v, w} #↑(⇑Equiv.ulift '' s')
Module: Mathlib.FieldTheory.AxGrothendieck

Goal state before:
pp: case intro
ι : Type u_1
K : Type u_2
R : Type u_3
inst✝⁴ : Field K
inst✝³ : Finite K
inst✝² : CommRing R
inst✝¹ : Finite ι
inst✝ : Algebra K R
alg : Algebra.IsAlgebraic K R
ps : ι → MvPolynomial ι R
S : Set (ι → R)
hm : Set.MapsTo (fun v i ↦ (eval v) (ps i)) S S
hinj : Set.InjOn (fun v i ↦ (eval v) (ps i)) S
is_int : ∀ (x : R), IsIntegral K x
v : ι → R
hvS : v ∈ S
val✝ : Fintype ι
s : Finset R := (univ.biUnion fun i ↦ image (fun x ↦ coeff x (ps i)) (ps i).support) ∪ image v univ
hv : ∀ (i : ι), v i ∈ Algebra.adjoin K ↑s
hs₁ : ∀ (i : ι), ∀ k ∈ (ps i).support, coeff k (ps i) ∈ Algebra.adjoin K ↑s
this : IsNoetherian K ↥(Algebra.adjoin K ↑s)
⊢ v ∈ (fun v i ↦ (eval v) (ps i)) '' S

Tactic:
have : Finite (Algebra.adjoin K (s : Set R)) := Module.finite_of_finite K

Goal state after:
case intro
ι : Type u_1
K : Type u_2
R : Type u_3
inst✝⁴ : Field K
inst✝³ : Finite K
inst✝² : CommRing R
inst✝¹ : Finite ι
inst✝ : Algebra K R
alg : Algebra.IsAlgebraic K R
ps : ι → MvPolynomial ι R
S : Set (ι → R)
hm : Set.MapsTo (fun v i ↦ (eval v) (ps i)) S S
hinj : Set.InjOn (fun v i ↦ (eval v) (ps i)) S
is_int : ∀ (x : R), IsIntegral K x
v : ι → R
hvS : v ∈ S
val✝ : Fintype ι
s : Finset R := (univ.biUnion fun i ↦ image (fun x ↦ coeff x (ps i)) (ps i).support) ∪ image v univ
hv : ∀ (i : ι), v i ∈ Algebra.adjoin K ↑s
hs₁ : ∀ (i : ι), ∀ k ∈ (ps i).support, coeff k (ps i) ∈ Algebra.adjoin K ↑s
this✝ : IsNoetherian K ↥(Algebra.adjoin K ↑s)
this : Finite ↥(Algebra.adjoin K ↑s)
⊢ v ∈ (fun v i ↦ (eval v) (ps i)) '' S
Module: Mathlib.RingTheory.Localization.Cardinality

Goal state before:
pp: R : Type u
inst✝³ : CommSemiring R
L : Type v
inst✝² : CommSemiring L
inst✝¹ : Algebra R L
S : Submonoid R
inst✝ : IsLocalization S L
⊢ Cardinal.lift.{u, v} #L ≤ Cardinal.lift.{v, u} #R

Tactic:
have := Localization.cardinalMk_le S

Goal state after:
R : Type u
inst✝³ : CommSemiring R
L : Type v
inst✝² : CommSemiring L
inst✝¹ : Algebra R L
S : Submonoid R
inst✝ : IsLocalization S L
this : #(Localization S) ≤ #R
⊢ Cardinal.lift.{u, v} #L ≤ Cardinal.lift.{v, u} #R
Module: Mathlib.FieldTheory.Cardinality

Goal state before:
pp: case inr
α : Type u
h : Infinite α
⊢ Nonempty (Field α) ↔ ℵ₀ ≤ #α ∨ ∃ n, #α = ↑n ∧ IsPrimePow n

Tactic:
· simpa only [← Cardinal.infinite_iff, h, true_or, iff_true] using Infinite.nonempty_field

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

Goal state before:
pp: n : ℕ
⊢ Prime ↑n ↔ Nat.Prime n

Tactic:
simp only [Prime, Nat.prime_iff]
  refine and_congr (by simp) (and_congr ?_ ⟨fun h b c hbc => ?_, fun h b c hbc => ?_⟩)
  · simp only [isUnit_iff, Nat.isUnit_iff]
    exact mod_cast Iff.rfl
  · exact mod_cast h b c (mod_cast hbc)
  rcases lt_or_ge (b * c) ℵ₀ with h' | h'
  · rcases mul_lt_aleph0_iff.mp h' with (rfl | rfl | ⟨hb, hc⟩)
    · simp
    · simp
    lift b to ℕ using hb
    lift c to ℕ using hc
    exact mod_cast h b c (mod_cast hbc)
  rcases aleph0_le_mul_iff.mp h' with ⟨hb, hc, hℵ₀⟩
  have hn : (n : Cardinal) ≠ 0 := by
    intro h
    rw [h, zero_dvd_iff, mul_eq_zero] at hbc
    cases hbc <;> contradiction
  wlog hℵ₀b : ℵ₀ ≤ b
  apply (this h c b _ _ hc hb hℵ₀.symm hn (hℵ₀.resolve_left hℵ₀b)).symm <;> try assumption
  · rwa [mul_comm] at hbc
  · rwa [mul_comm] at h'
  · exact Or.inl (dvd_of_le_of_aleph0_le hn (natCast_lt_aleph0.le.trans hℵ₀b) hℵ₀b)

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

Goal state before:
pp: F : Type u_2
K : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Differential F
inst✝² : Differential K
inst✝¹ : Algebra F K
inst✝ : DifferentialAlgebra F K
a : F
⊢ logDeriv ((algebraMap F K) a) = (algebraMap F K) (logDeriv a)

Tactic:
unfold logDeriv
  simp [deriv_algebraMap]

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

Goal state before:
pp: k : Type u_1
inst✝¹ : Field k
inst✝ : Finite k
f : k[X]
hi : Irreducible f
n : ℕ
hdvd : f.natDegree ∣ n
a : AdjoinRoot f := AdjoinRoot.root f
this✝² : NeZero f.natDegree
this✝¹ : Fact (Irreducible f)
p : ℕ
hp : CharP k p
this✝ : Fact (Nat.Prime p)
e : AdjoinRoot f ≃ₐ[k] Extension k p f.natDegree := algEquivExtension k p f.natDegree (AdjoinRoot f) ⋯
this : Fintype (Extension k p f.natDegree)
⊢ e a - e a = 0

Tactic:
sub_self

Goal state after:
k : Type u_1
inst✝¹ : Field k
inst✝ : Finite k
f : k[X]
hi : Irreducible f
n : ℕ
hdvd : f.natDegree ∣ n
a : AdjoinRoot f := AdjoinRoot.root f
this✝² : NeZero f.natDegree
this✝¹ : Fact (Irreducible f)
p : ℕ
hp : CharP k p
this✝ : Fact (Nat.Prime p)
e : AdjoinRoot f ≃ₐ[k] Extension k p f.natDegree := algEquivExtension k p f.natDegree (AdjoinRoot f) ⋯
this : Fintype (Extension k p f.natDegree)
⊢ 0 = 0
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 : σ
hi : a i ≠ b i
⊢ 1 - 1 = 0

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:
sub_self

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 : σ
hi : a i ≠ b i
⊢ 0 = 0

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