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

Goal state before:
pp: G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : SecondCountableTopology G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : μ.IsMulLeftInvariant
f : G →* G
hf : Dense (⋃ n, (⇑f)^[n] ⁻¹' 1)
s : Set G
hsm : MeasurableSet s
hs : ⇑f ⁻¹' s = s
n : ℕ
x : G
hx : (⇑f)^[n] x = 1
hsn : (⇑f)^[n] ⁻¹' s = s
⊢ x ∈ {g | (fun x ↦ g • x) ⁻¹' s = s}

Tactic:
mem_ofPred,

Goal state after:
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : SecondCountableTopology G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : μ.IsMulLeftInvariant
f : G →* G
hf : Dense (⋃ n, (⇑f)^[n] ⁻¹' 1)
s : Set G
hsm : MeasurableSet s
hs : ⇑f ⁻¹' s = s
n : ℕ
x : G
hx : (⇑f)^[n] x = 1
hsn : (⇑f)^[n] ⁻¹' s = s
⊢ (fun x_1 ↦ x • x_1) ⁻¹' s = s
Module: Mathlib.Dynamics.Ergodic.AddCircleAdd

Goal state before:
pp: p : ℝ
inst✝ : Fact (0 < p)
a : AddCircle p
⊢ Ergodic (fun x ↦ a + x) volume ↔ addOrderOf a = 0

Tactic:
by
  rw [← denseRange_zsmul_iff, ergodic_add_left_iff_denseRange_zsmul]

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

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hn : 1 ≤ ↑n
hI : I =ᵐ[volume] closedBall x (T / (2 * ↑n))
this : Fintype ↥G
⊢ #Finset.univ = Fintype.card ↥(AddSubgroup.zmultiples u)

Tactic:
rfl

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
f : X → X
⊢ fixedSupport f = closure (fixedPoints f)ᶜ

Tactic:
rfl

Goal state after:
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: case mpr
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
y : β
h : ∀ n ∈ 𝓝 y, ∀ {U : Set τ}, U ∈ f → ∃ x ∈ U, (s ∩ ϕ x ⁻¹' n).Nonempty
i✝ : Set τ
hu : i✝ ∈ f
t✝ : Set β
hn : t✝ ∈ 𝓝 y
⊢ (t✝ ∩ image2 ϕ i✝ s).Nonempty

Tactic:
rcases h _ hn hu with ⟨_, ht, _, hx, hϕtx⟩

Goal state after:
case mpr
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
y : β
h : ∀ n ∈ 𝓝 y, ∀ {U : Set τ}, U ∈ f → ∃ x ∈ U, (s ∩ ϕ x ⁻¹' n).Nonempty
i✝ : Set τ
hu : i✝ ∈ f
t✝ : Set β
hn : t✝ ∈ 𝓝 y
w✝¹ : τ
ht : w✝¹ ∈ i✝
w✝ : α
hx : w✝ ∈ s
hϕtx : w✝ ∈ ϕ w✝¹ ⁻¹' t✝
⊢ (t✝ ∩ image2 ϕ i✝ s).Nonempty
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
inter_nemp : (⋂ k, T^[m * ↑k] ⁻¹' ball (↑(t k)) (dynEntourage T U m)).Nonempty
⊢ ∃ y, ⋂ k, T^[m * ↑k] ⁻¹' ball (↑(t k)) (dynEntourage T U m) ⊆ ball y (dynEntourage T (U ○ U) (m * n))

Tactic:
obtain ⟨y, y_int⟩ := inter_nemp
      refine ⟨y, fun z z_int ↦ ?_⟩
      simp only [ball, dynEntourage, Prod.map_iterate, mem_iInter, Set.mem_preimage, Prod.map_apply,
        mem_comp] at y_int z_int ⊢
      intro k k_mn
      replace k_mn := Nat.div_lt_of_lt_mul k_mn
      specialize z_int ⟨(k / m), k_mn⟩ (k % m) (Nat.mod_lt k m_pos)
      specialize y_int ⟨(k / m), k_mn⟩ (k % m) (Nat.mod_lt k m_pos)
      rw [← Function.iterate_add_apply T (k % m) (m * (k / m)), Nat.mod_add_div k m] at y_int z_int
      exact mem_comp_of_mem_ball y_int z_int

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

Goal state before:
pp: case inr
X : Type u_1
U : SetRel X X
T : X → X
F : Set X
inst✝¹ : U.IsRefl
inst✝ : U.IsSymm
n : ℕ
h : netMaxcard T F U n < ⊤
s : Finset X
s_net : IsDynNetIn T F U n ↑s
s_card : ↑s.card = netMaxcard T F U n
⊢ IsDynCoverOf T F (U ○ U) n ↑s

Tactic:
rw [IsDynCoverOf, isCover_iff_subset_iUnion_ball]

Goal state after:
case inr
X : Type u_1
U : SetRel X X
T : X → X
F : Set X
inst✝¹ : U.IsRefl
inst✝ : U.IsSymm
n : ℕ
h : netMaxcard T F U n < ⊤
s : Finset X
s_net : IsDynNetIn T F U n ↑s
s_card : ↑s.card = netMaxcard T F U n
⊢ F ⊆ ⋃ y ∈ ↑s, ball y (dynEntourage T (U ○ U) n)
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
pp: case h
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
⊢ Monotone fun n ↦ ↑(netMaxcard T F U n)

pp: case h'
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
⊢ (fun n ↦ ↑(netMaxcard T F U n)) ≠ 0

Tactic:
· exact fun _ _ m_n ↦ ENat.toENNReal_mono (netMaxcard_monotone_time T F U m_n)

Goal state after:
case h'
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
⊢ (fun n ↦ ↑(netMaxcard T F U n)) ≠ 0
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 ν
this✝¹ : SigmaFinite (map f ν)
this✝ : SigmaFinite (map f (μ.singularPart ν))
this : SigmaFinite (map f (ν.withDensity (μ.rnDeriv ν)))
h_add :
  (map f (μ.singularPart ν) + map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν) =ᵐ[map f ν]
    (map f (μ.singularPart ν)).rnDeriv (map f ν) + (map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν)
⊢ (fun x ↦ (map f (μ.singularPart ν) + map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν) (f x)) =ᵐ[ν]
    (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv ν

Tactic:
rw [Filter.EventuallyEq, hf.ae_map_iff, ← Filter.EventuallyEq] at h_add

Goal state after:
α : 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)
⊢ (fun x ↦ (map f (μ.singularPart ν) + map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν) (f x)) =ᵐ[ν]
    (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
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 ν
h_add : map f μ = map f (μ.singularPart ν) + (map f ν).withDensity ((map f μ).rnDeriv (map f ν))
⊢ (map f μ).singularPart (map f ν) = map f (μ.singularPart ν)

Tactic:
refine (Measure.eq_singularPart (Measure.measurable_rnDeriv _ _) ?_ h_add).symm

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
h_add : map f μ = map f (μ.singularPart ν) + (map f ν).withDensity ((map f μ).rnDeriv (map f ν))
⊢ map f (μ.singularPart ν) ⟂ₘ map f ν
Module: Mathlib.RingTheory.Algebraic.Cardinality

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
L : Type v
inst✝⁴ : CommRing L
inst✝³ : IsDomain L
inst✝² : Algebra R L
inst✝¹ : IsTorsionFree R L
inst✝ : Algebra.IsAlgebraic R L
⊢ #((p : R[X]) × { x // x ∈ p.aroots L }) = #((i : R[X]) × ↑{x | x ∈ i.aroots L})

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: case mk
L : Language
L' : Language
onFunction✝ : ⦃n : ℕ⦄ → L.Functions n → L'.Functions n
onRelation✝ : ⦃n : ℕ⦄ → L.Relations n → L'.Relations n
⊢ LHom.id L' ∘ᴸ { onFunction := onFunction✝, onRelation := onRelation✝ } =
    { onFunction := onFunction✝, onRelation := onRelation✝ }

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: case mk
L : Language
L' : Language
onFunction✝ : ⦃n : ℕ⦄ → L.Functions n → L'.Functions n
onRelation✝ : ⦃n : ℕ⦄ → L.Relations n → L'.Relations n
⊢ { onFunction := onFunction✝, onRelation := onRelation✝ } ∘ᴸ LHom.id L =
    { onFunction := onFunction✝, onRelation := onRelation✝ }

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: case mk.mk.refl
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : L.Structure M
inst✝² : L.Structure N
P : Type u_1
inst✝¹ : L.Structure P
Q : Type u_2
inst✝ : L.Structure Q
toFun✝ : M → N
map_fun'✝¹ : ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toFun✝ (funMap f x) = funMap f (toFun✝ ∘ x)
map_rel'✝¹ : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r x → RelMap r (toFun✝ ∘ x)
map_fun'✝ : ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toFun✝ (funMap f x) = funMap f (toFun✝ ∘ x)
map_rel'✝ : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r x → RelMap r (toFun✝ ∘ x)
⊢ { toFun := toFun✝, map_fun' := map_fun'✝¹, map_rel' := map_rel'✝¹ } =
    { toFun := toFun✝, map_fun' := map_fun'✝, map_rel' := map_rel'✝ }

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : L.Structure M
inst✝² : L.Structure N
P : Type u_1
inst✝¹ : L.Structure P
Q : Type u_2
inst✝ : L.Structure Q
hnp : N →[L] P
hmn : M →[L] N
n✝ : ℕ
x✝¹ : L.Functions n✝
x✝ : Fin n✝ → M
⊢ funMap x✝¹ (⇑hnp ∘ ⇑hmn ∘ x✝) = funMap x✝¹ ((⇑hnp ∘ ⇑hmn) ∘ x✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: case h_fun
L : Language
α : Type w'
β : Type u_1
f : α → β
x✝¹ : ℕ
x✝ : L.Functions x✝¹
⊢ ((L.lhomWithConstantsMap f).comp LHom.sumInl).onFunction x✝ = (L.lhomWithConstants β).onFunction x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: case h_rel
L : Language
α : Type w'
β : Type u_1
f : α → β
x✝¹ : ℕ
x✝ : L.Relations x✝¹
⊢ ((L.lhomWithConstantsMap f).comp LHom.sumInl).onRelation x✝ = (L.lhomWithConstants β).onRelation x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: case refine_1.inr.zero
L : Language
L' : Language
M : Type w
inst✝² : L.Structure M
α : Type u_1
inst✝¹ : (constantsOn α).Structure M
A B : Set M
h : A ⊆ B
N : Type w'
inst✝ : L.Structure N
f : M ↪[L] N
x : Fin 0 → M
c : (constantsOn ↑A).Functions 0
⊢ f.toFun (funMap (Sum.inr c) x) = funMap (Sum.inr c) (f.toFun ∘ x)

Tactic:
rfl

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case h
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 : b ^ n = i a
hb' : b ≠ 0
s : Multiset E := (map i (X ^ n - C a)).roots
hs : map i (X ^ n - C a) = (Multiset.map (fun x ↦ X - C x) s).prod
hs' : s.card = n
C_mul_C : C (i a⁻¹) * C (i a) = 1
key1 : map i (X ^ n - 1) = C (i a⁻¹) * (map i (X ^ n - C a)).comp (C b * X)
key2 : ((fun q ↦ q.comp (C b * X)) ∘ fun c ↦ X - C c) = fun c ↦ C b * (X - C (c / b))
⊢ (Multiset.map (fun c ↦ X - C (c / b)) s).prod = (Multiset.map ((fun x ↦ X - C x) ∘ fun c ↦ c / b) s).prod

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
x : M
⊢ { toEquiv := _root_.Equiv.refl M, map_fun' := ⋯, map_rel' := ⋯ } x = x

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.Algebra.Ring.Basic

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝ : ring.Structure R
a✝¹ a✝ : R
⊢ funMap addFunc (Fin.cons a✝¹ (Fin.cons a✝ finZeroElim)) = a✝¹ + Fin.cons a✝¹ (Fin.cons a✝ finZeroElim) 1

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.Algebra.Ring.Basic

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝ : ring.Structure R
a✝¹ a✝ : R
⊢ funMap mulFunc (Fin.cons a✝¹ (Fin.cons a✝ finZeroElim)) = a✝¹ * Fin.cons a✝¹ (Fin.cons a✝ finZeroElim) 1

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.Algebra.Ring.Basic

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝ : ring.Structure R
a✝ : R
⊢ funMap negFunc (Fin.cons a✝ finZeroElim) = -a✝

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.Algebra.Ring.Basic

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝ : ring.Structure R
⊢ funMap zeroFunc finZeroElim = 0

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.Algebra.Ring.Basic

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝ : ring.Structure R
⊢ funMap oneFunc finZeroElim = 1

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case var
L : Language
α : Type u'
a✝ : α
⊢ relabel id (var a✝) = var a✝

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case var
L : Language
α : Type u'
β : Type v'
γ : Type u_1
f : α → β
g : β → γ
a✝ : α
⊢ relabel g (relabel f (var a✝)) = relabel (g ∘ f) (var a✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case var
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
a✝ : α
⊢ (var a✝).constantsToVars.varsToConstants = var a✝

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case var.inl
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
val✝ : γ
⊢ (var (Sum.inl val✝)).varsToConstants.constantsToVars = var (Sum.inl val✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case var.inr
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
val✝ : α
⊢ (var (Sum.inr val✝)).varsToConstants.constantsToVars = var (Sum.inr val✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case var
L : Language
α : Type u'
a✝ : α
⊢ ((var a✝).substFunc fun {n} ↦ Functions.term) = var a✝

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case var
L : Language
α : Type u'
a✝ : α
⊢ (LHom.id L).onTerm (var a✝) = id (var a✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case func
L : Language
α : Type u'
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term α
ih : ∀ (a : Fin l✝), (LHom.id L).onTerm (_ts✝ a) = id (_ts✝ a)
⊢ (func ((LHom.id L).onFunction _f✝) fun i ↦ id (_ts✝ i)) = id (func _f✝ _ts✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case var
L : Language
L' : Language
α : Type u'
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
a✝ : α
⊢ (φ.comp ψ).onTerm (var a✝) = (φ.onTerm ∘ ψ.onTerm) (var a✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case func
L : Language
L' : Language
α : Type u'
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term α
ih : ∀ (a : Fin l✝), (φ.comp ψ).onTerm (_ts✝ a) = (φ.onTerm ∘ ψ.onTerm) (_ts✝ a)
⊢ (func ((φ.comp ψ).onFunction _f✝) fun i ↦ (φ.onTerm ∘ ψ.onTerm) (_ts✝ i)) = (φ.onTerm ∘ ψ.onTerm) (func _f✝ _ts✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case falsum
L : Language
α : Type u'
n n✝ : ℕ
h : n✝ ≤ n✝
⊢ castLE h falsum = falsum

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case falsum
L : Language
α : Type u'
k n✝¹ m✝ n✝ : ℕ
km✝ : n✝¹ ≤ m✝
mn✝ : m✝ ≤ n✝
⊢ castLE mn✝ (castLE km✝ falsum) = castLE ⋯ falsum

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case falsum
L : Language
L' : Language
α : Type u'
β : Type v'
γ : Type u_1
L'' : Language
ft : (n : ℕ) → L.Term (α ⊕ Fin n) → L'.Term (β ⊕ Fin n)
fr : (n : ℕ) → L.Relations n → L'.Relations n
ft' : (n : ℕ) → L'.Term (β ⊕ Fin n) → L''.Term (γ ⊕ Fin n)
fr' : (n : ℕ) → L'.Relations n → L''.Relations n
n n✝ : ℕ
⊢ mapTermRel ft' fr' (fun x ↦ id) (mapTermRel ft fr (fun x ↦ id) falsum) =
    mapTermRel (fun x ↦ ft' x ∘ ft x) (fun x ↦ fr' x ∘ fr x) (fun x ↦ id) falsum

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case falsum
L : Language
α : Type u'
n n✝ : ℕ
⊢ mapTermRel (fun x ↦ id) (fun x ↦ id) (fun x ↦ id) falsum = falsum

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
n : ℕ
v : Fin n → M
f : L.Functions n
⊢ realize v f.term = funMap f v

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case var
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
g : α → β
v : β → M
a✝ : α
⊢ realize v (relabel g (var a✝)) = realize (v ∘ g) (var a✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case var
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
tf : α → L.Term β
v : β → M
a✝ : α
⊢ realize v ((var a✝).subst tf) = realize (fun a ↦ realize v (tf a)) (var a✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case falsum
L : Language
α : Type u'
n n✝ : ℕ
⊢ mapTermRel (fun x t ↦ Term.relabel (Sum.map id (natAdd 0)) t) (fun x ↦ id) (fun x ↦ castLE ⋯) falsum = castLE ⋯ falsum

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case rel
L : Language
α : Type u'
n n✝ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (α ⊕ Fin n✝)
⊢ (fun i ↦ Term.relabel (Sum.map id (Fin.cast ⋯)) (ts✝ i)) = Term.relabel (Sum.map id (Fin.cast ⋯)) ∘ ts✝

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case falsum
L : Language
α : Type u'
n n✝ : ℕ
⊢ (LHom.id L).onBoundedFormula falsum = id falsum

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case rel
L : Language
α : Type u'
n n✝ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (α ⊕ Fin n✝)
⊢ ((LHom.id L).onRelation R✝).boundedFormula (id ∘ ts✝) = id (rel R✝ ts✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case falsum
L : Language
L' : Language
α : Type u'
n : ℕ
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
n✝ : ℕ
⊢ (φ.comp ψ).onBoundedFormula falsum = (φ.onBoundedFormula ∘ ψ.onBoundedFormula) falsum

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.Quotients

Goal state before:
pp: case var
L : Language
M : Type u_1
s : Setoid M
ps : L.Prestructure s
β : Type u_2
x : β → M
a✝ : β
⊢ realize (fun i ↦ ⟦x i⟧) (var a✝) = ⟦realize x (var a✝)⟧

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case rel
L : Language
L' : Language
α : Type u'
n : ℕ
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
n✝ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (α ⊕ Fin n✝)
⊢ (φ.onRelation (ψ.onRelation R✝)).boundedFormula ((φ.onTerm ∘ ψ.onTerm) ∘ ts✝) =
    φ.onBoundedFormula ((ψ.onRelation R✝).boundedFormula (ψ.onTerm ∘ ts✝))

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case func.zero.inr
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
v : β → M
ts : Fin 0 → L[[α]].Term β
ih : ∀ (a : Fin 0), realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (ts a).constantsToVars = realize v (ts a)
val✝ : (constantsOn α).Functions 0
⊢ ↑(L.con val✝) = ↑(Sum.inr val✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.Semantics

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

Tactic:
induction t with
  | var => simp
  | @func n f ts ih =>
    cases n
    · cases f
      · simp only [realize, ih, constantsOn, constantsOnFunc, constantsToVars]
        -- Porting note: below lemma does not work with simp for some reason
        rw [withConstants_funMap_sumInl]
      · simp only [realize, constantsToVars, Sum.elim_inl, funMap_eq_coe_constants]
        rfl
    · obtain - | f := f
      · simp only [realize, ih, constantsOn, constantsOnFunc, constantsToVars]
        -- Porting note: below lemma does not work with simp for some reason
        rw [withConstants_funMap_sumInl]
      · exact isEmptyElim f

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case var
L : Language
L' : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : L'.Structure M
φ : L →ᴸ L'
inst✝ : φ.IsExpansionOn M
v : α → M
a✝ : α
⊢ Term.realize v (φ.onTerm (var a✝)) = Term.realize v (var a✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case var
L : Language
M : Type w
N : Type u_1
inst✝³ : L.Structure M
inst✝² : L.Structure N
α : Type u'
F : Type u_4
inst✝¹ : FunLike F M N
inst✝ : L.HomClass F M N
g : F
v : α → M
a✝ : α
⊢ Term.realize (⇑g ∘ v) (var a✝) = g (Term.realize v (var a✝))

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.Ultraproducts

Goal state before:
pp: case e'_3.e'_3.var
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝ : (a : α) → L.Structure (M a)
β : Type u_3
x : β → (a : α) → M a
a : α
a✝ : β
⊢ Term.realize (fun i ↦ x i a) (var a✝) = Term.realize x (var a✝) a

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.Ultraproducts

Goal state before:
pp: case e'_3.e'_3.func
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝ : (a : α) → L.Structure (M a)
β : Type u_3
x : β → (a : α) → M a
a : α
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term β
t_ih : ∀ (a_1 : Fin l✝), Term.realize (fun i ↦ x i a) (_ts✝ a_1) = Term.realize x (_ts✝ a_1) a
⊢ (funMap _f✝ fun i ↦ Term.realize x (_ts✝ i) a) = funMap _f✝ (fun i ↦ Term.realize x (_ts✝ i)) a

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
l : ℕ
φ ψ : L.BoundedFormula α l
v : α → M
xs : Fin l → M
⊢ (φ ⇔ ψ).Realize v xs ↔ (φ.Realize v xs ↔ ψ.Realize v xs)

Tactic:
by
  simp only [BoundedFormula.iff, realize_inf, realize_imp, ← iff_def]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case falsum
L : Language
L' : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : L'.Structure M
ft : (n : ℕ) → L.Term (α ⊕ Fin n) → L'.Term (β ⊕ Fin n)
fr : (n : ℕ) → L.Relations n → L'.Relations n
n : ℕ
v : α → M
v' : β → M
h1 : ∀ (n : ℕ) (t : L.Term (α ⊕ Fin n)) (xs : Fin n → M), realize (Sum.elim v' xs) (ft n t) = realize (Sum.elim v xs) t
h2 : ∀ (n : ℕ) (R : L.Relations n) (x : Fin n → M), RelMap (fr n R) x = RelMap R x
n✝ : ℕ
xs : Fin n✝ → M
⊢ (mapTermRel ft fr (fun x ↦ id) falsum).Realize v' xs ↔ falsum.Realize v xs

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case falsum
L : Language
L' : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : L'.Structure M
k : ℕ
ft : (n : ℕ) → L.Term (α ⊕ Fin n) → L'.Term (β ⊕ Fin (k + n))
fr : (n : ℕ) → L.Relations n → L'.Relations n
n : ℕ
v : {n : ℕ} → (Fin (k + n) → M) → α → M
v' : β → M
h1 :
  ∀ (n : ℕ) (t : L.Term (α ⊕ Fin n)) (xs' : Fin (k + n) → M),
    realize (Sum.elim v' xs') (ft n t) = realize (Sum.elim (v xs') (xs' ∘ natAdd k)) t
h2 : ∀ (n : ℕ) (R : L.Relations n) (x : Fin n → M), RelMap (fr n R) x = RelMap R x
hv : ∀ (n : ℕ) (xs : Fin (k + n) → M) (x : M), v (snoc xs x) = v xs
n✝ : ℕ
xs : Fin (k + n✝) → M
⊢ (mapTermRel ft fr (fun x ↦ castLE ⋯) falsum).Realize v' xs ↔ falsum.Realize (v xs) (xs ∘ natAdd k)

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case nil
L : Language
α : Type u'
h : ∀ (t : L.Term α) (l : List (α ⊕ (i : ℕ) × L.Functions i)), listDecode (t.listEncode ++ l) = t :: listDecode l
⊢ listDecode (flatMap listEncode []) = []

Tactic:
rfl

Goal state after: