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

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p p' : P
s₁ s₂ : AffineSubspace ℝ P
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
hne : ↑((orthogonalProjection s₁) p) ≠ ↑((orthogonalProjection s₂) p)
h : ∠ (↑((orthogonalProjection s₁) p)) p' p = ∠ p p' ↑((orthogonalProjection s₂) p)
this✝¹ : Nonempty ↥s₁
this✝ : Nonempty ↥s₂
this : Nonempty ↥(s₁ ⊓ s₂)
hp₁ : ↑((orthogonalProjection s₁) p) ≠ p'
hp₂ : ↑((orthogonalProjection s₂) p) ≠ p'
hc : ¬Collinear ℝ {p', ↑((orthogonalProjection s₁) p), ↑((orthogonalProjection s₂) p)}
⊢ ∡ (↑((orthogonalProjection s₁) p)) p' p = ∡ p p' ↑((orthogonalProjection s₂) p)

Tactic:
angle_eq_iff_oangle_eq_or_wbtw hp₁ 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
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p p' : P
s₁ s₂ : AffineSubspace ℝ P
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
hne : ↑((orthogonalProjection s₁) p) ≠ ↑((orthogonalProjection s₂) p)
this✝¹ : Nonempty ↥s₁
this✝ : Nonempty ↥s₂
h :
  ∡ (↑((orthogonalProjection s₁) p)) p' p = ∡ p p' ↑((orthogonalProjection s₂) p) ∨
    Wbtw ℝ p' ↑((orthogonalProjection s₁) p) ↑((orthogonalProjection s₂) p) ∨
      Wbtw ℝ p' ↑((orthogonalProjection s₂) p) ↑((orthogonalProjection s₁) p)
this : Nonempty ↥(s₁ ⊓ s₂)
hp₁ : ↑((orthogonalProjection s₁) p) ≠ p'
hp₂ : ↑((orthogonalProjection s₂) p) ≠ p'
hc : ¬Collinear ℝ {p', ↑((orthogonalProjection s₁) p), ↑((orthogonalProjection s₂) p)}
⊢ ∡ (↑((orthogonalProjection s₁) p)) p' p = ∡ p p' ↑((orthogonalProjection s₂) p)
Module: Mathlib.Geometry.Euclidean.Sphere.Basic

Goal state before:
pp: case inr
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
S : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥S
inst✝ : S.direction.HasOrthogonalProjection
ps : Set ↥S
p₀ : ↥S
hp₀ : p₀ ∈ ps
c : P
r : ℝ
hr : ∀ p ∈ Subtype.val '' ps, dist p c = r
c' : ↥S := (orthogonalProjection S) c
p : ↥S
hp : p ∈ ps
hp_dist : dist (↑p) c = r
⊢ dist p c' = dist p₀ c'

Tactic:
have hp₀_dist : dist (p₀ : P) c = r := by grind

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

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
as : AffineSubspace ℝ P
h : s.IsTangent as
⊢ Metric.infDist s.center ↑as = s.radius

Tactic:
obtain ⟨p, h⟩ := h

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
as : AffineSubspace ℝ P
p : P
h : s.IsTangentAt p as
⊢ Metric.infDist s.center ↑as = s.radius
Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius

Goal state before:
pp: case mp
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
hp : dist p s.center = s.radius
p' : P
hp's : p' ∈ s
hp'i : p' ∈ s.orthRadius p
h' : s.radius ^ 2 = s.radius ^ 2 + dist p' p ^ 2
⊢ p' = p

Tactic:
simpa using h'

Goal state after:
Module: Mathlib.Geometry.Euclidean.Sphere.Tangent

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₁ 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

pp: 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

Tactic:
· exact .inl h

Goal state after:
case neg
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
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.Tangent

Goal state before:
pp: case neg.refine_3.refine_1
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
h : dist s₁.center s₂.center = s₁.radius + s₂.radius
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
h0 : ¬s₁.radius + s₂.radius = 0
⊢ 0 ≤ s₁.radius / (s₁.radius + s₂.radius)

pp: case neg.refine_3.refine_2
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
h : dist s₁.center s₂.center = s₁.radius + s₂.radius
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
h0 : ¬s₁.radius + s₂.radius = 0
⊢ s₁.radius / (s₁.radius + s₂.radius) ≤ 1

Tactic:
· positivity

Goal state after:
case neg.refine_3.refine_2
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
h : dist s₁.center s₂.center = s₁.radius + s₂.radius
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
h0 : ¬s₁.radius + s₂.radius = 0
⊢ s₁.radius / (s₁.radius + s₂.radius) ≤ 1
Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius

Goal state before:
pp: case inr.inr
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 : s.radius < dist p s.center
⊢ Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p) = ∅ ↔
    s.radius < dist p s.center ∨
      Module.finrank ℝ V = 1 ∧ dist p s.center < s.radius ∧ p ≠ s.center ∨ Subsingleton V ∧ s.radius ≠ 0

Tactic:
· simp [h, inter_orthRadius_eq_empty_of_radius_lt_dist]

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

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
ι : Type u_3
hne : Nonempty ι
inst✝ : Finite ι
p : ι → P
ha : AffineIndependent ℝ p
⊢ ∃! cs, cs.center ∈ affineSpan ℝ (Set.range p) ∧ Set.range p ⊆ Metric.sphere cs.center cs.radius

Tactic:
cases nonempty_fintype ι

Goal state after:
case intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
ι : Type u_3
hne : Nonempty ι
inst✝ : Finite ι
p : ι → P
ha : AffineIndependent ℝ p
val✝ : Fintype ι
⊢ ∃! cs, cs.center ∈ affineSpan ℝ (Set.range p) ∧ Set.range p ⊆ Metric.sphere cs.center cs.radius
Module: Mathlib.Geometry.Euclidean.Circumcenter

Goal state before:
pp: α : Type u_3
inst✝ : AddCommMonoid α
n : ℕ
f : PointsWithCircumcenterIndex n → α
⊢ ∑ i, f i = ∑ i, f (pointIndex i) + f circumcenterIndex

Tactic:
by
  classical
  have h : univ = insert circumcenterIndex (univ.map (pointIndexEmbedding n)) := by
    ext x
    refine ⟨fun h => ?_, fun _ => mem_univ _⟩
    obtain i | - := x
    · exact mem_insert_of_mem (mem_map_of_mem _ (mem_univ i))
    · exact mem_insert_self _ _
  change _ = (∑ i, f (pointIndexEmbedding n i)) + _
  rw [add_comm, h, ← sum_map, sum_insert]
  simp_rw [Finset.mem_map, not_exists]
  rintro x ⟨_, h⟩
  injection h

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

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
a b c : P
h : ¬Collinear ℝ {a, b, c}
hsin : Real.sin (∠ a b c) * dist a b = Real.sin (∠ a c b) * dist a c
hac : dist a c > 0
hsinabc : Real.sin (∠ a b c) ≥ 0
h1 : ∠ a c b < ∠ a b c
h2 : π / 2 < ∠ a b c
w : dist a c ≤ dist a b
⊢ Real.sin (∠ a b c) ≤ Real.sin (∠ a c b)

Tactic:
by_contra! w1

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c : P
h : ¬Collinear ℝ {a, b, c}
hsin : Real.sin (∠ a b c) * dist a b = Real.sin (∠ a c b) * dist a c
hac : dist a c > 0
hsinabc : Real.sin (∠ a b c) ≥ 0
h1 : ∠ a c b < ∠ a b c
h2 : π / 2 < ∠ a b c
w : dist a c ≤ dist a b
w1 : Real.sin (∠ a c b) < Real.sin (∠ a b c)
⊢ False
Module: Mathlib.Geometry.Euclidean.Triangle

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
a b c : P
h : ¬Collinear ℝ {a, b, c}
hsin : Real.sin (∠ a b c) * dist a b = Real.sin (∠ a c b) * dist a c
hac : dist a c > 0
hsinabc : Real.sin (∠ a b c) ≥ 0
h1 : ∠ a c b < ∠ a b c
h2 : π / 2 < ∠ a b c
w : dist a c ≤ dist a b
h3 : Real.sin (π - ∠ a b c) ≤ Real.sin (∠ a c b)
h5 : π - ∠ a b c < π / 2
⊢ π - ∠ a b c ≤ ∠ a c b

Tactic:
by_contra! w1

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c : P
h : ¬Collinear ℝ {a, b, c}
hsin : Real.sin (∠ a b c) * dist a b = Real.sin (∠ a c b) * dist a c
hac : dist a c > 0
hsinabc : Real.sin (∠ a b c) ≥ 0
h1 : ∠ a c b < ∠ a b c
h2 : π / 2 < ∠ a b c
w : dist a c ≤ dist a b
h3 : Real.sin (π - ∠ a b c) ≤ Real.sin (∠ a c b)
h5 : π - ∠ a b c < π / 2
w1 : ∠ a c b < π - ∠ a b c
⊢ False
Module: Mathlib.Geometry.Euclidean.Circumcenter

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
i₁ i₂ : Fin (n + 1)
h : i₁ ≠ i₂
hc : #{i₁, i₂} = 2
W : AffineSubspace ℝ P := affineSpan ℝ (s.points '' {i₁, i₂})
h_faces : ↑((orthogonalProjection W) s.circumcenter) = ↑((s.face hc).orthogonalProjectionSpan s.circumcenter)
⊢ ∑ x,
        ((if x ∈ {i₁, i₂} then
            ((↑(#{i₁, i₂}))⁻¹ + (↑(#{i₁, i₂}))⁻¹) • (s.pointsWithCircumcenter (pointIndex x) -ᵥ Classical.choice ⋯)
          else 0) -
          if x = i₁ ∨ x = i₂ then 1 • (s.pointsWithCircumcenter (pointIndex x) -ᵥ Classical.choice ⋯) else 0) +
      (0 - 1 • (s.pointsWithCircumcenter circumcenterIndex -ᵥ Classical.choice ⋯) -
        -1 • (s.pointsWithCircumcenter circumcenterIndex -ᵥ Classical.choice ⋯)) =
    0

Tactic:
hc,

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
i₁ i₂ : Fin (n + 1)
h : i₁ ≠ i₂
hc : #{i₁, i₂} = 2
W : AffineSubspace ℝ P := affineSpan ℝ (s.points '' {i₁, i₂})
h_faces : ↑((orthogonalProjection W) s.circumcenter) = ↑((s.face hc).orthogonalProjectionSpan s.circumcenter)
⊢ ∑ x,
        ((if x ∈ {i₁, i₂} then ((↑2)⁻¹ + (↑2)⁻¹) • (s.pointsWithCircumcenter (pointIndex x) -ᵥ Classical.choice ⋯)
          else 0) -
          if x = i₁ ∨ x = i₂ then 1 • (s.pointsWithCircumcenter (pointIndex x) -ᵥ Classical.choice ⋯) else 0) +
      (0 - 1 • (s.pointsWithCircumcenter circumcenterIndex -ᵥ Classical.choice ⋯) -
        -1 • (s.pointsWithCircumcenter circumcenterIndex -ᵥ Classical.choice ⋯)) =
    0
Module: Mathlib.Geometry.Euclidean.Incenter

Goal state before:
pp: case inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
signs : Finset (Fin 3)
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h : Simplex.excenter t signs = Simplex.incenter t
⊢ Simplex.excenter t signs = Simplex.incenter t ∨
    Simplex.excenter t signs = Simplex.excenter t {i₁} ∨
      Simplex.excenter t signs = Simplex.excenter t {i₂} ∨ Simplex.excenter t signs = Simplex.excenter t {i₃}

pp: case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
signs : Finset (Fin 3)
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
i : Fin (2 + 1)
h : Simplex.excenter t signs = Simplex.excenter t {i}
⊢ Simplex.excenter t signs = Simplex.incenter t ∨
    Simplex.excenter t signs = Simplex.excenter t {i₁} ∨
      Simplex.excenter t signs = Simplex.excenter t {i₂} ∨ Simplex.excenter t signs = Simplex.excenter t {i₃}

Tactic:
· exact .inl h

Goal state after:
case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
signs : Finset (Fin 3)
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
i : Fin (2 + 1)
h : Simplex.excenter t signs = Simplex.excenter t {i}
⊢ Simplex.excenter t signs = Simplex.incenter t ∨
    Simplex.excenter t signs = Simplex.excenter t {i₁} ∨
      Simplex.excenter t signs = Simplex.excenter t {i₂} ∨ Simplex.excenter t signs = Simplex.excenter t {i₃}
Module: Mathlib.Geometry.Euclidean.Sphere.Power

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
h₃ : ‖z - y‖ = ‖z + y‖
r : ℝ
hr : x = r • y
hzy : ⟪z, y⟫ = 0
hzx : ⟪z, x⟫ = 0
⊢ |(r - 1) * (r + 1) * ‖y‖ ^ 2| = |r ^ 2 * ‖y‖ ^ 2 - ‖y‖ ^ 2|

Tactic:
by ring_nf

Goal state after:
Module: Mathlib.Geometry.Euclidean.Sphere.Ptolemy

Goal state before:
pp: V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d p : P
h : Cospherical {a, b, c, d}
hapc : ∠ a p c = π
hbpd : ∠ b p d = π
⊢ Cospherical {a, c, b, d}

Tactic:
Set.insert_comm c b {d}

Goal state after:
V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d p : P
h : Cospherical {a, b, c, d}
hapc : ∠ a p c = π
hbpd : ∠ b p d = π
⊢ Cospherical {a, b, c, d}
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 : ℕ∞ω
A : Type u_10
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : ContMDiffRing 𝓘(𝕜, A) n A
⊢ ⟨fun x ↦ (algebraMap 𝕜 A) 0, ⋯⟩ = 0

Tactic:
ext; exact (algebraMap 𝕜 A).map_zero

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
h : ¬Disjoint (ModelWithCorners.interior M) (ModelWithCorners.boundary M)
x : M
h1 : x ∈ ModelWithCorners.interior M
h2 : x ∈ ModelWithCorners.boundary M
⊢ False

Tactic:
← mem_empty_iff_false (extChartAt I x x),

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
h : ¬Disjoint (ModelWithCorners.interior M) (ModelWithCorners.boundary M)
x : M
h1 : x ∈ ModelWithCorners.interior M
h2 : x ∈ ModelWithCorners.boundary M
⊢ ↑(extChartAt I x) x ∈ ∅
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
h : I.IsInteriorPoint x ∧ I.IsBoundaryPoint x
⊢ False

Tactic:
← mem_empty_iff_false (extChartAt I x x),

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
x : M
h : I.IsInteriorPoint x ∧ I.IsBoundaryPoint x
⊢ ↑(extChartAt I x) x ∈ ∅
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
⊢ (ModelWithCorners.boundary M)ᶜ = ModelWithCorners.interior M

Tactic:
by
  rw [← compl_interior, compl_compl]

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
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'
p : M × N
⊢ interior (range ↑I) ×ˢ interior (range ↑J) = interior (range ↑(I.prod J))

Tactic:
rw [← interior_prod_eq, ← range_prodMap, modelWithCorners_prod_coe]

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
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'
inst✝ : BoundarylessManifold J N
⊢ ModelWithCorners.boundary (M × N) = (ModelWithCorners.boundary M).prod univ

Tactic:
rw [boundary_prod, Boundaryless.boundary_eq_empty (I := J)]

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'
inst✝ : BoundarylessManifold J N
⊢ univ.prod ∅ ∪ (ModelWithCorners.boundary M).prod univ = (ModelWithCorners.boundary M).prod univ
Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
F : Type u_4
M : Type u_5
E : B → Type u_6
inst✝¹⁵ : NontriviallyNormedField 𝕜
inst✝¹⁴ : NormedAddCommGroup F
inst✝¹³ : NormedSpace 𝕜 F
inst✝¹² : TopologicalSpace (TotalSpace F E)
inst✝¹¹ : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst✝¹⁰ : NormedAddCommGroup EB
inst✝⁹ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝⁸ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
EM : Type u_10
inst✝⁷ : NormedAddCommGroup EM
inst✝⁶ : NormedSpace 𝕜 EM
HM : Type u_11
inst✝⁵ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace HM M
inst✝² : TopologicalSpace B
inst✝¹ : ChartedSpace HB B
inst✝ : FiberBundle F E
f : M → TotalSpace F E
s : Set M
x₀ : M
hf : ContinuousWithinAt f s x₀
⊢ (MDiffAt[s] fun x ↦
        (↑(extChartAt IB (f x₀).proj) (↑(trivializationAt F E (f x₀).proj).toPartialEquiv (f x)).1,
          (↑(trivializationAt F E (f x₀).proj).toPartialEquiv (f x)).2))
      x₀ ↔
    (MDiffAt[s] fun x ↦ ↑(extChartAt IB (f x₀).proj) (f x).proj) x₀ ∧
      (MDiffAt[s] fun x ↦ (↑(trivializationAt F E (f x₀).proj) (f x)).2) x₀

Tactic:
refine (mdifferentiableWithinAt_prod_iff _).trans (and_congr ?_ Iff.rfl)

Goal state after:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
M : Type u_5
E : B → Type u_6
inst✝¹⁵ : NontriviallyNormedField 𝕜
inst✝¹⁴ : NormedAddCommGroup F
inst✝¹³ : NormedSpace 𝕜 F
inst✝¹² : TopologicalSpace (TotalSpace F E)
inst✝¹¹ : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst✝¹⁰ : NormedAddCommGroup EB
inst✝⁹ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝⁸ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
EM : Type u_10
inst✝⁷ : NormedAddCommGroup EM
inst✝⁶ : NormedSpace 𝕜 EM
HM : Type u_11
inst✝⁵ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace HM M
inst✝² : TopologicalSpace B
inst✝¹ : ChartedSpace HB B
inst✝ : FiberBundle F E
f : M → TotalSpace F E
s : Set M
x₀ : M
hf : ContinuousWithinAt f s x₀
⊢ MDiffAt[s]
        (Prod.fst ∘ fun x ↦
          (↑(extChartAt IB (f x₀).proj) (↑(trivializationAt F E (f x₀).proj).toPartialEquiv (f x)).1,
            (↑(trivializationAt F E (f x₀).proj).toPartialEquiv (f x)).2))
      x₀ ↔
    (MDiffAt[s] fun x ↦ ↑(extChartAt IB (f x₀).proj) (f x).proj) x₀