mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: 𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : IsScalarTower 𝕜 A A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : ContinuousStar A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
s : Set 𝕜
hs : IsCompact s
f : 𝕜 → 𝕜
hf : ContinuousOn f s
hf0 : f 0 = 0
hs0 : 0 ∈ s
x : ↑{a | p a ∧ quasispectrum 𝕜 a ⊆ s}
⊢ (cfcₙHom ⋯) { toFun := (quasispectrum 𝕜 ↑x).domRestrict f, continuous_toFun := ⋯, map_zero' := hf0 } =
    (cfcₙHom ⋯)
      ({ toFun := s.domRestrict f, continuous_toFun := ⋯, map_zero' := hf0 }.comp
        { toFun := Subtype.map id ⋯, continuous_toFun := ⋯, map_zero' := ⋯ })

Tactic:
congr!

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap

Goal state before:
pp: A₁ : Type u_1
A₂ : Type u_2
B₁ : Type u_3
B₂ : Type u_4
inst✝¹³ : NonUnitalCStarAlgebra A₁
inst✝¹² : NonUnitalCStarAlgebra A₂
inst✝¹¹ : PartialOrder A₁
inst✝¹⁰ : StarOrderedRing A₁
inst✝⁹ : PartialOrder A₂
inst✝⁸ : StarOrderedRing A₂
inst✝⁷ : CStarAlgebra B₁
inst✝⁶ : CStarAlgebra B₂
inst✝⁵ : PartialOrder B₁
inst✝⁴ : PartialOrder B₂
inst✝³ : StarOrderedRing B₁
F : Type u_5
inst✝² : FunLike F A₁ A₂
inst✝¹ : LinearMapClass F ℂ A₁ A₂
inst✝ : OrderHomClass F A₁ A₂
f : F
C : ℝ≥0
h : ∀ (a : A₁), ‖(ofClass f) a‖ ≤ ↑C * ‖a‖
⊢ ∃ C, ∀ (a : A₁), ‖f a‖ ≤ C * ‖a‖

Tactic:
exact ⟨C, h⟩

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix

Goal state before:
pp: m : Type u_1
n : Type u_2
A : Type u_5
inst✝⁴ : Fintype m
inst✝³ : NonUnitalCStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Fintype n
M : CStarMatrix m n A
v : C⋆ᵐᵒᵈ(A, m → A)
w : C⋆ᵐᵒᵈ(A, n → A)
⊢ ⟪(toCLM M) v, w⟫_A = ⟪v, (toCLM Mᴴ) w⟫_A

Tactic:
simpa using inner_toCLM_conjTranspose_left (M := Mᴴ) (v := v) (w := w)

Goal state after:
Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Opens X
hs : Nonempty ↥s
⊢ (e.subtypeRestr hs).target ⊆ e.target

Tactic:
rw [← e.image_source_eq_target, ← OpenPartialHomeomorph.image_source_eq_target,
    e.subtypeRestr_source]

Goal state after:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Opens X
hs : Nonempty ↥s
⊢ ↑(e.subtypeRestr hs) '' Subtype.val ⁻¹' e.source ⊆ ↑e '' e.source
Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions

Goal state before:
pp: case h
X✝ : Type u_1
X'✝ : Type u_2
Y : Type u_3
Y' : Type u_4
Z✝ : Type u_5
Z' : Type u_6
inst✝⁹ : TopologicalSpace X✝
inst✝⁸ : TopologicalSpace X'✝
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : TopologicalSpace Y'
inst✝⁵ : TopologicalSpace Z✝
inst✝⁴ : TopologicalSpace Z'
e✝ : OpenPartialHomeomorph X✝ Y
X : Type u_7
X' : Type u_8
Z : Type u_9
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Z
inst✝ : Nonempty Z
f : X → X'
e : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
h✝ : Nonempty X
F : X' → Z := extend f ↑e fun x ↦ Classical.arbitrary Z
F_eq : F = extend f ↑e fun x ↦ Classical.arbitrary Z
heq : EqOn F (↑e ∘ ↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm) (f '' e.source)
x' : X'
x : X
hx : x ∈ e.source
hx'x : f x = x'
⊢ ↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm x' ∈ e.source

Tactic:
rw [← hx'x, hf.toOpenPartialHomeomorph_left_inv]

Goal state after:
case h
X✝ : Type u_1
X'✝ : Type u_2
Y : Type u_3
Y' : Type u_4
Z✝ : Type u_5
Z' : Type u_6
inst✝⁹ : TopologicalSpace X✝
inst✝⁸ : TopologicalSpace X'✝
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : TopologicalSpace Y'
inst✝⁵ : TopologicalSpace Z✝
inst✝⁴ : TopologicalSpace Z'
e✝ : OpenPartialHomeomorph X✝ Y
X : Type u_7
X' : Type u_8
Z : Type u_9
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Z
inst✝ : Nonempty Z
f : X → X'
e : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
h✝ : Nonempty X
F : X' → Z := extend f ↑e fun x ↦ Classical.arbitrary Z
F_eq : F = extend f ↑e fun x ↦ Classical.arbitrary Z
heq : EqOn F (↑e ∘ ↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm) (f '' e.source)
x' : X'
x : X
hx : x ∈ e.source
hx'x : f x = x'
⊢ x ∈ e.source
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
e✝ : Pretrivialization F proj
x✝ : Z
e' : Pretrivialization F TotalSpace.proj
b : B
y : E b
e : Pretrivialization F proj
s : Set B
inst✝ : Nonempty (↑s → F → ↑(proj ⁻¹' s))
x : ↑s × F
hx : x ∈ Prod.map Subtype.val id ⁻¹' e.target
⊢ (if h : (↑x.1, x.2) ∈ e.target then ⟨e.invFun (↑x.1, x.2), ⋯⟩
    else Classical.arbitrary (↑s → F → ↑(proj ⁻¹' s)) x.1 x.2) ∈
    Subtype.val ⁻¹' e.source

Tactic:
simp only [mem_preimage, (Prod.map_apply), id_eq] at hx
    rw [dif_pos hx]; exact e.map_target' hx

Goal state after:
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: case left
ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i j : ι
x : B × F
⊢ x ∈ ((Z.localTrivAsPartialEquiv i).symm.trans (Z.localTrivAsPartialEquiv j)).source ↔ x ∈ (Z.trivChange i j).source

Tactic:
simp only [mem_localTrivAsPartialEquiv_target, mfld_simps]

Goal state after:
case left
ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i j : ι
x : B × F
⊢ x.1 ∈ Z.baseSet i ∧ ↑(Z.localTrivAsPartialEquiv i).symm x ∈ (Z.localTrivAsPartialEquiv j).source ↔
    x.1 ∈ Z.baseSet i ∧ x.1 ∈ Z.baseSet j
Module: Mathlib.Topology.SeparatedMap

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
⊢ IsLocallyInjective f ↔ IsOpenEmbedding (toPullbackDiag f)

Tactic:
isLocallyInjective_iff_isOpen_diagonal,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
⊢ IsOpen[instTopologicalSpaceSubtype] (Function.pullbackDiagonal f) ↔ IsOpenEmbedding (toPullbackDiag f)
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace (TotalSpace F E)
e✝ : Trivialization F proj
x : Z
e'✝ : Trivialization F TotalSpace.proj
b : B
y : E b
e e' : Trivialization F proj
H : Disjoint e.baseSet e'.baseSet
⊢ Disjoint e.source e'.source

Tactic:
rw [e.source_eq, e'.source_eq]

Goal state after:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace (TotalSpace F E)
e✝ : Trivialization F proj
x : Z
e'✝ : Trivialization F TotalSpace.proj
b : B
y : E b
e e' : Trivialization F proj
H : Disjoint e.baseSet e'.baseSet
⊢ Disjoint (proj ⁻¹' e.baseSet) (proj ⁻¹' e'.baseSet)
Module: Mathlib.Topology.Covering.Quotient

Goal state before:
pp: case refine_2
E : Type u_1
X : Type u_2
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace X
f : E → X
G : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G E
hf : IsQuotientMap f
inst✝² : ContinuousConstSMul G E
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
inst✝¹ : TopologicalSpace G
inst✝ : DiscreteTopology G
U : Set E
open_U : IsOpen[inst✝⁶] U
disjoint : ∀ (g : G), ((fun x ↦ g • x) '' U ∩ U).Nonempty → g = 1
pGE : ∀ (g : G) (e : E), f (g • e) = f e
preim_im : f ⁻¹' f '' U = ⋃ g, (fun x ↦ g • x) ⁻¹' U
this : Nonempty (X → E)
g : G
W : Set X
hWU : W ⊆ f '' U
isOpen : IsOpen[inst✝⁶] (f ⁻¹' W ∩ (fun x ↦ g • x) ⁻¹' U)
⊢ IsOpen[inst✝⁶] (f ⁻¹' W)

Tactic:
convert! isOpen_iUnion fun g : G ↦ isOpen.preimage (continuous_const_smul g)

Goal state after:
E : Type u_1
X : Type u_2
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace X
f : E → X
G : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G E
hf : IsQuotientMap f
inst✝² : ContinuousConstSMul G E
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
inst✝¹ : TopologicalSpace G
inst✝ : DiscreteTopology G
U : Set E
open_U : IsOpen[inst✝⁶] U
disjoint : ∀ (g : G), ((fun x ↦ g • x) '' U ∩ U).Nonempty → g = 1
pGE : ∀ (g : G) (e : E), f (g • e) = f e
preim_im : f ⁻¹' f '' U = ⋃ g, (fun x ↦ g • x) ⁻¹' U
this : Nonempty (X → E)
g : G
W : Set X
hWU : W ⊆ f '' U
isOpen : IsOpen[inst✝⁶] (f ⁻¹' W ∩ (fun x ↦ g • x) ⁻¹' U)
⊢ f ⁻¹' W = ⋃ i, (fun x ↦ i • x) ⁻¹' (f ⁻¹' W ∩ (fun x ↦ g • x) ⁻¹' U)
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
s : Set X
F : ↑s → Type u_3
inst✝ : (x : ↑s) → TopologicalSpace (F x)
hF : ∀ (x : ↑s), DiscreteTopology (F x)
e : (x : ↑s) → Trivialization (F x) f
h : ∀ (x : ↑s), ↑x ∈ (e x).baseSet
⊢ IsCoveringMapOn f s

Tactic:
cases isEmpty_or_nonempty E

Goal state after:
case inl
E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
s : Set X
F : ↑s → Type u_3
inst✝ : (x : ↑s) → TopologicalSpace (F x)
hF : ∀ (x : ↑s), DiscreteTopology (F x)
e : (x : ↑s) → Trivialization (F x) f
h : ∀ (x : ↑s), ↑x ∈ (e x).baseSet
h✝ : IsEmpty E
⊢ IsCoveringMapOn f s

case inr
E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
s : Set X
F : ↑s → Type u_3
inst✝ : (x : ↑s) → TopologicalSpace (F x)
hF : ∀ (x : ↑s), DiscreteTopology (F x)
e : (x : ↑s) → Trivialization (F x) f
h : ∀ (x : ↑s), ↑x ∈ (e x).baseSet
h✝ : Nonempty E
⊢ IsCoveringMapOn f s
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
s : Set X
hs : IsOpen[inst✝] s
f : E → X
h : ∀ (x : E), f x ∈ s
hf : IsCoveringMap fun x ↦ ⟨f x, ⋯⟩
⊢ f ⁻¹' s = Set.univ

Tactic:
simpa [Set.range, Set.subset_def] using h

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: x y : Circle
⊢ ⇑(x.path y) = ⇑exp ∘ ⇑(Path.segment (↑x).arg (x.angleDiff y + (↑x).arg))

Tactic:
ext t
  rw [path_apply, comp_apply]

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: case inr
A : Type u_1
inst✝ : CStarAlgebra A
u : A
hu : u ∈ unitary A
x : ℝ
hz : IsLeast (re '' spectrum ℂ u) x
h✝ : Nontrivial A
h_eqOn : Set.EqOn (fun z ↦ ‖z - 1‖ ^ 2) (fun z ↦ 2 * (1 - z.re)) (spectrum ℂ u)
⊢ ‖cfc (fun x ↦ x - 1 x) u‖ ^ 2 = 2 * (1 - x)

Tactic:
have h₂ : IsGreatest ((fun z ↦ 2 * (1 - z.re)) '' (spectrum ℂ u)) (2 * (1 - x)) := by
    have : Antitone (fun y : ℝ ↦ 2 * (1 - y)) := by intro _ _ _; simp only; gcongr
    simpa [Set.image_image] using this.map_isLeast hz

Goal state after:
case inr
A : Type u_1
inst✝ : CStarAlgebra A
u : A
hu : u ∈ unitary A
x : ℝ
hz : IsLeast (re '' spectrum ℂ u) x
h✝ : Nontrivial A
h_eqOn : Set.EqOn (fun z ↦ ‖z - 1‖ ^ 2) (fun z ↦ 2 * (1 - z.re)) (spectrum ℂ u)
h₂ : IsGreatest ((fun z ↦ 2 * (1 - z.re)) '' spectrum ℂ u) (2 * (1 - x))
⊢ ‖cfc (fun x ↦ x - 1 x) u‖ ^ 2 = 2 * (1 - x)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: T : ℝ
x : AddCircle T
⊢ (-x).toCircle * x.toCircle = x.toCircle⁻¹ * x.toCircle

Tactic:
simp [← toCircle_add]

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
ha_norm : ‖a‖ ≤ 1
h✝ : Nontrivial A
⊢ a + I • cfc Real.sqrt (1 - a ^ 2) = a + I • cfc (fun x ↦ √x) (cfc (fun x ↦ 1) a - cfc (fun x ↦ x) a ^ 2)

Tactic:
cfc_const_one ..,

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
ha_norm : ‖a‖ ≤ 1
h✝ : Nontrivial A
⊢ a + I • cfc Real.sqrt (1 - a ^ 2) = a + I • cfc (fun x ↦ √x) (1 - cfc (fun x ↦ x) a ^ 2)
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
⊢ span ℂ ↑(unitary A) = ⊤

Tactic:
eq_top_iff

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
⊢ ⊤ ≤ span ℂ ↑(unitary A)
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
T : E →L[𝕜] F
⊢ (↑T).kerᗮ = (↑(adjoint T)).rangeᗮᗮ

Tactic:
apply le_antisymm

Goal state after:
case a
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
T : E →L[𝕜] F
⊢ (↑T).kerᗮ ≤ (↑(adjoint T)).rangeᗮᗮ

case a
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
T : E →L[𝕜] F
⊢ (↑(adjoint T)).rangeᗮᗮ ≤ (↑T).kerᗮ
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
⊢ u ∈ pathComponent 1 ↔ ∃ l, (List.map expUnitary l).prod = u

Tactic:
constructor
  · revert u
    simp_rw [← Set.mem_range, ← Set.subset_def, pathComponent_eq_connectedComponent]
    refine IsClopen.connectedComponent_subset ?_ ⟨[], by simp⟩
    refine .of_thickening_subset_self zero_lt_two ?_
    intro u hu
    rw [mem_thickening_iff] at hu
    obtain ⟨v, ⟨⟨l, (hlv : (l.map expUnitary).prod = v)⟩, huv⟩⟩ := hu
    refine ⟨argSelfAdjoint (u * star v) :: l, ?_⟩
    simp [hlv, mul_assoc,
      expUnitary_eq_mul_inv u v (by simpa [Subtype.dist_eq, dist_eq_norm] using! huv)]
  · rintro ⟨l, rfl⟩
    induction l with
    | nil => simp
    | cons x xs ih => simpa using! (joined_one_expUnitary x).mul ih

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid

Goal state before:
pp: case mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
n : ℕ
inst✝ : CharZero k
s : Simplex k P n
p : P
h : 0 - ∑ x, (p -ᵥ s.centroid) = 0
this : ∑ i, (s.points i -ᵥ p) = ∑ i, (s.points i -ᵥ s.centroid - (p -ᵥ s.centroid))
⊢ p -ᵥ s.centroid = 0

Tactic:
simp only [sum_const, card_univ, Fintype.card_fin, zero_sub, neg_eq_zero] at h

Goal state after:
case mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
n : ℕ
inst✝ : CharZero k
s : Simplex k P n
p : P
this : ∑ i, (s.points i -ᵥ p) = ∑ i, (s.points i -ᵥ s.centroid - (p -ᵥ s.centroid))
h : (n + 1) • (p -ᵥ s.centroid) = 0
⊢ p -ᵥ s.centroid = 0
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : CharZero k
n : ℕ
s : Simplex k P n
fs₁ fs₂ : Finset (Fin (n + 1))
m₁ m₂ : ℕ
h₁ : #fs₁ = m₁ + 1
h₂ : #fs₂ = m₂ + 1
h :
  (affineCombination k univ s.points) (centroidWeightsIndicator k fs₁) =
    (affineCombination k univ s.points) (centroidWeightsIndicator k fs₂)
i : Fin (n + 1)
ha :
  (↑fs₁).indicator (Function.const (Fin (n + 1)) (↑(m₁ + 1))⁻¹) i =
    (↑fs₂).indicator (Function.const (Fin (n + 1)) (↑(m₂ + 1))⁻¹) i
key : ∀ (n : ℕ), ↑n + 1 ≠ 0
⊢ i ∈ fs₁ ↔ i ∈ fs₂

Tactic:
constructor <;> intro hi

Goal state after:
case mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : CharZero k
n : ℕ
s : Simplex k P n
fs₁ fs₂ : Finset (Fin (n + 1))
m₁ m₂ : ℕ
h₁ : #fs₁ = m₁ + 1
h₂ : #fs₂ = m₂ + 1
h :
  (affineCombination k univ s.points) (centroidWeightsIndicator k fs₁) =
    (affineCombination k univ s.points) (centroidWeightsIndicator k fs₂)
i : Fin (n + 1)
ha :
  (↑fs₁).indicator (Function.const (Fin (n + 1)) (↑(m₁ + 1))⁻¹) i =
    (↑fs₂).indicator (Function.const (Fin (n + 1)) (↑(m₂ + 1))⁻¹) i
key : ∀ (n : ℕ), ↑n + 1 ≠ 0
hi : i ∈ fs₁
⊢ i ∈ fs₂

case mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : CharZero k
n : ℕ
s : Simplex k P n
fs₁ fs₂ : Finset (Fin (n + 1))
m₁ m₂ : ℕ
h₁ : #fs₁ = m₁ + 1
h₂ : #fs₂ = m₂ + 1
h :
  (affineCombination k univ s.points) (centroidWeightsIndicator k fs₁) =
    (affineCombination k univ s.points) (centroidWeightsIndicator k fs₂)
i : Fin (n + 1)
ha :
  (↑fs₁).indicator (Function.const (Fin (n + 1)) (↑(m₁ + 1))⁻¹) i =
    (↑fs₂).indicator (Function.const (Fin (n + 1)) (↑(m₂ + 1))⁻¹) i
key : ∀ (n : ℕ), ↑n + 1 ≠ 0
hi : i ∈ fs₂
⊢ i ∈ fs₁
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : DecidableEq P
p : ι → P
s : Finset ι
n : ℕ
hc : #s = n + 1
⊢ 0 < n + 1

Tactic:
apply Nat.succ_pos

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

Goal state before:
pp: case inr.inr
k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s t : Finset V
hs : AffineIndependent k Subtype.val
hst : affineSpan k ↑s < affineSpan k ↑t
hs' : s.Nonempty
ht' : t.Nonempty
this✝ : Nonempty ↥s
this : Nonempty ↑↑t
dir_lt : vectorSpan k (Set.range Subtype.val) < vectorSpan k (Set.range Subtype.val)
finrank_lt : Fintype.card ↥s < finrank k ↥(vectorSpan k (Set.range Subtype.val)) + 1
⊢ #s < #t

Tactic:
simpa using finrank_lt.trans_le <| finrank_vectorSpan_range_add_one_le _ _

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
sp : AffineSubspace k P
inst✝ : FiniteDimensional k ↥sp.direction
hle : affineSpan k ↑(Finset.image p s) ≤ sp
hc : #s = finrank k ↥sp.direction + 1
⊢ 0 < finrank k ↥sp.direction + 1

Tactic:
apply Nat.succ_pos

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
n : ℕ
inst✝¹ : NeZero n
inst✝ : CharZero k
s : Simplex k P n
hn : 1 < n
p : P
h : ∀ (i : Fin (n + 1)), p ∈ s.median i
i₀ : Fin (n + 1) := 0
hp : p = (p -ᵥ s.centroid) +ᵥ s.centroid
s' : Finset (Fin (n + 1)) := {i₀}ᶜ
u : ↥s' → V := fun i ↦ s.points ↑i -ᵥ s.centroid
h_span : ∀ (i : ↥s'), p -ᵥ s.centroid ∈ k ∙ u i
hi : LinearIndependent k u
hcard : #s' = n
⊢ ∃ a ∈ s', ∃ a_1 ∈ s', ¬a = a_1

Tactic:
have hcard' : 1 < #s' := by grind

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
n : ℕ
inst✝¹ : NeZero n
inst✝ : CharZero k
s : Simplex k P n
hn : 1 < n
p : P
h : ∀ (i : Fin (n + 1)), p ∈ s.median i
i₀ : Fin (n + 1) := 0
hp : p = (p -ᵥ s.centroid) +ᵥ s.centroid
s' : Finset (Fin (n + 1)) := {i₀}ᶜ
u : ↥s' → V := fun i ↦ s.points ↑i -ᵥ s.centroid
h_span : ∀ (i : ↥s'), p -ᵥ s.centroid ∈ k ∙ u i
hi : LinearIndependent k u
hcard : #s' = n
hcard' : 1 < #s'
⊢ ∃ a ∈ s', ∃ a_1 ∈ s', ¬a = a_1
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
s : Set P
inst✝ : FiniteDimensional k ↥(affineSpan k s).direction
p : P
⊢ FiniteDimensional k ↥(affineSpan k (insert p s)).direction

Tactic:
by
  have : FiniteDimensional k (vectorSpan k s) := (direction_affineSpan k s) ▸ inferInstance
  rw [direction_affineSpan]
  infer_instance

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

Goal state before:
pp: case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₀ : P
h : p₀ ∈ s
v₀ : V
hv : ∀ v ∈ vectorSpan k s, ∃ r, r • v₀ = v
p : P
hp : p ∈ s
r : k
hr : r • v₀ = p -ᵥ p₀
⊢ p = r • v₀ +ᵥ p₀

Tactic:
eq_vadd_iff_vsub_eq

Goal state after:
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₀ : P
h : p₀ ∈ s
v₀ : V
hv : ∀ v ∈ vectorSpan k s, ∃ r, r • v₀ = v
p : P
hp : p ∈ s
r : k
hr : r • v₀ = p -ᵥ p₀
⊢ p -ᵥ p₀ = r • v₀
Module: Mathlib.Analysis.Normed.Affine.AddTorsorBases

Goal state before:
pp: V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
s : Set V
hs : Convex ℝ s
⊢ (interior s).Nonempty ↔ affineSpan ℝ s = ⊤

Tactic:
by
  rw [← interior_convexHull_nonempty_iff_affineSpan_eq_top, hs.convexHull_eq]

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inr.inr.inr.inr.inr
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hpq : q ≤ p
hq : 0 < q.toReal
left✝ : 0 < p.toReal
hpq' : q.toReal ≤ p.toReal
⊢ Memℓp f p

Tactic:
apply memℓp_gen
    have hf' := hfq.summable hq
    refine .of_norm_bounded_eventually hf' (@Set.Finite.subset _ { i | 1 ≤ ‖f i‖ } ?_ _ ?_)
    · have H : { x : α | 1 ≤ ‖f x‖ ^ q.toReal }.Finite := by
        simpa using hf'.tendsto_cofinite_zero.eventually_lt_const (by simp)
      exact H.subset fun i hi => Real.one_le_rpow hi hq.le
    · change ∀ i, ¬|‖f i‖ ^ p.toReal| ≤ ‖f i‖ ^ q.toReal → 1 ≤ ‖f i‖
      intro i hi
      have : 0 ≤ ‖f i‖ ^ p.toReal := by positivity
      simp only [abs_of_nonneg, this] at hi
      contrapose! hi
      exact Real.rpow_le_rpow_of_exponent_ge' (norm_nonneg _) hi.le hq.le hpq'

Goal state after:
Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv

Goal state before:
pp: case inr.left
ι : Type u_1
l : Filter ι
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
𝕜 : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
f' : ι → E → E →L[𝕜] G
x : E
r : ℝ
hf : ∀ (n : ι), ∀ y ∈ Metric.ball x r, HasFDerivAt (f n) (f' n y) y
hfg : Cauchy (map (fun n ↦ f n x) l)
this✝¹ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
hf' : ∀ ε > 0, ∀ᶠ (n : ι × ι) in l ×ˢ l, ∀ x_1 ∈ Metric.ball x r, dist (0 x_1) (-f' n.1 x_1 + f' n.2 x_1) < ε
this✝ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this : l.NeBot
hr : 0 < r
ε : ℝ
hε : ε > 0
q : ℝ
hqpos : 0 < q
hq : q * r < ε
⊢ ∀ᶠ (n : ι × ι) in l ×ˢ l, ∀ x_1 ∈ Metric.ball x r, dist (0 x_1) (f n.1 x_1 - f n.2 x_1 - (f n.1 x - f n.2 x)) < ε

Tactic:
apply (hf' q hqpos.gt).mono

Goal state after:
case inr.left
ι : Type u_1
l : Filter ι
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
𝕜 : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
f' : ι → E → E →L[𝕜] G
x : E
r : ℝ
hf : ∀ (n : ι), ∀ y ∈ Metric.ball x r, HasFDerivAt (f n) (f' n y) y
hfg : Cauchy (map (fun n ↦ f n x) l)
this✝¹ : RCLike 𝕜 := ⋯
hf' : ∀ ε > 0, ∀ᶠ (n : ι × ι) in l ×ˢ l, ∀ x_1 ∈ Metric.ball x r, dist (0 x_1) (-f' n.1 x_1 + f' n.2 x_1) < ε
this✝ : NormedSpace ℝ E := ⋯
this : l.NeBot
hr : 0 < r
ε : ℝ
hε : ε > 0
q : ℝ
hqpos : 0 < q
hq : q * r < ε
⊢ ∀ (x_1 : ι × ι),
    (∀ x_2 ∈ Metric.ball x r, dist (0 x_2) (-f' x_1.1 x_2 + f' x_1.2 x_2) < q) →
      ∀ x_2 ∈ Metric.ball x r, dist (0 x_2) (f x_1.1 x_2 - f x_1.2 x_2 - (f x_1.1 x - f x_1.2 x)) < ε