harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/ContinuedFractions/Computation/Approximations.lean
theorem of_one_le_get?_partDen {b : K}
    (nth_partDen_eq : (of v).partDens.get? n = some b) : 1 ≤ b

Proof state:
case intro.intro.refl.intro.intro
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
gp_n : Pair K
nth_s_eq : (of v).s.get? n = some gp_n
nth_partDen_eq : (of v).partDens.get? n = some gp_n.b
ifp_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_n
ifp_n_b_eq_gp_n_b : ↑ifp_n.b = gp_n.b
⊢ 1 ≤ gp_n.b

Tactic:
rw [← ifp_n_b_eq_gp_n_b]

Result:
case intro.intro.refl.intro.intro
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
gp_n : Pair K
nth_s_eq : (of v).s.get? n = some gp_n
nth_partDen_eq : (of v).partDens.get? n = some gp_n.b
ifp_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_n
ifp_n_b_eq_gp_n_b : ↑ifp_n.b = gp_n.b
⊢ 1 ≤ ↑ifp_n.b

Proof state:
case intro.intro.refl.intro.intro
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
gp_n : Pair K
nth_s_eq : (of v).s.get? n = some gp_n
nth_partDen_eq : (of v).partDens.get? n = some gp_n.b
ifp_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_n
ifp_n_b_eq_gp_n_b : ↑ifp_n.b = gp_n.b
⊢ 1 ≤ ↑ifp_n.b

Tactic:
exact mod_cast IntFractPair.one_le_succ_nth_stream_b succ_nth_stream_eq

Result:
no goals

Proof state:
case intro.intro.refl
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
gp_n : Pair K
nth_s_eq : (of v).s.get? n = some gp_n
nth_partDen_eq : (of v).partDens.get? n = some gp_n.b
⊢ 1 ≤ gp_n.b

Tactic:
obtain ⟨ifp_n, succ_nth_stream_eq, ifp_n_b_eq_gp_n_b⟩ :
    ∃ ifp, IntFractPair.stream v (n + 1) = some ifp ∧ (ifp.b : K) = gp_n.b :=
  IntFractPair.exists_succ_get?_stream_of_gcf_of_get?_eq_some nth_s_eq

Result:
case intro.intro.refl.intro.intro
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
gp_n : Pair K
nth_s_eq : (of v).s.get? n = some gp_n
nth_partDen_eq : (of v).partDens.get? n = some gp_n.b
ifp_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_n
ifp_n_b_eq_gp_n_b : ↑ifp_n.b = gp_n.b
⊢ 1 ≤ gp_n.b

Proof state:
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
b : K
nth_partDen_eq : (of v).partDens.get? n = some b
⊢ 1 ≤ b

Tactic:
obtain ⟨gp_n, nth_s_eq, ⟨-⟩⟩ : ∃ gp_n, (of v).s.get? n = some gp_n ∧ gp_n.b = b :=
  exists_s_b_of_partDen nth_partDen_eq

Result:
case intro.intro.refl
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
gp_n : Pair K
nth_s_eq : (of v).s.get? n = some gp_n
nth_partDen_eq : (of v).partDens.get? n = some gp_n.b
⊢ 1 ≤ gp_n.b
-- Mathlib/Algebra/Category/ModuleCat/Presheaf/Generator.lean
lemma isSeparating : IsSeparating (freeYoneda R)

Proof state:
case h.op.hf.h
C : Type u
inst✝ : Category.{v, u} C
R : Cᵒᵖ ⥤ RingCat
M N : PresheafOfModules R
f₁ f₂ : M ⟶ N
h : ∀ G ∈ freeYoneda R, ∀ (h : G ⟶ M), h ≫ f₁ = h ≫ f₂
X : C
m : ↑(M.obj (Opposite.op X))
⊢ (ModuleCat.Hom.hom (f₁.app (Opposite.op X))) m = (ModuleCat.Hom.hom (f₂.app (Opposite.op X))) m

Tactic:
obtain ⟨g, rfl⟩ := freeYonedaEquiv.surjective m

Result:
case h.op.hf.h.intro
C : Type u
inst✝ : Category.{v, u} C
R : Cᵒᵖ ⥤ RingCat
M N : PresheafOfModules R
f₁ f₂ : M ⟶ N
h : ∀ G ∈ freeYoneda R, ∀ (h : G ⟶ M), h ≫ f₁ = h ≫ f₂
X : C
g : (free R).obj (yoneda.obj X) ⟶ M
⊢ (ModuleCat.Hom.hom (f₁.app (Opposite.op X))) (freeYonedaEquiv g) =
    (ModuleCat.Hom.hom (f₂.app (Opposite.op X))) (freeYonedaEquiv g)

Proof state:
case h.op.hf.h.intro
C : Type u
inst✝ : Category.{v, u} C
R : Cᵒᵖ ⥤ RingCat
M N : PresheafOfModules R
f₁ f₂ : M ⟶ N
h : ∀ G ∈ freeYoneda R, ∀ (h : G ⟶ M), h ≫ f₁ = h ≫ f₂
X : C
g : (free R).obj (yoneda.obj X) ⟶ M
⊢ (ModuleCat.Hom.hom (f₁.app (Opposite.op X))) (freeYonedaEquiv g) =
    (ModuleCat.Hom.hom (f₂.app (Opposite.op X))) (freeYonedaEquiv g)

Tactic:
exact congr_arg freeYonedaEquiv (h _ ⟨X, rfl⟩ g)

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
R : Cᵒᵖ ⥤ RingCat
M N : PresheafOfModules R
f₁ f₂ : M ⟶ N
h : ∀ G ∈ freeYoneda R, ∀ (h : G ⟶ M), h ≫ f₁ = h ≫ f₂
⊢ f₁ = f₂

Tactic:
ext ⟨X⟩ m

Result:
case h.op.hf.h
C : Type u
inst✝ : Category.{v, u} C
R : Cᵒᵖ ⥤ RingCat
M N : PresheafOfModules R
f₁ f₂ : M ⟶ N
h : ∀ G ∈ freeYoneda R, ∀ (h : G ⟶ M), h ≫ f₁ = h ≫ f₂
X : C
m : ↑(M.obj (Opposite.op X))
⊢ (ModuleCat.Hom.hom (f₁.app (Opposite.op X))) m = (ModuleCat.Hom.hom (f₂.app (Opposite.op X))) m

Proof state:
C : Type u
inst✝ : Category.{v, u} C
R : Cᵒᵖ ⥤ RingCat
⊢ IsSeparating (freeYoneda R)

Tactic:
intro M N f₁ f₂ h

Result:
C : Type u
inst✝ : Category.{v, u} C
R : Cᵒᵖ ⥤ RingCat
M N : PresheafOfModules R
f₁ f₂ : M ⟶ N
h : ∀ G ∈ freeYoneda R, ∀ (h : G ⟶ M), h ≫ f₁ = h ≫ f₂
⊢ f₁ = f₂
-- Mathlib/Analysis/Convex/Slope.lean
theorem StrictConcaveOn.slope_anti_adjacent (hf : StrictConcaveOn 𝕜 s f) {x y z : 𝕜} (hx : x ∈ s)
    (hz : z ∈ s) (hxy : x < y) (hyz : y < z) : (f z - f y) / (z - y) < (f y - f x) / (y - x)

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConcaveOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
this : (f z - f y) / (z - y) < (f y - f x) / (y - x)
⊢ (f z - f y) / (z - y) < (f y - f x) / (y - x)

Tactic:
exact this

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConcaveOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
this : -(((-f) z - (-f) y) / (z - y)) < -(((-f) y - (-f) x) / (y - x))
⊢ (f z - f y) / (z - y) < (f y - f x) / (y - x)

Tactic:
simp only [Pi.neg_apply, ← neg_div, neg_sub', neg_neg] at this

Result:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConcaveOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
this : (f z - f y) / (z - y) < (f y - f x) / (y - x)
⊢ (f z - f y) / (z - y) < (f y - f x) / (y - x)

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConcaveOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
⊢ (f z - f y) / (z - y) < (f y - f x) / (y - x)

Tactic:
have := neg_lt_neg (StrictConvexOn.slope_strict_mono_adjacent hf.neg hx hz hxy hyz)

Result:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConcaveOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
this : -(((-f) z - (-f) y) / (z - y)) < -(((-f) y - (-f) x) / (y - x))
⊢ (f z - f y) / (z - y) < (f y - f x) / (y - x)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Clause.lean
theorem isUnit_iff (c : DefaultClause n) (l : Literal (PosFin n)) :
    isUnit c = some l ↔ toList c = [l]

Proof state:
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
x✝ : CNF.Clause (PosFin n)
hne : ∀ (l : Literal (PosFin n)), c.clause = [l] → False
⊢ ¬c.clause = [l]

Tactic:
apply hne

Result:
no goals

Proof state:
case h_2
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
x✝¹ : CNF.Clause (PosFin n)
x✝ : ∀ (l : Literal (PosFin n)), c.clause = [l] → False
⊢ none = some l ↔ c.clause = [l]

Tactic:
next hne =>
simp
apply hne

Result:
no goals

Proof state:
case h_1
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
x✝ : CNF.Clause (PosFin n)
l✝ : Literal (PosFin n)
heq✝ : c.clause = [l✝]
⊢ some l✝ = some l ↔ c.clause = [l]

Tactic:
next l' heq => simp [heq]

Result:
no goals

Proof state:
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
⊢ (match c.clause with
      | [l] => some l
      | x => none) =
      some l ↔
    c.clause = [l]

Tactic:
split

Result:
case h_1
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
x✝ : CNF.Clause (PosFin n)
l✝ : Literal (PosFin n)
heq✝ : c.clause = [l✝]
⊢ some l✝ = some l ↔ c.clause = [l]

case h_2
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
x✝¹ : CNF.Clause (PosFin n)
x✝ : ∀ (l : Literal (PosFin n)), c.clause = [l] → False
⊢ none = some l ↔ c.clause = [l]

Proof state:
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
x✝ : CNF.Clause (PosFin n)
l' : Literal (PosFin n)
heq : c.clause = [l']
⊢ some l' = some l ↔ c.clause = [l]

Tactic:
simp [heq]

Result:
no goals

Proof state:
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
⊢ c.isUnit = some l ↔ c.toList = [l]

Tactic:
simp only [isUnit, toList]

Result:
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
⊢ (match c.clause with
      | [l] => some l
      | x => none) =
      some l ↔
    c.clause = [l]

Proof state:
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
x✝ : CNF.Clause (PosFin n)
hne : ∀ (l : Literal (PosFin n)), c.clause = [l] → False
⊢ none = some l ↔ c.clause = [l]

Tactic:
simp

Result:
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
x✝ : CNF.Clause (PosFin n)
hne : ∀ (l : Literal (PosFin n)), c.clause = [l] → False
⊢ ¬c.clause = [l]
-- Mathlib/Analysis/SpecialFunctions/Choose.lean
theorem isTheta_choose (k : ℕ) :
    (fun (n : ℕ) ↦ (n.choose k : ℝ)) =Θ[atTop] (fun (n : ℕ) ↦ (n^k : ℝ))

Proof state:
k : ℕ
⊢ (fun n => ↑(n.choose k)) =Θ[atTop] fun n => ↑n ^ k

Tactic:
apply (isEquivalent_choose k).trans_isTheta

Result:
k : ℕ
⊢ (fun n => ↑n ^ k / ↑k !) =Θ[atTop] fun n => ↑n ^ k

Proof state:
k : ℕ
⊢ (fun n => (↑k !)⁻¹ * ↑n ^ k) =Θ[atTop] fun n => ↑n ^ k

Tactic:
exact isTheta_rfl.const_mul_left <| inv_ne_zero (mod_cast k.factorial_ne_zero)

Result:
no goals

Proof state:
k : ℕ
⊢ (fun n => ↑n ^ k / ↑k !) =Θ[atTop] fun n => ↑n ^ k

Tactic:
simp_rw [div_eq_mul_inv, mul_comm _ (_⁻¹)]

Result:
k : ℕ
⊢ (fun n => (↑k !)⁻¹ * ↑n ^ k) =Θ[atTop] fun n => ↑n ^ k
-- Mathlib/Order/SupIndep.lean
theorem iSupIndep.injOn (ht : iSupIndep t) : InjOn t {i | t i ≠ ⊥}

Proof state:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
ht : iSupIndep t
i : ι
a✝ : i ∈ {i | t i ≠ ⊥}
j : ι
hj : t j ≠ ⊥
h : t i = t j
contra : j ≠ i
⊢ t j ≤ ⨆ k, ⨆ (_ : k ≠ i), t k

Tactic:
exact le_iSup₂ (f := fun x _ ↦ t x) j contra

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
ht : iSupIndep t
i : ι
a✝ : i ∈ {i | t i ≠ ⊥}
j : ι
hj : t j ≠ ⊥
h : t i = t j
contra : i ≠ j
⊢ t j = ⊥

Tactic:
suffices t j ≤ ⨆ (k) (_ : k ≠ i), t k by
  replace ht := (ht i).mono_right this
  rwa [h, disjoint_self] at ht

Result:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
ht : iSupIndep t
i : ι
a✝ : i ∈ {i | t i ≠ ⊥}
j : ι
hj : t j ≠ ⊥
h : t i = t j
contra : i ≠ j
⊢ t j ≤ ⨆ k, ⨆ (_ : k ≠ i), t k

Proof state:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
ht : iSupIndep t
i : ι
a✝ : i ∈ {i | t i ≠ ⊥}
j : ι
hj : t j ≠ ⊥
h : t i = t j
contra : i ≠ j
⊢ t j ≤ ⨆ k, ⨆ (_ : k ≠ i), t k

Tactic:
replace contra : j ≠ i := Ne.symm contra

Result:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
ht : iSupIndep t
i : ι
a✝ : i ∈ {i | t i ≠ ⊥}
j : ι
hj : t j ≠ ⊥
h : t i = t j
contra : j ≠ i
⊢ t j ≤ ⨆ k, ⨆ (_ : k ≠ i), t k

Proof state:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
ht : iSupIndep t
i : ι
a✝ : i ∈ {i | t i ≠ ⊥}
j : ι
hj : t j ≠ ⊥
h : t i = t j
⊢ i = j

Tactic:
by_contra! contra

Result:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
ht : iSupIndep t
i : ι
a✝ : i ∈ {i | t i ≠ ⊥}
j : ι
hj : t j ≠ ⊥
h : t i = t j
contra : i ≠ j
⊢ False

Proof state:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
ht : iSupIndep t
i : ι
a✝ : i ∈ {i | t i ≠ ⊥}
j : ι
hj : t j ≠ ⊥
h : t i = t j
contra : i ≠ j
⊢ False

Tactic:
apply hj

Result:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
ht : iSupIndep t
i : ι
a✝ : i ∈ {i | t i ≠ ⊥}
j : ι
hj : t j ≠ ⊥
h : t i = t j
contra : i ≠ j
⊢ t j = ⊥

Proof state:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
ht : iSupIndep t
⊢ InjOn t {i | t i ≠ ⊥}

Tactic:
rintro i _ j (hj : t j ≠ ⊥) h

Result:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
ht : iSupIndep t
i : ι
a✝ : i ∈ {i | t i ≠ ⊥}
j : ι
hj : t j ≠ ⊥
h : t i = t j
⊢ i = j

Proof state:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
ht : iSupIndep t
i : ι
a✝ : i ∈ {i | t i ≠ ⊥}
j : ι
hj : t j ≠ ⊥
h : t i = t j
contra : i ≠ j
this : t j ≤ ⨆ k, ⨆ (_ : k ≠ i), t k
⊢ t j = ⊥

Tactic:
replace ht := (ht i).mono_right this

Result:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
i : ι
a✝ : i ∈ {i | t i ≠ ⊥}
j : ι
hj : t j ≠ ⊥
h : t i = t j
contra : i ≠ j
this : t j ≤ ⨆ k, ⨆ (_ : k ≠ i), t k
ht : Disjoint (t i) (t j)
⊢ t j = ⊥

Proof state:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
i : ι
a✝ : i ∈ {i | t i ≠ ⊥}
j : ι
hj : t j ≠ ⊥
h : t i = t j
contra : i ≠ j
this : t j ≤ ⨆ k, ⨆ (_ : k ≠ i), t k
ht : Disjoint (t i) (t j)
⊢ t j = ⊥

Tactic:
rwa [h, disjoint_self] at ht

Result:
no goals
-- Mathlib/Algebra/Polynomial/RingDivision.lean
theorem smul_modByMonic (c : R) (p : R[X]) : c • p %ₘ q = c • (p %ₘ q)

Proof state:
case pos
R : Type u
inst✝ : CommRing R
q : R[X]
c : R
p : R[X]
hq : q.Monic
⊢ c • p %ₘ q = c • (p %ₘ q)

Tactic:
rcases subsingleton_or_nontrivial R with hR | hR

Result:
case pos.inl
R : Type u
inst✝ : CommRing R
q : R[X]
c : R
p : R[X]
hq : q.Monic
hR : Subsingleton R
⊢ c • p %ₘ q = c • (p %ₘ q)

case pos.inr
R : Type u
inst✝ : CommRing R
q : R[X]
c : R
p : R[X]
hq : q.Monic
hR : Nontrivial R
⊢ c • p %ₘ q = c • (p %ₘ q)

Proof state:
R : Type u
inst✝ : CommRing R
q : R[X]
c : R
p : R[X]
⊢ c • p %ₘ q = c • (p %ₘ q)

Tactic:
by_cases hq : q.Monic

Result:
case pos
R : Type u
inst✝ : CommRing R
q : R[X]
c : R
p : R[X]
hq : q.Monic
⊢ c • p %ₘ q = c • (p %ₘ q)

case neg
R : Type u
inst✝ : CommRing R
q : R[X]
c : R
p : R[X]
hq : ¬q.Monic
⊢ c • p %ₘ q = c • (p %ₘ q)

Proof state:
case neg
R : Type u
inst✝ : CommRing R
q : R[X]
c : R
p : R[X]
hq : ¬q.Monic
⊢ c • p %ₘ q = c • (p %ₘ q)

Tactic:
simp_rw [modByMonic_eq_of_not_monic _ hq]

Result:
no goals

Proof state:
case pos.inr
R : Type u
inst✝ : CommRing R
q : R[X]
c : R
p : R[X]
hq : q.Monic
hR : Nontrivial R
⊢ c • p %ₘ q = c • (p %ₘ q)

Tactic:
exact
(div_modByMonic_unique (c • (p /ₘ q)) (c • (p %ₘ q)) hq
    ⟨by rw [mul_smul_comm, ← smul_add, modByMonic_add_div p hq],
      (degree_smul_le _ _).trans_lt (degree_modByMonic_lt _ hq)⟩).2

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
q : R[X]
c : R
p : R[X]
hq : q.Monic
hR : Nontrivial R
⊢ c • (p %ₘ q) + q * c • (p /ₘ q) = c • p

Tactic:
rw [mul_smul_comm, ← smul_add, modByMonic_add_div p hq]

Result:
no goals

Proof state:
case pos.inl
R : Type u
inst✝ : CommRing R
q : R[X]
c : R
p : R[X]
hq : q.Monic
hR : Subsingleton R
⊢ c • p %ₘ q = c • (p %ₘ q)

Tactic:
simp only [eq_iff_true_of_subsingleton]

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
theorem div_top : a / ∞ = 0

Proof state:
a : ℝ≥0∞
⊢ a / ⊤ = 0

Tactic:
rw [div_eq_mul_inv, inv_top, mul_zero]

Result:
no goals
-- Mathlib/Data/Nat/Bits.lean
@[simp]
lemma bodd_mul (m n : ℕ) : bodd (m * n) = (bodd m && bodd n)

Proof state:
m n : ℕ
⊢ (m * n).bodd = (m.bodd && n.bodd)

Tactic:
induction n with
| zero => simp
| succ n IH =>
  simp only [mul_succ, bodd_add, IH, bodd_succ]
  cases bodd m <;> cases bodd n <;> rfl

Result:
no goals

Proof state:
case succ
m n : ℕ
IH : (m * n).bodd = (m.bodd && n.bodd)
⊢ (m.bodd && n.bodd ^^ m.bodd) = (m.bodd && !n.bodd)

Tactic:
cases bodd m <;> cases bodd n <;> rfl

Result:
no goals

Proof state:
case succ
m n : ℕ
IH : (m * n).bodd = (m.bodd && n.bodd)
⊢ (m * (n + 1)).bodd = (m.bodd && (n + 1).bodd)

Tactic:
simp only [mul_succ, bodd_add, IH, bodd_succ]

Result:
case succ
m n : ℕ
IH : (m * n).bodd = (m.bodd && n.bodd)
⊢ (m.bodd && n.bodd ^^ m.bodd) = (m.bodd && !n.bodd)

Proof state:
case zero
m : ℕ
⊢ (m * 0).bodd = (m.bodd && bodd 0)

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Closed/Monoidal.lean
theorem ofEquiv_curry_def {X Y Z : C} (f : X ⊗ Y ⟶ Z) :
    letI := ofEquiv F adj
    MonoidalClosed.curry f =
      adj.homEquiv Y ((ihom (F.obj X)).obj (F.obj Z))
        (MonoidalClosed.curry (adj.toEquivalence.symm.toAdjunction.homEquiv (F.obj X ⊗ F.obj Y) Z
        ((Iso.compInverseIso (H := adj.toEquivalence)
          (Functor.Monoidal.commTensorLeft F X)).hom.app Y ≫ f)))

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : F.IsEquivalence
inst✝ : MonoidalClosed D
X Y Z : C
f : X ⊗ Y ⟶ Z
⊢ ({
            homEquiv := fun X_1 Y =>
              (Adjunction.equivHomsetLeftOfNatIso (Functor.Monoidal.commTensorLeft F X).compInverseIso.symm).trans
                ((adj.comp ((ihom.adjunction (F.obj X)).comp adj.toEquivalence.symm.toAdjunction)).homEquiv X_1 Y),
            homEquiv_naturality_left_symm := ⋯, homEquiv_naturality_right := ⋯ }.homEquiv
        Y Z)
      f =
    (adj.homEquiv Y ((ihom (F.obj X)).obj (F.obj Z)))
      (curry
        ((adj.toEquivalence.symm.toAdjunction.homEquiv (F.obj X ⊗ F.obj Y) Z)
          ((Functor.Monoidal.commTensorLeft F X).compInverseIso.hom.app Y ≫ f)))

Tactic:
dsimp

Result:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : F.IsEquivalence
inst✝ : MonoidalClosed D
X Y Z : C
f : X ⊗ Y ⟶ Z
⊢ ((adj.comp ((ihom.adjunction (F.obj X)).comp adj.toEquivalence.symm.toAdjunction)).homEquiv Y Z)
      ((Adjunction.equivHomsetLeftOfNatIso (Functor.Monoidal.commTensorLeft F X).compInverseIso.symm) f) =
    (adj.homEquiv Y ((ihom (F.obj X)).obj (F.obj Z)))
      (curry
        ((adj.toEquivalence.symm.toAdjunction.homEquiv (F.obj X ⊗ F.obj Y) Z)
          ((Functor.Monoidal.commTensorLeft F X).compInverseIso.hom.app Y ≫ f)))
-- Mathlib/CategoryTheory/Preadditive/AdditiveFunctor.lean
lemma additive_of_iso {G : C ⥤ D} (e : F ≅ G) : G.Additive

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_5, u_2} D
inst✝² : Preadditive C
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : F.Additive
G : C ⥤ D
e : F ≅ G
⊢ G.Additive

Tactic:
constructor

Result:
case map_add
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_5, u_2} D
inst✝² : Preadditive C
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : F.Additive
G : C ⥤ D
e : F ≅ G
⊢ autoParam (∀ {X Y : C} {f g : X ⟶ Y}, G.map (f + g) = G.map f + G.map g) _auto✝

Proof state:
case map_add
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_5, u_2} D
inst✝² : Preadditive C
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : F.Additive
G : C ⥤ D
e : F ≅ G
X Y : C
f g : X ⟶ Y
⊢ G.map (f + g) = G.map f + G.map g

Tactic:
simp only [← NatIso.naturality_1 e (f + g), map_add, Preadditive.add_comp,
  NatTrans.naturality, Preadditive.comp_add, Iso.inv_hom_id_app_assoc]

Result:
no goals

Proof state:
case map_add
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_5, u_2} D
inst✝² : Preadditive C
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : F.Additive
G : C ⥤ D
e : F ≅ G
⊢ autoParam (∀ {X Y : C} {f g : X ⟶ Y}, G.map (f + g) = G.map f + G.map g) _auto✝

Tactic:
intro X Y f g

Result:
case map_add
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_5, u_2} D
inst✝² : Preadditive C
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : F.Additive
G : C ⥤ D
e : F ≅ G
X Y : C
f g : X ⟶ Y
⊢ G.map (f + g) = G.map f + G.map g
-- Mathlib/LinearAlgebra/Span/Basic.lean
theorem span_smul_eq_of_isUnit (s : Set M) (r : R) (hr : IsUnit r) : span R (r • s) = span R s

Proof state:
case a
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
hr : IsUnit r
⊢ span R (r • s) ≤ span R s

Tactic:
apply span_smul_le

Result:
no goals

Proof state:
case h.e'_3.h.e'_6
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
hr : IsUnit r
⊢ s = ↑hr.unit⁻¹ • r • s

Tactic:
simp [smul_smul]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
hr : IsUnit r
⊢ span R (r • s) = span R s

Tactic:
apply le_antisymm

Result:
case a
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
hr : IsUnit r
⊢ span R (r • s) ≤ span R s

case a
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
hr : IsUnit r
⊢ span R s ≤ span R (r • s)

Proof state:
case a
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
hr : IsUnit r
⊢ span R s ≤ span R (r • s)

Tactic:
convert span_smul_le (r • s) ((hr.unit⁻¹ :) : R)

Result:
case h.e'_3.h.e'_6
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
hr : IsUnit r
⊢ s = ↑hr.unit⁻¹ • r • s
-- Mathlib/Data/Finsupp/NeLocus.lean
theorem neLocus_self_add_left : neLocus (f + g) f = g.support

Proof state:
α : Type u_1
N : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : AddGroup N
f g : α →₀ N
⊢ (f + g).neLocus f = g.support

Tactic:
rw [neLocus_comm, neLocus_self_add_right]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/HomeomorphBall.lean
theorem univBall_source (c : P) (r : ℝ) : (univBall c r).source = univ

Proof state:
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
⊢ (univBall c r).source = univ

Tactic:
unfold univBall

Result:
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
⊢ (if h : 0 < r then univUnitBall.trans' (unitBallBall c r h) ⋯
      else (IsometryEquiv.vaddConst c).toHomeomorph.toPartialHomeomorph).source =
    univ

Proof state:
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
⊢ (if h : 0 < r then univUnitBall.trans' (unitBallBall c r h) ⋯
      else (IsometryEquiv.vaddConst c).toHomeomorph.toPartialHomeomorph).source =
    univ

Tactic:
split_ifs <;> rfl

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/Cospan.lean
theorem spanExt_inv_app_zero : (spanExt iX iY iZ wf wg).inv.app WalkingSpan.zero = iX.inv

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
f : X ⟶ Y
g : X ⟶ Z
f' : X' ⟶ Y'
g' : X' ⟶ Z'
wf : iX.hom ≫ f' = f ≫ iY.hom
wg : iX.hom ≫ g' = g ≫ iZ.hom
⊢ (spanExt iX iY iZ wf wg).inv.app WalkingSpan.zero = iX.inv

Tactic:
dsimp [spanExt]

Result:
no goals
-- Mathlib/Topology/StoneCech.lean
lemma eq_if_stoneCechUnit_eq {a b : α} {f : α → β} (hcf : Continuous f)
    (h : stoneCechUnit a = stoneCechUnit b) : f a = f b

Proof state:
α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : CompactSpace β
a b : α
f : α → β
hcf : Continuous f
h : stoneCechUnit a = stoneCechUnit b
⊢ f a = f b

Tactic:
rw [← congrFun (stoneCechExtend_extends hcf), ← congrFun (stoneCechExtend_extends hcf)]

Result:
α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : CompactSpace β
a b : α
f : α → β
hcf : Continuous f
h : stoneCechUnit a = stoneCechUnit b
⊢ (stoneCechExtend hcf ∘ stoneCechUnit) a = (stoneCechExtend hcf ∘ stoneCechUnit) b

Proof state:
α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : CompactSpace β
a b : α
f : α → β
hcf : Continuous f
h : stoneCechUnit a = stoneCechUnit b
⊢ (stoneCechExtend hcf ∘ stoneCechUnit) a = (stoneCechExtend hcf ∘ stoneCechUnit) b

Tactic:
exact congrArg (stoneCechExtend hcf) h

Result:
no goals