mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Semiring T
inst✝ : Algebra R T
⊢ ∀ (a₁ a₂ : S) (b₁ b₂ : T),
    (linearEquivIncludeRange R S T) ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) =
      (linearEquivIncludeRange R S T) (a₁ ⊗ₜ[R] b₁) * (linearEquivIncludeRange R S T) (a₂ ⊗ₜ[R] b₂)

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra

Goal state before:
pp: case ha
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : CommSemiring T
inst✝ : Algebra R T
A B : Subalgebra R S
f : S →ₐ[R] T
x✝ : ↥A
⊢ ((((map f A).mulMap (map f B)).comp
            (Algebra.TensorProduct.map (AlgHom.subalgebraMap A f) (AlgHom.subalgebraMap B f))).comp
        Algebra.TensorProduct.includeLeft)
      x✝ =
    ((f.comp (A.mulMap B)).comp Algebra.TensorProduct.includeLeft) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra

Goal state before:
pp: case hb
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : CommSemiring T
inst✝ : Algebra R T
A B : Subalgebra R S
f : S →ₐ[R] T
x✝ : ↥B
⊢ ((AlgHom.restrictScalars R
            (((map f A).mulMap (map f B)).comp
              (Algebra.TensorProduct.map (AlgHom.subalgebraMap A f) (AlgHom.subalgebraMap B f)))).comp
        Algebra.TensorProduct.includeRight)
      x✝ =
    ((AlgHom.restrictScalars R (f.comp (A.mulMap B))).comp Algebra.TensorProduct.includeRight) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra

Goal state before:
pp: case ha
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
A B : Subalgebra R S
x✝ : ↥B
⊢ ((B.mulMap A).comp Algebra.TensorProduct.includeLeft) x✝ =
    (((A.mulMap B).comp ↑(Algebra.TensorProduct.comm R ↥B ↥A)).comp Algebra.TensorProduct.includeLeft) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra

Goal state before:
pp: case hb
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
A B : Subalgebra R S
x✝ : ↥A
⊢ ((AlgHom.restrictScalars R (B.mulMap A)).comp Algebra.TensorProduct.includeRight) x✝ =
    ((AlgHom.restrictScalars R ((A.mulMap B).comp ↑(Algebra.TensorProduct.comm R ↥B ↥A))).comp
        Algebra.TensorProduct.includeRight)
      x✝

Tactic:
simp

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
inst✝¹ : Free R ↥A
inst✝ : Free R ↥B
⊢ Module.rank R ↥(A ⊔ B) = Module.rank R ↥A * Module.rank R ↥B

Tactic:
by
  nontriviality R
  rw [← rank_tensorProduct', H.mulMap.toLinearEquiv.rank_eq]

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
inst✝³ : Free R ↥A
inst✝² : Free R ↥B
inst✝¹ : Module.Finite R ↥A
inst✝ : Module.Finite R ↥B
H : finrank R ↥(A ⊔ B) = finrank R (↥A ⊗[R] ↥B)
a✝ : Nontrivial R
j : Fin (finrank R (↥A ⊗[R] ↥B)) → ↥(A ⊔ B)
hj : Function.Injective ⇑(Finsupp.linearCombination R j)
⊢ finrank R (↥A ⊗[R] ↥B) = finrank R (Fin (finrank R (↥A ⊗[R] ↥B)) →₀ R)

Tactic:
simp

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
inst✝³ : Free R ↥A
inst✝² : Free R ↥B
inst✝¹ : Module.Finite R ↥A
inst✝ : Module.Finite R ↥B
H : finrank R ↥(A ⊔ B) = finrank R (↥A ⊗[R] ↥B)
a✝ : Nontrivial R
j : Fin (finrank R (↥A ⊗[R] ↥B)) → ↥(A ⊔ B)
j' : ↥A ⊗[R] ↥B →ₗ[R] ↥(A ⊔ B) :=
  Finsupp.linearCombination R j ∘ₗ ↑(LinearEquiv.ofFinrankEq (↥A ⊗[R] ↥B) (Fin (finrank R (↥A ⊗[R] ↥B)) →₀ R) ⋯)
hj : Function.Injective ⇑j'
⊢ A.LinearDisjoint B

Tactic:
have hf : Function.Surjective (mulMap' A B).toLinearMap := mulMap'_surjective A B

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✝³ : Free R ↥A
inst✝² : Free R ↥B
inst✝¹ : Module.Finite R ↥A
inst✝ : Module.Finite R ↥B
H : finrank R ↥(A ⊔ B) = finrank R (↥A ⊗[R] ↥B)
a✝ : Nontrivial R
j : Fin (finrank R (↥A ⊗[R] ↥B)) → ↥(A ⊔ B)
j' : ↥A ⊗[R] ↥B →ₗ[R] ↥(A ⊔ B) :=
  Finsupp.linearCombination R j ∘ₗ ↑(LinearEquiv.ofFinrankEq (↥A ⊗[R] ↥B) (Fin (finrank R (↥A ⊗[R] ↥B)) →₀ R) ⋯)
hj : Function.Injective ⇑j'
hf : Function.Surjective ⇑(A.mulMap' B).toLinearMap
⊢ A.LinearDisjoint B
Module: Mathlib.FieldTheory.LinearDisjoint

Goal state before:
pp: case e_a
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
x : E
⊢ x ∈ ↑A ↔ x ∈ Set.range ⇑(algebraMap (↥A) E)

Tactic:
simp

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
inst✝³ : Free R ↥A
inst✝² : Free R ↥B
inst✝¹ : Free ↥A ↥(Algebra.adjoin ↥A ↑B)
inst✝ : Free ↥B ↥(Algebra.adjoin ↥B ↑A)
H : (finrank R ↥A).Coprime (finrank R ↥B)
a✝ : Nontrivial R
h1 : ¬finrank R ↥A = 0
h2 : ¬finrank R ↥B = 0
this✝¹ : Module.Finite R ↥A
this✝ : Module.Finite R ↥B
this : Module.Finite R ↥(A ⊔ B)
⊢ toSubmodule A ≤ toSubmodule (A ⊔ B)

Tactic:
simp

Goal state after:
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
⊢ LinearIndependent F fun x ↦ v x ^ q ^ n

Tactic:
have h' := h.linearIndepOn_id
  let ι' := h'.extend (Set.range v).subset_univ
  let b : Basis ι' F E := Basis.extend h'
  let : Fintype ι' := FiniteDimensional.fintypeBasisIndex b
  have H := linearIndependent_of_top_le_span_of_card_eq_finrank
    (Field.span_map_pow_expChar_pow_eq_top_of_isSeparable q n b.span_eq).ge
    (Module.finrank_eq_card_basis b).symm
  let f (i : ι) : ι' := ⟨v i, h'.subset_extend _ ⟨i, rfl⟩⟩
  convert! H.comp f fun _ _ heq ↦ h.injective (by simpa only [f, Subtype.mk.injEq] using heq)
  simp_rw [Function.comp_apply, b]
  rw [Basis.extend_apply_self]

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
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 ∈ {x, y}

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

Goal state before:
pp: K : Type u_1
inst✝ : Field K
g : K⟮X⟯
x✝ : g ∈ ⊤
⊢ g = (aeval X) g.num / (aeval X) g.denom

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
⊢ {X} ⊆ ↑E ∪ {X}

Tactic:
simp

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
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 ∈ {x, y}

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

Goal state before:
pp: K : Type u_1
inst✝ : Field K
c : K
⊢ (C c).minpolyX ↥K⟮C c⟯ = 0

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

Goal state before:
pp: case pos
K : Type u_1
inst✝ : Field K
c : K
⊢ ((C c).minpolyX ↥K⟮C c⟯).natDegree = max (C c).num.natDegree (C c).denom.natDegree

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

Goal state before:
pp: K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ¬∃ c, f = C c
⊢ Transcendental K f

Tactic:
by
  intro H
  have := isAlgebraic_adjoin_simple H.isIntegral
  have tr : Algebra.Transcendental K K⟮X⟯ := by infer_instance
  rw [Algebra.transcendental_iff_not_isAlgebraic] at tr
  exact tr <| Algebra.IsAlgebraic.trans _ _ _ (alg := f.isAlgebraic_adjoin_simple_X' hf)

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

Goal state before:
pp: case e_a.e_f
K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ¬∃ c, f = C c
e : K[X] ≃ₐ[K] ↥K[f] := ⋯
φ : K[X][X] := ⋯
x✝ : K
⊢ ↑(((↑(aeval ⟨f, ⋯⟩)).comp Polynomial.C) x✝) = ↑((algebraMap K ↥K[f]) x✝)

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

Goal state before:
pp: case e_a.e_a
K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ¬∃ c, f = C c
e : K[X] ≃ₐ[K] ↥K[f] := ⋯
φ : K[X][X] := ⋯
n✝ : ℕ
⊢ ↑((Polynomial.map ((↑(aeval ⟨f, ⋯⟩)).comp Polynomial.C) f.denom).coeff n✝) =
    ↑((Polynomial.map (algebraMap K ↥K[f]) f.denom).coeff n✝)

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

Goal state before:
pp: case pos
K : Type u_1
inst✝ : Field K
c : K
⊢ 0 = max (C c).num.natDegree (C c).denom.natDegree

Tactic:
simp

Goal state after:
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
S : Set K
inst✝¹ : Algebra.IsAlgebraic F ↥(adjoin F S)
inst✝ : IsPurelyInseparable F E
⊢ sepDegree E ↥(adjoin E S) = sepDegree F ↥(adjoin F S)

Tactic:
set M := adjoin F S
  set L := adjoin E S
  let E' := (IsScalarTower.toAlgHom F E K).fieldRange
  let j : E ≃ₐ[F] E' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F E K)
  have hi : M ≤ L.restrictScalars F := by
    rw [restrictScalars_adjoin_of_algEquiv (E := K) j rfl, restrictScalars_adjoin]
    exact adjoin.mono _ _ _ Set.subset_union_right
  let i : M →+* L := Subsemiring.inclusion hi
  let : Algebra M L := i.toAlgebra
  let : SMul M L := Algebra.toSMul
  have : IsScalarTower F M L := IsScalarTower.of_algebraMap_eq (congrFun rfl)
  have : IsPurelyInseparable M L := by
    change IsPurelyInseparable M (extendScalars hi)
    obtain ⟨q, _⟩ := ExpChar.exists F
    have : extendScalars hi = adjoin M (E' : Set K) := restrictScalars_injective F <| by
      conv_lhs => rw [extendScalars_restrictScalars, restrictScalars_adjoin_of_algEquiv
        (E := K) j rfl, ← adjoin_self F E', adjoin_adjoin_comm]
    rw [this, isPurelyInseparable_adjoin_iff_pow_mem _ _ q]
    rintro x ⟨y, hy⟩
    obtain ⟨n, z, hz⟩ := IsPurelyInseparable.pow_mem F q y
    refine ⟨n, algebraMap F M z, ?_⟩
    rw [← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply F E K, hz, ← hy, map_pow,
      AlgHom.toRingHom_eq_coe, IsScalarTower.coe_toAlgHom]
  have h := lift_sepDegree_mul_lift_sepDegree_of_isAlgebraic F E L
  rw [IsPurelyInseparable.sepDegree_eq_one F E, Cardinal.lift_one, one_mul] at h
  rw [Cardinal.lift_injective h, ← sepDegree_mul_sepDegree_of_isAlgebraic F M L,
    IsPurelyInseparable.sepDegree_eq_one M L, mul_one]

Goal state after:
Module: Mathlib.Geometry.Convex.Cone.DualFinite

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsOrderedRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : M →ₗ[R] N →ₗ[R] R
⊢ dual p ↑∅ = ⊤

Tactic:
simp

Goal state after:
Module: Mathlib.Geometry.Convex.Cone.DualFinite

Goal state before:
pp: case h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsOrderedRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : M →ₗ[R] N →ₗ[R] R
s : Finset M
⊢ dual p ↑s = dual p ↑(Submodule.span { c // 0 ≤ c } ↑s)

Tactic:
simp

Goal state after:
Module: Mathlib.Geometry.Convex.Cone.DualFinite

Goal state before:
pp: case h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsOrderedRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : M →ₗ[R] N →ₗ[R] R
s : Finset M
⊢ dual LinearMap.id ↑(Finset.image (⇑p) s) = dual p ↑s

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.Valuation

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F⟮X⟯
⊢ exp (intDegree 1) = 1

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.Valuation

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F⟮X⟯
m : ℤ
⊢ (inftyValuation F) (RatFunc.X ^ m) = exp m

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.Valuation

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝² : Field F
inst✝¹ : Field K
inst✝ : DecidableEq F⟮X⟯
⊢ (inftyValuation F) X ≠ 0 ∧ (inftyValuation F) X ≠ 1

Tactic:
simp

Goal state after:
Module: Mathlib.Geometry.Convex.Cone.Face.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
C : PointedCone R M
F : Set (PointedCone R M)
h : ∀ f ∈ F, f.IsFaceOf C
⊢ ∀ {x y : M} {a : R}, x ∈ C → y ∈ C → 0 < a → a • x + y ∈ C ⊓ sInf F → x ∈ C ⊓ sInf F

Tactic:
by
    simp only [mem_inf, mem_sInf, and_imp]
    intro _ _ a xc yc a0 _ h'
    simpa [xc] using fun F Fs ↦ (h F Fs).mem_of_smul_add_mem xc yc a0 (h' F Fs)

Goal state after:
Module: Mathlib.Geometry.Convex.Cone.Face.Basic

Goal state before:
pp: case h
R : Type u_1
M : Type u_2
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
inst✝³ : IsOrderedRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
C F : PointedCone R M
ι : Type u_4
inst✝ : Fintype ι
f : ι → M
c : ι → R
hF : F.IsFaceOf C
hsC : ∀ (i : ι), f i ∈ C
hc : ∀ (i : ι), 0 ≤ c i
hs : ∑ i, c i • f i ∈ F
i : ι
hci : 0 < c i
⊢ i ∉ Finset.univ → c i • f i = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Geometry.Convex.Cone.Face.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsOrderedRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
C F : PointedCone R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Function.Injective ⇑f
sub : map f F ≤ map f C
x✝ y✝ : M
a✝ : R
hx : x✝ ∈ C
hy : y✝ ∈ C
ha : 0 < a✝
h : a✝ • x✝ + y✝ ∈ F
hF :
  ∀ {x y : N} {a : R},
    ∀ x_1 ∈ C, f x_1 = x → ∀ x_2 ∈ C, f x_2 = y → 0 < a → ∀ x_3 ∈ F, f x_3 = a • x + y → ∃ x_4 ∈ F, f x_4 = x
⊢ f (a✝ • x✝ + y✝) = a✝ • f x✝ + f y✝

Tactic:
simp

Goal state after:
Module: Mathlib.Geometry.Convex.Cone.Face.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : DivisionRing R
inst✝³ : LinearOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
C F : PointedCone R M
hF : F.IsFaceOf C
x✝ : M
hx : x✝ ∈ ↑C.lineal
⊢ x✝ + -x✝ ∈ F

Tactic:
simp

Goal state after:
Module: Mathlib.Geometry.Convex.Cone.Face.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : DivisionRing R
inst✝³ : LinearOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
C F : PointedCone R M
hF : F.IsFaceOf C
x✝¹ : M
x✝ : x✝¹ ∈ C.lineal
hx : x✝¹ ∈ ↑C.toAddSubmonoid
hx' : x✝¹ ∈ ↑(-C.toAddSubmonoid)
⊢ x✝¹ + -x✝¹ ∈ F

Tactic:
simp

Goal state after:
Module: Mathlib.Geometry.Convex.Cone.Face.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : DivisionRing R
inst✝³ : LinearOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
C F : PointedCone R M
hF : F.IsFaceOf C
x✝¹ : M
x✝ : x✝¹ ∈ C.lineal
hx : x✝¹ ∈ ↑C.toAddSubmonoid
hx' : x✝¹ ∈ ↑(-C.toAddSubmonoid)
⊢ -x✝¹ + x✝¹ ∈ F

Tactic:
simp

Goal state after:
Module: Mathlib.Geometry.Convex.Cone.Face.Basic

Goal state before:
pp: 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₂)
this : (map (↑(LinearEquiv.prodComm R M N)) F).IsFaceOf (map (↑(LinearEquiv.prodComm R M N)) (prod C₁ C₂))
x✝ : N
⊢ x✝ ∈ map (LinearMap.snd R M N) F ↔
    x✝ ∈ map (LinearMap.fst R N M) { carrier := (fun a ↦ a.swap) '' ↑F, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
F : Type u_1 := AlgebraicClosure K
H : ¬(Polynomial.map (algebraMap K F) (Q₂ h)).degree ≤ 0
α : F
hα : (aeval α) (Q₂ h) = 0
this :
  (aeval (Polynomial.C α)) (θ E) =
    (aeval (Polynomial.C α)) (Polynomial.map Polynomial.C (Q₂ h)) * (aeval (Polynomial.C α)) (Φ E)
x✝ : K
n✝ : ℕ
⊢ (((algebraMap K[X] F[X]).comp Polynomial.C) x✝).coeff n✝ = ((Polynomial.C.comp (algebraMap K F)) x✝).coeff n✝

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
F : Type u_1 := AlgebraicClosure K
H : ¬(Polynomial.map (algebraMap K F) (Q₂ h)).degree ≤ 0
α : F
hα : (aeval α) (Q₂ h) = 0
this :
  (algebraMap K[X] F[X]) (g E) * (aeval (Polynomial.C α)) (Polynomial.map Polynomial.C (f E)) -
      (algebraMap K[X] F[X]) (f E) * (aeval (Polynomial.C α)) (Polynomial.map Polynomial.C (g E)) =
    0
x✝ : K
n✝ : ℕ
⊢ (((algebraMap K[X] F[X]).comp Polynomial.C) x✝).coeff n✝ = ((Polynomial.C.comp (algebraMap K F)) x✝).coeff n✝

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
F : Type u_1 := AlgebraicClosure K
H : ¬(Polynomial.map (algebraMap K F) (Q₂ h)).degree ≤ 0
α : F
hα : (aeval α) (Q₂ h) = 0
this :
  (algebraMap K[X] F[X]) (g E) * Polynomial.C ((aeval α) (f E)) -
      (algebraMap K[X] F[X]) (f E) * (aeval (Polynomial.C α)) (Polynomial.map Polynomial.C (g E)) =
    0
x✝ : K
n✝ : ℕ
⊢ (((algebraMap K[X] F[X]).comp Polynomial.C) x✝).coeff n✝ = ((Polynomial.C.comp (algebraMap K F)) x✝).coeff n✝

Tactic:
simp

Goal state after:
Module: Mathlib.Geometry.Diffeology.Basic

Goal state before:
pp: case e'_5
X : Type u_1
d : CorePlotsOn X
n : ℕ
p : EuclideanSpace ℝ (Fin n) → X
h✝ :
  ∀ (x : EuclideanSpace ℝ (Fin n)),
    ∃ u,
      IsOpen u ∧
        x ∈ u ∧
          ∀ {m : ℕ} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
            (∀ (x : EuclideanSpace ℝ (Fin m)), f x ∈ u) → ContDiff ℝ ∞ f → p ∘ f ∈ {p | d.isPlot p}
x : EuclideanSpace ℝ (Fin n)
x✝ : x ∈ Set.univ
u : Set (EuclideanSpace ℝ (Fin n))
hu : IsOpen u
hxu : x ∈ u
hu' :
  ∀ {m : ℕ} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
    (∀ (x : EuclideanSpace ℝ (Fin m)), f x ∈ u) → ContDiff ℝ ∞ f → p ∘ f ∈ {p | d.isPlot p}
ε : ℝ
hε : ε > 0
hε' : Metric.ball x ε ⊆ u
h : d.isPlot (p ∘ ↑(OpenPartialHomeomorph.univBall x ε))
h' : d.isPlotOn ⋯ ((p ∘ ↑(OpenPartialHomeomorph.univBall x ε)) ∘ ↑(OpenPartialHomeomorph.univBall x ε).symm)
⊢ Metric.ball x ε = ((OpenPartialHomeomorph.univBall x ε).symm.trans (OpenPartialHomeomorph.univBall x ε)).source

Tactic:
simp [OpenPartialHomeomorph.univBall_target x hε]

Goal state after:
Module: Mathlib.Geometry.Diffeology.Basic

Goal state before:
pp: X : Type u_1
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace ℝ X
inst✝ : FiniteDimensional ℝ X
u : Set X
h : ∀ {n : ℕ} (p : EuclideanSpace ℝ (Fin n) → X), ContDiff ℝ ∞ p → IsOpen (p ⁻¹' u)
⊢ TopologicalSpace.IsOpen u

Tactic:
← toEuclidean.preimage_symm_preimage u

Goal state after:
X : Type u_1
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace ℝ X
inst✝ : FiniteDimensional ℝ X
u : Set X
h : ∀ {n : ℕ} (p : EuclideanSpace ℝ (Fin n) → X), ContDiff ℝ ∞ p → IsOpen (p ⁻¹' u)
⊢ TopologicalSpace.IsOpen (⇑toEuclidean ⁻¹' ⇑toEuclidean.symm ⁻¹' u)
Module: Mathlib.Geometry.Euclidean.Altitude

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MetricSpace P
inst✝⁴ : NormedAddTorsor V P
V₂ : Type u_3
P₂ : Type u_4
inst✝³ : NormedAddCommGroup V₂
inst✝² : InnerProductSpace ℝ V₂
inst✝¹ : MetricSpace P₂
inst✝ : NormedAddTorsor V₂ P₂
n : ℕ
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
i : Fin (n + 1)
⊢ (s.map f.toAffineMap ⋯).altitude i = AffineSubspace.map f.toAffineMap (s.altitude i)

Tactic:
refine (eq_iff_direction_eq_of_mem (p := f (s.points i)) ?_ ?_).mpr ?_

Goal state after:
case refine_1
V : Type u_1
P : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MetricSpace P
inst✝⁴ : NormedAddTorsor V P
V₂ : Type u_3
P₂ : Type u_4
inst✝³ : NormedAddCommGroup V₂
inst✝² : InnerProductSpace ℝ V₂
inst✝¹ : MetricSpace P₂
inst✝ : NormedAddTorsor V₂ P₂
n : ℕ
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
i : Fin (n + 1)
⊢ f (s.points i) ∈ (s.map f.toAffineMap ⋯).altitude i

case refine_2
V : Type u_1
P : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MetricSpace P
inst✝⁴ : NormedAddTorsor V P
V₂ : Type u_3
P₂ : Type u_4
inst✝³ : NormedAddCommGroup V₂
inst✝² : InnerProductSpace ℝ V₂
inst✝¹ : MetricSpace P₂
inst✝ : NormedAddTorsor V₂ P₂
n : ℕ
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
i : Fin (n + 1)
⊢ f (s.points i) ∈ AffineSubspace.map f.toAffineMap (s.altitude i)

case refine_3
V : Type u_1
P : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MetricSpace P
inst✝⁴ : NormedAddTorsor V P
V₂ : Type u_3
P₂ : Type u_4
inst✝³ : NormedAddCommGroup V₂
inst✝² : InnerProductSpace ℝ V₂
inst✝¹ : MetricSpace P₂
inst✝ : NormedAddTorsor V₂ P₂
n : ℕ
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
i : Fin (n + 1)
⊢ ((s.map f.toAffineMap ⋯).altitude i).direction = (AffineSubspace.map f.toAffineMap (s.altitude i)).direction
Module: Mathlib.Geometry.Euclidean.Projection

Goal state before:
pp: 𝕜 : 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 q : P
⊢ p -ᵥ ↑((orthogonalProjection s) q) ∈ s.directionᗮ ↔ p -ᵥ q + (q -ᵥ ↑((orthogonalProjection s) q)) ∈ s.directionᗮ

Tactic:
simp

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation

Goal state before:
pp: case e'_3
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
⊢ LinearMap.id x = 1 • x

Tactic:
simp

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation

Goal state before:
pp: V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
⊢ o.rotation 0 = LinearIsometryEquiv.refl ℝ V

Tactic:
ext; simp [rotation]

Goal state after: