mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.IsRealClosed.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
k : ℤ
hk : Odd k
⊢ ∃ r, x = r ^ k

Tactic:
by
  rcases k.eq_nat_or_neg with ⟨n, rfl | rfl⟩
  · simpa using exists_eq_pow_of_odd x (by simpa using hk)
  · rcases exists_eq_pow_of_odd x (by simpa using hk) with ⟨r, hr⟩
    exact ⟨r⁻¹, by simpa using hr⟩

Goal state after:
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : CommRing K
inst✝¹⁰ : CommRing L
inst✝⁹ : CommRing M
inst✝⁸ : CommRing N
i : K →+* L
j : K →+* M
g : L →+* N
p : ℕ
inst✝⁷ : ExpChar M p
inst✝⁶ : ExpChar K p
inst✝⁵ : PerfectRing M p
inst✝⁴ : IsPRadical i p
inst✝³ : ExpChar L p
inst✝² : ExpChar N p
inst✝¹ : IsPRadical g p
inst✝ : IsPRadical (g.comp i) p
⊢ (fun f ↦ f.comp (g.comp i)) (lift g (lift i j p) p) = (fun f ↦ f.comp (g.comp i)) (lift (g.comp i) j p)

Tactic:
simp_rw [← RingHom.comp_assoc _ _ (lift g _ p), lift_comp]

Goal state after:
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: case pos
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq (Subgroup G)
n : ℕ
ih :
  ∀ m < n,
    ∀ {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι},
      ⋃ i ∈ s, g i • ↑(H i) = Set.univ →
        ∀ j ∈ s,
          ⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H i) ≠ Set.univ →
            m = (Finset.image H s).card → ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
j : ι
hj : j ∈ s
hcovers'✝ : ⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H i) ≠ Set.univ
hn : n = (Finset.image H s).card
x : G
hx : ∀ (y : G), y • ↑(H j) ⊆ ⋃ i ∈ {x ∈ s | H x ≠ H j}, (y * x⁻¹ * g i) • ↑(H i)
κ : Type u_2 := ↥({x ∈ s | H x ≠ H j}) × Option ↥({x ∈ s | H x = H j})
f : κ → G :=
  fun x_1 ↦
    match x_1 with
    | (k₁, some k₂) => g ↑k₂ * x⁻¹ * g ↑k₁
    | (k₁, none) => g ↑k₁
K : κ → Subgroup G := fun k ↦ H ↑k.1
hK' : ∀ (k : κ), K k ∈ (Finset.image H s).erase (H j)
hK : ∀ (k : κ), K k ≠ H j
hcovers : ⋃ k ∈ Finset.univ, f k • ↑(K k) = Set.univ
k : κ
hcovers' : ⋃ i ∈ {x | K x = K k}, f i • ↑(K i) = Set.univ
⊢ ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex

Tactic:
rw [Set.iUnion₂_congr fun i hi => by rw [(Finset.mem_filter.mp hi).right]] at hcovers'

Goal state after:
case pos
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq (Subgroup G)
n : ℕ
ih :
  ∀ m < n,
    ∀ {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι},
      ⋃ i ∈ s, g i • ↑(H i) = Set.univ →
        ∀ j ∈ s,
          ⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H i) ≠ Set.univ →
            m = (Finset.image H s).card → ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
j : ι
hj : j ∈ s
hcovers'✝ : ⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H i) ≠ Set.univ
hn : n = (Finset.image H s).card
x : G
hx : ∀ (y : G), y • ↑(H j) ⊆ ⋃ i ∈ {x ∈ s | H x ≠ H j}, (y * x⁻¹ * g i) • ↑(H i)
κ : Type u_2 := ↥({x ∈ s | H x ≠ H j}) × Option ↥({x ∈ s | H x = H j})
f : κ → G :=
  fun x_1 ↦
    match x_1 with
    | (k₁, some k₂) => g ↑k₂ * x⁻¹ * g ↑k₁
    | (k₁, none) => g ↑k₁
K : κ → Subgroup G := fun k ↦ H ↑k.1
hK' : ∀ (k : κ), K k ∈ (Finset.image H s).erase (H j)
hK : ∀ (k : κ), K k ≠ H j
hcovers : ⋃ k ∈ Finset.univ, f k • ↑(K k) = Set.univ
k : κ
hcovers' : ⋃ i ∈ {x | K x = K k}, f i • ↑(K k) = Set.univ
⊢ ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: case pos
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
j : ι
hj : j ∈ s
hcovers' : ⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H i) = Set.univ
⊢ ∃ k ∈ s, (H k).FiniteIndex

Tactic:
rw [Set.iUnion₂_congr fun i hi => by rw [(Finset.mem_filter.mp hi).right]] at hcovers'

Goal state after:
case pos
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
j : ι
hj : j ∈ s
hcovers' : ⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H j) = Set.univ
⊢ ∃ k ∈ s, (H k).FiniteIndex
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 ∈ {x | K x = D}, f i • ↑D = Set.univ

Tactic:
← hk,

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
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 ∈ {x | K x = K k}, f i • ↑(K k) = Set.univ
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: K : Type u
inst✝¹ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
inst✝ : NeZero n
e : Gal(K[n√a]/K)
this✝ : Fact (Irreducible (X ^ n - C a))
this : Algebra K K[n√a] := ⋯
⊢ ↑((↑(autAdjoinRootXPowSubC n a)).toFun (AdjoinRootXPowSubCEquivToRootsOfUnity hζ H e)) (root (X ^ n - C a)) =
    ↑e (root (X ^ n - C a))

Tactic:
simp only [AdjoinRootXPowSubCEquivToRootsOfUnity, AdjoinRoot.algebraMap_eq, OneHom.toFun_eq_coe,
      MonoidHom.toOneHom_coe, AlgEquiv.coe_toAlgHom, autAdjoinRootXPowSubC_root, Algebra.smul_def]

Goal state after:
K : Type u
inst✝¹ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
inst✝ : NeZero n
e : Gal(K[n√a]/K)
this✝ : Fact (Irreducible (X ^ n - C a))
this : Algebra K K[n√a] := inferInstance
⊢ (of (X ^ n - C a))
        ↑↑((rootsOfUnityEquivOfPrimitiveRoots ⋯ hζ).symm
              (rootsOfUnity.mkOfPowEq (if a = 0 then 1 else e (root (X ^ n - C a)) / root (X ^ n - C a)) ⋯)) *
      root (X ^ n - C a) =
    e (root (X ^ n - C a))
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)
α : L
hα : α ^ n = (algebraMap K L) a
inst✝ : NeZero n
σ : Gal(L/K)
ζ : K
hζ'✝ : ζ ∈ primitiveRoots n K
hζ' : IsPrimitiveRoot ζ n
hn : 0 < n
⊢ (autEquivRootsOfUnity ⋯ H L) σ • α = σ α

Tactic:
← mem_nthRoots hn,

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)
α : L
hα : α ∈ nthRoots n ((algebraMap K L) a)
inst✝ : NeZero n
σ : Gal(L/K)
ζ : K
hζ'✝ : ζ ∈ primitiveRoots n K
hζ' : IsPrimitiveRoot ζ n
hn : 0 < n
⊢ (autEquivRootsOfUnity ⋯ H L) σ • α = σ α
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 = ⊤
⊢ restrictScalars R (Algebra.TensorProduct.productLeftAlgHom (Algebra.ofId (↥A) S) B.val).range = A ⊔ B

Tactic:
exact mulMap_range A B

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 B : IntermediateField F E
inst✝ : FiniteDimensional F E
h₁ : A.LinearDisjoint B.toSubalgebra
h₂ : A ⊔ B = ⊤
x : ↥B
⊢ (Algebra.norm ↥A) ((algebraMap (↥B) E) x) = (algebraMap F ↥A) ((Algebra.norm F) x)

Tactic:
refine h₁.norm_algebraMap ?_ x

Goal state after:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
A B : IntermediateField F E
inst✝ : FiniteDimensional F E
h₁ : A.LinearDisjoint B.toSubalgebra
h₂ : A ⊔ B = ⊤
x : ↥B
⊢ A.toSubalgebra ⊔ B.toSubalgebra = ⊤
Module: Mathlib.FieldTheory.RatFunc.Degree

Goal state before:
pp: case neg
K : Type u
inst✝ : Field K
x : K⟮X⟯
hx : ¬x = 0
⊢ (-x).intDegree = x.intDegree

Tactic:
· rw [intDegree, intDegree, ← natDegree_neg x.num]
    exact
      natDegree_sub_eq_of_prod_eq (num_ne_zero (neg_ne_zero.mpr hx)) (denom_ne_zero (-x))
        (neg_ne_zero.mpr (num_ne_zero hx)) (denom_ne_zero x) (num_denom_neg x)

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
inst✝ : IsPurelyInseparable F E
⊢ Cardinal.lift.{w, v} (Module.rank F E) * Cardinal.lift.{v, w} (insepDegree E K) =
    Cardinal.lift.{v, w} (insepDegree F K)

Tactic:
have h := (separableClosure F K).linearDisjoint_of_isPurelyInseparable_of_isSeparable E
    |>.lift_rank_right_mul_lift_adjoin_rank_eq_of_isAlgebraic_left
  rwa [separableClosure.adjoin_eq_of_isAlgebraic] at h

Goal state after:
Module: Mathlib.FieldTheory.Relrank

Goal state before:
pp: E : Type v
inst✝ : Field E
A : Subfield E
⊢ A.relrank ⊤ = Module.rank (↥A) E

Tactic:
relrank_eq_rank_of_le (show A ≤ ⊤ from le_top),

Goal state after:
E : Type v
inst✝ : Field E
A : Subfield E
⊢ Module.rank ↥A ↥(extendScalars ⋯) = Module.rank (↥A) E
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₁ s₂ : AffineSubspace 𝕜 P
inst✝⁴ : Nonempty ↥s₁
inst✝³ : Nonempty ↥s₂
inst✝² : s₁.direction.HasOrthogonalProjection
inst✝¹ : s₂.direction.HasOrthogonalProjection
p : P
h : ↑((orthogonalProjection s₁) p) = ↑((orthogonalProjection s₂) p)
inst✝ : (s₁ ⊔ s₂).direction.HasOrthogonalProjection
⊢ ↑((orthogonalProjection (s₁ ⊔ s₂)) p) = ↑((orthogonalProjection s₁) p)

Tactic:
coe_orthogonalProjection_eq_iff_mem

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₁ s₂ : AffineSubspace 𝕜 P
inst✝⁴ : Nonempty ↥s₁
inst✝³ : Nonempty ↥s₂
inst✝² : s₁.direction.HasOrthogonalProjection
inst✝¹ : s₂.direction.HasOrthogonalProjection
p : P
h : ↑((orthogonalProjection s₁) p) = ↑((orthogonalProjection s₂) p)
inst✝ : (s₁ ⊔ s₂).direction.HasOrthogonalProjection
⊢ ↑((orthogonalProjection s₁) p) ∈ s₁ ⊔ s₂ ∧ p -ᵥ ↑((orthogonalProjection s₁) p) ∈ (s₁ ⊔ s₂).directionᗮ
Module: Mathlib.Geometry.Euclidean.Altitude

Goal state before:
pp: case mp.left
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
p : P
h : vectorSpan ℝ {p, s.points i} = (s.altitude i).direction
heq : p = s.points i
⊢ False

Tactic:
rw [heq, Set.pair_eq_singleton, vectorSpan_singleton] at h

Goal state after:
case mp.left
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
p : P
h : ⊥ = (s.altitude i).direction
heq : p = s.points i
⊢ False
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
V₂ : Type u_4
P₂ : Type u_5
inst✝⁸ : NormedAddCommGroup V₂
inst✝⁷ : InnerProductSpace 𝕜 V₂
inst✝⁶ : MetricSpace P
inst✝⁵ : NormedAddTorsor V P
inst✝⁴ : MetricSpace P₂
inst✝³ : NormedAddTorsor V₂ P₂
s : AffineSubspace 𝕜 P
inst✝² : Nonempty ↥s
inst✝¹ : s.direction.HasOrthogonalProjection
f : P →ᵃⁱ[𝕜] P₂
inst✝ : (map f.toAffineMap s).direction.HasOrthogonalProjection
p : P
⊢ ↑((orthogonalProjection (map f.toAffineMap s)) (f p)) = f ↑((orthogonalProjection s) p)

Tactic:
coe_orthogonalProjection_eq_iff_mem

Goal state after:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝¹¹ : RCLike 𝕜
inst✝¹⁰ : NormedAddCommGroup V
inst✝⁹ : InnerProductSpace 𝕜 V
V₂ : Type u_4
P₂ : Type u_5
inst✝⁸ : NormedAddCommGroup V₂
inst✝⁷ : InnerProductSpace 𝕜 V₂
inst✝⁶ : MetricSpace P
inst✝⁵ : NormedAddTorsor V P
inst✝⁴ : MetricSpace P₂
inst✝³ : NormedAddTorsor V₂ P₂
s : AffineSubspace 𝕜 P
inst✝² : Nonempty ↥s
inst✝¹ : s.direction.HasOrthogonalProjection
f : P →ᵃⁱ[𝕜] P₂
inst✝ : (map f.toAffineMap s).direction.HasOrthogonalProjection
p : P
⊢ f ↑((orthogonalProjection s) p) ∈ map f.toAffineMap s ∧
    f p -ᵥ f ↑((orthogonalProjection s) p) ∈ (map f.toAffineMap s).directionᗮ
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation

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‖ = ‖y‖ → (o.rotation (o.oangle x y)) x = y

Tactic:
· intro h
    rw [o.eq_iff_oangle_eq_zero_of_norm_eq] <;> simp [h]

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

Goal state before:
pp: case neg
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
θ : Real.Angle
hx : ¬x = 0
⊢ o.oangle x y = θ ↔ x ≠ 0 ∧ y ≠ 0 ∧ y = (‖y‖ / ‖x‖) • (o.rotation θ) x ∨ θ = 0 ∧ (x = 0 ∨ y = 0)

Tactic:
by_cases hy : y = 0
    · simp [hy, eq_comm]
    · rw [o.oangle_eq_iff_eq_norm_div_norm_smul_rotation_of_ne_zero hx hy]
      simp [hx, hy]

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

Goal state before:
pp: case a.refine_2.refine_1
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)
hk : ∃ k, k ≠ i ∧ k ≠ j
hs :
  vectorSpan ℝ (Set.range s.points) =
    vectorSpan ℝ (Set.range (s.faceOpposite i).points) ⊔ vectorSpan ℝ (Set.range (s.faceOpposite j).points)
⊢ r • (s.points i -ᵥ s.altitudeFoot i) ∈ (vectorSpan ℝ (Set.range (s.faceOpposite i).points))ᗮ

Tactic:
← direction_affineSpan

Goal state after:
case a.refine_2.refine_1
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)
hk : ∃ k, k ≠ i ∧ k ≠ j
hs :
  vectorSpan ℝ (Set.range s.points) =
    vectorSpan ℝ (Set.range (s.faceOpposite i).points) ⊔ vectorSpan ℝ (Set.range (s.faceOpposite j).points)
⊢ r • (s.points i -ᵥ s.altitudeFoot i) ∈ (affineSpan ℝ (Set.range (s.faceOpposite i).points)).directionᗮ
Module: Mathlib.Geometry.Euclidean.Altitude

Goal state before:
pp: case a.refine_2.refine_2
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)
hk : ∃ k, k ≠ i ∧ k ≠ j
hs :
  vectorSpan ℝ (Set.range s.points) =
    vectorSpan ℝ (Set.range (s.faceOpposite i).points) ⊔ vectorSpan ℝ (Set.range (s.faceOpposite j).points)
⊢ s.points j -ᵥ s.altitudeFoot j ∈ (vectorSpan ℝ (Set.range (s.faceOpposite j).points))ᗮ

Tactic:
← direction_affineSpan

Goal state after:
case a.refine_2.refine_2
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)
hk : ∃ k, k ≠ i ∧ k ≠ j
hs :
  vectorSpan ℝ (Set.range s.points) =
    vectorSpan ℝ (Set.range (s.faceOpposite i).points) ⊔ vectorSpan ℝ (Set.range (s.faceOpposite j).points)
⊢ s.points j -ᵥ s.altitudeFoot j ∈ (affineSpan ℝ (Set.range (s.faceOpposite j).points)).directionᗮ
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
m : P := midpoint ℝ p₁ p₂
h : ‖p₃ -ᵥ m - (p₁ -ᵥ m)‖ = ‖p₃ -ᵥ m + (p₁ -ᵥ m)‖
h1 : p₃ -ᵥ p₁ = p₃ -ᵥ m - (p₁ -ᵥ m)
h2 : p₃ -ᵥ p₂ = p₃ -ᵥ m + (p₁ -ᵥ m)
⊢ ∠ p₃ (midpoint ℝ p₁ p₂) p₁ = π / 2

Tactic:
exact (norm_add_eq_norm_sub_iff_angle_eq_pi_div_two (p₃ -ᵥ m) (p₁ -ᵥ m)).mp h.symm

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

Goal state before:
pp: case inl.inl
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y z : V
h : InnerProductGeometry.angle 0 x = InnerProductGeometry.angle y z
hs : (o.oangle 0 x).sign = (o.oangle y z).sign
⊢ (o.oangle 0 x).sign = 0 ∧ (o.oangle y z).sign = 0

Tactic:
simpa using hs.symm

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

Goal state before:
pp: case inl.inr
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
w y z : V
h : InnerProductGeometry.angle w 0 = InnerProductGeometry.angle y z
hs : (o.oangle w 0).sign = (o.oangle y z).sign
⊢ (o.oangle w 0).sign = 0 ∧ (o.oangle y z).sign = 0

Tactic:
simpa using hs.symm

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

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₂⟫ = 0
⊢ Real.cos (∠ p₂ p₃ p₁) = dist p₃ p₂ / dist p₁ p₃

Tactic:
rw [angle, dist_eq_norm_vsub' V p₃ p₂, dist_eq_norm_vsub V p₁ p₃, ← vsub_add_vsub_cancel p₁ p₂ p₃,
    add_comm, cos_angle_add_of_inner_eq_zero h]

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

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₃ = π / 2
h0 : p₁ = p₂ ∨ p₃ ≠ p₂
⊢ Real.tan (∠ p₂ p₃ p₁) * dist p₃ p₂ = dist p₁ p₂

Tactic:
rw [angle, ← inner_eq_zero_iff_angle_eq_pi_div_two, real_inner_comm, ← neg_eq_zero, ←
    inner_neg_left, neg_vsub_eq_vsub_rev] at h
  rw [ne_comm, ← @vsub_ne_zero V, ← @vsub_eq_zero_iff_eq V, or_comm] at h0
  rw [angle, dist_eq_norm_vsub V p₁ p₂, dist_eq_norm_vsub' V p₃ p₂, ← vsub_add_vsub_cancel p₁ p₂ p₃,
    add_comm, tan_angle_add_mul_norm_of_inner_eq_zero h h0]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Bisector

Goal state before:
pp: case refine_1
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst✝¹ : s₁.direction.HasOrthogonalProjection
inst✝ : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
h' : p ∈ s₁
this✝ : Nonempty ↥s₁
this : Nonempty ↥s₂
h : dist p ↑((orthogonalProjection s₁) p) = dist p ↑((orthogonalProjection s₂) p)
⊢ ∠ p p' ↑((orthogonalProjection s₁) p) = ∠ p p' ↑((orthogonalProjection s₂) p)

pp: case refine_2
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst✝¹ : s₁.direction.HasOrthogonalProjection
inst✝ : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
h' : p ∈ s₁
this✝ : Nonempty ↥s₁
this : Nonempty ↥s₂
h : ∠ p p' ↑((orthogonalProjection s₁) p) = ∠ p p' ↑((orthogonalProjection s₂) p)
⊢ dist p ↑((orthogonalProjection s₁) p) = dist p ↑((orthogonalProjection s₂) p)

Tactic:
· rw [orthogonalProjection_eq_self_iff.2 h'] at h ⊢
    rw [dist_self, zero_eq_dist, eq_comm, orthogonalProjection_eq_self_iff] at h
    rw [orthogonalProjection_eq_self_iff.2 h]

Goal state after:
case refine_2
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst✝¹ : s₁.direction.HasOrthogonalProjection
inst✝ : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
h' : p ∈ s₁
this✝ : Nonempty ↥s₁
this : Nonempty ↥s₂
h : ∠ p p' ↑((orthogonalProjection s₁) p) = ∠ p p' ↑((orthogonalProjection s₂) p)
⊢ dist p ↑((orthogonalProjection s₁) p) = dist p ↑((orthogonalProjection s₂) p)
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₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ {p₅, p₁, p₂}
s : Set (P × P × P) := (fun x ↦ (↑x.1, p₅, x.2 +ᵥ ↑x.1)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
hf : ContinuousOn (fun p ↦ ∡ p.1 p.2.1 p.2.2) s
q : P
r : ℝ
hv0 : r • (p₂ -ᵥ p₁) ≠ 0
hq : q ∈ line[ℝ, p₁, p₂]
⊢ AffineIndependent ℝ ![q, p₅, r • (p₂ -ᵥ p₁) +ᵥ q]

Tactic:
refine affineIndependent_of_ne_of_mem_of_notMem_of_mem ?_ hq
          (fun h => hc₅₁₂ ((collinear_insert_iff_of_mem_affineSpan h).2 (collinear_pair _ _ _))) ?_

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
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ {p₅, p₁, p₂}
s : Set (P × P × P) := (fun x ↦ (↑x.1, p₅, x.2 +ᵥ ↑x.1)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
hf : ContinuousOn (fun p ↦ ∡ p.1 p.2.1 p.2.2) s
q : P
r : ℝ
hv0 : r • (p₂ -ᵥ p₁) ≠ 0
hq : q ∈ line[ℝ, p₁, p₂]
⊢ q ≠ r • (p₂ -ᵥ p₁) +ᵥ q

case refine_2
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₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ {p₅, p₁, p₂}
s : Set (P × P × P) := (fun x ↦ (↑x.1, p₅, x.2 +ᵥ ↑x.1)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
hf : ContinuousOn (fun p ↦ ∡ p.1 p.2.1 p.2.2) s
q : P
r : ℝ
hv0 : r • (p₂ -ᵥ p₁) ≠ 0
hq : q ∈ line[ℝ, p₁, p₂]
⊢ r • (p₂ -ᵥ p₁) +ᵥ q ∈ line[ℝ, p₁, p₂]