harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Dual.lean
theorem sum_dual_apply_smul_coord (f : Module.Dual R M) :
    (∑ x, f (b x) • b.coord x) = f

Proof state:
case h
R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Fintype ι
b : Basis ι R M
f : Dual R M
m : M
⊢ (∑ x : ι, f (b x) • b.coord x) m = f m

Tactic:
simp_rw [LinearMap.sum_apply, LinearMap.smul_apply, smul_eq_mul, mul_comm (f _), ← smul_eq_mul, ←
  f.map_smul, ← _root_.map_sum, Basis.coord_apply, Basis.sum_repr]

Result:
no goals

Proof state:
R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Fintype ι
b : Basis ι R M
f : Dual R M
⊢ ∑ x : ι, f (b x) • b.coord x = f

Tactic:
ext m

Result:
case h
R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Fintype ι
b : Basis ι R M
f : Dual R M
m : M
⊢ (∑ x : ι, f (b x) • b.coord x) m = f m
-- Mathlib/Data/List/Zip.lean
theorem reverse_revzip (l : List α) : reverse l.revzip = revzip l.reverse

Proof state:
α : Type u
l : List α
⊢ l.revzip.reverse = l.reverse.revzip

Tactic:
rw [← zip_unzip (revzip l).reverse]

Result:
α : Type u
l : List α
⊢ l.revzip.reverse.unzip.fst.zip l.revzip.reverse.unzip.snd = l.reverse.revzip

Proof state:
α : Type u
l : List α
⊢ l.revzip.reverse.unzip.fst.zip l.revzip.reverse.unzip.snd = l.reverse.revzip

Tactic:
simp [unzip_eq_map, revzip, map_reverse, map_fst_zip, map_snd_zip]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/Constraint.lean
theorem bmod_sat (m : Nat) (r : Int) (i : Nat) (x v : Coeffs)
    (h : x.length ≤ i)  -- during proof reconstruction this will be by `decide`
    (p : Coeffs.get v i = bmod_div_term m x v) -- and this will be by `rfl`
    (w : (Constraint.exact r).sat' x v) :
    (Constraint.exact (Int.bmod r m)).sat' (bmod_coeffs m i x) v

Proof state:
m : Nat
r : Int
i : Nat
x v : Coeffs
h : x.length ≤ i
p : v.get i = bmod_div_term m x v
w : r = x.dot v
⊢ r.bmod m = (x.bmod m).dot v + (↑m - (x.bmod m).get i) * bmod_div_term m x v

Tactic:
replace h := Nat.le_trans (Coeffs.bmod_length x m) h

Result:
m : Nat
r : Int
i : Nat
x v : Coeffs
p : v.get i = bmod_div_term m x v
w : r = x.dot v
h : (x.bmod m).length ≤ i
⊢ r.bmod m = (x.bmod m).dot v + (↑m - (x.bmod m).get i) * bmod_div_term m x v

Proof state:
m : Nat
r : Int
i : Nat
x v : Coeffs
p : v.get i = bmod_div_term m x v
w : r = x.dot v
h : (x.bmod m).length ≤ i
⊢ r.bmod m = (x.bmod m).dot v + (↑m - (x.bmod m).get i) * bmod_div_term m x v

Tactic:
rw [Coeffs.get_of_length_le h, Int.sub_zero,
  Int.mul_ediv_cancel' (Coeffs.dvd_bmod_dot_sub_dot_bmod _ _ _), w,
  ← Int.add_sub_assoc, Int.add_comm, Int.add_sub_assoc, Int.sub_self, Int.add_zero]

Result:
no goals

Proof state:
m : Nat
r : Int
i : Nat
x v : Coeffs
h : x.length ≤ i
p : v.get i = bmod_div_term m x v
w : r = x.dot v
⊢ (Constraint.exact (r.bmod m)).sat' (bmod_coeffs m i x) v = true

Tactic:
simp only [p, bmod_coeffs, Constraint.exact_sat, Coeffs.dot_set_left, decide_eq_true_eq]

Result:
m : Nat
r : Int
i : Nat
x v : Coeffs
h : x.length ≤ i
p : v.get i = bmod_div_term m x v
w : r = x.dot v
⊢ r.bmod m = (x.bmod m).dot v + (↑m - (x.bmod m).get i) * bmod_div_term m x v

Proof state:
m : Nat
r : Int
i : Nat
x v : Coeffs
h : x.length ≤ i
p : v.get i = bmod_div_term m x v
w : (Constraint.exact r).sat' x v = true
⊢ (Constraint.exact (r.bmod m)).sat' (bmod_coeffs m i x) v = true

Tactic:
simp at w

Result:
m : Nat
r : Int
i : Nat
x v : Coeffs
h : x.length ≤ i
p : v.get i = bmod_div_term m x v
w : r = x.dot v
⊢ (Constraint.exact (r.bmod m)).sat' (bmod_coeffs m i x) v = true
-- Mathlib/NumberTheory/LegendreSymbol/AddCharacter.lean
/-- If `r` is not a unit, then `e.mulShift r` is not primitive. -/
lemma not_isPrimitive_mulShift [Finite R] (e : AddChar R R') {r : R}
    (hr : ¬ IsUnit r) : ¬ IsPrimitive (e.mulShift r)

Proof state:
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommMonoid R'
inst✝ : Finite R
e : AddChar R R'
r : R
hr : ∃ x, ∃ (_ : x * r = 0), ¬x = 0
⊢ ∃ x, ∃ (_ : x ≠ 0), ¬(e.mulShift r).mulShift x ≠ 1

Tactic:
rcases hr with ⟨x, h, h'⟩

Result:
case intro.intro
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommMonoid R'
inst✝ : Finite R
e : AddChar R R'
r x : R
h : x * r = 0
h' : ¬x = 0
⊢ ∃ x, ∃ (_ : x ≠ 0), ¬(e.mulShift r).mulShift x ≠ 1

Proof state:
case intro.intro
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommMonoid R'
inst✝ : Finite R
e : AddChar R R'
r x : R
h : x * r = 0
h' : ¬x = 0
⊢ ∃ x, ∃ (_ : x ≠ 0), ¬(e.mulShift r).mulShift x ≠ 1

Tactic:
exact ⟨x, h', by simp only [mulShift_mulShift, mul_comm r, h, mulShift_zero, not_ne_iff]⟩

Result:
no goals

Proof state:
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommMonoid R'
inst✝ : Finite R
e : AddChar R R'
r x : R
h : x * r = 0
h' : ¬x = 0
⊢ ¬(e.mulShift r).mulShift x ≠ 1

Tactic:
simp only [mulShift_mulShift, mul_comm r, h, mulShift_zero, not_ne_iff]

Result:
no goals

Proof state:
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommMonoid R'
inst✝ : Finite R
e : AddChar R R'
r : R
hr : ¬IsUnit r
⊢ ¬(e.mulShift r).IsPrimitive

Tactic:
simp only [IsPrimitive, not_forall]

Result:
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommMonoid R'
inst✝ : Finite R
e : AddChar R R'
r : R
hr : ¬IsUnit r
⊢ ∃ x, ∃ (_ : x ≠ 0), ¬(e.mulShift r).mulShift x ≠ 1

Proof state:
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommMonoid R'
inst✝ : Finite R
e : AddChar R R'
r : R
hr : ¬IsUnit r
⊢ ∃ x, ∃ (_ : x ≠ 0), ¬(e.mulShift r).mulShift x ≠ 1

Tactic:
simp only [isUnit_iff_mem_nonZeroDivisors_of_finite, mem_nonZeroDivisors_iff, not_forall] at hr

Result:
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommMonoid R'
inst✝ : Finite R
e : AddChar R R'
r : R
hr : ∃ x, ∃ (_ : x * r = 0), ¬x = 0
⊢ ∃ x, ∃ (_ : x ≠ 0), ¬(e.mulShift r).mulShift x ≠ 1
-- Mathlib/Logic/Basic.lean
theorem dite_prop_iff_and {Q : P → Prop} {R : ¬P → Prop} :
    dite P Q R ↔ (∀ h, Q h) ∧ (∀ h, R h)

Proof state:
P : Prop
inst✝ : Decidable P
Q : P → Prop
R : ¬P → Prop
⊢ dite P Q R ↔ (∀ (h : P), Q h) ∧ ∀ (h : ¬P), R h

Tactic:
by_cases h : P <;> simp [h, forall_prop_of_false, forall_prop_of_true]

Result:
no goals
-- Mathlib/Algebra/Polynomial/BigOperators.lean
theorem natDegree_multiset_prod (h : (0 : R[X]) ∉ t) :
    natDegree t.prod = (t.map natDegree).sum

Proof state:
case h
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
t : Multiset R[X]
h : 0 ∉ t
a✝ : Nontrivial R
⊢ ¬∃ a ∈ t, a = 0

Tactic:
rintro ⟨_, h, rfl⟩

Result:
case h.intro.intro
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
t : Multiset R[X]
h✝ : 0 ∉ t
a✝ : Nontrivial R
h : 0 ∈ t
⊢ False

Proof state:
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
t : Multiset R[X]
h : 0 ∉ t
⊢ t.prod.natDegree = (Multiset.map natDegree t).sum

Tactic:
nontriviality R

Result:
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
t : Multiset R[X]
h : 0 ∉ t
a✝ : Nontrivial R
⊢ t.prod.natDegree = (Multiset.map natDegree t).sum

Proof state:
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
t : Multiset R[X]
h : 0 ∉ t
a✝ : Nontrivial R
⊢ t.prod.natDegree = (Multiset.map natDegree t).sum

Tactic:
rw [natDegree_multiset_prod']

Result:
case h
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
t : Multiset R[X]
h : 0 ∉ t
a✝ : Nontrivial R
⊢ (Multiset.map (fun f => f.leadingCoeff) t).prod ≠ 0

Proof state:
case h
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
t : Multiset R[X]
h : 0 ∉ t
a✝ : Nontrivial R
⊢ (Multiset.map (fun f => f.leadingCoeff) t).prod ≠ 0

Tactic:
simp_rw [Ne, Multiset.prod_eq_zero_iff, Multiset.mem_map, leadingCoeff_eq_zero]

Result:
case h
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
t : Multiset R[X]
h : 0 ∉ t
a✝ : Nontrivial R
⊢ ¬∃ a ∈ t, a = 0

Proof state:
case h.intro.intro
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
t : Multiset R[X]
h✝ : 0 ∉ t
a✝ : Nontrivial R
h : 0 ∈ t
⊢ False

Tactic:
contradiction

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/l2Space.lean
theorem summable_inner (f g : lp G 2) : Summable fun i => ⟪f i, g i⟫

Proof state:
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
f g : ↥(lp G 2)
⊢ Summable fun i => inner (↑f i) (↑g i)

Tactic:
refine .of_norm_bounded (fun i => ‖f i‖ * ‖g i‖) (lp.summable_mul ?_ f g) ?_

Result:
case refine_1
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
f g : ↥(lp G 2)
⊢ (ENNReal.toReal 2).IsConjExponent (ENNReal.toReal 2)

case refine_2
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
f g : ↥(lp G 2)
⊢ ∀ (i : ι), ‖inner (↑f i) (↑g i)‖ ≤ (fun i => ‖↑f i‖ * ‖↑g i‖) i

Proof state:
case refine_1
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
f g : ↥(lp G 2)
⊢ (ENNReal.toReal 2).IsConjExponent (ENNReal.toReal 2)

Tactic:
rw [Real.isConjExponent_iff]

Result:
case refine_1
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
f g : ↥(lp G 2)
⊢ 1 < ENNReal.toReal 2 ∧ (ENNReal.toReal 2)⁻¹ + (ENNReal.toReal 2)⁻¹ = 1

Proof state:
case refine_1
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
f g : ↥(lp G 2)
⊢ 1 < ENNReal.toReal 2 ∧ (ENNReal.toReal 2)⁻¹ + (ENNReal.toReal 2)⁻¹ = 1

Tactic:
norm_num

Result:
no goals

Proof state:
case refine_2
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
f g : ↥(lp G 2)
i : ι
⊢ ‖inner (↑f i) (↑g i)‖ ≤ (fun i => ‖↑f i‖ * ‖↑g i‖) i

Tactic:
exact norm_inner_le_norm (𝕜 := 𝕜) _ _

Result:
no goals

Proof state:
case refine_2
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
f g : ↥(lp G 2)
⊢ ∀ (i : ι), ‖inner (↑f i) (↑g i)‖ ≤ (fun i => ‖↑f i‖ * ‖↑g i‖) i

Tactic:
intro i

Result:
case refine_2
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
f g : ↥(lp G 2)
i : ι
⊢ ‖inner (↑f i) (↑g i)‖ ≤ (fun i => ‖↑f i‖ * ‖↑g i‖) i
-- Mathlib/CategoryTheory/Category/Basic.lean
theorem dite_comp {P : Prop} [Decidable P]
    {X Y Z : C} (f : P → (X ⟶ Y)) (f' : ¬P → (X ⟶ Y)) (g : Y ⟶ Z) :
    (if h : P then f h else f' h) ≫ g = if h : P then f h ≫ g else f' h ≫ g

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
P : Prop
inst✝ : Decidable P
X Y Z : C
f : P → (X ⟶ Y)
f' : ¬P → (X ⟶ Y)
g : Y ⟶ Z
⊢ (if h : P then f h else f' h) ≫ g = if h : P then f h ≫ g else f' h ≫ g

Tactic:
aesop

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean
theorem GammaSeq_tendsto_Gamma (s : ℂ) : Tendsto (GammaSeq s) atTop (𝓝 <| Gamma s)

Proof state:
case succ
m : ℕ
IH : ∀ (s : ℂ), -↑m < s.re → Tendsto s.GammaSeq atTop (𝓝 (GammaAux m s))
s : ℂ
hs : -↑(m + 1) < s.re
⊢ Tendsto s.GammaSeq atTop (𝓝 (GammaAux (m + 1) s))

Tactic:
rw [Nat.cast_succ, neg_add, ← sub_eq_add_neg, sub_lt_iff_lt_add, ← one_re, ← add_re] at hs

Result:
case succ
m : ℕ
IH : ∀ (s : ℂ), -↑m < s.re → Tendsto s.GammaSeq atTop (𝓝 (GammaAux m s))
s : ℂ
hs : -↑m < (s + 1).re
⊢ Tendsto s.GammaSeq atTop (𝓝 (GammaAux (m + 1) s))

Proof state:
case zero
s : ℂ
hs : -↑0 < s.re
⊢ Tendsto s.GammaSeq atTop (𝓝 (GammaAux 0 s))

Tactic:
rw [Nat.cast_zero, neg_zero] at hs

Result:
case zero
s : ℂ
hs : 0 < s.re
⊢ Tendsto s.GammaSeq atTop (𝓝 (GammaAux 0 s))

Proof state:
case succ
m : ℕ
IH : ∀ (s : ℂ), -↑m < s.re → Tendsto s.GammaSeq atTop (𝓝 (GammaAux m s))
s : ℂ
⊢ -↑(m + 1) < s.re → Tendsto s.GammaSeq atTop (𝓝 (GammaAux (m + 1) s))

Tactic:
intro hs

Result:
case succ
m : ℕ
IH : ∀ (s : ℂ), -↑m < s.re → Tendsto s.GammaSeq atTop (𝓝 (GammaAux m s))
s : ℂ
hs : -↑(m + 1) < s.re
⊢ Tendsto s.GammaSeq atTop (𝓝 (GammaAux (m + 1) s))

Proof state:
case a
s : ℂ
this : ∀ (m : ℕ), -↑m < s.re → Tendsto s.GammaSeq atTop (𝓝 (GammaAux m s))
⊢ -s.re < ↑⌊1 - s.re⌋₊

Tactic:
rcases lt_or_le 0 (re s) with (hs | hs)

Result:
case a.inl
s : ℂ
this : ∀ (m : ℕ), -↑m < s.re → Tendsto s.GammaSeq atTop (𝓝 (GammaAux m s))
hs : 0 < s.re
⊢ -s.re < ↑⌊1 - s.re⌋₊

case a.inr
s : ℂ
this : ∀ (m : ℕ), -↑m < s.re → Tendsto s.GammaSeq atTop (𝓝 (GammaAux m s))
hs : s.re ≤ 0
⊢ -s.re < ↑⌊1 - s.re⌋₊

Proof state:
case zero
s : ℂ
⊢ -↑0 < s.re → Tendsto s.GammaSeq atTop (𝓝 (GammaAux 0 s))

Tactic:
intro hs

Result:
case zero
s : ℂ
hs : -↑0 < s.re
⊢ Tendsto s.GammaSeq atTop (𝓝 (GammaAux 0 s))

Proof state:
case succ.refine_2
m : ℕ
IH : ∀ (s : ℂ), -↑m < s.re → Tendsto s.GammaSeq atTop (𝓝 (GammaAux m s))
s : ℂ
hs : -↑m < (s + 1).re
n : ℕ
hn : n ≠ 0
⊢ (s + 1).GammaSeq n / s = ?succ.refine_1 n

Tactic:
exact GammaSeq_add_one_left s hn

Result:
no goals

Proof state:
case succ
m : ℕ
IH : ∀ (s : ℂ), -↑m < s.re → Tendsto s.GammaSeq atTop (𝓝 (GammaAux m s))
s : ℂ
hs : -↑m < (s + 1).re
⊢ Tendsto s.GammaSeq atTop (𝓝 (GammaAux (m + 1) s))

Tactic:
rw [GammaAux]

Result:
case succ
m : ℕ
IH : ∀ (s : ℂ), -↑m < s.re → Tendsto s.GammaSeq atTop (𝓝 (GammaAux m s))
s : ℂ
hs : -↑m < (s + 1).re
⊢ Tendsto s.GammaSeq atTop (𝓝 ((fun s => GammaAux m (s + 1) / s) s))

Proof state:
case zero
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
⊢ (fun n => ∫ (x : ℝ) in 0 ..↑n, ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)) n = s.GammaSeq n

Tactic:
exact (GammaSeq_eq_approx_Gamma_integral hs hn).symm

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Regularity/Increment.lean
theorem increment_isEquipartition : (increment hP G ε).IsEquipartition

Proof state:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
⊢ ∃ b, ∀ a ∈ ↑(increment hP G ε).parts, #a = b ∨ #a = b + 1

Tactic:
refine ⟨m, fun A hA => ?_⟩

Result:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
A : Finset α
hA : A ∈ ↑(increment hP G ε).parts
⊢ #A = m ∨ #A = m + 1

Proof state:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
A : Finset α
hA : ∃ A_1, ∃ (hA : A_1 ∈ P.parts), A ∈ (chunk hP G ε hA).parts
⊢ #A = m ∨ #A = m + 1

Tactic:
obtain ⟨U, hU, hA⟩ := hA

Result:
case intro.intro
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
A U : Finset α
hU : U ∈ P.parts
hA : A ∈ (chunk hP G ε hU).parts
⊢ #A = m ∨ #A = m + 1

Proof state:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
A : Finset α
hA : A ∈ ↑(increment hP G ε).parts
⊢ #A = m ∨ #A = m + 1

Tactic:
rw [mem_coe, increment, mem_bind] at hA

Result:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
A : Finset α
hA : ∃ A_1, ∃ (hA : A_1 ∈ P.parts), A ∈ (chunk hP G ε hA).parts
⊢ #A = m ∨ #A = m + 1

Proof state:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
⊢ (increment hP G ε).IsEquipartition

Tactic:
simp_rw [IsEquipartition, Set.equitableOn_iff_exists_eq_eq_add_one]

Result:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
⊢ ∃ b, ∀ a ∈ ↑(increment hP G ε).parts, #a = b ∨ #a = b + 1

Proof state:
case intro.intro
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
A U : Finset α
hU : U ∈ P.parts
hA : A ∈ (chunk hP G ε hU).parts
⊢ #A = m ∨ #A = m + 1

Tactic:
exact card_eq_of_mem_parts_chunk hA

Result:
no goals
-- Mathlib/Algebra/Homology/Homotopy.lean
theorem nullHomotopicMap'_f {k₂ k₁ k₀ : ι} (r₂₁ : c.Rel k₂ k₁) (r₁₀ : c.Rel k₁ k₀)
    (h : ∀ i j, c.Rel j i → (C.X i ⟶ D.X j)) :
    (nullHomotopicMap' h).f k₁ = C.d k₁ k₀ ≫ h k₀ k₁ r₁₀ + h k₁ k₂ r₂₁ ≫ D.d k₂ k₁

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₂ k₁ k₀ : ι
r₂₁ : c.Rel k₂ k₁
r₁₀ : c.Rel k₁ k₀
h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
⊢ (nullHomotopicMap fun i j => dite (c.Rel j i) (h i j) fun x => 0).f k₁ =
    C.d k₁ k₀ ≫ h k₀ k₁ r₁₀ + h k₁ k₂ r₂₁ ≫ D.d k₂ k₁

Tactic:
rw [nullHomotopicMap_f r₂₁ r₁₀]

Result:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₂ k₁ k₀ : ι
r₂₁ : c.Rel k₂ k₁
r₁₀ : c.Rel k₁ k₀
h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
⊢ (C.d k₁ k₀ ≫ dite (c.Rel k₁ k₀) (h k₀ k₁) fun x => 0) + (dite (c.Rel k₂ k₁) (h k₁ k₂) fun x => 0) ≫ D.d k₂ k₁ =
    C.d k₁ k₀ ≫ h k₀ k₁ r₁₀ + h k₁ k₂ r₂₁ ≫ D.d k₂ k₁

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₂ k₁ k₀ : ι
r₂₁ : c.Rel k₂ k₁
r₁₀ : c.Rel k₁ k₀
h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
⊢ (C.d k₁ k₀ ≫ dite (c.Rel k₁ k₀) (h k₀ k₁) fun x => 0) + (dite (c.Rel k₂ k₁) (h k₁ k₂) fun x => 0) ≫ D.d k₂ k₁ =
    C.d k₁ k₀ ≫ h k₀ k₁ r₁₀ + h k₁ k₂ r₂₁ ≫ D.d k₂ k₁

Tactic:
split_ifs

Result:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₂ k₁ k₀ : ι
r₂₁ : c.Rel k₂ k₁
r₁₀ : c.Rel k₁ k₀
h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
⊢ C.d k₁ k₀ ≫ h k₀ k₁ r₁₀ + h k₁ k₂ r₂₁ ≫ D.d k₂ k₁ = C.d k₁ k₀ ≫ h k₀ k₁ r₁₀ + h k₁ k₂ r₂₁ ≫ D.d k₂ k₁

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₂ k₁ k₀ : ι
r₂₁ : c.Rel k₂ k₁
r₁₀ : c.Rel k₁ k₀
h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
⊢ (nullHomotopicMap' h).f k₁ = C.d k₁ k₀ ≫ h k₀ k₁ r₁₀ + h k₁ k₂ r₂₁ ≫ D.d k₂ k₁

Tactic:
simp only [nullHomotopicMap']

Result:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₂ k₁ k₀ : ι
r₂₁ : c.Rel k₂ k₁
r₁₀ : c.Rel k₁ k₀
h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
⊢ (nullHomotopicMap fun i j => dite (c.Rel j i) (h i j) fun x => 0).f k₁ =
    C.d k₁ k₀ ≫ h k₀ k₁ r₁₀ + h k₁ k₂ r₂₁ ≫ D.d k₂ k₁

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₂ k₁ k₀ : ι
r₂₁ : c.Rel k₂ k₁
r₁₀ : c.Rel k₁ k₀
h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
⊢ C.d k₁ k₀ ≫ h k₀ k₁ r₁₀ + h k₁ k₂ r₂₁ ≫ D.d k₂ k₁ = C.d k₁ k₀ ≫ h k₀ k₁ r₁₀ + h k₁ k₂ r₂₁ ≫ D.d k₂ k₁

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
theorem exists_eq_add_of_le {n : ℕ} {a b : Fin n} (h : a ≤ b) : ∃ k ≤ b, b = a + k

Proof state:
case intro
n : ℕ
a b : Fin n
h : a ≤ b
k : ℕ
hk : ↑b = ↑a + k
hkb : k ≤ ↑b
⊢ ∃ k ≤ b, b = a + k

Tactic:
refine ⟨⟨k, hkb.trans_lt b.is_lt⟩, hkb, ?_⟩

Result:
case intro
n : ℕ
a b : Fin n
h : a ≤ b
k : ℕ
hk : ↑b = ↑a + k
hkb : k ≤ ↑b
⊢ b = a + ⟨k, ⋯⟩

Proof state:
case intro
n : ℕ
a b : Fin n
h : a ≤ b
k : ℕ
hk : ↑b = ↑a + k
hkb : k ≤ ↑b
⊢ b = a + ⟨k, ⋯⟩

Tactic:
simp [Fin.ext_iff, Fin.val_add, ← hk, Nat.mod_eq_of_lt b.is_lt]

Result:
no goals

Proof state:
case intro
n : ℕ
a b : Fin n
h : a ≤ b
k : ℕ
hk : ↑b = ↑a + k
⊢ ∃ k ≤ b, b = a + k

Tactic:
have hkb : k ≤ b := by omega

Result:
case intro
n : ℕ
a b : Fin n
h : a ≤ b
k : ℕ
hk : ↑b = ↑a + k
hkb : k ≤ ↑b
⊢ ∃ k ≤ b, b = a + k

Proof state:
n : ℕ
a b : Fin n
h : a ≤ b
k : ℕ
hk : ↑b = ↑a + k
⊢ k ≤ ↑b

Tactic:
omega

Result:
no goals

Proof state:
n : ℕ
a b : Fin n
h : a ≤ b
⊢ ∃ k ≤ b, b = a + k

Tactic:
obtain ⟨k, hk⟩ : ∃ k : ℕ, (b : ℕ) = a + k := Nat.exists_eq_add_of_le h

Result:
case intro
n : ℕ
a b : Fin n
h : a ≤ b
k : ℕ
hk : ↑b = ↑a + k
⊢ ∃ k ≤ b, b = a + k
-- Mathlib/Data/Matrix/ColumnRowPartitioned.lean
@[simp]
lemma vecMul_fromCols [Fintype m] (B₁ : Matrix m n₁ R) (B₂ : Matrix m n₂ R) (v : m → R) :
    v ᵥ* fromCols B₁ B₂ = Sum.elim (v ᵥ* B₁) (v ᵥ* B₂)

Proof state:
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
inst✝¹ : Semiring R
inst✝ : Fintype m
B₁ : Matrix m n₁ R
B₂ : Matrix m n₂ R
v : m → R
⊢ v ᵥ* B₁.fromCols B₂ = Sum.elim (v ᵥ* B₁) (v ᵥ* B₂)

Tactic:
ext (_ | _) <;> rfl

Result:
no goals
-- Mathlib/RingTheory/Trace/Basic.lean
theorem traceMatrix_of_basis [Fintype κ] [DecidableEq κ] (b : Basis κ A B) :
    traceMatrix A b = BilinForm.toMatrix b (traceForm A B)

Proof state:
κ : Type w
A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Fintype κ
inst✝ : DecidableEq κ
b : Basis κ A B
⊢ traceMatrix A ⇑b = (BilinForm.toMatrix b) (traceForm A B)

Tactic:
ext (i j)

Result:
case a
κ : Type w
A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Fintype κ
inst✝ : DecidableEq κ
b : Basis κ A B
i j : κ
⊢ traceMatrix A (⇑b) i j = (BilinForm.toMatrix b) (traceForm A B) i j

Proof state:
case a
κ : Type w
A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Fintype κ
inst✝ : DecidableEq κ
b : Basis κ A B
i j : κ
⊢ traceMatrix A (⇑b) i j = (BilinForm.toMatrix b) (traceForm A B) i j

Tactic:
rw [traceMatrix_apply, traceForm_apply, traceForm_toMatrix]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Monadic.lean
theorem forIn_yield_eq_foldlM [Monad m] [LawfulMonad m]
    (l : Vector α n) (f : α → β → m γ) (g : α → β → γ → β) (init : β) :
    forIn l init (fun a b => (fun c => .yield (g a b c)) <$> f a b) =
      l.foldlM (fun b a => g a b <$> f a b) init

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
n : Nat
β γ : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m γ
g : α → β → γ → β
init : β
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ (forIn { toArray := toArray✝, size_toArray := size_toArray✝ } init fun a b =>
      (fun c => ForInStep.yield (g a b c)) <$> f a b) =
    foldlM (fun b a => g a b <$> f a b) init { toArray := toArray✝, size_toArray := size_toArray✝ }

Tactic:
simp

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
n : Nat
β γ : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : Vector α n
f : α → β → m γ
g : α → β → γ → β
init : β
⊢ (forIn l init fun a b => (fun c => ForInStep.yield (g a b c)) <$> f a b) = foldlM (fun b a => g a b <$> f a b) init l

Tactic:
cases l

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
n : Nat
β γ : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m γ
g : α → β → γ → β
init : β
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ (forIn { toArray := toArray✝, size_toArray := size_toArray✝ } init fun a b =>
      (fun c => ForInStep.yield (g a b c)) <$> f a b) =
    foldlM (fun b a => g a b <$> f a b) init { toArray := toArray✝, size_toArray := size_toArray✝ }