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

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 : Set P
t t₀ : Triangle ℝ P
ht : Set.range t.points ⊆ insert t₀.orthocenter (Set.range t₀.points)
ht₀o : t₀.orthocenter ∉ Set.range t₀.points
ht₀s : s = insert t₀.orthocenter (Set.range t₀.points)
hs : Set.range t.points = Set.range t₀.points
⊢ s = insert t.orthocenter (Set.range t₀.points)

Tactic:
convert! ht₀s using 2

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 : Set P
t t₀ : Triangle ℝ P
ht : Set.range t.points ⊆ insert t₀.orthocenter (Set.range t₀.points)
ht₀o : t₀.orthocenter ∉ Set.range t₀.points
ht₀s : s = insert t₀.orthocenter (Set.range t₀.points)
hs : Set.range t.points = Set.range t₀.points
⊢ t.orthocenter = t₀.orthocenter
Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary

Goal state before:
pp: case mp
𝕜 : 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
aux : interior (range ↑I) ×ˢ interior (range ↑J) = interior (range ↑(I.prod J))
hp : p ∈ ModelWithCorners.interior (M × N)
⊢ p ∈ ModelWithCorners.interior M ×ˢ ModelWithCorners.interior N

Tactic:
replace hp : (I.prod J).IsInteriorPoint p := hp
    rw [IsInteriorPoint, ← aux] at hp
    exact hp

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'
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 ×ˢ univ ∪ univ ×ˢ (ModelWithCorners.interior N)ᶜ =
    univ.prod (ModelWithCorners.boundary N) ∪ (ModelWithCorners.boundary M).prod univ

Tactic:
J.compl_interior,

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 ×ˢ univ ∪ univ ×ˢ ModelWithCorners.boundary N =
    univ.prod (ModelWithCorners.boundary N) ∪ (ModelWithCorners.boundary M).prod univ
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 : ℕ∞ω
g : M → N
P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop
x : M
hx : x ∈ {x | LiftSourceTargetPropertyAt I J n g x P}
y : M
hy : y ∈ (domChart hx).source
⊢ y ∈ {x | LiftSourceTargetPropertyAt I J n g x P}

Tactic:
exact ⟨hx.domChart, hx.codChart, hy, hx.source_subset_preimage_source hy,
    hx.domChart_mem_maximalAtlas, hx.codChart_mem_maximalAtlas, hx.source_subset_preimage_source,
    hx.property⟩

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

Goal state before:
pp: x y : ℝ
hxy : Fact (x < y)
⊢ ↑((IccLeftChart x y).extend (𝓡∂ 1)) ⊥ ∈ frontier (range ↑(𝓡∂ 1))

Tactic:
exact IccLeftChart_extend_bot_mem_frontier

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

Goal state before:
pp: 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
z' : EuclideanSpace ℝ (Fin 1)
hz' : z' ∈ ((chartAt (EuclideanHalfSpace 1) z).extend (𝓡∂ 1)).target
⊢ (∃ y, ↑(𝓡∂ 1) y = z') ∧ ↑(𝓡∂ 1).symm z' ∈ (IccLeftChart x y).target

Tactic:
simpa [hz] using! hz'

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

Goal state before:
pp: 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
z' : EuclideanSpace ℝ (Fin 1)
hz' : z' ∈ ((chartAt (EuclideanHalfSpace 1) z).extend (𝓡∂ 1)).target
⊢ (∃ y, ↑(𝓡∂ 1) y = z') ∧ ↑(𝓡∂ 1).symm z' ∈ (IccRightChart x y).target

Tactic:
simpa [hz] using! hz'

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
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'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
a : TangentBundle I M
b : TangentBundle I' M'
U : ∀ (w : H) (w' : H'), UniqueDiffWithinAt 𝕜 (range (Prod.map ↑I ↑I')) (↑I w, ↑I' w')
smooth_pM : ContMDiffAt (I.tangent.prod I'.tangent) I.tangent n Prod.fst (a, b)
p : TangentBundle I M × TangentBundle I' M'
hp : p.1.proj ∈ (chartAt H a.proj).source ∧ p.2.proj ∈ (chartAt H' b.proj).source
φ : E → E := fun x ↦ ↑I (↑(chartAt H a.proj) (↑(chartAt H p.1.proj).symm (↑I.symm x)))
D0 : DifferentiableWithinAt 𝕜 φ (range ↑I) (↑I (↑(chartAt H p.1.proj) p.1.proj))
w : TangentBundle I' M'
⊢ DifferentiableWithinAt 𝕜 φ (range ↑I) (↑I (↑(chartAt H p.1.proj) p.1.proj), ↑I' (↑(chartAt H' w.proj) w.proj)).1

Tactic:
exact D0

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
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'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
a : TangentBundle I M
b : TangentBundle I' M'
U : ∀ (w : H) (w' : H'), UniqueDiffWithinAt 𝕜 (range ↑I ×ˢ range ↑I') (↑I w, ↑I' w')
smooth_pM : ContMDiffAt (I.tangent.prod I'.tangent) I.tangent n Prod.fst (a, b)
p : TangentBundle I M × TangentBundle I' M'
hp : p.1.proj ∈ (chartAt H a.proj).source ∧ p.2.proj ∈ (chartAt H' b.proj).source
φ : E → E := fun x ↦ ↑I (↑(chartAt H a.proj) (↑(chartAt H p.1.proj).symm (↑I.symm x)))
D0 : DifferentiableWithinAt 𝕜 φ (range ↑I) (↑I (↑(chartAt H p.1.proj) p.1.proj))
D :
  ∀ (w : TangentBundle I' M'),
    DifferentiableWithinAt 𝕜 (φ ∘ Prod.fst) (range (Prod.map ↑I ↑I'))
      (↑I (↑(chartAt H p.1.proj) p.1.proj), ↑I' (↑(chartAt H' w.proj) w.proj))
⊢ DifferentiableWithinAt 𝕜 φ (range ↑I) (↑I (↑(chartAt H p.1.proj) p.1.proj), ↑I' (↑(chartAt H' p.2.proj) p.2.proj)).1

Tactic:
exact D0

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
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'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
a : TangentBundle I M
b : TangentBundle I' M'
U : ∀ (w : H) (w' : H'), UniqueDiffWithinAt 𝕜 (range (Prod.map ↑I ↑I')) (↑I w, ↑I' w')
smooth_pM' : ContMDiffAt (I.tangent.prod I'.tangent) I'.tangent n Prod.snd (a, b)
p : TangentBundle I M × TangentBundle I' M'
hp : p.1.proj ∈ (chartAt H a.proj).source ∧ p.2.proj ∈ (chartAt H' b.proj).source
φ : E' → E' := fun x ↦ ↑I' (↑(chartAt H' b.proj) (↑(chartAt H' p.2.proj).symm (↑I'.symm x)))
D0 : DifferentiableWithinAt 𝕜 φ (range ↑I') (↑I' (↑(chartAt H' p.2.proj) p.2.proj))
w : TangentBundle I M
⊢ DifferentiableWithinAt 𝕜 φ (range ↑I') (↑I (↑(chartAt H w.proj) w.proj), ↑I' (↑(chartAt H' p.2.proj) p.2.proj)).2

Tactic:
exact D0

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

Goal state before:
pp: E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
⊢ MetrizableSpace M

Tactic:
by
  have := I.locallyCompactSpace; have := ChartedSpace.locallyCompactSpace H M
  have := I.secondCountableTopology
  have := ChartedSpace.secondCountable_of_sigmaCompact H M
  exact metrizableSpace_of_t3_secondCountable M

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
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'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
a : TangentBundle I M
b : TangentBundle I' M'
U : ∀ (w : H) (w' : H'), UniqueDiffWithinAt 𝕜 (range ↑I ×ˢ range ↑I') (↑I w, ↑I' w')
smooth_pM' : ContMDiffAt (I.tangent.prod I'.tangent) I'.tangent n Prod.snd (a, b)
p : TangentBundle I M × TangentBundle I' M'
hp : p.1.proj ∈ (chartAt H a.proj).source ∧ p.2.proj ∈ (chartAt H' b.proj).source
φ : E' → E' := fun x ↦ ↑I' (↑(chartAt H' b.proj) (↑(chartAt H' p.2.proj).symm (↑I'.symm x)))
D0 : DifferentiableWithinAt 𝕜 φ (range ↑I') (↑I' (↑(chartAt H' p.2.proj) p.2.proj))
D :
  ∀ (w : TangentBundle I M),
    DifferentiableWithinAt 𝕜 (φ ∘ Prod.snd) (range (Prod.map ↑I ↑I'))
      (↑I (↑(chartAt H w.proj) w.proj), ↑I' (↑(chartAt H' p.2.proj) p.2.proj))
⊢ DifferentiableWithinAt 𝕜 φ (range ↑I') (↑I (↑(chartAt H p.1.proj) p.1.proj), ↑I' (↑(chartAt H' p.2.proj) p.2.proj)).2

Tactic:
exact D0

Goal state after:
Module: Mathlib.Geometry.Manifold.Sheaf.Smooth

Goal state before:
pp: 𝕜 : Type u_1
inst✝²⁸ : NontriviallyNormedField 𝕜
EM : Type u_2
inst✝²⁷ : NormedAddCommGroup EM
inst✝²⁶ : NormedSpace 𝕜 EM
HM : Type u_3
inst✝²⁵ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
E : Type u_4
inst✝²⁴ : NormedAddCommGroup E
inst✝²³ : NormedSpace 𝕜 E
H : Type u_5
inst✝²² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_6
inst✝²¹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E H'
M : Type u
inst✝²⁰ : TopologicalSpace M
inst✝¹⁹ : ChartedSpace HM M
N G A A' R : Type u
inst✝¹⁸ : TopologicalSpace N
inst✝¹⁷ : ChartedSpace H N
inst✝¹⁶ : TopologicalSpace G
inst✝¹⁵ : ChartedSpace H G
inst✝¹⁴ : TopologicalSpace A
inst✝¹³ : ChartedSpace H A
inst✝¹² : TopologicalSpace A'
inst✝¹¹ : ChartedSpace H' A'
inst✝¹⁰ : TopologicalSpace R
inst✝⁹ : ChartedSpace H R
EP : Type u_7
inst✝⁸ : NormedAddCommGroup EP
inst✝⁷ : NormedSpace 𝕜 EP
HP : Type u_8
inst✝⁶ : TopologicalSpace HP
IP : ModelWithCorners 𝕜 EP HP
P : Type u
inst✝⁵ : TopologicalSpace P
inst✝⁴ : ChartedSpace HP P
inst✝³ : CommGroup A
inst✝² : CommGroup A'
inst✝¹ : LieGroup I ∞ A
inst✝ : LieGroup I' ∞ A'
⊢ CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↑(TopCat.of M)) (smoothPresheafCommGroup IM I M A)

Tactic:
CategoryTheory.Presheaf.isSheaf_iff_isSheaf_forget _ _
        (CategoryTheory.forget CommGrpCat)

Goal state after:
𝕜 : Type u_1
inst✝²⁸ : NontriviallyNormedField 𝕜
EM : Type u_2
inst✝²⁷ : NormedAddCommGroup EM
inst✝²⁶ : NormedSpace 𝕜 EM
HM : Type u_3
inst✝²⁵ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
E : Type u_4
inst✝²⁴ : NormedAddCommGroup E
inst✝²³ : NormedSpace 𝕜 E
H : Type u_5
inst✝²² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_6
inst✝²¹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E H'
M : Type u
inst✝²⁰ : TopologicalSpace M
inst✝¹⁹ : ChartedSpace HM M
N G A A' R : Type u
inst✝¹⁸ : TopologicalSpace N
inst✝¹⁷ : ChartedSpace H N
inst✝¹⁶ : TopologicalSpace G
inst✝¹⁵ : ChartedSpace H G
inst✝¹⁴ : TopologicalSpace A
inst✝¹³ : ChartedSpace H A
inst✝¹² : TopologicalSpace A'
inst✝¹¹ : ChartedSpace H' A'
inst✝¹⁰ : TopologicalSpace R
inst✝⁹ : ChartedSpace H R
EP : Type u_7
inst✝⁸ : NormedAddCommGroup EP
inst✝⁷ : NormedSpace 𝕜 EP
HP : Type u_8
inst✝⁶ : TopologicalSpace HP
IP : ModelWithCorners 𝕜 EP HP
P : Type u
inst✝⁵ : TopologicalSpace P
inst✝⁴ : ChartedSpace HP P
inst✝³ : CommGroup A
inst✝² : CommGroup A'
inst✝¹ : LieGroup I ∞ A
inst✝ : LieGroup I' ∞ A'
⊢ CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↑(TopCat.of M))
    (CategoryTheory.Functor.comp (smoothPresheafCommGroup IM I M A) (CategoryTheory.forget CommGrpCat))
Module: Mathlib.Geometry.Manifold.Submersion

Goal state before:
pp: 𝕜 : Type u_1
E' : Type u_2
E'' : Type u_3
E''' : Type u_4
F : Type u_5
F' : Type u_6
H : Type u_7
H' : Type u_8
G : Type u_9
G' : Type u_10
E : Type u
inst✝²⁸ : NontriviallyNormedField 𝕜
inst✝²⁷ : NormedAddCommGroup E
inst✝²⁶ : NormedSpace 𝕜 E
inst✝²⁵ : NormedAddCommGroup E'
inst✝²⁴ : NormedSpace 𝕜 E'
inst✝²³ : NormedAddCommGroup E''
inst✝²² : NormedSpace 𝕜 E''
inst✝²¹ : NormedAddCommGroup E'''
inst✝²⁰ : NormedSpace 𝕜 E'''
inst✝¹⁹ : NormedAddCommGroup F
inst✝¹⁸ : NormedSpace 𝕜 F
inst✝¹⁷ : NormedAddCommGroup F'
inst✝¹⁶ : NormedSpace 𝕜 F'
inst✝¹⁵ : TopologicalSpace H
inst✝¹⁴ : TopologicalSpace H'
inst✝¹³ : TopologicalSpace G
inst✝¹² : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 E'' G
J' : ModelWithCorners 𝕜 E''' G'
M : Type u_11
M' : Type u_12
N : Type u_13
N' : Type u_14
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
inst✝⁹ : TopologicalSpace M'
inst✝⁸ : ChartedSpace H' M'
inst✝⁷ : TopologicalSpace N
inst✝⁶ : ChartedSpace G N
inst✝⁵ : TopologicalSpace N'
inst✝⁴ : ChartedSpace G' N'
n : ℕ∞ω
x : M
f : M → N
g : M' → N'
x' : M'
inst✝³ : IsManifold I n M
inst✝² : IsManifold I' n M'
inst✝¹ : IsManifold J n N
inst✝ : IsManifold J' n N'
hf : IsSubmersionAtOfComplement F I J n f x
hg : IsSubmersionAtOfComplement F' I' J' n g x'
⊢ IsSubmersionAtOfComplement (F × F') (I.prod I') (J.prod J') n (Prod.map f g) (x, x')

Tactic:
apply LiftSourceTargetPropertyAt.prodMap hf.property hg.property
  rintro f φ₁ ψ₁ g φ₂ ψ₂ ⟨equiv₁, hfprop⟩ ⟨equiv₂, hgprop⟩
  use (equiv₁.prodCongr equiv₂).trans (ContinuousLinearEquiv.prodProdProdComm 𝕜 E'' F E''' F')
  rw [φ₁.extend_prod φ₂, ψ₁.extend_prod, PartialEquiv.prod_target, eqOn_prod_iff]
  exact ⟨fun x ⟨hx, hx'⟩ ↦ by simpa using hfprop hx, fun x ⟨hx, hx'⟩ ↦ by simpa using hgprop hx'⟩

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorBundle.LocalFrame

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
F : Type u_5
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
V : M → Type u_6
inst✝⁴ : TopologicalSpace (TotalSpace F V)
inst✝³ : (x : M) → AddCommGroup (V x)
inst✝² : (x : M) → Module 𝕜 (V x)
inst✝¹ : (x : M) → TopologicalSpace (V x)
inst✝ : FiberBundle F V
ι : Type u_7
s : ι → (x : M) → V x
u u' : Set M
n : ℕ∞ω
hs : IsLocalFrameOn I F n s u
hu'u : u' ⊆ u
x : M
hx : x ∈ u'
⊢ ⊤ ≤ Submodule.span 𝕜 (Set.range fun x_1 ↦ s x_1 x)

Tactic:
exact hs.generating (hu'u hx)

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

Goal state before:
pp: case e'_3
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✝³ : RiemannianBundle fun x ↦ TangentSpace I x
inst✝² : IsManifold I 1 M
inst✝¹ : IsContinuousRiemannianBundle E fun x ↦ TangentSpace I x
inst✝ : RegularSpace M
x : M
s : Set M
hs : s ∈ 𝓝 x
C : ℝ≥0
C_pos : C > 0
hC✝ : ∀ᶠ (y : M) in 𝓝 x, ‖mfderiv% ↑(extChartAt I x) y‖ₑ < ↑C
u : Set M
u_mem : u ∈ 𝓝 x
u_closed : IsClosed[inst✝⁵] u
us : u ⊆ s
hu : u ⊆ {y | ‖mfderiv% ↑(extChartAt I x) y‖ₑ < ↑C}
uc : u ⊆ (extChartAt I x).source
uc' : u ⊆ (chartAt H x).source
v : Set M
hv : v ⊆ u
v_mem : v ∈ 𝓝 x
v_open : IsOpen[inst✝⁵] v
r : ℝ≥0
hr : ball (↑(extChartAt I x) x) ↑r ⊆ ↑(extChartAt I x).symm ⁻¹' v
r_pos : 0 < r
y : M
hy : y ∈ {y | riemannianEDist I x y < ↑(r / C)}
γ : ℝ → M
hγx : γ 0 = x
hγy : γ 1 = y
γ_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ
hγ : pathELength I γ 0 1 < ↑(r / C)
A : Set ℝ := γ ⁻¹' u
zero_mem : 0 ∈ A
A_closed : IsClosed (A ∩ Icc 0 1)
t₁ : ℝ
ht₁0 : 0 ≤ t₁
ht₁1 : t₁ < 1
t₁_mem : Icc 0 t₁ ⊆ A
γ' : ℝ → E := ↑(extChartAt I x) ∘ γ
hC : ContMDiffOn 𝓘(ℝ, ℝ) 𝓘(ℝ, E) 1 γ' (Icc 0 t₁)
this : ‖γ' t₁ - γ' 0‖ₑ < ↑r
⊢ ↑(extChartAt I x) x = γ' 0

Tactic:
simp [γ', hγx]

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic

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
F : Type u_5
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
V : M → Type u_6
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : ∀ (x : M), IsTopologicalAddGroup (V x)
inst✝¹ : ∀ (x : M), ContinuousSMul 𝕜 (V x)
inst✝ : FiberBundle F V
ι : Type u_7
s : Finset ι
u : Set M
cov : ι → ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
h : ∀ (i : ι), IsCovariantDerivativeOn F (cov i) u
f : ι → M → 𝕜
hf : ∑ i ∈ s, f i = 1
σ : (x : M) → V x
g : M → 𝕜
x : M
hσ : MDiffAt (T% σ) x
hg : MDiffAt g x
hx : x ∈ u
⊢ ∑ i ∈ s, f i x • cov i (g • σ) x = ∑ i ∈ s, (g x • f i x • cov i σ x + f i x • (d% g x).smulRight (σ x))

Tactic:
congr! 1 with i hi

Goal state after:
case a
𝕜 : 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
F : Type u_5
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
V : M → Type u_6
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : ∀ (x : M), IsTopologicalAddGroup (V x)
inst✝¹ : ∀ (x : M), ContinuousSMul 𝕜 (V x)
inst✝ : FiberBundle F V
ι : Type u_7
s : Finset ι
u : Set M
cov : ι → ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
h : ∀ (i : ι), IsCovariantDerivativeOn F (cov i) u
f : ι → M → 𝕜
hf : ∑ i ∈ s, f i = 1
σ : (x : M) → V x
g : M → 𝕜
x : M
hσ : MDiffAt (T% σ) x
hg : MDiffAt g x
hx : x ∈ u
i : ι
hi : i ∈ s
⊢ f i x • cov i (g • σ) x = g x • f i x • cov i σ x + f i x • (d% g x).smulRight (σ x)
Module: Mathlib.Geometry.Polygon.Basic

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AffineSpace V P
t : Triangle R P
ht : t.points = ![t.points 0, t.points 1, t.points 2]
h : AffineIndependent R ![t.points 0, t.points 1, t.points 2]
i : Fin 3
⊢ AffineIndependent R ![(toPolygon t).vertices i, (toPolygon t).vertices (i + 1), (toPolygon t).vertices (i + 2)]

Tactic:
fin_cases i <;> dsimp

Goal state after:
case «0»
R : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AffineSpace V P
t : Triangle R P
ht : t.points = ![t.points 0, t.points 1, t.points 2]
h : AffineIndependent R ![t.points 0, t.points 1, t.points 2]
⊢ AffineIndependent R ![t.points 0, t.points 1, t.points 2]

case «1»
R : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AffineSpace V P
t : Triangle R P
ht : t.points = ![t.points 0, t.points 1, t.points 2]
h : AffineIndependent R ![t.points 0, t.points 1, t.points 2]
⊢ AffineIndependent R ![t.points 1, t.points 2, t.points 0]

case «2»
R : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AffineSpace V P
t : Triangle R P
ht : t.points = ![t.points 0, t.points 1, t.points 2]
h : AffineIndependent R ![t.points 0, t.points 1, t.points 2]
⊢ AffineIndependent R ![t.points 2, t.points 0, t.points 1]