harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Normed/Algebra/MatrixExponential.lean
theorem exp_units_conj (U : (Matrix m m 𝔸)ˣ) (A : Matrix m m 𝔸) :
    exp 𝕂 (U * A * U⁻¹) = U * exp 𝕂 A * U⁻¹

Proof state:
𝕂 : Type u_1
m : Type u_2
𝔸 : Type u_5
inst✝⁵ : RCLike 𝕂
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
U : (Matrix m m 𝔸)ˣ
A : Matrix m m 𝔸
this : SeminormedRing (Matrix m m 𝔸) := Matrix.linftyOpSemiNormedRing
⊢ exp 𝕂 (↑U * A * ↑U⁻¹) = ↑U * exp 𝕂 A * ↑U⁻¹

Tactic:
letI : NormedRing (Matrix m m 𝔸) := Matrix.linftyOpNormedRing

Result:
𝕂 : Type u_1
m : Type u_2
𝔸 : Type u_5
inst✝⁵ : RCLike 𝕂
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
U : (Matrix m m 𝔸)ˣ
A : Matrix m m 𝔸
this✝ : SeminormedRing (Matrix m m 𝔸) := Matrix.linftyOpSemiNormedRing
this : NormedRing (Matrix m m 𝔸) := Matrix.linftyOpNormedRing
⊢ exp 𝕂 (↑U * A * ↑U⁻¹) = ↑U * exp 𝕂 A * ↑U⁻¹

Proof state:
𝕂 : Type u_1
m : Type u_2
𝔸 : Type u_5
inst✝⁵ : RCLike 𝕂
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
U : (Matrix m m 𝔸)ˣ
A : Matrix m m 𝔸
this✝ : SeminormedRing (Matrix m m 𝔸) := Matrix.linftyOpSemiNormedRing
this : NormedRing (Matrix m m 𝔸) := Matrix.linftyOpNormedRing
⊢ exp 𝕂 (↑U * A * ↑U⁻¹) = ↑U * exp 𝕂 A * ↑U⁻¹

Tactic:
letI : NormedAlgebra 𝕂 (Matrix m m 𝔸) := Matrix.linftyOpNormedAlgebra

Result:
𝕂 : Type u_1
m : Type u_2
𝔸 : Type u_5
inst✝⁵ : RCLike 𝕂
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
U : (Matrix m m 𝔸)ˣ
A : Matrix m m 𝔸
this✝¹ : SeminormedRing (Matrix m m 𝔸) := Matrix.linftyOpSemiNormedRing
this✝ : NormedRing (Matrix m m 𝔸) := Matrix.linftyOpNormedRing
this : NormedAlgebra 𝕂 (Matrix m m 𝔸) := Matrix.linftyOpNormedAlgebra
⊢ exp 𝕂 (↑U * A * ↑U⁻¹) = ↑U * exp 𝕂 A * ↑U⁻¹

Proof state:
𝕂 : Type u_1
m : Type u_2
𝔸 : Type u_5
inst✝⁵ : RCLike 𝕂
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
U : (Matrix m m 𝔸)ˣ
A : Matrix m m 𝔸
⊢ exp 𝕂 (↑U * A * ↑U⁻¹) = ↑U * exp 𝕂 A * ↑U⁻¹

Tactic:
letI : SeminormedRing (Matrix m m 𝔸) := Matrix.linftyOpSemiNormedRing

Result:
𝕂 : Type u_1
m : Type u_2
𝔸 : Type u_5
inst✝⁵ : RCLike 𝕂
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
U : (Matrix m m 𝔸)ˣ
A : Matrix m m 𝔸
this : SeminormedRing (Matrix m m 𝔸) := Matrix.linftyOpSemiNormedRing
⊢ exp 𝕂 (↑U * A * ↑U⁻¹) = ↑U * exp 𝕂 A * ↑U⁻¹

Proof state:
𝕂 : Type u_1
m : Type u_2
𝔸 : Type u_5
inst✝⁵ : RCLike 𝕂
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
U : (Matrix m m 𝔸)ˣ
A : Matrix m m 𝔸
this✝¹ : SeminormedRing (Matrix m m 𝔸) := Matrix.linftyOpSemiNormedRing
this✝ : NormedRing (Matrix m m 𝔸) := Matrix.linftyOpNormedRing
this : NormedAlgebra 𝕂 (Matrix m m 𝔸) := Matrix.linftyOpNormedAlgebra
⊢ exp 𝕂 (↑U * A * ↑U⁻¹) = ↑U * exp 𝕂 A * ↑U⁻¹

Tactic:
exact exp_units_conj _ U A

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValue?_insertEntry_self [BEq α] [EquivBEq α] {l : List ((_ : α) × β)} {k : α} {v : β} :
    getValue? k (insertEntry k v l) = some v

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × β)
k : α
v : β
⊢ getValue? k (insertEntry k v l) = some v

Tactic:
simp [getValue?_insertEntry]

Result:
no goals
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem half_lt_self_iff : a / 2 < a ↔ 0 < a

Proof state:
α : Type u_2
inst✝ : LinearOrderedSemifield α
a : α
⊢ a / 2 < a ↔ 0 < a

Tactic:
rw [div_lt_iff₀ (zero_lt_two' α), mul_two, lt_add_iff_pos_left]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem map_id_fun : map (n := n) (id : α → α) = id

Proof state:
n : Nat
α : Type u_1
⊢ map id = id

Tactic:
funext l

Result:
case h
n : Nat
α : Type u_1
l : Vector α n
⊢ map id l = id l

Proof state:
case h
n : Nat
α : Type u_1
l : Vector α n
⊢ map id l = id l

Tactic:
induction l <;> simp_all

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Zip.lean
theorem zip_eq_zipWith : ∀ (l₁ : List α) (l₂ : List β), zip l₁ l₂ = zipWith Prod.mk l₁ l₂
  | [], _ => rfl
  | _, [] => rfl
  | a :: l₁, b :: l₂ => by simp [zip_cons_cons, zip_eq_zipWith l₁ l₂]

Proof state:
α : Type u_1
β : Type u_2
a : α
l₁ : List α
b : β
l₂ : List β
⊢ (a :: l₁).zip (b :: l₂) = zipWith Prod.mk (a :: l₁) (b :: l₂)

Tactic:
simp [zip_cons_cons, zip_eq_zipWith l₁ l₂]

Result:
no goals
-- Mathlib/Algebra/Order/Ring/WithTop.lean
protected lemma pow_right_strictMono : ∀ {n : ℕ}, n ≠ 0 → StrictMono fun a : WithTop α ↦ a ^ n
  | 0, h => absurd rfl h
  | 1, _ => by simpa only [pow_one] using strictMono_id
  | n + 2, _ => fun x y h ↦ by
    simp_rw [pow_succ _ (n + 1)]
    exact WithTop.mul_lt_mul (WithTop.pow_right_strictMono n.succ_ne_zero h) h

Proof state:
α : Type u_1
inst✝⁶ : DecidableEq α
inst✝⁵ : CommSemiring α
inst✝⁴ : PartialOrder α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : PosMulStrictMono α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
x✝ : 1 ≠ 0
⊢ StrictMono fun a => a ^ 1

Tactic:
simpa only [pow_one] using strictMono_id

Result:
no goals

Proof state:
α : Type u_1
inst✝⁶ : DecidableEq α
inst✝⁵ : CommSemiring α
inst✝⁴ : PartialOrder α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : PosMulStrictMono α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
n : ℕ
x✝ : n + 2 ≠ 0
x y : WithTop α
h : x < y
⊢ (fun a => a ^ (n + 2)) x < (fun a => a ^ (n + 2)) y

Tactic:
simp_rw [pow_succ _ (n + 1)]

Result:
α : Type u_1
inst✝⁶ : DecidableEq α
inst✝⁵ : CommSemiring α
inst✝⁴ : PartialOrder α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : PosMulStrictMono α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
n : ℕ
x✝ : n + 2 ≠ 0
x y : WithTop α
h : x < y
⊢ x ^ (n + 1) * x < y ^ (n + 1) * y

Proof state:
α : Type u_1
inst✝⁶ : DecidableEq α
inst✝⁵ : CommSemiring α
inst✝⁴ : PartialOrder α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : PosMulStrictMono α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
n : ℕ
x✝ : n + 2 ≠ 0
x y : WithTop α
h : x < y
⊢ x ^ (n + 1) * x < y ^ (n + 1) * y

Tactic:
exact WithTop.mul_lt_mul (WithTop.pow_right_strictMono n.succ_ne_zero h) h

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem add_compLpL [Fact (1 ≤ p)] (L L' : E →L[𝕜] F) :
    (L + L').compLpL p μ = L.compLpL p μ + L'.compLpL p μ

Proof state:
case h
α : Type u_1
E : Type u_4
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
𝕜 : Type u_7
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜 F
inst✝ : Fact (1 ≤ p)
L L' : E →L[𝕜] F
f : ↥(Lp E p μ)
⊢ (compLpL p μ (L + L')) f = (compLpL p μ L + compLpL p μ L') f

Tactic:
exact add_compLp L L' f

Result:
no goals

Proof state:
α : Type u_1
E : Type u_4
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
𝕜 : Type u_7
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜 F
inst✝ : Fact (1 ≤ p)
L L' : E →L[𝕜] F
⊢ compLpL p μ (L + L') = compLpL p μ L + compLpL p μ L'

Tactic:
ext1 f

Result:
case h
α : Type u_1
E : Type u_4
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
𝕜 : Type u_7
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜 F
inst✝ : Fact (1 ≤ p)
L L' : E →L[𝕜] F
f : ↥(Lp E p μ)
⊢ (compLpL p μ (L + L')) f = (compLpL p μ L + compLpL p μ L') f
-- Mathlib/RingTheory/Binomial.lean
theorem choose_add_smul_choose [NatPowAssoc R] (r : R) (n k : ℕ) :
    (Nat.choose (n + k) k) • choose (r + k) (n + k) = choose (r + k) k * choose r n

Proof state:
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
r : R
n k : ℕ
⊢ (n + k).choose k • choose (r + ↑k) (n + k) = choose (r + ↑k) k * choose r n

Tactic:
rw [choose_smul_choose (r + k) (Nat.le_add_left k n), Nat.add_sub_cancel,
  add_sub_cancel_right]

Result:
no goals
-- Mathlib/Data/Int/Init.lean
lemma inductionOn'_self : b.inductionOn' b H0 Hs Hp = H0 :=
  cast_eq_iff_heq.mpr <| .symm <| by rw [b.sub_self, ← cast_eq_iff_heq]; rfl

Proof state:
C : ℤ → Sort u_1
b : ℤ
H0 : C b
Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)
Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)
⊢ HEq H0
    (match b - b with
    | ofNat n => inductionOn'.pos b H0 Hs n
    | -[n+1] => inductionOn'.neg b H0 Hp n)

Tactic:
rw [b.sub_self, ← cast_eq_iff_heq]

Result:
C : ℤ → Sort u_1
b : ℤ
H0 : C b
Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)
Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)
⊢ cast ?m.13031 H0 =
    match 0 with
    | ofNat n => inductionOn'.pos b H0 Hs n
    | -[n+1] => inductionOn'.neg b H0 Hp n

C : ℤ → Sort u_1
b : ℤ
H0 : C b
Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)
Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)
⊢ C b = (fun x => C x) (b + 0)

Proof state:
C : ℤ → Sort u_1
b : ℤ
H0 : C b
Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)
Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)
⊢ cast ?m.13031 H0 =
    match 0 with
    | ofNat n => inductionOn'.pos b H0 Hs n
    | -[n+1] => inductionOn'.neg b H0 Hp n

C : ℤ → Sort u_1
b : ℤ
H0 : C b
Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)
Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)
⊢ C b = (fun x => C x) (b + 0)

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Ring/Parity.lean
@[parity_simps] lemma odd_sub (h : n ≤ m) : Odd (m - n) ↔ (Odd m ↔ Even n)

Proof state:
m n : ℕ
h : n ≤ m
⊢ Odd (m - n) ↔ (Odd m ↔ Even n)

Tactic:
rw [← not_even_iff_odd, even_sub h, not_iff, ← not_even_iff_odd]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem exists_push_of_ne_empty {xs : Array α} (h : xs ≠ #[]) :
    ∃ (ys : Array α) (a : α), xs = ys.push a

Proof state:
case mk
α : Type u_1
xs : List α
h : ¬xs = []
⊢ ∃ ys a, { toList := xs } = ys.push a

Tactic:
exact ⟨(xs.take (xs.length - 1)).toArray, xs.getLast h, by simp⟩

Result:
no goals

Proof state:
case mk
α : Type u_1
xs : List α
h : { toList := xs } ≠ #[]
⊢ ∃ ys a, { toList := xs } = ys.push a

Tactic:
simp only [ne_eq, mk.injEq] at h

Result:
case mk
α : Type u_1
xs : List α
h : ¬xs = []
⊢ ∃ ys a, { toList := xs } = ys.push a

Proof state:
α : Type u_1
xs : List α
h : ¬xs = []
⊢ { toList := xs } = (List.take (xs.length - 1) xs).toArray.push (xs.getLast h)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
xs : Array α
h : xs ≠ #[]
⊢ ∃ ys a, xs = ys.push a

Tactic:
rcases xs with ⟨xs⟩

Result:
case mk
α : Type u_1
xs : List α
h : { toList := xs } ≠ #[]
⊢ ∃ ys a, { toList := xs } = ys.push a
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem dvd_antisymm {a b : Int} (H1 : 0 ≤ a) (H2 : 0 ≤ b) : a ∣ b → b ∣ a → a = b

Proof state:
a b : Int
H1 : 0 ≤ a
H2 : 0 ≤ b
⊢ a.natAbs ∣ b.natAbs → b.natAbs ∣ a.natAbs → a.natAbs = b.natAbs

Tactic:
apply Nat.dvd_antisymm

Result:
no goals

Proof state:
a b : Int
H1 : 0 ≤ a
H2 : 0 ≤ b
⊢ ↑a.natAbs ∣ ↑b.natAbs → ↑b.natAbs ∣ ↑a.natAbs → ↑a.natAbs = ↑b.natAbs

Tactic:
rw [ofNat_dvd, ofNat_dvd, ofNat_inj]

Result:
a b : Int
H1 : 0 ≤ a
H2 : 0 ≤ b
⊢ a.natAbs ∣ b.natAbs → b.natAbs ∣ a.natAbs → a.natAbs = b.natAbs

Proof state:
a b : Int
H1 : 0 ≤ a
H2 : 0 ≤ b
⊢ a ∣ b → b ∣ a → a = b

Tactic:
rw [← natAbs_of_nonneg H1, ← natAbs_of_nonneg H2]

Result:
a b : Int
H1 : 0 ≤ a
H2 : 0 ≤ b
⊢ ↑a.natAbs ∣ ↑b.natAbs → ↑b.natAbs ∣ ↑a.natAbs → ↑a.natAbs = ↑b.natAbs
-- Mathlib/Data/PNat/Xgcd.lean
theorem step_isSpecial (hs : u.IsSpecial) : u.step.IsSpecial

Proof state:
u : XgcdType
hs : u.wp + u.zp + u.wp * u.zp = u.x * u.y
⊢ u.y * u.q + u.zp + u.wp + (u.y * u.q + u.zp) * u.wp = u.y * ((u.wp + 1) * u.q + u.x)

Tactic:
rw [mul_add, mul_comm u.y u.x, ← hs]

Result:
u : XgcdType
hs : u.wp + u.zp + u.wp * u.zp = u.x * u.y
⊢ u.y * u.q + u.zp + u.wp + (u.y * u.q + u.zp) * u.wp = u.y * ((u.wp + 1) * u.q) + (u.wp + u.zp + u.wp * u.zp)

Proof state:
u : XgcdType
hs : u.wp + u.zp + u.wp * u.zp = u.x * u.y
⊢ u.y * u.q + u.zp + u.wp + (u.y * u.q + u.zp) * u.wp = u.y * ((u.wp + 1) * u.q) + (u.wp + u.zp + u.wp * u.zp)

Tactic:
ring

Result:
no goals

Proof state:
u : XgcdType
hs : u.IsSpecial
⊢ u.step.IsSpecial

Tactic:
dsimp [IsSpecial, step] at hs ⊢

Result:
u : XgcdType
hs : u.wp + u.zp + u.wp * u.zp = u.x * u.y
⊢ u.y * u.q + u.zp + u.wp + (u.y * u.q + u.zp) * u.wp = u.y * ((u.wp + 1) * u.q + u.x)
-- Mathlib/RingTheory/HopfAlgebra/Basic.lean
@[simp]
lemma sum_antipode_mul_eq {a : A} (repr : Repr R a) :
    ∑ i ∈ repr.index, antipode (R := R) (repr.left i) * repr.right i =
      algebraMap R A (counit a)

Proof state:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
a : A
repr : Coalgebra.Repr R a
⊢ ∑ i ∈ repr.index, antipode (repr.left i) * repr.right i = (algebraMap R A) (counit a)

Tactic:
simpa [← repr.eq, map_sum] using congr($(mul_antipode_rTensor_comul (R := R)) a)

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Associated.lean
theorem map {M N : Type*} [Monoid M] [Monoid N] {F : Type*} [FunLike F M N] [MonoidHomClass F M N]
    (f : F) {x y : M} (ha : Associated x y) : Associated (f x) (f y)

Proof state:
M : Type u_2
N : Type u_3
inst✝³ : Monoid M
inst✝² : Monoid N
F : Type u_4
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
f : F
x y : M
u : Mˣ
ha : x * ↑u = y
⊢ f x * ↑((Units.map ↑f) u) = f y

Tactic:
rw [← ha, map_mul, Units.coe_map, MonoidHom.coe_coe]

Result:
no goals

Proof state:
case intro
M : Type u_2
N : Type u_3
inst✝³ : Monoid M
inst✝² : Monoid N
F : Type u_4
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
f : F
x y : M
u : Mˣ
ha : x * ↑u = y
⊢ f x ~ᵤ f y

Tactic:
exact ⟨Units.map f u, by rw [← ha, map_mul, Units.coe_map, MonoidHom.coe_coe]⟩

Result:
no goals

Proof state:
M : Type u_2
N : Type u_3
inst✝³ : Monoid M
inst✝² : Monoid N
F : Type u_4
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
f : F
x y : M
ha : x ~ᵤ y
⊢ f x ~ᵤ f y

Tactic:
obtain ⟨u, ha⟩ := ha

Result:
case intro
M : Type u_2
N : Type u_3
inst✝³ : Monoid M
inst✝² : Monoid N
F : Type u_4
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
f : F
x y : M
u : Mˣ
ha : x * ↑u = y
⊢ f x ~ᵤ f y
-- Mathlib/RingTheory/Spectrum/Prime/FreeLocus.lean
lemma isOpen_freeLocus [Module.FinitePresentation R M] :
    IsOpen (freeLocus R M)

Proof state:
R : Type uR
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : FinitePresentation R M
x : PrimeSpectrum R
hx : x ∈ freeLocus R M
this : Free (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
⊢ ∃ t ⊆ freeLocus R M, IsOpen t ∧ x ∈ t

Tactic:
obtain ⟨r, hr, hr', _⟩ := Module.FinitePresentation.exists_free_localizedModule_powers
  x.asIdeal.primeCompl (LocalizedModule.mkLinearMap x.asIdeal.primeCompl M)
  (Localization.AtPrime x.asIdeal)

Result:
case intro.intro.intro
R : Type uR
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : FinitePresentation R M
x : PrimeSpectrum R
hx : x ∈ freeLocus R M
this : Free (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
r : R
hr : r ∈ x.asIdeal.primeCompl
hr' : Free (Localization (Submonoid.powers r)) (LocalizedModule (Submonoid.powers r) M)
right✝ :
  finrank (Localization (Submonoid.powers r)) (LocalizedModule (Submonoid.powers r) M) =
    finrank (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
⊢ ∃ t ⊆ freeLocus R M, IsOpen t ∧ x ∈ t

Proof state:
R : Type uR
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : FinitePresentation R M
⊢ IsOpen (freeLocus R M)

Tactic:
refine isOpen_iff_forall_mem_open.mpr fun x hx ↦ ?_

Result:
R : Type uR
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : FinitePresentation R M
x : PrimeSpectrum R
hx : x ∈ freeLocus R M
⊢ ∃ t ⊆ freeLocus R M, IsOpen t ∧ x ∈ t

Proof state:
R : Type uR
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : FinitePresentation R M
x : PrimeSpectrum R
hx : x ∈ freeLocus R M
⊢ ∃ t ⊆ freeLocus R M, IsOpen t ∧ x ∈ t

Tactic:
have : Module.Free _ _ := hx

Result:
R : Type uR
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : FinitePresentation R M
x : PrimeSpectrum R
hx : x ∈ freeLocus R M
this : Free (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
⊢ ∃ t ⊆ freeLocus R M, IsOpen t ∧ x ∈ t

Proof state:
case intro.intro.intro
R : Type uR
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : FinitePresentation R M
x : PrimeSpectrum R
hx : x ∈ freeLocus R M
this : Free (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
r : R
hr : r ∈ x.asIdeal.primeCompl
hr' : Free (Localization (Submonoid.powers r)) (LocalizedModule (Submonoid.powers r) M)
right✝ :
  finrank (Localization (Submonoid.powers r)) (LocalizedModule (Submonoid.powers r) M) =
    finrank (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
⊢ ∃ t ⊆ freeLocus R M, IsOpen t ∧ x ∈ t

Tactic:
exact ⟨basicOpen r, basicOpen_subset_freeLocus_iff.mpr inferInstance, (basicOpen r).2, hr⟩

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Hermite/Gaussian.lean
theorem hermite_eq_deriv_gaussian (n : ℕ) (x : ℝ) : aeval x (hermite n) =
    (-1 : ℝ) ^ n * deriv^[n] (fun y => Real.exp (-(y ^ 2 / 2))) x / Real.exp (-(x ^ 2 / 2))

Proof state:
n : ℕ
x : ℝ
⊢ -1 ≠ 0

Tactic:
norm_num

Result:
no goals

Proof state:
n : ℕ
x : ℝ
⊢ (aeval x) (hermite n) * Real.exp (-x ^ 2 / 2) = (-1) ^ n * ((-1) ^ n * (aeval x) (hermite n) * Real.exp (-x ^ 2 / 2))

Tactic:
rw [← @smul_eq_mul ℝ _ ((-1) ^ n), ← inv_smul_eq_iff₀, mul_assoc, smul_eq_mul, ← inv_pow, ←
  neg_inv, inv_one]

Result:
case ha
n : ℕ
x : ℝ
⊢ (-1) ^ n ≠ 0

Proof state:
n : ℕ
x : ℝ
⊢ (aeval x) (hermite n) = (-1) ^ n * deriv^[n] (fun y => Real.exp (-(y ^ 2 / 2))) x / Real.exp (-(x ^ 2 / 2))

Tactic:
rw [deriv_gaussian_eq_hermite_mul_gaussian]

Result:
n : ℕ
x : ℝ
⊢ (aeval x) (hermite n) =
    (-1) ^ n * ((-1) ^ n * (aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2))) / Real.exp (-(x ^ 2 / 2))

Proof state:
n : ℕ
x : ℝ
⊢ (aeval x) (hermite n) =
    (-1) ^ n * ((-1) ^ n * (aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2))) / Real.exp (-(x ^ 2 / 2))

Tactic:
field_simp [Real.exp_ne_zero]

Result:
n : ℕ
x : ℝ
⊢ (aeval x) (hermite n) * Real.exp (-x ^ 2 / 2) = (-1) ^ n * ((-1) ^ n * (aeval x) (hermite n) * Real.exp (-x ^ 2 / 2))

Proof state:
case ha
n : ℕ
x : ℝ
⊢ (-1) ^ n ≠ 0

Tactic:
exact pow_ne_zero _ (by norm_num)

Result:
no goals
-- Mathlib/CategoryTheory/IsConnected.lean
theorem isPreconnected_of_zigzag (h : ∀ j₁ j₂ : J, ∃ l,
    List.Chain Zag j₁ l ∧ List.getLast (j₁ :: l) (List.cons_ne_nil _ _) = j₂) :
    IsPreconnected J

Proof state:
case h
J : Type u₁
inst✝ : Category.{v₁, u₁} J
h : ∀ (j₁ j₂ : J), ∃ l, List.Chain Zag j₁ l ∧ (j₁ :: l).getLast ⋯ = j₂
j₁ j₂ : J
⊢ Zigzag j₁ j₂

Tactic:
rcases h j₁ j₂ with ⟨l, hl₁, hl₂⟩

Result:
case h.intro.intro
J : Type u₁
inst✝ : Category.{v₁, u₁} J
h : ∀ (j₁ j₂ : J), ∃ l, List.Chain Zag j₁ l ∧ (j₁ :: l).getLast ⋯ = j₂
j₁ j₂ : J
l : List J
hl₁ : List.Chain Zag j₁ l
hl₂ : (j₁ :: l).getLast ⋯ = j₂
⊢ Zigzag j₁ j₂

Proof state:
case h
J : Type u₁
inst✝ : Category.{v₁, u₁} J
h : ∀ (j₁ j₂ : J), ∃ l, List.Chain Zag j₁ l ∧ (j₁ :: l).getLast ⋯ = j₂
⊢ ∀ (j₁ j₂ : J), Zigzag j₁ j₂

Tactic:
intro j₁ j₂

Result:
case h
J : Type u₁
inst✝ : Category.{v₁, u₁} J
h : ∀ (j₁ j₂ : J), ∃ l, List.Chain Zag j₁ l ∧ (j₁ :: l).getLast ⋯ = j₂
j₁ j₂ : J
⊢ Zigzag j₁ j₂

Proof state:
case h.intro.intro
J : Type u₁
inst✝ : Category.{v₁, u₁} J
h : ∀ (j₁ j₂ : J), ∃ l, List.Chain Zag j₁ l ∧ (j₁ :: l).getLast ⋯ = j₂
j₁ j₂ : J
l : List J
hl₁ : List.Chain Zag j₁ l
hl₂ : (j₁ :: l).getLast ⋯ = j₂
⊢ Zigzag j₁ j₂

Tactic:
apply List.relationReflTransGen_of_exists_chain l hl₁ hl₂

Result:
no goals

Proof state:
J : Type u₁
inst✝ : Category.{v₁, u₁} J
h : ∀ (j₁ j₂ : J), ∃ l, List.Chain Zag j₁ l ∧ (j₁ :: l).getLast ⋯ = j₂
⊢ IsPreconnected J

Tactic:
apply zigzag_isPreconnected

Result:
case h
J : Type u₁
inst✝ : Category.{v₁, u₁} J
h : ∀ (j₁ j₂ : J), ∃ l, List.Chain Zag j₁ l ∧ (j₁ :: l).getLast ⋯ = j₂
⊢ ∀ (j₁ j₂ : J), Zigzag j₁ j₂
-- Mathlib/Algebra/Homology/ShortComplex/Exact.lean
lemma Exact.epi_f' (hS : S.Exact) (h : LeftHomologyData S) : Epi h.f' :=
  epi_of_isZero_cokernel' _ h.hπ (by
    haveI := hS.hasHomology
    dsimp
    simpa only [← h.exact_iff] using hS)

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
h : S.LeftHomologyData
this : S.HasHomology
⊢ IsZero h.H

Tactic:
simpa only [← h.exact_iff] using hS

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
h : S.LeftHomologyData
⊢ IsZero (CokernelCofork.ofπ h.π ⋯).pt

Tactic:
haveI := hS.hasHomology

Result:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
h : S.LeftHomologyData
this : S.HasHomology
⊢ IsZero (CokernelCofork.ofπ h.π ⋯).pt

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
h : S.LeftHomologyData
this : S.HasHomology
⊢ IsZero (CokernelCofork.ofπ h.π ⋯).pt

Tactic:
dsimp

Result:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
h : S.LeftHomologyData
this : S.HasHomology
⊢ IsZero h.H
-- Mathlib/RingTheory/MvPolynomial/Homogeneous.lean
theorem coeff_eq_zero (hφ : IsHomogeneous φ n) {d : σ →₀ ℕ} (hd : d.degree ≠ n) :
    coeff d φ = 0

Proof state:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
d : σ →₀ ℕ
hd : d.degree ≠ n
⊢ coeff d φ = 0

Tactic:
rw [degree_eq_weight_one] at hd

Result:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
d : σ →₀ ℕ
hd : (weight fun x => 1) d ≠ n
⊢ coeff d φ = 0

Proof state:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
d : σ →₀ ℕ
hd : (weight fun x => 1) d ≠ n
⊢ coeff d φ = 0

Tactic:
exact IsWeightedHomogeneous.coeff_eq_zero hφ d hd

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean
lemma mul_nonpos_iff_pos_imp_nonpos [PosMulStrictMono α] [MulPosStrictMono α]
    [AddLeftMono α] [AddLeftReflectLE α] :
    a * b ≤ 0 ↔ (0 < a → b ≤ 0) ∧ (b < 0 → 0 ≤ a)

Proof state:
α : Type u
inst✝⁵ : Ring α
inst✝⁴ : LinearOrder α
a b : α
inst✝³ : PosMulStrictMono α
inst✝² : MulPosStrictMono α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
⊢ a * b ≤ 0 ↔ (0 < a → b ≤ 0) ∧ (b < 0 → 0 ≤ a)

Tactic:
rw [← neg_nonneg, ← mul_neg, mul_nonneg_iff_pos_imp_nonneg (α := α)]

Result:
α : Type u
inst✝⁵ : Ring α
inst✝⁴ : LinearOrder α
a b : α
inst✝³ : PosMulStrictMono α
inst✝² : MulPosStrictMono α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
⊢ (0 < a → 0 ≤ -b) ∧ (0 < -b → 0 ≤ a) ↔ (0 < a → b ≤ 0) ∧ (b < 0 → 0 ≤ a)

Proof state:
α : Type u
inst✝⁵ : Ring α
inst✝⁴ : LinearOrder α
a b : α
inst✝³ : PosMulStrictMono α
inst✝² : MulPosStrictMono α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
⊢ (0 < a → 0 ≤ -b) ∧ (0 < -b → 0 ≤ a) ↔ (0 < a → b ≤ 0) ∧ (b < 0 → 0 ≤ a)

Tactic:
simp only [neg_pos, neg_nonneg]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Set/Basic.lean
theorem univ_pow : ∀ {n : ℕ}, n ≠ 0 → (univ : Set α) ^ n = univ
  | 0 => fun h => (h rfl).elim
  | 1 => fun _ => pow_one _
  | n + 2 => fun _ => by rw [pow_succ, univ_pow n.succ_ne_zero, univ_mul_univ]

Proof state:
α : Type u_2
inst✝ : Monoid α
n : ℕ
x✝ : n + 2 ≠ 0
⊢ univ ^ (n + 2) = univ

Tactic:
rw [pow_succ, univ_pow n.succ_ne_zero, univ_mul_univ]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma CFC.eq_one_of_spectrum_subset_one (h_spec : spectrum R a ⊆ {1}) (ha : p a

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
a : A
h_spec : spectrum R a ⊆ {1}
ha : autoParam (p a) _auto✝
⊢ a = 1

Tactic:
simpa using eq_algebraMap_of_spectrum_subset_singleton a 1 h_spec

Result:
no goals