harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicGeometry/Restrict.lean
lemma ι_app_self : U.ι.app U = X.presheaf.map (eqToHom (X := U.ι ''ᵁ _) (by simp)).op := rfl

Proof state:
C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
U : X.Opens
⊢ U.ι ''ᵁ unop (op (U.ι ⁻¹ᵁ U)) = U

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Dual.lean
theorem toDual_symm_apply {x : E} {y : NormedSpace.Dual 𝕜 E} : ⟪(toDual 𝕜 E).symm y, x⟫ = y x

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
x : E
y : NormedSpace.Dual 𝕜 E
⊢ ((toDual 𝕜 E) ((toDual 𝕜 E).symm y)) x = y x

Tactic:
simp only [LinearIsometryEquiv.apply_symm_apply]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
x : E
y : NormedSpace.Dual 𝕜 E
⊢ ⟪(toDual 𝕜 E).symm y, x⟫_𝕜 = y x

Tactic:
rw [← toDual_apply]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
x : E
y : NormedSpace.Dual 𝕜 E
⊢ ((toDual 𝕜 E) ((toDual 𝕜 E).symm y)) x = y x
-- Mathlib/LinearAlgebra/Matrix/FixedDetMatrices.lean
private lemma prop_red_T_pow (hS : ∀ B, C B → C (S • B)) (hT : ∀ B, C B → C (T • B)) :
     ∀ B (n : ℤ), C (T^n • B) ↔ C B

Proof state:
case hz
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (T • B)
B : FixedDetMatrix (Fin 2) ℤ m
⊢ C (T ^ 0 • B) ↔ C B

Tactic:
simp only [zpow_zero, one_smul, imp_self]

Result:
no goals

Proof state:
case hn
m✝ : ℤ
C : FixedDetMatrix (Fin 2) ℤ m✝ → Prop
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m✝), C B → C (S • B)
hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m✝), C B → C (T • B)
B : FixedDetMatrix (Fin 2) ℤ m✝
m : ℕ
hm : C (T ^ (-↑m) • B) ↔ C B
⊢ C (T ^ (-↑m - 1) • B) ↔ C B

Tactic:
rwa [sub_eq_neg_add, zpow_add, zpow_neg_one, ← prop_red_T hS hT, mul_smul, smul_inv_smul]

Result:
no goals

Proof state:
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (T • B)
⊢ ∀ (B : FixedDetMatrix (Fin 2) ℤ m) (n : ℤ), C (T ^ n • B) ↔ C B

Tactic:
intro B n

Result:
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (T • B)
B : FixedDetMatrix (Fin 2) ℤ m
n : ℤ
⊢ C (T ^ n • B) ↔ C B

Proof state:
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (T • B)
B : FixedDetMatrix (Fin 2) ℤ m
n : ℤ
⊢ C (T ^ n • B) ↔ C B

Tactic:
induction n with
| hz => simp only [zpow_zero, one_smul, imp_self]
| hp n hn =>
  simpa only [add_comm (n:ℤ), zpow_add _ 1, ← smul_eq_mul, zpow_one, smul_assoc, prop_red_T hS hT]
| hn m hm =>
  rwa [sub_eq_neg_add, zpow_add, zpow_neg_one, ← prop_red_T hS hT, mul_smul, smul_inv_smul]

Result:
no goals

Proof state:
case hp
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (T • B)
B : FixedDetMatrix (Fin 2) ℤ m
n : ℕ
hn : C (T ^ ↑n • B) ↔ C B
⊢ C (T ^ (↑n + 1) • B) ↔ C B

Tactic:
simpa only [add_comm (n:ℤ), zpow_add _ 1, ← smul_eq_mul, zpow_one, smul_assoc, prop_red_T hS hT]

Result:
no goals
-- Mathlib/Analysis/RCLike/Basic.lean
@[simp, norm_cast]
lemma ofReal_pos {x : ℝ} : 0 < (x : K) ↔ 0 < x

Proof state:
K : Type u_1
inst✝ : RCLike K
x : ℝ
⊢ 0 < ↑x ↔ 0 < x

Tactic:
rw [← ofReal_zero, ofReal_lt_ofReal]

Result:
no goals
-- Mathlib/Algebra/ContinuedFractions/Computation/Approximations.lean
theorem zero_le_of_den : 0 ≤ (of v).dens n

Proof state:
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
⊢ 0 ≤ (of v).dens n

Tactic:
rw [den_eq_conts_b, nth_cont_eq_succ_nth_contAux]

Result:
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
⊢ 0 ≤ ((of v).contsAux (n + 1)).b

Proof state:
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
⊢ 0 ≤ ((of v).contsAux (n + 1)).b

Tactic:
exact zero_le_of_contsAux_b

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem ushiftRight_and_distrib (x y : BitVec w) (n : Nat) :
    (x &&& y) >>> n = (x >>> n) &&& (y >>> n)

Proof state:
case pred
w : Nat
x y : BitVec w
n i✝ : Nat
a✝ : i✝ < w
⊢ ((x &&& y) >>> n).getLsbD i✝ = (x >>> n &&& y >>> n).getLsbD i✝

Tactic:
simp

Result:
no goals

Proof state:
w : Nat
x y : BitVec w
n : Nat
⊢ (x &&& y) >>> n = x >>> n &&& y >>> n

Tactic:
ext

Result:
case pred
w : Nat
x y : BitVec w
n i✝ : Nat
a✝ : i✝ < w
⊢ ((x &&& y) >>> n).getLsbD i✝ = (x >>> n &&& y >>> n).getLsbD i✝
-- Mathlib/Analysis/Calculus/FDeriv/Prod.lean
theorem hasStrictFDerivAt_pi' :
    HasStrictFDerivAt Φ Φ' x ↔ ∀ i, HasStrictFDerivAt (fun x => Φ x i) ((proj i).comp Φ') x

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
x : E
ι : Type u_6
inst✝² : Fintype ι
F' : ι → Type u_7
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
Φ : E → (i : ι) → F' i
Φ' : E →L[𝕜] (i : ι) → F' i
⊢ ((fun p => Φ p.1 - Φ p.2 - Φ' (p.1 - p.2)) =o[𝓝 (x, x)] fun p => p.1 - p.2) ↔
    ∀ (i : ι), (fun p => Φ p.1 i - Φ p.2 i - ((proj i).comp Φ') (p.1 - p.2)) =o[𝓝 (x, x)] fun p => p.1 - p.2

Tactic:
exact isLittleO_pi

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
x : E
ι : Type u_6
inst✝² : Fintype ι
F' : ι → Type u_7
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
Φ : E → (i : ι) → F' i
Φ' : E →L[𝕜] (i : ι) → F' i
⊢ HasStrictFDerivAt Φ Φ' x ↔ ∀ (i : ι), HasStrictFDerivAt (fun x => Φ x i) ((proj i).comp Φ') x

Tactic:
simp only [hasStrictFDerivAt_iff_isLittleO, ContinuousLinearMap.coe_pi]

Result:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
x : E
ι : Type u_6
inst✝² : Fintype ι
F' : ι → Type u_7
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
Φ : E → (i : ι) → F' i
Φ' : E →L[𝕜] (i : ι) → F' i
⊢ ((fun p => Φ p.1 - Φ p.2 - Φ' (p.1 - p.2)) =o[𝓝 (x, x)] fun p => p.1 - p.2) ↔
    ∀ (i : ι), (fun p => Φ p.1 i - Φ p.2 i - ((proj i).comp Φ') (p.1 - p.2)) =o[𝓝 (x, x)] fun p => p.1 - p.2
-- Mathlib/RingTheory/Ideal/MinimalPrime/Basic.lean
theorem Ideal.minimalPrimes_top : (⊤ : Ideal R).minimalPrimes = ∅

Proof state:
case h
R : Type u_1
inst✝ : CommSemiring R
p : Ideal R
⊢ p ∈ ⊤.minimalPrimes ↔ p ∈ ∅

Tactic:
simp only [Set.not_mem_empty, iff_false]

Result:
case h
R : Type u_1
inst✝ : CommSemiring R
p : Ideal R
⊢ p ∉ ⊤.minimalPrimes

Proof state:
case h
R : Type u_1
inst✝ : CommSemiring R
p : Ideal R
⊢ p ∉ ⊤.minimalPrimes

Tactic:
intro h

Result:
case h
R : Type u_1
inst✝ : CommSemiring R
p : Ideal R
h : p ∈ ⊤.minimalPrimes
⊢ False

Proof state:
R : Type u_1
inst✝ : CommSemiring R
⊢ ⊤.minimalPrimes = ∅

Tactic:
ext p

Result:
case h
R : Type u_1
inst✝ : CommSemiring R
p : Ideal R
⊢ p ∈ ⊤.minimalPrimes ↔ p ∈ ∅

Proof state:
case h
R : Type u_1
inst✝ : CommSemiring R
p : Ideal R
h : p ∈ ⊤.minimalPrimes
⊢ False

Tactic:
exact h.1.1.ne_top (top_le_iff.mp h.1.2)

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/Spectrum.lean
theorem eventually_isUnit_resolvent (a : A) : ∀ᶠ z in cobounded 𝕜, IsUnit (resolvent a z)

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
⊢ ∃ i, True ∧ ∀ ⦃x : 𝕜⦄, x ∈ norm ⁻¹' Set.Ioi i → IsUnit (resolvent a x)

Tactic:
exact ⟨‖a‖ * ‖(1 : A)‖, trivial, fun _ ↦ isUnit_resolvent.mp ∘ mem_resolventSet_of_norm_lt_mul⟩

Result:
no goals

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
⊢ ∀ᶠ (z : 𝕜) in cobounded 𝕜, IsUnit (resolvent a z)

Tactic:
rw [atTop_basis_Ioi.cobounded_of_norm.eventually_iff]

Result:
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
⊢ ∃ i, True ∧ ∀ ⦃x : 𝕜⦄, x ∈ norm ⁻¹' Set.Ioi i → IsUnit (resolvent a x)
-- Mathlib/Data/Seq/WSeq.lean
theorem join_think (S : WSeq (WSeq α)) : join (think S) = think (join S)

Proof state:
α : Type u
S : WSeq (WSeq α)
⊢ (Seq.map
        (fun o =>
          match o with
          | none => Seq1.ret none
          | some s => (none, s))
        (Seq.cons none S)).join =
    Seq.cons none
      (Seq.map
          (fun o =>
            match o with
            | none => Seq1.ret none
            | some s => (none, s))
          S).join

Tactic:
simp [join, Seq1.ret]

Result:
no goals

Proof state:
α : Type u
S : WSeq (WSeq α)
⊢ S.think.join = S.join.think

Tactic:
simp only [join, think]

Result:
α : Type u
S : WSeq (WSeq α)
⊢ ((fun o =>
          match o with
          | none => Seq1.ret none
          | some s => (none, s)) <$>
        Seq.cons none S).join =
    Seq.cons none
      ((fun o =>
            match o with
            | none => Seq1.ret none
            | some s => (none, s)) <$>
          S).join
-- Mathlib/Data/Int/WithZero.lean
theorem toNNReal_ne_zero {e : ℝ≥0} {m : ℤₘ₀} (he : e ≠ 0) (hm : m ≠ 0) : toNNReal he m ≠ 0

Proof state:
e : ℝ≥0
m : ℤₘ₀
he : e ≠ 0
hm : m ≠ 0
⊢ (toNNReal he) m ≠ 0

Tactic:
simp only [ne_eq, map_eq_zero, hm, not_false_eq_true]

Result:
no goals
-- Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean
lemma shortComplexH0_exact : (shortComplexH0 A).Exact

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑A.V
hx : (dZero A) x = 0
g : G
⊢ (A.ρ g) x - x = 0

Tactic:
exact congr_fun hx g

Result:
no goals

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ ∀ (x₂ : ↑(shortComplexH0 A).X₂),
    (ConcreteCategory.hom (shortComplexH0 A).g) x₂ = 0 → ∃ x₁, (ConcreteCategory.hom (shortComplexH0 A).f) x₁ = x₂

Tactic:
intro (x : A) (hx : dZero _ x = 0)

Result:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑A.V
hx : (dZero A) x = 0
⊢ ∃ x₁, (ConcreteCategory.hom (shortComplexH0 A).f) x₁ = x

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ (shortComplexH0 A).Exact

Tactic:
rw [ShortComplex.moduleCat_exact_iff]

Result:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ ∀ (x₂ : ↑(shortComplexH0 A).X₂),
    (ConcreteCategory.hom (shortComplexH0 A).g) x₂ = 0 → ∃ x₁, (ConcreteCategory.hom (shortComplexH0 A).f) x₁ = x₂

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑A.V
hx : (dZero A) x = 0
⊢ ∃ x₁, (ConcreteCategory.hom (shortComplexH0 A).f) x₁ = x

Tactic:
refine ⟨⟨x, fun g => ?_⟩, rfl⟩

Result:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑A.V
hx : (dZero A) x = 0
g : G
⊢ (A.ρ g) x = x

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑A.V
hx : (dZero A) x = 0
g : G
⊢ (A.ρ g) x = x

Tactic:
rw [← sub_eq_zero]

Result:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑A.V
hx : (dZero A) x = 0
g : G
⊢ (A.ρ g) x - x = 0
-- Mathlib/LinearAlgebra/Dimension/Finite.lean
theorem rank_pos_iff_exists_ne_zero : 0 < Module.rank R M ↔ ∃ x : M, x ≠ 0

Proof state:
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : NoZeroSMulDivisors R M
⊢ 0 < Module.rank R M ↔ ∃ x, x ≠ 0

Tactic:
rw [← not_iff_not]

Result:
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : NoZeroSMulDivisors R M
⊢ ¬0 < Module.rank R M ↔ ¬∃ x, x ≠ 0

Proof state:
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : NoZeroSMulDivisors R M
⊢ ¬0 < Module.rank R M ↔ ¬∃ x, x ≠ 0

Tactic:
simpa using rank_zero_iff_forall_zero

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
theorem coe_pow (s : Finset α) (n : ℕ) : ↑(s ^ n) = (s : Set α) ^ n

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
⊢ ↑(npowRec n s) = ↑s ^ n

Tactic:
induction' n with n ih

Result:
case zero
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
⊢ ↑(npowRec 0 s) = ↑s ^ 0

case succ
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
ih : ↑(npowRec n s) = ↑s ^ n
⊢ ↑(npowRec (n + 1) s) = ↑s ^ (n + 1)

Proof state:
case zero
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
⊢ ↑(npowRec 0 s) = ↑s ^ 0

Tactic:
rw [npowRec, pow_zero, coe_one]

Result:
no goals

Proof state:
case succ
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
ih : ↑(npowRec n s) = ↑s ^ n
⊢ ↑(npowRec (n + 1) s) = ↑s ^ (n + 1)

Tactic:
rw [npowRec, pow_succ, coe_mul, ih]

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
⊢ ↑(s ^ n) = ↑s ^ n

Tactic:
change ↑(npowRec n s) = (s : Set α) ^ n

Result:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
⊢ ↑(npowRec n s) = ↑s ^ n
-- Mathlib/Algebra/Order/Ring/Pow.lean
/-- **Bernoulli's inequality** reformulated to estimate `a^n`. -/
lemma one_add_mul_sub_le_pow (H : -1 ≤ a) (n : ℕ) : 1 + n * (a - 1) ≤ a ^ n

Proof state:
R : Type u_1
inst✝ : LinearOrderedRing R
a : R
H : -1 ≤ a
n : ℕ
⊢ 1 + ↑n * (a - 1) ≤ a ^ n

Tactic:
have : -2 ≤ a - 1 := by
  rwa [← one_add_one_eq_two, neg_add, ← sub_eq_add_neg, sub_le_sub_iff_right]

Result:
R : Type u_1
inst✝ : LinearOrderedRing R
a : R
H : -1 ≤ a
n : ℕ
this : -2 ≤ a - 1
⊢ 1 + ↑n * (a - 1) ≤ a ^ n

Proof state:
R : Type u_1
inst✝ : LinearOrderedRing R
a : R
H : -1 ≤ a
n : ℕ
⊢ -2 ≤ a - 1

Tactic:
rwa [← one_add_one_eq_two, neg_add, ← sub_eq_add_neg, sub_le_sub_iff_right]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : LinearOrderedRing R
a : R
H : -1 ≤ a
n : ℕ
this : -2 ≤ a - 1
⊢ 1 + ↑n * (a - 1) ≤ a ^ n

Tactic:
simpa only [add_sub_cancel] using one_add_mul_le_pow this n

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/MapIdx.lean
theorem back_mapIdx [NeZero n] {l : Vector α n} {f : Nat → α → β} :
    (mapIdx f l).back = f (l.size - 1) (l.back)

Proof state:
n : Nat
α : Type u_1
β : Type u_2
inst✝ : NeZero n
l : Vector α n
f : Nat → α → β
⊢ (mapIdx f l).back = f (l.size - 1) l.back

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
β : Type u_2
f : Nat → α → β
l : Array α
inst✝ : NeZero l.size
⊢ (mapIdx f { toArray := l, size_toArray := ⋯ }).back =
    f ({ toArray := l, size_toArray := ⋯ }.size - 1) { toArray := l, size_toArray := ⋯ }.back

Proof state:
case mk
α : Type u_1
β : Type u_2
f : Nat → α → β
l : Array α
inst✝ : NeZero l.size
⊢ (mapIdx f { toArray := l, size_toArray := ⋯ }).back =
    f ({ toArray := l, size_toArray := ⋯ }.size - 1) { toArray := l, size_toArray := ⋯ }.back

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem bsup_eq_blsub_of_lt_succ_limit {o : Ordinal.{u}} (ho : IsLimit o)
    {f : ∀ a < o, Ordinal.{max u v}} (hf : ∀ a ha, f a ha < f (succ a) (ho.succ_lt ha)) :
    bsup.{_, v} o f = blsub.{_, v} o f

Proof state:
o : Ordinal.{u}
ho : o.IsLimit
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
hf : ∀ (a : Ordinal.{u}) (ha : a < o), f a ha < f (succ a) ⋯
⊢ ∀ (i : Ordinal.{u}) (hi : i < o), f i hi < o.bsup f

Tactic:
exact fun i hi => (hf i hi).trans_le (le_bsup f _ _)

Result:
no goals

Proof state:
o : Ordinal.{u}
ho : o.IsLimit
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
hf : ∀ (a : Ordinal.{u}) (ha : a < o), f a ha < f (succ a) ⋯
⊢ o.bsup f = o.blsub f

Tactic:
rw [bsup_eq_blsub_iff_lt_bsup]

Result:
o : Ordinal.{u}
ho : o.IsLimit
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
hf : ∀ (a : Ordinal.{u}) (ha : a < o), f a ha < f (succ a) ⋯
⊢ ∀ (i : Ordinal.{u}) (hi : i < o), f i hi < o.bsup f
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable.lean
theorem mem_lpMeasSubgroup_iff_aeStronglyMeasurable {m m0 : MeasurableSpace α} {μ : Measure α}
    {f : Lp F p μ} : f ∈ lpMeasSubgroup F m p μ ↔ AEStronglyMeasurable[m] f μ

Proof state:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝ : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
f : ↥(Lp F p μ)
⊢ f ∈ lpMeasSubgroup F m p μ ↔ AEStronglyMeasurable (↑↑f) μ

Tactic:
rw [← AddSubgroup.mem_carrier, lpMeasSubgroup, Set.mem_setOf_eq]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Basic.lean
lemma ball_preimage {f : α → β} {U : Set (β × β)} {x : α} :
    UniformSpace.ball x (Prod.map f f ⁻¹' U) = f ⁻¹' UniformSpace.ball (f x) U

Proof state:
α : Type ua
β : Type ub
f : α → β
U : Set (β × β)
x : α
⊢ UniformSpace.ball x (Prod.map f f ⁻¹' U) = f ⁻¹' UniformSpace.ball (f x) U

Tactic:
ext : 1

Result:
case h
α : Type ua
β : Type ub
f : α → β
U : Set (β × β)
x x✝ : α
⊢ x✝ ∈ UniformSpace.ball x (Prod.map f f ⁻¹' U) ↔ x✝ ∈ f ⁻¹' UniformSpace.ball (f x) U

Proof state:
case h
α : Type ua
β : Type ub
f : α → β
U : Set (β × β)
x x✝ : α
⊢ x✝ ∈ UniformSpace.ball x (Prod.map f f ⁻¹' U) ↔ x✝ ∈ f ⁻¹' UniformSpace.ball (f x) U

Tactic:
simp only [UniformSpace.ball, mem_preimage, Prod.map_apply]

Result:
no goals
-- Mathlib/Order/Filter/Map.lean
theorem pure_bind (a : α) (m : α → Filter β) : bind (pure a) m = m a

Proof state:
α : Type u_1
β : Type u_2
a : α
m : α → Filter β
⊢ (pure a).bind m = m a

Tactic:
simp only [Bind.bind, bind, map_pure, join_pure]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Embeddings.lean
lemma card_stabilizer [IsGalois k K] :
    Nat.card (Stab w) = if IsUnramified k w then 1 else 2

Proof state:
case isFalse
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
w : InfinitePlace K
inst✝ : IsGalois k K
h✝ : ¬IsUnramified k w
⊢ Nat.card ↥(Stab w) = 2

Tactic:
rwa [← not_isUnramified_iff_card_stabilizer_eq_two]

Result:
no goals

Proof state:
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
w : InfinitePlace K
inst✝ : IsGalois k K
⊢ Nat.card ↥(Stab w) = if IsUnramified k w then 1 else 2

Tactic:
split

Result:
case isTrue
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
w : InfinitePlace K
inst✝ : IsGalois k K
h✝ : IsUnramified k w
⊢ Nat.card ↥(Stab w) = 1

case isFalse
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
w : InfinitePlace K
inst✝ : IsGalois k K
h✝ : ¬IsUnramified k w
⊢ Nat.card ↥(Stab w) = 2

Proof state:
case isTrue
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
w : InfinitePlace K
inst✝ : IsGalois k K
h✝ : IsUnramified k w
⊢ Nat.card ↥(Stab w) = 1

Tactic:
rwa [← isUnramified_iff_card_stabilizer_eq_one]

Result:
no goals
-- Mathlib/Algebra/Order/CauSeq/BigOperators.lean
lemma of_mono_bounded (f : ℕ → α) {a : α} {m : ℕ} (ham : ∀ n ≥ m, |f n| ≤ a)
    (hnm : ∀ n ≥ m, f n ≤ f n.succ) : IsCauSeq abs f :=
  (of_decreasing_bounded (-f) (a := a) (m := m) (by simpa using ham) <| by simpa using hnm).of_neg

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
f : ℕ → α
a : α
m : ℕ
ham : ∀ n ≥ m, |f n| ≤ a
hnm : ∀ n ≥ m, f n ≤ f n.succ
⊢ ∀ n ≥ m, |(-f) n| ≤ a

Tactic:
simpa using ham

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
f : ℕ → α
a : α
m : ℕ
ham : ∀ n ≥ m, |f n| ≤ a
hnm : ∀ n ≥ m, f n ≤ f n.succ
⊢ ∀ n ≥ m, (-f) n.succ ≤ (-f) n

Tactic:
simpa using hnm

Result:
no goals
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem inv_pow_lt_inv_pow_of_lt (a1 : 1 < a) {m n : ℕ} (mn : m < n) : (a ^ n)⁻¹ < (a ^ m)⁻¹

Proof state:
α : Type u_2
inst✝ : LinearOrderedSemifield α
a : α
a1 : 1 < a
m n : ℕ
mn : m < n
⊢ (a ^ n)⁻¹ < (a ^ m)⁻¹

Tactic:
convert one_div_pow_lt_one_div_pow_of_lt a1 mn using 1 <;> simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Model.lean
theorem toListModel_updateBucket [BEq α] [Hashable α] [PartialEquivBEq α] [LawfulHashable α]
    {m : Raw₀ α β} (hm : Raw.WFImp m.1) {a : α} {f : AssocList α β → AssocList α β}
    {g : List ((a : α) × β a) → List ((a : α) × β a)} (hfg : ∀ {l}, Perm (f l).toList (g l.toList))
    (hg₁ : ∀ {l l'}, DistinctKeys l → Perm l l' → Perm (g l) (g l'))
    (hg₂ : ∀ {l l'}, containsKey a l' = false → g (l ++ l') = g l ++ l') :
    Perm (toListModel (updateBucket m.1.buckets m.2 a f)) (g (toListModel m.1.2))

Proof state:
case intro.intro.intro
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : PartialEquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
hm : Raw.WFImp m.val
a : α
f : AssocList α β → AssocList α β
g : List ((a : α) × β a) → List ((a : α) × β a)
hfg : ∀ {l : AssocList α β}, (f l).toList.Perm (g l.toList)
hg₁ : ∀ {l l' : List ((a : α) × β a)}, DistinctKeys l → l.Perm l' → (g l).Perm (g l')
hg₂ : ∀ {l l' : List ((a : α) × β a)}, containsKey a l' = false → g (l ++ l') = g l ++ l'
l : List ((a : α) × β a)
h₁ : (toListModel m.val.buckets).Perm ((bucket m.val.buckets ⋯ a).toList ++ l)
h₂ : (toListModel (updateBucket m.val.buckets ⋯ a f)).Perm ((f (bucket m.val.buckets ⋯ a)).toList ++ l)
h₃ : ∀ [inst : LawfulHashable α], IsHashSelf m.val.buckets → ∀ (k' : α), hash a = hash k' → containsKey k' l = false
⊢ (toListModel (updateBucket m.val.buckets ⋯ a f)).Perm (g (toListModel m.val.buckets))

Tactic:
refine h₂.trans (Perm.trans ?_ (hg₁ hm.distinct h₁).symm)

Result:
case intro.intro.intro
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : PartialEquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
hm : Raw.WFImp m.val
a : α
f : AssocList α β → AssocList α β
g : List ((a : α) × β a) → List ((a : α) × β a)
hfg : ∀ {l : AssocList α β}, (f l).toList.Perm (g l.toList)
hg₁ : ∀ {l l' : List ((a : α) × β a)}, DistinctKeys l → l.Perm l' → (g l).Perm (g l')
hg₂ : ∀ {l l' : List ((a : α) × β a)}, containsKey a l' = false → g (l ++ l') = g l ++ l'
l : List ((a : α) × β a)
h₁ : (toListModel m.val.buckets).Perm ((bucket m.val.buckets ⋯ a).toList ++ l)
h₂ : (toListModel (updateBucket m.val.buckets ⋯ a f)).Perm ((f (bucket m.val.buckets ⋯ a)).toList ++ l)
h₃ : ∀ [inst : LawfulHashable α], IsHashSelf m.val.buckets → ∀ (k' : α), hash a = hash k' → containsKey k' l = false
⊢ ((f (bucket m.val.buckets ⋯ a)).toList ++ l).Perm (g ((bucket m.val.buckets ⋯ a).toList ++ l))
-- Mathlib/NumberTheory/Pell.lean
theorem x_ne_zero (h₀ : 0 ≤ d) (a : Solution₁ d) : a.x ≠ 0

Proof state:
d : ℤ
h₀ : 0 ≤ d
a : Solution₁ d
⊢ a.x ≠ 0

Tactic:
intro hx

Result:
d : ℤ
h₀ : 0 ≤ d
a : Solution₁ d
hx : a.x = 0
⊢ False

Proof state:
d : ℤ
h₀ : 0 ≤ d
a : Solution₁ d
hx : a.x = 0
h : 0 ≤ d * a.y ^ 2
⊢ False

Tactic:
rw [a.prop_y, hx, sq, zero_mul, zero_sub] at h

Result:
d : ℤ
h₀ : 0 ≤ d
a : Solution₁ d
hx : a.x = 0
h : 0 ≤ -1
⊢ False

Proof state:
d : ℤ
h₀ : 0 ≤ d
a : Solution₁ d
hx : a.x = 0
⊢ False

Tactic:
have h : 0 ≤ d * a.y ^ 2 := mul_nonneg h₀ (sq_nonneg _)

Result:
d : ℤ
h₀ : 0 ≤ d
a : Solution₁ d
hx : a.x = 0
h : 0 ≤ d * a.y ^ 2
⊢ False

Proof state:
d : ℤ
h₀ : 0 ≤ d
a : Solution₁ d
hx : a.x = 0
h : 0 ≤ -1
⊢ False

Tactic:
exact not_le.mpr (neg_one_lt_zero : (-1 : ℤ) < 0) h

Result:
no goals