mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Monotone.Union

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s
B : ∀ x ∈ s ∪ t, c ≤ x → x ∈ t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
hxy : x < y
hxc : x < c
⊢ f x < f y

pp: case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s
B : ∀ x ∈ s ∪ t, c ≤ x → x ∈ t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
hxy : x < y
hcx : c ≤ x
⊢ f x < f y

Tactic:
· have xs : x ∈ s := A _ hx hxc.le
    rcases lt_or_ge y c with (hyc | hcy)
    · exact h₁ xs (A _ hy hyc.le) hxy
    · exact (h₁ xs hs.1 hxc).trans_le (h₂.monotoneOn ht.1 (B _ hy hcy) hcy)

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s
B : ∀ x ∈ s ∪ t, c ≤ x → x ∈ t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
hxy : x < y
hcx : c ≤ x
⊢ f x < f y
Module: Mathlib.Analysis.Complex.Tietze

Goal state before:
pp: case pos
𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type w
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
this✝¹ : NormedSpace ℝ E
this✝ : IsScalarTower ℝ 𝕜 E
g : E → E := fun x ↦ ‖x‖⁻¹ • x
this : Continuous ((Metric.closedBall 0 1).piecewise id g)
x : E
hx : x ∈ Metric.closedBall 0 1
⊢ (Metric.closedBall 0 1).piecewise id g x ∈ Metric.closedBall 0 1

Tactic:
simpa [piecewise_eq_of_mem (hi := hx)] using hx

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: case h.«0».«0»
R : Type u_1
inst✝¹ : CommRing R
m : Matrix (Fin 2) (Fin 2) R
inst✝ : IsReduced R
hm : m 1 0 = 0
aux : m.discr = 0 ↔ m 0 0 = m 1 1
h : m 0 0 = m 1 1
h' : m 0 1 = 0
⊢ (scalar (Fin 2)) (m 1 1) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = m ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
simp [h, h', hm]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: case h.«0».«1»
R : Type u_1
inst✝¹ : CommRing R
m : Matrix (Fin 2) (Fin 2) R
inst✝ : IsReduced R
hm : m 1 0 = 0
aux : m.discr = 0 ↔ m 0 0 = m 1 1
h : m 0 0 = m 1 1
h' : m 0 1 = 0
⊢ (scalar (Fin 2)) (m 1 1) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = m ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
simp [h, h', hm]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: case h.«1».«0»
R : Type u_1
inst✝¹ : CommRing R
m : Matrix (Fin 2) (Fin 2) R
inst✝ : IsReduced R
hm : m 1 0 = 0
aux : m.discr = 0 ↔ m 0 0 = m 1 1
h : m 0 0 = m 1 1
h' : m 0 1 = 0
⊢ (scalar (Fin 2)) (m 1 1) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = m ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
simp [h, h', hm]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: case h.«1».«1»
R : Type u_1
inst✝¹ : CommRing R
m : Matrix (Fin 2) (Fin 2) R
inst✝ : IsReduced R
hm : m 1 0 = 0
aux : m.discr = 0 ↔ m 0 0 = m 1 1
h : m 0 0 = m 1 1
h' : m 0 1 = 0
⊢ (scalar (Fin 2)) (m 1 1) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = m ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
simp [h, h', hm]

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: g : GL (Fin 2) ℝ
z : ℍ
⊢ -g • z = g • z

Tactic:
ext1

Goal state after:
g : GL (Fin 2) ℝ
z : ℍ
⊢ ↑(-g • z) = ↑(g • z)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: a b : ℝ
ha : a ≠ 0
hc : ↑⟨!![a, b; 0, a⁻¹], ⋯⟩ 1 0 = 0
z : ℂ
hz : 0 < z.im
⊢ ⟨!![a, b; 0, a⁻¹], ⋯⟩ • { coe := z, coe_im_pos := hz } =
    ((fun x ↦ b * a +ᵥ x) ∘ fun x ↦ ⟨a * a, ⋯⟩ • x) { coe := z, coe_im_pos := hz }

Tactic:
ext1

Goal state after:
a b : ℝ
ha : a ≠ 0
hc : ↑⟨!![a, b; 0, a⁻¹], ⋯⟩ 1 0 = 0
z : ℂ
hz : 0 < z.im
⊢ ↑(⟨!![a, b; 0, a⁻¹], ⋯⟩ • { coe := z, coe_im_pos := hz }) =
    ↑(((fun x ↦ b * a +ᵥ x) ∘ fun x ↦ ⟨a * a, ⋯⟩ • x) { coe := z, coe_im_pos := hz })
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: case h
a b c d : ℝ
h : a * d - b * c = 1
h_denom : ∀ (z : ℍ), denom (toGL ⟨!![a, b; c, d], ⋯⟩) ↑z ≠ 0
hc : c ≠ 0
z : ℂ
hz : 0 < z.im
⊢ ⟨!![a, b; c, d], ⋯⟩ • { coe := z, coe_im_pos := hz } =
    ((fun x ↦ a / c +ᵥ x) ∘ (fun x ↦ ModularGroup.S • x) ∘ (fun x ↦ c * d +ᵥ x) ∘ fun x ↦ ⟨c * c, ⋯⟩ • x)
      { coe := z, coe_im_pos := hz }

Tactic:
ext1

Goal state after:
case h
a b c d : ℝ
h : a * d - b * c = 1
h_denom : ∀ (z : ℍ), denom (toGL ⟨!![a, b; c, d], ⋯⟩) ↑z ≠ 0
hc : c ≠ 0
z : ℂ
hz : 0 < z.im
⊢ ↑(⟨!![a, b; c, d], ⋯⟩ • { coe := z, coe_im_pos := hz }) =
    ↑(((fun x ↦ a / c +ᵥ x) ∘ (fun x ↦ ModularGroup.S • x) ∘ (fun x ↦ c * d +ᵥ x) ∘ fun x ↦ ⟨c * c, ⋯⟩ • x)
        { coe := z, coe_im_pos := hz })
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: case zero
n : Type u_4
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
R : Type u_1
S : Type u_2
m : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
inst✝ : Fintype m
f : S →+* Matrix n n R
l : IsEmpty m
⊢ (f 1).det = 1

Tactic:
map_one,

Goal state after:
case zero
n : Type u_4
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
R : Type u_1
S : Type u_2
m : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
inst✝ : Fintype m
f : S →+* Matrix n n R
l : IsEmpty m
⊢ det 1 = 1
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: case inl.inr
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Free R S
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : Module S A
inst✝¹ : IsScalarTower R S A
inst✝ : Module.Free S A
f : A →ₗ[S] A
a✝¹ : Nontrivial R
a✝ : Nontrivial A
this✝¹ : Nontrivial S
ιS : Type u_2
bS : Module.Basis ιS R S
ιA : Type u_3
bA : Module.Basis ιA S A
this✝ : Nonempty ιS
this : Nonempty ιA
val✝¹ : Fintype ιS
val✝ : Infinite ιA
⊢ LinearMap.det (↑R f) = (Algebra.norm R) 1

Tactic:
map_one,

Goal state after:
case inl.inr
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Free R S
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : Module S A
inst✝¹ : IsScalarTower R S A
inst✝ : Module.Free S A
f : A →ₗ[S] A
a✝¹ : Nontrivial R
a✝ : Nontrivial A
this✝¹ : Nontrivial S
ιS : Type u_2
bS : Module.Basis ιS R S
ιA : Type u_3
bA : Module.Basis ιA S A
this✝ : Nonempty ιS
this : Nonempty ιA
val✝¹ : Fintype ιS
val✝ : Infinite ιA
⊢ LinearMap.det (↑R f) = 1
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: case pos
R : Type u_1
inst✝⁶ : CommRing R
L : Type u_6
K : Type u_7
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Algebra R L
inst✝¹ : Algebra R K
inst✝ : IsScalarTower R K L
x : L
hx : IsIntegral R x
h : FiniteDimensional K L
F : IntermediateField K L := K⟮x⟯
⊢ IsIntegral R ((norm K) x)

Tactic:
rw [← norm_norm (S := F), ← coe_gen K x, ← IntermediateField.algebraMap_apply,
    norm_algebraMap_of_basis (Module.Free.chooseBasis F L) (gen K x), map_pow]

Goal state after:
case pos
R : Type u_1
inst✝⁶ : CommRing R
L : Type u_6
K : Type u_7
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Algebra R L
inst✝¹ : Algebra R K
inst✝ : IsScalarTower R K L
x : L
hx : IsIntegral R x
h : FiniteDimensional K L
F : IntermediateField K L := K⟮x⟯
⊢ IsIntegral R ((norm K) (gen K x) ^ Fintype.card (Free.ChooseBasisIndex (↥F) L))
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: case pos
L : Type u_6
K : Type u_7
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
h : FiniteDimensional K L
F : IntermediateField K L := K⟮x⟯
⊢ (norm K) x = (norm K) (gen K x) ^ finrank (↥K⟮x⟯) L

Tactic:
← coe_gen K x

Goal state after:
case pos
L : Type u_6
K : Type u_7
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
h : FiniteDimensional K L
F : IntermediateField K L := K⟮x⟯
⊢ (norm K) ↑(gen K x) = (norm K) (gen K x) ^ finrank (↥K⟮x⟯) L
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
β : Type v
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
g₁ g₂ : PreStoneCech α → β
h₁ : Continuous[_, inst✝¹] g₁
h₂ : Continuous[_, inst✝¹] g₂
h : g₁ ∘ preStoneCechUnit = g₂ ∘ preStoneCechUnit
⊢ g₁ = g₂

Tactic:
by
  apply Continuous.ext_on denseRange_preStoneCechUnit h₁ h₂
  rintro x ⟨x, rfl⟩
  apply congr_fun h x

Goal state after:
Module: Mathlib.Topology.Category.CompHaus.Basic

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCat := F ⋙ compHausToTop
⊢ {u | ∀ {i j : J} (f : i ⟶ j), (ConcreteCategory.hom (F.map f)) (u i) = u j} =
    ⋂ i, ⋂ j, ⋂ f, {u | (ConcreteCategory.hom (F.map f)) (u i) = u j}

Tactic:
ext1

Goal state after:
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCat := F ⋙ compHausToTop
x✝ : (j : J) → ↑(F.obj j).toTop
⊢ x✝ ∈ {u | ∀ {i j : J} (f : i ⟶ j), (ConcreteCategory.hom (F.map f)) (u i) = u j} ↔
    x✝ ∈ ⋂ i, ⋂ j, ⋂ f, {u | (ConcreteCategory.hom (F.map f)) (u i) = u j}
Module: Mathlib.Topology.Algebra.ProperAction.Basic

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
h_proper : ProperSMul G X
inst✝ : T1Space G
f : X → G × X := fun x ↦ (1, x)
proper_f : IsProperMap f
⊢ IsClosed[instTopologicalSpaceProd] (diagonal X)

Tactic:
let g := fun gx : G × X ↦ (gx.1 • gx.2, gx.2)

Goal state after:
G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
h_proper : ProperSMul G X
inst✝ : T1Space G
f : X → G × X := fun x ↦ (1, x)
proper_f : IsProperMap f
g : G × X → X × X := fun gx ↦ (gx.1 • gx.2, gx.2)
⊢ IsClosed[instTopologicalSpaceProd] (diagonal X)
Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace

Goal state before:
pp: X : Type w
tX : TopologicalSpace X
inst✝ : UCompactlyGeneratedSpace X
s : Set X
hs : ∀ (S : CompHaus) (f : C(↑S.toTop, X)), IsClosed (⇑f ⁻¹' s)
⊢ IsClosed[compactlyGenerated X] s

Tactic:
TopologicalSpace.compactlyGenerated,

Goal state after:
X : Type w
tX : TopologicalSpace X
inst✝ : UCompactlyGeneratedSpace X
s : Set X
hs : ∀ (S : CompHaus) (f : C(↑S.toTop, X)), IsClosed (⇑f ⁻¹' s)
⊢ IsClosed[coinduced
        (fun x ↦
          match x with
          | ⟨⟨fst, i⟩, s⟩ => i s)
        inferInstance]
    s
Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace

Goal state before:
pp: X : Type w
tX : TopologicalSpace X
inst✝ : UCompactlyGeneratedSpace X
s : Set X
hs : ∀ (S : CompHaus) (f : C(↑S.toTop, X)), IsOpen (⇑f ⁻¹' s)
⊢ IsOpen[compactlyGenerated X] s

Tactic:
TopologicalSpace.compactlyGenerated,

Goal state after:
X : Type w
tX : TopologicalSpace X
inst✝ : UCompactlyGeneratedSpace X
s : Set X
hs : ∀ (S : CompHaus) (f : C(↑S.toTop, X)), IsOpen (⇑f ⁻¹' s)
⊢ IsOpen[coinduced
        (fun x ↦
          match x with
          | ⟨⟨fst, i⟩, s⟩ => i s)
        inferInstance]
    s
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
s : Set (OnePoint X)
inst✝ : T0Space X
x y : OnePoint X
hxy : Inseparable x y
⊢ x = y

Tactic:
rcases inseparable_iff.1 hxy with (⟨rfl, rfl⟩ | ⟨x, rfl, y, rfl, h⟩)

Goal state after:
case inl
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
s : Set (OnePoint X)
inst✝ : T0Space X
hxy : Inseparable ∞ ∞
⊢ ∞ = ∞

case inr
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
s : Set (OnePoint X)
inst✝ : T0Space X
x y : X
h : Inseparable x y
hxy : Inseparable ↑x ↑y
⊢ ↑x = ↑y
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: f : ℂ → ℂ
h₁f : Meromorphic f
⊢ proximity f ⊤ - proximity f⁻¹ ⊤ = circleAverage (fun x ↦ log ‖f x‖) 0

Tactic:
ext R

Goal state after:
f : ℂ → ℂ
h₁f : Meromorphic f
R : ℝ
⊢ (proximity f ⊤ - proximity f⁻¹ ⊤) R = circleAverage (fun x ↦ log ‖f x‖) 0 R
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
h : Meromorphic f
μ : Measure ℝ := volume.restrict (Ioc 0 (2 * π))
h_meas_K : Measurable fun a ↦ (cartanKernel f R a.1 a.2)⁺
h_int_posLog : Integrable (fun β ↦ log⁺ ‖f (circleMap 0 R β)‖) μ
h_int_Bound : Integrable (fun β ↦ log⁺ ‖f (circleMap 0 R β)‖ + log 2) μ
β : ℝ
h_int_nonneg : 0 ≤ ∫ (α : ℝ), (cartanKernel f R α β)⁺ ∂μ
⊢ 0 ≤ 2 * π * (log⁺ ‖f (circleMap 0 R β)‖ + log 2)

Tactic:
positivity [posLog_nonneg (x := ‖f (circleMap 0 R β)‖)]

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

Goal state before:
pp: f : ℂ → ℂ
h : Meromorphic f
⊢ (fun R ↦ circleAverage (fun a ↦ circleAverage (fun x ↦ log ‖f x - a‖) 0 R) 0 1) = proximity f ⊤

Tactic:
ext R

Goal state after:
f : ℂ → ℂ
h : Meromorphic f
R : ℝ
⊢ circleAverage (fun a ↦ circleAverage (fun x ↦ log ‖f x - a‖) 0 R) 0 1 = proximity f ⊤ R
Module: Mathlib.Data.List.Triplewise

Goal state before:
pp: α : Type u_1
β : Type u_2
l : List α
p : α → α → α → Prop
f : α → β
p' : β → β → β → Prop
h : ∀ {a b c : α}, p' (f a) (f b) (f c) → p a b c
hl : Triplewise p' (map f l)
⊢ Triplewise p l

Tactic:
rw [triplewise_map] at hl

Goal state after:
α : Type u_1
β : Type u_2
l : List α
p : α → α → α → Prop
f : α → β
p' : β → β → β → Prop
h : ∀ {a b c : α}, p' (f a) (f b) (f c) → p a b c
hl : Triplewise (fun a b c ↦ p' (f a) (f b) (f c)) l
⊢ Triplewise p l
Module: Mathlib.Combinatorics.Hall.Finite

Goal state before:
pp: ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
n : ℕ
hn : Fintype.card ι = n + 1
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ih :
  ∀ {ι' : Type u} [inst : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n →
      (∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
ha : ∀ (s : Finset ι), s.Nonempty → s ≠ univ → #s < #(s.biUnion t)
this✝ : Nonempty ι
this : DecidableEq ι
x : ι := Classical.arbitrary ι
⊢ 0 < #(t x)

Tactic:
calc
      0 < 1 := Nat.one_pos
      _ ≤ #(.biUnion {x} t) := ht {x}
      _ = (t x).card := by rw [Finset.singleton_biUnion]

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

Goal state before:
pp: s : Set ℝ
f : ℝ → ℝ
hsc : IsClosed s
hfc : LowerSemicontinuousOn f s
hf : ConvexOn ℝ s f
⊢ ∃ c c', ∀ x ∈ s, c * x + c' ≤ f x

Tactic:
rcases s.eq_empty_or_nonempty with rfl | ⟨x, hxs⟩

Goal state after:
case inl
f : ℝ → ℝ
hsc : IsClosed ∅
hfc : LowerSemicontinuousOn f ∅
hf : ConvexOn ℝ ∅ f
⊢ ∃ c c', ∀ x ∈ ∅, c * x + c' ≤ f x

case inr
s : Set ℝ
f : ℝ → ℝ
hsc : IsClosed s
hfc : LowerSemicontinuousOn f s
hf : ConvexOn ℝ s f
x : ℝ
hxs : x ∈ s
⊢ ∃ c c', ∀ x ∈ s, c * x + c' ≤ f x
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : IsOrderedRing R
x y : P
⊢ affineSegment R x y = affineSegment R y x

Tactic:
refine Set.ext fun z => ?_
  constructor <;>
    · rintro ⟨t, ht, hxy⟩
      refine ⟨1 - t, ?_, ?_⟩
      · rwa [Set.sub_mem_Icc_iff_right, sub_self, sub_zero]
      · rwa [lineMap_apply_one_sub]

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

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x : R
⊢ Sbtw R 1 x 0 ↔ x ∈ Set.Ioo 0 1

Tactic:
sbtw_comm,

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x : R
⊢ Sbtw R 0 x 1 ↔ x ∈ Set.Ioo 0 1
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁷ : Ring R
inst✝⁶ : PartialOrder R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : IsOrderedRing R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R V
x z : P
hxz : x ≠ z
t : R
ht : t ∈ Set.Ioo 0 1
⊢ t • (z -ᵥ x) + (x -ᵥ x) ≠ 0 ∧ (t • (z -ᵥ x) +ᵥ x) -ᵥ z ≠ 0

Tactic:
vsub_self,

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁷ : Ring R
inst✝⁶ : PartialOrder R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : IsOrderedRing R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R V
x z : P
hxz : x ≠ z
t : R
ht : t ∈ Set.Ioo 0 1
⊢ t • (z -ᵥ x) + 0 ≠ 0 ∧ (t • (z -ᵥ x) +ᵥ x) -ᵥ z ≠ 0
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: case inr
J : Type u
inst✝³ : Category.{w, u} J
inst✝² : IsCofilteredOrEmpty J
F : J ⥤ Type v
inst✝¹ : ∀ (j : J), Finite (F.obj j)
inst✝ : ∀ (j : J), Nonempty (F.obj j)
J' : Type (max w v u) := AsSmall J
down : J' ⥤ J := AsSmall.down
F' : J' ⥤ Type (max u v w) := down ⋙ F ⋙ uliftFunctor.{max u w, v}
this✝¹ : ∀ (i : J'), Nonempty (F'.obj i)
this✝ : ∀ (i : J'), Finite (F'.obj i)
h✝ : Nonempty J
this : IsCofiltered J
⊢ F.sections.Nonempty

Tactic:
obtain ⟨u, hu⟩ := nonempty_sections_of_finite_cofiltered_system.init F'

Goal state after:
case inr
J : Type u
inst✝³ : Category.{w, u} J
inst✝² : IsCofilteredOrEmpty J
F : J ⥤ Type v
inst✝¹ : ∀ (j : J), Finite (F.obj j)
inst✝ : ∀ (j : J), Nonempty (F.obj j)
J' : Type (max w v u) := AsSmall J
down : J' ⥤ J := AsSmall.down
F' : J' ⥤ Type (max u v w) := down ⋙ F ⋙ uliftFunctor.{max u w, v}
this✝¹ : ∀ (i : J'), Nonempty (F'.obj i)
this✝ : ∀ (i : J'), Finite (F'.obj i)
h✝ : Nonempty J
this : IsCofiltered J
u : (j : J') → F'.obj j
hu : u ∈ F'.sections
⊢ F.sections.Nonempty
Module: Mathlib.Topology.Category.TopCat.Limits.Konig

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
F : J ⥤ TopCat
inst✝ : ∀ (j : J), T2Space ↑(F.obj j)
G : Finset J
H : Finset (FiniteDiagramArrow G)
⊢ partialSections F H = ⋂ f ∈ H, {u | (ConcreteCategory.hom (F.map f.snd.snd.snd.snd)) (u f.fst) = u f.snd.fst}

Tactic:
ext1

Goal state after:
J : Type u
inst✝¹ : SmallCategory J
F : J ⥤ TopCat
inst✝ : ∀ (j : J), T2Space ↑(F.obj j)
G : Finset J
H : Finset (FiniteDiagramArrow G)
x✝ : (j : J) → ↑(F.obj j)
⊢ x✝ ∈ partialSections F H ↔
    x✝ ∈ ⋂ f ∈ H, {u | (ConcreteCategory.hom (F.map f.snd.snd.snd.snd)) (u f.fst) = u f.snd.fst}
Module: Mathlib.Data.PEquiv

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

Tactic:
ofSet_eq_refl,

Goal state after:
α : Type u
β : Type v
f : α ≃. β
⊢ {a | (f a).isSome = true} = Set.univ ↔ ∀ (a : α), (f a).isSome = true
Module: Mathlib.LinearAlgebra.Matrix.Permutation

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝² : DecidableEq n
σ : Perm n
inst✝¹ : NonAssocSemiring R
inst✝ : StarRing R
⊢ (Perm.permMatrix R σ)ᴴ = Perm.permMatrix R σ⁻¹

Tactic:
by
  simp only [conjTranspose, transpose_permMatrix, map]
  aesop

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

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semifield R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
M : Matrix n n R
s : R
hs : 0 < s
hM : (∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j, M i j = s) ∧ ∀ (j : n), ∑ i, M i j = s
f : n → Finset n := ⋯
A : Finset n
this : ∀ (i : n), ∑ j ∈ f i, M i j = s
h₁ : ∑ i ∈ A, ∑ j ∈ f i, M i j = ↑(#A) * s
h₂ : ∑ i, ∑ j ∈ A.biUnion f, M i j = ↑(#(A.biUnion f)) * s
⊢ ∑ i ∈ A, ∑ j ∈ f i, M i j ≤ ∑ i ∈ A, ∑ j ∈ A.biUnion f, M i j

Tactic:
refine sum_le_sum fun i hi => ?_
      exact sum_le_sum_of_subset_of_nonneg (subset_biUnion_of_mem f hi) (by simp [*])

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

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : IsTorsionFree R V
t : Affine.Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
hu : Finset.univ = {i₁, i₂, i₃}
r₁ : R
hr₁0 : 0 < r₁
hr₁1 : r₁ < 1
h₁ : Sbtw R (t.points i₂) ((lineMap (t.points i₂) (t.points i₃)) r₁) (t.points i₃)
r₂ : R
hr₂0 : 0 < r₂
hr₂1 : r₂ < 1
h₂ : Sbtw R (t.points i₁) ((lineMap (t.points i₁) (t.points i₃)) r₂) (t.points i₃)
w : Fin (2 + 1) → R
hw : ∑ i, w i = 1
hp : (Finset.affineCombination R Finset.univ t.points) w ∈ affineSpan R (Set.range t.points)
h₁' :
  (Finset.affineCombination R Finset.univ t.points) w ∈
    line[R, (Finset.affineCombination R Finset.univ t.points) (Pi.single i₁ 1),
      (Finset.affineCombination R Finset.univ t.points) (Finset.affineCombinationLineMapWeights i₂ i₃ r₁)]
h₂' :
  (Finset.affineCombination R Finset.univ t.points) w ∈ line[R, t.points i₂, (lineMap (t.points i₁) (t.points i₃)) r₂]
h₁s : SignType.sign (w i₂) = SignType.sign (w i₃)
h₂s : SignType.sign (w i₁) = SignType.sign (w i₃)
hs : ∀ (i : Fin 3), SignType.sign (w i) = SignType.sign (w i₃)
hss : SignType.sign (w i₃) = 1
hs' : SignType.sign (∑ i, w i) = SignType.sign (w i₃)
⊢ w i₁ ∈ Set.Ioo 0 1

Tactic:
hss,

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : IsTorsionFree R V
t : Affine.Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
hu : Finset.univ = {i₁, i₂, i₃}
r₁ : R
hr₁0 : 0 < r₁
hr₁1 : r₁ < 1
h₁ : Sbtw R (t.points i₂) ((lineMap (t.points i₂) (t.points i₃)) r₁) (t.points i₃)
r₂ : R
hr₂0 : 0 < r₂
hr₂1 : r₂ < 1
h₂ : Sbtw R (t.points i₁) ((lineMap (t.points i₁) (t.points i₃)) r₂) (t.points i₃)
w : Fin (2 + 1) → R
hw : ∑ i, w i = 1
hp : (Finset.affineCombination R Finset.univ t.points) w ∈ affineSpan R (Set.range t.points)
h₁' :
  (Finset.affineCombination R Finset.univ t.points) w ∈
    line[R, (Finset.affineCombination R Finset.univ t.points) (Pi.single i₁ 1),
      (Finset.affineCombination R Finset.univ t.points) (Finset.affineCombinationLineMapWeights i₂ i₃ r₁)]
h₂' :
  (Finset.affineCombination R Finset.univ t.points) w ∈ line[R, t.points i₂, (lineMap (t.points i₁) (t.points i₃)) r₂]
h₁s : SignType.sign (w i₂) = SignType.sign (w i₃)
h₂s : SignType.sign (w i₁) = SignType.sign (w i₃)
hss : SignType.sign (w i₃) = 1
hs' : SignType.sign (∑ i, w i) = SignType.sign (w i₃)
hs : ∀ (i : Fin 3), SignType.sign (w i) = 1
⊢ w i₁ ∈ Set.Ioo 0 1