harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
theorem IsIndepSet.card_le_indepNum
    [Fintype α] {t : Finset α} (tc : G.IsIndepSet t) : #t ≤ G.indepNum

Proof state:
α : Type u_3
G : SimpleGraph α
inst✝ : Fintype α
t : Finset α
tc : G.IsIndepSet ↑t
⊢ #t ≤ G.indepNum

Tactic:
rw [← isClique_compl] at tc

Result:
α : Type u_3
G : SimpleGraph α
inst✝ : Fintype α
t : Finset α
tc : Gᶜ.IsClique ↑t
⊢ #t ≤ G.indepNum

Proof state:
α : Type u_3
G : SimpleGraph α
inst✝ : Fintype α
t : Finset α
tc : Gᶜ.IsClique ↑t
⊢ #t ≤ sSup {n | ∃ s, Gᶜ.IsNClique n s}

Tactic:
exact tc.card_le_cliqueNum

Result:
no goals

Proof state:
α : Type u_3
G : SimpleGraph α
inst✝ : Fintype α
t : Finset α
tc : Gᶜ.IsClique ↑t
⊢ #t ≤ G.indepNum

Tactic:
simp_rw [indepNum, ← isNClique_compl]

Result:
α : Type u_3
G : SimpleGraph α
inst✝ : Fintype α
t : Finset α
tc : Gᶜ.IsClique ↑t
⊢ #t ≤ sSup {n | ∃ s, Gᶜ.IsNClique n s}
-- Mathlib/Algebra/Homology/HomotopyCategory/Shift.lean
lemma shiftFunctorAdd'_hom_app_f' (K : CochainComplex C ℤ) (a b ab : ℤ) (h : a + b = ab) (n : ℤ) :
    ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) a b ab h).hom.app K).f n =
      (K.XIsoOfEq (by dsimp; rw [← h, add_assoc, add_comm a])).hom

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
a b ab : ℤ
h : a + b = ab
n : ℤ
⊢ ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) a b ab h).hom.app K).f n = (XIsoOfEq K ⋯).hom

Tactic:
subst h

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
a b n : ℤ
⊢ ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) a b (a + b) ⋯).hom.app K).f n = (XIsoOfEq K ⋯).hom

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
a b n : ℤ
⊢ ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) a b (a + b) ⋯).hom.app K).f n = (XIsoOfEq K ⋯).hom

Tactic:
rw [shiftFunctorAdd'_eq_shiftFunctorAdd, shiftFunctorAdd_hom_app_f]

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
K : CochainComplex C ℤ
a b ab : ℤ
h : a + b = ab
n : ℤ
⊢ n + { as := ab }.as = n + { as := b }.as + { as := a }.as

Tactic:
dsimp

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
K : CochainComplex C ℤ
a b ab : ℤ
h : a + b = ab
n : ℤ
⊢ n + ab = n + b + a

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
K : CochainComplex C ℤ
a b ab : ℤ
h : a + b = ab
n : ℤ
⊢ n + ab = n + b + a

Tactic:
rw [← h, add_assoc, add_comm a]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Basic.lean
theorem replaceF_eq_replaceFTR : @replaceF = @replaceFTR

Proof state:
case h.h.h
α : Type u_1
p : α → Option α
l : List α
⊢ replaceF p l = replaceFTR.go p l #[]

Tactic:
exact (go #[] _).symm

Result:
no goals

Proof state:
case none
α : Type u_1
p : α → Option α
l : List α
acc : Array α
x : α
xs : List α
⊢ replaceFTR.go p xs (acc.push x) = acc.toList ++ x :: replaceF p xs

Tactic:
rw [go _ xs]

Result:
case none
α : Type u_1
p : α → Option α
l : List α
acc : Array α
x : α
xs : List α
⊢ (acc.push x).toList ++ replaceF p xs = acc.toList ++ x :: replaceF p xs

Proof state:
⊢ @replaceF = @replaceFTR

Tactic:
funext α p l

Result:
case h.h.h
α : Type u_1
p : α → Option α
l : List α
⊢ replaceF p l = replaceFTR p l

Proof state:
α : Type u_1
p : α → Option α
l : List α
acc : Array α
⊢ replaceFTR.go p [] acc = acc.toList ++ replaceF p []

Tactic:
simp [replaceFTR.go, replaceF]

Result:
no goals

Proof state:
α : Type u_1
p : α → Option α
l : List α
acc : Array α
x : α
xs : List α
⊢ replaceFTR.go p (x :: xs) acc = acc.toList ++ replaceF p (x :: xs)

Tactic:
simp [replaceFTR.go, replaceF]

Result:
α : Type u_1
p : α → Option α
l : List α
acc : Array α
x : α
xs : List α
⊢ (match p x with
    | none => replaceFTR.go p xs (acc.push x)
    | some a' => acc.toList ++ a' :: xs) =
    acc.toList ++
      match p x with
      | none => x :: replaceF p xs
      | some a => a :: xs

Proof state:
α : Type u_1
p : α → Option α
l : List α
acc : Array α
x : α
xs : List α
⊢ (match p x with
    | none => replaceFTR.go p xs (acc.push x)
    | some a' => acc.toList ++ a' :: xs) =
    acc.toList ++
      match p x with
      | none => x :: replaceF p xs
      | some a => a :: xs

Tactic:
cases p x <;> simp

Result:
case none
α : Type u_1
p : α → Option α
l : List α
acc : Array α
x : α
xs : List α
⊢ replaceFTR.go p xs (acc.push x) = acc.toList ++ x :: replaceF p xs

Proof state:
case h.h.h
α : Type u_1
p : α → Option α
l : List α
⊢ replaceF p l = replaceFTR p l

Tactic:
simp [replaceFTR]

Result:
case h.h.h
α : Type u_1
p : α → Option α
l : List α
⊢ replaceF p l = replaceFTR.go p l #[]

Proof state:
case none
α : Type u_1
p : α → Option α
l : List α
acc : Array α
x : α
xs : List α
⊢ (acc.push x).toList ++ replaceF p xs = acc.toList ++ x :: replaceF p xs

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Convex/Cone/InnerDual.lean
theorem innerDualCone_insert (x : H) (s : Set H) :
    (insert x s).innerDualCone = Set.innerDualCone {x} ⊓ s.innerDualCone

Proof state:
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
x : H
s : Set H
⊢ (insert x s).innerDualCone = {x}.innerDualCone ⊓ s.innerDualCone

Tactic:
rw [insert_eq, innerDualCone_union]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem integral_comp_add_mul (hc : c ≠ 0) (d) :
    (∫ x in a..b, f (d + c * x)) = c⁻¹ • ∫ x in d + c * a..d + c * b, f x

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
hc : c ≠ 0
d : ℝ
⊢ ∫ (x : ℝ) in a..b, f (d + c * x) = c⁻¹ • ∫ (x : ℝ) in d + c * a..d + c * b, f x

Tactic:
rw [← integral_comp_add_left, ← integral_comp_mul_left _ hc]

Result:
no goals
-- Mathlib/Topology/DenseEmbedding.lean
theorem extend_eq' [T2Space γ] {f : α → γ} (di : IsDenseInducing i)
    (hf : ∀ b, ∃ c, Tendsto f (comap i (𝓝 b)) (𝓝 c)) (a : α) : di.extend f (i a) = f a

Proof state:
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
i : α → β
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space γ
f : α → γ
di : IsDenseInducing i
hf : ∀ (b : β), ∃ c, Tendsto f (comap i (𝓝 b)) (𝓝 c)
a : α
b : γ
hb : Tendsto f (comap i (𝓝 (i a))) (𝓝 b)
⊢ Tendsto f (𝓝 a) (𝓝 b)

Tactic:
rwa [← di.isInducing.nhds_eq_comap] at hb

Result:
no goals

Proof state:
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
i : α → β
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space γ
f : α → γ
di : IsDenseInducing i
hf : ∀ (b : β), ∃ c, Tendsto f (comap i (𝓝 b)) (𝓝 c)
a : α
b : γ
hb : Tendsto f (comap i (𝓝 (i a))) (𝓝 b)
⊢ di.extend f (i a) = f a

Tactic:
refine di.extend_eq_at' b ?_

Result:
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
i : α → β
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space γ
f : α → γ
di : IsDenseInducing i
hf : ∀ (b : β), ∃ c, Tendsto f (comap i (𝓝 b)) (𝓝 c)
a : α
b : γ
hb : Tendsto f (comap i (𝓝 (i a))) (𝓝 b)
⊢ Tendsto f (𝓝 a) (𝓝 b)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
i : α → β
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space γ
f : α → γ
di : IsDenseInducing i
hf : ∀ (b : β), ∃ c, Tendsto f (comap i (𝓝 b)) (𝓝 c)
a : α
⊢ di.extend f (i a) = f a

Tactic:
rcases hf (i a) with ⟨b, hb⟩

Result:
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
i : α → β
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space γ
f : α → γ
di : IsDenseInducing i
hf : ∀ (b : β), ∃ c, Tendsto f (comap i (𝓝 b)) (𝓝 c)
a : α
b : γ
hb : Tendsto f (comap i (𝓝 (i a))) (𝓝 b)
⊢ di.extend f (i a) = f a
-- Mathlib/MeasureTheory/Measure/WithDensity.lean
theorem withDensity_smul (r : ℝ≥0∞) {f : α → ℝ≥0∞} (hf : Measurable f) :
    μ.withDensity (r • f) = r • μ.withDensity f

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
⊢ μ.withDensity (r • f) = r • μ.withDensity f

Tactic:
refine Measure.ext fun s hs => ?_

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
⊢ (μ.withDensity (r • f)) s = (r • μ.withDensity f) s

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
⊢ (μ.withDensity (r • f)) s = (r • μ.withDensity f) s

Tactic:
rw [withDensity_apply _ hs, Measure.coe_smul, Pi.smul_apply, withDensity_apply _ hs,
  smul_eq_mul, ← lintegral_const_mul r hf]

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, (r • f) a ∂μ = ∫⁻ (a : α) in s, r * f a ∂μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, (r • f) a ∂μ = ∫⁻ (a : α) in s, r * f a ∂μ

Tactic:
simp only [Pi.smul_apply, smul_eq_mul]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Fin.lean
@[simp]
lemma card_Ioo : #(Ioo a b) = b - a - 1

Proof state:
n : ℕ
a b : Fin n
⊢ #(Ioo a b) = ↑b - ↑a - 1

Tactic:
rw [← Nat.card_Ioo, ← map_valEmbedding_Ioo, card_map]

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Map.lean
@[simp]
lemma comap_neg {f : M →ₗ[R] M₂} {p : Submodule R M₂} :
    p.comap (-f) = p.comap f

Proof state:
R : Type u_1
M : Type u_5
M₂ : Type u_7
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
f : M →ₗ[R] M₂
p : Submodule R M₂
⊢ comap (-f) p = comap f p

Tactic:
ext

Result:
case h
R : Type u_1
M : Type u_5
M₂ : Type u_7
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
f : M →ₗ[R] M₂
p : Submodule R M₂
x✝ : M
⊢ x✝ ∈ comap (-f) p ↔ x✝ ∈ comap f p

Proof state:
case h
R : Type u_1
M : Type u_5
M₂ : Type u_7
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
f : M →ₗ[R] M₂
p : Submodule R M₂
x✝ : M
⊢ x✝ ∈ comap (-f) p ↔ x✝ ∈ comap f p

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Polynomial/SeparableDegree.lean
theorem _root_.Irreducible.hasSeparableContraction (q : ℕ) [hF : ExpChar F q] {f : F[X]}
    (irred : Irreducible f) : HasSeparableContraction q f

Proof state:
case prime.intro.intro.intro
F : Type u_1
inst✝ : Field F
q : ℕ
f : F[X]
irred : Irreducible f
hprime✝ : Nat.Prime q
hchar✝ : CharP F q
n : ℕ
g : F[X]
hgs : g.Separable
hge : (expand F (q ^ n)) g = f
⊢ HasSeparableContraction q f

Tactic:
exact ⟨g, hgs, n, hge⟩

Result:
no goals

Proof state:
F : Type u_1
inst✝ : Field F
q : ℕ
hF : ExpChar F q
f : F[X]
irred : Irreducible f
⊢ HasSeparableContraction q f

Tactic:
cases hF

Result:
case zero
F : Type u_1
inst✝¹ : Field F
f : F[X]
irred : Irreducible f
inst✝ : CharZero F
⊢ HasSeparableContraction 1 f

case prime
F : Type u_1
inst✝ : Field F
q : ℕ
f : F[X]
irred : Irreducible f
hprime✝ : Nat.Prime q
hchar✝ : CharP F q
⊢ HasSeparableContraction q f

Proof state:
case zero
F : Type u_1
inst✝¹ : Field F
f : F[X]
irred : Irreducible f
inst✝ : CharZero F
⊢ HasSeparableContraction 1 f

Tactic:
exact ⟨f, irred.separable, ⟨0, by rw [pow_zero, expand_one]⟩⟩

Result:
no goals

Proof state:
case prime
F : Type u_1
inst✝ : Field F
q : ℕ
f : F[X]
irred : Irreducible f
hprime✝ : Nat.Prime q
hchar✝ : CharP F q
⊢ HasSeparableContraction q f

Tactic:
rcases exists_separable_of_irreducible q irred ‹q.Prime›.ne_zero with ⟨n, g, hgs, hge⟩

Result:
case prime.intro.intro.intro
F : Type u_1
inst✝ : Field F
q : ℕ
f : F[X]
irred : Irreducible f
hprime✝ : Nat.Prime q
hchar✝ : CharP F q
n : ℕ
g : F[X]
hgs : g.Separable
hge : (expand F (q ^ n)) g = f
⊢ HasSeparableContraction q f

Proof state:
F : Type u_1
inst✝¹ : Field F
f : F[X]
irred : Irreducible f
inst✝ : CharZero F
⊢ (expand F (1 ^ 0)) f = f

Tactic:
rw [pow_zero, expand_one]

Result:
no goals
-- Mathlib/Analysis/Convex/Side.lean
theorem isConnected_setOf_sSameSide {s : AffineSubspace ℝ P} {x : P} (hx : x ∉ s)
    (h : (s : Set P).Nonempty) : IsConnected { y | s.SSameSide x y }

Proof state:
case intro
V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
hx : x ∉ s
p : P
hp : p ∈ ↑s
this : Nonempty ↥s
⊢ ConnectedSpace ↑↑s

Tactic:
convert AddTorsor.connectedSpace s.direction s

Result:
no goals

Proof state:
case intro
V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
hx : x ∉ s
p : P
hp : p ∈ ↑s
this : Nonempty ↥s
⊢ IsConnected {y | s.SSameSide x y}

Tactic:
rw [setOf_sSameSide_eq_image2 hx hp, ← Set.image_prod]

Result:
case intro
V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
hx : x ∉ s
p : P
hp : p ∈ ↑s
this : Nonempty ↥s
⊢ IsConnected ((fun x_1 => x_1.1 • (x -ᵥ p) +ᵥ x_1.2) '' Set.Ioi 0 ×ˢ ↑s)

Proof state:
case intro
V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
hx : x ∉ s
p : P
hp : p ∈ ↑s
⊢ IsConnected {y | s.SSameSide x y}

Tactic:
haveI : Nonempty s := ⟨⟨p, hp⟩⟩

Result:
case intro
V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
hx : x ∉ s
p : P
hp : p ∈ ↑s
this : Nonempty ↥s
⊢ IsConnected {y | s.SSameSide x y}

Proof state:
case intro
V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
hx : x ∉ s
p : P
hp : p ∈ ↑s
this : Nonempty ↥s
⊢ IsConnected ((fun x_1 => x_1.1 • (x -ᵥ p) +ᵥ x_1.2) '' Set.Ioi 0 ×ˢ ↑s)

Tactic:
refine (isConnected_Ioi.prod (isConnected_iff_connectedSpace.2 ?_)).image _
  ((continuous_fst.smul continuous_const).vadd continuous_snd).continuousOn

Result:
case intro
V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
hx : x ∉ s
p : P
hp : p ∈ ↑s
this : Nonempty ↥s
⊢ ConnectedSpace ↑↑s

Proof state:
V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
hx : x ∉ s
h : (↑s).Nonempty
⊢ IsConnected {y | s.SSameSide x y}

Tactic:
obtain ⟨p, hp⟩ := h

Result:
case intro
V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
hx : x ∉ s
p : P
hp : p ∈ ↑s
⊢ IsConnected {y | s.SSameSide x y}
-- Mathlib/Order/Filter/Bases.lean
theorem hasBasis_pure (x : α) :
    (pure x : Filter α).HasBasis (fun _ : Unit => True) fun _ => {x}

Proof state:
α : Type u_1
x : α
⊢ (pure x).HasBasis (fun x => True) fun x_1 => {x}

Tactic:
simp only [← principal_singleton, hasBasis_principal]

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/HasFiniteIntegral.lean
theorem lintegral_edist_triangle {f g h : α → β} (hf : AEStronglyMeasurable f μ)
    (hh : AEStronglyMeasurable h μ) :
    (∫⁻ a, edist (f a) (g a) ∂μ) ≤ (∫⁻ a, edist (f a) (h a) ∂μ) + ∫⁻ a, edist (g a) (h a) ∂μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g h : α → β
hf : AEStronglyMeasurable f μ
hh : AEStronglyMeasurable h μ
a : α
⊢ edist (f a) (g a) ≤ edist (f a) (h a) + edist (g a) (h a)

Tactic:
apply edist_triangle_right

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g h : α → β
hf : AEStronglyMeasurable f μ
hh : AEStronglyMeasurable h μ
⊢ ∫⁻ (a : α), edist (f a) (g a) ∂μ ≤ ∫⁻ (a : α), edist (f a) (h a) ∂μ + ∫⁻ (a : α), edist (g a) (h a) ∂μ

Tactic:
rw [← lintegral_add_left' (hf.edist hh)]

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g h : α → β
hf : AEStronglyMeasurable f μ
hh : AEStronglyMeasurable h μ
⊢ ∫⁻ (a : α), edist (f a) (g a) ∂μ ≤ ∫⁻ (a : α), edist (f a) (h a) + edist (g a) (h a) ∂μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g h : α → β
hf : AEStronglyMeasurable f μ
hh : AEStronglyMeasurable h μ
⊢ ∫⁻ (a : α), edist (f a) (g a) ∂μ ≤ ∫⁻ (a : α), edist (f a) (h a) + edist (g a) (h a) ∂μ

Tactic:
refine lintegral_mono fun a => ?_

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g h : α → β
hf : AEStronglyMeasurable f μ
hh : AEStronglyMeasurable h μ
a : α
⊢ edist (f a) (g a) ≤ edist (f a) (h a) + edist (g a) (h a)
-- Mathlib/Data/Finset/Sym.lean
theorem sym2_image [DecidableEq β] (f : α → β) (s : Finset α) :
    (s.image f).sym2 = s.sym2.image (Sym2.map f)

Proof state:
case a
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Finset α
⊢ (Multiset.map f s.val).dedup.sym2 = (Multiset.map (Sym2.map f) s.val.sym2).dedup

Tactic:
rw [← Multiset.dedup_sym2, Multiset.sym2_map]

Result:
no goals

Proof state:
case a
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Finset α
⊢ (image f s).sym2.val = (image (Sym2.map f) s.sym2).val

Tactic:
dsimp [Finset.sym2]

Result:
case a
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Finset α
⊢ (Multiset.map f s.val).dedup.sym2 = (Multiset.map (Sym2.map f) s.val.sym2).dedup

Proof state:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Finset α
⊢ (image f s).sym2 = image (Sym2.map f) s.sym2

Tactic:
apply val_injective

Result:
case a
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Finset α
⊢ (image f s).sym2.val = (image (Sym2.map f) s.sym2).val
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem zero_lt_sub_of_lt (h : i < a) : 0 < a - i

Proof state:
i a : Nat
h : i < a
⊢ 0 < a - i

Tactic:
induction a with
| zero => contradiction
| succ a ih =>
  match Nat.eq_or_lt_of_le h with
  | Or.inl h => injection h with h; subst h; rw [Nat.add_sub_self_left]; decide
  | Or.inr h =>
    have : 0 < a - i := ih (Nat.lt_of_succ_lt_succ h)
    exact Nat.lt_of_lt_of_le this (Nat.sub_le_succ_sub _ _)

Result:
no goals

Proof state:
i a : Nat
ih : i < a → 0 < a - i
h✝ : i < a + 1
h : i.succ < a + 1
this : 0 < a - i
⊢ 0 < a + 1 - i

Tactic:
exact Nat.lt_of_lt_of_le this (Nat.sub_le_succ_sub _ _)

Result:
no goals

Proof state:
case zero
i : Nat
h : i < 0
⊢ 0 < 0 - i

Tactic:
contradiction

Result:
no goals

Proof state:
i : Nat
ih : i < i → 0 < i - i
h : i < i + 1
⊢ 0 < 1

Tactic:
decide

Result:
no goals

Proof state:
i a : Nat
ih : i < a → 0 < a - i
h✝ : i < a + 1
h : i.succ < a + 1
⊢ 0 < a + 1 - i

Tactic:
have : 0 < a - i := ih (Nat.lt_of_succ_lt_succ h)

Result:
i a : Nat
ih : i < a → 0 < a - i
h✝ : i < a + 1
h : i.succ < a + 1
this : 0 < a - i
⊢ 0 < a + 1 - i

Proof state:
i a : Nat
ih : i < a → 0 < a - i
h✝ : i < a + 1
h : i.succ = a + 1
⊢ 0 < a + 1 - i

Tactic:
injection h with h

Result:
i a : Nat
ih : i < a → 0 < a - i
h✝ : i < a + 1
h : i = a
⊢ 0 < a + 1 - i

Proof state:
i a : Nat
ih : i < a → 0 < a - i
h✝ : i < a + 1
h : i = a
⊢ 0 < a + 1 - i

Tactic:
subst h

Result:
i : Nat
ih : i < i → 0 < i - i
h : i < i + 1
⊢ 0 < i + 1 - i

Proof state:
case succ
i a : Nat
ih : i < a → 0 < a - i
h : i < a + 1
⊢ 0 < a + 1 - i

Tactic:
match Nat.eq_or_lt_of_le h with
| Or.inl h => injection h with h; subst h; rw [Nat.add_sub_self_left]; decide
| Or.inr h =>
  have : 0 < a - i := ih (Nat.lt_of_succ_lt_succ h)
  exact Nat.lt_of_lt_of_le this (Nat.sub_le_succ_sub _ _)

Result:
no goals

Proof state:
i : Nat
ih : i < i → 0 < i - i
h : i < i + 1
⊢ 0 < i + 1 - i

Tactic:
rw [Nat.add_sub_self_left]

Result:
i : Nat
ih : i < i → 0 < i - i
h : i < i + 1
⊢ 0 < 1
-- Mathlib/Combinatorics/SimpleGraph/Prod.lean
theorem ofBoxProdLeft_boxProdRight [DecidableEq α] [DecidableRel G.Adj] {a b₁ b₂ : α} :
    ∀ (w : G.Walk b₁ b₂), (w.boxProdRight G a).ofBoxProdRight = w
  | nil => rfl
  | cons' x y z h w => by
    rw [Walk.boxProdRight, map_cons, ofBoxProdRight, Or.by_cases, dif_pos, ←
      Walk.boxProdRight]
    · simp [ofBoxProdLeft_boxProdRight]
    · exact ⟨h, rfl⟩

Proof state:
case hc
α : Type u_1
G : SimpleGraph α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a b₁ b₂ x z y : α
h : G.Adj x y
w : G.Walk y z
⊢ G.Adj (a, x).2 ((G.boxProdRight G a).toHom y).2 ∧ (a, x).1 = ((G.boxProdRight G a).toHom y).1

Tactic:
exact ⟨h, rfl⟩

Result:
no goals

Proof state:
α : Type u_1
G : SimpleGraph α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a b₁ b₂ x z y : α
h : G.Adj x y
w : G.Walk y z
⊢ cons ⋯ (Walk.boxProdRight G a w).ofBoxProdRight = cons' x y z h w

Tactic:
simp [ofBoxProdLeft_boxProdRight]

Result:
no goals

Proof state:
α : Type u_1
G : SimpleGraph α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a b₁ b₂ x z y : α
h : G.Adj x y
w : G.Walk y z
⊢ (Walk.boxProdRight G a (cons' x y z h w)).ofBoxProdRight = cons' x y z h w

Tactic:
rw [Walk.boxProdRight, map_cons, ofBoxProdRight, Or.by_cases, dif_pos, ←
  Walk.boxProdRight]

Result:
α : Type u_1
G : SimpleGraph α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a b₁ b₂ x z y : α
h : G.Adj x y
w : G.Walk y z
⊢ cons ⋯ (Walk.boxProdRight G a w).ofBoxProdRight = cons' x y z h w

case hc
α : Type u_1
G : SimpleGraph α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a b₁ b₂ x z y : α
h : G.Adj x y
w : G.Walk y z
⊢ G.Adj (a, x).2 ((G.boxProdRight G a).toHom y).2 ∧ (a, x).1 = ((G.boxProdRight G a).toHom y).1
-- Mathlib/CategoryTheory/Monoidal/Preadditive.lean
theorem tensor_sum {P Q R S : C} {J : Type*} (s : Finset J) (f : P ⟶ Q) (g : J → (R ⟶ S)) :
    (f ⊗ ∑ j ∈ s, g j) = ∑ j ∈ s, f ⊗ g j

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalPreadditive C
P Q R S : C
J : Type u_2
s : Finset J
f : P ⟶ Q
g : J → (R ⟶ S)
⊢ f ⊗ ∑ j ∈ s, g j = ∑ j ∈ s, f ⊗ g j

Tactic:
simp only [tensorHom_def, whiskerLeft_sum, Preadditive.comp_sum]

Result:
no goals