harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean
theorem LinearMap.toMatrix₂_mul_basis_toMatrix (c₁ : Basis n' R M₁) (c₂ : Basis m' R M₂)
    (B : M₁ →ₗ[R] M₂ →ₗ[R] R) :
    (b₁.toMatrix c₁)ᵀ * LinearMap.toMatrix₂ b₁ b₂ B * b₂.toMatrix c₂ =
      LinearMap.toMatrix₂ c₁ c₂ B

Proof state:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R M₂
inst✝⁷ : DecidableEq n
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype m
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
c₁ : Basis n' R M₁
c₂ : Basis m' R M₂
B : M₁ →ₗ[R] M₂ →ₗ[R] R
⊢ (b₁.toMatrix ⇑c₁)ᵀ * (toMatrix₂ b₁ b₂) B * b₂.toMatrix ⇑c₂ = (toMatrix₂ c₁ c₂) B

Tactic:
simp_rw [← LinearMap.toMatrix_id_eq_basis_toMatrix]

Result:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R M₂
inst✝⁷ : DecidableEq n
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype m
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
c₁ : Basis n' R M₁
c₂ : Basis m' R M₂
B : M₁ →ₗ[R] M₂ →ₗ[R] R
⊢ ((toMatrix c₁ b₁) id)ᵀ * (toMatrix₂ b₁ b₂) B * (toMatrix c₂ b₂) id = (toMatrix₂ c₁ c₂) B

Proof state:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R M₂
inst✝⁷ : DecidableEq n
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype m
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
c₁ : Basis n' R M₁
c₂ : Basis m' R M₂
B : M₁ →ₗ[R] M₂ →ₗ[R] R
⊢ ((toMatrix c₁ b₁) id)ᵀ * (toMatrix₂ b₁ b₂) B * (toMatrix c₂ b₂) id = (toMatrix₂ c₁ c₂) B

Tactic:
rw [← LinearMap.toMatrix₂_compl₁₂, LinearMap.compl₁₂_id_id]

Result:
no goals
-- Mathlib/GroupTheory/QuotientGroup/Defs.lean
@[to_additive]
lemma image_coe_inj {s t : Set G} : ((↑) : G → Q) '' s = ((↑) : G → Q) '' t ↔ ↑N * s = N * t

Proof state:
G : Type u
inst✝ : Group G
N : Subgroup G
nN : N.Normal
s t : Set G
⊢ mk '' s = mk '' t ↔ mk ⁻¹' (mk '' s) = mk ⁻¹' (mk '' t)

Tactic:
exact QuotientGroup.mk_surjective.preimage_injective.eq_iff.symm

Result:
no goals

Proof state:
G : Type u
inst✝ : Group G
N : Subgroup G
nN : N.Normal
s t : Set G
⊢ mk '' s = mk '' t ↔ ↑N * s = ↑N * t

Tactic:
simp_rw [← preimage_image_coe]

Result:
G : Type u
inst✝ : Group G
N : Subgroup G
nN : N.Normal
s t : Set G
⊢ mk '' s = mk '' t ↔ mk ⁻¹' (mk '' s) = mk ⁻¹' (mk '' t)
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem two_nsmul_coe_pi : (2 : ℕ) • (π : Angle) = 0

Proof state:
⊢ 2 • ↑π = 0

Tactic:
simp [← natCast_mul_eq_nsmul]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Content.lean
theorem dvd_iff_content_dvd_content_and_primPart_dvd_primPart {p q : R[X]} (hq : q ≠ 0) :
    p ∣ q ↔ p.content ∣ q.content ∧ p.primPart ∣ q.primPart

Proof state:
case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hq : q ≠ 0
h : p.content ∣ q.content ∧ p.primPart ∣ q.primPart
⊢ C p.content * p.primPart ∣ C q.content * q.primPart

Tactic:
exact mul_dvd_mul (RingHom.map_dvd C h.1) h.2

Result:
no goals

Proof state:
case mp.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p r : R[X]
hq : p * r ≠ 0
⊢ p.content ∣ p.content * r.content ∧ p.primPart ∣ p * r

Tactic:
exact ⟨Dvd.intro _ rfl, p.primPart_dvd.trans (Dvd.intro _ rfl)⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hq : q ≠ 0
⊢ p ∣ q ↔ p.content ∣ q.content ∧ p.primPart ∣ q.primPart

Tactic:
constructor <;> intro h

Result:
case mp
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hq : q ≠ 0
h : p ∣ q
⊢ p.content ∣ q.content ∧ p.primPart ∣ q.primPart

case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hq : q ≠ 0
h : p.content ∣ q.content ∧ p.primPart ∣ q.primPart
⊢ p ∣ q

Proof state:
case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hq : q ≠ 0
h : p.content ∣ q.content ∧ p.primPart ∣ q.primPart
⊢ p ∣ q

Tactic:
rw [p.eq_C_content_mul_primPart, q.eq_C_content_mul_primPart]

Result:
case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hq : q ≠ 0
h : p.content ∣ q.content ∧ p.primPart ∣ q.primPart
⊢ C p.content * p.primPart ∣ C q.content * q.primPart

Proof state:
case mp.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p r : R[X]
hq : p * r ≠ 0
⊢ p.content ∣ (p * r).content ∧ p.primPart ∣ (p * r).primPart

Tactic:
rw [content_mul, p.isPrimitive_primPart.dvd_primPart_iff_dvd hq]

Result:
case mp.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p r : R[X]
hq : p * r ≠ 0
⊢ p.content ∣ p.content * r.content ∧ p.primPart ∣ p * r

Proof state:
case mp
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hq : q ≠ 0
h : p ∣ q
⊢ p.content ∣ q.content ∧ p.primPart ∣ q.primPart

Tactic:
rcases h with ⟨r, rfl⟩

Result:
case mp.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p r : R[X]
hq : p * r ≠ 0
⊢ p.content ∣ (p * r).content ∧ p.primPart ∣ (p * r).primPart
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Ico_diff_Ioo_self (h : a < b) : Ico a b \ Ioo a b = {a}

Proof state:
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidableEq α
h : a < b
⊢ Ico a b \ Ioo a b = {a}

Tactic:
simp [← coe_inj, h]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/HurwitzZeta.lean
/-- The difference of two Hurwitz zeta functions is differentiable everywhere. -/
lemma differentiable_hurwitzZeta_sub_hurwitzZeta (a b : UnitAddCircle) :
    Differentiable ℂ (fun s ↦ hurwitzZeta a s - hurwitzZeta b s)

Proof state:
case refine_2
a b : UnitAddCircle
⊢ Differentiable ℂ (hurwitzZetaOdd b)

Tactic:
apply differentiable_hurwitzZetaOdd

Result:
no goals

Proof state:
a b : UnitAddCircle
⊢ Differentiable ℂ fun s => hurwitzZetaEven a s - hurwitzZetaEven b s + (hurwitzZetaOdd a s - hurwitzZetaOdd b s)

Tactic:
refine (differentiable_hurwitzZetaEven_sub_hurwitzZetaEven a b).add (.sub ?_ ?_)

Result:
case refine_1
a b : UnitAddCircle
⊢ Differentiable ℂ (hurwitzZetaOdd a)

case refine_2
a b : UnitAddCircle
⊢ Differentiable ℂ (hurwitzZetaOdd b)

Proof state:
case refine_1
a b : UnitAddCircle
⊢ Differentiable ℂ (hurwitzZetaOdd a)

case refine_2
a b : UnitAddCircle
⊢ Differentiable ℂ (hurwitzZetaOdd b)

Tactic:
all_goals apply differentiable_hurwitzZetaOdd

Result:
no goals

Proof state:
a b : UnitAddCircle
⊢ Differentiable ℂ fun s => hurwitzZeta a s - hurwitzZeta b s

Tactic:
simp only [hurwitzZeta, add_sub_add_comm]

Result:
a b : UnitAddCircle
⊢ Differentiable ℂ fun s => hurwitzZetaEven a s - hurwitzZetaEven b s + (hurwitzZetaOdd a s - hurwitzZetaOdd b s)
-- Mathlib/Probability/Density.lean
theorem hasPDF_of_pdf_ne_zero {m : MeasurableSpace Ω} {ℙ : Measure Ω} {μ : Measure E} {X : Ω → E}
    (hac : map X ℙ ≪ μ) (hpdf : ¬pdf X ℙ μ =ᵐ[μ] 0) : HasPDF X ℙ μ

Proof state:
case refine_2
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
hac : map X ℙ ≪ μ
hpdf : ¬(map X ℙ).HaveLebesgueDecomposition μ
this : pdf X ℙ μ = 0
⊢ pdf X ℙ μ =ᶠ[ae μ] 0

Tactic:
filter_upwards using congrFun this

Result:
no goals

Proof state:
case refine_2
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
hac : map X ℙ ≪ μ
hpdf : ¬(map X ℙ).HaveLebesgueDecomposition μ
⊢ pdf X ℙ μ =ᶠ[ae μ] 0

Tactic:
have := pdf_of_not_haveLebesgueDecomposition hpdf

Result:
case refine_2
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
hac : map X ℙ ≪ μ
hpdf : ¬(map X ℙ).HaveLebesgueDecomposition μ
this : pdf X ℙ μ = 0
⊢ pdf X ℙ μ =ᶠ[ae μ] 0

Proof state:
case refine_1
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
hac : map X ℙ ≪ μ
hpdf : ¬pdf X ℙ μ =ᶠ[ae μ] 0
⊢ AEMeasurable X ℙ

Tactic:
exact aemeasurable_of_pdf_ne_zero X hpdf

Result:
no goals

Proof state:
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
hac : map X ℙ ≪ μ
hpdf : ¬pdf X ℙ μ =ᶠ[ae μ] 0
⊢ HasPDF X ℙ μ

Tactic:
refine ⟨?_, ?_, hac⟩

Result:
case refine_1
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
hac : map X ℙ ≪ μ
hpdf : ¬pdf X ℙ μ =ᶠ[ae μ] 0
⊢ AEMeasurable X ℙ

case refine_2
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
hac : map X ℙ ≪ μ
hpdf : ¬pdf X ℙ μ =ᶠ[ae μ] 0
⊢ (map X ℙ).HaveLebesgueDecomposition μ

Proof state:
case refine_2
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
hac : map X ℙ ≪ μ
hpdf : ¬pdf X ℙ μ =ᶠ[ae μ] 0
⊢ (map X ℙ).HaveLebesgueDecomposition μ

Tactic:
contrapose! hpdf

Result:
case refine_2
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
hac : map X ℙ ≪ μ
hpdf : ¬(map X ℙ).HaveLebesgueDecomposition μ
⊢ pdf X ℙ μ =ᶠ[ae μ] 0
-- Mathlib/GroupTheory/Schreier.lean
theorem closure_mul_image_eq (hR : IsComplement H R) (hR1 : (1 : G) ∈ R)
    (hS : closure S = ⊤) : closure ((R * S).image fun g => g * (hR.toRightFun g : G)⁻¹) = H

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : IsComplement (↑H) R
hR1 : 1 ∈ R
hS : closure S = ⊤
⊢ closure ((fun g => g * (↑(hR.toRightFun g))⁻¹) '' (R * S)) ≤ H

Tactic:
rw [closure_le]

Result:
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : IsComplement (↑H) R
hR1 : 1 ∈ R
hS : closure S = ⊤
⊢ (fun g => g * (↑(hR.toRightFun g))⁻¹) '' (R * S) ⊆ ↑H
-- Mathlib/NumberTheory/DirichletCharacter/Basic.lean
/-- The conductor of the trivial character is 1. -/
lemma conductor_one (hn : n ≠ 0) : conductor (1 : DirichletCharacter R n) = 1

Proof state:
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
hn : n ≠ 0
⊢ FactorsThrough 1 1

Tactic:
exact (factorsThrough_one_iff _).mpr rfl

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
hn : n ≠ 0
this : FactorsThrough 1 1
h : conductor 1 ≤ 1
⊢ conductor 1 = 1

Tactic:
exact Nat.le_antisymm h (Nat.pos_of_ne_zero <| conductor_ne_zero _ hn)

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
hn : n ≠ 0
this : FactorsThrough 1 1
⊢ conductor 1 = 1

Tactic:
have h : conductor (1 : DirichletCharacter R n) ≤ 1 :=
  Nat.sInf_le <| (mem_conductorSet_iff _).mpr this

Result:
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
hn : n ≠ 0
this : FactorsThrough 1 1
h : conductor 1 ≤ 1
⊢ conductor 1 = 1

Proof state:
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
hn : n ≠ 0
⊢ conductor 1 = 1

Tactic:
suffices FactorsThrough (1 : DirichletCharacter R n) 1 by
  have h : conductor (1 : DirichletCharacter R n) ≤ 1 :=
    Nat.sInf_le <| (mem_conductorSet_iff _).mpr this
  exact Nat.le_antisymm h (Nat.pos_of_ne_zero <| conductor_ne_zero _ hn)

Result:
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
hn : n ≠ 0
⊢ FactorsThrough 1 1
-- Mathlib/RingTheory/Polynomial/UniqueFactorization.lean
theorem uniqueFactorizationMonoid_of_fintype [Fintype σ] :
    UniqueFactorizationMonoid (MvPolynomial σ D) :=
  (renameEquiv D (Fintype.equivFin σ)).toMulEquiv.symm.uniqueFactorizationMonoid <| by
    induction' Fintype.card σ with d hd
    · apply (isEmptyAlgEquiv D (Fin 0)).toMulEquiv.symm.uniqueFactorizationMonoid
      infer_instance
    · apply (finSuccEquiv D d).toMulEquiv.symm.uniqueFactorizationMonoid
      exact Polynomial.uniqueFactorizationMonoid

Proof state:
case succ
σ : Type v
D : Type u
inst✝³ : CommRing D
inst✝² : IsDomain D
inst✝¹ : UniqueFactorizationMonoid D
inst✝ : Fintype σ
d : ℕ
hd : UniqueFactorizationMonoid (MvPolynomial (Fin d) D)
⊢ UniqueFactorizationMonoid (MvPolynomial (Fin d) D)[X]

Tactic:
exact Polynomial.uniqueFactorizationMonoid

Result:
no goals

Proof state:
case succ
σ : Type v
D : Type u
inst✝³ : CommRing D
inst✝² : IsDomain D
inst✝¹ : UniqueFactorizationMonoid D
inst✝ : Fintype σ
d : ℕ
hd : UniqueFactorizationMonoid (MvPolynomial (Fin d) D)
⊢ UniqueFactorizationMonoid (MvPolynomial (Fin (d + 1)) D)

Tactic:
apply (finSuccEquiv D d).toMulEquiv.symm.uniqueFactorizationMonoid

Result:
case succ
σ : Type v
D : Type u
inst✝³ : CommRing D
inst✝² : IsDomain D
inst✝¹ : UniqueFactorizationMonoid D
inst✝ : Fintype σ
d : ℕ
hd : UniqueFactorizationMonoid (MvPolynomial (Fin d) D)
⊢ UniqueFactorizationMonoid (MvPolynomial (Fin d) D)[X]

Proof state:
case zero
σ : Type v
D : Type u
inst✝³ : CommRing D
inst✝² : IsDomain D
inst✝¹ : UniqueFactorizationMonoid D
inst✝ : Fintype σ
⊢ UniqueFactorizationMonoid D

Tactic:
infer_instance

Result:
no goals

Proof state:
σ : Type v
D : Type u
inst✝³ : CommRing D
inst✝² : IsDomain D
inst✝¹ : UniqueFactorizationMonoid D
inst✝ : Fintype σ
⊢ UniqueFactorizationMonoid (MvPolynomial (Fin (Fintype.card σ)) D)

Tactic:
induction' Fintype.card σ with d hd

Result:
case zero
σ : Type v
D : Type u
inst✝³ : CommRing D
inst✝² : IsDomain D
inst✝¹ : UniqueFactorizationMonoid D
inst✝ : Fintype σ
⊢ UniqueFactorizationMonoid (MvPolynomial (Fin 0) D)

case succ
σ : Type v
D : Type u
inst✝³ : CommRing D
inst✝² : IsDomain D
inst✝¹ : UniqueFactorizationMonoid D
inst✝ : Fintype σ
d : ℕ
hd : UniqueFactorizationMonoid (MvPolynomial (Fin d) D)
⊢ UniqueFactorizationMonoid (MvPolynomial (Fin (d + 1)) D)

Proof state:
case zero
σ : Type v
D : Type u
inst✝³ : CommRing D
inst✝² : IsDomain D
inst✝¹ : UniqueFactorizationMonoid D
inst✝ : Fintype σ
⊢ UniqueFactorizationMonoid (MvPolynomial (Fin 0) D)

Tactic:
apply (isEmptyAlgEquiv D (Fin 0)).toMulEquiv.symm.uniqueFactorizationMonoid

Result:
case zero
σ : Type v
D : Type u
inst✝³ : CommRing D
inst✝² : IsDomain D
inst✝¹ : UniqueFactorizationMonoid D
inst✝ : Fintype σ
⊢ UniqueFactorizationMonoid D
-- Mathlib/LinearAlgebra/Matrix/Permutation.lean
@[simp]
lemma conjTranspose_permMatrix [Semiring R] [StarRing R] :
    (σ.permMatrix R).conjTranspose = (σ⁻¹).permMatrix R

Proof state:
n : Type u_1
R : Type u_2
inst✝² : DecidableEq n
σ : Perm n
inst✝¹ : Semiring R
inst✝ : StarRing R
⊢ (Perm.permMatrix R σ)ᴴ = Perm.permMatrix R σ⁻¹

Tactic:
simp only [conjTranspose, transpose_permMatrix, map]

Result:
n : Type u_1
R : Type u_2
inst✝² : DecidableEq n
σ : Perm n
inst✝¹ : Semiring R
inst✝ : StarRing R
⊢ (of fun i j => star (Perm.permMatrix R σ⁻¹ i j)) = Perm.permMatrix R σ⁻¹

Proof state:
n : Type u_1
R : Type u_2
inst✝² : DecidableEq n
σ : Perm n
inst✝¹ : Semiring R
inst✝ : StarRing R
⊢ (of fun i j => star (Perm.permMatrix R σ⁻¹ i j)) = Perm.permMatrix R σ⁻¹

Tactic:
aesop

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem zero_shiftLeft (n : Nat) : 0#w <<< n = 0#w

Proof state:
w n : Nat
⊢ 0#w <<< n = 0#w

Tactic:
simp [bv_toNat]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Maps.lean
theorem not_one_mem_ker [Nontrivial S] (f : F) : (1 : R) ∉ ker f

Proof state:
R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
rcf : RingHomClass F R S
inst✝ : Nontrivial S
f : F
⊢ ¬1 = 0

Tactic:
exact one_ne_zero

Result:
no goals

Proof state:
R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
rcf : RingHomClass F R S
inst✝ : Nontrivial S
f : F
⊢ 1 ∉ ker f

Tactic:
rw [mem_ker, map_one]

Result:
R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
rcf : RingHomClass F R S
inst✝ : Nontrivial S
f : F
⊢ ¬1 = 0
-- Mathlib/.lake/packages/batteries/Batteries/Data/PairingHeap.lean
theorem Heap.noSibling_deleteMin {s : Heap α} (eq : s.deleteMin le = some (a, s')) :
    s'.NoSibling

Proof state:
α : Type u_1
le : α → α → Bool
a : α
s' s : Heap α
eq : deleteMin le s = some (a, s')
⊢ s'.NoSibling

Tactic:
cases s with cases eq | node a c => exact noSibling_combine _ _

Result:
no goals

Proof state:
case node.refl
α : Type u_1
le : α → α → Bool
a : α
c sibling✝ : Heap α
⊢ (combine le c).NoSibling

Tactic:
exact noSibling_combine _ _

Result:
no goals
-- Mathlib/Algebra/Order/CauSeq/Basic.lean
theorem equiv_def₃ {f g : CauSeq β abv} (h : f ≈ g) {ε : α} (ε0 : 0 < ε) :
    ∃ i, ∀ j ≥ i, ∀ k ≥ j, abv (f k - g j) < ε :=
  (exists_forall_ge_and (h _ <| half_pos ε0) (f.cauchy₃ <| half_pos ε0)).imp fun _ H j ij k jk => by
    let ⟨h₁, h₂⟩ := H _ ij
    have := lt_of_le_of_lt (abv_add abv (f j - g j) _) (add_lt_add h₁ (h₂ _ jk))
    rwa [sub_add_sub_cancel', add_halves] at this

Proof state:
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
h : f ≈ g
ε : α
ε0 : 0 < ε
x✝ : ℕ
H : ∀ j ≥ x✝, abv (↑(f - g) j) < ε / 2 ∧ ∀ k ≥ j, abv (↑f k - ↑f j) < ε / 2
j : ℕ
ij : j ≥ x✝
k : ℕ
jk : k ≥ j
h₁ : abv (↑(f - g) j) < ε / 2
h₂ : ∀ k ≥ j, abv (↑f k - ↑f j) < ε / 2
this : abv (↑f j - ↑g j + (↑f k - ↑f j)) < ε / 2 + ε / 2
⊢ abv (↑f k - ↑g j) < ε

Tactic:
rwa [sub_add_sub_cancel', add_halves] at this

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
h : f ≈ g
ε : α
ε0 : 0 < ε
x✝ : ℕ
H : ∀ j ≥ x✝, abv (↑(f - g) j) < ε / 2 ∧ ∀ k ≥ j, abv (↑f k - ↑f j) < ε / 2
j : ℕ
ij : j ≥ x✝
k : ℕ
jk : k ≥ j
h₁ : abv (↑(f - g) j) < ε / 2
h₂ : ∀ k ≥ j, abv (↑f k - ↑f j) < ε / 2
⊢ abv (↑f k - ↑g j) < ε

Tactic:
have := lt_of_le_of_lt (abv_add abv (f j - g j) _) (add_lt_add h₁ (h₂ _ jk))

Result:
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
h : f ≈ g
ε : α
ε0 : 0 < ε
x✝ : ℕ
H : ∀ j ≥ x✝, abv (↑(f - g) j) < ε / 2 ∧ ∀ k ≥ j, abv (↑f k - ↑f j) < ε / 2
j : ℕ
ij : j ≥ x✝
k : ℕ
jk : k ≥ j
h₁ : abv (↑(f - g) j) < ε / 2
h₂ : ∀ k ≥ j, abv (↑f k - ↑f j) < ε / 2
this : abv (↑f j - ↑g j + (↑f k - ↑f j)) < ε / 2 + ε / 2
⊢ abv (↑f k - ↑g j) < ε

Proof state:
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
h : f ≈ g
ε : α
ε0 : 0 < ε
x✝ : ℕ
H : ∀ j ≥ x✝, abv (↑(f - g) j) < ε / 2 ∧ ∀ k ≥ j, abv (↑f k - ↑f j) < ε / 2
j : ℕ
ij : j ≥ x✝
k : ℕ
jk : k ≥ j
⊢ abv (↑f k - ↑g j) < ε

Tactic:
let ⟨h₁, h₂⟩ := H _ ij

Result:
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
h : f ≈ g
ε : α
ε0 : 0 < ε
x✝ : ℕ
H : ∀ j ≥ x✝, abv (↑(f - g) j) < ε / 2 ∧ ∀ k ≥ j, abv (↑f k - ↑f j) < ε / 2
j : ℕ
ij : j ≥ x✝
k : ℕ
jk : k ≥ j
h₁ : abv (↑(f - g) j) < ε / 2
h₂ : ∀ k ≥ j, abv (↑f k - ↑f j) < ε / 2
⊢ abv (↑f k - ↑g j) < ε
-- Mathlib/Algebra/Homology/HomotopyCofiber.lean
@[reassoc (attr := simp)]
lemma inrX_desc_f (i : ι) :
    inrX φ i ≫ (desc φ α hα).f i = α.f i

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
α : G ⟶ K
hα : Homotopy (φ ≫ α) 0
i : ι
⊢ (inrX φ i ≫
      if hj : c.Rel i (c.next i) then fstX φ i (c.next i) hj ≫ hα.hom (c.next i) i + sndX φ i ≫ α.f i
      else sndX φ i ≫ α.f i) =
    α.f i

Tactic:
split_ifs <;> simp

Result:
no goals

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
α : G ⟶ K
hα : Homotopy (φ ≫ α) 0
i : ι
⊢ inrX φ i ≫ (desc φ α hα).f i = α.f i

Tactic:
dsimp [desc]

Result:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
α : G ⟶ K
hα : Homotopy (φ ≫ α) 0
i : ι
⊢ (inrX φ i ≫
      if hj : c.Rel i (c.next i) then fstX φ i (c.next i) hj ≫ hα.hom (c.next i) i + sndX φ i ≫ α.f i
      else sndX φ i ≫ α.f i) =
    α.f i
-- Mathlib/Topology/Algebra/Module/Multilinear/Basic.lean
theorem toMultilinearMap_injective :
    Function.Injective
      (ContinuousMultilinearMap.toMultilinearMap :
        ContinuousMultilinearMap R M₁ M₂ → MultilinearMap R M₁ M₂)
  | ⟨f, hf⟩, ⟨g, hg⟩, h => by subst h; rfl

Proof state:
R : Type u
ι : Type v
M₁ : ι → Type w₁
M₂ : Type w₂
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁴ : AddCommMonoid M₂
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
inst✝¹ : (i : ι) → TopologicalSpace (M₁ i)
inst✝ : TopologicalSpace M₂
f : MultilinearMap R M₁ M₂
hf : Continuous f.toFun
hg : Continuous { toMultilinearMap := f, cont := hf }.toFun
⊢ { toMultilinearMap := f, cont := hf } =
    { toMultilinearMap := { toMultilinearMap := f, cont := hf }.toMultilinearMap, cont := hg }

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
ι : Type v
M₁ : ι → Type w₁
M₂ : Type w₂
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁴ : AddCommMonoid M₂
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
inst✝¹ : (i : ι) → TopologicalSpace (M₁ i)
inst✝ : TopologicalSpace M₂
f : MultilinearMap R M₁ M₂
hf : Continuous f.toFun
g : MultilinearMap R M₁ M₂
hg : Continuous g.toFun
h : { toMultilinearMap := f, cont := hf }.toMultilinearMap = { toMultilinearMap := g, cont := hg }.toMultilinearMap
⊢ { toMultilinearMap := f, cont := hf } = { toMultilinearMap := g, cont := hg }

Tactic:
subst h

Result:
R : Type u
ι : Type v
M₁ : ι → Type w₁
M₂ : Type w₂
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁴ : AddCommMonoid M₂
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
inst✝¹ : (i : ι) → TopologicalSpace (M₁ i)
inst✝ : TopologicalSpace M₂
f : MultilinearMap R M₁ M₂
hf : Continuous f.toFun
hg : Continuous { toMultilinearMap := f, cont := hf }.toFun
⊢ { toMultilinearMap := f, cont := hf } =
    { toMultilinearMap := { toMultilinearMap := f, cont := hf }.toMultilinearMap, cont := hg }
-- Mathlib/Topology/MetricSpace/Dilation.lean
theorem diam_range : Metric.diam (range (f : α → β)) = ratio f * Metric.diam (univ : Set α)

Proof state:
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
⊢ Metric.diam (range ⇑f) = ↑(ratio f) * Metric.diam univ

Tactic:
rw [← image_univ, diam_image]

Result:
no goals
-- Mathlib/Data/Fintype/Lattice.lean
theorem Finite.exists_min [Finite α] [Nonempty α] [LinearOrder β] (f : α → β) :
    ∃ x₀ : α, ∀ x, f x₀ ≤ f x

Proof state:
α : Type u_2
β : Type u_3
inst✝² : Finite α
inst✝¹ : Nonempty α
inst✝ : LinearOrder β
f : α → β
⊢ ∃ x₀, ∀ (x : α), f x₀ ≤ f x

Tactic:
cases nonempty_fintype α

Result:
case intro
α : Type u_2
β : Type u_3
inst✝² : Finite α
inst✝¹ : Nonempty α
inst✝ : LinearOrder β
f : α → β
val✝ : Fintype α
⊢ ∃ x₀, ∀ (x : α), f x₀ ≤ f x

Proof state:
case intro
α : Type u_2
β : Type u_3
inst✝² : Finite α
inst✝¹ : Nonempty α
inst✝ : LinearOrder β
f : α → β
val✝ : Fintype α
⊢ ∃ x₀, ∀ (x : α), f x₀ ≤ f x

Tactic:
simpa using exists_min_image univ f univ_nonempty

Result:
no goals