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
h : ⋃ i ∈ {x | K x = K k}, f i • ↑(K i) ≠ Set.univ
i : κ
hi : K i ≠ K k ∧ (K i).FiniteIndex
⊢ False

Tactic:
by_cases hfi : (H i.1.1).FiniteIndex

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
hcovers' : ⋃ k ∈ Finset.univ, f k • ↑(K k) = Set.univ
k : κ
hkfi : (H ↑k.fst).FiniteIndex
hk : K k = D
h : ⋃ i ∈ {x | K x = K k}, f i • ↑(K i) ≠ Set.univ
i : κ
hi : K i ≠ K k ∧ (K i).FiniteIndex
hfi : (H ↑i.fst).FiniteIndex
⊢ False

case neg
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
h : ⋃ i ∈ {x | K x = K k}, f i • ↑(K i) ≠ Set.univ
i : κ
hi : K i ≠ K k ∧ (K i).FiniteIndex
hfi : ¬(H ↑i.fst).FiniteIndex
⊢ False
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 D : PointedCone R N
hC : DualFG p C
hD : DualFG p D
⊢ DualFG p (C ⊓ D)

Tactic:
by classical
  obtain ⟨S, rfl⟩ := hC; obtain ⟨T, rfl⟩ := hD
  use S ∪ T; rw [Finset.coe_union, dual_union]

Goal state after:
Module: Mathlib.FieldTheory.Relrank

Goal state before:
pp: F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A : IntermediateField F E
⊢ ⊥.relrank A = Module.rank F ↥⊥ * ⊥.relrank A

Tactic:
IntermediateField.rank_bot,

Goal state after:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A : IntermediateField F E
⊢ ⊥.relrank A = 1 * ⊥.relrank A
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
θ : Real.Angle
⊢ (o.kahler x) ((o.rotation θ) y) = ↑θ.toCircle * (o.kahler x) y

Tactic:
by
  simp only [o.rotation_apply, map_add, map_smulₛₗ, RingHom.id_apply, real_smul,
    kahler_rightAngleRotation_right, Real.Angle.coe_toCircle]
  ring

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
r : ℝ
hr : r < 0
⊢ o.oangle x (r • y) = o.oangle x (-y)

Tactic:
rw [← neg_neg r, neg_smul, ← smul_neg, o.oangle_smul_right_of_pos _ _ (neg_pos_of_neg hr)]

Goal state after:
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₄ : P
h : InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₄ -ᵥ p₃) = π
left✝ : p₂ -ᵥ p₃ ≠ 0
r : ℝ
hpr : (-r + 1) • (p₃ -ᵥ p₂) = p₄ -ᵥ p₂
hr : 0 < -r + 1
⊢ InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₄ -ᵥ p₂) = InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)

Tactic:
exact angle_smul_right_of_pos p₁ hr hpr

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

Goal state before:
pp: 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
f : V ≃ₗᵢ[ℝ] V'
x : V'
⊢ (((map (Fin 2) f.toLinearEquiv) o).rotation θ) x = f ((o.rotation θ) (f.symm x))

Tactic:
by
  simp [rotation_apply, o.rightAngleRotation_map]

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

Goal state before:
pp: θ : Real.Angle
z : ℂ
⊢ (Complex.orientation.rotation θ) z = ↑θ.toCircle * z

Tactic:
simp only [rotation_apply, Complex.rightAngleRotation, Real.Angle.coe_toCircle, real_smul]
  ring

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

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
p₁ p₂ p₃ : P
h₃₂ : p₃ ≠ p₂
⊢ ∠ p₁ p₂ ((AffineEquiv.pointReflection ℝ p₂) p₃) = π - ∠ p₁ p₂ p₃

Tactic:
eq_sub_iff_add_eq

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
p₁ p₂ p₃ : P
h₃₂ : p₃ ≠ p₂
⊢ ∠ p₁ p₂ ((AffineEquiv.pointReflection ℝ p₂) p₃) + ∠ p₁ p₂ p₃ = π
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

Goal state before:
pp: case pos
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
w x y z : V
h : InnerProductGeometry.angle w x = InnerProductGeometry.angle y z
hs : (o.oangle w x).sign = (o.oangle y z).sign
h0 : (w = 0 ∨ x = 0) ∨ y = 0 ∨ z = 0
hswx : (o.oangle w x).sign = 0
hsyz : (o.oangle y z).sign = 0
hwx : InnerProductGeometry.angle w x = π / 2
hyz : InnerProductGeometry.angle y z = π / 2
hpi : π / 2 ≠ π
⊢ o.oangle w x = o.oangle y z

Tactic:
have h0wx : w = 0 ∨ x = 0 := by
      have h0' := o.eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero hswx
      simpa [hwx, Real.pi_pos.ne.symm, hpi] using h0'

Goal state after:
case pos
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
w x y z : V
h : InnerProductGeometry.angle w x = InnerProductGeometry.angle y z
hs : (o.oangle w x).sign = (o.oangle y z).sign
h0 : (w = 0 ∨ x = 0) ∨ y = 0 ∨ z = 0
hswx : (o.oangle w x).sign = 0
hsyz : (o.oangle y z).sign = 0
hwx : InnerProductGeometry.angle w x = π / 2
hyz : InnerProductGeometry.angle y z = π / 2
hpi : π / 2 ≠ π
h0wx : w = 0 ∨ x = 0
⊢ o.oangle w x = o.oangle y z
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

Goal state before:
pp: case neg.refine_2
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 : InnerProductGeometry.angle x y = π / 2
⊢ o.oangle x y = ↑(π / 2) ∨ o.oangle x y = ↑(-π / 2)

Tactic:
convert! o.oangle_eq_angle_or_eq_neg_angle hx hy using 2 <;> rw [h]

Goal state after:
case e'_2
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 : InnerProductGeometry.angle x y = π / 2
⊢ ↑(-π / 2) = -↑(π / 2)
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle

Goal state before:
pp: case inr.inr
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 : 0 < r
⊢ o.oangle x (x + r • (o.rotation ↑(π / 2)) x) = ↑(Real.arctan r)

Tactic:
· have ha : o.oangle x (r • o.rotation (π / 2 : ℝ) x) = (π / 2 : ℝ) := by
      rw [o.oangle_smul_right_of_pos _ _ hr, o.oangle_rotation_self_right h]
    rw [o.oangle_add_right_eq_arctan_of_oangle_eq_pi_div_two ha, norm_smul,
      LinearIsometryEquiv.norm_map, mul_div_assoc, div_self (norm_ne_zero_iff.2 h), mul_one,
      Real.norm_eq_abs, abs_of_pos hr]

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 y : V
h : ‖x‖ = ‖y‖
hn : ¬x = y
hy : y ≠ 0
r : ℝ
hr0 : 0 ≤ r
hr : r • y = x - y
⊢ |(o.oangle (y - x) y).toReal| < π / 2

Tactic:
eq_sub_iff_add_eq

Goal state after:
case neg.inl
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : ‖x‖ = ‖y‖
hn : ¬x = y
hy : y ≠ 0
r : ℝ
hr0 : 0 ≤ r
hr : r • y + y = x
⊢ |(o.oangle (y - x) y).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
v w : V
p q : P
⊢ ((signedDist v) (w +ᵥ p)) q = ((signedDist v) p) (-w +ᵥ q)

Tactic:
rw [signedDist_vadd_left, signedDist_vadd_right, inner_neg_right]

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

Goal state before:
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
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₂]

Tactic:
· refine vadd_mem_of_mem_direction ?_ hq
        rw [direction_affineSpan]
        exact smul_vsub_rev_mem_vectorSpan_pair _ _ _

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

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
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p p' : P
s₁ s₂ : AffineSubspace ℝ P
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
⊢ ↑((orthogonalProjection s₁) p) ≠ ↑((orthogonalProjection s₂) p) →
    dist p ↑((orthogonalProjection s₁) p) = dist p ↑((orthogonalProjection s₂) p) →
      ∡ (↑((orthogonalProjection s₁) p)) p' p = ∡ p p' ↑((orthogonalProjection s₂) p)

Tactic:
intro hne h

Goal state after:
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
s₁ s₂ : AffineSubspace ℝ P
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
hne : ↑((orthogonalProjection s₁) p) ≠ ↑((orthogonalProjection s₂) p)
h : dist p ↑((orthogonalProjection s₁) p) = dist p ↑((orthogonalProjection s₂) p)
⊢ ∡ (↑((orthogonalProjection s₁) p)) p' p = ∡ p p' ↑((orthogonalProjection s₂) p)
Module: Mathlib.Geometry.Euclidean.Sphere.Basic

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
S : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥S
inst✝ : S.direction.HasOrthogonalProjection
ps : Set ↥S
h : Cospherical (Subtype.val '' ps)
p₀ : ↥S
hp₀ : p₀ ∈ ps
⊢ Cospherical ps

Tactic:
rcases h with ⟨c, r, hr⟩

Goal state after:
case inr
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
S : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥S
inst✝ : S.direction.HasOrthogonalProjection
ps : Set ↥S
p₀ : ↥S
hp₀ : p₀ ∈ ps
c : P
r : ℝ
hr : ∀ p ∈ Subtype.val '' ps, dist p c = r
⊢ Cospherical ps
Module: Mathlib.Geometry.Euclidean.Sphere.Basic

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
s : Sphere P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
o : P := s.center
t : ℝ
hpt : (AffineMap.lineMap p₁ p₂) t = p
ht₀ : 0 ≤ t
ht₁ : t ≤ 1
hne₁ : p ≠ p₁
hne₂ : p ≠ p₂
ht₀' : 0 < t
h : t = 1
⊢ (AffineMap.lineMap p₁ p₂) 1 = p₂

Tactic:
AffineMap.lineMap_apply_one

Goal state after:
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
s : Sphere P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
o : P := s.center
t : ℝ
hpt : (AffineMap.lineMap p₁ p₂) t = p
ht₀ : 0 ≤ t
ht₁ : t ≤ 1
hne₁ : p ≠ p₁
hne₂ : p ≠ p₂
ht₀' : 0 < t
h : t = 1
⊢ p₂ = p₂
Module: Mathlib.Geometry.Euclidean.Sphere.Tangent

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
as : AffineSubspace ℝ P
p q : P
h : s.IsTangentAt p as
hq : q ∈ as
hqp : q ≠ p
⊢ s.radius ^ 2 < dist q s.center ^ 2

Tactic:
rw [h.dist_sq_eq_of_mem hq]

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
as : AffineSubspace ℝ P
p q : P
h : s.IsTangentAt p as
hq : q ∈ as
hqp : q ≠ p
⊢ s.radius ^ 2 < s.radius ^ 2 + dist q p ^ 2
Module: Mathlib.Geometry.Euclidean.Sphere.Basic

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
s : Sphere P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
o : P := s.center
t : ℝ
hpt : (AffineMap.lineMap p₁ p₂) t = p
ht₀ : 0 ≤ t
ht₁ : t ≤ 1
hne₁ : p ≠ p₁
hne₂ : p ≠ p₂
ht₀' : 0 < t
ht₁' : t < 1
u : V := p₁ -ᵥ o
v : V := p₂ -ᵥ o
hu : ‖u‖ = s.radius
hv : ‖v‖ = s.radius
huv : u ≠ v
hpo : p -ᵥ o = (1 - t) • u + t • v
hmem : (1 - t) • u + t • v ∈ Metric.ball 0 s.radius
⊢ ‖(1 - t) • u + t • v‖ < s.radius

Tactic:
Metric.mem_ball,

Goal state after:
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
s : Sphere P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
o : P := s.center
t : ℝ
hpt : (AffineMap.lineMap p₁ p₂) t = p
ht₀ : 0 ≤ t
ht₁ : t ≤ 1
hne₁ : p ≠ p₁
hne₂ : p ≠ p₂
ht₀' : 0 < t
ht₁' : t < 1
u : V := p₁ -ᵥ o
v : V := p₂ -ᵥ o
hu : ‖u‖ = s.radius
hv : ‖v‖ = s.radius
huv : u ≠ v
hpo : p -ᵥ o = (1 - t) • u + t • v
hmem : dist ((1 - t) • u + t • v) 0 < s.radius
⊢ ‖(1 - t) • u + t • v‖ < s.radius
Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius

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 : P
h : dist p s.center < s.radius
hp : p ≠ s.center
hb : ℝ ∙ (p -ᵥ s.center) ≠ ⊤
hn : ¬Subsingleton V
v : V
hv0 : v ≠ 0
hv : ∀ (w : V), ∃ c, c • v = w
c : ℝ
hc : c • v = p -ᵥ s.center
hc0 : c ≠ 0
c' : ℝ
⊢ ∃ r, r • (p -ᵥ s.center) = c' • v

Tactic:
refine ⟨c' / c, ?_⟩

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 : P
h : dist p s.center < s.radius
hp : p ≠ s.center
hb : ℝ ∙ (p -ᵥ s.center) ≠ ⊤
hn : ¬Subsingleton V
v : V
hv0 : v ≠ 0
hv : ∀ (w : V), ∃ c, c • v = w
c : ℝ
hc : c • v = p -ᵥ s.center
hc0 : c ≠ 0
c' : ℝ
⊢ (c' / c) • (p -ᵥ s.center) = c' • v
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₃
hd : dist (incenter t) (touchpoint t ∅ i₃) = dist (incenter t) (touchpoint t ∅ i₂)
⊢ ∡ (touchpoint t ∅ i₃) (t.points i₁) (incenter t) = ∡ (incenter t) (t.points i₁) (touchpoint t ∅ i₂)

Tactic:
simp_rw [touchpoint, orthogonalProjectionSpan] at hd ⊢

Goal state after:
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₃
hd :
  dist (incenter t) ↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₃).points))) (excenter t ∅)) =
    dist (incenter t) ↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₂).points))) (excenter t ∅))
⊢ ∡ (↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₃).points))) (excenter t ∅))) (t.points i₁)
      (incenter t) =
    ∡ (incenter t) (t.points i₁)
      ↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₂).points))) (excenter t ∅))
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₃
hd : dist (excenter t {i₁}) (touchpoint t {i₁} i₃) = dist (excenter t {i₁}) (touchpoint t {i₁} i₂)
⊢ ∡ (touchpoint t {i₁} i₃) (t.points i₁) (excenter t {i₁}) = ∡ (excenter t {i₁}) (t.points i₁) (touchpoint t {i₁} i₂)

Tactic:
simp_rw [touchpoint, orthogonalProjectionSpan] at hd ⊢

Goal state after:
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₃
hd :
  dist (excenter t {i₁})
      ↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₃).points))) (excenter t {i₁})) =
    dist (excenter t {i₁})
      ↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₂).points))) (excenter t {i₁}))
⊢ ∡ (↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₃).points))) (excenter t {i₁}))) (t.points i₁)
      (excenter t {i₁}) =
    ∡ (excenter t {i₁}) (t.points i₁)
      ↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₂).points))) (excenter t {i₁}))
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₃
hd : dist (excenter t {i₁}) (touchpoint t {i₁} i₃) = dist (excenter t {i₁}) (touchpoint t {i₁} i₁)
⊢ ∡ (touchpoint t {i₁} i₃) (t.points i₂) (excenter t {i₁}) = ∡ (excenter t {i₁}) (t.points i₂) (touchpoint t {i₁} i₁)

Tactic:
simp_rw [touchpoint, orthogonalProjectionSpan] at hd ⊢

Goal state after:
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₃
hd :
  dist (excenter t {i₁})
      ↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₃).points))) (excenter t {i₁})) =
    dist (excenter t {i₁})
      ↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₁).points))) (excenter t {i₁}))
⊢ ∡ (↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₃).points))) (excenter t {i₁}))) (t.points i₂)
      (excenter t {i₁}) =
    ∡ (excenter t {i₁}) (t.points i₂)
      ↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₁).points))) (excenter t {i₁}))
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₃
hd :
  dist (excenter t {i₁})
      ↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₃).points))) (excenter t {i₁})) =
    dist (excenter t {i₁})
      ↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₁).points))) (excenter t {i₁}))
⊢ ∡ (↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₃).points))) (excenter t {i₁}))) (t.points i₂)
      (excenter t {i₁}) =
    ∡ (excenter t {i₁}) (t.points i₂)
      ↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₁).points))) (excenter t {i₁}))

Tactic:
refine oangle_eq_of_dist_orthogonalProjection_eq (mem_affineSpan _ ?_) (mem_affineSpan _ ?_)
    ((t.excenterExists_singleton i₁).touchpoint_injective.ne h₁₃.symm) hd

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)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hd :
  dist (excenter t {i₁})
      ↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₃).points))) (excenter t {i₁})) =
    dist (excenter t {i₁})
      ↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₁).points))) (excenter t {i₁}))
⊢ t.points i₂ ∈ Set.range (faceOpposite t i₃).points

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)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hd :
  dist (excenter t {i₁})
      ↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₃).points))) (excenter t {i₁})) =
    dist (excenter t {i₁})
      ↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₁).points))) (excenter t {i₁}))
⊢ t.points i₂ ∈ Set.range (faceOpposite t i₁).points