harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicGeometry/IdealSheaf.lean
lemma ker_morphismRestrict_ideal (f : X.Hom Y) [QuasiCompact f]
    (U : Y.Opens) (V : U.toScheme.affineOpens) :
    (f ∣_ U).ker.ideal V = f.ker.ideal ⟨U.ι ''ᵁ V, V.2.image_of_isOpenImmersion _⟩

Proof state:
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
U : Y.Opens
V : ↑(↑U).affineOpens
⊢ (Hom.ker (f ∣_ U)).ideal V = f.ker.ideal ⟨U.ι ''ᵁ ↑V, ⋯⟩

Tactic:
have inst : QuasiCompact (f ∣_ U) := MorphismProperty.of_isPullback
    (isPullback_morphismRestrict _ _).flip inferInstance

Result:
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
U : Y.Opens
V : ↑(↑U).affineOpens
inst : QuasiCompact (f ∣_ U)
⊢ (Hom.ker (f ∣_ U)).ideal V = f.ker.ideal ⟨U.ι ''ᵁ ↑V, ⋯⟩

Proof state:
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
U : Y.Opens
V : ↑(↑U).affineOpens
inst : QuasiCompact (f ∣_ U)
⊢ (Hom.ker (f ∣_ U)).ideal V = f.ker.ideal ⟨U.ι ''ᵁ ↑V, ⋯⟩

Tactic:
ext x

Result:
case h
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
U : Y.Opens
V : ↑(↑U).affineOpens
inst : QuasiCompact (f ∣_ U)
x : ↑Γ(↑U, ↑V)
⊢ x ∈ (Hom.ker (f ∣_ U)).ideal V ↔ x ∈ f.ker.ideal ⟨U.ι ''ᵁ ↑V, ⋯⟩

Proof state:
case h
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
U : Y.Opens
V : ↑(↑U).affineOpens
inst : QuasiCompact (f ∣_ U)
x : ↑Γ(↑U, ↑V)
⊢ x ∈ (Hom.ker (f ∣_ U)).ideal V ↔ x ∈ f.ker.ideal ⟨U.ι ''ᵁ ↑V, ⋯⟩

Tactic:
simpa [Scheme.Hom.appLE] using map_eq_zero_iff _
  (ConcreteCategory.bijective_of_isIso
    (X.presheaf.map (eqToHom (image_morphismRestrict_preimage f U V)).op)).1

Result:
no goals
-- Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean
theorem l_csSup' (gc : GaloisConnection l u) {s : Set α} (hne : s.Nonempty) (hbdd : BddAbove s) :
    l (sSup s) = sSup (l '' s)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : ConditionallyCompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set α
hne : s.Nonempty
hbdd : BddAbove s
⊢ l (sSup s) = sSup (l '' s)

Tactic:
rw [gc.l_csSup hne hbdd, sSup_image']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem ushiftRight'_or_of_and_eq_zero {x : BitVec w₁} {y z : BitVec w₂}
    (h : y &&& z = 0#w₂) :
    x >>> (y ||| z) = x >>> y >>> z

Proof state:
w₁ w₂ : Nat
x : BitVec w₁
y z : BitVec w₂
h : y &&& z = 0#w₂
⊢ x >>> (y ||| z) = x >>> y >>> z

Tactic:
simp [← add_eq_or_of_and_eq_zero _ _ h, toNat_add_of_and_eq_zero h, shiftRight_add]

Result:
no goals
-- Mathlib/Logic/Function/Iterate.lean
theorem comp_iterate_pred_of_pos {n : ℕ} (hn : 0 < n) : f ∘ f^[n.pred] = f^[n]

Proof state:
α : Type u
f : α → α
n : ℕ
hn : 0 < n
⊢ f ∘ f^[n.pred] = f^[n]

Tactic:
rw [← iterate_succ', Nat.succ_pred_eq_of_pos hn]

Result:
no goals
-- Mathlib/Algebra/Lie/Solvable.lean
theorem derivedSeriesOfIdeal_baseChange {A : Type*} [CommRing A] [Algebra R A] (k : ℕ) :
    derivedSeriesOfIdeal A (A ⊗[R] L) k (I.baseChange A) =
      (derivedSeriesOfIdeal R L k I).baseChange A

Proof state:
case succ
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
I : LieIdeal R L
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
k : ℕ
ih : derivedSeriesOfIdeal A (A ⊗[R] L) k (LieSubmodule.baseChange A I) = LieSubmodule.baseChange A (D k I)
⊢ derivedSeriesOfIdeal A (A ⊗[R] L) (k + 1) (LieSubmodule.baseChange A I) = LieSubmodule.baseChange A (D (k + 1) I)

Tactic:
simp only [derivedSeriesOfIdeal_succ, ih, ← LieSubmodule.baseChange_top,
LieSubmodule.lie_baseChange]

Result:
no goals

Proof state:
case zero
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
I : LieIdeal R L
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ derivedSeriesOfIdeal A (A ⊗[R] L) 0 (LieSubmodule.baseChange A I) = LieSubmodule.baseChange A (D 0 I)

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
I : LieIdeal R L
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
k : ℕ
⊢ derivedSeriesOfIdeal A (A ⊗[R] L) k (LieSubmodule.baseChange A I) = LieSubmodule.baseChange A (D k I)

Tactic:
induction k with
| zero => simp
| succ k ih => simp only [derivedSeriesOfIdeal_succ, ih, ← LieSubmodule.baseChange_top,
  LieSubmodule.lie_baseChange]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem findSome?_map (f : β → γ) (l : List β) : findSome? p (l.map f) = l.findSome? (p ∘ f)

Proof state:
case nil
β : Type u_1
γ : Type u_2
α✝ : Type u_3
p : γ → Option α✝
f : β → γ
⊢ findSome? p (map f []) = findSome? (p ∘ f) []

Tactic:
simp

Result:
no goals

Proof state:
case cons
β : Type u_1
γ : Type u_2
α✝ : Type u_3
p : γ → Option α✝
f : β → γ
x : β
xs : List β
ih : findSome? p (map f xs) = findSome? (p ∘ f) xs
⊢ findSome? p (map f (x :: xs)) = findSome? (p ∘ f) (x :: xs)

Tactic:
simp only [map_cons, findSome?]

Result:
case cons
β : Type u_1
γ : Type u_2
α✝ : Type u_3
p : γ → Option α✝
f : β → γ
x : β
xs : List β
ih : findSome? p (map f xs) = findSome? (p ∘ f) xs
⊢ (match p (f x) with
    | some b => some b
    | none => findSome? p (map f xs)) =
    match (p ∘ f) x with
    | some b => some b
    | none => findSome? (p ∘ f) xs

Proof state:
β : Type u_1
γ : Type u_2
α✝ : Type u_3
p : γ → Option α✝
f : β → γ
l : List β
⊢ findSome? p (map f l) = findSome? (p ∘ f) l

Tactic:
induction l with
| nil => simp
| cons x xs ih =>
  simp only [map_cons, findSome?]
  split <;> simp_all

Result:
no goals

Proof state:
case cons
β : Type u_1
γ : Type u_2
α✝ : Type u_3
p : γ → Option α✝
f : β → γ
x : β
xs : List β
ih : findSome? p (map f xs) = findSome? (p ∘ f) xs
⊢ (match p (f x) with
    | some b => some b
    | none => findSome? p (map f xs)) =
    match (p ∘ f) x with
    | some b => some b
    | none => findSome? (p ∘ f) xs

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/RingTheory/Multiplicity.lean
theorem pow_dvd_of_le_emultiplicity {k : ℕ} (hk : k ≤ emultiplicity a b) :
    a ^ k ∣ b

Proof state:
case succ.isTrue
α : Type u_1
inst✝ : Monoid α
a b : α
n✝ : ℕ
h✝ : FiniteMultiplicity a b
hk : n✝ + 1 ≤ Nat.find h✝
⊢ a ^ (n✝ + 1) ∣ b

Tactic:
simpa using (Nat.find_min _ (lt_of_succ_le hk))

Result:
no goals

Proof state:
case succ.isTrue
α : Type u_1
inst✝ : Monoid α
a b : α
n✝ : ℕ
h✝ : FiniteMultiplicity a b
hk : ↑(n✝ + 1) ≤ ↑(Nat.find h✝)
⊢ a ^ (n✝ + 1) ∣ b

Tactic:
norm_cast at hk

Result:
case succ.isTrue
α : Type u_1
inst✝ : Monoid α
a b : α
n✝ : ℕ
h✝ : FiniteMultiplicity a b
hk : n✝ + 1 ≤ Nat.find h✝
⊢ a ^ (n✝ + 1) ∣ b

Proof state:
case zero
α : Type u_1
inst✝ : Monoid α
a b : α
hk : ↑0 ≤ emultiplicity a b
⊢ a ^ 0 ∣ b

Tactic:
simp

Result:
no goals

Proof state:
case succ
α : Type u_1
inst✝ : Monoid α
a b : α
n✝ : ℕ
hk : ↑(n✝ + 1) ≤ if h : FiniteMultiplicity a b then ↑(Nat.find h) else ⊤
⊢ a ^ (n✝ + 1) ∣ b

Tactic:
split at hk

Result:
case succ.isTrue
α : Type u_1
inst✝ : Monoid α
a b : α
n✝ : ℕ
h✝ : FiniteMultiplicity a b
hk : ↑(n✝ + 1) ≤ ↑(Nat.find h✝)
⊢ a ^ (n✝ + 1) ∣ b

case succ.isFalse
α : Type u_1
inst✝ : Monoid α
a b : α
n✝ : ℕ
h✝ : ¬FiniteMultiplicity a b
hk : ↑(n✝ + 1) ≤ ⊤
⊢ a ^ (n✝ + 1) ∣ b

Proof state:
α : Type u_1
inst✝ : Monoid α
a b : α
k : ℕ
hk : ↑k ≤ emultiplicity a b
⊢ a ^ k ∣ b

Tactic:
cases k

Result:
case zero
α : Type u_1
inst✝ : Monoid α
a b : α
hk : ↑0 ≤ emultiplicity a b
⊢ a ^ 0 ∣ b

case succ
α : Type u_1
inst✝ : Monoid α
a b : α
n✝ : ℕ
hk : ↑(n✝ + 1) ≤ emultiplicity a b
⊢ a ^ (n✝ + 1) ∣ b

Proof state:
case succ.isFalse
α : Type u_1
inst✝ : Monoid α
a b : α
n✝ : ℕ
h✝ : ¬FiniteMultiplicity a b
hk : ↑(n✝ + 1) ≤ ⊤
⊢ a ^ (n✝ + 1) ∣ b

Tactic:
apply FiniteMultiplicity.not_iff_forall.mp ‹_›

Result:
no goals

Proof state:
case succ
α : Type u_1
inst✝ : Monoid α
a b : α
n✝ : ℕ
hk : ↑(n✝ + 1) ≤ emultiplicity a b
⊢ a ^ (n✝ + 1) ∣ b

Tactic:
unfold emultiplicity at hk

Result:
case succ
α : Type u_1
inst✝ : Monoid α
a b : α
n✝ : ℕ
hk : ↑(n✝ + 1) ≤ if h : FiniteMultiplicity a b then ↑(Nat.find h) else ⊤
⊢ a ^ (n✝ + 1) ∣ b
-- Mathlib/FieldTheory/CardinalEmb.lean
theorem cardinal_eq_two_pow_sepDegree [Algebra.IsAlgebraic F E]
    (rank_inf : ℵ₀ ≤ sepDegree F E) : #(Field.Emb F E) = 2 ^ sepDegree F E

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
rank_inf : ℵ₀ ≤ sepDegree F E
⊢ #(Emb F E) = 2 ^ sepDegree F E

Tactic:
rw [← cardinal_separableClosure, cardinal_eq_two_pow_rank rank_inf]

Result:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
rank_inf : ℵ₀ ≤ sepDegree F E
⊢ 2 ^ Module.rank F ↥(separableClosure F E) = 2 ^ sepDegree F E

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
rank_inf : ℵ₀ ≤ sepDegree F E
⊢ 2 ^ Module.rank F ↥(separableClosure F E) = 2 ^ sepDegree F E

Tactic:
rfl

Result:
no goals
-- Mathlib/Probability/Distributions/Gamma.lean
/-- A Lebesgue Integral from -∞ to y can be expressed as the sum of one from -∞ to 0 and 0 to x -/
lemma lintegral_Iic_eq_lintegral_Iio_add_Icc {y z : ℝ} (f : ℝ → ℝ≥0∞) (hzy : z ≤ y) :
    ∫⁻ x in Iic y, f x = (∫⁻ x in Iio z, f x) + ∫⁻ x in Icc z y, f x

Proof state:
y z : ℝ
f : ℝ → ℝ≥0∞
hzy : z ≤ y
⊢ ∫⁻ (x : ℝ) in Iic y, f x = (∫⁻ (x : ℝ) in Iio z, f x) + ∫⁻ (x : ℝ) in Icc z y, f x

Tactic:
rw [← Iio_union_Icc_eq_Iic hzy, lintegral_union measurableSet_Icc]

Result:
y z : ℝ
f : ℝ → ℝ≥0∞
hzy : z ≤ y
⊢ Disjoint (Iio z) (Icc z y)

Proof state:
y z : ℝ
f : ℝ → ℝ≥0∞
hzy : z ≤ y
⊢ Disjoint (Iio z) (Icc z y)

Tactic:
simp_rw [Set.disjoint_iff_forall_ne, mem_Iio, mem_Icc]

Result:
y z : ℝ
f : ℝ → ℝ≥0∞
hzy : z ≤ y
⊢ ∀ ⦃a : ℝ⦄, a < z → ∀ ⦃b : ℝ⦄, z ≤ b ∧ b ≤ y → a ≠ b

Proof state:
y z : ℝ
f : ℝ → ℝ≥0∞
hzy : z ≤ y
⊢ ∀ ⦃a : ℝ⦄, a < z → ∀ ⦃b : ℝ⦄, z ≤ b ∧ b ≤ y → a ≠ b

Tactic:
intros

Result:
y z : ℝ
f : ℝ → ℝ≥0∞
hzy : z ≤ y
a✝² : ℝ
a✝¹ : a✝² < z
b✝ : ℝ
a✝ : z ≤ b✝ ∧ b✝ ≤ y
⊢ a✝² ≠ b✝

Proof state:
y z : ℝ
f : ℝ → ℝ≥0∞
hzy : z ≤ y
a✝² : ℝ
a✝¹ : a✝² < z
b✝ : ℝ
a✝ : z ≤ b✝ ∧ b✝ ≤ y
⊢ a✝² ≠ b✝

Tactic:
linarith

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_iSup_directed_of_measurable [Countable β] {f : β → α → ℝ≥0∞}
    (hf : ∀ b, Measurable (f b)) (h_directed : Directed (· ≤ ·) f) :
    ∫⁻ a, ⨆ b, f b a ∂μ = ⨆ b, ∫⁻ a, f b a ∂μ

Proof state:
case intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun x1 x2 => x1 ≤ x2) f
val✝ : Encodable β
⊢ ∫⁻ (a : α), ⨆ b, f b a ∂μ = ⨆ b, ∫⁻ (a : α), f b a ∂μ

Tactic:
cases isEmpty_or_nonempty β

Result:
case intro.inl
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun x1 x2 => x1 ≤ x2) f
val✝ : Encodable β
h✝ : IsEmpty β
⊢ ∫⁻ (a : α), ⨆ b, f b a ∂μ = ⨆ b, ∫⁻ (a : α), f b a ∂μ

case intro.inr
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun x1 x2 => x1 ≤ x2) f
val✝ : Encodable β
h✝ : Nonempty β
⊢ ∫⁻ (a : α), ⨆ b, f b a ∂μ = ⨆ b, ∫⁻ (a : α), f b a ∂μ
-- Mathlib/SetTheory/Game/Birthday.lean
theorem birthday_star : birthday ⟦PGame.star⟧ = 1

Proof state:
case a

⊢ 1 ≤ birthday ⟦PGame.star⟧

Tactic:
rw [Ordinal.one_le_iff_ne_zero, ne_eq, birthday_eq_zero, Game.zero_def,
  ← PGame.equiv_iff_game_eq]

Result:
case a

⊢ ¬PGame.star ≈ 0

Proof state:
case a

⊢ birthday ⟦PGame.star⟧ ≤ 1

Tactic:
rw [← PGame.birthday_star]

Result:
case a

⊢ birthday ⟦PGame.star⟧ ≤ PGame.star.birthday

Proof state:
⊢ birthday ⟦PGame.star⟧ = 1

Tactic:
apply le_antisymm

Result:
case a

⊢ birthday ⟦PGame.star⟧ ≤ 1

case a

⊢ 1 ≤ birthday ⟦PGame.star⟧

Proof state:
case a

⊢ ¬PGame.star ≈ 0

Tactic:
exact PGame.star_fuzzy_zero.not_equiv

Result:
no goals

Proof state:
case a

⊢ birthday ⟦PGame.star⟧ ≤ PGame.star.birthday

Tactic:
exact birthday_quot_le_pGameBirthday  _

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem S_add_two : ∀ n, S R (n + 2) = X * S R (n + 1) - S R n
  | (k : ℕ) => S.eq_3 R k
  | -(k + 1 : ℕ) => by linear_combination (norm := (simp [Int.negSucc_eq]; ring_nf)) S.eq_4 R k

Proof state:
R : Type u_1
inst✝ : CommRing R
k : ℕ
⊢ S R (-↑(k + 1) + 2) = X * S R (-↑(k + 1) + 1) - S R (-↑(k + 1))

Tactic:
linear_combination (norm := (simp [Int.negSucc_eq]; ring_nf)) S.eq_4 R k

Result:
no goals

Proof state:
case a.a
R : Type u_1
inst✝ : CommRing R
k : ℕ
⊢ S R (-↑(k + 1) + 2) + (X * S R (-↑k) - S R (-↑k + 1)) -
      (X * S R (-↑(k + 1) + 1) - S R (-↑(k + 1)) + S R (Int.negSucc k)) =
    0

Tactic:
simp [Int.negSucc_eq]

Result:
case a.a
R : Type u_1
inst✝ : CommRing R
k : ℕ
⊢ S R (-1 + -↑k + 2) + (X * S R (-↑k) - S R (-↑k + 1)) - X * S R (-↑k) = 0

Proof state:
case a.a
R : Type u_1
inst✝ : CommRing R
k : ℕ
⊢ S R (-1 + -↑k + 2) + (X * S R (-↑k) - S R (-↑k + 1)) - X * S R (-↑k) = 0

Tactic:
ring_nf

Result:
no goals
-- Mathlib/Algebra/SMulWithZero.lean
lemma boole_smul (a : M) : (if p then 1 else 0 : R) • a = if p then a else 0

Proof state:
R : Type u_1
M : Type u_3
inst✝³ : MonoidWithZero R
inst✝² : Zero M
inst✝¹ : MulActionWithZero R M
p : Prop
inst✝ : Decidable p
a : M
⊢ (if p then 1 else 0) • a = if p then a else 0

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Flat/CategoryTheory.lean
lemma lTensor_shortComplex_exact [Flat R M] (C : ShortComplex <| ModuleCat R) (hC : C.Exact) :
    C.map (tensorLeft M) |>.Exact

Proof state:
R : Type u
inst✝¹ : CommRing R
M : ModuleCat R
inst✝ : Flat R ↑M
C : ShortComplex (ModuleCat R)
hC : C.Exact
⊢ (C.map (tensorLeft M)).Exact

Tactic:
rw [moduleCat_exact_iff_function_exact] at hC ⊢

Result:
R : Type u
inst✝¹ : CommRing R
M : ModuleCat R
inst✝ : Flat R ↑M
C : ShortComplex (ModuleCat R)
hC : Function.Exact ⇑(ConcreteCategory.hom C.f) ⇑(ConcreteCategory.hom C.g)
⊢ Function.Exact ⇑(ConcreteCategory.hom (C.map (tensorLeft M)).f) ⇑(ConcreteCategory.hom (C.map (tensorLeft M)).g)

Proof state:
R : Type u
inst✝¹ : CommRing R
M : ModuleCat R
inst✝ : Flat R ↑M
C : ShortComplex (ModuleCat R)
hC : Function.Exact ⇑(ConcreteCategory.hom C.f) ⇑(ConcreteCategory.hom C.g)
⊢ Function.Exact ⇑(ConcreteCategory.hom (C.map (tensorLeft M)).f) ⇑(ConcreteCategory.hom (C.map (tensorLeft M)).g)

Tactic:
exact lTensor_exact M hC

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Zip.lean
theorem zipWith_map_right (l₁ : Array α) (l₂ : Array β) (f : β → β') (g : α → β' → γ) :
    zipWith g l₁ (l₂.map f) = zipWith (fun a b => g a (f b)) l₁ l₂

Proof state:
case mk
α : Type u_1
β : Type u_2
β' : Type u_3
γ : Type u_4
l₂ : Array β
f : β → β'
g : α → β' → γ
toList✝ : List α
⊢ zipWith g { toList := toList✝ } (map f l₂) = zipWith (fun a b => g a (f b)) { toList := toList✝ } l₂

Tactic:
cases l₂

Result:
case mk.mk
α : Type u_1
β : Type u_2
β' : Type u_3
γ : Type u_4
f : β → β'
g : α → β' → γ
toList✝¹ : List α
toList✝ : List β
⊢ zipWith g { toList := toList✝¹ } (map f { toList := toList✝ }) =
    zipWith (fun a b => g a (f b)) { toList := toList✝¹ } { toList := toList✝ }

Proof state:
α : Type u_1
β : Type u_2
β' : Type u_3
γ : Type u_4
l₁ : Array α
l₂ : Array β
f : β → β'
g : α → β' → γ
⊢ zipWith g l₁ (map f l₂) = zipWith (fun a b => g a (f b)) l₁ l₂

Tactic:
cases l₁

Result:
case mk
α : Type u_1
β : Type u_2
β' : Type u_3
γ : Type u_4
l₂ : Array β
f : β → β'
g : α → β' → γ
toList✝ : List α
⊢ zipWith g { toList := toList✝ } (map f l₂) = zipWith (fun a b => g a (f b)) { toList := toList✝ } l₂

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
β' : Type u_3
γ : Type u_4
f : β → β'
g : α → β' → γ
toList✝¹ : List α
toList✝ : List β
⊢ zipWith g { toList := toList✝¹ } (map f { toList := toList✝ }) =
    zipWith (fun a b => g a (f b)) { toList := toList✝¹ } { toList := toList✝ }

Tactic:
simp [List.zipWith_map_right]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem natDegree_X_pow_add_C {n : ℕ} {r : R} : (X ^ n + C r).natDegree = n

Proof state:
case neg
R : Type u
inst✝¹ : Nontrivial R
inst✝ : Semiring R
n : ℕ
r : R
hn : ¬n = 0
⊢ (X ^ n + C r).natDegree = n

Tactic:
exact natDegree_eq_of_degree_eq_some (degree_X_pow_add_C (pos_iff_ne_zero.mpr hn) r)

Result:
no goals

Proof state:
case pos
R : Type u
inst✝¹ : Nontrivial R
inst✝ : Semiring R
n : ℕ
r : R
hn : n = 0
⊢ (X ^ n + C r).natDegree = n

Tactic:
rw [hn, pow_zero, ← C_1, ← RingHom.map_add, natDegree_C]

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Nontrivial R
inst✝ : Semiring R
n : ℕ
r : R
⊢ (X ^ n + C r).natDegree = n

Tactic:
by_cases hn : n = 0

Result:
case pos
R : Type u
inst✝¹ : Nontrivial R
inst✝ : Semiring R
n : ℕ
r : R
hn : n = 0
⊢ (X ^ n + C r).natDegree = n

case neg
R : Type u
inst✝¹ : Nontrivial R
inst✝ : Semiring R
n : ℕ
r : R
hn : ¬n = 0
⊢ (X ^ n + C r).natDegree = n
-- Mathlib/Data/Finset/Insert.lean
theorem eq_singleton_iff_unique_mem {s : Finset α} {a : α} : s = {a} ↔ a ∈ s ∧ ∀ x ∈ s, x = a

Proof state:
case mpr.h
α : Type u_1
s : Finset α
a : α
t : a ∈ s ∧ ∀ x ∈ s, x = a
a✝ : α
⊢ a✝ ∈ s ↔ a✝ ∈ {a}

Tactic:
rw [Finset.mem_singleton]

Result:
case mpr.h
α : Type u_1
s : Finset α
a : α
t : a ∈ s ∧ ∀ x ∈ s, x = a
a✝ : α
⊢ a✝ ∈ s ↔ a✝ = a

Proof state:
α : Type u_1
s : Finset α
a : α
⊢ s = {a} ↔ a ∈ s ∧ ∀ x ∈ s, x = a

Tactic:
constructor <;> intro t

Result:
case mp
α : Type u_1
s : Finset α
a : α
t : s = {a}
⊢ a ∈ s ∧ ∀ x ∈ s, x = a

case mpr
α : Type u_1
s : Finset α
a : α
t : a ∈ s ∧ ∀ x ∈ s, x = a
⊢ s = {a}

Proof state:
case mp
α : Type u_1
s : Finset α
a : α
t : s = {a}
⊢ a ∈ {a} ∧ ∀ x ∈ {a}, x = a

Tactic:
exact ⟨Finset.mem_singleton_self _, fun _ => Finset.mem_singleton.1⟩

Result:
no goals

Proof state:
case mpr.h
α : Type u_1
s : Finset α
a : α
t : a ∈ s ∧ ∀ x ∈ s, x = a
a✝ : α
⊢ a✝ ∈ s ↔ a✝ = a

Tactic:
exact ⟨t.right _, fun r => r.symm ▸ t.left⟩

Result:
no goals

Proof state:
case mp
α : Type u_1
s : Finset α
a : α
t : s = {a}
⊢ a ∈ s ∧ ∀ x ∈ s, x = a

Tactic:
rw [t]

Result:
case mp
α : Type u_1
s : Finset α
a : α
t : s = {a}
⊢ a ∈ {a} ∧ ∀ x ∈ {a}, x = a

Proof state:
case mpr
α : Type u_1
s : Finset α
a : α
t : a ∈ s ∧ ∀ x ∈ s, x = a
⊢ s = {a}

Tactic:
ext

Result:
case mpr.h
α : Type u_1
s : Finset α
a : α
t : a ∈ s ∧ ∀ x ∈ s, x = a
a✝ : α
⊢ a✝ ∈ s ↔ a✝ ∈ {a}
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem sup_succ_le_lsub {ι : Type u} (f : ι → Ordinal.{max u v}) :
    succ (sup.{_, v} f) ≤ lsub.{_, v} f ↔ ∃ i, f i = sup.{_, v} f

Proof state:
case refine_1
ι : Type u
f : ι → Ordinal.{max u v}
h : succ (sup f) ≤ lsub f
⊢ ∃ i, f i = sup f

Tactic:
by_contra! hf

Result:
case refine_1
ι : Type u
f : ι → Ordinal.{max u v}
h : succ (sup f) ≤ lsub f
hf : ∀ (i : ι), f i ≠ sup f
⊢ False

Proof state:
case refine_1
ι : Type u
f : ι → Ordinal.{max u v}
h : succ (sup f) ≤ lsub f
hf : ∀ (i : ι), f i ≠ sup f
⊢ False

Tactic:
exact (succ_le_iff.1 h).ne ((sup_le_lsub f).antisymm (lsub_le (ne_sup_iff_lt_sup.1 hf)))

Result:
no goals

Proof state:
case refine_2.intro
ι : Type u
f : ι → Ordinal.{max u v}
w✝ : ι
hf : f w✝ = sup f
⊢ succ (sup f) ≤ lsub f

Tactic:
rw [succ_le_iff, ← hf]

Result:
case refine_2.intro
ι : Type u
f : ι → Ordinal.{max u v}
w✝ : ι
hf : f w✝ = sup f
⊢ f w✝ < lsub f

Proof state:
case refine_2.intro
ι : Type u
f : ι → Ordinal.{max u v}
w✝ : ι
hf : f w✝ = sup f
⊢ f w✝ < lsub f

Tactic:
exact lt_lsub _ _

Result:
no goals

Proof state:
ι : Type u
f : ι → Ordinal.{max u v}
⊢ succ (sup f) ≤ lsub f ↔ ∃ i, f i = sup f

Tactic:
refine ⟨fun h => ?_, ?_⟩

Result:
case refine_1
ι : Type u
f : ι → Ordinal.{max u v}
h : succ (sup f) ≤ lsub f
⊢ ∃ i, f i = sup f

case refine_2
ι : Type u
f : ι → Ordinal.{max u v}
⊢ (∃ i, f i = sup f) → succ (sup f) ≤ lsub f

Proof state:
case refine_2
ι : Type u
f : ι → Ordinal.{max u v}
⊢ (∃ i, f i = sup f) → succ (sup f) ≤ lsub f

Tactic:
rintro ⟨_, hf⟩

Result:
case refine_2.intro
ι : Type u
f : ι → Ordinal.{max u v}
w✝ : ι
hf : f w✝ = sup f
⊢ succ (sup f) ≤ lsub f
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem setWidth_setWidth {x : BitVec u} {w v : Nat} (h : ¬ (v < u ∧ v < w)) :
    setWidth w (setWidth v x) = setWidth w x

Proof state:
case pred
u : Nat
x : BitVec u
w v : Nat
h : ¬(v < u ∧ v < w)
i✝ : Nat
a✝ : i✝ < w
⊢ x.getLsbD i✝ = true → i✝ < v

Tactic:
intro h

Result:
case pred
u : Nat
x : BitVec u
w v : Nat
h✝ : ¬(v < u ∧ v < w)
i✝ : Nat
a✝ : i✝ < w
h : x.getLsbD i✝ = true
⊢ i✝ < v

Proof state:
case pred
u : Nat
x : BitVec u
w v : Nat
h : ¬(v < u ∧ v < w)
i✝ : Nat
a✝ : i✝ < w
⊢ (setWidth w (setWidth v x)).getLsbD i✝ = (setWidth w x).getLsbD i✝

Tactic:
simp_all only [getLsbD_setWidth, decide_true, Bool.true_and, Bool.and_iff_right_iff_imp,
  decide_eq_true_eq]

Result:
case pred
u : Nat
x : BitVec u
w v : Nat
h : ¬(v < u ∧ v < w)
i✝ : Nat
a✝ : i✝ < w
⊢ x.getLsbD i✝ = true → i✝ < v

Proof state:
case pred
u : Nat
x : BitVec u
w v : Nat
h✝ : ¬(v < u ∧ v < w)
i✝ : Nat
a✝ : i✝ < w
h : i✝ < u
⊢ i✝ < v

Tactic:
omega

Result:
no goals

Proof state:
u : Nat
x : BitVec u
w v : Nat
h : ¬(v < u ∧ v < w)
⊢ setWidth w (setWidth v x) = setWidth w x

Tactic:
ext

Result:
case pred
u : Nat
x : BitVec u
w v : Nat
h : ¬(v < u ∧ v < w)
i✝ : Nat
a✝ : i✝ < w
⊢ (setWidth w (setWidth v x)).getLsbD i✝ = (setWidth w x).getLsbD i✝

Proof state:
case pred
u : Nat
x : BitVec u
w v : Nat
h✝ : ¬(v < u ∧ v < w)
i✝ : Nat
a✝ : i✝ < w
h : x.getLsbD i✝ = true
⊢ i✝ < v

Tactic:
replace h := lt_of_getLsbD h

Result:
case pred
u : Nat
x : BitVec u
w v : Nat
h✝ : ¬(v < u ∧ v < w)
i✝ : Nat
a✝ : i✝ < w
h : i✝ < u
⊢ i✝ < v
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem find?_cons_of_neg (l) (h : ¬p a) : find? p (a :: l) = find? p l

Proof state:
α✝ : Type u_1
p : α✝ → Bool
a : α✝
l : List α✝
h : ¬p a = true
⊢ find? p (a :: l) = find? p l

Tactic:
simp [find?, h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem and_iff_left_iff_imp  : ∀ {a b : Bool}, ((a && b) = a) ↔ (a → b)

Proof state:
⊢ ∀ {a b : Bool}, (a && b) = a ↔ a = true → b = true

Tactic:
decide

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Field.lean
theorem tendsto_const_mul_atBot_iff_pos [NeBot l] (h : Tendsto f l atBot) :
    Tendsto (fun x => r * f x) l atBot ↔ 0 < r

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField α
l : Filter β
f : β → α
r : α
inst✝ : l.NeBot
h : Tendsto f l atBot
⊢ Tendsto (fun x => r * f x) l atBot ↔ 0 < r

Tactic:
simp [tendsto_const_mul_atBot_iff, h, h.not_tendsto disjoint_atBot_atTop]

Result:
no goals
-- Mathlib/Data/Sigma/Lex.lean
theorem lex_swap : Lex (Function.swap r) s a b ↔ Lex r (fun i => Function.swap (s i)) b a

Proof state:
case mpr
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
a b : (i : ι) × α i
⊢ Lex r (fun i => Function.swap (s i)) b a → Lex (Function.swap r) s a b

Tactic:
rintro (⟨a, b, h⟩ | ⟨a, b, h⟩)

Result:
case mpr.left
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
i✝ j✝ : ι
a : α i✝
b : α j✝
h : r i✝ j✝
⊢ Lex (Function.swap r) s ⟨j✝, b⟩ ⟨i✝, a⟩

case mpr.right
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
i✝ : ι
a b : α i✝
h : Function.swap (s i✝) a b
⊢ Lex (Function.swap r) s ⟨i✝, b⟩ ⟨i✝, a⟩

Proof state:
case mpr.right
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
i✝ : ι
a b : α i✝
h : Function.swap (s i✝) a b
⊢ Lex (Function.swap r) s ⟨i✝, b⟩ ⟨i✝, a⟩

Tactic:
exact Lex.right _ _ h

Result:
no goals

Proof state:
case mpr.left
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
i✝ j✝ : ι
a : α i✝
b : α j✝
h : r i✝ j✝
⊢ Lex (Function.swap r) s ⟨j✝, b⟩ ⟨i✝, a⟩

Tactic:
exact Lex.left _ _ h

Result:
no goals