awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Galois.NormalBasis
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
inst_4 : Infinite K
e : Module.Basis (Module.Free.ChooseBasisIndex K L) K L
M : Matrix Gal(L/K) Gal(L/K) (MvPolynomial (Module.Free.ChooseBasisIndex K L) L) :=
  (Matrix.of :
      (a : Gal(L/K) → Gal(L/K) → MvPolynomial (Module.Free.ChooseBasisIndex K L) L) →
        Matrix Gal(L/K) Gal(L/K) (MvPolynomial (Module.Free.ChooseBasisIndex K L) L))
    fun (i j : Gal(L/K)) ↦
    ∑ k : Module.Free.ChooseBasisIndex K L,
      HSMul.hSMul (α := L) (β := MvPolynomial (Module.Free.ChooseBasisIndex K L) L)
        ((i.symm : (a : L) → L) ((j : (a : L) → L) ((e : (a : Module.Free.ChooseBasisIndex K L) → L) k : L) : L) : L)
        (MvPolynomial.X k)
hq :
  Eq (α := Submodule L ((j : Gal(L/K)) → L))
    (Submodule.span L
      (Set.range fun (k : Module.Free.ChooseBasisIndex K L) (j : Gal(L/K)) ↦
        (j : (a : L) → L) ((e : (a : Module.Free.ChooseBasisIndex K L) → L) k : L)))
    ⊤
c : Module.Free.ChooseBasisIndex K L → L
hc : Eq (α := L) ((MvPolynomial.eval c : (a : MvPolynomial (Module.Free.ChooseBasisIndex K L) L) → L) M.det : L) (1 : L)
hM : M.det ≠ 0
b : Module.Free.ChooseBasisIndex K L → K
hb :
  Ne (α := L)
    ((MvPolynomial.eval ((⇑(algebraMap K L) : (a : K) → L) ∘ b) :
          (a : MvPolynomial (Module.Free.ChooseBasisIndex K L) L) → L)
        M.det :
      L)
    (0 : L)
a : Gal(L/K) → K
ha :
  Eq.{u_2 + 1} (α := L)
    (∑ i : Gal(L/K),
      HSMul.hSMul (β := L) (a i)
        ((i : (a : L) → L)
            (∑ k : Module.Free.ChooseBasisIndex K L,
              HSMul.hSMul (β := L) (b k) ((e : (a : Module.Free.ChooseBasisIndex K L) → L) k : L)) :
          L))
    0
simp_rw :
  Eq.{u_2 + 1} (α := Gal(L/K) → L) (fun (x : Gal(L/K)) ↦ ((algebraMap K L : K →+* L) : (a : K) → L) (a x))
    fun (x : Gal(L/K)) ↦ 0
⊢ Eq.{u_2 + 1} (α := Gal(L/K) → L)
    ((fun (x : Gal(L/K) → K) ↦ ((⇑(algebraMap K L : K →+* L) : (a : K) → L) ∘ x : Gal(L/K) → L)) a)
    ((fun (x : Gal(L/K) → K) ↦ ((⇑(algebraMap K L : K →+* L) : (a : K) → L) ∘ x : Gal(L/K) → L)) fun (i : Gal(L/K)) ↦ 0)

Tactic:
simp_rw [Function.comp_def, map_zero]

Premises used: map_zero, Function.comp_def
-- Module: Mathlib.FieldTheory.Galois.NormalBasis
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
inst_4 : Infinite K
e : Module.Basis (Module.Free.ChooseBasisIndex K L) K L
M : Matrix Gal(L/K) Gal(L/K) (MvPolynomial (Module.Free.ChooseBasisIndex K L) L) :=
  (Matrix.of :
      (a : Gal(L/K) → Gal(L/K) → MvPolynomial (Module.Free.ChooseBasisIndex K L) L) →
        Matrix Gal(L/K) Gal(L/K) (MvPolynomial (Module.Free.ChooseBasisIndex K L) L))
    fun (i j : Gal(L/K)) ↦
    ∑ k : Module.Free.ChooseBasisIndex K L,
      HSMul.hSMul (α := L) (β := MvPolynomial (Module.Free.ChooseBasisIndex K L) L)
        ((i.symm : (a : L) → L) ((j : (a : L) → L) ((e : (a : Module.Free.ChooseBasisIndex K L) → L) k : L) : L) : L)
        (MvPolynomial.X k)
hq :
  Eq (α := Submodule L ((j : Gal(L/K)) → L))
    (Submodule.span L
      (Set.range fun (k : Module.Free.ChooseBasisIndex K L) (j : Gal(L/K)) ↦
        (j : (a : L) → L) ((e : (a : Module.Free.ChooseBasisIndex K L) → L) k : L)))
    ⊤
c : Module.Free.ChooseBasisIndex K L → L
hc : Eq (α := L) ((MvPolynomial.eval c : (a : MvPolynomial (Module.Free.ChooseBasisIndex K L) L) → L) M.det : L) (1 : L)
hM : M.det ≠ 0
b : Module.Free.ChooseBasisIndex K L → K
hb :
  Ne (α := L)
    ((MvPolynomial.eval ((⇑(algebraMap K L) : (a : K) → L) ∘ b) :
          (a : MvPolynomial (Module.Free.ChooseBasisIndex K L) L) → L)
        M.det :
      L)
    (0 : L)
a : Gal(L/K) → K
ha :
  Eq.{u_2 + 1} (α := L)
    (∑ i : Gal(L/K),
      HSMul.hSMul (β := L) (a i)
        ((i : (a : L) → L)
            (∑ k : Module.Free.ChooseBasisIndex K L,
              HSMul.hSMul (β := L) (b k) ((e : (a : Module.Free.ChooseBasisIndex K L) → L) k : L)) :
          L))
    0
rw :
  ∀
    (hb :
      Ne (α := L)
        (Matrix.det
          (M.map
            (⇑(MvPolynomial.eval ((⇑(algebraMap K L) : (a : K) → L) ∘ b)) :
              (a : MvPolynomial (Module.Free.ChooseBasisIndex K L) L) → L)))
        0)
    (a : Gal(L/K) → K)
    (ha :
      Eq.{u_2 + 1} (α := L)
        (∑ i : Gal(L/K),
          HSMul.hSMul (β := L) (a i)
            ((i : (a : L) → L)
                (∑ k : Module.Free.ChooseBasisIndex K L,
                  HSMul.hSMul (β := L) (b k) ((e : (a : Module.Free.ChooseBasisIndex K L) → L) k : L)) :
              L))
        0),
    Eq.{u_2 + 1} (α := Gal(L/K) → L) (fun (x : Gal(L/K)) ↦ ((algebraMap K L : K →+* L) : (a : K) → L) (a x))
      fun (x : Gal(L/K)) ↦ 0
⊢ Eq.{u_2 + 1} (α := Gal(L/K) → L) (fun (x : Gal(L/K)) ↦ ((algebraMap K L : K →+* L) : (a : K) → L) (a x))
    fun (x : Gal(L/K)) ↦ 0

Tactic:
rw [RingHom.map_det, RingHom.mapMatrix_apply] at hb

Premises used: RingHom.mapMatrix_apply, RingHom.map_det
-- Module: Mathlib.FieldTheory.Galois.NormalBasis
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
inst_4 : Infinite K
e : Module.Basis (Module.Free.ChooseBasisIndex K L) K L
M : Matrix Gal(L/K) Gal(L/K) (MvPolynomial (Module.Free.ChooseBasisIndex K L) L) :=
  (Matrix.of :
      (a : Gal(L/K) → Gal(L/K) → MvPolynomial (Module.Free.ChooseBasisIndex K L) L) →
        Matrix Gal(L/K) Gal(L/K) (MvPolynomial (Module.Free.ChooseBasisIndex K L) L))
    fun (i j : Gal(L/K)) ↦
    ∑ k : Module.Free.ChooseBasisIndex K L,
      HSMul.hSMul (α := L) (β := MvPolynomial (Module.Free.ChooseBasisIndex K L) L)
        ((i.symm : (a : L) → L) ((j : (a : L) → L) ((e : (a : Module.Free.ChooseBasisIndex K L) → L) k : L) : L) : L)
        (MvPolynomial.X k)
hq :
  Eq (α := Submodule L ((j : Gal(L/K)) → L))
    (Submodule.span L
      (Set.range fun (k : Module.Free.ChooseBasisIndex K L) (j : Gal(L/K)) ↦
        (j : (a : L) → L) ((e : (a : Module.Free.ChooseBasisIndex K L) → L) k : L)))
    ⊤
c : Module.Free.ChooseBasisIndex K L → L
hc : Eq (α := L) ((MvPolynomial.eval c : (a : MvPolynomial (Module.Free.ChooseBasisIndex K L) L) → L) M.det : L) (1 : L)
hM : M.det ≠ 0
b : Module.Free.ChooseBasisIndex K L → K
hb :
  Ne (α := L)
    (Matrix.det
      (M.map
        (⇑(MvPolynomial.eval ((⇑(algebraMap K L) : (a : K) → L) ∘ b)) :
          (a : MvPolynomial (Module.Free.ChooseBasisIndex K L) L) → L)))
    0
a : Gal(L/K) → K
ha :
  Eq.{u_2 + 1} (α := L)
    (∑ i : Gal(L/K),
      HSMul.hSMul (β := L) (a i)
        ((i : (a : L) → L)
            (∑ k : Module.Free.ChooseBasisIndex K L,
              HSMul.hSMul (β := L) (b k) ((e : (a : Module.Free.ChooseBasisIndex K L) → L) k : L)) :
          L))
    0
⊢ Eq.{u_2 + 1} (α := Gal(L/K) → L) (fun (x : Gal(L/K)) ↦ ((algebraMap K L : K →+* L) : (a : K) → L) (a x))
    fun (x : Gal(L/K)) ↦ 0

Tactic:
Matrix.eq_zero_of_mulVec_eq_zero hb (funext fun i ↦ i.injective ?_)

Premises used: Matrix.eq_zero_of_mulVec_eq_zero, funext, AlgEquiv.injective
-- Module: Mathlib.FieldTheory.Galois.NormalBasis
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
inst_4 : Infinite K
e : Module.Basis (Module.Free.ChooseBasisIndex K L) K L
M : Matrix Gal(L/K) Gal(L/K) (MvPolynomial (Module.Free.ChooseBasisIndex K L) L) :=
  (Matrix.of :
      (a : Gal(L/K) → Gal(L/K) → MvPolynomial (Module.Free.ChooseBasisIndex K L) L) →
        Matrix Gal(L/K) Gal(L/K) (MvPolynomial (Module.Free.ChooseBasisIndex K L) L))
    fun (i j : Gal(L/K)) ↦
    ∑ k : Module.Free.ChooseBasisIndex K L,
      HSMul.hSMul (α := L) (β := MvPolynomial (Module.Free.ChooseBasisIndex K L) L)
        ((i.symm : (a : L) → L) ((j : (a : L) → L) ((e : (a : Module.Free.ChooseBasisIndex K L) → L) k : L) : L) : L)
        (MvPolynomial.X k)
hq :
  Eq (α := Submodule L ((j : Gal(L/K)) → L))
    (Submodule.span L
      (Set.range fun (k : Module.Free.ChooseBasisIndex K L) (j : Gal(L/K)) ↦
        (j : (a : L) → L) ((e : (a : Module.Free.ChooseBasisIndex K L) → L) k : L)))
    ⊤
c : Module.Free.ChooseBasisIndex K L → L
hc : Eq (α := L) ((MvPolynomial.eval c : (a : MvPolynomial (Module.Free.ChooseBasisIndex K L) L) → L) M.det : L) (1 : L)
hM : M.det ≠ 0
b : Module.Free.ChooseBasisIndex K L → K
hb :
  Ne (α := L)
    (Matrix.det
      (M.map
        (⇑(MvPolynomial.eval ((⇑(algebraMap K L) : (a : K) → L) ∘ b)) :
          (a : MvPolynomial (Module.Free.ChooseBasisIndex K L) L) → L)))
    0
a : Gal(L/K) → K
ha :
  Eq.{u_2 + 1} (α := L)
    (∑ i : Gal(L/K),
      HSMul.hSMul (β := L) (a i)
        ((i : (a : L) → L)
            (∑ k : Module.Free.ChooseBasisIndex K L,
              HSMul.hSMul (β := L) (b k) ((e : (a : Module.Free.ChooseBasisIndex K L) → L) k : L)) :
          L))
    0
refine :
  ∀ (i : Gal(L/K)),
    Eq (α := L)
      ((i : (a : L) → L)
          (Matrix.mulVec
            (M.map
              (⇑(MvPolynomial.eval ((⇑(algebraMap K L) : (a : K) → L) ∘ b)) :
                (a : MvPolynomial (Module.Free.ChooseBasisIndex K L) L) → L))
            (fun (x : Gal(L/K)) ↦ ((algebraMap K L : K →+* L) : (a : K) → L) (a x)) i) :
        L)
      ((i : (a : L) → L) (0 i) : L)
⊢ Eq.{u_2 + 1} (α := Gal(L/K) → L) (fun (x : Gal(L/K)) ↦ ((algebraMap K L : K →+* L) : (a : K) → L) (a x))
    fun (x : Gal(L/K)) ↦ 0

Tactic:
refine Matrix.eq_zero_of_mulVec_eq_zero hb (funext fun i ↦ i.injective ?_)

Premises used: Matrix.eq_zero_of_mulVec_eq_zero, funext, AlgEquiv.injective
-- Module: Mathlib.FieldTheory.Galois.NormalBasis
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
inst_4 : Infinite K
e : Module.Basis (Module.Free.ChooseBasisIndex K L) K L
M : Matrix Gal(L/K) Gal(L/K) (MvPolynomial (Module.Free.ChooseBasisIndex K L) L) :=
  (Matrix.of :
      (a : Gal(L/K) → Gal(L/K) → MvPolynomial (Module.Free.ChooseBasisIndex K L) L) →
        Matrix Gal(L/K) Gal(L/K) (MvPolynomial (Module.Free.ChooseBasisIndex K L) L))
    fun (i j : Gal(L/K)) ↦
    ∑ k : Module.Free.ChooseBasisIndex K L,
      HSMul.hSMul (α := L) (β := MvPolynomial (Module.Free.ChooseBasisIndex K L) L)
        ((i.symm : (a : L) → L) ((j : (a : L) → L) ((e : (a : Module.Free.ChooseBasisIndex K L) → L) k : L) : L) : L)
        (MvPolynomial.X k)
hq :
  Eq (α := Submodule L ((j : Gal(L/K)) → L))
    (Submodule.span L
      (Set.range fun (k : Module.Free.ChooseBasisIndex K L) (j : Gal(L/K)) ↦
        (j : (a : L) → L) ((e : (a : Module.Free.ChooseBasisIndex K L) → L) k : L)))
    ⊤
c : Module.Free.ChooseBasisIndex K L → L
hc : Eq (α := L) ((MvPolynomial.eval c : (a : MvPolynomial (Module.Free.ChooseBasisIndex K L) L) → L) M.det : L) (1 : L)
hM : M.det ≠ 0
b : Module.Free.ChooseBasisIndex K L → K
hb :
  Ne (α := L)
    (Matrix.det
      (M.map
        (⇑(MvPolynomial.eval ((⇑(algebraMap K L) : (a : K) → L) ∘ b)) :
          (a : MvPolynomial (Module.Free.ChooseBasisIndex K L) L) → L)))
    0
a : Gal(L/K) → K
ha :
  Eq.{u_2 + 1} (α := L)
    (∑ i : Gal(L/K),
      HSMul.hSMul (β := L) (a i)
        ((i : (a : L) → L)
            (∑ k : Module.Free.ChooseBasisIndex K L,
              HSMul.hSMul (β := L) (b k) ((e : (a : Module.Free.ChooseBasisIndex K L) → L) k : L)) :
          L))
    0
i : Gal(L/K)
⊢ Eq (α := L)
    ((i : (a : L) → L)
        (Matrix.mulVec
          (Matrix.map (α := MvPolynomial (Module.Free.ChooseBasisIndex K L) L)
            ((Matrix.of :
                (a : Gal(L/K) → Gal(L/K) → MvPolynomial (Module.Free.ChooseBasisIndex K L) L) →
                  Matrix Gal(L/K) Gal(L/K) (MvPolynomial (Module.Free.ChooseBasisIndex K L) L))
              fun (i j : Gal(L/K)) ↦
              ∑ k : Module.Free.ChooseBasisIndex K L,
                HSMul.hSMul (α := L) (β := MvPolynomial (Module.Free.ChooseBasisIndex K L) L)
                  ((i.symm : (a : L) → L)
                      ((j : (a : L) → L) ((e : (a : Module.Free.ChooseBasisIndex K L) → L) k : L) : L) :
                    L)
                  (MvPolynomial.X k))
            (⇑(MvPolynomial.eval ((⇑(algebraMap K L) : (a : K) → L) ∘ b)) :
              (a : MvPolynomial (Module.Free.ChooseBasisIndex K L) L) → L))
          (fun (x : Gal(L/K)) ↦ ((algebraMap K L : K →+* L) : (a : K) → L) (a x)) i) :
      L)
    (∑ i : Gal(L/K),
        HSMul.hSMul (β := L) (a i)
          ((i : (a : L) → L)
              (∑ k : Module.Free.ChooseBasisIndex K L,
                HSMul.hSMul (β := L) (b k) ((e : (a : Module.Free.ChooseBasisIndex K L) → L) k : L)) :
            L) :
      L)

Tactic:
simp [Algebra.smul_def, Matrix.mulVec_eq_sum, mul_comm]

Premises used: Matrix.mulVec_eq_sum, mul_comm, Algebra.smul_def
-- Module: Mathlib.FieldTheory.Galois.NormalBasis
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
inl : ∀ (h : Finite K), ∃ (x : L), LinearIndependent K (M := L) fun (σ : Gal(L/K)) ↦ (σ : (a : L) → L) x
inr : ∀ (h : Infinite K), ∃ (x : L), LinearIndependent K (M := L) fun (σ : Gal(L/K)) ↦ (σ : (a : L) → L) x
⊢ ∃ (x : L), LinearIndependent K (M := L) fun (σ : Gal(L/K)) ↦ (σ : (a : L) → L) x

Tactic:
obtain h | h := finite_or_infinite K

Premises used: finite_or_infinite
-- Module: Mathlib.FieldTheory.Galois.NormalBasis
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
h : Finite K
⊢ Finite L

Tactic:
have := Module.finite_of_finite K (M := L)
-- Module: Mathlib.FieldTheory.Galois.NormalBasis
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
h : Finite K
this : Finite L
⊢ ∃ (x : L), LinearIndependent K (M := L) fun (σ : Gal(L/K)) ↦ (σ : (a : L) → L) x

Tactic:
exists_linearIndependent_algEquiv_apply_of_finite K L

Premises used: _private.0.exists_linearIndependent_algEquiv_apply_of_finite
-- Module: Mathlib.FieldTheory.Galois.NormalBasis
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
h : Finite K
this : Finite L
⊢ ∃ (x : L), LinearIndependent K (M := L) fun (σ : Gal(L/K)) ↦ (σ : (a : L) → L) x

Tactic:
exact exists_linearIndependent_algEquiv_apply_of_finite K L

Premises used: _private.0.exists_linearIndependent_algEquiv_apply_of_finite
-- Module: Mathlib.FieldTheory.Galois.NormalBasis
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
h : Infinite K
⊢ ∃ (x : L), LinearIndependent K (M := L) fun (σ : Gal(L/K)) ↦ (σ : (a : L) → L) x

Tactic:
exists_linearIndependent_algEquiv_apply_of_infinite K L

Premises used: _private.0.exists_linearIndependent_algEquiv_apply_of_infinite
-- Module: Mathlib.FieldTheory.Galois.NormalBasis
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
h : Infinite K
⊢ ∃ (x : L), LinearIndependent K (M := L) fun (σ : Gal(L/K)) ↦ (σ : (a : L) → L) x

Tactic:
exact exists_linearIndependent_algEquiv_apply_of_infinite K L

Premises used: _private.0.exists_linearIndependent_algEquiv_apply_of_infinite
-- Module: Mathlib.FieldTheory.Galois.Profinite
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : (FiniteGaloisIntermediateField k K)ᵒᵖ
⊢ finGaloisGroupMap (𝟙 L) = 𝟙 (unop L).finGaloisGroup

Tactic:
ConcreteCategory.ext (AlgEquiv.restrictNormalHom_id _ _)

Premises used: CategoryTheory.ConcreteCategory.ext, AlgEquiv.restrictNormalHom_id
-- Module: Mathlib.FieldTheory.Galois.Profinite
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L₂ L₃ : (FiniteGaloisIntermediateField k K)ᵒᵖ
g : L₂ ⟶ L₃
L₁ : FiniteGaloisIntermediateField k K
f : op L₁ ⟶ L₂
⊢ finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g

Tactic:
?_
-- Module: Mathlib.FieldTheory.Galois.Profinite
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L₁ L₂ L₃ : (FiniteGaloisIntermediateField k K)ᵒᵖ
f : L₁ ⟶ L₂
g : L₂ ⟶ L₃
op :
  ∀ (L₁ : FiniteGaloisIntermediateField k K) (f : Opposite.op L₁ ⟶ L₂),
    finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g
⊢ finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g

Tactic:
induction L₁ with | _ L₁ => ?_
-- Module: Mathlib.FieldTheory.Galois.Profinite
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : 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:
?_
-- Module: Mathlib.FieldTheory.Galois.Profinite
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L₂ L₃ : (FiniteGaloisIntermediateField k K)ᵒᵖ
g : L₂ ⟶ L₃
L₁ : FiniteGaloisIntermediateField k K
f : Opposite.op L₁ ⟶ L₂
op :
  ∀ (L₂ : FiniteGaloisIntermediateField k K) (g : Opposite.op L₂ ⟶ L₃) (f : Opposite.op L₁ ⟶ Opposite.op L₂),
    finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g
⊢ finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g

Tactic:
induction L₂ with | _ L₂ => ?_
-- Module: Mathlib.FieldTheory.Galois.Profinite
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : 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

Tactic:
?_
-- Module: Mathlib.FieldTheory.Galois.Profinite
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L₃ : (FiniteGaloisIntermediateField k K)ᵒᵖ
L₁ L₂ : FiniteGaloisIntermediateField k K
g : Opposite.op L₂ ⟶ L₃
f : Opposite.op L₁ ⟶ Opposite.op L₂
op :
  ∀ (L₃ : FiniteGaloisIntermediateField k K) (g : Opposite.op L₂ ⟶ Opposite.op L₃),
    finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g
⊢ finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g

Tactic:
induction L₃ with | _ L₃ => ?_
-- Module: Mathlib.FieldTheory.Galois.Profinite
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L₂ L₃ : FiniteGaloisIntermediateField k K
g : op L₂ ⟶ op L₃
L₁ : IntermediateField k K
finiteDimensional : FiniteDimensional.{u_1, u_2} k ↥L₁
isGalois : IsGalois.{u_1, u_2} k ↥L₁
f :
  op
      { toIntermediateField := L₁, finiteDimensional := finiteDimensional, isGalois := isGalois :
        FiniteGaloisIntermediateField k K } ⟶
    op L₂
⊢ finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g

Tactic:
?_
-- Module: Mathlib.FieldTheory.Galois.Profinite
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L₁ L₂ : FiniteGaloisIntermediateField k K
f : Opposite.op L₁ ⟶ Opposite.op L₂
L₃ : FiniteGaloisIntermediateField k K
g : Opposite.op L₂ ⟶ Opposite.op L₃
op :
  ∀ (L₁ : IntermediateField k K) [finiteDimensional : FiniteDimensional.{u_1, u_2} k ↥L₁]
    [isGalois : IsGalois.{u_1, u_2} k ↥L₁]
    (f :
      Opposite.op
          { toIntermediateField := L₁, finiteDimensional := finiteDimensional, isGalois := isGalois :
            FiniteGaloisIntermediateField k K } ⟶
        Opposite.op L₂),
    finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g
⊢ finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g

Tactic:
induction L₁ with | _ L₁ => ?_
-- Module: Mathlib.FieldTheory.Galois.Profinite
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L₃ : FiniteGaloisIntermediateField k K
L₁ : IntermediateField k K
finiteDimensional : FiniteDimensional.{u_1, u_2} k ↥L₁
isGalois : IsGalois.{u_1, u_2} k ↥L₁
L₂ : IntermediateField k K
finiteDimensional_1 : FiniteDimensional.{u_1, u_2} k ↥L₂
isGalois_1 : IsGalois.{u_1, u_2} k ↥L₂
g :
  op
      { toIntermediateField := L₂, finiteDimensional := finiteDimensional_1, isGalois := isGalois_1 :
        FiniteGaloisIntermediateField k K } ⟶
    op L₃
f :
  op
      { toIntermediateField := L₁, finiteDimensional := finiteDimensional, isGalois := isGalois :
        FiniteGaloisIntermediateField k K } ⟶
    op { toIntermediateField := L₂, finiteDimensional := finiteDimensional_1, isGalois := isGalois_1 }
⊢ finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g

Tactic:
?_
-- Module: Mathlib.FieldTheory.Galois.Profinite
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L₂ L₃ : FiniteGaloisIntermediateField k K
g : Opposite.op L₂ ⟶ Opposite.op L₃
L₁ : IntermediateField k K
finiteDimensional : FiniteDimensional.{u_1, u_2} k ↥L₁
isGalois : IsGalois.{u_1, u_2} k ↥L₁
f :
  Opposite.op
      { toIntermediateField := L₁, finiteDimensional := finiteDimensional, isGalois := isGalois :
        FiniteGaloisIntermediateField k K } ⟶
    Opposite.op L₂
op :
  ∀ (L₂ : IntermediateField k K) [finiteDimensional_1 : FiniteDimensional.{u_1, u_2} k ↥L₂]
    [isGalois_1 : IsGalois.{u_1, u_2} k ↥L₂]
    (g :
      Opposite.op
          { toIntermediateField := L₂, finiteDimensional := finiteDimensional_1, isGalois := isGalois_1 :
            FiniteGaloisIntermediateField k K } ⟶
        Opposite.op L₃)
    (f :
      Opposite.op
          { toIntermediateField := L₁, finiteDimensional := finiteDimensional, isGalois := isGalois :
            FiniteGaloisIntermediateField k K } ⟶
        Opposite.op { toIntermediateField := L₂, finiteDimensional := finiteDimensional_1, isGalois := isGalois_1 }),
    finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g
⊢ finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g

Tactic:
induction L₂ with | _ L₂ => ?_
-- Module: Mathlib.FieldTheory.Galois.Profinite
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L₁ : IntermediateField k K
finiteDimensional : FiniteDimensional.{u_1, u_2} k ↥L₁
isGalois : IsGalois.{u_1, u_2} k ↥L₁
L₂ : IntermediateField k K
finiteDimensional_1 : FiniteDimensional.{u_1, u_2} k ↥L₂
isGalois_1 : IsGalois.{u_1, u_2} k ↥L₂
f :
  op
      { toIntermediateField := L₁, finiteDimensional := finiteDimensional, isGalois := isGalois :
        FiniteGaloisIntermediateField k K } ⟶
    op { toIntermediateField := L₂, finiteDimensional := finiteDimensional_1, isGalois := isGalois_1 }
L₃ : IntermediateField k K
finiteDimensional_2 : FiniteDimensional.{u_1, u_2} k ↥L₃
isGalois_2 : IsGalois.{u_1, u_2} k ↥L₃
g :
  op
      { toIntermediateField := L₂, finiteDimensional := finiteDimensional_1, isGalois := isGalois_1 :
        FiniteGaloisIntermediateField k K } ⟶
    op { toIntermediateField := L₃, finiteDimensional := finiteDimensional_2, isGalois := isGalois_2 }
⊢ finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g

Tactic:
?_
-- Module: Mathlib.FieldTheory.Galois.Profinite
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L₃ : FiniteGaloisIntermediateField k K
L₁ : IntermediateField k K
finiteDimensional : FiniteDimensional.{u_1, u_2} k ↥L₁
isGalois : IsGalois.{u_1, u_2} k ↥L₁
L₂ : IntermediateField k K
finiteDimensional_1 : FiniteDimensional.{u_1, u_2} k ↥L₂
isGalois_1 : IsGalois.{u_1, u_2} k ↥L₂
g :
  Opposite.op
      { toIntermediateField := L₂, finiteDimensional := finiteDimensional_1, isGalois := isGalois_1 :
        FiniteGaloisIntermediateField k K } ⟶
    Opposite.op L₃
f :
  Opposite.op
      { toIntermediateField := L₁, finiteDimensional := finiteDimensional, isGalois := isGalois :
        FiniteGaloisIntermediateField k K } ⟶
    Opposite.op { toIntermediateField := L₂, finiteDimensional := finiteDimensional_1, isGalois := isGalois_1 }
op :
  ∀ (L₃ : IntermediateField k K) [finiteDimensional_2 : FiniteDimensional.{u_1, u_2} k ↥L₃]
    [isGalois_2 : IsGalois.{u_1, u_2} k ↥L₃]
    (g :
      Opposite.op
          { toIntermediateField := L₂, finiteDimensional := finiteDimensional_1, isGalois := isGalois_1 :
            FiniteGaloisIntermediateField k K } ⟶
        Opposite.op { toIntermediateField := L₃, finiteDimensional := finiteDimensional_2, isGalois := isGalois_2 }),
    finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g
⊢ finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g

Tactic:
induction L₃ with | _ L₃ => ?_