mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.ZMod.Coprime

Goal state before:
pp: a : ℤ
p : ℕ
pp : Fact (Nat.Prime p)
⊢ ↑a = 0 ↔ a.gcd ↑p ≠ 1

Tactic:
rw [Ne, Int.gcd_comm, ← Int.isCoprime_iff_gcd_eq_one,
    (Nat.prime_iff_prime_int.1 pp.1).coprime_iff_not_dvd, Classical.not_not,
    intCast_zmod_eq_zero_iff_dvd]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
f : α → α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
e : α ≃ᵐ β
h : MeasurePreserving (⇑e) μ μ'
this : MeasurePreserving (⇑e ∘ f ∘ ⇑e.symm) μ' μ' ↔ MeasurePreserving f μ μ
⊢ Ergodic (⇑e ∘ f ∘ ⇑e.symm) μ' ↔ Ergodic f μ

Tactic:
replace h : PreErgodic (e ∘ f ∘ e.symm) μ' ↔ PreErgodic f μ := h.preErgodic_conjugate_iff

Goal state after:
α : Type u_1
m : MeasurableSpace α
f : α → α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
e : α ≃ᵐ β
this : MeasurePreserving (⇑e ∘ f ∘ ⇑e.symm) μ' μ' ↔ MeasurePreserving f μ μ
h : PreErgodic (⇑e ∘ f ∘ ⇑e.symm) μ' ↔ PreErgodic f μ
⊢ Ergodic (⇑e ∘ f ∘ ⇑e.symm) μ' ↔ Ergodic f μ
Module: Mathlib.Dynamics.Ergodic.Action.Basic

Goal state before:
pp: case refine_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → α
hf : Measurable f
x✝ :
  MeasurePreserving f μ μ ∧
    ∀ {s : Set α}, MeasurableSet s → (∀ (g : IterateMulAct f), (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s) → EventuallyConst s (ae μ)
h₁ : MeasurePreserving f μ μ
h₂ :
  ∀ {s : Set α}, MeasurableSet s → (∀ (g : IterateMulAct f), (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s) → EventuallyConst s (ae μ)
s : Set α
hm : MeasurableSet s
hs : f ⁻¹' s = s
n : IterateMulAct f
⊢ (fun x ↦ n • x) ⁻¹' s =ᵐ[μ] s

Tactic:
← Function.IsFixedPt.preimage_iterate hs n.val

Goal state after:
case refine_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → α
hf : Measurable f
x✝ :
  MeasurePreserving f μ μ ∧
    ∀ {s : Set α}, MeasurableSet s → (∀ (g : IterateMulAct f), (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s) → EventuallyConst s (ae μ)
h₁ : MeasurePreserving f μ μ
h₂ :
  ∀ {s : Set α}, MeasurableSet s → (∀ (g : IterateMulAct f), (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s) → EventuallyConst s (ae μ)
s : Set α
hm : MeasurableSet s
hs : f ⁻¹' s = s
n : IterateMulAct f
⊢ (fun x ↦ n • x) ⁻¹' s =ᵐ[μ] f^[n.val] ⁻¹' s
Module: Mathlib.MeasureTheory.Measure.ContinuousPreimage

Goal state before:
pp: case h₁
α : 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)
s : Set Y
hfg : Tendsto f l (𝓝 g)
hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a)) μ ν
hg : MeasurePreserving (⇑g) μ ν
hs : NullMeasurableSet s ν
hνs : ν s ≠ ∞
this✝ : ν.InnerRegularCompactLTTop
ε : ℝ≥0∞
hε : ε > 0
this :
  ∀ {s : Set Y},
    NullMeasurableSet s ν → ν s ≠ ∞ → ∀ ε > 0, IsOpen[inst✝⁵] s → ∀ᶠ (x : α) in l, μ ((⇑(f x) ⁻¹' s) ∆ (⇑g ⁻¹' s)) ≤ ε
hso : ¬IsOpen[inst✝⁵] s
H : 0 < ε / 3
U : Set Y
hUo : IsOpen[inst✝⁵] U
hU : ν U < ∞
hmU : NullMeasurableSet U ν
hUs : ν (U ∆ s) ≤ ε / 3
a : α
hfa : MeasurePreserving (⇑(f a)) μ ν
ha : μ ((⇑(f a) ⁻¹' U) ∆ (⇑g ⁻¹' U)) ≤ ε / 3
⊢ μ ((⇑(f a) ⁻¹' s) ∆ (⇑(f a) ⁻¹' U)) ≤ ε / 3

Tactic:
← preimage_symmDiff,

Goal state after:
case h₁
α : 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)
s : Set Y
hfg : Tendsto f l (𝓝 g)
hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a)) μ ν
hg : MeasurePreserving (⇑g) μ ν
hs : NullMeasurableSet s ν
hνs : ν s ≠ ∞
this✝ : ν.InnerRegularCompactLTTop
ε : ℝ≥0∞
hε : ε > 0
this :
  ∀ {s : Set Y},
    NullMeasurableSet s ν → ν s ≠ ∞ → ∀ ε > 0, IsOpen[inst✝⁵] s → ∀ᶠ (x : α) in l, μ ((⇑(f x) ⁻¹' s) ∆ (⇑g ⁻¹' s)) ≤ ε
hso : ¬IsOpen[inst✝⁵] s
H : 0 < ε / 3
U : Set Y
hUo : IsOpen[inst✝⁵] U
hU : ν U < ∞
hmU : NullMeasurableSet U ν
hUs : ν (U ∆ s) ≤ ε / 3
a : α
hfa : MeasurePreserving (⇑(f a)) μ ν
ha : μ ((⇑(f a) ⁻¹' U) ∆ (⇑g ⁻¹' U)) ≤ ε / 3
⊢ μ (⇑(f a) ⁻¹' s ∆ U) ≤ ε / 3
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f g : CircleDeg1Lift
h : Commute f g
n : ℕ
⊢ dist (((f * g) ^ n) 0) ((f ^ n) 0 + (g ^ n) 0) ≤ 1

Tactic:
rw [h.mul_pow, dist_comm]

Goal state after:
f g : CircleDeg1Lift
h : Commute f g
n : ℕ
⊢ dist ((f ^ n) 0 + (g ^ n) 0) ((f ^ n * g ^ n) 0) ≤ 1
Module: Mathlib.MeasureTheory.Measure.ContinuousPreimage

Goal state before:
pp: case h₂
α : 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)
s : Set Y
hfg : Tendsto f l (𝓝 g)
hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a)) μ ν
hg : MeasurePreserving (⇑g) μ ν
hs : NullMeasurableSet s ν
hνs : ν s ≠ ∞
this✝ : ν.InnerRegularCompactLTTop
ε : ℝ≥0∞
hε : ε > 0
this :
  ∀ {s : Set Y},
    NullMeasurableSet s ν → ν s ≠ ∞ → ∀ ε > 0, IsOpen[inst✝⁵] s → ∀ᶠ (x : α) in l, μ ((⇑(f x) ⁻¹' s) ∆ (⇑g ⁻¹' s)) ≤ ε
hso : ¬IsOpen[inst✝⁵] s
H : 0 < ε / 3
U : Set Y
hUo : IsOpen[inst✝⁵] U
hU : ν U < ∞
hmU : NullMeasurableSet U ν
hUs : ν (U ∆ s) ≤ ε / 3
a : α
hfa : MeasurePreserving (⇑(f a)) μ ν
ha : μ ((⇑(f a) ⁻¹' U) ∆ (⇑g ⁻¹' U)) ≤ ε / 3
⊢ μ ((⇑g ⁻¹' U) ∆ (⇑g ⁻¹' s)) ≤ ε / 3

Tactic:
← preimage_symmDiff,

Goal state after:
case h₂
α : 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)
s : Set Y
hfg : Tendsto f l (𝓝 g)
hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a)) μ ν
hg : MeasurePreserving (⇑g) μ ν
hs : NullMeasurableSet s ν
hνs : ν s ≠ ∞
this✝ : ν.InnerRegularCompactLTTop
ε : ℝ≥0∞
hε : ε > 0
this :
  ∀ {s : Set Y},
    NullMeasurableSet s ν → ν s ≠ ∞ → ∀ ε > 0, IsOpen[inst✝⁵] s → ∀ᶠ (x : α) in l, μ ((⇑(f x) ⁻¹' s) ∆ (⇑g ⁻¹' s)) ≤ ε
hso : ¬IsOpen[inst✝⁵] s
H : 0 < ε / 3
U : Set Y
hUo : IsOpen[inst✝⁵] U
hU : ν U < ∞
hmU : NullMeasurableSet U ν
hUs : ν (U ∆ s) ≤ ε / 3
a : α
hfa : MeasurePreserving (⇑(f a)) μ ν
ha : μ ((⇑(f a) ⁻¹' U) ∆ (⇑g ⁻¹' U)) ≤ ε / 3
⊢ μ (⇑g ⁻¹' U ∆ s) ≤ ε / 3
Module: Mathlib.Dynamics.Ergodic.Conservative

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
h0 : μ s ≠ 0
t : ℕ → Set α := fun n ↦ s ∩ f^[n] ⁻¹' s
H : {n | μ (s ∩ f^[n] ⁻¹' s) ≠ 0}.Finite
⊢ ∃ N, μ (t N) ≠ 0 ∧ ∀ n > N, μ (t n) = 0

Tactic:
convert! exists_max_image _ (·) H ⟨0, by simpa⟩ using 4

Goal state after:
case e'_2
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
h0 : μ s ≠ 0
t : ℕ → Set α := ⋯
H : {n | μ (s ∩ f^[n] ⁻¹' s) ≠ 0}.Finite
x✝ a✝ : ℕ
⊢ a✝ > x✝ → μ (t a✝) = 0 ↔ a✝ ∈ {n | μ (s ∩ f^[n] ⁻¹' s) ≠ 0} → a✝ ≤ x✝
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen[inst✝] n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst✝] (image2 ϕ v s) ⊆ c
k : Set β := closure[inst✝] (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u ↦ (closure[inst✝] (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ u ∈ f, IsOpen[inst✝] (j u)
hj₂ : k \ n ⊆ ⋃ u ∈ f, j u
g : Set (Set τ)
hg₁ : ∀ u ∈ g, u ∈ f
hg₂ : g.Finite
hg₃ : k \ n ⊆ ⋃ i ∈ g, j i
w : Set τ := (⋂ u ∈ g, u) ∩ v
hw₂ : w ∈ f
hw₃ : k \ n ⊆ (closure[inst✝] (image2 ϕ w s))ᶜ
hw₄ : kᶜ ⊆ (closure[inst✝] (image2 ϕ w s))ᶜ
⊢ nᶜ ⊆ k \ n ∪ kᶜ

Tactic:
rw [union_comm, ← inter_subset, sdiff_eq, inter_comm]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
s : Set α
hμs : μ s ≠ ∞
⊢ ∫ (x : α) in s, (μ.rnDeriv ν x).toReal ∂ν ≤ μ.real s

Tactic:
by
  set t := toMeasurable μ s with ht
  have ht_m : MeasurableSet t := measurableSet_toMeasurable μ s
  have hμt : μ t ≠ ∞ := by rwa [ht, measure_toMeasurable s]
  calc ∫ x in s, (μ.rnDeriv ν x).toReal ∂ν
    ≤ ∫ x in t, (μ.rnDeriv ν x).toReal ∂ν := by
        refine setIntegral_mono_set ?_ ?_ (LE.le.eventuallyLE (subset_toMeasurable _ _))
        · exact integrableOn_toReal_rnDeriv hμt
        · exact ae_of_all _ (by simp)
  _ = (withDensity ν (rnDeriv μ ν)).real t := setIntegral_toReal_rnDeriv_eq_withDensity' ht_m
  _ ≤ μ.real t := by
        simp only [measureReal_def]
        gcongr
        apply withDensity_rnDeriv_le
  _ = μ.real s := by rw [measureReal_def, measureReal_def, measure_toMeasurable s]

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

Goal state before:
pp: X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
⊢ coverEntropyInfEntourage T F univ = 0

Tactic:
rw [← expGrowthInf_const one_ne_zero one_ne_top, coverEntropyInfEntourage]

Goal state after:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
⊢ (expGrowthInf fun n ↦ ↑(coverMincard T F univ n)) = expGrowthInf fun x ↦ 1
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 : α
ha : μ.rnDeriv (μ + ν) a = 1 - (μ.rnDeriv ν a + 1)⁻¹
ha_lt_top : μ.rnDeriv ν a < ∞
⊢ 1 - (μ.rnDeriv ν a + 1)⁻¹ = μ.rnDeriv ν a / (μ.rnDeriv ν a + 1)

Tactic:
div_eq_mul_inv

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)⁻¹
ha_lt_top : μ.rnDeriv ν a < ∞
⊢ 1 - (μ.rnDeriv ν a + 1)⁻¹ = μ.rnDeriv ν a * (μ.rnDeriv ν a + 1)⁻¹
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite ξ
hμ : μ ≪ ξ
hν : ν ≪ ξ
⊢ (fun x ↦ μ.rnDeriv ξ x / ν.rnDeriv ξ x) =ᵐ[μ + ν] fun x ↦ μ.rnDeriv (μ + ν) x / ν.rnDeriv (μ + ν) x

Tactic:
have h1 : μ.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ =ᵐ[ξ] μ.rnDeriv ξ :=
    Measure.rnDeriv_mul_rnDeriv (rfl.absolutelyContinuous.add_right _)

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite ξ
hμ : μ ≪ ξ
hν : ν ≪ ξ
h1 : μ.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ =ᵐ[ξ] μ.rnDeriv ξ
⊢ (fun x ↦ μ.rnDeriv ξ x / ν.rnDeriv ξ x) =ᵐ[μ + ν] fun x ↦ μ.rnDeriv (μ + ν) x / ν.rnDeriv (μ + ν) x
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
⊢ Function.Injective fun x ↦ x.toHom

Tactic:
by
  intro f f' h
  ext
  exact congr_fun (congr_arg (↑) h) _

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case cons
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n : ℕ
v : α → M
xs : Fin n → M
φ : L.BoundedFormula α n
l : List (L.BoundedFormula α n)
ih : (List.foldr (fun x1 x2 ↦ x1 ⊓ x2) ⊤ l).Realize v xs ↔ ∀ φ ∈ l, φ.Realize v xs
⊢ (List.foldr (fun x1 x2 ↦ x1 ⊓ x2) ⊤ (φ :: l)).Realize v xs ↔ ∀ φ_1 ∈ φ :: l, φ_1.Realize v xs

Tactic:
| cons φ l ih =>

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case cons
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n : ℕ
v : α → M
xs : Fin n → M
φ : L.BoundedFormula α n
l : List (L.BoundedFormula α n)
ih : (List.foldr (fun x1 x2 ↦ x1 ⊔ x2) ⊥ l).Realize v xs ↔ ∃ φ ∈ l, φ.Realize v xs
⊢ (List.foldr (fun x1 x2 ↦ x1 ⊔ x2) ⊥ (φ :: l)).Realize v xs ↔ ∃ φ_1 ∈ φ :: l, φ_1.Realize v xs

Tactic:
| cons φ l ih =>

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n : ℕ
l : List (L.BoundedFormula α n)
v : α → M
xs : Fin n → M
⊢ (List.foldr (fun x1 x2 ↦ x1 ⊔ x2) ⊥ l).Realize v xs ↔ ∃ φ ∈ l, φ.Realize v xs

Tactic:
induction l with
  | nil => simp
  | cons φ l ih =>
    simp_rw [List.foldr_cons, realize_sup, ih, List.mem_cons, or_and_right, exists_or,
      exists_eq_left]

Goal state after:
Module: Mathlib.ModelTheory.Ultraproducts

Goal state before:
pp: α : 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
φ : L.Formula β
x : β → (a : α) → M a
⊢ (φ.Realize fun i ↦ Quotient.mk' (x i)) ↔ ∀ᶠ (a : α) in ↑u, φ.Realize fun i ↦ x i a

Tactic:
simp_rw [Formula.Realize, ← boundedFormula_realize_cast φ x, iff_eq_eq]
  exact congr rfl (Subsingleton.elim _ _)

Goal state after:
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case cons
L : Language
α : Type u'
h :
  ∀ (φ : (n : ℕ) × L.BoundedFormula α n) (l' : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode (φ.snd.listEncode ++ l') = φ :: listDecode l'
φ : (n : ℕ) × L.BoundedFormula α n
l : List ((n : ℕ) × L.BoundedFormula α n)
ih : listDecode (flatMap (fun φ ↦ φ.snd.listEncode) l) = l
⊢ listDecode (flatMap (fun φ ↦ φ.snd.listEncode) (φ :: l)) = φ :: l

Tactic:
| cons φ l ih =>

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 a, φ.Realize v (snoc xs a)) → ∃ xs, φ.Realize v xs

Tactic:
rintro ⟨xs, x, h⟩

Goal state after:
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
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case rel.hc
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 ⊕ ℕ)
h :
  ∀ (i : Fin φ_l),
    (List.map Sum.getLeft? (List.map (fun i ↦ Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l))[i]?.join =
      some ⟨φ_n, ts i⟩
⊢ ∀ (i : Fin φ_l),
    (List.map Sum.getLeft?
              (List.map (fun i ↦ Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l))[i]?.join.isSome =
      true

pp: case rel
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 ⊕ ℕ)
h :
  ∀ (i : Fin φ_l),
    (List.map Sum.getLeft? (List.map (fun i ↦ Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l))[i]?.join =
      some ⟨φ_n, ts i⟩
⊢ (if h' :
          ∀ (i : Fin φ_l),
            ((List.map Sum.getLeft?
                          (List.map (fun i ↦ Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l))[i]?.join.get
                  ⋯).fst =
              ⟨φ_n, rel φ_R ts⟩.fst then
        ⟨⟨φ_n, rel φ_R ts⟩.fst,
          rel φ_R fun i ↦
            ⋯.mp
              ((List.map Sum.getLeft?
                          (List.map (fun i ↦ Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l))[i]?.join.get
                  ⋯).snd⟩
      else default) ::
      listDecode (drop φ_l (List.map (fun i ↦ Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l)) =
    ⟨φ_n, rel φ_R ts⟩ :: listDecode l

Tactic:
· exact fun i => Option.isSome_iff_exists.2 ⟨⟨_, ts i⟩, h i⟩

Goal state after:
case rel
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 ⊕ ℕ)
h :
  ∀ (i : Fin φ_l),
    (List.map Sum.getLeft? (List.map (fun i ↦ Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l))[i]?.join =
      some ⟨φ_n, ts i⟩
⊢ (if h' :
          ∀ (i : Fin φ_l),
            ((List.map Sum.getLeft?
                          (List.map (fun i ↦ Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l))[i]?.join.get
                  ⋯).fst =
              ⟨φ_n, rel φ_R ts⟩.fst then
        ⟨⟨φ_n, rel φ_R ts⟩.fst,
          rel φ_R fun i ↦
            ⋯.mp
              ((List.map Sum.getLeft?
                          (List.map (fun i ↦ Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l))[i]?.join.get
                  ⋯).snd⟩
      else default) ::
      listDecode (drop φ_l (List.map (fun i ↦ Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l)) =
    ⟨φ_n, rel φ_R ts⟩ :: listDecode l
Module: Mathlib.ModelTheory.ElementarySubstructures

Goal state before:
pp: L : Language
M : Type u_1
inst✝ : L.Structure M
S : L.ElementarySubstructure M
D : Set M
x : M
hx : x ∈ D
φ : L[[↑↑S]].Formula (Fin 1)
hφ : {x | x 0 ∈ D} = ofPred φ.Realize
hφx : φ.Realize ![x]
ψ : L[[↑↑S]].Sentence := iExs (Fin 1) (relabel Sum.inr φ)
hψM : M ⊨ ψ
v' : Fin 1 → ↥S
hv' : φ.Realize v'
⊢ φ.Realize (Subtype.val ∘ v')

Tactic:
simp only [Formula.Realize, ← BoundedFormula.realize_constantsVarsEquiv,
      ← S.subtype.map_boundedFormula] at hv'

Goal state after:
L : Language
M : Type u_1
inst✝ : L.Structure M
S : L.ElementarySubstructure M
D : Set M
x : M
hx : x ∈ D
φ : L[[↑↑S]].Formula (Fin 1)
hφ : {x | x 0 ∈ D} = ofPred φ.Realize
hφx : φ.Realize ![x]
ψ : L[[↑↑S]].Sentence := iExs (Fin 1) (relabel Sum.inr φ)
hψM : M ⊨ ψ
v' : Fin 1 → ↥S
hv' :
  (BoundedFormula.constantsVarsEquiv φ).Realize (⇑S.subtype ∘ Sum.elim (fun a ↦ ↑(L.con a)) v') (⇑S.subtype ∘ default)
⊢ φ.Realize (Subtype.val ∘ v')
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: 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

pp: case refine_2
L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α n
⊢ T ⊨ᵇ φ → T ⊨ᵇ φ.toFormula

Tactic:
· have h' : φ.toFormula.Realize (Sum.elim v xs) := h.realize_formula M
    simp only [BoundedFormula.realize_toFormula, Sum.elim_comp_inl, Sum.elim_comp_inr] at h'
    exact h'

Goal state after:
case refine_2
L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α n
⊢ T ⊨ᵇ φ → T ⊨ᵇ φ.toFormula
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
inst✝ : Finite X
x : X
s : ↥S
⊢ ∃ a, (fun x ↦ x /ₒ 1) a = x /ₒ s

Tactic:
obtain ⟨i, j, hne, heq⟩ := Finite.exists_ne_map_eq_of_infinite (α := ℕ) (s ^ · • x)

Goal state after:
R : Type u
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type v
inst✝¹ : MulAction R X
inst✝ : Finite X
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i • x = s ^ j • x
⊢ ∃ a, (fun x ↦ x /ₒ 1) a = x /ₒ s
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 ^ Fintype.card l - X)

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
⊢ Fintype l

Tactic:
exact FiniteField.isSplittingField_sub l k

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

Goal state before:
pp: R : Type u_1
inst✝⁷ : Field R
inst✝⁶ : Differential R
a✝ b : R
F : Type u_2
inst✝⁵ : Field F
inst✝⁴ : Differential F
inst✝³ : CharZero F
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F K
default : { _a // DifferentialAlgebra F K } := ⟨differentialFiniteDimensional F K, ⋯⟩
x✝ : { _a // DifferentialAlgebra F K }
a : Differential K
ha : DifferentialAlgebra F K
x : K
⊢ (fun x_1 ↦ (aeval x) (mapCoeffs (minpoly F x)) + (aeval x) (derivative (minpoly F x)) * x_1) x′ =
    (fun x_1 ↦ (aeval x) (mapCoeffs (minpoly F x)) + (aeval x) (derivative (minpoly F x)) * x_1) x′

Tactic:
conv_lhs => apply (deriv_aeval_eq ..).symm

Goal state after:
R : Type u_1
inst✝⁷ : Field R
inst✝⁶ : Differential R
a✝ b : R
F : Type u_2
inst✝⁵ : Field F
inst✝⁴ : Differential F
inst✝³ : CharZero F
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F K
default : { _a // DifferentialAlgebra F K } := ⟨differentialFiniteDimensional F K, ⋯⟩
x✝ : { _a // DifferentialAlgebra F K }
a : Differential K
ha : DifferentialAlgebra F K
x : K
⊢ ((aeval x) (minpoly F x))′ =
    (fun x_1 ↦ (aeval x) (mapCoeffs (minpoly F x)) + (aeval x) (derivative (minpoly F x)) * x_1) 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
A : Type u_3
inst✝⁶ : Field A
inst✝⁵ : Algebra K A
inst✝⁴ : Algebra F A
inst✝³ : Differential A
inst✝² : IsScalarTower F K A
inst✝¹ : ContainConstants F K
inst1 : IsLiouville F K
inst2 : IsLiouville K A
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → A
v : A
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
ι₀ : Type
w✝ : Fintype ι₀
c₀ : ι₀ → K
hc₀ : ∀ (x : ι₀), (c₀ x)′ = 0
u₀ : ι₀ → K
v₀ : K
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:
have hc (x : ι₀) := mem_range_of_deriv_eq_zero F (hc₀ x)

Goal state after:
F : Type u_1
K : Type u_2
inst✝¹² : Field F
inst✝¹¹ : Field K
inst✝¹⁰ : Differential F
inst✝⁹ : Differential K
inst✝⁸ : Algebra F K
inst✝⁷ : DifferentialAlgebra F K
A : Type u_3
inst✝⁶ : Field A
inst✝⁵ : Algebra K A
inst✝⁴ : Algebra F A
inst✝³ : Differential A
inst✝² : IsScalarTower F K A
inst✝¹ : ContainConstants F K
inst1 : IsLiouville F K
inst2 : IsLiouville K A
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc✝ : ∀ (x : ι), (c x)′ = 0
u : ι → A
v : A
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
ι₀ : Type
w✝ : Fintype ι₀
c₀ : ι₀ → K
hc₀ : ∀ (x : ι₀), (c₀ x)′ = 0
u₀ : ι₀ → K
v₀ : K
h₀ : ↑a = ∑ x, c₀ x * logDeriv (u₀ x) + v₀′
hc : ∀ (x : ι₀), c₀ x ∈ (algebraMap F K).range
⊢ ∃ ι₀ x c₀, ∃ (_ : ∀ (x : ι₀), (c₀ x)′ = 0), ∃ u₀ v₀, a = ∑ x, c₀ x * logDeriv (u₀ x) + v₀′
Module: Mathlib.FieldTheory.CardinalEmb

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i j : (Module.rank F E).ord.ToType
h : i < j
⊢ φ i < φ j

Tactic:
by
  have least := isLeast_leastExt (F := F) (E := E)
  by_contra!
  obtain eq | lt := this.eq_or_lt
  · exact (least j).1 (subset_adjoin _ _ ⟨i, h, congr_arg b eq.symm⟩)
  · refine ((least i).2 <| mt (adjoin.mono _ _ _ (image_mono ?_) ·) (least j).1).not_gt lt
    exact fun k (hk : k < i) ↦ hk.trans h

Goal state after: