harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Opposite.lean
theorem unop_injective : Function.Injective (unop : αᵒᵖ → α) := fun ⟨_⟩⟨_⟩ => by simp

Proof state:
α : Sort u
x✝¹ x✝ : αᵒᵖ
unop✝¹ unop✝ : α
⊢ unop (op unop✝¹) = unop (op unop✝) → op unop✝¹ = op unop✝

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Interval/Set/OrderIso.lean
theorem preimage_Ico (e : α ≃o β) (a b : β) : e ⁻¹' Ico a b = Ico (e.symm a) (e.symm b)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
a b : β
⊢ ⇑e ⁻¹' Ico a b = Ico (e.symm a) (e.symm b)

Tactic:
simp [← Ici_inter_Iio]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Supported.lean
theorem mem_supported_vars (p : MvPolynomial σ R) : p ∈ supported R (↑p.vars : Set σ)

Proof state:
σ : Type u_1
R : Type u
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ p ∈ supported R ↑p.vars

Tactic:
rw [mem_supported]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean
lemma connected_induce_iff {s : Set V} :
    (G.induce s).Connected ↔ ((⊤ : G.Subgraph).induce s).Connected

Proof state:
V : Type u
G : SimpleGraph V
s : Set V
⊢ (induce s G).Connected ↔ (⊤.induce s).Connected

Tactic:
rw [induce_eq_coe_induce_top, ← Subgraph.connected_iff']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem foldl_reverse (l : List α) (f : β → α → β) (b) :
    l.reverse.foldl f b = l.foldr (fun x y => f y x) b

Proof state:
α : Type u_1
β : Type u_2
l : List α
f : β → α → β
b : β
⊢ foldl f b l.reverse = foldr (fun x y => f y x) b l

Tactic:
simp [foldl_eq_foldlM, foldr_eq_foldrM]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Quotient/Operations.lean
theorem mem_quotient_iff_mem_sup {I J : Ideal R} [I.IsTwoSided] {x : R} :
    Quotient.mk I x ∈ J.map (Quotient.mk I) ↔ x ∈ J ⊔ I

Proof state:
R : Type u
inst✝¹ : Ring R
I J : Ideal R
inst✝ : I.IsTwoSided
x : R
⊢ (Quotient.mk I) x ∈ map (Quotient.mk I) J ↔ x ∈ J ⊔ I

Tactic:
rw [← mem_comap, comap_map_of_surjective (Quotient.mk I) Quotient.mk_surjective, ←
  ker_eq_comap_bot, mk_ker]

Result:
no goals
-- Mathlib/Algebra/SMulWithZero.lean
lemma Pi.single_apply_smul {ι : Type*} [DecidableEq ι] (x : M) (i j : ι) :
    (Pi.single i 1 : ι → R) j • x = (Pi.single i x : ι → M) j

Proof state:
R : Type u_1
M : Type u_3
inst✝³ : MonoidWithZero R
inst✝² : Zero M
inst✝¹ : MulActionWithZero R M
ι : Type u_5
inst✝ : DecidableEq ι
x : M
i j : ι
⊢ single i 1 j • x = single i x j

Tactic:
rw [single_apply, ite_smul, one_smul, zero_smul, single_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem bmod_eq_self_sub_bdiv_mul (x : Int) (m : Nat) : bmod x m = x - bdiv x m * m

Proof state:
x : Int
m : Nat
⊢ x.bmod m = x - x.bdiv m * ↑m

Tactic:
rw [← Int.add_sub_cancel (bmod x m), bmod_add_bdiv']

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean
lemma b_relation_of_char_three : W.b₈ = W.b₂ * W.b₆ - W.b₄ ^ 2

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
⊢ W.b₈ = W.b₂ * W.b₆ - W.b₄ ^ 2

Tactic:
linear_combination W.b_relation - W.b₈ * CharP.cast_eq_zero R 3

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem le_refl (x : BitVec n) : x ≤ x

Proof state:
n : Nat
x : BitVec n
⊢ x ≤ x

Tactic:
simp [le_def]

Result:
no goals
-- Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean
theorem denom_apply (g : SL(2, ℤ)) (z : ℍ) :
    denom g z = g 1 0 * z + g 1 1

Proof state:
g : SL(2, ℤ)
z : ℍ
⊢ denom (↑g) z = ↑(↑g 1 0) * ↑z + ↑(↑g 1 1)

Tactic:
simp [denom, coe]

Result:
no goals
-- Mathlib/MeasureTheory/Group/FundamentalDomain.lean
theorem measure_fundamentalFrontier : μ (fundamentalFrontier G s) = 0

Proof state:
G : Type u_1
α : Type u_3
inst✝³ : Countable G
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsFundamentalDomain G s μ
⊢ μ (fundamentalFrontier G s) = 0

Tactic:
simpa only [fundamentalFrontier, iUnion₂_inter, one_smul, measure_iUnion_null_iff, inter_comm s,
  Function.onFun] using fun g (hg : g ≠ 1) => hs.aedisjoint hg

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/NegMulLog.lean
@[simp] lemma negMulLog_one : negMulLog (1 : ℝ) = 0

Proof state:
⊢ negMulLog 1 = 0

Tactic:
simp [negMulLog]

Result:
no goals
-- Mathlib/Deprecated/Cardinal/PartENat.lean
theorem toPartENat_natCast (n : ℕ) : toPartENat n = n

Proof state:
n : ℕ
⊢ toPartENat ↑n = ↑n

Tactic:
simp only [← partENatOfENat_toENat, toENat_nat, PartENat.ofENat_coe]

Result:
no goals
-- Mathlib/Data/Matrix/ColumnRowPartitioned.lean
@[simp]
lemma fromRows_mulVec [Fintype n] (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) (v : n → R) :
    fromRows A₁ A₂ *ᵥ v = Sum.elim (A₁ *ᵥ v) (A₂ *ᵥ v)

Proof state:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝¹ : Semiring R
inst✝ : Fintype n
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
v : n → R
⊢ A₁.fromRows A₂ *ᵥ v = Sum.elim (A₁ *ᵥ v) (A₂ *ᵥ v)

Tactic:
ext (_ | _) <;> rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/FinRange.lean
theorem getElem_finRange (i : Nat) (h : i < (List.finRange n).length) :
    (finRange n)[i] = Fin.cast (length_finRange n) ⟨i, h⟩

Proof state:
n i : Nat
h : i < (finRange n).length
⊢ (finRange n)[i] = Fin.cast ⋯ ⟨i, h⟩

Tactic:
simp [List.finRange]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Set/BigOperators.lean
theorem image_fintype_prod_pi [Fintype ι] (S : ι → Set α) :
    (fun f : ι → α => ∏ i, f i) '' univ.pi S = ∏ i, S i

Proof state:
ι : Type u_1
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : Fintype ι
S : ι → Set α
⊢ (fun f => ∏ i : ι, f i) '' univ.pi S = ∏ i : ι, S i

Tactic:
simpa only [Finset.coe_univ] using image_finset_prod_pi Finset.univ S

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Colim.lean
/-- Assume that `φ : X₁ ⟶ X₂` is a natural transformation in `J ⥤ C` which
consists of epimorphisms, then if `f : c₁.pt ⟶ c₂.pt` is a morphism
between the points of cocones `c₁` and `c₂` for `X₁` and `X₂`, in such
a way that `c₂` is colimit and `f` is compatible with `φ`, then `f` is an epimorphism. -/
lemma colim.map_epi'
    {X₁ X₂ : J ⥤ C} (φ : X₁ ⟶ X₂) [∀ j, Epi (φ.app j)]
    (c₁ : Cocone X₁) {c₂ : Cocone X₂} (hc₂ : IsColimit c₂)
    (f : c₁.pt ⟶ c₂.pt) (hf : ∀ j, c₁.ι.app j ≫ f = φ.app j ≫ c₂.ι.app j) : Epi f where
  left_cancellation {Z} g₁ g₂ h := hc₂.hom_ext (fun j ↦ by
    rw [← cancel_epi (φ.app j), ← reassoc_of% hf, h, reassoc_of% hf])

Proof state:
C : Type u
inst✝² : Category.{v, u} C
J : Type u'
inst✝¹ : Category.{v', u'} J
X₁ X₂ : J ⥤ C
φ : X₁ ⟶ X₂
inst✝ : ∀ (j : J), Epi (φ.app j)
c₁ : Cocone X₁
c₂ : Cocone X₂
hc₂ : IsColimit c₂
f : c₁.pt ⟶ c₂.pt
hf : ∀ (j : J), c₁.ι.app j ≫ f = φ.app j ≫ c₂.ι.app j
Z : C
g₁ g₂ : c₂.pt ⟶ Z
h : f ≫ g₁ = f ≫ g₂
j : J
⊢ c₂.ι.app j ≫ g₁ = c₂.ι.app j ≫ g₂

Tactic:
rw [← cancel_epi (φ.app j), ← reassoc_of% hf, h, reassoc_of% hf]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Zip.lean
theorem lt_size_right_of_zipWith {f : α → β → γ} {i : Nat} {l : Array α} {l' : Array β}
    (h : i < (zipWith f l l').size) : i < l'.size

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
i : Nat
l : Array α
l' : Array β
h : i < (zipWith f l l').size
⊢ i < l'.size

Tactic:
rw [size_zipWith] at h

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
i : Nat
l : Array α
l' : Array β
h : i < min l.size l'.size
⊢ i < l'.size

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
i : Nat
l : Array α
l' : Array β
h : i < min l.size l'.size
⊢ i < l'.size

Tactic:
omega

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem any_eq {xs : Vector α n} {p : α → Bool} : xs.any p = decide (∃ i : Nat, ∃ h, p (xs[i]'h))

Proof state:
case neg
α : Type u_1
n : Nat
xs : Vector α n
p : α → Bool
h : ¬xs.any p = true
⊢ xs.any p = decide (∃ i h, p xs[i] = true)

Tactic:
simp_all [any_eq_false]

Result:
no goals

Proof state:
case pos
α : Type u_1
n : Nat
xs : Vector α n
p : α → Bool
h : xs.any p = true
⊢ xs.any p = decide (∃ i h, p xs[i] = true)

Tactic:
simp_all [any_eq_true]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
xs : Vector α n
p : α → Bool
⊢ xs.any p = decide (∃ i h, p xs[i] = true)

Tactic:
by_cases h : xs.any p

Result:
case pos
α : Type u_1
n : Nat
xs : Vector α n
p : α → Bool
h : xs.any p = true
⊢ xs.any p = decide (∃ i h, p xs[i] = true)

case neg
α : Type u_1
n : Nat
xs : Vector α n
p : α → Bool
h : ¬xs.any p = true
⊢ xs.any p = decide (∃ i h, p xs[i] = true)
-- Mathlib/RingTheory/Flat/Basic.lean
lemma iff_lTensor_injectiveₛ : Flat R M ↔ ∀ ⦃P : Type u⦄ [AddCommMonoid P] [Module R P]
    (N : Submodule R P), Function.Injective (N.subtype.lTensor M)

Proof state:
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ Flat R M ↔
    ∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
      Function.Injective ⇑(lTensor M N.subtype)

Tactic:
simp_rw [iff_rTensor_injectiveₛ, LinearMap.lTensor_inj_iff_rTensor_inj]

Result:
no goals
-- Mathlib/Data/Fintype/Perm.lean
theorem length_permsOfList : ∀ l : List α, length (permsOfList l) = l.length !
  | [] => rfl
  | a :: l => by
    simp [Nat.factorial_succ, permsOfList, length_permsOfList, comp_def, succ_mul, add_comm]

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
⊢ (permsOfList (a :: l)).length = (a :: l).length !

Tactic:
simp [Nat.factorial_succ, permsOfList, length_permsOfList, comp_def, succ_mul, add_comm]

Result:
no goals
-- Mathlib/Condensed/Discrete/Characterization.lean
lemma mem_locallyConstant_essImage_of_isColimit_mapCocone (X : LightCondSet.{u})
    (h : ∀ S : LightProfinite.{u}, IsColimit <|
      X.val.mapCocone (coconeRightOpOfCone S.asLimitCone)) :
    LightCondSet.LocallyConstant.functor.essImage X

Proof state:
X : LightCondSet
h : (S : LightProfinite) → IsColimit (X.val.mapCocone (coconeRightOpOfCone S.asLimitCone))
⊢ LocallyConstant.functor.essImage X

Tactic:
let i : X.val ≅ (LightCondSet.LocallyConstant.functor.obj _).val :=
  LightCondensed.isoLocallyConstantOfIsColimit _ h

Result:
X : LightCondSet
h : (S : LightProfinite) → IsColimit (X.val.mapCocone (coconeRightOpOfCone S.asLimitCone))
i : X.val ≅ (LocallyConstant.functor.obj (X.val.obj (toLightProfinite.op.obj (Opposite.op (of PUnit.{u + 1}))))).val :=
  LightCondensed.isoLocallyConstantOfIsColimit X.val h
⊢ LocallyConstant.functor.essImage X

Proof state:
X : LightCondSet
h : (S : LightProfinite) → IsColimit (X.val.mapCocone (coconeRightOpOfCone S.asLimitCone))
i : X.val ≅ (LocallyConstant.functor.obj (X.val.obj (toLightProfinite.op.obj (Opposite.op (of PUnit.{u + 1}))))).val :=
  LightCondensed.isoLocallyConstantOfIsColimit X.val h
⊢ LocallyConstant.functor.essImage X

Tactic:
exact ⟨_, ⟨((sheafToPresheaf _ _).preimageIso i.symm)⟩⟩

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem IsBigOWith.prod_left_same (hf : IsBigOWith c l f' k') (hg : IsBigOWith c l g' k') :
    IsBigOWith c l (fun x => (f' x, g' x)) k'

Proof state:
α : Type u_1
E' : Type u_6
F' : Type u_7
G' : Type u_8
inst✝² : SeminormedAddCommGroup E'
inst✝¹ : SeminormedAddCommGroup F'
inst✝ : SeminormedAddCommGroup G'
c : ℝ
f' : α → E'
g' : α → F'
k' : α → G'
l : Filter α
hf : IsBigOWith c l f' k'
hg : IsBigOWith c l g' k'
⊢ IsBigOWith c l (fun x => (f' x, g' x)) k'

Tactic:
rw [isBigOWith_iff] at *

Result:
α : Type u_1
E' : Type u_6
F' : Type u_7
G' : Type u_8
inst✝² : SeminormedAddCommGroup E'
inst✝¹ : SeminormedAddCommGroup F'
inst✝ : SeminormedAddCommGroup G'
c : ℝ
f' : α → E'
g' : α → F'
k' : α → G'
l : Filter α
hf : ∀ᶠ (x : α) in l, ‖f' x‖ ≤ c * ‖k' x‖
hg : ∀ᶠ (x : α) in l, ‖g' x‖ ≤ c * ‖k' x‖
⊢ ∀ᶠ (x : α) in l, ‖(f' x, g' x)‖ ≤ c * ‖k' x‖

Proof state:
α : Type u_1
E' : Type u_6
F' : Type u_7
G' : Type u_8
inst✝² : SeminormedAddCommGroup E'
inst✝¹ : SeminormedAddCommGroup F'
inst✝ : SeminormedAddCommGroup G'
c : ℝ
f' : α → E'
g' : α → F'
k' : α → G'
l : Filter α
hf : ∀ᶠ (x : α) in l, ‖f' x‖ ≤ c * ‖k' x‖
hg : ∀ᶠ (x : α) in l, ‖g' x‖ ≤ c * ‖k' x‖
⊢ ∀ᶠ (x : α) in l, ‖(f' x, g' x)‖ ≤ c * ‖k' x‖

Tactic:
filter_upwards [hf, hg] with x using max_le

Result:
no goals
-- Mathlib/Combinatorics/Quiver/Cast.lean
theorem Path.cast_eq_iff_heq {u v u' v' : U} (hu : u = u') (hv : v = v') (p : Path u v)
    (p' : Path u' v') : p.cast hu hv = p' ↔ HEq p p'

Proof state:
U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
p : Path u v
p' : Path u' v'
⊢ cast hu hv p = p' ↔ HEq p p'

Tactic:
rw [Path.cast_eq_cast]

Result:
U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
p : Path u v
p' : Path u' v'
⊢ _root_.cast ⋯ p = p' ↔ HEq p p'

Proof state:
U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
p : Path u v
p' : Path u' v'
⊢ _root_.cast ⋯ p = p' ↔ HEq p p'

Tactic:
exact _root_.cast_eq_iff_heq

Result:
no goals
-- Mathlib/Data/Int/GCD.lean
theorem gcd_eq_right {i j : ℤ} (H : j ∣ i) : gcd i j = natAbs j

Proof state:
i j : ℤ
H : j ∣ i
⊢ i.gcd j = j.natAbs

Tactic:
rw [gcd_comm, gcd_eq_left H]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem negSucc_not_nonneg (n : Nat) : 0 ≤ -[n+1] ↔ False

Proof state:
n : Nat
⊢ -[n+1] < 0

Tactic:
exact Int.negSucc_lt_zero n

Result:
no goals

Proof state:
n : Nat
⊢ 0 ≤ -[n+1] ↔ False

Tactic:
simp only [Int.not_le, iff_false]

Result:
n : Nat
⊢ -[n+1] < 0
-- Mathlib/Topology/ContinuousOn.lean
theorem continuousWithinAt_univ (f : α → β) (x : α) :
    ContinuousWithinAt f Set.univ x ↔ ContinuousAt f x

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
x : α
⊢ ContinuousWithinAt f univ x ↔ ContinuousAt f x

Tactic:
rw [ContinuousAt, ContinuousWithinAt, nhdsWithin_univ]

Result:
no goals
-- Mathlib/RingTheory/ClassGroup.lean
theorem FractionalIdeal.canonicalEquiv_mk0 [IsDedekindDomain R] (K' : Type*) [Field K']
    [Algebra R K'] [IsFractionRing R K'] (I : (Ideal R)⁰) :
    FractionalIdeal.canonicalEquiv R⁰ K K' (FractionalIdeal.mk0 K I) =
    FractionalIdeal.mk0 K' I

Proof state:
R : Type u_1
K : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : Field K
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K' : Type u_3
inst✝² : Field K'
inst✝¹ : Algebra R K'
inst✝ : IsFractionRing R K'
I : ↥(Ideal R)⁰
⊢ (canonicalEquiv R⁰ K K') ↑((mk0 K) I) = ↑((mk0 K') I)

Tactic:
simp only [FractionalIdeal.coe_mk0, FractionalIdeal.canonicalEquiv_coeIdeal]

Result:
no goals
-- Mathlib/Geometry/RingedSpace/Basic.lean
@[simp]
lemma zeroLocus_empty_eq_univ {U : Opens X} :
    X.zeroLocus (∅ : Set (X.presheaf.obj (op U))) = Set.univ

Proof state:
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
⊢ X.zeroLocus ∅ = Set.univ

Tactic:
simp [zeroLocus]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma addU_of_Z_eq_zero_left {P Q : Fin 3 → F} (hPz : P z = 0) : addU P Q = 0

Proof state:
F : Type u
inst✝ : Field F
P Q : Fin 3 → F
hPz : P z = 0
⊢ addU P Q = 0

Tactic:
rw [addU, hPz, zero_mul, div_zero, neg_zero]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem cos_nat_mul_two_pi_add_pi (n : ℕ) : cos (n * (2 * π) + π) = -1

Proof state:
n : ℕ
⊢ cos (↑n * (2 * ↑π) + ↑π) = -1

Tactic:
simpa only [cos_zero] using (cos_periodic.nat_mul n).add_antiperiod_eq cos_antiperiodic

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
theorem measurable_eq_mp {i i' : δ} (h : i = i') : Measurable (congr_arg π h).mp

Proof state:
δ : Type u_4
π : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (π a)
i i' : δ
h : i = i'
⊢ Measurable ⋯.mp

Tactic:
cases h

Result:
case refl
δ : Type u_4
π : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (π a)
i : δ
⊢ Measurable ⋯.mp

Proof state:
case refl
δ : Type u_4
π : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (π a)
i : δ
⊢ Measurable ⋯.mp

Tactic:
exact measurable_id

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getElem_ofBool {b : Bool} : (ofBool b)[0] = b

Proof state:
b : Bool
⊢ (ofBool b)[0] = b

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/RootSystem.lean
@[simp]
lemma chainLength_zero [Nontrivial L] : chainLength 0 β = 0

Proof state:
K : Type u_1
L : Type u_2
inst✝⁸ : Field K
inst✝⁷ : CharZero K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : IsKilling K L
inst✝³ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝² : H.IsCartanSubalgebra
inst✝¹ : IsTriangularizable K (↥H) L
β : Weight K (↥H) L
inst✝ : Nontrivial L
⊢ chainLength 0 β = 0

Tactic:
simp [← chainBotCoeff_add_chainTopCoeff]

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
lemma denseRange_comap_iff_ker_le_nilRadical :
    DenseRange (comap f) ↔ RingHom.ker f ≤ nilradical R

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
⊢ DenseRange ⇑(comap f) ↔ RingHom.ker f ≤ nilradical R

Tactic:
rw [denseRange_iff_closure_range, closure_range_comap, ← Set.top_eq_univ, zeroLocus_eq_top_iff,
  SetLike.coe_subset_coe]

Result:
no goals
-- Mathlib/Data/Option/NAry.lean
theorem map₂_map_right (f : α → γ → δ) (g : β → γ) :
    map₂ f a (b.map g) = map₂ (fun a b => f a (g b)) a b

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : Option α
b : Option β
f : α → γ → δ
g : β → γ
⊢ map₂ f a (Option.map g b) = map₂ (fun a b => f a (g b)) a b

Tactic:
cases b <;> rfl

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/Biproducts.lean
theorem biproduct.lift_matrix {K : Type} [Finite K] [HasFiniteBiproducts C] {f : J → C} {g : K → C}
    {P} (x : ∀ j, P ⟶ f j) (m : ∀ j k, f j ⟶ g k) :
    biproduct.lift x ≫ biproduct.matrix m = biproduct.lift fun k => ∑ j, x j ≫ m j k

Proof state:
case w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
J : Type
inst✝² : Fintype J
K : Type
inst✝¹ : Finite K
inst✝ : HasFiniteBiproducts C
f : J → C
g : K → C
P : C
x : (j : J) → P ⟶ f j
m : (j : J) → (k : K) → f j ⟶ g k
j✝ : K
⊢ (lift x ≫ matrix m) ≫ π g j✝ = (lift fun k => ∑ j : J, x j ≫ m j k) ≫ π g j✝

Tactic:
simp [biproduct.lift_desc]

Result:
no goals

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
J : Type
inst✝² : Fintype J
K : Type
inst✝¹ : Finite K
inst✝ : HasFiniteBiproducts C
f : J → C
g : K → C
P : C
x : (j : J) → P ⟶ f j
m : (j : J) → (k : K) → f j ⟶ g k
⊢ lift x ≫ matrix m = lift fun k => ∑ j : J, x j ≫ m j k

Tactic:
ext

Result:
case w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
J : Type
inst✝² : Fintype J
K : Type
inst✝¹ : Finite K
inst✝ : HasFiniteBiproducts C
f : J → C
g : K → C
P : C
x : (j : J) → P ⟶ f j
m : (j : J) → (k : K) → f j ⟶ g k
j✝ : K
⊢ (lift x ≫ matrix m) ≫ π g j✝ = (lift fun k => ∑ j : J, x j ≫ m j k) ≫ π g j✝
-- Mathlib/Data/Finset/Piecewise.lean
lemma piecewise_singleton [DecidableEq ι] (i : ι) : piecewise {i} f g = update g i (f i)

Proof state:
ι : Type u_1
π : ι → Sort u_2
f g : (i : ι) → π i
inst✝ : DecidableEq ι
i : ι
⊢ {i}.piecewise f g = update g i (f i)

Tactic:
rw [← insert_emptyc_eq, piecewise_insert, piecewise_empty]

Result:
no goals
-- Mathlib/Algebra/FreeAlgebra.lean
theorem lift_ι_apply (f : X → A) (x) : lift R f (ι R x) = f x

Proof state:
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
x : X
⊢ ((lift R) f) (ι R x) = f x

Tactic:
rw [ι_def, lift]

Result:
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
x : X
⊢ ({ toFun := FreeAlgebra.liftAux R, invFun := fun F => ⇑F ∘ ι R, left_inv := ⋯, right_inv := ⋯ } f)
      (Quot.mk (Rel R X) (Pre.of x)) =
    f x

Proof state:
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
x : X
⊢ ({ toFun := FreeAlgebra.liftAux R, invFun := fun F => ⇑F ∘ ι R, left_inv := ⋯, right_inv := ⋯ } f)
      (Quot.mk (Rel R X) (Pre.of x)) =
    f x

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem sshiftRight'_or_of_and_eq_zero {x : BitVec w₁} {y z : BitVec w₂}
    (h : y &&& z = 0#w₂) :
    x.sshiftRight' (y ||| z) = (x.sshiftRight' y).sshiftRight' z

Proof state:
w₁ w₂ : Nat
x : BitVec w₁
y z : BitVec w₂
h : y &&& z = 0#w₂
⊢ x.sshiftRight' (y ||| z) = (x.sshiftRight' y).sshiftRight' z

Tactic:
simp [sshiftRight', ← add_eq_or_of_and_eq_zero _ _ h,
  toNat_add_of_and_eq_zero h, sshiftRight_add]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Mirror.lean
theorem mirror_eq_zero : p.mirror = 0 ↔ p = 0 :=
  ⟨fun h => by rw [← p.mirror_mirror, h, mirror_zero], fun h => by rw [h, mirror_zero]⟩

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
h : p = 0
⊢ p.mirror = 0

Tactic:
rw [h, mirror_zero]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
h : p.mirror = 0
⊢ p = 0

Tactic:
rw [← p.mirror_mirror, h, mirror_zero]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntegrableOn.lean
theorem integrableOn_Ici_iff_integrableOn_Ioi' (hb : μ {b} ≠ ∞) :
    IntegrableOn f (Ici b) μ ↔ IntegrableOn f (Ioi b) μ

Proof state:
α : Type u_1
E : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : Measure α
b : α
hb : μ {b} ≠ ⊤
⊢ IntegrableOn f (Ici b) μ ↔ IntegrableOn f (Ioi b) μ

Tactic:
rw [← Ioi_union_left, integrableOn_union,
  eq_true (integrableOn_singleton_iff.mpr <| Or.inr hb.lt_top), and_true]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean
theorem sum_filter_count_eq_countP [DecidableEq α] (p : α → Prop) [DecidablePred p] (l : List α) :
    ∑ x ∈ l.toFinset with p x, l.count x = l.countP p

Proof state:
α : Type u_3
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
l : List α
⊢ ∑ x ∈ filter (fun x => p x) l.toFinset, count x l = countP (fun b => decide (p b)) l

Tactic:
simp [Finset.sum, sum_map_count_dedup_filter_eq_countP p l]

Result:
no goals
-- Mathlib/Data/Finset/NatAntidiagonal.lean
theorem card_antidiagonal (n : ℕ) : (antidiagonal n).card = n + 1

Proof state:
n : ℕ
⊢ #(antidiagonal n) = n + 1

Tactic:
simp [antidiagonal]

Result:
no goals
-- Mathlib/LinearAlgebra/Determinant.lean
lemma det_mulRight (a : R) : (mulRight R a).det = a

Proof state:
R : Type u_1
inst✝ : CommRing R
a : R
⊢ LinearMap.det (mulRight R a) = a

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Norm.lean
theorem norm_algebraMap [Algebra.IsSeparable K L] (x : 𝓞 K) :
    norm K (algebraMap (𝓞 K) (𝓞 L) x) = x ^ finrank K L

Proof state:
L : Type u_1
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
x : 𝓞 K
⊢ (norm K) ((algebraMap (𝓞 K) (𝓞 L)) x) = x ^ finrank K L

Tactic:
rw [RingOfIntegers.ext_iff, RingOfIntegers.coe_eq_algebraMap,
  RingOfIntegers.algebraMap_norm_algebraMap, Algebra.norm_algebraMap,
  RingOfIntegers.coe_eq_algebraMap, map_pow]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Images.lean
theorem image.factorThruImage_preComp [HasImage g] [HasImage (f ≫ g)] :
    factorThruImage (f ≫ g) ≫ image.preComp f g = f ≫ factorThruImage g

Proof state:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝¹ : HasImage g
inst✝ : HasImage (f ≫ g)
⊢ factorThruImage (f ≫ g) ≫ preComp f g = f ≫ factorThruImage g

Tactic:
simp [image.preComp]

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/QuadraticChar/Basic.lean
theorem quadraticCharFun_zero : quadraticCharFun F 0 = 0

Proof state:
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
⊢ quadraticCharFun F 0 = 0

Tactic:
simp only [quadraticCharFun, if_true]

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ioo_union_left (hab : a < b) : Ioo a b ∪ {a} = Ico a b

Proof state:
α : Type u_1
inst✝ : PartialOrder α
a b : α
hab : a < b
⊢ Ioo a b ∪ {a} = Ico a b

Tactic:
rw [← Ico_diff_left, diff_union_self,
  union_eq_self_of_subset_right (singleton_subset_iff.2 <| left_mem_Ico.2 hab)]

Result:
no goals