harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Calculus/MeanValue.lean
theorem norm_image_sub_le_of_norm_deriv_le_segment {C : ℝ} (hf : DifferentiableOn ℝ f (Icc a b))
    (bound : ∀ x ∈ Ico a b, ‖derivWithin f (Icc a b) x‖ ≤ C) :
    ∀ x ∈ Icc a b, ‖f x - f a‖ ≤ C * (x - a)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b C : ℝ
hf : DifferentiableOn ℝ f (Icc a b)
bound : ∀ x ∈ Ico a b, ‖derivWithin f (Icc a b) x‖ ≤ C
⊢ ∀ x ∈ Icc a b, HasDerivWithinAt f (derivWithin f (Icc a b) x) (Icc a b) x

Tactic:
exact fun x hx => (hf x hx).hasDerivWithinAt

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b C : ℝ
hf : DifferentiableOn ℝ f (Icc a b)
bound : ∀ x ∈ Ico a b, ‖derivWithin f (Icc a b) x‖ ≤ C
⊢ ∀ x ∈ Icc a b, ‖f x - f a‖ ≤ C * (x - a)

Tactic:
refine norm_image_sub_le_of_norm_deriv_le_segment' ?_ bound

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b C : ℝ
hf : DifferentiableOn ℝ f (Icc a b)
bound : ∀ x ∈ Ico a b, ‖derivWithin f (Icc a b) x‖ ≤ C
⊢ ∀ x ∈ Icc a b, HasDerivWithinAt f (derivWithin f (Icc a b) x) (Icc a b) x
-- Mathlib/Algebra/Polynomial/Smeval.lean
theorem eval₂_smulOneHom_eq_smeval (R : Type*) [Semiring R] {S : Type*} [Semiring S] [Module R S]
    [IsScalarTower R S S] (p : R[X]) (x : S) :
    p.eval₂ RingHom.smulOneHom x = p.smeval x

Proof state:
case e_f.h.h
R : Type u_3
inst✝³ : Semiring R
S : Type u_4
inst✝² : Semiring S
inst✝¹ : Module R S
inst✝ : IsScalarTower R S S
p : R[X]
x : S
e : ℕ
a : R
⊢ RingHom.smulOneHom a * x ^ e = smul_pow x e a

Tactic:
simp only [RingHom.smulOneHom_apply, smul_one_mul, smul_pow]

Result:
no goals

Proof state:
R : Type u_3
inst✝³ : Semiring R
S : Type u_4
inst✝² : Semiring S
inst✝¹ : Module R S
inst✝ : IsScalarTower R S S
p : R[X]
x : S
⊢ (p.sum fun e a => RingHom.smulOneHom a * x ^ e) = p.sum (smul_pow x)

Tactic:
congr 1 with e a

Result:
case e_f.h.h
R : Type u_3
inst✝³ : Semiring R
S : Type u_4
inst✝² : Semiring S
inst✝¹ : Module R S
inst✝ : IsScalarTower R S S
p : R[X]
x : S
e : ℕ
a : R
⊢ RingHom.smulOneHom a * x ^ e = smul_pow x e a

Proof state:
R : Type u_3
inst✝³ : Semiring R
S : Type u_4
inst✝² : Semiring S
inst✝¹ : Module R S
inst✝ : IsScalarTower R S S
p : R[X]
x : S
⊢ eval₂ RingHom.smulOneHom x p = p.smeval x

Tactic:
rw [smeval_eq_sum, eval₂_eq_sum]

Result:
R : Type u_3
inst✝³ : Semiring R
S : Type u_4
inst✝² : Semiring S
inst✝¹ : Module R S
inst✝ : IsScalarTower R S S
p : R[X]
x : S
⊢ (p.sum fun e a => RingHom.smulOneHom a * x ^ e) = p.sum (smul_pow x)
-- Mathlib/Algebra/Quaternion.lean
theorem mul_re : (a * b).re = a.re * b.re - a.imI * b.imI - a.imJ * b.imJ - a.imK * b.imK :=
  (QuaternionAlgebra.mul_re a b).trans <| by simp [one_mul, neg_mul, sub_eq_add_neg, neg_neg]

Proof state:
R : Type u_3
inst✝ : CommRing R
a b : ℍ[R]
⊢ a.re * b.re + -1 * a.imI * b.imI + -1 * a.imJ * b.imJ + 0 * -1 * a.imJ * b.imK - -1 * -1 * a.imK * b.imK =
    a.re * b.re - a.imI * b.imI - a.imJ * b.imJ - a.imK * b.imK

Tactic:
simp [one_mul, neg_mul, sub_eq_add_neg, neg_neg]

Result:
no goals
-- Mathlib/Data/Set/Finite/Lattice.lean
theorem Finite.sUnion {s : Set (Set α)} (hs : s.Finite) (H : ∀ t ∈ s, Set.Finite t) :
    (⋃₀ s).Finite

Proof state:
α : Type u
s : Set (Set α)
hs : s.Finite
H : ∀ t ∈ s, t.Finite
⊢ (⋃₀ s).Finite

Tactic:
simpa only [sUnion_eq_biUnion] using hs.biUnion H

Result:
no goals
-- Mathlib/CategoryTheory/Limits/HasLimits.lean
theorem colimit.ι_inv_pre [IsIso (pre F E)] (k : K) :
    colimit.ι F (E.obj k) ≫ inv (colimit.pre F E) = colimit.ι (E ⋙ F) k

Proof state:
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁴ : Category.{v₂, u₂} K
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
inst✝² : HasColimit F
E : K ⥤ J
inst✝¹ : HasColimit (E ⋙ F)
inst✝ : IsIso (pre F E)
k : K
⊢ ι F (E.obj k) ≫ inv (pre F E) = ι (E ⋙ F) k

Tactic:
simp [IsIso.comp_inv_eq]

Result:
no goals
-- Mathlib/Topology/Compactness/Compact.lean
theorem prod_nhdsSet_le_of_disjoint_cocompact {t : Set Y} {f : Filter X} (ht : IsCompact t)
    (hf : Disjoint f (Filter.cocompact X)) :
    f ×ˢ 𝓝ˢ t ≤ 𝓝ˢ (Set.univ ×ˢ t)

Proof state:
case intro.intro
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
t : Set Y
f : Filter X
ht : IsCompact t
hf : Disjoint f (cocompact X)
K : Set X
hKf : K ∈ f
hK : IsCompact K
⊢ f ×ˢ 𝓝ˢ t ≤ 𝓝ˢ (univ ×ˢ t)

Tactic:
calc
  f ×ˢ 𝓝ˢ t
  _ ≤ (𝓟 K) ×ˢ 𝓝ˢ t      := Filter.prod_mono_left _ (Filter.le_principal_iff.mpr hKf)
  _ ≤ 𝓝ˢ K ×ˢ 𝓝ˢ t       := Filter.prod_mono_left _ principal_le_nhdsSet
  _ = 𝓝ˢ (K ×ˢ t)         := (hK.nhdsSet_prod_eq ht).symm
  _ ≤ 𝓝ˢ (Set.univ ×ˢ t)  := nhdsSet_mono (prod_mono_left le_top)

Result:
no goals

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
t : Set Y
f : Filter X
ht : IsCompact t
hf : Disjoint f (cocompact X)
⊢ f ×ˢ 𝓝ˢ t ≤ 𝓝ˢ (univ ×ˢ t)

Tactic:
obtain ⟨K, hKf, hK⟩ := (disjoint_cocompact_right f).mp hf

Result:
case intro.intro
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
t : Set Y
f : Filter X
ht : IsCompact t
hf : Disjoint f (cocompact X)
K : Set X
hKf : K ∈ f
hK : IsCompact K
⊢ f ×ˢ 𝓝ˢ t ≤ 𝓝ˢ (univ ×ˢ t)
-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem toSignedMeasure_smul (μ : Measure α) [IsFiniteMeasure μ] (r : ℝ≥0) :
    (r • μ).toSignedMeasure = r • μ.toSignedMeasure

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
r : ℝ≥0
⊢ (r • μ).toSignedMeasure = r • μ.toSignedMeasure

Tactic:
ext i hi

Result:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
r : ℝ≥0
i : Set α
hi : MeasurableSet i
⊢ ↑(r • μ).toSignedMeasure i = ↑(r • μ.toSignedMeasure) i

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
r : ℝ≥0
i : Set α
hi : MeasurableSet i
⊢ ↑(r • μ).toSignedMeasure i = ↑(r • μ.toSignedMeasure) i

Tactic:
rw [toSignedMeasure_apply_measurable hi, VectorMeasure.smul_apply,
  toSignedMeasure_apply_measurable hi, coe_smul, Pi.smul_apply, ENNReal.toReal_smul]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean
theorem arcsin_neg (x : ℝ) : arcsin (-x) = -arcsin x

Proof state:
case inl
x : ℝ
hx₁ : x ≤ -1
⊢ arcsin (-x) = -arcsin x

Tactic:
rw [arcsin_of_le_neg_one hx₁, neg_neg, arcsin_of_one_le (le_neg.2 hx₁)]

Result:
no goals

Proof state:
x : ℝ
⊢ arcsin (-x) = -arcsin x

Tactic:
rcases le_total x (-1) with hx₁ | hx₁

Result:
case inl
x : ℝ
hx₁ : x ≤ -1
⊢ arcsin (-x) = -arcsin x

case inr
x : ℝ
hx₁ : -1 ≤ x
⊢ arcsin (-x) = -arcsin x

Proof state:
case inr
x : ℝ
hx₁ : -1 ≤ x
⊢ arcsin (-x) = -arcsin x

Tactic:
rcases le_total 1 x with hx₂ | hx₂

Result:
case inr.inl
x : ℝ
hx₁ : -1 ≤ x
hx₂ : 1 ≤ x
⊢ arcsin (-x) = -arcsin x

case inr.inr
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ arcsin (-x) = -arcsin x

Proof state:
case inr.inr.refine_1
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ sin (-arcsin x) = -x

Tactic:
rw [sin_neg, sin_arcsin hx₁ hx₂]

Result:
no goals

Proof state:
case inr.inl
x : ℝ
hx₁ : -1 ≤ x
hx₂ : 1 ≤ x
⊢ arcsin (-x) = -arcsin x

Tactic:
rw [arcsin_of_one_le hx₂, arcsin_of_le_neg_one (neg_le_neg hx₂)]

Result:
no goals

Proof state:
case inr.inr.refine_2
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ -arcsin x ∈ Icc (-(π / 2)) (π / 2)

Tactic:
exact ⟨neg_le_neg (arcsin_le_pi_div_two _), neg_le.2 (neg_pi_div_two_le_arcsin _)⟩

Result:
no goals

Proof state:
case inr.inr
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ arcsin (-x) = -arcsin x

Tactic:
refine arcsin_eq_of_sin_eq ?_ ?_

Result:
case inr.inr.refine_1
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ sin (-arcsin x) = -x

case inr.inr.refine_2
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ -arcsin x ∈ Icc (-(π / 2)) (π / 2)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getMsbD_shiftLeftZeroExtend (x : BitVec m) (n : Nat) :
    getMsbD (shiftLeftZeroExtend x n) i = getMsbD x i

Proof state:
m i : Nat
x : BitVec m
n : Nat
this : m + n - m ≤ i + n
⊢ i + n + m - (m + n) = i

Tactic:
omega

Result:
no goals

Proof state:
m i : Nat
x : BitVec m
n : Nat
⊢ (x.shiftLeftZeroExtend n).getMsbD i = x.getMsbD i

Tactic:
have : m + n - m ≤ i + n := by omega

Result:
m i : Nat
x : BitVec m
n : Nat
this : m + n - m ≤ i + n
⊢ (x.shiftLeftZeroExtend n).getMsbD i = x.getMsbD i

Proof state:
m i : Nat
x : BitVec m
n : Nat
⊢ m + n - m ≤ i + n

Tactic:
omega

Result:
no goals

Proof state:
m i : Nat
x : BitVec m
n : Nat
this : m + n - m ≤ i + n
⊢ (x.shiftLeftZeroExtend n).getMsbD i = x.getMsbD i

Tactic:
have : i + n + m - (m + n) = i := by omega

Result:
m i : Nat
x : BitVec m
n : Nat
this✝ : m + n - m ≤ i + n
this : i + n + m - (m + n) = i
⊢ (x.shiftLeftZeroExtend n).getMsbD i = x.getMsbD i

Proof state:
m i : Nat
x : BitVec m
n : Nat
this✝ : m + n - m ≤ i + n
this : i + n + m - (m + n) = i
⊢ (x.shiftLeftZeroExtend n).getMsbD i = x.getMsbD i

Tactic:
simp_all [shiftLeftZeroExtend_eq]

Result:
no goals
-- Mathlib/Data/Int/Lemmas.lean
theorem natAbs_coe_sub_coe_le_of_le {a b n : ℕ} (a_le_n : a ≤ n) (b_le_n : b ≤ n) :
    natAbs (a - b : ℤ) ≤ n

Proof state:
a b n : ℕ
a_le_n : a ≤ n
b_le_n : b ≤ n
⊢ (↑a - ↑b).natAbs ≤ n

Tactic:
rw [← Nat.cast_le (α := ℤ), natCast_natAbs]

Result:
a b n : ℕ
a_le_n : a ≤ n
b_le_n : b ≤ n
⊢ |↑a - ↑b| ≤ ↑n

Proof state:
a b n : ℕ
a_le_n : a ≤ n
b_le_n : b ≤ n
⊢ |↑a - ↑b| ≤ ↑n

Tactic:
exact abs_sub_le_of_nonneg_of_le (ofNat_nonneg a) (ofNat_le.mpr a_le_n)
  (ofNat_nonneg b) (ofNat_le.mpr b_le_n)

Result:
no goals
-- Mathlib/Analysis/Normed/Affine/ContinuousAffineMap.lean
theorem coe_contLinear_eq_linear (f : P →ᴬ[R] Q) :
    (f.contLinear : V →ₗ[R] W) = (f : P →ᵃ[R] Q).linear

Proof state:
case h
R : Type u_2
V : Type u_3
W : Type u_4
P : Type u_6
Q : Type u_7
inst✝⁸ : NormedAddCommGroup V
inst✝⁷ : MetricSpace P
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : MetricSpace Q
inst✝³ : NormedAddTorsor W Q
inst✝² : NormedField R
inst✝¹ : NormedSpace R V
inst✝ : NormedSpace R W
f : P →ᴬ[R] Q
x✝ : V
⊢ ↑f.contLinear x✝ = (↑f).linear x✝

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_2
V : Type u_3
W : Type u_4
P : Type u_6
Q : Type u_7
inst✝⁸ : NormedAddCommGroup V
inst✝⁷ : MetricSpace P
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : MetricSpace Q
inst✝³ : NormedAddTorsor W Q
inst✝² : NormedField R
inst✝¹ : NormedSpace R V
inst✝ : NormedSpace R W
f : P →ᴬ[R] Q
⊢ ↑f.contLinear = (↑f).linear

Tactic:
ext

Result:
case h
R : Type u_2
V : Type u_3
W : Type u_4
P : Type u_6
Q : Type u_7
inst✝⁸ : NormedAddCommGroup V
inst✝⁷ : MetricSpace P
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : MetricSpace Q
inst✝³ : NormedAddTorsor W Q
inst✝² : NormedField R
inst✝¹ : NormedSpace R V
inst✝ : NormedSpace R W
f : P →ᴬ[R] Q
x✝ : V
⊢ ↑f.contLinear x✝ = (↑f).linear x✝
-- Mathlib/Topology/Compactness/Compact.lean
theorem IsCompact.mem_inf_nhdsSet_of_forall {K : Set X} {l : Filter X} {s : Set X}
    (hK : IsCompact K) (hs : ∀ y ∈ K, s ∈ l ⊓ 𝓝 y) : s ∈ l ⊓ 𝓝ˢ K :=
  (hK.inf_nhdsSet_eq_biSup l).symm ▸ by simpa using hs

Proof state:
X : Type u
inst✝ : TopologicalSpace X
K : Set X
l : Filter X
s : Set X
hK : IsCompact K
hs : ∀ y ∈ K, s ∈ l ⊓ 𝓝 y
⊢ s ∈ ⨆ x ∈ K, l ⊓ 𝓝 x

Tactic:
simpa using hs

Result:
no goals
-- Mathlib/FieldTheory/Finite/Basic.lean
lemma pow_card_sub_one {p : ℕ} [Fact p.Prime] (a : ZMod p) :
    a ^ (p - 1) = if a ≠ 0 then 1 else 0

Proof state:
case pos
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
⊢ a ^ (p - 1) = 1

Tactic:
exact pow_card_sub_one_eq_one ha

Result:
no goals

Proof state:
case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : ¬a ≠ 0
⊢ a ^ (p - 1) = 0

Tactic:
simp [of_not_not ha, (Fact.out : p.Prime).one_lt, tsub_eq_zero_iff_le]

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
⊢ a ^ (p - 1) = if a ≠ 0 then 1 else 0

Tactic:
split_ifs with ha

Result:
case pos
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
⊢ a ^ (p - 1) = 1

case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : ¬a ≠ 0
⊢ a ^ (p - 1) = 0
-- Mathlib/Probability/Process/Stopping.lean
theorem condExp_stopping_time_ae_eq_restrict_eq [FirstCountableTopology ι]
    [SigmaFiniteFiltration μ ℱ] (hτ : IsStoppingTime ℱ τ)
    [SigmaFinite (μ.trim hτ.measurableSpace_le)] (i : ι) :
    μ[f|hτ.measurableSpace] =ᵐ[μ.restrict {x | τ x = i}] μ[f|ℱ i]

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁹ : LinearOrder ι
μ : Measure Ω
ℱ : Filtration ι m
τ : Ω → ι
E : Type u_4
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
f : Ω → E
inst✝⁵ : atTop.IsCountablyGenerated
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : FirstCountableTopology ι
inst✝¹ : SigmaFiniteFiltration μ ℱ
hτ : IsStoppingTime ℱ τ
inst✝ : SigmaFinite (μ.trim ⋯)
i : ι
t : Set Ω
⊢ MeasurableSet ({x | τ x = i} ∩ t) ↔ MeasurableSet ({x | τ x = i} ∩ t)

Tactic:
rw [Set.inter_comm _ t, IsStoppingTime.measurableSet_inter_eq_iff]

Result:
no goals

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁹ : LinearOrder ι
μ : Measure Ω
ℱ : Filtration ι m
τ : Ω → ι
E : Type u_4
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
f : Ω → E
inst✝⁵ : atTop.IsCountablyGenerated
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : FirstCountableTopology ι
inst✝¹ : SigmaFiniteFiltration μ ℱ
hτ : IsStoppingTime ℱ τ
inst✝ : SigmaFinite (μ.trim ⋯)
i : ι
⊢ μ[f|hτ.measurableSpace] =ᶠ[ae (μ.restrict {x | τ x = i})] μ[f|↑ℱ i]

Tactic:
refine condExp_ae_eq_restrict_of_measurableSpace_eq_on hτ.measurableSpace_le (ℱ.le i)
  (hτ.measurableSet_eq' i) fun t => ?_

Result:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁹ : LinearOrder ι
μ : Measure Ω
ℱ : Filtration ι m
τ : Ω → ι
E : Type u_4
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
f : Ω → E
inst✝⁵ : atTop.IsCountablyGenerated
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : FirstCountableTopology ι
inst✝¹ : SigmaFiniteFiltration μ ℱ
hτ : IsStoppingTime ℱ τ
inst✝ : SigmaFinite (μ.trim ⋯)
i : ι
t : Set Ω
⊢ MeasurableSet ({x | τ x = i} ∩ t) ↔ MeasurableSet ({x | τ x = i} ∩ t)
-- Mathlib/RingTheory/DedekindDomain/Ideal.lean
theorem one_mem_inv_coe_ideal [IsDomain A] {I : Ideal A} (hI : I ≠ ⊥) :
    (1 : K) ∈ (I : FractionalIdeal A⁰ K)⁻¹

Proof state:
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDomain A
I : Ideal A
hI : I ≠ ⊥
⊢ 1 ∈ (↑I)⁻¹

Tactic:
rw [FractionalIdeal.mem_inv_iff (FractionalIdeal.coeIdeal_ne_zero.mpr hI)]

Result:
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDomain A
I : Ideal A
hI : I ≠ ⊥
⊢ ∀ y ∈ ↑I, 1 * y ∈ 1

Proof state:
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDomain A
I : Ideal A
hI : I ≠ ⊥
y : K
hy : y ∈ ↑I
⊢ 1 * y ∈ 1

Tactic:
rw [one_mul]

Result:
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDomain A
I : Ideal A
hI : I ≠ ⊥
y : K
hy : y ∈ ↑I
⊢ y ∈ 1

Proof state:
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDomain A
I : Ideal A
hI : I ≠ ⊥
⊢ ∀ y ∈ ↑I, 1 * y ∈ 1

Tactic:
intro y hy

Result:
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDomain A
I : Ideal A
hI : I ≠ ⊥
y : K
hy : y ∈ ↑I
⊢ 1 * y ∈ 1

Proof state:
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDomain A
I : Ideal A
hI : I ≠ ⊥
y : K
hy : y ∈ ↑I
⊢ y ∈ 1

Tactic:
exact FractionalIdeal.coeIdeal_le_one hy

Result:
no goals
-- Mathlib/Algebra/Order/Quantale.lean
theorem sup_mul_distrib : (x ⊔ y) * z = (x * z) ⊔ (y * z)

Proof state:
α : Type u_1
x y z : α
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
⊢ (x ⊔ y) * z = x * z ⊔ y * z

Tactic:
rw [← (@iSup_pair _ _ _ (fun _? => _? * z) _ _), ← sSup_pair, sSup_mul_distrib]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem getElem_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : Array α} (h : ∀ a ∈ l, p a) {i : Nat}
    (hi : i < (pmap f l h).size) :
    (pmap f l h)[i] =
      f (l[i]'(@size_pmap _ _ p f l h ▸ hi))
        (h _ (getElem_mem (@size_pmap _ _ p f l h ▸ hi)))

Proof state:
case mk
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
i : Nat
toList✝ : List α
h : ∀ (a : α), a ∈ { toList := toList✝ } → p a
hi : i < (pmap f { toList := toList✝ } h).size
⊢ (pmap f { toList := toList✝ } h)[i] = f { toList := toList✝ }[i] ⋯

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
l : Array α
h : ∀ (a : α), a ∈ l → p a
i : Nat
hi : i < (pmap f l h).size
⊢ (pmap f l h)[i] = f l[i] ⋯

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
i : Nat
toList✝ : List α
h : ∀ (a : α), a ∈ { toList := toList✝ } → p a
hi : i < (pmap f { toList := toList✝ } h).size
⊢ (pmap f { toList := toList✝ } h)[i] = f { toList := toList✝ }[i] ⋯
-- Mathlib/Algebra/Module/CharacterModule.lean
lemma dual_surjective_iff_injective {f : A →ₗ[R] A'} :
    Function.Surjective (dual f) ↔ Function.Injective f :=
  ⟨fun h ↦ (injective_iff_map_eq_zero _).2 fun a h0 ↦ eq_zero_of_character_apply fun c ↦ by
    obtain ⟨c, rfl⟩ := h c; exact congr(c $h0).trans c.map_zero,
  dual_surjective_of_injective f⟩

Proof state:
R : Type uR
inst✝⁴ : CommRing R
A : Type uA
inst✝³ : AddCommGroup A
A' : Type u_1
inst✝² : AddCommGroup A'
inst✝¹ : Module R A
inst✝ : Module R A'
f : A →ₗ[R] A'
h : Function.Surjective ⇑(dual f)
a : A
h0 : f a = 0
c : CharacterModule A
⊢ c a = 0

Tactic:
obtain ⟨c, rfl⟩ := h c

Result:
case intro
R : Type uR
inst✝⁴ : CommRing R
A : Type uA
inst✝³ : AddCommGroup A
A' : Type u_1
inst✝² : AddCommGroup A'
inst✝¹ : Module R A
inst✝ : Module R A'
f : A →ₗ[R] A'
h : Function.Surjective ⇑(dual f)
a : A
h0 : f a = 0
c : CharacterModule A'
⊢ ((dual f) c) a = 0

Proof state:
case intro
R : Type uR
inst✝⁴ : CommRing R
A : Type uA
inst✝³ : AddCommGroup A
A' : Type u_1
inst✝² : AddCommGroup A'
inst✝¹ : Module R A
inst✝ : Module R A'
f : A →ₗ[R] A'
h : Function.Surjective ⇑(dual f)
a : A
h0 : f a = 0
c : CharacterModule A'
⊢ ((dual f) c) a = 0

Tactic:
exact congr(c $h0).trans c.map_zero

Result:
no goals
-- Mathlib/Logic/Small/Basic.lean
theorem small_of_injective_of_exists {α : Type v} {β : Type w} {γ : Type v'} [Small.{u} α]
    (f : α → γ) {g : β → γ} (hg : Function.Injective g) (h : ∀ b : β, ∃ a : α, f a = g b) :
    Small.{u} β

Proof state:
α : Type v
β : Type w
γ : Type v'
inst✝ : Small.{u, v} α
f : α → γ
g : β → γ
hg : Function.Injective g
h : ∀ (b : β), ∃ a, f a = g b
⊢ Small.{u, w} β

Tactic:
by_cases hβ : Nonempty β

Result:
case pos
α : Type v
β : Type w
γ : Type v'
inst✝ : Small.{u, v} α
f : α → γ
g : β → γ
hg : Function.Injective g
h : ∀ (b : β), ∃ a, f a = g b
hβ : Nonempty β
⊢ Small.{u, w} β

case neg
α : Type v
β : Type w
γ : Type v'
inst✝ : Small.{u, v} α
f : α → γ
g : β → γ
hg : Function.Injective g
h : ∀ (b : β), ∃ a, f a = g b
hβ : ¬Nonempty β
⊢ Small.{u, w} β

Proof state:
case neg
α : Type v
β : Type w
γ : Type v'
inst✝ : Small.{u, v} α
f : α → γ
g : β → γ
hg : Function.Injective g
h : ∀ (b : β), ∃ a, f a = g b
hβ : ¬Nonempty β
⊢ Small.{u, w} β

Tactic:
simp only [not_nonempty_iff] at hβ

Result:
case neg
α : Type v
β : Type w
γ : Type v'
inst✝ : Small.{u, v} α
f : α → γ
g : β → γ
hg : Function.Injective g
h : ∀ (b : β), ∃ a, f a = g b
hβ : IsEmpty β
⊢ Small.{u, w} β

Proof state:
α : Type v
β : Type w
γ : Type v'
inst✝ : Small.{u, v} α
f : α → γ
g : β → γ
hg : Function.Injective g
h : ∀ (b : β), ∃ a, f a = g b
hβ : Nonempty β
b : β
a : α
ha : f a = g b
⊢ (Function.invFun g ∘ f) a = b

Tactic:
rw [Function.comp_apply, ha, Function.leftInverse_invFun hg]

Result:
no goals

Proof state:
case pos.intro
α : Type v
β : Type w
γ : Type v'
inst✝ : Small.{u, v} α
f : α → γ
g : β → γ
hg : Function.Injective g
h : ∀ (b : β), ∃ a, f a = g b
hβ : Nonempty β
b : β
a : α
ha : f a = g b
⊢ ∃ a, (Function.invFun g ∘ f) a = b

Tactic:
exact ⟨a, by rw [Function.comp_apply, ha, Function.leftInverse_invFun hg]⟩

Result:
no goals

Proof state:
case neg
α : Type v
β : Type w
γ : Type v'
inst✝ : Small.{u, v} α
f : α → γ
g : β → γ
hg : Function.Injective g
h : ∀ (b : β), ∃ a, f a = g b
hβ : IsEmpty β
⊢ Small.{u, w} β

Tactic:
infer_instance

Result:
no goals

Proof state:
case pos
α : Type v
β : Type w
γ : Type v'
inst✝ : Small.{u, v} α
f : α → γ
g : β → γ
hg : Function.Injective g
h : ∀ (b : β), ∃ a, f a = g b
hβ : Nonempty β
⊢ Small.{u, w} β

Tactic:
refine small_of_surjective (f := Function.invFun g ∘ f) (fun b => ?_)

Result:
case pos
α : Type v
β : Type w
γ : Type v'
inst✝ : Small.{u, v} α
f : α → γ
g : β → γ
hg : Function.Injective g
h : ∀ (b : β), ∃ a, f a = g b
hβ : Nonempty β
b : β
⊢ ∃ a, (Function.invFun g ∘ f) a = b

Proof state:
case pos
α : Type v
β : Type w
γ : Type v'
inst✝ : Small.{u, v} α
f : α → γ
g : β → γ
hg : Function.Injective g
h : ∀ (b : β), ∃ a, f a = g b
hβ : Nonempty β
b : β
⊢ ∃ a, (Function.invFun g ∘ f) a = b

Tactic:
obtain ⟨a, ha⟩ := h b

Result:
case pos.intro
α : Type v
β : Type w
γ : Type v'
inst✝ : Small.{u, v} α
f : α → γ
g : β → γ
hg : Function.Injective g
h : ∀ (b : β), ∃ a, f a = g b
hβ : Nonempty β
b : β
a : α
ha : f a = g b
⊢ ∃ a, (Function.invFun g ∘ f) a = b
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem mul_left_cancel {n m k : Nat} (np : 0 < n) (h : n * m = n * k) : m = k

Proof state:
n m k : Nat
np : 0 < n
h : n * m = n * k
p : k < m
r : n * k < n * m
⊢ m = k

Tactic:
simp [h] at r

Result:
no goals

Proof state:
n m k : Nat
np : 0 < n
h : n * m = n * k
p : k < m
⊢ m = k

Tactic:
have r : n * k < n * m := Nat.mul_lt_mul_of_pos_left p np

Result:
n m k : Nat
np : 0 < n
h : n * m = n * k
p : k < m
r : n * k < n * m
⊢ m = k

Proof state:
n m k : Nat
np : 0 < n
h : n * m = n * k
⊢ m = k

Tactic:
match Nat.lt_trichotomy m k with
| Or.inl p =>
  have r : n * m < n * k := Nat.mul_lt_mul_of_pos_left p np
  simp [h] at r
| Or.inr (Or.inl p) => exact p
| Or.inr (Or.inr p) =>
  have r : n * k < n * m := Nat.mul_lt_mul_of_pos_left p np
  simp [h] at r

Result:
no goals

Proof state:
n m k : Nat
np : 0 < n
h : n * m = n * k
p : m < k
r : n * m < n * k
⊢ m = k

Tactic:
simp [h] at r

Result:
no goals

Proof state:
n m k : Nat
np : 0 < n
h : n * m = n * k
p : m < k
⊢ m = k

Tactic:
have r : n * m < n * k := Nat.mul_lt_mul_of_pos_left p np

Result:
n m k : Nat
np : 0 < n
h : n * m = n * k
p : m < k
r : n * m < n * k
⊢ m = k

Proof state:
n m k : Nat
np : 0 < n
h : n * m = n * k
p : m = k
⊢ m = k

Tactic:
exact p

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Action/Defs.lean
theorem smul_neg (r : M) (x : A) : r • -x = -(r • x) :=
  eq_neg_of_add_eq_zero_left <| by rw [← smul_add, neg_add_cancel, smul_zero]

Proof state:
M : Type u_1
A : Type u_3
inst✝² : Monoid M
inst✝¹ : AddGroup A
inst✝ : DistribMulAction M A
r : M
x : A
⊢ r • -x + r • x = 0

Tactic:
rw [← smul_add, neg_add_cancel, smul_zero]

Result:
no goals
-- Mathlib/Algebra/CubicDiscriminant.lean
theorem natDegree_of_a_eq_zero (ha : P.a = 0) : P.toPoly.natDegree ≤ 2

Proof state:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
⊢ P.toPoly.natDegree ≤ 2

Tactic:
simpa only [of_a_eq_zero ha] using natDegree_quadratic_le

Result:
no goals
-- Mathlib/Computability/Halting.lean
theorem vec_iff {m n f} : @Vec m n f ↔ Computable f :=
  ⟨fun h => by simpa only [ofFn_get] using vector_ofFn fun i => to_part (h i), fun h i =>
    of_part <| vector_get.comp h (const i)⟩

Proof state:
m n : ℕ
f : List.Vector ℕ m → List.Vector ℕ n
h : Vec f
⊢ Computable f

Tactic:
simpa only [ofFn_get] using vector_ofFn fun i => to_part (h i)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Basic.lean
theorem ofBool_false : ofBool false = 0

Proof state:
⊢ ofBool false = 0

Tactic:
trivial

Result:
no goals