mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: J : Type u
inst✝ : Category.{v_1, u} J
F : J ⥤ Type v
i j k : J
s : Set (F.obj i)
X✝ Y✝ : J
g : X✝ ⟶ Y✝
x : (fun X ↦ X) (F.obj X✝)
h : ∀ (i_1 : X✝ ⟶ i), x ∈ ⇑(ConcreteCategory.hom (F.map i_1)) ⁻¹' s
f : Y✝ ⟶ i
⊢ (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (F.map g)) x) ∈ s ↔
    x ∈ ⇑(ConcreteCategory.hom (F.map g ≫ F.map f)) ⁻¹' s

Tactic:
;

Goal state after:
J : Type u
inst✝ : Category.{v_1, u} J
F : J ⥤ Type v
i j k : J
s : Set (F.obj i)
X✝ Y✝ : J
g : X✝ ⟶ Y✝
x : (fun X ↦ X) (F.obj X✝)
h : ∀ (i_1 : X✝ ⟶ i), x ∈ ⇑(ConcreteCategory.hom (F.map i_1)) ⁻¹' s
f : Y✝ ⟶ i
⊢ (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (F.map g)) x) ∈ s ↔
    x ∈ ⇑(ConcreteCategory.hom (F.map g ≫ F.map f)) ⁻¹' s
Module: Mathlib.Analysis.Convex.Approximation

Goal state before:
pp: case refine_1
𝕜 : Type u_1
E : Type u_2
φ : E → ℝ
inst✝⁸ : RCLike 𝕜
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : Module 𝕜 E
inst✝³ : IsScalarTower ℝ 𝕜 E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
𝓕 : Set ({ x // x ∈ univ } → ℝ) := {f | f ≤ φ ∘ Subtype.val ∧ ∃ l c, f = (⇑re ∘ ⇑l) ∘ Subtype.val + const (↑univ) c}
this : sSup {f | f ≤ φ ∘ Subtype.val ∧ ∃ l c, f = (⇑re ∘ ⇑l) ∘ Subtype.val + const (↑univ) c} = φ ∘ Subtype.val
f : E → ℝ
x✝ : f ≤ φ ∧ ∃ l c, f = ⇑re ∘ ⇑l + const E c
hp : f ≤ φ
l : E →L[𝕜] 𝕜
c : ℝ
hlc : f = ⇑re ∘ ⇑l + const E c
x : ↑univ
⊢ (f ∘ Subtype.val) x = ((⇑re ∘ ⇑l) ∘ Subtype.val + const (↑univ) c) x

Tactic:
;

Goal state after:
case refine_1
𝕜 : Type u_1
E : Type u_2
φ : E → ℝ
inst✝⁸ : RCLike 𝕜
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : Module 𝕜 E
inst✝³ : IsScalarTower ℝ 𝕜 E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
𝓕 : Set ({ x // x ∈ univ } → ℝ) := {f | f ≤ φ ∘ Subtype.val ∧ ∃ l c, f = (⇑re ∘ ⇑l) ∘ Subtype.val + const (↑univ) c}
this : sSup {f | f ≤ φ ∘ Subtype.val ∧ ∃ l c, f = (⇑re ∘ ⇑l) ∘ Subtype.val + const (↑univ) c} = φ ∘ Subtype.val
f : E → ℝ
x✝ : f ≤ φ ∧ ∃ l c, f = ⇑re ∘ ⇑l + const E c
hp : f ≤ φ
l : E →L[𝕜] 𝕜
c : ℝ
hlc : f = ⇑re ∘ ⇑l + const E c
x : ↑univ
⊢ (f ∘ Subtype.val) x = ((⇑re ∘ ⇑l) ∘ Subtype.val + const (↑univ) c) x
Module: Mathlib.Analysis.Convex.Approximation

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u_2
φ : E → ℝ
inst✝⁸ : RCLike 𝕜
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : Module 𝕜 E
inst✝³ : IsScalarTower ℝ 𝕜 E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
𝓕 : Set ({ x // x ∈ univ } → ℝ) := {f | f ≤ φ ∘ Subtype.val ∧ ∃ l c, f = (⇑re ∘ ⇑l) ∘ Subtype.val + const (↑univ) c}
this : sSup {f | f ≤ φ ∘ Subtype.val ∧ ∃ l c, f = (⇑re ∘ ⇑l) ∘ Subtype.val + const (↑univ) c} = φ ∘ Subtype.val
f : E → ℝ
x✝¹ : f ≤ φ ∧ ∃ l c, f = ⇑re ∘ ⇑l + const E c
hp : f ≤ φ
l : E →L[𝕜] 𝕜
c : ℝ
hlc : f = ⇑re ∘ ⇑l + const E c
x✝ : E
⊢ (fun g ↦ g ∘ ⇑(Equiv.Set.univ E).symm) (f ∘ Subtype.val) x✝ = f x✝

Tactic:
;

Goal state after:
case refine_2
𝕜 : Type u_1
E : Type u_2
φ : E → ℝ
inst✝⁸ : RCLike 𝕜
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : Module 𝕜 E
inst✝³ : IsScalarTower ℝ 𝕜 E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
𝓕 : Set ({ x // x ∈ univ } → ℝ) := {f | f ≤ φ ∘ Subtype.val ∧ ∃ l c, f = (⇑re ∘ ⇑l) ∘ Subtype.val + const (↑univ) c}
this : sSup {f | f ≤ φ ∘ Subtype.val ∧ ∃ l c, f = (⇑re ∘ ⇑l) ∘ Subtype.val + const (↑univ) c} = φ ∘ Subtype.val
f : E → ℝ
x✝¹ : f ≤ φ ∧ ∃ l c, f = ⇑re ∘ ⇑l + const E c
hp : f ≤ φ
l : E →L[𝕜] 𝕜
c : ℝ
hlc : f = ⇑re ∘ ⇑l + const E c
x✝ : E
⊢ (fun g ↦ g ∘ ⇑(Equiv.Set.univ E).symm) (f ∘ Subtype.val) x✝ = f x✝
Module: Mathlib.Analysis.Convex.Approximation

Goal state before:
pp: case refine_4
𝕜 : Type u_1
E : Type u_2
φ : E → ℝ
inst✝⁸ : RCLike 𝕜
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : Module 𝕜 E
inst✝³ : IsScalarTower ℝ 𝕜 E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
𝓕 : Set ({ x // x ∈ univ } → ℝ) := {f | f ≤ φ ∘ Subtype.val ∧ ∃ l c, f = (⇑re ∘ ⇑l) ∘ Subtype.val + const (↑univ) c}
this : sSup {f | f ≤ φ ∘ Subtype.val ∧ ∃ l c, f = (⇑re ∘ ⇑l) ∘ Subtype.val + const (↑univ) c} = φ ∘ Subtype.val
f : E → ℝ
x✝ : ∃ a ∈ 𝓕, (fun g ↦ g ∘ ⇑(Equiv.Set.univ E).symm) a = f
l : E →L[𝕜] 𝕜
c : ℝ
h : (⇑re ∘ ⇑l) ∘ Subtype.val + const (↑univ) c ≤ φ ∘ Subtype.val
hb : (fun g ↦ g ∘ ⇑(Equiv.Set.univ E).symm) ((⇑re ∘ ⇑l) ∘ Subtype.val + const (↑univ) c) = f
⊢ f = ⇑re ∘ ⇑l + const E c

Tactic:
;

Goal state after:
case refine_4
𝕜 : Type u_1
E : Type u_2
φ : E → ℝ
inst✝⁸ : RCLike 𝕜
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : Module 𝕜 E
inst✝³ : IsScalarTower ℝ 𝕜 E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
𝓕 : Set ({ x // x ∈ univ } → ℝ) := {f | f ≤ φ ∘ Subtype.val ∧ ∃ l c, f = (⇑re ∘ ⇑l) ∘ Subtype.val + const (↑univ) c}
this : sSup {f | f ≤ φ ∘ Subtype.val ∧ ∃ l c, f = (⇑re ∘ ⇑l) ∘ Subtype.val + const (↑univ) c} = φ ∘ Subtype.val
f : E → ℝ
x✝ : ∃ a ∈ 𝓕, (fun g ↦ g ∘ ⇑(Equiv.Set.univ E).symm) a = f
l : E →L[𝕜] 𝕜
c : ℝ
h : (⇑re ∘ ⇑l) ∘ Subtype.val + const (↑univ) c ≤ φ ∘ Subtype.val
hb : (fun g ↦ g ∘ ⇑(Equiv.Set.univ E).symm) ((⇑re ∘ ⇑l) ∘ Subtype.val + const (↑univ) c) = f
⊢ f = ⇑re ∘ ⇑l + const E c
Module: Mathlib.Analysis.Convex.Approximation

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
φ : E → ℝ
inst✝⁸ : RCLike 𝕜
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : Module 𝕜 E
inst✝³ : IsScalarTower ℝ 𝕜 E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
𝓕 : Set ({ x // x ∈ univ } → ℝ) := {f | f ≤ φ ∘ Subtype.val ∧ ∃ l c, f = (⇑re ∘ ⇑l) ∘ Subtype.val + const (↑univ) c}
this : sSup {f | f ≤ φ ∘ Subtype.val ∧ ∃ l c, f = (⇑re ∘ ⇑l) ∘ Subtype.val + const (↑univ) c} = φ ∘ Subtype.val
x : E
⊢ sSup ((fun g ↦ g ∘ ⇑(Equiv.Set.univ E).symm) '' 𝓕) x = (sSup 𝓕 ∘ ⇑(Equiv.Set.univ E).symm) x

Tactic:
;

Goal state after:
𝕜 : Type u_1
E : Type u_2
φ : E → ℝ
inst✝⁸ : RCLike 𝕜
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : Module 𝕜 E
inst✝³ : IsScalarTower ℝ 𝕜 E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
𝓕 : Set ({ x // x ∈ univ } → ℝ) := {f | f ≤ φ ∘ Subtype.val ∧ ∃ l c, f = (⇑re ∘ ⇑l) ∘ Subtype.val + const (↑univ) c}
this : sSup {f | f ≤ φ ∘ Subtype.val ∧ ∃ l c, f = (⇑re ∘ ⇑l) ∘ Subtype.val + const (↑univ) c} = φ ∘ Subtype.val
x : E
⊢ sSup ((fun g ↦ g ∘ ⇑(Equiv.Set.univ E).symm) '' 𝓕) x = (sSup 𝓕 ∘ ⇑(Equiv.Set.univ E).symm) x
Module: Mathlib.Analysis.Convex.Approximation

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
φ : E → ℝ
inst✝⁸ : RCLike 𝕜
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : Module 𝕜 E
inst✝³ : IsScalarTower ℝ 𝕜 E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
𝓕 : Set ({ x // x ∈ univ } → ℝ) := {f | f ≤ φ ∘ Subtype.val ∧ ∃ l c, f = (⇑re ∘ ⇑l) ∘ Subtype.val + const (↑univ) c}
this : sSup {f | f ≤ φ ∘ Subtype.val ∧ ∃ l c, f = (⇑re ∘ ⇑l) ∘ Subtype.val + const (↑univ) c} = φ ∘ Subtype.val
x : E
⊢ (⨆ a, ↑a ∘ ⇑(Equiv.Set.univ E).symm) x = ((⨆ a, ↑a) ∘ ⇑(Equiv.Set.univ E).symm) x

Tactic:
;

Goal state after:
𝕜 : Type u_1
E : Type u_2
φ : E → ℝ
inst✝⁸ : RCLike 𝕜
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : Module 𝕜 E
inst✝³ : IsScalarTower ℝ 𝕜 E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
𝓕 : Set ({ x // x ∈ univ } → ℝ) := {f | f ≤ φ ∘ Subtype.val ∧ ∃ l c, f = (⇑re ∘ ⇑l) ∘ Subtype.val + const (↑univ) c}
this : sSup {f | f ≤ φ ∘ Subtype.val ∧ ∃ l c, f = (⇑re ∘ ⇑l) ∘ Subtype.val + const (↑univ) c} = φ ∘ Subtype.val
x : E
⊢ (⨆ a, ↑a ∘ ⇑(Equiv.Set.univ E).symm) x = ((⨆ a, ↑a) ∘ ⇑(Equiv.Set.univ E).symm) x
Module: Mathlib.Analysis.Convex.Approximation

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
φ : E → ℝ
inst✝⁸ : RCLike 𝕜
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : Module 𝕜 E
inst✝³ : IsScalarTower ℝ 𝕜 E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
𝓕 : Set ({ x // x ∈ univ } → ℝ) := {f | f ≤ φ ∘ Subtype.val ∧ ∃ l c, f = (⇑re ∘ ⇑l) ∘ Subtype.val + const (↑univ) c}
this : sSup {f | f ≤ φ ∘ Subtype.val ∧ ∃ l c, f = (⇑re ∘ ⇑l) ∘ Subtype.val + const (↑univ) c} = φ ∘ Subtype.val
x✝ : E
⊢ (φ ∘ Subtype.val ∘ ⇑(Equiv.Set.univ E).symm) x✝ = φ x✝

Tactic:
;

Goal state after:
𝕜 : Type u_1
E : Type u_2
φ : E → ℝ
inst✝⁸ : RCLike 𝕜
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : Module 𝕜 E
inst✝³ : IsScalarTower ℝ 𝕜 E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
𝓕 : Set ({ x // x ∈ univ } → ℝ) := {f | f ≤ φ ∘ Subtype.val ∧ ∃ l c, f = (⇑re ∘ ⇑l) ∘ Subtype.val + const (↑univ) c}
this : sSup {f | f ≤ φ ∘ Subtype.val ∧ ∃ l c, f = (⇑re ∘ ⇑l) ∘ Subtype.val + const (↑univ) c} = φ ∘ Subtype.val
x✝ : E
⊢ (φ ∘ Subtype.val ∘ ⇑(Equiv.Set.univ E).symm) x✝ = φ x✝
Module: Mathlib.Analysis.Convex.Approximation

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
φ : E → ℝ
inst✝⁹ : RCLike 𝕜
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℝ E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : HereditarilyLindelofSpace E
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
𝓕 : Set (E → ℝ) := {f | f ≤ φ ∧ ∃ l c, f = ⇑re ∘ ⇑l + const E c}
hl : IsLUB 𝓕 φ
f : E → ℝ
hf : f ∈ 𝓕
l : E →L[𝕜] 𝕜
c : ℝ
hlc : f = ⇑re ∘ ⇑l + const E c
⊢ Continuous (⇑re ∘ ⇑l + const E c)

Tactic:
;

Goal state after:
𝕜 : Type u_1
E : Type u_2
φ : E → ℝ
inst✝⁹ : RCLike 𝕜
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℝ E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : HereditarilyLindelofSpace E
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
𝓕 : Set (E → ℝ) := {f | f ≤ φ ∧ ∃ l c, f = ⇑re ∘ ⇑l + const E c}
hl : IsLUB 𝓕 φ
f : E → ℝ
hf : f ∈ 𝓕
l : E →L[𝕜] 𝕜
c : ℝ
hlc : f = ⇑re ∘ ⇑l + const E c
⊢ Continuous (⇑re ∘ ⇑l + const E c)
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
δ : Type x
f₁ : α → Option β
f₂ : β → Option α
hf : ∀ (a : α) (b : β), f₂ b = some a ↔ f₁ a = some b
g₂ : β → Option α
hg : ∀ (a : α) (b : β), g₂ b = some a ↔ f₁ a = some b
⊢ { toFun := f₁, invFun := f₂, inv := hf } = { toFun := f₁, invFun := g₂, inv := hg }

Tactic:
congr with y x

Goal state after:
case e_invFun
α : Type u
β : Type v
γ : Type w
δ : Type x
f₁ : α → Option β
f₂ : β → Option α
hf : ∀ (a : α) (b : β), f₂ b = some a ↔ f₁ a = some b
g₂ : β → Option α
hg : ∀ (a : α) (b : β), g₂ b = some a ↔ f₁ a = some b
y : β
x : α
⊢ f₂ y = some x ↔ g₂ y = some x
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
f : α ≃. β
x✝ : α
a✝ : β
⊢ ((PEquiv.refl α).trans f) x✝ = some a✝ ↔ f x✝ = some a✝

Tactic:
;

Goal state after:
α : Type u
β : Type v
f : α ≃. β
x✝ : α
a✝ : β
⊢ ((PEquiv.refl α).trans f) x✝ = some a✝ ↔ f x✝ = some a✝
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
f : α ≃. β
x✝ : α
a✝ : β
⊢ { toFun := fun a ↦ f a, invFun := fun a ↦ (f.symm a).bind ⇑(PEquiv.refl α), inv := ⋯ } x✝ = some a✝ ↔ f x✝ = some a✝

Tactic:
;

Goal state after:
α : Type u
β : Type v
f : α ≃. β
x✝ : α
a✝ : β
⊢ { toFun := fun a ↦ f a, invFun := fun a ↦ (f.symm a).bind ⇑(PEquiv.refl α), inv := ⋯ } x✝ = some a✝ ↔ f x✝ = some a✝
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
f : α ≃. β
x✝ : α
a✝ : β
⊢ (f.trans (PEquiv.refl β)) x✝ = some a✝ ↔ f x✝ = some a✝

Tactic:
;

Goal state after:
α : Type u
β : Type v
f : α ≃. β
x✝ : α
a✝ : β
⊢ (f.trans (PEquiv.refl β)) x✝ = some a✝ ↔ f x✝ = some a✝
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
f : α ≃. β
x✝ : α
a✝ : β
⊢ (f x✝).bind ⇑(PEquiv.refl β) = some a✝ ↔ f x✝ = some a✝

Tactic:
;

Goal state after:
α : Type u
β : Type v
f : α ≃. β
x✝ : α
a✝ : β
⊢ (f x✝).bind ⇑(PEquiv.refl β) = some a✝ ↔ f x✝ = some a✝
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
f : α ≃. β
a₁ a₂ : α
b : β
h₁ : a₁ ∈ f.symm b
h₂ : a₂ ∈ f.symm b
⊢ a₁ = a₂

Tactic:
;

Goal state after:
α : Type u
β : Type v
f : α ≃. β
a₁ a₂ : α
b : β
h₁ : a₁ ∈ f.symm b
h₂ : a₂ ∈ f.symm b
⊢ a₁ = a₂
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
a : α
⊢ (a ∈ if a ∈ s then some a else none) ↔ a ∈ s

Tactic:
;

Goal state after:
α : Type u
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
a : α
⊢ (a ∈ if a ∈ s then some a else none) ↔ a ∈ s
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
f : α ≃. β
⊢ (∀ (x : α), x ∈ {a | (f a).isSome = true}) ↔ ∀ (a : α), (f a).isSome = true

Tactic:
;

Goal state after:
α : Type u
β : Type v
f : α ≃. β
⊢ (∀ (x : α), x ∈ {a | (f a).isSome = true}) ↔ ∀ (a : α), (f a).isSome = true
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α ≃. β
x✝ : α
a✝ : γ
⊢ (f.trans ⊥) x✝ = some a✝ ↔ ⊥ x✝ = some a✝

Tactic:
;

Goal state after:
α : Type u
β : Type v
γ : Type w
f : α ≃. β
x✝ : α
a✝ : γ
⊢ (f.trans ⊥) x✝ = some a✝ ↔ ⊥ x✝ = some a✝
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α ≃. β
x✝ : α
a✝ : γ
⊢ { toFun := fun a ↦ (f a).bind ⇑⊥, invFun := fun a ↦ none, inv := ⋯ } x✝ = some a✝ ↔ none = some a✝

Tactic:
;

Goal state after:
α : Type u
β : Type v
γ : Type w
f : α ≃. β
x✝ : α
a✝ : γ
⊢ { toFun := fun a ↦ (f a).bind ⇑⊥, invFun := fun a ↦ none, inv := ⋯ } x✝ = some a✝ ↔ none = some a✝
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : β ≃. γ
x✝ : α
a✝ : γ
⊢ (⊥.trans f) x✝ = some a✝ ↔ ⊥ x✝ = some a✝

Tactic:
;

Goal state after:
α : Type u
β : Type v
γ : Type w
f : β ≃. γ
x✝ : α
a✝ : γ
⊢ (⊥.trans f) x✝ = some a✝ ↔ ⊥ x✝ = some a✝
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : β ≃. γ
x✝ : α
a✝ : γ
⊢ { toFun := fun a ↦ none, invFun := fun a ↦ (f.symm a).bind ⇑⊥, inv := ⋯ } x✝ = some a✝ ↔ none = some a✝

Tactic:
;

Goal state after:
α : Type u
β : Type v
γ : Type w
f : β ≃. γ
x✝ : α
a✝ : γ
⊢ { toFun := fun a ↦ none, invFun := fun a ↦ (f.symm a).bind ⇑⊥, inv := ⋯ } x✝ = some a✝ ↔ none = some a✝
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a₁ a₂ : α
b₁ b₂ : β
⊢ (b₁ ∈ if a₁ = a₂ then some b₂ else none) ↔ a₁ = a₂ ∧ b₁ = b₂

Tactic:
;

Goal state after:
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a₁ a₂ : α
b₁ b₂ : β
⊢ (b₁ ∈ if a₁ = a₂ then some b₂ else none) ↔ a₁ = a₂ ∧ b₁ = b₂
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x✝³ x✝² : α ≃. β
x✝¹ : α
x✝ : β
⊢ (if x✝³ x✝¹ = x✝² x✝¹ then x✝³ x✝¹ else none) = some x✝ → x✝³ x✝¹ = some x✝

Tactic:
;

Goal state after:
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x✝³ x✝² : α ≃. β
x✝¹ : α
x✝ : β
⊢ (if x✝³ x✝¹ = x✝² x✝¹ then x✝³ x✝¹ else none) = some x✝ → x✝³ x✝¹ = some x✝
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x✝³ x✝² : α ≃. β
x✝¹ : α
x✝ : β
⊢ (if x✝³ x✝¹ = x✝² x✝¹ then x✝³ x✝¹ else none) = some x✝ → x✝² x✝¹ = some x✝

Tactic:
;

Goal state after:
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x✝³ x✝² : α ≃. β
x✝¹ : α
x✝ : β
⊢ (if x✝³ x✝¹ = x✝² x✝¹ then x✝³ x✝¹ else none) = some x✝ → x✝² x✝¹ = some x✝
Module: Mathlib.LinearAlgebra.Matrix.Permutation

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝² : DecidableEq n
σ τ : Perm n
inst✝¹ : Fintype n
inst✝ : NonAssocSemiring R
⊢ (toPEquiv (σ * τ)).toMatrix = Perm.permMatrix R τ * Perm.permMatrix R σ

Tactic:
Perm.mul_def,

Goal state after:
n : Type u_1
R : Type u_2
inst✝² : DecidableEq n
σ τ : Perm n
inst✝¹ : Fintype n
inst✝ : NonAssocSemiring R
⊢ (Equiv.trans τ σ).toPEquiv.toMatrix = Perm.permMatrix R τ * Perm.permMatrix R σ
Module: Mathlib.Data.Matrix.PEquiv

Goal state before:
pp: case h.none.none
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
f g : m ≃. n
i : m
hi : ¬none = none
hf : f i = none
hg : g i = none
⊢ ∃ x, ¬(if x ∈ none then 1 else 0) = if x ∈ none then 1 else 0

Tactic:
;

Goal state after:
case h.none.none
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
f g : m ≃. n
i : m
hi : ¬none = none
hf : f i = none
hg : g i = none
⊢ ∃ x, ¬(if x ∈ none then 1 else 0) = if x ∈ none then 1 else 0
Module: Mathlib.Analysis.Convex.Caratheodory

Goal state before:
pp: 𝕜 : Type u_1
E : Type u
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ y ∈ t, 0 ≤ f y
fsum : ∑ y ∈ t, f y = 1
g : E → 𝕜
gcombo : ∑ e ∈ t, g e • e = 0
gsum : ∑ e ∈ t, g e = 0
gpos : ∃ i ∈ t, 0 < g i
s : Finset E := {z ∈ t | 0 < g z}
i₀ : E
mem : i₀ ∈ s
w : ∀ i ∈ s, f i₀ / g i₀ ≤ f i / g i
hg : 0 < g i₀
hi₀ : i₀ ∈ t
k : E → 𝕜 := fun z ↦ f z - f i₀ / g i₀ * g z
hk : k i₀ = 0
ksum : ∑ e ∈ t.erase i₀, k e = 1
e : E
a✝ : ¬e = i₀
het : e ∈ t
hes : e ∉ s
⊢ f i₀ / g i₀ * g e ≤ 0

Tactic:
by
          apply mul_nonpos_of_nonneg_of_nonpos
          · apply div_nonneg (fpos i₀ (mem_of_subset (filter_subset _ t) mem)) (le_of_lt hg)
          · simpa only [s, mem_filter, het, true_and, not_lt] using hes

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

Goal state before:
pp: case hbc
V : Type u_1
inst✝² : SeminormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : ∀ (ε : ℝ), 0 < ε → ∃ N, ∀ (n : ℕ), N ≤ n → ‖↑(u n) - ↑0‖ < ε
C : ℝ
hC_pos : C > 0
hC_bdd : ∀ x ∈ ↑K, ‖x‖ ≤ C
ε : ℝ
hε : 0 < ε
n : ℕ
hn : |↑(u n)| * C < ε
y : V
hyK : y ∈ ↑K
h : (1 + ↑(u n)) • y ∈ ⋂ n, (1 + ↑(u n)) • ↑K
⊢ ‖y‖ ≤ C

Tactic:
;

Goal state after:
case hbc
V : Type u_1
inst✝² : SeminormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : ∀ (ε : ℝ), 0 < ε → ∃ N, ∀ (n : ℕ), N ≤ n → ‖↑(u n) - ↑0‖ < ε
C : ℝ
hC_pos : C > 0
hC_bdd : ∀ x ∈ ↑K, ‖x‖ ≤ C
ε : ℝ
hε : 0 < ε
n : ℕ
hn : |↑(u n)| * C < ε
y : V
hyK : y ∈ ↑K
h : (1 + ↑(u n)) • y ∈ ⋂ n, (1 + ↑(u n)) • ↑K
⊢ ‖y‖ ≤ C
Module: Mathlib.Analysis.Convex.Cone.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁹ : AddCommMonoid E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : Semifield 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderTopology 𝕜
inst✝² : DenselyOrdered 𝕜
inst✝¹ : NoMaxOrder 𝕜
inst✝ : ContinuousSMul 𝕜 E
C : ConvexCone 𝕜 E
hSclos : IsClosed ↑C
x : E
hx : x ∈ ↑C
f : 𝕜 → E := fun x_1 ↦ x_1 • x
w✝ : 𝕜
h : w✝ ∈ Ioi 0
⊢ f w✝ ∈ ↑C

Tactic:
;

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝⁹ : AddCommMonoid E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : Semifield 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderTopology 𝕜
inst✝² : DenselyOrdered 𝕜
inst✝¹ : NoMaxOrder 𝕜
inst✝ : ContinuousSMul 𝕜 E
C : ConvexCone 𝕜 E
hSclos : IsClosed ↑C
x : E
hx : x ∈ ↑C
f : 𝕜 → E := fun x_1 ↦ x_1 • x
w✝ : 𝕜
h : w✝ ∈ Ioi 0
⊢ f w✝ ∈ ↑C
Module: Mathlib.Analysis.Convex.Caratheodory

Goal state before:
pp: case h₂.convert_5
𝕜 : Type u_1
E : Type u
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
⊢ ∀ (i : Finset E), ⋃ (_ : ↑i ⊆ s), ⋃ (_ : AffineIndependent 𝕜 Subtype.val), (convexHull 𝕜) ↑i ⊆ (convexHull 𝕜) s

Tactic:
;

Goal state after:
case h₂.convert_5
𝕜 : Type u_1
E : Type u
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
⊢ ∀ (i : Finset E), ⋃ (_ : ↑i ⊆ s), ⋃ (_ : AffineIndependent 𝕜 Subtype.val), (convexHull 𝕜) ↑i ⊆ (convexHull 𝕜) s
Module: Mathlib.Analysis.Convex.Caratheodory

Goal state before:
pp: case h₂.convert_5.convert_5
𝕜 : Type u_1
E : Type u
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
i✝ : Finset E
⊢ ↑i✝ ⊆ s → ⋃ (_ : AffineIndependent 𝕜 Subtype.val), (convexHull 𝕜) ↑i✝ ⊆ (convexHull 𝕜) s

Tactic:
;

Goal state after:
case h₂.convert_5.convert_5
𝕜 : Type u_1
E : Type u
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
i✝ : Finset E
⊢ ↑i✝ ⊆ s → ⋃ (_ : AffineIndependent 𝕜 Subtype.val), (convexHull 𝕜) ↑i✝ ⊆ (convexHull 𝕜) s
Module: Mathlib.Analysis.Convex.Caratheodory

Goal state before:
pp: case h₂.convert_5.convert_5.convert_5
𝕜 : Type u_1
E : Type u
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
i✝¹ : Finset E
i✝ : ↑i✝¹ ⊆ s
⊢ AffineIndependent 𝕜 Subtype.val → (convexHull 𝕜) ↑i✝¹ ⊆ (convexHull 𝕜) s

Tactic:
;

Goal state after:
case h₂.convert_5.convert_5.convert_5
𝕜 : Type u_1
E : Type u
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
i✝¹ : Finset E
i✝ : ↑i✝¹ ⊆ s
⊢ AffineIndependent 𝕜 Subtype.val → (convexHull 𝕜) ↑i✝¹ ⊆ (convexHull 𝕜) s
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
s : AffineSubspace R P
hx : x ∈ s
hy : (lineMap x z) 0 ∈ s
hxy : x ≠ (lineMap x z) 0
⊢ False

Tactic:
;

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
s : AffineSubspace R P
hx : x ∈ s
hy : (lineMap x z) 0 ∈ s
hxy : x ≠ (lineMap x z) 0
⊢ False
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: case pos
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x : P
v : V
r₁ r₂ : R
hr₁ : 0 ≤ r₁
hr₂ : r₁ ≤ r₂
h : r₁ = 0
⊢ (lineMap x (r₂ • v +ᵥ x)) (r₁ / r₂) = r₁ • v +ᵥ x

pp: case neg
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x : P
v : V
r₁ r₂ : R
hr₁ : 0 ≤ r₁
hr₂ : r₁ ≤ r₂
h : ¬r₁ = 0
⊢ (lineMap x (r₂ • v +ᵥ x)) (r₁ / r₂) = r₁ • v +ᵥ x

Tactic:
;

Goal state after:
case pos
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x : P
v : V
r₁ r₂ : R
hr₁ : 0 ≤ r₁
hr₂ : r₁ ≤ r₂
h : r₁ = 0
⊢ (lineMap x (r₂ • v +ᵥ x)) (r₁ / r₂) = r₁ • v +ᵥ x

case neg
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x : P
v : V
r₁ r₂ : R
hr₁ : 0 ≤ r₁
hr₂ : r₁ ≤ r₂
h : ¬r₁ = 0
⊢ (lineMap x (r₂ • v +ᵥ x)) (r₁ / r₂) = r₁ • v +ᵥ x