harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Nat/Digits.lean
theorem sub_one_mul_sum_div_pow_eq_sub_sum_digits {p : ℕ}
    (L : List ℕ) {h_nonempty} (h_ne_zero : L.getLast h_nonempty ≠ 0) (h_lt : ∀ l ∈ L, l < p) :
    (p - 1) * ∑ i ∈ range L.length, (ofDigits p L) / p ^ i.succ = (ofDigits p L) - L.sum

Proof state:
case inl.cons.inr
p : ℕ
h : 1 < p
hd : ℕ
tl : List ℕ
ih✝ :
  ∀ {h_nonempty : tl ≠ []},
    tl.getLast h_nonempty ≠ 0 →
      (∀ l ∈ tl, l < p) → (p - 1) * ∑ i ∈ range tl.length, ofDigits p tl / p ^ i.succ = ofDigits p tl - tl.sum
h_nonempty : hd :: tl ≠ []
h_ne_zero : (hd :: tl).getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ hd :: tl, l < p
h' : ¬tl = []
w₁' : ∀ l ∈ tl, l < p
w₂' : ∀ (h : tl ≠ []), tl.getLast h ≠ 0
ih : (p - 1) * ∑ x ∈ range tl.length, ofDigits p (List.drop (1 + x) tl) = ofDigits p tl - tl.sum
this : ∑ x ∈ Ico tl.length (tl.length + 1), ofDigits p (List.drop x tl) = 0
h₁ : 1 ≤ tl.length
⊢ (p - 1) * ofDigits p tl + ofDigits p tl - tl.sum = hd + p * ofDigits p tl - (hd + tl.sum)

Tactic:
nth_rw 2 [← one_mul <| ofDigits p tl]

Result:
case inl.cons.inr
p : ℕ
h : 1 < p
hd : ℕ
tl : List ℕ
ih✝ :
  ∀ {h_nonempty : tl ≠ []},
    tl.getLast h_nonempty ≠ 0 →
      (∀ l ∈ tl, l < p) → (p - 1) * ∑ i ∈ range tl.length, ofDigits p tl / p ^ i.succ = ofDigits p tl - tl.sum
h_nonempty : hd :: tl ≠ []
h_ne_zero : (hd :: tl).getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ hd :: tl, l < p
h' : ¬tl = []
w₁' : ∀ l ∈ tl, l < p
w₂' : ∀ (h : tl ≠ []), tl.getLast h ≠ 0
ih : (p - 1) * ∑ x ∈ range tl.length, ofDigits p (List.drop (1 + x) tl) = ofDigits p tl - tl.sum
this : ∑ x ∈ Ico tl.length (tl.length + 1), ofDigits p (List.drop x tl) = 0
h₁ : 1 ≤ tl.length
⊢ (p - 1) * ofDigits p tl + 1 * ofDigits p tl - tl.sum = hd + p * ofDigits p tl - (hd + tl.sum)

Proof state:
case inl.nil
p : ℕ
h : 1 < p
h_nonempty : [] ≠ []
h_ne_zero : [].getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ [], l < p
⊢ (p - 1) * ∑ i ∈ range [].length, ofDigits p [] / p ^ i.succ = ofDigits p [] - [].sum

Tactic:
simp [ofDigits]

Result:
no goals
-- Mathlib/Topology/Algebra/Module/FiniteDimension.lean
theorem FiniteDimensional.complete [FiniteDimensional 𝕜 E] : CompleteSpace E

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : CompleteSpace 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : UniformSpace E
inst✝⁴ : T2Space E
inst✝³ : UniformAddGroup E
inst✝² : Module 𝕜 E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
e : E ≃L[𝕜] Fin (finrank 𝕜 E) → 𝕜 := ContinuousLinearEquiv.ofFinrankEq ⋯
⊢ CompleteSpace E

Tactic:
have : IsUniformEmbedding e.toEquiv.symm := e.symm.isUniformEmbedding

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : CompleteSpace 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : UniformSpace E
inst✝⁴ : T2Space E
inst✝³ : UniformAddGroup E
inst✝² : Module 𝕜 E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
e : E ≃L[𝕜] Fin (finrank 𝕜 E) → 𝕜 := ContinuousLinearEquiv.ofFinrankEq ⋯
this : IsUniformEmbedding ⇑e.toEquiv.symm
⊢ CompleteSpace E

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : CompleteSpace 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : UniformSpace E
inst✝⁴ : T2Space E
inst✝³ : UniformAddGroup E
inst✝² : Module 𝕜 E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
⊢ CompleteSpace E

Tactic:
set e := ContinuousLinearEquiv.ofFinrankEq (@finrank_fin_fun 𝕜 _ _ (finrank 𝕜 E)).symm

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : CompleteSpace 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : UniformSpace E
inst✝⁴ : T2Space E
inst✝³ : UniformAddGroup E
inst✝² : Module 𝕜 E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
e : E ≃L[𝕜] Fin (finrank 𝕜 E) → 𝕜 := ContinuousLinearEquiv.ofFinrankEq ⋯
⊢ CompleteSpace E

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : CompleteSpace 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : UniformSpace E
inst✝⁴ : T2Space E
inst✝³ : UniformAddGroup E
inst✝² : Module 𝕜 E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
e : E ≃L[𝕜] Fin (finrank 𝕜 E) → 𝕜 := ContinuousLinearEquiv.ofFinrankEq ⋯
this : IsUniformEmbedding ⇑e.toEquiv.symm
⊢ CompleteSpace E

Tactic:
exact (completeSpace_congr this).1 inferInstance

Result:
no goals
-- Mathlib/Data/Matroid/Circuit.lean
lemma IsCircuit.isCocircuit_disjoint_or_nontrivial_inter (hC : M.IsCircuit C)
    (hK : M.IsCocircuit K) : Disjoint C K ∨ (C ∩ K).Nontrivial

Proof state:
α : Type u_1
M : Matroid α
C K : Set α
hC : M.IsCircuit C
hK : M.IsCocircuit K
⊢ Disjoint C K ∨ (C ∩ K).Nontrivial

Tactic:
rw [or_iff_not_imp_left, disjoint_iff_inter_eq_empty, ← ne_eq, ← nonempty_iff_ne_empty]

Result:
α : Type u_1
M : Matroid α
C K : Set α
hC : M.IsCircuit C
hK : M.IsCocircuit K
⊢ (C ∩ K).Nonempty → (C ∩ K).Nontrivial

Proof state:
α : Type u_1
M : Matroid α
C K : Set α
hC : M.IsCircuit C
hK : M.IsCocircuit K
⊢ (C ∩ K).Nonempty → (C ∩ K).Nontrivial

Tactic:
exact hC.isCocircuit_inter_nontrivial hK

Result:
no goals
-- Mathlib/RingTheory/Norm/Transitivity.lean
lemma auxMat_toSquareBlock_eq : (auxMat M k).toSquareBlock (· ≠ k) False = 1

Proof state:
case a.mk.mk
S : Type u_2
m : Type u_5
inst✝¹ : CommRing S
M : Matrix m m S
inst✝ : DecidableEq m
k i : m
hi : (i ≠ k) = False
j : m
hj : (j ≠ k) = False
⊢ (auxMat M k).toSquareBlock (fun x => x ≠ k) False ⟨i, hi⟩ ⟨j, hj⟩ = 1 ⟨i, hi⟩ ⟨j, hj⟩

Tactic:
rw [eq_iff_iff, iff_false, not_not] at hi hj

Result:
case a.mk.mk
S : Type u_2
m : Type u_5
inst✝¹ : CommRing S
M : Matrix m m S
inst✝ : DecidableEq m
k i : m
hi✝ : (i ≠ k) = False
hi : i = k
j : m
hj✝ : (j ≠ k) = False
hj : j = k
⊢ (auxMat M k).toSquareBlock (fun x => x ≠ k) False ⟨i, hi✝⟩ ⟨j, hj✝⟩ = 1 ⟨i, hi✝⟩ ⟨j, hj✝⟩

Proof state:
S : Type u_2
m : Type u_5
inst✝¹ : CommRing S
M : Matrix m m S
inst✝ : DecidableEq m
k : m
⊢ (auxMat M k).toSquareBlock (fun x => x ≠ k) False = 1

Tactic:
ext ⟨i, hi⟩ ⟨j, hj⟩

Result:
case a.mk.mk
S : Type u_2
m : Type u_5
inst✝¹ : CommRing S
M : Matrix m m S
inst✝ : DecidableEq m
k i : m
hi : (i ≠ k) = False
j : m
hj : (j ≠ k) = False
⊢ (auxMat M k).toSquareBlock (fun x => x ≠ k) False ⟨i, hi⟩ ⟨j, hj⟩ = 1 ⟨i, hi⟩ ⟨j, hj⟩

Proof state:
case a.mk.mk
S : Type u_2
m : Type u_5
inst✝¹ : CommRing S
M : Matrix m m S
inst✝ : DecidableEq m
k i : m
hi✝ : (i ≠ k) = False
hi : i = k
j : m
hj✝ : (j ≠ k) = False
hj : j = k
⊢ (auxMat M k).toSquareBlock (fun x => x ≠ k) False ⟨i, hi✝⟩ ⟨j, hj✝⟩ = 1 ⟨i, hi✝⟩ ⟨j, hj✝⟩

Tactic:
simp [auxMat, toSquareBlock_def, if_pos hi, if_pos hj, Matrix.one_apply, if_pos (hj ▸ hi)]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem sin_sq_pi_over_two_pow_succ (n : ℕ) :
    sin (π / 2 ^ (n + 2)) ^ 2 = 1 / 2 - sqrtTwoAddSeries 0 n / 4

Proof state:
n : ℕ
⊢ sin (π / 2 ^ (n + 2)) ^ 2 = 1 / 2 - sqrtTwoAddSeries 0 n / 4

Tactic:
rw [sin_sq_pi_over_two_pow, sqrtTwoAddSeries, div_pow, sq_sqrt, add_div, ← sub_sub]

Result:
n : ℕ
⊢ 1 - 2 / 2 ^ 2 - sqrtTwoAddSeries 0 n / 2 ^ 2 = 1 / 2 - sqrtTwoAddSeries 0 n / 4

n : ℕ
⊢ 0 ≤ 2 + sqrtTwoAddSeries 0 n

Proof state:
n : ℕ
⊢ 0 ≤ 2 + sqrtTwoAddSeries 0 n

Tactic:
exact add_nonneg two_pos.le (sqrtTwoAddSeries_zero_nonneg _)

Result:
no goals

Proof state:
case e_a
n : ℕ
⊢ 1 - 2 / 2 ^ 2 = 1 / 2

Tactic:
norm_num

Result:
no goals

Proof state:
case e_a.e_a
n : ℕ
⊢ 2 ^ 2 = 4

Tactic:
norm_num

Result:
no goals

Proof state:
n : ℕ
⊢ 1 - 2 / 2 ^ 2 - sqrtTwoAddSeries 0 n / 2 ^ 2 = 1 / 2 - sqrtTwoAddSeries 0 n / 4

Tactic:
congr

Result:
case e_a
n : ℕ
⊢ 1 - 2 / 2 ^ 2 = 1 / 2

case e_a.e_a
n : ℕ
⊢ 2 ^ 2 = 4
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem le_add_iff_sub_le {x y z : BitVec w}
    (hxz : z ≤ x) (hbz : y.toNat + z.toNat < 2^w) :
      x ≤ y + z ↔ x - z ≤ y

Proof state:
w : Nat
x y z : BitVec w
hxz : z.toNat ≤ x.toNat
hbz : y.toNat + z.toNat < 2 ^ w
⊢ z ≤ x

Tactic:
rw [BitVec.le_def]

Result:
w : Nat
x y z : BitVec w
hxz : z.toNat ≤ x.toNat
hbz : y.toNat + z.toNat < 2 ^ w
⊢ z.toNat ≤ x.toNat

Proof state:
w : Nat
x y z : BitVec w
hxz : z.toNat ≤ x.toNat
hbz : y.toNat + z.toNat < 2 ^ w
⊢ x.toNat ≤ y.toNat + z.toNat ↔ x.toNat - z.toNat ≤ y.toNat

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x y z : BitVec w
hxz : z.toNat ≤ x.toNat
hbz : y.toNat + z.toNat < 2 ^ w
⊢ x.toNat ≤ (y + z).toNat ↔ (x - z).toNat ≤ y.toNat

Tactic:
rw [BitVec.toNat_sub_of_le (by rw [BitVec.le_def]; omega),
  BitVec.toNat_add_of_lt (by omega)]

Result:
w : Nat
x y z : BitVec w
hxz : z.toNat ≤ x.toNat
hbz : y.toNat + z.toNat < 2 ^ w
⊢ x.toNat ≤ y.toNat + z.toNat ↔ x.toNat - z.toNat ≤ y.toNat

Proof state:
w : Nat
x y z : BitVec w
hxz : z.toNat ≤ x.toNat
hbz : y.toNat + z.toNat < 2 ^ w
⊢ y.toNat + z.toNat < 2 ^ w

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x y z : BitVec w
hxz : z ≤ x
hbz : y.toNat + z.toNat < 2 ^ w
⊢ x ≤ y + z ↔ x - z ≤ y

Tactic:
simp_all only [BitVec.le_def]

Result:
w : Nat
x y z : BitVec w
hxz : z.toNat ≤ x.toNat
hbz : y.toNat + z.toNat < 2 ^ w
⊢ x.toNat ≤ (y + z).toNat ↔ (x - z).toNat ≤ y.toNat

Proof state:
w : Nat
x y z : BitVec w
hxz : z.toNat ≤ x.toNat
hbz : y.toNat + z.toNat < 2 ^ w
⊢ z.toNat ≤ x.toNat

Tactic:
omega

Result:
no goals
-- Mathlib/SetTheory/Game/Impartial.lean
theorem equiv_iff_add_equiv_zero (H : PGame) : H ≈ G ↔ H + G ≈ 0

Proof state:
G : PGame
inst✝ : G.Impartial
H : PGame
⊢ H ≈ G ↔ H + G ≈ 0

Tactic:
rw [equiv_iff_game_eq, ← add_right_cancel_iff (a := ⟦G⟧), mk'_add_self, ← quot_add,
  equiv_iff_game_eq, quot_zero]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/SchurComplement.lean
theorem invOf_fromBlocks_zero₁₂_eq (A : Matrix m m α) (C : Matrix n m α) (D : Matrix n n α)
    [Invertible A] [Invertible D] [Invertible (fromBlocks A 0 C D)] :
    ⅟ (fromBlocks A 0 C D) = fromBlocks (⅟ A) 0 (-(⅟ D * C * ⅟ A)) (⅟ D)

Proof state:
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : CommRing α
A : Matrix m m α
C : Matrix n m α
D : Matrix n n α
inst✝² : Invertible A
inst✝¹ : Invertible D
inst✝ : Invertible (fromBlocks A 0 C D)
⊢ ⅟(fromBlocks A 0 C D) = fromBlocks (⅟A) 0 (-(⅟D * C * ⅟A)) ⅟D

Tactic:
letI := fromBlocksZero₁₂Invertible A C D

Result:
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : CommRing α
A : Matrix m m α
C : Matrix n m α
D : Matrix n n α
inst✝² : Invertible A
inst✝¹ : Invertible D
inst✝ : Invertible (fromBlocks A 0 C D)
this : Invertible (fromBlocks A 0 C D) := A.fromBlocksZero₁₂Invertible C D
⊢ ⅟(fromBlocks A 0 C D) = fromBlocks (⅟A) 0 (-(⅟D * C * ⅟A)) ⅟D

Proof state:
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : CommRing α
A : Matrix m m α
C : Matrix n m α
D : Matrix n n α
inst✝² : Invertible A
inst✝¹ : Invertible D
inst✝ : Invertible (fromBlocks A 0 C D)
this : Invertible (fromBlocks A 0 C D) := A.fromBlocksZero₁₂Invertible C D
⊢ ⅟(fromBlocks A 0 C D) = fromBlocks (⅟A) 0 (-(⅟D * C * ⅟A)) ⅟D

Tactic:
convert (rfl : ⅟ (fromBlocks A 0 C D) = _)

Result:
no goals
-- Mathlib/LinearAlgebra/UnitaryGroup.lean
theorem mem_unitaryGroup_iff : A ∈ Matrix.unitaryGroup n α ↔ A * star A = 1

Proof state:
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A : Matrix n n α
⊢ A ∈ unitaryGroup n α ↔ A * star A = 1

Tactic:
refine ⟨And.right, fun hA => ⟨?_, hA⟩⟩

Result:
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A : Matrix n n α
hA : A * star A = 1
⊢ star A * A = 1

Proof state:
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A : Matrix n n α
hA : A * star A = 1
⊢ star A * A = 1

Tactic:
simpa only [mul_eq_one_comm] using hA

Result:
no goals
-- Mathlib/Algebra/Order/SuccPred.lean
lemma antitone_of_add_one_le : (∀ a, ¬ IsMax a → f (a + 1) ≤ f a) → Antitone f

Proof state:
α : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α
inst✝⁴ : Preorder β
inst✝³ : Add α
inst✝² : One α
inst✝¹ : SuccAddOrder α
inst✝ : IsSuccArchimedean α
f : α → β
⊢ (∀ (a : α), ¬IsMax a → f (a + 1) ≤ f a) → Antitone f

Tactic:
simpa [Order.succ_eq_add_one] using antitone_of_succ_le (f := f)

Result:
no goals
-- Mathlib/SetTheory/Nimber/Basic.lean
theorem add_ne_of_lt (a b : Nimber) :
    (∀ a' < a, a' + b ≠ a + b) ∧ ∀ b' < b, a + b' ≠ a + b

Proof state:
a b : Nimber
⊢ (∀ a' < a, a' + b ≠ a + b) ∧ ∀ b' < b, a + b' ≠ a + b

Tactic:
have H := csInf_mem (add_nonempty a b)

Result:
a b : Nimber
H : sInf {x | (∃ a' < a, a' + b = x) ∨ ∃ b' < b, a + b' = x}ᶜ ∈ {x | (∃ a' < a, a' + b = x) ∨ ∃ b' < b, a + b' = x}ᶜ
⊢ (∀ a' < a, a' + b ≠ a + b) ∧ ∀ b' < b, a + b' ≠ a + b

Proof state:
a b : Nimber
H : a + b ∈ {x | (∃ a' < a, a' + b = x) ∨ ∃ b' < b, a + b' = x}ᶜ
⊢ (∀ a' < a, a' + b ≠ a + b) ∧ ∀ b' < b, a + b' ≠ a + b

Tactic:
simpa using H

Result:
no goals

Proof state:
a b : Nimber
H : sInf {x | (∃ a' < a, a' + b = x) ∨ ∃ b' < b, a + b' = x}ᶜ ∈ {x | (∃ a' < a, a' + b = x) ∨ ∃ b' < b, a + b' = x}ᶜ
⊢ (∀ a' < a, a' + b ≠ a + b) ∧ ∀ b' < b, a + b' ≠ a + b

Tactic:
rw [← add_def] at H

Result:
a b : Nimber
H : a + b ∈ {x | (∃ a' < a, a' + b = x) ∨ ∃ b' < b, a + b' = x}ᶜ
⊢ (∀ a' < a, a' + b ≠ a + b) ∧ ∀ b' < b, a + b' ≠ a + b
-- Mathlib/LinearAlgebra/FreeModule/PID.lean
theorem Submodule.basisOfPid_bot {ι : Type*} [Finite ι] (b : Basis ι R M) :
    Submodule.basisOfPid b ⊥ = ⟨0, Basis.empty _⟩

Proof state:
case mk
R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
ι : Type u_4
inst✝ : Finite ι
b : Basis ι R M
n : ℕ
b' : Basis (Fin n) R ↥⊥
e : Fin n ≃ Fin 0 := b'.indexEquiv (Basis.empty ↥⊥)
⊢ ⟨n, b'⟩ = ⟨0, Basis.empty ↥⊥⟩

Tactic:
obtain rfl : n = 0 := by simpa using Fintype.card_eq.mpr ⟨e⟩

Result:
case mk
R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
ι : Type u_4
inst✝ : Finite ι
b : Basis ι R M
b' : Basis (Fin 0) R ↥⊥
e : Fin 0 ≃ Fin 0 := b'.indexEquiv (Basis.empty ↥⊥)
⊢ ⟨0, b'⟩ = ⟨0, Basis.empty ↥⊥⟩

Proof state:
R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
ι : Type u_4
inst✝ : Finite ι
b : Basis ι R M
⊢ basisOfPid b ⊥ = ⟨0, Basis.empty ↥⊥⟩

Tactic:
obtain ⟨n, b'⟩ := Submodule.basisOfPid b ⊥

Result:
case mk
R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
ι : Type u_4
inst✝ : Finite ι
b : Basis ι R M
n : ℕ
b' : Basis (Fin n) R ↥⊥
⊢ ⟨n, b'⟩ = ⟨0, Basis.empty ↥⊥⟩

Proof state:
case mk
R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
ι : Type u_4
inst✝ : Finite ι
b : Basis ι R M
b' : Basis (Fin 0) R ↥⊥
e : Fin 0 ≃ Fin 0 := b'.indexEquiv (Basis.empty ↥⊥)
⊢ ⟨0, b'⟩ = ⟨0, Basis.empty ↥⊥⟩

Tactic:
exact Sigma.eq rfl (Basis.eq_of_apply_eq <| finZeroElim)

Result:
no goals

Proof state:
case mk
R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
ι : Type u_4
inst✝ : Finite ι
b : Basis ι R M
n : ℕ
b' : Basis (Fin n) R ↥⊥
⊢ ⟨n, b'⟩ = ⟨0, Basis.empty ↥⊥⟩

Tactic:
let e : Fin n ≃ Fin 0 := b'.indexEquiv (Basis.empty _ : Basis (Fin 0) R (⊥ : Submodule R M))

Result:
case mk
R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
ι : Type u_4
inst✝ : Finite ι
b : Basis ι R M
n : ℕ
b' : Basis (Fin n) R ↥⊥
e : Fin n ≃ Fin 0 := b'.indexEquiv (Basis.empty ↥⊥)
⊢ ⟨n, b'⟩ = ⟨0, Basis.empty ↥⊥⟩

Proof state:
R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
ι : Type u_4
inst✝ : Finite ι
b : Basis ι R M
n : ℕ
b' : Basis (Fin n) R ↥⊥
e : Fin n ≃ Fin 0 := b'.indexEquiv (Basis.empty ↥⊥)
⊢ n = 0

Tactic:
simpa using Fintype.card_eq.mpr ⟨e⟩

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Orthogonal.lean
theorem isOrtho_sSup_right {U : Submodule 𝕜 E} {V : Set (Submodule 𝕜 E)} :
    U ⟂ sSup V ↔ ∀ Vᵢ ∈ V, U ⟂ Vᵢ :=
  isOrtho_comm.trans <| isOrtho_sSup_left.trans <| by simp_rw [isOrtho_comm]

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
U : Submodule 𝕜 E
V : Set (Submodule 𝕜 E)
⊢ (∀ Uᵢ ∈ V, Uᵢ ⟂ U) ↔ ∀ Vᵢ ∈ V, U ⟂ Vᵢ

Tactic:
simp_rw [isOrtho_comm]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
/-- In a unital C⋆-algebra, if `a` is nonnegative and invertible, and `a ≤ b`, then `b` is
invertible. -/
lemma CStarAlgebra.isUnit_of_le {a b : A} (h₀ : IsUnit a) (ha : 0 ≤ a

Proof state:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
h₀ : 0 ∉ spectrum ℝ≥0 a
ha : autoParam (0 ≤ a) _auto✝
hab : a ≤ b
a✝ : Nontrivial A
hb : 0 ≤ b
⊢ 0 ∉ spectrum ℝ≥0 b

Tactic:
rw [zero_not_mem_iff, SpectrumRestricts.nnreal_lt_iff (.nnreal_of_nonneg ‹_›),
  NNReal.coe_zero, ← CFC.exists_pos_algebraMap_le_iff (.of_nonneg ‹_›)] at h₀ ⊢

Result:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
h₀ : ∃ r > 0, (algebraMap ℝ A) r ≤ a
ha : autoParam (0 ≤ a) _auto✝
hab : a ≤ b
a✝ : Nontrivial A
hb : 0 ≤ b
⊢ ∃ r > 0, (algebraMap ℝ A) r ≤ b

Proof state:
case h.h
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
h₀ : ∃ r > 0, (algebraMap ℝ A) r ≤ a
ha : autoParam (0 ≤ a) _auto✝
hab : a ≤ b
a✝ : Nontrivial A
hb : 0 ≤ b
r : ℝ
hr : r > 0
this : (algebraMap ℝ A) r ≤ a
⊢ (algebraMap ℝ A) r ≤ b

Tactic:
exact this.trans hab

Result:
no goals

Proof state:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
h₀ : ∃ r > 0, (algebraMap ℝ A) r ≤ a
ha : autoParam (0 ≤ a) _auto✝
hab : a ≤ b
a✝ : Nontrivial A
hb : 0 ≤ b
⊢ ∃ r > 0, (algebraMap ℝ A) r ≤ b

Tactic:
peel h₀ with r hr _

Result:
case h.h
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
h₀ : ∃ r > 0, (algebraMap ℝ A) r ≤ a
ha : autoParam (0 ≤ a) _auto✝
hab : a ≤ b
a✝ : Nontrivial A
hb : 0 ≤ b
r : ℝ
hr : r > 0
this : (algebraMap ℝ A) r ≤ a
⊢ (algebraMap ℝ A) r ≤ b

Proof state:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
h₀ : 0 ∉ spectrum ℝ≥0 a
ha : autoParam (0 ≤ a) _auto✝
hab : a ≤ b
⊢ 0 ∉ spectrum ℝ≥0 b

Tactic:
nontriviality A

Result:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
h₀ : 0 ∉ spectrum ℝ≥0 a
ha : autoParam (0 ≤ a) _auto✝
hab : a ≤ b
a✝ : Nontrivial A
⊢ 0 ∉ spectrum ℝ≥0 b

Proof state:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
h₀ : 0 ∉ spectrum ℝ≥0 a
ha : autoParam (0 ≤ a) _auto✝
hab : a ≤ b
a✝ : Nontrivial A
⊢ 0 ∉ spectrum ℝ≥0 b

Tactic:
have hb := (show 0 ≤ a from ha).trans hab

Result:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
h₀ : 0 ∉ spectrum ℝ≥0 a
ha : autoParam (0 ≤ a) _auto✝
hab : a ≤ b
a✝ : Nontrivial A
hb : 0 ≤ b
⊢ 0 ∉ spectrum ℝ≥0 b

Proof state:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
h₀ : IsUnit a
ha : autoParam (0 ≤ a) _auto✝
hab : a ≤ b
⊢ IsUnit b

Tactic:
rw [← spectrum.zero_not_mem_iff ℝ≥0] at h₀ ⊢

Result:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
h₀ : 0 ∉ spectrum ℝ≥0 a
ha : autoParam (0 ≤ a) _auto✝
hab : a ≤ b
⊢ 0 ∉ spectrum ℝ≥0 b
-- Mathlib/NumberTheory/Padics/Hensel.lean
theorem bound' : Tendsto (fun n : ℕ => ‖F.derivative.eval a‖ * T ^ 2 ^ n) atTop (𝓝 0)

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2
⊢ Tendsto (fun n => ‖Polynomial.eval a (Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n) atTop
    (𝓝 (‖Polynomial.eval a (Polynomial.derivative F)‖ * 0))

Tactic:
exact
  tendsto_const_nhds.mul
    (Tendsto.comp (tendsto_pow_atTop_nhds_zero_of_lt_one (norm_nonneg _) (T_lt_one hnorm))
      (Nat.tendsto_pow_atTop_atTop_of_one_lt (by norm_num)))

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2
⊢ Tendsto (fun n => ‖Polynomial.eval a (Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n) atTop (𝓝 0)

Tactic:
rw [← mul_zero ‖F.derivative.eval a‖]

Result:
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2
⊢ Tendsto (fun n => ‖Polynomial.eval a (Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n) atTop
    (𝓝 (‖Polynomial.eval a (Polynomial.derivative F)‖ * 0))

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2
⊢ 1 < 2

Tactic:
norm_num

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Units/Basic.lean
theorem inverse_mul_cancel (x : M₀) (h : IsUnit x) : inverse x * x = 1

Proof state:
case intro
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
u : M₀ˣ
⊢ inverse ↑u * ↑u = 1

Tactic:
rw [inverse_unit, Units.inv_mul]

Result:
no goals

Proof state:
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
x : M₀
h : IsUnit x
⊢ inverse x * x = 1

Tactic:
rcases h with ⟨u, rfl⟩

Result:
case intro
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
u : M₀ˣ
⊢ inverse ↑u * ↑u = 1
-- Mathlib/Data/List/Chain.lean
lemma Chain'.chain {α : Type*} {R : α → α → Prop} {l : List α} {v : α}
    (hl : l.Chain' R) (hv : (lne : l ≠ []) → R v (l.head lne)) : l.Chain R v

Proof state:
case left
α : Type u_1
R : α → α → Prop
l : List α
v : α
hl : Chain' R l
hv : ∀ (lne : l ≠ []), R v (l.head lne)
h : 0 < l.length
⊢ R v (l.head ⋯)

Tactic:
apply hv

Result:
no goals

Proof state:
α : Type u_1
R : α → α → Prop
l : List α
v : α
hl : Chain' R l
hv : ∀ (lne : l ≠ []), R v (l.head lne)
⊢ (∀ (h : 0 < l.length), R v (l.get ⟨0, h⟩)) ∧ ∀ (i : ℕ) (h : i < l.length - 1), R (l.get ⟨i, ⋯⟩) (l.get ⟨i + 1, ⋯⟩)

Tactic:
constructor

Result:
case left
α : Type u_1
R : α → α → Prop
l : List α
v : α
hl : Chain' R l
hv : ∀ (lne : l ≠ []), R v (l.head lne)
⊢ ∀ (h : 0 < l.length), R v (l.get ⟨0, h⟩)

case right
α : Type u_1
R : α → α → Prop
l : List α
v : α
hl : Chain' R l
hv : ∀ (lne : l ≠ []), R v (l.head lne)
⊢ ∀ (i : ℕ) (h : i < l.length - 1), R (l.get ⟨i, ⋯⟩) (l.get ⟨i + 1, ⋯⟩)

Proof state:
case right
α : Type u_1
R : α → α → Prop
l : List α
v : α
hl : Chain' R l
hv : ∀ (lne : l ≠ []), R v (l.head lne)
⊢ ∀ (i : ℕ) (h : i < l.length - 1), R (l.get ⟨i, ⋯⟩) (l.get ⟨i + 1, ⋯⟩)

Tactic:
exact List.chain'_iff_get.mp hl

Result:
no goals

Proof state:
α : Type u_1
R : α → α → Prop
l : List α
v : α
hl : Chain' R l
hv : ∀ (lne : l ≠ []), R v (l.head lne)
⊢ Chain R v l

Tactic:
rw [List.chain_iff_get]

Result:
α : Type u_1
R : α → α → Prop
l : List α
v : α
hl : Chain' R l
hv : ∀ (lne : l ≠ []), R v (l.head lne)
⊢ (∀ (h : 0 < l.length), R v (l.get ⟨0, h⟩)) ∧ ∀ (i : ℕ) (h : i < l.length - 1), R (l.get ⟨i, ⋯⟩) (l.get ⟨i + 1, ⋯⟩)

Proof state:
case left
α : Type u_1
R : α → α → Prop
l : List α
v : α
hl : Chain' R l
hv : ∀ (lne : l ≠ []), R v (l.head lne)
h : 0 < l.length
⊢ R v (l.get ⟨0, h⟩)

Tactic:
rw [List.get_mk_zero]

Result:
case left
α : Type u_1
R : α → α → Prop
l : List α
v : α
hl : Chain' R l
hv : ∀ (lne : l ≠ []), R v (l.head lne)
h : 0 < l.length
⊢ R v (l.head ⋯)

Proof state:
case left
α : Type u_1
R : α → α → Prop
l : List α
v : α
hl : Chain' R l
hv : ∀ (lne : l ≠ []), R v (l.head lne)
⊢ ∀ (h : 0 < l.length), R v (l.get ⟨0, h⟩)

Tactic:
intro h

Result:
case left
α : Type u_1
R : α → α → Prop
l : List α
v : α
hl : Chain' R l
hv : ∀ (lne : l ≠ []), R v (l.head lne)
h : 0 < l.length
⊢ R v (l.get ⟨0, h⟩)