harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Localization/HomEquiv.lean
lemma homEquiv_trans (f : L₁.obj X ⟶ L₁.obj Y) :
    homEquiv W L₂ L₃ (homEquiv W L₁ L₂ f) = homEquiv W L₁ L₃ f

Proof state:
C : Type u_1
D₁ : Type u_5
D₂ : Type u_6
D₃ : Type u_7
inst✝⁶ : Category.{u_9, u_1} C
inst✝⁵ : Category.{u_8, u_5} D₁
inst✝⁴ : Category.{u_11, u_6} D₂
inst✝³ : Category.{u_10, u_7} D₃
W : MorphismProperty C
L₁ : C ⥤ D₁
inst✝² : L₁.IsLocalization W
L₂ : C ⥤ D₂
inst✝¹ : L₂.IsLocalization W
L₃ : C ⥤ D₃
inst✝ : L₃.IsLocalization W
X Y : C
f : L₁.obj X ⟶ L₁.obj Y
⊢ (homEquiv W L₂ L₃) ((homEquiv W L₁ L₂) f) = (homEquiv W L₁ L₃) f

Tactic:
dsimp only [homEquiv_apply]

Result:
C : Type u_1
D₁ : Type u_5
D₂ : Type u_6
D₃ : Type u_7
inst✝⁶ : Category.{u_9, u_1} C
inst✝⁵ : Category.{u_8, u_5} D₁
inst✝⁴ : Category.{u_11, u_6} D₂
inst✝³ : Category.{u_10, u_7} D₃
W : MorphismProperty C
L₁ : C ⥤ D₁
inst✝² : L₁.IsLocalization W
L₂ : C ⥤ D₂
inst✝¹ : L₂.IsLocalization W
L₃ : C ⥤ D₃
inst✝ : L₃.IsLocalization W
X Y : C
f : L₁.obj X ⟶ L₁.obj Y
⊢ (LocalizerMorphism.id W).homMap L₂ L₃ ((LocalizerMorphism.id W).homMap L₁ L₂ f) =
    (LocalizerMorphism.id W).homMap L₁ L₃ f

Proof state:
C : Type u_1
D₁ : Type u_5
D₂ : Type u_6
D₃ : Type u_7
inst✝⁶ : Category.{u_9, u_1} C
inst✝⁵ : Category.{u_8, u_5} D₁
inst✝⁴ : Category.{u_11, u_6} D₂
inst✝³ : Category.{u_10, u_7} D₃
W : MorphismProperty C
L₁ : C ⥤ D₁
inst✝² : L₁.IsLocalization W
L₂ : C ⥤ D₂
inst✝¹ : L₂.IsLocalization W
L₃ : C ⥤ D₃
inst✝ : L₃.IsLocalization W
X Y : C
f : L₁.obj X ⟶ L₁.obj Y
⊢ (LocalizerMorphism.id W).homMap L₂ L₃ ((LocalizerMorphism.id W).homMap L₁ L₂ f) =
    (LocalizerMorphism.id W).homMap L₁ L₃ f

Tactic:
apply LocalizerMorphism.homMap_homMap

Result:
no goals
-- Mathlib/Algebra/Polynomial/Module/AEval.lean
lemma of_symm_X_smul (m : AEval R M a) :
    (of R M a).symm ((X : R[X]) • m) = a • (of R M a).symm m

Proof state:
R : Type u_1
A : Type u_3
M : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
a : A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
m : AEval R M a
⊢ (of R M a).symm (X • m) = a • (of R M a).symm m

Tactic:
rw [of_symm_smul, aeval_X]

Result:
no goals
-- Mathlib/Data/List/TakeDrop.lean
theorem takeI_left' {l₁ l₂ : List α} {n} (h : length l₁ = n) : takeI n (l₁ ++ l₂) = l₁

Proof state:
α : Type u
inst✝ : Inhabited α
l₁ l₂ : List α
n : ℕ
h : l₁.length = n
⊢ takeI l₁.length (l₁ ++ l₂) = l₁

Tactic:
apply takeI_left

Result:
no goals

Proof state:
α : Type u
inst✝ : Inhabited α
l₁ l₂ : List α
n : ℕ
h : l₁.length = n
⊢ takeI n (l₁ ++ l₂) = l₁

Tactic:
rw [← h]

Result:
α : Type u
inst✝ : Inhabited α
l₁ l₂ : List α
n : ℕ
h : l₁.length = n
⊢ takeI l₁.length (l₁ ++ l₂) = l₁
-- Mathlib/Combinatorics/HalesJewett.lean
lemma apply_some (h : l.idxFun i = some a) : l x i = a

Proof state:
α : Type u_2
ι : Type u_3
l : Line α ι
i : ι
a x : α
h : l.idxFun i = some a
⊢ ↑l x i = a

Tactic:
simp [l.apply_def, h]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Projection.lean
theorem orthogonalProjection_map_apply {E E' : Type*} [NormedAddCommGroup E]
    [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 E'] (f : E ≃ₗᵢ[𝕜] E')
    (p : Submodule 𝕜 E) [HasOrthogonalProjection p] (x : E') :
    (orthogonalProjection (p.map (f.toLinearEquiv : E →ₗ[𝕜] E')) x : E') =
      f (orthogonalProjection p (f.symm x))

Proof state:
𝕜 : Type u_1
inst✝⁵ : RCLike 𝕜
E : Type u_4
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace 𝕜 E'
f : E ≃ₗᵢ[𝕜] E'
p : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection p
x : E'
⊢ ↑((orthogonalProjection (Submodule.map (↑f.toLinearEquiv) p)) x) = f ↑((orthogonalProjection p) (f.symm x))

Tactic:
simpa only [f.coe_toLinearIsometry, f.apply_symm_apply] using
  (f.toLinearIsometry.map_orthogonalProjection' p (f.symm x)).symm

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Int.lean
theorem abs_lt_one_iff {a : ℤ} : |a| < 1 ↔ a = 0

Proof state:
a : ℤ
⊢ |a| < 1 ↔ a = 0

Tactic:
rw [← zero_add 1, lt_add_one_iff, abs_nonpos_iff]

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Defs.lean
@[to_additive]
nonrec lemma orbitRel.Quotient.mapsTo_smul_orbit (g : G) (x : orbitRel.Quotient G α) :
    Set.MapsTo (g • ·) x.orbit x.orbit

Proof state:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
x : Quotient G α
⊢ Set.MapsTo (fun x => g • x) (MulAction.orbit G (Quotient.out x)) (MulAction.orbit G (Quotient.out x))

Tactic:
exact mapsTo_smul_orbit g x.out

Result:
no goals

Proof state:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
x : Quotient G α
⊢ Set.MapsTo (fun x => g • x) x.orbit x.orbit

Tactic:
rw [orbitRel.Quotient.orbit_eq_orbit_out x Quotient.out_eq']

Result:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
x : Quotient G α
⊢ Set.MapsTo (fun x => g • x) (MulAction.orbit G (Quotient.out x)) (MulAction.orbit G (Quotient.out x))
-- Mathlib/Data/Prod/TProd.lean
theorem mk_elim (hnd : l.Nodup) (h : ∀ i, i ∈ l) (v : TProd α l) : TProd.mk l (v.elim' h) = v :=
  TProd.ext hnd fun i hi => by simp [elim_mk]

Proof state:
ι : Type u
α : ι → Type v
l : List ι
inst✝ : DecidableEq ι
hnd : l.Nodup
h : ∀ (i : ι), i ∈ l
v : TProd α l
i : ι
hi : i ∈ l
⊢ (TProd.mk l (TProd.elim' h v)).elim hi = v.elim hi

Tactic:
simp [elim_mk]

Result:
no goals
-- Mathlib/Data/Int/Cast/Basic.lean
@[simp] lemma zsmul_one [AddGroupWithOne R] (n : ℤ) : n • (1 : R) = n

Proof state:
R : Type u_1
inst✝ : AddGroupWithOne R
n : ℤ
⊢ n • 1 = ↑n

Tactic:
cases n <;> simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/Restrict.lean
@[reassoc (attr := simp)]
lemma resLE_comp_ι : f.resLE U V e ≫ U.ι = V.ι ≫ f

Proof state:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
⊢ resLE f U V e ≫ U.ι = V.ι ≫ f

Tactic:
simp [resLE]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem orderIsoRpow_symm_eq (y : ℝ) (hy : 0 < y) :
    (orderIsoRpow y hy).symm = orderIsoRpow (1 / y) (one_div_pos.2 hy)

Proof state:
y : ℝ
hy : 0 < y
⊢ (StrictMono.orderIsoOfRightInverse (fun x => x ^ y) ⋯ (fun x => x ^ (1 / y)) ⋯).symm =
    StrictMono.orderIsoOfRightInverse (fun x => x ^ (1 / y)) ⋯ (fun x => x ^ y) ⋯

Tactic:
rfl

Result:
no goals

Proof state:
y : ℝ
hy : 0 < y
⊢ (orderIsoRpow y hy).symm = orderIsoRpow (1 / y) ⋯

Tactic:
simp only [orderIsoRpow, one_div_one_div]

Result:
y : ℝ
hy : 0 < y
⊢ (StrictMono.orderIsoOfRightInverse (fun x => x ^ y) ⋯ (fun x => x ^ (1 / y)) ⋯).symm =
    StrictMono.orderIsoOfRightInverse (fun x => x ^ (1 / y)) ⋯ (fun x => x ^ y) ⋯
-- Mathlib/LinearAlgebra/Contraction.lean
theorem dualTensorHomEquivOfBasis_apply (x : Module.Dual R M ⊗[R] N) :
    dualTensorHomEquivOfBasis b x = dualTensorHom R M N x

Proof state:
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
x : Dual R M ⊗[R] N
⊢ (dualTensorHomEquivOfBasis b) x = (dualTensorHom R M N) x

Tactic:
ext

Result:
case h
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
x : Dual R M ⊗[R] N
x✝ : M
⊢ ((dualTensorHomEquivOfBasis b) x) x✝ = ((dualTensorHom R M N) x) x✝

Proof state:
case h
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
x : Dual R M ⊗[R] N
x✝ : M
⊢ ((dualTensorHomEquivOfBasis b) x) x✝ = ((dualTensorHom R M N) x) x✝

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/Localization/Away/Basic.lean
lemma algebraMap_isUnit : IsUnit (algebraMap R S x) :=
  IsLocalization.map_units _ (⟨x, 1, by simp⟩ : Submonoid.powers x)

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
x : R
inst✝ : Away x S
⊢ (fun x_1 => x ^ x_1) 1 = x

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/NoetherianSpace.lean
theorem NoetherianSpace.exists_finite_set_isClosed_irreducible [NoetherianSpace α]
    {s : Set α} (hs : IsClosed s) : ∃ S : Set (Set α), S.Finite ∧
      (∀ t ∈ S, IsClosed t) ∧ (∀ t ∈ S, IsIrreducible t) ∧ s = ⋃₀ S

Proof state:
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
S : Set (Closeds α)
hSf : S.Finite
hS : ∀ t ∈ S, IsIrreducible ↑t
⊢ ∃ S_1, S_1.Finite ∧ (∀ t ∈ S_1, IsClosed t) ∧ (∀ t ∈ S_1, IsIrreducible t) ∧ ↑(sSup S) = ⋃₀ S_1

Tactic:
refine ⟨(↑) '' S, hSf.image _, Set.forall_mem_image.2 fun S _ ↦ S.2, Set.forall_mem_image.2 hS,
  ?_⟩

Result:
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
S : Set (Closeds α)
hSf : S.Finite
hS : ∀ t ∈ S, IsIrreducible ↑t
⊢ ↑(sSup S) = ⋃₀ (SetLike.coe '' S)

Proof state:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
S : Finset (Closeds α)
hS : ∀ t ∈ ↑S, IsIrreducible ↑t
⊢ ↑(sSup ↑S) = ⋃₀ (SetLike.coe '' ↑S)

Tactic:
simp [← Finset.sup_id_eq_sSup, Closeds.coe_finset_sup]

Result:
no goals

Proof state:
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
S : Set (Closeds α)
hSf : S.Finite
hS : ∀ t ∈ S, IsIrreducible ↑t
⊢ ↑(sSup S) = ⋃₀ (SetLike.coe '' S)

Tactic:
lift S to Finset (Closeds α) using hSf

Result:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
S : Finset (Closeds α)
hS : ∀ t ∈ ↑S, IsIrreducible ↑t
⊢ ↑(sSup ↑S) = ⋃₀ (SetLike.coe '' ↑S)

Proof state:
case intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Closeds α
⊢ ∃ S, S.Finite ∧ (∀ t ∈ S, IsClosed t) ∧ (∀ t ∈ S, IsIrreducible t) ∧ ↑s = ⋃₀ S

Tactic:
rcases NoetherianSpace.exists_finite_set_closeds_irreducible s with ⟨S, hSf, hS, rfl⟩

Result:
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
S : Set (Closeds α)
hSf : S.Finite
hS : ∀ t ∈ S, IsIrreducible ↑t
⊢ ∃ S_1, S_1.Finite ∧ (∀ t ∈ S_1, IsClosed t) ∧ (∀ t ∈ S_1, IsIrreducible t) ∧ ↑(sSup S) = ⋃₀ S_1

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Set α
hs : IsClosed s
⊢ ∃ S, S.Finite ∧ (∀ t ∈ S, IsClosed t) ∧ (∀ t ∈ S, IsIrreducible t) ∧ s = ⋃₀ S

Tactic:
lift s to Closeds α using hs

Result:
case intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Closeds α
⊢ ∃ S, S.Finite ∧ (∀ t ∈ S, IsClosed t) ∧ (∀ t ∈ S, IsIrreducible t) ∧ ↑s = ⋃₀ S
-- Mathlib/.lake/packages/batteries/Batteries/Classes/Order.lean
theorem gt_trans (h₁ : cmp x y = .gt) (h₂ : cmp y z = .gt) : cmp x z = .gt

Proof state:
cmp✝ : ?m.2927 → ?m.2927 → Ordering
inst✝¹ : TransCmp cmp✝
x✝ : Sort ?u.2925
cmp : x✝ → x✝ → Ordering
inst✝ : TransCmp cmp
x y z : x✝
h₁ : cmp x y = Ordering.gt
h₂ : cmp y z = Ordering.gt
⊢ cmp x z = Ordering.gt

Tactic:
rw [cmp_eq_gt] at h₁ h₂ ⊢

Result:
cmp✝ : ?m.2927 → ?m.2927 → Ordering
inst✝¹ : TransCmp cmp✝
x✝ : Sort ?u.2925
cmp : x✝ → x✝ → Ordering
inst✝ : TransCmp cmp
x y z : x✝
h₁ : cmp y x = Ordering.lt
h₂ : cmp z y = Ordering.lt
⊢ cmp z x = Ordering.lt

Proof state:
cmp✝ : ?m.2927 → ?m.2927 → Ordering
inst✝¹ : TransCmp cmp✝
x✝ : Sort ?u.2925
cmp : x✝ → x✝ → Ordering
inst✝ : TransCmp cmp
x y z : x✝
h₁ : cmp y x = Ordering.lt
h₂ : cmp z y = Ordering.lt
⊢ cmp z x = Ordering.lt

Tactic:
exact lt_trans h₂ h₁

Result:
no goals
-- Mathlib/LinearAlgebra/UnitaryGroup.lean
theorem toGL_mul (A B : unitaryGroup n α) : toGL (A * B) = toGL A * toGL B := Units.ext <| by
  simp only [coe_toGL, toLin'_mul]
  rfl

Proof state:
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A B : ↥(unitaryGroup n α)
⊢ ↑(toGL (A * B)) = ↑(toGL A * toGL B)

Tactic:
simp only [coe_toGL, toLin'_mul]

Result:
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A B : ↥(unitaryGroup n α)
⊢ toLin' A ∘ₗ toLin' B = ↑(toGL A * toGL B)

Proof state:
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A B : ↥(unitaryGroup n α)
⊢ toLin' A ∘ₗ toLin' B = ↑(toGL A * toGL B)

Tactic:
rfl

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/Bell.lean
theorem uniformBell_eq_div (m : ℕ) {n : ℕ} (hn : n ≠ 0) :
    uniformBell m n = (m * n) ! / (n ! ^ m * m !)

Proof state:
case H2
m n : ℕ
hn : n ≠ 0
⊢ (m * n)! = m.uniformBell n * (n ! ^ m * m !)

Tactic:
rw [← mul_assoc, ← uniformBell_mul_eq _ hn]

Result:
no goals

Proof state:
m n : ℕ
hn : n ≠ 0
⊢ (m * n)! / (n ! ^ m * m !) = m.uniformBell n

Tactic:
apply Nat.div_eq_of_eq_mul_left

Result:
case H1
m n : ℕ
hn : n ≠ 0
⊢ 0 < n ! ^ m * m !

case H2
m n : ℕ
hn : n ≠ 0
⊢ (m * n)! = m.uniformBell n * (n ! ^ m * m !)

Proof state:
m n : ℕ
hn : n ≠ 0
⊢ m.uniformBell n = (m * n)! / (n ! ^ m * m !)

Tactic:
rw [eq_comm]

Result:
m n : ℕ
hn : n ≠ 0
⊢ (m * n)! / (n ! ^ m * m !) = m.uniformBell n

Proof state:
case H1
m n : ℕ
hn : n ≠ 0
⊢ 0 < n ! ^ m * m !

Tactic:
exact Nat.mul_pos (Nat.pow_pos (Nat.factorial_pos n)) m.factorial_pos

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean
lemma periodic_exp : Periodic exp (2 * π) := fun z ↦ exp_eq_exp.2 ⟨1, by rw [Int.cast_one, one_mul]⟩

Proof state:
z : ℝ
⊢ z + 2 * π = z + ↑1 * (2 * π)

Tactic:
rw [Int.cast_one, one_mul]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Coeff.lean
theorem support_trinomial {k m n : ℕ} (hkm : k < m) (hmn : m < n) {x y z : R} (hx : x ≠ 0)
    (hy : y ≠ 0) (hz : z ≠ 0) :
    support (C x * X ^ k + C y * X ^ m + C z * X ^ n) = {k, m, n}

Proof state:
R : Type u
inst✝ : Semiring R
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : R
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ (C x * X ^ k + C y * X ^ m + C z * X ^ n).support = {k, m, n}

Tactic:
apply subset_antisymm (support_trinomial' k m n x y z)

Result:
R : Type u
inst✝ : Semiring R
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : R
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ {k, m, n} ⊆ (C x * X ^ k + C y * X ^ m + C z * X ^ n).support

Proof state:
R : Type u
inst✝ : Semiring R
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : R
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ {k, m, n} ⊆ (C x * X ^ k + C y * X ^ m + C z * X ^ n).support

Tactic:
simp_rw [insert_subset_iff, singleton_subset_iff, mem_support_iff, coeff_add, coeff_C_mul,
  coeff_X_pow_self, mul_one, coeff_X_pow, if_neg hkm.ne, if_neg hkm.ne', if_neg hmn.ne,
  if_neg hmn.ne', if_neg (hkm.trans hmn).ne, if_neg (hkm.trans hmn).ne', mul_zero, add_zero,
  zero_add, Ne, hx, hy, hz, not_false_eq_true, and_true]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Pairwise.lean
theorem pairwise_append {l₁ l₂ : List α} :
    (l₁ ++ l₂).Pairwise R ↔ l₁.Pairwise R ∧ l₂.Pairwise R ∧ ∀ a ∈ l₁, ∀ b ∈ l₂, R a b

Proof state:
α : Type u_1
R : α → α → Prop
l₁ l₂ : List α
⊢ Pairwise R (l₁ ++ l₂) ↔ Pairwise R l₁ ∧ Pairwise R l₂ ∧ ∀ (a : α), a ∈ l₁ → ∀ (b : α), b ∈ l₂ → R a b

Tactic:
induction l₁ <;> simp [*, or_imp, forall_and, and_assoc, and_left_comm]

Result:
no goals
-- Mathlib/Analysis/Normed/Affine/AddTorsor.lean
theorem dist_pointReflection_left (p q : P) :
    dist (Equiv.pointReflection p q) p = dist p q

Proof state:
V : Type u_1
P : Type u_2
inst✝² : SeminormedAddCommGroup V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
p q : P
⊢ dist ((Equiv.pointReflection p) q) p = dist p q

Tactic:
simp [dist_eq_norm_vsub V, Equiv.pointReflection_vsub_left (G := V)]

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Derivative.lean
theorem derivativeFun_one : derivativeFun (1 : R⟦X⟧) = 0

Proof state:
R : Type u_1
inst✝ : CommSemiring R
⊢ derivativeFun 1 = 0

Tactic:
rw [← map_one (C R), derivativeFun_C (1 : R)]

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/Basic.lean
theorem factors_pow_count_prod [DecidableEq α] {x : α} (hx : x ≠ 0) :
    (∏ p ∈ (factors x).toFinset, p ^ (factors x).count p) ~ᵤ x :=
  calc
  _ = prod (∑ a ∈ toFinset (factors x), count a (factors x) • {a})

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : DecidableEq α
x : α
hx : x ≠ 0
⊢ (∑ a ∈ (factors x).toFinset, count a (factors x) • {a}).prod = (factors x).prod

Tactic:
rw [toFinset_sum_count_nsmul_eq (factors x)]

Result:
no goals

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : DecidableEq α
x : α
hx : x ≠ 0
⊢ ∏ p ∈ (factors x).toFinset, p ^ count p (factors x) = (∑ a ∈ (factors x).toFinset, count a (factors x) • {a}).prod

Tactic:
simp only [prod_sum, prod_nsmul, prod_singleton]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Domain.lean
lemma eq_zero_of_dvd_of_degree_lt (h₁ : p ∣ q) (h₂ : degree q < degree p) : q = 0

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h₁ : p ∣ q
h₂ : q.degree < p.degree
⊢ q = 0

Tactic:
by_contra hc

Result:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h₁ : p ∣ q
h₂ : q.degree < p.degree
hc : ¬q = 0
⊢ False

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h₁ : p ∣ q
h₂ : q.degree < p.degree
hc : ¬q = 0
⊢ False

Tactic:
exact (lt_iff_not_ge _ _).mp h₂ (degree_le_of_dvd h₁ hc)

Result:
no goals
-- Mathlib/CategoryTheory/Localization/LocalizerMorphism.lean
lemma IsLocalizedEquivalence.mk' [CatCommSq Φ.functor L₁ L₂ G] [G.IsEquivalence] :
    Φ.IsLocalizedEquivalence where
  isEquivalence

Proof state:
C₁ : Type u₁
C₂ : Type u₂
D₁ : Type u₄
D₂ : Type u₅
inst✝⁷ : Category.{v₁, u₁} C₁
inst✝⁶ : Category.{v₂, u₂} C₂
inst✝⁵ : Category.{v₄, u₄} D₁
inst✝⁴ : Category.{v₅, u₅} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
inst✝³ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝² : L₂.IsLocalization W₂
G : D₁ ⥤ D₂
inst✝¹ : CatCommSq Φ.functor L₁ L₂ G
inst✝ : G.IsEquivalence
⊢ G.IsEquivalence

Tactic:
exact inferInstance

Result:
no goals

Proof state:
C₁ : Type u₁
C₂ : Type u₂
D₁ : Type u₄
D₂ : Type u₅
inst✝⁷ : Category.{v₁, u₁} C₁
inst✝⁶ : Category.{v₂, u₂} C₂
inst✝⁵ : Category.{v₄, u₄} D₁
inst✝⁴ : Category.{v₅, u₅} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
inst✝³ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝² : L₂.IsLocalization W₂
G : D₁ ⥤ D₂
inst✝¹ : CatCommSq Φ.functor L₁ L₂ G
inst✝ : G.IsEquivalence
⊢ (Φ.localizedFunctor W₁.Q W₂.Q).IsEquivalence

Tactic:
rw [Φ.isEquivalence_iff W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q) L₁ L₂ G]

Result:
C₁ : Type u₁
C₂ : Type u₂
D₁ : Type u₄
D₂ : Type u₅
inst✝⁷ : Category.{v₁, u₁} C₁
inst✝⁶ : Category.{v₂, u₂} C₂
inst✝⁵ : Category.{v₄, u₄} D₁
inst✝⁴ : Category.{v₅, u₅} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
inst✝³ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝² : L₂.IsLocalization W₂
G : D₁ ⥤ D₂
inst✝¹ : CatCommSq Φ.functor L₁ L₂ G
inst✝ : G.IsEquivalence
⊢ G.IsEquivalence
-- Mathlib/Algebra/Order/AbsoluteValue/Basic.lean
/-- Bound `abv (a - b)` from above -/
@[bound]
lemma sub_le_add (a b : R) : abv (a - b) ≤ abv a + abv b

Proof state:
R : Type u_3
S : Type u_4
inst✝² : OrderedCommRing S
inst✝¹ : Ring R
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
a b : R
⊢ abv (a - b) ≤ abv a + abv b

Tactic:
simpa only [← sub_eq_add_neg, AbsoluteValue.map_neg] using abv.add_le a (-b)

Result:
no goals
-- Mathlib/Data/Int/Interval.lean
theorem card_fintype_Ico : Fintype.card (Set.Ico a b) = (b - a).toNat

Proof state:
a b : ℤ
⊢ Fintype.card ↑(Set.Ico a b) = (b - a).toNat

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finset/Option.lean
theorem eraseNone_image_some [DecidableEq (Option α)] (s : Finset α) :
    eraseNone (s.image some) = s

Proof state:
α : Type u_1
inst✝ : DecidableEq (Option α)
s : Finset α
⊢ eraseNone (image some s) = s

Tactic:
simpa only [map_eq_image] using eraseNone_map_some s

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem ae_smul_measure {p : α → Prop} [SMul R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞]
    (h : ∀ᵐ x ∂μ, p x) (c : R) : ∀ᵐ x ∂c • μ, p x :=
  ae_iff.2 <| by rw [smul_apply, ae_iff.1 h, ← smul_one_smul ℝ≥0∞, smul_zero]

Proof state:
α : Type u_1
R : Type u_6
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
h : ∀ᵐ (x : α) ∂μ, p x
c : R
⊢ (c • μ) {a | ¬p a} = 0

Tactic:
rw [smul_apply, ae_iff.1 h, ← smul_one_smul ℝ≥0∞, smul_zero]

Result:
no goals
-- Mathlib/Order/Interval/Set/SuccPred.lean
lemma Ioc_pred_left_eq_Icc_of_not_isMin (ha : ¬ IsMin a) (b : α) : Ioc (pred a) b = Icc a b

Proof state:
case h
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a : α
ha : ¬IsMin a
b x : α
⊢ x ∈ Ioc (pred a) b ↔ x ∈ Icc a b

Tactic:
rw [mem_Ioc, mem_Icc, pred_lt_iff_of_not_isMin ha]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a : α
ha : ¬IsMin a
b : α
⊢ Ioc (pred a) b = Icc a b

Tactic:
ext x

Result:
case h
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a : α
ha : ¬IsMin a
b x : α
⊢ x ∈ Ioc (pred a) b ↔ x ∈ Icc a b
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem tdiv_sign : ∀ a b, a.tdiv (sign b) = a * sign b
  | _, succ _ => by simp [sign, Int.mul_one]
  | _, 0 => by simp [sign, Int.mul_zero]
  | _, -[_+1] => by simp [sign, Int.mul_neg, Int.mul_one]

Proof state:
x✝ : Int
a✝ : Nat
⊢ x✝.tdiv -[a✝+1].sign = x✝ * -[a✝+1].sign

Tactic:
simp [sign, Int.mul_neg, Int.mul_one]

Result:
no goals

Proof state:
x✝ : Int
n✝ : Nat
⊢ x✝.tdiv (↑n✝.succ).sign = x✝ * (↑n✝.succ).sign

Tactic:
simp [sign, Int.mul_one]

Result:
no goals

Proof state:
x✝ : Int
⊢ x✝.tdiv (sign 0) = x✝ * sign 0

Tactic:
simp [sign, Int.mul_zero]

Result:
no goals
-- Mathlib/Order/Interval/Set/SuccPred.lean
lemma Ioo_pred_left_eq_Ioc_of_not_isMin (ha : ¬ IsMin a) (b : α) : Ioo (pred a) b = Ico a b

Proof state:
case h
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a : α
ha : ¬IsMin a
b x : α
⊢ x ∈ Ioo (pred a) b ↔ x ∈ Ico a b

Tactic:
rw [mem_Ioo, mem_Ico, pred_lt_iff_of_not_isMin ha]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a : α
ha : ¬IsMin a
b : α
⊢ Ioo (pred a) b = Ico a b

Tactic:
ext x

Result:
case h
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a : α
ha : ¬IsMin a
b x : α
⊢ x ∈ Ioo (pred a) b ↔ x ∈ Ico a b
-- Mathlib/CategoryTheory/Subobject/Limits.lean
theorem factorThruImageSubobject_comp_self_assoc {W W' : C} (k : W ⟶ W') (k' : W' ⟶ X) (h) :
    (imageSubobject f).factorThru (k ≫ k' ≫ f) h = k ≫ k' ≫ factorThruImageSubobject f

Proof state:
case h
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : HasImage f
W W' : C
k : W ⟶ W'
k' : W' ⟶ X
h : (imageSubobject f).Factors (k ≫ k' ≫ f)
⊢ (imageSubobject f).factorThru (k ≫ k' ≫ f) h ≫ (imageSubobject f).arrow =
    (k ≫ k' ≫ factorThruImageSubobject f) ≫ (imageSubobject f).arrow

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : HasImage f
W W' : C
k : W ⟶ W'
k' : W' ⟶ X
h : (imageSubobject f).Factors (k ≫ k' ≫ f)
⊢ (imageSubobject f).factorThru (k ≫ k' ≫ f) h = k ≫ k' ≫ factorThruImageSubobject f

Tactic:
ext

Result:
case h
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : HasImage f
W W' : C
k : W ⟶ W'
k' : W' ⟶ X
h : (imageSubobject f).Factors (k ≫ k' ≫ f)
⊢ (imageSubobject f).factorThru (k ≫ k' ≫ f) h ≫ (imageSubobject f).arrow =
    (k ≫ k' ≫ factorThruImageSubobject f) ≫ (imageSubobject f).arrow
-- Mathlib/Topology/PartialHomeomorph.lean
theorem eventually_ne_nhdsWithin {x} (hx : x ∈ e.source) :
    ∀ᶠ x' in 𝓝[≠] x, e x' ≠ e x :=
  eventually_nhdsWithin_iff.2 <|
    (e.eventually_left_inverse hx).mono fun x' hx' =>
      mt fun h => by rw [mem_singleton_iff, ← e.left_inv hx, ← h, hx']

Proof state:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
x : X
hx : x ∈ e.source
x' : X
hx' : ↑e.symm (↑e x') = x'
h : ↑e x' = ↑e x
⊢ x' ∈ {x}

Tactic:
rw [mem_singleton_iff, ← e.left_inv hx, ← h, hx']

Result:
no goals