mathlib-initiative/mathlib-tactics huggingface dataset:
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) (LinearMap.det f)

Tactic:
det_eq_one_of_not_module_finite (Module.not_finite_of_infinite_basis bA),

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) = (Algebra.norm R) 1
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
⊢ 1 + (sinh (arsinh (dist ↑z ↑w / (2 * √(z.im * w.im)))) ^ 2 + sinh (arsinh (dist ↑z ↑w / (2 * √(z.im * w.im)))) ^ 2) =
    1 + dist ↑z ↑w ^ 2 / (2 * z.im * w.im)

Tactic:
← two_mul,

Goal state after:
z w : ℍ
⊢ 1 + 2 * sinh (arsinh (dist ↑z ↑w / (2 * √(z.im * w.im)))) ^ 2 = 1 + dist ↑z ↑w ^ 2 / (2 * z.im * w.im)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z : ℍ
⊢ z.center 0 = z

Tactic:
apply ext_re_im

Goal state after:
case hre
z : ℍ
⊢ (z.center 0).re = z.re

case him
z : ℍ
⊢ (z.center 0).im = z.im
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : CompactSpace β
a b : α
f : α → β
hcf : Continuous[inst✝³, inst✝²] f
h : stoneCechUnit a = stoneCechUnit b
⊢ f a = f b

Tactic:
← congrFun (stoneCechExtend_extends hcf),

Goal state after:
α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : CompactSpace β
a b : α
f : α → β
hcf : Continuous[inst✝³, inst✝²] f
h : stoneCechUnit a = stoneCechUnit b
⊢ (stoneCechExtend hcf ∘ stoneCechUnit) a = f b
Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace

Goal state before:
pp: X✝ : Type w
Y : Type x
X : Type v
t : TopologicalSpace X
inst✝ : DiscreteTopology X
⊢ t ≤ compactlyGenerated X

Tactic:
DiscreteTopology.eq_bot (t := t)

Goal state after:
X✝ : Type w
Y : Type x
X : Type v
t : TopologicalSpace X
inst✝ : DiscreteTopology X
⊢ ⊥ ≤ compactlyGenerated X
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_3
inst✝ : TopologicalSpace Y
f : OnePoint X → Y
x : X
⊢ Tendsto f (𝓝 ↑x) (𝓝 (f ↑x)) ↔ ContinuousAt (f ∘ some) x

Tactic:
nhds_coe_eq,

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_3
inst✝ : TopologicalSpace Y
f : OnePoint X → Y
x : X
⊢ Tendsto f (map some (𝓝 x)) (𝓝 (f ↑x)) ↔ ContinuousAt (f ∘ some) x
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✝¹ : WeaklyLocallyCompactSpace X
inst✝ : R1Space X
z : X
⊢ Disjoint (𝓝 ↑z) (map some (coclosedCompact X)) ∧ Disjoint (𝓝 ↑z) (pure ∞)

Tactic:
nhds_coe_eq,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
inst✝¹ : WeaklyLocallyCompactSpace X
inst✝ : R1Space X
z : X
⊢ Disjoint (map some (𝓝 z)) (map some (coclosedCompact X)) ∧ Disjoint (map some (𝓝 z)) (pure ∞)
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: case coe.coe
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
inst✝¹ : WeaklyLocallyCompactSpace X
inst✝ : R1Space X
key : ∀ (z : X), Disjoint (𝓝 ↑z) (𝓝 ∞)
x✝¹ x✝ : X
⊢ ↑x✝¹ ⤳ ↑x✝ ∨ Disjoint (𝓝 ↑x✝¹) (𝓝 ↑x✝)

Tactic:
nhds_coe_eq,

Goal state after:
case coe.coe
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
inst✝¹ : WeaklyLocallyCompactSpace X
inst✝ : R1Space X
key : ∀ (z : X), Disjoint (𝓝 ↑z) (𝓝 ∞)
x✝¹ x✝ : X
⊢ ↑x✝¹ ⤳ ↑x✝ ∨ Disjoint (map some (𝓝 x✝¹)) (𝓝 ↑x✝)
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: case coe.coe
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
inst✝¹ : WeaklyLocallyCompactSpace X
inst✝ : R1Space X
key : ∀ (z : X), Disjoint (𝓝 ↑z) (𝓝 ∞)
x✝¹ x✝ : X
⊢ ↑x✝¹ ⤳ ↑x✝ ∨ Disjoint (map some (𝓝 x✝¹)) (𝓝 ↑x✝)

Tactic:
nhds_coe_eq,

Goal state after:
case coe.coe
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
inst✝¹ : WeaklyLocallyCompactSpace X
inst✝ : R1Space X
key : ∀ (z : X), Disjoint (𝓝 ↑z) (𝓝 ∞)
x✝¹ x✝ : X
⊢ ↑x✝¹ ⤳ ↑x✝ ∨ Disjoint (map some (𝓝 x✝¹)) (map some (𝓝 x✝))
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: case coe.coe
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
inst✝¹ : WeaklyLocallyCompactSpace X
inst✝ : R1Space X
key : ∀ (z : X), Disjoint (𝓝 ↑z) (𝓝 ∞)
x✝¹ x✝ : X
⊢ x✝¹ ⤳ x✝ ∨ Disjoint (𝓝 x✝¹) (𝓝 x✝)

Tactic:
apply specializes_or_disjoint_nhds

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

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
a₀ : E
⊢ proximity f ↑a₀ = circleAverage (fun x ↦ log⁺ ‖f x - a₀‖⁻¹) 0

Tactic:
simp [proximity]

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

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
⊢ proximity f 0 = circleAverage (fun x ↦ log⁺ ‖f x‖⁻¹) 0

Tactic:
simp [proximity]

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

Goal state before:
pp: f : ℂ → ℂ
⊢ proximity f 0 = circleAverage (fun x ↦ log⁺ ‖f⁻¹ x‖) 0

Tactic:
simp [proximity]

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

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
⊢ proximity f ⊤ = circleAverage (fun x ↦ log⁺ ‖f x‖) 0

Tactic:
simp [proximity]

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

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f g : ℂ → E
a : WithTop E
r : ℝ
hfg : f =ᶠ[codiscreteWithin (sphere 0 |r|)] g
hr : r ≠ 0
h : a = ⊤
⊢ ∀ (a : ℂ), f a = g a → log⁺ ‖f a‖ = log⁺ ‖g a‖

Tactic:
by aesop

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

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f g : ℂ → E
a : WithTop E
r : ℝ
hfg : f =ᶠ[codiscreteWithin (sphere 0 |r|)] g
hr : r ≠ 0
h : ¬a = ⊤
⊢ ∀ (a_1 : ℂ), f a_1 = g a_1 → log⁺ ‖f a_1 - a.untop₀‖⁻¹ = log⁺ ‖g a_1 - a.untop₀‖⁻¹

Tactic:
by aesop

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

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
a₀ : E
⊢ proximity f ↑a₀ = proximity (f - fun x ↦ a₀) 0

Tactic:
simp [proximity]

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

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

Tactic:
simp [proximity]

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

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

Tactic:
simp [proximity]

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: E✝ : Type u_1
inst✝² : NormedAddCommGroup E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
⊢ (fun r ↦ ∑ᶠ (z : E), ↑(((toClosedBall r) 0) z) * log (r * ‖z‖⁻¹) + ↑(0 0) * log r) = 0

Tactic:
by aesop

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a₀ : E
f : ℂ → E
r : ℝ
h : Meromorphic f
h₁f : CircleIntegrable (fun x ↦ log⁺ ‖f x‖) 0 r
h₂f : CircleIntegrable (fun x ↦ log⁺ ‖f x - a₀‖) 0 r
⊢ |circleAverage ((fun x ↦ log⁺ ‖f x‖) - fun x ↦ log⁺ ‖f x - a₀‖) 0 r| ≤ log⁺ ‖a₀‖ + log 2

Tactic:
apply le_trans abs_circleAverage_le_circleAverage_abs

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a₀ : E
f : ℂ → E
r : ℝ
h : Meromorphic f
h₁f : CircleIntegrable (fun x ↦ log⁺ ‖f x‖) 0 r
h₂f : CircleIntegrable (fun x ↦ log⁺ ‖f x - a₀‖) 0 r
⊢ circleAverage |(fun x ↦ log⁺ ‖f x‖) - fun x ↦ log⁺ ‖f x - a₀‖| 0 r ≤ log⁺ ‖a₀‖ + log 2
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : DecidableEq E
inst✝ : ProperSpace E
D : locallyFinsupp E ℤ
e : E
hD : single e 1 ≤ D
⊢ logCounting D = logCounting (single e 1) + logCounting (D - single e 1)

Tactic:
by aesop

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: case pos
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
hfg : f =ᶠ[codiscrete ℂ] g
a : WithTop E
h : a = ⊤
⊢ logCounting f a = logCounting g a

pp: case neg
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
hfg : f =ᶠ[codiscrete ℂ] g
a : WithTop E
h : ¬a = ⊤
⊢ logCounting f a = logCounting g a

Tactic:
· simp only [logCounting, h, ↓reduceDIte]
    congr 2
    exact divisor_congr_codiscreteWithin hfg isOpen_univ

Goal state after:
case neg
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
hfg : f =ᶠ[codiscrete ℂ] g
a : WithTop E
h : ¬a = ⊤
⊢ logCounting f a = logCounting g a
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
l : ℝ≥0
x y z : ℝ
hfs : HasConstantSpeedOnWith f (Icc x y) l
hft : HasConstantSpeedOnWith f (Icc y z) l
⊢ HasConstantSpeedOnWith f (Icc x z) l

Tactic:
rcases le_total x y with (xy | yx)
  · rcases le_total y z with (yz | zy)
    · rw [← Set.Icc_union_Icc_eq_Icc xy yz]
      exact hfs.union hft (isGreatest_Icc xy) (isLeast_Icc yz)
    · rintro u ⟨xu, uz⟩ v ⟨xv, vz⟩
      rw [Icc_inter_Icc, sup_of_le_right xu, inf_of_le_right vz, ←
        hfs ⟨xu, uz.trans zy⟩ ⟨xv, vz.trans zy⟩, Icc_inter_Icc, sup_of_le_right xu,
        inf_of_le_right (vz.trans zy)]
  · rintro u ⟨xu, uz⟩ v ⟨xv, vz⟩
    rw [Icc_inter_Icc, sup_of_le_right xu, inf_of_le_right vz, ←
      hft ⟨yx.trans xu, uz⟩ ⟨yx.trans xv, vz⟩, Icc_inter_Icc, sup_of_le_right (yx.trans xu),
      inf_of_le_right vz]

Goal state after:
Module: Mathlib.Data.List.Triplewise

Goal state before:
pp: α : Type u_1
β : Type u_2
l : List α
f : α → β
p' : β → β → β → Prop
⊢ Triplewise p' (map f l) ↔ Triplewise (fun a b c ↦ p' (f a) (f b) (f c)) l

Tactic:
induction l with
  | nil => simp
  | cons h t ih => simp [map, triplewise_cons, ih, pairwise_map]

Goal state after:
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
φ : ℝ → ℝ
φm : MonotoneOn φ s
hfφ : HasUnitSpeedOn (f ∘ φ) s
hf : HasUnitSpeedOn f (φ '' s)
x : ℝ
xs : x ∈ s
⊢ EqOn φ (fun y ↦ y - x + φ x) s

Tactic:
dsimp only [HasUnitSpeedOn] at hf hfφ

Goal state after:
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
φ : ℝ → ℝ
φm : MonotoneOn φ s
hfφ : HasConstantSpeedOnWith (f ∘ φ) s 1
hf : HasConstantSpeedOnWith f (φ '' s) 1
x : ℝ
xs : x ∈ s
⊢ EqOn φ (fun y ↦ y - x + φ x) s
Module: Mathlib.Data.List.Triplewise

Goal state before:
pp: α : Type u_1
l : List α
p : α → α → α → Prop
⊢ Triplewise p l.reverse ↔ Triplewise (fun a b c ↦ p c b a) l

Tactic:
induction l with
  | nil => simp
  | cons h t ih =>
    simp [triplewise_append, pairwise_reverse, triplewise_cons, ih, and_comm]

Goal state after:
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: case inr.h
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a : α
as : a ∈ s
b : α
bs : b ∈ s
c : α
cs : c ∈ s
h : variationOnFromTo f s a b ≤ variationOnFromTo f s a c
bc : b ≤ c
⊢ ∀ ⦃x : α⦄, x ∈ s ∩ Icc b c → edist ((naturalParameterization f s a ∘ variationOnFromTo f s a) x) (f x) = 0

Tactic:
rintro x ⟨xs, _, _⟩

Goal state after:
case inr.h
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a : α
as : a ∈ s
b : α
bs : b ∈ s
c : α
cs : c ∈ s
h : variationOnFromTo f s a b ≤ variationOnFromTo f s a c
bc : b ≤ c
x : α
xs : x ∈ s
left✝ : b ≤ x
right✝ : x ≤ c
⊢ edist ((naturalParameterization f s a ∘ variationOnFromTo f s a) x) (f x) = 0
Module: Mathlib.Analysis.Convex.BetweenList

Goal state before:
pp: 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
l : List P
hl : l ≠ []
h : List.Wbtw R l
this : ∃ l', (∀ a ∈ l', 0 ≤ a) ∧ l'.SortedLE ∧ map (⇑(lineMap (l.head hl) (l.getLast hl))) l' = l
⊢ ∃ l', l'.SortedLE ∧ map (⇑(lineMap (l.head hl) (l.getLast hl))) l' = l

Tactic:
rcases this with ⟨l', -, hl'⟩

Goal state after:
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
l : List P
hl : l ≠ []
h : List.Wbtw R l
l' : List R
hl' : l'.SortedLE ∧ map (⇑(lineMap (l.head hl) (l.getLast hl))) l' = l
⊢ ∃ l', l'.SortedLE ∧ map (⇑(lineMap (l.head hl) (l.getLast hl))) l' = l
Module: Mathlib.Analysis.Convex.BetweenList

Goal state before:
pp: case refine_2.refine_2.cons
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
l' : List R
hl's : l'.SortedLE
head : P
tail : List P
hl : head :: tail ≠ []
hp : Pairwise (fun x1 x2 ↦ x1 ≠ x2) (head :: tail)
hl'l : map (⇑(lineMap ((head :: tail).head hl) ((head :: tail).getLast hl))) l' = head :: tail
⊢ (head :: tail).length = 1 ∨ (head :: tail).head hl ≠ (head :: tail).getLast hl

Tactic:
simp only [length_cons, add_eq_right, length_eq_zero_iff, head_cons]
        cases tail with
        | nil => simp
        | cons head2 tail =>
          simp only [reduceCtorEq, false_or]
          rw [pairwise_cons] at hp
          refine hp.1 ((head :: head2 :: tail).getLast hl) ?_
          simp

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Konig

Goal state before:
pp: J : Type u
inst✝ : SmallCategory J
F : J ⥤ TopCat
A B : FiniteDiagram J
ιA : FiniteDiagramArrow A.fst → FiniteDiagramArrow (A.fst ⊔ B.fst) :=
  fun f ↦ ⟨f.fst, ⟨f.snd.fst, ⟨⋯, ⟨⋯, f.snd.snd.snd.snd⟩⟩⟩⟩
ιB : FiniteDiagramArrow B.fst → FiniteDiagramArrow (A.fst ⊔ B.fst) :=
  fun f ↦ ⟨f.fst, ⟨f.snd.fst, ⟨⋯, ⟨⋯, f.snd.snd.snd.snd⟩⟩⟩⟩
u : (j : J) → ↑(F.obj j)
hu : u ∈ (fun G ↦ partialSections F G.snd) ⟨A.fst ⊔ B.fst, Finset.image ιA A.snd ⊔ Finset.image ιB B.snd⟩
f : FiniteDiagramArrow B.fst
hf : f ∈ B.snd
⊢ ιB f ∈ Finset.image ιA A.snd ⊔ Finset.image ιB B.snd

Tactic:
apply Finset.mem_union_right

Goal state after:
J : Type u
inst✝ : SmallCategory J
F : J ⥤ TopCat
A B : FiniteDiagram J
ιA : FiniteDiagramArrow A.fst → FiniteDiagramArrow (A.fst ⊔ B.fst) := ⋯
ιB : FiniteDiagramArrow B.fst → FiniteDiagramArrow (A.fst ⊔ B.fst) := ⋯
u : (j : J) → ↑(F.obj j)
hu : u ∈ (fun G ↦ partialSections F G.snd) ⟨A.fst ⊔ B.fst, Finset.image ιA A.snd ⊔ Finset.image ιB B.snd⟩
f : FiniteDiagramArrow B.fst
hf : f ∈ B.snd
⊢ ιB f ∈ Finset.image ιB B.snd
Module: Mathlib.Topology.Category.TopCat.Limits.Konig

Goal state before:
pp: case property
J : Type u
inst✝⁴ : SmallCategory J
F : J ⥤ TopCat
inst✝³ : IsCofilteredOrEmpty J
inst✝² : ∀ (j : J), Nonempty ↑(F.obj j)
inst✝¹ : ∀ (j : J), CompactSpace ↑(F.obj j)
inst✝ : ∀ (j : J), T2Space ↑(F.obj j)
u : (j : J) → ↑(F.obj j)
hu : u ∈ ⋂ i, partialSections F i.snd
⊢ u ∈ {u | ∀ {i j : J} (f : i ⟶ j), (ConcreteCategory.hom (F.map f)) (u i) = u j}

Tactic:
intro X Y f

Goal state after:
case property
J : Type u
inst✝⁴ : SmallCategory J
F : J ⥤ TopCat
inst✝³ : IsCofilteredOrEmpty J
inst✝² : ∀ (j : J), Nonempty ↑(F.obj j)
inst✝¹ : ∀ (j : J), CompactSpace ↑(F.obj j)
inst✝ : ∀ (j : J), T2Space ↑(F.obj j)
u : (j : J) → ↑(F.obj j)
hu : u ∈ ⋂ i, partialSections F i.snd
X Y : J
f : X ⟶ Y
⊢ (ConcreteCategory.hom (F.map f)) (u X) = u Y
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: case inr
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✝¹ : AffineSpace V P
inst✝ : IsOrderedRing R
n : ℕ
s : Simplex R P n
i j : Fin (n + 1)
h : i ≠ j
hji : j < i
⊢ affineSegment R (s.points i) (s.points j) = affineSegment R (s.points (min i j)) (s.points (max i j))

Tactic:
· nth_rw 2 [affineSegment_comm]
      simp [max_eq_left hji.le, min_eq_right hji.le]

Goal state after:
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v_1, u} J
F : J ⥤ Type v
i : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
h : F.IsMittagLeffler
j : J
⊢ ∃ i_1 f,
    ∀ ⦃k : J⦄ (g : k ⟶ i_1),
      range ⇑(ConcreteCategory.hom ((F.toPreimages s).map f)) ⊆
        range ⇑(ConcreteCategory.hom ((F.toPreimages s).map (g ≫ f)))

Tactic:
by
    obtain ⟨j₁, g₁, f₁, -⟩ := IsCofilteredOrEmpty.cone_objs i j
    obtain ⟨j₂, f₂, h₂⟩ := F.isMittagLeffler_iff_eventualRange.1 h j₁
    refine ⟨j₂, f₂ ≫ f₁, fun j₃ f₃ => ?_⟩
    rintro _ ⟨⟨x, hx⟩, rfl⟩
    have : F.map f₂ x ∈ F.eventualRange j₁ := by
      rw [h₂]
      exact ⟨_, rfl⟩
    obtain ⟨y, hy, h₃⟩ := h.subset_image_eventualRange F (f₃ ≫ f₂) this
    refine ⟨⟨y, mem_iInter.2 fun g₂ => ?_⟩, Subtype.ext ?_⟩
    · obtain ⟨j₄, f₄, h₄⟩ := IsCofilteredOrEmpty.cone_maps g₂ ((f₃ ≫ f₂) ≫ g₁)
      obtain ⟨y, rfl⟩ := F.mem_eventualRange_iff.1 hy f₄
      rw [← comp_apply, ← map_comp] at h₃
      rw [mem_preimage, ← comp_apply, ← map_comp, h₄, ← Category.assoc, map_comp, comp_apply, h₃,
        ← comp_apply, ← map_comp]
      apply mem_iInter.1 hx
    · simp only [toPreimages_obj, toPreimages_map, ConcreteCategory.hom_ofHom,
        TypeCat.Fun.coe_mk, MapsTo.val_restrict_apply]
      rw [← Category.assoc, map_comp, comp_apply, h₃, map_comp, comp_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Stochastic

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
M : Matrix n n R
⊢ Mᵀ ∈ rowStochastic R n ↔ M ∈ colStochastic R n

Tactic:
simp only [mem_colStochastic_iff_sum, mem_rowStochastic_iff_sum, transpose_apply,
    and_congr_left_iff]
  exact fun _ ↦ forall_comm

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Stochastic

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
M : Matrix n n R
⊢ Mᵀ ∈ colStochastic R n ↔ M ∈ rowStochastic R n

Tactic:
simp only [mem_colStochastic_iff_sum, mem_rowStochastic_iff_sum, transpose_apply,
    and_congr_left_iff]
  exact fun _ ↦ forall_comm

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

Goal state before:
pp: case mk
V : Type u_1
inst✝² : TopologicalSpace V
inst✝¹ : AddCommGroup V
inst✝ : Module ℝ V
L : ConvexBody V
carrier✝ : Set V
convex'✝ : Convex ℝ carrier✝
isCompact'✝ : IsCompact carrier✝
nonempty'✝ : carrier✝.Nonempty
h : { carrier := carrier✝, convex' := convex'✝, isCompact' := isCompact'✝, nonempty' := nonempty'✝ }.carrier = L.carrier
⊢ { carrier := carrier✝, convex' := convex'✝, isCompact' := isCompact'✝, nonempty' := nonempty'✝ } = L

Tactic:
cases L

Goal state after:
case mk.mk
V : Type u_1
inst✝² : TopologicalSpace V
inst✝¹ : AddCommGroup V
inst✝ : Module ℝ V
carrier✝¹ : Set V
convex'✝¹ : Convex ℝ carrier✝¹
isCompact'✝¹ : IsCompact carrier✝¹
nonempty'✝¹ : carrier✝¹.Nonempty
carrier✝ : Set V
convex'✝ : Convex ℝ carrier✝
isCompact'✝ : IsCompact carrier✝
nonempty'✝ : carrier✝.Nonempty
h :
  { carrier := carrier✝¹, convex' := convex'✝¹, isCompact' := isCompact'✝¹, nonempty' := nonempty'✝¹ }.carrier =
    { carrier := carrier✝, convex' := convex'✝, isCompact' := isCompact'✝, nonempty' := nonempty'✝ }.carrier
⊢ { carrier := carrier✝¹, convex' := convex'✝¹, isCompact' := isCompact'✝¹, nonempty' := nonempty'✝¹ } =
    { carrier := carrier✝, convex' := convex'✝, isCompact' := isCompact'✝, nonempty' := nonempty'✝ }
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
s : Set E
x : E
hx : x ∈ (convexHull 𝕜) s
k : ℕ := #(minCardFinsetOfMemConvexHull hx) - 1
hk : #(minCardFinsetOfMemConvexHull hx) = k + 1
h : ¬AffineIndependent 𝕜 Subtype.val
p : ↑↑(minCardFinsetOfMemConvexHull hx)
hp : x ∈ (convexHull 𝕜) ↑((minCardFinsetOfMemConvexHull hx).erase ↑p)
contra : #(minCardFinsetOfMemConvexHull hx) ≤ #((minCardFinsetOfMemConvexHull hx).erase ↑p)
⊢ False

Tactic:
← not_lt

Goal state after:
𝕜 : Type u_1
E : Type u
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : x ∈ (convexHull 𝕜) s
k : ℕ := #(minCardFinsetOfMemConvexHull hx) - 1
hk : #(minCardFinsetOfMemConvexHull hx) = k + 1
h : ¬AffineIndependent 𝕜 Subtype.val
p : ↑↑(minCardFinsetOfMemConvexHull hx)
hp : x ∈ (convexHull 𝕜) ↑((minCardFinsetOfMemConvexHull hx).erase ↑p)
contra : ¬#((minCardFinsetOfMemConvexHull hx).erase ↑p) < #(minCardFinsetOfMemConvexHull hx)
⊢ False
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✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x : P
v : V
r₁ r₂ : R
hr₁ : r₁ ≤ 0
hr₂ : r₂ ≤ 0
⊢ Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x) ∨ Wbtw R x (r₂ • v +ᵥ x) (r₁ • v +ᵥ x)

Tactic:
rcases le_total r₁ r₂ with (h | h)
  · exact Or.inr (wbtw_smul_vadd_smul_vadd_of_nonpos_of_le x v hr₂ h)
  · exact Or.inl (wbtw_smul_vadd_smul_vadd_of_nonpos_of_le x v hr₁ h)

Goal state after:
Module: Mathlib.Analysis.Convex.Cone.Dual

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : PartialOrder R
inst✝⁹ : IsOrderedRing R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : ClosedIciTopology R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : TopologicalSpace N
p : M →ₗ[R] N →ₗ[R] R
inst✝ : p.IsContPerfPair
s t : Set M
⊢ dual p (s ∪ t) = dual p s ⊓ dual p t

Tactic:
by aesop

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

Goal state before:
pp: case inr.inr.inr.inr
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
ty tz : R
h : ∀ (p : P), p = x ∨ p = ty • v +ᵥ x ∨ p = tz • v +ᵥ x → ∃ r, p = r • v +ᵥ x
hy0 : 0 < ty
hz0 : 0 < tz
⊢ Wbtw R x (ty • v +ᵥ x) (tz • v +ᵥ x) ∨ Wbtw R (ty • v +ᵥ x) (tz • v +ᵥ x) x ∨ Wbtw R (tz • v +ᵥ x) x (ty • v +ᵥ x)

Tactic:
rw [wbtw_comm (z := x)]
      rw [← or_assoc]
      exact Or.inl (wbtw_or_wbtw_smul_vadd_of_nonneg _ _ hy0.le hz0.le)

Goal state after:
Module: Mathlib.Geometry.Convex.Cone.Dual

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsOrderedRing R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : M →ₗ[R] N →ₗ[R] R
s t : Set M
⊢ dual p (s ∪ t) = dual p s ⊓ dual p t

Tactic:
by aesop

Goal state after: