mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Euclidean.Similarity

Goal state before:
pp: case neg
V₁ : Type u_2
V₂ : Type u_3
P₁ : Type u_4
P₂ : Type u_5
inst✝⁷ : NormedAddCommGroup V₁
inst✝⁶ : NormedAddCommGroup V₂
inst✝⁵ : InnerProductSpace ℝ V₁
inst✝⁴ : InnerProductSpace ℝ V₂
inst✝³ : MetricSpace P₁
inst✝² : MetricSpace P₂
inst✝¹ : NormedAddTorsor V₁ P₁
inst✝ : NormedAddTorsor V₂ P₂
a b c : P₁
a' b' c' : P₂
r : ℝ
hr_pos : 0 < r
hdist :
  ∀ (i₁ i₂ : Fin (Nat.succ 0).succ.succ),
    dist (![a, b, c] i₁) (![a, b, c] i₂) = r * dist (![a', b', c'] i₁) (![a', b', c'] i₂)
h_ab : dist a b = r * dist a' b'
h_cb : dist c b = r * dist c' b'
h_ac : dist a c = r * dist a' c'
h_cos' : dist a' c' ^ 2 = dist a' b' ^ 2 + dist c' b' ^ 2 - dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c')
heq : ¬dist a' b' * dist c' b' * 2 = 0
h_cos : ∠ a' b' c' = ∠ a b c
⊢ ∠ a b c = ∠ a' b' c'

pp: case a
V₁ : Type u_2
V₂ : Type u_3
P₁ : Type u_4
P₂ : Type u_5
inst✝⁷ : NormedAddCommGroup V₁
inst✝⁶ : NormedAddCommGroup V₂
inst✝⁵ : InnerProductSpace ℝ V₁
inst✝⁴ : InnerProductSpace ℝ V₂
inst✝³ : MetricSpace P₁
inst✝² : MetricSpace P₂
inst✝¹ : NormedAddTorsor V₁ P₁
inst✝ : NormedAddTorsor V₂ P₂
a b c : P₁
a' b' c' : P₂
r : ℝ
hr_pos : 0 < r
hdist :
  ∀ (i₁ i₂ : Fin (Nat.succ 0).succ.succ),
    dist (![a, b, c] i₁) (![a, b, c] i₂) = r * dist (![a', b', c'] i₁) (![a', b', c'] i₂)
h_ab : dist a b = r * dist a' b'
h_cb : dist c b = r * dist c' b'
h_ac : dist a c = r * dist a' c'
h_cos : Real.cos (∠ a' b' c') = Real.cos (∠ a b c)
h_cos' : dist a' c' ^ 2 = dist a' b' ^ 2 + dist c' b' ^ 2 - dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c')
heq : ¬dist a' b' * dist c' b' * 2 = 0
⊢ ∠ a' b' c' ∈ Set.Icc 0 Real.pi

pp: case a
V₁ : Type u_2
V₂ : Type u_3
P₁ : Type u_4
P₂ : Type u_5
inst✝⁷ : NormedAddCommGroup V₁
inst✝⁶ : NormedAddCommGroup V₂
inst✝⁵ : InnerProductSpace ℝ V₁
inst✝⁴ : InnerProductSpace ℝ V₂
inst✝³ : MetricSpace P₁
inst✝² : MetricSpace P₂
inst✝¹ : NormedAddTorsor V₁ P₁
inst✝ : NormedAddTorsor V₂ P₂
a b c : P₁
a' b' c' : P₂
r : ℝ
hr_pos : 0 < r
hdist :
  ∀ (i₁ i₂ : Fin (Nat.succ 0).succ.succ),
    dist (![a, b, c] i₁) (![a, b, c] i₂) = r * dist (![a', b', c'] i₁) (![a', b', c'] i₂)
h_ab : dist a b = r * dist a' b'
h_cb : dist c b = r * dist c' b'
h_ac : dist a c = r * dist a' c'
h_cos : Real.cos (∠ a' b' c') = Real.cos (∠ a b c)
h_cos' : dist a' c' ^ 2 = dist a' b' ^ 2 + dist c' b' ^ 2 - dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c')
heq : ¬dist a' b' * dist c' b' * 2 = 0
⊢ ∠ a b c ∈ Set.Icc 0 Real.pi

Tactic:
repeat grind [angle_nonneg, angle_le_pi]

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

Goal state before:
pp: case right
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
ho : t.orthocenter ∉ Set.range t.points
p : Fin 3 → P
hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)
hpi : Function.Injective p
i₁ i₂ i₃ j₂ j₃ : Fin 3
left✝² : i₁ ≠ i₂
left✝¹ : i₁ ≠ i₃
left✝ : i₂ ≠ i₃
h₁₂₃ : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
h₁ : p i₁ = t.orthocenter
hj₂₃ : j₂ ≠ j₃
h₂ : t.points j₂ = p i₂
h₃ : t.points j₃ = p i₃
p₁ : P
hp₁ : p₁ ∈ Set.range p
⊢ dist p₁ ((reflection (affineSpan ℝ (t.points '' {j₂, j₃}))) (Simplex.circumcenter t)) = Simplex.circumradius t

Tactic:
rcases hp₁ with ⟨i, rfl⟩

Goal state after:
case right
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
ho : t.orthocenter ∉ Set.range t.points
p : Fin 3 → P
hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)
hpi : Function.Injective p
i₁ i₂ i₃ j₂ j₃ : Fin 3
left✝² : i₁ ≠ i₂
left✝¹ : i₁ ≠ i₃
left✝ : i₂ ≠ i₃
h₁₂₃ : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
h₁ : p i₁ = t.orthocenter
hj₂₃ : j₂ ≠ j₃
h₂ : t.points j₂ = p i₂
h₃ : t.points j₃ = p i₃
i : Fin 3
⊢ dist (p i) ((reflection (affineSpan ℝ (t.points '' {j₂, j₃}))) (Simplex.circumcenter t)) = Simplex.circumradius t
Module: Mathlib.Geometry.Manifold.Algebra.SmoothFunctions

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹⁰ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝⁹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝⁸ : TopologicalSpace N
inst✝⁷ : ChartedSpace H N
E'' : Type u_7
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁴ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝³ : TopologicalSpace N'
inst✝² : ChartedSpace H'' N'
n : ℕ∞ω
V : Type u_10
inst✝¹ : NormedAddCommGroup V
inst✝ : NormedSpace 𝕜 V
r : C^n⟮I, N; 𝓘(𝕜, 𝕜), 𝕜⟯
⊢ r • 0 = 0

Tactic:
ext x; exact smul_zero _

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

Goal state before:
pp: case right
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
ho : t.orthocenter ∉ Set.range t.points
p : Fin 3 → P
hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)
hpi : Function.Injective p
hs : Set.range p = Set.range t.points
p₁ : P
hp₁ : p₁ ∈ Set.range t.points
⊢ dist p₁ (Simplex.circumcenter t) = Simplex.circumradius t

Tactic:
rcases hp₁ with ⟨i, rfl⟩

Goal state after:
case right
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
ho : t.orthocenter ∉ Set.range t.points
p : Fin 3 → P
hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)
hpi : Function.Injective p
hs : Set.range p = Set.range t.points
i : Fin (2 + 1)
⊢ dist (t.points i) (Simplex.circumcenter t) = Simplex.circumradius t
Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : BoundarylessManifold I M
⊢ (ModelWithCorners.interior M)ᶜ = ∅

Tactic:
I.interior_eq_univ,

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : BoundarylessManifold I M
⊢ univᶜ = ∅
Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
N : Type u_7
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H' N
J : ModelWithCorners 𝕜 E' H'
⊢ ModelWithCorners.boundary (M × N) = univ.prod (ModelWithCorners.boundary N) ∪ (ModelWithCorners.boundary M).prod univ

Tactic:
let h := calc (I.prod J).boundary (M × N)
    _ = ((I.prod J).interior (M × N))ᶜ := compl_interior.symm
    _ = ((I.interior M) ×ˢ (J.interior N))ᶜ := by rw [interior_prod]
    _ = (I.interior M)ᶜ ×ˢ univ ∪ univ ×ˢ (J.interior N)ᶜ := by rw [compl_prod_eq_union]

Goal state after:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
N : Type u_7
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H' N
J : ModelWithCorners 𝕜 E' H'
h : ModelWithCorners.boundary (M × N) =
  (ModelWithCorners.interior M)ᶜ ×ˢ univ ∪ univ ×ˢ (ModelWithCorners.interior N)ᶜ :=
  Trans.trans
    (Trans.trans (Trans.trans rfl (Eq.symm compl_interior))
      (Eq.mpr
        (id (congrArg (fun _a ↦ _aᶜ = (ModelWithCorners.interior M ×ˢ ModelWithCorners.interior N)ᶜ) interior_prod))
        (Eq.refl (ModelWithCorners.interior M ×ˢ ModelWithCorners.interior N)ᶜ)))
    (Eq.mpr
      (id
        (congrArg (fun _a ↦ _a = (ModelWithCorners.interior M)ᶜ ×ˢ univ ∪ univ ×ˢ (ModelWithCorners.interior N)ᶜ)
          (compl_prod_eq_union (ModelWithCorners.interior M) (ModelWithCorners.interior N))))
      (Eq.refl ((ModelWithCorners.interior M)ᶜ ×ˢ univ ∪ univ ×ˢ (ModelWithCorners.interior N)ᶜ)))
⊢ ModelWithCorners.boundary (M × N) = univ.prod (ModelWithCorners.boundary N) ∪ (ModelWithCorners.boundary M).prod univ
Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u_5
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
x : M'
hx : I.IsBoundaryPoint x
⊢ I.IsBoundaryPoint (Sum.inr x)

Tactic:
rw [I.isBoundaryPoint_iff, extChartAt, ChartedSpace.sum_chartAt_inr]

Goal state after:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u_5
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
x : M'
hx : I.IsBoundaryPoint x
⊢ ↑(((chartAt H x).lift_openEmbedding ⋯).extend I) (Sum.inr x) ∈ frontier (range ↑I)
Module: Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : ChartedSpace H G
inst✝¹ : Monoid G
inst✝ : ContMDiffMul I ∞ G
g : G
X : LeftInvariantDerivation I G
f : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
h : G
⊢ ((evalAt h) X) (f.comp (𝑳 I g)) = (X (f.comp (𝑳 I g))) h

Tactic:
evalAt_apply

Goal state after:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : ChartedSpace H G
inst✝¹ : Monoid G
inst✝ : ContMDiffMul I ∞ G
g : G
X : LeftInvariantDerivation I G
f : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
h : G
⊢ (X (f.comp (𝑳 I g))) h = (X (f.comp (𝑳 I g))) h
Module: Mathlib.Geometry.Manifold.GroupLieAlgebra

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : ChartedSpace H G
inst✝¹ : Group G
inst✝ : LieGroup I (minSmoothness 𝕜 3) G
g h : G
M : minSmoothness 𝕜 3 ≠ 0
this : ((fun x ↦ g⁻¹ * x) ∘ fun x ↦ g * x) = id
⊢ mfderiv% ((fun x ↦ g⁻¹ * x) ∘ fun x ↦ g * x) h = ContinuousLinearMap.id 𝕜 (TangentSpace I h)

Tactic:
rw [this, id_eq, mfderiv_id]

Goal state after:
Module: Mathlib.Geometry.Manifold.GroupLieAlgebra

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : ChartedSpace H G
inst✝¹ : Group G
inst✝ : LieGroup I (minSmoothness 𝕜 3) G
g h : G
M : minSmoothness 𝕜 3 ≠ 0
A : (mfderiv% fun x ↦ g⁻¹ * x) (g * h) ∘SL (mfderiv% fun x ↦ g * x) h = ContinuousLinearMap.id 𝕜 (TangentSpace I h)
this : ((fun x ↦ g * x) ∘ fun x ↦ g⁻¹ * x) = id
⊢ mfderiv% ((fun x ↦ g * x) ∘ fun x ↦ g⁻¹ * x) (g * h) = ContinuousLinearMap.id 𝕜 (TangentSpace I (g * h))

Tactic:
rw [this, id_eq, mfderiv_id]

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorField.Pullback

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹³ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹² : TopologicalSpace H
E : Type u_3
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : ChartedSpace H M
H' : Type u_5
inst✝⁷ : TopologicalSpace H'
E' : Type u_6
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁴ : TopologicalSpace M'
inst✝³ : ChartedSpace H' M'
f : M → M'
x₀ : M
V : (x : M') → TangentSpace I' x
n : ℕ∞ω
t : Set M'
y₀ : M'
inst✝² : IsManifold I 2 M
inst✝¹ : IsManifold I' 2 M'
inst✝ : CompleteSpace E
hV : MDiffAt[t] (T% V) y₀
hf : ContMDiffAt I I' n f x₀
hf' : (mfderiv% f x₀).IsInvertible
hmn : 2 ≤ n
hy₀ : y₀ = f x₀
⊢ (MDiffAt[f ⁻¹' t] fun x ↦ ⟨x, mpullback I I' f V x⟩) x₀

Tactic:
subst hy₀
  exact hV.mpullback_vectorField_preimage hf hf' hmn

Goal state after:
Module: Mathlib.Geometry.Manifold.GroupLieAlgebra

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁷ : TopologicalSpace H
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁴ : TopologicalSpace G
inst✝³ : ChartedSpace H G
inst✝² : Group G
inst✝¹ : LieGroup I (minSmoothness 𝕜 3) G
inst✝ : CompleteSpace E
u v w : GroupLieAlgebra I G
⊢ ⁅u + v, w⁆ = ⁅u, w⁆ + ⁅v, w⁆

Tactic:
by
    simp only [GroupLieAlgebra.bracket_def, mulInvariantVectorField_add]
    rw [mlieBracket_add_left]
    · exact mdifferentiableAt_mulInvariantVectorField _
    · exact mdifferentiableAt_mulInvariantVectorField _

Goal state after:
Module: Mathlib.Geometry.Manifold.Immersion

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
E'' : Type u
F : Type u_5
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : NormedAddCommGroup E''
inst✝⁸ : NormedSpace 𝕜 E''
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
H : Type u_7
inst✝⁵ : TopologicalSpace H
G : Type u_9
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
N : Type u_13
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f : M → N
x : M
h : IsImmersionAtOfComplement F I J n f x
this : ContinuousOn (⇑h.equiv ∘ fun x ↦ (x, 0)) (h.domChart.extend I).target
⊢ ContinuousOn (↑(h.codChart.extend J) ∘ f ∘ ↑(h.domChart.extend I).symm) (h.domChart.extend I).target

Tactic:
exact this.congr h.writtenInCharts

Goal state after:
Module: Mathlib.Geometry.Manifold.Instances.Real

Goal state before:
pp: x✝ y✝ : ℝ
hxy : Fact (x✝ < y✝)
x y : ℝ
h : Fact (x < y)
⊢ ∀ ⦃x_1 : EuclideanHalfSpace 1⦄, x_1 ∈ {z | (↑z).ofLp 0 < y - x} → ⟨max (y - (↑x_1).ofLp 0) x, ⋯⟩ ∈ {z | x < ↑z}

Tactic:
by
    simp only [lt_max_iff, mem_ofPred_eq]; intro z hz; left
    linarith

Goal state after:
Module: Mathlib.Geometry.Manifold.Instances.Sphere

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
x : ↑(sphere 0 1)
hx : ↑x ≠ v
a : ℝ := ((innerSL ℝ) v) ↑x
y : ↥(ℝ ∙ v)ᗮ := (ℝ ∙ v)ᗮ.orthogonalProjectionOnto ↑x
split : ↑x = a • v + ↑y
⊢ (‖(2 / (1 - a)) • y‖ ^ 2 + 4)⁻¹ • 4 • ↑((2 / (1 - a)) • y) +
      (‖(2 / (1 - a)) • y‖ ^ 2 + 4)⁻¹ • (‖(2 / (1 - a)) • y‖ ^ 2 - 4) • v =
    ↑x

Tactic:
have hvy : ⟪v, y⟫_ℝ = 0 := Submodule.mem_orthogonal_singleton_iff_inner_right.mp y.2

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
x : ↑(sphere 0 1)
hx : ↑x ≠ v
a : ℝ := ((innerSL ℝ) v) ↑x
y : ↥(ℝ ∙ v)ᗮ := (ℝ ∙ v)ᗮ.orthogonalProjectionOnto ↑x
split : ↑x = a • v + ↑y
hvy : ⟪v, ↑y⟫_ℝ = 0
⊢ (‖(2 / (1 - a)) • y‖ ^ 2 + 4)⁻¹ • 4 • ↑((2 / (1 - a)) • y) +
      (‖(2 / (1 - a)) • y‖ ^ 2 + 4)⁻¹ • (‖(2 / (1 - a)) • y‖ ^ 2 - 4) • v =
    ↑x
Module: Mathlib.Geometry.Manifold.Instances.Sphere

Goal state before:
pp: case e'_3.e'_5
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
x : ↑(sphere 0 1)
hx : ↑x ≠ v
a : ℝ := ((innerSL ℝ) v) ↑x
y : ↥(ℝ ∙ v)ᗮ := (ℝ ∙ v)ᗮ.orthogonalProjectionOnto ↑x
split : ↑x = a • v + ↑y
hvy : ⟪v, ↑y⟫_ℝ = 0
hvy' : ⟪a • v, ↑y⟫_ℝ = 0
⊢ a ^ 2 = ‖a • v‖ * ‖a • v‖

Tactic:
simp [norm_smul, hv, ← sq, sq_abs]

Goal state after:
Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
a : ℝ
ha : a ≠ 0
⊢ IsMIntegralCurve (γ ∘ fun x ↦ x * a) (a • v) ↔ IsMIntegralCurve γ v

Tactic:
refine ⟨fun hγ ↦ ?_, fun hγ ↦ hγ.comp_mul _⟩

Goal state after:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
a : ℝ
ha : a ≠ 0
hγ : IsMIntegralCurve (γ ∘ fun x ↦ x * a) (a • v)
⊢ IsMIntegralCurve γ v
Module: Mathlib.Geometry.Manifold.Instances.Sphere

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
⊢ ContMDiff ((𝓡 1).prod (𝓡 1)) (𝓡 1) ω fun p ↦ p.1 * p.2

Tactic:
apply ContMDiff.codRestrict_sphere
    let c : Circle → ℂ := (↑)
    have h₂ : ContMDiff (𝓘(ℝ, ℂ).prod 𝓘(ℝ, ℂ)) 𝓘(ℝ, ℂ) ω fun z : ℂ × ℂ => z.fst * z.snd := by
      rw [contMDiff_iff]
      exact ⟨continuous_mul, fun x y => contDiff_mul.contDiffOn⟩
    -- TODO bug: filling in ω yields an error; expected type has metavariables...
    suffices h₁ : ContMDiff _ _ _ (Prod.map c c) from
      h₂.comp h₁
    apply ContMDiff.prodMap <;> exact contMDiff_coe_sphere

Goal state after:
Module: Mathlib.Geometry.Manifold.Riemannian.PathELength

Goal state before:
pp: case hγ
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : (x : M) → ENorm (TangentSpace I x)
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
x y : M
r : ℝ≥0∞
a b : ℝ
hr : riemannianEDist I x y < r
hab : a < b
γ : ℝ → M
hγx : γ 0 = x
hγy : γ 1 = y
γ_smooth : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc 0 1)
hγ : pathELength I γ 0 1 < r
a' : ℝ
haa' : a < a'
ha'b : a' < b
b' : ℝ
ha'b' : a' < b'
hb'b : b' < b
η : ℝ → ℝ := ⋯
A : ∀ t < a', η t = 0
A' : ∀ t < a', (γ ∘ η) t = x
B : ∀ (t : ℝ), b' < t → η t = 1
B' : ∀ (t : ℝ), b' < t → (γ ∘ η) t = y
⊢ MDiff[Icc (η a) (η b)] γ

Tactic:
rw [A a haa', B b hb'b]
      apply γ_smooth.mdifferentiableOn one_ne_zero

Goal state after:
Module: Mathlib.Geometry.Manifold.Submersion

Goal state before:
pp: case pos
𝕜 : Type u_1
E'' : Type u_3
F : Type u_5
H : Type u_7
G : Type u_9
E : Type u
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : NormedAddCommGroup E''
inst✝⁸ : NormedSpace 𝕜 E''
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
N : Type u_13
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f : M → N
h : IsSubmersionOfComplement F I J n f
hM : IsEmpty M
⊢ IsSubmersion I J n f

pp: case neg
𝕜 : Type u_1
E'' : Type u_3
F : Type u_5
H : Type u_7
G : Type u_9
E : Type u
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : NormedAddCommGroup E''
inst✝⁸ : NormedSpace 𝕜 E''
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
N : Type u_13
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f : M → N
h : IsSubmersionOfComplement F I J n f
hM : Nonempty M
⊢ IsSubmersion I J n f

Tactic:
· rw [IsSubmersion]
    use PUnit, by infer_instance, by infer_instance
    exact fun x ↦ (IsEmpty.false x).elim

Goal state after:
case neg
𝕜 : Type u_1
E'' : Type u_3
F : Type u_5
H : Type u_7
G : Type u_9
E : Type u
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : NormedAddCommGroup E''
inst✝⁸ : NormedSpace 𝕜 E''
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
N : Type u_13
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f : M → N
h : IsSubmersionOfComplement F I J n f
hM : Nonempty M
⊢ IsSubmersion I J n f
Module: Mathlib.GroupTheory.ClassEquation

Goal state before:
pp: case e'_2.e'_6
G : Type u_2
inst✝⁴ : Group G
inst✝³ : (x : ConjClasses G) → Fintype ↑x.carrier
inst✝² : Fintype G
inst✝¹ : Fintype ↥(Subgroup.center G)
inst✝ : Fintype ↑(noncenter G)
⊢ ∑ x ∈ (noncenter G).toFinset, x.carrier.toFinset.card =
    ∑ᶠ (x : ConjClasses G) (_ : x ∈ noncenter G), Nat.card ↑x.carrier

Tactic:
← finsum_set_coe_eq_finsum_mem (noncenter G),

Goal state after:
case e'_2.e'_6
G : Type u_2
inst✝⁴ : Group G
inst✝³ : (x : ConjClasses G) → Fintype ↑x.carrier
inst✝² : Fintype G
inst✝¹ : Fintype ↥(Subgroup.center G)
inst✝ : Fintype ↑(noncenter G)
⊢ ∑ x ∈ (noncenter G).toFinset, x.carrier.toFinset.card = ∑ᶠ (j : ↑(noncenter G)), Nat.card ↑(↑j).carrier
Module: Mathlib.GroupTheory.GroupAction.CardCommute

Goal state before:
pp: case inr
G : Type u_3
inst✝ : Group G
val✝ : Infinite G
⊢ Nat.card { p // Commute p.1 p.2 } = Nat.card G * Nat.card (ConjClasses G)

Tactic:
Nat.card_eq_zero_of_infinite,

Goal state after:
case inr
G : Type u_3
inst✝ : Group G
val✝ : Infinite G
⊢ 0 = Nat.card G * Nat.card (ConjClasses G)
Module: Mathlib.GroupTheory.GroupAction.CardCommute

Goal state before:
pp: case inr
G : Type u_3
inst✝ : Group G
val✝ : Infinite G
⊢ 0 = Nat.card G * Nat.card (ConjClasses G)

Tactic:
Nat.card_eq_zero_of_infinite,

Goal state after:
case inr
G : Type u_3
inst✝ : Group G
val✝ : Infinite G
⊢ 0 = 0 * Nat.card (ConjClasses G)
Module: Mathlib.GroupTheory.SpecificGroups.KleinFour

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : IsKleinFour G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
x y : G
hx : x ≠ 1
hy : y ≠ 1
hxy : x ≠ y
⊢ {x * y, x, y, 1} = univ

Tactic:
apply Finset.eq_univ_of_card
  rw [card_four']
  repeat rw [card_insert_of_notMem]
  on_goal 4 => simpa using mul_notMem_of_exponent_two (by simp) hx hy hxy
  all_goals simp_all

Goal state after:
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: case neg
G : Type u_2
inst✝ : Group G
h : ¬↑(Nat.card G) = 0
⊢ ↑(Nat.card (ConjClasses G)) * ↑(Nat.card G) / (↑(Nat.card G) * ↑(Nat.card G)) =
    ↑(Nat.card (ConjClasses G)) / ↑(Nat.card G)

Tactic:
· exact mul_div_mul_right _ _ h

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: case r
n : ℕ
hodd : Odd n
hne1 : n ≠ 1
i : ZMod n
h : ∀ (g : DihedralGroup n), g * r i = r i * g
⊢ r i = 1

pp: case sr
n : ℕ
hodd : Odd n
hne1 : n ≠ 1
i : ZMod n
h : ∀ (g : DihedralGroup n), g * sr i = sr i * g
⊢ sr i = 1

Tactic:
· have heq := sr.inj (h (sr i))
    simp_all

Goal state after:
case sr
n : ℕ
hodd : Odd n
hne1 : n ≠ 1
i : ZMod n
h : ∀ (g : DihedralGroup n), g * sr i = sr i * g
⊢ sr i = 1
Module: Mathlib.GroupTheory.Coprod.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
⊢ MonoidHom.mrange inl ⊔ MonoidHom.mrange inr = ⊤

Tactic:
rw [← mclosure_range_inl_union_inr, Submonoid.closure_union, ← MonoidHom.coe_mrange,
    ← MonoidHom.coe_mrange, Submonoid.closure_eq, Submonoid.closure_eq]

Goal state after: