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

Goal state before:
pp: α : Type u
s✝ t✝ : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
s t : WSeq α
h : c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t)
⊢ BisimO (fun c1 c2 ↦ ∃ s t, c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t)) c1.destruct
    c2.destruct

Tactic:
rw [h.left, h.right]

Goal state after:
α : Type u
s✝ t✝ : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
s t : WSeq α
h : c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t)
⊢ BisimO (fun c1 c2 ↦ ∃ s t, c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
    (s.append t).destruct.destruct (s.destruct.bind (destruct_append.aux t)).destruct
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: α : Type u
β : Type v
f : α → β
S : WSeq (Computation α)
⊢ map f (parallel S) = parallel (WSeq.map (map f) S)

Tactic:
by
  refine
    eq_of_bisim
      (fun c1 c2 =>
        ∃ l S,
          c1 = map f (corec parallel.aux1 (l, S)) ∧
            c2 = corec parallel.aux1 (l.map (map f), S.map (map f)))
      ?_ ⟨[], S, rfl, rfl⟩
  intro c1 c2 h
  exact
    match c1, c2, h with
    | _, _, ⟨l, S, rfl, rfl⟩ => by
      have : parallel.aux2 (l.map (map f))
          = lmap f (rmap (List.map (map f)) (parallel.aux2 l)) := by
        simp only [parallel.aux2, rmap, lmap]
        induction l with
        | nil => grind
        | cons => grind [destruct_map, lmap, rmap]
      simp only [BisimO, destruct_map, lmap, rmap, corec_eq, parallel.aux1.eq_1]
      rw [this]
      rcases parallel.aux2 l with a | l'
      · simp
      simp only [lmap, rmap]
      induction S using WSeq.recOn <;> simpa using ⟨_, _, rfl, rfl⟩

Goal state after:
Module: Mathlib.Data.Tree.Traversable

Goal state before:
pp: α : Type u_1
F : Type u → Type u_3
G : Type u → Type u_4
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
η : ApplicativeTransformation F G
β : Type u
f : α → F β
t : BinaryTree α
⊢ (fun {α} ↦ η.app α) (traverse f t) = traverse (η.app β ∘ f) t

Tactic:
induction t with
  | nil => rw [traverse, traverse, η.preserves_pure]
  | node v l r hl hr =>
    rw [traverse, traverse, η.preserves_seq, η.preserves_seq, η.preserves_map, hl, hr,
      Function.comp_apply]

Goal state after:
Module: Mathlib.Data.Sum.Interval

Goal state before:
pp: α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c₁ : γ₁
⊢ (∃ a₁ b₁ c₁_1, a = inl a₁ ∧ b = inl b₁ ∧ inl c₁ = inl c₁_1 ∧ c₁_1 ∈ f a₁ b₁) ↔
    ∃ a₁ b₁, a = inl a₁ ∧ b = inl b₁ ∧ c₁ ∈ f a₁ b₁

Tactic:
simp only [inl.injEq, exists_and_left, exists_eq_left']

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

Goal state before:
pp: case right
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
xs : Vector α n
ys : Vector β n
f : α → β → σ → σ × γ
s₀ : σ
S : Set σ
h₀ : s₀ ∈ S
closure : ∀ (a : α) (b : β) (s : σ), s ∈ S → (f a b s).1 ∈ S
out : ∀ (a : α) (b : β) (s s' : σ), s ∈ S → s' ∈ S → (f a b s).2 = (f a b s').2
⊢ ∀ {s : σ} {q : Unit} (a : α) (b : β), s ∈ S → (f a b s).1 ∈ S ∧ (f a b s).2 = ((), (f a b s₀).2).2

Tactic:
exact @fun s _q a b h => ⟨closure a b s h, out a b s s₀ h h₀⟩

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

Goal state before:
pp: f : CircleDeg1Lift
x : ℝ
m : ℤ
h : f x = x + ↑m
n : ℕ
⊢ (⇑f)^[n] x = x + ↑n * ↑m

Tactic:
simpa only [nsmul_eq_mul, add_right_iterate] using (f.commute_add_int m).iterate_eq_of_map_eq n h

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

Goal state before:
pp: f : CircleDeg1Lift
hf : Continuous ⇑f
m : ℤ
n : ℕ
hn : 0 < n
⊢ τ f = ↑m / ↑n ↔ ∃ x, (f ^ n) x = x + ↑m

Tactic:
by
  rw [eq_div_iff, mul_comm, ← translationNumber_pow] <;> [skip; exact ne_of_gt (Nat.cast_pos.2 hn)]
  exact (f ^ n).translationNumber_eq_int_iff (f.continuous_pow hf n)

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (f₁ g) = τ (f₂ g)
x : ℝ
g : G
⊢ τ ↑(f₂.toHomUnits g)⁻¹ = -τ (f₂ g)

Tactic:
translationNumber_units_inv,

Goal state after:
G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (f₁ g) = τ (f₂ g)
x : ℝ
g : G
⊢ -τ ↑(f₂.toHomUnits g) = -τ (f₂ g)
Module: Mathlib.MeasureTheory.Group.AddCircle

Goal state before:
pp: case refine_1
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))
hI : I =ᵐ[volume] B
hn : 1 ≤ ↑n
⊢ NullMeasurableSet I volume

Tactic:
exact measurableSet_ball.nullMeasurableSet.congr hI.symm

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

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : l.NeBot
u : ι → AddCircle T
μ : Measure (AddCircle T) := volume
hs : NullMeasurableSet s μ
hu₁ : ∀ (i : ι), u i +ᵥ s =ᵐ[μ] s
n : ι → ℕ := addOrderOf ∘ u
hu₂ : Tendsto n l atTop
hT₀ : 0 < T
hT₁ : ENNReal.ofReal T ≠ 0
h : μ s ≠ 0
d : AddCircle T
I : ι → Set (AddCircle T) := fun j ↦ closedBall d (T / (2 * ↑(n j)))
hd : Tendsto (fun j ↦ μ (s ∩ I j) / μ (I j)) l (𝓝 1)
j : ι
hj : 0 < n j
this : addOrderOf (u j) = n j
huj : IsOfFinAddOrder (u j)
huj' : 1 ≤ ↑(n j)
hI₀ : μ (I j) ≠ 0
hI₁ : μ (I j) ≠ ∞
⊢ ENNReal.ofReal (min T (2 * (T / (2 * ↑(n j))))) * ↑(n j) = ENNReal.ofReal T

Tactic:
mul_div,

Goal state after:
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : l.NeBot
u : ι → AddCircle T
μ : Measure (AddCircle T) := volume
hs : NullMeasurableSet s μ
hu₁ : ∀ (i : ι), u i +ᵥ s =ᵐ[μ] s
n : ι → ℕ := addOrderOf ∘ u
hu₂ : Tendsto n l atTop
hT₀ : 0 < T
hT₁ : ENNReal.ofReal T ≠ 0
h : μ s ≠ 0
d : AddCircle T
I : ι → Set (AddCircle T) := fun j ↦ closedBall d (T / (2 * ↑(n j)))
hd : Tendsto (fun j ↦ μ (s ∩ I j) / μ (I j)) l (𝓝 1)
j : ι
hj : 0 < n j
this : addOrderOf (u j) = n j
huj : IsOfFinAddOrder (u j)
huj' : 1 ≤ ↑(n j)
hI₀ : μ (I j) ≠ 0
hI₁ : μ (I j) ≠ ∞
⊢ ENNReal.ofReal (min T (2 * T / (2 * ↑(n j)))) * ↑(n j) = ENNReal.ofReal T
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
⊢ ENNReal.ofReal T ≤ ENNReal.ofReal (#Finset.univ • min T (2 * (T / (2 * ↑n))))

Tactic:
mul_div,

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
⊢ ENNReal.ofReal T ≤ ENNReal.ofReal (#Finset.univ • min T (2 * T / (2 * ↑n)))
Module: Mathlib.Dynamics.Ergodic.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
n : ℤ
hn✝ : 1 < |n|
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun y ↦ n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun j ↦ ↑(1 / ↑(n.natAbs ^ j) * T)
hn : 1 < n.natAbs
hu₀ : ∀ (j : ℕ), addOrderOf (u j) = n.natAbs ^ j
hnu : ∀ (j : ℕ), n ^ j • u j = 0
hu₁ : ∀ (j : ℕ), u j +ᵥ s =ᵐ[volume] s
⊢ Tendsto (fun j ↦ addOrderOf (u j)) atTop atTop

Tactic:
simp_rw [hu₀]

Goal state after:
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn✝ : 1 < |n|
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun y ↦ n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun j ↦ ↑(1 / ↑(n.natAbs ^ j) * T)
hn : 1 < n.natAbs
hu₀ : ∀ (j : ℕ), addOrderOf (u j) = n.natAbs ^ j
hnu : ∀ (j : ℕ), n ^ j • u j = 0
hu₁ : ∀ (j : ℕ), u j +ᵥ s =ᵐ[volume] s
⊢ Tendsto (fun j ↦ n.natAbs ^ j) atTop atTop
Module: Mathlib.Dynamics.Ergodic.RadonNikodym

Goal state before:
pp: X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
s : Set X
hsm : MeasurableSet s
hνs : ν (f ⁻¹' s) = 0
hμs : (μ.singularPart ν) sᶜ = 0
⊢ (μ.singularPart ν) (f ⁻¹' s) = (ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν) (f ⁻¹' s)

Tactic:
rw [add_apply, withDensity_absolutelyContinuous _ _ hνs, zero_add]

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

Goal state before:
pp: X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
s : Set X
hsm : MeasurableSet s
hνs : ν s = 0
hμs : (μ.singularPart ν) sᶜ = 0
⊢ (ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν) s = (μ.singularPart ν) s

Tactic:
rw [add_apply, withDensity_absolutelyContinuous _ _ hνs, zero_add]

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

Goal state before:
pp: X : Type u_1
T : X → X
U : SetRel X X
n : ℕ
⊢ coverMincard T ∅ U n = 0

Tactic:
← nonpos_iff_eq_zero

Goal state after:
X : Type u_1
T : X → X
U : SetRel X X
n : ℕ
⊢ coverMincard T ∅ U n ≤ 0
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SFinite ν
s : Set α
⊢ (∫⁻ (a : α) in s, μ.rnDeriv ν a ∂ν).toReal = ((ν.withDensity (μ.rnDeriv ν)) s).toReal

pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SFinite ν
s : Set α
⊢ ∀ᵐ (x : α) ∂ν.restrict s, μ.rnDeriv ν x < ∞

Tactic:
· rw [ENNReal.toReal_eq_toReal_iff, ← withDensity_apply' _ s]
    simp

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SFinite ν
s : Set α
⊢ ∀ᵐ (x : α) ∂ν.restrict s, μ.rnDeriv ν x < ∞
Module: Mathlib.Dynamics.TopologicalEntropy.Subset

Goal state before:
pp: case inr.inr
X : Type u_1
T : X → X
F G : Set X
U : SetRel X X
n : ℕ
hF : coverMincard T F U n < ⊤
hG : coverMincard T G U n < ⊤
s : Finset X
s_cover : IsDynCoverOf T F U n ↑s
s_coverMincard : ↑s.card = coverMincard T F U n
t : Finset X
t_cover : IsDynCoverOf T G U n ↑t
t_coverMincard : ↑t.card = coverMincard T G U n
⊢ coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n

Tactic:
rw [← s_coverMincard, ← t_coverMincard, ← ENat.natCast_add]

Goal state after:
case inr.inr
X : Type u_1
T : X → X
F G : Set X
U : SetRel X X
n : ℕ
hF : coverMincard T F U n < ⊤
hG : coverMincard T G U n < ⊤
s : Finset X
s_cover : IsDynCoverOf T F U n ↑s
s_coverMincard : ↑s.card = coverMincard T F U n
t : Finset X
t_cover : IsDynCoverOf T G U n ↑t
t_coverMincard : ↑t.card = coverMincard T G U n
⊢ coverMincard T (F ∪ G) U n ≤ ↑(s.card + t.card)
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: F : Type u_1
inst✝ : Field F
n : ℕ+
hn : ¬↑n = 0
hn'' : X ^ ↑n - 1 ≠ 0
σ✝ τ : (X ^ ↑n - 1).Gal
a : (X ^ ↑n - 1).SplittingField
ha : a ^ ↑n = 1
σ : (X ^ ↑n - 1).Gal
⊢ ∃ m, σ a = a ^ m

Tactic:
exact map_rootsOfUnity_eq_pow_self σ.toAlgHom (rootsOfUnity.mkOfPowEq a ha)

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: 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 (i a⁻¹) * C (i a) = 1

Tactic:
← C_mul,

Goal state after:
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 (i a⁻¹ * i a) = 1
Module: Mathlib.FieldTheory.IsAlgClosed.Classification

Goal state before:
pp: K : Type u
L : Type v
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
inst✝¹ : CharZero K
inst✝ : CharZero L
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
s : Set K
hs : IsTranscendenceBasis ℤ Subtype.val
t : Set L
ht : IsTranscendenceBasis ℤ Subtype.val
hL : ℵ₀ < #L
⊢ Cardinal.lift.{v, u} #↑s = Cardinal.lift.{u, v} #↑t

Tactic:
rw [← lift_injective (cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt _
        hs (le_of_eq mk_int) hK),
      ← lift_injective (cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt _
        ht (le_of_eq mk_int) hL)]

Goal state after:
K : Type u
L : Type v
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
inst✝¹ : CharZero K
inst✝ : CharZero L
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
s : Set K
hs : IsTranscendenceBasis ℤ Subtype.val
t : Set L
ht : IsTranscendenceBasis ℤ Subtype.val
hL : ℵ₀ < #L
⊢ Cardinal.lift.{v, u} #K = Cardinal.lift.{u, v} #L
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: 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)
c : E
⊢ C b * X - C c = C b * X - C b * C (c / b)

Tactic:
← C_mul,

Goal state after:
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)
c : E
⊢ C b * X - C c = C b * X - C (b * (c / b))
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))
⊢ map i (X ^ n - 1) = (Multiset.map ((fun x ↦ X - C x) ∘ fun c ↦ c / b) s).prod

Tactic:
rw [key1, hs, multiset_prod_comp, Multiset.map_map, key2, Multiset.prod_map_mul,
    Function.const_def (α := E) (y := C b), Multiset.map_const, Multiset.prod_replicate,
    hs', ← C_pow, hb, ← mul_assoc, C_mul_C, one_mul]

Goal state after:
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
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case nil
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
k : ℕ
f : L.BoundedFormula α k
v : α → M
xs : Fin k → M
⊢ (List.foldr imp f []).Realize v xs = ((∀ i ∈ [], i.Realize v xs) → f.Realize v xs)

pp: case cons
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
k : ℕ
f : L.BoundedFormula α k
v : α → M
xs : Fin k → M
head✝ : L.BoundedFormula α k
tail✝ : List (L.BoundedFormula α k)
tail_ih✝ : (List.foldr imp f tail✝).Realize v xs = ((∀ i ∈ tail✝, i.Realize v xs) → f.Realize v xs)
⊢ (List.foldr imp f (head✝ :: tail✝)).Realize v xs = ((∀ i ∈ head✝ :: tail✝, i.Realize v xs) → f.Realize v xs)

Tactic:
next => simp

Goal state after:
case cons
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
k : ℕ
f : L.BoundedFormula α k
v : α → M
xs : Fin k → M
head✝ : L.BoundedFormula α k
tail✝ : List (L.BoundedFormula α k)
tail_ih✝ : (List.foldr imp f tail✝).Realize v xs = ((∀ i ∈ tail✝, i.Realize v xs) → f.Realize v xs)
⊢ (List.foldr imp f (head✝ :: tail✝)).Realize v xs = ((∀ i ∈ head✝ :: tail✝, i.Realize v xs) → f.Realize v xs)
Module: Mathlib.ModelTheory.Ultraproducts

Goal state before:
pp: α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝ : (a : α) → L.Structure (M a)
n : ℕ
f : L.Functions n
x y : Fin n → (a : α) → M a
xy : x ≈ y
a : α
ha : ∀ (i : Fin n), x i a = y i a
⊢ a ∈ {x_1 | (fun a ↦ funMap f x a = funMap f y a) x_1}

Tactic:
simp only [Set.mem_ofPred_eq, ha]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case mp
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : DecidableEq α
inst✝ : Nonempty M
φ : L.Formula α
⊢ (∃ v, M ⊨ equivSentence φ) → M ⊨ φ.exClosure

Tactic:
rintro ⟨v, hv⟩
    exact (Formula.realize_exClosure φ).mpr ⟨fun a => v a,
      (BoundedFormula.realize_restrictFreeVar (φ := φ) (f := id) (v := fun a => v a) (v' := v)
        (fun _ => rfl)).2
        (by simpa [Formula.Realize]
          using (realize_equivSentence_symm M (Formula.equivSentence φ) v).2 hv)⟩

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
L : Language
inst✝ : L.Structure M
A : Set M
⊢ A.Definable₂ L (Set.diagonal M)

Tactic:
exists (Term.var 0).equal (Term.var 1)

Goal state after:
Module: Mathlib.ModelTheory.Skolem

Goal state before:
pp: case refine_2
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
κ : Cardinal.{w'}
h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ
h4 : lift.{w, w'} κ ≤ lift.{w', w} #M
s' : Set (ULift.{w', w} M)
h2 : lift.{w', w} #↑s ≤ #↑s'
h1 : ℵ₀ ≤ #↑s'
hs' : #↑s' = lift.{w, w'} κ
this : Nonempty M
h : lift.{w', w} #↑(⇑Equiv.ulift '' s') = #↑s'
⊢ ℵ₀ ≤ #↑(⇑Equiv.ulift '' s') ∧ lift.{w, max u v} L.card ≤ lift.{max u v, w} #↑(⇑Equiv.ulift '' s')

Tactic:
and_comm,

Goal state after:
case refine_2
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
κ : Cardinal.{w'}
h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ
h4 : lift.{w, w'} κ ≤ lift.{w', w} #M
s' : Set (ULift.{w', w} M)
h2 : lift.{w', w} #↑s ≤ #↑s'
h1 : ℵ₀ ≤ #↑s'
hs' : #↑s' = lift.{w, w'} κ
this : Nonempty M
h : lift.{w', w} #↑(⇑Equiv.ulift '' s') = #↑s'
⊢ lift.{w, max u v} L.card ≤ lift.{max u v, w} #↑(⇑Equiv.ulift '' s') ∧ ℵ₀ ≤ #↑(⇑Equiv.ulift '' s')
Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CompatibleRing K
p : ℕ
inst✝¹ : CharP K p
inst✝ : IsAlgClosed K
⊢ K ⊨ Theory.ACF p

Tactic:
refine Theory.model_union_iff.2 ⟨inferInstance, ?_⟩

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : CompatibleRing K
p : ℕ
inst✝¹ : CharP K p
inst✝ : IsAlgClosed K
⊢ K ⊨ genericMonicPolyHasRoot '' {n | 0 < n}
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
M : Type w'
inst✝ : L.Structure M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h3 : lift.{w', w} κ ≤ lift.{w, w'} #M
⊢ ∃ N, Nonempty (↑N ↪ₑ[L] M) ∧ #↑N = κ

Tactic:
by
  obtain ⟨S, _, hS⟩ := exists_elementarySubstructure_card_eq L ∅ κ h1 (by simp) h2 h3
  have : Small.{w} S := by
    rw [← lift_inj.{_, w + 1}, lift_lift, lift_lift] at hS
    exact small_iff_lift_mk_lt_univ.2 (lt_of_eq_of_lt hS κ.lift_lt_univ')
  refine
    ⟨(equivShrink S).bundledInduced L,
      ⟨S.subtype.comp (Equiv.bundledInducedEquiv L _).symm.toElementaryEmbedding⟩,
      lift_inj.1 (_root_.trans ?_ hS)⟩
  simp only [Equiv.bundledInduced_α, lift_mk_shrink']

Goal state after:
Module: Mathlib.GroupTheory.OreLocalization.Cardinality

Goal state before:
pp: R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : MulAction R X
hc : ∀ (s s' : ↥S), Commute s s'
⊢ #(OreLocalization S X) ≤ lift.{u, v} #X

Tactic:
by
  rcases finite_or_infinite X with _ | _
  · have := lift_mk_le_lift_mk_of_surjective (oreDiv_one_surjective_of_finite_right S X)
    rwa [lift_umax.{v, u}, lift_id'] at this
  have key (x : X) (s s' : S) (h : s • x = s' • x) (hc : Commute s s') : x /ₒ s = x /ₒ s' := by
    rw [oreDiv_eq_iff]
    refine ⟨s, s'.1, h, ?_⟩
    · exact_mod_cast hc
  let i (x : X × S) := x.1 /ₒ x.2
  have hsurj : Surjective i := Quotient.mk''_surjective
  have hi := rightInverse_surjInv hsurj
  let j := (fun x : X × S ↦ (x.1, x.2 • x.1)) ∘ surjInv hsurj
  suffices Injective j by
    have := lift_mk_le_lift_mk_of_injective this
    rwa [lift_umax.{v, u}, lift_id', mk_prod, lift_id, lift_mul, mul_eq_self (by simp)] at this
  intro
  grind

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

Goal state before:
pp: a : Cardinal.{u_1}
⊢ IsPrimePow a ↔ ℵ₀ ≤ a ∨ ∃ n, a = ↑n ∧ IsPrimePow n

Tactic:
by
  by_cases h : ℵ₀ ≤ a
  · simp [h, (prime_of_aleph0_le h).isPrimePow]
  simp only [h, false_or, isPrimePow_nat_iff]
  lift a to ℕ using not_le.mp h
  rw [isPrimePow_def]
  refine
    ⟨?_, fun ⟨n, han, p, k, hp, hk, h⟩ =>
          ⟨p, k, nat_is_prime_iff.2 hp, hk, by rw [han]; exact mod_cast h⟩⟩
  rintro ⟨p, k, hp, hk, hpk⟩
  have key : p ^ (1 : Cardinal) ≤ ↑a := by
    rw [← hpk]; apply power_le_power_left hp.ne_zero; exact mod_cast hk
  rw [power_one] at key
  lift p to ℕ using key.trans_lt natCast_lt_aleph0
  exact ⟨a, rfl, p, k, nat_is_prime_iff.mp hp, hk, mod_cast hpk⟩

Goal state after:
Module: Mathlib.FieldTheory.Finite.Polynomial

Goal state before:
pp: case intro
K : Type u_1
σ : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Finite σ
val✝ : Fintype σ
e : (σ → K) → K
x✝ : e ∈ ⊤
⊢ ∃ y ∈ restrictDegree σ K (Fintype.card K - 1), (evalₗ K σ) y = e

Tactic:
classical
  refine ⟨∑ n : σ → K, e n • indicator n, ?_, ?_⟩
  · exact sum_mem fun c _ => smul_mem _ _ (indicator_mem_restrictDegree _)
  · ext n
    simp only [evalₗ_apply, map_sum, smul_eval]
    rw [Finset.sum_eq_single n] <;>
      aesop (add simp [eval_indicator_apply_eq_zero, eval_indicator_apply_eq_one, eq_comm])

Goal state after:
Module: Mathlib.FieldTheory.Finite.Valuation

Goal state before:
pp: Fq : Type u_1
A : Type u_2
Γ : Type u_3
inst✝⁴ : Field Fq
inst✝³ : Finite Fq
inst✝² : Ring A
inst✝¹ : Algebra Fq A
inst✝ : LinearOrderedCommMonoidWithZero Γ
v : Valuation A Γ
a : Fq
⊢ v ((algebraMap Fq A) a) ≤ 1

Tactic:
by_cases a = 0

Goal state after:
case pos
Fq : Type u_1
A : Type u_2
Γ : Type u_3
inst✝⁴ : Field Fq
inst✝³ : Finite Fq
inst✝² : Ring A
inst✝¹ : Algebra Fq A
inst✝ : LinearOrderedCommMonoidWithZero Γ
v : Valuation A Γ
a : Fq
h✝ : a = 0
⊢ v ((algebraMap Fq A) a) ≤ 1

case neg
Fq : Type u_1
A : Type u_2
Γ : Type u_3
inst✝⁴ : Field Fq
inst✝³ : Finite Fq
inst✝² : Ring A
inst✝¹ : Algebra Fq A
inst✝ : LinearOrderedCommMonoidWithZero Γ
v : Valuation A Γ
a : Fq
h✝ : ¬a = 0
⊢ v ((algebraMap Fq A) a) ≤ 1