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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1✝ : WSeq α
s2✝ : WSeq β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1✝ s2✝
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
s1 : WSeq γ
s2 : WSeq δ
h✝ : (fun s1 s2 ↦ ∃ s t, s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) s1 s2
s : WSeq α
t : WSeq β
h : LiftRel R s t
⊢ ∀ {a : Option (α × WSeq α)} {b : Option (β × WSeq β)},
    LiftRelO R (LiftRel R) a b →
      LiftRelO S (fun s1 s2 ↦ ∃ s, s1 = map f1 s ∧ ∃ x, s2 = map f2 x ∧ LiftRel R s x)
        (Option.map (Prod.map f1 (map f1)) a) (Option.map (Prod.map f2 (map f2)) b)

Tactic:
intro o

Goal state after:
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1✝ : WSeq α
s2✝ : WSeq β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1✝ s2✝
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
s1 : WSeq γ
s2 : WSeq δ
h✝ : (fun s1 s2 ↦ ∃ s t, s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) s1 s2
s : WSeq α
t : WSeq β
h : LiftRel R s t
o : Option (α × WSeq α)
⊢ ∀ {b : Option (β × WSeq β)},
    LiftRelO R (LiftRel R) o b →
      LiftRelO S (fun s1 s2 ↦ ∃ s, s1 = map f1 s ∧ ∃ x, s2 = map f2 x ∧ LiftRel R s x)
        (Option.map (Prod.map f1 (map f1)) o) (Option.map (Prod.map f2 (map f2)) b)
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
s1✝ s2 : WSeq α
t1✝ t2 : WSeq β
h1 : LiftRel R s1✝ t1✝
h2 : LiftRel R s2 t2
s : WSeq α
t : WSeq β
h✝ : (fun s t ↦ LiftRel R s t ∨ ∃ s1 t1, s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1) s t
s1 : WSeq α
t1 : WSeq β
h : LiftRel R s1 t1
⊢ ∀ {a : Option (α × WSeq α)} {b : Option (β × WSeq β)},
    LiftRelO R (LiftRel R) a b →
      Computation.LiftRel
        (LiftRelO R fun s t ↦ LiftRel R s t ∨ ∃ s1, s = s1.append s2 ∧ ∃ x, t = x.append t2 ∧ LiftRel R s1 x)
        (destruct_append.aux s2 a) (destruct_append.aux t2 b)

Tactic:
intro o

Goal state after:
α : Type u
β : Type v
R : α → β → Prop
s1✝ s2 : WSeq α
t1✝ t2 : WSeq β
h1 : LiftRel R s1✝ t1✝
h2 : LiftRel R s2 t2
s : WSeq α
t : WSeq β
h✝ : (fun s t ↦ LiftRel R s t ∨ ∃ s1 t1, s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1) s t
s1 : WSeq α
t1 : WSeq β
h : LiftRel R s1 t1
o : Option (α × WSeq α)
⊢ ∀ {b : Option (β × WSeq β)},
    LiftRelO R (LiftRel R) o b →
      Computation.LiftRel
        (LiftRelO R fun s t ↦ LiftRel R s t ∨ ∃ s1, s = s1.append s2 ∧ ∃ x, t = x.append t2 ∧ LiftRel R s1 x)
        (destruct_append.aux s2 o) (destruct_append.aux t2 b)
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: α : Type u
S : WSeq (Computation α)
a : α
h : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)
C : Computation α
aC : a ∈ C
⊢ ∀ (l : List (Computation α)) (S : WSeq (Computation α)), corec parallel.aux1 (l, S) = C → ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c

Tactic:
apply memRecOn aC <;> [skip; intro C' IH] <;> intro l S e

Goal state after:
case h1
α : Type u
S✝ : WSeq (Computation α)
a : α
h : a ∈ parallel S✝
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)
C : Computation α
aC : a ∈ C
l : List (Computation α)
S : WSeq (Computation α)
e : corec parallel.aux1 (l, S) = pure a
⊢ ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c

case h2
α : Type u
S✝ : WSeq (Computation α)
a : α
h : a ∈ parallel S✝
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)
C : Computation α
aC : a ∈ C
C' : Computation α
IH :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    corec parallel.aux1 (l, S) = C' → ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c
l : List (Computation α)
S : WSeq (Computation α)
e : corec parallel.aux1 (l, S) = C'.think
⊢ ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case intro.inl
α : Type u
a : α
ss : WSeq α
h : a ∈ ss
S : WSeq (WSeq α)
x✝ : α
s✝ : WSeq α
ej : (cons x✝ s✝).append S.join = cons x✝ (s✝.append S.join)
m : a = x✝ ∨ a ∈ s✝.append S.join
e : a = x✝
⊢ (a = x✝ ∨ a ∈ s✝) ∨ ∃ s ∈ S, a ∈ s

Tactic:
simp [e]

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

Goal state before:
pp: case intro.inr.inl
α : Type u
a : α
ss : WSeq α
h : a ∈ ss
S : WSeq (WSeq α)
x✝ : α
s✝ : WSeq α
ej : (cons x✝ s✝).append S.join = cons x✝ (s✝.append S.join)
IH :
  ∀ (s : WSeq α) (S_1 : WSeq (WSeq α)),
    s.append S_1.join = s✝.append S.join → a ∈ s.append S_1.join → a ∈ s ∨ ∃ s ∈ S_1, a ∈ s
e : a = x✝
⊢ (a = x✝ ∨ a ∈ s✝) ∨ ∃ s ∈ S, a ∈ s

Tactic:
simp [e]

Goal state after:
Module: Mathlib.Data.String.Basic

Goal state before:
pp: case nil.cons
head✝ : Char
tail✝ : List Char
⊢ ltb { s := ofList [], i := 0 } { s := ofList (head✝ :: tail✝), i := 0 } = true ↔ [] < head✝ :: tail✝

Tactic:
rename_i c₂ cs₂

Goal state after:
case nil.cons
c₂ : Char
cs₂ : List Char
⊢ ltb { s := ofList [], i := 0 } { s := ofList (c₂ :: cs₂), i := 0 } = true ↔ [] < c₂ :: cs₂
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s✝ : WSeq α
c1 c2 : Computation (Option (β × WSeq β))
s : WSeq α
h : c1 = (map f s.think).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.think.destruct
⊢ BisimO (fun c1 c2 ↦ ∃ s, c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct)
    (map f s.think).destruct.destruct (Computation.map (Option.map (Prod.map f (map f))) s.think.destruct).destruct

Tactic:
exact ⟨s, by simp⟩

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
g' : G
hg' : g' ^ n ^ j = 1
y : G
hy : y ∈ (fun x ↦ x ^ n)^[j] ⁻¹' s
⊢ (⇑(zpowGroupHom n))^[j] g' = 1

Tactic:
simpa [zpowGroupHom]

Goal state after:
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f✝ g✝ f g : CircleDeg1Lift
x : ℝ
⊢ (f.comp g.toOrderHom).toFun (x + 1) = (f.comp g.toOrderHom).toFun x + 1

Tactic:
by simp [map_add_one]

Goal state after:
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f : CircleDeg1Lift
x : ℕ → ℝ
C : ℝ
H : ∀ (n : ℕ), dist ((f ^ n) 0) (x n) ≤ C
⊢ ∀ (t : ℕ), dist (f.transnumAuxSeq t) (x (2 ^ t) / 2 ^ t) ≤ C / 2 ^ t

Tactic:
intro n
    have : 0 < (2 ^ n : ℝ) := pow_pos zero_lt_two _
    convert! (div_le_div_iff_of_pos_right this).2 (H (2 ^ n)) using 1
    rw [transnumAuxSeq, Real.dist_eq, ← sub_div, abs_div, abs_of_pos this, Real.dist_eq]

Goal state after:
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f : CircleDeg1Lift
n : ℕ
⊢ ↑n * τ f + τ f = (↑n + 1) * τ f

Tactic:
add_mul,

Goal state after:
f : CircleDeg1Lift
n : ℕ
⊢ ↑n * τ f + τ f = ↑n * τ f + 1 * τ f
Module: Mathlib.MeasureTheory.Measure.ContinuousPreimage

Goal state before:
pp: X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : MeasurableSpace X
inst✝⁸ : BorelSpace X
inst✝⁷ : R1Space X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : MeasurableSpace Y
inst✝⁴ : BorelSpace Y
inst✝³ : R1Space Y
inst✝² : TopologicalSpace Z
μ : Measure X
ν : Measure Y
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : IsLocallyFiniteMeasure ν
f : Z → C(X, Y)
hf : Continuous[inst✝², _] f
hfm : ∀ (z : Z), MeasurePreserving (⇑(f z)) μ ν
s : Set X
t : Set Y
htm : NullMeasurableSet t ν
ht : ν t ≠ ∞
z : Z
hz : ∀ᶠ (ε : ℝ≥0∞) in 𝓝 0, ε < μ ((⇑(f z) ⁻¹' t) ∆ s)
w : Z
hw : μ ((⇑(f w) ⁻¹' t) ∆ (⇑(f z) ⁻¹' t)) < μ ((⇑(f z) ⁻¹' t) ∆ s)
hw' : ⇑(f w) ⁻¹' t =ᵐ[μ] s
⊢ False

Tactic:
rw [measure_congr (hw'.symmDiff (ae_eq_refl _)), symmDiff_comm] at hw

Goal state after:
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : MeasurableSpace X
inst✝⁸ : BorelSpace X
inst✝⁷ : R1Space X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : MeasurableSpace Y
inst✝⁴ : BorelSpace Y
inst✝³ : R1Space Y
inst✝² : TopologicalSpace Z
μ : Measure X
ν : Measure Y
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : IsLocallyFiniteMeasure ν
f : Z → C(X, Y)
hf : Continuous[inst✝², _] f
hfm : ∀ (z : Z), MeasurePreserving (⇑(f z)) μ ν
s : Set X
t : Set Y
htm : NullMeasurableSet t ν
ht : ν t ≠ ∞
z : Z
hz : ∀ᶠ (ε : ℝ≥0∞) in 𝓝 0, ε < μ ((⇑(f z) ⁻¹' t) ∆ s)
w : Z
hw : μ ((⇑(f z) ⁻¹' t) ∆ s) < μ ((⇑(f z) ⁻¹' t) ∆ s)
hw' : ⇑(f w) ⁻¹' t =ᵐ[μ] s
⊢ False
Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup

Goal state before:
pp: p : ℝ
inst✝ : Fact (0 < p)
s : AddSubgroup (AddCircle p)
h : ¬Dense ↑s
⊢ ∃ a, s = AddSubgroup.zmultiples a

Tactic:
rw [← QuotientAddGroup.dense_preimage_mk, ← QuotientAddGroup.coe_mk',
        ← AddSubgroup.coe_comap, xor_iff_not_iff'.1 (AddSubgroup.dense_xor_cyclic _)] at h
      rcases h with ⟨a, ha⟩
      use a
      rw [← QuotientAddGroup.coe_mk', ← AddMonoidHom.map_zmultiples, ← ha,
        AddSubgroup.map_comap_eq_self_of_surjective]
      exact Quot.mk_surjective

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

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
f : AddCircle T → AddCircle T := fun y ↦ n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving (⇑e) volume volume
h : n - 1 ≠ 0
hnx : n • DivisibleBy.div x (n - 1) = x + DivisibleBy.div x (n - 1)
y : AddCircle T
⊢ (⇑e ∘ f ∘ ⇑e.symm) y = n • y

Tactic:
simp only [f, e, hnx, MeasurableEquiv.coe_addLeft, MeasurableEquiv.symm_addLeft, comp_apply,
    smul_add, zsmul_neg', neg_smul, neg_add_rev]

Goal state after:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
f : AddCircle T → AddCircle T := fun y ↦ n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving (⇑e) volume volume
h : n - 1 ≠ 0
hnx : n • DivisibleBy.div x (n - 1) = x + DivisibleBy.div x (n - 1)
y : AddCircle T
⊢ DivisibleBy.div x (n - 1) + (-DivisibleBy.div x (n - 1) + -x + n • y + x) = n • y
Module: Mathlib.Dynamics.OmegaLimit

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

Tactic:
rcases hc₂ with ⟨v, hv₁, hv₂⟩
  rw [omegaLimit_eq_iInter_inter _ _ _ hv₁]
  apply IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed
  · rintro ⟨u₁, hu₁⟩ ⟨u₂, hu₂⟩
    use ⟨u₁ ∩ u₂, inter_mem hu₁ hu₂⟩
    constructor
    all_goals exact closure_mono (image2_subset (inter_subset_inter_left _ (by simp)) Subset.rfl)
  · intro u
    have hn : (image2 ϕ (u ∩ v) s).Nonempty :=
      Nonempty.image2 (Filter.nonempty_of_mem (inter_mem u.prop hv₁)) hs
    exact hn.mono subset_closure
  · intro
    apply hc₁.of_isClosed_subset isClosed_closure
    grw [inter_subset_right, hv₂]
  · exact fun _ ↦ isClosed_closure

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
⊢ (μ.rnDeriv ν)⁻¹ =ᵐ[μ] ν.rnDeriv μ

Tactic:
suffices (μ.rnDeriv ν)⁻¹ =ᵐ[μ] (μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)))⁻¹
      ∧ ν.rnDeriv μ =ᵐ[μ] (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ by
    refine (this.1.trans (Filter.EventuallyEq.trans ?_ this.2.symm))
    exact Measure.inv_rnDeriv_aux (absolutelyContinuous_withDensity_rnDeriv hμν)
      (withDensity_absolutelyContinuous _ _)
  constructor
  · filter_upwards [rnDeriv_withDensity_rnDeriv hμν] with x hx
    simp only [Pi.inv_apply, inv_inj]
    exact hx.symm
  · exact (Measure.rnDeriv_withDensity μ (Measure.measurable_rnDeriv ν μ)).symm

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 ≠ ∞
t : Set α := toMeasurable μ s
ht : t = toMeasurable μ s
⊢ ∫ (x : α) in s, (μ.rnDeriv ν x).toReal ∂ν ≤ μ.real s

Tactic:
have ht_m : MeasurableSet t := measurableSet_toMeasurable μ s

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
s : Set α
hμs : μ s ≠ ∞
t : Set α := toMeasurable μ s
ht : t = toMeasurable μ s
ht_m : MeasurableSet t
⊢ ∫ (x : α) in s, (μ.rnDeriv ν x).toReal ∂ν ≤ μ.real s
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

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

Tactic:
apply smaller_cover.coverMincard_le_card.not_gt

Goal state after:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
n : ℕ
inst✝ : U.IsSymm
s : Finset X
h : IsDynCoverOf T F U n ↑s
h' : ↑(#s) = coverMincard T F U n
x : X
x_s : x ∈ s
ball_empt : F ∩ ball x (dynEntourage T U n) = ∅
smaller_cover : IsDynCoverOf T F U n ↑(s.erase x)
⊢ ↑(#(s.erase x)) < coverMincard T F U n
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : SigmaFinite ν
⊢ ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν = (μ Set.univ).toReal - ((μ.singularPart ν) Set.univ).toReal

Tactic:
← ENNReal.toReal_sub_of_le (μ.singularPart_le ν Set.univ) (measure_ne_top _ _),

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : SigmaFinite ν
⊢ ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν = (μ Set.univ - (μ.singularPart ν) Set.univ).toReal
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: X : Type u_1
inst✝ : UniformSpace X
ι : Sort u_2
p : ι → Prop
s : ι → SetRel X X
h : (𝓤 X).HasBasis p s
T : X → X
F : Set X
⊢ coverEntropyInf T F = ⨆ i, ⨆ (_ : p i), coverEntropyInfEntourage T F (s i)

Tactic:
by
  refine (iSup₂_le fun U U_uni ↦ ?_).antisymm
    (iSup₂_mono' fun i h_i ↦ ⟨s i, HasBasis.mem_of_mem h h_i, le_refl _⟩)
  obtain ⟨i, h_i, si_U⟩ := (HasBasis.mem_iff h).1 U_uni
  exact (coverEntropyInfEntourage_antitone T F si_U).trans
    (le_iSup₂ (f := fun (i : ι) (_ : p i) ↦ coverEntropyInfEntourage T F (s i)) i h_i)

Goal state after:
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: case mk
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
g : M →[L] N
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)
h : { toFun := toFun✝, map_fun' := map_fun'✝, map_rel' := map_rel'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, map_fun' := map_fun'✝, map_rel' := map_rel'✝ } = g

Tactic:
cases g

Goal state after:
case mk.mk
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)
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)
h :
  { toFun := toFun✝¹, map_fun' := map_fun'✝¹, map_rel' := map_rel'✝¹ }.toFun =
    { toFun := toFun✝, map_fun' := map_fun'✝, map_rel' := map_rel'✝ }.toFun
⊢ { toFun := toFun✝¹, map_fun' := map_fun'✝¹, map_rel' := map_rel'✝¹ } =
    { toFun := toFun✝, map_fun' := map_fun'✝, map_rel' := map_rel'✝ }
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: case mk
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
g : M ↪[L] N
toEmbedding✝ : M ↪ N
map_fun'✝ :
  ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toEmbedding✝.toFun (funMap f x) = funMap f (toEmbedding✝.toFun ∘ x)
map_rel'✝ : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r (toEmbedding✝.toFun ∘ x) ↔ RelMap r x
h :
  (fun f ↦ f.toFun) { toEmbedding := toEmbedding✝, map_fun' := map_fun'✝, map_rel' := map_rel'✝ } = (fun f ↦ f.toFun) g
⊢ { toEmbedding := toEmbedding✝, map_fun' := map_fun'✝, map_rel' := map_rel'✝ } = g

Tactic:
cases g

Goal state after:
case mk.mk
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
toEmbedding✝¹ : M ↪ N
map_fun'✝¹ :
  ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toEmbedding✝¹.toFun (funMap f x) = funMap f (toEmbedding✝¹.toFun ∘ x)
map_rel'✝¹ : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r (toEmbedding✝¹.toFun ∘ x) ↔ RelMap r x
toEmbedding✝ : M ↪ N
map_fun'✝ :
  ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toEmbedding✝.toFun (funMap f x) = funMap f (toEmbedding✝.toFun ∘ x)
map_rel'✝ : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r (toEmbedding✝.toFun ∘ x) ↔ RelMap r x
h :
  (fun f ↦ f.toFun) { toEmbedding := toEmbedding✝¹, map_fun' := map_fun'✝¹, map_rel' := map_rel'✝¹ } =
    (fun f ↦ f.toFun) { toEmbedding := toEmbedding✝, map_fun' := map_fun'✝, map_rel' := map_rel'✝ }
⊢ { toEmbedding := toEmbedding✝¹, map_fun' := map_fun'✝¹, map_rel' := map_rel'✝¹ } =
    { toEmbedding := toEmbedding✝, map_fun' := map_fun'✝, map_rel' := map_rel'✝ }
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: case mk
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
g : M ≃[L] N
toEquiv✝ : M ≃ N
map_fun'✝ : ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toEquiv✝.toFun (funMap f x) = funMap f (toEquiv✝.toFun ∘ x)
map_rel'✝ : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r (toEquiv✝.toFun ∘ x) ↔ RelMap r x
h₁ : { toEquiv := toEquiv✝, map_fun' := map_fun'✝, map_rel' := map_rel'✝ }.toFun = g.toFun
h₂ : { toEquiv := toEquiv✝, map_fun' := map_fun'✝, map_rel' := map_rel'✝ }.invFun = g.invFun
⊢ { toEquiv := toEquiv✝, map_fun' := map_fun'✝, map_rel' := map_rel'✝ } = g

Tactic:
cases g

Goal state after:
case mk.mk
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
toEquiv✝¹ : M ≃ N
map_fun'✝¹ :
  ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toEquiv✝¹.toFun (funMap f x) = funMap f (toEquiv✝¹.toFun ∘ x)
map_rel'✝¹ : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r (toEquiv✝¹.toFun ∘ x) ↔ RelMap r x
toEquiv✝ : M ≃ N
map_fun'✝ : ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toEquiv✝.toFun (funMap f x) = funMap f (toEquiv✝.toFun ∘ x)
map_rel'✝ : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r (toEquiv✝.toFun ∘ x) ↔ RelMap r x
h₁ :
  { toEquiv := toEquiv✝¹, map_fun' := map_fun'✝¹, map_rel' := map_rel'✝¹ }.toFun =
    { toEquiv := toEquiv✝, map_fun' := map_fun'✝, map_rel' := map_rel'✝ }.toFun
h₂ :
  { toEquiv := toEquiv✝¹, map_fun' := map_fun'✝¹, map_rel' := map_rel'✝¹ }.invFun =
    { toEquiv := toEquiv✝, map_fun' := map_fun'✝, map_rel' := map_rel'✝ }.invFun
⊢ { toEquiv := toEquiv✝¹, map_fun' := map_fun'✝¹, map_rel' := map_rel'✝¹ } =
    { toEquiv := toEquiv✝, map_fun' := map_fun'✝, map_rel' := map_rel'✝ }
Module: Mathlib.ModelTheory.Algebra.Ring.Basic

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝⁵ : Add R
inst✝⁴ : Mul R
inst✝³ : Neg R
inst✝² : One R
inst✝¹ : Zero R
inst✝ : CompatibleRing R
v : α → R
⊢ Term.realize v 1 = 1

Tactic:
by
  simp [one_def, funMap_one, constantMap]

Goal state after:
Module: Mathlib.ModelTheory.Encoding

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

Tactic:
intro t l

Goal state after:
L : Language
α : Type u'
l✝ : List (L.Term α)
t : L.Term α
l : List (α ⊕ (i : ℕ) × L.Functions i)
⊢ listDecode (t.listEncode ++ l) = t :: listDecode l
Module: Mathlib.ModelTheory.ElementaryMaps

Goal state before:
pp: case mk
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : L.Structure M
inst✝² : L.Structure N
inst✝¹ : L.Structure P
inst✝ : L.Structure Q
g : M ↪ₑ[L] N
toFun✝ : M → N
map_formula'✝ : ∀ ⦃n : ℕ⦄ (φ : L.Formula (Fin n)) (x : Fin n → M), φ.Realize (toFun✝ ∘ x) ↔ φ.Realize x
h : (fun f ↦ ↑f) { toFun := toFun✝, map_formula' := map_formula'✝ } = (fun f ↦ ↑f) g
⊢ { toFun := toFun✝, map_formula' := map_formula'✝ } = g

Tactic:
cases g

Goal state after:
case mk.mk
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : L.Structure M
inst✝² : L.Structure N
inst✝¹ : L.Structure P
inst✝ : L.Structure Q
toFun✝¹ : M → N
map_formula'✝¹ : ∀ ⦃n : ℕ⦄ (φ : L.Formula (Fin n)) (x : Fin n → M), φ.Realize (toFun✝¹ ∘ x) ↔ φ.Realize x
toFun✝ : M → N
map_formula'✝ : ∀ ⦃n : ℕ⦄ (φ : L.Formula (Fin n)) (x : Fin n → M), φ.Realize (toFun✝ ∘ x) ↔ φ.Realize x
h :
  (fun f ↦ ↑f) { toFun := toFun✝¹, map_formula' := map_formula'✝¹ } =
    (fun f ↦ ↑f) { toFun := toFun✝, map_formula' := map_formula'✝ }
⊢ { toFun := toFun✝¹, map_formula' := map_formula'✝¹ } = { toFun := toFun✝, map_formula' := map_formula'✝ }
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin (n + 1) → M
⊢ (liftAt 1 n φ).Realize v xs ↔ φ.Realize v (xs ∘ castSucc)

Tactic:
realize_liftAt_one (refl n),

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin (n + 1) → M
⊢ φ.Realize v (xs ∘ fun i ↦ if ↑i < n then i.castSucc else i.succ) ↔ φ.Realize v (xs ∘ castSucc)
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case refine_1
L : Language
α : Type u'
i : ℕ
⊢ lift.{max u' u, 0} ↑i + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i)) ≤
    ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))

Tactic:
lift_natCast,

Goal state after:
case refine_1
L : Language
α : Type u'
i : ℕ
⊢ ↑i + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i)) ≤
    ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝³ : L.Structure M
inst✝² : L.Structure N
inst✝¹ : L.Structure P
S : L.Substructure M
s : Set M
inst✝ : Small.{u, w} ↑s
⊢ Small.{u, w} ↑(range (Term.realize Subtype.val))

Tactic:
exact small_range _

Goal state after:
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : L.Structure M
inst✝¹ : L.Structure N
inst✝ : L.Structure P
S✝ : L.Substructure M
s : Set M
ι : Type u_3
f : M →[L] N
hf : Function.Surjective ⇑f
S : L.Substructure N
x : N
h : x ∈ S
y : M
hy : f y = x
⊢ y ∈ comap f S ∧ f y = x

Tactic:
by simp [hy, h]

Goal state after: