mathlib-initiative/mathlib-tactics huggingface dataset:
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)
⊢ (X ^ n - C a).Separable

Tactic:
let := Fact.mk H

Goal state after:
K : Type u
inst✝ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
this : Fact (Irreducible (X ^ n - C a)) := { out := H }
⊢ (X ^ n - C a).Separable
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)
⊢ (liftAlgHom (X ^ n - C a) (Algebra.ofId K K[n√a]) (↑↑1 • root (X ^ n - C a)) ⋯) (root (X ^ n - C a)) =
    1 (root (X ^ n - C a))

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
H' : A ⊔ B = ⊤
x : ↥B
⊢ ↑x = (H.mulMapLeftOfSupEqTop H') (1 ⊗ₜ[R] x)

Tactic:
by simp

Goal state after:
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
inst✝ : Flat R ↥B
ι : Type u_1
a : ι → ↥A
ha : LinearIndependent R a
⊢ LinearIndependent (↥B.op) (MulOpposite.op ∘ ⇑A.val ∘ a)

Tactic:
have h := Submodule.LinearDisjoint.linearIndependent_left_of_flat H ha
  rwa [mulLeftMap_ker_eq_bot_iff_linearIndependent_op] at h

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

Goal state before:
pp: K : Type u_1
L : Type u_2
S : Type u_3
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Field S
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra K S
inst✝⁴ : Algebra L S
inst✝³ : IsScalarTower K L S
inst✝² : Normal K L
inst✝¹ : DecidableEq L
inst✝ : Fintype Gal(L/K)
c : ConjRootClass K L
x : L
⊢ mk K x = c ↔ (fun x ↦ x ∈ c.carrier) x

Tactic:
by simp

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
ι : Type u_1
a : ι → ↥A
ha : LinearIndependent F a
⊢ ∀ (r : L), (AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)) r = 0 → r = 0

Tactic:
by simp

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
ι : Type u_1
a : ι → ↥A
ha : LinearIndependent F a
⊢ ∀ (m : E), (AddMonoidHom.id E) m = 0 → m = 0

Tactic:
by simp

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
ι : Type u_1
a : Basis ι F ↥A
H : LinearIndependent L (⇑A.val ∘ ⇑a)
⊢ ∀ (m : E), (AddMonoidHom.id E) m = 0 → m = 0

Tactic:
by simp

Goal state after:
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 = (↑(Module.finrank F ↥E'))⁻¹ • (trace F ↥E⟮a⟯) (AdjoinSimple.gen E a)

Tactic:
h_trace_eq,

Goal state after:
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 = (↑(Module.finrank F ↥E'))⁻¹ • (trace F ↥E') (AdjoinSimple.gen E a)
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
inst✝¹ : CharZero F
inst✝ : Algebra.IsIntegral F K
a : F
⊢ (normalizedTrace F K) ((algebraMap F K) a) = a

Tactic:
by simp

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

Goal state before:
pp: case refine_1
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 : Subalgebra R S
a b : ↥A
x y : ↥⊥
x' : R
hx : (algebraMap R ↥⊥) x' = x
y' : R
hy : (algebraMap R ↥⊥) y' = y
⊢ (toSubmodule A).rTensorOne ((a * b) ⊗ₜ[R] (algebraMap R ↥⊥) (x' * y')) = x' • a * y' • b

Tactic:
(toSubmodule A).rTensorOne_tmul (x' * y') (a * b),

Goal state after:
case refine_1
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 : Subalgebra R S
a b : ↥A
x y : ↥⊥
x' : R
hx : (algebraMap R ↥⊥) x' = x
y' : R
hy : (algebraMap R ↥⊥) y' = y
⊢ (x' * y') • (a * b) = x' • a * y' • b
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:
by simp

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.Exponent

Goal state before:
pp: F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : HasExponent K L
p : ℕ
inst✝ : ExpChar K p
n : ℕ
hn : exponent K L ≤ n
a b : L
inj : Function.Injective ⇑(algebraMap K L)
⊢ iterateFrobeniusAux K L p n (a + b) = iterateFrobeniusAux K L p n a + iterateFrobeniusAux K L p n b

Tactic:
have : ExpChar L p := expChar_of_injective_ringHom inj p

Goal state after:
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : HasExponent K L
p : ℕ
inst✝ : ExpChar K p
n : ℕ
hn : exponent K L ≤ n
a b : L
inj : Function.Injective ⇑(algebraMap K L)
this : ExpChar L p
⊢ iterateFrobeniusAux K L p n (a + b) = iterateFrobeniusAux K L p n a + iterateFrobeniusAux K L p n b
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:
by 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✝² : Flat R ↥B
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
this : LinearIndependent (↥B) (⇑A.val ∘ ⇑(Free.chooseBasis R ↥A))
⊢ Module.rank ↥B ↥(Submodule.span (↥B) (Set.range (⇑A.val ∘ ⇑(Free.chooseBasis R ↥A)))) =
    Cardinal.mk (Free.ChooseBasisIndex R ↥A)

Tactic:
rw [rank_span this, Cardinal.mk_range_eq _ this.injective]

Goal state after:
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: case pos
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
⊢ A.LinearDisjoint B

Tactic:
rw [h1, Nat.coprime_zero_left] at H

Goal state after:
case pos
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 ↥B = 1
a✝ : Nontrivial R
h1 : finrank R ↥A = 0
⊢ A.LinearDisjoint B
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: case pos
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
⊢ A.LinearDisjoint B

Tactic:
rw [h2, Nat.coprime_zero_right] at H

Goal state after:
case pos
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 = 1
a✝ : Nontrivial R
h1 : ¬finrank R ↥A = 0
h2 : finrank R ↥B = 0
⊢ A.LinearDisjoint B
Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure

Goal state before:
pp: case hdeg
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
q : ℕ
hF : ExpChar F q
inst✝ : ExpChar E q
n : ℕ
a : E
hsep : IsSeparable F a
hai : IsIntegral F a
hapi : IsIntegral F ((iterateFrobenius E q n) a)
⊢ finrank F ↥F⟮a ^ q ^ n⟯ ≤ finrank F ↥F⟮(iterateFrobenius E q n) a⟯

Tactic:
iterateFrobenius_def

Goal state after:
case hdeg
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
q : ℕ
hF : ExpChar F q
inst✝ : ExpChar E q
n : ℕ
a : E
hsep : IsSeparable F a
hai : IsIntegral F a
hapi : IsIntegral F ((iterateFrobenius E q n) a)
⊢ finrank F ↥F⟮a ^ q ^ n⟯ ≤ finrank F ↥F⟮a ^ q ^ n⟯
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:
by 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:
by simp

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:
by 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:
by simp

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

Goal state before:
pp: case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F⟮X⟯
x y : F⟮X⟯
hx : ¬x = 0
hy : y = 0
⊢ (if x * y = 0 then 0 else exp (x * y).intDegree) =
    (if x = 0 then 0 else exp x.intDegree) * if y = 0 then 0 else exp y.intDegree

pp: case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F⟮X⟯
x y : F⟮X⟯
hx : ¬x = 0
hy : ¬y = 0
⊢ (if x * y = 0 then 0 else exp (x * y).intDegree) =
    (if x = 0 then 0 else exp x.intDegree) * if y = 0 then 0 else exp y.intDegree

Tactic:
· rw [hy, mul_zero, if_pos (Eq.refl _), mul_zero]

Goal state after:
case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F⟮X⟯
x y : F⟮X⟯
hx : ¬x = 0
hy : ¬y = 0
⊢ (if x * y = 0 then 0 else exp (x * y).intDegree) =
    (if x = 0 then 0 else exp x.intDegree) * if y = 0 then 0 else exp y.intDegree
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:
by 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:
by 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 ≠ ⊥
⊢ m E ≤ (Bivariate.swap (Φ E)).natDegree

Tactic:
rw [← sum_monomial_eq (Φ E), sum_def, map_sum]
  conv in (fun _ ↦ _) =>
    ext
    rw [Bivariate.swap_monomial, mul_comm, ← Polynomial.smul_eq_C_mul,
      ← monomial_one_right_eq_X_pow, ← Polynomial.algebraMap_eq]
  rw [natDegree_sum_eq_of_linearIndepOn _
    (coe_basisMonomials K ▸ (basisMonomials K).linearIndepOn (Φ E).support)]
  apply max_le
  · exact (le_Φ_coeff_generatorIndex_natDegree h).trans <|
      Finset.le_sup (f := fun i ↦ ((Φ E).coeff i).natDegree) <|
      mem_support_iff.mpr (Φ_coeff_generatorIndex_ne_zero h)
  · exact (le_Φ_coeff_natDegree_natDegree h).trans <|
      Finset.le_sup (f := fun i ↦ ((Φ E).coeff i).natDegree) <|
      mem_support_iff.mpr (Φ_coeff_φ_natDegree_ne_zero h)

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:
by 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:
by 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:
by 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:
by 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₁ F₁ : PointedCone R M
C₂ F₂ : PointedCone R N
hF₁ : F₁.IsFaceOf C₁
hF₂ : F₂.IsFaceOf C₂
⊢ IsFaceOf (prod F₁ F₂) (prod C₁ C₂)

Tactic:
refine ⟨fun x hx ↦ by simpa [mem_prod] using ⟨hF₁.le hx.1, hF₂.le hx.2⟩, ?_⟩
  simp only [mem_prod, Prod.fst_add, Prod.smul_fst, Prod.snd_add,
    Prod.smul_snd, and_imp, Prod.forall]
  intro _ _ _ _ _ xc₁ xc₂ yc₁ yc₂ a0 hab₁ hab₂
  exact ⟨hF₁.mem_of_smul_add_mem xc₁ yc₁ a0 hab₁, hF₂.mem_of_smul_add_mem xc₂ yc₂ a0 hab₂⟩

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

Goal state before:
pp: 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)
hf : Function.Injective ⇑f.linear
⊢ ((s.map f.toAffineMap ⋯).altitude i).direction = (AffineSubspace.map f.toAffineMap (s.altitude i)).direction

Tactic:
rw [map_direction, direction_altitude, direction_altitude, Submodule.map_inf _ hf,
    AffineIsometry.linear_eq_linearIsometry, Submodule.map_orthogonal,
    ← AffineIsometry.linear_eq_linearIsometry, map_points, Set.range_comp,
    Set.image_comp, ← AffineMap.map_vectorSpan, inf_assoc, ← Submodule.map_top,
    ← Submodule.map_inf _ hf, top_inf_eq, ← AffineMap.map_vectorSpan]

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

Goal state before:
pp: case e'_2
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
⊢ ((θ.cos • LinearMap.id - θ.sin • ↑o.rightAngleRotation.toLinearEquiv) ∘ₗ (o.rotationAux θ).toLinearMap) x =
    (θ.cos ^ 2 + θ.sin ^ 2) • x

Tactic:
simp only [o.rightAngleRotation_rightAngleRotation, o.rotationAux_apply,
          Function.comp_apply, id, LinearEquiv.coe_coe, LinearIsometry.coe_toLinearMap,
          LinearIsometryEquiv.coe_toLinearEquiv, map_add, map_smul, LinearMap.coe_comp,
          LinearMap.id_coe, LinearMap.smul_apply, LinearMap.sub_apply]
        module

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)
x : V
⊢ (o.rotation ↑π) x = -x

Tactic:
by simp

Goal state after:
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
n : ℕ
s : Simplex ℝ P n
inst✝ : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
⊢ s.points i -ᵥ s.altitudeFoot i ≠ 0

Tactic:
by simp

Goal state after:
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
n : ℕ
s : Simplex ℝ P n
inst✝ : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
⊢ s.points j -ᵥ s.altitudeFoot j ≠ 0

Tactic:
by 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)
x y : V
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
⊢ o.oangle x y = θ ↔ y = (‖y‖ / ‖x‖) • (o.rotation θ) x

Tactic:
have hp := div_pos (norm_pos_iff.2 hy) (norm_pos_iff.2 hx)

Goal state after:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
hp : 0 < ‖y‖ / ‖x‖
⊢ o.oangle x y = θ ↔ y = (‖y‖ / ‖x‖) • (o.rotation θ) x
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
s' : AffineSubspace 𝕜 ↥s
inst✝² : Nonempty ↥s'
inst✝¹ : s'.direction.HasOrthogonalProjection
inst✝ : (map s.subtype s').direction.HasOrthogonalProjection
p : ↥s
⊢ ↑↑((orthogonalProjection s') p) = ↑((orthogonalProjection (map s.subtype s')) ↑p)

Tactic:
by
  rw [eq_comm]
  have : (s'.map s.subtypeₐᵢ.toAffineMap).direction.HasOrthogonalProjection := by
    rw [subtypeₐᵢ_toAffineMap]
    infer_instance
  convert! orthogonalProjection_map s' s.subtypeₐᵢ p

Goal state after:
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
n : ℕ
s : Simplex ℝ P n
inst✝ : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
r : ℝ
hr : r ≠ 0
h : s.points j -ᵥ s.altitudeFoot j = r • (s.points i -ᵥ s.altitudeFoot i)
k : Fin (n + 1)
hki : k ≠ i
hkj : k ≠ j
hki' : s.points k ∈ Set.range (s.faceOpposite i).points
hkj' : s.points k ∈ Set.range (s.faceOpposite j).points
⊢ Set.range s.points = s.points '' ({i}ᶜ ∪ {j}ᶜ)

Tactic:
← Set.image_univ,

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
inst✝ : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
r : ℝ
hr : r ≠ 0
h : s.points j -ᵥ s.altitudeFoot j = r • (s.points i -ᵥ s.altitudeFoot i)
k : Fin (n + 1)
hki : k ≠ i
hkj : k ≠ j
hki' : s.points k ∈ Set.range (s.faceOpposite i).points
hkj' : s.points k ∈ Set.range (s.faceOpposite j).points
⊢ s.points '' Set.univ = s.points '' ({i}ᶜ ∪ {j}ᶜ)
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine

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
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π
⊢ ∠ p₂ p₃ p₁ = 0

Tactic:
rw [angle_comm] at h
  exact angle_eq_zero_of_angle_eq_pi_left h

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

Goal state before:
pp: case mp
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ x = y → ‖x‖ = ‖y‖ ∧ SameRay ℝ x y

Tactic:
rintro rfl
    simp; rfl

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

Goal state before:
pp: V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ ⟪x, y⟫ = ‖x‖ * ‖y‖ * (o.oangle x y).cos

Tactic:
by_cases hx : x = 0; · simp [hx]
  by_cases hy : y = 0; · simp [hy]
  rw [oangle, Real.Angle.cos_coe, Complex.cos_arg, o.norm_kahler]
  · simp only [kahler_apply_apply, real_smul, add_re, ofReal_re, mul_re, I_re, ofReal_im]
    simp [field]
  · exact o.kahler_ne_zero hx hy

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
⊢ -1 ≤ 0

Tactic:
by simp

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x ≠ 0 ∨ y ≠ 0
⊢ -1 ≤ 0

Tactic:
by simp

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
⊢ Real.tan (angle x (x + y)) = ‖y‖ / ‖x‖

Tactic:
by
  by_cases h0 : x = 0; · simp [h0]
  rw [angle_add_eq_arctan_of_inner_eq_zero h h0, Real.tan_arctan]

Goal state after: