mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.MvRatFunc.Rank

Goal state before:
pp: case refine_2
σ : Type u
F : Type v
inst✝¹ : Field F
inst✝ : Nonempty σ
R : Type (max v u) := MvPolynomial σ F
K : Type (max u v) := FractionRing R
hinj : Function.Injective ⇑(algebraMap R K)
h1 : max (lift.{v, u} #σ) (lift.{v, u} ℵ₀) ≤ Module.rank F K
⊢ max (max (lift.{u, v} #F) (lift.{v, u} #σ)) ℵ₀ ≤ Module.rank F (FractionRing (MvPolynomial σ F))

Tactic:
lift_aleph0,

Goal state after:
case refine_2
σ : Type u
F : Type v
inst✝¹ : Field F
inst✝ : Nonempty σ
R : Type (max v u) := MvPolynomial σ F
K : Type (max u v) := FractionRing R
hinj : Function.Injective ⇑(algebraMap R K)
h1 : max (lift.{v, u} #σ) ℵ₀ ≤ Module.rank F K
⊢ max (max (lift.{u, v} #F) (lift.{v, u} #σ)) ℵ₀ ≤ Module.rank F (FractionRing (MvPolynomial σ F))
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⁻¹ * c = 1

Tactic:
inv_mul_cancel_of_invertible

Goal state after:
Module: Mathlib.FieldTheory.JacobsonNoether

Goal state before:
pp: L : Type u_2
D : Type u_3
inst✝⁴ : Field L
inst✝³ : DivisionRing D
inst✝² : Algebra L D
inst✝¹ : Algebra.IsAlgebraic L D
inst✝ : IsCentral L D
hneq : ⊥ ≠ ⊤
hcenter : Subalgebra.center L D = ⊥
ntrivial : k ≠ ⊤
φ : ↥⊥ ≃ₐ[L] ↥(Subalgebra.center L D) := ⊥.equivOfEq (Subalgebra.center L D) ⋯
equiv : L ≃+* ↥k := ((botEquiv L D).symm.trans φ).toRingEquiv
x✝² : Algebra L ↥k := equiv.toRingHom.toAlgebra
x✝¹ : Algebra (↥k) L := equiv.symm.toRingHom.toAlgebra
x✝ : IsScalarTower L (↥k) D
x : ↥k
⊢ (algebraMap (↥k) D) x = (algebraMap (↥k) D) ((algebraMap L ↥k) ((algebraMap (↥k) L) x))

Tactic:
congr

Goal state after:
case e_6
L : Type u_2
D : Type u_3
inst✝⁴ : Field L
inst✝³ : DivisionRing D
inst✝² : Algebra L D
inst✝¹ : Algebra.IsAlgebraic L D
inst✝ : IsCentral L D
hneq : ⊥ ≠ ⊤
hcenter : Subalgebra.center L D = ⊥
ntrivial : k ≠ ⊤
φ : ↥⊥ ≃ₐ[L] ↥(Subalgebra.center L D) := ⋯
equiv : L ≃+* ↥k := ⋯
x✝² : Algebra L ↥k := ⋯
x✝¹ : Algebra (↥k) L := ⋯
x✝ : IsScalarTower L (↥k) D
x : ↥k
⊢ x = (algebraMap L ↥k) ((algebraMap (↥k) L) x)
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 = ⊥ ↔
    Function.Injective ⇑(Finsupp.linearCombination (↥B.op) (MulOpposite.op ∘ ⇑A.val ∘ a))

Tactic:
LinearMap.ker_eq_bot

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
⊢ Function.Injective ⇑(Submodule.mulLeftMap (toSubmodule B) a) ↔
    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 = ⊥ ↔ Function.Injective ⇑(Finsupp.linearCombination (↥A) (⇑B.val ∘ b))

Tactic:
LinearMap.ker_eq_bot

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
⊢ Function.Injective ⇑((toSubmodule A).mulRightMap b) ↔
    Function.Injective ⇑(Finsupp.linearCombination (↥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
H : A.LinearDisjoint B
hf : Flat R ↥A ∨ Flat R ↥B
hc : ∀ (a b : ↥(A ⊓ B)), Commute ↑a ↑b
hinj : Function.Injective ⇑(algebraMap R S)
a✝ : Nontrivial R
⊢ 1 ≤ Module.rank R ↥(A ⊓ B)

Tactic:
have : Cardinal.lift.{u} (Module.rank R (⊥ : Subalgebra R S)) =
      Cardinal.lift.{v} (Module.rank R R) :=
    lift_rank_range_of_injective (Algebra.linearMap R S) hinj

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
hf : Flat R ↥A ∨ Flat R ↥B
hc : ∀ (a b : ↥(A ⊓ B)), Commute ↑a ↑b
hinj : Function.Injective ⇑(algebraMap R S)
a✝ : Nontrivial R
this : Cardinal.lift.{u, v} (Module.rank R ↥⊥) = Cardinal.lift.{v, u} (Module.rank R R)
⊢ 1 ≤ Module.rank R ↥(A ⊓ B)
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 : ConjRootClass K L
⊢ ∀ ⦃a₂ : ConjRootClass K L⦄, x.carrier = a₂.carrier → x = a₂

Tactic:
y

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
⊢ x.carrier = y.carrier → x = y
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 ⋯)
⊢ (↑(Module.finrank F ↥F⟮a⟯))⁻¹ • (trace F ↥F⟮f a⟯) (AdjoinSimple.gen F (f a)) =
    (↑(Module.finrank F ↥F⟮a⟯))⁻¹ • (trace F ↥F⟮a⟯) (AdjoinSimple.gen F a)

Tactic:
congr

Goal state after:
case e_a
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 ⋯)
⊢ (trace F ↥F⟮f a⟯) (AdjoinSimple.gen F (f a)) = (trace F ↥F⟮a⟯) (AdjoinSimple.gen F a)
Module: Mathlib.FieldTheory.NormalizedTrace

Goal state before:
pp: F : Type u_3
E : Type u_4
K : Type u_5
inst✝¹² : Field F
inst✝¹¹ : Field E
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F E
inst✝⁸ : Algebra E K
inst✝⁷ : Algebra F K
inst✝⁶ : IsScalarTower F E K
inst✝⁵ : Algebra.IsIntegral F E
inst✝⁴ : Algebra.IsIntegral F K
inst✝³ : CharZero F
inst✝² : FiniteDimensional F E
inst✝¹ : Algebra.IsIntegral E K
inst✝ : CharZero E
a : K
this✝ : FiniteDimensional E ↥E⟮a⟯
E' : IntermediateField F K := IntermediateField.restrictScalars F E⟮a⟯
this : FiniteDimensional F ↥E'
h_finrank_eq : Module.finrank F ↥E⟮a⟯ = Module.finrank F ↥E'
h_trace_eq : (trace F ↥E⟮a⟯) (AdjoinSimple.gen E a) = (trace F ↥E') (AdjoinSimple.gen E a)
a' : ↥E' := AdjoinSimple.gen E a
⊢ (normalizedTrace F K) a = (normalizedTrace F K) ↑a'

Tactic:
congr

Goal state after:
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
halg : Algebra.IsAlgebraic F ↥A ∨ Algebra.IsAlgebraic F L
L' : Subalgebra F E := (IsScalarTower.toAlgHom F L E).range
i : L ≃ₐ[F] ↥L' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)
⊢ (adjoin L ↑A).toSubsemiring = (Algebra.adjoin ↥L' ↑A).toSubsemiring

Tactic:
rw [adjoin_intermediateField_toSubalgebra_of_isAlgebraic _ _ halg.symm,
      Algebra.adjoin_toSubsemiring, Algebra.adjoin_toSubsemiring]

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
halg : Algebra.IsAlgebraic F ↥A ∨ Algebra.IsAlgebraic F L
L' : Subalgebra F E := (IsScalarTower.toAlgHom F L E).range
i : L ≃ₐ[F] ↥L' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)
⊢ Subsemiring.closure (Set.range ⇑(algebraMap L E) ∪ ↑A) = Subsemiring.closure (Set.range ⇑(algebraMap (↥L') E) ∪ ↑A)
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
inst✝ : Algebra.IsIntegral R ↥A
H : ∀ A' ≤ A, ∀ [Module.Finite R ↥A'], A'.LinearDisjoint B
x : ↥(toSubmodule A) ⊗[R] ↥(toSubmodule B)
⊢ ∀ ⦃a₂ : ↥(toSubmodule A) ⊗[R] ↥(toSubmodule B)⦄,
    ((toSubmodule A).mulMap (toSubmodule B)) x = ((toSubmodule A).mulMap (toSubmodule B)) a₂ → x = a₂

Tactic:
y

Goal state after:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
A B : Subalgebra R S
inst✝ : Algebra.IsIntegral R ↥A
H : ∀ A' ≤ A, ∀ [Module.Finite R ↥A'], A'.LinearDisjoint B
x y : ↥(toSubmodule A) ⊗[R] ↥(toSubmodule B)
⊢ ((toSubmodule A).mulMap (toSubmodule B)) x = ((toSubmodule A).mulMap (toSubmodule B)) y → x = y
Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure

Goal state before:
pp: F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
q n : ℕ
hF : ExpChar F q
ι : Type u_1
v : ι → E
inst✝¹ : FiniteDimensional F E
inst✝ : Algebra.IsSeparable F E
h : LinearIndependent F v
h' : LinearIndepOn F id (Set.range v)
ι' : Set E := h'.extend ⋯
b : Basis (↑ι') F E := Basis.extend h'
this : Fintype ↑ι' := FiniteDimensional.fintypeBasisIndex b
H : LinearIndependent F fun (x : ↑ι') ↦ b x ^ q ^ n
f : ι → ↑ι' := fun i ↦ ⟨v i, ⋯⟩
x✝ : ι
⊢ v x✝ ^ q ^ n = ((fun x ↦ b x ^ q ^ n) ∘ f) x✝

Tactic:
Function.comp_apply,

Goal state after:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
q n : ℕ
hF : ExpChar F q
ι : Type u_1
v : ι → E
inst✝¹ : FiniteDimensional F E
inst✝ : Algebra.IsSeparable F E
h : LinearIndependent F v
h' : LinearIndepOn F id (Set.range v)
ι' : Set E := h'.extend ⋯
b : Basis (↑ι') F E := Basis.extend h'
this : Fintype ↑ι' := FiniteDimensional.fintypeBasisIndex b
H : LinearIndependent F fun (x : ↑ι') ↦ b x ^ q ^ n
f : ι → ↑ι' := fun i ↦ ⟨v i, ⋯⟩
x✝ : ι
⊢ v x✝ ^ q ^ n = b (f x✝) ^ q ^ n
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
inst✝ : Algebra.IsIntegral R ↥A
H : ∀ A' ≤ A, ∀ [Module.Finite R ↥A'], A'.LinearDisjoint B
x y : ↥(toSubmodule A) ⊗[R] ↥(toSubmodule B)
hxy : ((toSubmodule A).mulMap (toSubmodule B)) x = ((toSubmodule A).mulMap (toSubmodule B)) y
M' : Submodule R S
hM : M' ≤ toSubmodule A
hf : Module.Finite R ↥M'
s : Finset S
hs : Submodule.span R ↑s = M'
hs' : ↑s ⊆ ↑A
A' : Subalgebra R S := Algebra.adjoin R ↑s
hf' : Module.Finite R ↥A'
hA : toSubmodule A' ≤ toSubmodule A
h : {x, y} ⊆ ↑(LinearMap.rTensor (↥(toSubmodule B)) (Submodule.inclusion hA)).range
x' : ↥(toSubmodule A') ⊗[R] ↥(toSubmodule B)
hx' : (LinearMap.rTensor (↥(toSubmodule B)) (Submodule.inclusion hA)) x' = x
y' : ↥(toSubmodule A') ⊗[R] ↥(toSubmodule B)
hy' : (LinearMap.rTensor (↥(toSubmodule B)) (Submodule.inclusion hA)) y' = y
⊢ (LinearMap.rTensor (↥(toSubmodule B)) (Submodule.inclusion hA)) x' =
    (LinearMap.rTensor (↥(toSubmodule B)) (Submodule.inclusion hA)) y'

Tactic:
congr

Goal state after:
case e_6
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
A B : Subalgebra R S
inst✝ : Algebra.IsIntegral R ↥A
H : ∀ A' ≤ A, ∀ [Module.Finite R ↥A'], A'.LinearDisjoint B
x y : ↥(toSubmodule A) ⊗[R] ↥(toSubmodule B)
hxy : ((toSubmodule A).mulMap (toSubmodule B)) x = ((toSubmodule A).mulMap (toSubmodule B)) y
M' : Submodule R S
hM : M' ≤ toSubmodule A
hf : Module.Finite R ↥M'
s : Finset S
hs : Submodule.span R ↑s = M'
hs' : ↑s ⊆ ↑A
A' : Subalgebra R S := ⋯
hf' : Module.Finite R ↥A'
hA : toSubmodule A' ≤ toSubmodule A
h : {x, y} ⊆ ↑(LinearMap.rTensor (↥(toSubmodule B)) (Submodule.inclusion hA)).range
x' : ↥(toSubmodule A') ⊗[R] ↥(toSubmodule B)
hx' : (LinearMap.rTensor (↥(toSubmodule B)) (Submodule.inclusion hA)) x' = x
y' : ↥(toSubmodule A') ⊗[R] ↥(toSubmodule B)
hy' : (LinearMap.rTensor (↥(toSubmodule B)) (Submodule.inclusion hA)) y' = y
⊢ x' = y'
Module: Mathlib.FieldTheory.PurelyInseparable.Tower

Goal state before:
pp: F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
x : K
hsep : IsSeparable F x
inst✝ : IsPurelyInseparable F E
hi : IsIntegral F x
hi' : IsIntegral E x
hsep' : IsSeparable E x
this✝ : Algebra.IsSeparable F ↥F⟮x⟯
this : Algebra.IsSeparable E ↥E⟮x⟯
⊢ (Polynomial.map (algebraMap F E) (minpoly F x)).natDegree = (minpoly E x).natDegree

Tactic:
have := Algebra.IsSeparable.isAlgebraic F F⟮x⟯

Goal state after:
F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
x : K
hsep : IsSeparable F x
inst✝ : IsPurelyInseparable F E
hi : IsIntegral F x
hi' : IsIntegral E x
hsep' : IsSeparable E x
this✝¹ : Algebra.IsSeparable F ↥F⟮x⟯
this✝ : Algebra.IsSeparable E ↥E⟮x⟯
this : Algebra.IsAlgebraic F ↥F⟮x⟯
⊢ (Polynomial.map (algebraMap F E) (minpoly F x)).natDegree = (minpoly E x).natDegree
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ Polynomial.C ((algebraMap K[X] K⟮X⟯) (Φ' E).content)⁻¹ *
      Polynomial.map (algebraMap K[X] K⟮X⟯) (Polynomial.C (Φ' E).content * (Φ' E).primPart) =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (Φ E)

Tactic:
Polynomial.map_mul,

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ Polynomial.C ((algebraMap K[X] K⟮X⟯) (Φ' E).content)⁻¹ *
      (Polynomial.map (algebraMap K[X] K⟮X⟯) (Polynomial.C (Φ' E).content) *
        Polynomial.map (algebraMap K[X] K⟮X⟯) (Φ' E).primPart) =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (Φ E)
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ Polynomial.C ((algebraMap K[X] K⟮X⟯) (g E)) *
      (Polynomial.map ((algebraMap (↥E) K⟮X⟯).comp (algebraMap ↥K⟮generator E⟯ ↥E))
          (Polynomial.map (algebraMap K ↥K⟮generator E⟯) (generator E).num) -
        Polynomial.map ((algebraMap (↥E) K⟮X⟯).comp (algebraMap ↥K⟮generator E⟯ ↥E))
          (Polynomial.C ((algebraMap ↥K[generator E] ↥K⟮generator E⟯) ⟨generator E, ⋯⟩) *
            Polynomial.map (algebraMap K ↥K⟮generator E⟯) (generator E).denom)) =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E)

Tactic:
Polynomial.map_mul,

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ Polynomial.C ((algebraMap K[X] K⟮X⟯) (g E)) *
      (Polynomial.map ((algebraMap (↥E) K⟮X⟯).comp (algebraMap ↥K⟮generator E⟯ ↥E))
          (Polynomial.map (algebraMap K ↥K⟮generator E⟯) (generator E).num) -
        Polynomial.map ((algebraMap (↥E) K⟮X⟯).comp (algebraMap ↥K⟮generator E⟯ ↥E))
            (Polynomial.C ((algebraMap ↥K[generator E] ↥K⟮generator E⟯) ⟨generator E, ⋯⟩)) *
          Polynomial.map ((algebraMap (↥E) K⟮X⟯).comp (algebraMap ↥K⟮generator E⟯ ↥E))
            (Polynomial.map (algebraMap K ↥K⟮generator E⟯) (generator E).denom)) =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E)
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ Polynomial.C ((algebraMap K[X] K⟮X⟯) (g E)) *
      (Polynomial.map ((algebraMap (↥E) K⟮X⟯).comp (algebraMap ↥K⟮generator E⟯ ↥E))
          (Polynomial.map (algebraMap K ↥K⟮generator E⟯) (generator E).num) -
        Polynomial.C
            ((⇑(algebraMap (↥E) K⟮X⟯) ∘ ⇑(algebraMap ↥K⟮generator E⟯ ↥E))
              ((algebraMap ↥K[generator E] ↥K⟮generator E⟯) ⟨generator E, ⋯⟩)) *
          Polynomial.map ((algebraMap (↥E) K⟮X⟯).comp (algebraMap ↥K⟮generator E⟯ ↥E))
            (Polynomial.map (algebraMap K ↥K⟮generator E⟯) (generator E).denom)) =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E)

Tactic:
Function.comp_apply,

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ Polynomial.C ((algebraMap K[X] K⟮X⟯) (g E)) *
      (Polynomial.map ((algebraMap (↥E) K⟮X⟯).comp (algebraMap ↥K⟮generator E⟯ ↥E))
          (Polynomial.map (algebraMap K ↥K⟮generator E⟯) (generator E).num) -
        Polynomial.C
            ((algebraMap (↥E) K⟮X⟯)
              ((algebraMap ↥K⟮generator E⟯ ↥E) ((algebraMap ↥K[generator E] ↥K⟮generator E⟯) ⟨generator E, ⋯⟩))) *
          Polynomial.map ((algebraMap (↥E) K⟮X⟯).comp (algebraMap ↥K⟮generator E⟯ ↥E))
            (Polynomial.map (algebraMap K ↥K⟮generator E⟯) (generator E).denom)) =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E)
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ Polynomial.C ((algebraMap K[X] K⟮X⟯) (g E)) *
        Polynomial.map (((algebraMap (↥E) K⟮X⟯).comp ↑(inclusion ⋯)).comp (algebraMap K ↥K⟮generator E⟯))
          (generator E).num -
      Polynomial.C ((algebraMap K[X] K⟮X⟯) (generator E).num) *
        Polynomial.map (((algebraMap (↥E) K⟮X⟯).comp ↑(inclusion ⋯)).comp (algebraMap K ↥K⟮generator E⟯))
          (generator E).denom =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (Polynomial.C (g E) * Polynomial.map Polynomial.C (f E)) -
      Polynomial.map (algebraMap K[X] K⟮X⟯) (Polynomial.C (f E) * Polynomial.map Polynomial.C (g E))

Tactic:
Polynomial.map_mul,

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ Polynomial.C ((algebraMap K[X] K⟮X⟯) (g E)) *
        Polynomial.map (((algebraMap (↥E) K⟮X⟯).comp ↑(inclusion ⋯)).comp (algebraMap K ↥K⟮generator E⟯))
          (generator E).num -
      Polynomial.C ((algebraMap K[X] K⟮X⟯) (generator E).num) *
        Polynomial.map (((algebraMap (↥E) K⟮X⟯).comp ↑(inclusion ⋯)).comp (algebraMap K ↥K⟮generator E⟯))
          (generator E).denom =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (Polynomial.C (g E)) *
        Polynomial.map (algebraMap K[X] K⟮X⟯) (Polynomial.map Polynomial.C (f E)) -
      Polynomial.map (algebraMap K[X] K⟮X⟯) (Polynomial.C (f E) * Polynomial.map Polynomial.C (g E))
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ Polynomial.C ((algebraMap K[X] K⟮X⟯) (g E)) *
        Polynomial.map (((algebraMap (↥E) K⟮X⟯).comp ↑(inclusion ⋯)).comp (algebraMap K ↥K⟮generator E⟯))
          (generator E).num -
      Polynomial.C ((algebraMap K[X] K⟮X⟯) (generator E).num) *
        Polynomial.map (((algebraMap (↥E) K⟮X⟯).comp ↑(inclusion ⋯)).comp (algebraMap K ↥K⟮generator E⟯))
          (generator E).denom =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (Polynomial.C (g E)) *
        Polynomial.map (algebraMap K[X] K⟮X⟯) (Polynomial.map Polynomial.C (f E)) -
      Polynomial.map (algebraMap K[X] K⟮X⟯) (Polynomial.C (f E) * Polynomial.map Polynomial.C (g E))

Tactic:
Polynomial.map_mul,

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ Polynomial.C ((algebraMap K[X] K⟮X⟯) (g E)) *
        Polynomial.map (((algebraMap (↥E) K⟮X⟯).comp ↑(inclusion ⋯)).comp (algebraMap K ↥K⟮generator E⟯))
          (generator E).num -
      Polynomial.C ((algebraMap K[X] K⟮X⟯) (generator E).num) *
        Polynomial.map (((algebraMap (↥E) K⟮X⟯).comp ↑(inclusion ⋯)).comp (algebraMap K ↥K⟮generator E⟯))
          (generator E).denom =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (Polynomial.C (g E)) *
        Polynomial.map (algebraMap K[X] K⟮X⟯) (Polynomial.map Polynomial.C (f E)) -
      Polynomial.map (algebraMap K[X] K⟮X⟯) (Polynomial.C (f E)) *
        Polynomial.map (algebraMap K[X] K⟮X⟯) (Polynomial.map Polynomial.C (g E))
Module: Mathlib.Geometry.Convex.Cone.Face.Basic

Goal state before:
pp: case mem_of_smul_add_mem
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : DivisionRing R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsOrderedRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
C₁ : PointedCone R M
C₂ : PointedCone R N
F : PointedCone R (M × N)
hF : F.IsFaceOf (prod C₁ C₂)
x : M
⊢ ∀ {y : M} {a : R}, x ∈ C₁ → y ∈ C₁ → 0 < a → ∀ (x_1 : N), (a • x + y, x_1) ∈ F → ∃ x_2, (x, x_2) ∈ F

Tactic:
y

Goal state after:
case mem_of_smul_add_mem
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : DivisionRing R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsOrderedRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
C₁ : PointedCone R M
C₂ : PointedCone R N
F : PointedCone R (M × N)
hF : F.IsFaceOf (prod C₁ C₂)
x y : M
⊢ ∀ {a : R}, x ∈ C₁ → y ∈ C₁ → 0 < a → ∀ (x_1 : N), (a • x + y, x_1) ∈ F → ∃ x_2, (x, x_2) ∈ F
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ Polynomial.map (algebraMap K[X] K⟮X⟯) (Q₁ h * Φ E) = Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E)

Tactic:
Polynomial.map_mul,

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ Polynomial.map (algebraMap K[X] K⟮X⟯) (Q₁ h) * Polynomial.map (algebraMap K[X] K⟮X⟯) (Φ E) =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E)
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
u : K⟮X⟯
⊢ ↑((algEquiv h) u) = (aeval (generator E)) u.num / (aeval (generator E)) u.denom

Tactic:
simp [algEquiv, algEquivOfTranscendental_apply]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Projection

Goal state before:
pp: case mpr
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace 𝕜 V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst✝¹ : Nonempty ↥s
inst✝ : s.direction.HasOrthogonalProjection
p : P
h : p ∈ s
hp : p ∈ ↑s ∩ ↑(mk' p s.directionᗮ)
⊢ ↑((orthogonalProjection s) p) = p

Tactic:
inter_eq_singleton_orthogonalProjection p

Goal state after:
case mpr
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace 𝕜 V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst✝¹ : Nonempty ↥s
inst✝ : s.direction.HasOrthogonalProjection
p : P
h : p ∈ s
hp : p ∈ {↑((orthogonalProjection s) p)}
⊢ ↑((orthogonalProjection s) p) = p
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation

Goal state before:
pp: V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
x : V
⊢ ∀ (y : V),
    ⟪(θ.cos • LinearMap.id + θ.sin • ↑o.rightAngleRotation.toLinearEquiv) x,
        (θ.cos • LinearMap.id + θ.sin • ↑o.rightAngleRotation.toLinearEquiv) y⟫ =
      ⟪x, y⟫

Tactic:
y

Goal state after:
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
x y : V
⊢ ⟪(θ.cos • LinearMap.id + θ.sin • ↑o.rightAngleRotation.toLinearEquiv) x,
      (θ.cos • LinearMap.id + θ.sin • ↑o.rightAngleRotation.toLinearEquiv) y⟫ =
    ⟪x, y⟫