harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean
theorem mem_span_finset {s : Finset M} {x : M} :
    x ∈ span R (↑s : Set M) ↔ ∃ f : M → R, ∑ i ∈ s, f i • i = x :=
  ⟨fun hx =>
    let ⟨v, hvs, hvx⟩ :=
      (Finsupp.mem_span_image_iff_linearCombination _).1
        (show x ∈ span R (_root_.id '' (↑s : Set M)) by rwa [Set.image_id])
    ⟨v, hvx ▸ (linearCombination_apply_of_mem_supported _ hvs).symm⟩,
    fun ⟨_, hf⟩ => hf ▸ sum_mem fun _ hi => smul_mem _ _ <| subset_span hi⟩

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset M
x : M
hx : x ∈ span R ↑s
⊢ x ∈ span R (_root_.id '' ↑s)

Tactic:
rwa [Set.image_id]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma one_le_cfc (f : R → R) (a : A) (h : ∀ x ∈ spectrum R a, 1 ≤ f x)
    (hf : ContinuousOn f (spectrum R a)

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : OrderedCommSemiring R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : ∀ (α : Type ?u.739476) [inst : TopologicalSpace α], StarOrderedRing C(α, R)
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
f : R → R
a : A
h : ∀ x ∈ spectrum R a, 1 ≤ f x
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
ha : autoParam (p a) _auto✝
⊢ 1 ≤ cfc f a

Tactic:
simpa using algebraMap_le_cfc f 1 a h

Result:
no goals
-- Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean
theorem cardQuot_apply (S : Submodule R M) : cardQuot S = Nat.card (M ⧸ S)

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submodule R M
⊢ S.cardQuot = Nat.card (M ⧸ S)

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Calculus/LineDeriv/Basic.lean
theorem lineDifferentiableAt_smul_iff {c : 𝕜} (hc : c ≠ 0) :
    LineDifferentiableAt 𝕜 f x (c • v) ↔ LineDifferentiableAt 𝕜 f x v :=
  ⟨fun h ↦ by simpa [smul_smul, inv_mul_cancel₀ hc] using h.smul (c ⁻¹), fun h ↦ h.smul c⟩

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : E → F
x v : E
c : 𝕜
hc : c ≠ 0
h : LineDifferentiableAt 𝕜 f x (c • v)
⊢ LineDifferentiableAt 𝕜 f x v

Tactic:
simpa [smul_smul, inv_mul_cancel₀ hc] using h.smul (c ⁻¹)

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem compl_sInf (S : Set (LowerSet α)) : (sInf S).compl = ⨅ s ∈ S, LowerSet.compl s :=
  UpperSet.ext <| by simp only [coe_compl, coe_sInf, compl_iInter₂, UpperSet.coe_iInf₂]

Proof state:
α : Type u_1
inst✝ : LE α
S : Set (LowerSet α)
⊢ ↑(sInf S).compl = ↑(⨅ s ∈ S, s.compl)

Tactic:
simp only [coe_compl, coe_sInf, compl_iInter₂, UpperSet.coe_iInf₂]

Result:
no goals
-- Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean
theorem map_one_fst_of_isTwoCocycle {f : G × G → A} (hf : IsTwoCocycle f) (g : G) :
    f (1, g) = f (1, 1)

Proof state:
G : Type u_1
A : Type u_2
inst✝² : Monoid G
inst✝¹ : AddCommGroup A
inst✝ : MulAction G A
f : G × G → A
hf : IsTwoCocycle f
g : G
⊢ f (1, g) = f (1, 1)

Tactic:
simpa only [one_smul, one_mul, mul_one, add_right_inj] using (hf 1 1 g).symm

Result:
no goals
-- Mathlib/Algebra/Module/LinearMap/Defs.lean
@[simp]
lemma restrictScalars_comp [AddCommMonoid P] [Module S P] [Module R P]
    [CompatibleSMul N P R S] [CompatibleSMul M P R S] (f : N →ₗ[S] P) (g : M →ₗ[S] N) :
    (f ∘ₗ g).restrictScalars R = f.restrictScalars R ∘ₗ g.restrictScalars R

Proof state:
R : Type u_14
S : Type u_15
M : Type u_16
N : Type u_17
P : Type u_18
inst✝¹³ : Semiring R
inst✝¹² : Semiring S
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : Module R M
inst✝⁸ : Module R N
inst✝⁷ : Module S M
inst✝⁶ : Module S N
inst✝⁵ : CompatibleSMul M N R S
inst✝⁴ : AddCommMonoid P
inst✝³ : Module S P
inst✝² : Module R P
inst✝¹ : CompatibleSMul N P R S
inst✝ : CompatibleSMul M P R S
f : N →ₗ[S] P
g : M →ₗ[S] N
⊢ ↑R (f ∘ₗ g) = ↑R f ∘ₗ ↑R g

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/SuccPred/Basic.lean
theorem pred_eq_iff_covBy : pred b = a ↔ a ⋖ b :=
  ⟨by
    rintro rfl
    exact pred_covBy _, CovBy.pred_eq⟩

Proof state:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : PredOrder α
a b : α
inst✝ : NoMinOrder α
⊢ pred b = a → a ⋖ b

Tactic:
rintro rfl

Result:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : PredOrder α
b : α
inst✝ : NoMinOrder α
⊢ pred b ⋖ b

Proof state:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : PredOrder α
b : α
inst✝ : NoMinOrder α
⊢ pred b ⋖ b

Tactic:
exact pred_covBy _

Result:
no goals
-- Mathlib/GroupTheory/Perm/List.lean
theorem formPerm_apply_get_zero (l : List α) (h : Nodup l) (hl : 1 < l.length) :
    formPerm l (l.get (Fin.mk 0 (by omega))) = l.get (Fin.mk 1 hl) :=
  formPerm_apply_getElem_zero l h hl

Proof state:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : l.Nodup
hl : 1 < l.length
⊢ 0 < l.length

Tactic:
omega

Result:
no goals
-- Mathlib/MeasureTheory/Function/EssSup.lean
@[simp] lemma essSup_count [MeasurableSingletonClass α] (f : α → β) : essSup f .count = ⨆ i, f i :=
  essSup_eq_iSup (by simp) _

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : CompleteLattice β
inst✝ : MeasurableSingletonClass α
f : α → β
⊢ ∀ (a : α), Measure.count {a} ≠ 0

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Regularity/Bound.lean
theorem le_stepBound : id ≤ stepBound := fun n =>
  Nat.le_mul_of_pos_right _ <| pow_pos (by norm_num) n

Proof state:
n : ℕ
⊢ 0 < 4

Tactic:
norm_num

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem mul_ne_zero_iff {a b : Int} : a * b ≠ 0 ↔ a ≠ 0 ∧ b ≠ 0

Proof state:
a b : Int
⊢ a * b ≠ 0 ↔ a ≠ 0 ∧ b ≠ 0

Tactic:
rw [ne_eq, Int.mul_eq_zero, not_or, ne_eq]

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
theorem mul_comm_div : a / b * c = a * (c / b)

Proof state:
a b c : ℝ≥0∞
⊢ a / b * c = a * (c / b)

Tactic:
simp only [div_eq_mul_inv, mul_right_comm, ← mul_assoc]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma negAddY_of_X_eq {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P z ≠ 0)
    (hQz : Q z ≠ 0) (hx : P x * Q z ^ 2 = Q x * P z ^ 2) : W.negAddY P Q = (-addU P Q) ^ 3

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ W.negAddY P Q = (-addU P Q) ^ 3

Tactic:
rw [addU, neg_neg, div_pow, ← negAddY_of_X_eq' hP hQ hx,
  mul_div_cancel_right₀ _ <| pow_ne_zero 3 <| mul_ne_zero hPz hQz]

Result:
no goals
-- Mathlib/Algebra/Group/Semiconj/Basic.lean
theorem inv_inv_symm_iff : SemiconjBy a⁻¹ x⁻¹ y⁻¹ ↔ SemiconjBy a y x

Proof state:
G : Type u_1
inst✝ : DivisionMonoid G
a x y : G
⊢ SemiconjBy a⁻¹ x⁻¹ y⁻¹ ↔ SemiconjBy a y x

Tactic:
simp_rw [SemiconjBy, ← mul_inv_rev, inv_inj, eq_comm]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Functor.lean
theorem δ_natural {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y') :
    δ F X X' ≫ (F.map f ⊗ F.map g) = F.map (f ⊗ g) ≫ δ F Y Y'

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X Y X' Y' : C
f : X ⟶ Y
g : X' ⟶ Y'
⊢ δ F X X' ≫ (F.map f ⊗ F.map g) = F.map (f ⊗ g) ≫ δ F Y Y'

Tactic:
simp [tensorHom_def]

Result:
no goals
-- Mathlib/Algebra/Homology/SingleHomology.lean
@[reassoc (attr := simp)]
lemma singleObjHomologySelfIso_hom_singleObjHomologySelfIso_inv :
    (singleObjCyclesSelfIso c j A).hom ≫ (singleObjHomologySelfIso c j A).inv =
      ((single C c j).obj A).homologyπ j

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
⊢ (singleObjCyclesSelfIso c j A).hom ≫ (singleObjHomologySelfIso c j A).inv = ((single C c j).obj A).homologyπ j

Tactic:
simp only [← cancel_mono (singleObjHomologySelfIso _ _ _).hom, assoc,
  Iso.inv_hom_id, comp_id, homologyπ_singleObjHomologySelfIso_hom]

Result:
no goals
-- Mathlib/CategoryTheory/Generator/Basic.lean
theorem isSeparator_coprod_of_isSeparator_left (G H : C) [HasBinaryCoproduct G H]
    (hG : IsSeparator G) : IsSeparator (G ⨿ H) :=
  (isSeparator_coprod _ _).2 <| IsSeparating.mono hG <| by simp

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryCoproduct G H
hG : IsSeparator G
⊢ {G} ⊆ {G, H}

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Uniform.lean
theorem le_mul_norm_div {f : E → F} (hf : AntilipschitzWith K f) (x y : E) :
    ‖x / y‖ ≤ K * ‖f x / f y‖

Proof state:
F : Type u_3
inst✝¹ : SeminormedCommGroup F
E : Type u_5
inst✝ : SeminormedCommGroup E
K : ℝ≥0
f : E → F
hf : AntilipschitzWith K f
x y : E
⊢ ‖x / y‖ ≤ ↑K * ‖f x / f y‖

Tactic:
simp [← dist_eq_norm_div, hf.le_mul_dist x y]

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Defs.lean
theorem generateFrom_insert_empty (S : Set (Set α)) :
    generateFrom (insert ∅ S) = generateFrom S

Proof state:
α : Type u_1
S : Set (Set α)
⊢ generateFrom (insert ∅ S) = generateFrom S

Tactic:
rw [insert_eq, ← generateFrom_sup_generateFrom, generateFrom_singleton_empty, bot_sup_eq]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
lemma IsPath.of_adj {G : SimpleGraph V} {u v : V} (h : G.Adj u v) : h.toWalk.IsPath

Proof state:
V : Type u
G : SimpleGraph V
u v : V
h : G.Adj u v
⊢ h.toWalk.IsPath

Tactic:
aesop

Result:
no goals
-- Mathlib/Algebra/Homology/ImageToKernel.lean
theorem imageToKernel_arrow (w : f ≫ g = 0) :
    imageToKernel f g w ≫ (kernelSubobject g).arrow = (imageSubobject f).arrow

Proof state:
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹ : HasImage f
g : B ⟶ C
inst✝ : HasKernel g
w : f ≫ g = 0
⊢ imageToKernel f g w ≫ (kernelSubobject g).arrow = (imageSubobject f).arrow

Tactic:
simp [imageToKernel]

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem Valid'.node4L_lemma₄ {a b c d : ℕ} (lr₁ : 3 * a ≤ b + c + 1 + d) (mr₂ : b + c + 1 ≤ 3 * d)
    (mm₁ : b ≤ 3 * c) : a + b + 1 ≤ 3 * (c + d + 1)

Proof state:
a b c d : ℕ
lr₁ : 3 * a ≤ b + c + 1 + d
mr₂ : b + c + 1 ≤ 3 * d
mm₁ : b ≤ 3 * c
⊢ a + b + 1 ≤ 3 * (c + d + 1)

Tactic:
omega

Result:
no goals
-- Mathlib/Analysis/Matrix.lean
theorem linftyOpBoundedSMul
    [SeminormedRing R] [SeminormedAddCommGroup α] [Module R α] [BoundedSMul R α] :
    BoundedSMul R (Matrix m n α) :=
  (by infer_instance : BoundedSMul R (m → PiLp 1 fun j : n => α))

Proof state:
R : Type u_1
m : Type u_3
n : Type u_4
α : Type u_5
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : SeminormedRing R
inst✝² : SeminormedAddCommGroup α
inst✝¹ : Module R α
inst✝ : BoundedSMul R α
⊢ BoundedSMul R (m → PiLp 1 fun j => α)

Tactic:
infer_instance

Result:
no goals
-- Mathlib/Analysis/Calculus/LineDeriv/Basic.lean
theorem HasLineDerivAt.lineDeriv (h : HasLineDerivAt 𝕜 f f' x v) :
    lineDeriv 𝕜 f x v = f'

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : E → F
f' : F
x v : E
h : HasLineDerivAt 𝕜 f f' x v
⊢ lineDeriv 𝕜 f x v = f'

Tactic:
rw [h.unique h.lineDifferentiableAt.hasLineDerivAt]

Result:
no goals
-- Mathlib/NumberTheory/Modular.lean
theorem re_T_zpow_smul (n : ℤ) : (T ^ n • z).re = z.re + n

Proof state:
z : ℍ
n : ℤ
⊢ (T ^ n • z).re = z.re + ↑n

Tactic:
rw [← coe_re, coe_T_zpow_smul_eq, add_re, intCast_re, coe_re]

Result:
no goals
-- Mathlib/Topology/UniformSpace/CompactConvergence.lean
theorem mem_compactConvergence_entourage_iff (X : Set (C(α, β) × C(α, β))) :
    X ∈ 𝓤 C(α, β) ↔
      ∃ (K : Set α) (V : Set (β × β)), IsCompact K ∧ V ∈ 𝓤 β ∧
        { fg : C(α, β) × C(α, β) | ∀ x ∈ K, (fg.1 x, fg.2 x) ∈ V } ⊆ X

Proof state:
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
X : Set (C(α, β) × C(α, β))
⊢ X ∈ 𝓤 C(α, β) ↔ ∃ K V, IsCompact K ∧ V ∈ 𝓤 β ∧ {fg | ∀ x ∈ K, (fg.1 x, fg.2 x) ∈ V} ⊆ X

Tactic:
simp [hasBasis_compactConvergenceUniformity.mem_iff, and_assoc]

Result:
no goals
-- Mathlib/AlgebraicGeometry/StructureSheaf.lean
theorem isUnit_to_basicOpen_self (f : R) : IsUnit (toOpen R (PrimeSpectrum.basicOpen f) f) :=
  isUnit_of_mul_eq_one _ (const R 1 f (PrimeSpectrum.basicOpen f) fun _ => id) <| by
    rw [toOpen_eq_const, const_mul_rev]

Proof state:
R : Type u
inst✝ : CommRing R
f : R
⊢ (ConcreteCategory.hom (toOpen R (PrimeSpectrum.basicOpen f))) f * const R 1 f (PrimeSpectrum.basicOpen f) ⋯ = 1

Tactic:
rw [toOpen_eq_const, const_mul_rev]

Result:
no goals
-- Mathlib/Algebra/Ring/Commute.lean
@[simp] lemma sq_eq_one_iff : a ^ 2 = 1 ↔ a = 1 ∨ a = -1

Proof state:
R : Type u
inst✝¹ : Ring R
a : R
inst✝ : NoZeroDivisors R
⊢ a ^ 2 = 1 ↔ a = 1 ∨ a = -1

Tactic:
rw [← (Commute.one_right a).sq_eq_sq_iff_eq_or_eq_neg, one_pow]

Result:
no goals
-- Mathlib/Data/Fintype/BigOperators.lean
lemma card_filter_piFinset_const_eq_of_mem (s : Finset κ) (i : ι) {x : κ} (hx : x ∈ s) :
    #{f ∈ piFinset fun _ ↦ s | f i = x} = #s ^ (card ι - 1) :=
  (card_filter_piFinset_eq_of_mem _ _ hx).trans <| by
    rw [prod_const #s, card_erase_of_mem (mem_univ _), card_univ]

Proof state:
ι : Type u_4
κ : Type u_5
inst✝² : DecidableEq ι
inst✝¹ : DecidableEq κ
inst✝ : Fintype ι
s : Finset κ
i : ι
x : κ
hx : x ∈ s
⊢ ∏ j ∈ univ.erase i, #s = #s ^ (card ι - 1)

Tactic:
rw [prod_const #s, card_erase_of_mem (mem_univ _), card_univ]

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Invariant.lean
protected lemma mk_eq_top_iff {p : Submodule R M} (hp : p ∈ f.invtSubmodule) :
    (⟨p, hp⟩ : f.invtSubmodule) = ⊤ ↔ p = ⊤ :=
  Subtype.mk_eq_top_iff (by simp [invtSubmodule]) _

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
⊢ ⊤ ∈ f.invtSubmodule

Tactic:
simp [invtSubmodule]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Bivariate.lean
@[simp]
lemma evalEval_intCast (x y : R) (n : ℤ) : (n : R[X][Y]).evalEval x y = n

Proof state:
R : Type u_1
inst✝ : Ring R
x y : R
n : ℤ
⊢ evalEval x y ↑n = ↑n

Tactic:
simp only [evalEval, eval_intCast]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getLsbD_ofBoolListBE :
    (ofBoolListBE bs).getLsbD i = (decide (i < bs.length) && bs.getD (bs.length - 1 - i) false)

Proof state:
bs : List Bool
i : Nat
⊢ (ofBoolListBE bs).getLsbD i = (decide (i < bs.length) && bs.getD (bs.length - 1 - i) false)

Tactic:
simp [getLsbD_eq_getMsbD]

Result:
no goals
-- Mathlib/Topology/UnitInterval.lean
theorem one_minus_le_one (x : I) : 1 - (x : ℝ) ≤ 1

Proof state:
x : ↑I
⊢ 1 - ↑x ≤ 1

Tactic:
simpa using x.2.1

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean
theorem le_mul_iff_one_le_left [MulOneClass α] [i : @Std.Commutative α (· * ·)]
    [MulLeftMono α] {a b : α} (ha : MulLECancellable a) :
    a ≤ b * a ↔ 1 ≤ b

Proof state:
α : Type u_1
inst✝² : LE α
inst✝¹ : MulOneClass α
i : Std.Commutative fun x1 x2 => x1 * x2
inst✝ : MulLeftMono α
a b : α
ha : MulLECancellable a
⊢ a ≤ b * a ↔ 1 ≤ b

Tactic:
rw [i.comm, ha.le_mul_iff_one_le_right]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Erase.lean
theorem eraseIdx_set_eq {l : Array α} {i : Nat} {a : α} {h : i < l.size} :
    (l.set i a).eraseIdx i (by simp; omega) = l.eraseIdx i

Proof state:
α : Type ?u.69261
l : Array α
i : Nat
a : α
h : i < l.size
⊢ i < (l.set i a h).size

Tactic:
simp

Result:
α : Type ?u.69261
l : Array α
i : Nat
a : α
h : i < l.size
⊢ i < l.size

Proof state:
α : Type u_1
l : Array α
i : Nat
a : α
h : i < l.size
⊢ (l.set i a h).eraseIdx i ⋯ = l.eraseIdx i h

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
i : Nat
a : α
l : List α
h : i < { toList := l }.size
⊢ ({ toList := l }.set i a h).eraseIdx i ⋯ = { toList := l }.eraseIdx i h

Proof state:
case mk
α : Type u_1
i : Nat
a : α
l : List α
h : i < { toList := l }.size
⊢ ({ toList := l }.set i a h).eraseIdx i ⋯ = { toList := l }.eraseIdx i h

Tactic:
simp [List.eraseIdx_set_eq, *]

Result:
no goals

Proof state:
α : Type ?u.69261
l : Array α
i : Nat
a : α
h : i < l.size
⊢ i < l.size

Tactic:
omega

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem encard_diff_add_encard (s t : Set α) : (s \ t).encard + t.encard = (s ∪ t).encard

Proof state:
α : Type u_1
s t : Set α
⊢ (s \ t).encard + t.encard = (s ∪ t).encard

Tactic:
rw [← encard_union_eq disjoint_sdiff_left, diff_union_self]

Result:
no goals
-- Mathlib/Data/Part.lean
theorem map_none (f : α → β) : map f none = none :=
  eq_none_iff.2 fun a => by simp

Proof state:
α : Type u_1
β : Type u_2
f : α → β
a : β
⊢ a ∉ map f none

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Div/Basic.lean
theorem mul_div_left (m : Nat) {n : Nat} (H : 0 < n) : m * n / n = m

Proof state:
m n : Nat
H : 0 < n
⊢ m * n / n = m

Tactic:
rw [Nat.mul_comm, mul_div_right _ H]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean
lemma compProd_add_left (μ ν : Measure α) [SFinite μ] [SFinite ν] (κ : Kernel α β) :
    (μ + ν) ⊗ₘ κ = μ ⊗ₘ κ + ν ⊗ₘ κ

Proof state:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
inst✝¹ : SFinite μ
inst✝ : SFinite ν
κ : Kernel α β
hκ : IsSFiniteKernel κ
⊢ (μ + ν) ⊗ₘ κ = μ ⊗ₘ κ + ν ⊗ₘ κ

Tactic:
simp_rw [Measure.compProd, Kernel.const_add, Kernel.compProd_add_left, Kernel.add_apply]

Result:
no goals

Proof state:
case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
inst✝¹ : SFinite μ
inst✝ : SFinite ν
κ : Kernel α β
hκ : ¬IsSFiniteKernel κ
⊢ (μ + ν) ⊗ₘ κ = μ ⊗ₘ κ + ν ⊗ₘ κ

Tactic:
simp [hκ]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
inst✝¹ : SFinite μ
inst✝ : SFinite ν
κ : Kernel α β
⊢ (μ + ν) ⊗ₘ κ = μ ⊗ₘ κ + ν ⊗ₘ κ

Tactic:
by_cases hκ : IsSFiniteKernel κ

Result:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
inst✝¹ : SFinite μ
inst✝ : SFinite ν
κ : Kernel α β
hκ : IsSFiniteKernel κ
⊢ (μ + ν) ⊗ₘ κ = μ ⊗ₘ κ + ν ⊗ₘ κ

case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
inst✝¹ : SFinite μ
inst✝ : SFinite ν
κ : Kernel α β
hκ : ¬IsSFiniteKernel κ
⊢ (μ + ν) ⊗ₘ κ = μ ⊗ₘ κ + ν ⊗ₘ κ
-- Mathlib/Order/RelSeries.lean
lemma Rel.not_infiniteDimensional_iff [Nonempty α] :
    ¬ r.InfiniteDimensional ↔ r.FiniteDimensional

Proof state:
α : Type u_1
r : Rel α α
inst✝ : Nonempty α
⊢ ¬r.InfiniteDimensional ↔ r.FiniteDimensional

Tactic:
rw [← not_finiteDimensional_iff, not_not]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Functor.lean
@[simp, reassoc]
lemma left_unitality (X : C) :
    (λ_ (F.obj X)).inv = F.map (λ_ X).inv ≫ δ F (𝟙_ C) X ≫ η F ▷ F.obj X

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X : C
⊢ (λ_ (F.obj X)).inv = F.map (λ_ X).inv ≫ δ F (𝟙_ C) X ≫ η F ▷ F.obj X

Tactic:
apply oplax_left_unitality'

Result:
no goals
-- Mathlib/RepresentationTheory/GroupCohomology/Functoriality.lean
@[reassoc (attr := simp), elementwise (attr := simp)]
lemma cocyclesMap_comp_isoTwoCocycles_hom :
    cocyclesMap f φ 2 ≫ (isoTwoCocycles B).hom = (isoTwoCocycles A).hom ≫ mapTwoCocycles f φ

Proof state:
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : (Action.res (ModuleCat k) f).obj A ⟶ B
⊢ (cocyclesMap f φ 2 ≫
        (HomologicalComplex.cyclesIsoSc' (inhomogeneousCochains B) 1 2 3 isoTwoCocycles.proof_3
              isoTwoCocycles.proof_4 ≪≫
            cyclesMapIso (shortComplexH2Iso B) ≪≫ (shortComplexH2 B).moduleCatCyclesIso).hom) ≫
      (shortComplexH2 B).moduleCatLeftHomologyData.i =
    ((HomologicalComplex.cyclesIsoSc' (inhomogeneousCochains A) 1 2 3 isoTwoCocycles.proof_3 isoTwoCocycles.proof_4 ≪≫
            cyclesMapIso (shortComplexH2Iso A) ≪≫ (shortComplexH2 A).moduleCatCyclesIso).hom ≫
        (shortComplexH2 A).moduleCatLeftHomologyData.i) ≫
      (mapShortComplexH2 f φ).τ₂

Tactic:
simp [cochainsMap_f_2_comp_twoCochainsLequiv f, mapShortComplexH2, ← LinearEquiv.toModuleIso_hom]

Result:
no goals

Proof state:
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : (Action.res (ModuleCat k) f).obj A ⟶ B
⊢ cocyclesMap f φ 2 ≫ (isoTwoCocycles B).hom = (isoTwoCocycles A).hom ≫ mapTwoCocycles f φ

Tactic:
simp_rw [← cancel_mono (moduleCatLeftHomologyData (shortComplexH2 B)).i, mapTwoCocycles,
    Category.assoc, cyclesMap'_i, isoTwoCocycles, ← Category.assoc]

Result:
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : (Action.res (ModuleCat k) f).obj A ⟶ B
⊢ (cocyclesMap f φ 2 ≫
        (HomologicalComplex.cyclesIsoSc' (inhomogeneousCochains B) 1 2 3 isoTwoCocycles.proof_3
              isoTwoCocycles.proof_4 ≪≫
            cyclesMapIso (shortComplexH2Iso B) ≪≫ (shortComplexH2 B).moduleCatCyclesIso).hom) ≫
      (shortComplexH2 B).moduleCatLeftHomologyData.i =
    ((HomologicalComplex.cyclesIsoSc' (inhomogeneousCochains A) 1 2 3 isoTwoCocycles.proof_3 isoTwoCocycles.proof_4 ≪≫
            cyclesMapIso (shortComplexH2Iso A) ≪≫ (shortComplexH2 A).moduleCatCyclesIso).hom ≫
        (shortComplexH2 A).moduleCatLeftHomologyData.i) ≫
      (mapShortComplexH2 f φ).τ₂
-- Mathlib/Algebra/Group/Units/Basic.lean
theorem inv_unique {u₁ u₂ : αˣ} (h : (↑u₁ : α) = ↑u₂) : (↑u₁⁻¹ : α) = ↑u₂⁻¹ :=
  Units.inv_eq_of_mul_eq_one_right <| by rw [h, u₂.mul_inv]

Proof state:
α : Type u
inst✝ : Monoid α
u₁ u₂ : αˣ
h : ↑u₁ = ↑u₂
⊢ ↑u₁ * ↑u₂⁻¹ = 1

Tactic:
rw [h, u₂.mul_inv]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean
theorem _root_.Submodule.finrank_eq_rank [Module.Finite R M] (N : Submodule R M) :
    finrank R N = Module.rank R N

Proof state:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
⊢ ↑(finrank R ↥N) = Module.rank R ↥N

Tactic:
rw [finrank, Cardinal.cast_toNat_of_lt_aleph0]

Result:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
⊢ Module.rank R ↥N < ℵ₀

Proof state:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
⊢ Module.rank R ↥N < ℵ₀

Tactic:
exact lt_of_le_of_lt (Submodule.rank_le N) (rank_lt_aleph0 R M)

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem ext_iff_of_biUnion_eq_univ {S : Set ι} {s : ι → Set α} (hc : S.Countable)
    (hs : ⋃ i ∈ S, s i = univ) : μ = ν ↔ ∀ i ∈ S, μ.restrict (s i) = ν.restrict (s i)

Proof state:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
S : Set ι
s : ι → Set α
hc : S.Countable
hs : ⋃ i ∈ S, s i = univ
⊢ μ = ν ↔ ∀ i ∈ S, μ.restrict (s i) = ν.restrict (s i)

Tactic:
rw [← restrict_biUnion_congr hc, hs, restrict_univ, restrict_univ]

Result:
no goals
-- Mathlib/Data/Seq/Computation.lean
theorem LiftRelAux.ret_right (R : α → β → Prop) (C : Computation α → Computation β → Prop) (b ca) :
    LiftRelAux R C (destruct ca) (Sum.inl b) ↔ ∃ a, a ∈ ca ∧ R a b

Proof state:
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
b : β
ca : Computation α
⊢ LiftRelAux R C ca.destruct (Sum.inl b) ↔ ∃ a, a ∈ ca ∧ R a b

Tactic:
rw [← LiftRelAux.swap, LiftRelAux.ret_left]

Result:
no goals