mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ False

Tactic:
have hc' : c⁻¹ * a = a * c⁻¹ := by
    apply_fun (c⁻¹ * · * c⁻¹) at hc
    rw [mul_assoc, mul_assoc, mul_inv_cancel₀ hb.1, mul_one, ← mul_assoc,
      inv_mul_cancel₀ hb.1, one_mul] at hc
    exact hc

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⁻¹
⊢ False
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
⊢ c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b - c⁻¹ * (⇑((ad (↥k) D) a))^[n - 1] b * a = 1

Tactic:
[

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
⊢ c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b - c⁻¹ * (⇑((ad (↥k) D) a))^[n - 1] b * a = 1
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.Transcendental F ↥A
hB : Algebra.Transcendental F ↥B
this✝¹ : Algebra.Transcendental F ↥(A ⊔ B)
this✝ : Infinite ↥A
this : Infinite ↥B
⊢ Module.rank F ↥(A ⊔ B) ≤ Module.rank F ↥A * Module.rank F ↥B

Tactic:
[

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
this✝¹ : Algebra.Transcendental F ↥(A ⊔ B)
this✝ : Infinite ↥A
this : Infinite ↥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
σ : Gal(K[n√a]/K)
this : Fact (Irreducible (X ^ n - C a))
⊢ (if a = 0 then root (X ^ n - C a) else σ (root (X ^ n - C a)) / root (X ^ n - C a) * root (X ^ n - C a)) =
    σ (root (X ^ n - C a))

Tactic:
[

Goal state after:
K : Type u
inst✝¹ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
inst✝ : NeZero n
σ : Gal(K[n√a]/K)
this : Fact (Irreducible (X ^ n - C a))
⊢ (if a = 0 then root (X ^ n - C a) else σ (root (X ^ n - C a)) / root (X ^ n - C a) * root (X ^ n - C a)) =
    σ (root (X ^ n - C a))
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: 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
inst✝¹ : IsGalois K L
inst✝ : IsCyclic Gal(L/K)
ζ : K
hζ : IsPrimitiveRoot ζ (finrank K L)
σ : Gal(L/K)
hσ : Function.Surjective fun x ↦ σ ^ x
hσ' : orderOf σ = Nat.card Gal(L/K)
this : (minpoly K σ.toLinearMap).IsRoot ζ
v : L
hv : End.HasEigenvector σ.toLinearMap ζ v
hv' : ∀ (n : ℕ), (σ.toLinearMap ^ n) v = ζ ^ n • v
⊢ ∃ α, α ^ finrank K L ∈ Set.range ⇑(algebraMap K L) ∧ K⟮α⟯ = ⊤

Tactic:
[

Goal state after:
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
inst✝¹ : IsGalois K L
inst✝ : IsCyclic Gal(L/K)
ζ : K
hζ : IsPrimitiveRoot ζ (finrank K L)
σ : Gal(L/K)
hσ : Function.Surjective fun x ↦ σ ^ x
hσ' : orderOf σ = Nat.card Gal(L/K)
this : (minpoly K σ.toLinearMap).IsRoot ζ
v : L
hv : End.HasEigenvector σ.toLinearMap ζ v
hv' : ∀ (n : ℕ), (σ.toLinearMap ^ n) v = ζ ^ n • v
⊢ ∃ α, α ^ finrank K L ∈ Set.range ⇑(algebraMap K L) ∧ K⟮α⟯ = ⊤
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⟮α⟯ = ⊤
⊢ eval₂ (algebraMap K L) α (X ^ finrank K L) - eval₂ (algebraMap K L) α (C a) = 0

Tactic:
eval₂_X_pow,

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⟮α⟯ = ⊤
⊢ α ^ finrank K L - eval₂ (algebraMap K L) α (C a) = 0
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
A B : Subalgebra R S
ι : Type u_1
a : ι → ↥A
⊢ (Submodule.mulLeftMap (toSubmodule B) a).ker = ⊥ ↔ LinearIndependent (↥B.op) (MulOpposite.op ∘ ⇑A.val ∘ a)

Tactic:
[

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
A B : Subalgebra R S
ι : Type u_1
a : ι → ↥A
⊢ (Submodule.mulLeftMap (toSubmodule B) a).ker = ⊥ ↔ LinearIndependent (↥B.op) (MulOpposite.op ∘ ⇑A.val ∘ a)
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
A B : Subalgebra R S
ι : Type u_1
a : ι → ↥A
i : (ι →₀ ↥B) →ₗ[R] S := Submodule.mulLeftMap (toSubmodule B) a
j : (ι →₀ ↥B) →ₗ[R] S :=
  ↑(MulOpposite.opLinearEquiv R).symm ∘ₗ
    ↑R (Finsupp.linearCombination (↥B.op) (MulOpposite.op ∘ ⇑A.val ∘ a)) ∘ₗ
      ↑(Finsupp.mapRange.linearEquiv B.linearEquivOp)
this : i = j
⊢ Function.Injective ⇑i ↔ Function.Injective ⇑(Finsupp.linearCombination (↥B.op) (MulOpposite.op ∘ ⇑A.val ∘ a))

Tactic:
[

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
A B : Subalgebra R S
ι : Type u_1
a : ι → ↥A
i : (ι →₀ ↥B) →ₗ[R] S := Submodule.mulLeftMap (toSubmodule B) a
j : (ι →₀ ↥B) →ₗ[R] S :=
  ↑(MulOpposite.opLinearEquiv R).symm ∘ₗ
    ↑R (Finsupp.linearCombination (↥B.op) (MulOpposite.op ∘ ⇑A.val ∘ a)) ∘ₗ
      ↑(Finsupp.mapRange.linearEquiv B.linearEquivOp)
this : i = j
⊢ Function.Injective ⇑i ↔ Function.Injective ⇑(Finsupp.linearCombination (↥B.op) (MulOpposite.op ∘ ⇑A.val ∘ a))
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
A B : Subalgebra R S
ι : Type u_1
b : ι → ↥B
⊢ ((toSubmodule A).mulRightMap b).ker = ⊥ ↔ LinearIndependent (↥A) (⇑B.val ∘ b)

Tactic:
[

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
A B : Subalgebra R S
ι : Type u_1
b : ι → ↥B
⊢ ((toSubmodule A).mulRightMap b).ker = ⊥ ↔ LinearIndependent (↥A) (⇑B.val ∘ b)
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
A B : Subalgebra R S
ι : Type u_1
b : ι → ↥B
i : (ι →₀ ↥A) →ₗ[R] S := (toSubmodule A).mulRightMap b
j : (ι →₀ ↥A) →ₗ[R] S := ↑R (Finsupp.linearCombination (↥A) (⇑B.val ∘ b))
this : i = j
⊢ Function.Injective ⇑i ↔ Function.Injective ⇑j

Tactic:
this

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
A B : Subalgebra R S
ι : Type u_1
b : ι → ↥B
i : (ι →₀ ↥A) →ₗ[R] S := (toSubmodule A).mulRightMap b
j : (ι →₀ ↥A) →ₗ[R] S := ↑R (Finsupp.linearCombination (↥A) (⇑B.val ∘ b))
this : i = j
⊢ Function.Injective ⇑j ↔ Function.Injective ⇑j
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: k : Type u_1
E : Type u_2
inst✝⁴ : DivisionRing k
inst✝³ : Infinite k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
ι : Sort u_3
inst✝ : Finite ι
p : ι → Subspace k E
hcovers : ⋃ i, ↑(p i) = Set.univ
this : Fintype ↑(Set.range p)
⊢ ∃ i, p i = ⊤

Tactic:
[

Goal state after:
k : Type u_1
E : Type u_2
inst✝⁴ : DivisionRing k
inst✝³ : Infinite k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
ι : Sort u_3
inst✝ : Finite ι
p : ι → Subspace k E
hcovers : ⋃ i, ↑(p i) = Set.univ
this : Fintype ↑(Set.range p)
⊢ ∃ i, p i = ⊤
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
⊢ mk K x = 0 ↔ x = 0

Tactic:
eq_comm (b := 0),

Goal state after:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
⊢ 0 = mk K x ↔ x = 0
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

Goal state before:
pp: 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

Tactic:
[

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
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x y : ConjRootClass K L
⊢ (∃ a ∈ x.carrier, ∃ b ∈ y.carrier, a + b = 0) ↔ x = -y

Tactic:
[

Goal state after:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x y : ConjRootClass K L
⊢ (∃ a ∈ x.carrier, ∃ b ∈ y.carrier, a + b = 0) ↔ x = -y
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x y : ConjRootClass K L
⊢ (∃ a ∈ x.carrier, ∃ b ∈ y.carrier, a + b = 0) ↔ x = -y

Tactic:
by
  simp_rw [mem_carrier]
  constructor
  · rintro ⟨a, rfl, b, rfl, h⟩
    rw [mk_neg, mk_eq_mk, add_eq_zero_iff_eq_neg.mp h]
  · rintro rfl
    induction y with
    | h y => exact ⟨-y, mk_neg y, y, rfl, neg_add_cancel _⟩

Goal state after:
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
H' : A ⊔ B = ⊤
inst✝¹ : Free R ↥B
inst✝ : Module.Finite R ↥B
x : ↥B
⊢ (Algebra.trace (↥A) S) ((algebraMap (↥B) S) x) = (algebraMap R ↥A) ((Algebra.trace R ↥B) x)

Tactic:
[

Goal state after:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
H' : A ⊔ B = ⊤
inst✝¹ : Free R ↥B
inst✝ : Module.Finite R ↥B
x : ↥B
⊢ (Algebra.trace (↥A) S) ((algebraMap (↥B) S) x) = (algebraMap R ↥A) ((Algebra.trace R ↥B) x)
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsSeparable K L
c : ConjRootClass K L
inst✝ : Fintype ↑c.carrier
⊢ c.minpoly.aroots L = c.carrier.toFinset.val

Tactic:
[

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsSeparable K L
c : ConjRootClass K L
inst✝ : Fintype ↑c.carrier
⊢ c.minpoly.aroots L = c.carrier.toFinset.val
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Algebra.IsSeparable K L
inst✝¹ : Normal K L
c : ConjRootClass K L
inst✝ : Fintype ↑c.carrier
⊢ map (algebraMap K L) c.minpoly = ∏ x ∈ c.carrier.toFinset, (X - C x)

Tactic:
[

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Algebra.IsSeparable K L
inst✝¹ : Normal K L
c : ConjRootClass K L
inst✝ : Fintype ↑c.carrier
⊢ map (algebraMap K L) c.minpoly = ∏ x ∈ c.carrier.toFinset, (X - C x)
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
H' : A ⊔ B = ⊤
inst✝¹ : Free R ↥B
inst✝ : Module.Finite R ↥B
x : ↥B
⊢ (Algebra.norm ↥A) ((algebraMap (↥B) S) x) = (algebraMap R ↥A) ((Algebra.norm R) x)

Tactic:
[

Goal state after:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
H' : A ⊔ B = ⊤
inst✝¹ : Free R ↥B
inst✝ : Module.Finite R ↥B
x : ↥B
⊢ (Algebra.norm ↥A) ((algebraMap (↥B) S) x) = (algebraMap R ↥A) ((Algebra.norm R) x)
Module: Mathlib.FieldTheory.NormalizedTrace

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Algebra F K
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
f : E →ₐ[F] K
a : E
e : ↥F⟮a⟯ ≃ₐ[F] ↥F⟮f a⟯ := (F⟮a⟯.equivMap f).trans (equivOfEq ⋯)
⊢ normalizedTraceAux F K (f a) = normalizedTraceAux F E a

Tactic:
[

Goal state after:
F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Algebra F K
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
f : E →ₐ[F] K
a : E
e : ↥F⟮a⟯ ≃ₐ[F] ↥F⟮f a⟯ := (F⟮a⟯.equivMap f).trans (equivOfEq ⋯)
⊢ normalizedTraceAux F K (f a) = normalizedTraceAux F E a
Module: Mathlib.FieldTheory.LinearDisjoint

Goal state before:
pp: F : Type u
E : Type v
inst✝²⁰ : Field F
inst✝¹⁹ : Field E
inst✝¹⁸ : Algebra F E
L : Type w
inst✝¹⁷ : Field L
inst✝¹⁶ : Algebra F L
inst✝¹⁵ : Algebra L E
inst✝¹⁴ : IsScalarTower F L E
L' : Type u_1
inst✝¹³ : Field L'
inst✝¹² : Algebra F L'
inst✝¹¹ : Algebra L' E
inst✝¹⁰ : IsScalarTower F L' E
H : (IsScalarTower.toAlgHom F L E).fieldRange.LinearDisjoint (IsScalarTower.toAlgHom F L' E).range
K : Type u_2
inst✝⁹ : Field K
inst✝⁸ : Algebra F K
inst✝⁷ : Algebra L K
inst✝⁶ : IsScalarTower F L K
inst✝⁵ : Algebra L' K
inst✝⁴ : IsScalarTower F L' K
inst✝³ : Algebra E K
inst✝² : IsScalarTower F E K
inst✝¹ : IsScalarTower L E K
inst✝ : IsScalarTower L' E K
this :
  (Subalgebra.map (IsScalarTower.toAlgHom F E K) (IsScalarTower.toAlgHom F L E).fieldRange.toSubalgebra).LinearDisjoint
    (Subalgebra.map (IsScalarTower.toAlgHom F E K) (IsScalarTower.toAlgHom F L' E).range)
⊢ (IsScalarTower.toAlgHom F L K).fieldRange.LinearDisjoint (IsScalarTower.toAlgHom F L' K).range

Tactic:
[

Goal state after:
F : Type u
E : Type v
inst✝²⁰ : Field F
inst✝¹⁹ : Field E
inst✝¹⁸ : Algebra F E
L : Type w
inst✝¹⁷ : Field L
inst✝¹⁶ : Algebra F L
inst✝¹⁵ : Algebra L E
inst✝¹⁴ : IsScalarTower F L E
L' : Type u_1
inst✝¹³ : Field L'
inst✝¹² : Algebra F L'
inst✝¹¹ : Algebra L' E
inst✝¹⁰ : IsScalarTower F L' E
H : (IsScalarTower.toAlgHom F L E).fieldRange.LinearDisjoint (IsScalarTower.toAlgHom F L' E).range
K : Type u_2
inst✝⁹ : Field K
inst✝⁸ : Algebra F K
inst✝⁷ : Algebra L K
inst✝⁶ : IsScalarTower F L K
inst✝⁵ : Algebra L' K
inst✝⁴ : IsScalarTower F L' K
inst✝³ : Algebra E K
inst✝² : IsScalarTower F E K
inst✝¹ : IsScalarTower L E K
inst✝ : IsScalarTower L' E K
this :
  (Subalgebra.map (IsScalarTower.toAlgHom F E K) (IsScalarTower.toAlgHom F L E).fieldRange.toSubalgebra).LinearDisjoint
    (Subalgebra.map (IsScalarTower.toAlgHom F E K) (IsScalarTower.toAlgHom F L' E).range)
⊢ (IsScalarTower.toAlgHom F L K).fieldRange.LinearDisjoint (IsScalarTower.toAlgHom F L' K).range
Module: Mathlib.FieldTheory.LinearDisjoint

Goal state before:
pp: F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
H : A.LinearDisjoint L
ι : Type u_1
a : ι → ↥A
ha : LinearIndependent F a
x✝¹ : L
x✝ : E
⊢ (AddMonoidHom.id E) ((AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)) x✝¹ • x✝) =
    x✝¹ • (AddMonoidHom.id E) x✝

Tactic:
[

Goal state after:
F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
H : A.LinearDisjoint L
ι : Type u_1
a : ι → ↥A
ha : LinearIndependent F a
x✝¹ : L
x✝ : E
⊢ (AddMonoidHom.id E) ((AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)) x✝¹ • x✝) =
    x✝¹ • (AddMonoidHom.id E) x✝
Module: Mathlib.FieldTheory.LinearDisjoint

Goal state before:
pp: F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
ι : Type u_1
a : Basis ι F ↥A
H : LinearIndependent L (⇑A.val ∘ ⇑a)
x✝¹ : L
x✝ : E
⊢ (AddMonoidHom.id E) (x✝¹ • x✝) =
    (AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)) x✝¹ • (AddMonoidHom.id E) x✝

Tactic:
[

Goal state after:
F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
ι : Type u_1
a : Basis ι F ↥A
H : LinearIndependent L (⇑A.val ∘ ⇑a)
x✝¹ : L
x✝ : E
⊢ (AddMonoidHom.id E) (x✝¹ • x✝) =
    (AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)) x✝¹ • (AddMonoidHom.id E) x✝
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
inst✝⁸ : CommRing R
A : Type v
inst✝⁷ : CommRing A
B : Type w
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Flat R A
inst✝² : Flat R B
inst✝¹ : Algebra.Transcendental R A
inst✝ : Algebra.Transcendental R B
H : IsField (A ⊗[R] B)
this✝⁴ : Field (A ⊗[R] B) := H.toField
a : A
b : B
ha : Function.Injective ⇑(algebraMap R A)
hb : Function.Injective ⇑(algebraMap R B)
fa : A →ₐ[R] A ⊗[R] B := Algebra.TensorProduct.includeLeft
fb : B →ₐ[R] A ⊗[R] B := Algebra.TensorProduct.includeRight
hfa : Function.Injective ⇑fa
hfb : Function.Injective ⇑fb
this✝³ : IsDomain A
this✝² : IsDomain B
this✝¹ : IsDomain R
this✝ : Flat R ↥(toSubmodule fa.range)
key1 : Module.rank R ↥(fa.range ⊓ fb.range) ≤ 1
ga : R[X] →ₐ[R] A := aeval a
gb : R[X] →ₐ[R] B := aeval b
gab : R[X] →ₐ[R] A ⊗[R] B := fa.comp ga
hta : Function.Injective ⇑ga
htb : Function.Injective ⇑gb
htab : Function.Injective ⇑gab
algInst✝¹ : Algebra R[X] A := ga.toAlgebra
algInst✝ : Algebra R[X] B := gb.toAlgebra
f : A ⊗[R] B →ₐ[R] A ⊗[R[X]] B := Algebra.TensorProduct.mapOfCompatibleSMul R[X] R R A B
this : Nontrivial (A ⊗[R[X]] B)
hf : Function.Injective ⇑f
⊢ gab.range ≤ fa.range ⊓ fb.range

Tactic:
[

Goal state after:
R : Type u
inst✝⁸ : CommRing R
A : Type v
inst✝⁷ : CommRing A
B : Type w
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Flat R A
inst✝² : Flat R B
inst✝¹ : Algebra.Transcendental R A
inst✝ : Algebra.Transcendental R B
H : IsField (A ⊗[R] B)
this✝⁴ : Field (A ⊗[R] B) := H.toField
a : A
b : B
ha : Function.Injective ⇑(algebraMap R A)
hb : Function.Injective ⇑(algebraMap R B)
fa : A →ₐ[R] A ⊗[R] B := Algebra.TensorProduct.includeLeft
fb : B →ₐ[R] A ⊗[R] B := Algebra.TensorProduct.includeRight
hfa : Function.Injective ⇑fa
hfb : Function.Injective ⇑fb
this✝³ : IsDomain A
this✝² : IsDomain B
this✝¹ : IsDomain R
this✝ : Flat R ↥(toSubmodule fa.range)
key1 : Module.rank R ↥(fa.range ⊓ fb.range) ≤ 1
ga : R[X] →ₐ[R] A := aeval a
gb : R[X] →ₐ[R] B := aeval b
gab : R[X] →ₐ[R] A ⊗[R] B := fa.comp ga
hta : Function.Injective ⇑ga
htb : Function.Injective ⇑gb
htab : Function.Injective ⇑gab
algInst✝¹ : Algebra R[X] A := ga.toAlgebra
algInst✝ : Algebra R[X] B := gb.toAlgebra
f : A ⊗[R] B →ₐ[R] A ⊗[R[X]] B := Algebra.TensorProduct.mapOfCompatibleSMul R[X] R R A B
this : Nontrivial (A ⊗[R[X]] B)
hf : Function.Injective ⇑f
⊢ gab.range ≤ fa.range ⊓ fb.range
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
inst✝⁸ : CommRing R
A : Type v
inst✝⁷ : CommRing A
B : Type w
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Flat R A
inst✝² : Flat R B
inst✝¹ : Algebra.Transcendental R A
inst✝ : Algebra.Transcendental R B
H : IsField (A ⊗[R] B)
this✝⁴ : Field (A ⊗[R] B) := H.toField
a : A
b : B
ha : Function.Injective ⇑(algebraMap R A)
hb : Function.Injective ⇑(algebraMap R B)
fa : A →ₐ[R] A ⊗[R] B := Algebra.TensorProduct.includeLeft
fb : B →ₐ[R] A ⊗[R] B := Algebra.TensorProduct.includeRight
hfa : Function.Injective ⇑fa
hfb : Function.Injective ⇑fb
this✝³ : IsDomain A
this✝² : IsDomain B
this✝¹ : IsDomain R
this✝ : Flat R ↥(toSubmodule fa.range)
key1 : Module.rank R ↥(fa.range ⊓ fb.range) ≤ 1
ga : R[X] →ₐ[R] A := aeval a
gb : R[X] →ₐ[R] B := aeval b
gab : R[X] →ₐ[R] A ⊗[R] B := fa.comp ga
hta : Function.Injective ⇑ga
htb : Function.Injective ⇑gb
htab : Function.Injective ⇑gab
algInst✝¹ : Algebra R[X] A := ga.toAlgebra
algInst✝ : Algebra R[X] B := gb.toAlgebra
f : A ⊗[R] B →ₐ[R] A ⊗[R[X]] B := Algebra.TensorProduct.mapOfCompatibleSMul R[X] R R A B
this : Nontrivial (A ⊗[R[X]] B)
hf : Function.Injective ⇑f
⊢ R[a ⊗ₜ[R] 1] ≤ fa.range ⊓ fb.range

Tactic:
[

Goal state after:
R : Type u
inst✝⁸ : CommRing R
A : Type v
inst✝⁷ : CommRing A
B : Type w
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Flat R A
inst✝² : Flat R B
inst✝¹ : Algebra.Transcendental R A
inst✝ : Algebra.Transcendental R B
H : IsField (A ⊗[R] B)
this✝⁴ : Field (A ⊗[R] B) := H.toField
a : A
b : B
ha : Function.Injective ⇑(algebraMap R A)
hb : Function.Injective ⇑(algebraMap R B)
fa : A →ₐ[R] A ⊗[R] B := Algebra.TensorProduct.includeLeft
fb : B →ₐ[R] A ⊗[R] B := Algebra.TensorProduct.includeRight
hfa : Function.Injective ⇑fa
hfb : Function.Injective ⇑fb
this✝³ : IsDomain A
this✝² : IsDomain B
this✝¹ : IsDomain R
this✝ : Flat R ↥(toSubmodule fa.range)
key1 : Module.rank R ↥(fa.range ⊓ fb.range) ≤ 1
ga : R[X] →ₐ[R] A := aeval a
gb : R[X] →ₐ[R] B := aeval b
gab : R[X] →ₐ[R] A ⊗[R] B := fa.comp ga
hta : Function.Injective ⇑ga
htb : Function.Injective ⇑gb
htab : Function.Injective ⇑gab
algInst✝¹ : Algebra R[X] A := ga.toAlgebra
algInst✝ : Algebra R[X] B := gb.toAlgebra
f : A ⊗[R] B →ₐ[R] A ⊗[R[X]] B := Algebra.TensorProduct.mapOfCompatibleSMul R[X] R R A B
this : Nontrivial (A ⊗[R[X]] B)
hf : Function.Injective ⇑f
⊢ R[a ⊗ₜ[R] 1] ≤ fa.range ⊓ fb.range