harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Category/ModuleCat/Presheaf.lean
@[simp]
lemma comp_app {M₁ M₂ M₃ : PresheafOfModules R} (f : M₁ ⟶ M₂) (g : M₂ ⟶ M₃) (X : Cᵒᵖ) :
    (f ≫ g).app X = f.app X ≫ g.app X

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M₁ M₂ M₃ : PresheafOfModules R
f : M₁ ⟶ M₂
g : M₂ ⟶ M₃
X : Cᵒᵖ
⊢ (f ≫ g).app X = f.app X ≫ g.app X

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem mem_attach (l : Array α) : ∀ x, x ∈ l.attach
  | ⟨a, h⟩ => by
    have := mem_map.1 (by rw [attach_map_subtype_val] <;> exact h)
    rcases this with ⟨⟨_, _⟩, m, rfl⟩
    exact m

Proof state:
α : Type u_1
l : Array α
a : α
h : a ∈ l
⊢ ?m.26357 ∈ map ?m.26358 ?m.26359

Tactic:
rw [attach_map_subtype_val] <;> exact h

Result:
no goals

Proof state:
α : Type u_1
l : Array α
a : α
h : a ∈ l
this : ∃ a_1, a_1 ∈ l.attach ∧ a_1.val = a
⊢ ⟨a, h⟩ ∈ l.attach

Tactic:
rcases this with ⟨⟨_, _⟩, m, rfl⟩

Result:
case intro.mk.intro
α : Type u_1
l : Array α
val✝ : α
property✝ : val✝ ∈ l
m : ⟨val✝, property✝⟩ ∈ l.attach
h : ⟨val✝, property✝⟩.val ∈ l
⊢ ⟨⟨val✝, property✝⟩.val, h⟩ ∈ l.attach

Proof state:
case intro.mk.intro
α : Type u_1
l : Array α
val✝ : α
property✝ : val✝ ∈ l
m : ⟨val✝, property✝⟩ ∈ l.attach
h : ⟨val✝, property✝⟩.val ∈ l
⊢ ⟨⟨val✝, property✝⟩.val, h⟩ ∈ l.attach

Tactic:
exact m

Result:
no goals

Proof state:
α : Type u_1
l : Array α
a : α
h : a ∈ l
⊢ ⟨a, h⟩ ∈ l.attach

Tactic:
have := mem_map.1 (by rw [attach_map_subtype_val] <;> exact h)

Result:
α : Type u_1
l : Array α
a : α
h : a ∈ l
this : ∃ a_1, a_1 ∈ l.attach ∧ a_1.val = a
⊢ ⟨a, h⟩ ∈ l.attach
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem pi_ne_zero : (π : Angle) ≠ 0

Proof state:
⊢ ↑π ≠ 0

Tactic:
rw [← toReal_injective.ne_iff, toReal_pi, toReal_zero]

Result:
⊢ π ≠ 0

Proof state:
⊢ π ≠ 0

Tactic:
exact Real.pi_ne_zero

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean
theorem cyclotomic_pos_and_nonneg (n : ℕ) {R} [LinearOrderedCommRing R] (x : R) :
    (1 < x → 0 < eval x (cyclotomic n R)) ∧ (1 ≤ x → 0 ≤ eval x (cyclotomic n R))

Proof state:
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
n : ℕ
a✝ : 1 ≤ x
⊢ 2 < n + 1 + 1 + 1

Tactic:
omega

Result:
no goals

Proof state:
case succ.succ.zero
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
⊢ (1 < x → 0 < eval x (cyclotomic (0 + 1 + 1) R)) ∧ (1 ≤ x → 0 ≤ eval x (cyclotomic (0 + 1 + 1) R))

Tactic:
simp only [zero_add, reduceAdd, cyclotomic_two, eval_add, eval_X, eval_one]

Result:
case succ.succ.zero
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
⊢ (1 < x → 0 < x + 1) ∧ (1 ≤ x → 0 ≤ x + 1)

Proof state:
case succ.succ.succ
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
n : ℕ
⊢ (1 < x → 0 < eval x (cyclotomic (n + 1 + 1 + 1) R)) ∧ (1 ≤ x → 0 ≤ eval x (cyclotomic (n + 1 + 1 + 1) R))

Tactic:
constructor <;> intro <;> [skip; apply le_of_lt] <;> apply cyclotomic_pos (by omega)

Result:
no goals

Proof state:
case succ.succ.zero
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
⊢ (1 < x → 0 < x + 1) ∧ (1 ≤ x → 0 ≤ x + 1)

Tactic:
constructor <;> intro <;> linarith

Result:
no goals

Proof state:
n : ℕ
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
⊢ (1 < x → 0 < eval x (cyclotomic n R)) ∧ (1 ≤ x → 0 ≤ eval x (cyclotomic n R))

Tactic:
rcases n with (_ | _ | _ | n)

Result:
case zero
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
⊢ (1 < x → 0 < eval x (cyclotomic 0 R)) ∧ (1 ≤ x → 0 ≤ eval x (cyclotomic 0 R))

case succ.zero
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
⊢ (1 < x → 0 < eval x (cyclotomic (0 + 1) R)) ∧ (1 ≤ x → 0 ≤ eval x (cyclotomic (0 + 1) R))

case succ.succ.zero
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
⊢ (1 < x → 0 < eval x (cyclotomic (0 + 1 + 1) R)) ∧ (1 ≤ x → 0 ≤ eval x (cyclotomic (0 + 1 + 1) R))

case succ.succ.succ
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
n : ℕ
⊢ (1 < x → 0 < eval x (cyclotomic (n + 1 + 1 + 1) R)) ∧ (1 ≤ x → 0 ≤ eval x (cyclotomic (n + 1 + 1 + 1) R))

Proof state:
case zero
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
⊢ (1 < x → 0 < eval x (cyclotomic 0 R)) ∧ (1 ≤ x → 0 ≤ eval x (cyclotomic 0 R))

Tactic:
simp only [cyclotomic_zero, eval_one, zero_lt_one, implies_true, zero_le_one, and_self]

Result:
no goals

Proof state:
case succ.zero
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
⊢ (1 < x → 0 < eval x (cyclotomic (0 + 1) R)) ∧ (1 ≤ x → 0 ≤ eval x (cyclotomic (0 + 1) R))

Tactic:
simp only [zero_add, cyclotomic_one, eval_sub, eval_X, eval_one, sub_pos, imp_self, sub_nonneg,
  and_self]

Result:
no goals
-- Mathlib/Topology/Algebra/Field.lean
theorem IsPreconnected.eq_one_or_eq_neg_one_of_sq_eq [Ring 𝕜] [NoZeroDivisors 𝕜]
    (hS : IsPreconnected S) (hf : ContinuousOn f S) (hsq : EqOn (f ^ 2) 1 S) :
    EqOn f 1 S ∨ EqOn f (-1) S

Proof state:
α : Type u_2
𝕜 : Type u_3
f : α → 𝕜
S : Set α
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace 𝕜
inst✝² : T1Space 𝕜
inst✝¹ : Ring 𝕜
inst✝ : NoZeroDivisors 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hsq : EqOn (f ^ 2) 1 S
this : DiscreteTopology ↑{1, -1}
⊢ EqOn f 1 S ∨ EqOn f (-1) S

Tactic:
have hmaps : MapsTo f S {1, -1} := by
  simpa only [EqOn, Pi.one_apply, Pi.pow_apply, sq_eq_one_iff] using hsq

Result:
α : Type u_2
𝕜 : Type u_3
f : α → 𝕜
S : Set α
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace 𝕜
inst✝² : T1Space 𝕜
inst✝¹ : Ring 𝕜
inst✝ : NoZeroDivisors 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hsq : EqOn (f ^ 2) 1 S
this : DiscreteTopology ↑{1, -1}
hmaps : MapsTo f S {1, -1}
⊢ EqOn f 1 S ∨ EqOn f (-1) S

Proof state:
α : Type u_2
𝕜 : Type u_3
f : α → 𝕜
S : Set α
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace 𝕜
inst✝² : T1Space 𝕜
inst✝¹ : Ring 𝕜
inst✝ : NoZeroDivisors 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hsq : EqOn (f ^ 2) 1 S
this : DiscreteTopology ↑{1, -1}
⊢ MapsTo f S {1, -1}

Tactic:
simpa only [EqOn, Pi.one_apply, Pi.pow_apply, sq_eq_one_iff] using hsq

Result:
no goals

Proof state:
α : Type u_2
𝕜 : Type u_3
f : α → 𝕜
S : Set α
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace 𝕜
inst✝² : T1Space 𝕜
inst✝¹ : Ring 𝕜
inst✝ : NoZeroDivisors 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hsq : EqOn (f ^ 2) 1 S
this : DiscreteTopology ↑{1, -1}
hmaps : MapsTo f S {1, -1}
⊢ EqOn f 1 S ∨ EqOn f (-1) S

Tactic:
simpa using hS.eqOn_const_of_mapsTo hf hmaps

Result:
no goals

Proof state:
α : Type u_2
𝕜 : Type u_3
f : α → 𝕜
S : Set α
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace 𝕜
inst✝² : T1Space 𝕜
inst✝¹ : Ring 𝕜
inst✝ : NoZeroDivisors 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hsq : EqOn (f ^ 2) 1 S
⊢ EqOn f 1 S ∨ EqOn f (-1) S

Tactic:
have : DiscreteTopology ({1, -1} : Set 𝕜) := Finite.instDiscreteTopology

Result:
α : Type u_2
𝕜 : Type u_3
f : α → 𝕜
S : Set α
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace 𝕜
inst✝² : T1Space 𝕜
inst✝¹ : Ring 𝕜
inst✝ : NoZeroDivisors 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hsq : EqOn (f ^ 2) 1 S
this : DiscreteTopology ↑{1, -1}
⊢ EqOn f 1 S ∨ EqOn f (-1) S
-- Mathlib/RingTheory/Flat/Basic.lean
theorem iff_lTensor_injective' :
    Flat R M ↔ ∀ (I : Ideal R), Function.Injective (lTensor M I.subtype)

Proof state:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Flat R M ↔ ∀ (I : Ideal R), Function.Injective ⇑(lTensor M (Submodule.subtype I))

Tactic:
simpa [← comm_comp_rTensor_comp_comm_eq] using iff_rTensor_injective'

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Simproc.lean
theorem sub_add_eq_comm (a b c : Nat) : a - (b + c) = a - c - b

Proof state:
a b c : Nat
⊢ a - (b + c) = a - c - b

Tactic:
rw [Nat.add_comm b c]

Result:
a b c : Nat
⊢ a - (c + b) = a - c - b

Proof state:
a b c : Nat
⊢ a - (c + b) = a - c - b

Tactic:
exact Nat.sub_add_eq a c b

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/ZPow.lean
theorem zpow_neg_one (A : M) : A ^ (-1 : ℤ) = A⁻¹

Proof state:
case h.e'_3.h.e'_3
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
⊢ A = DivInvMonoid.zpow (↑(Nat.succ 0)) A

Tactic:
simp only [zpow_one, Int.ofNat_zero, Int.ofNat_succ, zpow_eq_pow, zero_add]

Result:
no goals

Proof state:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
⊢ A ^ (-1) = A⁻¹

Tactic:
convert DivInvMonoid.zpow_neg' 0 A

Result:
case h.e'_3.h.e'_3
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
⊢ A = DivInvMonoid.zpow (↑(Nat.succ 0)) A
-- Mathlib/Topology/Baire/Lemmas.lean
theorem mem_residual {s : Set X} : s ∈ residual X ↔ ∃ t ⊆ s, IsGδ t ∧ Dense t

Proof state:
case mpr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
s : Set X
⊢ (∃ t ⊆ s, IsGδ t ∧ Dense t) → s ∈ residual X

Tactic:
rintro ⟨t, ts, ho, hd⟩

Result:
case mpr.intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
s t : Set X
ts : t ⊆ s
ho : IsGδ t
hd : Dense t
⊢ s ∈ residual X

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
s : Set X
⊢ s ∈ residual X ↔ ∃ t ⊆ s, IsGδ t ∧ Dense t

Tactic:
constructor

Result:
case mp
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
s : Set X
⊢ s ∈ residual X → ∃ t ⊆ s, IsGδ t ∧ Dense t

case mpr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
s : Set X
⊢ (∃ t ⊆ s, IsGδ t ∧ Dense t) → s ∈ residual X

Proof state:
case mp.intro.intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
s : Set X
S : Set (Set X)
hSo : ∀ t ∈ S, IsOpen t
hSd : ∀ t ∈ S, Dense t
Sct : S.Countable
Ss : ⋂₀ S ⊆ s
⊢ Dense (⋂₀ S)

Tactic:
exact dense_sInter_of_isOpen hSo Sct hSd

Result:
no goals

Proof state:
case mp
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
s : Set X
⊢ (∃ S, (∀ t ∈ S, IsOpen t) ∧ (∀ t ∈ S, Dense t) ∧ S.Countable ∧ ⋂₀ S ⊆ s) → ∃ t ⊆ s, IsGδ t ∧ Dense t

Tactic:
rintro ⟨S, hSo, hSd, Sct, Ss⟩

Result:
case mp.intro.intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
s : Set X
S : Set (Set X)
hSo : ∀ t ∈ S, IsOpen t
hSd : ∀ t ∈ S, Dense t
Sct : S.Countable
Ss : ⋂₀ S ⊆ s
⊢ ∃ t ⊆ s, IsGδ t ∧ Dense t

Proof state:
case mpr.intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
s t : Set X
ts : t ⊆ s
ho : IsGδ t
hd : Dense t
⊢ s ∈ residual X

Tactic:
exact mem_of_superset (residual_of_dense_Gδ ho hd) ts

Result:
no goals

Proof state:
case mp.intro.intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
s : Set X
S : Set (Set X)
hSo : ∀ t ∈ S, IsOpen t
hSd : ∀ t ∈ S, Dense t
Sct : S.Countable
Ss : ⋂₀ S ⊆ s
⊢ ∃ t ⊆ s, IsGδ t ∧ Dense t

Tactic:
refine ⟨_, Ss, ⟨_, fun t ht => hSo _ ht, Sct, rfl⟩, ?_⟩

Result:
case mp.intro.intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
s : Set X
S : Set (Set X)
hSo : ∀ t ∈ S, IsOpen t
hSd : ∀ t ∈ S, Dense t
Sct : S.Countable
Ss : ⋂₀ S ⊆ s
⊢ Dense (⋂₀ S)

Proof state:
case mp
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
s : Set X
⊢ s ∈ residual X → ∃ t ⊆ s, IsGδ t ∧ Dense t

Tactic:
rw [mem_residual_iff]

Result:
case mp
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
s : Set X
⊢ (∃ S, (∀ t ∈ S, IsOpen t) ∧ (∀ t ∈ S, Dense t) ∧ S.Countable ∧ ⋂₀ S ⊆ s) → ∃ t ⊆ s, IsGδ t ∧ Dense t
-- Mathlib/LinearAlgebra/Projectivization/Subspace.lean
theorem span_sup {S : Set (ℙ K V)} {W : Subspace K V} : span S ⊔ W = span (S ∪ W)

Proof state:
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (ℙ K V)
W : Subspace K V
⊢ span S ⊔ W = span (S ∪ ↑W)

Tactic:
rw [span_union, span_coe]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem set_comm (a b : α) : ∀ {n m : Nat} (l : List α), n ≠ m →
    (l.set n a).set m b = (l.set m b).set n a
  | _, _, [], _ => by simp
  | _+1, 0, _ :: _, _ => by simp [set]
  | 0, _+1, _ :: _, _ => by simp [set]
  | _+1, _+1, _ :: t, h =>
    congrArg _ <| set_comm a b t fun h' => h <| Nat.succ_inj'.mpr h'

Proof state:
α : Type u_1
a b : α
n✝ : Nat
head✝ : α
tail✝ : List α
x✝ : 0 ≠ n✝ + 1
⊢ ((head✝ :: tail✝).set 0 a).set (n✝ + 1) b = ((head✝ :: tail✝).set (n✝ + 1) b).set 0 a

Tactic:
simp [set]

Result:
no goals

Proof state:
α : Type u_1
a b : α
n✝ : Nat
head✝ : α
tail✝ : List α
x✝ : n✝ + 1 ≠ 0
⊢ ((head✝ :: tail✝).set (n✝ + 1) a).set 0 b = ((head✝ :: tail✝).set 0 b).set (n✝ + 1) a

Tactic:
simp [set]

Result:
no goals

Proof state:
α : Type u_1
a b : α
x✝² x✝¹ : Nat
x✝ : x✝² ≠ x✝¹
⊢ ([].set x✝² a).set x✝¹ b = ([].set x✝¹ b).set x✝² a

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Ends/Defs.lean
theorem exists_adj_boundary_pair (Gc : G.Preconnected) (hK : K.Nonempty) :
    ∀ C : G.ComponentCompl K, ∃ ck : V × V, ck.1 ∈ C ∧ ck.2 ∈ K ∧ G.Adj ck.1 ck.2

Proof state:
V : Type u
G : SimpleGraph V
K : Set V
Gc : G.Preconnected
hK : K.Nonempty
v : V
vnK : v ∉ K
C : G.ComponentCompl K := G.componentComplMk vnK
dis : K ∩ ↑C ⊆ ∅ := Set.disjoint_iff.mp (ComponentCompl.disjoint_right C)
⊢ ∃ ck, ck.1 ∈ G.componentComplMk vnK ∧ ck.2 ∈ K ∧ G.Adj ck.1 ck.2

Tactic:
by_contra! h

Result:
V : Type u
G : SimpleGraph V
K : Set V
Gc : G.Preconnected
hK : K.Nonempty
v : V
vnK : v ∉ K
C : G.ComponentCompl K := G.componentComplMk vnK
dis : K ∩ ↑C ⊆ ∅ := Set.disjoint_iff.mp (ComponentCompl.disjoint_right C)
h : ∀ (ck : V × V), ck.1 ∈ G.componentComplMk vnK → ck.2 ∈ K → ¬G.Adj ck.1 ck.2
⊢ False
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Complex.lean
theorem tan_eq {z : ℂ}
    (h :
      ((∀ k : ℤ, (z.re : ℂ) ≠ (2 * k + 1) * π / 2) ∧
          ∀ l : ℤ, (z.im : ℂ) * I ≠ (2 * l + 1) * π / 2) ∨
        (∃ k : ℤ, (z.re : ℂ) = (2 * k + 1) * π / 2) ∧
          ∃ l : ℤ, (z.im : ℂ) * I = (2 * l + 1) * π / 2) :
    tan z = (tan z.re + tanh z.im * I) / (1 - tan z.re * tanh z.im * I)

Proof state:
z : ℂ
h :
  ((∀ (k : ℤ), ↑z.re ≠ (2 * ↑k + 1) * ↑π / 2) ∧ ∀ (l : ℤ), ↑z.im * I ≠ (2 * ↑l + 1) * ↑π / 2) ∨
    (∃ k, ↑z.re = (2 * ↑k + 1) * ↑π / 2) ∧ ∃ l, ↑z.im * I = (2 * ↑l + 1) * ↑π / 2
⊢ tan z = (tan ↑z.re + tanh ↑z.im * I) / (1 - tan ↑z.re * tanh ↑z.im * I)

Tactic:
convert tan_add_mul_I h

Result:
case h.e'_2.h.e'_1
z : ℂ
h :
  ((∀ (k : ℤ), ↑z.re ≠ (2 * ↑k + 1) * ↑π / 2) ∧ ∀ (l : ℤ), ↑z.im * I ≠ (2 * ↑l + 1) * ↑π / 2) ∨
    (∃ k, ↑z.re = (2 * ↑k + 1) * ↑π / 2) ∧ ∃ l, ↑z.im * I = (2 * ↑l + 1) * ↑π / 2
⊢ z = ↑z.re + ↑z.im * I

Proof state:
case h.e'_2.h.e'_1
z : ℂ
h :
  ((∀ (k : ℤ), ↑z.re ≠ (2 * ↑k + 1) * ↑π / 2) ∧ ∀ (l : ℤ), ↑z.im * I ≠ (2 * ↑l + 1) * ↑π / 2) ∨
    (∃ k, ↑z.re = (2 * ↑k + 1) * ↑π / 2) ∧ ∃ l, ↑z.im * I = (2 * ↑l + 1) * ↑π / 2
⊢ z = ↑z.re + ↑z.im * I

Tactic:
exact (re_add_im z).symm

Result:
no goals
-- Mathlib/Algebra/Lie/Nilpotent.lean
theorem _root_.LieAlgebra.ad_nilpotent_of_nilpotent {a : A} (h : IsNilpotent a) :
    IsNilpotent (LieAlgebra.ad R A a)

Proof state:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
h : IsNilpotent a
hl : IsNilpotent (LinearMap.mulLeft R a)
hr : IsNilpotent (LinearMap.mulRight R a)
⊢ IsNilpotent ((LinearMap.mulLeft R - LinearMap.mulRight R) a)

Tactic:
have := @LinearMap.commute_mulLeft_right R A _ _ _ _ _ a a

Result:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
h : IsNilpotent a
hl : IsNilpotent (LinearMap.mulLeft R a)
hr : IsNilpotent (LinearMap.mulRight R a)
this : Commute (LinearMap.mulLeft R a) (LinearMap.mulRight R a)
⊢ IsNilpotent ((LinearMap.mulLeft R - LinearMap.mulRight R) a)

Proof state:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
h : IsNilpotent a
hl : IsNilpotent (LinearMap.mulLeft R a)
hr : IsNilpotent (LinearMap.mulRight R a)
this : Commute (LinearMap.mulLeft R a) (LinearMap.mulRight R a)
⊢ IsNilpotent ((LinearMap.mulLeft R - LinearMap.mulRight R) a)

Tactic:
exact this.isNilpotent_sub hl hr

Result:
no goals

Proof state:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
h : IsNilpotent a
hl : IsNilpotent (LinearMap.mulLeft R a)
⊢ IsNilpotent ((LinearMap.mulLeft R - LinearMap.mulRight R) a)

Tactic:
have hr : IsNilpotent (LinearMap.mulRight R a) := by rwa [LinearMap.isNilpotent_mulRight_iff]

Result:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
h : IsNilpotent a
hl : IsNilpotent (LinearMap.mulLeft R a)
hr : IsNilpotent (LinearMap.mulRight R a)
⊢ IsNilpotent ((LinearMap.mulLeft R - LinearMap.mulRight R) a)

Proof state:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
h : IsNilpotent a
⊢ IsNilpotent ((LinearMap.mulLeft R - LinearMap.mulRight R) a)

Tactic:
have hl : IsNilpotent (LinearMap.mulLeft R a) := by rwa [LinearMap.isNilpotent_mulLeft_iff]

Result:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
h : IsNilpotent a
hl : IsNilpotent (LinearMap.mulLeft R a)
⊢ IsNilpotent ((LinearMap.mulLeft R - LinearMap.mulRight R) a)

Proof state:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
h : IsNilpotent a
⊢ IsNilpotent (LinearMap.mulLeft R a)

Tactic:
rwa [LinearMap.isNilpotent_mulLeft_iff]

Result:
no goals

Proof state:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
h : IsNilpotent a
⊢ IsNilpotent ((LieAlgebra.ad R A) a)

Tactic:
rw [LieAlgebra.ad_eq_lmul_left_sub_lmul_right]

Result:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
h : IsNilpotent a
⊢ IsNilpotent ((LinearMap.mulLeft R - LinearMap.mulRight R) a)

Proof state:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
h : IsNilpotent a
hl : IsNilpotent (LinearMap.mulLeft R a)
⊢ IsNilpotent (LinearMap.mulRight R a)

Tactic:
rwa [LinearMap.isNilpotent_mulRight_iff]

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
theorem vecMul_sub [Fintype m] (A B : Matrix m n α) (x : m → α) :
    x ᵥ* (A - B) = x ᵥ* A - x ᵥ* B

Proof state:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype m
A B : Matrix m n α
x : m → α
⊢ x ᵥ* (A - B) = x ᵥ* A - x ᵥ* B

Tactic:
simp [sub_eq_add_neg, vecMul_add, vecMul_neg]

Result:
no goals
-- Mathlib/Analysis/Analytic/Constructions.lean
/-- The Cartesian product of analytic functions is analytic. -/
@[fun_prop]
lemma AnalyticAt.prod {e : E} {f : E → F} {g : E → G}
    (hf : AnalyticAt 𝕜 f e) (hg : AnalyticAt 𝕜 g e) :
    AnalyticAt 𝕜 (fun x ↦ (f x, g x)) e

Proof state:
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
e : E
f : E → F
g : E → G
hf : AnalyticAt 𝕜 f e
hg : AnalyticAt 𝕜 g e
⊢ AnalyticAt 𝕜 (fun x => (f x, g x)) e

Tactic:
rcases hf with ⟨_, hf⟩

Result:
case intro
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
e : E
f : E → F
g : E → G
hg : AnalyticAt 𝕜 g e
w✝ : FormalMultilinearSeries 𝕜 E F
hf : HasFPowerSeriesAt f w✝ e
⊢ AnalyticAt 𝕜 (fun x => (f x, g x)) e

Proof state:
case intro.intro
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
e : E
f : E → F
g : E → G
w✝¹ : FormalMultilinearSeries 𝕜 E F
hf : HasFPowerSeriesAt f w✝¹ e
w✝ : FormalMultilinearSeries 𝕜 E G
hg : HasFPowerSeriesAt g w✝ e
⊢ AnalyticAt 𝕜 (fun x => (f x, g x)) e

Tactic:
exact ⟨_, hf.prod hg⟩

Result:
no goals

Proof state:
case intro
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
e : E
f : E → F
g : E → G
hg : AnalyticAt 𝕜 g e
w✝ : FormalMultilinearSeries 𝕜 E F
hf : HasFPowerSeriesAt f w✝ e
⊢ AnalyticAt 𝕜 (fun x => (f x, g x)) e

Tactic:
rcases hg with ⟨_, hg⟩

Result:
case intro.intro
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
e : E
f : E → F
g : E → G
w✝¹ : FormalMultilinearSeries 𝕜 E F
hf : HasFPowerSeriesAt f w✝¹ e
w✝ : FormalMultilinearSeries 𝕜 E G
hg : HasFPowerSeriesAt g w✝ e
⊢ AnalyticAt 𝕜 (fun x => (f x, g x)) e
-- Mathlib/Algebra/Polynomial/Bivariate.lean
lemma evalEval_sum (x y : R) (p : R[X]) (f : ℕ → R → R[X][Y]) :
    (p.sum f).evalEval x y = p.sum fun n a => (f n a).evalEval x y

Proof state:
R : Type u_1
inst✝ : Semiring R
x y : R
p : R[X]
f : ℕ → R → R[X][Y]
⊢ evalEval x y (p.sum f) = p.sum fun n a => evalEval x y (f n a)

Tactic:
simp only [evalEval, eval, eval₂_sum]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/RankNullity.lean
theorem exists_linearIndependent_snoc_of_lt_rank [StrongRankCondition R] {n : ℕ} {v : Fin n → M}
    (hv : LinearIndependent R v) (h : n < Module.rank R M) :
    ∃ (x : M), LinearIndependent R (Fin.snoc v x)

Proof state:
R : Type u_1
M : Type u
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : HasRankNullity.{u, u_1} R
inst✝ : StrongRankCondition R
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
h : ↑n < Module.rank R M
⊢ ∃ x, LinearIndependent R fun i => Fin.cons x v ((finRotate (n + 1)) i)

Tactic:
have ⟨x, hx⟩ := exists_linearIndependent_cons_of_lt_rank hv h

Result:
R : Type u_1
M : Type u
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : HasRankNullity.{u, u_1} R
inst✝ : StrongRankCondition R
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
h : ↑n < Module.rank R M
x : M
hx : LinearIndependent R (Fin.cons x v)
⊢ ∃ x, LinearIndependent R fun i => Fin.cons x v ((finRotate (n + 1)) i)

Proof state:
R : Type u_1
M : Type u
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : HasRankNullity.{u, u_1} R
inst✝ : StrongRankCondition R
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
h : ↑n < Module.rank R M
x : M
hx : LinearIndependent R (Fin.cons x v)
⊢ ∃ x, LinearIndependent R fun i => Fin.cons x v ((finRotate (n + 1)) i)

Tactic:
exact ⟨x, hx.comp _ (finRotate _).injective⟩

Result:
no goals

Proof state:
R : Type u_1
M : Type u
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : HasRankNullity.{u, u_1} R
inst✝ : StrongRankCondition R
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
h : ↑n < Module.rank R M
⊢ ∃ x, LinearIndependent R (Fin.snoc v x)

Tactic:
simp only [Fin.snoc_eq_cons_rotate]

Result:
R : Type u_1
M : Type u
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : HasRankNullity.{u, u_1} R
inst✝ : StrongRankCondition R
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
h : ↑n < Module.rank R M
⊢ ∃ x, LinearIndependent R fun i => Fin.cons x v ((finRotate (n + 1)) i)
-- Mathlib/Analysis/SpecialFunctions/Stirling.lean
theorem tendsto_self_div_two_mul_self_add_one :
    Tendsto (fun n : ℕ => (n : ℝ) / (2 * n + 1)) atTop (𝓝 (1 / 2))

Proof state:
n : ℕ
hn : n ≥ 1
⊢ (2 + 1 / ↑n)⁻¹ = (fun n => ↑n / (2 * ↑n + 1)) n

Tactic:
rw [add_div' (1 : ℝ) 2 n (cast_ne_zero.mpr (one_le_iff_ne_zero.mp hn)), inv_div]

Result:
no goals

Proof state:
⊢ Tendsto (fun n => ↑n / (2 * ↑n + 1)) atTop (𝓝 (2 + 0)⁻¹)

Tactic:
refine (((tendsto_const_div_atTop_nhds_zero_nat 1).const_add (2 : ℝ)).inv₀
  ((add_zero (2 : ℝ)).symm ▸ two_ne_zero)).congr' (eventually_atTop.mpr ⟨1, fun n hn => ?_⟩)

Result:
n : ℕ
hn : n ≥ 1
⊢ (2 + 1 / ↑n)⁻¹ = (fun n => ↑n / (2 * ↑n + 1)) n
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Gcd.lean
theorem gcd_gcd_self_left_right (m n : Nat) : gcd (gcd n m) m = gcd n m

Proof state:
m n : Nat
⊢ (n.gcd m).gcd m = n.gcd m

Tactic:
rw [gcd_comm, gcd_gcd_self_right_right]

Result:
no goals