harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean
lemma cfcₙ_apply : cfcₙ f a = cfcₙHom (a := a) ha ⟨⟨_, hf.restrict⟩, hf0⟩

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R p
f : R → R
a : A
hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝
hf0 : autoParam (f 0 = 0) _auto✝
ha : autoParam (p a) _auto✝
⊢ cfcₙ f a = (cfcₙHom ha) { toFun := (σₙ R a).restrict f, continuous_toFun := ⋯, map_zero' := hf0 }

Tactic:
rw [cfcₙ_def, dif_pos ⟨ha, hf, hf0⟩]

Result:
no goals
-- Mathlib/Topology/Bornology/Constructions.lean
theorem boundedSpace_subtype_iff {p : α → Prop} :
    BoundedSpace (Subtype p) ↔ IsBounded { x | p x }

Proof state:
α : Type u_1
inst✝ : Bornology α
p : α → Prop
⊢ BoundedSpace (Subtype p) ↔ Bornology.IsBounded {x | p x}

Tactic:
rw [boundedSpace_induced_iff, Subtype.range_coe_subtype]

Result:
no goals
-- Mathlib/Data/Finset/Insert.lean
theorem coe_cons {a s h} : (@cons α a s h : Set α) = insert a (s : Set α)

Proof state:
α : Type u_1
a : α
s : Finset α
h : a ∉ s
⊢ ↑(cons a s h) = insert a ↑s

Tactic:
ext

Result:
case h
α : Type u_1
a : α
s : Finset α
h : a ∉ s
x✝ : α
⊢ x✝ ∈ ↑(cons a s h) ↔ x✝ ∈ insert a ↑s

Proof state:
case h
α : Type u_1
a : α
s : Finset α
h : a ∉ s
x✝ : α
⊢ x✝ ∈ ↑(cons a s h) ↔ x✝ ∈ insert a ↑s

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem lt_of_getMsb?_isSome (x : BitVec w) (i : Nat) : (getMsb? x i).isSome → i < w

Proof state:
w : Nat
x : BitVec w
i : Nat
⊢ (x.getMsb? i).isSome = true → i < w

Tactic:
if h : i < w then
  simp [h]
else
  simp [Nat.ge_of_not_lt h]

Result:
no goals

Proof state:
w : Nat
x : BitVec w
i : Nat
h : ¬i < w
⊢ (x.getMsb? i).isSome = true → i < w

Tactic:
simp [Nat.ge_of_not_lt h]

Result:
no goals

Proof state:
w : Nat
x : BitVec w
i : Nat
h : i < w
⊢ (x.getMsb? i).isSome = true → i < w

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Order.lean
theorem tprod_le_of_prod_le' (ha₂ : 1 ≤ a₂) (h : ∀ s, ∏ i ∈ s, f i ≤ a₂) : ∏' i, f i ≤ a₂

Proof state:
case neg
ι : Type u_1
α : Type u_3
inst✝² : OrderedCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a₂ : α
ha₂ : 1 ≤ a₂
h : ∀ (s : Finset ι), ∏ i ∈ s, f i ≤ a₂
hf : ¬Multipliable f
⊢ 1 ≤ a₂

Tactic:
exact ha₂

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_3
inst✝² : OrderedCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a₂ : α
ha₂ : 1 ≤ a₂
h : ∀ (s : Finset ι), ∏ i ∈ s, f i ≤ a₂
⊢ ∏' (i : ι), f i ≤ a₂

Tactic:
by_cases hf : Multipliable f

Result:
case pos
ι : Type u_1
α : Type u_3
inst✝² : OrderedCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a₂ : α
ha₂ : 1 ≤ a₂
h : ∀ (s : Finset ι), ∏ i ∈ s, f i ≤ a₂
hf : Multipliable f
⊢ ∏' (i : ι), f i ≤ a₂

case neg
ι : Type u_1
α : Type u_3
inst✝² : OrderedCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a₂ : α
ha₂ : 1 ≤ a₂
h : ∀ (s : Finset ι), ∏ i ∈ s, f i ≤ a₂
hf : ¬Multipliable f
⊢ ∏' (i : ι), f i ≤ a₂

Proof state:
case neg
ι : Type u_1
α : Type u_3
inst✝² : OrderedCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a₂ : α
ha₂ : 1 ≤ a₂
h : ∀ (s : Finset ι), ∏ i ∈ s, f i ≤ a₂
hf : ¬Multipliable f
⊢ ∏' (i : ι), f i ≤ a₂

Tactic:
rw [tprod_eq_one_of_not_multipliable hf]

Result:
case neg
ι : Type u_1
α : Type u_3
inst✝² : OrderedCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a₂ : α
ha₂ : 1 ≤ a₂
h : ∀ (s : Finset ι), ∏ i ∈ s, f i ≤ a₂
hf : ¬Multipliable f
⊢ 1 ≤ a₂

Proof state:
case pos
ι : Type u_1
α : Type u_3
inst✝² : OrderedCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a₂ : α
ha₂ : 1 ≤ a₂
h : ∀ (s : Finset ι), ∏ i ∈ s, f i ≤ a₂
hf : Multipliable f
⊢ ∏' (i : ι), f i ≤ a₂

Tactic:
exact tprod_le_of_prod_le hf h

Result:
no goals
-- Mathlib/Topology/Algebra/Valued/ValuedField.lean
theorem extension_extends (x : K) : extension (x : hat K) = v x

Proof state:
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x : K
⊢ Tendsto (⇑v) (𝓝 x) (𝓝 (v x))

Tactic:
exact Valued.continuous_valuation.continuousAt

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x : K
⊢ extension ↑x = v x

Tactic:
refine Completion.isDenseInducing_coe.extend_eq_of_tendsto ?_

Result:
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x : K
⊢ Tendsto (⇑v) (Filter.comap Completion.coe' (𝓝 ↑x)) (𝓝 (v x))

Proof state:
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x : K
⊢ Tendsto (⇑v) (Filter.comap Completion.coe' (𝓝 ↑x)) (𝓝 (v x))

Tactic:
rw [← Completion.isDenseInducing_coe.nhds_eq_comap]

Result:
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x : K
⊢ Tendsto (⇑v) (𝓝 x) (𝓝 (v x))
-- Mathlib/Combinatorics/SimpleGraph/Diam.lean
lemma diam_eq_zero_of_ediam_eq_top (h : G.ediam = ⊤) : G.diam = 0

Proof state:
α : Type u_1
G : SimpleGraph α
h : G.ediam = ⊤
⊢ G.diam = 0

Tactic:
rw [diam, h, ENat.toNat_top]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
theorem prod.associator_naturality [HasBinaryProducts C] {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁)
    (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) :
    prod.map (prod.map f₁ f₂) f₃ ≫ (prod.associator Y₁ Y₂ Y₃).hom =
      (prod.associator X₁ X₂ X₃).hom ≫ prod.map f₁ (prod.map f₂ f₃)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasBinaryProducts C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ map (map f₁ f₂) f₃ ≫ (associator Y₁ Y₂ Y₃).hom = (associator X₁ X₂ X₃).hom ≫ map f₁ (map f₂ f₃)

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem mem_unitOfList [EquivBEq α] [LawfulHashable α]
    {l : List α} {k : α} :
    k ∈ unitOfList l ↔ l.contains k

Proof state:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List α
k : α
⊢ k ∈ unitOfList l ↔ l.contains k = true

Tactic:
simp [mem_iff_contains]

Result:
no goals
-- Mathlib/RingTheory/Algebraic/Integral.lean
lemma extendScalars [NoZeroDivisors S] [Algebra.IsAlgebraic R S] : Transcendental S a

Proof state:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Ring A
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
a : A
inst✝¹ : NoZeroDivisors S
inst✝ : Algebra.IsAlgebraic R S
ha : IsAlgebraic S a
⊢ IsAlgebraic R a

Tactic:
exact ha.restrictScalars _

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Ring A
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
a : A
inst✝¹ : NoZeroDivisors S
inst✝ : Algebra.IsAlgebraic R S
ha : ¬Transcendental S a
⊢ ¬Transcendental R a

Tactic:
rw [Transcendental, not_not] at ha ⊢

Result:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Ring A
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
a : A
inst✝¹ : NoZeroDivisors S
inst✝ : Algebra.IsAlgebraic R S
ha : IsAlgebraic S a
⊢ IsAlgebraic R a

Proof state:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Ring A
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
a : A
ha : Transcendental R a
inst✝¹ : NoZeroDivisors S
inst✝ : Algebra.IsAlgebraic R S
⊢ Transcendental S a

Tactic:
contrapose ha

Result:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Ring A
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
a : A
inst✝¹ : NoZeroDivisors S
inst✝ : Algebra.IsAlgebraic R S
ha : ¬Transcendental S a
⊢ ¬Transcendental R a
-- Mathlib/Data/ENat/Lattice.lean
lemma add_iSup [Nonempty ι] (f : ι → ℕ∞) : a + ⨆ i, f i = ⨆ i, a + f i

Proof state:
case inr
ι : Sort u_2
a : ℕ∞
inst✝ : Nonempty ι
f : ι → ℕ∞
ha : a ≠ ⊤
⊢ a + ⨆ i, f i = ⨆ i, a + f i

Tactic:
refine le_antisymm ?_ <| iSup_le fun i ↦ add_le_add_left (le_iSup ..) _

Result:
case inr
ι : Sort u_2
a : ℕ∞
inst✝ : Nonempty ι
f : ι → ℕ∞
ha : a ≠ ⊤
⊢ a + ⨆ i, f i ≤ ⨆ i, a + f i

Proof state:
ι : Sort u_2
a : ℕ∞
inst✝ : Nonempty ι
f : ι → ℕ∞
⊢ a + ⨆ i, f i = ⨆ i, a + f i

Tactic:
obtain rfl | ha := eq_or_ne a ⊤

Result:
case inl
ι : Sort u_2
inst✝ : Nonempty ι
f : ι → ℕ∞
⊢ ⊤ + ⨆ i, f i = ⨆ i, ⊤ + f i

case inr
ι : Sort u_2
a : ℕ∞
inst✝ : Nonempty ι
f : ι → ℕ∞
ha : a ≠ ⊤
⊢ a + ⨆ i, f i = ⨆ i, a + f i

Proof state:
case inr
ι : Sort u_2
a : ℕ∞
inst✝ : Nonempty ι
f : ι → ℕ∞
ha : a ≠ ⊤
⊢ a + ⨆ i, f i ≤ ⨆ i, a + f i

Tactic:
refine add_le_of_le_tsub_left_of_le (le_iSup_of_le (Classical.arbitrary _) le_self_add) ?_

Result:
case inr
ι : Sort u_2
a : ℕ∞
inst✝ : Nonempty ι
f : ι → ℕ∞
ha : a ≠ ⊤
⊢ ⨆ i, f i ≤ (⨆ i, a + f i) - a

Proof state:
case inl
ι : Sort u_2
inst✝ : Nonempty ι
f : ι → ℕ∞
⊢ ⊤ + ⨆ i, f i = ⨆ i, ⊤ + f i

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem cast_succ (n : ℕ) : ((n + 1 : ℕ) : Cardinal.{u}) = n + 1

Proof state:
n : ℕ
⊢ ↑(n + 1) = ↑n + 1

Tactic:
change #(ULift.{u} _) = #(ULift.{u} _) + 1

Result:
n : ℕ
⊢ #(ULift.{u, 0} (Fin (n + 1))) = #(ULift.{u, 0} (Fin n)) + 1

Proof state:
n : ℕ
⊢ #(ULift.{u, 0} (Fin (n + 1))) = #(ULift.{u, 0} (Fin n)) + 1

Tactic:
rw [← mk_option]

Result:
n : ℕ
⊢ #(ULift.{u, 0} (Fin (n + 1))) = #(Option (ULift.{u, 0} (Fin n)))

Proof state:
n : ℕ
⊢ #(ULift.{u, 0} (Fin (n + 1))) = #(Option (ULift.{u, 0} (Fin n)))

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Adjugate.lean
theorem adjugate_subsingleton [Subsingleton n] (A : Matrix n n α) : adjugate A = 1

Proof state:
case a
n : Type v
α : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : CommRing α
inst✝ : Subsingleton n
A : Matrix n n α
i j : n
⊢ A.adjugate i j = 1 i j

Tactic:
simp [Subsingleton.elim i j, adjugate_apply, det_eq_elem_of_subsingleton _ i, one_apply]

Result:
no goals

Proof state:
n : Type v
α : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : CommRing α
inst✝ : Subsingleton n
A : Matrix n n α
⊢ A.adjugate = 1

Tactic:
ext i j

Result:
case a
n : Type v
α : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : CommRing α
inst✝ : Subsingleton n
A : Matrix n n α
i j : n
⊢ A.adjugate i j = 1 i j
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem div_lt_one_of_neg (hb : b < 0) : a / b < 1 ↔ b < a

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a b : α
hb : b < 0
⊢ a / b < 1 ↔ b < a

Tactic:
rw [div_lt_iff_of_neg hb, one_mul]

Result:
no goals
-- Mathlib/GroupTheory/Coprod/Basic.lean
theorem comp_lift {P' : Type*} [Monoid P'] (f : P →* P') (g₁ : M →* P) (g₂ : N →* P) :
    f.comp (lift g₁ g₂) = lift (f.comp g₁) (f.comp g₂) :=
  hom_ext (by rw [MonoidHom.comp_assoc, lift_comp_inl, lift_comp_inl]) <| by
    rw [MonoidHom.comp_assoc, lift_comp_inr, lift_comp_inr]

Proof state:
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : Monoid P
P' : Type u_4
inst✝ : Monoid P'
f : P →* P'
g₁ : M →* P
g₂ : N →* P
⊢ (f.comp (lift g₁ g₂)).comp inr = (lift (f.comp g₁) (f.comp g₂)).comp inr

Tactic:
rw [MonoidHom.comp_assoc, lift_comp_inr, lift_comp_inr]

Result:
no goals

Proof state:
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : Monoid P
P' : Type u_4
inst✝ : Monoid P'
f : P →* P'
g₁ : M →* P
g₂ : N →* P
⊢ (f.comp (lift g₁ g₂)).comp inl = (lift (f.comp g₁) (f.comp g₂)).comp inl

Tactic:
rw [MonoidHom.comp_assoc, lift_comp_inl, lift_comp_inl]

Result:
no goals
-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem coe_normUnit {p : R[X]} : (normUnit p : R[X]) = C ↑(normUnit p.leadingCoeff)

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizationMonoid R
p : R[X]
⊢ ↑(normUnit p) = C ↑(normUnit p.leadingCoeff)

Tactic:
simp [normUnit]

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
@[simp]
protected lemma id_comp {n : ℤ} (z₂ : Cochain F G n) :
    (Cochain.ofHom (𝟙 F)).comp z₂ (zero_add n) = z₂

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n : ℤ
z₂ : Cochain F G n
⊢ (ofHom (𝟙 F)).comp z₂ ⋯ = z₂

Tactic:
ext p q hpq

Result:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n : ℤ
z₂ : Cochain F G n
p q : ℤ
hpq : p + n = q
⊢ ((ofHom (𝟙 F)).comp z₂ ⋯).v p q hpq = z₂.v p q hpq

Proof state:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n : ℤ
z₂ : Cochain F G n
p q : ℤ
hpq : p + n = q
⊢ ((ofHom (𝟙 F)).comp z₂ ⋯).v p q hpq = z₂.v p q hpq

Tactic:
simp only [zero_cochain_comp_v, ofHom_v, HomologicalComplex.id_f, id_comp]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/PiL2.lean
theorem repr_symm_single [DecidableEq ι] (b : OrthonormalBasis ι 𝕜 E) (i : ι) :
    b.repr.symm (EuclideanSpace.single i (1 : 𝕜)) = b i

Proof state:
ι : Type u_1
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : OrthonormalBasis ι 𝕜 E
i : ι
⊢ b.repr.symm (EuclideanSpace.single i 1) = b i

Tactic:
dsimp only [DFunLike.coe]

Result:
ι : Type u_1
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : OrthonormalBasis ι 𝕜 E
i : ι
⊢ EquivLike.coe b.repr.symm (EuclideanSpace.single i 1) = EquivLike.coe b.repr.symm (EuclideanSpace.single i 1)

Proof state:
ι : Type u_1
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : OrthonormalBasis ι 𝕜 E
i : ι
⊢ EquivLike.coe b.repr.symm (EuclideanSpace.single i 1) = EquivLike.coe b.repr.symm (EuclideanSpace.single i 1)

Tactic:
congr!

Result:
no goals
-- Mathlib/Algebra/Order/Group/CompleteLattice.lean
@[to_additive]
lemma ciSup_div (hf : BddAbove (range f)) (a : G) : (⨆ i, f i) / a = ⨆ i, f i / a

Proof state:
ι : Type u_1
G : Type u_2
inst✝³ : Group G
inst✝² : ConditionallyCompleteLattice G
inst✝¹ : Nonempty ι
f : ι → G
inst✝ : MulRightMono G
hf : BddAbove (range f)
a : G
⊢ (⨆ i, f i) / a = ⨆ i, f i / a

Tactic:
simp only [div_eq_mul_inv, ciSup_mul hf]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
/-- See also `Finset.prod_dite_eq`. -/
@[to_additive "See also `Finset.sum_dite_eq`."] lemma prod_dite_eq (i : ι) (f : ∀ j, i = j → α) :
    ∏ j, (if h : i = j then f j h else 1) = f i rfl

Proof state:
ι : Type u_6
α : Type u_8
inst✝² : Fintype ι
inst✝¹ : CommMonoid α
inst✝ : DecidableEq ι
i : ι
f : (j : ι) → i = j → α
⊢ (∏ j : ι, if h : i = j then f j h else 1) = f i ⋯

Tactic:
rw [Finset.prod_dite_eq, if_pos (mem_univ _)]

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem casesOn' {f g} (hf : Nat.Primrec f) (hg : Nat.Primrec g) :
    Nat.Primrec (unpaired fun z n => n.casesOn (f z) fun y => g <| Nat.pair z y) :=
  (prec hf (hg.comp (pair left (left.comp right)))).of_eq fun n => by simp

Proof state:
f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
n : ℕ
⊢ unpaired
      (fun z n =>
        Nat.rec (f z)
          (fun y IH =>
            g (Nat.pair (unpair (Nat.pair z (Nat.pair y IH))).1 (unpair (unpair (Nat.pair z (Nat.pair y IH))).2).1))
          n)
      n =
    unpaired (fun z n => Nat.casesOn n (f z) fun y => g (Nat.pair z y)) n

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Normed/Module/Convex.lean
theorem Convex.thickening (hs : Convex ℝ s) (δ : ℝ) : Convex ℝ (thickening δ s)

Proof state:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
hs : Convex ℝ s
δ : ℝ
⊢ Convex ℝ (Metric.thickening δ s)

Tactic:
rw [← add_ball_zero]

Result:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
hs : Convex ℝ s
δ : ℝ
⊢ Convex ℝ (s + ball 0 δ)

Proof state:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
hs : Convex ℝ s
δ : ℝ
⊢ Convex ℝ (s + ball 0 δ)

Tactic:
exact hs.add (convex_ball 0 _)

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Homogeneous.lean
theorem totalDegree_zero_iff_isHomogeneous {p : MvPolynomial σ R} :
    p.totalDegree = 0 ↔ IsHomogeneous p 0

Proof state:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ p.totalDegree = 0 ↔ p.IsHomogeneous 0

Tactic:
rw [← weightedTotalDegree_one,
  ← isWeightedHomogeneous_zero_iff_weightedTotalDegree_eq_zero, IsHomogeneous]

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean
protected lemma add_lt_add_left [LT α] [AddLeftStrictMono α] (hx : x ≠ ⊤) :
    y < z → x + y < x + z

Proof state:
case intro
α : Type u
inst✝² : Add α
y z : WithTop α
inst✝¹ : LT α
inst✝ : AddLeftStrictMono α
x : α
⊢ y < z → ↑x + y < ↑x + z

Tactic:
cases y <;> cases z <;> simp [← coe_add]

Result:
case intro.coe.coe
α : Type u
inst✝² : Add α
inst✝¹ : LT α
inst✝ : AddLeftStrictMono α
x a✝¹ a✝ : α
⊢ a✝¹ < a✝ → x + a✝¹ < x + a✝

Proof state:
α : Type u
inst✝² : Add α
x y z : WithTop α
inst✝¹ : LT α
inst✝ : AddLeftStrictMono α
hx : x ≠ ⊤
⊢ y < z → x + y < x + z

Tactic:
lift x to α using hx

Result:
case intro
α : Type u
inst✝² : Add α
y z : WithTop α
inst✝¹ : LT α
inst✝ : AddLeftStrictMono α
x : α
⊢ y < z → ↑x + y < ↑x + z
-- Mathlib/Data/Matrix/Bilinear.lean
theorem pow_mulLeftLinearMap (a : Matrix m m A) (k : ℕ) :
    mulLeftLinearMap n R a ^ k = mulLeftLinearMap n R (a ^ k) :=
  match k with
  | 0 => by rw [pow_zero, pow_zero, mulLeftLinearMap_one, LinearMap.one_eq_id]
  | (n + 1) => by
    rw [pow_succ, pow_succ, mulLeftLinearMap_mul, LinearMap.mul_eq_comp, pow_mulLeftLinearMap]

Proof state:
m : Type u_2
n✝ : Type u_3
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
inst✝³ : Semiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : SMulCommClass R A A
a : Matrix m m A
k n : ℕ
⊢ mulLeftLinearMap n✝ R a ^ (n + 1) = mulLeftLinearMap n✝ R (a ^ (n + 1))

Tactic:
rw [pow_succ, pow_succ, mulLeftLinearMap_mul, LinearMap.mul_eq_comp, pow_mulLeftLinearMap]

Result:
no goals

Proof state:
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
inst✝³ : Semiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : SMulCommClass R A A
a : Matrix m m A
k : ℕ
⊢ mulLeftLinearMap n R a ^ 0 = mulLeftLinearMap n R (a ^ 0)

Tactic:
rw [pow_zero, pow_zero, mulLeftLinearMap_one, LinearMap.one_eq_id]

Result:
no goals
-- Mathlib/Data/Int/Init.lean
@[simp] lemma toNat_pred_coe_of_pos {i : ℤ} (h : 0 < i) : ((i.toNat - 1 : ℕ) : ℤ) = i - 1

Proof state:
i : ℤ
h : 0 < i
⊢ ↑(i.toNat - 1) = i - 1

Tactic:
simp only [lt_toNat, Nat.cast_ofNat_Int, h, natCast_pred_of_pos, Int.le_of_lt h, toNat_of_nonneg]

Result:
no goals
-- Mathlib/Data/Set/BoolIndicator.lean
theorem mem_iff_boolIndicator (x : α) : x ∈ s ↔ s.boolIndicator x = true

Proof state:
α : Type u_1
s : Set α
x : α
⊢ x ∈ s ↔ s.boolIndicator x = true

Tactic:
unfold boolIndicator

Result:
α : Type u_1
s : Set α
x : α
⊢ x ∈ s ↔ (if x ∈ s then true else false) = true

Proof state:
α : Type u_1
s : Set α
x : α
⊢ x ∈ s ↔ (if x ∈ s then true else false) = true

Tactic:
split_ifs with h <;> simp [h]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/GramSchmidtOrtho.lean
theorem gramSchmidtOrthonormalBasis_det [DecidableEq ι] :
    (gramSchmidtOrthonormalBasis h f).toBasis.det f =
      ∏ i, ⟪gramSchmidtOrthonormalBasis h f i, f i⟫

Proof state:
case h.e'_3.a
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝⁵ : LinearOrder ι
inst✝⁴ : LocallyFiniteOrderBot ι
inst✝³ : WellFoundedLT ι
inst✝² : Fintype ι
inst✝¹ : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f : ι → E
inst✝ : DecidableEq ι
x✝ : ι
a✝ : x✝ ∈ Finset.univ
⊢ inner ((gramSchmidtOrthonormalBasis h f) x✝) (f x✝) = (gramSchmidtOrthonormalBasis h f).toBasis.toMatrix f x✝ x✝

Tactic:
exact ((gramSchmidtOrthonormalBasis h f).repr_apply_apply (f _) _).symm

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝⁵ : LinearOrder ι
inst✝⁴ : LocallyFiniteOrderBot ι
inst✝³ : WellFoundedLT ι
inst✝² : Fintype ι
inst✝¹ : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f : ι → E
inst✝ : DecidableEq ι
⊢ (gramSchmidtOrthonormalBasis h f).toBasis.det f = ∏ i : ι, inner ((gramSchmidtOrthonormalBasis h f) i) (f i)

Tactic:
convert Matrix.det_of_upperTriangular (gramSchmidtOrthonormalBasis_inv_blockTriangular h f)

Result:
case h.e'_3.a
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝⁵ : LinearOrder ι
inst✝⁴ : LocallyFiniteOrderBot ι
inst✝³ : WellFoundedLT ι
inst✝² : Fintype ι
inst✝¹ : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f : ι → E
inst✝ : DecidableEq ι
x✝ : ι
a✝ : x✝ ∈ Finset.univ
⊢ inner ((gramSchmidtOrthonormalBasis h f) x✝) (f x✝) = (gramSchmidtOrthonormalBasis h f).toBasis.toMatrix f x✝ x✝
-- Mathlib/NumberTheory/MulChar/Basic.lean
theorem IsQuadratic.pow_odd {χ : MulChar R R'} (hχ : χ.IsQuadratic) {n : ℕ} (hn : Odd n) :
    χ ^ n = χ

Proof state:
case intro
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
n : ℕ
⊢ χ ^ (2 * n + 1) = χ

Tactic:
rw [pow_add, pow_one, hχ.pow_even (even_two_mul _), one_mul]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
n : ℕ
hn : Odd n
⊢ χ ^ n = χ

Tactic:
obtain ⟨n, rfl⟩ := hn

Result:
case intro
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
n : ℕ
⊢ χ ^ (2 * n + 1) = χ
-- Mathlib/Data/Multiset/Fintype.lean
theorem toEnumFinset_subset_iff {m₁ m₂ : Multiset α} :
    m₁.toEnumFinset ⊆ m₂.toEnumFinset ↔ m₁ ≤ m₂ :=
  ⟨fun h ↦ by simpa using map_fst_le_of_subset_toEnumFinset h, Multiset.toEnumFinset_mono⟩

Proof state:
α : Type u_1
inst✝ : DecidableEq α
m₁ m₂ : Multiset α
h : m₁.toEnumFinset ⊆ m₂.toEnumFinset
⊢ m₁ ≤ m₂

Tactic:
simpa using map_fst_le_of_subset_toEnumFinset h

Result:
no goals
-- Mathlib/Algebra/Free.lean
theorem length_map (x) : (map f x).length = x.length :=
  FreeSemigroup.recOnMul x (fun _ ↦ rfl) (fun x y hx hy ↦ by simp only [map_mul, length_mul, *])

Proof state:
α : Type u
β : Type v
f : α → β
x✝ : FreeSemigroup α
x : α
y : FreeSemigroup α
hx : ((map f) (of x)).length = (of x).length
hy : ((map f) y).length = y.length
⊢ ((map f) (of x * y)).length = (of x * y).length

Tactic:
simp only [map_mul, length_mul, *]

Result:
no goals
-- Mathlib/GroupTheory/OrderOfElement.lean
theorem orderOf_dvd_iff_zpow_eq_one : (orderOf x : ℤ) ∣ i ↔ x ^ i = 1

Proof state:
case intro.inr
G : Type u_1
inst✝ : Group G
x : G
i : ℕ
⊢ ↑(orderOf x) ∣ -↑i ↔ x ^ (-↑i) = 1

Tactic:
rw [dvd_neg, Int.natCast_dvd_natCast, zpow_neg, inv_eq_one, zpow_natCast,
  orderOf_dvd_iff_pow_eq_one]

Result:
no goals

Proof state:
case intro.inl
G : Type u_1
inst✝ : Group G
x : G
i : ℕ
⊢ ↑(orderOf x) ∣ ↑i ↔ x ^ ↑i = 1

Tactic:
rw [Int.natCast_dvd_natCast, orderOf_dvd_iff_pow_eq_one, zpow_natCast]

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
x : G
i : ℤ
⊢ ↑(orderOf x) ∣ i ↔ x ^ i = 1

Tactic:
rcases Int.eq_nat_or_neg i with ⟨i, rfl | rfl⟩

Result:
case intro.inl
G : Type u_1
inst✝ : Group G
x : G
i : ℕ
⊢ ↑(orderOf x) ∣ ↑i ↔ x ^ ↑i = 1

case intro.inr
G : Type u_1
inst✝ : Group G
x : G
i : ℕ
⊢ ↑(orderOf x) ∣ -↑i ↔ x ^ (-↑i) = 1