mathlib-initiative/mathlib-tactics huggingface dataset:
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
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
i : ↥s
x✝ : i ∈ s.attach
hfi : (H ↑i).FiniteIndex
⊢ ∑ s_1, ↑(if K ⟨i, s_1⟩ = D then 1 else 0) = (↑(H ↑i).index)⁻¹ * ↑D.index

Tactic:
← relIndex_mul_index (hD_le i.2 hfi),

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
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
i : ↥s
x✝ : i ∈ s.attach
hfi : (H ↑i).FiniteIndex
⊢ ∑ s_1, ↑(if K ⟨i, s_1⟩ = D then 1 else 0) = (↑(H ↑i).index)⁻¹ * ↑(D.relIndex (H ↑i) * (H ↑i).index)
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 b : K
E : IntermediateField F K := F⟮a⟯ ⊔ F⟮b⟯
this✝ : FiniteDimensional F ↥F⟮a⟯
this : FiniteDimensional F ↥F⟮b⟯
ha : a ∈ E
hb : b ∈ E
hab : a + b ∈ E
a' : ↥E := ⟨a, ha⟩
b' : ↥E := ⟨b, hb⟩
ab' : ↥E := ⟨a + b, hab⟩
⊢ normalizedTraceAux F K (a + b) = normalizedTraceAux F (↥E) a' + normalizedTraceAux F K b

Tactic:
normalizedTraceAux_intermediateField F K b',

Goal state after:
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 b : K
E : IntermediateField F K := F⟮a⟯ ⊔ F⟮b⟯
this✝ : FiniteDimensional F ↥F⟮a⟯
this : FiniteDimensional F ↥F⟮b⟯
ha : a ∈ E
hb : b ∈ E
hab : a + b ∈ E
a' : ↥E := ⟨a, ha⟩
b' : ↥E := ⟨b, hb⟩
ab' : ↥E := ⟨a + b, hab⟩
⊢ normalizedTraceAux F K (a + b) = normalizedTraceAux F (↥E) a' + normalizedTraceAux F (↥E) 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
H : A.LinearDisjoint B
inst✝¹ : Free R ↥A
inst✝ : Free R ↥B
⊢ finrank R ↥(A ⊔ B) = finrank R ↥A * finrank R ↥B

Tactic:
by
  simpa only [map_mul] using! congr(Cardinal.toNat $(H.rank_sup_of_free))

Goal state after:
Module: Mathlib.FieldTheory.LinearDisjoint

Goal state before:
pp: F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
H : A.LinearDisjoint L
halg : Algebra.IsAlgebraic F ↥A ∨ Algebra.IsAlgebraic F L
⊢ Module.rank ↥A ↥(extendScalars ⋯) * Module.rank (↥(adjoin L ↑A)) E = Module.rank (↥A) E

Tactic:
exact rank_mul_rank A (extendScalars
    (show A ≤ (adjoin L (A : Set E)).restrictScalars F from subset_adjoin L (A : Set E))) E

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
⊢ A.LinearDisjoint B

Tactic:
by_cases h1 : Module.finrank R A = 0

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 (finrank R ↥B)
a✝ : Nontrivial R
h1 : finrank R ↥A = 0
⊢ A.LinearDisjoint B

case neg
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
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: case pos
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E = ⊥
⊢ generator E ∈ E

Tactic:
generator_eq_zero h

Goal state after:
case pos
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E = ⊥
⊢ 0 ∈ E
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
this :
  c E * (Polynomial.map (algebraMap (↥E) K⟮X⟯) (φ E)).coeff (φ E).natDegree =
    (Polynomial.map (algebraMap K[X] K⟮X⟯) (Φ E)).coeff (φ E).natDegree
⊢ (algebraMap K[X] K⟮X⟯) ((Φ E).coeff (φ E).natDegree) = c E

Tactic:
coeff_map,

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
this :
  c E * (algebraMap (↥E) K⟮X⟯) ((φ E).coeff (φ E).natDegree) =
    (Polynomial.map (algebraMap K[X] K⟮X⟯) (Φ E)).coeff (φ E).natDegree
⊢ (algebraMap K[X] K⟮X⟯) ((Φ E).coeff (φ E).natDegree) = c E
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
this :
  c E * (algebraMap (↥E) K⟮X⟯) ((φ E).coeff (φ E).natDegree) =
    (Polynomial.map (algebraMap K[X] K⟮X⟯) (Φ E)).coeff (φ E).natDegree
⊢ (algebraMap K[X] K⟮X⟯) ((Φ E).coeff (φ E).natDegree) = c E

Tactic:
coeff_map,

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
this : c E * (algebraMap (↥E) K⟮X⟯) ((φ E).coeff (φ E).natDegree) = (algebraMap K[X] K⟮X⟯) ((Φ E).coeff (φ E).natDegree)
⊢ (algebraMap K[X] K⟮X⟯) ((Φ E).coeff (φ E).natDegree) = c E
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
this :
  (Polynomial.C (c E) * Polynomial.map (algebraMap (↥E) K⟮X⟯) (φ E)).coeff (generatorIndex h) =
    (Polynomial.map (algebraMap K[X] K⟮X⟯) (Φ E)).coeff (generatorIndex h)
⊢ (algebraMap K[X] K⟮X⟯) ((Φ E).coeff (generatorIndex h)) = (algebraMap K[X] K⟮X⟯) (c E).num * generator E

Tactic:
coeff_map,

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
this :
  (Polynomial.C (c E) * Polynomial.map (algebraMap (↥E) K⟮X⟯) (φ E)).coeff (generatorIndex h) =
    (algebraMap K[X] K⟮X⟯) ((Φ E).coeff (generatorIndex h))
⊢ (algebraMap K[X] K⟮X⟯) ((Φ E).coeff (generatorIndex h)) = (algebraMap K[X] K⟮X⟯) (c E).num * generator E
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
this :
  c E * (Polynomial.map (algebraMap (↥E) K⟮X⟯) (φ E)).coeff (generatorIndex h) =
    (algebraMap K[X] K⟮X⟯) ((Φ E).coeff (generatorIndex h))
⊢ (algebraMap K[X] K⟮X⟯) ((Φ E).coeff (generatorIndex h)) = (algebraMap K[X] K⟮X⟯) (c E).num * generator E

Tactic:
coeff_map,

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
this :
  c E * (algebraMap (↥E) K⟮X⟯) ((φ E).coeff (generatorIndex h)) =
    (algebraMap K[X] K⟮X⟯) ((Φ E).coeff (generatorIndex h))
⊢ (algebraMap K[X] K⟮X⟯) ((Φ E).coeff (generatorIndex h)) = (algebraMap K[X] K⟮X⟯) (c E).num * generator E
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 F : PointedCone R M
hF : F.IsFaceOf C
x y : M
hx : x ∈ C
hy : y ∈ C
hxy : x + y ∈ F
⊢ x ∈ F

Tactic:
by
  nontriviality R using Module.subsingleton R M
  simpa [hxy] using hF.mem_of_smul_add_mem hx hy zero_lt_one

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
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
i : Fin (n + 1)
this : Nonempty ↥S
⊢ (s.restrict S hS).altitude i = comap S.subtype (s.altitude i)

Tactic:
rw [← s.map_altitude_restrict S hS, comap_map_eq_of_injective S.subtype_injective]

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

Goal state before:
pp: case neg.inl
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
r : ℝ
hx : ¬x = 0
hr : r < 0
⊢ SameRay ℝ x (r • x) ∨ x ≠ 0 ∧ r • x ≠ 0 ∧ SameRay ℝ x (-r • x)

Tactic:
exact Or.inr ⟨hx, smul_ne_zero hr.ne hx,
        SameRay.sameRay_pos_smul_right x (Left.neg_pos_iff.2 hr)⟩

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

Goal state before:
pp: case neg.inr.inl
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
r : ℝ
hx : ¬x = 0
hr : r = 0
⊢ SameRay ℝ x (r • x) ∨ x ≠ 0 ∧ r • x ≠ 0 ∧ SameRay ℝ x (-(r • x))

pp: case neg.inr.inr
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
r : ℝ
hx : ¬x = 0
hr : 0 < r
⊢ SameRay ℝ x (r • x) ∨ x ≠ 0 ∧ r • x ≠ 0 ∧ SameRay ℝ x (-(r • x))

Tactic:
· simp [hr]

Goal state after:
case neg.inr.inr
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
r : ℝ
hx : ¬x = 0
hr : 0 < r
⊢ SameRay ℝ x (r • x) ∨ x ≠ 0 ∧ r • x ≠ 0 ∧ SameRay ℝ x (-(r • x))
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
⊢ 0 < ‖x‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)

Tactic:
exact div_pos (norm_pos_iff.2 h0) (Real.sqrt_pos.2 (Left.add_pos_of_pos_of_nonneg
    (mul_self_pos.2 (norm_ne_zero_iff.2 h0)) (mul_self_nonneg _)))

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
⊢ ‖x‖ ≤ ‖x + y‖

Tactic:
mul_self_le_mul_self_iff (norm_nonneg _) (norm_nonneg _),

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
⊢ ‖x‖ * ‖x‖ ≤ ‖x + y‖ * ‖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 ∨ y ≠ 0
⊢ ‖y‖ ≤ ‖x + y‖

Tactic:
mul_self_le_mul_self_iff (norm_nonneg _) (norm_nonneg _),

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x ≠ 0 ∨ y ≠ 0
⊢ ‖y‖ * ‖y‖ ≤ ‖x + y‖ * ‖x + y‖
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine

Goal state before:
pp: case mpr.inl
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
hp₁p₂ : p₁ ≠ p₂
h : Wbtw ℝ p₂ p₁ p₃
⊢ ∠ p₁ p₂ p₃ = 0

pp: case mpr.inr
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
hp₃p₂ : p₃ ≠ p₂
h : Wbtw ℝ p₂ p₃ p₁
⊢ ∠ p₁ p₂ p₃ = 0

Tactic:
· exact h.angle₂₁₃_eq_zero_of_ne hp₁p₂

Goal state after:
case mpr.inr
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
hp₃p₂ : p₃ ≠ p₂
h : Wbtw ℝ p₂ p₃ p₁
⊢ ∠ p₁ p₂ p₃ = 0
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine

Goal state before:
pp: case pos
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₂ ((AffineEquiv.pointReflection ℝ p₂) p₃) = π - ∠ p₁ p₂ p₃

Tactic:
simp [h₃₂]

Goal state after:
case pos
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₂
⊢ π / 2 = π - π / 2
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle

Goal state before:
pp: case neg.h
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : ¬x = 0 ∨ ¬y = 0
⊢ ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ ≠ 0

Tactic:
refine (ne_of_lt ?_).symm

Goal state after:
case neg.h
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : ¬x = 0 ∨ ¬y = 0
⊢ 0 < ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
hs : (o.oangle x (x + y)).sign = 1
⊢ ↑(InnerProductGeometry.angle x (x + y)) = ↑(Real.arccos (‖x‖ / ‖x + y‖))

Tactic:
InnerProductGeometry.angle_add_eq_arccos_of_inner_eq_zero
      (o.inner_eq_zero_of_oangle_eq_pi_div_two h)

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
hs : (o.oangle x (x + y)).sign = 1
⊢ ↑(Real.arccos (‖x‖ / ‖x + y‖)) = ↑(Real.arccos (‖x‖ / ‖x + y‖))
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
r : ℝ
⊢ o.oangle x (r • x + y) = 0 ∨ o.oangle x (r • x + y) = ↑π ↔ o.oangle x y = 0 ∨ o.oangle x y = ↑π

Tactic:
by
  simp_rw [oangle_eq_zero_or_eq_pi_iff_not_linearIndependent, Fintype.not_linearIndependent_iff,
    Fin.sum_univ_two, Fin.exists_fin_two]
  refine ⟨fun h => ?_, fun h => ?_⟩
  · rcases h with ⟨m, h, hm⟩
    change m 0 • x + m 1 • (r • x + y) = 0 at h
    refine ⟨![m 0 + m 1 * r, m 1], ?_⟩
    change (m 0 + m 1 * r) • x + m 1 • y = 0 ∧ (m 0 + m 1 * r ≠ 0 ∨ m 1 ≠ 0)
    rw [smul_add, smul_smul, ← add_assoc, ← add_smul] at h
    refine ⟨h, not_and_or.1 fun h0 => ?_⟩
    obtain ⟨h0, h1⟩ := h0
    rw [h1] at h0 hm
    rw [zero_mul, add_zero] at h0
    simp [h0] at hm
  · rcases h with ⟨m, h, hm⟩
    change m 0 • x + m 1 • y = 0 at h
    refine ⟨![m 0 - m 1 * r, m 1], ?_⟩
    change (m 0 - m 1 * r) • x + m 1 • (r • x + y) = 0 ∧ (m 0 - m 1 * r ≠ 0 ∨ m 1 ≠ 0)
    rw [sub_smul, smul_add, smul_smul, ← add_assoc, sub_add_cancel]
    refine ⟨h, not_and_or.1 fun h0 => ?_⟩
    obtain ⟨h0, h1⟩ := h0
    rw [h1] at h0 hm
    rw [zero_mul, sub_zero] at h0
    simp [h0] at hm

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

Goal state before:
pp: case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : r = 0
⊢ o.oangle (x + r • (o.rotation ↑(π / 2)) x) (r • (o.rotation ↑(π / 2)) x) = ↑(Real.arctan r⁻¹)

pp: case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : ¬r = 0
⊢ o.oangle (x + r • (o.rotation ↑(π / 2)) x) (r • (o.rotation ↑(π / 2)) x) = ↑(Real.arctan r⁻¹)

Tactic:
· simp [hr]

Goal state after:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : ¬r = 0
⊢ o.oangle (x + r • (o.rotation ↑(π / 2)) x) (r • (o.rotation ↑(π / 2)) x) = ↑(Real.arctan r⁻¹)
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle

Goal state before:
pp: case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : r = 0
⊢ o.oangle (r • (o.rotation ↑(π / 2)) x) (r • (o.rotation ↑(π / 2)) x - x) = ↑(Real.arctan r⁻¹)

pp: case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : ¬r = 0
⊢ o.oangle (r • (o.rotation ↑(π / 2)) x) (r • (o.rotation ↑(π / 2)) x - x) = ↑(Real.arctan r⁻¹)

Tactic:
· simp [hr]

Goal state after:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : ¬r = 0
⊢ o.oangle (r • (o.rotation ↑(π / 2)) x) (r • (o.rotation ↑(π / 2)) x - x) = ↑(Real.arctan r⁻¹)
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle

Goal state before:
pp: case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : r = 0
⊢ o.oangle (x - r • (o.rotation ↑(π / 2)) x) x = ↑(Real.arctan r)

pp: case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : ¬r = 0
⊢ o.oangle (x - r • (o.rotation ↑(π / 2)) x) x = ↑(Real.arctan r)

Tactic:
· simp [hr]

Goal state after:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : ¬r = 0
⊢ o.oangle (x - r • (o.rotation ↑(π / 2)) x) x = ↑(Real.arctan r)
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle

Goal state before:
pp: case pos
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

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:
· simp [hp₁, Real.pi_pos]

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₁).toReal| < π / 2
Module: Mathlib.Geometry.Euclidean.SignedDist

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 q : P
⊢ (affineSpan ℝ {q}).signedInfDist p = (signedDist (p -ᵥ q)) q

Tactic:
simpa using signedInfDist_eq_signedDist_of_mem (mem_affineSpan ℝ (Set.mem_singleton q))

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

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
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ≠ p₂
hp₄ : p₄ ≠ p₂
h : SameRay ℝ (p₁ -ᵥ p₂) (p₄ -ᵥ p₂)
r : ℝ
hr : 0 < r
he : r • (p₁ -ᵥ p₂) = p₄ -ᵥ p₂
⊢ Wbtw ℝ p₂ p₁ p₄ ∨ Wbtw ℝ p₂ p₄ p₁

Tactic:
← vsub_vadd p₁ p₂,

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
hp₁ : p₁ ≠ p₂
hp₄ : p₄ ≠ p₂
h : SameRay ℝ (p₁ -ᵥ p₂) (p₄ -ᵥ p₂)
r : ℝ
hr : 0 < r
he : r • (p₁ -ᵥ p₂) = p₄ -ᵥ p₂
⊢ Wbtw ℝ p₂ ((p₁ -ᵥ p₂) +ᵥ p₂) p₄ ∨ Wbtw ℝ p₂ p₄ ((p₁ -ᵥ p₂) +ᵥ p₂)
Module: Mathlib.Geometry.Euclidean.Angle.Bisector

Goal state before:
pp: case inr
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p p₁ p₂ p₃ : P
h₂ : p₁ ≠ p₂
h₃ : p₁ ≠ p₃
h : 2 • ∡ p₂ p₁ p = 2 • ∡ p p₁ p₃
h' : ↑((orthogonalProjection line[ℝ, p₁, p₃]) p) = p₁
⊢ dist p ↑((orthogonalProjection line[ℝ, p₁, p₂]) p) = dist p ↑((orthogonalProjection line[ℝ, p₁, p₃]) p)

Tactic:
· refine (dist_orthogonalProjection_line_eq_of_two_zsmul_oangle_eq_aux₁ h₃ ?_ h').symm
    rw [oangle_rev, smul_neg, ← h, oangle_rev, smul_neg, neg_neg]

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

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)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
p : P
ha : AffineIndependent ℝ ![t.points i₁, t.points i₂, t.points i₃]
⊢ dist p ↑((orthogonalProjection (affineSpan ℝ (t.points '' {i₃}ᶜ))) p) =
      dist p ↑((orthogonalProjection (affineSpan ℝ (t.points '' {i₂}ᶜ))) p) ↔
    dist p ↑((orthogonalProjection line[ℝ, t.points i₁, t.points i₂]) p) =
      dist p ↑((orthogonalProjection line[ℝ, t.points i₁, t.points i₃]) p)

Tactic:
simp_rw [(by grind : ({i₃}ᶜ : Set (Fin 3)) = {i₁, i₂}),
    (by grind : ({i₂}ᶜ : Set (Fin 3)) = {i₁, i₃}), Set.image_insert_eq, Set.image_singleton]

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

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 : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
⊢ ∑ i, s.excenterWeights signs i = 1 ↔ s.ExcenterExists signs

Tactic:
by
  classical
  simp [sum_excenterWeights]

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

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
s : Sphere P
p q : P
h : ∠ q p s.center = π / 2
hp : p ∈ s
hp_mem : p ∈ line[ℝ, p, q]
⊢ s.IsTangentAt p line[ℝ, p, q]

Tactic:
refine ⟨hp, hp_mem, ?_⟩

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p q : P
h : ∠ q p s.center = π / 2
hp : p ∈ s
hp_mem : p ∈ line[ℝ, p, q]
⊢ line[ℝ, p, q] ≤ s.orthRadius p