harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem moebius_eq_or (n : ℕ) : μ n = 0 ∨ μ n = 1 ∨ μ n = -1

Proof state:
case neg.h
n : ℕ
h✝ : ¬Squarefree n
⊢ 0 = 0

Tactic:
rfl

Result:
no goals

Proof state:
n : ℕ
⊢ μ n = 0 ∨ μ n = 1 ∨ μ n = -1

Tactic:
simp only [moebius, coe_mk]

Result:
n : ℕ
⊢ (if Squarefree n then (-1) ^ Ω n else 0) = 0 ∨
    (if Squarefree n then (-1) ^ Ω n else 0) = 1 ∨ (if Squarefree n then (-1) ^ Ω n else 0) = -1

Proof state:
case pos.h
n : ℕ
h✝ : Squarefree n
⊢ (-1) ^ Ω n = 1 ∨ (-1) ^ Ω n = -1

Tactic:
exact neg_one_pow_eq_or ..

Result:
no goals

Proof state:
n : ℕ
⊢ (if Squarefree n then (-1) ^ Ω n else 0) = 0 ∨
    (if Squarefree n then (-1) ^ Ω n else 0) = 1 ∨ (if Squarefree n then (-1) ^ Ω n else 0) = -1

Tactic:
split_ifs

Result:
case pos
n : ℕ
h✝ : Squarefree n
⊢ (-1) ^ Ω n = 0 ∨ (-1) ^ Ω n = 1 ∨ (-1) ^ Ω n = -1

case neg
n : ℕ
h✝ : ¬Squarefree n
⊢ 0 = 0 ∨ 0 = 1 ∨ False

Proof state:
case neg
n : ℕ
h✝ : ¬Squarefree n
⊢ 0 = 0 ∨ 0 = 1 ∨ False

Tactic:
left

Result:
case neg.h
n : ℕ
h✝ : ¬Squarefree n
⊢ 0 = 0

Proof state:
case pos
n : ℕ
h✝ : Squarefree n
⊢ (-1) ^ Ω n = 0 ∨ (-1) ^ Ω n = 1 ∨ (-1) ^ Ω n = -1

Tactic:
right

Result:
case pos.h
n : ℕ
h✝ : Squarefree n
⊢ (-1) ^ Ω n = 1 ∨ (-1) ^ Ω n = -1
-- Mathlib/Combinatorics/Enumerative/IncidenceAlgebra.lean
@[simp]
lemma zeta_prod_zeta [DecidableRel (α := α) (· ≤ ·)] [DecidableRel (α := β) (· ≤ ·)] :
    (zeta 𝕜).prod (zeta 𝕜) = (zeta 𝕜 : IncidenceAlgebra 𝕜 (α × β))

Proof state:
case h
𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst✝⁴ : Ring 𝕜
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
x y : α × β
hxy : x ≤ y
⊢ ((zeta 𝕜).prod (zeta 𝕜)) x y = (zeta 𝕜) x y

Tactic:
simp [hxy, hxy.1, hxy.2]

Result:
no goals

Proof state:
𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst✝⁴ : Ring 𝕜
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
⊢ (zeta 𝕜).prod (zeta 𝕜) = zeta 𝕜

Tactic:
ext x y hxy

Result:
case h
𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst✝⁴ : Ring 𝕜
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
x y : α × β
hxy : x ≤ y
⊢ ((zeta 𝕜).prod (zeta 𝕜)) x y = (zeta 𝕜) x y
-- Mathlib/Analysis/SpecialFunctions/BinaryEntropy.lean
@[fun_prop] lemma differentiableAt_qaryEntropy (hp₀ : p ≠ 0) (hp₁ : p ≠ 1) :
    DifferentiableAt ℝ (qaryEntropy q) p

Proof state:
q : ℕ
p : ℝ
hp₀ : p ≠ 0
hp₁ : p ≠ 1
⊢ DifferentiableAt ℝ (fun p => p * log ↑(↑q - 1) + binEntropy p) p

Tactic:
fun_prop (disch := assumption)

Result:
no goals

Proof state:
q : ℕ
p : ℝ
hp₀ : p ≠ 0
hp₁ : p ≠ 1
⊢ DifferentiableAt ℝ (qaryEntropy q) p

Tactic:
unfold qaryEntropy

Result:
q : ℕ
p : ℝ
hp₀ : p ≠ 0
hp₁ : p ≠ 1
⊢ DifferentiableAt ℝ (fun p => p * log ↑(↑q - 1) + binEntropy p) p

Proof state:
case funProp.discharger
q : ℕ
p : ℝ
hp₀ : p ≠ 0
hp₁ : p ≠ 1
⊢ p ≠ 1

Tactic:
assumption

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem eq_zero_of_eq_zero (h : (0 : R) = (1 : R)) (p : R[X]) : p = 0

Proof state:
R : Type u
inst✝ : Semiring R
h : 0 = 1
p : R[X]
⊢ p = 0

Tactic:
rw [← one_smul R p, ← h, zero_smul]

Result:
no goals
-- Mathlib/RingTheory/TensorProduct/Basic.lean
theorem lift_comp_includeRight (f : A →ₐ[S] C) (g : B →ₐ[R] C) (hfg : ∀ x y, Commute (f x) (g y)) :
    ((lift f g hfg).restrictScalars R).comp includeRight = g :=
  AlgHom.ext <| by simp

Proof state:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
C : Type uC
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
inst✝⁹ : Semiring A
inst✝⁸ : Algebra R A
inst✝⁷ : Algebra S A
inst✝⁶ : IsScalarTower R S A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : Semiring C
inst✝² : Algebra S C
inst✝¹ : Algebra R C
inst✝ : IsScalarTower R S C
f : A →ₐ[S] C
g : B →ₐ[R] C
hfg : ∀ (x : A) (y : B), Commute (f x) (g y)
⊢ ∀ (x : B), ((AlgHom.restrictScalars R (lift f g hfg)).comp includeRight) x = g x

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Set/Subsingleton.lean
theorem not_nontrivial_singleton {x} : ¬({x} : Set α).Nontrivial := fun H => by
  rw [nontrivial_iff_exists_ne (mem_singleton x)] at H
  let ⟨y, hy, hya⟩ := H
  exact hya (mem_singleton_iff.1 hy)

Proof state:
α : Type u
x : α
H : {x}.Nontrivial
⊢ False

Tactic:
rw [nontrivial_iff_exists_ne (mem_singleton x)] at H

Result:
α : Type u
x : α
H : ∃ y ∈ {x}, y ≠ x
⊢ False

Proof state:
α : Type u
x : α
H : ∃ y ∈ {x}, y ≠ x
⊢ False

Tactic:
let ⟨y, hy, hya⟩ := H

Result:
α : Type u
x : α
H : ∃ y ∈ {x}, y ≠ x
y : α
hy : y ∈ {x}
hya : y ≠ x
⊢ False

Proof state:
α : Type u
x : α
H : ∃ y ∈ {x}, y ≠ x
y : α
hy : y ∈ {x}
hya : y ≠ x
⊢ False

Tactic:
exact hya (mem_singleton_iff.1 hy)

Result:
no goals
-- Mathlib/Logic/Equiv/Basic.lean
theorem swap_apply_of_ne_of_ne {a b x : α} : x ≠ a → x ≠ b → swap a b x = x

Proof state:
α : Sort u_1
inst✝ : DecidableEq α
a b x : α
⊢ x ≠ a → x ≠ b → (swap a b) x = x

Tactic:
simp +contextual [swap_apply_def]

Result:
no goals
-- Mathlib/Data/Nat/ModEq.lean
theorem add_left_cancel (h₁ : a ≡ b [MOD n]) (h₂ : a + c ≡ b + d [MOD n]) :
    c ≡ d [MOD n]

Proof state:
n a b c d : ℕ
h₁ : ↑n ∣ ↑b - ↑a
h₂ : ↑n ∣ ↑b - ↑a + (↑d - ↑c)
⊢ ↑n ∣ ↑d - ↑c

Tactic:
convert Int.dvd_sub h₂ h₁ using 1

Result:
case h.e'_4
n a b c d : ℕ
h₁ : ↑n ∣ ↑b - ↑a
h₂ : ↑n ∣ ↑b - ↑a + (↑d - ↑c)
⊢ ↑d - ↑c = ↑b - ↑a + (↑d - ↑c) - (↑b - ↑a)

Proof state:
n a b c d : ℕ
h₁ : a ≡ b [MOD n]
h₂ : a + c ≡ b + d [MOD n]
⊢ c ≡ d [MOD n]

Tactic:
simp only [modEq_iff_dvd, Int.ofNat_add] at *

Result:
n a b c d : ℕ
h₁ : ↑n ∣ ↑b - ↑a
h₂ : ↑n ∣ ↑b + ↑d - (↑a + ↑c)
⊢ ↑n ∣ ↑d - ↑c

Proof state:
n a b c d : ℕ
h₁ : ↑n ∣ ↑b - ↑a
h₂ : ↑n ∣ ↑b + ↑d - (↑a + ↑c)
⊢ ↑n ∣ ↑d - ↑c

Tactic:
rw [add_sub_add_comm] at h₂

Result:
n a b c d : ℕ
h₁ : ↑n ∣ ↑b - ↑a
h₂ : ↑n ∣ ↑b - ↑a + (↑d - ↑c)
⊢ ↑n ∣ ↑d - ↑c

Proof state:
case h.e'_4
n a b c d : ℕ
h₁ : ↑n ∣ ↑b - ↑a
h₂ : ↑n ∣ ↑b - ↑a + (↑d - ↑c)
⊢ ↑d - ↑c = ↑b - ↑a + (↑d - ↑c) - (↑b - ↑a)

Tactic:
rw [add_sub_cancel_left]

Result:
no goals
-- Mathlib/Data/Sum/Order.lean
theorem noMaxOrder_iff [LT α] [LT β] : NoMaxOrder (α ⊕ β) ↔ NoMaxOrder α ∧ NoMaxOrder β :=
  ⟨fun _ =>
    ⟨⟨fun a => by
        obtain ⟨b | b, h⟩ := exists_gt (inl a : α ⊕ β)
        · exact ⟨b, inl_lt_inl_iff.1 h⟩
        · exact (not_inl_lt_inr h).elim⟩,
      ⟨fun a => by
        obtain ⟨b | b, h⟩ := exists_gt (inr a : α ⊕ β)
        · exact (not_inr_lt_inl h).elim
        · exact ⟨b, inr_lt_inr_iff.1 h⟩⟩⟩,
    fun h => @Sum.noMaxOrder _ _ _ _ h.1 h.2⟩

Proof state:
case intro.inr
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMaxOrder (α ⊕ β)
a b : β
h : inr a < inr b
⊢ ∃ b, a < b

Tactic:
exact ⟨b, inr_lt_inr_iff.1 h⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMaxOrder (α ⊕ β)
a : α
⊢ ∃ b, a < b

Tactic:
obtain ⟨b | b, h⟩ := exists_gt (inl a : α ⊕ β)

Result:
case intro.inl
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMaxOrder (α ⊕ β)
a b : α
h : inl a < inl b
⊢ ∃ b, a < b

case intro.inr
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMaxOrder (α ⊕ β)
a : α
b : β
h : inl a < inr b
⊢ ∃ b, a < b

Proof state:
case intro.inl
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMaxOrder (α ⊕ β)
a b : α
h : inl a < inl b
⊢ ∃ b, a < b

Tactic:
exact ⟨b, inl_lt_inl_iff.1 h⟩

Result:
no goals

Proof state:
case intro.inr
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMaxOrder (α ⊕ β)
a : α
b : β
h : inl a < inr b
⊢ ∃ b, a < b

Tactic:
exact (not_inl_lt_inr h).elim

Result:
no goals

Proof state:
case intro.inl
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMaxOrder (α ⊕ β)
a : β
b : α
h : inr a < inl b
⊢ ∃ b, a < b

Tactic:
exact (not_inr_lt_inl h).elim

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMaxOrder (α ⊕ β)
a : β
⊢ ∃ b, a < b

Tactic:
obtain ⟨b | b, h⟩ := exists_gt (inr a : α ⊕ β)

Result:
case intro.inl
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMaxOrder (α ⊕ β)
a : β
b : α
h : inr a < inl b
⊢ ∃ b, a < b

case intro.inr
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMaxOrder (α ⊕ β)
a b : β
h : inr a < inr b
⊢ ∃ b, a < b
-- Mathlib/Algebra/Homology/DerivedCategory/Ext/ExtClass.lean
private lemma hasSmallLocalizedHom_S'_X₃_K :
    HasSmallLocalizedHom.{w} W (S').X₃ K

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
⊢ HasSmallLocalizedHom W ((CochainComplex.singleFunctor C 0).obj S.X₃) ((CochainComplex.singleFunctor C 0).obj S.X₃)

Tactic:
apply Localization.hasSmallLocalizedHom_of_hasSmallLocalizedShiftedHom₀ (M := ℤ)

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
⊢ HasSmallLocalizedHom W (S.map (CochainComplex.singleFunctor C 0)).X₃
    (CochainComplex.mappingCone (S.map (CochainComplex.singleFunctor C 0)).f)

Tactic:
rw [Localization.hasSmallLocalizedHom_iff_target W (S').X₃ qis hqis]

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
⊢ HasSmallLocalizedHom W (S.map (CochainComplex.singleFunctor C 0)).X₃ (S.map (CochainComplex.singleFunctor C 0)).X₃

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
⊢ HasSmallLocalizedHom W (S.map (CochainComplex.singleFunctor C 0)).X₃ (S.map (CochainComplex.singleFunctor C 0)).X₃

Tactic:
dsimp

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
⊢ HasSmallLocalizedHom W ((CochainComplex.singleFunctor C 0).obj S.X₃) ((CochainComplex.singleFunctor C 0).obj S.X₃)
-- Mathlib/Analysis/Normed/Algebra/MatrixExponential.lean
theorem exp_zsmul (z : ℤ) (A : Matrix m m 𝔸) : exp 𝕂 (z • A) = exp 𝕂 A ^ z

Proof state:
case intro.inr
𝕂 : Type u_1
m : Type u_2
𝔸 : Type u_5
inst✝⁵ : RCLike 𝕂
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : NormedCommRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
A : Matrix m m 𝔸
n : ℕ
⊢ exp 𝕂 (-↑n • A) = exp 𝕂 A ^ (-↑n)

Tactic:
have : IsUnit (exp 𝕂 A).det := (Matrix.isUnit_iff_isUnit_det _).mp (isUnit_exp _ _)

Result:
case intro.inr
𝕂 : Type u_1
m : Type u_2
𝔸 : Type u_5
inst✝⁵ : RCLike 𝕂
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : NormedCommRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
A : Matrix m m 𝔸
n : ℕ
this : IsUnit (exp 𝕂 A).det
⊢ exp 𝕂 (-↑n • A) = exp 𝕂 A ^ (-↑n)

Proof state:
case intro.inr
𝕂 : Type u_1
m : Type u_2
𝔸 : Type u_5
inst✝⁵ : RCLike 𝕂
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : NormedCommRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
A : Matrix m m 𝔸
n : ℕ
this : IsUnit (exp 𝕂 A).det
⊢ exp 𝕂 (-↑n • A) = exp 𝕂 A ^ (-↑n)

Tactic:
rw [Matrix.zpow_neg this, zpow_natCast, neg_smul, exp_neg, natCast_zsmul, exp_nsmul]

Result:
no goals

Proof state:
case intro.inl
𝕂 : Type u_1
m : Type u_2
𝔸 : Type u_5
inst✝⁵ : RCLike 𝕂
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : NormedCommRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
A : Matrix m m 𝔸
n : ℕ
⊢ exp 𝕂 (↑n • A) = exp 𝕂 A ^ ↑n

Tactic:
rw [zpow_natCast, natCast_zsmul, exp_nsmul]

Result:
no goals

Proof state:
𝕂 : Type u_1
m : Type u_2
𝔸 : Type u_5
inst✝⁵ : RCLike 𝕂
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : NormedCommRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
z : ℤ
A : Matrix m m 𝔸
⊢ exp 𝕂 (z • A) = exp 𝕂 A ^ z

Tactic:
obtain ⟨n, rfl | rfl⟩ := z.eq_nat_or_neg

Result:
case intro.inl
𝕂 : Type u_1
m : Type u_2
𝔸 : Type u_5
inst✝⁵ : RCLike 𝕂
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : NormedCommRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
A : Matrix m m 𝔸
n : ℕ
⊢ exp 𝕂 (↑n • A) = exp 𝕂 A ^ ↑n

case intro.inr
𝕂 : Type u_1
m : Type u_2
𝔸 : Type u_5
inst✝⁵ : RCLike 𝕂
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : NormedCommRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
A : Matrix m m 𝔸
n : ℕ
⊢ exp 𝕂 (-↑n • A) = exp 𝕂 A ^ (-↑n)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean
theorem eval_zeroExtend : eval assign (.zeroExtend v expr) = BitVec.zeroExtend v (eval assign expr)

Proof state:
assign : Assignment
v a✝ : Nat
expr : BVExpr a✝
⊢ eval assign (zeroExtend v expr) = BitVec.zeroExtend v (eval assign expr)

Tactic:
rfl

Result:
no goals
-- Mathlib/RepresentationTheory/Rep.lean
theorem to_Module_monoidAlgebra_map_aux {k G : Type*} [CommRing k] [Monoid G] (V W : Type*)
    [AddCommGroup V] [AddCommGroup W] [Module k V] [Module k W] (ρ : G →* V →ₗ[k] V)
    (σ : G →* W →ₗ[k] W) (f : V →ₗ[k] W) (w : ∀ g : G, f.comp (ρ g) = (σ g).comp f)
    (r : MonoidAlgebra k G) (x : V) :
    f ((((MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ) r) x) =
      (((MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) r) (f x)

Proof state:
case hsmul
k : Type u_1
G : Type u_2
inst✝⁵ : CommRing k
inst✝⁴ : Monoid G
V : Type u_3
W : Type u_4
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup W
inst✝¹ : Module k V
inst✝ : Module k W
ρ : G →* V →ₗ[k] V
σ : G →* W →ₗ[k] W
f : V →ₗ[k] W
w : ∀ (g : G), f ∘ₗ ρ g = σ g ∘ₗ f
r : MonoidAlgebra k G
x : V
⊢ ∀ (r : k) (f_1 : MonoidAlgebra k G),
    f ((((MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ) f_1) x) = (((MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) f_1) (f x) →
      f ((((MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ) (r • f_1)) x) =
        (((MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) (r • f_1)) (f x)

Tactic:
intro r g w

Result:
case hsmul
k : Type u_1
G : Type u_2
inst✝⁵ : CommRing k
inst✝⁴ : Monoid G
V : Type u_3
W : Type u_4
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup W
inst✝¹ : Module k V
inst✝ : Module k W
ρ : G →* V →ₗ[k] V
σ : G →* W →ₗ[k] W
f : V →ₗ[k] W
w✝ : ∀ (g : G), f ∘ₗ ρ g = σ g ∘ₗ f
r✝ : MonoidAlgebra k G
x : V
r : k
g : MonoidAlgebra k G
w : f ((((MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ) g) x) = (((MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) g) (f x)
⊢ f ((((MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ) (r • g)) x) = (((MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) (r • g)) (f x)
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Icc_ssubset_Icc_left (hI : a₂ ≤ b₂) (ha : a₂ < a₁) (hb : b₁ ≤ b₂) :
    Icc a₁ b₁ ⊂ Icc a₂ b₂

Proof state:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
hI : a₂ ≤ b₂
ha : a₂ < a₁
hb : b₁ ≤ b₂
⊢ Set.Icc a₁ b₁ ⊂ Set.Icc a₂ b₂

Tactic:
exact Set.Icc_ssubset_Icc_left hI ha hb

Result:
no goals

Proof state:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
hI : a₂ ≤ b₂
ha : a₂ < a₁
hb : b₁ ≤ b₂
⊢ Icc a₁ b₁ ⊂ Icc a₂ b₂

Tactic:
rw [← coe_ssubset, coe_Icc, coe_Icc]

Result:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
hI : a₂ ≤ b₂
ha : a₂ < a₁
hb : b₁ ≤ b₂
⊢ Set.Icc a₁ b₁ ⊂ Set.Icc a₂ b₂
-- Mathlib/NumberTheory/Cyclotomic/Basic.lean
theorem splits_cyclotomic [IsCyclotomicExtension S K L] (hS : n ∈ S) :
    Splits (algebraMap K L) (cyclotomic n K)

Proof state:
n : ℕ+
S : Set ℕ+
K : Type w
L : Type z
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension S K L
hS : n ∈ S
⊢ Splits (algebraMap K L) (cyclotomic (↑n) K)

Tactic:
refine splits_of_splits_of_dvd _ (X_pow_sub_C_ne_zero n.pos _) (splits_X_pow_sub_one K L hS) ?_

Result:
n : ℕ+
S : Set ℕ+
K : Type w
L : Type z
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension S K L
hS : n ∈ S
⊢ cyclotomic (↑n) K ∣ X ^ ↑n - C 1

Proof state:
n : ℕ+
S : Set ℕ+
K : Type w
L : Type z
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension S K L
hS : n ∈ S
⊢ cyclotomic (↑n) K ∣ X ^ ↑n - C 1

Tactic:
use ∏ i ∈ (n : ℕ).properDivisors, Polynomial.cyclotomic i K

Result:
case h
n : ℕ+
S : Set ℕ+
K : Type w
L : Type z
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension S K L
hS : n ∈ S
⊢ X ^ ↑n - C 1 = cyclotomic (↑n) K * ∏ i ∈ (↑n).properDivisors, cyclotomic i K

Proof state:
case h
n : ℕ+
S : Set ℕ+
K : Type w
L : Type z
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension S K L
hS : n ∈ S
⊢ X ^ ↑n - C 1 = cyclotomic (↑n) K * ∏ i ∈ (↑n).properDivisors, cyclotomic i K

Tactic:
rw [(eq_cyclotomic_iff n.pos _).1 rfl, RingHom.map_one]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Option.lean
theorem prod_eraseNone (f : α → M) (s : Finset (Option α)) :
    ∏ x ∈ eraseNone s, f x = ∏ x ∈ s, Option.elim' 1 f x

Proof state:
α : Type u_1
M : Type u_2
inst✝ : CommMonoid M
f : α → M
s : Finset (Option α)
⊢ ∏ x ∈ eraseNone s, f x = ∏ x ∈ s, Option.elim' 1 f x

Tactic:
calc
∏ x ∈ eraseNone s, f x = ∏ x ∈ (eraseNone s).map Embedding.some, Option.elim' 1 f x :=
(prod_map (eraseNone s) Embedding.some <| Option.elim' 1 f).symm
_ = ∏ x ∈ s.erase none, Option.elim' 1 f x := by rw [map_some_eraseNone]
_ = ∏ x ∈ s, Option.elim' 1 f x := prod_erase _ rfl

Result:
no goals

Proof state:
α : Type u_1
M : Type u_2
inst✝ : CommMonoid M
f : α → M
s : Finset (Option α)
⊢ ∏ x ∈ map Embedding.some (eraseNone s), Option.elim' 1 f x = ∏ x ∈ s.erase none, Option.elim' 1 f x

Tactic:
rw [map_some_eraseNone]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_2
inst✝ : CommMonoid M
f : α → M
s : Finset (Option α)
⊢ ∏ x ∈ eraseNone s, f x = ∏ x ∈ s, Option.elim' 1 f x

Tactic:
classical calc
    ∏ x ∈ eraseNone s, f x = ∏ x ∈ (eraseNone s).map Embedding.some, Option.elim' 1 f x :=
      (prod_map (eraseNone s) Embedding.some <| Option.elim' 1 f).symm
    _ = ∏ x ∈ s.erase none, Option.elim' 1 f x := by rw [map_some_eraseNone]
    _ = ∏ x ∈ s, Option.elim' 1 f x := prod_erase _ rfl

Result:
no goals
-- Mathlib/Algebra/Lie/Subalgebra.lean
theorem Submodule.exists_lieSubalgebra_coe_eq_iff (p : Submodule R L) :
    (∃ K : LieSubalgebra R L, ↑K = p) ↔ ∀ x y : L, x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p

Proof state:
case mpr
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
p : Submodule R L
h : ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p
⊢ ∃ K, K.toSubmodule = p

Tactic:
use { p with lie_mem' := h _ _ }

Result:
no goals

Proof state:
case mpr
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
p : Submodule R L
⊢ (∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p) → ∃ K, K.toSubmodule = p

Tactic:
intro h

Result:
case mpr
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
p : Submodule R L
h : ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p
⊢ ∃ K, K.toSubmodule = p

Proof state:
case mp
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
p : Submodule R L
⊢ (∃ K, K.toSubmodule = p) → ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p

Tactic:
rintro ⟨K, rfl⟩ _ _

Result:
case mp.intro
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K : LieSubalgebra R L
x✝ y✝ : L
⊢ x✝ ∈ K.toSubmodule → y✝ ∈ K.toSubmodule → ⁅x✝, y✝⁆ ∈ K.toSubmodule

Proof state:
case mp.intro
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K : LieSubalgebra R L
x✝ y✝ : L
⊢ x✝ ∈ K.toSubmodule → y✝ ∈ K.toSubmodule → ⁅x✝, y✝⁆ ∈ K.toSubmodule

Tactic:
exact K.lie_mem'

Result:
no goals

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
p : Submodule R L
⊢ (∃ K, K.toSubmodule = p) ↔ ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p

Tactic:
constructor

Result:
case mp
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
p : Submodule R L
⊢ (∃ K, K.toSubmodule = p) → ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p

case mpr
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
p : Submodule R L
⊢ (∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p) → ∃ K, K.toSubmodule = p
-- Mathlib/AlgebraicGeometry/AffineScheme.lean
theorem range_fromSpec :
    Set.range hU.fromSpec.base = (U : Set X)

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Set.range ⇑(ConcreteCategory.hom (hU.isoSpec.inv ≫ U.ι).base) = ↑U

Tactic:
dsimp [IsAffineOpen.isoSpec_inv]

Result:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Set.range
      (⇑(TopCat.Hom.hom U.ι.base) ∘
        ⇑(TopCat.Hom.hom (↑U).isoSpec.inv.base) ∘ ⇑(TopCat.Hom.hom (Spec.map (X.presheaf.map (eqToHom ⋯).op)).base)) =
    ↑U

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Epi ((Spec.map (X.presheaf.map (eqToHom ⋯).op)).base ≫ (↑U).isoSpec.inv.base)

Tactic:
infer_instance

Result:
no goals

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Set.range
      (⇑(TopCat.Hom.hom U.ι.base) ∘
        ⇑(TopCat.Hom.hom (↑U).isoSpec.inv.base) ∘ ⇑(TopCat.Hom.hom (Spec.map (X.presheaf.map (eqToHom ⋯).op)).base)) =
    ↑U

Tactic:
rw [Set.range_comp, Set.range_eq_univ.mpr, Set.image_univ]

Result:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Set.range ⇑(TopCat.Hom.hom U.ι.base) = ↑U

X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Function.Surjective
    (⇑(TopCat.Hom.hom (↑U).isoSpec.inv.base) ∘ ⇑(TopCat.Hom.hom (Spec.map (X.presheaf.map (eqToHom ⋯).op)).base))

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Function.Surjective
    (⇑(TopCat.Hom.hom (↑U).isoSpec.inv.base) ∘ ⇑(TopCat.Hom.hom (Spec.map (X.presheaf.map (eqToHom ⋯).op)).base))

Tactic:
rw [← TopCat.coe_comp, ← TopCat.epi_iff_surjective]

Result:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Epi ((Spec.map (X.presheaf.map (eqToHom ⋯).op)).base ≫ (↑U).isoSpec.inv.base)

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Set.range ⇑(TopCat.Hom.hom U.ι.base) = ↑U

Tactic:
exact Subtype.range_coe

Result:
no goals

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Set.range ⇑(ConcreteCategory.hom hU.fromSpec.base) = ↑U

Tactic:
delta IsAffineOpen.fromSpec

Result:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Set.range ⇑(ConcreteCategory.hom (hU.isoSpec.inv ≫ U.ι).base) = ↑U
-- Mathlib/Algebra/Homology/ShortComplex/PreservesHomology.lean
/-- If a short complex `S` is such that `S.f = 0` and that the kernel of `S.g` is preserved
by a functor `F`, then `F` preserves the left homology of `S`. -/
lemma preservesLeftHomology_of_zero_f (hf : S.f = 0)
    [PreservesLimit (parallelPair S.g 0) F] :
    F.PreservesLeftHomologyOf S := ⟨fun h =>
  { g

Proof state:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_3, u_1} C
inst✝⁴ : Category.{u_4, u_2} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
S : ShortComplex C
hf : S.f = 0
inst✝ : PreservesLimit (parallelPair S.g 0) F
h : S.LeftHomologyData
⊢ PreservesLimit (parallelPair S.g 0) F

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_3, u_1} C
inst✝⁴ : Category.{u_4, u_2} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
S : ShortComplex C
hf : S.f = 0
inst✝ : PreservesLimit (parallelPair S.g 0) F
h : S.LeftHomologyData
⊢ h.f' = 0

Tactic:
rw [← cancel_mono h.i, h.f'_i, zero_comp, hf]

Result:
no goals
-- Mathlib/Data/List/SplitOn.lean
theorem splitOnP_cons (x : α) (xs : List α) :
    (x :: xs).splitOnP p =
      if p x then [] :: xs.splitOnP p else (xs.splitOnP p).modifyHead (cons x)

Proof state:
α : Type u_1
p : α → Bool
x : α
xs : List α
⊢ (if p x = true then [].reverse :: splitOnP.go p xs [] else splitOnP.go p xs [x]) =
    if p x = true then [] :: splitOnP p xs else modifyHead (cons x) (splitOnP p xs)

Tactic:
split <;> [rfl; simp [splitOnP.go_acc]]

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
x : α
xs : List α
⊢ splitOnP p (x :: xs) = if p x = true then [] :: splitOnP p xs else modifyHead (cons x) (splitOnP p xs)

Tactic:
rw [splitOnP, splitOnP.go]

Result:
α : Type u_1
p : α → Bool
x : α
xs : List α
⊢ (if p x = true then [].reverse :: splitOnP.go p xs [] else splitOnP.go p xs [x]) =
    if p x = true then [] :: splitOnP p xs else modifyHead (cons x) (splitOnP p xs)