harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem map_fst_darts {u v : V} (p : G.Walk u v) : p.darts.map (·.fst) = p.support.dropLast

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ List.map (fun x => x.toProd.1) p.darts = p.support.dropLast

Tactic:
simpa! using congr_arg List.dropLast (map_fst_darts_append p)

Result:
no goals
-- Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean
theorem WithTop.iInf_empty [IsEmpty ι] [InfSet α] (f : ι → WithTop α) :
    ⨅ i, f i = ⊤

Proof state:
α : Type u_1
ι : Sort u_4
inst✝² : Preorder α
inst✝¹ : IsEmpty ι
inst✝ : InfSet α
f : ι → WithTop α
⊢ ⨅ i, f i = ⊤

Tactic:
rw [iInf, range_eq_empty, WithTop.sInf_empty]

Result:
no goals
-- Mathlib/SetTheory/ZFC/Basic.lean
theorem mem_prod {x y z : ZFSet.{u}} : z ∈ prod x y ↔ ∃ a ∈ x, ∃ b ∈ y, z = pair a b

Proof state:
x y z : ZFSet.{u}
⊢ z ∈ x.prod y ↔ ∃ a ∈ x, ∃ b ∈ y, z = a.pair b

Tactic:
simp [prod]

Result:
no goals
-- Mathlib/Algebra/Lie/Submodule.lean
theorem incl_isIdealMorphism : I.incl.IsIdealMorphism

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ toLieSubalgebra R L I = I.incl.range

Tactic:
exact (I : LieSubalgebra R L).incl_range.symm

Result:
no goals

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ I.incl.IsIdealMorphism

Tactic:
rw [I.incl.isIdealMorphism_def, incl_idealRange]

Result:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ toLieSubalgebra R L I = I.incl.range
-- Mathlib/MeasureTheory/Function/L1Space/HasFiniteIntegral.lean
theorem hasFiniteIntegral_zero_measure {m : MeasurableSpace α} (f : α → β) :
    HasFiniteIntegral f (0 : Measure α)

Proof state:
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
m : MeasurableSpace α
f : α → β
⊢ HasFiniteIntegral f 0

Tactic:
simp only [HasFiniteIntegral, lintegral_zero_measure, zero_lt_top]

Result:
no goals
-- Mathlib/Topology/Compactification/OnePoint.lean
theorem isOpen_iff_of_mem' (h : ∞ ∈ s) :
    IsOpen s ↔ IsCompact ((↑) ⁻¹' s : Set X)ᶜ ∧ IsOpen ((↑) ⁻¹' s : Set X)

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
h : ∞ ∈ s
⊢ IsOpen s ↔ IsCompact (some ⁻¹' s)ᶜ ∧ IsOpen (some ⁻¹' s)

Tactic:
simp [isOpen_def, h]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean
theorem vadd_mem_spanPoints_of_mem_spanPoints_of_mem_vectorSpan {s : Set P} {p : P} {v : V}
    (hp : p ∈ spanPoints k s) (hv : v ∈ vectorSpan k s) : v +ᵥ p ∈ spanPoints k s

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p : P
v : V
hp : p ∈ spanPoints k s
hv : v ∈ vectorSpan k s
⊢ v +ᵥ p ∈ spanPoints k s

Tactic:
rcases hp with ⟨p₂, ⟨hp₂, ⟨v₂, ⟨hv₂, hv₂p⟩⟩⟩⟩

Result:
case intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p : P
v : V
hv : v ∈ vectorSpan k s
p₂ : P
hp₂ : p₂ ∈ s
v₂ : V
hv₂ : v₂ ∈ vectorSpan k s
hv₂p : p = v₂ +ᵥ p₂
⊢ v +ᵥ p ∈ spanPoints k s

Proof state:
case intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p : P
v : V
hv : v ∈ vectorSpan k s
p₂ : P
hp₂ : p₂ ∈ s
v₂ : V
hv₂ : v₂ ∈ vectorSpan k s
hv₂p : p = v₂ +ᵥ p₂
⊢ (v + v₂) +ᵥ p₂ ∈ spanPoints k s

Tactic:
exact ⟨p₂, hp₂, v + v₂, (vectorSpan k s).add_mem hv hv₂, rfl⟩

Result:
no goals

Proof state:
case intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p : P
v : V
hv : v ∈ vectorSpan k s
p₂ : P
hp₂ : p₂ ∈ s
v₂ : V
hv₂ : v₂ ∈ vectorSpan k s
hv₂p : p = v₂ +ᵥ p₂
⊢ v +ᵥ p ∈ spanPoints k s

Tactic:
rw [hv₂p, vadd_vadd]

Result:
case intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p : P
v : V
hv : v ∈ vectorSpan k s
p₂ : P
hp₂ : p₂ ∈ s
v₂ : V
hv₂ : v₂ ∈ vectorSpan k s
hv₂p : p = v₂ +ᵥ p₂
⊢ (v + v₂) +ᵥ p₂ ∈ spanPoints k s
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sort/Lemmas.lean
theorem splitInTwo_fst (l : { l : List α // l.length = n }) :
    (splitInTwo l).1 = ⟨l.1.take ((n+1)/2), by simp [splitInTwo, splitAt_eq, l.2]; omega⟩

Proof state:
α : Type u_1
n : Nat
l : { l // l.length = n }
⊢ (splitInTwo l).fst = ⟨take ((n + 1) / 2) l.val, ⋯⟩

Tactic:
simp [splitInTwo, splitAt_eq]

Result:
no goals

Proof state:
α : Type ?u.28
n : Nat
l : { l // l.length = n }
⊢ min ((n + 1) / 2) n = (n + 1) / 2

Tactic:
omega

Result:
no goals

Proof state:
α : Type ?u.28
n : Nat
l : { l // l.length = n }
⊢ (take ((n + 1) / 2) l.val).length = (n + 1) / 2

Tactic:
simp [splitInTwo, splitAt_eq, l.2]

Result:
α : Type ?u.28
n : Nat
l : { l // l.length = n }
⊢ min ((n + 1) / 2) n = (n + 1) / 2
-- Mathlib/Combinatorics/Additive/ETransform.lean
theorem mulETransformRight.card :
    (mulETransformLeft e x).2.card + (mulETransformRight e x).2.card = 2 * x.2.card :=
  (card_union_add_card_inter _ _).trans <| by rw [card_smul_finset, two_mul]

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Group α
e : α
x : Finset α × Finset α
⊢ #x.2 + #(e⁻¹ • x.2) = 2 * #x.2

Tactic:
rw [card_smul_finset, two_mul]

Result:
no goals
-- Mathlib/Analysis/Seminorm.lean
theorem bddAbove_range_iff {ι : Sort*} {p : ι → Seminorm 𝕜 E} :
    BddAbove (range p) ↔ ∀ x, BddAbove (range fun i ↦ p i x)

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
ι : Sort u_12
p : ι → Seminorm 𝕜 E
⊢ BddAbove (range p) ↔ ∀ (x : E), BddAbove (range fun i => (p i) x)

Tactic:
rw [Seminorm.bddAbove_iff, ← range_comp, bddAbove_range_pi]

Result:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
ι : Sort u_12
p : ι → Seminorm 𝕜 E
⊢ (∀ (a : E), BddAbove (range fun i => (DFunLike.coe ∘ p) i a)) ↔ ∀ (x : E), BddAbove (range fun i => (p i) x)

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
ι : Sort u_12
p : ι → Seminorm 𝕜 E
⊢ (∀ (a : E), BddAbove (range fun i => (DFunLike.coe ∘ p) i a)) ↔ ∀ (x : E), BddAbove (range fun i => (p i) x)

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Generator/Basic.lean
theorem HasDetector.hasCodetector_of_hasDetector_op [HasDetector Cᵒᵖ] :
    HasCodetector C

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasDetector Cᵒᵖ
⊢ HasCodetector C

Tactic:
simp_all

Result:
no goals
-- Mathlib/NumberTheory/LSeries/AbstractFuncEq.lean
lemma Λ₀_eq (s : ℂ) : P.Λ₀ s = P.Λ s + (1 / s) • P.f₀ + (P.ε / (P.k - s)) • P.g₀

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
⊢ mellin P.f_modif s =
    mellin P.f_modif s - (1 / s) • P.f₀ - (P.ε / (↑P.k - s)) • P.g₀ + (1 / s) • P.f₀ + (P.ε / (↑P.k - s)) • P.g₀

Tactic:
abel

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
⊢ P.Λ₀ s = P.Λ s + (1 / s) • P.f₀ + (P.ε / (↑P.k - s)) • P.g₀

Tactic:
unfold Λ Λ₀

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
⊢ mellin P.f_modif s =
    mellin P.f_modif s - (1 / s) • P.f₀ - (P.ε / (↑P.k - s)) • P.g₀ + (1 / s) • P.f₀ + (P.ε / (↑P.k - s)) • P.g₀
-- Mathlib/Algebra/Polynomial/Splits.lean
theorem eval_eq_prod_roots_sub_of_splits_id {p : K[X]}
    (hsplit : Splits (RingHom.id K) p) (v : K) :
    eval v p = p.leadingCoeff * (p.roots.map fun a ↦ v - a).prod

Proof state:
case h.e'_3.h.e'_6.h.e'_3.a.h.e'_4.h
K : Type v
inst✝ : Field K
p : K[X]
hsplit : Splits (RingHom.id K) p
v : K
⊢ p = map (algebraMap K K) p

Tactic:
rw [Algebra.id.map_eq_id, map_id]

Result:
no goals

Proof state:
K : Type v
inst✝ : Field K
p : K[X]
hsplit : Splits (RingHom.id K) p
v : K
⊢ eval v p = p.leadingCoeff * (Multiset.map (fun a => v - a) p.roots).prod

Tactic:
convert aeval_eq_prod_aroots_sub_of_splits hsplit v

Result:
case h.e'_3.h.e'_6.h.e'_3.a.h.e'_4.h
K : Type v
inst✝ : Field K
p : K[X]
hsplit : Splits (RingHom.id K) p
v : K
⊢ p = map (algebraMap K K) p
-- Mathlib/RingTheory/Polynomial/Hermite/Basic.lean
theorem leadingCoeff_hermite (n : ℕ) : (hermite n).leadingCoeff = 1

Proof state:
n : ℕ
⊢ (hermite n).leadingCoeff = 1

Tactic:
rw [← coeff_natDegree, natDegree_hermite, coeff_hermite_self]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean
theorem smul_map_volume_mul_right {a : ℝ} (h : a ≠ 0) :
    ENNReal.ofReal |a| • Measure.map (· * a) volume = volume

Proof state:
a : ℝ
h : a ≠ 0
⊢ ofReal |a| • Measure.map (fun x => x * a) volume = volume

Tactic:
simpa only [mul_comm] using Real.smul_map_volume_mul_left h

Result:
no goals
-- Mathlib/Data/NNRat/Defs.lean
@[simp] lemma num_ne_zero : q.num ≠ 0 ↔ q ≠ 0

Proof state:
q : ℚ≥0
⊢ q.num ≠ 0 ↔ q ≠ 0

Tactic:
simp [num]

Result:
no goals
-- Mathlib/Data/List/Zip.lean
theorem length_revzip (l : List α) : length (revzip l) = length l

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

Tactic:
simp only [revzip, length_zip, length_reverse, min_self]

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem mem_nhdsWithin_insert {a : α} {s t : Set α} : t ∈ 𝓝[insert a s] a ↔ a ∈ t ∧ t ∈ 𝓝[s] a

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
s t : Set α
⊢ t ∈ 𝓝[insert a s] a ↔ a ∈ t ∧ t ∈ 𝓝[s] a

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Lie/Classical.lean
theorem jb_transform : (PB l R)ᵀ * JB l R * PB l R = (2 : R) • Matrix.fromBlocks 1 0 0 (S l R)

Proof state:
l : Type u_4
R : Type u₂
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
⊢ (PB l R)ᵀ * JB l R * PB l R = 2 • fromBlocks 1 0 0 (S l R)

Tactic:
simp [PB, JB, jd_transform, Matrix.fromBlocks_transpose, Matrix.fromBlocks_multiply,
  Matrix.fromBlocks_smul]

Result:
no goals
-- Mathlib/Data/List/Intervals.lean
theorem filter_lt_of_ge {n m l : ℕ} (hlm : l ≤ m) :
    ((Ico n m).filter fun x => x < l) = Ico n l

Proof state:
case inl
n m l : ℕ
hlm : l ≤ m
hnl : n ≤ l
⊢ filter (fun x => decide (x < l)) (Ico n m) = Ico n l

Tactic:
rw [← append_consecutive hnl hlm, filter_append, filter_lt_of_top_le (le_refl l),
  filter_lt_of_le_bot (le_refl l), append_nil]

Result:
no goals

Proof state:
case inr
n m l : ℕ
hlm : l ≤ m
hln : l ≤ n
⊢ filter (fun x => decide (x < l)) (Ico n m) = Ico n l

Tactic:
rw [eq_nil_of_le hln, filter_lt_of_le_bot hln]

Result:
no goals

Proof state:
n m l : ℕ
hlm : l ≤ m
⊢ filter (fun x => decide (x < l)) (Ico n m) = Ico n l

Tactic:
rcases le_total n l with hnl | hln

Result:
case inl
n m l : ℕ
hlm : l ≤ m
hnl : n ≤ l
⊢ filter (fun x => decide (x < l)) (Ico n m) = Ico n l

case inr
n m l : ℕ
hlm : l ≤ m
hln : l ≤ n
⊢ filter (fun x => decide (x < l)) (Ico n m) = Ico n l
-- Mathlib/Combinatorics/Enumerative/IncidenceAlgebra.lean
lemma sum_Icc_mu_left (a b : α) : ∑ x ∈ Icc a b, mu 𝕜 x b = if a = b then 1 else 0

Proof state:
𝕜 : Type u_2
α : Type u_5
inst✝³ : Ring 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
⊢ ∑ x ∈ Icc a b, (mu 𝕜) x b = if a = b then 1 else 0

Tactic:
rw [mu_eq_mu', sum_Icc_mu'_left]

Result:
no goals
-- Mathlib/Algebra/Group/Fin/Tuple.lean
@[to_additive (attr := simp)]
lemma insertNth_one_right [∀ j, One (α j)] (i : Fin (n + 1)) (x : α i) :
    i.insertNth x 1 = Pi.mulSingle i x :=
  insertNth_eq_iff.2 <| by unfold removeNth; simp [succAbove_ne, Pi.one_def]

Proof state:
n : ℕ
α : Fin (n + 1) → Type u_1
inst✝ : (j : Fin (n + 1)) → One (α j)
i : Fin (n + 1)
x : α i
⊢ x = Pi.mulSingle i x i ∧ 1 = fun i_1 => Pi.mulSingle i x (i.succAbove i_1)

Tactic:
simp [succAbove_ne, Pi.one_def]

Result:
no goals

Proof state:
n : ℕ
α : Fin (n + 1) → Type u_1
inst✝ : (j : Fin (n + 1)) → One (α j)
i : Fin (n + 1)
x : α i
⊢ x = Pi.mulSingle i x i ∧ 1 = i.removeNth (Pi.mulSingle i x)

Tactic:
unfold removeNth

Result:
n : ℕ
α : Fin (n + 1) → Type u_1
inst✝ : (j : Fin (n + 1)) → One (α j)
i : Fin (n + 1)
x : α i
⊢ x = Pi.mulSingle i x i ∧ 1 = fun i_1 => Pi.mulSingle i x (i.succAbove i_1)
-- Mathlib/RingTheory/MvPolynomial/Symmetric/Defs.lean
theorem _root_.MvPolynomial.isSymmetric_rename {e : σ ≃ τ} :
    (MvPolynomial.rename e φ).IsSymmetric ↔ φ.IsSymmetric :=
  ⟨fun h => by simpa using (IsSymmetric.rename (R := R) h e.symm), (IsSymmetric.rename · e)⟩

Proof state:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
e : σ ≃ τ
h : ((rename ⇑e) φ).IsSymmetric
⊢ φ.IsSymmetric

Tactic:
simpa using (IsSymmetric.rename (R := R) h e.symm)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getElem_of_append {l : List α} (eq : l = l₁ ++ a :: l₂) (h : l₁.length = i) :
    l[i]'(eq ▸ h ▸ by simp_arith) = a := Option.some.inj <| by
  rw [← getElem?_eq_getElem, eq, getElem?_append_right (h ▸ Nat.le_refl _), h]
  simp

Proof state:
α : Type u_1
l₁ : List α
a : α
l₂ : List α
i : Nat
l : List α
eq : l = l₁ ++ a :: l₂
h : l₁.length = i
⊢ (a :: l₂)[i - i]? = some a

Tactic:
simp

Result:
no goals

Proof state:
α : Type ?u.185407
l₁ : List α
a : α
l₂ : List α
i : Nat
l : List α
eq : l = l₁ ++ a :: l₂
h : l₁.length = i
⊢ l₁.length < (l₁ ++ a :: l₂).length

Tactic:
simp_arith

Result:
no goals

Proof state:
α : Type u_1
l₁ : List α
a : α
l₂ : List α
i : Nat
l : List α
eq : l = l₁ ++ a :: l₂
h : l₁.length = i
⊢ some l[i] = some a

Tactic:
rw [← getElem?_eq_getElem, eq, getElem?_append_right (h ▸ Nat.le_refl _), h]

Result:
α : Type u_1
l₁ : List α
a : α
l₂ : List α
i : Nat
l : List α
eq : l = l₁ ++ a :: l₂
h : l₁.length = i
⊢ (a :: l₂)[i - i]? = some a
-- Mathlib/Analysis/Analytic/IsolatedZeros.lean
theorem frequently_eq_iff_eventually_eq (hf : AnalyticAt 𝕜 f z₀) (hg : AnalyticAt 𝕜 g z₀) :
    (∃ᶠ z in 𝓝[≠] z₀, f z = g z) ↔ ∀ᶠ z in 𝓝 z₀, f z = g z

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
hg : AnalyticAt 𝕜 g z₀
⊢ (∃ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = g z) ↔ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = g z

Tactic:
simpa [sub_eq_zero] using frequently_zero_iff_eventually_zero (hf.sub hg)

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/Defs.lean
theorem reindexFinsetRange_apply (x : Finset.univ.image b) : b.reindexFinsetRange x = x

Proof state:
case mk
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
b : Basis ι R M
inst✝¹ : Fintype ι
inst✝ : DecidableEq M
bi : M
hbi : bi ∈ Finset.image (⇑b) Finset.univ
⊢ b.reindexFinsetRange ⟨bi, hbi⟩ = ↑⟨bi, hbi⟩

Tactic:
rcases Finset.mem_image.mp hbi with ⟨i, -, rfl⟩

Result:
case mk.intro.intro
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
b : Basis ι R M
inst✝¹ : Fintype ι
inst✝ : DecidableEq M
i : ι
hbi : b i ∈ Finset.image (⇑b) Finset.univ
⊢ b.reindexFinsetRange ⟨b i, hbi⟩ = ↑⟨b i, hbi⟩

Proof state:
case mk.intro.intro
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
b : Basis ι R M
inst✝¹ : Fintype ι
inst✝ : DecidableEq M
i : ι
hbi : b i ∈ Finset.image (⇑b) Finset.univ
⊢ b.reindexFinsetRange ⟨b i, hbi⟩ = ↑⟨b i, hbi⟩

Tactic:
exact b.reindexFinsetRange_self i

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
b : Basis ι R M
inst✝¹ : Fintype ι
inst✝ : DecidableEq M
x : { x // x ∈ Finset.image (⇑b) Finset.univ }
⊢ b.reindexFinsetRange x = ↑x

Tactic:
rcases x with ⟨bi, hbi⟩

Result:
case mk
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
b : Basis ι R M
inst✝¹ : Fintype ι
inst✝ : DecidableEq M
bi : M
hbi : bi ∈ Finset.image (⇑b) Finset.univ
⊢ b.reindexFinsetRange ⟨bi, hbi⟩ = ↑⟨bi, hbi⟩
-- Mathlib/Topology/Algebra/InfiniteSum/Defs.lean
theorem Multipliable.hasProd (ha : Multipliable f) : HasProd f (∏' b, f b)

Proof state:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
ha : Multipliable f
H : (mulSupport f).Finite
⊢ HasProd f (if (mulSupport fun b => f b).Finite then ∏ᶠ (b : β), f b else Exists.choose ⋯)

Tactic:
simp [H, hasProd_prod_of_ne_finset_one, finprod_eq_prod]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
ha : Multipliable f
⊢ HasProd f (∏' (b : β), f b)

Tactic:
simp only [tprod_def, ha, dite_true]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
ha : Multipliable f
⊢ HasProd f (if (mulSupport fun b => f b).Finite then ∏ᶠ (b : β), f b else Exists.choose ⋯)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
ha : Multipliable f
⊢ HasProd f (if (mulSupport fun b => f b).Finite then ∏ᶠ (b : β), f b else Exists.choose ⋯)

Tactic:
by_cases H : (mulSupport f).Finite

Result:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
ha : Multipliable f
H : (mulSupport f).Finite
⊢ HasProd f (if (mulSupport fun b => f b).Finite then ∏ᶠ (b : β), f b else Exists.choose ⋯)

case neg
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
ha : Multipliable f
H : ¬(mulSupport f).Finite
⊢ HasProd f (if (mulSupport fun b => f b).Finite then ∏ᶠ (b : β), f b else Exists.choose ⋯)

Proof state:
case neg
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
ha : Multipliable f
H : ¬(mulSupport f).Finite
⊢ HasProd f (if (mulSupport fun b => f b).Finite then ∏ᶠ (b : β), f b else Exists.choose ⋯)

Tactic:
simpa [H] using ha.choose_spec

Result:
no goals
-- Mathlib/GroupTheory/Coxeter/Basic.lean
theorem subgroup_closure_range_simple : Subgroup.closure (range cs.simple) = ⊤

Proof state:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
this : cs.simple = ⇑cs.mulEquiv.symm ∘ PresentedGroup.of
⊢ cs.mulEquiv.symm.toMonoidHom.range = ⊤

Tactic:
exact MonoidHom.range_eq_top.2 (MulEquiv.surjective _)

Result:
no goals

Proof state:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
this : cs.simple = ⇑cs.mulEquiv.symm ∘ PresentedGroup.of
⊢ Subgroup.closure (Set.range cs.simple) = ⊤

Tactic:
rw [this, Set.range_comp, ← MulEquiv.coe_toMonoidHom, ← MonoidHom.map_closure,
  PresentedGroup.closure_range_of, ← MonoidHom.range_eq_map]

Result:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
this : cs.simple = ⇑cs.mulEquiv.symm ∘ PresentedGroup.of
⊢ cs.mulEquiv.symm.toMonoidHom.range = ⊤

Proof state:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
⊢ Subgroup.closure (Set.range cs.simple) = ⊤

Tactic:
have : cs.simple = cs.mulEquiv.symm ∘ PresentedGroup.of := rfl

Result:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
this : cs.simple = ⇑cs.mulEquiv.symm ∘ PresentedGroup.of
⊢ Subgroup.closure (Set.range cs.simple) = ⊤
-- Mathlib/MeasureTheory/Measure/Regular.lean
theorem _root_.MeasurableSet.exists_isCompact_diff_lt [OpensMeasurableSpace α] [T2Space α]
    [InnerRegularCompactLTTop μ]  ⦃A : Set α⦄ (hA : MeasurableSet A) (h'A : μ A ≠ ∞)
    {ε : ℝ≥0∞} (hε : ε ≠ 0) :
    ∃ K, K ⊆ A ∧ IsCompact K ∧ μ (A \ K) < ε

Proof state:
case intro.intro.intro
α : Type u_1
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : T2Space α
inst✝ : μ.InnerRegularCompactLTTop
A : Set α
hA : MeasurableSet A
h'A : μ A ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
K : Set α
hKA : K ⊆ A
hKc : IsCompact K
hK : μ A < μ K + ε
⊢ ∃ K ⊆ A, IsCompact K ∧ μ (A \ K) < ε

Tactic:
exact ⟨K, hKA, hKc, measure_diff_lt_of_lt_add hKc.nullMeasurableSet hKA
  (ne_top_of_le_ne_top h'A <| measure_mono hKA) hK⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : T2Space α
inst✝ : μ.InnerRegularCompactLTTop
A : Set α
hA : MeasurableSet A
h'A : μ A ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ K ⊆ A, IsCompact K ∧ μ (A \ K) < ε

Tactic:
rcases hA.exists_isCompact_lt_add h'A hε with ⟨K, hKA, hKc, hK⟩

Result:
case intro.intro.intro
α : Type u_1
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : T2Space α
inst✝ : μ.InnerRegularCompactLTTop
A : Set α
hA : MeasurableSet A
h'A : μ A ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
K : Set α
hKA : K ⊆ A
hKc : IsCompact K
hK : μ A < μ K + ε
⊢ ∃ K ⊆ A, IsCompact K ∧ μ (A \ K) < ε
-- Mathlib/Algebra/Group/Basic.lean
theorem div_one (a : G) : a / 1 = a

Proof state:
G : Type u_3
inst✝ : DivInvOneMonoid G
a : G
⊢ a / 1 = a

Tactic:
simp [div_eq_mul_inv]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Attach.lean
theorem attachWith_congr {o₁ o₂ : Option α} (w : o₁ = o₂) {P : α → Prop} {H : ∀ x ∈ o₁, P x} :
    o₁.attachWith P H = o₂.attachWith P fun _ h => H _ (w ▸ h)

Proof state:
α : Type u_1
o₁ o₂ : Option α
w : o₁ = o₂
P : α → Prop
H : ∀ (x : α), x ∈ o₁ → P x
⊢ o₁.attachWith P H = o₂.attachWith P ⋯

Tactic:
subst w

Result:
α : Type u_1
o₁ : Option α
P : α → Prop
H : ∀ (x : α), x ∈ o₁ → P x
⊢ o₁.attachWith P H = o₁.attachWith P ⋯

Proof state:
α : Type u_1
o₁ : Option α
P : α → Prop
H : ∀ (x : α), x ∈ o₁ → P x
⊢ o₁.attachWith P H = o₁.attachWith P ⋯

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Measure/WithDensity.lean
theorem withDensity_add_right (f : α → ℝ≥0∞) {g : α → ℝ≥0∞} (hg : Measurable g) :
    μ.withDensity (f + g) = μ.withDensity f + μ.withDensity g

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hg : Measurable g
⊢ μ.withDensity (f + g) = μ.withDensity f + μ.withDensity g

Tactic:
simpa only [add_comm] using withDensity_add_left hg f

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/TruncLEHomology.lean
lemma acyclic_truncLE_iff_isSupportedOutside :
    (K.truncLE e).Acyclic ↔ K.IsSupportedOutside e

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
⊢ (K.truncLE e).op.Acyclic ↔ K.op.IsSupportedOutside e.op

Tactic:
exact K.op.acyclic_truncGE_iff_isSupportedOutside e.op

Result:
no goals

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
⊢ (K.truncLE e).Acyclic ↔ K.IsSupportedOutside e

Tactic:
rw [← acyclic_op_iff, ← isSupportedOutside_op_iff]

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
⊢ (K.truncLE e).op.Acyclic ↔ K.op.IsSupportedOutside e.op
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem pow_add_one' {m n : Nat} : m ^ (n + 1) = m * m ^ n

Proof state:
m n : Nat
⊢ m ^ (n + 1) = m * m ^ n

Tactic:
rw [Nat.pow_add_one, Nat.mul_comm]

Result:
no goals
-- Mathlib/Algebra/CubicDiscriminant.lean
theorem b_eq_three_roots (ha : P.a ≠ 0) (h3 : (map φ P).roots = {x, y, z}) :
    φ P.b = φ P.a * -(x + y + z)

Proof state:
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ φ P.b = φ P.a * -(x + y + z)

Tactic:
injection eq_sum_three_roots ha h3

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem map_reverse (f : α → β) (l : Array α) : l.reverse.map f = (l.map f).reverse

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l : Array α
⊢ map f l.reverse = (map f l).reverse

Tactic:
cases l <;> simp [*]

Result:
no goals