mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Dynamics.Ergodic.Extreme

Goal state before:
pp: X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
c : ℝ≥0∞
hc : c ≠ ∞
h : μ ∈ extremePoints ℝ≥0∞ {ν | MeasurePreserving f ν ν ∧ ν univ = c}
hf : MeasurePreserving f μ μ
hc₀ : c ≠ 0
⊢ IsFiniteMeasure μ

Tactic:
constructor

Goal state after:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
c : ℝ≥0∞
hc : c ≠ ∞
h : μ ∈ extremePoints ℝ≥0∞ {ν | MeasurePreserving f ν ν ∧ ν univ = c}
hf : MeasurePreserving f μ μ
hc₀ : c ≠ 0
⊢ μ univ < ∞
Module: Mathlib.Dynamics.Ergodic.Extreme

Goal state before:
pp: X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
f : X → X
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμ : Ergodic f μ
hfν : MeasurePreserving f ν ν
hνμ : ν ≪ μ
⊢ ∃ c, ν = c • μ

Tactic:
have := hfν.rnDeriv_comp_aeEq hμ.toMeasurePreserving
  obtain ⟨c, hc⟩ := hμ.ae_eq_const_of_ae_eq_comp₀ (measurable_rnDeriv _ _).nullMeasurable this
  use c
  ext s hs
  calc
    ν s = ∫⁻ a in s, ν.rnDeriv μ a ∂μ := .symm <| setLIntegral_rnDeriv hνμ _
    _ = ∫⁻ _ in s, c ∂μ := lintegral_congr_ae <| hc.filter_mono <| ae_mono restrict_le_self
    _ = (c • μ) s := by simp

Goal state after:
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
ϕ : τ → α → β
s : Set α
m : τ → τ
f₁ f₂ : Filter τ
hf : Tendsto m f₁ f₂
u : Set τ
hu : u ∈ f₂
⊢ closure[inst✝] (image2 (fun t x ↦ ϕ (m t) x) (m ⁻¹' u) s) ⊆ closure[inst✝] (image2 ϕ u s)

Tactic:
rw [← image2_image_left]

Goal state after:
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
ϕ : τ → α → β
s : Set α
m : τ → τ
f₁ f₂ : Filter τ
hf : Tendsto m f₁ f₂
u : Set τ
hu : u ∈ f₂
⊢ closure[inst✝] (image2 ϕ (m '' m ⁻¹' u) s) ⊆ closure[inst✝] (image2 ϕ u s)
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
p : Pattern A G
g : G
x : G → A
⊢ x ∈ {x | p.mulOccursInAt x g} ↔ x ∈ cylinder (Finset.image (fun x ↦ g * x) p.support) (p.mulShift g)

Tactic:
constructor

Goal state after:
case mp
A : Type u_1
inst✝² : Inhabited A
G : Type u_2
inst✝¹ : Monoid G
inst✝ : IsLeftCancelMul G
p : Pattern A G
g : G
x : G → A
⊢ x ∈ {x | p.mulOccursInAt x g} → x ∈ cylinder (Finset.image (fun x ↦ g * x) p.support) (p.mulShift g)

case mpr
A : Type u_1
inst✝² : Inhabited A
G : Type u_2
inst✝¹ : Monoid G
inst✝ : IsLeftCancelMul G
p : Pattern A G
g : G
x : G → A
⊢ x ∈ cylinder (Finset.image (fun x ↦ g * x) p.support) (p.mulShift g) → x ∈ {x | p.mulOccursInAt x g}
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
y : β
⊢ (∀ i ∈ f, ∀ t ∈ 𝓝 y, (t ∩ image2 ϕ i s).Nonempty) ↔
    ∀ n ∈ 𝓝 y, ∀ {U : Set τ}, U ∈ f → ∃ x ∈ U, (s ∩ ϕ x ⁻¹' n).Nonempty

Tactic:
constructor

Goal state after:
case mp
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
y : β
⊢ (∀ i ∈ f, ∀ t ∈ 𝓝 y, (t ∩ image2 ϕ i s).Nonempty) →
    ∀ n ∈ 𝓝 y, ∀ {U : Set τ}, U ∈ f → ∃ x ∈ U, (s ∩ ϕ x ⁻¹' n).Nonempty

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
Module: Mathlib.Dynamics.SymbolicDynamics.Basic

Goal state before:
pp: A : Type u_1
inst✝⁴ : TopologicalSpace A
inst✝³ : Inhabited A
G : Type u_2
inst✝² : Monoid G
inst✝¹ : IsLeftCancelMul G
inst✝ : DiscreteTopology A
F : Set (Pattern A G)
⊢ {x | ∀ p ∈ F, ∀ (v : G), ¬p.mulOccursInAt x v} = ⋂ p ∈ F, ⋂ v, {x | ¬p.mulOccursInAt x v}

Tactic:
ext

Goal state after:
A : Type u_1
inst✝⁴ : TopologicalSpace A
inst✝³ : Inhabited A
G : Type u_2
inst✝² : Monoid G
inst✝¹ : IsLeftCancelMul G
inst✝ : DiscreteTopology A
F : Set (Pattern A G)
x✝ : G → A
⊢ x✝ ∈ {x | ∀ p ∈ F, ∀ (v : G), ¬p.mulOccursInAt x v} ↔ x✝ ∈ ⋂ p ∈ F, ⋂ v, {x | ¬p.mulOccursInAt x v}
Module: Mathlib.Dynamics.SymbolicDynamics.Basic

Goal state before:
pp: A : Type u_1
inst✝⁴ : TopologicalSpace A
inst✝³ : Inhabited A
G : Type u_2
inst✝² : Monoid G
inst✝¹ : IsLeftCancelMul G
inst✝ : DiscreteTopology A
F : Set (Pattern A G)
h_eq : {x | ∀ p ∈ F, ∀ (v : G), ¬p.mulOccursInAt x v} = ⋂ p ∈ F, ⋂ v, {x | ¬p.mulOccursInAt x v}
p : Pattern A G
hp : p ∈ F
⊢ IsClosed[Pi.topologicalSpace] (⋂ v, {x | ¬p.mulOccursInAt x v})

Tactic:
refine isClosed_iInter (fun v => ?_)

Goal state after:
A : Type u_1
inst✝⁴ : TopologicalSpace A
inst✝³ : Inhabited A
G : Type u_2
inst✝² : Monoid G
inst✝¹ : IsLeftCancelMul G
inst✝ : DiscreteTopology A
F : Set (Pattern A G)
h_eq : {x | ∀ p ∈ F, ∀ (v : G), ¬p.mulOccursInAt x v} = ⋂ p ∈ F, ⋂ v, {x | ¬p.mulOccursInAt x v}
p : Pattern A G
hp : p ∈ F
v : G
⊢ IsClosed[Pi.topologicalSpace] {x | ¬p.mulOccursInAt x v}
Module: Mathlib.Dynamics.SymbolicDynamics.Basic

Goal state before:
pp: A : Type u_1
inst✝⁴ : TopologicalSpace A
inst✝³ : Inhabited A
G : Type u_2
inst✝² : Monoid G
inst✝¹ : IsLeftCancelMul G
inst✝ : DiscreteTopology A
F : Set (Pattern A G)
h_eq : {x | ∀ p ∈ F, ∀ (v : G), ¬p.mulOccursInAt x v} = ⋂ p ∈ F, ⋂ v, {x | ¬p.mulOccursInAt x v}
p : Pattern A G
hp : p ∈ F
v : G
⊢ {x | ¬p.mulOccursInAt x v} = {x | p.mulOccursInAt x v}ᶜ

Tactic:
ext

Goal state after:
A : Type u_1
inst✝⁴ : TopologicalSpace A
inst✝³ : Inhabited A
G : Type u_2
inst✝² : Monoid G
inst✝¹ : IsLeftCancelMul G
inst✝ : DiscreteTopology A
F : Set (Pattern A G)
h_eq : {x | ∀ p ∈ F, ∀ (v : G), ¬p.mulOccursInAt x v} = ⋂ p ∈ F, ⋂ v, {x | ¬p.mulOccursInAt x v}
p : Pattern A G
hp : p ∈ F
v : G
x✝ : G → A
⊢ x✝ ∈ {x | ¬p.mulOccursInAt x v} ↔ x✝ ∈ {x | p.mulOccursInAt x v}ᶜ
Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage

Goal state before:
pp: X : Type u_1
T : X → X
U V : SetRel X X
m n : ℕ
x y : X
inst✝ : U.IsRefl
⊢ (dynEntourage T U n).IsRefl

Tactic:
simp only [dynEntourage, map_iterate]
  infer_instance

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

Goal state before:
pp: X : Type u_1
T : X → X
U V : SetRel X X
m n : ℕ
x y : X
inst✝ : U.IsSymm
⊢ (dynEntourage T U n).IsSymm

Tactic:
simp only [dynEntourage, map_iterate]
  infer_instance

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₁ s₂ : Set α
y : β
⊢ y ∈ ω f ϕ (s₁ ∪ s₂) ↔ y ∈ ω f ϕ s₁ ∪ ω f ϕ s₂

Tactic:
constructor

Goal state after:
case mp
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s₁ s₂ : Set α
y : β
⊢ y ∈ ω f ϕ (s₁ ∪ s₂) → y ∈ ω f ϕ s₁ ∪ ω f ϕ s₂

case mpr
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s₁ s₂ : Set α
y : β
⊢ y ∈ ω f ϕ s₁ ∪ ω f ϕ s₂ → y ∈ ω f ϕ (s₁ ∪ s₂)
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: case h
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : f.NeBot
c : Set β
hc₁ : IsCompact c
hs : s.Nonempty
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst✝¹] (image2 ϕ v s) ⊆ c
u₁ : Set τ
hu₁ : u₁ ∈ f.sets
u₂ : Set τ
hu₂ : u₂ ∈ f.sets
⊢ (fun x1 x2 ↦ x1 ⊇ x2) ((fun i ↦ closure[inst✝¹] (image2 ϕ (↑i ∩ v) s)) ⟨u₁, hu₁⟩)
      ((fun i ↦ closure[inst✝¹] (image2 ϕ (↑i ∩ v) s)) ⟨u₁ ∩ u₂, ⋯⟩) ∧
    (fun x1 x2 ↦ x1 ⊇ x2) ((fun i ↦ closure[inst✝¹] (image2 ϕ (↑i ∩ v) s)) ⟨u₂, hu₂⟩)
      ((fun i ↦ closure[inst✝¹] (image2 ϕ (↑i ∩ v) s)) ⟨u₁ ∩ u₂, ⋯⟩)

Tactic:
constructor

Goal state after:
case h.left
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : f.NeBot
c : Set β
hc₁ : IsCompact c
hs : s.Nonempty
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst✝¹] (image2 ϕ v s) ⊆ c
u₁ : Set τ
hu₁ : u₁ ∈ f.sets
u₂ : Set τ
hu₂ : u₂ ∈ f.sets
⊢ (fun x1 x2 ↦ x1 ⊇ x2) ((fun i ↦ closure[inst✝¹] (image2 ϕ (↑i ∩ v) s)) ⟨u₁, hu₁⟩)
    ((fun i ↦ closure[inst✝¹] (image2 ϕ (↑i ∩ v) s)) ⟨u₁ ∩ u₂, ⋯⟩)

case h.right
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : f.NeBot
c : Set β
hc₁ : IsCompact c
hs : s.Nonempty
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst✝¹] (image2 ϕ v s) ⊆ c
u₁ : Set τ
hu₁ : u₁ ∈ f.sets
u₂ : Set τ
hu₂ : u₂ ∈ f.sets
⊢ (fun x1 x2 ↦ x1 ⊇ x2) ((fun i ↦ closure[inst✝¹] (image2 ϕ (↑i ∩ v) s)) ⟨u₂, hu₂⟩)
    ((fun i ↦ closure[inst✝¹] (image2 ϕ (↑i ∩ v) s)) ⟨u₁ ∩ u₂, ⋯⟩)
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: case inr.inr.refine_1
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
dyncover : (Fin n → ↥s) → X
h_dyncover :
  ∀ (t : Fin n → ↥s),
    ⋂ k, T^[m * ↑k] ⁻¹' ball (↑(t k)) (dynEntourage T U m) ⊆ ball (dyncover t) (dynEntourage T (U ○ U) (m * n))
sn : Set X := range dyncover
⊢ IsDynCoverOf T F (U ○ U) (m * n) ↑sn.toFinset

Tactic:
rw [Finset.coe_nonempty] at s_nemp
    have _ : Nonempty s := Finset.Nonempty.coe_sort s_nemp
    intro y y_F
    have key : ∀ k : Fin n, ∃ z : s, y ∈ T^[m * k] ⁻¹' ball z (dynEntourage T U m) := by
      intro k
      have := h (MapsTo.iterate F_inv (m * k) y_F)
      simp only [Finset.mem_coe] at this
      obtain ⟨z, z_s, hz⟩ := this
      exact ⟨⟨z, z_s⟩, (dynEntourage T U m).symm hz⟩
    choose! t ht using key
    simp only [toFinset_range, Finset.coe_image, Finset.coe_univ, image_univ, mem_range,
      exists_exists_eq_and, sn]
    refine ⟨t, (dynEntourage T (U ○ U) (m * n)).symm <| h_dyncover t <| by simpa using ht⟩

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

Goal state before:
pp: case inr
X : Type u_1
Y : Type u_2
F : Set X
V : SetRel Y Y
S : X → X
T : Y → Y
φ : X → Y
n : ℕ
h : Semiconj φ S T
inst✝ : V.IsSymm
t : Finset Y
h' : IsDynCoverOf T (φ '' F) V n ↑t
h✝¹ : Nonempty X
s : Finset Y
s_cover : IsDynCoverOf T (φ '' F) V n ↑s
s_card : s.card ≤ t.card
s_inter : ∀ x ∈ s, (ball x (dynEntourage T V n) ∩ φ '' F).Nonempty
g : Y → Y
g_rel : ∀ x ∈ s, g x ∈ ball x (dynEntourage T V n)
g_mem : ∀ x ∈ s, g x ∈ φ '' F
f : Y → X
h✝ : ∀ y ∈ φ '' F, f y ∈ F
φ_f : ∀ y ∈ φ '' F, φ (f y) = y
x : X
hx : x ∈ F
y : Y
hy : y ∈ ↑s
hxy : (φ x, y) ∈ dynEntourage T V n
⊢ ∃ a ∈ s, (φ x, φ (f (g a))) ∈ dynEntourage T (V ○ V) n

Tactic:
refine ⟨y, hy, dynEntourage_comp_subset _ _ _ _ ⟨_, hxy, ?_⟩⟩

Goal state after:
case inr
X : Type u_1
Y : Type u_2
F : Set X
V : SetRel Y Y
S : X → X
T : Y → Y
φ : X → Y
n : ℕ
h : Semiconj φ S T
inst✝ : V.IsSymm
t : Finset Y
h' : IsDynCoverOf T (φ '' F) V n ↑t
h✝¹ : Nonempty X
s : Finset Y
s_cover : IsDynCoverOf T (φ '' F) V n ↑s
s_card : s.card ≤ t.card
s_inter : ∀ x ∈ s, (ball x (dynEntourage T V n) ∩ φ '' F).Nonempty
g : Y → Y
g_rel : ∀ x ∈ s, g x ∈ ball x (dynEntourage T V n)
g_mem : ∀ x ∈ s, g x ∈ φ '' F
f : Y → X
h✝ : ∀ y ∈ φ '' F, f y ∈ F
φ_f : ∀ y ∈ φ '' F, φ (f y) = y
x : X
hx : x ∈ F
y : Y
hy : y ∈ ↑s
hxy : (φ x, y) ∈ dynEntourage T V n
⊢ (y, φ (f (g y))) ∈ dynEntourage T V n
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

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

Tactic:
constructor

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

case right
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
⊢ ν.rnDeriv μ =ᵐ[μ] (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ
Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj

Goal state before:
pp: X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : SetRel Y Y
n : ℕ
⊢ coverMincard T (φ '' F) V n ≤ coverMincard S F (map φ φ ⁻¹' V) n

Tactic:
classical
  rcases eq_top_or_lt_top (coverMincard S F ((map φ φ) ⁻¹' V) n) with h' | h'
  · exact h' ▸ le_top
  obtain ⟨s, s_cover, s_card⟩ := (coverMincard_finite_iff S F ((map φ φ) ⁻¹' V) n).1 h'
  rw [← s_card]
  have := s_cover.image h
  rw [← s.coe_image] at this
  exact this.coverMincard_le_card.trans (WithTop.coe_le_coe.2 s.card_image_le)

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
p : α → Prop
h : ∀ᵐ (a : α) ∂μ, p a
⊢ (∀ᵐ (x : α) ∂ν.singularPart μ, μ.rnDeriv (ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)) x ≠ 0 → p x) ∧
    ∀ᵐ (x : α) ∂μ.withDensity (ν.rnDeriv μ), μ.rnDeriv (ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)) x ≠ 0 → p x

Tactic:
constructor

Goal state after:
case left
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
p : α → Prop
h : ∀ᵐ (a : α) ∂μ, p a
⊢ ∀ᵐ (x : α) ∂ν.singularPart μ, μ.rnDeriv (ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)) x ≠ 0 → p x

case right
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
p : α → Prop
h : ∀ᵐ (a : α) ∂μ, p a
⊢ ∀ᵐ (x : α) ∂μ.withDensity (ν.rnDeriv μ), μ.rnDeriv (ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)) x ≠ 0 → p x
Module: Mathlib.FieldTheory.IsAlgClosed.Classification

Goal state before:
pp: case refine_1
R : Type u_1
L : Type u_2
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : Field L
inst✝² : Algebra R L
ι : Type u_4
v : ι → K
κ : Type u_5
w : κ → L
hv✝ : AlgebraicIndependent R v
hw✝ : AlgebraicIndependent R w
inst✝¹ : IsAlgClosed K
inst✝ : IsAlgClosed L
e : ι ≃ κ
hv : IsTranscendenceBasis R v
hw : IsTranscendenceBasis R w
this✝ : IsAlgClosure (↥(Algebra.adjoin R (Set.range v))) K := isAlgClosure_of_transcendence_basis v hv
this : IsAlgClosure (↥(Algebra.adjoin R (Set.range w))) L := isAlgClosure_of_transcendence_basis w hw
⊢ (MvPolynomial.rename ⇑e).comp (MvPolynomial.rename ⇑e.symm) = AlgHom.id R (MvPolynomial κ R)

Tactic:
ext

Goal state after:
case refine_1
R : Type u_1
L : Type u_2
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : Field L
inst✝² : Algebra R L
ι : Type u_4
v : ι → K
κ : Type u_5
w : κ → L
hv✝ : AlgebraicIndependent R v
hw✝ : AlgebraicIndependent R w
inst✝¹ : IsAlgClosed K
inst✝ : IsAlgClosed L
e : ι ≃ κ
hv : IsTranscendenceBasis R v
hw : IsTranscendenceBasis R w
this✝ : IsAlgClosure (↥(Algebra.adjoin R (Set.range v))) K := isAlgClosure_of_transcendence_basis v hv
this : IsAlgClosure (↥(Algebra.adjoin R (Set.range w))) L := isAlgClosure_of_transcendence_basis w hw
i✝ : κ
m✝ : κ →₀ ℕ
⊢ MvPolynomial.coeff m✝ (((MvPolynomial.rename ⇑e).comp (MvPolynomial.rename ⇑e.symm)) (MvPolynomial.X i✝)) =
    MvPolynomial.coeff m✝ ((AlgHom.id R (MvPolynomial κ R)) (MvPolynomial.X i✝))
Module: Mathlib.FieldTheory.IsAlgClosed.Classification

Goal state before:
pp: case refine_2
R : Type u_1
L : Type u_2
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : Field L
inst✝² : Algebra R L
ι : Type u_4
v : ι → K
κ : Type u_5
w : κ → L
hv✝ : AlgebraicIndependent R v
hw✝ : AlgebraicIndependent R w
inst✝¹ : IsAlgClosed K
inst✝ : IsAlgClosed L
e : ι ≃ κ
hv : IsTranscendenceBasis R v
hw : IsTranscendenceBasis R w
this✝ : IsAlgClosure (↥(Algebra.adjoin R (Set.range v))) K := isAlgClosure_of_transcendence_basis v hv
this : IsAlgClosure (↥(Algebra.adjoin R (Set.range w))) L := isAlgClosure_of_transcendence_basis w hw
⊢ (MvPolynomial.rename ⇑e.symm).comp (MvPolynomial.rename ⇑e) = AlgHom.id R (MvPolynomial ι R)

Tactic:
ext

Goal state after:
case refine_2
R : Type u_1
L : Type u_2
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : Field L
inst✝² : Algebra R L
ι : Type u_4
v : ι → K
κ : Type u_5
w : κ → L
hv✝ : AlgebraicIndependent R v
hw✝ : AlgebraicIndependent R w
inst✝¹ : IsAlgClosed K
inst✝ : IsAlgClosed L
e : ι ≃ κ
hv : IsTranscendenceBasis R v
hw : IsTranscendenceBasis R w
this✝ : IsAlgClosure (↥(Algebra.adjoin R (Set.range v))) K := isAlgClosure_of_transcendence_basis v hv
this : IsAlgClosure (↥(Algebra.adjoin R (Set.range w))) L := isAlgClosure_of_transcendence_basis w hw
i✝ : ι
m✝ : ι →₀ ℕ
⊢ MvPolynomial.coeff m✝ (((MvPolynomial.rename ⇑e.symm).comp (MvPolynomial.rename ⇑e)) (MvPolynomial.X i✝)) =
    MvPolynomial.coeff m✝ ((AlgHom.id R (MvPolynomial ι R)) (MvPolynomial.X i✝))
Module: Mathlib.FieldTheory.IsAlgClosed.Classification

Goal state before:
pp: R : Type u
K : Type v
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsAlgClosed K
ι : Type w
v : ι → K
hv : IsTranscendenceBasis R v
⊢ Cardinal.lift.{max (max u v) w, max u w} (max #(MvPolynomial ι R) ℵ₀) =
    Cardinal.lift.{v, max u w} (max #(MvPolynomial ι R) ℵ₀)

Tactic:
lift_umax.{max u w, v}

Goal state after:
R : Type u
K : Type v
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsAlgClosed K
ι : Type w
v : ι → K
hv : IsTranscendenceBasis R v
⊢ Cardinal.lift.{v, max u w} (max #(MvPolynomial ι R) ℵ₀) = Cardinal.lift.{v, max u w} (max #(MvPolynomial ι R) ℵ₀)
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f f' : M ↪[L] N
h : (fun x ↦ x.toHom) f = (fun x ↦ x.toHom) f'
⊢ f = f'

Tactic:
ext

Goal state after:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f f' : M ↪[L] N
h : (fun x ↦ x.toHom) f = (fun x ↦ x.toHom) f'
x✝ : M
⊢ f x✝ = f' x✝
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝² : L.Structure M
inst✝¹ : L.Structure N
inst✝ : L.IsAlgebraic
f : M →[L] N
hf : Function.Injective ⇑f
⊢ (ofInjective hf).toHom = f

Tactic:
ext

Goal state after:
L : Language
M : Type w
N : Type w'
inst✝² : L.Structure M
inst✝¹ : L.Structure N
inst✝ : L.IsAlgebraic
f : M →[L] N
hf : Function.Injective ⇑f
x✝ : M
⊢ (ofInjective hf).toHom x✝ = f x✝
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: L : Language
L' : Language
M : Type w
inst✝ : L.Structure M
L'' : Language
e'✝ : L' ≃ᴸ L''
e✝ e : L ≃ᴸ L'
e' : L' ≃ᴸ L''
⊢ e'.toLHom.comp ((e.toLHom.comp e.invLHom).comp e'.invLHom) = LHom.id L''

Tactic:
e.right_inv,

Goal state after:
L : Language
L' : Language
M : Type w
inst✝ : L.Structure M
L'' : Language
e'✝ : L' ≃ᴸ L''
e✝ e : L ≃ᴸ L'
e' : L' ≃ᴸ L''
⊢ e'.toLHom.comp ((LHom.id L').comp e'.invLHom) = LHom.id L''
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: L : Language
α : Type w'
β : Type u_1
f : α → β
⊢ (L.lhomWithConstantsMap f).comp LHom.sumInl = L.lhomWithConstants β

Tactic:
ext

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: L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃[L] N
⊢ f.comp f.symm = refl L N

Tactic:
ext

Goal state after:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃[L] N
x✝ : N
⊢ (f.comp f.symm) x✝ = (refl L N) x✝
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃[L] N
⊢ f.symm.comp f = refl L M

Tactic:
ext

Goal state after:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃[L] N
x✝ : M
⊢ (f.symm.comp f) x✝ = (refl L M) x✝
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case imp
L : Language
α : Type u'
n n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 : ∀ (h : n✝ ≤ n✝), castLE h f₁✝ = f₁✝
ih2 : ∀ (h : n✝ ≤ n✝), castLE h f₂✝ = f₂✝
h : n✝ ≤ n✝
⊢ castLE h (f₁✝.imp f₂✝) = f₁✝.imp f₂✝

Tactic:
| imp _ _ ih1 ih2 =>

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case imp
L : Language
α : Type u'
k n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 : ∀ {m n : ℕ} (km : n✝ ≤ m) (mn : m ≤ n), castLE mn (castLE km f₁✝) = castLE ⋯ f₁✝
ih2 : ∀ {m n : ℕ} (km : n✝ ≤ m) (mn : m ≤ n), castLE mn (castLE km f₂✝) = castLE ⋯ f₂✝
⊢ ∀ {m n : ℕ} (km : n✝ ≤ m) (mn : m ≤ n), castLE mn (castLE km (f₁✝.imp f₂✝)) = castLE ⋯ (f₁✝.imp f₂✝)

Tactic:
| imp _ _ ih1 ih2 =>

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case imp
L : Language
L' : Language
α : Type u'
β : Type v'
γ : Type u_1
L'' : Language
ft : (n : ℕ) → L.Term (α ⊕ Fin n) → L'.Term (β ⊕ Fin n)
fr : (n : ℕ) → L.Relations n → L'.Relations n
ft' : (n : ℕ) → L'.Term (β ⊕ Fin n) → L''.Term (γ ⊕ Fin n)
fr' : (n : ℕ) → L'.Relations n → L''.Relations n
n n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 :
  mapTermRel ft' fr' (fun x ↦ id) (mapTermRel ft fr (fun x ↦ id) f₁✝) =
    mapTermRel (fun x ↦ ft' x ∘ ft x) (fun x ↦ fr' x ∘ fr x) (fun x ↦ id) f₁✝
ih2 :
  mapTermRel ft' fr' (fun x ↦ id) (mapTermRel ft fr (fun x ↦ id) f₂✝) =
    mapTermRel (fun x ↦ ft' x ∘ ft x) (fun x ↦ fr' x ∘ fr x) (fun x ↦ id) f₂✝
⊢ mapTermRel ft' fr' (fun x ↦ id) (mapTermRel ft fr (fun x ↦ id) (f₁✝.imp f₂✝)) =
    mapTermRel (fun x ↦ ft' x ∘ ft x) (fun x ↦ fr' x ∘ fr x) (fun x ↦ id) (f₁✝.imp f₂✝)

Tactic:
| imp _ _ ih1 ih2 =>

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case imp
L : Language
α : Type u'
n n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 : mapTermRel (fun x ↦ id) (fun x ↦ id) (fun x ↦ id) f₁✝ = f₁✝
ih2 : mapTermRel (fun x ↦ id) (fun x ↦ id) (fun x ↦ id) f₂✝ = f₂✝
⊢ mapTermRel (fun x ↦ id) (fun x ↦ id) (fun x ↦ id) (f₁✝.imp f₂✝) = f₁✝.imp f₂✝

Tactic:
| imp _ _ ih1 ih2 =>

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: α : Type u'
n k : ℕ
x : α ⊕ Fin k
⊢ relabelAux Sum.inl k x = Sum.map id (natAdd n) x

Tactic:
cases x <;> · simp [relabelAux]

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case add
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x y z : E
hy : y ∈ solvableByRad F E
hz : z ∈ solvableByRad F E
hy' : Group.IsSolvable (minpoly F y).Gal
hz' : Group.IsSolvable (minpoly F z).Gal
⊢ Group.IsSolvable (minpoly F (y + z)).Gal

Tactic:
| add y z hy hz hy' hz' =>

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case imp
L : Language
α : Type u'
n n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 : mapTermRel (fun x t ↦ Term.relabel (Sum.map id (natAdd 0)) t) (fun x ↦ id) (fun x ↦ castLE ⋯) f₁✝ = castLE ⋯ f₁✝
ih2 : mapTermRel (fun x t ↦ Term.relabel (Sum.map id (natAdd 0)) t) (fun x ↦ id) (fun x ↦ castLE ⋯) f₂✝ = castLE ⋯ f₂✝
⊢ mapTermRel (fun x t ↦ Term.relabel (Sum.map id (natAdd 0)) t) (fun x ↦ id) (fun x ↦ castLE ⋯) (f₁✝.imp f₂✝) =
    castLE ⋯ (f₁✝.imp f₂✝)

Tactic:
| imp _ _ ih1 ih2 =>

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case imp
L : Language
α : Type u'
n n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 : (LHom.id L).onBoundedFormula f₁✝ = id f₁✝
ih2 : (LHom.id L).onBoundedFormula f₂✝ = id f₂✝
⊢ (LHom.id L).onBoundedFormula (f₁✝.imp f₂✝) = id (f₁✝.imp f₂✝)

Tactic:
| imp _ _ ih1 ih2 =>

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case imp
L : Language
L' : Language
α : Type u'
n : ℕ
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 : (φ.comp ψ).onBoundedFormula f₁✝ = (φ.onBoundedFormula ∘ ψ.onBoundedFormula) f₁✝
ih2 : (φ.comp ψ).onBoundedFormula f₂✝ = (φ.onBoundedFormula ∘ ψ.onBoundedFormula) f₂✝
⊢ (φ.comp ψ).onBoundedFormula (f₁✝.imp f₂✝) = (φ.onBoundedFormula ∘ ψ.onBoundedFormula) (f₁✝.imp f₂✝)

Tactic:
| imp _ _ ih1 ih2 =>

Goal state after: