harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Connected/Basic.lean
theorem IsPreconnected.union' {s t : Set α} (H : (s ∩ t).Nonempty) (hs : IsPreconnected s)
    (ht : IsPreconnected t) : IsPreconnected (s ∪ t)

Proof state:
α : Type u
inst✝ : TopologicalSpace α
s t : Set α
H : (s ∩ t).Nonempty
hs : IsPreconnected s
ht : IsPreconnected t
⊢ IsPreconnected (s ∪ t)

Tactic:
rcases H with ⟨x, hxs, hxt⟩

Result:
case intro.intro
α : Type u
inst✝ : TopologicalSpace α
s t : Set α
hs : IsPreconnected s
ht : IsPreconnected t
x : α
hxs : x ∈ s
hxt : x ∈ t
⊢ IsPreconnected (s ∪ t)

Proof state:
case intro.intro
α : Type u
inst✝ : TopologicalSpace α
s t : Set α
hs : IsPreconnected s
ht : IsPreconnected t
x : α
hxs : x ∈ s
hxt : x ∈ t
⊢ IsPreconnected (s ∪ t)

Tactic:
exact hs.union x hxs hxt ht

Result:
no goals
-- Mathlib/GroupTheory/Exponent.lean
theorem MonoidHom.exponent_dvd {F M₁ M₂ : Type*} [Monoid M₁] [Monoid M₂]
    [FunLike F M₁ M₂] [MonoidHomClass F M₁ M₂]
    {f : F} (hf : Function.Surjective f) : exponent M₂ ∣ exponent M₁

Proof state:
F : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst✝³ : Monoid M₁
inst✝² : Monoid M₂
inst✝¹ : FunLike F M₁ M₂
inst✝ : MonoidHomClass F M₁ M₂
f : F
hf : Function.Surjective ⇑f
⊢ exponent M₂ ∣ exponent M₁

Tactic:
refine Monoid.exponent_dvd_of_forall_pow_eq_one fun m₂ ↦ ?_

Result:
F : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst✝³ : Monoid M₁
inst✝² : Monoid M₂
inst✝¹ : FunLike F M₁ M₂
inst✝ : MonoidHomClass F M₁ M₂
f : F
hf : Function.Surjective ⇑f
m₂ : M₂
⊢ m₂ ^ exponent M₁ = 1

Proof state:
F : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst✝³ : Monoid M₁
inst✝² : Monoid M₂
inst✝¹ : FunLike F M₁ M₂
inst✝ : MonoidHomClass F M₁ M₂
f : F
hf : Function.Surjective ⇑f
m₂ : M₂
⊢ m₂ ^ exponent M₁ = 1

Tactic:
obtain ⟨m₁, rfl⟩ := hf m₂

Result:
case intro
F : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst✝³ : Monoid M₁
inst✝² : Monoid M₂
inst✝¹ : FunLike F M₁ M₂
inst✝ : MonoidHomClass F M₁ M₂
f : F
hf : Function.Surjective ⇑f
m₁ : M₁
⊢ f m₁ ^ exponent M₁ = 1

Proof state:
case intro
F : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst✝³ : Monoid M₁
inst✝² : Monoid M₂
inst✝¹ : FunLike F M₁ M₂
inst✝ : MonoidHomClass F M₁ M₂
f : F
hf : Function.Surjective ⇑f
m₁ : M₁
⊢ f m₁ ^ exponent M₁ = 1

Tactic:
rw [← map_pow, pow_exponent_eq_one, map_one]

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/Exact.lean
private lemma top_le_span_of_aux (v : κ ⊕ σ → M)
    (hg : Function.Surjective g) (hslzero : ∀ i, s (v (.inl i)) = 0)
    (hli : LinearIndependent R (s ∘ v ∘ .inr)) (hsp : ⊤ ≤ Submodule.span R (Set.range v)) :
    ⊤ ≤ Submodule.span R (Set.range <| g ∘ v ∘ .inl)

Proof state:
case intro.inr
R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup K
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R K
inst✝ : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
s : M →ₗ[R] K
hs : s ∘ₗ f = LinearMap.id
hfg : Function.Exact ⇑f ⇑g
κ : Type u_6
σ : Type u_7
v : κ ⊕ σ → M
hg : Function.Surjective ⇑g
hslzero : ∀ (i : κ), s (v (Sum.inl i)) = 0
hli : LinearIndependent R (⇑s ∘ v ∘ Sum.inr)
hsp : ⊤ ≤ Submodule.span R (Set.range v)
m : M
this :
  ∀ {R : Type u_1} {M : Type u_2} {K : Type u_3} {P : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M]
    [inst_2 : AddCommGroup K] [inst_3 : AddCommGroup P] [inst_4 : Module R M] [inst_5 : Module R K]
    [inst_6 : Module R P] {f : K →ₗ[R] M} {g : M →ₗ[R] P} {s : M →ₗ[R] K},
    s ∘ₗ f = LinearMap.id →
      Function.Exact ⇑f ⇑g →
        ∀ {κ : Type u_6} {σ : Type u_7} (v : κ ⊕ σ → M),
          Function.Surjective ⇑g →
            (∀ (i : κ), s (v (Sum.inl i)) = 0) →
              LinearIndependent R (⇑s ∘ v ∘ Sum.inr) →
                ⊤ ≤ Submodule.span R (Set.range v) →
                  ∀ m ∈ LinearMap.ker s, g m ∈ Submodule.span R (Set.range (⇑g ∘ v ∘ Sum.inl))
h : m ∉ LinearMap.ker s
x : M := f (s m)
⊢ g (m - f (s m)) ∈ Submodule.span R (Set.range (⇑g ∘ v ∘ Sum.inl))

Tactic:
apply this hs hfg v hg hslzero hli hsp

Result:
case intro.inr.h
R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup K
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R K
inst✝ : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
s : M →ₗ[R] K
hs : s ∘ₗ f = LinearMap.id
hfg : Function.Exact ⇑f ⇑g
κ : Type u_6
σ : Type u_7
v : κ ⊕ σ → M
hg : Function.Surjective ⇑g
hslzero : ∀ (i : κ), s (v (Sum.inl i)) = 0
hli : LinearIndependent R (⇑s ∘ v ∘ Sum.inr)
hsp : ⊤ ≤ Submodule.span R (Set.range v)
m : M
this :
  ∀ {R : Type u_1} {M : Type u_2} {K : Type u_3} {P : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M]
    [inst_2 : AddCommGroup K] [inst_3 : AddCommGroup P] [inst_4 : Module R M] [inst_5 : Module R K]
    [inst_6 : Module R P] {f : K →ₗ[R] M} {g : M →ₗ[R] P} {s : M →ₗ[R] K},
    s ∘ₗ f = LinearMap.id →
      Function.Exact ⇑f ⇑g →
        ∀ {κ : Type u_6} {σ : Type u_7} (v : κ ⊕ σ → M),
          Function.Surjective ⇑g →
            (∀ (i : κ), s (v (Sum.inl i)) = 0) →
              LinearIndependent R (⇑s ∘ v ∘ Sum.inr) →
                ⊤ ≤ Submodule.span R (Set.range v) →
                  ∀ m ∈ LinearMap.ker s, g m ∈ Submodule.span R (Set.range (⇑g ∘ v ∘ Sum.inl))
h : m ∉ LinearMap.ker s
x : M := f (s m)
⊢ m - f (s m) ∈ LinearMap.ker s
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean
@[simp]
lemma Φ_four : W.Φ 4 = X * W.preΨ₄ ^ 2 * W.Ψ₂Sq - W.Ψ₃ * (W.preΨ₄ * W.Ψ₂Sq ^ 2 - W.Ψ₃ ^ 3)

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ X * W.preΨ₄ ^ 2 * W.Ψ₂Sq - (W.preΨ₄ * 1 ^ 3 * W.Ψ₂Sq ^ 2 - 1 * W.Ψ₃ ^ 3 * 1) * W.Ψ₃ * 1 =
    X * W.preΨ₄ ^ 2 * W.Ψ₂Sq - W.Ψ₃ * (W.preΨ₄ * W.Ψ₂Sq ^ 2 - W.Ψ₃ ^ 3)

Tactic:
ring1

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ ¬Even 3

Tactic:
decide

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ 4 = ↑3 + 1

Tactic:
rfl

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ 3 + 2 = 2 * 2 + 1

Tactic:
rfl

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ W.Φ 4 = X * W.preΨ₄ ^ 2 * W.Ψ₂Sq - W.Ψ₃ * (W.preΨ₄ * W.Ψ₂Sq ^ 2 - W.Ψ₃ ^ 3)

Tactic:
rw [show 4 = ((3 : ℕ) + 1 : ℤ) by rfl, Φ_ofNat, preΨ'_four, if_neg <| by decide,
  show 3 + 2 = 2 * 2 + 1 by rfl, preΨ'_odd, preΨ'_four, preΨ'_two, if_pos Even.zero, preΨ'_one,
  preΨ'_three, if_pos Even.zero, if_neg <| by decide]

Result:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ X * W.preΨ₄ ^ 2 * W.Ψ₂Sq - (W.preΨ₄ * 1 ^ 3 * W.Ψ₂Sq ^ 2 - 1 * W.Ψ₃ ^ 3 * 1) * W.Ψ₃ * 1 =
    X * W.preΨ₄ ^ 2 * W.Ψ₂Sq - W.Ψ₃ * (W.preΨ₄ * W.Ψ₂Sq ^ 2 - W.Ψ₃ ^ 3)
-- Mathlib/Algebra/Homology/Embedding/Boundary.lean
lemma boundaryLE_embeddingUpIntLE_iff (p : ℤ) (n : ℕ) :
    (embeddingUpIntGE p).BoundaryGE n ↔ n = 0

Proof state:
case mp.succ
p : ℤ
n : ℕ
h : (embeddingUpIntGE p).BoundaryGE (n + 1)
⊢ n + 1 = 0

Tactic:
have := h.2 n

Result:
case mp.succ
p : ℤ
n : ℕ
h : (embeddingUpIntGE p).BoundaryGE (n + 1)
this : ¬(up ℤ).Rel ((embeddingUpIntGE p).f n) ((embeddingUpIntGE p).f (n + 1))
⊢ n + 1 = 0

Proof state:
case mp.zero
p : ℤ
h : (embeddingUpIntGE p).BoundaryGE 0
⊢ 0 = 0

Tactic:
rfl

Result:
no goals

Proof state:
case mpr
p : ℤ
⊢ (embeddingUpIntGE p).BoundaryGE 0

Tactic:
constructor

Result:
case mpr.left
p : ℤ
⊢ (up ℤ).Rel ((up ℤ).prev ((embeddingUpIntGE p).f 0)) ((embeddingUpIntGE p).f 0)

case mpr.right
p : ℤ
⊢ ∀ (i : ℕ), ¬(up ℤ).Rel ((embeddingUpIntGE p).f i) ((embeddingUpIntGE p).f 0)

Proof state:
p : ℤ
n : ℕ
⊢ (embeddingUpIntGE p).BoundaryGE n ↔ n = 0

Tactic:
constructor

Result:
case mp
p : ℤ
n : ℕ
⊢ (embeddingUpIntGE p).BoundaryGE n → n = 0

case mpr
p : ℤ
n : ℕ
⊢ n = 0 → (embeddingUpIntGE p).BoundaryGE n

Proof state:
case mp
p : ℤ
n : ℕ
⊢ (embeddingUpIntGE p).BoundaryGE n → n = 0

Tactic:
intro h

Result:
case mp
p : ℤ
n : ℕ
h : (embeddingUpIntGE p).BoundaryGE n
⊢ n = 0

Proof state:
case mpr.right
p : ℤ
i : ℕ
hi : p + ↑i + 1 = p + 0
⊢ False

Tactic:
omega

Result:
no goals

Proof state:
case mpr
p : ℤ
n : ℕ
⊢ n = 0 → (embeddingUpIntGE p).BoundaryGE n

Tactic:
rintro rfl

Result:
case mpr
p : ℤ
⊢ (embeddingUpIntGE p).BoundaryGE 0

Proof state:
case mp.succ
p : ℤ
n : ℕ
h : (embeddingUpIntGE p).BoundaryGE (n + 1)
this : ¬(up ℤ).Rel ((embeddingUpIntGE p).f n) ((embeddingUpIntGE p).f (n + 1))
⊢ n + 1 = 0

Tactic:
dsimp at this

Result:
case mp.succ
p : ℤ
n : ℕ
h : (embeddingUpIntGE p).BoundaryGE (n + 1)
this : ¬p + ↑n + 1 = p + ↑(n + 1)
⊢ n + 1 = 0

Proof state:
case mpr.right
p : ℤ
⊢ ∀ (i : ℕ), ¬(up ℤ).Rel ((embeddingUpIntGE p).f i) ((embeddingUpIntGE p).f 0)

Tactic:
intro i hi

Result:
case mpr.right
p : ℤ
i : ℕ
hi : (up ℤ).Rel ((embeddingUpIntGE p).f i) ((embeddingUpIntGE p).f 0)
⊢ False

Proof state:
case mpr.left
p : ℤ
⊢ (up ℤ).Rel ((up ℤ).prev ((embeddingUpIntGE p).f 0)) ((embeddingUpIntGE p).f 0)

Tactic:
simp

Result:
no goals

Proof state:
case mp
p : ℤ
n : ℕ
h : (embeddingUpIntGE p).BoundaryGE n
⊢ n = 0

Tactic:
obtain _|n := n

Result:
case mp.zero
p : ℤ
h : (embeddingUpIntGE p).BoundaryGE 0
⊢ 0 = 0

case mp.succ
p : ℤ
n : ℕ
h : (embeddingUpIntGE p).BoundaryGE (n + 1)
⊢ n + 1 = 0

Proof state:
case mp.succ
p : ℤ
n : ℕ
h : (embeddingUpIntGE p).BoundaryGE (n + 1)
this : ¬p + ↑n + 1 = p + ↑(n + 1)
⊢ n + 1 = 0

Tactic:
omega

Result:
no goals

Proof state:
case mpr.right
p : ℤ
i : ℕ
hi : (up ℤ).Rel ((embeddingUpIntGE p).f i) ((embeddingUpIntGE p).f 0)
⊢ False

Tactic:
dsimp at hi

Result:
case mpr.right
p : ℤ
i : ℕ
hi : p + ↑i + 1 = p + 0
⊢ False
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem findIdx?_mkArray :
    (mkArray n a).findIdx? p = if 0 < n ∧ p a then some 0 else none

Proof state:
n : Nat
α✝ : Type u_1
a : α✝
p : α✝ → Bool
⊢ findIdx? p (List.replicate n a).toArray = if 0 < n ∧ p a = true then some 0 else none

Tactic:
simp only [List.findIdx?_toArray]

Result:
n : Nat
α✝ : Type u_1
a : α✝
p : α✝ → Bool
⊢ List.findIdx? p (List.replicate n a) = if 0 < n ∧ p a = true then some 0 else none

Proof state:
n : Nat
α✝ : Type u_1
a : α✝
p : α✝ → Bool
⊢ findIdx? p (mkArray n a) = if 0 < n ∧ p a = true then some 0 else none

Tactic:
rw [← List.toArray_replicate]

Result:
n : Nat
α✝ : Type u_1
a : α✝
p : α✝ → Bool
⊢ findIdx? p (List.replicate n a).toArray = if 0 < n ∧ p a = true then some 0 else none

Proof state:
n : Nat
α✝ : Type u_1
a : α✝
p : α✝ → Bool
⊢ List.findIdx? p (List.replicate n a) = if 0 < n ∧ p a = true then some 0 else none

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Convex/Basic.lean
theorem Convex.mem_smul_of_zero_mem (h : Convex 𝕜 s) {x : E} (zero_mem : (0 : E) ∈ s) (hx : x ∈ s)
    {t : 𝕜} (ht : 1 ≤ t) : x ∈ t • s

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
h : Convex 𝕜 s
x : E
zero_mem : 0 ∈ s
hx : x ∈ s
t : 𝕜
ht : 1 ≤ t
⊢ t⁻¹ • x ∈ s

Tactic:
exact h.smul_mem_of_zero_mem zero_mem hx
  ⟨inv_nonneg.2 (zero_le_one.trans ht), inv_le_one_of_one_le₀ ht⟩

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
h : Convex 𝕜 s
x : E
zero_mem : 0 ∈ s
hx : x ∈ s
t : 𝕜
ht : 1 ≤ t
⊢ x ∈ t • s

Tactic:
rw [mem_smul_set_iff_inv_smul_mem₀ (zero_lt_one.trans_le ht).ne']

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
h : Convex 𝕜 s
x : E
zero_mem : 0 ∈ s
hx : x ∈ s
t : 𝕜
ht : 1 ≤ t
⊢ t⁻¹ • x ∈ s
-- Mathlib/ModelTheory/Algebra/Field/IsAlgClosed.lean
theorem realize_genericMonicPolyHasRoot [Field K] [CompatibleRing K] (n : ℕ) :
    K ⊨ genericMonicPolyHasRoot n ↔
      ∀ p : { p : K[X] // p.Monic ∧ p.natDegree = n }, ∃ x, p.1.eval x = 0

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
n : ℕ
x✝ : DecidableEq K := Classical.decEq K
⊢ K ⊨ genericMonicPolyHasRoot n ↔
    ∀ (b : Fin n → K), ∃ x, eval x ↑(((monicEquivDegreeLT n).trans (degreeLTEquiv K n).toEquiv).symm b) = 0

Tactic:
simp [Sentence.Realize, genericMonicPolyHasRoot, lift_genericMonicPoly]

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
n : ℕ
⊢ K ⊨ genericMonicPolyHasRoot n ↔ ∀ (p : { p // p.Monic ∧ p.natDegree = n }), ∃ x, eval x ↑p = 0

Tactic:
let _ := Classical.decEq K

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
n : ℕ
x✝ : DecidableEq K := Classical.decEq K
⊢ K ⊨ genericMonicPolyHasRoot n ↔ ∀ (p : { p // p.Monic ∧ p.natDegree = n }), ∃ x, eval x ↑p = 0

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
n : ℕ
x✝ : DecidableEq K := Classical.decEq K
⊢ K ⊨ genericMonicPolyHasRoot n ↔ ∀ (p : { p // p.Monic ∧ p.natDegree = n }), ∃ x, eval x ↑p = 0

Tactic:
rw [Equiv.forall_congr_left ((monicEquivDegreeLT n).trans (degreeLTEquiv K n).toEquiv)]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
n : ℕ
x✝ : DecidableEq K := Classical.decEq K
⊢ K ⊨ genericMonicPolyHasRoot n ↔
    ∀ (b : Fin n → K), ∃ x, eval x ↑(((monicEquivDegreeLT n).trans (degreeLTEquiv K n).toEquiv).symm b) = 0
-- Mathlib/Algebra/Lie/Nilpotent.lean
theorem LieAlgebra.isNilpotent_range_ad_iff : IsNilpotent (ad R L).range ↔ IsNilpotent L

Proof state:
case refine_2
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
⊢ LieRing.IsNilpotent L → LieRing.IsNilpotent ↥(ad R L).range

Tactic:
intro h

Result:
case refine_2
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h : LieRing.IsNilpotent L
⊢ LieRing.IsNilpotent ↥(ad R L).range

Proof state:
case refine_1
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h : LieRing.IsNilpotent ↥(ad R L).range
⊢ LieRing.IsNilpotent L

Tactic:
have : (ad R L).ker = center R L := by simp

Result:
case refine_1
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h : LieRing.IsNilpotent ↥(ad R L).range
this : (ad R L).ker = center R L
⊢ LieRing.IsNilpotent L

Proof state:
case refine_1
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h : LieRing.IsNilpotent ↥(ad R L).range
this : (ad R L).ker = center R L
⊢ LieRing.IsNilpotent L

Tactic:
exact
  LieAlgebra.nilpotent_of_nilpotent_quotient (le_of_eq this)
    ((ad R L).quotKerEquivRange.nilpotent_iff_equiv_nilpotent.mpr h)

Result:
no goals

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h : LieRing.IsNilpotent ↥(ad R L).range
⊢ (ad R L).ker = center R L

Tactic:
simp

Result:
no goals

Proof state:
case refine_2
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h : LieRing.IsNilpotent L
⊢ LieRing.IsNilpotent ↥(ad R L).range

Tactic:
exact (ad R L).isNilpotent_range

Result:
no goals

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
⊢ LieRing.IsNilpotent ↥(ad R L).range ↔ LieRing.IsNilpotent L

Tactic:
refine ⟨fun h => ?_, ?_⟩

Result:
case refine_1
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h : LieRing.IsNilpotent ↥(ad R L).range
⊢ LieRing.IsNilpotent L

case refine_2
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
⊢ LieRing.IsNilpotent L → LieRing.IsNilpotent ↥(ad R L).range
-- Mathlib/LinearAlgebra/DFinsupp.lean
theorem lapply_comp_lsingle_of_ne [DecidableEq ι] (i i' : ι) (h : i ≠ i') :
    lapply i ∘ₗ lsingle i' = (0 : M i' →ₗ[R] M i)

Proof state:
ι : Type u_1
R : Type u_2
M : ι → Type u_4
inst✝³ : Semiring R
inst✝² : (i : ι) → AddCommMonoid (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : DecidableEq ι
i i' : ι
h : i ≠ i'
⊢ lapply i ∘ₗ lsingle i' = 0

Tactic:
ext

Result:
case h
ι : Type u_1
R : Type u_2
M : ι → Type u_4
inst✝³ : Semiring R
inst✝² : (i : ι) → AddCommMonoid (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : DecidableEq ι
i i' : ι
h : i ≠ i'
x✝ : M i'
⊢ (lapply i ∘ₗ lsingle i') x✝ = 0 x✝

Proof state:
case h
ι : Type u_1
R : Type u_2
M : ι → Type u_4
inst✝³ : Semiring R
inst✝² : (i : ι) → AddCommMonoid (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : DecidableEq ι
i i' : ι
h : i ≠ i'
x✝ : M i'
⊢ (lapply i ∘ₗ lsingle i') x✝ = 0 x✝

Tactic:
simp [h.symm]

Result:
no goals
-- Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean
lemma commute_of_mem_adjoin_of_forall_mem_commute {a b : A} {s : Set A}
    (hb : b ∈ adjoin R s) (h : ∀ b ∈ s, Commute a b) :
    Commute a b

Proof state:
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a b : A
s : Set A
hb : b ∈ adjoin R s
h : ∀ b ∈ s, Commute a b
this : a ∈ centralizer R s
⊢ Commute a b

Tactic:
exact adjoin_le_centralizer_centralizer R s hb a this

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a b : A
s : Set A
hb : b ∈ adjoin R s
h : ∀ b ∈ s, Commute a b
⊢ Commute a b

Tactic:
have : a ∈ centralizer R s := by simpa only [Commute.symm_iff (a := a)] using h

Result:
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a b : A
s : Set A
hb : b ∈ adjoin R s
h : ∀ b ∈ s, Commute a b
this : a ∈ centralizer R s
⊢ Commute a b

Proof state:
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a b : A
s : Set A
hb : b ∈ adjoin R s
h : ∀ b ∈ s, Commute a b
⊢ a ∈ centralizer R s

Tactic:
simpa only [Commute.symm_iff (a := a)] using h

Result:
no goals
-- Mathlib/Topology/Sheaves/Alexandrov.lean
theorem Topology.IsUpperSet.isSheaf_of_isRightKanExtension
    (P : (Opens X)ᵒᵖ ⥤ C)
    (η : Alexandrov.principals X ⋙ P ⟶ F)
    [P.IsRightKanExtension η] :
    Presheaf.IsSheaf (Opens.grothendieckTopology X) P

Proof state:
X : Type v
inst✝⁵ : TopologicalSpace X
inst✝⁴ : Preorder X
inst✝³ : Topology.IsUpperSet X
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
F : X ⥤ C
P : (Opens X)ᵒᵖ ⥤ C
η : principals X ⋙ P ⟶ F
inst✝ : P.IsRightKanExtension η
γ : principals X ⋙ principalsKanExtension F ⟶ F := (principals X).pointwiseRightKanExtensionCounit F
x✝ : (principalsKanExtension F).IsRightKanExtension γ := inferInstance
⊢ (principalsKanExtension F).IsRightKanExtension ?m.88333

Tactic:
assumption

Result:
no goals

Proof state:
X : Type v
inst✝⁵ : TopologicalSpace X
inst✝⁴ : Preorder X
inst✝³ : Topology.IsUpperSet X
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
F : X ⥤ C
P : (Opens X)ᵒᵖ ⥤ C
η : principals X ⋙ P ⟶ F
inst✝ : P.IsRightKanExtension η
γ : principals X ⋙ principalsKanExtension F ⟶ F := (principals X).pointwiseRightKanExtensionCounit F
x✝¹ : (principalsKanExtension F).IsRightKanExtension γ := inferInstance
this : P ≅ principalsKanExtension F
x✝ : Preorder ↑(of X) := inferInstanceAs (Preorder X)
⊢ TopCat.Presheaf.IsSheaf (principalsKanExtension F)

Tactic:
have _ : Topology.IsUpperSet (TopCat.of X) := inferInstanceAs <| Topology.IsUpperSet X

Result:
X : Type v
inst✝⁵ : TopologicalSpace X
inst✝⁴ : Preorder X
inst✝³ : Topology.IsUpperSet X
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
F : X ⥤ C
P : (Opens X)ᵒᵖ ⥤ C
η : principals X ⋙ P ⟶ F
inst✝ : P.IsRightKanExtension η
γ : principals X ⋙ principalsKanExtension F ⟶ F := (principals X).pointwiseRightKanExtensionCounit F
x✝² : (principalsKanExtension F).IsRightKanExtension γ := inferInstance
this : P ≅ principalsKanExtension F
x✝¹ : Preorder ↑(of X) := inferInstanceAs (Preorder X)
x✝ : Topology.IsUpperSet ↑(of X)
⊢ TopCat.Presheaf.IsSheaf (principalsKanExtension F)
-- Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean
theorem iteratedFDerivWithin_eventually_congr_set' (y : E) (h : s =ᶠ[𝓝[{y}ᶜ] x] t) (n : ℕ) :
    iteratedFDerivWithin 𝕜 n f s =ᶠ[𝓝 x] iteratedFDerivWithin 𝕜 n f t

Proof state:
case succ
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s t : Set E
f : E → F
y✝ : E
n : ℕ
ihn : ∀ {x : E}, s =ᶠ[𝓝[{y✝}ᶜ] x] t → iteratedFDerivWithin 𝕜 n f s =ᶠ[𝓝 x] iteratedFDerivWithin 𝕜 n f t
x : E
h : s =ᶠ[𝓝[{y✝}ᶜ] x] t
y : E
hy : ∀ᶠ (x : E) in 𝓝[{y✝}ᶜ] y, s x = t x
⊢ (continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F).symm (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s y) =
    (continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F).symm (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f t) t y)

Tactic:
rw [(ihn hy).fderivWithin_eq_nhds, fderivWithin_congr_set' _ hy]

Result:
no goals

Proof state:
case zero
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s t : Set E
f : E → F
y x : E
h : s =ᶠ[𝓝[{y}ᶜ] x] t
⊢ iteratedFDerivWithin 𝕜 0 f s =ᶠ[𝓝 x] iteratedFDerivWithin 𝕜 0 f t

Tactic:
rfl

Result:
no goals

Proof state:
case succ
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s t : Set E
f : E → F
y : E
n : ℕ
ihn : ∀ {x : E}, s =ᶠ[𝓝[{y}ᶜ] x] t → iteratedFDerivWithin 𝕜 n f s =ᶠ[𝓝 x] iteratedFDerivWithin 𝕜 n f t
x : E
h : s =ᶠ[𝓝[{y}ᶜ] x] t
⊢ iteratedFDerivWithin 𝕜 (n + 1) f s =ᶠ[𝓝 x] iteratedFDerivWithin 𝕜 (n + 1) f t

Tactic:
refine (eventually_nhds_nhdsWithin.2 h).mono fun y hy => ?_

Result:
case succ
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s t : Set E
f : E → F
y✝ : E
n : ℕ
ihn : ∀ {x : E}, s =ᶠ[𝓝[{y✝}ᶜ] x] t → iteratedFDerivWithin 𝕜 n f s =ᶠ[𝓝 x] iteratedFDerivWithin 𝕜 n f t
x : E
h : s =ᶠ[𝓝[{y✝}ᶜ] x] t
y : E
hy : ∀ᶠ (x : E) in 𝓝[{y✝}ᶜ] y, s x = t x
⊢ iteratedFDerivWithin 𝕜 (n + 1) f s y = iteratedFDerivWithin 𝕜 (n + 1) f t y
-- Mathlib/Data/List/Rotate.lean
theorem map_rotate {β : Type*} (f : α → β) (l : List α) (n : ℕ) :
    map f (l.rotate n) = (map f l).rotate n

Proof state:
α : Type u
β : Type u_1
f : α → β
l : List α
n : ℕ
⊢ map f (l.rotate n) = (map f l).rotate n

Tactic:
induction' n with n hn IH generalizing l

Result:
case zero
α : Type u
β : Type u_1
f : α → β
l : List α
⊢ map f (l.rotate 0) = (map f l).rotate 0

case succ
α : Type u
β : Type u_1
f : α → β
n : ℕ
hn : ∀ (l : List α), map f (l.rotate n) = (map f l).rotate n
l : List α
⊢ map f (l.rotate (n + 1)) = (map f l).rotate (n + 1)

Proof state:
case zero
α : Type u
β : Type u_1
f : α → β
l : List α
⊢ map f (l.rotate 0) = (map f l).rotate 0

Tactic:
simp

Result:
no goals

Proof state:
case succ.cons
α : Type u
β : Type u_1
f : α → β
n : ℕ
hn : ∀ (l : List α), map f (l.rotate n) = (map f l).rotate n
hd : α
tl : List α
⊢ map f ((hd :: tl).rotate (n + 1)) = (map f (hd :: tl)).rotate (n + 1)

Tactic:
simp [hn]

Result:
no goals

Proof state:
case succ.nil
α : Type u
β : Type u_1
f : α → β
n : ℕ
hn : ∀ (l : List α), map f (l.rotate n) = (map f l).rotate n
⊢ map f ([].rotate (n + 1)) = (map f []).rotate (n + 1)

Tactic:
simp

Result:
no goals

Proof state:
case succ
α : Type u
β : Type u_1
f : α → β
n : ℕ
hn : ∀ (l : List α), map f (l.rotate n) = (map f l).rotate n
l : List α
⊢ map f (l.rotate (n + 1)) = (map f l).rotate (n + 1)

Tactic:
rcases l with - | ⟨hd, tl⟩

Result:
case succ.nil
α : Type u
β : Type u_1
f : α → β
n : ℕ
hn : ∀ (l : List α), map f (l.rotate n) = (map f l).rotate n
⊢ map f ([].rotate (n + 1)) = (map f []).rotate (n + 1)

case succ.cons
α : Type u
β : Type u_1
f : α → β
n : ℕ
hn : ∀ (l : List α), map f (l.rotate n) = (map f l).rotate n
hd : α
tl : List α
⊢ map f ((hd :: tl).rotate (n + 1)) = (map f (hd :: tl)).rotate (n + 1)