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

Goal state before:
pp: τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : CompactSpace β
v : Set β
hv₁ : IsOpen[inst✝¹] v
hv₂ : ω f ϕ s ⊆ v
u : Set τ
hu_mem : u ∈ f
hu : closure[inst✝¹] (image2 ϕ u s) ⊆ v
t : τ
ht : t ∈ u
x : α
hx : x ∈ s
⊢ ϕ t x ∈ v

Tactic:
exact hu (subset_closure <| mem_image2_of_mem ht hx)

Goal state after:
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: case htc
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : f.NeBot
c : Set β
hc₁ : IsCompact c
hs : s.Nonempty
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst✝¹] (image2 ϕ v s) ⊆ c
⊢ ∀ (i : ↑f.sets), IsCompact (closure[inst✝¹] (image2 ϕ (↑i ∩ v) s))

Tactic:
intro

Goal state after:
case htc
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : f.NeBot
c : Set β
hc₁ : IsCompact c
hs : s.Nonempty
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst✝¹] (image2 ϕ v s) ⊆ c
i✝ : ↑f.sets
⊢ IsCompact (closure[inst✝¹] (image2 ϕ (↑i✝ ∩ v) s))
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: τ : Type u_1
inst✝² : TopologicalSpace τ
inst✝¹ : AddMonoid τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
t : τ
ht : Tendsto (fun x ↦ x + t) f f
⊢ ω f ϕ.toFun (ϕ.toFun t '' s) ⊆ ω f ϕ.toFun s

Tactic:
by
  simp only [omegaLimit_image_eq, ← map_add]
  exact omegaLimit_subset_of_tendsto ϕ s ht

Goal state after:
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: τ : Type u_1
inst✝² : TopologicalSpace τ
inst✝¹ : AddCommGroup τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
hf : ∀ (t : τ), Tendsto (fun x ↦ t + x) f f
x✝ : α
h : ∀ n ∈ 𝓝 x✝, ∀ {U : Set τ}, U ∈ f → ∃ x ∈ U, (ϕ.toFun x '' ω f ϕ.toFun s ∩ n).Nonempty
n : Set α
hn : n ∈ 𝓝 x✝
u : Set τ
hu : u ∈ f
o : Set α
ho₁ : o ⊆ n
ho₂ : IsOpen[inst✝] o
ho₃ : x✝ ∈ o
t : τ
_ht₁ : t ∈ u
ht₂ : (ϕ.toFun t '' ω f ϕ.toFun s ∩ o).Nonempty
l₁ : (ω f ϕ.toFun s ∩ o).Nonempty
l₂ : (closure[inst✝] (image2 ϕ.toFun u s) ∩ o).Nonempty
⊢ (o ∩ image2 ϕ.toFun u s).Nonempty

Tactic:
rcases l₂ with ⟨b, hb₁, hb₂⟩

Goal state after:
τ : Type u_1
inst✝² : TopologicalSpace τ
inst✝¹ : AddCommGroup τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
hf : ∀ (t : τ), Tendsto (fun x ↦ t + x) f f
x✝ : α
h : ∀ n ∈ 𝓝 x✝, ∀ {U : Set τ}, U ∈ f → ∃ x ∈ U, (ϕ.toFun x '' ω f ϕ.toFun s ∩ n).Nonempty
n : Set α
hn : n ∈ 𝓝 x✝
u : Set τ
hu : u ∈ f
o : Set α
ho₁ : o ⊆ n
ho₂ : IsOpen[inst✝] o
ho₃ : x✝ ∈ o
t : τ
_ht₁ : t ∈ u
ht₂ : (ϕ.toFun t '' ω f ϕ.toFun s ∩ o).Nonempty
l₁ : (ω f ϕ.toFun s ∩ o).Nonempty
b : α
hb₁ : b ∈ closure[inst✝] (image2 ϕ.toFun u s)
hb₂ : b ∈ o
⊢ (o ∩ image2 ϕ.toFun u s).Nonempty
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

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

Tactic:
rw [s_net, Finset.card_empty, CharP.cast_eq_zero, bot_eq_zero']

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hμs : μ s ≠ ∞
⊢ IntegrableOn (fun x ↦ (μ.rnDeriv ν x).toReal) s ν

Tactic:
refine integrable_toReal_of_lintegral_ne_top (Measure.measurable_rnDeriv _ _).aemeasurable ?_
  exact ((setLIntegral_rnDeriv_le _).trans_lt hμs.lt_top).ne

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

Goal state before:
pp: 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 : ℕ
⊢ coverMincard T F (U ○ U) (m * n) ≤ coverMincard T F U m ^ n

Tactic:
rcases F.eq_empty_or_nonempty with rfl | F_nonempty
  · simp
  obtain rfl | hn := eq_or_ne n 0
  · rw [mul_zero, coverMincard_zero T F_nonempty (U ○ U), pow_zero]
  rcases eq_top_or_lt_top (coverMincard T F U m) with h | h
  · simp [*]
  · 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.CoverEntropy

Goal state before:
pp: X : Type u_1
T : X → X
U : SetRel X X
F : Set X
n : ℕ
inst✝ : U.IsSymm
s : Finset X
h : IsDynCoverOf T F U n ↑s
h' : ↑(#s) = coverMincard T F U n
⊢ ∀ x ∈ s, (F ∩ ball x (dynEntourage T U n)).Nonempty

Tactic:
by_contra! ⟨x, x_s, ball_empt⟩
  have smaller_cover : IsDynCoverOf T F U n (s.erase x) := by
    intro y y_F
    specialize h y_F
    simp only [s.mem_coe] at h
    simp only [s.coe_erase, mem_sdiff, s.mem_coe, mem_singleton_iff]
    obtain ⟨z, z_s, hz⟩ := h
    refine ⟨z, ⟨z_s, fun z_x ↦ notMem_empty y ?_⟩, hz⟩
    rw [← ball_empt]
    rw [z_x] at hz
    exact mem_inter y_F <| (dynEntourage T U n).symm hz
  apply smaller_cover.coverMincard_le_card.not_gt
  rw [← h']
  exact_mod_cast s.card_erase_lt_of_mem x_s

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 α
inst✝ : IsMinimal M α
⊢ IsTopologicallyTransitive M α

Tactic:
by
  refine (isTopologicallyTransitive_iff_dense_iUnion_preimage M).mpr fun h hn ↦ ?_
  simp only [h.iUnion_preimage_smul M hn, dense_univ]

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: F : Type u_1
inst✝ : Field F
⊢ Group.IsSolvable (Gal 0)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: F : Type u_1
inst✝ : Field F
⊢ Group.IsSolvable (Gal 1)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: F : Type u_1
inst✝ : Field F
x : F
⊢ Group.IsSolvable (C x).Gal

Tactic:
infer_instance

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: F : Type u_1
inst✝ : Field F
⊢ Group.IsSolvable X.Gal

Tactic:
infer_instance

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: F : Type u_1
inst✝ : Field F
x : F
⊢ Group.IsSolvable (X - C x).Gal

Tactic:
infer_instance

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: F : Type u_1
inst✝ : Field F
n : ℕ
⊢ Group.IsSolvable (X ^ n).Gal

Tactic:
infer_instance

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

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

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

Tactic:
· refine (Measure.rnDeriv_singularPart μ ν).trans ?_
    symm
    suffices (fun x ↦ ((μ.singularPart ν).map f).rnDeriv (ν.map f) x) =ᵐ[ν.map f] 0 by
      rw [Filter.EventuallyEq, hf.ae_map_iff] at this
      exact this
    refine Measure.rnDeriv_eq_zero_of_mutuallySingular ?_ Measure.AbsolutelyContinuous.rfl
    exact hf.mutuallySingular_map (μ.mutuallySingular_singularPart ν)

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

Goal state before:
pp: α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite μ
f : α → E
hμν : μ ≪ ν
⊢ ∫ (x : α), (μ.rnDeriv ν x).toReal • f x ∂ν = ∫ (x : α), f x ∂μ

Tactic:
rw [← integral_withDensity_eq_integral_toReal_smul (measurable_rnDeriv _ _) (rnDeriv_lt_top _ _),
    withDensity_rnDeriv_eq _ _ hμν]

Goal state after:
Module: Mathlib.FieldTheory.IsAlgClosed.Classification

Goal state before:
pp: R : Type u_1
K : Type u_3
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : Algebra R K
ι : Type u_4
v : ι → K
inst✝ : IsAlgClosed K
hv : IsTranscendenceBasis R v
this : Nontrivial R := RingHom.domain_nontrivial (algebraMap R K)
⊢ IsAlgClosed K

Tactic:
infer_instance

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case neg
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : (map (RingHom.id F) (X ^ n - 1)).Splits
ha : ¬a = 0
ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
mem_range : ∀ {c : (X ^ n - C a).SplittingField}, c ^ n = 1 → ∃ d, (algebraMap F (X ^ n - C a).SplittingField) d = c
σ τ : (X ^ n - C a).Gal
b : (X ^ n - C a).SplittingField
hb : b ^ n = (algebraMap F (X ^ n - C a).SplittingField) a
hb' : b ≠ 0
key : ∀ (σ : (X ^ n - C a).Gal), ∃ c, σ b = b * (algebraMap F (X ^ n - C a).SplittingField) c
c : F
hc : σ b = b * (algebraMap F (X ^ n - C a).SplittingField) c
d : F
hd : τ b = b * (algebraMap F (X ^ n - C a).SplittingField) d
⊢ (algebraMap F (X ^ n - C a).SplittingField) c * (algebraMap F (X ^ n - C a).SplittingField) d =
    (algebraMap F (X ^ n - C a).SplittingField) d * (algebraMap F (X ^ n - C a).SplittingField) c

Tactic:
mul_comm

Goal state after:
case neg
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : (map (RingHom.id F) (X ^ n - 1)).Splits
ha : ¬a = 0
ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
mem_range : ∀ {c : (X ^ n - C a).SplittingField}, c ^ n = 1 → ∃ d, (algebraMap F (X ^ n - C a).SplittingField) d = c
σ τ : (X ^ n - C a).Gal
b : (X ^ n - C a).SplittingField
hb : b ^ n = (algebraMap F (X ^ n - C a).SplittingField) a
hb' : b ≠ 0
key : ∀ (σ : (X ^ n - C a).Gal), ∃ c, σ b = b * (algebraMap F (X ^ n - C a).SplittingField) c
c : F
hc : σ b = b * (algebraMap F (X ^ n - C a).SplittingField) c
d : F
hd : τ b = b * (algebraMap F (X ^ n - C a).SplittingField) d
⊢ (algebraMap F (X ^ n - C a).SplittingField) d * (algebraMap F (X ^ n - C a).SplittingField) c =
    (algebraMap F (X ^ n - C a).SplittingField) d * (algebraMap F (X ^ n - C a).SplittingField) c
Module: Mathlib.FieldTheory.AbelRuffini

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

Tactic:
eval_map,

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

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x y z : E
hx : x ∈ solvableByRad F E
hy : y ∈ solvableByRad F E
hz : z ∈ solvableByRad F E
hx' : Group.IsSolvable (minpoly F x).Gal
hy' : Group.IsSolvable (minpoly F y).Gal
hz' : z ∈ F⟮x, y⟯
p : F[X] := minpoly F x
q : F[X] := minpoly F y
hpq :
  (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F x)).Splits ∧
    (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F y)).Splits
f : ↥F⟮x, y⟯ →ₐ[F] (p * q).SplittingField
key : minpoly F z = minpoly F (f ⟨z, hz'⟩)
⊢ Normal F (p * q).SplittingField

Tactic:
infer_instance

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case mem
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
y : F
⊢ Group.IsSolvable (X - C y).Gal

Tactic:
infer_instance

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

Goal state before:
pp: p : ℕ
K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
⊢ K ⊨ Theory.field

Tactic:
infer_instance

Goal state after:
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : L.Structure M
inst✝¹ : L.Structure N
inst✝ : L.Structure P
p q : L.Substructure M
h : ↑p = ↑q
⊢ p = q

Tactic:
cases p; cases q; congr

Goal state after:
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
ι : Type u_3
hι : Nonempty ι
S : ι → L.Substructure M
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : M
⊢ x ∈ ⨆ i, S i → ∃ i, x ∈ S i

Tactic:
suffices x ∈ closure L (⋃ i, (S i : Set M)) → ∃ i, x ∈ S i by
    simpa only [closure_iUnion, closure_eq (S _)] using this

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
ι : Type u_3
hι : Nonempty ι
S : ι → L.Substructure M
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : M
⊢ x ∈ (closure L).toFun (⋃ i, ↑(S i)) → ∃ i, x ∈ S i
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case h
L : Language
α : Type u'
l✝ : List ((n : ℕ) × L.BoundedFormula α n)
n φ_n φ_l : ℕ
φ_R : L.Relations φ_l
ts : Fin φ_l → L.Term (α ⊕ Fin φ_n)
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
i : Fin φ_l
⊢ ↑i < (List.map (Sum.getLeft? ∘ fun i ↦ Sum.inl ⟨φ_n, ts i⟩) (finRange φ_l)).length

Tactic:
· simp only [length_map, length_finRange, is_lt]

Goal state after:
Module: Mathlib.ModelTheory.ElementaryMaps

Goal state before:
pp: case refine_4
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
⊢ ∀ {n : ℕ} (f₁ f₂ : L.BoundedFormula Empty n),
    (∀ (xs : Fin n → M), f₁.Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ f₁.Realize default xs) →
      (∀ (xs : Fin n → M), f₂.Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ f₂.Realize default xs) →
        ∀ (xs : Fin n → M), (f₁ ⟹ f₂).Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ (f₁ ⟹ f₂).Realize default xs

pp: case refine_5
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
⊢ ∀ {n : ℕ} (f_1 : L.BoundedFormula Empty (n + 1)),
    (∀ (xs : Fin (n + 1) → M), f_1.Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ f_1.Realize default xs) →
      ∀ (xs : Fin n → M), (∀' f_1).Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ (∀' f_1).Realize default xs

Tactic:
· intro _ _ _ ih1 ih2 _
    simp [ih1, ih2]

Goal state after:
case refine_5
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
⊢ ∀ {n : ℕ} (f_1 : L.BoundedFormula Empty (n + 1)),
    (∀ (xs : Fin (n + 1) → M), f_1.Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ f_1.Realize default xs) →
      ∀ (xs : Fin n → M), (∀' f_1).Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ (∀' f_1).Realize default xs
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case left
L : Language
α : Type u'
inst✝¹ : Countable α
inst✝ : Countable L.Symbols
⊢ Countable L.Symbols

Tactic:
infer_instance

Goal state after:
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case right
L : Language
α : Type u'
inst✝¹ : Countable α
inst✝ : Countable L.Symbols
⊢ Countable (constantsOn α).Symbols

Tactic:
infer_instance

Goal state after:
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case left
L : Language
α : Type u'
inst✝¹ : Countable α
inst✝ : Countable L.Symbols
⊢ Countable α

Tactic:
infer_instance

Goal state after:
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case right
L : Language
α : Type u'
inst✝¹ : Countable α
inst✝ : Countable L.Symbols
⊢ Countable L.Symbols

Tactic:
infer_instance

Goal state after:
Module: Mathlib.ModelTheory.Skolem

Goal state before:
pp: L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : L.Structure M
⊢ Small.{max u v, w} ↥⊥

Tactic:
infer_instance

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

Goal state before:
pp: case hT
p : ℕ
hp : Nat.Prime p ∨ p = 0
M : Type
struc✝ : Language.ring.Structure M
is_model✝ : M ⊨ Theory.ACF p
nonempty'✝ : Nonempty M
x✝¹ : Field M := fieldOfModelACF p M
this✝ : M ⊨ Theory.field
x✝ : CompatibleRing M := compatibleRingOfModelField M
this : IsAlgClosed M
⊢ Infinite ↑{ Carrier := M, struc := struc✝, is_model := is_model✝, nonempty' := nonempty'✝ }

Tactic:
infer_instance

Goal state after:
Module: Mathlib.RingTheory.Nullstellensatz

Goal state before:
pp: k : Type u_1
K : Type u_2
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
σ : Type u_3
x : σ → K
⊢ (vanishingIdeal k {x}).IsPrime

Tactic:
infer_instance

Goal state after:
Module: Mathlib.RingTheory.Nullstellensatz

Goal state before:
pp: k : Type u_1
K : Type u_2
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
σ : Type u_3
V : Set (σ → K)
x✝ : MvPolynomial σ k
hp : x✝ ∈ PrimeSpectrum.vanishingIdeal (pointToPoint '' V)
x : σ → K
hx : x ∈ V
⊢ (vanishingIdeal k {x}).IsPrime

Tactic:
infer_instance

Goal state after:
Module: Mathlib.GroupTheory.OreLocalization.Cardinality

Goal state before:
pp: R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : MulAction R X
h✝¹ : Infinite X
h✝ : Infinite ↥S
⊢ lift.{u, v} #X * lift.{v, u} #↥S = max (lift.{v, u} #↥S) (lift.{u, v} #X)

Tactic:
mul_comm

Goal state after:
R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : MulAction R X
h✝¹ : Infinite X
h✝ : Infinite ↥S
⊢ lift.{v, u} #↥S * lift.{u, v} #X = max (lift.{v, u} #↥S) (lift.{u, v} #X)
Module: Mathlib.GroupTheory.OreLocalization.Cardinality

Goal state before:
pp: case inr
R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : MulAction R X
hc : ∀ (s s' : ↥S), Commute s s'
h✝ : Infinite X
key : ∀ (x : X) (s s' : ↥S), s • x = s' • x → Commute s s' → x /ₒ s = x /ₒ s'
i : X × ↥S → OreLocalization S X := fun x ↦ x.1 /ₒ x.2
hsurj : Surjective i
hi : RightInverse (surjInv hsurj) i
j : OreLocalization S X → X × X := (fun x ↦ (x.1, x.2 • x.1)) ∘ surjInv hsurj
⊢ Injective j

Tactic:
intro

Goal state after:
case inr
R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : MulAction R X
hc : ∀ (s s' : ↥S), Commute s s'
h✝ : Infinite X
key : ∀ (x : X) (s s' : ↥S), s • x = s' • x → Commute s s' → x /ₒ s = x /ₒ s'
i : X × ↥S → OreLocalization S X := fun x ↦ x.1 /ₒ x.2
hsurj : Surjective i
hi : RightInverse (surjInv hsurj) i
j : OreLocalization S X → X × X := (fun x ↦ (x.1, x.2 • x.1)) ∘ surjInv hsurj
a₁✝ : OreLocalization S X
⊢ ∀ ⦃a₂ : OreLocalization S X⦄, j a₁✝ = j a₂ → a₁✝ = a₂
Module: Mathlib.RingTheory.Localization.Cardinality

Goal state before:
pp: R : Type u
inst✝ : CommRing R
S : Submonoid R
hS : S ≤ R⁰
⊢ S ≤ nonZeroDivisorsLeft R

Tactic:
rwa [nonZeroDivisorsLeft_eq_nonZeroDivisors]

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

Goal state before:
pp: case inr.ha
a : Cardinal.{u}
h : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
t : Cardinal.{u}
ht : a * t = 1
⊢ 1 ≤ a

pp: case inr.hb
a : Cardinal.{u}
h : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
t : Cardinal.{u}
ht : a * t = 1
⊢ 1 ≤ t

Tactic:
· exact Cardinal.one_le_iff_ne_zero.mpr ha

Goal state after:
case inr.hb
a : Cardinal.{u}
h : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
t : Cardinal.{u}
ht : a * t = 1
⊢ 1 ≤ t
Module: Mathlib.SetTheory.Cardinal.Divisibility

Goal state before:
pp: case refine_2.inr.inr.inr.hbc
a : Cardinal.{u}
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this : ∀ {a : Cardinal.{u}}, ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : b ≤ c
⊢ a ∣ c * b

Tactic:
mul_comm

Goal state after:
case refine_2.inr.inr.inr.hbc
a : Cardinal.{u}
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this : ∀ {a : Cardinal.{u}}, ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : b ≤ c
⊢ a ∣ b * c
Module: Mathlib.SetTheory.Cardinal.Divisibility

Goal state before:
pp: case refine_2.inr.inr.inr.hz
a : Cardinal.{u}
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this : ∀ {a : Cardinal.{u}}, ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : b ≤ c
⊢ c * b ≠ 0

Tactic:
mul_comm

Goal state after:
case refine_2.inr.inr.inr.hz
a : Cardinal.{u}
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this : ∀ {a : Cardinal.{u}}, ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : b ≤ c
⊢ b * c ≠ 0
Module: Mathlib.SetTheory.Cardinal.Divisibility

Goal state before:
pp: n : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : ↑n ≠ 0
this :
  ∀ {n : ℕ},
    (∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b) →
      ∀ (b c : Cardinal.{u_1}),
        ↑n ∣ b * c → ℵ₀ ≤ b * c → b ≠ 0 → c ≠ 0 → ℵ₀ ≤ b ∨ ℵ₀ ≤ c → ↑n ≠ 0 → ℵ₀ ≤ b → ↑n ∣ b ∨ ↑n ∣ c
hℵ₀b : ¬ℵ₀ ≤ b
⊢ ↑n ∣ c * b

Tactic:
mul_comm

Goal state after:
n : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ c * b
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : ↑n ≠ 0
this :
  ∀ {n : ℕ},
    (∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b) →
      ∀ (b c : Cardinal.{u_1}),
        ↑n ∣ b * c → ℵ₀ ≤ b * c → b ≠ 0 → c ≠ 0 → ℵ₀ ≤ b ∨ ℵ₀ ≤ c → ↑n ≠ 0 → ℵ₀ ≤ b → ↑n ∣ b ∨ ↑n ∣ c
hℵ₀b : ¬ℵ₀ ≤ b
⊢ ↑n ∣ c * b
Module: Mathlib.SetTheory.Cardinal.Divisibility

Goal state before:
pp: n : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : ↑n ≠ 0
this :
  ∀ {n : ℕ},
    (∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b) →
      ∀ (b c : Cardinal.{u_1}),
        ↑n ∣ b * c → ℵ₀ ≤ b * c → b ≠ 0 → c ≠ 0 → ℵ₀ ≤ b ∨ ℵ₀ ≤ c → ↑n ≠ 0 → ℵ₀ ≤ b → ↑n ∣ b ∨ ↑n ∣ c
hℵ₀b : ¬ℵ₀ ≤ b
⊢ ℵ₀ ≤ c * b

Tactic:
mul_comm

Goal state after:
n : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ c * b
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : ↑n ≠ 0
this :
  ∀ {n : ℕ},
    (∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b) →
      ∀ (b c : Cardinal.{u_1}),
        ↑n ∣ b * c → ℵ₀ ≤ b * c → b ≠ 0 → c ≠ 0 → ℵ₀ ≤ b ∨ ℵ₀ ≤ c → ↑n ≠ 0 → ℵ₀ ≤ b → ↑n ∣ b ∨ ↑n ∣ c
hℵ₀b : ¬ℵ₀ ≤ b
⊢ ℵ₀ ≤ c * b
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:
rwa [Ne, funext_iff, not_forall] at h

Goal state after: