mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case right.ST
α : Type u
β : Type v
R : α → β → Prop
S✝ : WSeq (WSeq α)
T✝ : WSeq (WSeq β)
h✝ : LiftRel (LiftRel R) S✝ T✝
s1 : WSeq α
s2 : WSeq β
x✝¹ :
  (fun s1 s2 ↦ ∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) s1 s2
s : WSeq α
t : WSeq β
S : WSeq (WSeq α)
T : WSeq (WSeq β)
h1 : s1 = s.append S.join
h2 : s2 = t.append T.join
st : LiftRel R s t
ST : LiftRel (LiftRel R) S T
o : Option (α × WSeq α)
p : Option (β × WSeq β)
h : LiftRelO R (LiftRel R) o p
x✝ : LiftRelO R (LiftRel R) none none
b : Option (β × WSeq β)
mb : b ∈ T.join.destruct
⊢ LiftRel (swap (LiftRel R)) ?m.340 S

Tactic:
← LiftRel.swap

Goal state after:
case right.ST
α : Type u
β : Type v
R : α → β → Prop
S✝ : WSeq (WSeq α)
T✝ : WSeq (WSeq β)
h✝ : LiftRel (LiftRel R) S✝ T✝
s1 : WSeq α
s2 : WSeq β
x✝¹ :
  (fun s1 s2 ↦ ∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) s1 s2
s : WSeq α
t : WSeq β
S : WSeq (WSeq α)
T : WSeq (WSeq β)
h1 : s1 = s.append S.join
h2 : s2 = t.append T.join
st : LiftRel R s t
ST : LiftRel (LiftRel R) S T
o : Option (α × WSeq α)
p : Option (β × WSeq β)
h : LiftRelO R (LiftRel R) o p
x✝ : LiftRelO R (LiftRel R) none none
b : Option (β × WSeq β)
mb : b ∈ T.join.destruct
⊢ swap (LiftRel (LiftRel R)) ?m.340 S
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
xs : Vector α n
ys : Vector β n
f₁ : α → β → σ₁ → σ₁ × γ
f₂ : α → β → σ₂ → σ₂ × γ
s₁ : σ₁
s₂ : σ₂
h :
  ∃ R, R s₁ s₂ ∧ ∀ {s : σ₁} {q : σ₂} (a : α) (b : β), R s q → R (f₁ a b s).1 (f₂ a b q).1 ∧ (f₁ a b s).2 = (f₂ a b q).2
⊢ (mapAccumr₂ f₁ xs ys s₁).2 = (mapAccumr₂ f₂ xs ys s₂).2

Tactic:
by
  rcases h with ⟨R, h₀, hR⟩
  exact (mapAccumr₂_bisim R h₀ hR).2

Goal state after:
Module: Mathlib.Data.WSeq.Defs

Goal state before:
pp: α : Type u
s : WSeq α
⊢ s.length = Computation.map List.length s.toList

Tactic:
by
  refine
    Computation.eq_of_bisim
      (fun c1 c2 =>
        ∃ (l : List α) (s : WSeq α),
          c1 = Computation.corec (fun ⟨n, s⟩ =>
            match Seq.destruct s with
            | none => Sum.inl n
            | some (none, s') => Sum.inr (n, s')
            | some (some _, s') => Sum.inr (n + 1, s')) (l.length, s) ∧
            c2 = Computation.map List.length (Computation.corec (fun ⟨l, s⟩ =>
              match Seq.destruct s with
              | none => Sum.inl l.reverse
              | some (none, s') => Sum.inr (l, s')
              | some (some a, s') => Sum.inr (a::l, s')) (l, s)))
      ?_ ⟨[], s, rfl, rfl⟩
  intro s1 s2 h; rcases h with ⟨l, s, h⟩; rw [h.left, h.right]
  induction s using WSeq.recOn with
  | nil => simp [nil]
  | cons a s => simpa using ⟨a::l, s, by simp, by simp⟩
  | think s => simpa using ⟨l, s, by simp, by simp⟩

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

Goal state before:
pp: G : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : SMul G α
inst✝ : ErgodicSMul G α μ
s : Set α
hm : NullMeasurableSet s μ
h : ∀ (g : G), (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s
⊢ EventuallyConst s (ae μ)

Tactic:
by
  rcases hm with ⟨t, htm, hst⟩
  refine .congr ?_ hst.symm
  refine ErgodicSMul.aeconst_of_forall_preimage_smul_ae_eq htm fun g : G ↦ ?_
  refine .trans (.trans ?_ (h g)) hst
  exact tendsto_smul_ae _ _ hst.symm

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

Goal state before:
pp: G : Type u_1
inst✝ : CommGroup G
n : ℤ
s : Set G
hs : (fun x ↦ x ^ n) ⁻¹' s = s
g : G
j : ℕ
hg : g ^ n ^ j = 1
this : ∀ {g' : G}, g' ^ n ^ j = 1 → g' • s ⊆ s
⊢ g⁻¹ ^ n ^ j = 1

Tactic:
rw [inv_zpow, hg, inv_one]

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup

Goal state before:
pp: case mp
p : ℝ
inst✝ : Fact (0 < p)
a : AddCircle p
ha : addOrderOf a ≠ 0
hd : Dense ↑(AddSubgroup.zmultiples a)
⊢ False

Tactic:
rw [AddSubgroup.coe_zmultiples, ← DenseRange, denseRange_zsmul_iff] at hd

Goal state after:
case mp
p : ℝ
inst✝ : Fact (0 < p)
a : AddCircle p
ha : addOrderOf a ≠ 0
hd : addOrderOf a = 0
⊢ False
Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage

Goal state before:
pp: X : Type u_1
T : X → X
U : SetRel X X
inst✝ : UniformSpace X
h : UniformContinuous T
U_uni : U ∈ 𝓤 X
n : ℕ
⊢ dynEntourage T U n ∈ 𝓤 X

Tactic:
rw [dynEntourage_eq_inter_Ico T U n]
  induction n with
  | zero => simp
  | succ n ih =>
    simp only [iInter_coe_set, mem_Ico, Nat.zero_le, true_and] at ih ⊢
    rw [Set.biInter_lt_succ]
    apply Filter.inter_mem ih
    rw [map_iterate T T n]
    exact uniformContinuous_def.1 (UniformContinuous.iterate T n h) U U_uni

Goal state after:
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 β := ⋯
hk : IsCompact (k \ n)
j : Set τ → Set β := ⋯
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 τ := ⋯
hw₂ : w ∈ f
⊢ ⋃ i ∈ g, j i ⊆ (closure[inst✝] (image2 ϕ w s))ᶜ

Tactic:
simp only [j, iUnion_subset_iff, compl_subset_compl]

Goal state after:
τ : 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
⊢ ∀ i ∈ g, closure[inst✝] (image2 ϕ w s) ⊆ closure[inst✝] (image2 ϕ (i ∩ v) s)
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite ν'
hμν' : μ ⟂ₘ ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') =ᵐ[ν + ν']
    (μ.singularPart ν).rnDeriv (ν + ν') + (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν')
h₂ :
  (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv ν =ᵐ[ν]
    (μ.singularPart ν).rnDeriv ν + (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
h₃ : (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') =ᵐ[ν] (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
h₄ : (μ.singularPart ν).rnDeriv (ν + ν') =ᵐ[ν] 0
h₅ : (μ.singularPart ν).rnDeriv ν =ᵐ[ν] 0
⊢ (μ.singularPart ν).rnDeriv (ν + ν') + (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') =ᵐ[ν]
    (μ.singularPart ν).rnDeriv ν + (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν

Tactic:
filter_upwards [h₃, h₄, h₅] with x hx₃ hx₄ hx₅

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite ν'
hμν' : μ ⟂ₘ ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') =ᵐ[ν + ν']
    (μ.singularPart ν).rnDeriv (ν + ν') + (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν')
h₂ :
  (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv ν =ᵐ[ν]
    (μ.singularPart ν).rnDeriv ν + (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
h₃ : (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') =ᵐ[ν] (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
h₄ : (μ.singularPart ν).rnDeriv (ν + ν') =ᵐ[ν] 0
h₅ : (μ.singularPart ν).rnDeriv ν =ᵐ[ν] 0
x : α
hx₃ : (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') x = (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν x
hx₄ : (μ.singularPart ν).rnDeriv (ν + ν') x = 0 x
hx₅ : (μ.singularPart ν).rnDeriv ν x = 0 x
⊢ ((μ.singularPart ν).rnDeriv (ν + ν') + (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν')) x =
    ((μ.singularPart ν).rnDeriv ν + (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν) x
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: case refine_2
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᵐ[ν + ν']
    (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')
h₂ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᵐ[ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
h₃ : (μ.singularPart ν').rnDeriv (ν + ν') =ᵐ[ν] (μ.singularPart ν').rnDeriv ν
h₄ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᵐ[ν] 0
h₅ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᵐ[ν] 0
⊢ (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᵐ[ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν

Tactic:
filter_upwards [h₃, h₄, h₅] with x hx₃ hx₄ hx₅

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᵐ[ν + ν']
    (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')
h₂ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᵐ[ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
h₃ : (μ.singularPart ν').rnDeriv (ν + ν') =ᵐ[ν] (μ.singularPart ν').rnDeriv ν
h₄ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᵐ[ν] 0
h₅ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᵐ[ν] 0
x : α
hx₃ : (μ.singularPart ν').rnDeriv (ν + ν') x = (μ.singularPart ν').rnDeriv ν x
hx₄ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') x = 0 x
hx₅ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν x = 0 x
⊢ ((μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')) x =
    ((μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν) x
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: case refine_2
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᵐ[ν + ν']
    (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')
h₂ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᵐ[ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
h₃ : (μ.singularPart ν').rnDeriv (ν + ν') =ᵐ[ν] (μ.singularPart ν').rnDeriv ν
⊢ (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᵐ[ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν

pp: case refine_1
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᵐ[ν + ν']
    (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')
h₂ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᵐ[ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
⊢ μ.singularPart ν' ⟂ₘ ν'

Tactic:
· have h₄ : (ν'.withDensity (rnDeriv μ ν')).rnDeriv (ν + ν') =ᵐ[ν] 0 := by
      refine rnDeriv_eq_zero_of_mutuallySingular ?_ h_ac
      exact hνν'.symm.withDensity
    have h₅ : (ν'.withDensity (rnDeriv μ ν')).rnDeriv ν =ᵐ[ν] 0 := by
      rw [rnDeriv_eq_zero]
      exact hνν'.symm.withDensity
    filter_upwards [h₃, h₄, h₅] with x hx₃ hx₄ hx₅
    rw [Pi.add_apply, Pi.add_apply, hx₃, hx₄, hx₅]

Goal state after:
case refine_1
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᵐ[ν + ν']
    (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')
h₂ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᵐ[ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
⊢ μ.singularPart ν' ⟂ₘ ν'
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
pp: case a
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
⊢ (fun U ↦ netEntropyEntourage T F U) (SetRel.symmetrize U) ≤ coverEntropyEntourage T F (SetRel.symmetrize U)

Tactic:
exact netEntropyEntourage_le_coverEntropyEntourage T F

Goal state after:
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
⊢ ∀ᵐ (x : α) ∂ν, x ∈ f ⁻¹' s → μ.rnDeriv ν x = (map f μ).rnDeriv (map f ν) (f x)

Tactic:
filter_upwards [hf.rnDeriv_map μ ν] with a ha _ using ha.symm

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
⊢ (σ * τ) b = (τ * σ) b

Tactic:
rw [σ.mul_apply, τ.mul_apply, hc, map_mul, τ.commutes, hd, map_mul, σ.commutes, hc,
    mul_assoc, mul_assoc, mul_right_inj' hb', mul_comm]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
f : L.Functions 1
t : L.Term α
v : α → M
⊢ realize v (f.apply₁ t) = funMap f ![realize v t]

Tactic:
rw [Functions.apply₁, Term.realize]

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
f : L.Functions 1
t : L.Term α
v : α → M
⊢ (funMap f fun i ↦ realize v (![t] i)) = funMap f ![realize v t]
Module: Mathlib.ModelTheory.Ultraproducts

Goal state before:
pp: case all.h₂
α : 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), φ.Realize (fun i ↦ Quotient.mk' (x i)) (Fin.snoc (Quotient.mk' ∘ v) (Quotient.mk' m))) ↔
    ∀ᶠ (a : α) in ↑u, ∀ (x_1 : M a), φ.Realize (fun i ↦ x i a) (Fin.snoc (fun i ↦ v i a) x_1)

Tactic:
have h' :
      ∀ (m : ∀ a, M a) (a : α),
        (fun i : Fin (k + 1) => (Fin.snoc v m : _ → ∀ a, M a) i a) =
          Fin.snoc (fun i : Fin k => v i a) (m a) := by
      refine fun m a => funext (Fin.reverseInduction ?_ fun i _ => ?_)
      · simp only [Fin.snoc_last]
      · simp only [Fin.snoc_castSucc]

Goal state after:
case all.h₂
α : 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
h' : ∀ (m : (a : α) → M a) (a : α), (fun i ↦ Fin.snoc v m i a) = Fin.snoc (fun i ↦ v i a) (m a)
⊢ (∀ (m : (a : α) → M a), φ.Realize (fun i ↦ Quotient.mk' (x i)) (Fin.snoc (Quotient.mk' ∘ v) (Quotient.mk' m))) ↔
    ∀ᶠ (a : α) in ↑u, ∀ (x_1 : M a), φ.Realize (fun i ↦ x i a) (Fin.snoc (fun i ↦ v i a) x_1)
Module: Mathlib.ModelTheory.ElementaryMaps

Goal state before:
pp: case refine_3
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✝ l✝ : ℕ
R : L.Relations l✝
ts : Fin l✝ → L.Term (Empty ⊕ Fin n✝)
xs : Fin n✝ → M
⊢ (RelMap R fun i ↦ ((⇑f ∘ Term.realize (Sum.elim default xs)) ∘ ts) i) ↔
    RelMap R fun i ↦ (Term.realize (Sum.elim default xs) ∘ ts) i

Tactic:
rw [Function.comp_assoc, map_rel f]

Goal state after:
Module: Mathlib.ModelTheory.ElementarySubstructures

Goal state before:
pp: L : Language
M : Type u_1
inst✝ : L.Structure M
A : Set M
hA : MeetsDefinable A
⊢ ((closure L).toFun A).IsElementary

Tactic:
by
  refine isElementary_of_exists ((closure L).toFun A) ?_
  intro n φ x a hφ
  let D : Set M := {y : M | φ.Realize default (Fin.snoc (Subtype.val ∘ x) y)}
  have hD_ne : D.Nonempty := ⟨a,hφ⟩
  have hD : A.Definable₁ L D := by
    simp only [Definable₁, Definable, Fin.isValue]
    refine ⟨((L.lhomWithConstants A).onBoundedFormula φ).toFormula.relabel
      (Sum.elim Empty.elim id) |>.subst fun i => Fin.lastCases (Term.var 0)
        (fun j => (L.con ⟨x j, by
        nth_rw 1 [← hA.closure_eq_self]
        simp only [Subtype.coe_prop]
        ⟩).term) i, ?_⟩
    ext v
    simp only [Fin.isValue, mem_ofPred_eq, Formula.relabel, Formula.Realize,
      BoundedFormula.realize_subst, BoundedFormula.realize_relabel, Nat.add_zero, Fin.castAdd_zero,
      Fin.cast_refl, Function.comp_id, Fin.natAdd_zero, D]
    rw [← Formula.Realize, BoundedFormula.realize_toFormula, LHom.realize_onBoundedFormula]
    congr! 1
    ext i; cases i using Fin.lastCases <;> simp
  obtain ⟨b, hbD, hbA⟩ := hA D hD_ne hD
  exact ⟨⟨b, by rwa [← hA.closure_eq_self] at hbA⟩, hbD⟩

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case imp
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₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 : ∀ {xs : Fin n✝ → M}, f₁✝.Realize (⇑g ∘ v) (⇑g ∘ xs) ↔ f₁✝.Realize v xs
ih2 : ∀ {xs : Fin n✝ → M}, f₂✝.Realize (⇑g ∘ v) (⇑g ∘ xs) ↔ f₂✝.Realize v xs
xs : Fin n✝ → M
⊢ (f₁✝ ⟹ f₂✝).Realize (⇑g ∘ v) (⇑g ∘ xs) ↔ (f₁✝ ⟹ f₂✝).Realize v xs

Tactic:
rw [BoundedFormula.Realize, ih1, ih2, BoundedFormula.Realize]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
n : ℕ
⊢ M ⊨ Sentence.cardGe L n ↔ ↑n ≤ #M

Tactic:
rw [← lift_mk_fin, ← lift_le.{0}, lift_lift, lift_mk_le, Sentence.cardGe, Sentence.Realize,
    BoundedFormula.realize_exs]

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
n : ℕ
⊢ (∃ xs,
      (List.foldr (fun x1 x2 ↦ x1 ⊓ x2) ⊤
            (List.map (fun ij ↦ ∼((var ∘ Sum.inr) ij.1 =' (var ∘ Sum.inr) ij.2))
              (List.filter (fun ij ↦ decide (ij.1 ≠ ij.2)) (List.finRange n ×ˢ List.finRange n)))).Realize
        default xs) ↔
    Nonempty (Fin n ↪ M)
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type u_1
L : Language
inst✝¹ : L.Structure M
A : Set M
α : Type u_4
β : Type u_5
inst✝ : Finite β
F : (α → M) → β → M
hF : DefinableMap L A F
S : Set (β → M)
hS : A.Definable L S
i : β
⊢ A.Definable L {x | F (x ∘ Sum.inl) i = x (Sum.inr i)}

Tactic:
simpa [tupleGraph] using!
      (hF i).preimage_comp (fun | none => Sum.inr i | some j => Sum.inl j)

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
ι : Type u_1
inst✝ : Nonempty ι
T : ι → L.Theory
h : Directed (fun x1 x2 ↦ x1 ⊆ x2) T
h' : ∀ (i : ι), (T i).IsSatisfiable
⊢ IsSatisfiable (⋃ i, T i)

Tactic:
rw [isSatisfiable_iff_isFinitelySatisfiable, IsFinitelySatisfiable]

Goal state after:
L : Language
ι : Type u_1
inst✝ : Nonempty ι
T : ι → L.Theory
h : Directed (fun x1 x2 ↦ x1 ⊆ x2) T
h' : ∀ (i : ι), (T i).IsSatisfiable
⊢ ∀ (T0 : Finset L.Sentence), ↑T0 ⊆ ⋃ i, T i → IsSatisfiable ↑T0
Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed

Goal state before:
pp: φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : ↑T0 ⊆ Theory.ACF 0
h : ↑T0 ⊨ᵇ φ
ψ : Language.ring.Sentence
hψ : ψ ∈ Theory.field ∪ genericMonicPolyHasRoot '' {n | 0 < n} ∨ ψ ∈ (fun q ↦ ∼(eqZero q)) '' {q | Nat.Prime q}
⊢ { s // ∀ q ∉ s, Theory.ACF ↑q ⊨ᵇ ψ }

Tactic:
Set.mem_image

Goal state after:
φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : ↑T0 ⊆ Theory.ACF 0
h : ↑T0 ⊨ᵇ φ
ψ : Language.ring.Sentence
hψ : ψ ∈ Theory.field ∪ genericMonicPolyHasRoot '' {n | 0 < n} ∨ ∃ x ∈ {q | Nat.Prime q}, ∼(eqZero x) = ψ
⊢ { s // ∀ q ∉ s, Theory.ACF ↑q ⊨ᵇ ψ }
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
φ : L.Sentence
⊢ ¬(T ∪ {Formula.not φ}).IsSatisfiable ↔ ∃ T0, ↑T0 ⊆ T ∧ ¬(↑T0 ∪ {Formula.not φ}).IsSatisfiable

Tactic:
rw [isSatisfiable_iff_isFinitelySatisfiable, IsFinitelySatisfiable]

Goal state after:
L : Language
T : L.Theory
φ : L.Sentence
⊢ (¬∀ (T0 : Finset L.Sentence), ↑T0 ⊆ T ∪ {Formula.not φ} → IsSatisfiable ↑T0) ↔
    ∃ T0, ↑T0 ⊆ T ∧ ¬(↑T0 ∪ {Formula.not φ}).IsSatisfiable
Module: Mathlib.SetTheory.Cardinal.Divisibility

Goal state before:
pp: case inr.inr
n m : ℕ
k : Cardinal.{u_1}
hk : ↑m = ↑n * k
hk' : k < ℵ₀
⊢ n ∣ m

Tactic:
lift k to ℕ using hk'

Goal state after:
case inr.inr
n m k : ℕ
hk : ↑m = ↑n * ↑k
⊢ n ∣ m
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
x : Extension k p n
⊢ (frob k p n) x = x ^ Nat.card k

Tactic:
by
  simp [frob, ← Nat.card_eq_fintype_card]

Goal state after: