harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem norm_inner_symm (x y : E) : ‖⟪x, y⟫‖ = ‖⟪y, x⟫‖

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ ‖⟪x, y⟫_𝕜‖ = ‖⟪y, x⟫_𝕜‖

Tactic:
rw [← inner_conj_symm, norm_conj]

Result:
no goals
-- Mathlib/Data/Matroid/Loop.lean
@[simp]
lemma comap_isLoop_iff {M : Matroid β} {f : α → β} : (M.comap f).IsLoop e ↔ M.IsLoop (f e)

Proof state:
α : Type u_1
β : Type u_2
e : α
M : Matroid β
f : α → β
⊢ (M.comap f).IsLoop e ↔ M.IsLoop (f e)

Tactic:
simp [isLoop_iff]

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/BorelCantelli.lean
theorem measure_liminf_cofinite_eq_zero [Infinite ι]  {s : ι → Set α} (h : ∑' i, μ (s i) ≠ ∞) :
    μ (liminf s cofinite) = 0

Proof state:
α : Type u_1
ι : Type u_2
F : Type u_3
inst✝³ : FunLike F (Set α) ℝ≥0∞
inst✝² : OuterMeasureClass F α
inst✝¹ : Countable ι
μ : F
inst✝ : Infinite ι
s : ι → Set α
h : ∑' (i : ι), μ (s i) ≠ ⊤
⊢ μ (liminf s cofinite) ≤ μ (limsup s cofinite)

Tactic:
exact measure_mono liminf_le_limsup

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_2
F : Type u_3
inst✝³ : FunLike F (Set α) ℝ≥0∞
inst✝² : OuterMeasureClass F α
inst✝¹ : Countable ι
μ : F
inst✝ : Infinite ι
s : ι → Set α
h : ∑' (i : ι), μ (s i) ≠ ⊤
⊢ μ (liminf s cofinite) = 0

Tactic:
rw [← le_zero_iff, ← measure_limsup_cofinite_eq_zero h]

Result:
α : Type u_1
ι : Type u_2
F : Type u_3
inst✝³ : FunLike F (Set α) ℝ≥0∞
inst✝² : OuterMeasureClass F α
inst✝¹ : Countable ι
μ : F
inst✝ : Infinite ι
s : ι → Set α
h : ∑' (i : ι), μ (s i) ≠ ⊤
⊢ μ (liminf s cofinite) ≤ μ (limsup s cofinite)
-- Mathlib/Algebra/Polynomial/EraseLead.lean
theorem eraseLead_zero : eraseLead (0 : R[X]) = 0

Proof state:
R : Type u_1
inst✝ : Semiring R
⊢ eraseLead 0 = 0

Tactic:
simp only [eraseLead, erase_zero]

Result:
no goals
-- Mathlib/LinearAlgebra/Orientation.lean
theorem Orientation.reindex_refl : (Orientation.reindex R M <| Equiv.refl ι) = Equiv.refl _

Proof state:
R : Type u_1
inst✝² : StrictOrderedCommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_4
⊢ reindex R M (Equiv.refl ι) = Equiv.refl (Orientation R M ι)

Tactic:
rw [Orientation.reindex, AlternatingMap.domDomCongrₗ_refl, Module.Ray.map_refl]

Result:
no goals
-- Mathlib/Order/Iterate.lean
theorem monotone_iterate_of_le_map (hf : Monotone f) (hx : x ≤ f x) : Monotone fun n => f^[n] x :=
  monotone_nat_of_le_succ fun n => by
    rw [iterate_succ_apply]
    exact hf.iterate n hx

Proof state:
α : Type u_1
inst✝ : Preorder α
f : α → α
x : α
hf : Monotone f
hx : x ≤ f x
n : ℕ
⊢ f^[n] x ≤ f^[n] (f x)

Tactic:
exact hf.iterate n hx

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
f : α → α
x : α
hf : Monotone f
hx : x ≤ f x
n : ℕ
⊢ f^[n] x ≤ f^[n + 1] x

Tactic:
rw [iterate_succ_apply]

Result:
α : Type u_1
inst✝ : Preorder α
f : α → α
x : α
hf : Monotone f
hx : x ≤ f x
n : ℕ
⊢ f^[n] x ≤ f^[n] (f x)
-- Mathlib/GroupTheory/Perm/Support.lean
theorem apply_mem_support {x : α} : f x ∈ f.support ↔ x ∈ f.support

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
⊢ f x ∈ f.support ↔ x ∈ f.support

Tactic:
rw [mem_support, mem_support, Ne, Ne, apply_eq_iff_eq]

Result:
no goals
-- Mathlib/Algebra/Homology/SingleHomology.lean
lemma isZero_single_obj_homology (A : C) (i : ι) (hi : i ≠ j) :
    IsZero (((single C c j).obj A).homology i)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A : C
i : ι
hi : i ≠ j
⊢ IsZero (((single C c j).obj A).homology i)

Tactic:
simpa only [← exactAt_iff_isZero_homology]
  using exactAt_single_obj c j A i hi

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/LinearCombo.lean
theorem mul_eval_of_const_right (l₁ l₂ : LinearCombo) (v : Coeffs) (w : l₂.coeffs.isZero) :
    (mul l₁ l₂).eval v = l₁.eval v * l₂.eval v

Proof state:
l₁ l₂ : LinearCombo
v : Coeffs
w : l₂.coeffs.isZero
this : l₂.coeffs.dot v = 0
⊢ (l₁.mul l₂).eval v = l₁.eval v * l₂.eval v

Tactic:
simp [mul, eval, this, Coeffs.sub_eq_add_neg, Coeffs.dot_distrib_left, Int.add_mul, Int.mul_add,
  Int.mul_comm]

Result:
no goals

Proof state:
l₁ l₂ : LinearCombo
v : Coeffs
w : l₂.coeffs.isZero
⊢ (l₁.mul l₂).eval v = l₁.eval v * l₂.eval v

Tactic:
have : Coeffs.dot l₂.coeffs v = 0 := IntList.dot_of_left_zero w

Result:
l₁ l₂ : LinearCombo
v : Coeffs
w : l₂.coeffs.isZero
this : l₂.coeffs.dot v = 0
⊢ (l₁.mul l₂).eval v = l₁.eval v * l₂.eval v
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem?_eq_none {a : Array α} (h : a.size ≤ i) : a[i]? = none

Proof state:
α : Type u_1
i : Nat
a : Array α
h : a.size ≤ i
⊢ a[i]? = none

Tactic:
simp [getElem?_eq_none_iff, h]

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/Defs.lean
theorem reindex_refl : b.reindex (Equiv.refl ι) = b :=
  eq_of_apply_eq fun i => by simp

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
i : ι
⊢ (b.reindex (Equiv.refl ι)) i = b i

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Jacobson/Radical.lean
theorem map_jacobson_of_bijective (hf : Function.Bijective f) :
    map f (jacobson R M) = jacobson R₂ M₂ :=
  map_jacobson_of_ker_le hf.2 <| by simp_rw [(LinearMapClass.ker_eq_bot _).mpr hf.1, bot_le]

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : Ring R₂
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝² : RingHomSurjective τ₁₂
F : Type u_5
inst✝¹ : FunLike F M M₂
inst✝ : SemilinearMapClass F τ₁₂ M M₂
f : F
hf : Function.Bijective ⇑f
⊢ LinearMap.ker f ≤ jacobson R M

Tactic:
simp_rw [(LinearMapClass.ker_eq_bot _).mpr hf.1, bot_le]

Result:
no goals
-- Mathlib/Data/Nat/Fib/Basic.lean
@[simp] lemma fib_pos {n : ℕ} : 0 < fib n ↔ 0 < n

Proof state:
n : ℕ
⊢ 0 < fib n ↔ 0 < n

Tactic:
simp [pos_iff_ne_zero]

Result:
no goals
-- Mathlib/CategoryTheory/ConcreteCategory/Basic.lean
theorem forget_obj (X : C) : (forget C).obj X = ToType X

Proof state:
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X : C
⊢ (forget C).obj X = ToType X

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X : C
⊢ (forget C).obj X = ToType X

Tactic:
with_reducible_and_instances rfl

Result:
no goals
-- Mathlib/LinearAlgebra/Span/Basic.lean
theorem eqOn_span_iff {s : Set M} {f g : F} : Set.EqOn f g (span R s) ↔ Set.EqOn f g s

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M₂
inst✝² : Module R₂ M₂
F : Type u_8
σ₁₂ : R →+* R₂
inst✝¹ : FunLike F M M₂
inst✝ : SemilinearMapClass F σ₁₂ M M₂
s : Set M
f g : F
⊢ s ⊆ ↑(eqLocus f g) ↔ Set.EqOn (⇑f) (⇑g) s

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M₂
inst✝² : Module R₂ M₂
F : Type u_8
σ₁₂ : R →+* R₂
inst✝¹ : FunLike F M M₂
inst✝ : SemilinearMapClass F σ₁₂ M M₂
s : Set M
f g : F
⊢ Set.EqOn ⇑f ⇑g ↑(span R s) ↔ Set.EqOn (⇑f) (⇑g) s

Tactic:
rw [← le_eqLocus, span_le]

Result:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M₂
inst✝² : Module R₂ M₂
F : Type u_8
σ₁₂ : R →+* R₂
inst✝¹ : FunLike F M M₂
inst✝ : SemilinearMapClass F σ₁₂ M M₂
s : Set M
f g : F
⊢ s ⊆ ↑(eqLocus f g) ↔ Set.EqOn (⇑f) (⇑g) s
-- Mathlib/Data/Multiset/Lattice.lean
theorem inf_add (s₁ s₂ : Multiset α) : (s₁ + s₂).inf = s₁.inf ⊓ s₂.inf :=
  Eq.trans (by simp [inf]) (fold_add _ _ _ _ _)

Proof state:
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
s₁ s₂ : Multiset α
⊢ (s₁ + s₂).inf = fold (fun x1 x2 => x1 ⊓ x2) (⊤ ⊓ ⊤) (s₁ + s₂)

Tactic:
simp [inf]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
theorem mem_inv_smul_finset_iff : b ∈ a⁻¹ • s ↔ a • b ∈ s

Proof state:
α : Type u_2
β : Type u_3
inst✝² : DecidableEq β
inst✝¹ : Group α
inst✝ : MulAction α β
s : Finset β
a : α
b : β
⊢ b ∈ a⁻¹ • s ↔ a • b ∈ s

Tactic:
rw [← smul_mem_smul_finset_iff a, smul_inv_smul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Count.lean
theorem count_push_of_ne (h : b ≠ a) (l : Vector α n) : count a (l.push b) = count a l

Proof state:
case mk
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
b a : α
h : b ≠ a
l : Array α
⊢ count a ({ toArray := l, size_toArray := ⋯ }.push b) = count a { toArray := l, size_toArray := ⋯ }

Tactic:
simp [Array.count_push_of_ne, h]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
b a : α
n : Nat
h : b ≠ a
l : Vector α n
⊢ count a (l.push b) = count a l

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
b a : α
h : b ≠ a
l : Array α
⊢ count a ({ toArray := l, size_toArray := ⋯ }.push b) = count a { toArray := l, size_toArray := ⋯ }
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem mem_keys [LawfulBEq α] {k : α} :
    k ∈ m.keys ↔ k ∈ m

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝ : LawfulBEq α
k : α
⊢ k ∈ m.keys ↔ m.contains k = true

Tactic:
exact Raw₀.mem_keys ⟨m.1, _⟩ m.2

Result:
no goals

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝ : LawfulBEq α
k : α
⊢ k ∈ m.keys ↔ k ∈ m

Tactic:
rw [mem_iff_contains]

Result:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝ : LawfulBEq α
k : α
⊢ k ∈ m.keys ↔ m.contains k = true
-- Mathlib/GroupTheory/Index.lean
theorem relindex_mul_relindex (hHK : H ≤ K) (hKL : K ≤ L) :
    H.relindex K * K.relindex L = H.relindex L

Proof state:
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
hHK : H ≤ K
hKL : K ≤ L
⊢ H.relindex K * K.relindex L = H.relindex L

Tactic:
rw [← relindex_subgroupOf hKL]

Result:
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
hHK : H ≤ K
hKL : K ≤ L
⊢ (H.subgroupOf L).relindex (K.subgroupOf L) * K.relindex L = H.relindex L

Proof state:
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
hHK : H ≤ K
hKL : K ≤ L
⊢ (H.subgroupOf L).relindex (K.subgroupOf L) * K.relindex L = H.relindex L

Tactic:
exact relindex_mul_index fun x hx => hHK hx

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem hausdorffDist_self_zero : hausdorffDist s s = 0

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
⊢ hausdorffDist s s = 0

Tactic:
simp [hausdorffDist]

Result:
no goals
-- Mathlib/Tactic/NormNum/Basic.lean
theorem isNat_natDiv : {a b : ℕ} → {a' b' c : ℕ} →
    IsNat a a' → IsNat b b' → Nat.div a' b' = c → IsNat (a / b) c
  | _, _, _, _, _, ⟨rfl⟩, ⟨rfl⟩, rfl => ⟨by aesop⟩

Proof state:
n✝¹ n✝ : ℕ
⊢ ↑n✝¹ / ↑n✝ = ↑(n✝¹.div n✝)

Tactic:
aesop

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean
theorem det_eq_of_eq_mul_det_one {A B : Matrix n n R} (C : Matrix n n R) (hC : det C = 1)
    (hA : A = B * C) : det A = det B :=
  calc
    det A = det (B * C) := congr_arg _ hA
    _ = det B * det C := det_mul _ _
    _ = det B

Proof state:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A B C : Matrix n n R
hC : C.det = 1
hA : A = B * C
⊢ B.det * C.det = B.det

Tactic:
rw [hC, mul_one]

Result:
no goals
-- Mathlib/NumberTheory/Ostrowski.lean
private lemma expr_pos : 0 < m * f m / (f m - 1)

Proof state:
f : AbsoluteValue ℚ ℝ
m : ℕ
hm : 1 < m
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
⊢ 0 < ↑m * f ↑m / (f ↑m - 1)

Tactic:
apply div_pos (mul_pos (mod_cast zero_lt_of_lt hm)
  (map_pos_of_ne_zero f (mod_cast ne_zero_of_lt hm)))

Result:
f : AbsoluteValue ℚ ℝ
m : ℕ
hm : 1 < m
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
⊢ 0 < f ↑m - 1

Proof state:
f : AbsoluteValue ℚ ℝ
m : ℕ
hm : 1 < m
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
⊢ 0 < f ↑m - 1

Tactic:
linarith only [one_lt_of_not_bounded notbdd hm]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/ModelsWithJ.lean
lemma ofJNe0Or1728_Δ : (ofJNe0Or1728 j).Δ = j ^ 2 * (j - 1728) ^ 9

Proof state:
R : Type u_1
inst✝ : CommRing R
j : R
⊢ (ofJNe0Or1728 j).Δ = j ^ 2 * (j - 1728) ^ 9

Tactic:
simp only [ofJNe0Or1728, Δ, b₂, b₄, b₆, b₈]

Result:
R : Type u_1
inst✝ : CommRing R
j : R
⊢ -((j - 1728) ^ 2 + 4 * 0) ^ 2 *
            ((j - 1728) ^ 2 * -(j - 1728) ^ 5 + 4 * 0 * -(j - 1728) ^ 5 - (j - 1728) * 0 * (-36 * (j - 1728) ^ 3) +
                0 * 0 ^ 2 -
              (-36 * (j - 1728) ^ 3) ^ 2) -
          8 * (2 * (-36 * (j - 1728) ^ 3) + (j - 1728) * 0) ^ 3 -
        27 * (0 ^ 2 + 4 * -(j - 1728) ^ 5) ^ 2 +
      9 * ((j - 1728) ^ 2 + 4 * 0) * (2 * (-36 * (j - 1728) ^ 3) + (j - 1728) * 0) * (0 ^ 2 + 4 * -(j - 1728) ^ 5) =
    j ^ 2 * (j - 1728) ^ 9

Proof state:
R : Type u_1
inst✝ : CommRing R
j : R
⊢ -((j - 1728) ^ 2 + 4 * 0) ^ 2 *
            ((j - 1728) ^ 2 * -(j - 1728) ^ 5 + 4 * 0 * -(j - 1728) ^ 5 - (j - 1728) * 0 * (-36 * (j - 1728) ^ 3) +
                0 * 0 ^ 2 -
              (-36 * (j - 1728) ^ 3) ^ 2) -
          8 * (2 * (-36 * (j - 1728) ^ 3) + (j - 1728) * 0) ^ 3 -
        27 * (0 ^ 2 + 4 * -(j - 1728) ^ 5) ^ 2 +
      9 * ((j - 1728) ^ 2 + 4 * 0) * (2 * (-36 * (j - 1728) ^ 3) + (j - 1728) * 0) * (0 ^ 2 + 4 * -(j - 1728) ^ 5) =
    j ^ 2 * (j - 1728) ^ 9

Tactic:
ring1

Result:
no goals
-- Mathlib/Data/Finsupp/Basic.lean
@[to_additive]
lemma prod_sumElim {ι₁ ι₂ α M : Type*} [Zero α] [CommMonoid M]
    (f₁ : ι₁ →₀ α) (f₂ : ι₂ →₀ α) (g : ι₁ ⊕ ι₂ → α → M) :
    (f₁.sumElim f₂).prod g = f₁.prod (g ∘ Sum.inl) * f₂.prod (g ∘ Sum.inr)

Proof state:
ι₁ : Type u_13
ι₂ : Type u_14
α : Type u_15
M : Type u_16
inst✝¹ : Zero α
inst✝ : CommMonoid M
f₁ : ι₁ →₀ α
f₂ : ι₂ →₀ α
g : ι₁ ⊕ ι₂ → α → M
⊢ (f₁.sumElim f₂).prod g = f₁.prod (g ∘ Sum.inl) * f₂.prod (g ∘ Sum.inr)

Tactic:
simp [Finsupp.prod, Finset.prod_disj_sum]

Result:
no goals
-- Mathlib/Algebra/Pointwise/Stabilizer.lean
@[to_additive]
lemma stabilizer_union_eq_right (hdisj : Disjoint s t) (hstab : stabilizer G t ≤ stabilizer G s)
    (hstab_union : stabilizer G (s ∪ t) ≤ stabilizer G s)  :
    stabilizer G (s ∪ t) = stabilizer G t

Proof state:
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
s t : Set α
hdisj : Disjoint s t
hstab : stabilizer G t ≤ stabilizer G s
hstab_union : stabilizer G (s ∪ t) ≤ stabilizer G s
⊢ stabilizer G (s ∪ t) = stabilizer G t

Tactic:
rw [union_comm, stabilizer_union_eq_left hdisj.symm hstab (union_comm .. ▸ hstab_union)]

Result:
no goals
-- Mathlib/Topology/Algebra/Monoid.lean
theorem tendsto_multiset_prod {f : ι → α → M} {x : Filter α} {a : ι → M} (s : Multiset ι) :
    (∀ i ∈ s, Tendsto (f i) x (𝓝 (a i))) →
      Tendsto (fun b => (s.map fun c => f c b).prod) x (𝓝 (s.map a).prod)

Proof state:
case mk
ι : Type u_1
α : Type u_2
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → α → M
x : Filter α
a : ι → M
s : Multiset ι
l : List ι
⊢ (∀ i ∈ Quot.mk (⇑(List.isSetoid ι)) l, Tendsto (f i) x (𝓝 (a i))) →
    Tendsto (fun b => (Multiset.map (fun c => f c b) (Quot.mk (⇑(List.isSetoid ι)) l)).prod) x
      (𝓝 (Multiset.map a (Quot.mk (⇑(List.isSetoid ι)) l)).prod)

Tactic:
simpa using tendsto_list_prod l

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → α → M
x : Filter α
a : ι → M
s : Multiset ι
⊢ (∀ i ∈ s, Tendsto (f i) x (𝓝 (a i))) →
    Tendsto (fun b => (Multiset.map (fun c => f c b) s).prod) x (𝓝 (Multiset.map a s).prod)

Tactic:
rcases s with ⟨l⟩

Result:
case mk
ι : Type u_1
α : Type u_2
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → α → M
x : Filter α
a : ι → M
s : Multiset ι
l : List ι
⊢ (∀ i ∈ Quot.mk (⇑(List.isSetoid ι)) l, Tendsto (f i) x (𝓝 (a i))) →
    Tendsto (fun b => (Multiset.map (fun c => f c b) (Quot.mk (⇑(List.isSetoid ι)) l)).prod) x
      (𝓝 (Multiset.map a (Quot.mk (⇑(List.isSetoid ι)) l)).prod)
-- Mathlib/Algebra/BigOperators/GroupWithZero/Finset.lean
lemma Units.mk0_prod [CommGroupWithZero G₀] (s : Finset ι) (f : ι → G₀) (h) :
    Units.mk0 (∏ i ∈ s, f i) h =
      ∏ i ∈ s.attach, Units.mk0 (f i) fun hh ↦ h (Finset.prod_eq_zero i.2 hh)

Proof state:
ι : Type u_1
G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
s : Finset ι
f : ι → G₀
h : ∏ i ∈ s, f i ≠ 0
⊢ mk0 (∏ i ∈ s, f i) h = ∏ i ∈ s.attach, mk0 (f ↑i) ⋯

Tactic:
classical induction s using Finset.induction_on <;> simp [*]

Result:
no goals

Proof state:
ι : Type u_1
G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
s : Finset ι
f : ι → G₀
h : ∏ i ∈ s, f i ≠ 0
⊢ mk0 (∏ i ∈ s, f i) h = ∏ i ∈ s.attach, mk0 (f ↑i) ⋯

Tactic:
induction s using Finset.induction_on <;> simp [*]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Charpoly/Basic.lean
lemma charmatrix_toSquareBlock {α : Type*} [DecidableEq α] {b : n → α} {a : α} :
    (M.toSquareBlock b a).charmatrix = M.charmatrix.toSquareBlock b a

Proof state:
case a
R : Type u_1
inst✝³ : CommRing R
n : Type u_4
inst✝² : DecidableEq n
inst✝¹ : Fintype n
M : Matrix n n R
α : Type u_5
inst✝ : DecidableEq α
b : n → α
a : α
i j : { a_1 // b a_1 = a }
⊢ (M.toSquareBlock b a).charmatrix i j = M.charmatrix.toSquareBlock b a i j

Tactic:
simp [charmatrix_apply, toSquareBlock_def, diagonal_apply, Subtype.ext_iff]

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : CommRing R
n : Type u_4
inst✝² : DecidableEq n
inst✝¹ : Fintype n
M : Matrix n n R
α : Type u_5
inst✝ : DecidableEq α
b : n → α
a : α
⊢ (M.toSquareBlock b a).charmatrix = M.charmatrix.toSquareBlock b a

Tactic:
ext i j : 1

Result:
case a
R : Type u_1
inst✝³ : CommRing R
n : Type u_4
inst✝² : DecidableEq n
inst✝¹ : Fintype n
M : Matrix n n R
α : Type u_5
inst✝ : DecidableEq α
b : n → α
a : α
i j : { a_1 // b a_1 = a }
⊢ (M.toSquareBlock b a).charmatrix i j = M.charmatrix.toSquareBlock b a i j
-- Mathlib/Data/Matroid/Basic.lean
theorem not_rankFinite (M : Matroid α) [RankInfinite M] : ¬ RankFinite M

Proof state:
case intro
α : Type u_1
M : Matroid α
inst✝ : M.RankInfinite
h : M.RankFinite
B : Set α
hB : M.IsBase B
⊢ False

Tactic:
exact hB.infinite hB.finite

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
inst✝ : M.RankInfinite
⊢ ¬M.RankFinite

Tactic:
intro h

Result:
α : Type u_1
M : Matroid α
inst✝ : M.RankInfinite
h : M.RankFinite
⊢ False

Proof state:
α : Type u_1
M : Matroid α
inst✝ : M.RankInfinite
h : M.RankFinite
⊢ False

Tactic:
obtain ⟨B,hB⟩ := M.exists_isBase

Result:
case intro
α : Type u_1
M : Matroid α
inst✝ : M.RankInfinite
h : M.RankFinite
B : Set α
hB : M.IsBase B
⊢ False
-- Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean
theorem changeForm_ι (m : M) : changeForm h (ι (M := M) Q m) = ι (M := M) Q' m :=
  (foldr_ι _ _ _ _ _).trans <|
    Eq.symm <| by rw [changeFormAux_apply_apply, mul_one, contractLeft_one, sub_zero]

Proof state:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' : QuadraticForm R M
B : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
m : M
⊢ (ι Q') m = ((changeFormAux Q' B) m) 1

Tactic:
rw [changeFormAux_apply_apply, mul_one, contractLeft_one, sub_zero]

Result:
no goals
-- Mathlib/Algebra/Tropical/BigOperators.lean
theorem untrop_sum [ConditionallyCompleteLinearOrder R] [Fintype S] (f : S → Tropical (WithTop R)) :
    untrop (∑ i : S, f i) = ⨅ i : S, untrop (f i)

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrder R
inst✝ : Fintype S
f : S → Tropical (WithTop R)
⊢ untrop (∑ i : S, f i) = ⨅ i, untrop (f i)

Tactic:
rw [iInf, ← Set.image_univ, ← coe_univ, untrop_sum_eq_sInf_image, Function.comp_def]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/ConformalLinearMap.lean
theorem isConformalMap_id : IsConformalMap (id R M) :=
  ⟨1, one_ne_zero, id, by simp⟩

Proof state:
R : Type u_1
M : Type u_2
inst✝² : NormedField R
inst✝¹ : SeminormedAddCommGroup M
inst✝ : NormedSpace R M
⊢ ContinuousLinearMap.id R M = 1 • LinearIsometry.id.toContinuousLinearMap

Tactic:
simp

Result:
no goals
-- Mathlib/Computability/DFA.lean
theorem evalFrom_reindex (g : σ ≃ σ') (s : σ') (x : List α) :
    (reindex g M).evalFrom s x = g (M.evalFrom (g.symm s) x)

Proof state:
case nil
α : Type u
σ : Type v
M : DFA α σ
σ' : Type u_2
g : σ ≃ σ'
s : σ'
⊢ ((reindex g) M).evalFrom s [] = g (M.evalFrom (g.symm s) [])

Tactic:
simp

Result:
no goals

Proof state:
case append_singleton
α : Type u
σ : Type v
M : DFA α σ
σ' : Type u_2
g : σ ≃ σ'
s : σ'
x : List α
a : α
ih : ((reindex g) M).evalFrom s x = g (M.evalFrom (g.symm s) x)
⊢ ((reindex g) M).evalFrom s (x ++ [a]) = g (M.evalFrom (g.symm s) (x ++ [a]))

Tactic:
simp [ih]

Result:
no goals

Proof state:
α : Type u
σ : Type v
M : DFA α σ
σ' : Type u_2
g : σ ≃ σ'
s : σ'
x : List α
⊢ ((reindex g) M).evalFrom s x = g (M.evalFrom (g.symm s) x)

Tactic:
induction x using List.reverseRecOn with
| nil => simp
| append_singleton x a ih => simp [ih]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Modify.lean
theorem eraseIdx_eq_modifyTailIdx : ∀ n (l : List α), eraseIdx l n = modifyTailIdx tail n l
  | 0, l => by cases l <;> rfl
  | _+1, [] => rfl
  | _+1, _ :: _ => congrArg (cons _) (eraseIdx_eq_modifyTailIdx _ _)

Proof state:
α : Type u_1
l : List α
⊢ l.eraseIdx 0 = modifyTailIdx tail 0 l

Tactic:
cases l <;> rfl

Result:
no goals
-- Mathlib/FieldTheory/PurelyInseparable/PerfectClosure.lean
theorem mem_perfectClosure_iff_pow_mem (q : ℕ) [ExpChar F q] {x : E} :
    x ∈ perfectClosure F E ↔ ∃ n : ℕ, x ^ q ^ n ∈ (algebraMap F E).range

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
q : ℕ
inst✝ : ExpChar F q
x : E
⊢ x ∈ perfectClosure F E ↔ ∃ n, x ^ q ^ n ∈ (algebraMap F E).range

Tactic:
rw [mem_perfectClosure_iff, ringExpChar.eq F q]

Result:
no goals
-- Mathlib/Data/Nat/GCD/Basic.lean
theorem gcd_add_self_right (m n : ℕ) : gcd m (n + m) = gcd m n :=
  Eq.trans (by rw [one_mul]) (gcd_add_mul_right_right m n 1)

Proof state:
m n : ℕ
⊢ m.gcd (n + m) = m.gcd (n + 1 * m)

Tactic:
rw [one_mul]

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/Biproducts.lean
theorem biprod.desc_eq {T : C} {f : X ⟶ T} {g : Y ⟶ T} :
    biprod.desc f g = biprod.fst ≫ f + biprod.snd ≫ g

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X Y : C
inst✝ : HasBinaryBiproduct X Y
T : C
f : X ⟶ T
g : Y ⟶ T
⊢ desc f g = fst ≫ f + snd ≫ g

Tactic:
ext <;> simp [add_comp]

Result:
no goals
-- Mathlib/CategoryTheory/Functor/Category.lean
theorem map_hom_inv_id_app {X Y : C} (e : X ≅ Y) (F : C ⥤ D ⥤ E) (Z : D) :
    (F.map e.hom).app Z ≫ (F.map e.inv).app Z = 𝟙 _

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
X Y : C
e : X ≅ Y
F : C ⥤ D ⥤ E
Z : D
⊢ (F.map e.hom).app Z ≫ (F.map e.inv).app Z = 𝟙 ((F.obj X).obj Z)

Tactic:
simp [← NatTrans.comp_app, ← Functor.map_comp]

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Iic_diff_Ioc_self_of_le (hab : a ≤ b) : Iic b \ Ioc a b = Iic a

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
hab : a ≤ b
⊢ Iic b \ Ioc a b = Iic a

Tactic:
rw [Iic_diff_Ioc, min_eq_left hab]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getD_alter {k k' : α} {fallback : β} (h : m.1.WF) {f : Option β → Option β} :
    Const.getD (Const.alter m k f) k' fallback =
      if k == k' then
        f (Const.get? m k) |>.getD fallback
      else
        Const.getD m k' fallback

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
k k' : α
fallback : β
h : m.val.WF
f : Option β → Option β
⊢ getD (alter m k f) k' fallback = if (k == k') = true then (f (get? m k)).getD fallback else getD m k' fallback

Tactic:
simp_to_model [Const.alter] using List.Const.getValueD_alterKey

Result:
no goals