mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality

Goal state before:
pp: case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hz : ‖z‖ = 1
H : angle x z ≠ π
H0 : angle x z = angle x y + angle y z
H1 : ¬angle x z = 0
Hxz : Real.sin (angle x z) ≠ 0
H2 : ¬angle x y = 0
H3 : ¬angle y z = 0
H4 : ¬angle x y = π
H5 : ¬angle y z = π
H6 :
  Real.cos (angle x y) * Real.cos (angle y z) - Real.sin (angle x y) * Real.sin (angle y z) =
    Real.cos (angle x y) * Real.cos (angle y z) +
      Real.sin (angle x y) * Real.sin (angle y z) *
        ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫
Hw : Real.sin (angle x y) * Real.sin (angle y z) ≠ 0
H8 : ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫ = -1
H9 : ortho y x ≠ 0
H10 : ortho y z ≠ 0
H11 : ‖NormedSpace.normalize (ortho y x)‖ = 1
H12 : ‖NormedSpace.normalize (ortho y z)‖ = 1
⊢ Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z

Tactic:
rw [inner_eq_neg_one_iff_of_norm_eq_one H11 H12] at H8

Goal state after:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hz : ‖z‖ = 1
H : angle x z ≠ π
H0 : angle x z = angle x y + angle y z
H1 : ¬angle x z = 0
Hxz : Real.sin (angle x z) ≠ 0
H2 : ¬angle x y = 0
H3 : ¬angle y z = 0
H4 : ¬angle x y = π
H5 : ¬angle y z = π
H6 :
  Real.cos (angle x y) * Real.cos (angle y z) - Real.sin (angle x y) * Real.sin (angle y z) =
    Real.cos (angle x y) * Real.cos (angle y z) +
      Real.sin (angle x y) * Real.sin (angle y z) *
        ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫
Hw : Real.sin (angle x y) * Real.sin (angle y z) ≠ 0
H8 : NormedSpace.normalize (ortho y x) = -NormedSpace.normalize (ortho y z)
H9 : ortho y x ≠ 0
H10 : ortho y z ≠ 0
H11 : ‖NormedSpace.normalize (ortho y x)‖ = 1
H12 : ‖NormedSpace.normalize (ortho y z)‖ = 1
⊢ Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
hy : y ≠ 0
h_mem : y ∈ Submodule.span ℝ≥0 {x, z}
⊢ angle x z = angle x y + angle y z

Tactic:
rw [Submodule.mem_span_pair] at h_mem

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
hy : y ≠ 0
h_mem : ∃ a b, a • x + b • z = y
⊢ angle x z = angle x y + angle y z
Module: Mathlib.Geometry.Euclidean.Congruence

Goal state before:
pp: 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₂
h : ∠ a b c = ∠ a' b' c'
hd₁ : dist a b = dist a' b'
hd₂ : dist b c = dist b' c'
⊢ dist c a = dist c' a'

Tactic:
rw [dist_comm, dist_comm c' a', ← sq_eq_sq₀ (by positivity) (by positivity), pow_two, pow_two,
    EuclideanGeometry.law_cos a b c, EuclideanGeometry.law_cos a' b' c']

Goal state after:
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₂
h : ∠ a b c = ∠ a' b' c'
hd₁ : dist a b = dist a' b'
hd₂ : dist b c = dist b' c'
⊢ dist a b * dist a b + dist c b * dist c b - 2 * dist a b * dist c b * Real.cos (∠ a b c) =
    dist a' b' * dist a' b' + dist c' b' * dist c' b' - 2 * dist a' b' * dist c' b' * Real.cos (∠ a' b' c')
Module: Mathlib.Geometry.Euclidean.Circumcenter

Goal state before:
pp: case neg.inr
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
p p₁ p₂ : P
r : ℝ
h₁ : ∀ (i : Fin (n + 1)), dist (s.points i) p₁ = r
h₂ : ∀ (i : Fin (n + 1)), dist (s.points i) p₂ = r
span_s : AffineSubspace ℝ P := ⋯
h₁' : ↑(s.orthogonalProjectionSpan p₁) = s.circumcenter
h₂' : ↑(s.orthogonalProjectionSpan p₂) = s.circumcenter
r₁ r₂ : ℝ
hp₁o : ↑(s.orthogonalProjectionSpan p₁) ∈ affineSpan ℝ (Set.range s.points)
hp₁ : p₁ = r₁ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ s.circumcenter
hp₂o : ↑(s.orthogonalProjectionSpan p₂) ∈ affineSpan ℝ (Set.range s.points)
hp₂ : p₂ = r₂ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ s.circumcenter
h : s.points 0 ∈ span_s
hd₂ : dist p₂ s.circumcenter * dist p₂ s.circumcenter = r * r - s.circumradius * s.circumradius
hp : ¬p = ↑(s.orthogonalProjectionSpan p)
hz : ⟪p -ᵥ ↑((orthogonalProjection span_s) p), p -ᵥ ↑((orthogonalProjection span_s) p)⟫ ≠ 0
hd₁ : r₁ = -r₂
⊢ r₁ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ s.circumcenter =
    (reflection (affineSpan ℝ (Set.range s.points)))
      (r₂ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ s.circumcenter)

Tactic:
hd₁,

Goal state after:
case neg.inr
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
p p₁ p₂ : P
r : ℝ
h₁ : ∀ (i : Fin (n + 1)), dist (s.points i) p₁ = r
h₂ : ∀ (i : Fin (n + 1)), dist (s.points i) p₂ = r
span_s : AffineSubspace ℝ P := affineSpan ℝ (Set.range s.points)
h₁' : ↑(s.orthogonalProjectionSpan p₁) = s.circumcenter
h₂' : ↑(s.orthogonalProjectionSpan p₂) = s.circumcenter
r₁ r₂ : ℝ
hp₁o : ↑(s.orthogonalProjectionSpan p₁) ∈ affineSpan ℝ (Set.range s.points)
hp₁ : p₁ = r₁ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ s.circumcenter
hp₂o : ↑(s.orthogonalProjectionSpan p₂) ∈ affineSpan ℝ (Set.range s.points)
hp₂ : p₂ = r₂ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ s.circumcenter
h : s.points 0 ∈ span_s
hd₂ : dist p₂ s.circumcenter * dist p₂ s.circumcenter = r * r - s.circumradius * s.circumradius
hp : ¬p = ↑(s.orthogonalProjectionSpan p)
hz : ⟪p -ᵥ ↑((orthogonalProjection span_s) p), p -ᵥ ↑((orthogonalProjection span_s) p)⟫ ≠ 0
hd₁ : r₁ = -r₂
⊢ -r₂ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ s.circumcenter =
    (reflection (affineSpan ℝ (Set.range s.points)))
      (r₂ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ s.circumcenter)
Module: Mathlib.Geometry.Euclidean.NinePointCircle

Goal state before:
pp: case pos
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Simplex ℝ P 0
i : Fin (0 + 1)
hrange : Set.range s.points = {s.points i}
hmonge : s.mongePoint ∈ affineSpan ℝ (Set.range s.points)
⊢ s.points i -ᵥ s.mongePoint - (↑0)⁻¹ • (s.points i -ᵥ s.mongePoint) = ((↑0 - 1) / ↑0) • (s.points i -ᵥ s.mongePoint)

Tactic:
hrange,

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 : Simplex ℝ P 0
i : Fin (0 + 1)
hrange : Set.range s.points = {s.points i}
hmonge : s.mongePoint ∈ affineSpan ℝ {s.points i}
⊢ s.points i -ᵥ s.mongePoint - (↑0)⁻¹ • (s.points i -ᵥ s.mongePoint) = ((↑0 - 1) / ↑0) • (s.points i -ᵥ s.mongePoint)
Module: Mathlib.Geometry.Euclidean.MongePoint

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
h : Invertible (↑n + 2 + 1)
⊢ ∑ i, centroidWeights ℝ univ i • (s.points i -ᵥ s.circumcenter) = ∑ x, ⅟(↑n + 2 + 1) • (s.points x -ᵥ s.circumcenter)

Tactic:
simp only [centroidWeights_apply, card_univ, Fintype.card_fin, Nat.cast_add, Nat.cast_ofNat,
    Nat.cast_one, invOf_eq_inv]

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

Goal state before:
pp: 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₂
h_not_col : ¬Collinear ℝ {a, b, c}
h₁ : ∠ a b c = ∠ a' b' c'
h₂ : ∠ b c a = ∠ b' c' a'
hne_pi_div_two : ∠ a b c ≠ Real.pi / 2 ∨ ∠ b c a ≠ Real.pi / 2
not_all_eq : a' ≠ b' ∨ b' ≠ c' ∨ a' ≠ c'
h_not_col' : ¬Collinear ℝ {a', b', c'}
h_pos1 : 0 < dist a b
h_pos1' : 0 < dist a' b'
h_pos2 : 0 < dist b c
h_pos2' : 0 < dist b' c'
h₃ : ∠ c a b = ∠ c' a' b'
h_sin_ne1 : Real.sin (∠ b c a) ≠ 0
h_sin_ne2 : Real.sin (∠ c a b) ≠ 0
h_sin1 : Real.sin (∠ c a b) * dist a b = Real.sin (∠ b c a) * dist b c
h_sin1' : Real.sin (∠ c' a' b') * dist a' b' = Real.sin (∠ b' c' a') * dist b' c'
⊢ ![a, b, c] ∼ ![a', b', c']

Tactic:
← eq_div_iff_mul_eq (by positivity)

Goal state after:
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₂
h_not_col : ¬Collinear ℝ {a, b, c}
h₁ : ∠ a b c = ∠ a' b' c'
h₂ : ∠ b c a = ∠ b' c' a'
hne_pi_div_two : ∠ a b c ≠ Real.pi / 2 ∨ ∠ b c a ≠ Real.pi / 2
not_all_eq : a' ≠ b' ∨ b' ≠ c' ∨ a' ≠ c'
h_not_col' : ¬Collinear ℝ {a', b', c'}
h_pos1 : 0 < dist a b
h_pos1' : 0 < dist a' b'
h_pos2 : 0 < dist b c
h_pos2' : 0 < dist b' c'
h₃ : ∠ c a b = ∠ c' a' b'
h_sin_ne1 : Real.sin (∠ b c a) ≠ 0
h_sin_ne2 : Real.sin (∠ c a b) ≠ 0
h_sin1 : Real.sin (∠ c a b) = Real.sin (∠ b c a) * dist b c / dist a b
h_sin1' : Real.sin (∠ c' a' b') = Real.sin (∠ b' c' a') * dist b' c' / dist a' b'
⊢ ![a, b, c] ∼ ![a', b', c']
Module: Mathlib.Geometry.Euclidean.Similarity

Goal state before:
pp: 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₂
h_not_col : ¬Collinear ℝ {a, b, c}
h₁ : ∠ a b c = ∠ a' b' c'
h₂ : ∠ b c a = ∠ b' c' a'
hne_pi_div_two : ∠ a b c ≠ Real.pi / 2 ∨ ∠ b c a ≠ Real.pi / 2
not_all_eq : a' ≠ b' ∨ b' ≠ c' ∨ a' ≠ c'
h_not_col' : ¬Collinear ℝ {a', b', c'}
h_pos1 : 0 < dist a b
h_pos1' : 0 < dist a' b'
h_pos2 : 0 < dist b c
h_pos2' : 0 < dist b' c'
h₃ : ∠ c a b = ∠ c' a' b'
h_sin_ne1 : Real.sin (∠ b c a) ≠ 0
h_sin_ne2 : Real.sin (∠ c a b) ≠ 0
h_sin1 : dist a b * dist b' c' = dist b c * dist a' b'
h_sin1' : Real.sin (∠ c a b) = Real.sin (∠ b c a) * dist b' c' / dist a' b'
h_sin2 : Real.sin (∠ a b c) * dist b c = Real.sin (∠ c a b) * dist c a
h_sin2' : Real.sin (∠ a' b' c') * dist b' c' = Real.sin (∠ c' a' b') * dist c' a'
⊢ ![a, b, c] ∼ ![a', b', c']

Tactic:
← eq_div_iff_mul_eq (by positivity)

Goal state after:
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₂
h_not_col : ¬Collinear ℝ {a, b, c}
h₁ : ∠ a b c = ∠ a' b' c'
h₂ : ∠ b c a = ∠ b' c' a'
hne_pi_div_two : ∠ a b c ≠ Real.pi / 2 ∨ ∠ b c a ≠ Real.pi / 2
not_all_eq : a' ≠ b' ∨ b' ≠ c' ∨ a' ≠ c'
h_not_col' : ¬Collinear ℝ {a', b', c'}
h_pos1 : 0 < dist a b
h_pos1' : 0 < dist a' b'
h_pos2 : 0 < dist b c
h_pos2' : 0 < dist b' c'
h₃ : ∠ c a b = ∠ c' a' b'
h_sin_ne1 : Real.sin (∠ b c a) ≠ 0
h_sin_ne2 : Real.sin (∠ c a b) ≠ 0
h_sin1 : dist a b * dist b' c' = dist b c * dist a' b'
h_sin1' : Real.sin (∠ c a b) = Real.sin (∠ b c a) * dist b' c' / dist a' b'
h_sin2 : Real.sin (∠ a b c) = Real.sin (∠ c a b) * dist c a / dist b c
h_sin2' : Real.sin (∠ a' b' c') = Real.sin (∠ c' a' b') * dist c' a' / dist b' c'
⊢ ![a, b, c] ∼ ![a', b', c']
Module: Mathlib.Geometry.Euclidean.MongePoint

Goal state before:
pp: n : ℕ
i₁ i₂ : Fin (n + 3)
h : i₁ ≠ i₂
⊢ 1 - ∑ x, centroidWeightsWithCircumcenter {i₁, i₂}ᶜ x = 0

Tactic:
rw [sum_centroidWeightsWithCircumcenter, sub_self]

Goal state after:
n : ℕ
i₁ i₂ : Fin (n + 3)
h : i₁ ≠ i₂
⊢ {i₁, i₂}ᶜ.Nonempty
Module: Mathlib.Geometry.Euclidean.MongePoint

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
e : Fin (n + 3) ≃ Fin (n + 3)
i₁ i₂ : Fin (n + 3)
⊢ (s.reindex e).mongePlane i₁ i₂ = s.mongePlane (e.symm i₁) (e.symm i₂)

Tactic:
simp_rw [mongePlane, reindex_points, reindex_range_points, Function.comp_apply, centroid_def,
    reindex]

Goal state after:
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 + 2)
e : Fin (n + 3) ≃ Fin (n + 3)
i₁ i₂ : Fin (n + 3)
⊢ mk' ((affineCombination ℝ {i₁, i₂}ᶜ (s.points ∘ ⇑e.symm)) (centroidWeights ℝ {i₁, i₂}ᶜ))
        (ℝ ∙ (s.points (e.symm i₁) -ᵥ s.points (e.symm i₂)))ᗮ ⊓
      affineSpan ℝ (Set.range s.points) =
    mk' ((affineCombination ℝ {e.symm i₁, e.symm i₂}ᶜ s.points) (centroidWeights ℝ {e.symm i₁, e.symm i₂}ᶜ))
        (ℝ ∙ (s.points (e.symm i₁) -ᵥ s.points (e.symm i₂)))ᗮ ⊓
      affineSpan ℝ (Set.range s.points)
Module: Mathlib.Geometry.Group.Growth.LinearLowerBound

Goal state before:
pp: case inr
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hXclosure : (↑(closure ↑X)).Infinite
hX : X.Nontrivial
⊢ StrictMono fun n ↦ X ^ n

Tactic:
have h n : (X ^ (n - 1) : Set G) ≠ closure (X : Set G) :=
    fun h ↦ by simp [← h, ← coe_pow] at hXclosure

Goal state after:
case inr
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hXclosure : (↑(closure ↑X)).Infinite
hX : X.Nontrivial
h : ∀ (n : ℕ), ↑X ^ (n - 1) ≠ ↑(closure ↑X)
⊢ StrictMono fun n ↦ X ^ n
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
x : M
⊢ I.IsInteriorPoint x ↔ ¬I.IsBoundaryPoint x

Tactic:
refine ⟨?_,
    by simpa only [or_iff_not_imp_right] using isInteriorPoint_or_isBoundaryPoint x (I := I)⟩
  by_contra! h
  rw [← mem_empty_iff_false (extChartAt I x x),
    ← disjoint_iff_inter_eq_empty.mp disjoint_interior_frontier, mem_inter_iff]
  exact h

Goal state after:
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✝
n✝ : WithTop ℕ∞
e✝ e'✝ : OpenPartialHomeomorph M✝ H✝
x✝² : M✝
𝕜 : 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
n : WithTop ℕ∞
inst✝ : IsManifold I n M
e e' : OpenPartialHomeomorph M H
x : M
hn : n ≠ 0
he : e ∈ atlas H M
he' : e' ∈ atlas H M
hex : x ∈ e.source
hex' : x ∈ e'.source
hx : ↑(e.extend I) x ∈ interior (e.extend I).target
φ : PartialEquiv E E := extendCoordChange e e'
hφ : ContDiffOn 𝕜 n (↑φ) φ.source
h✝ : IsRCLikeNormedField 𝕜
x✝¹ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x✝ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
hφx' : Surjective ⇑(ContinuousLinearMap.restrictScalars ℝ (fderivWithin 𝕜 (↑φ) φ.source (↑(e.extend I) x)))
hφx : φ.source ∈ 𝓝 (↑(e.extend I) x)
⊢ ↑(e.extend I) x ∈ φ.source

Tactic:
by simp [φ, hex, hex']

Goal state after:
Module: Mathlib.Topology.VectorBundle.Hom

Goal state before:
pp: 𝕜₁ : Type u_1
inst✝²⁰ : NontriviallyNormedField 𝕜₁
𝕜₂ : Type u_2
inst✝¹⁹ : NontriviallyNormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
B : Type u_3
F₁ : Type u_4
inst✝¹⁸ : NormedAddCommGroup F₁
inst✝¹⁷ : NormedSpace 𝕜₁ F₁
E₁ : B → Type u_5
inst✝¹⁶ : (x : B) → AddCommGroup (E₁ x)
inst✝¹⁵ : (x : B) → Module 𝕜₁ (E₁ x)
inst✝¹⁴ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_6
inst✝¹³ : NormedAddCommGroup F₂
inst✝¹² : NormedSpace 𝕜₂ F₂
E₂ : B → Type u_7
inst✝¹¹ : (x : B) → AddCommGroup (E₂ x)
inst✝¹⁰ : (x : B) → Module 𝕜₂ (E₂ x)
inst✝⁹ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁸ : TopologicalSpace B
e₁ e₁' : Trivialization F₁ TotalSpace.proj
e₂ e₂' : Trivialization F₂ TotalSpace.proj
inst✝⁷ : (x : B) → TopologicalSpace (E₁ x)
inst✝⁶ : FiberBundle F₁ E₁
inst✝⁵ : (x : B) → TopologicalSpace (E₂ x)
inst✝⁴ : FiberBundle F₂ E₂
inst✝³ : Trivialization.IsLinear 𝕜₁ e₁
inst✝² : Trivialization.IsLinear 𝕜₁ e₁'
inst✝¹ : Trivialization.IsLinear 𝕜₂ e₂
inst✝ : Trivialization.IsLinear 𝕜₂ e₂'
b : B
hb : b ∈ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet)
L : F₁ →SL[σ] F₂
v : F₁
⊢ (↑(Trivialization.coordChangeL 𝕜₂ e₂ e₂' b) ∘SL L ∘SL ↑(Trivialization.coordChangeL 𝕜₁ e₁' e₁ b).symm.symm) v =
    (Trivialization.continuousLinearMapAt 𝕜₂ e₂' b ∘SL
        (continuousLinearMap σ e₁ e₂).symm b L ∘SL Trivialization.symmL 𝕜₁ e₁' b)
      v

Tactic:
continuousLinearMap_symm_apply' σ e₁ e₂ hb.1,

Goal state after:
𝕜₁ : Type u_1
inst✝²⁰ : NontriviallyNormedField 𝕜₁
𝕜₂ : Type u_2
inst✝¹⁹ : NontriviallyNormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
B : Type u_3
F₁ : Type u_4
inst✝¹⁸ : NormedAddCommGroup F₁
inst✝¹⁷ : NormedSpace 𝕜₁ F₁
E₁ : B → Type u_5
inst✝¹⁶ : (x : B) → AddCommGroup (E₁ x)
inst✝¹⁵ : (x : B) → Module 𝕜₁ (E₁ x)
inst✝¹⁴ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_6
inst✝¹³ : NormedAddCommGroup F₂
inst✝¹² : NormedSpace 𝕜₂ F₂
E₂ : B → Type u_7
inst✝¹¹ : (x : B) → AddCommGroup (E₂ x)
inst✝¹⁰ : (x : B) → Module 𝕜₂ (E₂ x)
inst✝⁹ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁸ : TopologicalSpace B
e₁ e₁' : Trivialization F₁ TotalSpace.proj
e₂ e₂' : Trivialization F₂ TotalSpace.proj
inst✝⁷ : (x : B) → TopologicalSpace (E₁ x)
inst✝⁶ : FiberBundle F₁ E₁
inst✝⁵ : (x : B) → TopologicalSpace (E₂ x)
inst✝⁴ : FiberBundle F₂ E₂
inst✝³ : Trivialization.IsLinear 𝕜₁ e₁
inst✝² : Trivialization.IsLinear 𝕜₁ e₁'
inst✝¹ : Trivialization.IsLinear 𝕜₂ e₂
inst✝ : Trivialization.IsLinear 𝕜₂ e₂'
b : B
hb : b ∈ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet)
L : F₁ →SL[σ] F₂
v : F₁
⊢ (↑(Trivialization.coordChangeL 𝕜₂ e₂ e₂' b) ∘SL L ∘SL ↑(Trivialization.coordChangeL 𝕜₁ e₁' e₁ b).symm.symm) v =
    (Trivialization.continuousLinearMapAt 𝕜₂ e₂' b ∘SL
        (Trivialization.symmL 𝕜₂ e₂ b ∘SL L ∘SL Trivialization.continuousLinearMapAt 𝕜₁ e₁ b) ∘SL
          Trivialization.symmL 𝕜₁ e₁' b)
      v
Module: Mathlib.Geometry.Manifold.VectorField.Pullback

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
E' : Type u_6
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace 𝕜 E'
f : E → E'
V : E' → E'
s : Set E
x : E
⊢ mpullbackWithin 𝓘(𝕜, E) 𝓘(𝕜, E') f V s x = pullbackWithin 𝕜 f V s x

Tactic:
simp only [mpullbackWithin, mfderivWithin_eq_fderivWithin, pullbackWithin]

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
E' : Type u_6
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace 𝕜 E'
f : E → E'
V : E' → E'
s : Set E
x : E
⊢ (fderivWithin 𝕜 f s x).inverse (V (f x)) = (fderivWithin 𝕜 f s x).inverse (V (f x))
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, v⁆ + ⁅u, w⁆

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

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_4
H : Type u_6
G : Type u_8
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_10
N : Type u_12
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f g : M → N
x : M
P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop
hP : IsLocalSourceTargetProperty P
hf : LiftSourceTargetPropertyAt I J n f x P
h' : f =ᶠ[𝓝 x] g
⊢ LiftSourceTargetPropertyAt I J n g x P

Tactic:
obtain ⟨s', hxs', hfg⟩ := h'.exists_mem

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_4
H : Type u_6
G : Type u_8
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_10
N : Type u_12
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f g : M → N
x : M
P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop
hP : IsLocalSourceTargetProperty P
hf : LiftSourceTargetPropertyAt I J n f x P
h' : f =ᶠ[𝓝 x] g
s' : Set M
hxs' : s' ∈ 𝓝 x
hfg : EqOn f g s'
⊢ LiftSourceTargetPropertyAt I J n g x P
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
equiv : (E × F) ≃L[𝕜] E''
domChart : OpenPartialHomeomorph M H
codChart : OpenPartialHomeomorph N G
hx : x ∈ domChart.source
hfx : f x ∈ codChart.source
hdomChart : domChart ∈ IsManifold.maximalAtlas I n M
hcodChart : codChart ∈ IsManifold.maximalAtlas J n N
hsource : domChart.source ⊆ f ⁻¹' codChart.source
hwrittenInExtend :
  EqOn (↑(codChart.extend J) ∘ f ∘ ↑(domChart.extend I).symm) (⇑equiv ∘ fun x ↦ (x, 0)) (domChart.extend I).target
⊢ IsImmersionAtOfComplement F I J n f x

Tactic:
by
  use domChart, codChart
  use equiv

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

Goal state before:
pp: case hφ'
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ↑(Icc x y)
φ₀ : (EuclideanSpace ℝ (Fin 1) × Unit) ≃L[ℝ] EuclideanSpace ℝ (Fin 1) :=
  ContinuousLinearEquiv.prodUnique ℝ (EuclideanSpace ℝ (Fin 1)) Unit
φ : (EuclideanSpace ℝ (Fin 1) × Unit) ≃L[ℝ] ℝ := φ₀.trans (PiLp.equivOfUnique 2 ℝ fun x ↦ ℝ)
hz : ↑z < y
this : ContDiff ℝ n fun y ↦ x + y
⊢ ContMDiffOn 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) n (↑(Homeomorph.addLeft (-x)).toOpenPartialHomeomorph.symm)
    (Homeomorph.addLeft (-x)).toOpenPartialHomeomorph.target

Tactic:
simpa [contMDiffOn_iff_contDiffOn, contDiffOn_univ, Homeomorph.addLeft]

Goal state after: