harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Sum/Basic.lean
theorem update_inr_apply_inr [DecidableEq β] [DecidableEq (α ⊕ β)] {f : α ⊕ β → γ} {i j : β}
    {x : γ} : update f (inr i) x (inr j) = update (f ∘ inr) i x j

Proof state:
α : Type u
β : Type v
γ : Type u_1
inst✝¹ : DecidableEq β
inst✝ : DecidableEq (α ⊕ β)
f : α ⊕ β → γ
i j : β
x : γ
⊢ update f (inr i) x (inr j) = update (f ∘ inr) i x j

Tactic:
rw [← update_inr_comp_inr, Function.comp_apply]

Result:
no goals
-- Mathlib/Analysis/Convex/Topology.lean
theorem stdSimplex_subset_closedBall : stdSimplex ℝ ι ⊆ Metric.closedBall 0 1 := fun f hf ↦ by
  rw [Metric.mem_closedBall, dist_pi_le_iff zero_le_one]
  intro x
  rw [Pi.zero_apply, Real.dist_0_eq_abs, abs_of_nonneg <| hf.1 x]
  exact (mem_Icc_of_mem_stdSimplex hf x).2

Proof state:
ι : Type u_1
inst✝ : Fintype ι
f : ι → ℝ
hf : f ∈ stdSimplex ℝ ι
⊢ ∀ (b : ι), dist (f b) (0 b) ≤ 1

Tactic:
intro x

Result:
ι : Type u_1
inst✝ : Fintype ι
f : ι → ℝ
hf : f ∈ stdSimplex ℝ ι
x : ι
⊢ dist (f x) (0 x) ≤ 1

Proof state:
ι : Type u_1
inst✝ : Fintype ι
f : ι → ℝ
hf : f ∈ stdSimplex ℝ ι
x : ι
⊢ dist (f x) (0 x) ≤ 1

Tactic:
rw [Pi.zero_apply, Real.dist_0_eq_abs, abs_of_nonneg <| hf.1 x]

Result:
ι : Type u_1
inst✝ : Fintype ι
f : ι → ℝ
hf : f ∈ stdSimplex ℝ ι
x : ι
⊢ f x ≤ 1

Proof state:
ι : Type u_1
inst✝ : Fintype ι
f : ι → ℝ
hf : f ∈ stdSimplex ℝ ι
x : ι
⊢ f x ≤ 1

Tactic:
exact (mem_Icc_of_mem_stdSimplex hf x).2

Result:
no goals

Proof state:
ι : Type u_1
inst✝ : Fintype ι
f : ι → ℝ
hf : f ∈ stdSimplex ℝ ι
⊢ f ∈ closedBall 0 1

Tactic:
rw [Metric.mem_closedBall, dist_pi_le_iff zero_le_one]

Result:
ι : Type u_1
inst✝ : Fintype ι
f : ι → ℝ
hf : f ∈ stdSimplex ℝ ι
⊢ ∀ (b : ι), dist (f b) (0 b) ≤ 1
-- Mathlib/Analysis/Asymptotics/SuperpolynomialDecay.lean
theorem superpolynomialDecay_param_pow_mul_iff (hk : Tendsto k l atTop) (n : ℕ) :
    SuperpolynomialDecay l k (k ^ n * f) ↔ SuperpolynomialDecay l k f

Proof state:
case zero
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
⊢ SuperpolynomialDecay l k (k ^ 0 * f) ↔ SuperpolynomialDecay l k f

Tactic:
simp

Result:
no goals

Proof state:
case succ
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
n : ℕ
hn : SuperpolynomialDecay l k (k ^ n * f) ↔ SuperpolynomialDecay l k f
⊢ SuperpolynomialDecay l k (k ^ (n + 1) * f) ↔ SuperpolynomialDecay l k f

Tactic:
simpa [pow_succ, ← mul_comm k, mul_assoc,
  superpolynomialDecay_param_mul_iff (k ^ n * f) hk] using hn

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
n : ℕ
⊢ SuperpolynomialDecay l k (k ^ n * f) ↔ SuperpolynomialDecay l k f

Tactic:
induction n with
| zero => simp
| succ n hn =>
  simpa [pow_succ, ← mul_comm k, mul_assoc,
    superpolynomialDecay_param_mul_iff (k ^ n * f) hk] using hn

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem isBigOWith_zero_right_iff : (IsBigOWith c l f'' fun _x => (0 : F')) ↔ f'' =ᶠ[l] 0

Proof state:
α : Type u_1
F' : Type u_7
E'' : Type u_9
inst✝¹ : SeminormedAddCommGroup F'
inst✝ : NormedAddCommGroup E''
c : ℝ
f'' : α → E''
l : Filter α
⊢ (IsBigOWith c l f'' fun _x => 0) ↔ f'' =ᶠ[l] 0

Tactic:
simp only [IsBigOWith_def, exists_prop, norm_zero, mul_zero,
  norm_le_zero_iff, EventuallyEq, Pi.zero_apply]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem card_iUnion_lt_iff_forall_of_isRegular {ι : Type u} {α : Type u} {t : ι → Set α}
    {c : Cardinal} (hc : c.IsRegular) (hι : #ι < c) : #(⋃ i, t i) < c ↔ ∀ i, #(t i) < c

Proof state:
ι α : Type u
t : ι → Set α
c : Cardinal.{u}
hc : c.IsRegular
hι : #ι < c
h : ∀ (i : ι), #↑(t i) < c
⊢ #↑(range fun i => t i) * ⨆ s, #↑↑s < c

Tactic:
apply Cardinal.mul_lt_of_lt hc.aleph0_le
  (lt_of_le_of_lt Cardinal.mk_range_le hι)

Result:
ι α : Type u
t : ι → Set α
c : Cardinal.{u}
hc : c.IsRegular
hι : #ι < c
h : ∀ (i : ι), #↑(t i) < c
⊢ ⨆ s, #↑↑s < c

Proof state:
ι α : Type u
t : ι → Set α
c : Cardinal.{u}
hc : c.IsRegular
hι : #ι < c
h : ∀ (i : ι), #↑(t i) < c
⊢ #↑(⋃ i, t i) < c

Tactic:
apply lt_of_le_of_lt (Cardinal.mk_sUnion_le _)

Result:
ι α : Type u
t : ι → Set α
c : Cardinal.{u}
hc : c.IsRegular
hι : #ι < c
h : ∀ (i : ι), #↑(t i) < c
⊢ #↑(range fun i => t i) * ⨆ s, #↑↑s < c

Proof state:
ι α : Type u
t : ι → Set α
c : Cardinal.{u}
hc : c.IsRegular
hι : #ι < c
⊢ #↑(⋃ i, t i) < c ↔ ∀ (i : ι), #↑(t i) < c

Tactic:
refine ⟨card_lt_of_card_iUnion_lt, fun h ↦ ?_⟩

Result:
ι α : Type u
t : ι → Set α
c : Cardinal.{u}
hc : c.IsRegular
hι : #ι < c
h : ∀ (i : ι), #↑(t i) < c
⊢ #↑(⋃ i, t i) < c

Proof state:
ι α : Type u
t : ι → Set α
c : Cardinal.{u}
hc : c.IsRegular
hι : #ι < c
h : ∀ (i : ι), #↑(t i) < c
⊢ ⨆ s, #↑↑s < c

Tactic:
apply Cardinal.iSup_lt_of_isRegular hc (lt_of_le_of_lt Cardinal.mk_range_le hι)

Result:
ι α : Type u
t : ι → Set α
c : Cardinal.{u}
hc : c.IsRegular
hι : #ι < c
h : ∀ (i : ι), #↑(t i) < c
⊢ ∀ (i : ↑(range fun i => t i)), #↑↑i < c

Proof state:
ι α : Type u
t : ι → Set α
c : Cardinal.{u}
hc : c.IsRegular
hι : #ι < c
h : ∀ (i : ι), #↑(t i) < c
⊢ ∀ (i : ↑(range fun i => t i)), #↑↑i < c

Tactic:
simpa

Result:
no goals
-- Mathlib/Topology/VectorBundle/Basic.lean
theorem linearMapAt_apply (e : Trivialization F (π F E)) [e.IsLinear R] {b : B} (y : E b) :
    e.linearMapAt R b y = if b ∈ e.baseSet then (e ⟨b, y⟩).2 else 0

Proof state:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst✝⁸ : Semiring R
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace (TotalSpace F E)
inst✝⁴ : AddCommMonoid F
inst✝³ : Module R F
inst✝² : (x : B) → AddCommMonoid (E x)
inst✝¹ : (x : B) → Module R (E x)
e : Trivialization F TotalSpace.proj
inst✝ : Trivialization.IsLinear R e
b : B
y : E b
⊢ (Trivialization.linearMapAt R e b) y = if b ∈ e.baseSet then (↑e { proj := b, snd := y }).2 else 0

Tactic:
rw [coe_linearMapAt]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem contains_insert_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β k} :
    (m.insert k v).contains k

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k : α
v : β k
⊢ (m.insert k v).contains k = true

Tactic:
simp_to_raw using Raw₀.contains_insert_self

Result:
no goals
-- Mathlib/Analysis/SumIntegralComparisons.lean
theorem MonotoneOn.integral_le_sum (hf : MonotoneOn f (Icc x₀ (x₀ + a))) :
    (∫ x in x₀..x₀ + a, f x) ≤ ∑ i ∈ Finset.range a, f (x₀ + (i + 1 : ℕ))

Proof state:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : MonotoneOn f (Icc x₀ (x₀ + ↑a))
⊢ ∑ x ∈ Finset.range a, -f (x₀ + ↑(x + 1)) ≤ ∫ (x : ℝ) in x₀..x₀ + ↑a, -f x

Tactic:
exact hf.neg.sum_le_integral

Result:
no goals

Proof state:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : MonotoneOn f (Icc x₀ (x₀ + ↑a))
⊢ ∫ (x : ℝ) in x₀..x₀ + ↑a, f x ≤ ∑ i ∈ Finset.range a, f (x₀ + ↑(i + 1))

Tactic:
rw [← neg_le_neg_iff, ← Finset.sum_neg_distrib, ← intervalIntegral.integral_neg]

Result:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : MonotoneOn f (Icc x₀ (x₀ + ↑a))
⊢ ∑ x ∈ Finset.range a, -f (x₀ + ↑(x + 1)) ≤ ∫ (x : ℝ) in x₀..x₀ + ↑a, -f x
-- Mathlib/SetTheory/Ordinal/Exponential.lean
theorem log_eq_zero {b o : Ordinal} (hbo : o < b) : log b o = 0

Proof state:
case inl
b : Ordinal.{u_1}
hbo : 0 < b
⊢ log b 0 = 0

Tactic:
exact log_zero_right b

Result:
no goals

Proof state:
b o : Ordinal.{u_1}
hbo : o < b
⊢ log b o = 0

Tactic:
rcases eq_or_ne o 0 with (rfl | ho)

Result:
case inl
b : Ordinal.{u_1}
hbo : 0 < b
⊢ log b 0 = 0

case inr
b o : Ordinal.{u_1}
hbo : o < b
ho : o ≠ 0
⊢ log b o = 0

Proof state:
case inr.inl.inr
o : Ordinal.{u_1}
ho : o ≠ 0
hbo : o < 1
hb : 1 ≤ 1
⊢ log 1 o = 0

Tactic:
exact log_one_left o

Result:
no goals

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

Tactic:
rcases le_one_iff.1 hb with (rfl | rfl)

Result:
case inr.inl.inl
o : Ordinal.{u_1}
ho : o ≠ 0
hbo : o < 0
hb : 0 ≤ 1
⊢ log 0 o = 0

case inr.inl.inr
o : Ordinal.{u_1}
ho : o ≠ 0
hbo : o < 1
hb : 1 ≤ 1
⊢ log 1 o = 0

Proof state:
case inr
b o : Ordinal.{u_1}
hbo : o < b
ho : o ≠ 0
⊢ log b o = 0

Tactic:
rcases le_or_lt b 1 with hb | hb

Result:
case inr.inl
b o : Ordinal.{u_1}
hbo : o < b
ho : o ≠ 0
hb : b ≤ 1
⊢ log b o = 0

case inr.inr
b o : Ordinal.{u_1}
hbo : o < b
ho : o ≠ 0
hb : 1 < b
⊢ log b o = 0

Proof state:
case inr.inl.inl
o : Ordinal.{u_1}
ho : o ≠ 0
hbo : o < 0
hb : 0 ≤ 1
⊢ log 0 o = 0

Tactic:
exact log_zero_left o

Result:
no goals

Proof state:
case inr.inr
b o : Ordinal.{u_1}
hbo : o < b
ho : o ≠ 0
hb : 1 < b
⊢ log b o = 0

Tactic:
rwa [← Ordinal.le_zero, ← lt_succ_iff, succ_zero, ← lt_opow_iff_log_lt hb ho, opow_one]

Result:
no goals
-- Mathlib/Data/Set/Finite/Basic.lean
theorem toFinset_setOf [Fintype α] (p : α → Prop) [DecidablePred p]
    (h : { x | p x }.Finite) : h.toFinset = Finset.univ.filter p

Proof state:
α : Type u
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
h : {x | p x}.Finite
⊢ h.toFinset = Finset.filter p Finset.univ

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/RCLike/Inner.lean
@[simp] lemma wInner_zero_right (w : ι → ℝ) (f : ∀ i, E i) : ⟪f, 0⟫_[𝕜, w] = 0

Proof state:
ι : Type u_1
𝕜 : Type u_3
E : ι → Type u_4
inst✝³ : Fintype ι
inst✝² : RCLike 𝕜
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (E i)
w : ι → ℝ
f : (i : ι) → E i
⊢ wInner w f 0 = 0

Tactic:
simp [wInner]

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem IsClosed.inter (h₁ : IsClosed s₁) (h₂ : IsClosed s₂) : IsClosed (s₁ ∩ s₂)

Proof state:
X : Type u
s₁ s₂ : Set X
inst✝ : TopologicalSpace X
h₁ : IsOpen s₁ᶜ
h₂ : IsOpen s₂ᶜ
⊢ IsOpen (s₁ᶜ ∪ s₂ᶜ)

Tactic:
exact IsOpen.union h₁ h₂

Result:
no goals

Proof state:
X : Type u
s₁ s₂ : Set X
inst✝ : TopologicalSpace X
h₁ : IsOpen s₁ᶜ
h₂ : IsOpen s₂ᶜ
⊢ IsOpen (s₁ ∩ s₂)ᶜ

Tactic:
rw [compl_inter]

Result:
X : Type u
s₁ s₂ : Set X
inst✝ : TopologicalSpace X
h₁ : IsOpen s₁ᶜ
h₂ : IsOpen s₂ᶜ
⊢ IsOpen (s₁ᶜ ∪ s₂ᶜ)

Proof state:
X : Type u
s₁ s₂ : Set X
inst✝ : TopologicalSpace X
h₁ : IsClosed s₁
h₂ : IsClosed s₂
⊢ IsClosed (s₁ ∩ s₂)

Tactic:
rw [← isOpen_compl_iff] at *

Result:
X : Type u
s₁ s₂ : Set X
inst✝ : TopologicalSpace X
h₁ : IsOpen s₁ᶜ
h₂ : IsOpen s₂ᶜ
⊢ IsOpen (s₁ ∩ s₂)ᶜ
-- Mathlib/Probability/Kernel/Disintegration/CDFToKernel.lean
lemma IsRatCondKernelCDF.tendsto_atTop_one (hf : IsRatCondKernelCDF f κ ν) (a : α) :
    ∀ᵐ b ∂(ν a), Tendsto (f (a, b)) atTop (𝓝 1)

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDF f κ ν
a : α
⊢ ∀ᵐ (b : β) ∂ν a, Tendsto (f (a, b)) atTop (𝓝 1)

Tactic:
filter_upwards [hf.isRatStieltjesPoint_ae a] with b hb using hb.tendsto_atTop_one

Result:
no goals
-- Mathlib/AlgebraicGeometry/AffineScheme.lean
@[reassoc]
lemma Spec_map_appLE_fromSpec (f : X ⟶ Y) {V : X.Opens} {U : Y.Opens}
    (hU : IsAffineOpen U) (hV : IsAffineOpen V) (i : V ≤ f ⁻¹ᵁ U) :
    Spec.map (f.appLE U V i) ≫ hU.fromSpec = hV.fromSpec ≫ f

Proof state:
X Y : Scheme
f : X ⟶ Y
V : X.Opens
U : Y.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
i : V ≤ f ⁻¹ᵁ U
this : IsAffine ↑U
⊢ Spec.map (Scheme.Hom.appLE f U V i) ≫ Spec.map (Y.presheaf.map (eqToHom ⋯).op) ≫ (↑U).isoSpec.inv ≫ U.ι =
    Spec.map (X.presheaf.map (eqToHom ⋯).op) ≫ (↑V).isoSpec.inv ≫ (X.homOfLE i ≫ (f ⁻¹ᵁ U).ι) ≫ f

Tactic:
rw [Category.assoc, ← morphismRestrict_ι,
  ← Category.assoc _ (f ∣_ U) U.ι, ← @Scheme.isoSpec_inv_naturality_assoc,
  ← Spec.map_comp_assoc, ← Spec.map_comp_assoc, Scheme.comp_appTop, morphismRestrict_appTop,
  Scheme.homOfLE_appTop, Scheme.Hom.app_eq_appLE, Scheme.Hom.appLE_map,
  Scheme.Hom.appLE_map, Scheme.Hom.appLE_map, Scheme.Hom.map_appLE]

Result:
no goals

Proof state:
X Y : Scheme
f : X ⟶ Y
V : X.Opens
U : Y.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
i : V ≤ f ⁻¹ᵁ U
⊢ Spec.map (Scheme.Hom.appLE f U V i) ≫ hU.fromSpec = hV.fromSpec ≫ f

Tactic:
have : IsAffine U := hU

Result:
X Y : Scheme
f : X ⟶ Y
V : X.Opens
U : Y.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
i : V ≤ f ⁻¹ᵁ U
this : IsAffine ↑U
⊢ Spec.map (Scheme.Hom.appLE f U V i) ≫ hU.fromSpec = hV.fromSpec ≫ f

Proof state:
X Y : Scheme
f : X ⟶ Y
V : X.Opens
U : Y.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
i : V ≤ f ⁻¹ᵁ U
this : IsAffine ↑U
⊢ Spec.map (Scheme.Hom.appLE f U V i) ≫ hU.fromSpec = hV.fromSpec ≫ f

Tactic:
simp only [IsAffineOpen.fromSpec, Category.assoc, isoSpec_inv]

Result:
X Y : Scheme
f : X ⟶ Y
V : X.Opens
U : Y.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
i : V ≤ f ⁻¹ᵁ U
this : IsAffine ↑U
⊢ Spec.map (Scheme.Hom.appLE f U V i) ≫ Spec.map (Y.presheaf.map (eqToHom ⋯).op) ≫ (↑U).isoSpec.inv ≫ U.ι =
    Spec.map (X.presheaf.map (eqToHom ⋯).op) ≫ (↑V).isoSpec.inv ≫ V.ι ≫ f

Proof state:
X Y : Scheme
f : X ⟶ Y
V : X.Opens
U : Y.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
i : V ≤ f ⁻¹ᵁ U
this : IsAffine ↑U
⊢ Spec.map (Scheme.Hom.appLE f U V i) ≫ Spec.map (Y.presheaf.map (eqToHom ⋯).op) ≫ (↑U).isoSpec.inv ≫ U.ι =
    Spec.map (X.presheaf.map (eqToHom ⋯).op) ≫ (↑V).isoSpec.inv ≫ V.ι ≫ f

Tactic:
simp_rw [← Scheme.homOfLE_ι _ i]

Result:
X Y : Scheme
f : X ⟶ Y
V : X.Opens
U : Y.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
i : V ≤ f ⁻¹ᵁ U
this : IsAffine ↑U
⊢ Spec.map (Scheme.Hom.appLE f U V i) ≫ Spec.map (Y.presheaf.map (eqToHom ⋯).op) ≫ (↑U).isoSpec.inv ≫ U.ι =
    Spec.map (X.presheaf.map (eqToHom ⋯).op) ≫ (↑V).isoSpec.inv ≫ (X.homOfLE i ≫ (f ⁻¹ᵁ U).ι) ≫ f
-- Mathlib/Algebra/DirectSum/Internal.lean
theorem coe_of_mul_apply_of_le {i : ι} (r : A i) (r' : ⨁ i, A i) (n : ι) (h : i ≤ n) :
    ((of (fun i => A i) i r * r') n : R) = r * r' (n - i) :=
  coe_of_mul_apply_aux _ _ _ fun x => by rw [eq_tsub_iff_add_eq_of_le h, add_comm]

Proof state:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝¹⁰ : DecidableEq ι
inst✝⁹ : Semiring R
inst✝⁸ : SetLike σ R
inst✝⁷ : AddSubmonoidClass σ R
A : ι → σ
inst✝⁶ : AddCommMonoid ι
inst✝⁵ : PartialOrder ι
inst✝⁴ : CanonicallyOrderedAdd ι
inst✝³ : SetLike.GradedMonoid A
inst✝² : Sub ι
inst✝¹ : OrderedSub ι
inst✝ : AddLeftReflectLE ι
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
n : ι
h : i ≤ n
x : ι
⊢ i + x = n ↔ x = n - i

Tactic:
rw [eq_tsub_iff_add_eq_of_le h, add_comm]

Result:
no goals
-- Mathlib/CategoryTheory/Comma/StructuredArrow/Basic.lean
theorem existsUnique (h : IsUniversal f) (g : StructuredArrow S T) :
    ∃! η : f.right ⟶ g.right, f.hom ≫ T.map η = g.hom :=
  ⟨h.desc g, h.fac g, fun f w ↦ h.hom_ext <| by simp [w]⟩

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : D
T : C ⥤ D
f✝ : StructuredArrow S T
h : f✝.IsUniversal
g : StructuredArrow S T
f : f✝.right ⟶ g.right
w : (fun η => f✝.hom ≫ T.map η = g.hom) f
⊢ f✝.hom ≫ T.map f = f✝.hom ≫ T.map (h.desc g)

Tactic:
simp [w]

Result:
no goals
-- Mathlib/Logic/Equiv/Set.lean
theorem image_symm_preimage {α β} {f : α → β} (hf : Injective f) (u s : Set α) :
    (fun x => (Set.image f s hf).symm x : f '' s → α) ⁻¹' u = Subtype.val ⁻¹' (f '' u)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
u s : Set α
⊢ (fun x => ↑((Set.image f s hf).symm x)) ⁻¹' u = Subtype.val ⁻¹' (f '' u)

Tactic:
ext ⟨b, a, has, rfl⟩

Result:
case h.mk.intro.intro
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
u s : Set α
a : α
has : a ∈ s
⊢ ⟨f a, ⋯⟩ ∈ (fun x => ↑((Set.image f s hf).symm x)) ⁻¹' u ↔ ⟨f a, ⋯⟩ ∈ Subtype.val ⁻¹' (f '' u)

Proof state:
case h.mk.intro.intro
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
u s : Set α
a : α
has : a ∈ s
⊢ ⟨f a, ⋯⟩ ∈ (fun x => ↑((Set.image f s hf).symm x)) ⁻¹' u ↔ ⟨f a, ⋯⟩ ∈ Subtype.val ⁻¹' (f '' u)

Tactic:
simp [hf.eq_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getElem_signExtend {x  : BitVec w} {v i : Nat} (h : i < v) :
    (x.signExtend v)[i] = if i < w then x.getLsbD i else x.msb

Proof state:
w : Nat
x : BitVec w
v i : Nat
h : i < v
⊢ (signExtend v x)[i] = if i < w then x.getLsbD i else x.msb

Tactic:
rw [←getLsbD_eq_getElem, getLsbD_signExtend]

Result:
w : Nat
x : BitVec w
v i : Nat
h : i < v
⊢ (decide (i < v) && if i < w then x.getLsbD i else x.msb) = if i < w then x.getLsbD i else x.msb

Proof state:
w : Nat
x : BitVec w
v i : Nat
h : i < v
⊢ (decide (i < v) && if i < w then x.getLsbD i else x.msb) = if i < w then x.getLsbD i else x.msb

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Algebra/Algebra/Operations.lean
theorem one_eq_range : (1 : Submodule R A) = LinearMap.range (Algebra.linearMap R A)

Proof state:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ 1 = LinearMap.range (Algebra.linearMap R A)

Tactic:
rw [one_eq_span, LinearMap.span_singleton_eq_range,
  LinearMap.toSpanSingleton_eq_algebra_linearMap]

Result:
no goals
-- Mathlib/Algebra/Category/Ring/Under/Basic.lean
@[reassoc (attr := simp)]
lemma pushout_inl_tensorProdObjIsoPushoutObj_inv_right (A : Under R) :
    pushout.inl A.hom (ofHom <| algebraMap R S) ≫ (tensorProdObjIsoPushoutObj S A).inv.right =
      (ofHom <| Algebra.TensorProduct.includeRight.toRingHom)

Proof state:
R S : CommRingCat
inst✝ : Algebra ↑R ↑S
A : Under R
⊢ pushout.inl A.hom (ofHom (algebraMap ↑R ↑S)) ≫ (tensorProdObjIsoPushoutObj S A).inv.right =
    ofHom Algebra.TensorProduct.includeRight.toRingHom

Tactic:
simp [tensorProdObjIsoPushoutObj]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Div.lean
theorem exists_eq_pow_rootMultiplicity_mul_and_not_dvd (p : R[X]) (hp : p ≠ 0) (a : R) :
    ∃ q : R[X], p = (X - C a) ^ p.rootMultiplicity a * q ∧ ¬ (X - C a) ∣ q

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
hp : p ≠ 0
a : R
⊢ ∃ q, p = (X - C a) ^ rootMultiplicity a p * q ∧ ¬X - C a ∣ q

Tactic:
rw [rootMultiplicity_eq_multiplicity, if_neg hp]

Result:
R : Type u
inst✝ : Ring R
p : R[X]
hp : p ≠ 0
a : R
⊢ ∃ q, p = (X - C a) ^ multiplicity (X - C a) p * q ∧ ¬X - C a ∣ q

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
hp : p ≠ 0
a : R
⊢ ∃ q, p = (X - C a) ^ multiplicity (X - C a) p * q ∧ ¬X - C a ∣ q

Tactic:
apply (finiteMultiplicity_X_sub_C a hp).exists_eq_pow_mul_and_not_dvd

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
hp : p ≠ 0
a : R
⊢ ∃ q, p = (X - C a) ^ rootMultiplicity a p * q ∧ ¬X - C a ∣ q

Tactic:
classical
rw [rootMultiplicity_eq_multiplicity, if_neg hp]
apply (finiteMultiplicity_X_sub_C a hp).exists_eq_pow_mul_and_not_dvd

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/TwoDim.lean
theorem areaForm_comp_rightAngleRotation (x y : E) : ω (J x) (J y) = ω x y

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ (o.areaForm (o.rightAngleRotation x)) (o.rightAngleRotation y) = (o.areaForm x) y

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Polynomial/ScaleRoots.lean
lemma scaleRoots_dvd (p q : R[X]) {r : R} [NoZeroDivisors R] (hpq : p ∣ q) :
    p.scaleRoots r ∣ q.scaleRoots r

Proof state:
case intro
R : Type u_1
inst✝¹ : CommSemiring R
p : R[X]
r : R
inst✝ : NoZeroDivisors R
a : R[X]
⊢ p.scaleRoots r ∣ p.scaleRoots r * a.scaleRoots r

Tactic:
exact dvd_mul_right (scaleRoots p r) (scaleRoots a r)

Result:
no goals

Proof state:
case intro
R : Type u_1
inst✝¹ : CommSemiring R
p : R[X]
r : R
inst✝ : NoZeroDivisors R
a : R[X]
⊢ p.scaleRoots r ∣ (p * a).scaleRoots r

Tactic:
rw [mul_scaleRoots_of_noZeroDivisors]

Result:
case intro
R : Type u_1
inst✝¹ : CommSemiring R
p : R[X]
r : R
inst✝ : NoZeroDivisors R
a : R[X]
⊢ p.scaleRoots r ∣ p.scaleRoots r * a.scaleRoots r

Proof state:
R : Type u_1
inst✝¹ : CommSemiring R
p q : R[X]
r : R
inst✝ : NoZeroDivisors R
hpq : p ∣ q
⊢ p.scaleRoots r ∣ q.scaleRoots r

Tactic:
obtain ⟨a, rfl⟩ := hpq

Result:
case intro
R : Type u_1
inst✝¹ : CommSemiring R
p : R[X]
r : R
inst✝ : NoZeroDivisors R
a : R[X]
⊢ p.scaleRoots r ∣ (p * a).scaleRoots r
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
lemma map_negAddY :
    (W'.map f).toAffine.negAddY (f x₁) (f x₂) (f y₁) (f ℓ) = f (W'.negAddY x₁ x₂ y₁ ℓ)

Proof state:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Affine R
f : R →+* S
x₁ y₁ x₂ ℓ : R
⊢ (map W' f).toAffine.negAddY (f x₁) (f x₂) (f y₁) (f ℓ) = f (W'.negAddY x₁ x₂ y₁ ℓ)

Tactic:
simp only [negAddY, map_addX]

Result:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Affine R
f : R →+* S
x₁ y₁ x₂ ℓ : R
⊢ f ℓ * (f (W'.addX x₁ x₂ ℓ) - f x₁) + f y₁ = f (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁)

Proof state:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Affine R
f : R →+* S
x₁ y₁ x₂ ℓ : R
⊢ f ℓ * (f (W'.addX x₁ x₂ ℓ) - f x₁) + f y₁ = f (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁)

Tactic:
map_simp

Result:
no goals
-- Mathlib/Data/Multiset/UnionInter.lean
lemma add_eq_union_right_of_le [DecidableEq α] {x y z : Multiset α} (h : z ≤ y) :
    x + y = x ∪ z ↔ y = z ∧ Disjoint x y

Proof state:
α : Type u_1
inst✝ : DecidableEq α
x y z : Multiset α
h : z ≤ y
⊢ x + y = x ∪ z ↔ y = z ∧ _root_.Disjoint x y

Tactic:
simpa only [and_comm] using add_eq_union_left_of_le h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Count.lean
theorem count_push_self (a : α) (l : Vector α n) : count a (l.push a) = count a l + 1

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
n : Nat
a : α
l : Vector α n
⊢ count a (l.push a) = count a l + 1

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : Array α
⊢ count a ({ toArray := l, size_toArray := ⋯ }.push a) = count a { toArray := l, size_toArray := ⋯ } + 1

Proof state:
case mk
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : Array α
⊢ count a ({ toArray := l, size_toArray := ⋯ }.push a) = count a { toArray := l, size_toArray := ⋯ } + 1

Tactic:
simp [Array.count_push_self]

Result:
no goals
-- Mathlib/Algebra/GCDMonoid/Multiset.lean
theorem dvd_gcd {s : Multiset α} {a : α} : a ∣ s.gcd ↔ ∀ b ∈ s, a ∣ b :=
  Multiset.induction_on s (by simp)
    (by simp +contextual [or_imp, forall_and, dvd_gcd_iff])

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
a : α
⊢ ∀ (a_1 : α) (s : Multiset α), (a ∣ s.gcd ↔ ∀ b ∈ s, a ∣ b) → (a ∣ (a_1 ::ₘ s).gcd ↔ ∀ b ∈ a_1 ::ₘ s, a ∣ b)

Tactic:
simp +contextual [or_imp, forall_and, dvd_gcd_iff]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
a : α
⊢ a ∣ gcd 0 ↔ ∀ b ∈ 0, a ∣ b

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicTopology/DoldKan/Projections.lean
theorem Q_idem (q : ℕ) : (Q q : K[X] ⟶ K[X]) ≫ Q q = Q q

Proof state:
case h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
⊢ (Q q ≫ Q q).f n = (Q q).f n

Tactic:
exact Q_f_idem q n

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ Q q ≫ Q q = Q q

Tactic:
ext n

Result:
case h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
⊢ (Q q ≫ Q q).f n = (Q q).f n
-- Mathlib/Data/Fintype/Card.lean
theorem card_congr' {α β} [Fintype α] [Fintype β] (h : α = β) : card α = card β :=
  card_congr (by rw [h])

Proof state:
α β : Type u_4
inst✝¹ : Fintype α
inst✝ : Fintype β
h : α = β
⊢ α ≃ β

Tactic:
rw [h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem all_bne [BEq α] {xs : Vector α n} : (xs.all fun x => a != x) = !xs.contains a

Proof state:
case mk
α : Type u_1
a : α
inst✝ : BEq α
xs : Array α
⊢ ({ toArray := xs, size_toArray := ⋯ }.all fun x => a != x) = !{ toArray := xs, size_toArray := ⋯ }.contains a

Tactic:
simp [Array.all_bne]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
a : α
inst✝ : BEq α
xs : Vector α n
⊢ (xs.all fun x => a != x) = !xs.contains a

Tactic:
rcases xs with ⟨xs, rfl⟩

Result:
case mk
α : Type u_1
a : α
inst✝ : BEq α
xs : Array α
⊢ ({ toArray := xs, size_toArray := ⋯ }.all fun x => a != x) = !{ toArray := xs, size_toArray := ⋯ }.contains a