mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.AffineSpace.Restrict

Goal state before:
pp: case refine_1
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : AddCommGroup V₂
inst✝⁵ : Module k V₁
inst✝⁴ : Module k V₂
inst✝³ : AddTorsor V₁ P₁
inst✝² : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst✝¹ : Nonempty ↥E
inst✝ : Nonempty ↥F
hEF : AffineSubspace.map φ E ≤ F
⊢ ↥E → ↥F

pp: case refine_2
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : AddCommGroup V₂
inst✝⁵ : Module k V₁
inst✝⁴ : Module k V₂
inst✝³ : AddTorsor V₁ P₁
inst✝² : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst✝¹ : Nonempty ↥E
inst✝ : Nonempty ↥F
hEF : AffineSubspace.map φ E ≤ F
⊢ ↥E.direction →ₗ[k] ↥F.direction

pp: case refine_3
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : AddCommGroup V₂
inst✝⁵ : Module k V₁
inst✝⁴ : Module k V₂
inst✝³ : AddTorsor V₁ P₁
inst✝² : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst✝¹ : Nonempty ↥E
inst✝ : Nonempty ↥F
hEF : AffineSubspace.map φ E ≤ F
⊢ ∀ (p : ↥E) (v : ↥E.direction), ?refine_1 (v +ᵥ p) = ?refine_2 v +ᵥ ?refine_1 p

Tactic:
· exact fun x => ⟨φ x, hEF <| AffineSubspace.mem_map.mpr ⟨x, x.property, rfl⟩⟩

Goal state after:
case refine_2
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : AddCommGroup V₂
inst✝⁵ : Module k V₁
inst✝⁴ : Module k V₂
inst✝³ : AddTorsor V₁ P₁
inst✝² : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst✝¹ : Nonempty ↥E
inst✝ : Nonempty ↥F
hEF : AffineSubspace.map φ E ≤ F
⊢ ↥E.direction →ₗ[k] ↥F.direction

case refine_3
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : AddCommGroup V₂
inst✝⁵ : Module k V₁
inst✝⁴ : Module k V₂
inst✝³ : AddTorsor V₁ P₁
inst✝² : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst✝¹ : Nonempty ↥E
inst✝ : Nonempty ↥F
hEF : AffineSubspace.map φ E ≤ F
⊢ ∀ (p : ↥E) (v : ↥E.direction), ⟨φ ↑(v +ᵥ p), ⋯⟩ = ?refine_2 v +ᵥ ⟨φ ↑p, ⋯⟩
Module: Mathlib.Analysis.Convex.StdSimplex

Goal state before:
pp: case refine_1
R : Type u_1
ι : Type u_2
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ (range fun i j ↦ if i = j then 1 else 0) ⊆ stdSimplex R ι

Tactic:
rintro _ ⟨i, rfl⟩
    exact ite_eq_mem_stdSimplex R i

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Torsor

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : Group V
inst✝³ : TopologicalSpace V
inst✝² : Torsor V P
inst✝¹ : TopologicalSpace P
inst✝ : IsTopologicalTorsor P
p : P
v : V
⊢ v⁻¹ = (p /ₛ p) / v

Tactic:
sdiv_self,

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁴ : Group V
inst✝³ : TopologicalSpace V
inst✝² : Torsor V P
inst✝¹ : TopologicalSpace P
inst✝ : IsTopologicalTorsor P
p : P
v : V
⊢ v⁻¹ = 1 / v
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : PartialOrder k
inst✝ : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
⊢ s.interior ⊂ s.closedInterior

Tactic:
rw [Set.ssubset_iff_exists]
  exact ⟨s.interior_subset_closedInterior, s.points 0, s.point_mem_closedInterior 0,
    s.point_notMem_interior 0⟩

Goal state after:
Module: Mathlib.Topology.Algebra.Affine

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace V
inst✝⁵ : AddTorsor V P
inst✝⁴ : TopologicalSpace P
inst✝³ : IsTopologicalAddTorsor P
inst✝² : Field R
inst✝¹ : Module R V
inst✝ : ContinuousConstSMul R V
x : P
t : R
ht : t ≠ 0
⊢ IsOpenMap ⇑(homothety x t)

Tactic:
by
  apply IsOpenMap.of_inverse (homothety_continuous x t⁻¹) <;> intro e <;>
    simp [← AffineMap.comp_apply, ← homothety_mul, ht]

Goal state after:
Module: Mathlib.Topology.AlexandrovDiscrete

Goal state before:
pp: ι : Sort u_1
κ : ι → Sort u_2
α : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : IndiscreteTopology α
⊢ ∀ (S : Set (Set α)), (∀ s ∈ S, IsOpen[inst✝²] s) → IsOpen[inst✝²] (⋂₀ S)

Tactic:
grind [isOpen_iff]

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

Goal state before:
pp: case inr
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
h : AffineIndependent k fun p ↦ ↑p
p₁ : P
hp₁ : p₁ ∈ s
⊢ ∃ t, s ⊆ t ∧ (AffineIndependent k fun p ↦ ↑p) ∧ affineSpan k t = ⊤

Tactic:
· rw [affineIndependent_set_iff_linearIndependent_vsub k hp₁] at h
    let bsv := Basis.extend h
    have hsvi := bsv.linearIndependent
    have hsvt := bsv.span_eq
    rw [Basis.coe_extend] at hsvi hsvt
    rw [linearIndependent_subtype_iff] at hsvi h
    have hsv := h.subset_extend (Set.subset_univ _)
    have h0 : ∀ v : V, v ∈ h.extend (Set.subset_univ _) → v ≠ 0 := by
      intro v hv
      simpa [bsv] using bsv.ne_zero ⟨v, hv⟩
    rw [← linearIndependent_subtype_iff,
      linearIndependent_set_iff_affineIndependent_vadd_union_singleton k h0 p₁] at hsvi
    refine ⟨{p₁} ∪ (fun v => v +ᵥ p₁) '' h.extend (Set.subset_univ _), ?_, ?_⟩
    · refine Set.Subset.trans ?_ (Set.union_subset_union_right _ (Set.image_mono hsv))
      simp [Set.image_image]
    · use hsvi
      exact affineSpan_singleton_union_vadd_eq_top_of_span_eq_top p₁ hsvt

Goal state after:
Module: Mathlib.Topology.AlexandrovDiscrete

Goal state before:
pp: α : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : AlexandrovDiscrete α
β : Type u_5
f : α → β
S : Set (Set β)
hS : ∀ s ∈ S, IsOpen[coinduced f inst✝¹] s
⊢ IsOpen[inst✝¹] (⋂ t ∈ S, f ⁻¹' t)

Tactic:
exact isOpen_iInter₂ hS

Goal state after:
Module: Mathlib.Topology.AlexandrovDiscrete

Goal state before:
pp: ι : Sort u_1
κ : ι → Sort u_2
α : Type u_3
β : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : AlexandrovDiscrete α
inst✝ : AlexandrovDiscrete β
s t : Set α
a : α
⊢ AlexandrovDiscrete (α × β)

Tactic:
by
  simp_rw [alexandrovDiscrete_iff_nhds, Prod.forall, nhds_prod_eq, ← principal_nhdsKer_singleton,
    prod_principal_principal, nhdsKer_pair, forall_true_iff]

Goal state after:
Module: Mathlib.Analysis.Convex.Topology

Goal state before:
pp: case mp
𝕜 : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
x : 𝕜
hx : x ∈ s
y : 𝕜
hy : y ∈ s
h : x ≠ y
hs' : (Ioo (min x y) (max x y)).Nonempty → (interior s).Nonempty
⊢ (interior s).Nonempty

Tactic:
nonempty_Ioo,

Goal state after:
case mp
𝕜 : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
x : 𝕜
hx : x ∈ s
y : 𝕜
hy : y ∈ s
h : x ≠ y
hs' : min x y < max x y → (interior s).Nonempty
⊢ (interior s).Nonempty
Module: Mathlib.Analysis.Convex.Topology

Goal state before:
pp: case mp
𝕜 : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
x : 𝕜
hx : x ∈ s
y : 𝕜
hy : y ∈ s
h : x ≠ y
hs' : x ≠ y → (interior s).Nonempty
⊢ (interior s).Nonempty

Tactic:
exact hs' h

Goal state after:
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: case inr.refine_2
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x y✝ z : X
ι : Type u_3
F : Set X
inst✝¹ : LocallyPathConnectedSpace X
inst✝ : LocallyPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
y : Y
hxu : inr y ∈ u
⊢ IsOpen[instTopologicalSpaceSum] (inr '' pathComponentIn (inr ⁻¹' u) y)

pp: case inr.refine_3
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x y✝ z : X
ι : Type u_3
F : Set X
inst✝¹ : LocallyPathConnectedSpace X
inst✝ : LocallyPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
y : Y
hxu : inr y ∈ u
⊢ inr y ∈ inr '' pathComponentIn (inr ⁻¹' u) y

Tactic:
· exact isOpenMap_inr _ <| (hu.preimage continuous_inr).pathComponentIn _

Goal state after:
case inr.refine_3
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x y✝ z : X
ι : Type u_3
F : Set X
inst✝¹ : LocallyPathConnectedSpace X
inst✝ : LocallyPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
y : Y
hxu : inr y ∈ u
⊢ inr y ∈ inr '' pathComponentIn (inr ⁻¹' u) y
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

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 : AffineSubspace k P
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∉ s
⊢ AffineIndependent k ((fun x ↦ ![p₁, p₂, p₃] ↑x) ∘ ⇑(finSuccAboveEquiv 2))

Tactic:
convert! affineIndependent_of_ne k hp₁p₂

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 : AffineSubspace k P
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∉ s
⊢ (fun x ↦ ![p₁, p₂, p₃] ↑x) ∘ ⇑(finSuccAboveEquiv 2) = ![p₁, p₂]
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring k
inst✝⁴ : LinearOrder k
inst✝³ : IsStrictOrderedRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
h : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
hw : ∑ i ∈ s, w i = 1
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
i j : ι
hi : i ∈ s
hj : j ∈ s
hi0 : w₁ i = 0
hj0 : w₁ j = 0
hij : SignType.sign (w₂ i) = SignType.sign (w₂ j)
r : k
hr : ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i
⊢ SignType.sign (w i) = SignType.sign (w j)

Tactic:
rw [hr i hi, hr j hj, hi0, hj0, add_zero, add_zero, sub_zero, sub_zero, sign_mul, sign_mul, hij]

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

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring k
inst✝⁴ : LinearOrder k
inst✝³ : IsStrictOrderedRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
h : AffineIndependent k p
w : ι → k
s : Finset ι
hw : ∑ i ∈ s, w i = 1
i₁ i₂ i₃ : ι
h₁ : i₁ ∈ s
h₂ : i₂ ∈ s
h₃ : i₃ ∈ s
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
c : k
hc0 : 0 < c
hc1 : c < 1
hs :
  (affineCombination k s p) w ∈ line[k, (affineCombination k s p) (Pi.single i₁ 1), (AffineMap.lineMap (p i₂) (p i₃)) c]
⊢ SignType.sign (w i₂) = SignType.sign (w i₃)

Tactic:
←
      s.affineCombination_affineCombinationLineMapWeights p h₂ h₃ c

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring k
inst✝⁴ : LinearOrder k
inst✝³ : IsStrictOrderedRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
h : AffineIndependent k p
w : ι → k
s : Finset ι
hw : ∑ i ∈ s, w i = 1
i₁ i₂ i₃ : ι
h₁ : i₁ ∈ s
h₂ : i₂ ∈ s
h₃ : i₃ ∈ s
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
c : k
hc0 : 0 < c
hc1 : c < 1
hs :
  (affineCombination k s p) w ∈
    line[k, (affineCombination k s p) (Pi.single i₁ 1),
      (affineCombination k s p) (affineCombinationLineMapWeights i₂ i₃ c)]
⊢ SignType.sign (w i₂) = SignType.sign (w i₃)
Module: Mathlib.Analysis.Normed.Module.Convex

Goal state before:
pp: case top
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : E
⊢ Convex ℝ (eball a ⊤)

Tactic:
| top =>

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Convex

Goal state before:
pp: case top
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : E
⊢ Convex ℝ (closedEBall a ⊤)

Tactic:
| top =>

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
t : TopologicalSpace E
inst✝ : IsTopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
h : WithSeminorms p
⊢ 𝓝 0 = p.moduleFilterBasis.filter

Tactic:
exact AddGroupFilterBasis.nhds_zero_eq _

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: case refine_3.refine_2.inl
𝕜 : Type u_2
E : Type u_6
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : p.ball 0 1 ∈ 𝓝 0
h' : IsVonNBounded 𝕜 (p.ball 0 1)
s : Set E
hs : s ∈ (SeminormFamily.moduleFilterBasis fun x ↦ p).filter
t : Set E
ht : t ∈ (SeminormFamily.moduleFilterBasis fun x ↦ p).toFilterBasis
ts : t ⊆ s
r : ℝ
r_pos : 0 < r
hw : t = (∅.sup fun x ↦ p).ball 0 r
⊢ t ∈ 𝓝 0

Tactic:
simp only [ball, Finset.sup_empty, sub_zero, coe_bot, Pi.zero_apply, r_pos, ofPred_true] at hw
      simp [hw]

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.NNNorm

Goal state before:
pp: case h₁
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : DenselyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
hbdd : ∀ y ∈ (fun x ↦ ‖f x‖₊) '' closedBall 0 1, y ≤ ‖f‖₊
⊢ BddAbove ((fun x ↦ ‖f x‖₊) '' closedBall 0 1)

pp: case h
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : DenselyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
hbdd : ∀ y ∈ (fun x ↦ ‖f x‖₊) '' closedBall 0 1, y ≤ ‖f‖₊
⊢ ball 0 1 ⊆ closedBall 0 1

Tactic:
exacts [⟨‖f‖₊, hbdd⟩, ball_subset_closedBall]

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Bilinear

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
Eₗ : Type u_5
F : Type u_6
Fₗ : Type u_7
G : Type u_8
Gₗ : Type u_9
𝓕 : Type u_10
inst✝¹⁸ : SeminormedAddCommGroup E
inst✝¹⁷ : SeminormedAddCommGroup Eₗ
inst✝¹⁶ : SeminormedAddCommGroup F
inst✝¹⁵ : SeminormedAddCommGroup Fₗ
inst✝¹⁴ : SeminormedAddCommGroup G
inst✝¹³ : SeminormedAddCommGroup Gₗ
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : NontriviallyNormedField 𝕜₂
inst✝¹⁰ : NontriviallyNormedField 𝕜₃
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 Eₗ
inst✝⁷ : NormedSpace 𝕜₂ F
inst✝⁶ : NormedSpace 𝕜 Fₗ
inst✝⁵ : NormedSpace 𝕜₃ G
inst✝⁴ : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝² : FunLike 𝓕 E F
inst✝¹ : RingHomIsometric σ₂₃
inst✝ : RingHomIsometric σ₁₃
f : E →SL[σ₁₃] F →SL[σ₂₃] G
y : F
x : E
⊢ ‖f‖ * ‖x‖ * ‖y‖ = ‖f‖ * ‖y‖ * ‖x‖

Tactic:
simp only [mul_right_comm]

Goal state after:
Module: Mathlib.Probability.ConditionalProbability

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s : Set Ω
hcs : μ s ≠ 0
hs : μ s ≠ ∞
⊢ (μ s)⁻¹ * μ s = 1

Tactic:
exact ENNReal.inv_mul_cancel hcs hs

Goal state after:
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: case mp
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
⊢ (∃ b, ∀ᶠ (a : ι) in f, ↑(u a) ≥ b) → ∃ x, ∃ (_ : 0 ≤ x), ∀ᶠ (a : ι) in f, x ≤ ↑(u a)

pp: case mpr
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
⊢ (∃ x, ∃ (_ : 0 ≤ x), ∀ᶠ (a : ι) in f, x ≤ ↑(u a)) → ∃ b, ∀ᶠ (a : ι) in f, ↑(u a) ≥ b

Tactic:
· rintro ⟨b, hb⟩
    exact ⟨b.toNNReal, by simp, by simpa⟩

Goal state after:
case mpr
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
⊢ (∃ x, ∃ (_ : 0 ≤ x), ∀ᶠ (a : ι) in f, x ≤ ↑(u a)) → ∃ b, ∀ᶠ (a : ι) in f, ↑(u a) ≥ b
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝² : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ✝ : (i : ι) → Measure (α i)
δ : Type u_4
X : δ → Type u_5
inst✝ : (i : δ) → MeasurableSpace (X i)
l : List δ
μ : (i : δ) → Measure (X i)
⊢ Measure (TProd X l)

Tactic:
induction l with
  | nil => exact dirac PUnit.unit
  | cons i l ih => exact (μ i).prod (α := X i) ih

Goal state after:
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace β
b : β
⊢ ∃ b', ↑(const α b) = fun x ↦ b'

Tactic:
simp only [cast]
  split_ifs with h
  case neg => exact h.elim ⟨b, rfl⟩
  exact ⟨Classical.choose h, by ext; simp⟩

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Indicator

Goal state before:
pp: α : Type u_1
ε : Type u_2
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
s : Set α
f : α → ε
a : α
⊢ ‖s.indicator f a‖ₑ ≤ ‖f a‖ₑ

Tactic:
enorm_indicator_eq_indicator_enorm

Goal state after:
α : Type u_1
ε : Type u_2
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
s : Set α
f : α → ε
a : α
⊢ s.indicator (fun a ↦ ‖f a‖ₑ) a ≤ ‖f a‖ₑ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator

Goal state before:
pp: case neg.e_a.e_f
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
s : Set α
hs : MeasurableSet s
hp_zero : ¬p = 0
hp_top : ¬p = ∞
⊢ (fun x ↦ ‖s.indicator f x‖ₑ ^ p.toReal) = fun a ↦ s.indicator (fun x ↦ ‖f x‖ₑ ^ p.toReal) a

Tactic:
enorm_indicator_eq_indicator_enorm

Goal state after:
case neg.e_a.e_f
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
s : Set α
hs : MeasurableSet s
hp_zero : ¬p = 0
hp_top : ¬p = ∞
⊢ (fun x ↦ s.indicator (fun a ↦ ‖f a‖ₑ) x ^ p.toReal) = fun a ↦ s.indicator (fun x ↦ ‖f x‖ₑ ^ p.toReal) a
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
s : Set α
f : α → ε
⊢ ∀ (x : α), ‖s.indicator f x‖ₑ ≤ ‖f x‖ₑ

Tactic:
enorm_indicator_eq_indicator_enorm

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
s : Set α
f : α → ε
⊢ ∀ (x : α), s.indicator (fun a ↦ ‖f a‖ₑ) x ≤ ‖f x‖ₑ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
s : Set α
f : α → ε
x : α
⊢ ‖s.indicator f x‖ₑ ≤ ‖f x‖ₑ

Tactic:
enorm_indicator_eq_indicator_enorm

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
s : Set α
f : α → ε
x : α
⊢ s.indicator (fun a ↦ ‖f a‖ₑ) x ≤ ‖f x‖ₑ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity

Goal state before:
pp: case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst✝³ : TopologicalSpace ε'
inst✝² : ContinuousENorm ε'
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
hp : 0 < p
hp' : ¬p < 0
hc : c = ∞
hg' : eLpNorm' g p μ = 0
this : ∀ᵐ (x : α) ∂μ, ‖g x‖ₑ = 0
⊢ eLpNorm' f p μ ≤ c * eLpNorm' g p μ

Tactic:
have : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ = 0 := (this.and h).mono fun x ⟨h, h'⟩ ↦ by simp_all

Goal state after:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst✝³ : TopologicalSpace ε'
inst✝² : ContinuousENorm ε'
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
hp : 0 < p
hp' : ¬p < 0
hc : c = ∞
hg' : eLpNorm' g p μ = 0
this✝ : ∀ᵐ (x : α) ∂μ, ‖g x‖ₑ = 0
this : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ = 0
⊢ eLpNorm' f p μ ≤ c * eLpNorm' g p μ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
s : Set α
β : Type u_9
inst✝ : NormedAddCommGroup β
μ : Measure α
hp : p ≠ ∞
hs : MeasurableSet s
c : ℝ
hc : 0 ≤ c
f g : α → β
h : ∀ (x : α), dist (f x) (g x) ≤ c
hs₁ : Function.support f ⊆ s
hs₂ : Function.support g ⊆ s
⊢ s.indicator (f - g) = f - g

Tactic:
Set.indicator_eq_self

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
s : Set α
β : Type u_9
inst✝ : NormedAddCommGroup β
μ : Measure α
hp : p ≠ ∞
hs : MeasurableSet s
c : ℝ
hc : 0 ≤ c
f g : α → β
h : ∀ (x : α), dist (f x) (g x) ≤ c
hs₁ : Function.support f ⊆ s
hs₂ : Function.support g ⊆ s
⊢ Function.support (f - g) ⊆ s
Module: Mathlib.Data.ENNReal.Holder

Goal state before:
pp: p q r : ℝ≥0∞
inst✝ : p.HolderTriple q r
hq : q ≠ 0
⊢ r⁻¹ - q⁻¹ = p⁻¹

Tactic:
obtain (rfl | hr) := eq_zero_or_pos r

Goal state after:
case inl
p q : ℝ≥0∞
hq : q ≠ 0
inst✝ : p.HolderTriple q 0
⊢ 0⁻¹ - q⁻¹ = p⁻¹

case inr
p q r : ℝ≥0∞
inst✝ : p.HolderTriple q r
hq : q ≠ 0
hr : 0 < r
⊢ r⁻¹ - q⁻¹ = p⁻¹
Module: Mathlib.Data.ENNReal.Holder

Goal state before:
pp: case mpr
p : ℝ≥0∞
inst✝ : p.HolderConjugate 1
⊢ p = ∞

Tactic:
← inv_inv p,

Goal state after:
case mpr
p : ℝ≥0∞
inst✝ : p.HolderConjugate 1
⊢ p⁻¹⁻¹ = ∞
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: case left
q r : ℝ≥0
hr : r ≠ 0
h : (↑0).HolderTriple ↑q ↑r
⊢ False

Tactic:
apply hr

Goal state after:
case left
q r : ℝ≥0
hr : r ≠ 0
h : (↑0).HolderTriple ↑q ↑r
⊢ r = 0
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: case right
p r : ℝ≥0
hr : r ≠ 0
h : (↑p).HolderTriple ↑0 ↑r
⊢ False

Tactic:
apply hr

Goal state after:
case right
p r : ℝ≥0
hr : r ≠ 0
h : (↑p).HolderTriple ↑0 ↑r
⊢ r = 0
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
c : ℝ≥0∞
μ μ' : Measure α
h : μ' ≤ c • μ
f : α → ε
p : ℝ≥0∞
⊢ eLpNorm f p (c • μ) ≤ c ^ (1 / p).toReal • eLpNorm f p μ

Tactic:
eLpNorm_smul_measure_le

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
c : ℝ≥0∞
μ μ' : Measure α
h : μ' ≤ c • μ
f : α → ε
p : ℝ≥0∞
⊢ c ^ (1 / p).toReal • eLpNorm f p μ ≤ c ^ (1 / p).toReal • eLpNorm f p μ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
β : Type u_8
mβ : MeasurableSpace β
f : α → β
g : β → ε
hf : MeasurableEmbedding f
⊢ AEStronglyMeasurable g (Measure.map f μ) ∧ eLpNorm g p (Measure.map f μ) < ∞ ↔
    AEStronglyMeasurable (g ∘ f) μ ∧ eLpNorm (g ∘ f) p μ < ∞

Tactic:
hf.aestronglyMeasurable_map_iff,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
β : Type u_8
mβ : MeasurableSpace β
f : α → β
g : β → ε
hf : MeasurableEmbedding f
⊢ AEStronglyMeasurable (g ∘ f) μ ∧ eLpNorm g p (Measure.map f μ) < ∞ ↔
    AEStronglyMeasurable (g ∘ f) μ ∧ eLpNorm (g ∘ f) p μ < ∞
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
hp0 : ¬p.toReal = 0
h : p = 0
⊢ False

Tactic:
simp [h] at hp0

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
hp0 : ¬p.toReal = 0
hp : p ≠ 0
h : p = ∞
⊢ False

Tactic:
simp [h] at hp0

Goal state after: