mathlib-initiative/mathlib-tactics huggingface dataset:
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
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✝))

Tactic:
;

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.ModelTheory.Basic

Goal state before:
pp: case mk
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
g : M →[L] N
toFun✝ : M → N
map_fun'✝ : ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toFun✝ (funMap f x) = funMap f (toFun✝ ∘ x)
map_rel'✝ : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r x → RelMap r (toFun✝ ∘ x)
h : { toFun := toFun✝, map_fun' := map_fun'✝, map_rel' := map_rel'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, map_fun' := map_fun'✝, map_rel' := map_rel'✝ } = g

Tactic:
;

Goal state after:
case mk
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
g : M →[L] N
toFun✝ : M → N
map_fun'✝ : ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toFun✝ (funMap f x) = funMap f (toFun✝ ∘ x)
map_rel'✝ : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r x → RelMap r (toFun✝ ∘ x)
h : { toFun := toFun✝, map_fun' := map_fun'✝, map_rel' := map_rel'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, map_fun' := map_fun'✝, map_rel' := map_rel'✝ } = g
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: case mk.mk
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
toFun✝¹ : M → N
map_fun'✝¹ : ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toFun✝¹ (funMap f x) = funMap f (toFun✝¹ ∘ x)
map_rel'✝¹ : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r x → RelMap r (toFun✝¹ ∘ x)
toFun✝ : M → N
map_fun'✝ : ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toFun✝ (funMap f x) = funMap f (toFun✝ ∘ x)
map_rel'✝ : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r x → RelMap r (toFun✝ ∘ x)
h :
  { toFun := toFun✝¹, map_fun' := map_fun'✝¹, map_rel' := map_rel'✝¹ }.toFun =
    { toFun := toFun✝, map_fun' := map_fun'✝, map_rel' := map_rel'✝ }.toFun
⊢ { toFun := toFun✝¹, map_fun' := map_fun'✝¹, map_rel' := map_rel'✝¹ } =
    { toFun := toFun✝, map_fun' := map_fun'✝, map_rel' := map_rel'✝ }

Tactic:
;

Goal state after:
case mk.mk
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
toFun✝¹ : M → N
map_fun'✝¹ : ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toFun✝¹ (funMap f x) = funMap f (toFun✝¹ ∘ x)
map_rel'✝¹ : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r x → RelMap r (toFun✝¹ ∘ x)
toFun✝ : M → N
map_fun'✝ : ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toFun✝ (funMap f x) = funMap f (toFun✝ ∘ x)
map_rel'✝ : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r x → RelMap r (toFun✝ ∘ x)
h :
  { toFun := toFun✝¹, map_fun' := map_fun'✝¹, map_rel' := map_rel'✝¹ }.toFun =
    { toFun := toFun✝, map_fun' := map_fun'✝, map_rel' := map_rel'✝ }.toFun
⊢ { toFun := toFun✝¹, map_fun' := map_fun'✝¹, map_rel' := map_rel'✝¹ } =
    { toFun := toFun✝, map_fun' := map_fun'✝, map_rel' := map_rel'✝ }
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: case mk.mk.refl
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
toFun✝ : M → N
map_fun'✝¹ : ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toFun✝ (funMap f x) = funMap f (toFun✝ ∘ x)
map_rel'✝¹ : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r x → RelMap r (toFun✝ ∘ x)
map_fun'✝ : ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toFun✝ (funMap f x) = funMap f (toFun✝ ∘ x)
map_rel'✝ : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r x → RelMap r (toFun✝ ∘ x)
⊢ { toFun := toFun✝, map_fun' := map_fun'✝¹, map_rel' := map_rel'✝¹ } =
    { toFun := toFun✝, map_fun' := map_fun'✝, map_rel' := map_rel'✝ }

Tactic:
;

Goal state after:
case mk.mk.refl
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
toFun✝ : M → N
map_fun'✝¹ : ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toFun✝ (funMap f x) = funMap f (toFun✝ ∘ x)
map_rel'✝¹ : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r x → RelMap r (toFun✝ ∘ x)
map_fun'✝ : ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toFun✝ (funMap f x) = funMap f (toFun✝ ∘ x)
map_rel'✝ : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r x → RelMap r (toFun✝ ∘ x)
⊢ { toFun := toFun✝, map_fun' := map_fun'✝¹, map_rel' := map_rel'✝¹ } =
    { toFun := toFun✝, map_fun' := map_fun'✝, map_rel' := map_rel'✝ }
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : L.Structure M
inst✝² : L.Structure N
P : Type u_1
inst✝¹ : L.Structure P
Q : Type u_2
inst✝ : L.Structure Q
hnp : N →[L] P
hmn : M →[L] N
n✝ : ℕ
x✝¹ : L.Functions n✝
x✝ : Fin n✝ → M
⊢ funMap x✝¹ (⇑hnp ∘ ⇑hmn ∘ x✝) = funMap x✝¹ ((⇑hnp ∘ ⇑hmn) ∘ x✝)

Tactic:
;

Goal state after:
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : L.Structure M
inst✝² : L.Structure N
P : Type u_1
inst✝¹ : L.Structure P
Q : Type u_2
inst✝ : L.Structure Q
hnp : N →[L] P
hmn : M →[L] N
n✝ : ℕ
x✝¹ : L.Functions n✝
x✝ : Fin n✝ → M
⊢ funMap x✝¹ (⇑hnp ∘ ⇑hmn ∘ x✝) = funMap x✝¹ ((⇑hnp ∘ ⇑hmn) ∘ x✝)
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: case refine_2
L : Language
L' : Language
ϕ : L →ᴸ L'
inst✝³ : (n : ℕ) → (f : L'.Functions n) → Decidable (f ∈ Set.range fun f ↦ ϕ.onFunction f)
inst✝² : (n : ℕ) → (r : L'.Relations n) → Decidable (r ∈ Set.range fun r ↦ ϕ.onRelation r)
h : ϕ.Injective
M : Type u_1
inst✝¹ : Inhabited M
inst✝ : L.Structure M
this : L'.Structure M := ϕ.defaultExpansion M
n : ℕ
r : L.Relations n
xs : Fin n → M
hr : ϕ.onRelation r ∈ Set.range fun r ↦ ϕ.onRelation r
⊢ RelMap (ϕ.onRelation r) xs = RelMap r xs

Tactic:
refine (dif_pos hr).trans ?_

Goal state after:
case refine_2
L : Language
L' : Language
ϕ : L →ᴸ L'
inst✝³ : (n : ℕ) → (f : L'.Functions n) → Decidable (f ∈ Set.range fun f ↦ ϕ.onFunction f)
inst✝² : (n : ℕ) → (r : L'.Relations n) → Decidable (r ∈ Set.range fun r ↦ ϕ.onRelation r)
h : ϕ.Injective
M : Type u_1
inst✝¹ : Inhabited M
inst✝ : L.Structure M
this : L'.Structure M := ϕ.defaultExpansion M
n : ℕ
r : L.Relations n
xs : Fin n → M
hr : ϕ.onRelation r ∈ Set.range fun r ↦ ϕ.onRelation r
⊢ RelMap (Exists.choose hr) xs = RelMap r xs
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
x✝ : M
⊢ (ofInjective hf).toHom x✝ = f x✝

Tactic:
;

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.Basic

Goal state before:
pp: L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : L.Structure M
inst✝² : L.Structure N
P : Type u_1
inst✝¹ : L.Structure P
Q : Type u_2
inst✝ : L.Structure Q
hnp : N ↪[L] P
hmn : M ↪[L] N
n✝ : ℕ
f✝ : L.Functions n✝
x✝ : Fin n✝ → M
⊢ (⇑hnp ∘ ⇑hmn) (funMap f✝ x✝) = funMap f✝ ((⇑hnp ∘ ⇑hmn) ∘ x✝)

Tactic:
;

Goal state after:
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : L.Structure M
inst✝² : L.Structure N
P : Type u_1
inst✝¹ : L.Structure P
Q : Type u_2
inst✝ : L.Structure Q
hnp : N ↪[L] P
hmn : M ↪[L] N
n✝ : ℕ
f✝ : L.Functions n✝
x✝ : Fin n✝ → M
⊢ (⇑hnp ∘ ⇑hmn) (funMap f✝ x✝) = funMap f✝ ((⇑hnp ∘ ⇑hmn) ∘ x✝)
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : L.Structure M
inst✝² : L.Structure N
P : Type u_1
inst✝¹ : L.Structure P
Q : Type u_2
inst✝ : L.Structure Q
hnp : N ↪[L] P
hmn : M ↪[L] N
n✝ : ℕ
f✝ : L.Functions n✝
x✝ : Fin n✝ → M
⊢ funMap f✝ (⇑hnp ∘ ⇑hmn ∘ x✝) = funMap f✝ ((⇑hnp ∘ ⇑hmn) ∘ x✝)

Tactic:
;

Goal state after:
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : L.Structure M
inst✝² : L.Structure N
P : Type u_1
inst✝¹ : L.Structure P
Q : Type u_2
inst✝ : L.Structure Q
hnp : N ↪[L] P
hmn : M ↪[L] N
n✝ : ℕ
f✝ : L.Functions n✝
x✝ : Fin n✝ → M
⊢ funMap f✝ (⇑hnp ∘ ⇑hmn ∘ x✝) = funMap f✝ ((⇑hnp ∘ ⇑hmn) ∘ x✝)
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : L.Structure M
inst✝² : L.Structure N
P : Type u_1
inst✝¹ : L.Structure P
Q : Type u_2
inst✝ : L.Structure Q
hnp : N ↪[L] P
hmn : M ↪[L] N
n✝ : ℕ
r✝ : L.Relations n✝
x✝ : Fin n✝ → M
⊢ RelMap r✝ ((⇑hnp ∘ ⇑hmn) ∘ x✝) ↔ RelMap r✝ x✝

Tactic:
;

Goal state after:
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : L.Structure M
inst✝² : L.Structure N
P : Type u_1
inst✝¹ : L.Structure P
Q : Type u_2
inst✝ : L.Structure Q
hnp : N ↪[L] P
hmn : M ↪[L] N
n✝ : ℕ
r✝ : L.Relations n✝
x✝ : Fin n✝ → M
⊢ RelMap r✝ ((⇑hnp ∘ ⇑hmn) ∘ x✝) ↔ RelMap r✝ 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
P : Type u_1
inst✝ : L.Structure P
h : N ↪[L] P
f g : M ↪[L] N
hfg : h.comp f = h.comp g
x : M
⊢ f x = g x

Tactic:
;

Goal state after:
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 : N ↪[L] P
f g : M ↪[L] N
hfg : h.comp f = h.comp g
x : M
⊢ f x = g 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
P : Type u_1
inst✝ : L.Structure P
h : N ↪[L] P
f g : M →[L] N
hfg : h.toHom.comp f = h.toHom.comp g
x : M
⊢ f x = g x

Tactic:
;

Goal state after:
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 : N ↪[L] P
f g : M →[L] N
hfg : h.toHom.comp f = h.toHom.comp g
x : M
⊢ f x = g 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
a₁✝ a₂✝ : M ≃[L] N
h : a₁✝.toEmbedding = a₂✝.toEmbedding
⊢ a₁✝ = a₂✝

Tactic:
;

Goal state after:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
a₁✝ a₂✝ : M ≃[L] N
h : a₁✝.toEmbedding = a₂✝.toEmbedding
⊢ a₁✝ = a₂✝
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
a₁✝ a₂✝ : M ≃[L] N
h : a₁✝.toEmbedding = a₂✝.toEmbedding
⊢ ⇑a₁✝ = ⇑a₂✝

Tactic:
;

Goal state after:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
a₁✝ a₂✝ : M ≃[L] N
h : a₁✝.toEmbedding = a₂✝.toEmbedding
⊢ ⇑a₁✝ = ⇑a₂✝
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
x : M
⊢ (refl L M) x = x

Tactic:
simp [refl]

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
x : M
⊢ { toEquiv := _root_.Equiv.refl M, map_fun' := ⋯, map_rel' := ⋯ } x = x
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
x : M
⊢ { toEquiv := _root_.Equiv.refl M, map_fun' := ⋯, map_rel' := ⋯ } x = x

Tactic:
;

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
x : M
⊢ { toEquiv := _root_.Equiv.refl M, map_fun' := ⋯, map_rel' := ⋯ } x = x
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : L.Structure M
inst✝² : L.Structure N
P : Type u_1
inst✝¹ : L.Structure P
Q : Type u_2
inst✝ : L.Structure Q
hnp : N ≃[L] P
hmn : M ≃[L] N
n✝ : ℕ
f✝ : L.Functions n✝
x✝ : Fin n✝ → M
⊢ (⇑hnp ∘ ⇑hmn) (funMap f✝ x✝) = funMap f✝ ((⇑hnp ∘ ⇑hmn) ∘ x✝)

Tactic:
;

Goal state after:
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : L.Structure M
inst✝² : L.Structure N
P : Type u_1
inst✝¹ : L.Structure P
Q : Type u_2
inst✝ : L.Structure Q
hnp : N ≃[L] P
hmn : M ≃[L] N
n✝ : ℕ
f✝ : L.Functions n✝
x✝ : Fin n✝ → M
⊢ (⇑hnp ∘ ⇑hmn) (funMap f✝ x✝) = funMap f✝ ((⇑hnp ∘ ⇑hmn) ∘ x✝)
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : L.Structure M
inst✝² : L.Structure N
P : Type u_1
inst✝¹ : L.Structure P
Q : Type u_2
inst✝ : L.Structure Q
hnp : N ≃[L] P
hmn : M ≃[L] N
n✝ : ℕ
f✝ : L.Functions n✝
x✝ : Fin n✝ → M
⊢ funMap f✝ (⇑hnp ∘ ⇑hmn ∘ x✝) = funMap f✝ ((⇑hnp ∘ ⇑hmn) ∘ x✝)

Tactic:
;

Goal state after:
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : L.Structure M
inst✝² : L.Structure N
P : Type u_1
inst✝¹ : L.Structure P
Q : Type u_2
inst✝ : L.Structure Q
hnp : N ≃[L] P
hmn : M ≃[L] N
n✝ : ℕ
f✝ : L.Functions n✝
x✝ : Fin n✝ → M
⊢ funMap f✝ (⇑hnp ∘ ⇑hmn ∘ x✝) = funMap f✝ ((⇑hnp ∘ ⇑hmn) ∘ x✝)
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : L.Structure M
inst✝² : L.Structure N
P : Type u_1
inst✝¹ : L.Structure P
Q : Type u_2
inst✝ : L.Structure Q
hnp : N ≃[L] P
hmn : M ≃[L] N
n✝ : ℕ
r✝ : L.Relations n✝
x✝ : Fin n✝ → M
⊢ RelMap r✝ ((⇑hnp ∘ ⇑hmn) ∘ x✝) ↔ RelMap r✝ x✝

Tactic:
;

Goal state after:
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : L.Structure M
inst✝² : L.Structure N
P : Type u_1
inst✝¹ : L.Structure P
Q : Type u_2
inst✝ : L.Structure Q
hnp : N ≃[L] P
hmn : M ≃[L] N
n✝ : ℕ
r✝ : L.Relations n✝
x✝ : Fin n✝ → M
⊢ RelMap r✝ ((⇑hnp ∘ ⇑hmn) ∘ x✝) ↔ RelMap r✝ 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
P : Type u_1
inst✝ : L.Structure P
h : N ≃[L] P
f g : M ≃[L] N
hfg : h.comp f = h.comp g
x : M
⊢ f x = g x

Tactic:
;

Goal state after:
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 : N ≃[L] P
f g : M ≃[L] N
hfg : h.comp f = h.comp g
x : M
⊢ f x = g 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
x✝ : N
⊢ (f.comp f.symm) x✝ = (refl L N) x✝

Tactic:
;

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
x✝ : M
⊢ (f.symm.comp f) x✝ = (refl L M) x✝

Tactic:
;

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.Algebra.Ring.Basic

Goal state before:
pp: α : Type u_1
⊢ (↑[Sum.inl ⟨2, add⟩, Sum.inl ⟨2, mul⟩, Sum.inl ⟨1, neg⟩, Sum.inl ⟨0, zero⟩, Sum.inl ⟨0, one⟩]).Nodup

Tactic:
;

Goal state after:
α : Type u_1
⊢ (↑[Sum.inl ⟨2, add⟩, Sum.inl ⟨2, mul⟩, Sum.inl ⟨1, neg⟩, Sum.inl ⟨0, zero⟩, Sum.inl ⟨0, one⟩]).Nodup
Module: Mathlib.ModelTheory.Algebra.Ring.Basic

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝ : ring.Structure R
a✝¹ a✝ : R
⊢ funMap addFunc (Fin.cons a✝¹ (Fin.cons a✝ finZeroElim)) = a✝¹ + Fin.cons a✝¹ (Fin.cons a✝ finZeroElim) 1

Tactic:
;

Goal state after:
α : Type u_1
R : Type u_2
inst✝ : ring.Structure R
a✝¹ a✝ : R
⊢ funMap addFunc (Fin.cons a✝¹ (Fin.cons a✝ finZeroElim)) = a✝¹ + Fin.cons a✝¹ (Fin.cons a✝ finZeroElim) 1
Module: Mathlib.ModelTheory.Algebra.Ring.Basic

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝ : ring.Structure R
a✝¹ a✝ : R
⊢ funMap mulFunc (Fin.cons a✝¹ (Fin.cons a✝ finZeroElim)) = a✝¹ * Fin.cons a✝¹ (Fin.cons a✝ finZeroElim) 1

Tactic:
;

Goal state after:
α : Type u_1
R : Type u_2
inst✝ : ring.Structure R
a✝¹ a✝ : R
⊢ funMap mulFunc (Fin.cons a✝¹ (Fin.cons a✝ finZeroElim)) = a✝¹ * Fin.cons a✝¹ (Fin.cons a✝ finZeroElim) 1
Module: Mathlib.ModelTheory.Algebra.Ring.Basic

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝ : ring.Structure R
a✝ : R
⊢ funMap negFunc (Fin.cons a✝ finZeroElim) = -a✝

Tactic:
;

Goal state after:
α : Type u_1
R : Type u_2
inst✝ : ring.Structure R
a✝ : R
⊢ funMap negFunc (Fin.cons a✝ finZeroElim) = -a✝
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case func
L : Language
α : Type u'
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term α
ih : ∀ (a : Fin l✝), (LHom.id L).onTerm (_ts✝ a) = id (_ts✝ a)
⊢ (func ((LHom.id L).onFunction _f✝) fun i ↦ id (_ts✝ i)) = id (func _f✝ _ts✝)

Tactic:
;

Goal state after:
case func
L : Language
α : Type u'
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term α
ih : ∀ (a : Fin l✝), (LHom.id L).onTerm (_ts✝ a) = id (_ts✝ a)
⊢ (func ((LHom.id L).onFunction _f✝) fun i ↦ id (_ts✝ i)) = id (func _f✝ _ts✝)
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case func
L : Language
L' : Language
α : Type u'
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term α
ih : ∀ (a : Fin l✝), (φ.comp ψ).onTerm (_ts✝ a) = (φ.onTerm ∘ ψ.onTerm) (_ts✝ a)
⊢ (func ((φ.comp ψ).onFunction _f✝) fun i ↦ (φ.onTerm ∘ ψ.onTerm) (_ts✝ i)) = (φ.onTerm ∘ ψ.onTerm) (func _f✝ _ts✝)

Tactic:
;

Goal state after:
case func
L : Language
L' : Language
α : Type u'
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term α
ih : ∀ (a : Fin l✝), (φ.comp ψ).onTerm (_ts✝ a) = (φ.onTerm ∘ ψ.onTerm) (_ts✝ a)
⊢ (func ((φ.comp ψ).onFunction _f✝) fun i ↦ (φ.onTerm ∘ ψ.onTerm) (_ts✝ i)) = (φ.onTerm ∘ ψ.onTerm) (func _f✝ _ts✝)
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case falsum
L : Language
α : Type u'
k n✝¹ m✝ n✝ : ℕ
km✝ : n✝¹ ≤ m✝
mn✝ : m✝ ≤ n✝
⊢ castLE mn✝ (castLE km✝ falsum) = castLE ⋯ falsum

Tactic:
;

Goal state after:
case falsum
L : Language
α : Type u'
k n✝¹ m✝ n✝ : ℕ
km✝ : n✝¹ ≤ m✝
mn✝ : m✝ ≤ n✝
⊢ castLE mn✝ (castLE km✝ falsum) = castLE ⋯ falsum
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case all
L : Language
α : Type u'
k n✝¹ : ℕ
f✝ : L.BoundedFormula α (n✝¹ + 1)
ih3 : ∀ {m n : ℕ} (km : n✝¹ + 1 ≤ m) (mn : m ≤ n), castLE mn (castLE km f✝) = castLE ⋯ f✝
m✝ n✝ : ℕ
km✝ : n✝¹ ≤ m✝
mn✝ : m✝ ≤ n✝
⊢ castLE mn✝ (castLE km✝ f✝.all) = castLE ⋯ f✝.all

Tactic:
;

Goal state after:
case all
L : Language
α : Type u'
k n✝¹ : ℕ
f✝ : L.BoundedFormula α (n✝¹ + 1)
ih3 : ∀ {m n : ℕ} (km : n✝¹ + 1 ≤ m) (mn : m ≤ n), castLE mn (castLE km f✝) = castLE ⋯ f✝
m✝ n✝ : ℕ
km✝ : n✝¹ ≤ m✝
mn✝ : m✝ ≤ n✝
⊢ castLE mn✝ (castLE km✝ f✝.all) = castLE ⋯ f✝.all
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case all
L : Language
α : Type u'
k n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ {m n : ℕ} (km : n✝ + 1 ≤ m) (mn : m ≤ n), castLE mn (castLE km f✝) = castLE ⋯ f✝
⊢ ∀ {m n : ℕ} (km : n✝ ≤ m) (mn : m ≤ n), castLE mn (castLE km f✝.all) = castLE ⋯ f✝.all

Tactic:
intros; simp only [castLE, ih3]

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case mem
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
y : F
⊢ Group.IsSolvable (X - C y).Gal

Tactic:
;

Goal state after:
case mem
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
y : F
⊢ Group.IsSolvable (X - C y).Gal
Module: Mathlib.ModelTheory.Syntax

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

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

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case rel
L : Language
α : Type u'
n n✝ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (α ⊕ Fin n✝)
⊢ (fun i ↦ Term.relabel (Sum.map id (Fin.cast ⋯)) (ts✝ i)) = Term.relabel (Sum.map id (Fin.cast ⋯)) ∘ ts✝

Tactic:
;

Goal state after:
case rel
L : Language
α : Type u'
n n✝ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (α ⊕ Fin n✝)
⊢ (fun i ↦ Term.relabel (Sum.map id (Fin.cast ⋯)) (ts✝ i)) = Term.relabel (Sum.map id (Fin.cast ⋯)) ∘ ts✝
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case rel
L : Language
α : Type u'
n n✝ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (α ⊕ Fin n✝)
⊢ ((LHom.id L).onRelation R✝).boundedFormula (id ∘ ts✝) = id (rel R✝ ts✝)

Tactic:
;

Goal state after:
case rel
L : Language
α : Type u'
n n✝ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (α ⊕ Fin n✝)
⊢ ((LHom.id L).onRelation R✝).boundedFormula (id ∘ ts✝) = id (rel R✝ ts✝)
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case rel
L : Language
L' : Language
α : Type u'
n : ℕ
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
n✝ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (α ⊕ Fin n✝)
⊢ (φ.onRelation (ψ.onRelation R✝)).boundedFormula ((φ.onTerm ∘ ψ.onTerm) ∘ ts✝) =
    φ.onBoundedFormula ((ψ.onRelation R✝).boundedFormula (ψ.onTerm ∘ ts✝))

Tactic:
;

Goal state after:
case rel
L : Language
L' : Language
α : Type u'
n : ℕ
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
n✝ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (α ⊕ Fin n✝)
⊢ (φ.onRelation (ψ.onRelation R✝)).boundedFormula ((φ.onTerm ∘ ψ.onTerm) ∘ ts✝) =
    φ.onBoundedFormula ((ψ.onRelation R✝).boundedFormula (ψ.onTerm ∘ ts✝))
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
α : Type u'
s t : Set α
h : s ⊆ t
⊢ (fun ab ↦ ((L.con ab.1).term.equal (L.con ab.2).term).not) '' (s ×ˢ s ∩ (diagonal α)ᶜ) ⊆
    (fun ab ↦ ((L.con ab.1).term.equal (L.con ab.2).term).not) '' (t ×ˢ t ∩ (diagonal α)ᶜ)

Tactic:
;

Goal state after:
L : Language
α : Type u'
s t : Set α
h : s ⊆ t
⊢ (fun ab ↦ ((L.con ab.1).term.equal (L.con ab.2).term).not) '' (s ×ˢ s ∩ (diagonal α)ᶜ) ⊆
    (fun ab ↦ ((L.con ab.1).term.equal (L.con ab.2).term).not) '' (t ×ˢ t ∩ (diagonal α)ᶜ)
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case e_v
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
n : ℕ
t : L[[α]].Term (β ⊕ Fin n)
v : β → M
xs : Fin n → M
⊢ Sum.elim (Sum.elim (fun a ↦ ↑(L.con a)) v) xs ∘ ⇑(Equiv.sumAssoc α β (Fin n)).symm =
    Sum.elim (fun a ↦ ↑(L.con a)) (Sum.elim v xs)

Tactic:
;

Goal state after:
case e_v
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
n : ℕ
t : L[[α]].Term (β ⊕ Fin n)
v : β → M
xs : Fin n → M
⊢ Sum.elim (Sum.elim (fun a ↦ ↑(L.con a)) v) xs ∘ ⇑(Equiv.sumAssoc α β (Fin n)).symm =
    Sum.elim (fun a ↦ ↑(L.con a)) (Sum.elim v xs)