mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
N : Type u_1
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪[L] N
⊢ f.toHom.range.subtype.comp f.equivRange.toEmbedding = f

Tactic:
by
  ext; rfl

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case imp
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 : ∀ (v : α ⊕ Fin n✝ → M), f₁✝.toFormula.Realize v ↔ f₁✝.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
ih2 : ∀ (v : α ⊕ Fin n✝ → M), f₂✝.toFormula.Realize v ↔ f₂✝.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
v : α ⊕ Fin n✝ → M
⊢ f₁✝.Realize (v ∘ Sum.inl) (v ∘ Sum.inr) → f₂✝.toFormula.Realize v ↔ (f₁✝ ⟹ f₂✝).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)

Tactic:
ih2,

Goal state after:
case imp
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 : ∀ (v : α ⊕ Fin n✝ → M), f₁✝.toFormula.Realize v ↔ f₁✝.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
ih2 : ∀ (v : α ⊕ Fin n✝ → M), f₂✝.toFormula.Realize v ↔ f₂✝.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
v : α ⊕ Fin n✝ → M
⊢ f₁✝.Realize (v ∘ Sum.inl) (v ∘ Sum.inr) → f₂✝.Realize (v ∘ Sum.inl) (v ∘ Sum.inr) ↔
    (f₁✝ ⟹ f₂✝).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
Module: Mathlib.ModelTheory.ElementarySubstructures

Goal state before:
pp: L : Language
M : Type u_1
inst✝ : L.Structure M
A : Set M
hA : MeetsDefinable A
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
x : Fin n → ↥((closure L).toFun A)
a : M
hφ : φ.Realize default (Fin.snoc (Subtype.val ∘ x) a)
D : Set M := {y | φ.Realize default (Fin.snoc (Subtype.val ∘ x) y)}
hD_ne : D.Nonempty
i : Fin (n + 1)
j : Fin n
⊢ ↑(x j) ∈ A

Tactic:
nth_rw 1 [← hA.closure_eq_self]

Goal state after:
L : Language
M : Type u_1
inst✝ : L.Structure M
A : Set M
hA : MeetsDefinable A
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
x : Fin n → ↥((closure L).toFun A)
a : M
hφ : φ.Realize default (Fin.snoc (Subtype.val ∘ x) a)
D : Set M := {y | φ.Realize default (Fin.snoc (Subtype.val ∘ x) y)}
hD_ne : D.Nonempty
i : Fin (n + 1)
j : Fin n
⊢ ↑(x j) ∈ ↑((closure L).toFun A)
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
f g : Set (α → M)
hf : A.Definable L f
hg : A.Definable L g
⊢ A.Definable L (f ∪ g)

Tactic:
by
  rcases hf with ⟨φ, hφ⟩
  rcases hg with ⟨θ, hθ⟩
  refine ⟨φ ⊔ θ, ?_⟩
  ext
  rw [hφ, hθ, mem_ofPred_eq, Formula.realize_sup, mem_union, mem_ofPred_eq, mem_ofPred_eq]

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: case mp
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
⊢ A.Definable L s → ∃ A0, ↑A0 ⊆ A ∧ (↑A0).Definable L s

Tactic:
simp only [definable_iff_exists_formula_sum]
    rintro ⟨φ, rfl⟩
    let A0 := (φ.freeVarFinset.toLeft).image Subtype.val
    refine ⟨A0, by simp [A0], (φ.restrictFreeVar <| fun x => Sum.casesOn x.1
        (fun x hx => Sum.inl ⟨x, by simp [A0, hx]⟩) (fun x _ => Sum.inr x) x.2), ?_⟩
    ext
    simp only [Formula.Realize, mem_ofPred_eq, Finset.coe_sort_coe]
    exact iff_comm.1 <| BoundedFormula.realize_restrictFreeVar _ (by simp)

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case imp
L : Language
M : Type w
N : Type u_1
inst✝³ : L.Structure M
inst✝² : L.Structure N
α : Type u'
n : ℕ
F : Type u_4
inst✝¹ : EquivLike F M N
inst✝ : L.StrongHomClass F M N
g : F
v : α → M
n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 : ∀ {xs : Fin n✝ → M}, f₁✝.Realize (⇑g ∘ v) (⇑g ∘ xs) ↔ f₁✝.Realize v xs
ih2 : ∀ {xs : Fin n✝ → M}, f₂✝.Realize (⇑g ∘ v) (⇑g ∘ xs) ↔ f₂✝.Realize v xs
xs : Fin n✝ → M
⊢ f₁✝.Realize v xs → f₂✝.Realize (⇑g ∘ v) (⇑g ∘ xs) ↔ (f₁✝ ⟹ f₂✝).Realize v xs

Tactic:
ih2,

Goal state after:
case imp
L : Language
M : Type w
N : Type u_1
inst✝³ : L.Structure M
inst✝² : L.Structure N
α : Type u'
n : ℕ
F : Type u_4
inst✝¹ : EquivLike F M N
inst✝ : L.StrongHomClass F M N
g : F
v : α → M
n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 : ∀ {xs : Fin n✝ → M}, f₁✝.Realize (⇑g ∘ v) (⇑g ∘ xs) ↔ f₁✝.Realize v xs
ih2 : ∀ {xs : Fin n✝ → M}, f₂✝.Realize (⇑g ∘ v) (⇑g ∘ xs) ↔ f₂✝.Realize v xs
xs : Fin n✝ → M
⊢ f₁✝.Realize v xs → f₂✝.Realize v xs ↔ (f₁✝ ⟹ f₂✝).Realize v xs
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type u_1
L : Language
inst✝ : L.Structure M
A : Set M
a : M
γ : Type u_4
ha : a ∈ A
⊢ DefinableFun L[[↑A]] ∅ fun x ↦ a

Tactic:
exact ((L.con (⟨a,ha⟩ : ↑A)).term).definableFun_realize

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case refine_2
L : Language
α : Type u'
M : Type w
inst✝ : L[[α]].Structure M
s : Set α
h : Set.InjOn (fun i ↦ ↑(L.con i)) s
a b : α
ab : (a, b) ∈ (Set.diagonal α)ᶜ
as : (a, b).1 ∈ s
bs : (a, b).2 ∈ s
⊢ M ⊨ ((L.con a).term.equal (L.con b).term).not

Tactic:
simp only [Sentence.Realize, Formula.realize_not, Formula.realize_equal, Term.realize_constants]

Goal state after:
case refine_2
L : Language
α : Type u'
M : Type w
inst✝ : L[[α]].Structure M
s : Set α
h : Set.InjOn (fun i ↦ ↑(L.con i)) s
a b : α
ab : (a, b) ∈ (Set.diagonal α)ᶜ
as : (a, b).1 ∈ s
bs : (a, b).2 ∈ s
⊢ ¬↑(L.con a) = ↑(L.con b)
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: case refine_1
L : Language
T : L.Theory
α : Type w
φ : L.Formula α
h : T ⊨ᵇ φ
M : ((L.lhomWithConstants α).onTheory T).ModelType
this✝ : L.Structure ↑M := (L.lhomWithConstants α).reduct ↑M
this : ↑M ⊨ T
⊢ φ.Realize fun a ↦ ↑(L.con a)

Tactic:
let M' := Theory.ModelType.of T M

Goal state after:
case refine_1
L : Language
T : L.Theory
α : Type w
φ : L.Formula α
h : T ⊨ᵇ φ
M : ((L.lhomWithConstants α).onTheory T).ModelType
this✝ : L.Structure ↑M := (L.lhomWithConstants α).reduct ↑M
this : ↑M ⊨ T
M' : T.ModelType := ModelType.of T ↑M
⊢ φ.Realize fun a ↦ ↑(L.con a)
Module: Mathlib.RingTheory.Nullstellensatz

Goal state before:
pp: k : Type u_1
K : Type u_2
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
σ : Type u_3
I : Ideal (MvPolynomial σ k)
p : MvPolynomial σ k
hp : p ∈ sInf {J | I ≤ J ∧ J.IsPrime}
x : σ → K
hx : x ∈ zeroLocus K I
⊢ p ∈ vanishingIdeal k {x}

Tactic:
refine
    (mem_sInf.mp hp)
      ⟨le_trans (le_vanishingIdeal_zeroLocus I)
          (vanishingIdeal_anti_mono fun y hy => hy.symm ▸ hx),
        inferInstance⟩

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

Goal state before:
pp: case h
R : Type u
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type v
inst✝¹ : MulAction R X
inst✝ : Finite ↥S
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i = s ^ j
hlt : j < i
⊢ (fun x ↦ x /ₒ 1) (s ^ (i - (j + 1)) • x) = x /ₒ s

Tactic:
oreDiv_eq_iff

Goal state after:
case h
R : Type u
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type v
inst✝¹ : MulAction R X
inst✝ : Finite ↥S
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i = s ^ j
hlt : j < i
⊢ ∃ u v, u • x = v • s ^ (i - (j + 1)) • x ∧ ↑u * ↑s = v * ↑1
Module: Mathlib.GroupTheory.OreLocalization.Cardinality

Goal state before:
pp: case h
R : Type u
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type v
inst✝¹ : MulAction R X
inst✝ : Finite X
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i • x = s ^ j • x
hlt : j < i
⊢ (fun x ↦ x /ₒ 1) (s ^ (i - (j + 1)) • x) = x /ₒ s

Tactic:
oreDiv_eq_iff

Goal state after:
case h
R : Type u
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type v
inst✝¹ : MulAction R X
inst✝ : Finite X
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i • x = s ^ j • x
hlt : j < i
⊢ ∃ u v, u • x = v • s ^ (i - (j + 1)) • x ∧ ↑u * ↑s = v * ↑1
Module: Mathlib.FieldTheory.AxGrothendieck

Goal state before:
pp: ι : Type u_1
K : Type u_2
R : Type u_3
inst✝⁴ : Field K
inst✝³ : Finite K
inst✝² : CommRing R
inst✝¹ : Finite ι
inst✝ : Algebra K R
alg : Algebra.IsAlgebraic K R
ps : ι → MvPolynomial ι R
S : Set (ι → R)
hm : Set.MapsTo (fun v i ↦ (eval v) (ps i)) S S
hinj : Set.InjOn (fun v i ↦ (eval v) (ps i)) S
⊢ Set.SurjOn (fun v i ↦ (eval v) (ps i)) S S

Tactic:
have is_int : ∀ x : R, IsIntegral K x := fun x => isAlgebraic_iff_isIntegral.1
    (alg.isAlgebraic x)

Goal state after:
ι : Type u_1
K : Type u_2
R : Type u_3
inst✝⁴ : Field K
inst✝³ : Finite K
inst✝² : CommRing R
inst✝¹ : Finite ι
inst✝ : Algebra K R
alg : Algebra.IsAlgebraic K R
ps : ι → MvPolynomial ι R
S : Set (ι → R)
hm : Set.MapsTo (fun v i ↦ (eval v) (ps i)) S S
hinj : Set.InjOn (fun v i ↦ (eval v) (ps i)) S
is_int : ∀ (x : R), IsIntegral K x
⊢ Set.SurjOn (fun v i ↦ (eval v) (ps i)) S S
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'
h✝ : Infinite X
x : X
s s' : ↥S
h : s • x = s' • x
hc : Commute s s'
⊢ x /ₒ s = x /ₒ s'

Tactic:
oreDiv_eq_iff

Goal state after:
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'
h✝ : Infinite X
x : X
s s' : ↥S
h : s • x = s' • x
hc : Commute s s'
⊢ ∃ u v, u • x = v • x ∧ ↑u * ↑s' = v * ↑s
Module: Mathlib.FieldTheory.FinTrdeg

Goal state before:
pp: case mpr
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
⊢ Algebra.trdeg K L < Cardinal.aleph0 → FinTrdeg K L

Tactic:
· intro h
    obtain ⟨s, hs⟩ := exists_isTranscendenceBasis K L
    have fin : s.Finite := Cardinal.lt_aleph0_iff_set_finite.1 (hs.cardinalMk_eq_trdeg.trans_lt h)
    constructor
    refine ⟨adjoin K s, fg_adjoin_of_finite fin, ?_⟩
    have alg := hs.isAlgebraic_field
    rwa [Subtype.range_coe] at alg

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

Goal state before:
pp: K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
⊢ (indicator c).degrees ≤ ∑ s, (Fintype.card K - 1) • {s}

Tactic:
indicator

Goal state after:
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
⊢ (∏ n, (1 - (X n - C (c n)) ^ (Fintype.card K - 1))).degrees ≤ ∑ s, (Fintype.card K - 1) • {s}
Module: Mathlib.FieldTheory.Finite.Polynomial

Goal state before:
pp: K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
s : σ
x✝ : s ∈ Finset.univ
⊢ 0 ∪ ((X s - C (c s)) ^ (Fintype.card K - 1)).degrees ≤ (Fintype.card K - 1) • {s}

Tactic:
Multiset.zero_union

Goal state after:
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
s : σ
x✝ : s ∈ Finset.univ
⊢ ((X s - C (c s)) ^ (Fintype.card K - 1)).degrees ≤ (Fintype.card K - 1) • {s}
Module: Mathlib.FieldTheory.Finite.Polynomial

Goal state before:
pp: K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
⊢ ∀ (i : σ), Multiset.count i (indicator c).degrees ≤ Fintype.card K - 1

Tactic:
indicator

Goal state after:
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
⊢ ∀ (i : σ), Multiset.count i (∏ n, (1 - (X n - C (c n)) ^ (Fintype.card K - 1))).degrees ≤ Fintype.card K - 1
Module: Mathlib.Topology.Separation.Connected

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : ConnectedSpace X
inst✝¹ : Nontrivial X
inst✝ : T1Space X
x : X
contra : ¬(𝓝[≠] x).NeBot
⊢ False

Tactic:
rw [not_neBot, ← isOpen_singleton_iff_punctured_nhds] at contra

Goal state after:
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : ConnectedSpace X
inst✝¹ : Nontrivial X
inst✝ : T1Space X
x : X
contra : IsOpen[inst✝³] {x}
⊢ False
Module: Mathlib.FieldTheory.Differential.Liouville

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁹ : Field F
inst✝⁸ : Field K
inst✝⁷ : Differential F
inst✝⁶ : Differential K
inst✝⁵ : Algebra F K
inst✝⁴ : DifferentialAlgebra F K
inst✝³ : CharZero F
inst✝² : FiniteDimensional F K
inst✝¹ : IsGalois F K
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → K
v : K
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
this : CharZero K
c₀ : ι → F := fun i ↦ c i / ↑(Fintype.card Gal(K/F))
⊢ ∃ ι₀ x c₀, ∃ (_ : ∀ (x : ι₀), (c₀ x)′ = 0), ∃ u₀ v₀, a = ∑ x, c₀ x * logDeriv (u₀ x) + v₀′

Tactic:
let u₁ (i : ι) := ∏ x : (K ≃ₐ[F] K), x (u i)

Goal state after:
F : Type u_1
K : Type u_2
inst✝⁹ : Field F
inst✝⁸ : Field K
inst✝⁷ : Differential F
inst✝⁶ : Differential K
inst✝⁵ : Algebra F K
inst✝⁴ : DifferentialAlgebra F K
inst✝³ : CharZero F
inst✝² : FiniteDimensional F K
inst✝¹ : IsGalois F K
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → K
v : K
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
this : CharZero K
c₀ : ι → F := fun i ↦ c i / ↑(Fintype.card Gal(K/F))
u₁ : ι → K := fun i ↦ ∏ x, x (u i)
⊢ ∃ ι₀ x c₀, ∃ (_ : ∀ (x : ι₀), (c₀ x)′ = 0), ∃ u₀ v₀, a = ∑ x, c₀ x * logDeriv (u₀ x) + v₀′
Module: Mathlib.FieldTheory.IntermediateField.ExtendRight

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Algebra K L
F : IntermediateField K L
M : Type u_3
inst✝⁸ : Field M
inst✝⁷ : Algebra K M
inst✝⁶ : Algebra L M
inst✝⁵ : IsScalarTower K L M
R : Type u_4
S : Type u_5
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra S ↥F
inst✝¹ : Algebra S M
inst✝ : IsScalarTower S (↥F) M
s : S
x : ↥(F.extendRight M)
⊢ s • ↑x ∈ F.extendRight M

Tactic:
Algebra.smul_def

Goal state after:
K : Type u_1
L : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Algebra K L
F : IntermediateField K L
M : Type u_3
inst✝⁸ : Field M
inst✝⁷ : Algebra K M
inst✝⁶ : Algebra L M
inst✝⁵ : IsScalarTower K L M
R : Type u_4
S : Type u_5
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra S ↥F
inst✝¹ : Algebra S M
inst✝ : IsScalarTower S (↥F) M
s : S
x : ↥(F.extendRight M)
⊢ (algebraMap S M) s * ↑x ∈ F.extendRight M
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y : ℕ
⊢ ↑x = ↑y ↔ ↑x = ↑y

Tactic:
constructor <;> intro H
  · rw [natCast K p 0, natCast K p 0, mk_eq_iff] at H
    obtain ⟨z, H⟩ := H
    simpa only [zero_add, iterate_fixed (map_natCast _ _)] using H
  rw [natCast K p 0, natCast K p 0, H]

Goal state after:
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : CommRing K
inst✝¹⁰ : CommRing L
inst✝⁹ : CommRing M
inst✝⁸ : CommRing N
i : K →+* L
j : K →+* M
g : L →+* N
p : ℕ
inst✝⁷ : ExpChar M p
inst✝⁶ : ExpChar K p
inst✝⁵ : PerfectRing M p
inst✝⁴ : IsPRadical i p
inst✝³ : ExpChar L p
inst✝² : ExpChar N p
inst✝¹ : IsPRadical g p
inst✝ : IsPRadical (g.comp i) p
⊢ lift g (lift i j p) p = lift (g.comp i) j p

Tactic:
refine IsPRadical.injective_comp_of_perfect _ (g.comp i) p ?_

Goal state after:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : CommRing K
inst✝¹⁰ : CommRing L
inst✝⁹ : CommRing M
inst✝⁸ : CommRing N
i : K →+* L
j : K →+* M
g : L →+* N
p : ℕ
inst✝⁷ : ExpChar M p
inst✝⁶ : ExpChar K p
inst✝⁵ : PerfectRing M p
inst✝⁴ : IsPRadical i p
inst✝³ : ExpChar L p
inst✝² : ExpChar N p
inst✝¹ : IsPRadical g p
inst✝ : IsPRadical (g.comp i) p
⊢ (fun f ↦ f.comp (g.comp i)) (lift g (lift i j p) p) = (fun f ↦ f.comp (g.comp i)) (lift (g.comp i) j p)
Module: Mathlib.FieldTheory.Isaacs

Goal state before:
pp: F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (x : E), ∃ y, (aeval y) (minpoly F x) = 0
S : Finset E
p : K[X] := ∏ x ∈ S, Polynomial.map (algebraMap F K) (minpoly F x)
⊢ ↥(adjoin F ↑S) →ₐ[F] K

Tactic:
let K' := SplittingField p

Goal state after:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (x : E), ∃ y, (aeval y) (minpoly F x) = 0
S : Finset E
p : K[X] := ∏ x ∈ S, Polynomial.map (algebraMap F K) (minpoly F x)
K' : Type u_3 := p.SplittingField
⊢ ↥(adjoin F ↑S) →ₐ[F] K
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: case ind
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq (Subgroup G)
n : ℕ
ih :
  ∀ m < n,
    ∀ {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι},
      ⋃ i ∈ s, g i • ↑(H i) = Set.univ →
        ∀ j ∈ s,
          ⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H i) ≠ Set.univ →
            m = (Finset.image H s).card → ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
j : ι
hj : j ∈ s
hcovers' : ⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H i) ≠ Set.univ
hn : n = (Finset.image H s).card
x : G
hx : ∀ (y : G), y • ↑(H j) ⊆ ⋃ i ∈ {x ∈ s | H x ≠ H j}, (y * x⁻¹ * g i) • ↑(H i)
κ : Type u_2 := ↥({x ∈ s | H x ≠ H j}) × Option ↥({x ∈ s | H x = H j})
f : κ → G :=
  fun x_1 ↦
    match x_1 with
    | (k₁, some k₂) => g ↑k₂ * x⁻¹ * g ↑k₁
    | (k₁, none) => g ↑k₁
K : κ → Subgroup G := fun k ↦ H ↑k.1
⊢ ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex

Tactic:
have hK' (k : κ) : K k ∈ (s.image H).erase (H j) := by
      have := Finset.mem_filter.mp k.1.property
      exact Finset.mem_erase.mpr ⟨this.2, Finset.mem_image_of_mem H this.1⟩

Goal state after:
case ind
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq (Subgroup G)
n : ℕ
ih :
  ∀ m < n,
    ∀ {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι},
      ⋃ i ∈ s, g i • ↑(H i) = Set.univ →
        ∀ j ∈ s,
          ⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H i) ≠ Set.univ →
            m = (Finset.image H s).card → ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
j : ι
hj : j ∈ s
hcovers' : ⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H i) ≠ Set.univ
hn : n = (Finset.image H s).card
x : G
hx : ∀ (y : G), y • ↑(H j) ⊆ ⋃ i ∈ {x ∈ s | H x ≠ H j}, (y * x⁻¹ * g i) • ↑(H i)
κ : Type u_2 := ↥({x ∈ s | H x ≠ H j}) × Option ↥({x ∈ s | H x = H j})
f : κ → G :=
  fun x_1 ↦
    match x_1 with
    | (k₁, some k₂) => g ↑k₂ * x⁻¹ * g ↑k₁
    | (k₁, none) => g ↑k₁
K : κ → Subgroup G := fun k ↦ H ↑k.1
hK' : ∀ (k : κ), K k ∈ (Finset.image H s).erase (H j)
⊢ ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
Module: Mathlib.RingTheory.Algebraic.LinearIndependent

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
H : ∀ (p : F[X]), (aeval x) p = 0 → p = 0
s : Finset F
m : F → F
i : F
hi : i ∈ s
hnz : ∀ (a : F), x - (algebraMap F E) a ≠ 0
b : E := ∏ j ∈ s, (x - (algebraMap F E) j)
h1 : ∀ i ∈ s, m i • (b * (x - (algebraMap F E) i)⁻¹) = m i • ∏ j ∈ s.erase i, (x - (algebraMap F E) j)
hm : ∑ x_1 ∈ s, m x_1 • ∏ j ∈ s.erase x_1, (x - (algebraMap F E) j) = 0
p : F[X] := ∑ i ∈ s, C (m i) * ∏ j ∈ s.erase i, (X - C j)
⊢ ∑ x_1 ∈ s, (algebraMap F E) (m x_1) * ∏ x_2 ∈ s.erase x_1, (x - (algebraMap F E) x_2) =
    ∑ x_1 ∈ s, m x_1 • ∏ j ∈ s.erase x_1, (x - (algebraMap F E) j)

Tactic:
Algebra.smul_def

Goal state after:
Module: Mathlib.FieldTheory.JacobsonNoether

Goal state before:
pp: case neg
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
H : k ≠ ⊤
p : ℕ
hp : ExpChar D p
insep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
a : D
ha : a ∉ k
ha₀ : a ≠ 0
b : D
hb1 : ((ad (↥k) D) a) b ≠ 0
m : ℕ
hm2 : ∀ (n : ℕ), p ^ m ≤ n → (⇑((ad (↥k) D) a))^[n] = 0
h_exist : ∃ n, 0 < n ∧ (⇑((ad (↥k) D) a))^[n + 1] b = 0
t : ℕ := Nat.find h_exist - 1
ht : t = Nat.find h_exist - 1
h_pos : Nat.find h_exist - 1 = 0
⊢ Nat.find h_exist = 1

Tactic:
Nat.sub_eq_zero_iff_le

Goal state after:
case neg
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
H : k ≠ ⊤
p : ℕ
hp : ExpChar D p
insep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
a : D
ha : a ∉ k
ha₀ : a ≠ 0
b : D
hb1 : ((ad (↥k) D) a) b ≠ 0
m : ℕ
hm2 : ∀ (n : ℕ), p ^ m ≤ n → (⇑((ad (↥k) D) a))^[n] = 0
h_exist : ∃ n, 0 < n ∧ (⇑((ad (↥k) D) a))^[n + 1] b = 0
t : ℕ := Nat.find h_exist - 1
ht : t = Nat.find h_exist - 1
h_pos : Nat.find h_exist ≤ 1
⊢ Nat.find h_exist = 1
Module: Mathlib.RingTheory.Algebraic.LinearIndependent

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
H : ∀ (p : F[X]), (aeval x) p = 0 → p = 0
s : Finset F
m : F → F
i : F
hi : i ∈ s
hnz : ∀ (a : F), x - (algebraMap F E) a ≠ 0
b : E := ∏ j ∈ s, (x - (algebraMap F E) j)
h1 : ∀ i ∈ s, m i • (b * (x - (algebraMap F E) i)⁻¹) = m i • ∏ j ∈ s.erase i, (x - (algebraMap F E) j)
p : F[X] := ∑ i ∈ s, C (m i) * ∏ j ∈ s.erase i, (X - C j)
hm : (aeval i) p = (aeval i) 0
j : F
hj : j ∈ s.erase i
⊢ m j * ∏ x ∈ s.erase j, (i - x) = 0

Tactic:
by
    have := Finset.mem_erase_of_ne_of_mem (Finset.ne_of_mem_erase hj).symm hi
    simp_rw [← (s.erase j).prod_erase_mul _ this, sub_self, mul_zero]

Goal state after:
Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
ι : Type w
x : ι → E
inst✝ : Nonempty ι
hx : IsTranscendenceBasis F x
⊢ lift.{max u w, v} (Module.rank F E) = max (max (lift.{max v w, u} #F) (lift.{max u v, w} #ι)) ℵ₀

Tactic:
let K := IntermediateField.adjoin F (Set.range x)

Goal state after:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
ι : Type w
x : ι → E
inst✝ : Nonempty ι
hx : IsTranscendenceBasis F x
K : IntermediateField F E := IntermediateField.adjoin F (range x)
⊢ lift.{max u w, v} (Module.rank F E) = max (max (lift.{max v w, u} #F) (lift.{max u v, w} #ι)) ℵ₀
Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality

Goal state before:
pp: case pos
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A B : IntermediateField F E
hA : ¬Algebra.IsAlgebraic F ↥A
hB : Algebra.IsAlgebraic F ↥B
⊢ Module.rank F ↥(A ⊔ B) ≤ Module.rank F ↥A * Module.rank F ↥B

pp: case neg
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A B : IntermediateField F E
hA : ¬Algebra.IsAlgebraic F ↥A
hB : ¬Algebra.IsAlgebraic F ↥B
⊢ Module.rank F ↥(A ⊔ B) ≤ Module.rank F ↥A * Module.rank F ↥B

Tactic:
· exact rank_sup_le_of_isAlgebraic A B (Or.inr hB)

Goal state after:
case neg
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A B : IntermediateField F E
hA : ¬Algebra.IsAlgebraic F ↥A
hB : ¬Algebra.IsAlgebraic F ↥B
⊢ Module.rank F ↥(A ⊔ B) ≤ Module.rank F ↥A * Module.rank F ↥B
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: K : Type u
inst✝¹ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
inst✝ : NeZero n
⊢ Function.RightInverse (AdjoinRootXPowSubCEquivToRootsOfUnity hζ H) (↑(autAdjoinRootXPowSubC n a)).toFun

Tactic:
by
    intro e
    have := Fact.mk H
    let : Algebra K K[n√a] := inferInstance
    apply AlgEquiv.coe_toAlgHom_injective
    apply AdjoinRoot.algHom_ext
    simp only [AdjoinRootXPowSubCEquivToRootsOfUnity, AdjoinRoot.algebraMap_eq, OneHom.toFun_eq_coe,
      MonoidHom.toOneHom_coe, AlgEquiv.coe_toAlgHom, autAdjoinRootXPowSubC_root, Algebra.smul_def]
    rw [rootsOfUnityEquivOfPrimitiveRoots_symm_apply, rootsOfUnity.val_mkOfPowEq_coe]
    split_ifs with h
    · obtain rfl := not_imp_not.mp (fun hn ↦ ne_zero_of_irreducible_X_pow_sub_C' hn H) h
      rw [(pow_one _).symm.trans (root_X_pow_sub_C_pow 1 a), one_mul,
        ← AdjoinRoot.algebraMap_eq, AlgEquiv.commutes]
    · refine div_mul_cancel₀ _ (root_X_pow_sub_C_ne_zero' (NeZero.pos n) h)

Goal state after: