harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/Enumerative/Composition.lean
theorem length_pos_of_mem_splitWrtComposition {l l' : List α} {c : Composition l.length}
    (h : l' ∈ l.splitWrtComposition c) : 0 < length l'

Proof state:
α : Type u_1
l l' : List α
c : Composition l.length
h : l' ∈ l.splitWrtComposition c
this : l'.length ∈ map length (l.splitWrtComposition c)
⊢ 0 < l'.length

Tactic:
rw [map_length_splitWrtComposition] at this

Result:
α : Type u_1
l l' : List α
c : Composition l.length
h : l' ∈ l.splitWrtComposition c
this : l'.length ∈ c.blocks
⊢ 0 < l'.length

Proof state:
α : Type u_1
l l' : List α
c : Composition l.length
h : l' ∈ l.splitWrtComposition c
⊢ 0 < l'.length

Tactic:
have : l'.length ∈ (l.splitWrtComposition c).map List.length :=
  List.mem_map_of_mem List.length h

Result:
α : Type u_1
l l' : List α
c : Composition l.length
h : l' ∈ l.splitWrtComposition c
this : l'.length ∈ map length (l.splitWrtComposition c)
⊢ 0 < l'.length

Proof state:
α : Type u_1
l l' : List α
c : Composition l.length
h : l' ∈ l.splitWrtComposition c
this : l'.length ∈ c.blocks
⊢ 0 < l'.length

Tactic:
exact c.blocks_pos this

Result:
no goals
-- Mathlib/Probability/Distributions/Uniform.lean
theorem toMeasurable_iff {X : Ω → E} {s : Set E} :
    IsUniform X (toMeasurable μ s) ℙ μ ↔ IsUniform X s ℙ μ

Proof state:
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
⊢ IsUniform X (toMeasurable μ s) ℙ μ ↔ IsUniform X s ℙ μ

Tactic:
unfold IsUniform

Result:
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
⊢ Measure.map X ℙ = ProbabilityTheory.cond μ (toMeasurable μ s) ↔ Measure.map X ℙ = ProbabilityTheory.cond μ s

Proof state:
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
⊢ Measure.map X ℙ = ProbabilityTheory.cond μ (toMeasurable μ s) ↔ Measure.map X ℙ = ProbabilityTheory.cond μ s

Tactic:
rw [ProbabilityTheory.cond_toMeasurable_eq]

Result:
no goals
-- Mathlib/Order/Heyting/Basic.lean
theorem sup_sdiff_left_self : (a ⊔ b) \ a = b \ a

Proof state:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ (a ⊔ b) \ a = b \ a

Tactic:
rw [sup_comm, sup_sdiff_right_self]

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
theorem mul_zero [Fintype n] (M : Matrix m n α) : M * (0 : Matrix n o α) = 0

Proof state:
case a
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
M : Matrix m n α
i✝ : m
j✝ : o
⊢ (M * 0) i✝ j✝ = 0 i✝ j✝

Tactic:
apply dotProduct_zero

Result:
no goals

Proof state:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
M : Matrix m n α
⊢ M * 0 = 0

Tactic:
ext

Result:
case a
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
M : Matrix m n α
i✝ : m
j✝ : o
⊢ (M * 0) i✝ j✝ = 0 i✝ j✝
-- Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean
theorem map_id (M : CStarMatrix m n A) : M.map id = M

Proof state:
m : Type u_1
n : Type u_2
A : Type u_3
M : CStarMatrix m n A
⊢ M.map id = M

Tactic:
ext

Result:
case h
m : Type u_1
n : Type u_2
A : Type u_3
M : CStarMatrix m n A
i✝ : m
j✝ : n
⊢ M.map id i✝ j✝ = M i✝ j✝

Proof state:
case h
m : Type u_1
n : Type u_2
A : Type u_3
M : CStarMatrix m n A
i✝ : m
j✝ : n
⊢ M.map id i✝ j✝ = M i✝ j✝

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/TruncLEHomology.lean
lemma quasiIsoAt_ιTruncLE {j : ι} {j' : ι'} (hj' : e.f j = j') :
    QuasiIsoAt (K.ιTruncLE e) j'

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{u_4, u_3} C
inst✝³ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsTruncLE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : HasZeroObject C
j : ι
j' : ι'
hj' : e.f j = j'
⊢ QuasiIsoAt (K.ιTruncLE e) j'

Tactic:
have := K.op.quasiIsoAt_πTruncGE e.op hj'

Result:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{u_4, u_3} C
inst✝³ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsTruncLE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : HasZeroObject C
j : ι
j' : ι'
hj' : e.f j = j'
this : QuasiIsoAt (K.op.πTruncGE e.op) j'
⊢ QuasiIsoAt (K.ιTruncLE e) j'

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{u_4, u_3} C
inst✝³ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsTruncLE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : HasZeroObject C
j : ι
j' : ι'
hj' : e.f j = j'
this : QuasiIsoAt (K.op.πTruncGE e.op) j'
⊢ QuasiIsoAt (K.ιTruncLE e) j'

Tactic:
exact inferInstanceAs (QuasiIsoAt ((unopFunctor _ _ ).map (K.op.πTruncGE e.op).op) j')

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Symmetric/NewtonIdentities.lean
theorem esymm_summand_to_weight (k : ℕ) (A : Finset σ) (h : A ∈ powersetCard k univ) :
    ∑ j ∈ A, weight σ R k (A, j) = k * (-1) ^ k * (∏ i ∈ A, X i : MvPolynomial σ R)

Proof state:
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype σ
k : ℕ
A : Finset σ
h : A ∈ powersetCard k univ
⊢ ∑ j ∈ A, MvPolynomial.NewtonIdentities.weight σ R k (A, j) = ↑k * (-1) ^ k * ∏ i ∈ A, X i

Tactic:
simp [weight, mem_powersetCard_univ.mp h, mul_assoc]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/Basic.lean
theorem norm_star_mul_self {x : E} : ‖x⋆ * x‖ = ‖x‖ * ‖x‖ :=
  le_antisymm ((norm_mul_le _ _).trans (by rw [norm_star])) (CStarRing.norm_mul_self_le x)

Proof state:
E : Type u_2
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
x : E
⊢ ‖x⋆‖ * ‖x‖ ≤ ‖x‖ * ‖x‖

Tactic:
rw [norm_star]

Result:
no goals
-- Mathlib/Topology/ContinuousMap/CompactlySupported.lean
@[simp] lemma toReal_smul (r : ℝ≥0) (f : C_c(α, ℝ≥0)) : (r • f).toReal = r • f.toReal

Proof state:
α : Type u_2
inst✝ : TopologicalSpace α
r : ℝ≥0
f : α →C_c ℝ≥0
⊢ (r • f).toReal = r • f.toReal

Tactic:
ext

Result:
case h
α : Type u_2
inst✝ : TopologicalSpace α
r : ℝ≥0
f : α →C_c ℝ≥0
x✝ : α
⊢ (r • f).toReal x✝ = (r • f.toReal) x✝

Proof state:
case h
α : Type u_2
inst✝ : TopologicalSpace α
r : ℝ≥0
f : α →C_c ℝ≥0
x✝ : α
⊢ (r • f).toReal x✝ = (r • f.toReal) x✝

Tactic:
simp [NNReal.smul_def]

Result:
no goals
-- Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
theorem tendsto_translation_number₀' :
    Tendsto (fun n : ℕ => (f ^ (n + 1) : CircleDeg1Lift) 0 / ((n : ℝ) + 1)) atTop (𝓝 <| τ f)

Proof state:
f : CircleDeg1Lift
n : ℕ
⊢ dist ((f ^ (n + 1)) 0 / (↑n + 1)) (τ f) ≤ ((fun n => 1 / ↑n) ∘ fun a => a + 1) n

Tactic:
dsimp

Result:
f : CircleDeg1Lift
n : ℕ
⊢ dist ((f ^ (n + 1)) 0 / (↑n + 1)) (τ f) ≤ 1 / ↑(n + 1)

Proof state:
f : CircleDeg1Lift
n : ℕ
this : 0 < ↑n + 1
⊢ dist ((f ^ (n + 1)) 0) (↑(n + 1) * τ f) ≤ 1

Tactic:
apply dist_pow_map_zero_mul_translationNumber_le

Result:
no goals

Proof state:
f : CircleDeg1Lift
n : ℕ
this : 0 < ↑n + 1
⊢ dist ((f ^ (n + 1)) 0 / (↑n + 1)) (τ f) ≤ 1 / ↑(n + 1)

Tactic:
rw [Real.dist_eq, div_sub' (ne_of_gt this), abs_div, ← Real.dist_eq, abs_of_pos this,
  Nat.cast_add_one, div_le_div_iff_of_pos_right this, ← Nat.cast_add_one]

Result:
f : CircleDeg1Lift
n : ℕ
this : 0 < ↑n + 1
⊢ dist ((f ^ (n + 1)) 0) (↑(n + 1) * τ f) ≤ 1

Proof state:
f : CircleDeg1Lift
⊢ Tendsto (fun n => (f ^ (n + 1)) 0 / (↑n + 1)) atTop (𝓝 (τ f))

Tactic:
refine
  tendsto_iff_dist_tendsto_zero.2 <|
    squeeze_zero (fun _ => dist_nonneg) (fun n => ?_)
      ((tendsto_const_div_atTop_nhds_zero_nat 1).comp (tendsto_add_atTop_nat 1))

Result:
f : CircleDeg1Lift
n : ℕ
⊢ dist ((f ^ (n + 1)) 0 / (↑n + 1)) (τ f) ≤ ((fun n => 1 / ↑n) ∘ fun a => a + 1) n

Proof state:
f : CircleDeg1Lift
n : ℕ
⊢ dist ((f ^ (n + 1)) 0 / (↑n + 1)) (τ f) ≤ 1 / ↑(n + 1)

Tactic:
have : (0 : ℝ) < n + 1 := n.cast_add_one_pos

Result:
f : CircleDeg1Lift
n : ℕ
this : 0 < ↑n + 1
⊢ dist ((f ^ (n + 1)) 0 / (↑n + 1)) (τ f) ≤ 1 / ↑(n + 1)
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem data_dropWhile (p : Char → Bool) (s : String) :
    (s.dropWhile p).1 = s.1.dropWhile p

Proof state:
p : Char → Bool
s : String
⊢ (s.dropWhile p).data = List.dropWhile p s.data

Tactic:
rw [dropWhile_eq]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/BinaryEntropy.lean
lemma binEntropy_eq_zero : binEntropy p = 0 ↔ p = 0 ∨ p = 1

Proof state:
case inr
p : ℝ
h : p ≠ 0 ∧ p ≠ 1
hp₀ : 0 < p
⊢ binEntropy p ≠ 0

Tactic:
obtain hp₁ | hp₁ := h.2.lt_or_lt.symm

Result:
case inr.inl
p : ℝ
h : p ≠ 0 ∧ p ≠ 1
hp₀ : 0 < p
hp₁ : 1 < p
⊢ binEntropy p ≠ 0

case inr.inr
p : ℝ
h : p ≠ 0 ∧ p ≠ 1
hp₀ : 0 < p
hp₁ : p < 1
⊢ binEntropy p ≠ 0

Proof state:
case inl
p : ℝ
h : p ≠ 0 ∧ p ≠ 1
hp₀ : p < 0
⊢ binEntropy p ≠ 0

Tactic:
exact (binEntropy_neg_of_neg hp₀).ne

Result:
no goals

Proof state:
p : ℝ
⊢ binEntropy p = 0 ↔ p = 0 ∨ p = 1

Tactic:
refine ⟨fun h ↦ ?_, by rintro (rfl | rfl) <;> simp⟩

Result:
p : ℝ
h : binEntropy p = 0
⊢ p = 0 ∨ p = 1

Proof state:
case inr.inr
p : ℝ
h : p ≠ 0 ∧ p ≠ 1
hp₀ : 0 < p
hp₁ : p < 1
⊢ binEntropy p ≠ 0

Tactic:
exact (binEntropy_pos hp₀ hp₁).ne'

Result:
no goals

Proof state:
p : ℝ
⊢ p = 0 ∨ p = 1 → binEntropy p = 0

Tactic:
rintro (rfl | rfl) <;> simp

Result:
no goals

Proof state:
case inr.inl
p : ℝ
h : p ≠ 0 ∧ p ≠ 1
hp₀ : 0 < p
hp₁ : 1 < p
⊢ binEntropy p ≠ 0

Tactic:
exact (binEntropy_neg_of_one_lt hp₁).ne

Result:
no goals

Proof state:
p : ℝ
h : p ≠ 0 ∧ p ≠ 1
⊢ binEntropy p ≠ 0

Tactic:
obtain hp₀ | hp₀ := h.1.lt_or_lt

Result:
case inl
p : ℝ
h : p ≠ 0 ∧ p ≠ 1
hp₀ : p < 0
⊢ binEntropy p ≠ 0

case inr
p : ℝ
h : p ≠ 0 ∧ p ≠ 1
hp₀ : 0 < p
⊢ binEntropy p ≠ 0

Proof state:
p : ℝ
h : binEntropy p = 0
⊢ p = 0 ∨ p = 1

Tactic:
contrapose! h

Result:
p : ℝ
h : p ≠ 0 ∧ p ≠ 1
⊢ binEntropy p ≠ 0
-- Mathlib/Algebra/Order/Group/PosPart.lean
@[to_additive] lemma inf_eq_div_oneLePart_div (a b : α) : a ⊓ b = a / (a / b)⁺ᵐ

Proof state:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ a ⊓ b = a / (a / b)⁺ᵐ

Tactic:
simp [oneLePart, div_sup, inf_comm]

Result:
no goals
-- Mathlib/Order/WithBot.lean
theorem unbotD_eq_iff {d y : α} {x : WithBot α} : unbotD d x = y ↔ x = y ∨ x = ⊥ ∧ y = d

Proof state:
α : Type u_1
d y : α
x : WithBot α
⊢ unbotD d x = y ↔ x = ↑y ∨ x = ⊥ ∧ y = d

Tactic:
induction x <;> simp [@eq_comm _ d]

Result:
no goals
-- Mathlib/Analysis/Calculus/DSlope.lean
theorem ContinuousLinearMap.dslope_comp {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
    (f : E →L[𝕜] F) (g : 𝕜 → E) (a b : 𝕜) (H : a = b → DifferentiableAt 𝕜 g a) :
    dslope (f ∘ g) a b = f (dslope g a b)

Proof state:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E →L[𝕜] F
g : 𝕜 → E
a b : 𝕜
H : a = b → DifferentiableAt 𝕜 g a
hne : b ≠ a
⊢ dslope (⇑f ∘ g) a b = f (dslope g a b)

Tactic:
simpa only [dslope_of_ne _ hne] using f.toLinearMap.slope_comp g a b

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E →L[𝕜] F
g : 𝕜 → E
a b : 𝕜
H : a = b → DifferentiableAt 𝕜 g a
⊢ dslope (⇑f ∘ g) a b = f (dslope g a b)

Tactic:
rcases eq_or_ne b a with (rfl | hne)

Result:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E →L[𝕜] F
g : 𝕜 → E
b : 𝕜
H : b = b → DifferentiableAt 𝕜 g b
⊢ dslope (⇑f ∘ g) b b = f (dslope g b b)

case inr
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E →L[𝕜] F
g : 𝕜 → E
a b : 𝕜
H : a = b → DifferentiableAt 𝕜 g a
hne : b ≠ a
⊢ dslope (⇑f ∘ g) a b = f (dslope g a b)

Proof state:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E →L[𝕜] F
g : 𝕜 → E
b : 𝕜
H : b = b → DifferentiableAt 𝕜 g b
⊢ deriv (⇑f ∘ g) b = f (deriv g b)

Tactic:
exact (f.hasFDerivAt.comp_hasDerivAt b (H rfl).hasDerivAt).deriv

Result:
no goals

Proof state:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E →L[𝕜] F
g : 𝕜 → E
b : 𝕜
H : b = b → DifferentiableAt 𝕜 g b
⊢ dslope (⇑f ∘ g) b b = f (dslope g b b)

Tactic:
simp only [dslope_same]

Result:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E →L[𝕜] F
g : 𝕜 → E
b : 𝕜
H : b = b → DifferentiableAt 𝕜 g b
⊢ deriv (⇑f ∘ g) b = f (deriv g b)
-- Mathlib/Data/Stream/Init.lean
theorem mem_interleave_left {a : α} {s₁ : Stream' α} (s₂ : Stream' α) : a ∈ s₁ → a ∈ s₁ ⋈ s₂ :=
  fun ⟨n, h⟩ => Exists.intro (2 * n) (by rw [h, get_interleave_left])

Proof state:
α : Type u
a : α
s₁ s₂ : Stream' α
x✝ : a ∈ s₁
n : ℕ
h : (fun b => a = b) (s₁.get n)
⊢ (fun b => a = b) ((s₁ ⋈ s₂).get (2 * n))

Tactic:
rw [h, get_interleave_left]

Result:
no goals
-- Mathlib/Algebra/Order/Module/Defs.lean
lemma smul_nonneg [PosSMulMono α β] (ha : 0 ≤ a) (hb : 0 ≤ b₁) : 0 ≤ a • b₁

Proof state:
α : Type u_1
β : Type u_2
a : α
b₁ : β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMulZeroClass α β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : PosSMulMono α β
ha : 0 ≤ a
hb : 0 ≤ b₁
⊢ 0 ≤ a • b₁

Tactic:
simpa only [smul_zero] using smul_le_smul_of_nonneg_left hb ha

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem coeSucc_eq_succ {a : Fin n} : a.castSucc + 1 = a.succ

Proof state:
case succ
n✝ : Nat
a : Fin (n✝ + 1)
⊢ a.castSucc + 1 = a.succ

Tactic:
simp [Fin.ext_iff, add_def, Nat.mod_eq_of_lt (Nat.succ_lt_succ a.is_lt)]

Result:
no goals

Proof state:
n : Nat
a : Fin n
⊢ a.castSucc + 1 = a.succ

Tactic:
cases n

Result:
case zero
a : Fin 0
⊢ a.castSucc + 1 = a.succ

case succ
n✝ : Nat
a : Fin (n✝ + 1)
⊢ a.castSucc + 1 = a.succ

Proof state:
case zero
a : Fin 0
⊢ a.castSucc + 1 = a.succ

Tactic:
exact a.elim0

Result:
no goals
-- Mathlib/Order/PartialSups.lean
theorem partialSups_succ [LinearOrder ι] [LocallyFiniteOrderBot ι] [SuccOrder ι]
    (f : ι → α) (i : ι) :
    partialSups f (Order.succ i) = partialSups f i ⊔ f (Order.succ i)

Proof state:
α : Type u_1
ι : Type u_2
inst✝³ : SemilatticeSup α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
i : ι
⊢ (partialSups f) (Order.succ i) = (partialSups f) i ⊔ f (Order.succ i)

Tactic:
suffices Iic (Order.succ i) = Iic i ∪ {Order.succ i} by simp only [partialSups_apply, this,
  sup'_union nonempty_Iic ⟨_, mem_singleton_self _⟩ f, sup'_singleton]

Result:
α : Type u_1
ι : Type u_2
inst✝³ : SemilatticeSup α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
i : ι
⊢ Iic (Order.succ i) = Iic i ∪ {Order.succ i}

Proof state:
α : Type u_1
ι : Type u_2
inst✝³ : SemilatticeSup α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
i : ι
⊢ Iic (Order.succ i) = Iic i ∪ {Order.succ i}

Tactic:
ext

Result:
case h
α : Type u_1
ι : Type u_2
inst✝³ : SemilatticeSup α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
i a✝ : ι
⊢ a✝ ∈ Iic (Order.succ i) ↔ a✝ ∈ Iic i ∪ {Order.succ i}

Proof state:
α : Type u_1
ι : Type u_2
inst✝³ : SemilatticeSup α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
i : ι
this : Iic (Order.succ i) = Iic i ∪ {Order.succ i}
⊢ (partialSups f) (Order.succ i) = (partialSups f) i ⊔ f (Order.succ i)

Tactic:
simp only [partialSups_apply, this,
sup'_union nonempty_Iic ⟨_, mem_singleton_self _⟩ f, sup'_singleton]

Result:
no goals

Proof state:
case h.mp
α : Type u_1
ι : Type u_2
inst✝³ : SemilatticeSup α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
i a✝ : ι
⊢ a✝ ≤ Order.succ i → a✝ ≤ i ∨ a✝ = Order.succ i

Tactic:
exact fun h ↦ (Order.le_succ_iff_eq_or_le.mp h).symm

Result:
no goals

Proof state:
case h
α : Type u_1
ι : Type u_2
inst✝³ : SemilatticeSup α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
i a✝ : ι
⊢ a✝ ≤ Order.succ i ↔ a✝ ≤ i ∨ a✝ = Order.succ i

Tactic:
constructor

Result:
case h.mp
α : Type u_1
ι : Type u_2
inst✝³ : SemilatticeSup α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
i a✝ : ι
⊢ a✝ ≤ Order.succ i → a✝ ≤ i ∨ a✝ = Order.succ i

case h.mpr
α : Type u_1
ι : Type u_2
inst✝³ : SemilatticeSup α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
i a✝ : ι
⊢ a✝ ≤ i ∨ a✝ = Order.succ i → a✝ ≤ Order.succ i

Proof state:
case h
α : Type u_1
ι : Type u_2
inst✝³ : SemilatticeSup α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
i a✝ : ι
⊢ a✝ ∈ Iic (Order.succ i) ↔ a✝ ∈ Iic i ∪ {Order.succ i}

Tactic:
simp only [mem_Iic, mem_union, mem_singleton]

Result:
case h
α : Type u_1
ι : Type u_2
inst✝³ : SemilatticeSup α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
i a✝ : ι
⊢ a✝ ≤ Order.succ i ↔ a✝ ≤ i ∨ a✝ = Order.succ i
-- Mathlib/Algebra/BigOperators/Group/List/Basic.lean
theorem prod_drop_succ :
    ∀ (L : List G) (i : ℕ) (p : i < L.length), (L.drop (i + 1)).prod = L[i]⁻¹ * (L.drop i).prod
  | [], _, p => False.elim (Nat.not_lt_zero _ p)
  | _ :: _, 0, _ => by simp
  | _ :: xs, i + 1, p => prod_drop_succ xs i (Nat.lt_of_succ_lt_succ p)

Proof state:
G : Type u_7
inst✝ : Group G
head✝ : G
tail✝ : List G
x✝ : 0 < (head✝ :: tail✝).length
⊢ (drop (0 + 1) (head✝ :: tail✝)).prod = (head✝ :: tail✝)[0]⁻¹ * (drop 0 (head✝ :: tail✝)).prod

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem castNum_and : ∀ m n : Num, ↑(m &&& n) = (↑m &&& ↑n : ℕ)

Proof state:
case pbb
a✝ b✝ : Bool
m✝ n✝ : PosNum
⊢ (PosNum.bit a✝ m✝).land (PosNum.bit b✝ n✝) = bit (a✝ && b✝) (m✝.land n✝)

Tactic:
try cases_type* Bool

Result:
case pbb.false.false
m✝ n✝ : PosNum
⊢ (PosNum.bit false m✝).land (PosNum.bit false n✝) = bit (false && false) (m✝.land n✝)

case pbb.false.true
m✝ n✝ : PosNum
⊢ (PosNum.bit false m✝).land (PosNum.bit true n✝) = bit (false && true) (m✝.land n✝)

case pbb.true.false
m✝ n✝ : PosNum
⊢ (PosNum.bit true m✝).land (PosNum.bit false n✝) = bit (true && false) (m✝.land n✝)

case pbb.true.true
m✝ n✝ : PosNum
⊢ (PosNum.bit true m✝).land (PosNum.bit true n✝) = bit (true && true) (m✝.land n✝)

Proof state:
⊢ ∀ (m n : Num), ↑(m &&& n) = ↑m &&& ↑n

Tactic:
apply castNum_eq_bitwise PosNum.land <;> intros <;> (try cases_type* Bool) <;> rfl

Result:
no goals

Proof state:
case pbb
a✝ b✝ : Bool
m✝ n✝ : PosNum
⊢ (PosNum.bit a✝ m✝).land (PosNum.bit b✝ n✝) = bit (a✝ && b✝) (m✝.land n✝)

Tactic:
cases_type* Bool

Result:
case pbb.false.false
m✝ n✝ : PosNum
⊢ (PosNum.bit false m✝).land (PosNum.bit false n✝) = bit (false && false) (m✝.land n✝)

case pbb.false.true
m✝ n✝ : PosNum
⊢ (PosNum.bit false m✝).land (PosNum.bit true n✝) = bit (false && true) (m✝.land n✝)

case pbb.true.false
m✝ n✝ : PosNum
⊢ (PosNum.bit true m✝).land (PosNum.bit false n✝) = bit (true && false) (m✝.land n✝)

case pbb.true.true
m✝ n✝ : PosNum
⊢ (PosNum.bit true m✝).land (PosNum.bit true n✝) = bit (true && true) (m✝.land n✝)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem filter_eq_self {l} : filter p l = l ↔ ∀ a ∈ l, p a

Proof state:
case cons.false
α✝ : Type u_1
p : α✝ → Bool
a : α✝
l : List α✝
ih : filter p l = l ↔ ∀ (a : α✝), a ∈ l → p a = true
h✝ : p a = false
h : filter p l = a :: l
⊢ False

Tactic:
exact Nat.lt_irrefl _ (h ▸ length_filter_le p l)

Result:
no goals

Proof state:
case cons.false
α✝ : Type u_1
p : α✝ → Bool
a : α✝
l : List α✝
ih : filter p l = l ↔ ∀ (a : α✝), a ∈ l → p a = true
h : p a = false
⊢ ¬filter p l = a :: l

Tactic:
intro h

Result:
case cons.false
α✝ : Type u_1
p : α✝ → Bool
a : α✝
l : List α✝
ih : filter p l = l ↔ ∀ (a : α✝), a ∈ l → p a = true
h✝ : p a = false
h : filter p l = a :: l
⊢ False

Proof state:
case cons
α✝ : Type u_1
p : α✝ → Bool
a : α✝
l : List α✝
ih : filter p l = l ↔ ∀ (a : α✝), a ∈ l → p a = true
⊢ filter p (a :: l) = a :: l ↔ p a = true ∧ ∀ (a : α✝), a ∈ l → p a = true

Tactic:
cases h : p a <;> simp [*]

Result:
case cons.false
α✝ : Type u_1
p : α✝ → Bool
a : α✝
l : List α✝
ih : filter p l = l ↔ ∀ (a : α✝), a ∈ l → p a = true
h : p a = false
⊢ ¬filter p l = a :: l

Proof state:
α✝ : Type u_1
p : α✝ → Bool
l : List α✝
⊢ filter p l = l ↔ ∀ (a : α✝), a ∈ l → p a = true

Tactic:
induction l with simp
| cons a l ih =>
  cases h : p a <;> simp [*]
  intro h; exact Nat.lt_irrefl _ (h ▸ length_filter_le p l)

Result:
no goals
-- Mathlib/Algebra/Module/Basic.lean
lemma indicator_smul_apply_left (s : Set α) (r : α → R) (f : α → M) (a : α) :
    indicator s (fun a ↦ r a • f a) a = indicator s r a • f a

Proof state:
case pos
α : Type u_1
R : Type u_2
M : Type u_3
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : SMulWithZero R M
s : Set α
r : α → R
f : α → M
a : α
h✝ : a ∈ s
⊢ r a • f a = r a • f a

case neg
α : Type u_1
R : Type u_2
M : Type u_3
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : SMulWithZero R M
s : Set α
r : α → R
f : α → M
a : α
h✝ : a ∉ s
⊢ 0 = 0 • f a

Tactic:
exacts [rfl, (zero_smul _ (f a)).symm]

Result:
no goals

Proof state:
α : Type u_1
R : Type u_2
M : Type u_3
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : SMulWithZero R M
s : Set α
r : α → R
f : α → M
a : α
⊢ s.indicator (fun a => r a • f a) a = s.indicator r a • f a

Tactic:
dsimp only [indicator]

Result:
α : Type u_1
R : Type u_2
M : Type u_3
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : SMulWithZero R M
s : Set α
r : α → R
f : α → M
a : α
⊢ (if a ∈ s then r a • f a else 0) = (if a ∈ s then r a else 0) • f a

Proof state:
α : Type u_1
R : Type u_2
M : Type u_3
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : SMulWithZero R M
s : Set α
r : α → R
f : α → M
a : α
⊢ (if a ∈ s then r a • f a else 0) = (if a ∈ s then r a else 0) • f a

Tactic:
split_ifs

Result:
case pos
α : Type u_1
R : Type u_2
M : Type u_3
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : SMulWithZero R M
s : Set α
r : α → R
f : α → M
a : α
h✝ : a ∈ s
⊢ r a • f a = r a • f a

case neg
α : Type u_1
R : Type u_2
M : Type u_3
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : SMulWithZero R M
s : Set α
r : α → R
f : α → M
a : α
h✝ : a ∉ s
⊢ 0 = 0 • f a
-- Mathlib/CategoryTheory/Limits/Shapes/Types.lean
@[simp]
lemma sectionsEquiv_apply_val (s : I.sections) (i : J.L) :
    c.ι i (sectionsEquiv hc s) = s.val i

Proof state:
case intro
J : MulticospanShape
I : MulticospanIndex J (Type u)
c : Multifork I
hc : IsLimit c
i : J.L
x : c.pt
⊢ c.ι i ((sectionsEquiv hc) ((sectionsEquiv hc).symm x)) = ((sectionsEquiv hc).symm x).val i

Tactic:
simp

Result:
no goals

Proof state:
J : MulticospanShape
I : MulticospanIndex J (Type u)
c : Multifork I
hc : IsLimit c
s : I.sections
i : J.L
⊢ c.ι i ((sectionsEquiv hc) s) = s.val i

Tactic:
obtain ⟨x, rfl⟩ := (sectionsEquiv hc).symm.surjective s

Result:
case intro
J : MulticospanShape
I : MulticospanIndex J (Type u)
c : Multifork I
hc : IsLimit c
i : J.L
x : c.pt
⊢ c.ι i ((sectionsEquiv hc) ((sectionsEquiv hc).symm x)) = ((sectionsEquiv hc).symm x).val i