harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem coe_zeta_smul_apply {M} [Semiring R] [AddCommMonoid M] [Module R M]
    {f : ArithmeticFunction M} {x : ℕ} :
    ((↑ζ : ArithmeticFunction R) • f) x = ∑ i ∈ divisors x, f i

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : ArithmeticFunction M
x : ℕ
⊢ ∑ x ∈ x.divisorsAntidiagonal, ↑ζ x.1 • f x.2 = ∑ i ∈ x.divisorsAntidiagonal, f i.2

Tactic:
refine sum_congr rfl fun i hi => ?_

Result:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : ArithmeticFunction M
x : ℕ
i : ℕ × ℕ
hi : i ∈ x.divisorsAntidiagonal
⊢ ↑ζ i.1 • f i.2 = f i.2

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : ArithmeticFunction M
x : ℕ
i : ℕ × ℕ
hi : i ∈ x.divisorsAntidiagonal
⊢ ↑ζ i.1 • f i.2 = f i.2

Tactic:
rcases mem_divisorsAntidiagonal.1 hi with ⟨rfl, h⟩

Result:
case intro
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : ArithmeticFunction M
i : ℕ × ℕ
hi : i ∈ (i.1 * i.2).divisorsAntidiagonal
h : i.1 * i.2 ≠ 0
⊢ ↑ζ i.1 • f i.2 = f i.2

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : ArithmeticFunction M
x : ℕ
⊢ ∑ i ∈ x.divisorsAntidiagonal, f i.2 = ∑ i ∈ x.divisors, f i

Tactic:
rw [← map_div_left_divisors, sum_map, Function.Embedding.coeFn_mk]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : ArithmeticFunction M
x : ℕ
⊢ ∑ x ∈ x.divisorsAntidiagonal, ↑ζ x.1 • f x.2 = ∑ i ∈ x.divisors, f i

Tactic:
trans ∑ i ∈ divisorsAntidiagonal x, f i.snd

Result:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : ArithmeticFunction M
x : ℕ
⊢ ∑ x ∈ x.divisorsAntidiagonal, ↑ζ x.1 • f x.2 = ∑ i ∈ x.divisorsAntidiagonal, f i.2

R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : ArithmeticFunction M
x : ℕ
⊢ ∑ i ∈ x.divisorsAntidiagonal, f i.2 = ∑ i ∈ x.divisors, f i

Proof state:
case intro
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : ArithmeticFunction M
i : ℕ × ℕ
hi : i ∈ (i.1 * i.2).divisorsAntidiagonal
h : i.1 * i.2 ≠ 0
⊢ ↑ζ i.1 • f i.2 = f i.2

Tactic:
rw [natCoe_apply, zeta_apply_ne (left_ne_zero_of_mul h), cast_one, one_smul]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : ArithmeticFunction M
x : ℕ
⊢ (↑ζ • f) x = ∑ i ∈ x.divisors, f i

Tactic:
rw [smul_apply]

Result:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : ArithmeticFunction M
x : ℕ
⊢ ∑ x ∈ x.divisorsAntidiagonal, ↑ζ x.1 • f x.2 = ∑ i ∈ x.divisors, f i
-- Mathlib/Algebra/Lie/Nilpotent.lean
theorem isTrivial_of_nilpotencyLength_le_one [IsNilpotent L M] (h : nilpotencyLength L M ≤ 1) :
    IsTrivial L M

Proof state:
case inl
L : Type v
M : Type w
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : LieRingModule L M
inst✝ : IsNilpotent L M
h✝ : nilpotencyLength L M ≤ 1
a✝ : Nontrivial M
h : Subsingleton M
⊢ IsTrivial L M

Tactic:
infer_instance

Result:
no goals

Proof state:
case inr
L : Type v
M : Type w
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : LieRingModule L M
inst✝ : IsNilpotent L M
h✝ : nilpotencyLength L M ≤ 1
a✝ : Nontrivial M
h : nilpotencyLength L M = 1
⊢ IsTrivial L M

Tactic:
rwa [nilpotencyLength_eq_one_iff] at h

Result:
no goals

Proof state:
L : Type v
M : Type w
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : LieRingModule L M
inst✝ : IsNilpotent L M
h : nilpotencyLength L M ≤ 1
a✝ : Nontrivial M
⊢ IsTrivial L M

Tactic:
rcases Nat.le_one_iff_eq_zero_or_eq_one.mp h with h | h

Result:
case inl
L : Type v
M : Type w
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : LieRingModule L M
inst✝ : IsNilpotent L M
h✝ : nilpotencyLength L M ≤ 1
a✝ : Nontrivial M
h : nilpotencyLength L M = 0
⊢ IsTrivial L M

case inr
L : Type v
M : Type w
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : LieRingModule L M
inst✝ : IsNilpotent L M
h✝ : nilpotencyLength L M ≤ 1
a✝ : Nontrivial M
h : nilpotencyLength L M = 1
⊢ IsTrivial L M

Proof state:
L : Type v
M : Type w
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : LieRingModule L M
inst✝ : IsNilpotent L M
h : nilpotencyLength L M ≤ 1
⊢ IsTrivial L M

Tactic:
nontriviality M

Result:
L : Type v
M : Type w
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : LieRingModule L M
inst✝ : IsNilpotent L M
h : nilpotencyLength L M ≤ 1
a✝ : Nontrivial M
⊢ IsTrivial L M

Proof state:
case inl
L : Type v
M : Type w
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : LieRingModule L M
inst✝ : IsNilpotent L M
h✝ : nilpotencyLength L M ≤ 1
a✝ : Nontrivial M
h : nilpotencyLength L M = 0
⊢ IsTrivial L M

Tactic:
rw [nilpotencyLength_eq_zero_iff] at h

Result:
case inl
L : Type v
M : Type w
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : LieRingModule L M
inst✝ : IsNilpotent L M
h✝ : nilpotencyLength L M ≤ 1
a✝ : Nontrivial M
h : Subsingleton M
⊢ IsTrivial L M
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Entails.lean
theorem Limplies.trans {α : Type u} {σ1 : Type v} {σ2 : Type w} {σ3 : Type x}
    [Entails α σ1] [Entails α σ2] [Entails α σ3] (f1 : σ1) (f2 : σ2) (f3 : σ3) :
    Limplies α f1 f2 → Limplies α f2 f3 → Limplies α f1 f3

Proof state:
α : Type u
σ1 : Type v
σ2 : Type w
σ3 : Type x
inst✝² : Entails α σ1
inst✝¹ : Entails α σ2
inst✝ : Entails α σ3
f1 : σ1
f2 : σ2
f3 : σ3
f1_implies_f2 : Limplies α f1 f2
f2_implies_f3 : Limplies α f2 f3
a : α → Bool
a_entails_f1 : a ⊨ f1
⊢ a ⊨ f3

Tactic:
exact f2_implies_f3 a <| f1_implies_f2 a a_entails_f1

Result:
no goals

Proof state:
α : Type u
σ1 : Type v
σ2 : Type w
σ3 : Type x
inst✝² : Entails α σ1
inst✝¹ : Entails α σ2
inst✝ : Entails α σ3
f1 : σ1
f2 : σ2
f3 : σ3
⊢ Limplies α f1 f2 → Limplies α f2 f3 → Limplies α f1 f3

Tactic:
intros f1_implies_f2 f2_implies_f3 a a_entails_f1

Result:
α : Type u
σ1 : Type v
σ2 : Type w
σ3 : Type x
inst✝² : Entails α σ1
inst✝¹ : Entails α σ2
inst✝ : Entails α σ3
f1 : σ1
f2 : σ2
f3 : σ3
f1_implies_f2 : Limplies α f1 f2
f2_implies_f3 : Limplies α f2 f3
a : α → Bool
a_entails_f1 : a ⊨ f1
⊢ a ⊨ f3
-- Mathlib/Algebra/Module/LinearMap/Defs.lean
theorem toLinearMap_injective {F : Type*} [FunLike F M M₃] [SemilinearMapClass F σ M M₃]
    {f g : F} (h : (f : M →ₛₗ[σ] M₃) = (g : M →ₛₗ[σ] M₃)) :
    f = g

Proof state:
case h
R : Type u_1
S : Type u_5
M : Type u_8
M₃ : Type u_11
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module S M₃
σ : R →+* S
F : Type u_14
inst✝¹ : FunLike F M M₃
inst✝ : SemilinearMapClass F σ M M₃
f g : F
h : ↑f = ↑g
m : M
⊢ f m = g m

Tactic:
exact DFunLike.congr_fun h m

Result:
no goals

Proof state:
case h
R : Type u_1
S : Type u_5
M : Type u_8
M₃ : Type u_11
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module S M₃
σ : R →+* S
F : Type u_14
inst✝¹ : FunLike F M M₃
inst✝ : SemilinearMapClass F σ M M₃
f g : F
h : ↑f = ↑g
⊢ ∀ (x : M), f x = g x

Tactic:
intro m

Result:
case h
R : Type u_1
S : Type u_5
M : Type u_8
M₃ : Type u_11
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module S M₃
σ : R →+* S
F : Type u_14
inst✝¹ : FunLike F M M₃
inst✝ : SemilinearMapClass F σ M M₃
f g : F
h : ↑f = ↑g
m : M
⊢ f m = g m

Proof state:
R : Type u_1
S : Type u_5
M : Type u_8
M₃ : Type u_11
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module S M₃
σ : R →+* S
F : Type u_14
inst✝¹ : FunLike F M M₃
inst✝ : SemilinearMapClass F σ M M₃
f g : F
h : ↑f = ↑g
⊢ f = g

Tactic:
apply DFunLike.ext

Result:
case h
R : Type u_1
S : Type u_5
M : Type u_8
M₃ : Type u_11
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module S M₃
σ : R →+* S
F : Type u_14
inst✝¹ : FunLike F M M₃
inst✝ : SemilinearMapClass F σ M M₃
f g : F
h : ↑f = ↑g
⊢ ∀ (x : M), f x = g x
-- Mathlib/LinearAlgebra/Ray.lean
theorem sameRay_neg_iff : SameRay R (-x) (-y) ↔ SameRay R x y

Proof state:
R : Type u_1
inst✝² : StrictOrderedCommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
⊢ SameRay R (-x) (-y) ↔ SameRay R x y

Tactic:
simp only [SameRay, neg_eq_zero, smul_neg, neg_inj]

Result:
no goals
-- Mathlib/Probability/CondVar.lean
@[simp]
lemma condVar_const (hm : m ≤ m₀) (c : ℝ) : Var[fun _ ↦ c; μ | m] = 0

Proof state:
case inl
Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
hm : m ≤ m₀
⊢ Var[fun x => 0; μ | m] = 0

Tactic:
simp [← Pi.zero_def]

Result:
no goals

Proof state:
case pos
Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
hm : m ≤ m₀
c : ℝ
hc : c ≠ 0
hμm : IsFiniteMeasure μ
⊢ Var[fun x => c; μ | m] = 0

Tactic:
simp [condVar, hm, Pi.pow_def]

Result:
no goals

Proof state:
case inr
Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
hm : m ≤ m₀
c : ℝ
hc : c ≠ 0
⊢ Var[fun x => c; μ | m] = 0

Tactic:
by_cases hμm : IsFiniteMeasure μ

Result:
case pos
Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
hm : m ≤ m₀
c : ℝ
hc : c ≠ 0
hμm : IsFiniteMeasure μ
⊢ Var[fun x => c; μ | m] = 0

case neg
Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
hm : m ≤ m₀
c : ℝ
hc : c ≠ 0
hμm : ¬IsFiniteMeasure μ
⊢ Var[fun x => c; μ | m] = 0

Proof state:
case neg
Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
hm : m ≤ m₀
c : ℝ
hc : c ≠ 0
hμm : ¬IsFiniteMeasure μ
⊢ Var[fun x => c; μ | m] = 0

Tactic:
simp [condVar, condExp_of_not_integrable, integrable_const_iff_isFiniteMeasure hc,
  integrable_const_iff_isFiniteMeasure <| pow_ne_zero _ hc, hμm, Pi.pow_def]

Result:
no goals

Proof state:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
hm : m ≤ m₀
c : ℝ
⊢ Var[fun x => c; μ | m] = 0

Tactic:
obtain rfl | hc := eq_or_ne c 0

Result:
case inl
Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
hm : m ≤ m₀
⊢ Var[fun x => 0; μ | m] = 0

case inr
Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
hm : m ≤ m₀
c : ℝ
hc : c ≠ 0
⊢ Var[fun x => c; μ | m] = 0
-- Mathlib/Algebra/Polynomial/Smeval.lean
theorem smeval_assoc_X_pow (m n : ℕ) :
    p.smeval x * x ^ m * x ^ n = p.smeval x * (x ^ m * x ^ n)

Proof state:
case h_monomial
R : Type u_1
inst✝⁵ : Semiring R
p : R[X]
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Module R S
inst✝² : Pow S ℕ
x : S
inst✝¹ : NatPowAssoc S
inst✝ : IsScalarTower R S S
m n✝ n : ℕ
a : R
⊢ ((monomial n) a).smeval x * x ^ m * x ^ n✝ = ((monomial n) a).smeval x * (x ^ m * x ^ n✝)

Tactic:
rw [smeval_monomial, smul_mul_assoc, smul_mul_assoc, npow_mul_assoc, ← smul_mul_assoc]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁵ : Semiring R
p : R[X]
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Module R S
inst✝² : Pow S ℕ
x : S
inst✝¹ : NatPowAssoc S
inst✝ : IsScalarTower R S S
m n : ℕ
⊢ p.smeval x * x ^ m * x ^ n = p.smeval x * (x ^ m * x ^ n)

Tactic:
induction p using Polynomial.induction_on' with
| h_add p q ph qh =>
  simp only [smeval_add, ph, qh, add_mul]
| h_monomial n a =>
  rw [smeval_monomial, smul_mul_assoc, smul_mul_assoc, npow_mul_assoc, ← smul_mul_assoc]

Result:
no goals

Proof state:
case h_add
R : Type u_1
inst✝⁵ : Semiring R
p✝ : R[X]
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Module R S
inst✝² : Pow S ℕ
x : S
inst✝¹ : NatPowAssoc S
inst✝ : IsScalarTower R S S
m n : ℕ
p q : R[X]
ph : p.smeval x * x ^ m * x ^ n = p.smeval x * (x ^ m * x ^ n)
qh : q.smeval x * x ^ m * x ^ n = q.smeval x * (x ^ m * x ^ n)
⊢ (p + q).smeval x * x ^ m * x ^ n = (p + q).smeval x * (x ^ m * x ^ n)

Tactic:
simp only [smeval_add, ph, qh, add_mul]

Result:
no goals
-- Mathlib/Data/Matroid/Restrict.lean
theorem ofMatroid_lt_iff {M M' : Matroid α} :
    Matroidᵣ.ofMatroid M < Matroidᵣ.ofMatroid M' ↔ M <r M'

Proof state:
α : Type u_1
M M' : Matroid α
⊢ { toMatroid := M } < { toMatroid := M' } ↔ M <r M'

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Homology/Homotopy.lean
theorem prevD_succ_cochainComplex (f : ∀ i j, P.X i ⟶ Q.X j) (i : ℕ) :
    prevD (i + 1) f = f (i + 1) _ ≫ Q.d i (i + 1)

Proof state:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : CochainComplex V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
i : ℕ
this : (ComplexShape.up ℕ).prev (i + 1) = i
⊢ f (i + 1) ((ComplexShape.up ℕ).prev (i + 1)) ≫ Q.d ((ComplexShape.up ℕ).prev (i + 1)) (i + 1) =
    f (i + 1) i ≫ Q.d i (i + 1)

Tactic:
congr 2

Result:
no goals

Proof state:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : CochainComplex V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
i : ℕ
⊢ (prevD (i + 1)) f = f (i + 1) i ≫ Q.d i (i + 1)

Tactic:
dsimp [prevD]

Result:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : CochainComplex V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
i : ℕ
⊢ f (i + 1) ((ComplexShape.up ℕ).prev (i + 1)) ≫ Q.d ((ComplexShape.up ℕ).prev (i + 1)) (i + 1) =
    f (i + 1) i ≫ Q.d i (i + 1)

Proof state:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : CochainComplex V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
i : ℕ
⊢ f (i + 1) ((ComplexShape.up ℕ).prev (i + 1)) ≫ Q.d ((ComplexShape.up ℕ).prev (i + 1)) (i + 1) =
    f (i + 1) i ≫ Q.d i (i + 1)

Tactic:
have : (ComplexShape.up ℕ).prev (i + 1) = i := CochainComplex.prev_nat_succ i

Result:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : CochainComplex V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
i : ℕ
this : (ComplexShape.up ℕ).prev (i + 1) = i
⊢ f (i + 1) ((ComplexShape.up ℕ).prev (i + 1)) ≫ Q.d ((ComplexShape.up ℕ).prev (i + 1)) (i + 1) =
    f (i + 1) i ≫ Q.d i (i + 1)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/IntList.lean
theorem gcd_cons_div_right' : (gcd (x::xs) : Int) ∣ (gcd xs : Int)

Proof state:
x : Int
xs : List Int
⊢ ↑(gcd (x :: xs)) ∣ ↑(gcd xs)

Tactic:
rw [Int.ofNat_dvd_left, Int.natAbs_ofNat]

Result:
x : Int
xs : List Int
⊢ gcd (x :: xs) ∣ gcd xs

Proof state:
x : Int
xs : List Int
⊢ gcd (x :: xs) ∣ gcd xs

Tactic:
exact gcd_cons_div_right

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean
theorem homeomorphCircle_apply (hT : T ≠ 0) (x : AddCircle T) :
    homeomorphCircle hT x = toCircle x

Proof state:
T : ℝ
hT : T ≠ 0
x : AddCircle T
⊢ (homeomorphCircle hT) x = x.toCircle

Tactic:
induction' x using QuotientAddGroup.induction_on with x

Result:
case H
T : ℝ
hT : T ≠ 0
x : ℝ
⊢ (homeomorphCircle hT) ↑x = toCircle ↑x

Proof state:
case H
T : ℝ
hT : T ≠ 0
x : ℝ
⊢ Circle.exp (x * (T⁻¹ * (2 * π))) = Circle.exp (2 * π / T * x)

Tactic:
ring_nf

Result:
no goals

Proof state:
case H
T : ℝ
hT : T ≠ 0
x : ℝ
⊢ (homeomorphCircle hT) ↑x = toCircle ↑x

Tactic:
rw [homeomorphCircle, Homeomorph.trans_apply,
  homeomorphAddCircle_apply_mk, homeomorphCircle'_apply_mk, toCircle_apply_mk]

Result:
case H
T : ℝ
hT : T ≠ 0
x : ℝ
⊢ Circle.exp (x * (T⁻¹ * (2 * π))) = Circle.exp (2 * π / T * x)
-- Mathlib/CategoryTheory/Sites/LocallySurjective.lean
theorem isLocallySurjective_of_surjective {F G : Cᵒᵖ ⥤ A} (f : F ⟶ G)
    (H : ∀ U, Function.Surjective (f.app U)) : IsLocallySurjective J f where
  imageSieve_mem {U} s

Proof state:
case intro
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝¹ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝ : ConcreteCategory A FA
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
H : ∀ (U : Cᵒᵖ), Function.Surjective ⇑(ConcreteCategory.hom (f.app U))
U : C
t : CA (F.obj (op U))
⊢ imageSieve f ((ConcreteCategory.hom (f.app (op U))) t) ∈ J U

Tactic:
rw [imageSieve_app]

Result:
case intro
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝¹ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝ : ConcreteCategory A FA
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
H : ∀ (U : Cᵒᵖ), Function.Surjective ⇑(ConcreteCategory.hom (f.app U))
U : C
t : CA (F.obj (op U))
⊢ ⊤ ∈ J U

Proof state:
case intro
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝¹ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝ : ConcreteCategory A FA
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
H : ∀ (U : Cᵒᵖ), Function.Surjective ⇑(ConcreteCategory.hom (f.app U))
U : C
t : CA (F.obj (op U))
⊢ ⊤ ∈ J U

Tactic:
exact J.top_mem _

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝¹ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝ : ConcreteCategory A FA
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
H : ∀ (U : Cᵒᵖ), Function.Surjective ⇑(ConcreteCategory.hom (f.app U))
U : C
s : ToType (G.obj (op U))
⊢ imageSieve f s ∈ J U

Tactic:
obtain ⟨t, rfl⟩ := H _ s

Result:
case intro
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝¹ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝ : ConcreteCategory A FA
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
H : ∀ (U : Cᵒᵖ), Function.Surjective ⇑(ConcreteCategory.hom (f.app U))
U : C
t : CA (F.obj (op U))
⊢ imageSieve f ((ConcreteCategory.hom (f.app (op U))) t) ∈ J U
-- Mathlib/SetTheory/Game/Birthday.lean
theorem birthday_one : birthday 1 = 1

Proof state:
⊢ birthday 1 = 1

Tactic:
rw [← Nat.cast_one, birthday_natCast, Nat.cast_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem_toList {α n} (xs : Vector α n) (i : Nat) (h : i < xs.toList.length) :
    xs.toList[i] = xs[i]'(by simpa using h)

Proof state:
case mk
α : Type u_1
n i : Nat
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
h : i < { toArray := toArray✝, size_toArray := size_toArray✝ }.toList.length
⊢ { toArray := toArray✝, size_toArray := size_toArray✝ }.toList[i] =
    { toArray := toArray✝, size_toArray := size_toArray✝ }[i]

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n : Nat
xs : Vector α n
i : Nat
h : i < xs.toList.length
⊢ xs.toList[i] = xs[i]

Tactic:
cases xs

Result:
case mk
α : Type u_1
n i : Nat
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
h : i < { toArray := toArray✝, size_toArray := size_toArray✝ }.toList.length
⊢ { toArray := toArray✝, size_toArray := size_toArray✝ }.toList[i] =
    { toArray := toArray✝, size_toArray := size_toArray✝ }[i]

Proof state:
α : Type ?u.54660
n : Nat
xs : Vector α n
i : Nat
h : i < xs.toList.length
⊢ i < n

Tactic:
simpa using h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem exists_eq_add_one : (∃ n, a = n + 1) ↔ 0 < a :=
  ⟨fun ⟨n, h⟩ => by omega, fun h => ⟨a - 1, by omega⟩⟩

Proof state:
a : Nat
x✝ : ∃ n, a = n + 1
n : Nat
h : a = n + 1
⊢ 0 < a

Tactic:
omega

Result:
no goals

Proof state:
a : Nat
h : 0 < a
⊢ a = a - 1 + 1

Tactic:
omega

Result:
no goals
-- Mathlib/Topology/UniformSpace/Cauchy.lean
theorem complete_univ {α : Type u} [UniformSpace α] [CompleteSpace α] :
    IsComplete (univ : Set α) := fun f hf _ => by
  rcases CompleteSpace.complete hf with ⟨x, hx⟩
  exact ⟨x, mem_univ x, hx⟩

Proof state:
α : Type u
inst✝¹ : UniformSpace α
inst✝ : CompleteSpace α
f : Filter α
hf : Cauchy f
x✝ : f ≤ 𝓟 univ
⊢ ∃ x ∈ univ, f ≤ 𝓝 x

Tactic:
rcases CompleteSpace.complete hf with ⟨x, hx⟩

Result:
case intro
α : Type u
inst✝¹ : UniformSpace α
inst✝ : CompleteSpace α
f : Filter α
hf : Cauchy f
x✝ : f ≤ 𝓟 univ
x : α
hx : f ≤ 𝓝 x
⊢ ∃ x ∈ univ, f ≤ 𝓝 x

Proof state:
case intro
α : Type u
inst✝¹ : UniformSpace α
inst✝ : CompleteSpace α
f : Filter α
hf : Cauchy f
x✝ : f ≤ 𝓟 univ
x : α
hx : f ≤ 𝓝 x
⊢ ∃ x ∈ univ, f ≤ 𝓝 x

Tactic:
exact ⟨x, mem_univ x, hx⟩

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem unbounded_of_unbounded_sUnion (r : α → α → Prop) [wo : IsWellOrder α r] {s : Set (Set α)}
    (h₁ : Unbounded r <| ⋃₀ s) (h₂ : #s < Order.cof (swap rᶜ)) : ∃ x ∈ s, Unbounded r x

Proof state:
α : Type u
r : α → α → Prop
wo : IsWellOrder α r
s : Set (Set α)
h₁ : Unbounded r (⋃₀ s)
h₂ : #↑s < Order.cof (swap rᶜ)
h : ∀ x ∈ s, ¬Unbounded r x
⊢ False

Tactic:
simp_rw [not_unbounded_iff] at h

Result:
α : Type u
r : α → α → Prop
wo : IsWellOrder α r
s : Set (Set α)
h₁ : Unbounded r (⋃₀ s)
h₂ : #↑s < Order.cof (swap rᶜ)
h : ∀ x ∈ s, Bounded r x
⊢ False

Proof state:
α : Type u
r : α → α → Prop
wo : IsWellOrder α r
s : Set (Set α)
h₁ : Unbounded r (⋃₀ s)
h₂ : #↑s < Order.cof (swap rᶜ)
h : ∀ x ∈ s, Bounded r x
f : ↑s → α := fun x => ⋯.sup ↑x ⋯
⊢ False

Tactic:
refine h₂.not_le (le_trans (csInf_le' ⟨range f, fun x => ?_, rfl⟩) mk_range_le)

Result:
α : Type u
r : α → α → Prop
wo : IsWellOrder α r
s : Set (Set α)
h₁ : Unbounded r (⋃₀ s)
h₂ : #↑s < Order.cof (swap rᶜ)
h : ∀ x ∈ s, Bounded r x
f : ↑s → α := fun x => ⋯.sup ↑x ⋯
x : α
⊢ ∃ b ∈ range f, swap rᶜ x b

Proof state:
case intro.intro.intro.intro
α : Type u
r : α → α → Prop
wo : IsWellOrder α r
s : Set (Set α)
h₁ : Unbounded r (⋃₀ s)
h₂ : #↑s < Order.cof (swap rᶜ)
h : ∀ x ∈ s, Bounded r x
f : ↑s → α := fun x => ⋯.sup ↑x ⋯
x y : α
hxy : ¬r y x
c : Set α
hc : c ∈ s
hy : y ∈ c
⊢ ∃ b ∈ range f, swap rᶜ x b

Tactic:
exact ⟨f ⟨c, hc⟩, mem_range_self _, fun hxz => hxy (Trans.trans (wo.wf.lt_sup _ hy) hxz)⟩

Result:
no goals

Proof state:
α : Type u
r : α → α → Prop
wo : IsWellOrder α r
s : Set (Set α)
h₁ : Unbounded r (⋃₀ s)
h₂ : #↑s < Order.cof (swap rᶜ)
h : ∀ x ∈ s, Bounded r x
⊢ False

Tactic:
let f : s → α := fun x : s => wo.wf.sup x (h x.1 x.2)

Result:
α : Type u
r : α → α → Prop
wo : IsWellOrder α r
s : Set (Set α)
h₁ : Unbounded r (⋃₀ s)
h₂ : #↑s < Order.cof (swap rᶜ)
h : ∀ x ∈ s, Bounded r x
f : ↑s → α := fun x => ⋯.sup ↑x ⋯
⊢ False

Proof state:
α : Type u
r : α → α → Prop
wo : IsWellOrder α r
s : Set (Set α)
h₁ : Unbounded r (⋃₀ s)
h₂ : #↑s < Order.cof (swap rᶜ)
h : ∀ x ∈ s, Bounded r x
f : ↑s → α := fun x => ⋯.sup ↑x ⋯
x : α
⊢ ∃ b ∈ range f, swap rᶜ x b

Tactic:
rcases h₁ x with ⟨y, ⟨c, hc, hy⟩, hxy⟩

Result:
case intro.intro.intro.intro
α : Type u
r : α → α → Prop
wo : IsWellOrder α r
s : Set (Set α)
h₁ : Unbounded r (⋃₀ s)
h₂ : #↑s < Order.cof (swap rᶜ)
h : ∀ x ∈ s, Bounded r x
f : ↑s → α := fun x => ⋯.sup ↑x ⋯
x y : α
hxy : ¬r y x
c : Set α
hc : c ∈ s
hy : y ∈ c
⊢ ∃ b ∈ range f, swap rᶜ x b

Proof state:
α : Type u
r : α → α → Prop
wo : IsWellOrder α r
s : Set (Set α)
h₁ : Unbounded r (⋃₀ s)
h₂ : #↑s < Order.cof (swap rᶜ)
⊢ ∃ x ∈ s, Unbounded r x

Tactic:
by_contra! h

Result:
α : Type u
r : α → α → Prop
wo : IsWellOrder α r
s : Set (Set α)
h₁ : Unbounded r (⋃₀ s)
h₂ : #↑s < Order.cof (swap rᶜ)
h : ∀ x ∈ s, ¬Unbounded r x
⊢ False
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem norm_inner_le_norm (x y : E) : ‖⟪x, y⟫‖ ≤ ‖x‖ * ‖y‖

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ ‖⟪x, y⟫_𝕜‖ ≤ √(re ⟪x, x⟫_𝕜) * √(re ⟪y, y⟫_𝕜)

Tactic:
letI : PreInnerProductSpace.Core 𝕜 E := PreInnerProductSpace.toCore

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
this : PreInnerProductSpace.Core 𝕜 E := PreInnerProductSpace.toCore
⊢ ‖⟪x, y⟫_𝕜‖ ≤ √(re ⟪x, x⟫_𝕜) * √(re ⟪y, y⟫_𝕜)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ ‖⟪x, y⟫_𝕜‖ ≤ ‖x‖ * ‖y‖

Tactic:
rw [norm_eq_sqrt_inner (𝕜 := 𝕜) x, norm_eq_sqrt_inner (𝕜 := 𝕜) y]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ ‖⟪x, y⟫_𝕜‖ ≤ √(re ⟪x, x⟫_𝕜) * √(re ⟪y, y⟫_𝕜)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
this : PreInnerProductSpace.Core 𝕜 E := PreInnerProductSpace.toCore
⊢ ‖⟪x, y⟫_𝕜‖ ≤ √(re ⟪x, x⟫_𝕜) * √(re ⟪y, y⟫_𝕜)

Tactic:
exact InnerProductSpace.Core.norm_inner_le_norm x y

Result:
no goals