harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
theorem norm_mkPiAlgebraFin_le_of_pos (hn : 0 < n) :
    ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n A‖ ≤ 1

Proof state:
case intro
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
A : Type u_1
inst✝¹ : SeminormedRing A
inst✝ : NormedAlgebra 𝕜 A
n : ℕ
hn : 0 < n.succ
⊢ ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n.succ A‖ ≤ 1

Tactic:
exact norm_mkPiAlgebraFin_succ_le

Result:
no goals

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
n : ℕ
A : Type u_1
inst✝¹ : SeminormedRing A
inst✝ : NormedAlgebra 𝕜 A
hn : 0 < n
⊢ ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n A‖ ≤ 1

Tactic:
obtain ⟨n, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hn.ne'

Result:
case intro
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
A : Type u_1
inst✝¹ : SeminormedRing A
inst✝ : NormedAlgebra 𝕜 A
n : ℕ
hn : 0 < n.succ
⊢ ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n.succ A‖ ≤ 1
-- Mathlib/Data/Finset/Lattice/Fold.lean
theorem _root_.List.foldr_sup_eq_sup_toFinset [DecidableEq α] (l : List α) :
    l.foldr (· ⊔ ·) ⊥ = l.toFinset.sup id

Proof state:
α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
l : List α
⊢ Multiset.fold (fun x1 x2 => x1 ⊔ x2) ⊥ (↑l).dedup = (↑l).dedup.sup

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
l : List α
⊢ List.foldr (fun x1 x2 => x1 ⊔ x2) ⊥ l = l.toFinset.sup id

Tactic:
rw [← coe_fold_r, ← Multiset.fold_dedup_idem, sup_def, ← List.toFinset_coe, toFinset_val,
  Multiset.map_id]

Result:
α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
l : List α
⊢ Multiset.fold (fun x1 x2 => x1 ⊔ x2) ⊥ (↑l).dedup = (↑l).dedup.sup
-- Mathlib/Data/DFinsupp/Module.lean
theorem comapDomain'_smul [Monoid γ] [∀ i, AddMonoid (β i)] [∀ i, DistribMulAction γ (β i)]
    (h : κ → ι) {h' : ι → κ} (hh' : Function.LeftInverse h' h) (r : γ) (f : Π₀ i, β i) :
    comapDomain' h hh' (r • f) = r • comapDomain' h hh' f

Proof state:
case h
ι : Type u
γ : Type w
β : ι → Type v
κ : Type u_1
inst✝² : Monoid γ
inst✝¹ : (i : ι) → AddMonoid (β i)
inst✝ : (i : ι) → DistribMulAction γ (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
r : γ
f : Π₀ (i : ι), β i
i✝ : κ
⊢ (comapDomain' h hh' (r • f)) i✝ = (r • comapDomain' h hh' f) i✝

Tactic:
rw [smul_apply, comapDomain'_apply, smul_apply, comapDomain'_apply]

Result:
no goals

Proof state:
ι : Type u
γ : Type w
β : ι → Type v
κ : Type u_1
inst✝² : Monoid γ
inst✝¹ : (i : ι) → AddMonoid (β i)
inst✝ : (i : ι) → DistribMulAction γ (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
r : γ
f : Π₀ (i : ι), β i
⊢ comapDomain' h hh' (r • f) = r • comapDomain' h hh' f

Tactic:
ext

Result:
case h
ι : Type u
γ : Type w
β : ι → Type v
κ : Type u_1
inst✝² : Monoid γ
inst✝¹ : (i : ι) → AddMonoid (β i)
inst✝ : (i : ι) → DistribMulAction γ (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
r : γ
f : Π₀ (i : ι), β i
i✝ : κ
⊢ (comapDomain' h hh' (r • f)) i✝ = (r • comapDomain' h hh' f) i✝
-- Mathlib/RingTheory/Valuation/ValuationSubring.lean
theorem valuationSubring_valuation : A.valuation.valuationSubring = A

Proof state:
case h
K : Type u
inst✝ : Field K
A : ValuationSubring K
x✝ : K
⊢ x✝ ∈ A.valuation.valuationSubring ↔ x✝ ∈ A

Tactic:
rw [← A.valuation_le_one_iff]

Result:
case h
K : Type u
inst✝ : Field K
A : ValuationSubring K
x✝ : K
⊢ x✝ ∈ A.valuation.valuationSubring ↔ A.valuation x✝ ≤ 1

Proof state:
case h
K : Type u
inst✝ : Field K
A : ValuationSubring K
x✝ : K
⊢ x✝ ∈ A.valuation.valuationSubring ↔ A.valuation x✝ ≤ 1

Tactic:
rfl

Result:
no goals

Proof state:
K : Type u
inst✝ : Field K
A : ValuationSubring K
⊢ A.valuation.valuationSubring = A

Tactic:
ext

Result:
case h
K : Type u
inst✝ : Field K
A : ValuationSubring K
x✝ : K
⊢ x✝ ∈ A.valuation.valuationSubring ↔ x✝ ∈ A
-- Mathlib/Topology/Instances/Matrix.lean
theorem Matrix.conjTranspose_tsum [StarAddMonoid R] [ContinuousStar R] [T2Space R]
    {f : X → Matrix m n R} : (∑' x, f x)ᴴ = ∑' x, (f x)ᴴ

Proof state:
case neg
X : Type u_1
m : Type u_4
n : Type u_5
R : Type u_8
inst✝⁴ : AddCommMonoid R
inst✝³ : TopologicalSpace R
inst✝² : StarAddMonoid R
inst✝¹ : ContinuousStar R
inst✝ : T2Space R
f : X → Matrix m n R
hf : ¬Summable f
hft : ¬Summable fun x => (f x)ᴴ
⊢ (∑' (x : X), f x)ᴴ = ∑' (x : X), (f x)ᴴ

Tactic:
rw [tsum_eq_zero_of_not_summable hf, tsum_eq_zero_of_not_summable hft, conjTranspose_zero]

Result:
no goals

Proof state:
case neg
X : Type u_1
m : Type u_4
n : Type u_5
R : Type u_8
inst✝⁴ : AddCommMonoid R
inst✝³ : TopologicalSpace R
inst✝² : StarAddMonoid R
inst✝¹ : ContinuousStar R
inst✝ : T2Space R
f : X → Matrix m n R
hf : ¬Summable f
⊢ (∑' (x : X), f x)ᴴ = ∑' (x : X), (f x)ᴴ

Tactic:
have hft := summable_matrix_conjTranspose.not.mpr hf

Result:
case neg
X : Type u_1
m : Type u_4
n : Type u_5
R : Type u_8
inst✝⁴ : AddCommMonoid R
inst✝³ : TopologicalSpace R
inst✝² : StarAddMonoid R
inst✝¹ : ContinuousStar R
inst✝ : T2Space R
f : X → Matrix m n R
hf : ¬Summable f
hft : ¬Summable fun x => (f x)ᴴ
⊢ (∑' (x : X), f x)ᴴ = ∑' (x : X), (f x)ᴴ

Proof state:
case pos
X : Type u_1
m : Type u_4
n : Type u_5
R : Type u_8
inst✝⁴ : AddCommMonoid R
inst✝³ : TopologicalSpace R
inst✝² : StarAddMonoid R
inst✝¹ : ContinuousStar R
inst✝ : T2Space R
f : X → Matrix m n R
hf : Summable f
⊢ (∑' (x : X), f x)ᴴ = ∑' (x : X), (f x)ᴴ

Tactic:
exact hf.hasSum.matrix_conjTranspose.tsum_eq.symm

Result:
no goals

Proof state:
X : Type u_1
m : Type u_4
n : Type u_5
R : Type u_8
inst✝⁴ : AddCommMonoid R
inst✝³ : TopologicalSpace R
inst✝² : StarAddMonoid R
inst✝¹ : ContinuousStar R
inst✝ : T2Space R
f : X → Matrix m n R
⊢ (∑' (x : X), f x)ᴴ = ∑' (x : X), (f x)ᴴ

Tactic:
by_cases hf : Summable f

Result:
case pos
X : Type u_1
m : Type u_4
n : Type u_5
R : Type u_8
inst✝⁴ : AddCommMonoid R
inst✝³ : TopologicalSpace R
inst✝² : StarAddMonoid R
inst✝¹ : ContinuousStar R
inst✝ : T2Space R
f : X → Matrix m n R
hf : Summable f
⊢ (∑' (x : X), f x)ᴴ = ∑' (x : X), (f x)ᴴ

case neg
X : Type u_1
m : Type u_4
n : Type u_5
R : Type u_8
inst✝⁴ : AddCommMonoid R
inst✝³ : TopologicalSpace R
inst✝² : StarAddMonoid R
inst✝¹ : ContinuousStar R
inst✝ : T2Space R
f : X → Matrix m n R
hf : ¬Summable f
⊢ (∑' (x : X), f x)ᴴ = ∑' (x : X), (f x)ᴴ
-- Mathlib/SetTheory/Game/PGame.lean
/-- Adding a gift horse right option does not change the value of `x`. A gift horse right option is
 a game `x'` with `x ⧏ x'`. It is called "gift horse" because it seems like Right has gotten the
 "gift" of a new option, but actually the value of the game did not change. -/
lemma insertRight_equiv_of_lf {x x' : PGame} (h : x ⧏ x') : insertRight x x' ≈ x

Proof state:
x x' : PGame
h : x ⧏ x'
⊢ x.insertRight x' ≈ x

Tactic:
rw [← neg_equiv_neg_iff, ← neg_insertLeft_neg]

Result:
x x' : PGame
h : x ⧏ x'
⊢ (-x).insertLeft (-x') ≈ -x

Proof state:
x x' : PGame
h : x ⧏ x'
⊢ (-x).insertLeft (-x') ≈ -x

Tactic:
exact insertLeft_equiv_of_lf (neg_lf_neg_iff.mpr h)

Result:
no goals
-- Mathlib/Algebra/BigOperators/Finsupp.lean
theorem prod_ite_eq [DecidableEq α] (f : α →₀ M) (a : α) (b : α → M → N) :
    (f.prod fun x v => ite (a = x) (b x v) 1) = ite (a ∈ f.support) (b a (f a)) 1

Proof state:
α : Type u_1
M : Type u_8
N : Type u_10
inst✝² : Zero M
inst✝¹ : CommMonoid N
inst✝ : DecidableEq α
f : α →₀ M
a : α
b : α → M → N
⊢ (∏ a_1 ∈ f.support, if a = a_1 then b a_1 (f a_1) else 1) = if a ∈ f.support then b a (f a) else 1

Tactic:
rw [f.support.prod_ite_eq]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_8
N : Type u_10
inst✝² : Zero M
inst✝¹ : CommMonoid N
inst✝ : DecidableEq α
f : α →₀ M
a : α
b : α → M → N
⊢ (f.prod fun x v => if a = x then b x v else 1) = if a ∈ f.support then b a (f a) else 1

Tactic:
dsimp [Finsupp.prod]

Result:
α : Type u_1
M : Type u_8
N : Type u_10
inst✝² : Zero M
inst✝¹ : CommMonoid N
inst✝ : DecidableEq α
f : α →₀ M
a : α
b : α → M → N
⊢ (∏ a_1 ∈ f.support, if a = a_1 then b a_1 (f a_1) else 1) = if a ∈ f.support then b a (f a) else 1
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem infDist_lt_iff {r : ℝ} (hs : s.Nonempty) : infDist x s < r ↔ ∃ y ∈ s, dist x y < r

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x : α
r : ℝ
hs : s.Nonempty
⊢ infDist x s < r ↔ ∃ y ∈ s, dist x y < r

Tactic:
simp_rw [infDist, ← ENNReal.lt_ofReal_iff_toReal_lt (infEdist_ne_top hs), infEdist_lt_iff,
  ENNReal.lt_ofReal_iff_toReal_lt (edist_ne_top _ _), ← dist_edist]

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean
theorem eq_const_to_zero {n : SimplexCategory} (f : n ⟶ ⦋0⦌) :
    f = const n _ 0

Proof state:
case a.h.h
n : SimplexCategory
f : n ⟶ ⦋0⦌
x✝ : Fin (n.len + 1)
⊢ (Hom.toOrderHom f) x✝ = (Hom.toOrderHom (n.const ⦋0⦌ 0)) x✝

Tactic:
apply @Subsingleton.elim (Fin 1)

Result:
no goals

Proof state:
n : SimplexCategory
f : n ⟶ ⦋0⦌
⊢ f = n.const ⦋0⦌ 0

Tactic:
ext : 3

Result:
case a.h.h
n : SimplexCategory
f : n ⟶ ⦋0⦌
x✝ : Fin (n.len + 1)
⊢ (Hom.toOrderHom f) x✝ = (Hom.toOrderHom (n.const ⦋0⦌ 0)) x✝
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldl_toList_eq_flatMap (l : List α) (acc : Array β)
    (F : Array β → α → Array β) (G : α → List β)
    (H : ∀ acc a, (F acc a).toList = acc.toList ++ G a) :
    (l.foldl F acc).toList = acc.toList ++ l.flatMap G

Proof state:
α : Type u_1
β : Type u_2
l : List α
acc : Array β
F : Array β → α → Array β
G : α → List β
H : ∀ (acc : Array β) (a : α), (F acc a).toList = acc.toList ++ G a
⊢ (List.foldl F acc l).toList = acc.toList ++ List.flatMap G l

Tactic:
induction l generalizing acc <;> simp [*, List.flatMap]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
@[to_additive (attr := simp)]
lemma mem_inv' : a ∈ s⁻¹ ↔ a⁻¹ ∈ s

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : InvolutiveInv α
s : Finset α
a : α
⊢ a ∈ s⁻¹ ↔ a⁻¹ ∈ s

Tactic:
simp [mem_inv, inv_eq_iff_eq_inv]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem or_and_distrib_right : ∀ (x y z : Bool), (x && y || z) = ((x || z) && (y || z))

Proof state:
⊢ ∀ (x y z : Bool), (x && y || z) = ((x || z) && (y || z))

Tactic:
decide

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/Composition.lean
theorem index_embedding (i : Fin c.length) (j : Fin (c.blocksFun i)) :
    c.index (c.embedding i j) = i

Proof state:
n : ℕ
c : Composition n
i : Fin c.length
j : Fin (c.blocksFun i)
⊢ i = c.index ((c.embedding i) j)

Tactic:
rw [← mem_range_embedding_iff']

Result:
n : ℕ
c : Composition n
i : Fin c.length
j : Fin (c.blocksFun i)
⊢ (c.embedding i) j ∈ Set.range ⇑(c.embedding i)

Proof state:
n : ℕ
c : Composition n
i : Fin c.length
j : Fin (c.blocksFun i)
⊢ c.index ((c.embedding i) j) = i

Tactic:
symm

Result:
n : ℕ
c : Composition n
i : Fin c.length
j : Fin (c.blocksFun i)
⊢ i = c.index ((c.embedding i) j)

Proof state:
n : ℕ
c : Composition n
i : Fin c.length
j : Fin (c.blocksFun i)
⊢ (c.embedding i) j ∈ Set.range ⇑(c.embedding i)

Tactic:
apply Set.mem_range_self

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/OverAdjunction.lean
@[reassoc (attr := simp)]
lemma Over.pullbackCongr_hom_app_left_fst {X Y : T} {f g : X ⟶ Y} (h : f = g) (A : P.Over Q Y) :
    ((Over.pullbackCongr h).hom.app A).left ≫ pullback.fst A.hom g =
      pullback.fst A.hom f

Proof state:
T : Type u_1
inst✝⁴ : Category.{u_2, u_1} T
P Q : MorphismProperty T
inst✝³ : Q.IsMultiplicative
inst✝² : HasPullbacks T
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : Q.IsStableUnderBaseChange
X Y : T
f : X ⟶ Y
A : P.Over Q Y
⊢ ((pullbackCongr ⋯).hom.app A).left ≫ pullback.fst A.hom f = pullback.fst A.hom f

Tactic:
simp [pullbackCongr]

Result:
no goals

Proof state:
T : Type u_1
inst✝⁴ : Category.{u_2, u_1} T
P Q : MorphismProperty T
inst✝³ : Q.IsMultiplicative
inst✝² : HasPullbacks T
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : Q.IsStableUnderBaseChange
X Y : T
f g : X ⟶ Y
h : f = g
A : P.Over Q Y
⊢ ((pullbackCongr h).hom.app A).left ≫ pullback.fst A.hom g = pullback.fst A.hom f

Tactic:
subst h

Result:
T : Type u_1
inst✝⁴ : Category.{u_2, u_1} T
P Q : MorphismProperty T
inst✝³ : Q.IsMultiplicative
inst✝² : HasPullbacks T
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : Q.IsStableUnderBaseChange
X Y : T
f : X ⟶ Y
A : P.Over Q Y
⊢ ((pullbackCongr ⋯).hom.app A).left ≫ pullback.fst A.hom f = pullback.fst A.hom f
-- Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean
/-- A version of the layer cake formula for bounded continuous functions which have finite integral:
∫ f dμ = ∫ t in (0, ‖f‖], μ {x | f(x) ≥ t} dt. -/
lemma BoundedContinuousFunction.integral_eq_integral_meas_le_of_hasFiniteIntegral
    {α : Type*} [MeasurableSpace α] [TopologicalSpace α] [OpensMeasurableSpace α]
    (f : α →ᵇ ℝ) (μ : Measure α) (f_nn : 0 ≤ᵐ[μ] f) (hf : HasFiniteIntegral f μ) :
    ∫ ω, f ω ∂μ = ∫ t in Ioc 0 ‖f‖, ENNReal.toReal (μ {a : α | t ≤ f a})

Proof state:
α : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
inst✝ : OpensMeasurableSpace α
f : α →ᵇ ℝ
μ : Measure α
f_nn : 0 ≤ᶠ[ae μ] ⇑f
hf : HasFiniteIntegral (⇑f) μ
⊢ ⇑f ≤ᶠ[ae μ] fun x => ‖f‖

Tactic:
exact Eventually.of_forall (fun x ↦ BoundedContinuousFunction.apply_le_norm f x)

Result:
no goals

Proof state:
α : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
inst✝ : OpensMeasurableSpace α
f : α →ᵇ ℝ
μ : Measure α
f_nn : 0 ≤ᶠ[ae μ] ⇑f
hf : HasFiniteIntegral (⇑f) μ
⊢ Integrable (⇑f) μ

Tactic:
refine ⟨f.continuous.measurable.aestronglyMeasurable, hf⟩

Result:
no goals

Proof state:
α : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
inst✝ : OpensMeasurableSpace α
f : α →ᵇ ℝ
μ : Measure α
f_nn : 0 ≤ᶠ[ae μ] ⇑f
hf : HasFiniteIntegral (⇑f) μ
⊢ ∫ (ω : α), f ω ∂μ = ∫ (t : ℝ) in Ioc 0 ‖f‖, (μ {a | t ≤ f a}).toReal

Tactic:
rw [Integrable.integral_eq_integral_Ioc_meas_le (M := ‖f‖) ?_ f_nn ?_]

Result:
α : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
inst✝ : OpensMeasurableSpace α
f : α →ᵇ ℝ
μ : Measure α
f_nn : 0 ≤ᶠ[ae μ] ⇑f
hf : HasFiniteIntegral (⇑f) μ
⊢ Integrable (⇑f) μ

α : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
inst✝ : OpensMeasurableSpace α
f : α →ᵇ ℝ
μ : Measure α
f_nn : 0 ≤ᶠ[ae μ] ⇑f
hf : HasFiniteIntegral (⇑f) μ
⊢ ⇑f ≤ᶠ[ae μ] fun x => ‖f‖
-- Mathlib/Data/Finset/Pairwise.lean
theorem PairwiseDisjoint.image_finset_of_le [DecidableEq ι] {s : Finset ι} {f : ι → α}
    (hs : (s : Set ι).PairwiseDisjoint f) {g : ι → ι} (hf : ∀ a, f (g a) ≤ f a) :
    (s.image g : Set ι).PairwiseDisjoint f

Proof state:
α : Type u_1
ι : Type u_2
inst✝² : SemilatticeInf α
inst✝¹ : OrderBot α
inst✝ : DecidableEq ι
s : Finset ι
f : ι → α
hs : (↑s).PairwiseDisjoint f
g : ι → ι
hf : ∀ (a : ι), f (g a) ≤ f a
⊢ (↑(Finset.image g s)).PairwiseDisjoint f

Tactic:
rw [coe_image]

Result:
α : Type u_1
ι : Type u_2
inst✝² : SemilatticeInf α
inst✝¹ : OrderBot α
inst✝ : DecidableEq ι
s : Finset ι
f : ι → α
hs : (↑s).PairwiseDisjoint f
g : ι → ι
hf : ∀ (a : ι), f (g a) ≤ f a
⊢ (g '' ↑s).PairwiseDisjoint f

Proof state:
α : Type u_1
ι : Type u_2
inst✝² : SemilatticeInf α
inst✝¹ : OrderBot α
inst✝ : DecidableEq ι
s : Finset ι
f : ι → α
hs : (↑s).PairwiseDisjoint f
g : ι → ι
hf : ∀ (a : ι), f (g a) ≤ f a
⊢ (g '' ↑s).PairwiseDisjoint f

Tactic:
exact hs.image_of_le hf

Result:
no goals
-- Mathlib/Data/List/FinRange.lean
theorem ofFn_eq_pmap {n} {f : Fin n → α} :
    ofFn f = pmap (fun i hi => f ⟨i, hi⟩) (range n) fun _ => mem_range.1

Proof state:
α : Type u
n : ℕ
f : Fin n → α
⊢ (ofFn f).length = (map (fun x => f ⟨↑x, ⋯⟩) (range n).attach).length

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
n : ℕ
f : Fin n → α
i : ℕ
hi1 : i < (ofFn f).length
hi2 : i < (map (fun x => f ⟨↑x, ⋯⟩) (range n).attach).length
⊢ (ofFn f)[i] = (map (fun x => f ⟨↑x, ⋯⟩) (range n).attach)[i]

Tactic:
simp [List.getElem_ofFn f i hi1]

Result:
no goals

Proof state:
α : Type u
n : ℕ
f : Fin n → α
⊢ ofFn f = map (fun x => f ⟨↑x, ⋯⟩) (range n).attach

Tactic:
exact ext_getElem (by simp) fun i hi1 hi2 => by simp [List.getElem_ofFn f i hi1]

Result:
no goals

Proof state:
α : Type u
n : ℕ
f : Fin n → α
⊢ ofFn f = pmap (fun i hi => f ⟨i, hi⟩) (range n) ⋯

Tactic:
rw [pmap_eq_map_attach]

Result:
α : Type u
n : ℕ
f : Fin n → α
⊢ ofFn f = map (fun x => f ⟨↑x, ⋯⟩) (range n).attach
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem attach_map_subtype_val (l : Vector α n) : l.attach.map Subtype.val = l

Proof state:
α : Type u_1
n : Nat
l : Vector α n
⊢ map Subtype.val l.attach = l

Tactic:
cases l

Result:
case mk
α : Type u_1
n : Nat
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ map Subtype.val { toArray := toArray✝, size_toArray := size_toArray✝ }.attach =
    { toArray := toArray✝, size_toArray := size_toArray✝ }

Proof state:
case mk
α : Type u_1
n : Nat
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ map Subtype.val { toArray := toArray✝, size_toArray := size_toArray✝ }.attach =
    { toArray := toArray✝, size_toArray := size_toArray✝ }

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Disjoint.lean
theorem isCompl_coe : IsCompl (a : α) b ↔ IsCompl a b

Proof state:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a b : Complementeds α
⊢ IsCompl ↑a ↑b ↔ IsCompl a b

Tactic:
simp_rw [isCompl_iff, disjoint_coe, codisjoint_coe]

Result:
no goals
-- Mathlib/Data/Nat/Nth.lean
theorem nth_zero_of_exists [DecidablePred p] (h : ∃ n, p n) : nth p 0 = Nat.find h

Proof state:
p : ℕ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
⊢ sInf (setOf p) = Nat.find h

Tactic:
convert Nat.sInf_def h

Result:
no goals

Proof state:
p : ℕ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
⊢ nth p 0 = Nat.find h

Tactic:
rw [nth_zero]

Result:
p : ℕ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
⊢ sInf (setOf p) = Nat.find h
-- Mathlib/CategoryTheory/Shift/Basic.lean
theorem shiftComm_symm (i j : A) : (shiftComm X i j).symm = shiftComm X j i

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
X : C
i j : A
⊢ (shiftComm X i j).symm = shiftComm X j i

Tactic:
ext

Result:
case w
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
X : C
i j : A
⊢ (shiftComm X i j).symm.hom = (shiftComm X j i).hom

Proof state:
case w
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
X : C
i j : A
⊢ (shiftComm X i j).symm.hom = (shiftComm X j i).hom

Tactic:
exact NatTrans.congr_app (congr_arg Iso.hom (shiftFunctorComm_symm C i j)) X

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean
theorem eval_rotateRight : eval (rotateRight n) = ((BitVec.rotateRight · n) : BitVec w → BitVec w)

Proof state:
n w : Nat
⊢ (rotateRight n).eval = fun x => x.rotateRight n

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/Compactness/Compact.lean
theorem IsCompact.elim_finite_subfamily_closed {ι : Type v} (hs : IsCompact s)
    (t : ι → Set X) (htc : ∀ i, IsClosed (t i)) (hst : (s ∩ ⋂ i, t i) = ∅) :
    ∃ u : Finset ι, (s ∩ ⋂ i ∈ u, t i) = ∅ :=
  hs.elim_directed_family_closed _ (fun _ ↦ isClosed_biInter fun _ _ ↦ htc _)
    (by rwa [← iInter_eq_iInter_finset])
    (directed_of_isDirected_le fun _ _ h ↦ biInter_subset_biInter_left h)

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
ι : Type v
hs : IsCompact s
t : ι → Set X
htc : ∀ (i : ι), IsClosed (t i)
hst : s ∩ ⋂ i, t i = ∅
⊢ s ∩ ⋂ i, ⋂ i_1 ∈ i, t i_1 = ∅

Tactic:
rwa [← iInter_eq_iInter_finset]

Result:
no goals
-- Mathlib/Data/ENNReal/Real.lean
theorem toNNReal_mul_top (a : ℝ≥0∞) : ENNReal.toNNReal (a * ∞) = 0

Proof state:
a : ℝ≥0∞
⊢ (a * ⊤).toNNReal = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Logic/Hydra.lean
theorem acc_of_singleton [IsIrrefl α r] {s : Multiset α} (hs : ∀ a ∈ s, Acc (CutExpand r) {a}) :
    Acc (CutExpand r) s

Proof state:
case cons
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
a : α
s : Multiset α
ihs : (∀ a ∈ s, Acc (CutExpand r) {a}) → Acc (CutExpand r) s
hs : Acc (CutExpand r) {a} ∧ ∀ x ∈ s, Acc (CutExpand r) {x}
⊢ Acc (CutExpand r) ({a} + s)

Tactic:
exact (hs.1.prod_gameAdd <| ihs fun a ha ↦ hs.2 a ha).of_fibration _ (cutExpand_fibration r)

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
s : Multiset α
hs : ∀ a ∈ s, Acc (CutExpand r) {a}
⊢ Acc (CutExpand r) s

Tactic:
induction s using Multiset.induction with
| empty => exact Acc.intro 0 fun s h ↦ (not_cutExpand_zero s h).elim
| cons a s ihs =>
  rw [← s.singleton_add a]
  rw [forall_mem_cons] at hs
  exact (hs.1.prod_gameAdd <| ihs fun a ha ↦ hs.2 a ha).of_fibration _ (cutExpand_fibration r)

Result:
no goals

Proof state:
case cons
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
a : α
s : Multiset α
ihs : (∀ a ∈ s, Acc (CutExpand r) {a}) → Acc (CutExpand r) s
hs : ∀ a_1 ∈ a ::ₘ s, Acc (CutExpand r) {a_1}
⊢ Acc (CutExpand r) (a ::ₘ s)

Tactic:
rw [← s.singleton_add a]

Result:
case cons
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
a : α
s : Multiset α
ihs : (∀ a ∈ s, Acc (CutExpand r) {a}) → Acc (CutExpand r) s
hs : ∀ a_1 ∈ a ::ₘ s, Acc (CutExpand r) {a_1}
⊢ Acc (CutExpand r) ({a} + s)

Proof state:
case empty
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
hs : ∀ a ∈ 0, Acc (CutExpand r) {a}
⊢ Acc (CutExpand r) 0

Tactic:
exact Acc.intro 0 fun s h ↦ (not_cutExpand_zero s h).elim

Result:
no goals

Proof state:
case cons
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
a : α
s : Multiset α
ihs : (∀ a ∈ s, Acc (CutExpand r) {a}) → Acc (CutExpand r) s
hs : ∀ a_1 ∈ a ::ₘ s, Acc (CutExpand r) {a_1}
⊢ Acc (CutExpand r) ({a} + s)

Tactic:
rw [forall_mem_cons] at hs

Result:
case cons
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
a : α
s : Multiset α
ihs : (∀ a ∈ s, Acc (CutExpand r) {a}) → Acc (CutExpand r) s
hs : Acc (CutExpand r) {a} ∧ ∀ x ∈ s, Acc (CutExpand r) {x}
⊢ Acc (CutExpand r) ({a} + s)
-- Mathlib/Data/Matrix/Mul.lean
theorem smul_eq_mul_diagonal [Fintype n] [DecidableEq n] (M : Matrix m n α) (a : α) :
    a • M = M * diagonal fun _ => a

Proof state:
m : Type u_2
n : Type u_3
α : Type v
inst✝² : CommSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix m n α
a : α
⊢ a • M = M * diagonal fun x => a

Tactic:
ext

Result:
case a
m : Type u_2
n : Type u_3
α : Type v
inst✝² : CommSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix m n α
a : α
i✝ : m
j✝ : n
⊢ (a • M) i✝ j✝ = (M * diagonal fun x => a) i✝ j✝

Proof state:
case a
m : Type u_2
n : Type u_3
α : Type v
inst✝² : CommSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix m n α
a : α
i✝ : m
j✝ : n
⊢ (a • M) i✝ j✝ = (M * diagonal fun x => a) i✝ j✝

Tactic:
simp [mul_comm]

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Monoidal/Normalize.lean
theorem evalHorizontalComp_nil_cons {f f' g g' h i : C}
    {α : f ≅ g} {β : f' ≅ g'} {η : g' ⟶ h} {ηs : h ⟶ i}
    {η₁ : g ⊗ g' ⟶ g ⊗ h} {ηs₁ : g ⊗ h ⟶ g ⊗ i}
    {η₂ : g ⊗ g' ⟶ g ⊗ i} {η₃ : f ⊗ f' ⟶ g ⊗ i}
    (e_η₁ : g ◁ ((Iso.refl _).hom ≫ η ≫ (Iso.refl _).hom) = η₁)
    (e_ηs₁ : g ◁ ηs = ηs₁) (e_η₂ : η₁ ≫ ηs₁ = η₂)
    (e_η₃ : (α ⊗ β).hom ≫ η₂ = η₃) :
    α.hom ⊗ (β.hom ≫ η ≫ ηs) = η₃

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f f' g g' h i : C
α : f ≅ g
β : f' ≅ g'
η : g' ⟶ h
ηs : h ⟶ i
η₁ : g ⊗ g' ⟶ g ⊗ h
ηs₁ : g ⊗ h ⟶ g ⊗ i
η₂ : g ⊗ g' ⟶ g ⊗ i
η₃ : f ⊗ f' ⟶ g ⊗ i
e_η₁ : g ◁ ((Iso.refl g').hom ≫ η ≫ (Iso.refl h).hom) = η₁
e_ηs₁ : g ◁ ηs = ηs₁
e_η₂ : η₁ ≫ ηs₁ = η₂
e_η₃ : (α ⊗ β).hom ≫ η₂ = η₃
⊢ α.hom ⊗ β.hom ≫ η ≫ ηs = η₃

Tactic:
simp_all [MonoidalCategory.tensorHom_def]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem mem_iff_mem_toList {t : RBSet α cmp} : x ∈ t ↔ ∃ y ∈ toList t, cmp x y = .eq :=
  RBNode.mem_def.trans <| by simp [mem_toList]

Proof state:
α : Type u_1
cmp : α → α → Ordering
x : α
t : RBSet α cmp
⊢ (∃ y, y ∈ t.val ∧ cmp x y = Ordering.eq) ↔ ∃ y, y ∈ t.toList ∧ cmp x y = Ordering.eq

Tactic:
simp [mem_toList]

Result:
no goals
-- Mathlib/Data/Finset/Insert.lean
@[norm_cast]
lemma coe_subset_singleton : (s : Set α) ⊆ {a} ↔ s ⊆ {a}

Proof state:
α : Type u_1
s : Finset α
a : α
⊢ ↑s ⊆ {a} ↔ s ⊆ {a}

Tactic:
rw [← coe_subset, coe_singleton]

Result:
no goals