mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.ContinuousPreimage

Goal state before:
pp: α : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁹ : TopologicalSpace X
inst✝⁸ : MeasurableSpace X
inst✝⁷ : BorelSpace X
inst✝⁶ : R1Space X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : MeasurableSpace Y
inst✝³ : BorelSpace Y
inst✝² : R1Space Y
μ : Measure X
ν : Measure Y
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : IsLocallyFiniteMeasure ν
l : Filter α
f : α → C(X, Y)
g : C(X, Y)
hfg : Tendsto f l (𝓝 g)
hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a)) μ ν
hg : MeasurePreserving (⇑g) μ ν
this : ν.InnerRegularCompactLTTop
s : Set Y
hs : NullMeasurableSet s ν
hνs : ν s ≠ ∞
ε : ℝ≥0∞
hε : ε > 0
hso : IsOpen[inst✝⁵] s
hνs' : μ (⇑g ⁻¹' s) ≠ ∞
K : Set X
hKg : MapsTo (⇑g) K s
hKco : IsCompact K
hKcl : IsClosed[inst✝⁹] K
hKμ : μ (⇑g ⁻¹' s \ K) < ε / 2
hKm : NullMeasurableSet K μ
a : α
hfa : MeasurePreserving (⇑(f a)) μ ν
⊢ MapsTo (⇑(f a)) K s → μ ((⇑(f a) ⁻¹' s) ∆ (⇑g ⁻¹' s)) ≤ ε

Tactic:
ha

Goal state after:
α : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁹ : TopologicalSpace X
inst✝⁸ : MeasurableSpace X
inst✝⁷ : BorelSpace X
inst✝⁶ : R1Space X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : MeasurableSpace Y
inst✝³ : BorelSpace Y
inst✝² : R1Space Y
μ : Measure X
ν : Measure Y
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : IsLocallyFiniteMeasure ν
l : Filter α
f : α → C(X, Y)
g : C(X, Y)
hfg : Tendsto f l (𝓝 g)
hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a)) μ ν
hg : MeasurePreserving (⇑g) μ ν
this : ν.InnerRegularCompactLTTop
s : Set Y
hs : NullMeasurableSet s ν
hνs : ν s ≠ ∞
ε : ℝ≥0∞
hε : ε > 0
hso : IsOpen[inst✝⁵] s
hνs' : μ (⇑g ⁻¹' s) ≠ ∞
K : Set X
hKg : MapsTo (⇑g) K s
hKco : IsCompact K
hKcl : IsClosed[inst✝⁹] K
hKμ : μ (⇑g ⁻¹' s \ K) < ε / 2
hKm : NullMeasurableSet K μ
a : α
hfa : MeasurePreserving (⇑(f a)) μ ν
ha : MapsTo (⇑(f a)) K s
⊢ μ ((⇑(f a) ⁻¹' s) ∆ (⇑g ⁻¹' s)) ≤ ε
Module: Mathlib.Dynamics.Ergodic.Extreme

Goal state before:
pp: X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
c : ℝ≥0∞
hc : c ≠ ∞
h : μ ∈ extremePoints ℝ≥0∞ {ν | MeasurePreserving f ν ν ∧ ν univ = c}
hf : MeasurePreserving f μ μ
⊢ Ergodic f μ

Tactic:
rcases eq_or_ne c 0 with rfl | hc₀

Goal state after:
case inl
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
hf : MeasurePreserving f μ μ
hc : 0 ≠ ∞
h : μ ∈ extremePoints ℝ≥0∞ {ν | MeasurePreserving f ν ν ∧ ν univ = 0}
⊢ Ergodic f μ

case inr
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
c : ℝ≥0∞
hc : c ≠ ∞
h : μ ∈ extremePoints ℝ≥0∞ {ν | MeasurePreserving f ν ν ∧ ν univ = c}
hf : MeasurePreserving f μ μ
hc₀ : c ≠ 0
⊢ Ergodic f μ
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
y : β
⊢ y ∈ ω f ϕ s ↔ ∀ n ∈ 𝓝 y, ∃ᶠ (t : τ) in f, (ϕ t '' s ∩ n).Nonempty

Tactic:
by
  simp_rw [mem_omegaLimit_iff_frequently, image_inter_nonempty_iff]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝² : μ.HaveLebesgueDecomposition ν
inst✝¹ : μ.HaveLebesgueDecomposition (ν + ν')
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hνν' : ν ⟂ₘ ν'
t : Set α := hνν'.nullSet
ht : MeasurableSet t
⊢ μ.rnDeriv (ν + ν') =ᵐ[ν.restrict tᶜ] μ.rnDeriv ν

Tactic:
← withDensity_eq_iff_of_sigmaFinite (μ := ν.restrict tᶜ)
    (Measure.measurable_rnDeriv _ _).aemeasurable (Measure.measurable_rnDeriv _ _).aemeasurable

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝² : μ.HaveLebesgueDecomposition ν
inst✝¹ : μ.HaveLebesgueDecomposition (ν + ν')
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hνν' : ν ⟂ₘ ν'
t : Set α := hνν'.nullSet
ht : MeasurableSet t
⊢ (ν.restrict tᶜ).withDensity (μ.rnDeriv (ν + ν')) = (ν.restrict tᶜ).withDensity (μ.rnDeriv ν)
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: case inr
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
m : ℕ
F_inv : MapsTo T F F
inst✝ : U.IsSymm
n : ℕ
s : Finset X
h : IsDynCoverOf T F U m ↑s
x✝ : Nonempty X
s_nemp : (↑s).Nonempty
x : X
x_F : x ∈ F
m_pos : m > 0
t : Fin n → ↥s
y z : X
k : ℕ
k_mn : k / m < n
y_int : (T^[k % m] ↑(t ⟨k / m, k_mn⟩), T^[k % m] (T^[m * ↑⟨k / m, k_mn⟩] y)) ∈ U
z_int : (T^[k % m] ↑(t ⟨k / m, k_mn⟩), T^[k % m] (T^[m * ↑⟨k / m, k_mn⟩] z)) ∈ U
⊢ ∃ b, (T^[k] y, b) ∈ U ∧ (b, T^[k] z) ∈ U

Tactic:
← Function.iterate_add_apply T (k % m) (m * (k / m)),

Goal state after:
case inr
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
m : ℕ
F_inv : MapsTo T F F
inst✝ : U.IsSymm
n : ℕ
s : Finset X
h : IsDynCoverOf T F U m ↑s
x✝ : Nonempty X
s_nemp : (↑s).Nonempty
x : X
x_F : x ∈ F
m_pos : m > 0
t : Fin n → ↥s
y z : X
k : ℕ
k_mn : k / m < n
y_int : (T^[k % m] ↑(t ⟨k / m, k_mn⟩), T^[k % m + m * (k / m)] y) ∈ U
z_int : (T^[k % m] ↑(t ⟨k / m, k_mn⟩), T^[k % m + m * (k / m)] z) ∈ U
⊢ ∃ b, (T^[k] y, b) ∈ U ∧ (b, T^[k] z) ∈ U
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 = coverMincard T F U n
h : ¬Nonempty { s // IsDynCoverOf T F U n ↑s }
⊢ ⨅ s, ⨅ (_ : IsDynCoverOf T F U n ↑s), ↑(#s) = ⊤

Tactic:
iInf₂_eq_top

Goal state after:
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 = coverMincard T F U n
h : ¬Nonempty { s // IsDynCoverOf T F U n ↑s }
⊢ ∀ (i : Finset X), IsDynCoverOf T F U n ↑i → ↑(#i) = ⊤
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
pp: X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : netMaxcard T F U n = 0
x : X
x_F : x ∈ F
key : 1 ≤ 0
⊢ False

Tactic:
exact key.not_gt zero_lt_one

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

Goal state before:
pp: X : Type u_1
U : SetRel X X
T : X → X
F : Set X
inst✝¹ : U.IsRefl
inst✝ : U.IsSymm
n : ℕ
⊢ coverMincard T F (U ○ U) n ≤ netMaxcard T F U n

Tactic:
rcases eq_top_or_lt_top (netMaxcard T F U n) with h | h
  · exact h ▸ le_top
  obtain ⟨s, s_net, s_card⟩ := (netMaxcard_finite_iff T F U n).1 h
  rw [← s_card]
  apply IsDynCoverOf.coverMincard_le_card
  --  We have to check that `s` is a cover for `dynEntourage T F (U ○ U) n`.
  -- If `s` is not a cover, then we can add to `s` a point `x` which is not covered
  -- and get a new net. This contradicts the maximality of `s`.
  rw [IsDynCoverOf, isCover_iff_subset_iUnion_ball]
  by_contra h
  obtain ⟨x, x_F, x_uncov⟩ := not_subset.1 h
  simp only [Finset.mem_coe, mem_iUnion, exists_prop, not_exists, not_and] at x_uncov
  have larger_net : IsDynNetIn T F U n (insert x s) := by
    refine ⟨insert_subset x_F s_net.1, pairwiseDisjoint_insert.2 ⟨s_net.2, ?_⟩⟩
    refine fun y y_s _ ↦ disjoint_left.2 fun z z_x z_y ↦ x_uncov y y_s ?_
    exact mem_ball_dynEntourage_comp T n x y (nonempty_of_mem ⟨z_x, z_y⟩)
  rw [← s.coe_insert x] at larger_net
  apply larger_net.card_le_netMaxcard.not_gt
  rw [← s_card, Nat.cast_lt]
  refine (lt_add_one s.card).trans_eq (s.card_insert_of_notMem fun x_s ↦ ?_).symm
  exact x_uncov x x_s (ball_mono (dynEntourage_monotone T n SetRel.left_subset_comp) x <|
    SetRel.rfl (dynEntourage T U n))

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
h_add : (μ + ν).rnDeriv (μ + ν) =ᵐ[ν] μ.rnDeriv (μ + ν) + ν.rnDeriv (μ + ν)
h_one_add : ∀ᵐ (x : α) ∂ν, (μ + ν).rnDeriv (μ + ν) x = (fun x ↦ 1) x
this : μ.rnDeriv (μ + ν) =ᵐ[ν] fun x ↦ 1 - (μ.rnDeriv ν x + 1)⁻¹
a : α
⊢ μ.rnDeriv (μ + ν) a = 1 - (μ.rnDeriv ν a + 1)⁻¹ →
    μ.rnDeriv ν a < ∞ → μ.rnDeriv (μ + ν) a = μ.rnDeriv ν a / (μ.rnDeriv ν a + 1)

Tactic:
ha

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
h_add : (μ + ν).rnDeriv (μ + ν) =ᵐ[ν] μ.rnDeriv (μ + ν) + ν.rnDeriv (μ + ν)
h_one_add : ∀ᵐ (x : α) ∂ν, (μ + ν).rnDeriv (μ + ν) x = (fun x ↦ 1) x
this : μ.rnDeriv (μ + ν) =ᵐ[ν] fun x ↦ 1 - (μ.rnDeriv ν x + 1)⁻¹
a : α
ha : μ.rnDeriv (μ + ν) a = 1 - (μ.rnDeriv ν a + 1)⁻¹
⊢ μ.rnDeriv ν a < ∞ → μ.rnDeriv (μ + ν) a = μ.rnDeriv ν a / (μ.rnDeriv ν a + 1)
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case h₂
F : Type u_1
inst✝ : Field F
s : Multiset F[X]
hs : ∀ p ∈ s, Group.IsSolvable p.Gal
p : F[X]
t : Multiset F[X]
⊢ p ∈ s → t ⊆ s → Group.IsSolvable t.prod.Gal → Group.IsSolvable (insert p t).prod.Gal

Tactic:
hps

Goal state after:
case h₂
F : Type u_1
inst✝ : Field F
s : Multiset F[X]
hs : ∀ p ∈ s, Group.IsSolvable p.Gal
p : F[X]
t : Multiset F[X]
hps : p ∈ s
⊢ t ⊆ s → Group.IsSolvable t.prod.Gal → Group.IsSolvable (insert p t).prod.Gal
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
⊢ Measurable (μ.rnDeriv ν)

pp: case refine_3
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
s : Set α
x✝¹ : MeasurableSet s
x✝ : ν s < ∞
⊢ ∫⁻ (x : α) in s, (map f μ).rnDeriv (map f ν) (f x) ∂ν = ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν

Tactic:
· exact Measure.measurable_rnDeriv _ _

Goal state after:
case refine_3
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
s : Set α
x✝¹ : MeasurableSet s
x✝ : ν s < ∞
⊢ ∫⁻ (x : α) in s, (map f μ).rnDeriv (map f ν) (f x) ∂ν = ∫⁻ (x : α) in s, μ.rnDeriv ν 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 ν
s : Set β
hs : MeasurableSet s
a : α
⊢ (map f μ).rnDeriv (map f ν) (f a) = μ.rnDeriv ν a → a ∈ f ⁻¹' s → μ.rnDeriv ν a = (map f μ).rnDeriv (map f ν) (f a)

Tactic:
ha

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
s : Set β
hs : MeasurableSet s
a : α
ha : (map f μ).rnDeriv (map f ν) (f a) = μ.rnDeriv ν a
⊢ a ∈ f ⁻¹' s → μ.rnDeriv ν a = (map f μ).rnDeriv (map f ν) (f a)
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μν : μ ≪ ν
⊢ Integrable (fun x ↦ (μ.rnDeriv ν x).toReal • f x) ν ↔ Integrable f μ

Tactic:
nth_rw 2 [← withDensity_rnDeriv_eq μ ν hμν]
  rw [← integrable_withDensity_iff_integrable_smul' (E := E)
    (measurable_rnDeriv μ ν) (rnDeriv_lt_top μ ν)]

Goal state after:
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: 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 : N ≃[L] P
⊢ Function.Injective h.comp

Tactic:
by
  intro f g hfg
  ext x; exact h.injective (congr_fun (congr_arg DFunLike.coe hfg) x)

Goal state after:
Module: Mathlib.ModelTheory.Ultraproducts

Goal state before:
pp: case refine_2
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → L.Structure (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
k : ℕ
φ : L.BoundedFormula β (k + 1)
ih :
  ∀ (v : Fin (k + 1) → (a : α) → M a),
    (φ.Realize (fun i ↦ Quotient.mk' (x i)) fun i ↦ Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in ↑u, φ.Realize (fun i ↦ x i a) fun i ↦ v i a
v : Fin k → (a : α) → M a
m : (a : α) → M a
a : α
i : Fin k
x✝ : Fin.snoc v m i.succ a = Fin.snoc (fun i ↦ v i a) (m a) i.succ
⊢ Fin.snoc v m i.castSucc a = Fin.snoc (fun i ↦ v i a) (m a) i.castSucc

Tactic:
· simp only [Fin.snoc_castSucc]

Goal state after:
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
φ : M ↪ₑ[L] N
n : ℕ
f : L.Functions n
x : Fin n → M
h : (Formula.graph f).Realize (⇑φ ∘ Fin.cons (funMap f x) x) ↔ funMap f x = funMap f x
⊢ φ (funMap f x) = funMap f (⇑φ ∘ x)

Tactic:
Fin.comp_cons,

Goal state after:
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
φ : M ↪ₑ[L] N
n : ℕ
f : L.Functions n
x : Fin n → M
h : (Formula.graph f).Realize (Fin.cons (φ (funMap f x)) (⇑φ ∘ x)) ↔ funMap f x = funMap f x
⊢ φ (funMap f x) = funMap f (⇑φ ∘ x)
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
n : ℕ
φ : L.BoundedFormula α n
f : ↥φ.freeVarFinset → β
v : β → M
xs : Fin n → M
v' : α → M
hv' : ∀ (a : ↥φ.freeVarFinset), v (f a) = v' ↑a
⊢ (φ.restrictFreeVar f).Realize v xs ↔ φ.Realize v' xs

Tactic:
induction φ with
  | falsum => rfl
  | equal =>
    simp only [Realize, restrictFreeVar]
    rw [realize_restrictVarLeft v' (by simp [hv']), realize_restrictVarLeft v' (by simp [hv'])]
    simp
  | rel =>
    simp only [Realize, restrictFreeVar]
    congr!
    rw [realize_restrictVarLeft v' (by simp [hv'])]
    simp
  | imp _ _ ih1 ih2 =>
    simp only [Realize, restrictFreeVar]
    rw [ih1, ih2] <;> simp [hv']
  | all _ ih3 =>
    simp only [restrictFreeVar, Realize]
    refine forall_congr' (fun _ => ?_)
    rw [ih3]; simp [hv']

Goal state after:
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
A s : Set M
a : M
⊢ a ∈ A → a ∈ ↑((closure L[[↑A]]).toFun s)

Tactic:
ha

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
A s : Set M
a : M
ha : a ∈ A
⊢ a ∈ ↑((closure L[[↑A]]).toFun s)
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
v' : Fin 0 → M
⊢ Realize (Formula.iExs γ φ) v v' ↔ ∃ i, φ.Realize (Sum.elim v i)

Tactic:
rw [← Formula.realize_iExs, iff_iff_eq]

Goal state after:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
v' : Fin 0 → M
⊢ Realize (Formula.iExs γ φ) v v' = (Formula.iExs γ φ).Realize v
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
hf : A.Definable L s
⊢ A.Definable L sᶜ

Tactic:
by
  rcases hf with ⟨φ, hφ⟩
  refine ⟨φ.not, ?_⟩
  ext v
  rw [hφ, compl_ofPred, mem_ofPred, mem_ofPred, Formula.realize_not]

Goal state after:
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
h : φ.Realize default (Fin.snoc (Subtype.val ∘ x) a)
⊢ ∃ b, φ.Realize default (Fin.snoc (Subtype.val ∘ x) ↑b)

Tactic:
let φ' : (L.sum L.skolem₁).Functions n := LHom.sumInr.onFunction φ

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
h : φ.Realize default (Fin.snoc (Subtype.val ∘ x) a)
φ' : (L.sum L.skolem₁).Functions n := LHom.sumInr.onFunction φ
⊢ ∃ b, φ.Realize default (Fin.snoc (Subtype.val ∘ x) ↑b)
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
r : L.Relations 2
⊢ M ⊨ r.transitive ↔ IsTrans M fun x y ↦ RelMap r ![x, y]

Tactic:
by
  rw [isTrans_def]
  exact forall₃_congr fun _ _ _ ↦ imp_congr realize_rel₂ <| imp_congr realize_rel₂ realize_rel₂

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type u_1
L : Language
inst✝¹ : L.Structure M
α : Type u_2
β : Type u_3
A : Set M
f : (α → M) → M
inst✝ : Finite α
g : (β → M) → α → M
hg : DefinableMap L A g
hf : DefinableFun L A f
⊢ DefinableFun L A fun v ↦ f (g v)

Tactic:
by
  let G : (Option β → M) → Option α → M := fun w j =>
    match j with
    | none => w none
    | some i => g (w ∘ some) i
  have hG : A.DefinableMap L G := by
    intro i
    cases i with
    | none => fun_prop
    | some j =>
      simpa [tupleGraph] using!
        ((hg j).preimage_comp fun | none => none | some i => some (some i))
  simpa [DefinableFun, G, tupleGraph] using! hf.preimage_map hG

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 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
x✝ : lift.{w', w} κ ≤ lift.{w, w'} #M ∨ lift.{w, w'} #M < lift.{w', w} κ
⊢ ∃ N, (Nonempty (↑N ↪ₑ[L] M) ∨ Nonempty (M ↪ₑ[L] ↑N)) ∧ #↑N = κ

Tactic:
cases le_or_gt (lift.{w'} κ) (Cardinal.lift.{w} #M) with

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α n
⊢ T ⊨ᵇ φ.toFormula ↔ T ⊨ᵇ φ

Tactic:
refine ⟨fun h M v xs => ?_, ?_⟩

Goal state after:
case refine_1
L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α n
h : T ⊨ᵇ φ.toFormula
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
⊢ φ.Realize v xs

case refine_2
L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α n
⊢ T ⊨ᵇ φ → T ⊨ᵇ φ.toFormula
Module: Mathlib.RingTheory.Localization.Cardinality

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
L : Type v
inst✝² : CommRing L
inst✝¹ : Algebra R L
S : Submonoid R
inst✝ : IsLocalization S L
hS : S ≤ R⁰
this : #(Localization S) = #R
⊢ Cardinal.lift.{u, v} #L = Cardinal.lift.{v, u} #R

Tactic:
← lift_inj.{u, v},

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

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
L : Type u
inst✝² : CommRing L
inst✝¹ : Algebra R L
S : Submonoid R
inst✝ : IsLocalization S L
hS : S ≤ R⁰
⊢ #L = #R

Tactic:
by
  simpa using lift_cardinalMk L S hS

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

Goal state before:
pp: case neg
a : ℕ
h : ¬ℵ₀ ≤ ↑a
p : Cardinal.{u_1}
k : ℕ
hp : Prime p
hk : 0 < k
hpk : p ^ k = ↑a
key : p ≤ ↑a
⊢ ∃ n, ↑a = ↑n ∧ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n

Tactic:
lift p to ℕ using key.trans_lt natCast_lt_aleph0

Goal state after:
case neg
a : ℕ
h : ¬ℵ₀ ≤ ↑a
k : ℕ
hk : 0 < k
p : ℕ
hp : Prime ↑p
hpk : ↑p ^ k = ↑a
key : ↑p ≤ ↑a
⊢ ∃ n, ↑a = ↑n ∧ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
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 l - X)

Tactic:
← Fintype.card_eq_nat_card

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 ^ Fintype.card l - X)

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
⊢ Fintype l
Module: Mathlib.FieldTheory.Finite.Polynomial

Goal state before:
pp: K : Type u_1
σ : Type u_2
inst✝ : CommSemiring K
a : K
p : MvPolynomial σ K
⊢ (fun e ↦ (eval e) (a • p)) = (RingHom.id K) a • fun e ↦ (eval e) p

Tactic:
ext e; simp

Goal state after:
Module: Mathlib.Topology.Separation.Connected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
h : TotallyDisconnectedSpace X
⊢ T1Space X

Tactic:
rw [((t1Space_TFAE X).out 0 1 :)]

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
h : TotallyDisconnectedSpace X
⊢ ∀ (x : X), IsClosed[inst✝] {x}
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′
⊢ ∃ ι₀ x c₀, ∃ (_ : ∀ (x : ι₀), (c₀ x)′ = 0), ∃ u₀ v₀, a = ∑ x, c₀ x * logDeriv (u₀ x) + v₀′

Tactic:
apply inst.isLiouville a ι c hc (B.val ∘ u) (B.val v)
    dsimp only [coe_val, Function.comp_apply]
    conv =>
      rhs
      congr
      · rhs
        intro x
        rhs
        apply logDeriv_algebraMap (u x)
      · apply (deriv_algebraMap v)
    simp_rw [IsScalarTower.algebraMap_apply F B K]
    norm_cast

Goal state after:
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
a : PerfectClosure K p
x✝ : ℕ × K
m : ℕ
x : K
⊢ mk K p ((0, 0).1 + (m, x).1, (⇑(frobenius K p))^[(m, x).1] (0, 0).2 * (⇑(frobenius K p))^[(0, 0).1] (m, x).2) =
    mk K p (0, 0)

Tactic:
simp only [zero_add, iterate_zero, id_eq, iterate_map_zero, zero_mul, mk_zero_right]

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

Goal state before:
pp: R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
n : ℕ
hn : Odd n
⊢ ∃ r, x = r ^ n

Tactic:
rcases exists_isRoot_of_odd_natDegree (f := X ^ n - C x) (by simp [hn]) with ⟨r, hr⟩

Goal state after:
R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
n : ℕ
hn : Odd n
r : R
hr : (X ^ n - C x).IsRoot r
⊢ ∃ 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
x : ℕ
⊢ ↑x = 0 ↔ ↑x = 0

Tactic:
← Nat.cast_zero,

Goal state after:
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : ℕ
⊢ ↑x = ↑0 ↔ ↑x = 0
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 ^ p ^ n = 0

Tactic:
← Nat.sub_add_cancel ((n.lt_pow_self (Fact.out : p.Prime).one_lt).le),

Goal state after:
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 ^ (p ^ n - n + n) = 0
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: case mpr
G : Type u_1
inst✝¹ : Group G
D H : Subgroup G
inst✝ : D.FiniteIndex
hD_le_H : D ≤ H
t : Set ↥H
ht : IsComplement t ↑(D.subgroupOf H) ∧ 1 ∈ t
hf : t.Finite
x : G
⊢ x ∈ H → ∃ y ∈ t, ∃ d ∈ D, ↑y * d = x

Tactic:
· intro hx
    exact ⟨_, (ht.1.toLeftFun ⟨x, hx⟩).2, _,
      ht.1.inv_toLeftFun_mul_mem ⟨x, hx⟩, mul_inv_cancel_left _ _⟩

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

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
H : Transcendental F x
⊢ LinearIndependent F fun a ↦ (x - (algebraMap F E) a)⁻¹

Tactic:
rw [transcendental_iff] at H

Goal state after:
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
H : ∀ (p : F[X]), (aeval x) p = 0 → p = 0
⊢ LinearIndependent F fun a ↦ (x - (algebraMap F E) a)⁻¹