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

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
f : L.Functions 2
t₁ t₂ : L.Term α
v : α → M
⊢ (funMap f fun i ↦ realize v (![t₁, t₂] i)) = funMap f ![realize v t₁, realize v t₂]

Tactic:
refine congr rfl (funext (Fin.cases ?_ ?_))

Goal state after:
case refine_1
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
f : L.Functions 2
t₁ t₂ : L.Term α
v : α → M
⊢ realize v (![t₁, t₂] 0) = ![realize v t₁, realize v t₂] 0

case refine_2
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
f : L.Functions 2
t₁ t₂ : L.Term α
v : α → M
⊢ ∀ (i : Fin 1), realize v (![t₁, t₂] i.succ) = ![realize v t₁, realize v t₂] i.succ
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case refine_3
L : Language
α : Type u'
s : Set α
i j : α
⊢ (∃ i_1, (∃ (x : i ∈ s), ⟨i, ⋯⟩ ∈ i_1) ∧ ∃ (x : j ∈ s), ⟨j, ⋯⟩ ∈ i_1) → i ∈ s ∧ j ∈ s

Tactic:
· rintro ⟨t, ⟨is, _⟩, ⟨js, _⟩⟩
      exact ⟨is, js⟩

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
l : ℕ
v : α → M
xs : Fin l → M
R : L.Relations 2
t₁ t₂ : L.Term (α ⊕ Fin l)
⊢ (RelMap R fun i ↦ realize (Sum.elim v xs) (![t₁, t₂] i)) =
    RelMap R ![realize (Sum.elim v xs) t₁, realize (Sum.elim v xs) t₂]

Tactic:
refine congr rfl (funext (Fin.cases ?_ ?_))

Goal state after:
case refine_1
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
l : ℕ
v : α → M
xs : Fin l → M
R : L.Relations 2
t₁ t₂ : L.Term (α ⊕ Fin l)
⊢ realize (Sum.elim v xs) (![t₁, t₂] 0) = ![realize (Sum.elim v xs) t₁, realize (Sum.elim v xs) t₂] 0

case refine_2
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
l : ℕ
v : α → M
xs : Fin l → M
R : L.Relations 2
t₁ t₂ : L.Term (α ⊕ Fin l)
⊢ ∀ (i : Fin 1),
    realize (Sum.elim v xs) (![t₁, t₂] i.succ) = ![realize (Sum.elim v xs) t₁, realize (Sum.elim v xs) t₂] i.succ
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: L : Language
α : Type u'
h1 : Countable α
h2 : Countable ((l : ℕ) × L.Functions l)
⊢ ℵ₀ ≤ ℵ₀ ∧ #(α ⊕ (i : ℕ) × L.Functions i) ≤ ℵ₀

Tactic:
simp only [le_refl, mk_sum, add_le_aleph0, lift_le_aleph0, true_and]

Goal state after:
L : Language
α : Type u'
h1 : Countable α
h2 : Countable ((l : ℕ) × L.Functions l)
⊢ #α ≤ ℵ₀ ∧ #((i : ℕ) × L.Functions i) ≤ ℵ₀
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case imp
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 :
  ∀ {f : ↥f₁✝.freeVarFinset → β} {xs : Fin n✝ → M},
    (∀ (a : ↥f₁✝.freeVarFinset), v (f a) = v' ↑a) → ((f₁✝.restrictFreeVar f).Realize v xs ↔ f₁✝.Realize v' xs)
ih2 :
  ∀ {f : ↥f₂✝.freeVarFinset → β} {xs : Fin n✝ → M},
    (∀ (a : ↥f₂✝.freeVarFinset), v (f a) = v' ↑a) → ((f₂✝.restrictFreeVar f).Realize v xs ↔ f₂✝.Realize v' xs)
f : ↥(f₁✝ ⟹ f₂✝).freeVarFinset → β
xs : Fin n✝ → M
hv' : ∀ (a : ↥(f₁✝ ⟹ f₂✝).freeVarFinset), v (f a) = v' ↑a
⊢ (f₁✝.restrictFreeVar (f ∘ Set.inclusion ⋯)).Realize v xs → (f₂✝.restrictFreeVar (f ∘ Set.inclusion ⋯)).Realize v xs ↔
    f₁✝.Realize v' xs → f₂✝.Realize v' xs

Tactic:
rw [ih1, ih2]

Goal state after:
case imp
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 :
  ∀ {f : ↥f₁✝.freeVarFinset → β} {xs : Fin n✝ → M},
    (∀ (a : ↥f₁✝.freeVarFinset), v (f a) = v' ↑a) → ((f₁✝.restrictFreeVar f).Realize v xs ↔ f₁✝.Realize v' xs)
ih2 :
  ∀ {f : ↥f₂✝.freeVarFinset → β} {xs : Fin n✝ → M},
    (∀ (a : ↥f₂✝.freeVarFinset), v (f a) = v' ↑a) → ((f₂✝.restrictFreeVar f).Realize v xs ↔ f₂✝.Realize v' xs)
f : ↥(f₁✝ ⟹ f₂✝).freeVarFinset → β
xs : Fin n✝ → M
hv' : ∀ (a : ↥(f₁✝ ⟹ f₂✝).freeVarFinset), v (f a) = v' ↑a
⊢ ∀ (a : ↥f₂✝.freeVarFinset), v ((f ∘ Set.inclusion ⋯) a) = v' ↑a

case imp
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 :
  ∀ {f : ↥f₁✝.freeVarFinset → β} {xs : Fin n✝ → M},
    (∀ (a : ↥f₁✝.freeVarFinset), v (f a) = v' ↑a) → ((f₁✝.restrictFreeVar f).Realize v xs ↔ f₁✝.Realize v' xs)
ih2 :
  ∀ {f : ↥f₂✝.freeVarFinset → β} {xs : Fin n✝ → M},
    (∀ (a : ↥f₂✝.freeVarFinset), v (f a) = v' ↑a) → ((f₂✝.restrictFreeVar f).Realize v xs ↔ f₂✝.Realize v' xs)
f : ↥(f₁✝ ⟹ f₂✝).freeVarFinset → β
xs : Fin n✝ → M
hv' : ∀ (a : ↥(f₁✝ ⟹ f₂✝).freeVarFinset), v (f a) = v' ↑a
⊢ ∀ (a : ↥f₁✝.freeVarFinset), v ((f ∘ Set.inclusion ⋯) a) = v' ↑a
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: case refine_1
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
h : s ∈ (closure L).closed
n : ℕ
f : L.Functions n
⊢ ClosedUnder f s

Tactic:
rw [← h]
    exact Substructure.fun_mem _ _

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
v : α → M
R : L.Relations 2
t₁ t₂ : L.Term α
⊢ (RelMap R fun i ↦ Term.realize v (![t₁, t₂] i)) = RelMap R ![Term.realize v t₁, Term.realize v t₂]

Tactic:
refine congr rfl (funext (Fin.cases ?_ ?_))

Goal state after:
case refine_1
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
v : α → M
R : L.Relations 2
t₁ t₂ : L.Term α
⊢ Term.realize v (![t₁, t₂] 0) = ![Term.realize v t₁, Term.realize v t₂] 0

case refine_2
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
v : α → M
R : L.Relations 2
t₁ t₂ : L.Term α
⊢ ∀ (i : Fin 1), Term.realize v (![t₁, t₂] i.succ) = ![Term.realize v t₁, Term.realize v t₂] i.succ
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case rel.refine_2
L : Language
α : Type u'
l✝ : List ((n : ℕ) × L.BoundedFormula α n)
n φ_n φ_l : ℕ
φ_R : L.Relations φ_l
ts : Fin φ_l → L.Term (α ⊕ Fin φ_n)
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
h :
  ∀ (i : Fin φ_l),
    (List.map Sum.getLeft? (List.map (fun i ↦ Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l))[i]?.join =
      some ⟨φ_n, ts i⟩
⊢ (List.map (fun i ↦ Sum.inl ⟨φ_n, ts i⟩) (finRange φ_l)).length ≤ φ_l

Tactic:
rw [length_map, length_finRange]

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: case intro.intro
M : Type w
A : Set M
L : Language
inst✝² : L.Structure M
α : Type u₁
β : Type u_1
s : Set (β → M)
h : A.Definable L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
⊢ A.Definable L ((fun g ↦ g ∘ f) '' s)

Tactic:
have h :=
      (((h.image_comp_equiv (Equiv.Set.sumCompl (range f))).image_comp_equiv
                (Equiv.sumCongr (_root_.Equiv.refl _)
                  (Fintype.equivFin _).symm)).image_comp_sumInl_fin
            _).preimage_comp
        (rangeSplitting f)

Goal state after:
case intro.intro
M : Type w
A : Set M
L : Language
inst✝² : L.Structure M
α : Type u₁
β : Type u_1
s : Set (β → M)
h✝ : A.Definable L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  A.Definable L
    ((fun g ↦ g ∘ rangeSplitting f) ⁻¹'
      (fun g ↦ g ∘ Sum.inl) ''
        (fun g ↦ g ∘ ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ''
          (fun g ↦ g ∘ ⇑(Equiv.Set.sumCompl (range f))) '' s)
⊢ A.Definable L ((fun g ↦ g ∘ f) '' s)
Module: Mathlib.ModelTheory.Skolem

Goal state before:
pp: case w
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : L.Structure M
S : (L.sum L.skolem₁).Substructure M
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
x : Fin n → ↥(LHom.sumInl.substructureReduct S)
a : M
h : φ.Realize default (Fin.snoc (Subtype.val ∘ x) a)
φ' : (L.sum L.skolem₁).Functions n := LHom.sumInr.onFunction φ
⊢ funMap φ' (Subtype.val ∘ x) ∈ LHom.sumInl.substructureReduct S

Tactic:
· exact S.fun_mem (LHom.sumInr.onFunction φ) ((↑) ∘ x) (by
      exact fun i => (x i).2)

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: case intro.intro.mpr
M : Type w
A : Set M
L : Language
inst✝² : L.Structure M
α : Type u₁
β : Type u_1
s : Set (β → M)
h✝ : A.Definable L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  A.Definable L
    ((fun g ↦ g ∘ rangeSplitting f) ⁻¹'
      (fun g ↦ g ∘ Sum.inl) ''
        (fun g ↦ g ∘ ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ''
          (fun g ↦ g ∘ ⇑(Equiv.Set.sumCompl (range f))) '' s)
h' : A.Definable L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
x : α → M
⊢ (∃ x_1 ∈ s, x_1 ∘ f = x) →
    (∃ a ∈ s,
        ((a ∘ ⇑(Equiv.Set.sumCompl (range f))) ∘
              ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ∘
            Sum.inl =
          x ∘ rangeSplitting f) ∧
      ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))

Tactic:
· rintro ⟨y, ys, rfl⟩
      refine ⟨⟨y, ys, ?_⟩, fun a => ?_⟩
      · ext
        simp [Set.apply_rangeSplitting f]
      · rw [Function.comp_apply, Function.comp_apply, apply_rangeSplitting f,
          rangeFactorization_coe]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case refine_1
L : Language
M : Type w
inst✝ : L.Structure M
n : ℕ
xs : Fin n → M
h :
  ∀ (φ : L.BoundedFormula Empty n) (x x_1 : Fin n),
    (decide ¬x = x_1) = true → ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → φ.Realize default xs
i j : Fin n
ij : i ≠ j
⊢ xs i ≠ xs j

Tactic:
exact h _ i j (by simpa using ij) rfl

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: case pos
M : Type u_1
L : Language
inst✝¹ : L.Structure M
α : Type u_2
A : Set M
f : (α → M) → M
p : (α → M) → Prop
g : (α → M) → M
inst✝ : DecidablePred p
hp : A.Definable L (ofPred p)
hf : DefinableFun L A f
hg : DefinableFun L A g
P : Set (Option α → M) := {w | p (w ∘ some)}
hP : A.Definable L P
w : Option α → M
h : p (w ∘ some)
⊢ (w ∈ tupleGraph fun v ↦ if p v then f v else g v) ↔ w ∈ P ∩ tupleGraph f ∪ Pᶜ ∩ tupleGraph g

Tactic:
simp [tupleGraph, P, h]

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: case neg
M : Type u_1
L : Language
inst✝¹ : L.Structure M
α : Type u_2
A : Set M
f : (α → M) → M
p : (α → M) → Prop
g : (α → M) → M
inst✝ : DecidablePred p
hp : A.Definable L (ofPred p)
hf : DefinableFun L A f
hg : DefinableFun L A g
P : Set (Option α → M) := {w | p (w ∘ some)}
hP : A.Definable L P
w : Option α → M
h : ¬p (w ∘ some)
⊢ (w ∈ tupleGraph fun v ↦ if p v then f v else g v) ↔ w ∈ P ∩ tupleGraph f ∪ Pᶜ ∩ tupleGraph g

Tactic:
simp [tupleGraph, P, h]

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
φ : L.Sentence
M : T.ModelType
h : ↑M ⊨ Formula.not φ
⊢ Nonempty (T ∪ {Formula.not φ}).ModelType

Tactic:
refine
    ⟨{  Carrier := M
        is_model := ⟨fun ψ hψ => hψ.elim (realize_sentence_of_mem _) fun h' => ?_⟩ }⟩

Goal state after:
L : Language
T : L.Theory
φ : L.Sentence
M : T.ModelType
h : ↑M ⊨ Formula.not φ
ψ : L.Sentence
hψ : ψ ∈ T ∪ {Formula.not φ}
h' : ψ ∈ {Formula.not φ}
⊢ ↑M ⊨ ψ
Module: Mathlib.RingTheory.Localization.Cardinality

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
L : Type v
inst✝² : CommRing L
inst✝¹ : Algebra R L
S : Submonoid R
inst✝ : IsLocalization S L
hS : S ≤ R⁰
this : #(Localization S) = #R
⊢ Cardinal.lift.{u, v} #L = Cardinal.lift.{v, u} #R

Tactic:
rwa [← lift_inj.{u, v}, lift_mk_eq'.2 ⟨(Localization.algEquiv S L).toEquiv⟩] at this

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

Goal state before:
pp: case neg
a : ℕ
h : ¬ℵ₀ ≤ ↑a
⊢ IsPrimePow ↑a ↔ ∃ n, ↑a = ↑n ∧ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n

Tactic:
rw [isPrimePow_def]

Goal state after:
case neg
a : ℕ
h : ¬ℵ₀ ≤ ↑a
⊢ (∃ p k, Prime p ∧ 0 < k ∧ p ^ k = ↑a) ↔ ∃ n, ↑a = ↑n ∧ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
Module: Mathlib.FieldTheory.Finite.Extension

Goal state before:
pp: k : Type u_1
inst✝⁶ : Field k
inst✝⁵ : Finite k
p : ℕ
inst✝⁴ : Fact (Nat.Prime p)
inst✝³ : CharP k p
n : ℕ
inst✝² : NeZero n
l : Type u_2
inst✝¹ : Field l
inst✝ : Algebra k l
h : Module.finrank k l = n
this✝¹ : Module.Finite k l
this✝ : Finite l
this : Fintype l
⊢ IsSplittingField k l (X ^ Nat.card k ^ Module.finrank k l - X)

Tactic:
← Module.natCard_eq_pow_finrank,

Goal state after:
k : Type u_1
inst✝⁶ : Field k
inst✝⁵ : Finite k
p : ℕ
inst✝⁴ : Fact (Nat.Prime p)
inst✝³ : CharP k p
n : ℕ
inst✝² : NeZero n
l : Type u_2
inst✝¹ : Field l
inst✝ : Algebra k l
h : Module.finrank k l = n
this✝¹ : Module.Finite k l
this✝ : Finite l
this : Fintype l
⊢ IsSplittingField k l (X ^ Nat.card l - X)
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
⊢ degrees 1 ∪ ((X s - C (c s)) ^ (Fintype.card K - 1)).degrees ≤ (Fintype.card K - 1) • {s}

Tactic:
degrees_one,

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
⊢ 0 ∪ ((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
⊢ (indicator c).degrees ≤ ∑ s, (Fintype.card K - 1) • {s}

Tactic:
by
  rw [indicator]
  classical
  refine degrees_prod_le.trans <| Finset.sum_le_sum fun s _ ↦ degrees_sub_le.trans ?_
  rw [degrees_one, Multiset.zero_union]
  refine le_trans degrees_pow_le (nsmul_le_nsmul_right ?_ _)
  refine degrees_sub_le.trans ?_
  rw [degrees_C, Multiset.union_zero]
  exact degrees_X' _

Goal state after:
Module: Mathlib.FieldTheory.CardinalEmb

Goal state before:
pp: F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝¹ : Algebra.IsAlgebraic F E
inst✝ : Algebra.IsSeparable F E
i : (Module.rank F E).ord.ToType
⊢ 2 ≤ #(Emb ↥(adjoin F (⇑b ∘ φ '' Iio i)) ↥(↥(adjoin F (⇑b ∘ φ '' Iio i)))⟮b (φ i)⟯)

Tactic:
rw [← Nat.cast_ofNat, ← toNat_le_iff_le_of_lt_aleph0 natCast_lt_aleph0 (deg_lt_aleph0 i),
    toNat_natCast, ← Nat.card, ← finSepDegree, finSepDegree_eq_finrank_of_isSeparable,
    Nat.succ_le_iff]
  by_contra!
  obtain ⟨x, hx⟩ := finrank_adjoin_simple_eq_one_iff.mp (this.antisymm Module.finrank_pos)
  refine (isLeast_leastExt i).1 (hx ▸ ?_)
  exact x.2

Goal state after:
Module: Mathlib.FieldTheory.Galois.Profinite

Goal state before:
pp: case op.op
k : Type u_1
K : Type u_2
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
L₃ : (FiniteGaloisIntermediateField k K)ᵒᵖ
L₁ L₂ : FiniteGaloisIntermediateField k K
g : op L₂ ⟶ L₃
f : op L₁ ⟶ op L₂
⊢ finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g

Tactic:
induction L₃ with

Goal state after:
case op.op.op
k : Type u_1
K : Type u_2
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
L₁ L₂ : FiniteGaloisIntermediateField k K
f : op L₁ ⟶ op L₂
L₃ : FiniteGaloisIntermediateField k K
g : op L₂ ⟶ op L₃
⊢ finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g
Module: Mathlib.FieldTheory.Galois.Profinite

Goal state before:
pp: case op.op.op.mk.mk
k : Type u_1
K : Type u_2
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
L₃ : FiniteGaloisIntermediateField k K
L₁ : IntermediateField k K
finiteDimensional✝¹ : FiniteDimensional k ↥L₁
isGalois✝¹ : IsGalois k ↥L₁
L₂ : IntermediateField k K
finiteDimensional✝ : FiniteDimensional k ↥L₂
isGalois✝ : IsGalois k ↥L₂
g : op { toIntermediateField := L₂, finiteDimensional := finiteDimensional✝, isGalois := isGalois✝ } ⟶ op L₃
f :
  op { toIntermediateField := L₁, finiteDimensional := finiteDimensional✝¹, isGalois := isGalois✝¹ } ⟶
    op { toIntermediateField := L₂, finiteDimensional := finiteDimensional✝, isGalois := isGalois✝ }
⊢ finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g

Tactic:
induction L₃ with

Goal state after:
case op.op.op.mk.mk.mk
k : Type u_1
K : Type u_2
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
L₁ : IntermediateField k K
finiteDimensional✝² : FiniteDimensional k ↥L₁
isGalois✝² : IsGalois k ↥L₁
L₂ : IntermediateField k K
finiteDimensional✝¹ : FiniteDimensional k ↥L₂
isGalois✝¹ : IsGalois k ↥L₂
f :
  op { toIntermediateField := L₁, finiteDimensional := finiteDimensional✝², isGalois := isGalois✝² } ⟶
    op { toIntermediateField := L₂, finiteDimensional := finiteDimensional✝¹, isGalois := isGalois✝¹ }
L₃ : IntermediateField k K
finiteDimensional✝ : FiniteDimensional k ↥L₃
isGalois✝ : IsGalois k ↥L₃
g :
  op { toIntermediateField := L₂, finiteDimensional := finiteDimensional✝¹, isGalois := isGalois✝¹ } ⟶
    op { toIntermediateField := L₃, finiteDimensional := finiteDimensional✝, isGalois := isGalois✝ }
⊢ finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g
Module: Mathlib.FieldTheory.Galois.Profinite

Goal state before:
pp: k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
g : ↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop
x : K
L : FiniteGaloisIntermediateField k K
hx' : toAlgEquivAux g x ∈ L.toIntermediateField
hx : x ∈ L.toIntermediateField
⊢ ↑⟨toAlgEquivAux g x, hx'⟩ = ↑(((proj L) g) ⟨x, hx⟩)

Tactic:
Subtype.coe_mk,

Goal state after:
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
g : ↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop
x : K
L : FiniteGaloisIntermediateField k K
hx' : toAlgEquivAux g x ∈ L.toIntermediateField
hx : x ∈ L.toIntermediateField
⊢ toAlgEquivAux g x = ↑(((proj L) g) ⟨x, hx⟩)
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✝¹ : PerfectClosure K p
x : ℕ × K
x✝ : IsNilpotent (mk K p x)
n : ℕ
h : ∃ z, (iterateFrobenius K p z) (x.2 ^ p ^ n) = 0
⊢ ∃ z, (iterateFrobenius K p z) x.2 = 0

Tactic:
obtain ⟨m, h⟩ := h

Goal state after:
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x✝¹ : PerfectClosure K p
x : ℕ × K
x✝ : IsNilpotent (mk K p x)
n m : ℕ
h : (iterateFrobenius K p m) (x.2 ^ p ^ n) = 0
⊢ ∃ z, (iterateFrobenius K p z) x.2 = 0
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: 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 : ∀ i ∈ s, H i = H j → ↑(g i) ≠ ↑x
y z : G
⊢ z ∈ y • ↑(H j) → z ∈ ⋃ i ∈ {x ∈ s | H x ≠ H j}, (y * x⁻¹ * g i) • ↑(H i)

Tactic:
hz

Goal state after:
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 : ∀ i ∈ s, H i = H j → ↑(g i) ≠ ↑x
y z : G
hz : z ∈ y • ↑(H j)
⊢ z ∈ ⋃ i ∈ {x ∈ s | H x ≠ H j}, (y * x⁻¹ * g i) • ↑(H i)
Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality

Goal state before:
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:
rw [← Algebra.transcendental_iff_not_isAlgebraic] at hA 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.Transcendental F ↥A
hB : Algebra.Transcendental F ↥B
⊢ Module.rank F ↥(A ⊔ B) ≤ Module.rank F ↥A * Module.rank F ↥B
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
hn : 0 < n
e : α ^ n = a
K : Type u_1 := FractionRing R
i : R →+* K := algebraMap R K
h : Function.Injective ⇑(algebraMap R K)
⊢ Polynomial.map i (X ^ n - C a) = Polynomial.map i (∏ i ∈ Finset.range n, (X - C (ζ ^ i * α)))

Tactic:
simpa only [Polynomial.map_sub, Polynomial.map_pow, map_X, map_C, map_mul, map_pow,
    Polynomial.map_prod, Polynomial.map_mul]
    using X_pow_sub_C_eq_prod' (hζ.map_of_injective h) hn <| map_pow i α n ▸ congrArg i e

Goal state after:
Module: Mathlib.FieldTheory.JacobsonNoether

Goal state before:
pp: 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
n : ℕ
hn : 0 < n
c : D := (⇑((ad (↥k) D) a))^[n] b
hb : c ≠ 0 ∧ (⇑((ad (↥k) D) a))^[n + 1] b = 0
hc_def : c = (⇑((ad (↥k) D) a))^[n] b
x✝ : Invertible c := { invOf := c⁻¹, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }
hc : a * c = c * a
d : D := c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b
hd_def : d = c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b
hc' : c⁻¹ * a = a * c⁻¹
c_eq : a * (⇑((ad (↥k) D) a))^[n - 1] b - (⇑((ad (↥k) D) a))^[n - 1] b * a = c
eq1 : c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b - c⁻¹ * (⇑((ad (↥k) D) a))^[n - 1] b * a = 1
⊢ False

Tactic:
have deq : a * d - d * a = a := by
    nth_rw 3 [← mul_one a]
    rw [hd_def, ← eq1, mul_sub, mul_assoc _ _ a, sub_right_inj, hc',
      ← mul_assoc, ← mul_assoc, ← mul_assoc]

Goal state after:
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
n : ℕ
hn : 0 < n
c : D := (⇑((ad (↥k) D) a))^[n] b
hb : c ≠ 0 ∧ (⇑((ad (↥k) D) a))^[n + 1] b = 0
hc_def : c = (⇑((ad (↥k) D) a))^[n] b
x✝ : Invertible c := { invOf := c⁻¹, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }
hc : a * c = c * a
d : D := c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b
hd_def : d = c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b
hc' : c⁻¹ * a = a * c⁻¹
c_eq : a * (⇑((ad (↥k) D) a))^[n - 1] b - (⇑((ad (↥k) D) a))^[n - 1] b * a = c
eq1 : c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b - c⁻¹ * (⇑((ad (↥k) D) a))^[n - 1] b * a = 1
deq : a * d - d * a = a
⊢ False
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: case adjoin_rootSet'
K : Type u
inst✝³ : Field K
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
a : K
α : L
ha : α ^ finrank K L = (algebraMap K L) a
hα : K⟮α⟯ = ⊤
⊢ K⟮α⟯.toSubalgebra ≤ Algebra.adjoin K ((X ^ finrank K L - C a).rootSet L)

Tactic:
IntermediateField.adjoin_simple_toSubalgebra_of_isAlgebraic (IsAlgebraic.of_finite K α)

Goal state after:
case adjoin_rootSet'
K : Type u
inst✝³ : Field K
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
a : K
α : L
ha : α ^ finrank K L = (algebraMap K L) a
hα : K⟮α⟯ = ⊤
⊢ K [α] ≤ Algebra.adjoin K ((X ^ finrank K L - C a).rootSet L)
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

Goal state before:
pp: case h
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
y : ConjRootClass K L
x : L
H : (mk K x).carrier = y.carrier
⊢ mk K x = y

Tactic:
induction y with | h y => ?_

Goal state after:
case h.h
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x y : L
H : (mk K x).carrier = (mk K y).carrier
⊢ mk K x = mk K y