harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Sites/Sieves.lean
lemma mem_ofArrows_iff {W : C} (g : W ⟶ X) :
    ofArrows Y f g ↔ ∃ (i : I) (a : W ⟶ Y i), g = a ≫ f i

Proof state:
case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
X : C
Y : I → C
f : (i : I) → Y i ⟶ X
W : C
g : W ⟶ X
⊢ (ofArrows Y f).arrows g → ∃ i a, g = a ≫ f i

Tactic:
rintro ⟨T, a, b, ⟨i⟩, rfl⟩

Result:
case mp.intro.intro.intro.intro.mk
C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
X : C
Y✝ : I → C
f : (i : I) → Y✝ i ⟶ X
W Y : C
i : I
a : W ⟶ Y✝ i
⊢ ∃ i_1 a_1, a ≫ f i = a_1 ≫ f i_1

Proof state:
case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
X : C
Y : I → C
f : (i : I) → Y i ⟶ X
W : C
g : W ⟶ X
⊢ (∃ i a, g = a ≫ f i) → (ofArrows Y f).arrows g

Tactic:
rintro ⟨i, a, rfl⟩

Result:
case mpr.intro.intro
C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
X : C
Y : I → C
f : (i : I) → Y i ⟶ X
W : C
i : I
a : W ⟶ Y i
⊢ (ofArrows Y f).arrows (a ≫ f i)

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
X : C
Y : I → C
f : (i : I) → Y i ⟶ X
W : C
g : W ⟶ X
⊢ (ofArrows Y f).arrows g ↔ ∃ i a, g = a ≫ f i

Tactic:
constructor

Result:
case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
X : C
Y : I → C
f : (i : I) → Y i ⟶ X
W : C
g : W ⟶ X
⊢ (ofArrows Y f).arrows g → ∃ i a, g = a ≫ f i

case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
X : C
Y : I → C
f : (i : I) → Y i ⟶ X
W : C
g : W ⟶ X
⊢ (∃ i a, g = a ≫ f i) → (ofArrows Y f).arrows g

Proof state:
case mp.intro.intro.intro.intro.mk
C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
X : C
Y✝ : I → C
f : (i : I) → Y✝ i ⟶ X
W Y : C
i : I
a : W ⟶ Y✝ i
⊢ ∃ i_1 a_1, a ≫ f i = a_1 ≫ f i_1

Tactic:
exact ⟨i, a, rfl⟩

Result:
no goals

Proof state:
case mpr.intro.intro
C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
X : C
Y : I → C
f : (i : I) → Y i ⟶ X
W : C
i : I
a : W ⟶ Y i
⊢ (ofArrows Y f).arrows (a ≫ f i)

Tactic:
apply downward_closed _ (ofArrows_mk Y f i)

Result:
no goals
-- Mathlib/Data/Set/Function.lean
theorem MapsTo.piecewise_ite {s s₁ s₂ : Set α} {t t₁ t₂ : Set β} {f₁ f₂ : α → β}
    [∀ i, Decidable (i ∈ s)] (h₁ : MapsTo f₁ (s₁ ∩ s) (t₁ ∩ t))
    (h₂ : MapsTo f₂ (s₂ ∩ sᶜ) (t₂ ∩ tᶜ)) :
    MapsTo (s.piecewise f₁ f₂) (s.ite s₁ s₂) (t.ite t₁ t₂)

Proof state:
α : Type u_1
β : Type u_2
s s₁ s₂ : Set α
t t₁ t₂ : Set β
f₁ f₂ : α → β
inst✝ : (i : α) → Decidable (i ∈ s)
h₁ : MapsTo f₁ (s₁ ∩ s) (t₁ ∩ t)
h₂ : MapsTo f₂ (s₂ ∩ sᶜ) (t₂ ∩ tᶜ)
⊢ MapsTo (s.piecewise f₁ f₂) (s.ite s₁ s₂) (t.ite t₁ t₂)

Tactic:
refine (h₁.congr ?_).union_union (h₂.congr ?_)

Result:
case refine_1
α : Type u_1
β : Type u_2
s s₁ s₂ : Set α
t t₁ t₂ : Set β
f₁ f₂ : α → β
inst✝ : (i : α) → Decidable (i ∈ s)
h₁ : MapsTo f₁ (s₁ ∩ s) (t₁ ∩ t)
h₂ : MapsTo f₂ (s₂ ∩ sᶜ) (t₂ ∩ tᶜ)
⊢ EqOn f₁ (s.piecewise f₁ f₂) (s₁ ∩ s)

case refine_2
α : Type u_1
β : Type u_2
s s₁ s₂ : Set α
t t₁ t₂ : Set β
f₁ f₂ : α → β
inst✝ : (i : α) → Decidable (i ∈ s)
h₁ : MapsTo f₁ (s₁ ∩ s) (t₁ ∩ t)
h₂ : MapsTo f₂ (s₂ ∩ sᶜ) (t₂ ∩ tᶜ)
⊢ EqOn f₂ (s.piecewise f₁ f₂) (s₂ ∩ sᶜ)

Proof state:
case refine_1
α : Type u_1
β : Type u_2
s s₁ s₂ : Set α
t t₁ t₂ : Set β
f₁ f₂ : α → β
inst✝ : (i : α) → Decidable (i ∈ s)
h₁ : MapsTo f₁ (s₁ ∩ s) (t₁ ∩ t)
h₂ : MapsTo f₂ (s₂ ∩ sᶜ) (t₂ ∩ tᶜ)
⊢ EqOn f₁ (s.piecewise f₁ f₂) (s₁ ∩ s)

case refine_2
α : Type u_1
β : Type u_2
s s₁ s₂ : Set α
t t₁ t₂ : Set β
f₁ f₂ : α → β
inst✝ : (i : α) → Decidable (i ∈ s)
h₁ : MapsTo f₁ (s₁ ∩ s) (t₁ ∩ t)
h₂ : MapsTo f₂ (s₂ ∩ sᶜ) (t₂ ∩ tᶜ)
⊢ EqOn f₂ (s.piecewise f₁ f₂) (s₂ ∩ sᶜ)

Tactic:
exacts [(piecewise_eqOn s f₁ f₂).symm.mono inter_subset_right,
  (piecewise_eqOn_compl s f₁ f₂).symm.mono inter_subset_right]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean
theorem mul_right_mem_nonZeroDivisors_eq_zero_iff (hr : r ∈ M₀⁰) : x * r = 0 ↔ x = 0 :=
  ⟨hr _, by simp +contextual⟩

Proof state:
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
r x : M₀
hr : r ∈ M₀⁰
⊢ x = 0 → x * r = 0

Tactic:
simp +contextual

Result:
no goals
-- Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
theorem exists_lt_of_lt_csSup' {s : Set α} {a : α} (h : a < sSup s) : ∃ b ∈ s, a < b

Proof state:
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set α
a : α
h : ∀ b ∈ s, b ≤ a
⊢ sSup s ≤ a

Tactic:
exact csSup_le' h

Result:
no goals

Proof state:
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set α
a : α
h : a < sSup s
⊢ ∃ b ∈ s, a < b

Tactic:
contrapose! h

Result:
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set α
a : α
h : ∀ b ∈ s, b ≤ a
⊢ sSup s ≤ a
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
lemma measure_preimage_eq_zero_iff_of_countable {s : Set β} {f : α → β} (hs : s.Countable) :
    μ (f ⁻¹' s) = 0 ↔ ∀ x ∈ s, μ (f ⁻¹' {x}) = 0

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
s : Set β
f : α → β
hs : s.Countable
⊢ μ (f ⁻¹' s) = 0 ↔ ∀ x ∈ s, μ (f ⁻¹' {x}) = 0

Tactic:
rw [← biUnion_preimage_singleton, measure_biUnion_null_iff hs]

Result:
no goals
-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem irreducible_iff_degree_lt (p : R[X]) (hp0 : p ≠ 0) (hpu : ¬ IsUnit p) :
    Irreducible p ↔ ∀ q, q.degree ≤ ↑(natDegree p / 2) → q ∣ p → IsUnit q

Proof state:
R : Type u
inst✝ : Field R
p : R[X]
hp0 : p ≠ 0
hpu : ¬IsUnit p
⊢ Irreducible p ↔ ∀ (q : R[X]), q.degree ≤ ↑(p.natDegree / 2) → q ∣ p → IsUnit q

Tactic:
rw [← irreducible_mul_leadingCoeff_inv,
    (monic_mul_leadingCoeff_inv hp0).irreducible_iff_degree_lt]

Result:
R : Type u
inst✝ : Field R
p : R[X]
hp0 : p ≠ 0
hpu : ¬IsUnit p
⊢ (∀ (q : R[X]), q.degree ≤ ↑((p * C p.leadingCoeff⁻¹).natDegree / 2) → q ∣ p * C p.leadingCoeff⁻¹ → IsUnit q) ↔
    ∀ (q : R[X]), q.degree ≤ ↑(p.natDegree / 2) → q ∣ p → IsUnit q

R : Type u
inst✝ : Field R
p : R[X]
hp0 : p ≠ 0
hpu : ¬IsUnit p
⊢ p * C p.leadingCoeff⁻¹ ≠ 1

Proof state:
R : Type u
inst✝ : Field R
p : R[X]
hp0 : p ≠ 0
hpu : ¬IsUnit p
⊢ (∀ (q : R[X]), q.degree ≤ ↑((p * C p.leadingCoeff⁻¹).natDegree / 2) → q ∣ p * C p.leadingCoeff⁻¹ → IsUnit q) ↔
    ∀ (q : R[X]), q.degree ≤ ↑(p.natDegree / 2) → q ∣ p → IsUnit q

Tactic:
simp [hp0, natDegree_mul_leadingCoeff_inv]

Result:
no goals

Proof state:
R : Type u
inst✝ : Field R
p : R[X]
hp0 : p ≠ 0
hpu : p * C p.leadingCoeff⁻¹ = 1
⊢ IsUnit p

Tactic:
exact isUnit_of_mul_eq_one _ _ hpu

Result:
no goals

Proof state:
R : Type u
inst✝ : Field R
p : R[X]
hp0 : p ≠ 0
hpu : ¬IsUnit p
⊢ p * C p.leadingCoeff⁻¹ ≠ 1

Tactic:
contrapose! hpu

Result:
R : Type u
inst✝ : Field R
p : R[X]
hp0 : p ≠ 0
hpu : p * C p.leadingCoeff⁻¹ = 1
⊢ IsUnit p
-- Mathlib/LinearAlgebra/Matrix/Adjugate.lean
theorem det_smul_adjugate_adjugate (A : Matrix n n α) :
    det A • adjugate (adjugate A) = det A ^ (Fintype.card n - 1) • A

Proof state:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
⊢ A * (A.adjugate * A.adjugate.adjugate) = A * A.det ^ (Fintype.card n - 1) • 1

Tactic:
rw [← adjugate_mul_distrib, adjugate_mul, adjugate_smul, adjugate_one]

Result:
no goals

Proof state:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
⊢ A.det • A.adjugate.adjugate = A.det ^ (Fintype.card n - 1) • A

Tactic:
have : A * (A.adjugate * A.adjugate.adjugate) =
    A * (A.det ^ (Fintype.card n - 1) • (1 : Matrix n n α)) := by
  rw [← adjugate_mul_distrib, adjugate_mul, adjugate_smul, adjugate_one]

Result:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
this : A * (A.adjugate * A.adjugate.adjugate) = A * A.det ^ (Fintype.card n - 1) • 1
⊢ A.det • A.adjugate.adjugate = A.det ^ (Fintype.card n - 1) • A

Proof state:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
this : A * (A.adjugate * A.adjugate.adjugate) = A * A.det ^ (Fintype.card n - 1) • 1
⊢ A.det • A.adjugate.adjugate = A.det ^ (Fintype.card n - 1) • A

Tactic:
rwa [← Matrix.mul_assoc, mul_adjugate, Matrix.mul_smul, Matrix.mul_one, Matrix.smul_mul,
  Matrix.one_mul] at this

Result:
no goals
-- Mathlib/Algebra/BigOperators/Finsupp.lean
lemma sum_cons [AddCommMonoid M] (n : ℕ) (σ : Fin n →₀ M) (i : M) :
    (sum (cons i σ) fun _ e ↦ e) = i + sum σ (fun _ e ↦ e)

Proof state:
M : Type u_8
inst✝ : AddCommMonoid M
n : ℕ
σ : Fin n →₀ M
i : M
⊢ ((cons i σ).sum fun x e => e) = i + σ.sum fun x e => e

Tactic:
rw [sum_fintype _ _ (fun _ => rfl), sum_fintype _ _ (fun _ => rfl)]

Result:
M : Type u_8
inst✝ : AddCommMonoid M
n : ℕ
σ : Fin n →₀ M
i : M
⊢ ∑ i_1 : Fin (n + 1), (cons i σ) i_1 = i + ∑ i : Fin n, σ i

Proof state:
M : Type u_8
inst✝ : AddCommMonoid M
n : ℕ
σ : Fin n →₀ M
i : M
⊢ ∑ i_1 : Fin (n + 1), (cons i σ) i_1 = i + ∑ i : Fin n, σ i

Tactic:
exact Fin.sum_cons i σ

Result:
no goals
-- Mathlib/GroupTheory/Goursat.lean
@[to_additive (attr := simp)]
lemma mem_goursatSnd {h : H} : h ∈ I.goursatSnd ↔ (1, h) ∈ I

Proof state:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
h : H
⊢ h ∈ I.goursatSnd ↔ (1, h) ∈ I

Tactic:
simp [goursatSnd]

Result:
no goals
-- Mathlib/Data/PFunctor/Multivariate/W.lean
theorem w_ind {α : TypeVec n} {C : P.W α → Prop}
    (ih : ∀ (a : P.A) (f' : P.drop.B a ⟹ α) (f : P.last.B a → P.W α),
        (∀ i, C (f i)) → C (P.wMk a f' f)) :
    ∀ x, C x

Proof state:
case mk.ih
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
C : P.W α → Prop
ih :
  ∀ (a : P.A) (f' : P.drop.B a ⟹ α) (f : P.last.B a → P.W α),
    (∀ (i : P.last.B a), C (f i)) → C ⟨WType.mk a fun i => (f i).fst, P.wPathCasesOn f' fun i => (f i).snd⟩
a✝ : P.wp.A
f✝ : P.wp.B a✝ ⟹ α
a : P.A
f : P.last.B a → P.last.W
f' : P.WPath (WType.mk a f) ⟹ α
ih' : ∀ (i : P.last.B a), C ⟨f i, P.wPathDestRight f' i⟩
⊢ C ⟨WType.mk a f, f'⟩

Tactic:
let ih'' := ih a (P.wPathDestLeft f') fun i => ⟨f i, P.wPathDestRight f' i⟩

Result:
case mk.ih
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
C : P.W α → Prop
ih :
  ∀ (a : P.A) (f' : P.drop.B a ⟹ α) (f : P.last.B a → P.W α),
    (∀ (i : P.last.B a), C (f i)) → C ⟨WType.mk a fun i => (f i).fst, P.wPathCasesOn f' fun i => (f i).snd⟩
a✝ : P.wp.A
f✝ : P.wp.B a✝ ⟹ α
a : P.A
f : P.last.B a → P.last.W
f' : P.WPath (WType.mk a f) ⟹ α
ih' : ∀ (i : P.last.B a), C ⟨f i, P.wPathDestRight f' i⟩
ih'' : (∀ (i : P.last.B a), C ⟨f i, P.wPathDestRight f' i⟩) →
  C
    ⟨WType.mk a fun i => ⟨f i, P.wPathDestRight f' i⟩.fst,
      P.wPathCasesOn (P.wPathDestLeft f') fun i => ⟨f i, P.wPathDestRight f' i⟩.snd⟩ :=
  ih a (P.wPathDestLeft f') fun i => ⟨f i, P.wPathDestRight f' i⟩
⊢ C ⟨WType.mk a f, f'⟩

Proof state:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
C : P.W α → Prop
ih : ∀ (a : P.A) (f' : P.drop.B a ⟹ α) (f : P.last.B a → P.W α), (∀ (i : P.last.B a), C (f i)) → C (P.wMk a f' f)
⊢ ∀ (x : P.W α), C x

Tactic:
intro x

Result:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
C : P.W α → Prop
ih : ∀ (a : P.A) (f' : P.drop.B a ⟹ α) (f : P.last.B a → P.W α), (∀ (i : P.last.B a), C (f i)) → C (P.wMk a f' f)
x : P.W α
⊢ C x

Proof state:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
C : P.W α → Prop
ih : ∀ (a : P.A) (f' : P.drop.B a ⟹ α) (f : P.last.B a → P.W α), (∀ (i : P.last.B a), C (f i)) → C (P.wMk a f' f)
x : P.W α
⊢ C x

Tactic:
obtain ⟨a, f⟩ := x

Result:
case mk
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
C : P.W α → Prop
ih : ∀ (a : P.A) (f' : P.drop.B a ⟹ α) (f : P.last.B a → P.W α), (∀ (i : P.last.B a), C (f i)) → C (P.wMk a f' f)
a : P.wp.A
f : P.wp.B a ⟹ α
⊢ C ⟨a, f⟩
-- Mathlib/Data/List/Permutation.lean
theorem nodup_permutations'Aux_of_not_mem (s : List α) (x : α) (hx : x ∉ s) :
    Nodup (permutations'Aux x s)

Proof state:
case cons
α : Type u_1
x y : α
s : List α
IH : x ∉ s → (permutations'Aux x s).Nodup
hx : ¬x = y ∧ x ∉ s
⊢ Injective (cons y)

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u_1
x y : α
s : List α
IH : x ∉ s → (permutations'Aux x s).Nodup
hx : ¬x = y ∧ x ∉ s
⊢ (permutations'Aux x s).Nodup

Tactic:
exact IH hx.right

Result:
no goals

Proof state:
case cons
α : Type u_1
x y : α
s : List α
IH : x ∉ s → (permutations'Aux x s).Nodup
hx : ¬x = y ∧ x ∉ s
⊢ (y :: s ∈ permutations'Aux x s → ¬y = x) ∧ (map (cons y) (permutations'Aux x s)).Nodup

Tactic:
refine ⟨fun _ => Ne.symm hx.left, ?_⟩

Result:
case cons
α : Type u_1
x y : α
s : List α
IH : x ∉ s → (permutations'Aux x s).Nodup
hx : ¬x = y ∧ x ∉ s
⊢ (map (cons y) (permutations'Aux x s)).Nodup

Proof state:
case cons
α : Type u_1
x y : α
s : List α
IH : x ∉ s → (permutations'Aux x s).Nodup
hx : ¬x = y ∧ x ∉ s
⊢ (permutations'Aux x (y :: s)).Nodup

Tactic:
simp only [permutations'Aux, nodup_cons, mem_map, cons.injEq, exists_eq_right_right, not_and]

Result:
case cons
α : Type u_1
x y : α
s : List α
IH : x ∉ s → (permutations'Aux x s).Nodup
hx : ¬x = y ∧ x ∉ s
⊢ (y :: s ∈ permutations'Aux x s → ¬y = x) ∧ (map (cons y) (permutations'Aux x s)).Nodup

Proof state:
case nil
α : Type u_1
x : α
hx : x ∉ []
⊢ (permutations'Aux x []).Nodup

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u_1
x y : α
s : List α
IH : x ∉ s → (permutations'Aux x s).Nodup
hx : ¬x = y ∧ x ∉ s
⊢ (map (cons y) (permutations'Aux x s)).Nodup

Tactic:
rw [nodup_map_iff]

Result:
case cons
α : Type u_1
x y : α
s : List α
IH : x ∉ s → (permutations'Aux x s).Nodup
hx : ¬x = y ∧ x ∉ s
⊢ (permutations'Aux x s).Nodup

case cons
α : Type u_1
x y : α
s : List α
IH : x ∉ s → (permutations'Aux x s).Nodup
hx : ¬x = y ∧ x ∉ s
⊢ Injective (cons y)

Proof state:
case cons
α : Type u_1
x y : α
s : List α
IH : x ∉ s → (permutations'Aux x s).Nodup
hx : x ∉ y :: s
⊢ (permutations'Aux x (y :: s)).Nodup

Tactic:
simp only [not_or, mem_cons] at hx

Result:
case cons
α : Type u_1
x y : α
s : List α
IH : x ∉ s → (permutations'Aux x s).Nodup
hx : ¬x = y ∧ x ∉ s
⊢ (permutations'Aux x (y :: s)).Nodup

Proof state:
α : Type u_1
s : List α
x : α
hx : x ∉ s
⊢ (permutations'Aux x s).Nodup

Tactic:
induction' s with y s IH

Result:
case nil
α : Type u_1
x : α
hx : x ∉ []
⊢ (permutations'Aux x []).Nodup

case cons
α : Type u_1
x y : α
s : List α
IH : x ∉ s → (permutations'Aux x s).Nodup
hx : x ∉ y :: s
⊢ (permutations'Aux x (y :: s)).Nodup
-- Mathlib/.lake/packages/batteries/Batteries/Data/Stream.lean
theorem List.stream_take_eq_take_drop (l : List α) :
    Stream.take l n = (l.take n, l.drop n)

Proof state:
α : Type u_1
n : Nat
ih : ∀ (l : List α), Stream.take l n = (take n l, drop n l)
l : List α
⊢ Stream.take [] (n + 1) = (take (n + 1) [], drop (n + 1) [])

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
n : Nat
l : List α
⊢ Stream.take l n = (take n l, drop n l)

Tactic:
induction n generalizing l with
| zero => rfl
| succ n ih =>
  match l with
  | [] => rfl
  | _::_ => simp [Stream.take, ih]

Result:
no goals

Proof state:
case succ
α : Type u_1
n : Nat
ih : ∀ (l : List α), Stream.take l n = (take n l, drop n l)
l : List α
⊢ Stream.take l (n + 1) = (take (n + 1) l, drop (n + 1) l)

Tactic:
match l with
| [] => rfl
| _::_ => simp [Stream.take, ih]

Result:
no goals

Proof state:
case zero
α : Type u_1
l : List α
⊢ Stream.take l 0 = (take 0 l, drop 0 l)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
n : Nat
ih : ∀ (l : List α), Stream.take l n = (take n l, drop n l)
l : List α
head✝ : α
tail✝ : List α
⊢ Stream.take (head✝ :: tail✝) (n + 1) = (take (n + 1) (head✝ :: tail✝), drop (n + 1) (head✝ :: tail✝))

Tactic:
simp [Stream.take, ih]

Result:
no goals
-- Mathlib/Order/Bounds/Basic.lean
theorem isLeast_union_iff {a : α} {s t : Set α} :
    IsLeast (s ∪ t) a ↔ IsLeast s a ∧ a ∈ lowerBounds t ∨ a ∈ lowerBounds s ∧ IsLeast t a

Proof state:
α : Type u
inst✝ : Preorder α
a : α
s t : Set α
⊢ IsLeast (s ∪ t) a ↔ IsLeast s a ∧ a ∈ lowerBounds t ∨ a ∈ lowerBounds s ∧ IsLeast t a

Tactic:
simp [IsLeast, lowerBounds_union, or_and_right, and_comm (a := a ∈ t), and_assoc]

Result:
no goals
-- Mathlib/NumberTheory/Multiplicity.lean
theorem Int.two_pow_two_pow_add_two_pow_two_pow {x y : ℤ} (hx : ¬2 ∣ x) (hxy : 4 ∣ x - y) (i : ℕ) :
    emultiplicity 2 (x ^ 2 ^ i + y ^ 2 ^ i) = ↑(1 : ℕ)

Proof state:
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
hxy' : 2 ^ (1 + 1) ∣ x ^ 2 ^ 0 + y ^ 2 ^ 0
this : 4 ∣ x - y + (x ^ 2 ^ 0 + y ^ 2 ^ 0)
⊢ 2 * 2 ∣ 2 * x

Tactic:
norm_num at *

Result:
x y : ℤ
hxy : 4 ∣ x - y
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
hx : x % 2 = 1
hxy' : 4 ∣ x + y
this : 4 ∣ x + x
⊢ 4 ∣ 2 * x
-- Mathlib/Computability/Tape.lean
theorem Tape.write_self {Γ} [Inhabited Γ] : ∀ T : Tape Γ, T.write T.1 = T

Proof state:
case mk
Γ : Type u_1
inst✝ : Inhabited Γ
head✝ : Γ
left✝ right✝ : ListBlank Γ
⊢ write { head := head✝, left := left✝, right := right✝ }.head { head := head✝, left := left✝, right := right✝ } =
    { head := head✝, left := left✝, right := right✝ }

Tactic:
rfl

Result:
no goals

Proof state:
Γ : Type u_1
inst✝ : Inhabited Γ
⊢ ∀ (T : Tape Γ), write T.head T = T

Tactic:
rintro ⟨⟩

Result:
case mk
Γ : Type u_1
inst✝ : Inhabited Γ
head✝ : Γ
left✝ right✝ : ListBlank Γ
⊢ write { head := head✝, left := left✝, right := right✝ }.head { head := head✝, left := left✝, right := right✝ } =
    { head := head✝, left := left✝, right := right✝ }
-- Mathlib/CategoryTheory/MorphismProperty/Composition.lean
lemma multiplicativeClosure_eq_multiplicativeClosure' :
    W.multiplicativeClosure = W.multiplicativeClosure' :=
  le_antisymm
    ((multiplicativeClosure_le_iff _ _).mpr (fun _ _ f hf ↦ .of f hf)) <|
    fun x y f hf ↦ by induction hf with
      | of _ h => exact .of _ h
      | id x => exact .id x
      | of_comp f g hf hg hr => exact W.multiplicativeClosure.comp_mem f g (.of f hf) hr

Proof state:
case of_comp
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
x y : C
f✝ : x ⟶ y
x✝ y✝ z✝ : C
f : x✝ ⟶ y✝
g : y✝ ⟶ z✝
hf : W f
hg : W.multiplicativeClosure' g
hr : W.multiplicativeClosure g
⊢ W.multiplicativeClosure (f ≫ g)

Tactic:
exact W.multiplicativeClosure.comp_mem f g (.of f hf) hr

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
x y : C
f : x ⟶ y
hf : W.multiplicativeClosure' f
⊢ W.multiplicativeClosure f

Tactic:
induction hf with
| of _ h => exact .of _ h
| id x => exact .id x
| of_comp f g hf hg hr => exact W.multiplicativeClosure.comp_mem f g (.of f hf) hr

Result:
no goals

Proof state:
case id
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
x✝ y : C
f : x✝ ⟶ y
x : C
⊢ W.multiplicativeClosure (𝟙 x)

Tactic:
exact .id x

Result:
no goals

Proof state:
case of
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
x y : C
f : x ⟶ y
x✝ y✝ : C
f✝ : x✝ ⟶ y✝
h : W f✝
⊢ W.multiplicativeClosure f✝

Tactic:
exact .of _ h

Result:
no goals
-- Mathlib/RingTheory/FractionalIdeal/Operations.lean
theorem mul_one_div_le_one {I : FractionalIdeal R₁⁰ K} : I * (1 / I) ≤ 1

Proof state:
case neg
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
hI : ¬I = 0
⊢ I * (1 / I) ≤ 1

Tactic:
rw [← coe_le_coe, coe_mul, coe_div hI, coe_one]

Result:
case neg
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
hI : ¬I = 0
⊢ ↑I * (1 / ↑I) ≤ 1

Proof state:
case pos
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
hI : I = 0
⊢ I * (1 / I) ≤ 1

Tactic:
rw [hI, div_zero, mul_zero]

Result:
case pos
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
hI : I = 0
⊢ 0 ≤ 1

Proof state:
case neg
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
hI : ¬I = 0
⊢ ↑I * (1 / ↑I) ≤ 1

Tactic:
apply Submodule.mul_one_div_le_one

Result:
no goals

Proof state:
case pos
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
hI : I = 0
⊢ 0 ≤ 1

Tactic:
exact zero_le 1

Result:
no goals

Proof state:
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
⊢ I * (1 / I) ≤ 1

Tactic:
by_cases hI : I = 0

Result:
case pos
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
hI : I = 0
⊢ I * (1 / I) ≤ 1

case neg
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
hI : ¬I = 0
⊢ I * (1 / I) ≤ 1
-- Mathlib/RingTheory/KrullDimension/Basic.lean
lemma Ring.krullDimLE_one_iff_of_noZeroDivisors [NoZeroDivisors R] :
    Ring.KrullDimLE 1 R ↔ ∀ I : Ideal R, I ≠ ⊥ → I.IsPrime → I.IsMaximal

Proof state:
case inr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
h✝ : Nontrivial R
this : ⊥.IsPrime
⊢ KrullDimLE 1 R ↔ ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal

Tactic:
exact Ring.krullDimLE_one_iff_of_isPrime_bot

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
⊢ KrullDimLE 1 R ↔ ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal

Tactic:
cases subsingleton_or_nontrivial R

Result:
case inl
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
h✝ : Subsingleton R
⊢ KrullDimLE 1 R ↔ ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal

case inr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
h✝ : Nontrivial R
⊢ KrullDimLE 1 R ↔ ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal

Proof state:
case inr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
h✝ : Nontrivial R
⊢ KrullDimLE 1 R ↔ ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal

Tactic:
have := Ideal.bot_prime (α := R)

Result:
case inr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
h✝ : Nontrivial R
this : ⊥.IsPrime
⊢ KrullDimLE 1 R ↔ ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal

Proof state:
case inl
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
h✝ : Subsingleton R
⊢ KrullDimLE 1 R ↔ ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal

Tactic:
exact iff_of_true inferInstance fun I h ↦ (h <| Subsingleton.elim ..).elim

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Zip.lean
theorem zipWith_foldl_eq_zip_foldl {f : α → β → γ} (i : δ):
    (zipWith f l₁ l₂).foldl g i = (zip l₁ l₂).foldl (fun r p => g r (f p.1 p.2)) i

Proof state:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
g : δ → γ → δ
f : α → β → γ
i : δ
l₁ : Array α
l₂ : Vector β l₁.size
⊢ foldl g i (zipWith f { toArray := l₁, size_toArray := ⋯ } l₂) =
    foldl (fun r p => g r (f p.fst p.snd)) i ({ toArray := l₁, size_toArray := ⋯ }.zip l₂)

Tactic:
rcases l₂ with ⟨l₂, h⟩

Result:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
g : δ → γ → δ
f : α → β → γ
i : δ
l₁ : Array α
l₂ : Array β
h : l₂.size = l₁.size
⊢ foldl g i (zipWith f { toArray := l₁, size_toArray := ⋯ } { toArray := l₂, size_toArray := h }) =
    foldl (fun r p => g r (f p.fst p.snd)) i
      ({ toArray := l₁, size_toArray := ⋯ }.zip { toArray := l₂, size_toArray := h })

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
n✝ : Nat
l₁ : Vector α n✝
l₂ : Vector β n✝
g : δ → γ → δ
f : α → β → γ
i : δ
⊢ foldl g i (zipWith f l₁ l₂) = foldl (fun r p => g r (f p.fst p.snd)) i (l₁.zip l₂)

Tactic:
rcases l₁ with ⟨l₁, rfl⟩

Result:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
g : δ → γ → δ
f : α → β → γ
i : δ
l₁ : Array α
l₂ : Vector β l₁.size
⊢ foldl g i (zipWith f { toArray := l₁, size_toArray := ⋯ } l₂) =
    foldl (fun r p => g r (f p.fst p.snd)) i ({ toArray := l₁, size_toArray := ⋯ }.zip l₂)

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
g : δ → γ → δ
f : α → β → γ
i : δ
l₁ : Array α
l₂ : Array β
h : l₂.size = l₁.size
⊢ foldl g i (zipWith f { toArray := l₁, size_toArray := ⋯ } { toArray := l₂, size_toArray := h }) =
    foldl (fun r p => g r (f p.fst p.snd)) i
      ({ toArray := l₁, size_toArray := ⋯ }.zip { toArray := l₂, size_toArray := h })

Tactic:
simpa using Array.zipWith_foldl_eq_zip_foldl _

Result:
no goals