mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
inst✝ : DecidablePred FiniteIndex
D : Subgroup G := ⨅ k ∈ {i ∈ s | (H i).FiniteIndex}, H k
hD : D.FiniteIndex
hD_le : ∀ {i : ι}, i ∈ s → (H i).FiniteIndex → D ≤ H i
t : (i : ι) → i ∈ s → (H i).FiniteIndex → Finset ↥(H i)
ht :
  ∀ (i : ι) (hi : i ∈ s) (hfi : (H i).FiniteIndex),
    IsComplement ↑(t i hi hfi) ↑(D.subgroupOf (H i)) ∧ ⋃ g ∈ t i hi hfi, ↑g • ↑D = ↑(H i)
κ : Type (max u_2 u_1) := (i : ↥s) × ↥(if h : (H ↑i).FiniteIndex then t ↑i ⋯ h else {1})
f : κ → G := fun k ↦ g ↑k.fst * ↑↑k.snd
K : κ → Subgroup G := fun k ↦ if (H ↑k.fst).FiniteIndex then D else H ↑k.fst
hcovers' : ⋃ k ∈ Finset.univ, f k • ↑(K k) = Set.univ
k : κ
hkfi : (H ↑k.fst).FiniteIndex
hk : K k = D
i : κ
hi : i ∈ {x | K x = K k}
⊢ f i • ↑(K k) = ?m.488 i hi

Tactic:
by rw [← (Finset.mem_filter.mp hi).2]

Goal state after:
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)
L : Type u_1
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : IsSplittingField K L (X ^ n - C a)
inst✝ : NeZero n
σ : Gal(L/K)
ζ : K
hζ'✝ : ζ ∈ primitiveRoots n K
hζ' : IsPrimitiveRoot ζ n
hn : 0 < n
i : ℕ
left✝ : i < n
⊢ (autEquivRootsOfUnity ⋯ H L) σ • ((algebraMap K L) ζ ^ i * rootOfSplitsXPowSubC ⋯ a L) =
    σ ((algebraMap K L) ζ ^ i * rootOfSplitsXPowSubC ⋯ a L)

Tactic:
simp only [← map_pow, ← Algebra.smul_def, map_smul,
    autEquivRootsOfUnity_apply_rootOfSplit hζ H L]

Goal state after:
K : Type u
inst✝⁴ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
L : Type u_1
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : IsSplittingField K L (X ^ n - C a)
inst✝ : NeZero n
σ : Gal(L/K)
ζ : K
hζ'✝ : ζ ∈ primitiveRoots n K
hζ' : IsPrimitiveRoot ζ n
hn : 0 < n
i : ℕ
left✝ : i < n
⊢ (autEquivRootsOfUnity ⋯ H L) σ • ζ ^ i • rootOfSplitsXPowSubC ⋯ a L =
    ζ ^ i • (autEquivRootsOfUnity hζ H L) σ • rootOfSplitsXPowSubC ⋯ a L
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⟮α⟯ = ⊤
⊢ {α} ⊆ (X ^ finrank K L - C a).rootSet L

Tactic:
rw [Set.singleton_subset_iff, mem_rootSet_of_ne (X_pow_sub_C_ne_zero finrank_pos a),
      aeval_def, eval₂_sub, eval₂_X_pow, eval₂_C, ha, sub_self]

Goal state after:
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: case refine_3
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
inst✝ : DecidablePred FiniteIndex
D : Subgroup G := ⨅ k ∈ {i ∈ s | (H i).FiniteIndex}, H k
hD : D.FiniteIndex
hD_le : ∀ {i : ι}, i ∈ s → (H i).FiniteIndex → D ≤ H i
t : (i : ι) → i ∈ s → (H i).FiniteIndex → Finset ↥(H i)
ht :
  ∀ (i : ι) (hi : i ∈ s) (hfi : (H i).FiniteIndex),
    IsComplement ↑(t i hi hfi) ↑(D.subgroupOf (H i)) ∧ ⋃ g ∈ t i hi hfi, ↑g • ↑D = ↑(H i)
κ : Type (max u_2 u_1) := (i : ↥s) × ↥(if h : (H ↑i).FiniteIndex then t ↑i ⋯ h else {1})
f : κ → G := fun k ↦ g ↑k.fst * ↑↑k.snd
K : κ → Subgroup G := fun k ↦ if (H ↑k.fst).FiniteIndex then D else H ↑k.fst
k : κ
hkfi : (H ↑k.fst).FiniteIndex
hk : K k = D
hcovers' : ⋃ i ∈ {x | K x = D}, f i • ↑D = Set.univ
hHD : ∀ (i : ι), ¬(H i).FiniteIndex → H i ≠ D
hdensity : ∑ i ∈ s, (↑(H i).index)⁻¹ = ↑{x | K x = D}.card * (↑D.index)⁻¹
h : {x | K x = D}.card = D.index
i : ι
hi : i ∈ {x | x ∈ s ∧ (H x).FiniteIndex}
j : ι
hj : j ∈ {x | x ∈ s ∧ (H x).FiniteIndex}
hij : i ≠ j
c : Set G
⊢ c ⊆ (fun i ↦ g i • ↑(H i)) i → c ⊆ (fun i ↦ g i • ↑(H i)) j → c ⊆ ⊥

Tactic:
hi'

Goal state after:
case refine_3
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
inst✝ : DecidablePred FiniteIndex
D : Subgroup G := ⨅ k ∈ {i ∈ s | (H i).FiniteIndex}, H k
hD : D.FiniteIndex
hD_le : ∀ {i : ι}, i ∈ s → (H i).FiniteIndex → D ≤ H i
t : (i : ι) → i ∈ s → (H i).FiniteIndex → Finset ↥(H i)
ht :
  ∀ (i : ι) (hi : i ∈ s) (hfi : (H i).FiniteIndex),
    IsComplement ↑(t i hi hfi) ↑(D.subgroupOf (H i)) ∧ ⋃ g ∈ t i hi hfi, ↑g • ↑D = ↑(H i)
κ : Type (max u_2 u_1) := (i : ↥s) × ↥(if h : (H ↑i).FiniteIndex then t ↑i ⋯ h else {1})
f : κ → G := fun k ↦ g ↑k.fst * ↑↑k.snd
K : κ → Subgroup G := fun k ↦ if (H ↑k.fst).FiniteIndex then D else H ↑k.fst
k : κ
hkfi : (H ↑k.fst).FiniteIndex
hk : K k = D
hcovers' : ⋃ i ∈ {x | K x = D}, f i • ↑D = Set.univ
hHD : ∀ (i : ι), ¬(H i).FiniteIndex → H i ≠ D
hdensity : ∑ i ∈ s, (↑(H i).index)⁻¹ = ↑{x | K x = D}.card * (↑D.index)⁻¹
h : {x | K x = D}.card = D.index
i : ι
hi : i ∈ {x | x ∈ s ∧ (H x).FiniteIndex}
j : ι
hj : j ∈ {x | x ∈ s ∧ (H x).FiniteIndex}
hij : i ≠ j
c : Set G
hi' : c ⊆ (fun i ↦ g i • ↑(H i)) i
⊢ c ⊆ (fun i ↦ g i • ↑(H i)) j → c ⊆ ⊥
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
      (⇑↑(MulOpposite.opLinearEquiv R).symm ∘
        ⇑(↑R (Finsupp.linearCombination (↥B.op) (MulOpposite.op ∘ ⇑A.val ∘ a))) ∘
          ⇑↑(Finsupp.mapRange.linearEquiv B.linearEquivOp)) ↔
    Function.Injective ⇑(Finsupp.linearCombination (↥B.op) (MulOpposite.op ∘ ⇑A.val ∘ a))

Tactic:
LinearEquiv.coe_coe,

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
      (⇑(MulOpposite.opLinearEquiv R).symm ∘
        ⇑(↑R (Finsupp.linearCombination (↥B.op) (MulOpposite.op ∘ ⇑A.val ∘ a))) ∘
          ⇑(Finsupp.mapRange.linearEquiv B.linearEquivOp)) ↔
    Function.Injective ⇑(Finsupp.linearCombination (↥B.op) (MulOpposite.op ∘ ⇑A.val ∘ a))
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: G : Type u_1
inst✝ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
h : ∀ i ∈ s, (H i).FiniteIndex → s.card < (H i).index
⊢ False

Tactic:
apply (one_le_sum_inv_index_of_leftCoset_cover hcovers).not_gt

Goal state after:
G : Type u_1
inst✝ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
h : ∀ i ∈ s, (H i).FiniteIndex → s.card < (H i).index
⊢ ∑ i ∈ s, (↑(H i).index)⁻¹ < 1
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 : Basis ι R ↥B
H : LinearIndependent (↥A) (⇑B.val ∘ ⇑b)
⊢ A.LinearDisjoint B

Tactic:
by
  rw [← mulRightMap_ker_eq_bot_iff_linearIndependent] at H
  exact Submodule.LinearDisjoint.of_basis_right _ _ b H

Goal state after:
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:
simp_rw [normalizedTraceAux, ← LinearEquiv.finrank_eq e.toLinearEquiv]

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 ⋯)
⊢ (↑(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)
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
⊢ Module.rank ↥B ↥(toSubmodule (Algebra.adjoin ↥B ↑A)) = Module.rank R ↥A

Tactic:
Module.Free.rank_eq_card_chooseBasisIndex R A,

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
inst✝³ : Free R ↥A
inst✝² : Flat R ↥B
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
⊢ Module.rank ↥B ↥(toSubmodule (Algebra.adjoin ↥B ↑A)) = Cardinal.mk (Free.ChooseBasisIndex R ↥A)
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:
h2,

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).Coprime 0
a✝ : Nontrivial R
h1 : ¬finrank R ↥A = 0
h2 : finrank R ↥B = 0
⊢ A.LinearDisjoint B
Module: Mathlib.FieldTheory.RatFunc.Degree

Goal state before:
pp: K : Type u
inst✝ : Field K
p : K[X]
⊢ ↑((algebraMap K[X] K⟮X⟯) p).num.natDegree - ↑((algebraMap K[X] K⟮X⟯) p).denom.natDegree = ↑p.natDegree

Tactic:
RatFunc.num_algebraMap,

Goal state after:
K : Type u
inst✝ : Field K
p : K[X]
⊢ ↑p.natDegree - ↑((algebraMap K[X] K⟮X⟯) p).denom.natDegree = ↑p.natDegree
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

Goal state before:
pp: K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ¬∃ c, f = C c
⊢ f.num.natDegree ≤ (f.minpolyX ↥K⟮f⟯).natDegree

Tactic:
have f_ne_zero : f ≠ 0 := by
    rintro rfl
    exact hf ⟨0, (RingHom.map_zero C).symm⟩

Goal state after:
K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ¬∃ c, f = C c
f_ne_zero : f ≠ 0
⊢ f.num.natDegree ≤ (f.minpolyX ↥K⟮f⟯).natDegree
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
C : PointedCone R N
hC : DualFG p C
⊢ DualFG LinearMap.id C

Tactic:
obtain ⟨s, rfl⟩ := hC

Goal state after:
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
⊢ DualFG LinearMap.id (dual p ↑s)
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
C : PointedCone R M
hC : Submodule.FG C
⊢ DualFG p (dual p ↑C)

Tactic:
obtain ⟨s, rfl⟩ := hC

Goal state after:
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
⊢ DualFG p (dual p ↑(Submodule.span { c // 0 ≤ c } ↑s))
Module: Mathlib.FieldTheory.RatFunc.Valuation

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F⟮X⟯
x y : F⟮X⟯
⊢ inftyValuationDef F (x * y) = inftyValuationDef F x * inftyValuationDef F y

Tactic:
rw [inftyValuationDef, inftyValuationDef, inftyValuationDef]
  by_cases hx : x = 0
  · rw [hx, zero_mul, if_pos (Eq.refl _), zero_mul]
  · by_cases hy : y = 0
    · rw [hy, mul_zero, if_pos (Eq.refl _), mul_zero]
    · simp_all [RatFunc.intDegree_mul]

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 ≠ ⊥
this :
  ((Φ E).coeff (generatorIndex h)).natDegree + (generator E).denom.natDegree =
    (c E).num.natDegree + (generator E).num.natDegree
⊢ (f E).natDegree ≤ ((Φ E).coeff (generatorIndex h)).natDegree

Tactic:
grind [natDegree_le_of_dvd (generator_denom_dvd_c_num h) (num_ne_zero (c_ne_zero h))]

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

Goal state before:
pp: case h₂
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ (g E).natDegree ≤ (Φ E).support.sup fun i ↦ ((Φ E).coeff i).natDegree

Tactic:
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.Hull

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R X
s : Set X
x : X
hs : IsConvexSet R s
hx : x ∉ (convexHull R) (s \ {x})
y : X
hy : y ∈ (convexHull R) (s \ {x})
⊢ y ∉ {x}

Tactic:
rintro rfl; exact hx hy

Goal state after:
Module: Mathlib.Geometry.Convex.Hull

Goal state before:
pp: R : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : ConvexSpace R X
inst✝ : ConvexSpace R Y
f : X → Y
hf : IsAffineMap R f
s : Set X
⊢ (convexHull R) s ⊆ f ⁻¹' (convexHull R) (f '' s) ∧ (convexHull R) (f '' s) ⊆ f '' (convexHull R) s

Tactic:
(IsConvexSet.convexHull.preimage hf).convexHull_subset_iff,

Goal state after:
R : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : ConvexSpace R X
inst✝ : ConvexSpace R Y
f : X → Y
hf : IsAffineMap R f
s : Set X
⊢ s ⊆ f ⁻¹' (convexHull R) (f '' s) ∧ (convexHull R) (f '' s) ⊆ f '' (convexHull R) s
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: case e'_4.e'_3
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ (f E).natDegree = (Polynomial.C (g E) * Polynomial.map Polynomial.C (f E)).natDegree

Tactic:
natDegree_mul (C_ne_zero.mpr (generator E).denom_ne_zero)
      (Polynomial.map_ne_zero (num_ne_zero (generator_ne_zero h))),

Goal state after:
case e'_4.e'_3
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ (f E).natDegree =
    (Polynomial.C (generator E).denom).natDegree + (Polynomial.map Polynomial.C (generator E).num).natDegree
Module: Mathlib.Geometry.Diffeology.Basic

Goal state before:
pp: X : Type u_1
d : DiffeologicalSpace X
t : TopologicalSpace X
h : dTopology = t
⊢ ∀ {u : Set X}, TopologicalSpace.IsOpen u ↔ ∀ {n : ℕ}, ∀ p ∈ plots n, IsOpen (p ⁻¹' u)

Tactic:
intro _; rw [← d.isOpen_iff_preimages_plots, ← h]

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

Goal state before:
pp: 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}
⊢ p ∈ {p | d.isPlot p}

Tactic:
by
    refine d.isPlotOn_univ.mp <| d.locality _ fun x _ ↦ ?_
    let ⟨u, hu, hxu, hu'⟩ := h x
    let ⟨ε, hε, hε'⟩ := Metric.isOpen_iff.mp hu x hxu
    have h : d.isPlot (p ∘ OpenPartialHomeomorph.univBall x ε) := hu'
      (f := OpenPartialHomeomorph.univBall x ε)
      (fun x' ↦ by
        replace h := (OpenPartialHomeomorph.univBall x ε).map_source (x := x')
        rw [OpenPartialHomeomorph.univBall_target x hε] at h
        aesop)
      OpenPartialHomeomorph.contDiff_univBall
    have h' := d.isPlotOn_reparam (Metric.isOpen_ball) (Set.mapsTo_univ _ _)
      (d.isPlotOn_univ.mpr h) (OpenPartialHomeomorph.contDiffOn_univBall_symm (c := x) (r := ε))
    refine ⟨_, Metric.isOpen_ball, Metric.mem_ball_self hε, (d.isPlotOn_congr _ ?_).mp h'⟩
    rw [Function.comp_assoc, ← OpenPartialHomeomorph.coe_trans]
    apply Set.EqOn.comp_left
    convert! (OpenPartialHomeomorph.symm_trans_self (OpenPartialHomeomorph.univBall x ε)).2
    simp [OpenPartialHomeomorph.univBall_target x hε]

Goal state after:
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 : P
⊢ ↑(s.direction.orthogonalProjectionOnto (p -ᵥ ↑(Classical.arbitrary ↥s))) - (p -ᵥ ↑(Classical.arbitrary ↥s)) ∈
    s.directionᗮ

Tactic:
← Submodule.neg_mem_iff,

Goal state after:
𝕜 : 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
⊢ -(↑(s.direction.orthogonalProjectionOnto (p -ᵥ ↑(Classical.arbitrary ↥s))) - (p -ᵥ ↑(Classical.arbitrary ↥s))) ∈
    s.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₁ p₂ : P
hp₁ : p₁ ∈ s
⊢ dist p₁ p₂ * dist p₁ p₂ =
    dist p₁ ↑((orthogonalProjection s) p₂) * dist p₁ ↑((orthogonalProjection s) p₂) +
      dist p₂ ↑((orthogonalProjection s) p₂) * dist p₂ ↑((orthogonalProjection s) p₂)

Tactic:
rw [dist_comm p₂ _, dist_eq_norm_vsub V p₁ _, dist_eq_norm_vsub V p₁ _, dist_eq_norm_vsub V _ p₂,
    ← vsub_add_vsub_cancel p₁ (orthogonalProjection s p₂) p₂,
    norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero (𝕜 := 𝕜)]
  exact Submodule.inner_right_of_mem_orthogonal (vsub_orthogonalProjection_mem_direction p₂ hp₁)
    (orthogonalProjection_vsub_mem_direction_orthogonal s p₂)

Goal state after:
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✝ : s.direction.HasOrthogonalProjection
p₁ p₂ : P
hp₂ : p₂ ∈ s
⊢ dist p₁ ↑((orthogonalProjection s) p₁) = dist p₁ p₂ ↔ ↑((orthogonalProjection s) p₁) = p₂

Tactic:
by
  have : Nonempty s := ⟨p₂, hp₂⟩
  constructor
  · intro h
    rwa [← sq_eq_sq₀ dist_nonneg dist_nonneg, pow_two, pow_two, dist_comm _ p₂,
      dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq _ hp₂,
      right_eq_add, mul_eq_zero, dist_eq_zero, or_self, eq_comm] at h
  · intro h
    nth_rw 4 [← h]

Goal state after:
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 : P
x : P := ↑(Classical.arbitrary ↥s)
v : V := s.direction.starProjection (p -ᵥ x)
⊢ s.direction.reflection (p -ᵥ x) +ᵥ x = ((v +ᵥ x) -ᵥ p) +ᵥ v +ᵥ x

Tactic:
Submodule.reflection_apply,

Goal state after:
𝕜 : 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
x : P := ↑(Classical.arbitrary ↥s)
v : V := s.direction.starProjection (p -ᵥ x)
⊢ (2 • s.direction.starProjection (p -ᵥ x) - (p -ᵥ x)) +ᵥ x = ((v +ᵥ x) -ᵥ p) +ᵥ v +ᵥ 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
inst✝ : s.direction.HasOrthogonalProjection
p : P
⊢ (reflection s) ((reflection s) p) = p

Tactic:
by
  simp [reflection, -AffineIsometryEquiv.map_vadd]

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₁ s₂ : AffineSubspace 𝕜 P
inst✝³ : Nonempty ↥s₁
inst✝² : Nonempty ↥s₂
inst✝¹ : s₁.direction.HasOrthogonalProjection
inst✝ : s₂.direction.HasOrthogonalProjection
p : P
⊢ ↑((orthogonalProjection s₁) p) = ↑((orthogonalProjection s₂) p) →
    (↑((orthogonalProjection s₁) p) -ᵥ p) +ᵥ ↑((orthogonalProjection s₁) p) =
      (↑((orthogonalProjection s₂) p) -ᵥ p) +ᵥ ↑((orthogonalProjection s₂) p)

Tactic:
· intro h
    rw [h]

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

Goal state before:
pp: case mpr
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ x ≠ 0 ∧ y ≠ 0 ∧ o.oangle x (-y) = 0 → o.oangle x y = ↑π

Tactic:
rintro ⟨hx, hy, h⟩

Goal state after:
case mpr
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
h : o.oangle x (-y) = 0
⊢ o.oangle x y = ↑π
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
⊢ angle x (x + y) = Real.arctan (‖y‖ / ‖x‖)

Tactic:
rw [angle_add_eq_arcsin_of_inner_eq_zero h (Or.inl h0), Real.arctan_eq_arcsin, ←
    div_mul_eq_div_div, norm_add_eq_sqrt_iff_real_inner_eq_zero.2 h]
  nth_rw 3 [← Real.sqrt_sq (norm_nonneg x)]
  rw_mod_cast [← Real.sqrt_mul (sq_nonneg _), div_pow, pow_two, pow_two, mul_add, mul_one, mul_div,
    mul_comm (‖x‖ * ‖x‖), ← mul_div, div_self (mul_self_pos.2 (norm_ne_zero_iff.2 h0)).ne', mul_one]

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
⊢ angle x (x - y) ≤ π / 2

Tactic:
by
  rw [← neg_eq_zero, ← inner_neg_right] at h
  rw [sub_eq_add_neg]
  exact angle_add_le_pi_div_two_of_inner_eq_zero h

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : dist p₁ p₂ = dist p₁ p₃
⊢ |(∡ p₁ p₂ p₃).toReal| < π / 2

Tactic:
simp_rw [dist_eq_norm_vsub V] at h
  rw [oangle, ← vsub_sub_vsub_cancel_left p₃ p₂ p₁]
  exact o.abs_oangle_sub_right_toReal_lt_pi_div_two h

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

Goal state before:
pp: case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π / 2
hp₂ : ¬p₂ = p₃
hp₁ : ¬p₁ = p₃
⊢ |(∡ p₂ p₃ p₁).toReal| < π / 2

Tactic:
← angle_eq_abs_oangle_toReal hp₂ hp₁

Goal state after:
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π / 2
hp₂ : ¬p₂ = p₃
hp₁ : ¬p₁ = p₃
⊢ ∠ p₂ p₃ p₁ < π / 2