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

Goal state before:
pp: case none.some.some
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : IsTrans α R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝¹ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct u.destruct
ha : none ∈ s.destruct
c : α × WSeq α
hc : some c ∈ u.destruct
val✝ : α × WSeq α
hb : some val✝ ∈ t.destruct
t1 : LiftRelO R (LiftRel R) none (some val✝)
t2 : LiftRelO R (LiftRel R) (some val✝) (some c)
⊢ LiftRelO R (fun s u ↦ ∃ t, LiftRel R s t ∧ LiftRel R t u) none (some c)

Tactic:
cases t1

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

Goal state before:
pp: case some.none.mk.none
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : IsTrans α R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝¹ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct u.destruct
hc : none ∈ u.destruct
fst✝ : α
snd✝ : WSeq α
ha : some (fst✝, snd✝) ∈ s.destruct
hb : none ∈ t.destruct
t2 : LiftRelO R (LiftRel R) none none
t1 : LiftRelO R (LiftRel R) (some (fst✝, snd✝)) none
⊢ LiftRelO R (fun s u ↦ ∃ t, LiftRel R s t ∧ LiftRel R t u) (some (fst✝, snd✝)) none

Tactic:
cases t1

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

Goal state before:
pp: case some.some.none
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : IsTrans α R
s✝¹ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝¹ t✝
h2✝¹ : LiftRel R t✝ u✝
s✝ u t : WSeq α
h1✝ : LiftRel R s✝ t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s✝.destruct t.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct u.destruct
c : α × WSeq α
hc : some c ∈ u.destruct
a : α
s : WSeq α
ha : some (a, s) ∈ s✝.destruct
hb : none ∈ t.destruct
t2 : LiftRelO R (LiftRel R) none (some c)
t1 : LiftRelO R (LiftRel R) (some (a, s)) none
⊢ LiftRelO R (fun s u ↦ ∃ t, LiftRel R s t ∧ LiftRel R t u) (some (a, s)) (some c)

Tactic:
cases t1

Goal state after:
Module: Mathlib.Data.Sigma.Order

Goal state before:
pp: case mp
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → Preorder (α i)
i : ι
a b : α i
hab : a < b
⊢ a ≤ b ∧ ¬b ≤ a

Tactic:
← lt_iff_le_not_ge

Goal state after:
case mp
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → Preorder (α i)
i : ι
a b : α i
hab : a < b
⊢ a < b
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
s : Seq α
n : ℕ
⊢ ((↑s).drop n).head = Computation.pure (s.get? n)

Tactic:
dropn_ofSeq,

Goal state after:
α : Type u
s : Seq α
n : ℕ
⊢ (↑(s.drop n)).head = Computation.pure (s.get? n)
Module: Mathlib.Data.SubtypeNeLift

Goal state before:
pp: ι : Type u_1
inst✝ : DecidableEq ι
M : ι → Type u_2
φ : (i : ι) → M i
i₀ : ι
⊢ subtypeNeLift i₀ (fun i ↦ φ ↑i) (φ i₀) = φ

Tactic:
by
  ext i
  by_cases h : i = i₀
  · subst h
    simp
  · rw [subtypeNeLift_of_neq _ _ _ _ h]

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

Goal state before:
pp: α : Type u
S : WSeq (WSeq α)
⊢ S.join.destruct = S.destruct.bind destruct_join.aux

Tactic:
apply
    Computation.eq_of_bisim
      (fun c1 c2 =>
        c1 = c2 ∨ ∃ S, c1 = destruct (join S) ∧ c2 = (destruct S).bind destruct_join.aux)
      _ (Or.inr ⟨S, rfl, rfl⟩)

Goal state after:
α : Type u
S : WSeq (WSeq α)
⊢ Computation.IsBisimulation fun c1 c2 ↦ c1 = c2 ∨ ∃ S, c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux
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
⊢ C a

Tactic:
let T : WSeq (Computation (α × Computation α)) := S.map fun c => c.map fun a => (a, c)

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
⊢ C a
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)
⊢ C a

Tactic:
have h' := h

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 ∈ parallel S
⊢ C a
Module: Mathlib.Data.Vector.Snoc

Goal state before:
pp: α : Type u_1
n : ℕ
x : α
xs : Vector α n
⊢ (xs.snoc x).reverse = x ::ᵥ xs.reverse

Tactic:
cases xs
  simp only [reverse, snoc, cons, toList_mk]
  congr
  simp [toList, append_def]

Goal state after:
Module: Mathlib.Data.Vector.Zip

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
x : Vector α n
y : Vector β n
⊢ (zipWith f x y).tail = zipWith f x.tail y.tail

Tactic:
by
  ext
  simp [get_tail]

Goal state after:
Module: Mathlib.Data.Vector.MapLemmas

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

Tactic:
induction xs using Vector.revInductionOn generalizing s₁ s₂
  next => exact ⟨h₀, rfl⟩
  next xs x ih =>
    rcases (hR x h₀) with ⟨hR, _⟩
    simp only [mapAccumr_snoc, ih hR, true_and]
    congr 1

Goal state after:
Module: Mathlib.Data.Vector3

Goal state before:
pp: α : Type u_1
m n : ℕ
a : α
t : Vector3 α m
v : Vector3 α n
i : Fin2 (n + 1)
e : n + 1 + m = n + m + 1
⊢ insert a (t +-+ v) (Eq.recOn e (i.add m)) = Eq.recOn e (t +-+ insert a v i)

Tactic:
refine Vector3.recOn t (fun e => ?_) (@fun k b t IH _ => ?_) e

Goal state after:
case refine_1
α : Type u_1
m n : ℕ
a : α
t : Vector3 α m
v : Vector3 α n
i : Fin2 (n + 1)
e✝ : n + 1 + m = n + m + 1
e : n + 1 + 0 = n + 0 + 1
⊢ insert a ([] +-+ v) (Eq.recOn e (i.add 0)) = Eq.recOn e ([] +-+ insert a v i)

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
⊢ insert a ((b :: t) +-+ v) (Eq.recOn x✝ (i.add (k + 1))) = Eq.recOn x✝ ((b :: t) +-+ insert a v i)
Module: Mathlib.Data.WSeq.Productive

Goal state before:
pp: α : Type u
s : Seq α
n : ℕ
⊢ ((↑s).get? n).Terminates

Tactic:
rw [get?_ofSeq]; infer_instance

Goal state after:
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:
by simpa only [smul_smul] using! ((smul_set_ae_eq g₁).2 h₂).trans h₁

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}, g' ^ n ^ j = 1 → g' • s ⊆ s

Tactic:
(IsFixedPt.preimage_iterate hs j : (zpowGroupHom n)^[j] ⁻¹' s = s).symm

Goal state after:
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}, g' ^ n ^ j = 1 → g' • (fun x ↦ x ^ n)^[j] ⁻¹' s ⊆ (fun x ↦ x ^ n)^[j] ⁻¹' s
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
hI : I =ᵐ[volume] ball x (T / (2 * ↑(addOrderOf u)))
⊢ IsAddFundamentalDomain (↥(AddSubgroup.zmultiples u)) I volume

Tactic:
set G := AddSubgroup.zmultiples u

Goal state after:
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
hI : I =ᵐ[volume] ball x (T / (2 * ↑(addOrderOf u)))
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
⊢ IsAddFundamentalDomain (↥G) I volume
Module: Mathlib.MeasureTheory.Group.AddCircle

Goal state before:
pp: case refine_4
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
hG_card : #Finset.univ = n
⊢ volume univ ≤ ∑' (g : ↥G), volume (g +ᵥ I)

Tactic:
measure_vadd

Goal state after:
case refine_4
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
hG_card : #Finset.univ = n
⊢ volume univ ≤ ∑' (g : ↥G), volume I
Module: Mathlib.Topology.Order.CountableSeparating

Goal state before:
pp: case inl
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
he : Ioo x y = ∅
⊢ False

Tactic:
| inl he =>

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
μ' : Measure α := ν.withDensity (μ.rnDeriv ν)
h₁ : μ'.rnDeriv (ν.withDensity f) =ᵐ[ν] μ.rnDeriv (ν.withDensity f)
h₂ : μ.rnDeriv ν =ᵐ[ν] μ'.rnDeriv ν
hμ' :
  (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) =ᵐ[ν] fun x ↦
    (f x)⁻¹ * (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν x
x : α
⊢ μ'.rnDeriv (ν.withDensity f) x = μ.rnDeriv (ν.withDensity f) x →
    μ.rnDeriv ν x = μ'.rnDeriv ν x →
      (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) x = (f x)⁻¹ * (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν x →
        μ.rnDeriv (ν.withDensity f) x = (f x)⁻¹ * μ.rnDeriv ν x

Tactic:
hx₁

Goal state after:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
μ' : Measure α := ν.withDensity (μ.rnDeriv ν)
h₁ : μ'.rnDeriv (ν.withDensity f) =ᵐ[ν] μ.rnDeriv (ν.withDensity f)
h₂ : μ.rnDeriv ν =ᵐ[ν] μ'.rnDeriv ν
hμ' :
  (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) =ᵐ[ν] fun x ↦
    (f x)⁻¹ * (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν x
x : α
hx₁ : μ'.rnDeriv (ν.withDensity f) x = μ.rnDeriv (ν.withDensity f) x
⊢ μ.rnDeriv ν x = μ'.rnDeriv ν x →
    (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) x = (f x)⁻¹ * (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν x →
      μ.rnDeriv (ν.withDensity f) x = (f x)⁻¹ * μ.rnDeriv ν x
Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage

Goal state before:
pp: X : Type u_1
T : X → X
U V : SetRel X X
n : ℕ
⊢ ∀ i < n,
    (⋂ k, ⋂ (_ : k < n), map T^[k] T^[k] ⁻¹' U) ○ ⋂ k, ⋂ (_ : k < n), map T^[k] T^[k] ⁻¹' V ⊆
      map T^[i] T^[i] ⁻¹' (U ○ V)

Tactic:
intro k k_n xy xy_comp

Goal state after:
X : Type u_1
T : X → X
U V : SetRel X X
n k : ℕ
k_n : k < n
xy : X × X
xy_comp : xy ∈ (⋂ k, ⋂ (_ : k < n), map T^[k] T^[k] ⁻¹' U) ○ ⋂ k, ⋂ (_ : k < n), map T^[k] T^[k] ⁻¹' V
⊢ xy ∈ map T^[k] T^[k] ⁻¹' (U ○ V)
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν'
inst✝ : SigmaFinite ν'
h : μ ⟂ₘ ν
hνν' : ν ≪ ν'
⊢ μ.rnDeriv ν' =ᵐ[ν] 0

Tactic:
by
  let t := h.nullSet
  have ht : MeasurableSet t := h.measurableSet_nullSet
  refine ae_of_ae_restrict_of_ae_restrict_compl t ?_ (by simp [t])
  change μ.rnDeriv ν' =ᵐ[ν.restrict t] 0
  have : μ.rnDeriv ν' =ᵐ[ν.restrict t] (μ.restrict t).rnDeriv ν' := by
    have h : (μ.restrict t).rnDeriv ν' =ᵐ[ν] t.indicator (μ.rnDeriv ν') :=
      hνν'.ae_le (rnDeriv_restrict μ ν' ht)
    rw [Filter.EventuallyEq, ae_restrict_iff' ht]
    filter_upwards [h] with x hx hxt
    rw [hx, Set.indicator_of_mem hxt]
  refine this.trans ?_
  simp only [t, MutuallySingular.restrict_nullSet]
  suffices (0 : Measure α).rnDeriv ν' =ᵐ[ν'] 0 by
    have h_ac' : ν.restrict t ≪ ν' := restrict_le_self.absolutelyContinuous.trans hνν'
    exact h_ac'.ae_le this
  exact rnDeriv_zero _

Goal state after:
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
y z : X
k : ℕ
k_mn : k / m < n
y_int : (T^[k % m] ↑(t ⟨k / m, k_mn⟩), T^[k % m + m * (k / m)] y) ∈ U
z_int : (T^[k % m] ↑(t ⟨k / m, k_mn⟩), T^[k % m + m * (k / m)] z) ∈ U
⊢ ∃ b, (T^[k] y, b) ∈ U ∧ (b, T^[k] z) ∈ U

Tactic:
Nat.mod_add_div k m

Goal state after:
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
y z : X
k : ℕ
k_mn : k / m < n
y_int : (T^[k % m] ↑(t ⟨k / m, k_mn⟩), T^[k] y) ∈ U
z_int : (T^[k % m] ↑(t ⟨k / m, k_mn⟩), T^[k] z) ∈ U
⊢ ∃ b, (T^[k] y, b) ∈ U ∧ (b, T^[k] z) ∈ U
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: X : Type u_1
T : X → X
U : SetRel X X
F : Set X
inst✝ : UniformSpace X
F_comp : IsCompact F
F_inv : MapsTo T F F
U_uni : U ∈ 𝓤 X
n : ℕ
⊢ ∃ s, IsDynCoverOf T F U n ↑s

Tactic:
obtain ⟨(V : SetRel X X), V_uni, V_symm, V_U⟩ := comp_symm_mem_uniformity_sets U_uni

Goal state after:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
inst✝ : UniformSpace X
F_comp : IsCompact F
F_inv : MapsTo T F F
U_uni : U ∈ 𝓤 X
n : ℕ
V : SetRel X X
V_uni : V ∈ 𝓤 X
V_symm : V.IsSymm
V_U : V ○ V ⊆ U
⊢ ∃ s, IsDynCoverOf T F U n ↑s
Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj

Goal state before:
pp: X : Type u_1
Y : Type u_2
s F : Set X
V : SetRel Y Y
S : X → X
T : Y → Y
φ : X → Y
n : ℕ
h : Semiconj φ S T
h' : IsDynCoverOf S F (map φ φ ⁻¹' V) n s
x : X
hx : x ∈ F
⊢ ∃ y ∈ φ '' s, (φ x, y) ∈ dynEntourage T V n

Tactic:
obtain ⟨y, hy, hxy⟩ := h' hx

Goal state after:
X : Type u_1
Y : Type u_2
s F : Set X
V : SetRel Y Y
S : X → X
T : Y → Y
φ : X → Y
n : ℕ
h : Semiconj φ S T
h' : IsDynCoverOf S F (map φ φ ⁻¹' V) n s
x : X
hx : x ∈ F
y : X
hy : y ∈ s
hxy : (x, y) ∈ dynEntourage S (map φ φ ⁻¹' V) n
⊢ ∃ y ∈ φ '' s, (φ x, y) ∈ dynEntourage T V n
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

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

Tactic:
← expGrowthSup_const one_ne_zero one_ne_top,

Goal state after:
X : Type u_1
T : X → X
F : Set X
h : F.Nonempty
⊢ netEntropyEntourage T F univ = expGrowthSup fun x ↦ 1
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

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

Tactic:
← expGrowthSup_const one_ne_zero one_ne_top,

Goal state after:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
⊢ coverEntropyEntourage T F univ = expGrowthSup fun x ↦ 1
Module: Mathlib.FieldTheory.IsAlgClosed.Classification

Goal state before:
pp: case inr
K : Type u
L : Type v
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
p : ℕ
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
hp : p = 0
⊢ Nonempty (K ≃+* L)

Tactic:
· simp only [hp] at *
    let : CharZero K := CharP.charP_to_charZero K
    let : CharZero L := CharP.charP_to_charZero L
    exact ringEquiv_of_equiv_of_charZero hK hKL

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

Goal state before:
pp: ⊢ ring.card = 5

Tactic:
have : Fintype.card Language.ring.Symbols = 5 := rfl

Goal state after:
this : Fintype.card ring.Symbols = 5
⊢ ring.card = 5
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
φ : L ≃ᴸ L'
⊢ Function.RightInverse φ.invLHom.onTerm φ.toLHom.onTerm

Tactic:
Function.rightInverse_iff_comp,

Goal state after:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
φ : L ≃ᴸ L'
⊢ φ.toLHom.onTerm ∘ φ.invLHom.onTerm = id
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x y z : E
hx : x ∈ solvableByRad F E
hy : y ∈ solvableByRad F E
hz : z ∈ solvableByRad F E
hx' : Group.IsSolvable (minpoly F x).Gal
hy' : Group.IsSolvable (minpoly F y).Gal
hz' : z ∈ F⟮x, y⟯
p : F[X] := minpoly F x
q : F[X] := minpoly F y
hpq :
  (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F x)).Splits ∧
    (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F y)).Splits
⊢ Group.IsSolvable (minpoly F z).Gal

Tactic:
have f : ↥F⟮x, y⟯ →ₐ[F] (p * q).SplittingField :=
    Classical.choice <| nonempty_algHom_adjoin_of_splits <| by
      rintro a (rfl | rfl)
      · exact ⟨isIntegral_of_mem_solvableByRad hx, hpq.1⟩
      · exact ⟨isIntegral_of_mem_solvableByRad hy, hpq.2⟩

Goal state after:
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x y z : E
hx : x ∈ solvableByRad F E
hy : y ∈ solvableByRad F E
hz : z ∈ solvableByRad F E
hx' : Group.IsSolvable (minpoly F x).Gal
hy' : Group.IsSolvable (minpoly F y).Gal
hz' : z ∈ F⟮x, y⟯
p : F[X] := minpoly F x
q : F[X] := minpoly F y
hpq :
  (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F x)).Splits ∧
    (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F y)).Splits
f : ↥F⟮x, y⟯ →ₐ[F] (p * q).SplittingField
⊢ Group.IsSolvable (minpoly F z).Gal
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n : ℕ
φ : L ≃ᴸ L'
⊢ Function.RightInverse φ.invLHom.onBoundedFormula φ.toLHom.onBoundedFormula

Tactic:
Function.rightInverse_iff_comp,

Goal state after:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n : ℕ
φ : L ≃ᴸ L'
⊢ φ.toLHom.onBoundedFormula ∘ φ.invLHom.onBoundedFormula = id
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case succ.mp
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n✝ : ℕ
v : α → M
n : ℕ
ih : ∀ {φ : L.BoundedFormula α n}, φ.exs.Realize v ↔ ∃ xs, φ.Realize v xs
φ : L.BoundedFormula α (n + 1)
⊢ (∃ xs a, φ.Realize v (snoc xs a)) → ∃ xs, φ.Realize v xs

Tactic:
rintro ⟨xs, x, h⟩
      exact ⟨_, h⟩

Goal state after:
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
N : Type u_1
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M →[L] N
p : L.Substructure N
⊢ Substructure.map f ⊤ ≤ p ↔ comap f p = ⊤

Tactic:
map_le_iff_le_comap,

Goal state after:
L : Language
M : Type w
N : Type u_1
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M →[L] N
p : L.Substructure N
⊢ ⊤ ≤ comap f p ↔ comap f p = ⊤
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: case intro.intro.mp
M : Type w
A : Set M
L : Language
inst✝² : L.Structure M
α : Type u₁
β : Type u_1
s : Set (β → M)
h✝ : A.Definable L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  A.Definable L
    ((fun g ↦ g ∘ rangeSplitting f) ⁻¹'
      (fun g ↦ g ∘ Sum.inl) ''
        (fun g ↦ g ∘ ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ''
          (fun g ↦ g ∘ ⇑(Equiv.Set.sumCompl (range f))) '' s)
h' : A.Definable L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
x : α → M
hx : ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))
y : β → M
ys : y ∈ s
hy :
  ((y ∘ ⇑(Equiv.Set.sumCompl (range f))) ∘ ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ∘
      Sum.inl =
    x ∘ rangeSplitting f
a : α
⊢ (y ∘ f) a = x (rangeSplitting f (rangeFactorization f a))

Tactic:
← Function.comp_apply (f := x),

Goal state after:
case intro.intro.mp
M : Type w
A : Set M
L : Language
inst✝² : L.Structure M
α : Type u₁
β : Type u_1
s : Set (β → M)
h✝ : A.Definable L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  A.Definable L
    ((fun g ↦ g ∘ rangeSplitting f) ⁻¹'
      (fun g ↦ g ∘ Sum.inl) ''
        (fun g ↦ g ∘ ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ''
          (fun g ↦ g ∘ ⇑(Equiv.Set.sumCompl (range f))) '' s)
h' : A.Definable L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
x : α → M
hx : ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))
y : β → M
ys : y ∈ s
hy :
  ((y ∘ ⇑(Equiv.Set.sumCompl (range f))) ∘ ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ∘
      Sum.inl =
    x ∘ rangeSplitting f
a : α
⊢ (y ∘ f) a = (x ∘ rangeSplitting f) (rangeFactorization f a)
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
α : Type u'
M : Type w
inst✝ : L[[α]].Structure M
s : Set α
⊢ M ⊨ L.distinctConstantsTheory s ↔ Set.InjOn (fun i ↦ ↑(L.con i)) s

Tactic:
by
  simp only [distinctConstantsTheory, Theory.model_iff, Set.mem_image,
    Prod.exists, forall_exists_index, and_imp]
  refine ⟨fun h a as b bs ab => ?_, ?_⟩
  · contrapose! ab
    have h' := h _ a b ⟨⟨as, bs⟩, ab⟩ rfl
    simp only [Sentence.Realize, Formula.realize_not, Formula.realize_equal,
      Term.realize_constants] at h'
    exact h'
  · rintro h φ a b ⟨⟨as, bs⟩, ab⟩ rfl
    simp only [Sentence.Realize, Formula.realize_not, Formula.realize_equal, Term.realize_constants]
    exact fun contra => ab (h as bs contra)

Goal state after:
Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed

Goal state before:
pp: K : Type u_1
inst✝¹ : CommRing K
inst✝ : Nontrivial K
n : ℕ
v : Fin (n + 1) → K
⊢ (lift v) (genericMonicPoly n) =
    eval (v (Fin.last n)) ↑(((monicEquivDegreeLT n).trans (degreeLTEquiv K n).toEquiv).symm (v ∘ Fin.castSucc))

Tactic:
by
  simp [genericMonicPoly, monicEquivDegreeLT, degreeLTEquiv, eval_finsetSum]

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: case mpr
L : Language
T : L.Theory
φ : L.Sentence
this : DecidableEq L.Sentence := ⋯
⊢ (∀ (T0 : Finset L.Sentence), ↑T0 ⊆ T → (↑T0 ∪ {Formula.not φ}).IsSatisfiable) →
    ∀ (T0 : Finset L.Sentence), ↑T0 ⊆ T ∪ {Formula.not φ} → IsSatisfiable ↑T0

Tactic:
intro h T0 hT0
    exact IsSatisfiable.mono (h (T0.erase (Formula.not φ))
      (by simpa using hT0)) (by simp)

Goal state after:
Module: Mathlib.FieldTheory.Cardinality

Goal state before:
pp: α : Type u
inst✝ : Infinite α
⊢ Nonempty (Field α)

Tactic:
by
  suffices #α = #(FractionRing (MvPolynomial α <| ULift.{u} ℚ)) from
    (Cardinal.eq.1 this).map (·.field)
  simp

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Divisibility

Goal state before:
pp: a : ℕ
h : ¬ℵ₀ ≤ ↑a
p : Cardinal.{u_1}
k : ℕ
hp : Prime p
hk : 0 < k
hpk : p ^ k = ↑a
⊢ p ^ 1 ≤ p ^ k

Tactic:
apply power_le_power_left hp.ne_zero

Goal state after:
a : ℕ
h : ¬ℵ₀ ≤ ↑a
p : Cardinal.{u_1}
k : ℕ
hp : Prime p
hk : 0 < k
hpk : p ^ k = ↑a
⊢ 1 ≤ ↑k
Module: Mathlib.FieldTheory.FinTrdeg

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
ι : Type u_3
inst✝ : Finite ι
x : ι → L
hx : IsTranscendenceBasis K x
⊢ FinTrdeg K L

Tactic:
rw [finTrdeg_iff_trdeg, ← Cardinal.lift_lt_aleph0,
    ← hx.lift_cardinalMk_eq_trdeg, Cardinal.lift_lt_aleph0]
  exact Cardinal.mk_lt_aleph0

Goal state after: