mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.MvRatFunc.Rank

Goal state before:
pp: case refine_1
σ : Type u
F : Type v
inst✝¹ : Field F
inst✝ : Nonempty σ
R : Type (max v u) := MvPolynomial σ F
K : Type (max u v) := FractionRing R
⊢ #(FractionRing (MvPolynomial σ F)) ≤ max (max (lift.{u, v} #F) (lift.{v, u} #σ)) ℵ₀

pp: case refine_2
σ : Type u
F : Type v
inst✝¹ : Field F
inst✝ : Nonempty σ
R : Type (max v u) := MvPolynomial σ F
K : Type (max u v) := FractionRing R
⊢ max (max (lift.{u, v} #F) (lift.{v, u} #σ)) ℵ₀ ≤ Module.rank F (FractionRing (MvPolynomial σ F))

Tactic:
· rw [FractionRing.cardinalMk, MvPolynomial.cardinalMk_eq_max_lift]

Goal state after:
case refine_2
σ : Type u
F : Type v
inst✝¹ : Field F
inst✝ : Nonempty σ
R : Type (max v u) := MvPolynomial σ F
K : Type (max u v) := FractionRing R
⊢ max (max (lift.{u, v} #F) (lift.{v, u} #σ)) ℵ₀ ≤ Module.rank F (FractionRing (MvPolynomial σ F))
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: k : Type u_1
E : Type u_2
inst✝³ : DivisionRing k
inst✝² : Infinite k
inst✝¹ : AddCommGroup E
inst✝ : Module k E
s : Finset (Subspace k E)
hs : ⊤ ∉ s
hcovers : ⋃ p ∈ s, ↑p = Set.univ
⊢ False

Tactic:
have ⟨p, hp, hfi⟩ := Submodule.exists_finiteIndex_of_cover hcovers

Goal state after:
k : Type u_1
E : Type u_2
inst✝³ : DivisionRing k
inst✝² : Infinite k
inst✝¹ : AddCommGroup E
inst✝ : Module k E
s : Finset (Subspace k E)
hs : ⊤ ∉ s
hcovers : ⋃ p ∈ s, ↑p = Set.univ
p : Subspace k E
hp : p ∈ s
hfi : (Submodule.toAddSubgroup p).FiniteIndex
⊢ False
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

Goal state before:
pp: case mpr
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x y : ConjRootClass K L
⊢ x = -y → ∃ a, mk K a = x ∧ ∃ b, mk K b = y ∧ a + b = 0

Tactic:
· rintro rfl
    induction y with
    | h y => exact ⟨-y, mk_neg y, y, rfl, neg_add_cancel _⟩

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

Goal state before:
pp: case h
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
x : E
n : ℕ
hx : x ^ ringExpChar F ^ n ∈ (algebraMap F E).rangeS
⊢ x⁻¹ ^ ringExpChar F ^ n ∈ (algebraMap F E).rangeS

Tactic:
inv_pow

Goal state after:
case h
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
x : E
n : ℕ
hx : x ^ ringExpChar F ^ n ∈ (algebraMap F E).rangeS
⊢ (x ^ ringExpChar F ^ n)⁻¹ ∈ (algebraMap F E).rangeS
Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
q : ℕ
hF : ExpChar F q
inst✝ : ExpChar E q
n : ℕ
a : E
hsep : IsSeparable F a
⊢ minpoly F ((iterateFrobenius E q n) a) = Polynomial.map (iterateFrobenius F q n) (minpoly F a)

Tactic:
have hai : IsIntegral F a := hsep.isIntegral
  have hapi : IsIntegral F (iterateFrobenius E q n a) := hai.pow _
  symm
  refine Polynomial.eq_of_monic_of_dvd_of_natDegree_le
    (minpoly.monic hapi)
    (minpoly.monic hai |>.map _)
    (minpoly.dvd F (a ^ q ^ n) ?haeval)
    ?hdeg
  · simpa using! Eq.symm <|
      (minpoly F a).map_aeval_eq_aeval_map (RingHom.iterateFrobenius_comm _ q n) a
  · rw [(minpoly F a).natDegree_map_eq_of_injective (iterateFrobenius F q n).injective,
      ← IntermediateField.adjoin.finrank hai,
      IntermediateField.adjoin_simple_eq_adjoin_pow_expChar_pow_of_isSeparable F E hsep q n,
      ← IntermediateField.adjoin.finrank hapi, iterateFrobenius_def]

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 ≠ ⊥
⊢ (g E).natDegree ≤ ((Φ E).coeff (φ E).natDegree).natDegree

Tactic:
rw [Φ_coeff_φ_natDegree' h]
  exact natDegree_le_of_dvd (generator_denom_dvd_c_num h) (num_ne_zero (c_ne_zero h))

Goal state after:
Module: Mathlib.Geometry.Convex.Cone.Face.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsOrderedRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
C F : PointedCone R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Function.Injective ⇑f
hF : F.IsFaceOf C
a : R
x : M
hx : x ∈ ↑C
y : M
hy : y ∈ ↑C
ha : 0 < a
z : M
hz₁ : z ∈ ↑F
hz₂ : f z = f (a • x + y)
⊢ (↑{ c // 0 ≤ c } f) x ∈ map f F

Tactic:
exact ⟨x, hF.mem_of_smul_add_mem hx hy ha (hf hz₂ ▸ hz₁), rfl⟩

Goal state after:
Module: Mathlib.Geometry.Convex.Cone.Face.Basic

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsOrderedRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
C F : PointedCone R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Function.Injective ⇑f
sub : map f F ≤ map f C
hF : ∀ {x y : N} {a : R}, x ∈ map f C → y ∈ map f C → 0 < a → a • x + y ∈ map f F → x ∈ map f F
x✝ y✝ : M
a✝ : R
hx : x✝ ∈ C
hy : y✝ ∈ C
ha : 0 < a✝
h : a✝ • x✝ + y✝ ∈ F
⊢ x✝ ∈ F

Tactic:
simp only [mem_map, forall_exists_index, and_imp] at hF

Goal state after:
case refine_2
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsOrderedRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
C F : PointedCone R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Function.Injective ⇑f
sub : map f F ≤ map f C
x✝ y✝ : M
a✝ : R
hx : x✝ ∈ C
hy : y✝ ∈ C
ha : 0 < a✝
h : a✝ • x✝ + y✝ ∈ F
hF :
  ∀ {x y : N} {a : R},
    ∀ x_1 ∈ C, f x_1 = x → ∀ x_2 ∈ C, f x_2 = y → 0 < a → ∀ x_3 ∈ F, f x_3 = a • x + y → ∃ x_4 ∈ F, f x_4 = x
⊢ x✝ ∈ F
Module: Mathlib.Geometry.Convex.Cone.Face.Basic

Goal state before:
pp: case mem_of_smul_add_mem
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : DivisionRing R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsOrderedRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
C₁ : PointedCone R M
C₂ : PointedCone R N
F : PointedCone R (M × N)
hF : F.IsFaceOf (prod C₁ C₂)
x y : M
a : R
hx : x ∈ C₁
hy : y ∈ C₁
⊢ 0 < a → ∀ (x_1 : N), (a • x + y, x_1) ∈ F → ∃ x_2, (x, x_2) ∈ F

Tactic:
ha

Goal state after:
case mem_of_smul_add_mem
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : DivisionRing R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsOrderedRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
C₁ : PointedCone R M
C₂ : PointedCone R N
F : PointedCone R (M × N)
hF : F.IsFaceOf (prod C₁ C₂)
x y : M
a : R
hx : x ∈ C₁
hy : y ∈ C₁
ha : 0 < a
⊢ ∀ (x_1 : N), (a • x + y, x_1) ∈ F → ∃ x_2, (x, x_2) ∈ F
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:
← d.isOpen_iff_preimages_plots,

Goal state after:
X : Type u_1
d : DiffeologicalSpace X
t : TopologicalSpace X
h : dTopology = t
u✝ : Set X
⊢ TopologicalSpace.IsOpen u✝ ↔ TopologicalSpace.IsOpen u✝
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: case inr
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
F : Type u_1 := AlgebraicClosure K
H✝ : ¬(Polynomial.map (algebraMap K F) (Q₂ h)).degree ≤ 0
α : F
hα : (aeval α) (Q₂ h) = 0
eq :
  (Polynomial.mapRingHom (algebraMap K F)) (g E) * Polynomial.C ((aeval α) (f E)) =
    (Polynomial.mapRingHom (algebraMap K F)) (f E) * Polynomial.C ((aeval α) (g E))
H : (aeval α) (generator E).denom ≠ 0
⊢ (aeval α) (f E) ≠ 0 ∧ (aeval α) (g E) ≠ 0

Tactic:
refine ⟨Polynomial.C_injective.ne_iff.mp ?_, H⟩

Goal state after:
case inr
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
F : Type u_1 := AlgebraicClosure K
H✝ : ¬(Polynomial.map (algebraMap K F) (Q₂ h)).degree ≤ 0
α : F
hα : (aeval α) (Q₂ h) = 0
eq :
  (Polynomial.mapRingHom (algebraMap K F)) (g E) * Polynomial.C ((aeval α) (f E)) =
    (Polynomial.mapRingHom (algebraMap K F)) (f E) * Polynomial.C ((aeval α) (g E))
H : (aeval α) (generator E).denom ≠ 0
⊢ Polynomial.C ((aeval α) (f E)) ≠ Polynomial.C 0
Module: Mathlib.Geometry.Diffeology.Basic

Goal state before:
pp: X : Type u_1
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace ℝ X
inst✝ : FiniteDimensional ℝ X
d : DiffeologicalSpace X
x✝ : IsContDiffCompatible X
⊢ d = NormedSpace.toDiffeology X

Tactic:
ext n p

Goal state after:
X : Type u_1
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace ℝ X
inst✝ : FiniteDimensional ℝ X
d : DiffeologicalSpace X
x✝ : IsContDiffCompatible X
n : ℕ
p : EuclideanSpace ℝ (Fin n) → X
⊢ IsPlot p ↔ IsPlot p
Module: Mathlib.Geometry.Diffeology.Basic

Goal state before:
pp: X : Type u_1
d d' : DiffeologicalSpace X
h : d.toPlots = d'.toPlots
⊢ d = d'

Tactic:
ext n p

Goal state after:
X : Type u_1
d d' : DiffeologicalSpace X
h : d.toPlots = d'.toPlots
n : ℕ
p : EuclideanSpace ℝ (Fin n) → X
⊢ IsPlot p ↔ IsPlot p
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 : V
hx : x ≠ 0
θ : Real.Angle
r : ℝ
hr : 0 < r
hy : r • (o.rotation θ) x ≠ 0
⊢ o.oangle x (r • (o.rotation θ) x) = θ

Tactic:
rw [o.oangle_smul_right_of_pos _ _ hr, o.oangle_rotation_self_right hx]

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
h : dist p₃ p₁ = dist p₃ p₂
⊢ ∠ p₃ (midpoint ℝ p₁ p₂) p₁ = π / 2

Tactic:
let m : P := midpoint ℝ p₁ p₂

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
h : dist p₃ p₁ = dist p₃ p₂
m : P := midpoint ℝ p₁ p₂
⊢ ∠ p₃ (midpoint ℝ p₁ p₂) p₁ = π / 2
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 : ℕ
inst✝ : n.AtLeastTwo
s : Simplex ℝ P n
i j : Fin (n + 1)
⊢ -1 < ⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫ / (s.height i * s.height j)

Tactic:
rw [neg_lt, neg_div', div_lt_one (by simp [height]), neg_lt]
  exact neg_mul_lt_inner_vsub_altitudeFoot _ _ _

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)
x : P × P × P
hx12 : x.1 ≠ x.2.1
hx32 : x.2.2 ≠ x.2.1
⊢ ContinuousAt (fun y ↦ ∡ y.1 y.2.1 y.2.2) x

Tactic:
unfold oangle
  fun_prop (disch := simp [*])

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ : P
hp₁p₂ : p₁ -ᵥ p₂ ≠ 0
r : ℝ
hr : r < 0
hp₃p₂ : p₃ = r • (p₁ -ᵥ p₂) +ᵥ p₂
⊢ p₂ -ᵥ p₁ = (1 / (1 - r) * -r + 1 / (1 - r)) • (p₂ -ᵥ p₁)

Tactic:
convert! (one_smul ℝ (p₂ -ᵥ p₁)).symm

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
hp₁p₂ : p₁ -ᵥ p₂ ≠ 0
r : ℝ
hr : r < 0
hp₃p₂ : p₃ = r • (p₁ -ᵥ p₂) +ᵥ p₂
⊢ 1 / (1 - r) * -r + 1 / (1 - r) = 1
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

Goal state before:
pp: case inr
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
h0 : 0 ≤ InnerProductGeometry.angle x y
hpi : InnerProductGeometry.angle x y ≤ π
h : o.oangle x y = -↑(InnerProductGeometry.angle x y)
⊢ InnerProductGeometry.angle x y = |(o.oangle x y).toReal|

Tactic:
rw [h, eq_comm, Real.Angle.abs_toReal_neg_coe_eq_self_iff]
    exact ⟨h0, hpi⟩

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₄ p₅ p₆ : P
h₂ : p₂ ∉ line[ℝ, p₁, p₃]
h₄ : p₄ ∈ line[ℝ, p₁, p₃]
h₆ : p₆ ∈ line[ℝ, p₁, p₃]
h₁₂₄₅ : line[ℝ, p₁, p₂] ∥ line[ℝ, p₄, p₅]
h₃₂₆₅ : line[ℝ, p₃, p₂] ∥ line[ℝ, p₆, p₅]
⊢ line[ℝ, p₆, p₄].direction ≤ line[ℝ, p₃, p₁].direction

Tactic:
Set.pair_comm p₃

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)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₂ : p₂ ∉ line[ℝ, p₁, p₃]
h₄ : p₄ ∈ line[ℝ, p₁, p₃]
h₆ : p₆ ∈ line[ℝ, p₁, p₃]
h₁₂₄₅ : line[ℝ, p₁, p₂] ∥ line[ℝ, p₄, p₅]
h₃₂₆₅ : line[ℝ, p₃, p₂] ∥ line[ℝ, p₆, p₅]
⊢ line[ℝ, p₆, p₄].direction ≤ line[ℝ, p₁, p₃].direction
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

Goal state before:
pp: case neg.refine_1
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 = ↑π
⊢ InnerProductGeometry.angle x y = π

Tactic:
o.angle_eq_abs_oangle_toReal hx hy,

Goal state after:
case neg.refine_1
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 = ↑π
⊢ |(o.oangle x y).toReal| = π
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

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

Tactic:
o.angle_eq_abs_oangle_toReal hx hy,

Goal state after:
case neg.refine_1
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 = ↑(π / 2) ∨ o.oangle x y = ↑(-π / 2)
⊢ |(o.oangle x y).toReal| = π / 2
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
h : Sbtw ℝ p₃ p₂ p₃'
hp₁p₂ : p₁ ≠ p₂
⊢ ∡ p₁ p₂ p₃ = ∡ p₁ p₂ p₃' + ↑π

Tactic:
by
  rw [← h.oangle₃₂₁_eq_pi, oangle_add hp₁p₂ h.right_ne h.left_ne]

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

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
r : ℝ
h : ¬(o.oangle x y = 0 ∨ o.oangle x y = ↑π)
h' : ∀ (r' : ℝ), o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ ↑π
s : Set (V × V) := (fun r' ↦ (x, r' • x + y)) '' Set.univ
⊢ (o.oangle x (r • x + y)).sign = (o.oangle x y).sign

Tactic:
have hc : IsConnected s := isConnected_univ.image _ (by fun_prop)

Goal state after:
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
r : ℝ
h : ¬(o.oangle x y = 0 ∨ o.oangle x y = ↑π)
h' : ∀ (r' : ℝ), o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ ↑π
s : Set (V × V) := (fun r' ↦ (x, r' • x + y)) '' Set.univ
hc : IsConnected s
⊢ (o.oangle x (r • x + y)).sign = (o.oangle x y).sign
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

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
r₁ r₂ r₃ r₄ : ℝ
hr₁ : ¬r₁ = 0
⊢ SignType.sign (-r₃ / r₁ * (r₂ * r₁) + r₄ * r₁) * (o.oangle x y).sign =
    SignType.sign (r₁ * r₄ - r₂ * r₃) * (o.oangle x y).sign

Tactic:
mul_comm r₂ r₁,

Goal state after:
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
r₁ r₂ r₃ r₄ : ℝ
hr₁ : ¬r₁ = 0
⊢ SignType.sign (-r₃ / r₁ * (r₁ * r₂) + r₄ * r₁) * (o.oangle x y).sign =
    SignType.sign (r₁ * r₄ - r₂ * r₃) * (o.oangle x y).sign
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : (∡ p₃ p₁ p₂).sign = 1
⊢ (∡ p₃ p₁ p₂).sin = dist p₃ p₂ / dist p₁ p₃

Tactic:
rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm, Real.Angle.sin_coe,
    sin_angle_of_angle_eq_pi_div_two (angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two h)
      (Or.inr (left_ne_of_oangle_eq_pi_div_two h)),
    dist_comm p₁ p₃]

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₄ 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
p : P × P × P
hp : p ∈ s
⊢ ∡ p.1 p.2.1 p.2.2 ≠ 0 ∧ ∡ p.1 p.2.1 p.2.2 ≠ ↑π

Tactic:
simp_rw [s, Set.mem_image, Set.mem_prod, Set.mem_ofPred, Set.mem_univ, true_and,
        Prod.ext_iff] at hp

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)
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
p : P × P × P
hp : ∃ x, (SameRay ℝ (p₂ -ᵥ p₁) x.2 ∧ x.2 ≠ 0) ∧ ↑x.1 = p.1 ∧ p₅ = p.2.1 ∧ x.2 +ᵥ ↑x.1 = p.2.2
⊢ ∡ p.1 p.2.1 p.2.2 ≠ 0 ∧ ∡ p.1 p.2.1 p.2.2 ≠ ↑π
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
h₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄ + ↑π
hs : line[ℝ, p₁, p₂].SSameSide p₃ p₄
h₃₂ : p₃ ≠ p₂
h₄₂ : p₄ ≠ p₂
ha' : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ ((AffineEquiv.pointReflection ℝ p₂) p₄)
hs' : line[ℝ, p₁, p₂].SOppSide p₄ ((AffineEquiv.pointReflection ℝ p₂) p₄)
⊢ ∠ p₁ p₂ p₃ = (∠ p₁ p₂ p₄ + π) / 2

Tactic:
obtain h := angle_eq_pi_sub_angle_div_two_of_oangle_eq_of_sOppSide h₁₂ ha' (hs.trans_sOppSide hs')

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)
p₁ p₂ p₃ p₄ : P
h₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄ + ↑π
hs : line[ℝ, p₁, p₂].SSameSide p₃ p₄
h₃₂ : p₃ ≠ p₂
h₄₂ : p₄ ≠ p₂
ha' : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ ((AffineEquiv.pointReflection ℝ p₂) p₄)
hs' : line[ℝ, p₁, p₂].SOppSide p₄ ((AffineEquiv.pointReflection ℝ p₂) p₄)
h : ∠ p₁ p₂ p₃ = π - ∠ p₁ p₂ ((AffineEquiv.pointReflection ℝ p₂) p₄) / 2
⊢ ∠ p₁ p₂ p₃ = (∠ p₁ p₂ p₄ + π) / 2
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 q : P
⊢ q ∈ s ∧ dist q s.center ^ 2 = dist p s.center ^ 2 + dist q p ^ 2 ↔
    0 ≤ s.radius ∧
      dist q p ^ 2 = s.radius ^ 2 - dist p s.center ^ 2 ∧ dist q s.center ^ 2 = dist p s.center ^ 2 + dist q p ^ 2

Tactic:
rw [← and_assoc, and_congr_left_iff]

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
⊢ dist q s.center ^ 2 = dist p s.center ^ 2 + dist q p ^ 2 →
    (q ∈ s ↔ 0 ≤ s.radius ∧ dist q p ^ 2 = s.radius ^ 2 - dist p s.center ^ 2)
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₁ s₂ : Sphere P
as : AffineSubspace ℝ P
⊢ (∃ p ∈ as, Wbtw ℝ s₁.center p s₂.center) ∨ ∀ p ∈ as, ¬Sbtw ℝ s₁.center p s₂.center

Tactic:
by_cases! h : ∃ p ∈ as, Wbtw ℝ s₁.center p s₂.center

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
s₁ s₂ : Sphere P
as : AffineSubspace ℝ P
h : ∃ p ∈ as, Wbtw ℝ s₁.center p s₂.center
⊢ (∃ p ∈ as, Wbtw ℝ s₁.center p s₂.center) ∨ ∀ p ∈ as, ¬Sbtw ℝ s₁.center p s₂.center

case neg
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s₁ s₂ : Sphere P
as : AffineSubspace ℝ P
h : ∀ p ∈ as, ¬Wbtw ℝ s₁.center p s₂.center
⊢ (∃ p ∈ as, Wbtw ℝ s₁.center p s₂.center) ∨ ∀ p ∈ as, ¬Sbtw ℝ s₁.center p s₂.center
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
⊢ ∀ (v : V), ∃ r, r • (p -ᵥ s.center) = v

Tactic:
have hc0 : c ≠ 0 := by
            rintro rfl
            rw [zero_smul, eq_comm, vsub_eq_zero_iff_eq] at hc
            simp [hc] at hp

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
⊢ ∀ (v : V), ∃ r, r • (p -ᵥ s.center) = v
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
hf2 : Fact (Module.finrank ℝ V = 2)
s : Sphere P
p : P
hp : dist p s.center ≤ s.radius
hpc : p ≠ s.center
v : V
hv : v ∈ (ℝ ∙ (p -ᵥ s.center))ᗮ
hv1 : ‖v‖ = 1
hr : 0 ≤ s.radius
hv0 : v ≠ 0
hf : ∀ (w : ↥(ℝ ∙ (p -ᵥ s.center))ᗮ), ∃ c, c • ⟨v, hv⟩ = w
⊢ ∀ w ∈ (ℝ ∙ (p -ᵥ s.center))ᗮ, ∃ c, c • v = w

Tactic:
intro w hw

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
hf2 : Fact (Module.finrank ℝ V = 2)
s : Sphere P
p : P
hp : dist p s.center ≤ s.radius
hpc : p ≠ s.center
v : V
hv : v ∈ (ℝ ∙ (p -ᵥ s.center))ᗮ
hv1 : ‖v‖ = 1
hr : 0 ≤ s.radius
hv0 : v ≠ 0
hf : ∀ (w : ↥(ℝ ∙ (p -ᵥ s.center))ᗮ), ∃ c, c • ⟨v, hv⟩ = w
w : V
hw : w ∈ (ℝ ∙ (p -ᵥ s.center))ᗮ
⊢ ∃ c, c • v = w