mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Sigma.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝² x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
⊢ ⟨k, c⟩ ∈ sigmaLift (fun x ↦ Ioc) ⟨i, a⟩ ⟨j, b⟩ ↔ ⟨i, a⟩ < ⟨k, c⟩ ∧ ⟨k, c⟩ ≤ ⟨j, b⟩

Tactic:
mem_sigmaLift,

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝² x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
⊢ (∃ (h : i = k) (h_1 : j = k), c ∈ Ioc (⋯ ▸ a) (⋯ ▸ b)) ↔ ⟨i, a⟩ < ⟨k, c⟩ ∧ ⟨k, c⟩ ≤ ⟨j, b⟩
Module: Mathlib.Data.Sigma.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝² x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
⊢ ⟨k, c⟩ ∈ sigmaLift (fun x ↦ Ioo) ⟨i, a⟩ ⟨j, b⟩ ↔ ⟨i, a⟩ < ⟨k, c⟩ ∧ ⟨k, c⟩ < ⟨j, b⟩

Tactic:
mem_sigmaLift,

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝² x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
⊢ (∃ (h : i = k) (h_1 : j = k), c ∈ Ioo (⋯ ▸ a) (⋯ ▸ b)) ↔ ⟨i, a⟩ < ⟨k, c⟩ ∧ ⟨k, c⟩ < ⟨j, b⟩
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case right
α : 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 β)
⊢ b ∈ T.join.destruct →
    ∃ a ∈ S.join.destruct,
      LiftRelO R
        (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) a
        b

Tactic:
mb

Goal state after:
case right
α : 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
⊢ ∃ a ∈ S.join.destruct,
    LiftRelO R
      (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) a b
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case refl.refl
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun c ↦ map (fun a ↦ (a, c)) c) S
this✝ : S = WSeq.map (map fun c ↦ c.1) T
pe : parallel S = map (fun c ↦ c.1) (parallel T)
h' : a ∈ map (fun c ↦ c.1) (parallel T)
this : (parallel T).Terminates
c : Computation α
dT : (a, c) ∈ parallel T
d' : Computation (α × Computation α)
dT' : d' ∈ T
ad' : (a, c) ∈ d'
c' : Computation α
cs' : c' ∈ S
e' : map (fun a ↦ (a, c')) c' = d'
⊢ a ∈ c ∧ c ∈ S

Tactic:
← e'

Goal state after:
case refl.refl
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun c ↦ map (fun a ↦ (a, c)) c) S
this✝ : S = WSeq.map (map fun c ↦ c.1) T
pe : parallel S = map (fun c ↦ c.1) (parallel T)
h' : a ∈ map (fun c ↦ c.1) (parallel T)
this : (parallel T).Terminates
c : Computation α
dT : (a, c) ∈ parallel T
d' : Computation (α × Computation α)
dT' : d' ∈ T
c' : Computation α
ad' : (a, c) ∈ map (fun a ↦ (a, c')) c'
cs' : c' ∈ S
e' : map (fun a ↦ (a, c')) c' = d'
⊢ a ∈ c ∧ c ∈ S
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun c ↦ map (fun a ↦ (a, c)) c) S
this✝¹ : S = WSeq.map (map fun c ↦ c.1) T
pe : parallel S = map (fun c ↦ c.1) (parallel T)
h' : a ∈ map (fun c ↦ c.1) (parallel T)
this✝ : (parallel T).Terminates
a' : α
c : Computation α
e : (parallel T).get = (a', c)
this : a ∈ c ∧ c ∈ S
⊢ C a

Tactic:
obtain ⟨ac, cs⟩ := this

Goal state after:
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun c ↦ map (fun a ↦ (a, c)) c) S
this✝ : S = WSeq.map (map fun c ↦ c.1) T
pe : parallel S = map (fun c ↦ c.1) (parallel T)
h' : a ∈ map (fun c ↦ c.1) (parallel T)
this : (parallel T).Terminates
a' : α
c : Computation α
e : (parallel T).get = (a', c)
ac : a ∈ c
cs : c ∈ S
⊢ C a
Module: Mathlib.Data.Vector.Snoc

Goal state before:
pp: case succ
α : Type u_1
n✝ : ℕ
val : α
n : ℕ
ih : replicate (n + 1) val = (replicate n val).snoc val
⊢ val ::ᵥ replicate (n + 1) val = val ::ᵥ (replicate n val).snoc val

Tactic:
ih

Goal state after:
case succ
α : Type u_1
n✝ : ℕ
val : α
n : ℕ
ih : replicate (n + 1) val = (replicate n val).snoc val
⊢ val ::ᵥ (replicate n val).snoc val = val ::ᵥ (replicate n val).snoc val
Module: Mathlib.Data.Vector.Mem

Goal state before:
pp: α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
a' : α
v' : Vector α n
h : v = a' ::ᵥ v'
⊢ a = a' ∨ a ∈ v'.toList ↔ a = a' ∨ a ∈ (a' ::ᵥ v').tail.toList

Tactic:
Vector.tail_cons

Goal state after:
Module: Mathlib.Data.W.Constructions

Goal state before:
pp: γ : Type u
f : Listβ γ Listα.nil → WType (Listβ γ)
⊢ ofList γ (toList γ (mk Listα.nil f)) = mk Listα.nil f

Tactic:
simp only [toList, ofList, mk.injEq, heq_eq_eq, true_and]
    ext x
    cases x

Goal state after:
Module: Mathlib.Data.Vector3

Goal state before:
pp: case refine_2
α : Type u_1
m n : ℕ
a : α
t✝ : Vector3 α m
v : Vector3 α n
i : Fin2 (n + 1)
e : n + 1 + m = n + m + 1
k : ℕ
b : α
t : Vector3 α k
IH : ∀ (x : n + 1 + k = n + k + 1), insert a (t +-+ v) (Eq.recOn x (i.add k)) = Eq.recOn x (t +-+ insert a v i)
x✝ : n + 1 + (k + 1) = n + (k + 1) + 1
e' : n + 1 + k = n + k + 1
⊢ insert a (b :: t +-+ v) (Eq.recOn ⋯ (i.add k).fs) = Eq.recOn ⋯ (b :: t +-+ insert a v i)

Tactic:
rw [← (Eq.recOn e' rfl :
      fs (Eq.recOn e' (i.add k) : Fin2 ((n + k) + 1)) =
        Eq.recOn (congr_arg (· + 1) e' : _ + 1 = _) (fs (i.add k)))]

Goal state after:
case refine_2
α : Type u_1
m n : ℕ
a : α
t✝ : Vector3 α m
v : Vector3 α n
i : Fin2 (n + 1)
e : n + 1 + m = n + m + 1
k : ℕ
b : α
t : Vector3 α k
IH : ∀ (x : n + 1 + k = n + k + 1), insert a (t +-+ v) (Eq.recOn x (i.add k)) = Eq.recOn x (t +-+ insert a v i)
x✝ : n + 1 + (k + 1) = n + (k + 1) + 1
e' : n + 1 + k = n + k + 1
⊢ insert a (b :: t +-+ v) (Eq.recOn e' (i.add k)).fs = Eq.recOn ⋯ (b :: t +-+ insert a v i)
Module: Mathlib.MeasureTheory.Group.AEStabilizer

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
s : Set α
g₁ g₂ : G
h₁ : g₁ ∈ {g | g • s =ᵐ[μ] s}
h₂ : g₂ ∈ {g | g • s =ᵐ[μ] s}
⊢ g₁ * g₂ ∈ {g | g • s =ᵐ[μ] s}

Tactic:
simpa only [smul_smul] using! ((smul_set_ae_eq g₁).2 h₂).trans h₁

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

Goal state before:
pp: f : CircleDeg1Lift
x : ℝ
m : ℤ
n : ℕ
hn : 0 < n
⊢ (⇑f)^[n] x < x + ↑n * ↑m ↔ f x < x + ↑m

Tactic:
by
  simpa only [nsmul_eq_mul, add_right_iterate] using
    (f.commute_add_int m).iterate_pos_lt_iff_map_lt f.monotone (strictMono_id.add_const (m : ℝ)) hn

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

Goal state before:
pp: case inr.mp
a b : ℝ
hb : b ≠ 0
⊢ Dense ↑(AddSubgroup.closure {a, b}) → Irrational (a / b)

Tactic:
rintro hd ⟨r, hr⟩

Goal state after:
case inr.mp
a b : ℝ
hb : b ≠ 0
hd : Dense ↑(AddSubgroup.closure {a, b})
r : ℚ
hr : ↑r = a / b
⊢ False
Module: Mathlib.Dynamics.Ergodic.Conservative

Goal state before:
pp: case e'_2
α : 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
x✝ a✝ : ℕ
⊢ ¬μ (t a✝) = 0 → a✝ ≤ x✝ ↔ a✝ ∈ {n | μ (s ∩ f^[n] ⁻¹' s) ≠ 0} → a✝ ≤ x✝

Tactic:
mem_ofPred

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 α := fun n ↦ s ∩ f^[n] ⁻¹' s
H : {n | μ (s ∩ f^[n] ⁻¹' s) ≠ 0}.Finite
x✝ a✝ : ℕ
⊢ ¬μ (t a✝) = 0 → a✝ ≤ x✝ ↔ μ (s ∩ f^[a✝] ⁻¹' s) ≠ 0 → a✝ ≤ x✝
Module: Mathlib.Topology.Order.CountableSeparating

Goal state before:
pp: case refine_3
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : LinearOrder X
inst✝¹ : OrderTopology X
inst✝ : SecondCountableTopology X
s✝ s : Set X
hsc : s.Countable
hsd : Dense s
t : Set X := s ∪ {x | ∃ y, y ⋖ x}
x y : X
h : ∀ s ∈ Iio '' t, x ∈ s ↔ y ∈ s
hne : x ≠ y
⊢ False

Tactic:
wlog hlt : x < y generalizing x y

Goal state after:
case refine_3.inr
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : LinearOrder X
inst✝¹ : OrderTopology X
inst✝ : SecondCountableTopology X
s✝ s : Set X
hsc : s.Countable
hsd : Dense s
t : Set X := s ∪ {x | ∃ y, y ⋖ x}
x y : X
h : ∀ s ∈ Iio '' t, x ∈ s ↔ y ∈ s
hne : x ≠ y
this : ∀ (x y : X), (∀ s ∈ Iio '' t, x ∈ s ↔ y ∈ s) → x ≠ y → x < y → False
hlt : ¬x < y
⊢ False

X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : LinearOrder X
inst✝¹ : OrderTopology X
inst✝ : SecondCountableTopology X
s✝ s : Set X
hsc : s.Countable
hsd : Dense s
t : Set X := s ∪ {x | ∃ y, y ⋖ x}
x y : X
h : ∀ s ∈ Iio '' t, x ∈ s ↔ y ∈ s
hne : x ≠ y
hlt : x < y
⊢ False
Module: Mathlib.Dynamics.Ergodic.RadonNikodym

Goal state before:
pp: X : Type u_1
m : MeasurableSpace X
μ✝ ν : Measure X
inst✝¹ : IsFiniteMeasure ν
f : X → X
hfν : MeasurePreserving f ν ν
μ : Measure X
inst✝ : IsFiniteMeasure μ
hfμ : MeasurePreserving f μ μ
hμν : μ ≪ ν
c : ENNReal
s : Set X := {a | μ.rnDeriv ν a < c}
hsm : MeasurableSet s
⊢ ∀ᵐ (a : X) ∂ν, (μ.rnDeriv ν ∘ f) a < c ↔ μ.rnDeriv ν a < c

Tactic:
have hμ_sdiff : μ (f ⁻¹' s \ s) = μ (s \ f ⁻¹' s) :=
    measure_sdiff_symm (hfμ.measurable hsm).nullMeasurableSet hsm.nullMeasurableSet
      (hfμ.measure_preimage hsm.nullMeasurableSet) (by finiteness)

Goal state after:
X : Type u_1
m : MeasurableSpace X
μ✝ ν : Measure X
inst✝¹ : IsFiniteMeasure ν
f : X → X
hfν : MeasurePreserving f ν ν
μ : Measure X
inst✝ : IsFiniteMeasure μ
hfμ : MeasurePreserving f μ μ
hμν : μ ≪ ν
c : ENNReal
s : Set X := {a | μ.rnDeriv ν a < c}
hsm : MeasurableSet s
hμ_sdiff : μ (f ⁻¹' s \ s) = μ (s \ f ⁻¹' s)
⊢ ∀ᵐ (a : X) ∂ν, (μ.rnDeriv ν ∘ f) a < c ↔ μ.rnDeriv ν a < c
Module: Mathlib.Dynamics.Ergodic.Extreme

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

Tactic:
rw [mem_extremePoints_iff_left]

Goal state after:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
inst✝ : IsFiniteMeasure μ
hμ : Ergodic f μ
⊢ μ ∈ {ν | MeasurePreserving f ν ν ∧ ν univ = μ univ} ∧
    ∀ x₁ ∈ {ν | MeasurePreserving f ν ν ∧ ν univ = μ univ},
      ∀ x₂ ∈ {ν | MeasurePreserving f ν ν ∧ ν univ = μ univ}, μ ∈ openSegment ℝ≥0∞ x₁ x₂ → x₁ = μ
Module: Mathlib.Dynamics.SymbolicDynamics.Basic

Goal state before:
pp: A : Type u_1
inst✝² : Inhabited A
G : Type u_2
inst✝¹ : Monoid G
inst✝ : IsLeftCancelMul G
x : G → A
U : Finset G
⊢ Pattern A G

Tactic:
classical
  exact { config := fun g => if g ∈ U then x g else default,
          support := U,
          condition := fun g hg => if_neg hg }

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 : β
⊢ (∀ n ∈ 𝓝 y, ∀ {U : Set τ}, U ∈ f → ∃ x ∈ U, (s ∩ ϕ x ⁻¹' n).Nonempty) →
    ∀ i ∈ f, ∀ t ∈ 𝓝 y, (t ∩ image2 ϕ i s).Nonempty

Tactic:
· intro h _ hu _ hn
    rcases h _ hn hu with ⟨_, ht, _, hx, hϕtx⟩
    exact ⟨_, hϕtx, _, ht, _, hx, rfl⟩

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 α
u : Set τ
hu : u ∈ f
a✝ : β
hx : a✝ ∈ ⋂ u, closure[inst✝] (image2 ϕ (↑u) s)
⊢ a✝ ∈ closure[inst✝] (image2 ϕ u s)

Tactic:
mem_iInter

Goal state after:
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
u : Set τ
hu : u ∈ f
a✝ : β
hx : ∀ (i : ↑f.sets), a✝ ∈ closure[inst✝] (image2 ϕ (↑i) s)
⊢ a✝ ∈ closure[inst✝] (image2 ϕ u s)
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)
this : ⋃ u ∈ f, j u = ⋃ u, j ↑u
⊢ k \ ⋃ u, j ↑u ⊆ n

Tactic:
sdiff_iUnion

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)
this : ⋃ u ∈ f, j u = ⋃ u, j ↑u
⊢ ⋂ i, k \ j ↑i ⊆ n
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
pp: X : Type u_1
T : X → X
U : SetRel X X
n : ℕ
F : Set X
s t : Finset X
hs : IsDynNetIn T F U n ↑s
ht : IsDynCoverOf T F U n ↑t
⊢ s.card ≤ t.card

Tactic:
have (x : X) (x_s : x ∈ s) : ∃ z ∈ t, z ∈ ball x (dynEntourage T U n) := by
    simpa using! ht (hs.1 x_s)

Goal state after:
X : Type u_1
T : X → X
U : SetRel X X
n : ℕ
F : Set X
s t : Finset X
hs : IsDynNetIn T F U n ↑s
ht : IsDynCoverOf T F U n ↑t
this : ∀ x ∈ s, ∃ z ∈ t, z ∈ ball x (dynEntourage T U n)
⊢ s.card ≤ t.card
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h_fin : coverMincard T F U n < ⊤
k : ℕ
k_min : ↑k = coverMincard T F U n
h : ¬Nonempty { s // IsDynCoverOf T F U n ↑s }
⊢ ∀ (i : Finset X), IsDynCoverOf T F U n ↑i → ↑(#i) = ⊤

Tactic:
simp only [ENat.natCast_ne_top, imp_false]

Goal state after:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h_fin : coverMincard T F U n < ⊤
k : ℕ
k_min : ↑k = coverMincard T F U n
h : ¬Nonempty { s // IsDynCoverOf T F U n ↑s }
⊢ ∀ (i : Finset X), ¬IsDynCoverOf T F U n ↑i
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: X : Type u_1
T : X → X
U : SetRel X X
⊢ (expGrowthSup fun n ↦ ↑0) = ⊥

Tactic:
rw [ENat.toENNReal_zero, ← Pi.zero_def, expGrowthSup_zero]

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

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), netEntropyInfEntourage T F (s i)

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

Goal state after:
Module: Mathlib.FieldTheory.IsAlgClosed.Classification

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
K' : Type u
inst✝³ : Field K'
inst✝² : Algebra R K'
inst✝¹ : IsAlgClosed K'
ι' : Type u
v' : ι' → K'
inst✝ : Nontrivial R
hv : IsTranscendenceBasis R v'
hR : #R ≤ ℵ₀
hK : ℵ₀ < #K'
⊢ #K' = #ι'

Tactic:
by
  simpa using cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt v' hv hR hK

Goal state after:
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: L : Language
L' : Language
M : Type w
inst✝ : L.Structure M
α : Type w'
ie : IsEmpty α
⊢ (L.lhomWithConstants α).comp ((LHom.id L).sumElim (LHom.ofIsEmpty (constantsOn α) L)) = LHom.id L[[α]]

Tactic:
simp only [LHom.comp_sumElim, lhomWithConstants, LHom.comp_id]

Goal state after:
L : Language
L' : Language
M : Type w
inst✝ : L.Structure M
α : Type w'
ie : IsEmpty α
⊢ LHom.sumInl.sumElim (LHom.sumInl.comp (LHom.ofIsEmpty (constantsOn α) L)) = LHom.id L[[α]]
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
f : M ≃[L] N
n : ℕ
f' : L.Functions n
x : Fin n → N
⊢ funMap f' x = f.toEquiv (funMap f' (⇑f.symm ∘ x))

Tactic:
refine Eq.trans ?_ (f.map_fun' f' (f.toEquiv.symm ∘ x)).symm

Goal state after:
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
f : M ≃[L] N
n : ℕ
f' : L.Functions n
x : Fin n → N
⊢ funMap f' x = funMap f' (f.toFun ∘ ⇑f.symm ∘ x)
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: case e'_2
L : Language
M : Type w
N : Type w'
inst✝² : L.Structure M
inst✝¹ : L.Structure N
P : Type u_1
inst✝ : L.Structure P
h : M ≃[L] N
f g : N ≃[L] P
hfg : (fun f ↦ f.comp h) f = (fun f ↦ f.comp h) g
⊢ f = f.comp (refl L N)

Tactic:
comp_refl

Goal state after:
case e'_2
L : Language
M : Type w
N : Type w'
inst✝² : L.Structure M
inst✝¹ : L.Structure N
P : Type u_1
inst✝ : L.Structure P
h : M ≃[L] N
f g : N ≃[L] P
hfg : (fun f ↦ f.comp h) f = (fun f ↦ f.comp h) g
⊢ f = f
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: case e'_3
L : Language
M : Type w
N : Type w'
inst✝² : L.Structure M
inst✝¹ : L.Structure N
P : Type u_1
inst✝ : L.Structure P
h : M ≃[L] N
f g : N ≃[L] P
hfg : (fun f ↦ f.comp h) f = (fun f ↦ f.comp h) g
⊢ g = g.comp (refl L N)

Tactic:
comp_refl

Goal state after:
case e'_3
L : Language
M : Type w
N : Type w'
inst✝² : L.Structure M
inst✝¹ : L.Structure N
P : Type u_1
inst✝ : L.Structure P
h : M ≃[L] N
f g : N ≃[L] P
hfg : (fun f ↦ f.comp h) f = (fun f ↦ f.comp h) g
⊢ g = g
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case func.zero.inr
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
_ts✝ : Fin 0 → L[[γ]].Term α
ih : ∀ (a : Fin 0), (_ts✝ a).constantsToVars.varsToConstants = _ts✝ a
val✝ : (constantsOn γ).Functions 0
⊢ (func (Sum.inr val✝) _ts✝).constantsToVars.varsToConstants = func (Sum.inr val✝) _ts✝

Tactic:
simp [constantsToVars, varsToConstants, Constants.term, eq_iff_true_of_subsingleton]

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 ↦ (LHom.id L).onTerm (_ts✝ i)) = id (func _f✝ _ts✝)

Tactic:
ih

Goal state after:
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✝)
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 ↦ (φ.comp ψ).onTerm (_ts✝ i)) = (φ.onTerm ∘ ψ.onTerm) (func _f✝ _ts✝)

Tactic:
ih

Goal state after:
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✝)
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
n : ℕ
t : L[[α]].Term (β ⊕ Fin n)
v : β → M
xs : Fin n → M
⊢ realize (Sum.elim (Sum.elim (fun a ↦ ↑(L.con a)) v) xs) (constantsVarsEquivLeft t) = realize (Sum.elim v xs) t

Tactic:
by
  simp only [constantsVarsEquivLeft, realize_relabel, Equiv.coe_trans, Function.comp_apply,
    constantsVarsEquiv_apply, relabelEquiv_symm_apply]
  refine _root_.trans ?_ realize_constantsToVars
  congr 1; funext x -- Note: was previously rcongr x
  rcases x with (a | (b | i)) <;> simp

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 [ih]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
l : ℕ
v : α → M
xs : Fin l → M
R : L.Relations 2
t₁ t₂ : L.Term (α ⊕ Fin l)
⊢ (R.boundedFormula₂ t₁ t₂).Realize v xs ↔ RelMap R ![realize (Sum.elim v xs) t₁, realize (Sum.elim v xs) t₂]

Tactic:
rw [Relations.boundedFormula₂, realize_rel, iff_eq_eq]
  refine congr rfl (funext (Fin.cases ?_ ?_))
  · simp only [Matrix.cons_val_zero]
  · simp only [Matrix.cons_val_succ, Matrix.cons_val_fin_one, forall_const]

Goal state after:
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: case var
L : Language
M : Type w
inst✝ : L.Structure M
S : L.Substructure M
α : Type u_3
xs : α → M
h : ∀ (a : α), xs a ∈ S
a : α
⊢ realize xs (var a) ∈ S

Tactic:
exact h a

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:
ih

Goal state after:
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
⊢ φ :: l = φ :: l
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
S : Set (L.Substructure M)
Sne : S.Nonempty
hS : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) S
x : M
this : Nonempty ↑S
⊢ x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s

Tactic:
simp only [sSup_eq_iSup', mem_iSup_of_directed hS.directed_val, Subtype.exists, exists_prop]

Goal state after: