mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
pp: case nil
α : Type u_1
γ : Type u_3
σ : Type u_5
n : ℕ
f : α → α → σ → σ × γ
comm : ∀ (a₁ a₂ : α) (s : σ), f a₁ a₂ s = f a₂ a₁ s
s : σ
⊢ mapAccumr₂ f nil nil s = mapAccumr₂ f nil nil s

pp: case cons
α : Type u_1
γ : Type u_3
σ : Type u_5
n : ℕ
f : α → α → σ → σ × γ
comm : ∀ (a₁ a₂ : α) (s : σ), f a₁ a₂ s = f a₂ a₁ s
n✝ : ℕ
a✝¹ b✝ : α
x✝ y✝ : Vector α n✝
a✝ : ∀ {s : σ}, mapAccumr₂ f x✝ y✝ s = mapAccumr₂ f y✝ x✝ s
s : σ
⊢ mapAccumr₂ f (a✝¹ ::ᵥ x✝) (b✝ ::ᵥ y✝) s = mapAccumr₂ f (b✝ ::ᵥ y✝) (a✝¹ ::ᵥ x✝) s

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
γ : Type u_3
σ : Type u_5
n : ℕ
f : α → α → σ → σ × γ
comm : ∀ (a₁ a₂ : α) (s : σ), f a₁ a₂ s = f a₂ a₁ s
s : σ
⊢ mapAccumr₂ f nil nil s = mapAccumr₂ f nil nil s

case cons
α : Type u_1
γ : Type u_3
σ : Type u_5
n : ℕ
f : α → α → σ → σ × γ
comm : ∀ (a₁ a₂ : α) (s : σ), f a₁ a₂ s = f a₂ a₁ s
n✝ : ℕ
a✝¹ b✝ : α
x✝ y✝ : Vector α n✝
a✝ : ∀ {s : σ}, mapAccumr₂ f x✝ y✝ s = mapAccumr₂ f y✝ x✝ s
s : σ
⊢ mapAccumr₂ f (a✝¹ ::ᵥ x✝) (b✝ ::ᵥ y✝) s = mapAccumr₂ f (b✝ ::ᵥ y✝) (a✝¹ ::ᵥ x✝) s
Module: Mathlib.Data.Vector3

Goal state before:
pp: case refine_1
α : Type u_1
n : ℕ
a b : α
v : Vector3 α n
i : Fin2 (n + 1)
j✝ : Fin2 (n + 1 + 1)
j : Fin2 (n + 1)
⊢ (a :: b :: v)
      (match fz with
      | fz => fz
      | k.fs => k.fs.fs) =
    (a :: v) fz

pp: case refine_2
α : Type u_1
n : ℕ
a b : α
v : Vector3 α n
i : Fin2 (n + 1)
j✝ : Fin2 (n + 1 + 1)
j : Fin2 (n + 1)
⊢ ∀ (n_1 : Fin2 n),
    (a :: b :: v)
        (match n_1.fs with
        | fz => fz
        | k.fs => k.fs.fs) =
      (a :: v) n_1.fs

Tactic:
<;>

Goal state after:
case refine_1
α : Type u_1
n : ℕ
a b : α
v : Vector3 α n
i : Fin2 (n + 1)
j✝ : Fin2 (n + 1 + 1)
j : Fin2 (n + 1)
⊢ (a :: b :: v)
      (match fz with
      | fz => fz
      | k.fs => k.fs.fs) =
    (a :: v) fz

case refine_2
α : Type u_1
n : ℕ
a b : α
v : Vector3 α n
i : Fin2 (n + 1)
j✝ : Fin2 (n + 1 + 1)
j : Fin2 (n + 1)
⊢ ∀ (n_1 : Fin2 n),
    (a :: b :: v)
        (match n_1.fs with
        | fz => fz
        | k.fs => k.fs.fs) =
      (a :: v) n_1.fs
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
xs : Vector α n
ys : Vector β n
f : α → β → γ
⊢ map₂ f nil nil = map₂ (flip f) nil nil

pp: case cons
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
xs : Vector α n
ys : Vector β n
f : α → β → γ
n✝ : ℕ
a✝¹ : α
b✝ : β
x✝ : Vector α n✝
y✝ : Vector β n✝
a✝ : map₂ f x✝ y✝ = map₂ (flip f) y✝ x✝
⊢ map₂ f (a✝¹ ::ᵥ x✝) (b✝ ::ᵥ y✝) = map₂ (flip f) (b✝ ::ᵥ y✝) (a✝¹ ::ᵥ x✝)

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
xs : Vector α n
ys : Vector β n
f : α → β → γ
⊢ map₂ f nil nil = map₂ (flip f) nil nil

case cons
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
xs : Vector α n
ys : Vector β n
f : α → β → γ
n✝ : ℕ
a✝¹ : α
b✝ : β
x✝ : Vector α n✝
y✝ : Vector β n✝
a✝ : map₂ f x✝ y✝ = map₂ (flip f) y✝ x✝
⊢ map₂ f (a✝¹ ::ᵥ x✝) (b✝ ::ᵥ y✝) = map₂ (flip f) (b✝ ::ᵥ y✝) (a✝¹ ::ᵥ x✝)
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
s : σ
xs : Vector α n
ys : Vector β n
f : α → β → σ → σ × γ
⊢ mapAccumr₂ f nil nil s = mapAccumr₂ (flip f) nil nil s

pp: case cons
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
s : σ
xs : Vector α n
ys : Vector β n
f : α → β → σ → σ × γ
n✝ : ℕ
a✝¹ : α
b✝ : β
x✝ : Vector α n✝
y✝ : Vector β n✝
a✝ : mapAccumr₂ f x✝ y✝ s = mapAccumr₂ (flip f) y✝ x✝ s
⊢ mapAccumr₂ f (a✝¹ ::ᵥ x✝) (b✝ ::ᵥ y✝) s = mapAccumr₂ (flip f) (b✝ ::ᵥ y✝) (a✝¹ ::ᵥ x✝) s

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
s : σ
xs : Vector α n
ys : Vector β n
f : α → β → σ → σ × γ
⊢ mapAccumr₂ f nil nil s = mapAccumr₂ (flip f) nil nil s

case cons
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
s : σ
xs : Vector α n
ys : Vector β n
f : α → β → σ → σ × γ
n✝ : ℕ
a✝¹ : α
b✝ : β
x✝ : Vector α n✝
y✝ : Vector β n✝
a✝ : mapAccumr₂ f x✝ y✝ s = mapAccumr₂ (flip f) y✝ x✝ s
⊢ mapAccumr₂ f (a✝¹ ::ᵥ x✝) (b✝ ::ᵥ y✝) s = mapAccumr₂ (flip f) (b✝ ::ᵥ y✝) (a✝¹ ::ᵥ x✝) s
Module: Mathlib.Order.SemiconjSup

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β
g : β → α
h : IsOrderRightAdjoint f g
e : γ ≃o α
y : β
⊢ IsLUB (⇑e ⁻¹' {x | f x ≤ y}) (e.symm (g y))

Tactic:
rw [e.isLUB_preimage, e.apply_symm_apply]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β
g : β → α
h : IsOrderRightAdjoint f g
e : γ ≃o α
y : β
⊢ IsLUB {x | f x ≤ y} (g y)
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

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

Tactic:
exact fun n => C / 2 ^ n

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

Goal state before:
pp: case refine_1
G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (f₁ g) = τ (f₂ g)
this : ∀ (x : ℝ), BddAbove (range fun g ↦ (f₂ g⁻¹) ((f₁ g) x))
F₁ : G →* ℝ ≃o ℝ := toOrderIso.comp f₁.toHomUnits
F₂ : G →* ℝ ≃o ℝ := toOrderIso.comp f₂.toHomUnits
hF₁ : ∀ (g : G), ⇑(F₁ g) = ⇑(f₁ g)
hF₂ : ∀ (g : G), ⇑(F₂ g) = ⇑(f₂ g)
x y : ℝ
hxy : x ≤ y
⊢ (fun x ↦ ⨆ g', (F₂ g')⁻¹ ((F₁ g') x)) x ≤ (fun x ↦ ⨆ g', (F₂ g')⁻¹ ((F₁ g') x)) y

pp: case refine_2
G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (f₁ g) = τ (f₂ g)
this : ∀ (x : ℝ), BddAbove (range fun g ↦ (f₂ g⁻¹) ((f₁ g) x))
F₁ : G →* ℝ ≃o ℝ := toOrderIso.comp f₁.toHomUnits
F₂ : G →* ℝ ≃o ℝ := toOrderIso.comp f₂.toHomUnits
hF₁ : ∀ (g : G), ⇑(F₁ g) = ⇑(f₁ g)
hF₂ : ∀ (g : G), ⇑(F₂ g) = ⇑(f₂ g)
x : ℝ
⊢ { toFun := fun x ↦ ⨆ g', (F₂ g')⁻¹ ((F₁ g') x), monotone' := ⋯ }.toFun (x + 1) =
    { toFun := fun x ↦ ⨆ g', (F₂ g')⁻¹ ((F₁ g') x), monotone' := ⋯ }.toFun x + 1

pp: case refine_3
G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (f₁ g) = τ (f₂ g)
this : ∀ (x : ℝ), BddAbove (range fun g ↦ (f₂ g⁻¹) ((f₁ g) x))
F₁ : G →* ℝ ≃o ℝ := toOrderIso.comp f₁.toHomUnits
F₂ : G →* ℝ ≃o ℝ := toOrderIso.comp f₂.toHomUnits
hF₁ : ∀ (g : G), ⇑(F₁ g) = ⇑(f₁ g)
hF₂ : ∀ (g : G), ⇑(F₂ g) = ⇑(f₂ g)
x : ℝ
⊢ BddAbove (range fun g ↦ (F₂ g)⁻¹ ((F₁ g) x))

Tactic:
<;>

Goal state after:
case refine_1
G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (f₁ g) = τ (f₂ g)
this : ∀ (x : ℝ), BddAbove (range fun g ↦ (f₂ g⁻¹) ((f₁ g) x))
F₁ : G →* ℝ ≃o ℝ := toOrderIso.comp f₁.toHomUnits
F₂ : G →* ℝ ≃o ℝ := toOrderIso.comp f₂.toHomUnits
hF₁ : ∀ (g : G), ⇑(F₁ g) = ⇑(f₁ g)
hF₂ : ∀ (g : G), ⇑(F₂ g) = ⇑(f₂ g)
x y : ℝ
hxy : x ≤ y
⊢ (fun x ↦ ⨆ g', (F₂ g')⁻¹ ((F₁ g') x)) x ≤ (fun x ↦ ⨆ g', (F₂ g')⁻¹ ((F₁ g') x)) y

case refine_2
G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (f₁ g) = τ (f₂ g)
this : ∀ (x : ℝ), BddAbove (range fun g ↦ (f₂ g⁻¹) ((f₁ g) x))
F₁ : G →* ℝ ≃o ℝ := toOrderIso.comp f₁.toHomUnits
F₂ : G →* ℝ ≃o ℝ := toOrderIso.comp f₂.toHomUnits
hF₁ : ∀ (g : G), ⇑(F₁ g) = ⇑(f₁ g)
hF₂ : ∀ (g : G), ⇑(F₂ g) = ⇑(f₂ g)
x : ℝ
⊢ { toFun := fun x ↦ ⨆ g', (F₂ g')⁻¹ ((F₁ g') x), monotone' := ⋯ }.toFun (x + 1) =
    { toFun := fun x ↦ ⨆ g', (F₂ g')⁻¹ ((F₁ g') x), monotone' := ⋯ }.toFun x + 1

case refine_3
G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (f₁ g) = τ (f₂ g)
this : ∀ (x : ℝ), BddAbove (range fun g ↦ (f₂ g⁻¹) ((f₁ g) x))
F₁ : G →* ℝ ≃o ℝ := toOrderIso.comp f₁.toHomUnits
F₂ : G →* ℝ ≃o ℝ := toOrderIso.comp f₂.toHomUnits
hF₁ : ∀ (g : G), ⇑(F₁ g) = ⇑(f₁ g)
hF₂ : ∀ (g : G), ⇑(F₂ g) = ⇑(f₂ g)
x : ℝ
⊢ BddAbove (range fun g ↦ (F₂ g)⁻¹ ((F₁ g) x))
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
pp: case mp
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
⊢ netMaxcard T F U n < ⊤ → ∃ s, IsDynNetIn T F U n ↑s ∧ ↑s.card = netMaxcard T F U n

pp: case mpr
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
⊢ (∃ s, IsDynNetIn T F U n ↑s ∧ ↑s.card = netMaxcard T F U n) → netMaxcard T F U n < ⊤

Tactic:
<;>

Goal state after:
case mp
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
⊢ netMaxcard T F U n < ⊤ → ∃ s, IsDynNetIn T F U n ↑s ∧ ↑s.card = netMaxcard T F U n

case mpr
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
⊢ (∃ s, IsDynNetIn T F U n ↑s ∧ ↑s.card = netMaxcard T F U n) → netMaxcard T F U n < ⊤
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 : ℕ
V : SetRel X X
V_uni : V ∈ 𝓤 X
V_symm : V.IsSymm
V_U : V ○ V ⊆ U
s : Finset X
left✝ : ∀ x ∈ s, x ∈ F
s_cover : F ⊆ ⋃ x ∈ s, ball x V
⊢ ∃ s, IsDynCoverOf T F U n ↑s

Tactic:
have : IsDynCoverOf T F V 1 s := .of_subset_iUnion_ball <| by simpa using s_cover

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 : Finset X
left✝ : ∀ x ∈ s, x ∈ F
s_cover : F ⊆ ⋃ x ∈ s, ball x V
this : IsDynCoverOf T F V 1 ↑s
⊢ ∃ s, IsDynCoverOf T F U n ↑s
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: τ : Type u_1
inst✝² : TopologicalSpace τ
inst✝¹ : AddCommGroup τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
hf : ∀ (t : τ), Tendsto (fun x ↦ t + x) f f
x✝ : α
h : ∀ n ∈ 𝓝 x✝, ∀ {U : Set τ}, U ∈ f → ∃ x ∈ U, (ϕ.toFun x '' ω f ϕ.toFun s ∩ n).Nonempty
n : Set α
hn : n ∈ 𝓝 x✝
u : Set τ
hu : u ∈ f
o : Set α
ho₁ : o ⊆ n
ho₂ : IsOpen[inst✝] o
ho₃ : x✝ ∈ o
t : τ
_ht₁ : t ∈ u
ht₂ : (ϕ.toFun t '' ω f ϕ.toFun s ∩ o).Nonempty
l₁ : (ω f ϕ.toFun s ∩ o).Nonempty
⊢ ∃ x ∈ u, (ϕ.toFun x '' s ∩ n).Nonempty

Tactic:
have l₂ : (closure (image2 ϕ u s) ∩ o).Nonempty :=
    l₁.mono fun b hb ↦ ⟨omegaLimit_subset_closure_image2 _ _ _ hu hb.1, hb.2⟩

Goal state after:
τ : Type u_1
inst✝² : TopologicalSpace τ
inst✝¹ : AddCommGroup τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
hf : ∀ (t : τ), Tendsto (fun x ↦ t + x) f f
x✝ : α
h : ∀ n ∈ 𝓝 x✝, ∀ {U : Set τ}, U ∈ f → ∃ x ∈ U, (ϕ.toFun x '' ω f ϕ.toFun s ∩ n).Nonempty
n : Set α
hn : n ∈ 𝓝 x✝
u : Set τ
hu : u ∈ f
o : Set α
ho₁ : o ⊆ n
ho₂ : IsOpen[inst✝] o
ho₃ : x✝ ∈ o
t : τ
_ht₁ : t ∈ u
ht₂ : (ϕ.toFun t '' ω f ϕ.toFun s ∩ o).Nonempty
l₁ : (ω f ϕ.toFun s ∩ o).Nonempty
l₂ : (closure[inst✝] (image2 ϕ.toFun u s) ∩ o).Nonempty
⊢ ∃ x ∈ u, (ϕ.toFun x '' s ∩ n).Nonempty
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
pp: X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
⊢ netMaxcard T F U 0 = 1

Tactic:
apply (iSup₂_le _).antisymm ((one_le_netMaxcard_iff T F U 0).2 h)
  intro s ⟨_, s_net⟩
  simp only [ball, dynEntourage_zero, preimage_univ] at s_net
  norm_cast
  refine Finset.card_le_one.2 fun x x_s y y_s ↦ ?_
  exact PairwiseDisjoint.elim_set s_net x_s y_s x (mem_univ x) (mem_univ x)

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

Goal state before:
pp: case mp
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
⊢ netMaxcard T F U n = ⊤ → ∀ (k : ℕ), ∃ s, IsDynNetIn T F U n ↑s ∧ k ≤ s.card

pp: case mpr
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
⊢ (∀ (k : ℕ), ∃ s, IsDynNetIn T F U n ↑s ∧ k ≤ s.card) → netMaxcard T F U n = ⊤

Tactic:
<;>

Goal state after:
case mp
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
⊢ netMaxcard T F U n = ⊤ → ∀ (k : ℕ), ∃ s, IsDynNetIn T F U n ↑s ∧ k ≤ s.card

case mpr
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
⊢ (∀ (k : ℕ), ∃ s, IsDynNetIn T F U n ↑s ∧ k ≤ s.card) → netMaxcard T F U n = ⊤
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
pp: case a
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
⊢ coverEntropyInf T F ≤ ⨆ U ∈ 𝓤 X, netEntropyInfEntourage T F U

pp: case a
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
⊢ ⨆ U ∈ 𝓤 X, netEntropyInfEntourage T F U ≤ coverEntropyInf T F

Tactic:
<;>

Goal state after:
case a
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
⊢ coverEntropyInf T F ≤ ⨆ U ∈ 𝓤 X, netEntropyInfEntourage T F U

case a
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
⊢ ⨆ U ∈ 𝓤 X, netEntropyInfEntourage T F U ≤ coverEntropyInf T F
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
pp: case a
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
⊢ coverEntropy T F ≤ ⨆ U ∈ 𝓤 X, netEntropyEntourage T F U

pp: case a
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
⊢ ⨆ U ∈ 𝓤 X, netEntropyEntourage T F U ≤ coverEntropy T F

Tactic:
<;>

Goal state after:
case a
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
⊢ coverEntropy T F ≤ ⨆ U ∈ 𝓤 X, netEntropyEntourage T F U

case a
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
⊢ ⨆ U ∈ 𝓤 X, netEntropyEntourage T F U ≤ coverEntropy T F
Module: Mathlib.Dynamics.TopologicalEntropy.Subset

Goal state before:
pp: X : Type u_1
T : X → X
F : Set X
inst✝ : UniformSpace X
h : Continuous T
⊢ coverEntropyInf T (closure F) = coverEntropyInf T F

Tactic:
refine (iSup₂_le fun U U_uni ↦ ?_).antisymm (coverEntropyInf_monotone T subset_closure)

Goal state after:
X : Type u_1
T : X → X
F : Set X
inst✝ : UniformSpace X
h : Continuous T
U : Set (X × X)
U_uni : U ∈ 𝓤 X
⊢ coverEntropyInfEntourage T (closure F) U ≤ coverEntropyInf T F
Module: Mathlib.RingTheory.Algebraic.Cardinality

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
L : Type v
inst✝⁴ : CommRing L
inst✝³ : IsDomain L
inst✝² : Algebra R L
inst✝¹ : IsTorsionFree R L
inst✝ : Algebra.IsAlgebraic R L
x y : L
⊢ (fun x ↦
          let p := Classical.indefiniteDescription (fun x_1 ↦ x_1 ≠ 0 ∧ (Polynomial.aeval x) x_1 = 0) ⋯;
          ⟨↑p, ⟨x, ⋯⟩⟩)
        x =
      (fun x ↦
          let p := Classical.indefiniteDescription (fun x_1 ↦ x_1 ≠ 0 ∧ (Polynomial.aeval x) x_1 = 0) ⋯;
          ⟨↑p, ⟨x, ⋯⟩⟩)
        y →
    x = y

Tactic:
intro h
      simp only [Set.coe_ofPred, ne_eq, Set.mem_ofPred_eq, Sigma.mk.inj_iff] at h
      refine (Subtype.heq_iff_coe_eq ?_).1 h.2
      simp only [h.1, forall_true_iff]

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case neg
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
⊢ (map i (X ^ n - 1)).Splits

Tactic:
let s := ((X ^ n - C a).map i).roots

Goal state after:
case neg
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
⊢ (map i (X ^ n - 1)).Splits
Module: Mathlib.ModelTheory.LanguageMap

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

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

Tactic:
<;>

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

case h_rel
L : Language
α : Type w'
β : Type u_1
f : α → β
x✝¹ : ℕ
x✝ : L.Relations x✝¹
⊢ ((L.lhomWithConstantsMap f).comp LHom.sumInl).onRelation x✝ = (L.lhomWithConstants β).onRelation x✝
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 = ((fun f ↦ f.comp h) f).comp h.symm

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 = ((fun f ↦ f.comp h) g).comp h.symm

Tactic:
<;>

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 = ((fun f ↦ f.comp h) f).comp h.symm

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 = ((fun f ↦ f.comp h) g).comp h.symm
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: case funMap
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
a : Language.empty.Structure M
x✝¹ : ℕ
f : Language.empty.Functions x✝¹
x✝ : Fin x✝¹ → M
⊢ funMap f x✝ = funMap f x✝

pp: case RelMap
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
a : Language.empty.Structure M
x✝¹ : ℕ
f : Language.empty.Relations x✝¹
x✝ : Fin x✝¹ → M
⊢ RelMap f x✝ ↔ RelMap f x✝

Tactic:
<;>

Goal state after:
case funMap
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
a : Language.empty.Structure M
x✝¹ : ℕ
f : Language.empty.Functions x✝¹
x✝ : Fin x✝¹ → M
⊢ funMap f x✝ = funMap f x✝

case RelMap
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
a : Language.empty.Structure M
x✝¹ : ℕ
f : Language.empty.Relations x✝¹
x✝ : Fin x✝¹ → M
⊢ RelMap f x✝ ↔ RelMap f x✝
Module: Mathlib.ModelTheory.Algebra.Ring.Basic

Goal state before:
pp: case inl.add
α : Type u_1
⊢ Sum.inl ⟨2, add⟩ ∈
    { val := ↑[Sum.inl ⟨2, add⟩, Sum.inl ⟨2, mul⟩, Sum.inl ⟨1, neg⟩, Sum.inl ⟨0, zero⟩, Sum.inl ⟨0, one⟩],
      nodup := instFintypeSymbolsRing._proof_1 }

pp: case inl.mul
α : Type u_1
⊢ Sum.inl ⟨2, mul⟩ ∈
    { val := ↑[Sum.inl ⟨2, add⟩, Sum.inl ⟨2, mul⟩, Sum.inl ⟨1, neg⟩, Sum.inl ⟨0, zero⟩, Sum.inl ⟨0, one⟩],
      nodup := instFintypeSymbolsRing._proof_1 }

pp: case inl.neg
α : Type u_1
⊢ Sum.inl ⟨1, neg⟩ ∈
    { val := ↑[Sum.inl ⟨2, add⟩, Sum.inl ⟨2, mul⟩, Sum.inl ⟨1, neg⟩, Sum.inl ⟨0, zero⟩, Sum.inl ⟨0, one⟩],
      nodup := instFintypeSymbolsRing._proof_1 }

pp: case inl.zero
α : Type u_1
⊢ Sum.inl ⟨0, zero⟩ ∈
    { val := ↑[Sum.inl ⟨2, add⟩, Sum.inl ⟨2, mul⟩, Sum.inl ⟨1, neg⟩, Sum.inl ⟨0, zero⟩, Sum.inl ⟨0, one⟩],
      nodup := instFintypeSymbolsRing._proof_1 }

pp: case inl.one
α : Type u_1
⊢ Sum.inl ⟨0, one⟩ ∈
    { val := ↑[Sum.inl ⟨2, add⟩, Sum.inl ⟨2, mul⟩, Sum.inl ⟨1, neg⟩, Sum.inl ⟨0, zero⟩, Sum.inl ⟨0, one⟩],
      nodup := instFintypeSymbolsRing._proof_1 }

Tactic:
<;>

Goal state after:
case inl.add
α : Type u_1
⊢ Sum.inl ⟨2, add⟩ ∈
    { val := ↑[Sum.inl ⟨2, add⟩, Sum.inl ⟨2, mul⟩, Sum.inl ⟨1, neg⟩, Sum.inl ⟨0, zero⟩, Sum.inl ⟨0, one⟩],
      nodup := instFintypeSymbolsRing._proof_1 }

case inl.mul
α : Type u_1
⊢ Sum.inl ⟨2, mul⟩ ∈
    { val := ↑[Sum.inl ⟨2, add⟩, Sum.inl ⟨2, mul⟩, Sum.inl ⟨1, neg⟩, Sum.inl ⟨0, zero⟩, Sum.inl ⟨0, one⟩],
      nodup := instFintypeSymbolsRing._proof_1 }

case inl.neg
α : Type u_1
⊢ Sum.inl ⟨1, neg⟩ ∈
    { val := ↑[Sum.inl ⟨2, add⟩, Sum.inl ⟨2, mul⟩, Sum.inl ⟨1, neg⟩, Sum.inl ⟨0, zero⟩, Sum.inl ⟨0, one⟩],
      nodup := instFintypeSymbolsRing._proof_1 }

case inl.zero
α : Type u_1
⊢ Sum.inl ⟨0, zero⟩ ∈
    { val := ↑[Sum.inl ⟨2, add⟩, Sum.inl ⟨2, mul⟩, Sum.inl ⟨1, neg⟩, Sum.inl ⟨0, zero⟩, Sum.inl ⟨0, one⟩],
      nodup := instFintypeSymbolsRing._proof_1 }

case inl.one
α : Type u_1
⊢ Sum.inl ⟨0, one⟩ ∈
    { val := ↑[Sum.inl ⟨2, add⟩, Sum.inl ⟨2, mul⟩, Sum.inl ⟨1, neg⟩, Sum.inl ⟨0, zero⟩, Sum.inl ⟨0, one⟩],
      nodup := instFintypeSymbolsRing._proof_1 }
Module: Mathlib.ModelTheory.Algebra.Ring.Basic

Goal state before:
pp: case add
α : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : NonAssocRing R
inst✝² : NonAssocRing S
inst✝¹ : CompatibleRing R
inst✝ : CompatibleRing S
f : R ≃+* S
⊢ ∀ (x : Fin 2 → R), f.toFun (funMap add x) = funMap add (f.toFun ∘ x)

pp: case mul
α : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : NonAssocRing R
inst✝² : NonAssocRing S
inst✝¹ : CompatibleRing R
inst✝ : CompatibleRing S
f : R ≃+* S
⊢ ∀ (x : Fin 2 → R), f.toFun (funMap mul x) = funMap mul (f.toFun ∘ x)

pp: case neg
α : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : NonAssocRing R
inst✝² : NonAssocRing S
inst✝¹ : CompatibleRing R
inst✝ : CompatibleRing S
f : R ≃+* S
⊢ ∀ (x : Fin 1 → R), f.toFun (funMap neg x) = funMap neg (f.toFun ∘ x)

pp: case zero
α : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : NonAssocRing R
inst✝² : NonAssocRing S
inst✝¹ : CompatibleRing R
inst✝ : CompatibleRing S
f : R ≃+* S
⊢ ∀ (x : Fin 0 → R), f.toFun (funMap zero x) = funMap zero (f.toFun ∘ x)

pp: case one
α : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : NonAssocRing R
inst✝² : NonAssocRing S
inst✝¹ : CompatibleRing R
inst✝ : CompatibleRing S
f : R ≃+* S
⊢ ∀ (x : Fin 0 → R), f.toFun (funMap one x) = funMap one (f.toFun ∘ x)

Tactic:
<;>

Goal state after:
case add
α : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : NonAssocRing R
inst✝² : NonAssocRing S
inst✝¹ : CompatibleRing R
inst✝ : CompatibleRing S
f : R ≃+* S
⊢ ∀ (x : Fin 2 → R), f.toFun (funMap add x) = funMap add (f.toFun ∘ x)

case mul
α : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : NonAssocRing R
inst✝² : NonAssocRing S
inst✝¹ : CompatibleRing R
inst✝ : CompatibleRing S
f : R ≃+* S
⊢ ∀ (x : Fin 2 → R), f.toFun (funMap mul x) = funMap mul (f.toFun ∘ x)

case neg
α : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : NonAssocRing R
inst✝² : NonAssocRing S
inst✝¹ : CompatibleRing R
inst✝ : CompatibleRing S
f : R ≃+* S
⊢ ∀ (x : Fin 1 → R), f.toFun (funMap neg x) = funMap neg (f.toFun ∘ x)

case zero
α : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : NonAssocRing R
inst✝² : NonAssocRing S
inst✝¹ : CompatibleRing R
inst✝ : CompatibleRing S
f : R ≃+* S
⊢ ∀ (x : Fin 0 → R), f.toFun (funMap zero x) = funMap zero (f.toFun ∘ x)

case one
α : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : NonAssocRing R
inst✝² : NonAssocRing S
inst✝¹ : CompatibleRing R
inst✝ : CompatibleRing S
f : R ≃+* S
⊢ ∀ (x : Fin 0 → R), f.toFun (funMap one x) = funMap one (f.toFun ∘ x)
Module: Mathlib.ModelTheory.Syntax

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

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

Tactic:
<;>

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

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