mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ : ι
b : B
a : F
i : ι
⊢ ∀ (t : Set (B × F)),
    IsOpen[instTopologicalSpaceProd] t →
      IsOpen ((Z.localTrivAsPartialEquiv i).source ∩ ↑(Z.localTrivAsPartialEquiv i) ⁻¹' t)

Tactic:
intro s

Goal state after:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ : ι
b : B
a : F
i : ι
s : Set (B × F)
⊢ IsOpen[instTopologicalSpaceProd] s →
    IsOpen ((Z.localTrivAsPartialEquiv i).source ∩ ↑(Z.localTrivAsPartialEquiv i) ⁻¹' s)
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ : ι
b : B
a : F
i : ι
t : Set Z.TotalSpace
j : ι
s : Set (B × F)
s_open : IsOpen[instTopologicalSpaceProd] s
ts : t = (Z.localTrivAsPartialEquiv j).source ∩ ↑(Z.localTrivAsPartialEquiv j) ⁻¹' s
e : PartialEquiv Z.TotalSpace (B × F) := Z.localTrivAsPartialEquiv i
e' : PartialEquiv Z.TotalSpace (B × F) := Z.localTrivAsPartialEquiv j
f : PartialEquiv (B × F) (B × F) := e.symm.trans e'
⊢ IsOpen[instTopologicalSpaceProd] (f.source ∩ ↑f ⁻¹' s)

Tactic:
PartialEquiv.EqOnSource.source_inter_preimage_eq (Z.localTrivAsPartialEquiv_trans i j)

Goal state after:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ : ι
b : B
a : F
i : ι
t : Set Z.TotalSpace
j : ι
s : Set (B × F)
s_open : IsOpen[instTopologicalSpaceProd] s
ts : t = (Z.localTrivAsPartialEquiv j).source ∩ ↑(Z.localTrivAsPartialEquiv j) ⁻¹' s
e : PartialEquiv Z.TotalSpace (B × F) := Z.localTrivAsPartialEquiv i
e' : PartialEquiv Z.TotalSpace (B × F) := Z.localTrivAsPartialEquiv j
f : PartialEquiv (B × F) (B × F) := e.symm.trans e'
⊢ IsOpen[instTopologicalSpaceProd] ((Z.trivChange i j).source ∩ ↑(Z.trivChange i j).toPartialEquiv ⁻¹' s)
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e : Trivialization F proj
α : Type u_5
l : Filter α
f : α → Z
z : Z
hz : z ∈ e.source
⊢ Tendsto f l (𝓝 z) ↔ Tendsto (proj ∘ f) l (𝓝 (proj z)) ∧ Tendsto (fun x ↦ (↑e (f x)).2) l (𝓝 (↑e z).2)

Tactic:
rw [e.nhds_eq_comap_inf_principal hz, tendsto_inf, tendsto_comap_iff, Prod.tendsto_iff, coe_coe,
    tendsto_principal, coe_fst _ hz]

Goal state after:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e : Trivialization F proj
α : Type u_5
l : Filter α
f : α → Z
z : Z
hz : z ∈ e.source
⊢ ((Tendsto (fun n ↦ ((↑e ∘ f) n).1) l (𝓝 (proj z)) ∧ Tendsto (fun n ↦ ((↑e ∘ f) n).2) l (𝓝 (↑e z).2)) ∧
      ∀ᶠ (a : α) in l, f a ∈ e.source) ↔
    Tendsto (proj ∘ f) l (𝓝 (proj z)) ∧ Tendsto (fun x ↦ (↑e (f x)).2) l (𝓝 (↑e z).2)
Module: Mathlib.Analysis.CStarAlgebra.Multiplier

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
n : ℤ
x y : A
⊢ (↑n).2 x * y = x * (↑n).1 y

Tactic:
rw [Prod.snd_intCast, Prod.fst_intCast]
      simp only [← Int.smul_one_eq_cast, smul_apply, one_apply_eq_self, mul_smul_comm,
        smul_mul_assoc]

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

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
k : 𝕜
x y : A
⊢ ((algebraMap 𝕜 (A →L[𝕜] A)) k) x * y = x * ((algebraMap 𝕜 (A →L[𝕜] A)) k) y

Tactic:
Algebra.algebraMap_eq_smul_one,

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
k : 𝕜
x y : A
⊢ (k • 1) x * y = x * (k • 1) y
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
I : Type u_3
inst✝¹ : TopologicalSpace I
inst✝ : DiscreteTopology I
x : X
t : Trivialization I f
hx : x ∈ t.baseSet
xi : ↑t.baseSet × I
⊢ (fun e ↦ (⟨f ↑e, ⋯⟩, (↑t ↑e).2)) ((fun xi ↦ ⟨t.invFun (↑xi.1, xi.2), ⋯⟩) xi) = xi

Tactic:
simp [t.proj_symm_apply', t.apply_symm_apply']

Goal state after:
Module: Mathlib.Topology.Covering.Quotient

Goal state before:
pp: case refine_4
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)
⊢ ∀ (i : G), Set.SurjOn f ((fun x ↦ i • x) ⁻¹' U) (f '' U)

Tactic:
rintro g x ⟨e, hU, rfl⟩; exact ⟨g⁻¹ • e, by apply (smul_inv_smul g e).symm ▸ hU, pGE _ e⟩

Goal state after:
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
hf : IsCoveringMap f
e₁ e₂ : E
he : f e₁ = f e₂
hne : e₁ ≠ e₂
⊢ ∃ s₁ s₂, IsOpen[inst✝¹] s₁ ∧ IsOpen[inst✝¹] s₂ ∧ e₁ ∈ s₁ ∧ e₂ ∈ s₂ ∧ Disjoint s₁ s₂

Tactic:
have : Nonempty (f ⁻¹' {f e₁}) := ⟨⟨e₁, rfl⟩⟩

Goal state after:
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
f : E → X
hf : IsCoveringMap f
e₁ e₂ : E
he : f e₁ = f e₂
hne : e₁ ≠ e₂
this : Nonempty ↑(f ⁻¹' {f e₁})
⊢ ∃ s₁ s₂, IsOpen[inst✝¹] s₁ ∧ IsOpen[inst✝¹] s₂ ∧ e₁ ∈ s₁ ∧ e₂ ∈ s₂ ∧ Disjoint s₁ s₂
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic

Goal state before:

Tactic:
_ = cfc (fun z => Real.log r + Real.log z) a :=
      cfc_congr (Real.log_mul hr <| ha₂ · ·)
    _ = _ := by rw [cfc_const_add _ _ _]

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

Goal state before:
pp: z : Circle
s : ℝ
n : ℕ
hs : s ≤ π
h1 : z ∈ centeredArc (π / ↑n)
h2 : z ^ n ∈ centeredArc s
⊢ 0 < s

Tactic:
contrapose! h2

Goal state after:
z : Circle
s : ℝ
n : ℕ
hs : s ≤ π
h1 : z ∈ centeredArc (π / ↑n)
h2 : s ≤ 0
⊢ z ^ n ∉ centeredArc s
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: n : ℤ
inst✝ : NeZero n
hn : IsUnit ↑n
e : AddCircle 1 ≃ₜ Circle := homeomorphCircle ⋯
⊢ IsQuotientCoveringMap (fun x ↦ x ^ n) ↥(zpowGroupHom n).ker

Tactic:
refine Topology.IsQuotientMap.isQuotientCoveringMap_of_isDiscrete_ker_monoidHom
    (f := zpowGroupHom (α := Circle) n) ?_ (Set.Finite.isDiscrete <| .of_preimage ?_ e.surjective)

Goal state after:
case refine_1
n : ℤ
inst✝ : NeZero n
hn : IsUnit ↑n
e : AddCircle 1 ≃ₜ Circle := homeomorphCircle ⋯
⊢ Topology.IsQuotientMap ⇑(zpowGroupHom n)

case refine_2
n : ℤ
inst✝ : NeZero n
hn : IsUnit ↑n
e : AddCircle 1 ≃ₜ Circle := homeomorphCircle ⋯
⊢ (⇑e ⁻¹' ↑(zpowGroupHom n).ker).Finite
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
A : E →L[𝕜] F
x : E
h : ⟪(adjoint A ∘SL A) x, x⟫_𝕜 = ⟪A x, A x⟫_𝕜
⊢ ‖A x‖ ^ 2 = re ⟪A x, A x⟫_𝕜

Tactic:
← inner_self_eq_norm_sq (𝕜 := 𝕜) _

Goal state after:
𝕜 : 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
A : E →L[𝕜] F
x : E
h : ⟪(adjoint A ∘SL A) x, x⟫_𝕜 = ⟪A x, A x⟫_𝕜
⊢ re ⟪A x, A x⟫_𝕜 = re ⟪A x, A x⟫_𝕜
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
A : E →L[𝕜] F
x : E
h : ⟪x, (adjoint A ∘SL A) x⟫_𝕜 = ⟪A x, A x⟫_𝕜
⊢ ‖A x‖ ^ 2 = re ⟪A x, A x⟫_𝕜

Tactic:
← inner_self_eq_norm_sq (𝕜 := 𝕜) _

Goal state after:
𝕜 : 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
A : E →L[𝕜] F
x : E
h : ⟪x, (adjoint A ∘SL A) x⟫_𝕜 = ⟪A x, A x⟫_𝕜
⊢ re ⟪A x, A x⟫_𝕜 = re ⟪A x, A x⟫_𝕜
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
x : A
⊢ ∃ u c, x = ∑ i, c i • ↑(u i) ∧ ∀ (i : Fin 4), ‖c i‖ ≤ ‖x‖ / 2

Tactic:
let _ := CStarAlgebra.spectralOrder
  let _ := CStarAlgebra.spectralOrderedRing
  obtain (rfl | hx) := eq_or_ne x 0
  · exact ⟨![1, -1, 1, -1], 0, by simp⟩
  · have := norm_smul_two_inv_smul_add_four_unitary x hx
    extract_lets u₁ u₂ at this
    use ![u₁, star u₁, u₂, star u₂], ![‖x‖ * 2⁻¹, ‖x‖ * 2⁻¹, ‖x‖ * 2⁻¹ * I, ‖x‖ * 2⁻¹ * I]
    constructor
    · conv_lhs => rw [this]
      simp [Fin.sum_univ_four, ← Complex.coe_smul]
      module
    · intro i
      fin_cases i
      all_goals simp [div_eq_mul_inv]

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

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u v : ↥(unitary A)
huv : ‖↑v - ↑u‖ < 2
⊢ expUnitary (↑1 • argSelfAdjoint (v * star u)) * u = v

Tactic:
simp [expUnitary_eq_mul_inv v u huv, mul_assoc]

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

Goal state before:
pp: f : ℝ → ℝ
s : Set ℝ
hs : UniqueDiffOn ℝ s
n : ℕ
x : ℝ
hx : x ∈ s
p : ℝ → FormalMultilinearSeries ℝ ℝ ℝ
hp : HasFTaylorSeriesUpToOn ∞ f p s
hp_nn : ∀ (n : ℕ) ⦃x : ℝ⦄, x ∈ s → 0 ≤ (p x n) fun x ↦ 1
heq : p x n = iteratedFDerivWithin ℝ n f s x
⊢ 0 ≤ iteratedDerivWithin n f s x

Tactic:
iteratedDerivWithin_eq_iteratedFDerivWithin,

Goal state after:
f : ℝ → ℝ
s : Set ℝ
hs : UniqueDiffOn ℝ s
n : ℕ
x : ℝ
hx : x ∈ s
p : ℝ → FormalMultilinearSeries ℝ ℝ ℝ
hp : HasFTaylorSeriesUpToOn ∞ f p s
hp_nn : ∀ (n : ℕ) ⦃x : ℝ⦄, x ∈ s → 0 ≤ (p x n) fun x ↦ 1
heq : p x n = iteratedFDerivWithin ℝ n f s x
⊢ 0 ≤ (iteratedFDerivWithin ℝ n f s x) fun x ↦ 1
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
x : E
y : F
⊢ adjoint (((rankOne 𝕜) x) y) = ((rankOne 𝕜) y) x

Tactic:
by
  simp [rankOne_def', adjoint_comp, ← adjoint_innerSL_apply]

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
inst✝ : CompleteSpace E
⊢ ↑(star T * T) - ↑(T * star T) = ↑0 ↔ ∀ (v : E), ‖↑T v‖ = ‖↑(adjoint T) v‖

Tactic:
toLinearMap_zero

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
inst✝ : CompleteSpace E
⊢ ↑(star T * T) - ↑(T * star T) = 0 ↔ ∀ (v : E), ‖↑T v‖ = ‖↑(adjoint T) v‖
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✝ : CharZero k
s : Simplex k P n
t : Set (Fin (n + 1))
ht : t ≠ Set.univ
⊢ s.centroid ∉ affineSpan k (s.points '' t)

Tactic:
by
  intro h
  have hssubset : t ⊂ Set.univ := by grind
  obtain ⟨i, hi⟩ := Set.exists_of_ssubset hssubset
  rw [s.centroid_eq_affineCombination] at h
  set w := (centroidWeights k (univ : Finset (Fin (n + 1)))) with wdef
  have hw : ∑ i, w i = 1 := by rw [sum_centroidWeights_eq_one_of_nonempty _ _ (by simp)]
  have h1 := AffineIndependent.eq_zero_of_affineCombination_mem_affineSpan s.independent hw h
    (by simp) hi.2
  have h2 : w i = (1 : k) / (n + 1) := by
    simp [wdef, centroidWeights_apply, card_univ, Fintype.card_fin, Nat.cast_add,
      Nat.cast_one]
  simp only [h2, one_div, inv_eq_zero] at h1
  norm_cast at h1

Goal state after:
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✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
⊢ Function.Injective (⇑A ∘ ⇑(adjoint A)) ↔ Function.Injective ⇑(adjoint A)

Tactic:
simpa using A.adjoint.adjoint_comp_self_injective_iff

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
i : Fin (n + 1)
⊢ ((({i}ᶜ.weightedVSubOfPoint s.points (s.points i)) fun x ↦ (↑n)⁻¹) +ᵥ s.points i) -ᵥ s.points i =
    (↑n)⁻¹ • ∑ x, (s.points x -ᵥ s.points i)

Tactic:
simp only [weightedVSubOfPoint_apply, vadd_vsub]
    have h (i : Fin (n + 1)) : ∑ j ∈ {i}ᶜ, (n : k)⁻¹ • (s.points j -ᵥ s.points i) =
      ∑ j : (Fin (n + 1)), ((n : k)⁻¹ • (s.points j -ᵥ s.points i)) := by
      rw [← Finset.sum_compl_add_sum {i}]
      simp
    rw [h i, smul_sum]

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
H : Type u_5
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : CompleteSpace H
K : Type u_6
inst✝² : NormedAddCommGroup K
inst✝¹ : InnerProductSpace 𝕜 K
inst✝ : CompleteSpace K
f g : H ≃ₗᵢ[𝕜] K
⊢ (∀ (a : H →L[𝕜] H), ↑↑g ∘SL a ∘SL ↑↑g.symm = ↑↑f ∘SL a ∘SL ↑↑f.symm) ↔ ∃ α, ∀ (x : H), f x = (α • g) x

Tactic:
← eq_toContinuousLinearMap_symm_comp,

Goal state after:
𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
H : Type u_5
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : CompleteSpace H
K : Type u_6
inst✝² : NormedAddCommGroup K
inst✝¹ : InnerProductSpace 𝕜 K
inst✝ : CompleteSpace K
f g : H ≃ₗᵢ[𝕜] K
⊢ (∀ (a : H →L[𝕜] H), a ∘SL ↑↑g.symm = ↑(↑g).symm ∘SL ↑↑f ∘SL a ∘SL ↑↑f.symm) ↔ ∃ α, ∀ (x : H), f x = (α • g) x
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✝ : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
i₁ : ι
⊢ Set.finrank k (Set.range fun i ↦ p ↑i -ᵥ p i₁) = Fintype.card { x // x ≠ i₁ } ↔
    finrank k ↥(Submodule.span k (Set.range fun i ↦ p ↑i -ᵥ p i₁)) = n

Tactic:
Set.finrank

Goal state after:
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✝ : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
i₁ : ι
⊢ finrank k ↥(Submodule.span k (Set.range fun i ↦ p ↑i -ᵥ p i₁)) = Fintype.card { x // x ≠ i₁ } ↔
    finrank k ↥(Submodule.span k (Set.range fun i ↦ p ↑i -ᵥ p i₁)) = n
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

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
s : Set P
p : P
h : p ∈ affineSpan k s
⊢ Module.rank k ↥(vectorSpan k (insert p s)) ≤ 1 ↔ Module.rank k ↥(vectorSpan k s) ≤ 1

Tactic:
vectorSpan_insert_eq_vectorSpan h

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
s : Set P
p : P
h : p ∈ affineSpan k s
⊢ Module.rank k ↥(vectorSpan k s) ≤ 1 ↔ Module.rank k ↥(vectorSpan k s) ≤ 1
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

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
s : Set P
p : P
h : p ∈ affineSpan k s
⊢ Module.rank k ↥(vectorSpan k (insert p s)) ≤ 2 ↔ Module.rank k ↥(vectorSpan k s) ≤ 2

Tactic:
vectorSpan_insert_eq_vectorSpan h

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
s : Set P
p : P
h : p ∈ affineSpan k s
⊢ Module.rank k ↥(vectorSpan k s) ≤ 2 ↔ Module.rank k ↥(vectorSpan k s) ≤ 2
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 : AffineSubspace k P
p : P
hf : FiniteDimensional k ↥s.direction
p₀ : P
hp₀ : p₀ ∈ ↑s
v : ↥(k ∙ (p -ᵥ p₀))
c : k
hc : c • (p -ᵥ p₀) = ↑v
⊢ ∃ c, c • ⟨p -ᵥ p₀, ⋯⟩ = v

Tactic:
refine ⟨c, ?_⟩

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 : AffineSubspace k P
p : P
hf : FiniteDimensional k ↥s.direction
p₀ : P
hp₀ : p₀ ∈ ↑s
v : ↥(k ∙ (p -ᵥ p₀))
c : k
hc : c • (p -ᵥ p₀) = ↑v
⊢ c • ⟨p -ᵥ p₀, ⋯⟩ = v
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p q : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
I : Type u_5
B : I → Type u_6
inst✝² : (i : I) → NormedRing (B i)
inst✝¹ : ∀ (i : I), NormOneClass (B i)
inst✝ : Nonempty I
⊢ ⨆ i, 1 = 1

Tactic:
ciSup_const

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

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝² : (i : α) → NormedAddCommGroup (E i)
inst✝¹ : DecidableEq α
inst✝ : Fact (1 ≤ p)
hp : p ≠ ∞
f : ↥(lp E p)
hp₀ : 0 < p
hp' : 0 < p.toReal
this :
  ∀ ε > 0,
    ∀ᶠ (x : Finset α) in (SummationFilter.unconditional α).filter,
      dist (∑ b ∈ x, ‖↑f b‖ ^ p.toReal) (‖f‖ ^ p.toReal) < ε
ε : ℝ
hε : ε > 0
⊢ ∀ (x : Finset α),
    dist (∑ b ∈ x, ‖↑f b‖ ^ p.toReal) (‖f‖ ^ p.toReal) < ε ^ p.toReal → dist (∑ b ∈ x, lp.single p b (↑f b)) f < ε

Tactic:
intro s

Goal state after:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝² : (i : α) → NormedAddCommGroup (E i)
inst✝¹ : DecidableEq α
inst✝ : Fact (1 ≤ p)
hp : p ≠ ∞
f : ↥(lp E p)
hp₀ : 0 < p
hp' : 0 < p.toReal
this :
  ∀ ε > 0,
    ∀ᶠ (x : Finset α) in (SummationFilter.unconditional α).filter,
      dist (∑ b ∈ x, ‖↑f b‖ ^ p.toReal) (‖f‖ ^ p.toReal) < ε
ε : ℝ
hε : ε > 0
s : Finset α
⊢ dist (∑ b ∈ s, ‖↑f b‖ ^ p.toReal) (‖f‖ ^ p.toReal) < ε ^ p.toReal → dist (∑ b ∈ s, lp.single p b (↑f b)) f < ε
Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition

Goal state before:
pp: h✝ : AnalyticAt ℝ expNegInvGlue 0
r : ℝ
hr : 0 < r
h : AnalyticOnNhd ℝ expNegInvGlue (Metric.ball 0 r)
this : expNegInvGlue (r / 2) = 0
⊢ False

Tactic:
by simpa [hr, not_le_of_gt]

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace 𝕜 E
bound : α → ℝ
F : 𝕜 → α → E
x₀ : 𝕜
s : Set 𝕜
F' : α → E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
h_lipsch : ∀ᵐ (a : α) ∂μ, LipschitzOnWith (Real.nnabs (bound a)) (fun x ↦ F x a) s
bound_integrable : Integrable bound μ
L : E →L[𝕜] 𝕜 →L[𝕜] E := (ContinuousLinearMap.smulRightL 𝕜 𝕜 E) 1
h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt (fun x ↦ F x a) (L (F' a)) x₀
hm : AEStronglyMeasurable (⇑L ∘ F') μ
hF'_int : Integrable (⇑L ∘ F') μ
key : HasFDerivAt (fun x ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), (⇑L ∘ F') a ∂μ) x₀
⊢ Integrable F' μ ∧ HasDerivAt (fun x ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀

Tactic:
replace hF'_int : Integrable F' μ := by
    rw [← integrable_norm_iff hm] at hF'_int
    simpa [L, (· ∘ ·), integrable_norm_iff hF'_meas] using! hF'_int

Goal state after:
α : Type u_1
inst✝⁴ : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace 𝕜 E
bound : α → ℝ
F : 𝕜 → α → E
x₀ : 𝕜
s : Set 𝕜
F' : α → E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
h_lipsch : ∀ᵐ (a : α) ∂μ, LipschitzOnWith (Real.nnabs (bound a)) (fun x ↦ F x a) s
bound_integrable : Integrable bound μ
L : E →L[𝕜] 𝕜 →L[𝕜] E := (ContinuousLinearMap.smulRightL 𝕜 𝕜 E) 1
h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt (fun x ↦ F x a) (L (F' a)) x₀
hm : AEStronglyMeasurable (⇑L ∘ F') μ
key : HasFDerivAt (fun x ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), (⇑L ∘ F') a ∂μ) x₀
hF'_int : Integrable F' μ
⊢ Integrable F' μ ∧ HasDerivAt (fun x ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀
Module: Mathlib.MeasureTheory.Measure.EverywherePos

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : OpensMeasurableSpace α
inst✝ : μ.InnerRegular
hs : MeasurableSet s
x : α
hx : x ∈ μ.everywherePosSubset s
n : Set α
hn : n ∈ 𝓝[μ.everywherePosSubset s] x
u : Set α
u_mem : u ∈ 𝓝 x
hu : u ∩ μ.everywherePosSubset s ⊆ n
this : u ∩ s ∈ 𝓝[s] x
⊢ 0 < μ (u ∩ s)

Tactic:
exact hx.2 _ this

Goal state after:
Module: Mathlib.MeasureTheory.Measure.EverywherePos

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : OpensMeasurableSpace α
inst✝ : μ.InnerRegularCompactLTTop
hs : MeasurableSet s
h's : μ s ≠ ∞
x : α
hx : x ∈ μ.everywherePosSubset s
n : Set α
hn : n ∈ 𝓝[μ.everywherePosSubset s] x
u : Set α
u_mem : u ∈ 𝓝 x
hu : u ∩ μ.everywherePosSubset s ⊆ n
this : u ∩ s ∈ 𝓝[s] x
⊢ 0 < μ (u ∩ s)

Tactic:
exact hx.2 _ this

Goal state after:
Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
n : ℕ∞
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : s.Nonempty
ι : Type (max 0 u_1) := { f // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
⊢ ∃ T, T.Countable ∧ ⋃ f ∈ T, support ↑f = s

Tactic:
by
    have : ⋃ f : ι, (f : E → ℝ).support = s := by
      refine Subset.antisymm (iUnion_subset fun f => f.2.1) ?_
      intro x hx
      rcases exists_contDiff_tsupport_subset (hs.mem_nhds hx) with ⟨f, hf⟩
      let g : ι := ⟨f, (subset_tsupport f).trans hf.1, hf.2.1, hf.2.2.1, hf.2.2.2.1⟩
      have : x ∈ support (g : E → ℝ) := by
        simp only [g, hf.2.2.2.2, mem_support, Ne, one_ne_zero, not_false_iff]
      exact mem_iUnion_of_mem _ this
    simp_rw [← this]
    apply isOpen_iUnion_countable
    rintro ⟨f, hf⟩
    exact hf.2.2.1.continuous.isOpen_support

Goal state after: