harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean
theorem one_add_mul_self_le_rpow_one_add {s : ℝ} (hs : -1 ≤ s) {p : ℝ} (hp : 1 ≤ p) :
    1 + p * s ≤ (1 + s) ^ p

Proof state:
s : ℝ
hs : -1 ≤ s
p : ℝ
hp : 1 ≤ p
⊢ 1 + p * s ≤ (1 + s) ^ p

Tactic:
rcases eq_or_lt_of_le hp with (rfl | hp)

Result:
case inl
s : ℝ
hs : -1 ≤ s
hp : 1 ≤ 1
⊢ 1 + 1 * s ≤ (1 + s) ^ 1

case inr
s : ℝ
hs : -1 ≤ s
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
⊢ 1 + p * s ≤ (1 + s) ^ p

Proof state:
case inl
s : ℝ
hs : -1 ≤ s
hp : 1 ≤ 1
⊢ 1 + 1 * s ≤ (1 + s) ^ 1

Tactic:
simp

Result:
no goals

Proof state:
case pos
s : ℝ
hs : -1 ≤ s
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
hs' : s = 0
⊢ 1 + p * s ≤ (1 + s) ^ p

Tactic:
simp [hs']

Result:
no goals

Proof state:
case neg
s : ℝ
hs : -1 ≤ s
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
hs' : ¬s = 0
⊢ 1 + p * s ≤ (1 + s) ^ p

Tactic:
exact (one_add_mul_self_lt_rpow_one_add hs hs' hp).le

Result:
no goals

Proof state:
case inr
s : ℝ
hs : -1 ≤ s
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
⊢ 1 + p * s ≤ (1 + s) ^ p

Tactic:
by_cases hs' : s = 0

Result:
case pos
s : ℝ
hs : -1 ≤ s
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
hs' : s = 0
⊢ 1 + p * s ≤ (1 + s) ^ p

case neg
s : ℝ
hs : -1 ≤ s
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
hs' : ¬s = 0
⊢ 1 + p * s ≤ (1 + s) ^ p
-- Mathlib/Analysis/NormedSpace/HahnBanach/SeparatingDual.lean
theorem t2Space [T2Space R] : T2Space V

Proof state:
R : Type u_1
V : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup V
inst✝⁴ : TopologicalSpace V
inst✝³ : TopologicalSpace R
inst✝² : Module R V
inst✝¹ : SeparatingDual R V
inst✝ : T2Space R
⊢ T2Space V

Tactic:
apply (t2Space_iff _).2 (fun {x} {y} hxy ↦ ?_)

Result:
R : Type u_1
V : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup V
inst✝⁴ : TopologicalSpace V
inst✝³ : TopologicalSpace R
inst✝² : Module R V
inst✝¹ : SeparatingDual R V
inst✝ : T2Space R
x y : V
hxy : x ≠ y
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v

Proof state:
R : Type u_1
V : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup V
inst✝⁴ : TopologicalSpace V
inst✝³ : TopologicalSpace R
inst✝² : Module R V
inst✝¹ : SeparatingDual R V
inst✝ : T2Space R
x y : V
hxy : x ≠ y
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v

Tactic:
rcases exists_separating_of_ne (R := R) hxy with ⟨f, hf⟩

Result:
case intro
R : Type u_1
V : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup V
inst✝⁴ : TopologicalSpace V
inst✝³ : TopologicalSpace R
inst✝² : Module R V
inst✝¹ : SeparatingDual R V
inst✝ : T2Space R
x y : V
hxy : x ≠ y
f : V →L[R] R
hf : f x ≠ f y
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v

Proof state:
case intro
R : Type u_1
V : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup V
inst✝⁴ : TopologicalSpace V
inst✝³ : TopologicalSpace R
inst✝² : Module R V
inst✝¹ : SeparatingDual R V
inst✝ : T2Space R
x y : V
hxy : x ≠ y
f : V →L[R] R
hf : f x ≠ f y
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v

Tactic:
exact separated_by_continuous f.continuous hf

Result:
no goals
-- Mathlib/Data/Nat/Cast/Order/Field.lean
theorem cast_div_le {m n : ℕ} : ((m / n : ℕ) : α) ≤ m / n

Proof state:
case succ
α : Type u_1
inst✝ : LinearOrderedSemifield α
m n✝ : ℕ
⊢ 0 < ↑(n✝ + 1)

Tactic:
exact Nat.cast_pos.2 (Nat.succ_pos _)

Result:
no goals

Proof state:
case succ
α : Type u_1
inst✝ : LinearOrderedSemifield α
m n✝ : ℕ
⊢ m / (n✝ + 1) * (n✝ + 1) ≤ m

Tactic:
exact Nat.div_mul_le_self m _

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedSemifield α
m n : ℕ
⊢ ↑(m / n) ≤ ↑m / ↑n

Tactic:
cases n

Result:
case zero
α : Type u_1
inst✝ : LinearOrderedSemifield α
m : ℕ
⊢ ↑(m / 0) ≤ ↑m / ↑0

case succ
α : Type u_1
inst✝ : LinearOrderedSemifield α
m n✝ : ℕ
⊢ ↑(m / (n✝ + 1)) ≤ ↑m / ↑(n✝ + 1)

Proof state:
case succ
α : Type u_1
inst✝ : LinearOrderedSemifield α
m n✝ : ℕ
⊢ ↑(m / (n✝ + 1)) ≤ ↑m / ↑(n✝ + 1)

Tactic:
rw [le_div_iff₀, ← Nat.cast_mul, @Nat.cast_le]

Result:
case succ
α : Type u_1
inst✝ : LinearOrderedSemifield α
m n✝ : ℕ
⊢ m / (n✝ + 1) * (n✝ + 1) ≤ m

case succ
α : Type u_1
inst✝ : LinearOrderedSemifield α
m n✝ : ℕ
⊢ 0 < ↑(n✝ + 1)

Proof state:
case zero
α : Type u_1
inst✝ : LinearOrderedSemifield α
m : ℕ
⊢ ↑(m / 0) ≤ ↑m / ↑0

Tactic:
rw [cast_zero, div_zero, Nat.div_zero, cast_zero]

Result:
no goals
-- Mathlib/Order/Filter/Basic.lean
theorem EventuallyEq.prod_mk {l} {f f' : α → β} (hf : f =ᶠ[l] f') {g g' : α → γ} (hg : g =ᶠ[l] g') :
    (fun x => (f x, g x)) =ᶠ[l] fun x => (f' x, g' x) :=
  hf.mp <|
    hg.mono <| by
      intros
      simp only [*]

Proof state:
α : Type u
β : Type v
γ : Type w
l : Filter α
f f' : α → β
hf : f =ᶠ[l] f'
g g' : α → γ
hg : g =ᶠ[l] g'
x✝ : α
a✝¹ : g x✝ = g' x✝
a✝ : f x✝ = f' x✝
⊢ (fun x => (f x, g x)) x✝ = (fun x => (f' x, g' x)) x✝

Tactic:
simp only [*]

Result:
no goals

Proof state:
α : Type u
β : Type v
γ : Type w
l : Filter α
f f' : α → β
hf : f =ᶠ[l] f'
g g' : α → γ
hg : g =ᶠ[l] g'
⊢ ∀ (x : α), g x = g' x → f x = f' x → (fun x => (f x, g x)) x = (fun x => (f' x, g' x)) x

Tactic:
intros

Result:
α : Type u
β : Type v
γ : Type w
l : Filter α
f f' : α → β
hf : f =ᶠ[l] f'
g g' : α → γ
hg : g =ᶠ[l] g'
x✝ : α
a✝¹ : g x✝ = g' x✝
a✝ : f x✝ = f' x✝
⊢ (fun x => (f x, g x)) x✝ = (fun x => (f' x, g' x)) x✝
-- Mathlib/Algebra/Order/Ring/Unbundled/Rat.lean
theorem ofScientific_nonneg (m : ℕ) (s : Bool) (e : ℕ) :
    0 ≤ Rat.ofScientific m s e

Proof state:
m : ℕ
s : Bool
e : ℕ
⊢ 0 ≤ Rat.ofScientific m s e

Tactic:
rw [Rat.ofScientific]

Result:
m : ℕ
s : Bool
e : ℕ
⊢ 0 ≤ if s = true then normalize (↑m) (10 ^ e) ⋯ else ↑(m * 10 ^ e)

Proof state:
case true
m e : ℕ
⊢ 0 ≤ if true = true then normalize (↑m) (10 ^ e) ⋯ else ↑(m * 10 ^ e)

Tactic:
rw [if_pos rfl, normalize_eq_mkRat]

Result:
case true
m e : ℕ
⊢ 0 ≤ mkRat (↑m) (10 ^ e)

Proof state:
case false
m e : ℕ
⊢ 0 ≤ ↑(m * 10 ^ e)

Tactic:
exact Int.natCast_nonneg _

Result:
no goals

Proof state:
case true
m e : ℕ
⊢ 0 ≤ mkRat (↑m) (10 ^ e)

Tactic:
exact Rat.mkRat_nonneg (Int.natCast_nonneg _) _

Result:
no goals

Proof state:
m e : ℕ
⊢ ¬false = true

Tactic:
decide

Result:
no goals

Proof state:
m : ℕ
s : Bool
e : ℕ
⊢ 0 ≤ if s = true then normalize (↑m) (10 ^ e) ⋯ else ↑(m * 10 ^ e)

Tactic:
cases s

Result:
case false
m e : ℕ
⊢ 0 ≤ if false = true then normalize (↑m) (10 ^ e) ⋯ else ↑(m * 10 ^ e)

case true
m e : ℕ
⊢ 0 ≤ if true = true then normalize (↑m) (10 ^ e) ⋯ else ↑(m * 10 ^ e)

Proof state:
case false
m e : ℕ
⊢ 0 ≤ if false = true then normalize (↑m) (10 ^ e) ⋯ else ↑(m * 10 ^ e)

Tactic:
rw [if_neg (by decide)]

Result:
case false
m e : ℕ
⊢ 0 ≤ ↑(m * 10 ^ e)

Proof state:
case false
m e : ℕ
⊢ 0 ≤ (↑(m * 10 ^ e)).num

Tactic:
rw [num_natCast]

Result:
case false
m e : ℕ
⊢ 0 ≤ ↑(m * 10 ^ e)

Proof state:
case false
m e : ℕ
⊢ 0 ≤ ↑(m * 10 ^ e)

Tactic:
refine num_nonneg.mp ?_

Result:
case false
m e : ℕ
⊢ 0 ≤ (↑(m * 10 ^ e)).num
-- Mathlib/Logic/Equiv/Fin.lean
theorem finRotate_succ_apply (i : Fin (n + 1)) : finRotate (n + 1) i = i + 1

Proof state:
n : ℕ
i : Fin (n + 1)
⊢ (finRotate (n + 1)) i = i + 1

Tactic:
cases n

Result:
case zero
i : Fin (0 + 1)
⊢ (finRotate (0 + 1)) i = i + 1

case succ
n✝ : ℕ
i : Fin (n✝ + 1 + 1)
⊢ (finRotate (n✝ + 1 + 1)) i = i + 1

Proof state:
case succ.inr
n✝ : ℕ
i : Fin (n✝ + 1 + 1)
h : i < Fin.last (n✝ + 1)
⊢ (finRotate (n✝ + 1 + 1)) i = i + 1

Tactic:
cases i

Result:
case succ.inr.mk
n✝ val✝ : ℕ
isLt✝ : val✝ < n✝ + 1 + 1
h : ⟨val✝, isLt✝⟩ < Fin.last (n✝ + 1)
⊢ (finRotate (n✝ + 1 + 1)) ⟨val✝, isLt✝⟩ = ⟨val✝, isLt✝⟩ + 1

Proof state:
case succ
n✝ : ℕ
i : Fin (n✝ + 1 + 1)
⊢ (finRotate (n✝ + 1 + 1)) i = i + 1

Tactic:
obtain rfl | h := Fin.eq_or_lt_of_le i.le_last

Result:
case succ.inl
n✝ : ℕ
⊢ (finRotate (n✝ + 1 + 1)) (Fin.last (n✝ + 1)) = Fin.last (n✝ + 1) + 1

case succ.inr
n✝ : ℕ
i : Fin (n✝ + 1 + 1)
h : i < Fin.last (n✝ + 1)
⊢ (finRotate (n✝ + 1 + 1)) i = i + 1

Proof state:
case zero
i : Fin (0 + 1)
⊢ (finRotate (0 + 1)) i = i + 1

Tactic:
exact @Subsingleton.elim (Fin 1) _ _ _

Result:
no goals

Proof state:
case succ.inr.mk
n✝ val✝ : ℕ
isLt✝ : val✝ < n✝ + 1 + 1
h : ⟨val✝, isLt✝⟩ < Fin.last (n✝ + 1)
⊢ (finRotate (n✝ + 1 + 1)) ⟨val✝, isLt✝⟩ = ⟨val✝, isLt✝⟩ + 1

Tactic:
simp only [Fin.lt_iff_val_lt_val, Fin.val_last, Fin.val_mk] at h

Result:
case succ.inr.mk
n✝ val✝ : ℕ
isLt✝ : val✝ < n✝ + 1 + 1
h : val✝ < n✝ + 1
⊢ (finRotate (n✝ + 1 + 1)) ⟨val✝, isLt✝⟩ = ⟨val✝, isLt✝⟩ + 1

Proof state:
case succ.inr.mk
n✝ val✝ : ℕ
isLt✝ : val✝ < n✝ + 1 + 1
h : val✝ < n✝ + 1
⊢ (finRotate (n✝ + 1 + 1)) ⟨val✝, isLt✝⟩ = ⟨val✝, isLt✝⟩ + 1

Tactic:
simp [finRotate_of_lt h, Fin.ext_iff, Fin.add_def, Nat.mod_eq_of_lt (Nat.succ_lt_succ h)]

Result:
no goals

Proof state:
case succ.inl
n✝ : ℕ
⊢ (finRotate (n✝ + 1 + 1)) (Fin.last (n✝ + 1)) = Fin.last (n✝ + 1) + 1

Tactic:
simp [finRotate_last]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Perm.lean
theorem set_set_perm' {as : List α} {i j : Nat} (h₁ : i < as.length) (h₂ : i + j < as.length)
    (hj : 0 < j) :
    (as.set i as[i + j]).set (i + j) as[i] ~ as

Proof state:
case a
α : Type u_1
as : List α
i j : Nat
h₁ : i < as.length
h₂ : i + j < as.length
hj : 0 < j
this : as = take i as ++ as[i] :: drop (i + 1) (take (i + j) as) ++ as[i + j] :: drop (i + j + 1) as
⊢ as[i + j] :: drop (i + 1) (take (i + j) as) ++ as[i] :: drop (i + j + 1) as ~
    as[i] :: drop (i + 1) (take (i + j) as) ++ as[i + j] :: drop (i + j + 1) as

Tactic:
apply cons_append_cons_perm

Result:
no goals
-- Mathlib/Order/SuccPred/Limit.lean
theorem isSuccLimitRecOn_succ_of_not_isMax (hb : ¬ IsMax b) :
    isSuccLimitRecOn (succ b) hm hs hl = hs b hb

Proof state:
α : Type u_1
b : α
C : α → Sort u_2
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
hm : (a : α) → IsMin a → C a
hs : (a : α) → ¬IsMax a → C (succ a)
hl : (a : α) → IsSuccLimit a → C a
hb : ¬IsMax b
⊢ isSuccLimitRecOn (succ b) hm hs hl = hs b hb

Tactic:
rw [isSuccLimitRecOn, isSuccPrelimitRecOn_succ_of_not_isMax]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Over.lean
@[simp]
lemma overEquiv_symm_top {X : C} (Y : Over X) :
    (overEquiv Y).symm ⊤ = ⊤ :=
  (overEquiv Y).injective (by simp)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
⊢ (overEquiv Y) ((overEquiv Y).symm ⊤) = (overEquiv Y) ⊤

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/CharP/Defs.lean
lemma ringChar_ne_one [Nontrivial R] : ringChar R ≠ 1

Proof state:
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
h : ringChar R = 1
⊢ 0 = 1

Tactic:
symm

Result:
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
h : ringChar R = 1
⊢ 1 = 0

Proof state:
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
h : ringChar R = 1
⊢ False

Tactic:
apply zero_ne_one' R

Result:
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
h : ringChar R = 1
⊢ 0 = 1

Proof state:
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
h : ringChar R = 1
⊢ 1 = 0

Tactic:
rw [← Nat.cast_one, ringChar.spec, h]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
⊢ ringChar R ≠ 1

Tactic:
intro h

Result:
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
h : ringChar R = 1
⊢ False
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem mem_rootSet {p : T[X]} {S : Type*} [CommRing S] [IsDomain S] [Algebra T S]
    [NoZeroSMulDivisors T S] {a : S} : a ∈ p.rootSet S ↔ p ≠ 0 ∧ aeval a p = 0

Proof state:
T : Type w
inst✝⁴ : CommRing T
p : T[X]
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : NoZeroSMulDivisors T S
a : S
⊢ a ∈ p.rootSet S ↔ p ≠ 0 ∧ (aeval a) p = 0

Tactic:
rw [mem_rootSet', Polynomial.map_ne_zero_iff (FaithfulSMul.algebraMap_injective T S)]

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
theorem Finset.tprod_subtype (s : Finset β) (f : β → α) :
    ∏' x : { x // x ∈ s }, f x = ∏ x ∈ s, f x

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
s : Finset β
f : β → α
⊢ ∏' (x : { x // x ∈ s }), f ↑x = ∏ x ∈ s.attach, f ↑x

Tactic:
exact tprod_fintype _

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
s : Finset β
f : β → α
⊢ ∏' (x : { x // x ∈ s }), f ↑x = ∏ x ∈ s, f x

Tactic:
rw [← prod_attach]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
s : Finset β
f : β → α
⊢ ∏' (x : { x // x ∈ s }), f ↑x = ∏ x ∈ s.attach, f ↑x
-- Mathlib/Order/Filter/Basic.lean
theorem frequently_imp_distrib_left {f : Filter α} [NeBot f] {p : Prop} {q : α → Prop} :
    (∃ᶠ x in f, p → q x) ↔ p → ∃ᶠ x in f, q x

Proof state:
α : Type u
f : Filter α
inst✝ : f.NeBot
p : Prop
q : α → Prop
⊢ (∃ᶠ (x : α) in f, p → q x) ↔ p → ∃ᶠ (x : α) in f, q x

Tactic:
simp [frequently_imp_distrib]

Result:
no goals
-- Mathlib/RingTheory/FractionalIdeal/Basic.lean
theorem _root_.IsFractional.nsmul {I : Submodule R P} :
    ∀ n : ℕ, IsFractional S I → IsFractional S (n • I : Submodule R P)
  | 0, _ => by
    rw [zero_smul]
    convert ((0 : Ideal R) : FractionalIdeal S P).isFractional
    simp
  | n + 1, h => by
    rw [succ_nsmul]
    exact (IsFractional.nsmul n h).sup h

Proof state:
case h.e'_7
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : Submodule R P
x✝ : IsFractional S I
⊢ 0 = ↑↑0

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : Submodule R P
n : ℕ
h : IsFractional S I
⊢ IsFractional S (n • I + I)

Tactic:
exact (IsFractional.nsmul n h).sup h

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : Submodule R P
x✝ : IsFractional S I
⊢ IsFractional S (0 • I)

Tactic:
rw [zero_smul]

Result:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : Submodule R P
x✝ : IsFractional S I
⊢ IsFractional S 0

Proof state:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : Submodule R P
n : ℕ
h : IsFractional S I
⊢ IsFractional S ((n + 1) • I)

Tactic:
rw [succ_nsmul]

Result:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : Submodule R P
n : ℕ
h : IsFractional S I
⊢ IsFractional S (n • I + I)

Proof state:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : Submodule R P
x✝ : IsFractional S I
⊢ IsFractional S 0

Tactic:
convert ((0 : Ideal R) : FractionalIdeal S P).isFractional

Result:
case h.e'_7
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : Submodule R P
x✝ : IsFractional S I
⊢ 0 = ↑↑0
-- Mathlib/Algebra/Homology/Homotopy.lean
theorem prevD_nat (C D : CochainComplex V ℕ) (i : ℕ) (f : ∀ i j, C.X i ⟶ D.X j) :
    prevD i f = f i (i - 1) ≫ D.d (i - 1) i

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

Tactic:
dsimp [prevD]

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

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

Tactic:
cases i

Result:
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
C D : CochainComplex V ℕ
f : (i j : ℕ) → C.X i ⟶ D.X j
⊢ f 0 ((ComplexShape.up ℕ).prev 0) ≫ D.d ((ComplexShape.up ℕ).prev 0) 0 = f 0 (0 - 1) ≫ D.d (0 - 1) 0

case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
C D : CochainComplex V ℕ
f : (i j : ℕ) → C.X i ⟶ D.X j
n✝ : ℕ
⊢ f (n✝ + 1) ((ComplexShape.up ℕ).prev (n✝ + 1)) ≫ D.d ((ComplexShape.up ℕ).prev (n✝ + 1)) (n✝ + 1) =
    f (n✝ + 1) (n✝ + 1 - 1) ≫ D.d (n✝ + 1 - 1) (n✝ + 1)

Proof state:
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
C D : CochainComplex V ℕ
f : (i j : ℕ) → C.X i ⟶ D.X j
⊢ f 0 ((ComplexShape.up ℕ).prev 0) ≫ D.d ((ComplexShape.up ℕ).prev 0) 0 = f 0 (0 - 1) ≫ D.d (0 - 1) 0

Tactic:
simp only [shape, CochainComplex.prev_nat_zero, ComplexShape.up_Rel, Nat.one_ne_zero,
  not_false_iff, comp_zero, reduceCtorEq]

Result:
no goals

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

Tactic:
congr <;> simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/Limits.lean
lemma exists_sigmaι_eq (x : (∐ f :)) : ∃ i y, (Sigma.ι f i).base y = x

Proof state:
case intro.intro
ι : Type u
f : ι → Scheme
x : ↑↑(∐ f).toPresheafedSpace
i : (disjointGlueData f).J
y : ↑↑((disjointGlueData f).U i).toPresheafedSpace
e : (ConcreteCategory.hom ((disjointGlueData f).ι i).base) y = (ConcreteCategory.hom (sigmaIsoGlued f).hom.base) x
⊢ ∃ i y, (ConcreteCategory.hom (Sigma.ι f i).base) y = x

Tactic:
refine ⟨i, y, (sigmaIsoGlued f).hom.isOpenEmbedding.injective ?_⟩

Result:
case intro.intro
ι : Type u
f : ι → Scheme
x : ↑↑(∐ f).toPresheafedSpace
i : (disjointGlueData f).J
y : ↑↑((disjointGlueData f).U i).toPresheafedSpace
e : (ConcreteCategory.hom ((disjointGlueData f).ι i).base) y = (ConcreteCategory.hom (sigmaIsoGlued f).hom.base) x
⊢ (ConcreteCategory.hom (sigmaIsoGlued f).hom.base) ((ConcreteCategory.hom (Sigma.ι f i).base) y) =
    (ConcreteCategory.hom (sigmaIsoGlued f).hom.base) x

Proof state:
case intro.intro
ι : Type u
f : ι → Scheme
x : ↑↑(∐ f).toPresheafedSpace
i : (disjointGlueData f).J
y : ↑↑((disjointGlueData f).U i).toPresheafedSpace
e : (ConcreteCategory.hom ((disjointGlueData f).ι i).base) y = (ConcreteCategory.hom (sigmaIsoGlued f).hom.base) x
⊢ (ConcreteCategory.hom (sigmaIsoGlued f).hom.base) ((ConcreteCategory.hom (Sigma.ι f i).base) y) =
    (ConcreteCategory.hom (sigmaIsoGlued f).hom.base) x

Tactic:
rwa [← Scheme.comp_base_apply, ι_sigmaIsoGlued_hom]

Result:
no goals

Proof state:
ι : Type u
f : ι → Scheme
x : ↑↑(∐ f).toPresheafedSpace
⊢ ∃ i y, (ConcreteCategory.hom (Sigma.ι f i).base) y = x

Tactic:
obtain ⟨i, y, e⟩ := (disjointGlueData f).ι_jointly_surjective ((sigmaIsoGlued f).hom.base x)

Result:
case intro.intro
ι : Type u
f : ι → Scheme
x : ↑↑(∐ f).toPresheafedSpace
i : (disjointGlueData f).J
y : ↑↑((disjointGlueData f).U i).toPresheafedSpace
e : (ConcreteCategory.hom ((disjointGlueData f).ι i).base) y = (ConcreteCategory.hom (sigmaIsoGlued f).hom.base) x
⊢ ∃ i y, (ConcreteCategory.hom (Sigma.ι f i).base) y = x
-- Mathlib/MeasureTheory/Integral/IntegrableOn.lean
theorem IntegrableAtFilter.inf_ae_iff {l : Filter α} :
    IntegrableAtFilter f (l ⊓ ae μ) μ ↔ IntegrableAtFilter f l μ

Proof state:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
μ : Measure α
l : Filter α
⊢ IntegrableAtFilter f (l ⊓ ae μ) μ → IntegrableAtFilter f l μ

Tactic:
rintro ⟨s, ⟨t, ht, u, hu, rfl⟩, hf⟩

Result:
case intro.intro.intro.intro.intro.intro
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
μ : Measure α
l : Filter α
t : Set α
ht : t ∈ l
u : Set α
hu : u ∈ ae μ
hf : IntegrableOn f (t ∩ u) μ
⊢ IntegrableAtFilter f l μ

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
μ : Measure α
l : Filter α
t : Set α
ht : t ∈ l
u : Set α
hu : u ∈ ae μ
hf : IntegrableOn f (t ∩ u) μ
⊢ IntegrableAtFilter f l μ

Tactic:
refine ⟨t, ht, hf.congr_set_ae <| eventuallyEq_set.2 ?_⟩

Result:
case intro.intro.intro.intro.intro.intro
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
μ : Measure α
l : Filter α
t : Set α
ht : t ∈ l
u : Set α
hu : u ∈ ae μ
hf : IntegrableOn f (t ∩ u) μ
⊢ ∀ᵐ (x : α) ∂μ, x ∈ t ↔ x ∈ t ∩ u

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
μ : Measure α
l : Filter α
t : Set α
ht : t ∈ l
u : Set α
hu : u ∈ ae μ
hf : IntegrableOn f (t ∩ u) μ
⊢ ∀ᵐ (x : α) ∂μ, x ∈ t ↔ x ∈ t ∩ u

Tactic:
filter_upwards [hu] with x hx using (and_iff_left hx).symm

Result:
no goals

Proof state:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
μ : Measure α
l : Filter α
⊢ IntegrableAtFilter f (l ⊓ ae μ) μ ↔ IntegrableAtFilter f l μ

Tactic:
refine ⟨?_, fun h ↦ h.filter_mono inf_le_left⟩

Result:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
μ : Measure α
l : Filter α
⊢ IntegrableAtFilter f (l ⊓ ae μ) μ → IntegrableAtFilter f l μ
-- Mathlib/SetTheory/Ordinal/Exponential.lean
theorem div_opow_log_pos (b : Ordinal) {o : Ordinal} (ho : o ≠ 0) : 0 < o / (b ^ log b o)

Proof state:
case inr
b o : Ordinal.{u_1}
ho : o ≠ 0
hb : 0 < b
⊢ 0 < o / b ^ log b o

Tactic:
rw [div_pos (opow_ne_zero _ hb.ne')]

Result:
case inr
b o : Ordinal.{u_1}
ho : o ≠ 0
hb : 0 < b
⊢ b ^ log b o ≤ o

Proof state:
b o : Ordinal.{u_1}
ho : o ≠ 0
⊢ 0 < o / b ^ log b o

Tactic:
rcases eq_zero_or_pos b with (rfl | hb)

Result:
case inl
o : Ordinal.{u_1}
ho : o ≠ 0
⊢ 0 < o / 0 ^ log 0 o

case inr
b o : Ordinal.{u_1}
ho : o ≠ 0
hb : 0 < b
⊢ 0 < o / b ^ log b o

Proof state:
case inl
o : Ordinal.{u_1}
ho : o ≠ 0
⊢ 0 < o / 0 ^ log 0 o

Tactic:
simpa using Ordinal.pos_iff_ne_zero.2 ho

Result:
no goals

Proof state:
case inr
b o : Ordinal.{u_1}
ho : o ≠ 0
hb : 0 < b
⊢ b ^ log b o ≤ o

Tactic:
exact opow_log_le_self b ho

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/Pow.lean
theorem le_max_of_sq_le_mul {a b c : M} (h : a ^ 2 ≤ b * c) : a ≤ max b c

Proof state:
M : Type u_3
inst✝³ : Monoid M
inst✝² : LinearOrder M
inst✝¹ : MulLeftStrictMono M
inst✝ : MulRightStrictMono M
a b c : M
h : a ^ 2 ≤ b * c
⊢ a ≤ b ⊔ c

Tactic:
simpa using min_le_max_of_mul_le_mul ((pow_two _).symm.trans_le h)

Result:
no goals
-- Mathlib/RingTheory/Unramified/LocalRing.lean
/-- Let `A` be an essentially of finite type `R`-algebra, `q` be a prime over `p`.
Then `A` is unramified at `p` if and only if `κ(q)/κ(p)` is separable, and `pS_q = qS_q`. -/
lemma isUnramifiedAt_iff_map_eq [EssFiniteType R S]
    (p : Ideal R) [p.IsPrime] (q : Ideal S) [q.IsPrime] [q.LiesOver p] :
    Algebra.IsUnramifiedAt R q ↔
      Algebra.IsSeparable p.ResidueField q.ResidueField ∧
      p.map (algebraMap R (Localization.AtPrime q)) = maximalIdeal _

Proof state:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : EssFiniteType R S
p : Ideal R
inst✝² : p.IsPrime
q : Ideal S
inst✝¹ : q.IsPrime
inst✝ : q.LiesOver p
⊢ IsUnramifiedAt R q ↔
    Algebra.IsSeparable p.ResidueField q.ResidueField ∧
      Ideal.map (algebraMap R (Localization.AtPrime q)) p = maximalIdeal (Localization.AtPrime q)

Tactic:
letI : Algebra (Localization.AtPrime p) (Localization.AtPrime q) :=
  (Localization.localRingHom p q (algebraMap R S) Ideal.LiesOver.over).toAlgebra

Result:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : EssFiniteType R S
p : Ideal R
inst✝² : p.IsPrime
q : Ideal S
inst✝¹ : q.IsPrime
inst✝ : q.LiesOver p
this : Algebra (Localization.AtPrime p) (Localization.AtPrime q) :=
  (Localization.localRingHom p q (algebraMap R S) ⋯).toAlgebra
⊢ IsUnramifiedAt R q ↔
    Algebra.IsSeparable p.ResidueField q.ResidueField ∧
      Ideal.map (algebraMap R (Localization.AtPrime q)) p = maximalIdeal (Localization.AtPrime q)
-- Mathlib/Analysis/BoxIntegral/Partition/Split.lean
theorem splitLower_le : I.splitLower i x ≤ I :=
  withBotCoe_subset_iff.1 <| by simp

Proof state:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ ↑(I.splitLower i x) ⊆ ↑↑I

Tactic:
simp

Result:
no goals