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

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
ih : (y : (Module.rank F E).ord.ToType) → y < i → (Module.rank F E).ord.ToType
s : Set E := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this✝¹ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this✝ : Module.rank F ↥(adjoin F s) = Module.rank F ↥⊤
this : #↑(Iio i) < #(Module.rank F E).ord.ToType
⊢ Module.rank F ↥(adjoin F s) < Module.rank F E

Tactic:
mk_toType,

Goal state after:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
ih : (y : (Module.rank F E).ord.ToType) → y < i → (Module.rank F E).ord.ToType
s : Set E := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this✝¹ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this✝ : Module.rank F ↥(adjoin F s) = Module.rank F ↥⊤
this : #↑(Iio i) < (Module.rank F E).ord.card
⊢ Module.rank F ↥(adjoin F s) < Module.rank F E
Module: Mathlib.FieldTheory.CardinalEmb

Goal state before:
pp: case refine_1
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
⊢ ⇑b ∘ φ '' Iio i ⊆ ⇑b '' Iio (φ i)

pp: case refine_2
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
⊢ ⇑b '' Iio (φ i) ⊆ ↑(adjoin F (⇑b ∘ φ '' Iio i))

Tactic:
· rw [image_comp]; apply image_mono; rintro _ ⟨j, hj, rfl⟩; exact strictMono_leastExt hj

Goal state after:
case refine_2
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
⊢ ⇑b '' Iio (φ i) ⊆ ↑(adjoin F (⇑b ∘ φ '' Iio i))
Module: Mathlib.FieldTheory.CardinalEmb

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
rank_inf : ℵ₀ ≤ Module.rank F E
⊢ #(Emb F E) = 2 ^ Module.rank F E

Tactic:
have := Fact.mk rank_inf
  rw [Emb.Cardinal.embEquivPi.cardinal_eq, mk_pi]
  apply le_antisymm
  · rw [← power_eq_two_power rank_inf natCast_le_aleph0 rank_inf]
    conv_rhs => rw [← mk_ord_toType (Module.rank F E), ← prod_const']
    exact prod_le_prod _ _ fun i ↦ (Emb.Cardinal.deg_lt_aleph0 _).le
  · conv_lhs => rw [← mk_ord_toType (Module.rank F E), ← prod_const']
    exact prod_le_prod _ _ Emb.Cardinal.two_le_deg

Goal state after:
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: case mk.mk
K : Type u
inst✝⁵ : CommRing K
p : ℕ
inst✝⁴ : Fact (Nat.Prime p)
inst✝³ : CharP K p
L : Type v
inst✝² : CommSemiring L
inst✝¹ : CharP L p
inst✝ : PerfectRing L p
f : K →+* L
x✝ : PerfectClosure K p
n : ℕ
x : K
y✝ : PerfectClosure K p
m : ℕ
y : K
this : ∀ (n : ℕ), LeftInverse (⇑(frobeniusEquiv L p).symm)^[n] (⇑(frobenius L p))^[n]
⊢ (⇑(frobeniusEquiv L p).symm)^[n + m] ((⇑(frobenius L p))^[m] (f x)) *
      (⇑(frobeniusEquiv L p).symm)^[n + m] ((⇑(frobenius L p))^[n] (f y)) =
    (⇑(frobeniusEquiv L p).symm)^[n] (f x) * (⇑(frobeniusEquiv L p).symm)^[m] (f y)

Tactic:
rw [iterate_add_apply, this _ _, add_comm, iterate_add_apply, this _ _]

Goal state after:
Module: Mathlib.FieldTheory.JacobsonNoether

Goal state before:
pp: D : Type u_1
inst✝² : DivisionRing D
inst✝¹ : Algebra.IsAlgebraic (↥k) D
p : ℕ
inst✝ : ExpChar D p
a : D
ha : a ∉ k
hinsep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
hn : a ∈ k
⊢ False

Tactic:
exact ha hn

Goal state after:
Module: Mathlib.FieldTheory.JacobsonNoether

Goal state before:
pp: case pos
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
H : k ≠ ⊤
p : ℕ
hp : ExpChar D p
insep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
a : D
ha : a ∉ k
ha₀ : a ≠ 0
b : D
hb1 : ((ad (↥k) D) a) b ≠ 0
m : ℕ
hm2 : ∀ (n : ℕ), p ^ m ≤ n → (⇑((ad (↥k) D) a))^[n] = 0
h_exist : ∃ n, 0 < n ∧ (⇑((ad (↥k) D) a))^[n + 1] b = 0
t : ℕ := Nat.find h_exist - 1
ht : t = Nat.find h_exist - 1
h_pos : 0 < t
⊢ (⇑((ad (↥k) D) a))^[Nat.find h_exist] b ≠ 0

pp: case neg
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
H : k ≠ ⊤
p : ℕ
hp : ExpChar D p
insep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
a : D
ha : a ∉ k
ha₀ : a ≠ 0
b : D
hb1 : ((ad (↥k) D) a) b ≠ 0
m : ℕ
hm2 : ∀ (n : ℕ), p ^ m ≤ n → (⇑((ad (↥k) D) a))^[n] = 0
h_exist : ∃ n, 0 < n ∧ (⇑((ad (↥k) D) a))^[n + 1] b = 0
t : ℕ := Nat.find h_exist - 1
ht : t = Nat.find h_exist - 1
h_pos : t ≤ 0
⊢ (⇑((ad (↥k) D) a))^[Nat.find h_exist] b ≠ 0

Tactic:
· convert! (ne_eq _ _) ▸ not_and.mp (Nat.find_min h_exist (m := t) (by lia)) h_pos
      lia

Goal state after:
case neg
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
H : k ≠ ⊤
p : ℕ
hp : ExpChar D p
insep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
a : D
ha : a ∉ k
ha₀ : a ≠ 0
b : D
hb1 : ((ad (↥k) D) a) b ≠ 0
m : ℕ
hm2 : ∀ (n : ℕ), p ^ m ≤ n → (⇑((ad (↥k) D) a))^[n] = 0
h_exist : ∃ n, 0 < n ∧ (⇑((ad (↥k) D) a))^[n + 1] b = 0
t : ℕ := Nat.find h_exist - 1
ht : t = Nat.find h_exist - 1
h_pos : t ≤ 0
⊢ (⇑((ad (↥k) D) a))^[Nat.find h_exist] b ≠ 0
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: case neg
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
hn' : (Finset.image K Finset.univ).card < n
k' : κ
hk' : k' ∈ Finset.univ ∧ K k' ≠ K k ∧ (K k').FiniteIndex
⊢ ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex

Tactic:
exact ⟨k'.1.1, Finset.mem_of_mem_filter k'.1.1 k'.1.2, hK k', hk'.2.2⟩

Goal state after:
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: K : Type u
inst✝⁵ : Field K
L : Type u_1
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
inst✝¹ : IsGalois K L
inst✝ : IsCyclic Gal(L/K)
ζ : K
hζ : IsPrimitiveRoot ζ (finrank K L)
σ : Gal(L/K)
hσ : Function.Surjective fun x ↦ σ ^ x
hσ'✝ : orderOf σ = Nat.card Gal(L/K)
this✝ : (minpoly K σ.toLinearMap).IsRoot ζ
v : L
hv : End.HasEigenvector σ.toLinearMap ζ v
hv' : ∀ (n : ℕ), (σ ^ n) v = ζ ^ n • v
n : ℕ
hσ' : σ ^ n ∈ IsGalois.intermediateFieldEquivSubgroup K⟮v⟯
this : ζ ^ n • v = v
| v

Tactic:
rw [← one_smul K v]

Goal state after:
K : Type u
inst✝⁵ : Field K
L : Type u_1
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
inst✝¹ : IsGalois K L
inst✝ : IsCyclic Gal(L/K)
ζ : K
hζ : IsPrimitiveRoot ζ (finrank K L)
σ : Gal(L/K)
hσ : Function.Surjective fun x ↦ σ ^ x
hσ'✝ : orderOf σ = Nat.card Gal(L/K)
this✝ : (minpoly K σ.toLinearMap).IsRoot ζ
v : L
hv : End.HasEigenvector σ.toLinearMap ζ v
hv' : ∀ (n : ℕ), (σ ^ n) v = ζ ^ n • v
n : ℕ
hσ' : σ ^ n ∈ IsGalois.intermediateFieldEquivSubgroup K⟮v⟯
this : ζ ^ n • v = v
| 1 • v
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Algebra.IsSeparable K L
inst✝¹ : Normal K L
c : ConjRootClass K L
inst✝ : Fintype ↑c.carrier
⊢ (map (algebraMap K L) c.minpoly).Splits

Tactic:
exact c.splits_minpoly

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 L ↥(adjoin L ↑A) = Module.rank F ↥A

Tactic:
refine Eq.trans ?_ (Subalgebra.LinearDisjoint.adjoin_rank_eq_rank_left H)

Goal state after:
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 L ↥(adjoin L ↑A) =
    Module.rank ↥(IsScalarTower.toAlgHom F L E).range
      ↥(Algebra.adjoin ↥(IsScalarTower.toAlgHom F L E).range ↑A.toSubalgebra)
Module: Mathlib.FieldTheory.RatFunc.Degree

Goal state before:
pp: K : Type u
inst✝ : Field K
⊢ ↑X.num.natDegree - ↑X.denom.natDegree = 1

Tactic:
num_X,

Goal state after:
K : Type u
inst✝ : Field K
⊢ ↑Polynomial.X.natDegree - ↑X.denom.natDegree = 1
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; exact IsContDiffCompatible.isPlot_iff

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

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace 𝕜 V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst✝¹ : Nonempty ↥s
inst✝ : s.direction.HasOrthogonalProjection
p : P
⊢ s.direction.orthogonalProjectionOnto (p -ᵥ ↑((orthogonalProjection s) p)) = 0

Tactic:
simpa using vsub_orthogonalProjection_mem_direction_orthogonal _ _

Goal state after:
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
⊢ p ≠ s.points i

Tactic:
intro heq

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 : vectorSpan ℝ {p, s.points i} = (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
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst✝¹ : Nonempty ↥s
inst✝ : s.direction.HasOrthogonalProjection
p : P
⊢ nndist p ↑((orthogonalProjection s) p) = Metric.infNndist p ↑s

Tactic:
rw [← NNReal.coe_inj]
  simp [dist_orthogonalProjection_eq_infDist]

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

Goal state before:
pp: case mpr.refine_2
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
hne : p ≠ s.points i
h : p -ᵥ s.points i ∈ (s.altitude i).direction
⊢ finrank ℝ ↥(ℝ ∙ (p -ᵥ s.points i)) = finrank ℝ ↥(s.altitude i).direction

Tactic:
rw [finrank_direction_altitude, finrank_span_set_eq_card]

Goal state after:
case mpr.refine_2
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
hne : p ≠ s.points i
h : p -ᵥ s.points i ∈ (s.altitude i).direction
⊢ #{p -ᵥ s.points i}.toFinset = 1

case mpr.refine_2
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
hne : p ≠ s.points i
h : p -ᵥ s.points i ∈ (s.altitude i).direction
⊢ LinearIndepOn ℝ id {p -ᵥ s.points i}
Module: Mathlib.Geometry.Euclidean.Altitude

Goal state before:
pp: case a
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, r ≠ 0 ∧ s.points j -ᵥ s.altitudeFoot j = r • (s.points i -ᵥ s.altitudeFoot i)

Tactic:
rintro ⟨r, hr, h⟩

Goal state after:
case a
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)
⊢ False
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation

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)
x y : V
θ : Real.Angle
hx : ¬x = 0
hy : y = 0
⊢ o.oangle x y = θ ↔ x ≠ 0 ∧ y ≠ 0 ∧ y = (‖y‖ / ‖x‖) • (o.rotation θ) x ∨ θ = 0 ∧ (x = 0 ∨ y = 0)

Tactic:
simp [hy, eq_comm]

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

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)
x y : V
θ : Real.Angle
hx : ¬x = 0
hy : y = 0
⊢ o.oangle x y = θ ↔ (x ≠ 0 ∧ y ≠ 0 ∧ ∃ r, 0 < r ∧ y = r • (o.rotation θ) x) ∨ θ = 0 ∧ (x = 0 ∨ y = 0)

Tactic:
simp [hy, eq_comm]

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
⊢ Real.arccos (⟪x, x⟫ / (‖x‖ * ‖x + y‖)) = Real.arccos (‖x‖ / ‖x + y‖)

Tactic:
real_inner_self_eq_norm_mul_norm

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
⊢ Real.arccos (‖x‖ * ‖x‖ / (‖x‖ * ‖x + y‖)) = Real.arccos (‖x‖ / ‖x + y‖)
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle

Goal state before:
pp: case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
hx : ¬‖x‖ = 0
⊢ Real.arccos (‖x‖ * ‖x‖ / (‖x‖ * ‖x + y‖)) = Real.arccos (‖x‖ / ‖x + y‖)

Tactic:
div_mul_eq_div_div,

Goal state after:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
hx : ¬‖x‖ = 0
⊢ Real.arccos (‖x‖ * ‖x‖ / ‖x‖ / ‖x + y‖) = Real.arccos (‖x‖ / ‖x + y‖)
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
⊢ ∠ p₂ p₃ p₁ ≤ π / 2

Tactic:
by
  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 [angle, ← vsub_add_vsub_cancel p₁ p₂ p₃, add_comm]
  exact angle_add_le_pi_div_two_of_inner_eq_zero h

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
hx : ¬x = 0
hy : ¬y = 0
⊢ (o.oangle x y + ↑π).sign = -(o.oangle x y).sign

Tactic:
Real.Angle.sign_add_pi

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
hx : ¬x = 0
hy : ¬y = 0
⊢ -(o.oangle x y).sign = -(o.oangle x y).sign
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:
oangle_eq_zero_or_eq_pi_iff_not_linearIndependent,

Goal state after:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
⊢ ¬LinearIndependent ℝ ![x, r • x + y] ↔ ¬LinearIndependent ℝ ![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
⊢ (o.oangle (x - y) y).sign = (o.oangle x y).sign

Tactic:
← o.oangle_sign_sub_smul_left x y 1,

Goal state after:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ (o.oangle (x - y) y).sign = (o.oangle (x - 1 • y) y).sign
Module: Mathlib.Geometry.Euclidean.Angle.Bisector

Goal state before:
pp: case refine_2.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
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) = 0 ∨ dist p p' = 0
hpp' : p ≠ p'
hn : p ∉ s₂
⊢ False

Tactic:
simp only [dist_eq_zero, hpp', or_false] at h
        rw [eq_comm] at h
        simp [orthogonalProjection_eq_self_iff, hn] at h

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
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst✝¹ : s₁.direction.HasOrthogonalProjection
inst✝ : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
h' : p ∈ s₁
⊢ dist p ↑((orthogonalProjection s₁) p) = dist p ↑((orthogonalProjection s₂) p) ↔
    ∠ p p' ↑((orthogonalProjection s₁) p) = ∠ p p' ↑((orthogonalProjection s₂) p)

Tactic:
by
  have : Nonempty s₁ := ⟨p', hp'₁⟩
  have : Nonempty s₂ := ⟨p', hp'₂⟩
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · 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]
  · rw [orthogonalProjection_eq_self_iff.2 h'] at h ⊢
    rw [dist_self, zero_eq_dist, eq_comm, orthogonalProjection_eq_self_iff]
    obtain rfl | hpp' := eq_or_ne p p'
    · exact hp'₂
    · by_contra hn
      rw [angle_self_of_ne hpp', angle_comm,
        angle_eq_arcsin_of_angle_eq_pi_div_two (angle_self_orthogonalProjection p hp'₂),
        Real.zero_eq_arcsin_iff, div_eq_zero_iff] at h
      · simp only [dist_eq_zero, hpp', or_false] at h
        rw [eq_comm] at h
        simp [orthogonalProjection_eq_self_iff, hn] at h
      · exact .inl (Ne.symm (orthogonalProjection_eq_self_iff.symm.not.1 hn))

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
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst✝¹ : s₁.direction.HasOrthogonalProjection
inst✝ : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
h' : p ∈ s₁ ∨ p ∈ s₂
this✝ : Nonempty ↥s₁
this : Nonempty ↥s₂
⊢ dist p ↑((orthogonalProjection s₁) p) = dist p ↑((orthogonalProjection s₂) p) ↔
    ∠ p p' ↑((orthogonalProjection s₁) p) = ∠ p p' ↑((orthogonalProjection s₂) p)

Tactic:
rcases h' with h' | h'

Goal state after:
case 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
s₁ s₂ : AffineSubspace ℝ P
inst✝¹ : s₁.direction.HasOrthogonalProjection
inst✝ : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
this✝ : Nonempty ↥s₁
this : Nonempty ↥s₂
h' : p ∈ s₁
⊢ dist p ↑((orthogonalProjection s₁) p) = dist p ↑((orthogonalProjection s₂) p) ↔
    ∠ p p' ↑((orthogonalProjection s₁) p) = ∠ p p' ↑((orthogonalProjection s₂) p)

case 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
s₁ s₂ : AffineSubspace ℝ P
inst✝¹ : s₁.direction.HasOrthogonalProjection
inst✝ : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
this✝ : Nonempty ↥s₁
this : Nonempty ↥s₂
h' : p ∈ s₂
⊢ dist p ↑((orthogonalProjection s₁) p) = dist p ↑((orthogonalProjection s₂) p) ↔
    ∠ p p' ↑((orthogonalProjection s₁) p) = ∠ p p' ↑((orthogonalProjection s₂) p)
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)
⊢ dist p₁ p₂ / (∡ p₂ p₃ p₁).tan = dist p₃ p₂

Tactic:
have hs : (∡ p₂ p₃ p₁).sign = 1 := by rw [oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
  rw [oangle_eq_angle_of_sign_eq_one hs, Real.Angle.tan_coe,
    dist_div_tan_angle_of_angle_eq_pi_div_two (angle_eq_pi_div_two_of_oangle_eq_pi_div_two h)
      (Or.inl (left_ne_of_oangle_eq_pi_div_two h))]

Goal state after:
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
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : s.direction.HasOrthogonalProjection
p x : P
h : x ∈ affineSpan ℝ (insert p ↑s)
⊢ |(s.signedInfDist p) x| = dist x ↑((orthogonalProjection s) x)

Tactic:
mem_affineSpan_insert_iff (orthogonalProjection s p).property

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 : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : s.direction.HasOrthogonalProjection
p x : P
h : ∃ r, ∃ p0 ∈ s, x = r • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ p0
⊢ |(s.signedInfDist p) x| = dist x ↑((orthogonalProjection s) x)
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₂
hadd : ∡ p₁ p₂ p₃ + ∡ p₃ p₂ p₄ = ∡ p₁ p₂ p₄
h : ∡ p₁ p₂ p₃ ≠ ↑π
⊢ (∡ p₁ p₂ p₃).sign = (∡ p₁ p₂ p₄).sign

Tactic:
← oangle_swap₂₃_sign p₁ 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
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₂
hadd : ∡ p₁ p₂ p₃ + ∡ p₃ p₂ p₄ = ∡ p₁ p₂ p₄
h : ∡ p₁ p₂ p₃ ≠ ↑π
⊢ -(∡ p₁ p₃ p₂).sign = (∡ p₁ p₂ p₄).sign