harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Normed/Lp/lpSpace.lean
theorem _root_.one_memℓp_infty : Memℓp (1 : ∀ i, B i) ∞ :=
  ⟨1, by rintro i ⟨i, rfl⟩; exact norm_one.le⟩

Proof state:
I : Type u_5
B : I → Type u_6
inst✝¹ : (i : I) → NormedRing (B i)
inst✝ : ∀ (i : I), NormOneClass (B i)
⊢ 1 ∈ upperBounds (Set.range fun i => ‖1 i‖)

Tactic:
rintro i ⟨i, rfl⟩

Result:
case intro
I : Type u_5
B : I → Type u_6
inst✝¹ : (i : I) → NormedRing (B i)
inst✝ : ∀ (i : I), NormOneClass (B i)
i : I
⊢ (fun i => ‖1 i‖) i ≤ 1

Proof state:
case intro
I : Type u_5
B : I → Type u_6
inst✝¹ : (i : I) → NormedRing (B i)
inst✝ : ∀ (i : I), NormOneClass (B i)
i : I
⊢ (fun i => ‖1 i‖) i ≤ 1

Tactic:
exact norm_one.le

Result:
no goals
-- Mathlib/MeasureTheory/Measure/WithDensity.lean
theorem restrict_withDensity {s : Set α} (hs : MeasurableSet s) (f : α → ℝ≥0∞) :
    (μ.withDensity f).restrict s = (μ.restrict s).withDensity f

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
⊢ (μ.withDensity f).restrict s = (μ.restrict s).withDensity f

Tactic:
ext1 t ht

Result:
case h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
t : Set α
ht : MeasurableSet t
⊢ ((μ.withDensity f).restrict s) t = ((μ.restrict s).withDensity f) t

Proof state:
case h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
t : Set α
ht : MeasurableSet t
⊢ ((μ.withDensity f).restrict s) t = ((μ.restrict s).withDensity f) t

Tactic:
rw [restrict_apply ht, withDensity_apply _ ht, withDensity_apply _ (ht.inter hs),
  restrict_restrict ht]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Opposites.lean
theorem unop_fst {X Y Z : Cᵒᵖ} {f : X ⟶ Y} {g : X ⟶ Z} (c : PushoutCocone f g) :
    c.unop.fst = c.inl.unop

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
⊢ c.unop.fst = c.inl.unop

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Maps/Basic.lean
lemma IsOpenEmbedding.isOpen_iff_preimage_isOpen (hf : IsOpenEmbedding f) {s : Set Y}
    (hs : s ⊆ range f) : IsOpen s ↔ IsOpen (f ⁻¹' s)

Proof state:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsOpenEmbedding f
s : Set Y
hs : s ⊆ range f
⊢ IsOpen s ↔ IsOpen (f ⁻¹' s)

Tactic:
rw [hf.isOpen_iff_image_isOpen, image_preimage_eq_inter_range, inter_eq_self_of_subset_left hs]

Result:
no goals
-- Mathlib/ModelTheory/Equivalence.lean
theorem all {φ ψ : L.BoundedFormula α (n + 1)}
    (h : φ ⇔[T] ψ) : φ.all ⇔[T] ψ.all

Proof state:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α (n + 1)
h : φ ⇔[T] ψ
⊢ ∀ (M : T.ModelType) (v : α → ↑M) (xs : Fin n → ↑M),
    (∀ (a : ↑M), φ.Realize v (Fin.snoc xs a)) ↔ ∀ (a : ↑M), ψ.Realize v (Fin.snoc xs a)

Tactic:
exact fun M v xs => forall_congr' fun a => h.realize_bd_iff

Result:
no goals

Proof state:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α (n + 1)
h : φ ⇔[T] ψ
⊢ ∀'φ ⇔[T] ∀'ψ

Tactic:
simp_rw [Theory.Iff, ModelsBoundedFormula, BoundedFormula.realize_iff,
  BoundedFormula.realize_all]

Result:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α (n + 1)
h : φ ⇔[T] ψ
⊢ ∀ (M : T.ModelType) (v : α → ↑M) (xs : Fin n → ↑M),
    (∀ (a : ↑M), φ.Realize v (Fin.snoc xs a)) ↔ ∀ (a : ↑M), ψ.Realize v (Fin.snoc xs a)
-- Mathlib/Algebra/Order/Interval/Multiset.lean
lemma map_add_left_Icc (a b c : α) : (Icc a b).map (c + ·) = Icc (c + a) (c + b)

Proof state:
α : Type u_1
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x => c + x) (Icc a b) = Icc (c + a) (c + b)

Tactic:
rw [Icc, Icc, ← Finset.image_add_left_Icc, Finset.image_val,
((Finset.nodup _).map <| add_right_injective c).dedup]

Result:
no goals

Proof state:
α : Type u_1
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x => c + x) (Icc a b) = Icc (c + a) (c + b)

Tactic:
classical rw [Icc, Icc, ← Finset.image_add_left_Icc, Finset.image_val,
    ((Finset.nodup _).map <| add_right_injective c).dedup]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Mul.lean
theorem DifferentiableAt.finset_prod (hd : ∀ i ∈ u, DifferentiableAt 𝕜 (f i) x) :
    DifferentiableAt 𝕜 (∏ i ∈ u, f i ·) x

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_2
𝔸' : Type u_3
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
hd : ∀ i ∈ u, DifferentiableAt 𝕜 (f i) x
⊢ DifferentiableAt 𝕜 (fun x => ∏ i ∈ u, f i x) x

Tactic:
classical
exact
  (HasDerivAt.finset_prod (fun i hi ↦ DifferentiableAt.hasDerivAt (hd i hi))).differentiableAt

Result:
no goals

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_2
𝔸' : Type u_3
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
hd : ∀ i ∈ u, DifferentiableAt 𝕜 (f i) x
⊢ DifferentiableAt 𝕜 (fun x => ∏ i ∈ u, f i x) x

Tactic:
exact
  (HasDerivAt.finset_prod (fun i hi ↦ DifferentiableAt.hasDerivAt (hd i hi))).differentiableAt

Result:
no goals
-- Mathlib/Analysis/Normed/Lp/lpSpace.lean
theorem coeFn_sum {ι : Type*} (f : ι → lp E p) (s : Finset ι) :
    ⇑(∑ i ∈ s, f i) = ∑ i ∈ s, ⇑(f i)

Proof state:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
f : ι → ↥(lp E p)
s : Finset ι
⊢ ↑(∑ i ∈ s, f i) = ∑ i ∈ s, ↑(f i)

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Function/EssSup.lean
theorem essSup_indicator_eq_essSup_restrict {s : Set α} {f : α → ℝ≥0∞} (hs : MeasurableSet s) :
    essSup (s.indicator f) μ = essSup f (μ.restrict s)

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hs : MeasurableSet s
⊢ essSup (s.indicator f) μ = essSup f (μ.restrict s)

Tactic:
simp only [← piecewise_eq_indicator, essSup_piecewise hs, max_eq_left_iff]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hs : MeasurableSet s
⊢ essSup 0 (μ.restrict sᶜ) ≤ essSup f (μ.restrict s)

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hs : MeasurableSet s
⊢ essSup 0 (μ.restrict sᶜ) ≤ essSup f (μ.restrict s)

Tactic:
exact limsup_const_bot.trans_le (zero_le _)

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hs : MeasurableSet s
⊢ essSup (s.indicator f) μ = essSup f (μ.restrict s)

Tactic:
classical
simp only [← piecewise_eq_indicator, essSup_piecewise hs, max_eq_left_iff]
exact limsup_const_bot.trans_le (zero_le _)

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem surjOn_cos : SurjOn cos (Icc 0 π) (Icc (-1) 1)

Proof state:
⊢ SurjOn cos (Icc 0 π) (Icc (-1) 1)

Tactic:
simpa only [cos_zero, cos_pi] using intermediate_value_Icc' pi_pos.le continuous_cos.continuousOn

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma baseChange_dblY (P : Fin 3 → A) : (W'.baseChange B).toJacobian.dblY (f ∘ P) =
    f ((W'.baseChange A).toJacobian.dblY P)

Proof state:
R : Type r
inst✝¹⁰ : CommRing R
W' : Jacobian R
S : Type s
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
A : Type u
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
B : Type v
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
⊢ (baseChange W' B).toJacobian.dblY (⇑f ∘ P) = f ((baseChange W' A).toJacobian.dblY P)

Tactic:
rw [← RingHom.coe_coe, ← map_dblY, map_baseChange]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem containsKey_of_beq [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a b : α}
    (hla : containsKey a l) (hab : a == b) : containsKey b l

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
a b : α
hla : containsKey a l = true
hab : (a == b) = true
⊢ containsKey b l = true

Tactic:
rwa [← containsKey_congr hab]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem subNatNat_add_right : subNatNat m (m + n + 1) = negSucc n

Proof state:
m n : Nat
⊢ subNatNat m (m + n + 1) = -[n+1]

Tactic:
simp [subNatNat, Nat.add_assoc, Nat.add_sub_cancel_left]

Result:
no goals
-- Mathlib/Probability/Kernel/Integral.lean
theorem integral_restrict (hs : MeasurableSet s) :
    ∫ x, f x ∂κ.restrict hs a = ∫ x in s, f x ∂κ a

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : β → E
a : α
s : Set β
hs : MeasurableSet s
⊢ ∫ (x : β), f x ∂(κ.restrict hs) a = ∫ (x : β) in s, f x ∂κ a

Tactic:
rw [restrict_apply]

Result:
no goals
-- Mathlib/Data/Int/ModEq.lean
theorem modEq_zero_iff_dvd : a ≡ 0 [ZMOD n] ↔ n ∣ a

Proof state:
n a : ℤ
⊢ a ≡ 0 [ZMOD n] ↔ n ∣ a

Tactic:
rw [ModEq, zero_emod, dvd_iff_emod_eq_zero]

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Lemmas.lean
theorem union_empty (s : Finset α) : s ∪ ∅ = s :=
  ext fun x => mem_union.trans <| by simp

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x : α
⊢ x ∈ s ∨ x ∈ ∅ ↔ x ∈ s

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Homology/QuasiIso.lean
lemma quasiIso_of_comp_left (φ : K ⟶ L) (φ' : L ⟶ M) [∀ i, K.HasHomology i]
    [∀ i, L.HasHomology i] [∀ i, M.HasHomology i]
    [hφ : QuasiIso φ] [hφφ' : QuasiIso (φ ≫ φ')] :
    QuasiIso φ'

Proof state:
ι : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
inst✝² : ∀ (i : ι), K.HasHomology i
inst✝¹ : ∀ (i : ι), L.HasHomology i
inst✝ : ∀ (i : ι), M.HasHomology i
hφ : QuasiIso φ
hφφ' : QuasiIso (φ ≫ φ')
⊢ QuasiIso φ'

Tactic:
rw [← quasiIso_iff_comp_left φ φ']

Result:
ι : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
inst✝² : ∀ (i : ι), K.HasHomology i
inst✝¹ : ∀ (i : ι), L.HasHomology i
inst✝ : ∀ (i : ι), M.HasHomology i
hφ : QuasiIso φ
hφφ' : QuasiIso (φ ≫ φ')
⊢ QuasiIso (φ ≫ φ')

Proof state:
ι : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
inst✝² : ∀ (i : ι), K.HasHomology i
inst✝¹ : ∀ (i : ι), L.HasHomology i
inst✝ : ∀ (i : ι), M.HasHomology i
hφ : QuasiIso φ
hφφ' : QuasiIso (φ ≫ φ')
⊢ QuasiIso (φ ≫ φ')

Tactic:
infer_instance

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Summable.lean
lemma Complex.summable_log_one_add_of_summable {f : ι → ℂ} (hf : Summable f) :
    Summable (fun i : ι => Complex.log (1 + f i))

Proof state:
case h
ι : Type u_1
f : ι → ℂ
hf : Summable f
i : ι
hi : ‖f i‖ ≤ 1 / 2
⊢ ‖log (1 + f i)‖ ≤ (3 / 2) • ‖f i‖

Tactic:
exact norm_log_one_add_half_le_self hi

Result:
no goals

Proof state:
ι : Type u_1
f : ι → ℂ
hf : Summable f
⊢ ∀ᶠ (i : ι) in cofinite, ‖log (1 + f i)‖ ≤ (3 / 2) • ‖f i‖

Tactic:
filter_upwards [hf.norm.tendsto_cofinite_zero.eventually_le_const one_half_pos] with i hi

Result:
case h
ι : Type u_1
f : ι → ℂ
hf : Summable f
i : ι
hi : ‖f i‖ ≤ 1 / 2
⊢ ‖log (1 + f i)‖ ≤ (3 / 2) • ‖f i‖

Proof state:
ι : Type u_1
f : ι → ℂ
hf : Summable f
⊢ Summable fun i => log (1 + f i)

Tactic:
apply (hf.norm.const_smul (3 / 2 : ℝ)).of_norm_bounded_eventually

Result:
ι : Type u_1
f : ι → ℂ
hf : Summable f
⊢ ∀ᶠ (i : ι) in cofinite, ‖log (1 + f i)‖ ≤ (3 / 2) • ‖f i‖
-- Mathlib/Algebra/DirectSum/Internal.lean
theorem coe_mul_apply [AddMonoid ι] [SetLike.GradedMonoid A]
    [∀ (i : ι) (x : A i), Decidable (x ≠ 0)] (r r' : ⨁ i, A i) (n : ι) :
    ((r * r') n : R) =
      ∑ ij ∈ (r.support ×ˢ r'.support).filter (fun ij : ι × ι => ij.1 + ij.2 = n),
        (r ij.1 * r' ij.2 : R)

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✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : ↥(A i)) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), ↥(A i)
n : ι
⊢ ∑ i ∈ DFinsupp.support r ×ˢ DFinsupp.support r',
      ↑(((of (fun i => ↥(A i)) (i.1 + i.2)) (GradedMonoid.GMul.mul (r i.1) (r' i.2))) n) =
    ∑ ij ∈ Finset.filter (fun ij => ij.1 + ij.2 = n) (DFinsupp.support r ×ˢ DFinsupp.support r'), ↑(r ij.1) * ↑(r' ij.2)

Tactic:
simp_rw [coe_of_apply, apply_ite, ZeroMemClass.coe_zero, ← Finset.sum_filter, SetLike.coe_gMul]

Result:
no goals

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✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : ↥(A i)) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), ↥(A i)
n : ι
⊢ ↑((r * r') n) =
    ∑ ij ∈ Finset.filter (fun ij => ij.1 + ij.2 = n) (DFinsupp.support r ×ˢ DFinsupp.support r'), ↑(r ij.1) * ↑(r' ij.2)

Tactic:
rw [mul_eq_sum_support_ghas_mul, DFinsupp.finset_sum_apply, AddSubmonoidClass.coe_finset_sum]

Result:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : ↥(A i)) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), ↥(A i)
n : ι
⊢ ∑ i ∈ DFinsupp.support r ×ˢ DFinsupp.support r',
      ↑(((of (fun i => ↥(A i)) (i.1 + i.2)) (GradedMonoid.GMul.mul (r i.1) (r' i.2))) n) =
    ∑ ij ∈ Finset.filter (fun ij => ij.1 + ij.2 = n) (DFinsupp.support r ×ˢ DFinsupp.support r'), ↑(r ij.1) * ↑(r' ij.2)
-- Mathlib/Data/Set/NAry.lean
theorem image2_inter_union_subset_union :
    image2 f (s ∩ s') (t ∪ t') ⊆ image2 f s t ∪ image2 f s' t'

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s s' : Set α
t t' : Set β
⊢ image2 f (s ∩ s') (t ∪ t') ⊆ image2 f s t ∪ image2 f s' t'

Tactic:
rw [image2_union_right]

Result:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s s' : Set α
t t' : Set β
⊢ image2 f (s ∩ s') t ∪ image2 f (s ∩ s') t' ⊆ image2 f s t ∪ image2 f s' t'

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s s' : Set α
t t' : Set β
⊢ image2 f (s ∩ s') t ∪ image2 f (s ∩ s') t' ⊆ image2 f s t ∪ image2 f s' t'

Tactic:
exact
  union_subset_union (image2_subset_right inter_subset_left)
    (image2_subset_right inter_subset_right)

Result:
no goals
-- Mathlib/Data/Real/GoldenRatio.lean
theorem one_sub_goldConj : 1 - φ = ψ

Proof state:
⊢ 1 - φ = ψ

Tactic:
linarith [gold_add_goldConj]

Result:
no goals
-- Mathlib/Data/Finset/Sym.lean
theorem replicate_mem_sym (ha : a ∈ s) (n : ℕ) : Sym.replicate n a ∈ s.sym n :=
  mem_sym_iff.2 fun b hb ↦ by rwa [(Sym.mem_replicate.1 hb).2]

Proof state:
α : Type u_1
s : Finset α
a : α
inst✝ : DecidableEq α
ha : a ∈ s
n : ℕ
b : α
hb : b ∈ Sym.replicate n a
⊢ b ∈ s

Tactic:
rwa [(Sym.mem_replicate.1 hb).2]

Result:
no goals
-- Mathlib/GroupTheory/Congruence/Defs.lean
theorem coe_iInf {ι : Sort*} (f : ι → Con M) : ⇑(iInf f) = ⨅ i, ⇑(f i)

Proof state:
M : Type u_1
inst✝ : Mul M
ι : Sort u_4
f : ι → Con M
⊢ ⇑(iInf f) = ⨅ i, ⇑(f i)

Tactic:
rw [iInf, coe_sInf, ← Set.range_comp, sInf_range, Function.comp_def]

Result:
no goals
-- Mathlib/Data/Matrix/RowCol.lean
theorem updateCol_conjTranspose [DecidableEq m] [Star α] :
    updateCol Mᴴ i (star b) = (updateRow M i b)ᴴ

Proof state:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
b : n → α
inst✝¹ : DecidableEq m
inst✝ : Star α
⊢ ((M.map star).updateRow i (star b))ᵀ = ((M.map star).updateRow i (star ∘ b))ᵀ

Tactic:
rfl

Result:
no goals

Proof state:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
b : n → α
inst✝¹ : DecidableEq m
inst✝ : Star α
⊢ Mᴴ.updateCol i (star b) = (M.updateRow i b)ᴴ

Tactic:
rw [conjTranspose, conjTranspose, transpose_map, transpose_map, updateCol_transpose,
  map_updateRow]

Result:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
b : n → α
inst✝¹ : DecidableEq m
inst✝ : Star α
⊢ ((M.map star).updateRow i (star b))ᵀ = ((M.map star).updateRow i (star ∘ b))ᵀ
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem coe_support_append {u v w : V} (p : G.Walk u v) (p' : G.Walk v w) :
    ((p.append p').support : Multiset V) = {u} + p.support.tail + p'.support.tail

Proof state:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
p' : G.Walk v w
⊢ ↑(p.append p').support = {u} + ↑p.support.tail + ↑p'.support.tail

Tactic:
rw [support_append, ← Multiset.coe_add, coe_support]

Result:
no goals
-- Mathlib/Analysis/Convex/Topology.lean
theorem Convex.add_smul_mem_interior' {s : Set E} (hs : Convex 𝕜 s) {x y : E} (hx : x ∈ closure s)
    (hy : x + y ∈ interior s) {t : 𝕜} (ht : t ∈ Ioc (0 : 𝕜) 1) : x + t • y ∈ interior s

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
x y : E
hx : x ∈ closure s
hy : x + y ∈ interior s
t : 𝕜
ht : t ∈ Ioc 0 1
⊢ x + t • y ∈ interior s

Tactic:
simpa only [add_sub_cancel_left] using hs.add_smul_sub_mem_interior' hx hy ht

Result:
no goals
-- Mathlib/Analysis/Normed/Operator/BoundedLinearMaps.lean
theorem map_sub₂ (f : M →SL[ρ₁₂] F →SL[σ₁₂] G') (x x' : M) (y : F) :
    f (x - x') y = f x y - f x' y

Proof state:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹¹ : SeminormedAddCommGroup F
inst✝¹⁰ : NormedSpace 𝕜 F
R : Type u_5
𝕜₂ : Type u_6
𝕜' : Type u_7
inst✝⁹ : NontriviallyNormedField 𝕜'
inst✝⁸ : NontriviallyNormedField 𝕜₂
M : Type u_8
inst✝⁷ : TopologicalSpace M
σ₁₂ : 𝕜 →+* 𝕜₂
G' : Type u_9
inst✝⁶ : SeminormedAddCommGroup G'
inst✝⁵ : NormedSpace 𝕜₂ G'
inst✝⁴ : NormedSpace 𝕜' G'
inst✝³ : SMulCommClass 𝕜₂ 𝕜' G'
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ρ₁₂ : R →+* 𝕜'
f : M →SL[ρ₁₂] F →SL[σ₁₂] G'
x x' : M
y : F
⊢ (f (x - x')) y = (f x) y - (f x') y

Tactic:
rw [f.map_sub, sub_apply]

Result:
no goals
-- Mathlib/Combinatorics/Additive/FreimanHom.lean
@[to_additive]
lemma IsMulFreimanHom.inv (hf : IsMulFreimanHom n A B f) : IsMulFreimanHom n A B⁻¹ f⁻¹ where
  mapsTo := hf.mapsTo.inv
  map_prod_eq_map_prod s t hsA htA hs ht h

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : DivisionCommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
hf : IsMulFreimanHom n A B f
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
h : s.prod = t.prod
⊢ (map f⁻¹ s).prod = (map f⁻¹ t).prod

Tactic:
rw [Pi.inv_def, prod_map_inv, prod_map_inv, hf.map_prod_eq_map_prod hsA htA hs ht h]

Result:
no goals
-- Mathlib/Data/Analysis/Filter.lean
theorem ofEquiv_val (E : σ ≃ τ) (F : CFilter α σ) (a : τ) : F.ofEquiv E a = F (E.symm a)

Proof state:
α : Type u_1
σ : Type u_3
τ : Type u_4
inst✝ : PartialOrder α
E : σ ≃ τ
F : CFilter α σ
a : τ
⊢ (ofEquiv E F).f a = F.f (E.symm a)

Tactic:
cases F

Result:
case mk
α : Type u_1
σ : Type u_3
τ : Type u_4
inst✝ : PartialOrder α
E : σ ≃ τ
a : τ
f✝ : σ → α
pt✝ : σ
inf✝ : σ → σ → σ
inf_le_left✝ : ∀ (a b : σ), f✝ (inf✝ a b) ≤ f✝ a
inf_le_right✝ : ∀ (a b : σ), f✝ (inf✝ a b) ≤ f✝ b
⊢ (ofEquiv E { f := f✝, pt := pt✝, inf := inf✝, inf_le_left := inf_le_left✝, inf_le_right := inf_le_right✝ }).f a =
    { f := f✝, pt := pt✝, inf := inf✝, inf_le_left := inf_le_left✝, inf_le_right := inf_le_right✝ }.f (E.symm a)

Proof state:
case mk
α : Type u_1
σ : Type u_3
τ : Type u_4
inst✝ : PartialOrder α
E : σ ≃ τ
a : τ
f✝ : σ → α
pt✝ : σ
inf✝ : σ → σ → σ
inf_le_left✝ : ∀ (a b : σ), f✝ (inf✝ a b) ≤ f✝ a
inf_le_right✝ : ∀ (a b : σ), f✝ (inf✝ a b) ≤ f✝ b
⊢ (ofEquiv E { f := f✝, pt := pt✝, inf := inf✝, inf_le_left := inf_le_left✝, inf_le_right := inf_le_right✝ }).f a =
    { f := f✝, pt := pt✝, inf := inf✝, inf_le_left := inf_le_left✝, inf_le_right := inf_le_right✝ }.f (E.symm a)

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/VonNeumannAlgebra/Basic.lean
theorem coe_commutant (S : VonNeumannAlgebra H) :
    ↑S.commutant = Set.centralizer (S : Set (H →L[ℂ] H))

Proof state:
H : Type u
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℂ H
inst✝ : CompleteSpace H
S : VonNeumannAlgebra H
⊢ ↑S.commutant = (↑S).centralizer

Tactic:
simp [commutant]

Result:
no goals
-- Mathlib/Tactic/Ring/Basic.lean
theorem natCast_add {a₁ a₂ : ℕ}
    (_ : ((a₁ : ℕ) : R) = b₁) (_ : ((a₂ : ℕ) : R) = b₂) : ((a₁ + a₂ : ℕ) : R) = b₁ + b₂

Proof state:
R : Type u_1
inst✝ : CommSemiring R
a₁ a₂ : ℕ
⊢ ↑(a₁ + a₂) = ↑a₁ + ↑a₂

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommSemiring R
b₁ b₂ : R
a₁ a₂ : ℕ
x✝¹ : ↑a₁ = b₁
x✝ : ↑a₂ = b₂
⊢ ↑(a₁ + a₂) = b₁ + b₂

Tactic:
subst_vars

Result:
R : Type u_1
inst✝ : CommSemiring R
a₁ a₂ : ℕ
⊢ ↑(a₁ + a₂) = ↑a₁ + ↑a₂
-- Mathlib/Combinatorics/Colex.lean
lemma toColex_inj {s t : Finset α} : toColex s = toColex t ↔ s = t

Proof state:
α : Type u_1
s t : Finset α
⊢ { ofColex := s } = { ofColex := t } ↔ s = t

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem forall_lt_succ_right {p : Nat → Prop} :
    (∀ m, m < n + 1 → p m) ↔ (∀ m, m < n → p m) ∧ p n

Proof state:
n : Nat
p : Nat → Prop
⊢ (∀ (m : Nat), m < n + 1 → p m) ↔ (∀ (m : Nat), m < n → p m) ∧ p n

Tactic:
simpa using forall_lt_succ_right' (p := fun m _ => p m)

Result:
no goals
-- Mathlib/CategoryTheory/Adjunction/Mates.lean
theorem conjugateEquiv_of_iso (α : L₂ ⟶ L₁) [IsIso (conjugateEquiv adj₁ adj₂ α)] :
    IsIso α

Proof state:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : L₂ ⟶ L₁
inst✝ : IsIso ((conjugateEquiv adj₁ adj₂) α)
this : IsIso ((conjugateEquiv adj₁ adj₂).symm ((conjugateEquiv adj₁ adj₂) α))
⊢ IsIso α

Tactic:
simpa using this

Result:
no goals

Proof state:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : L₂ ⟶ L₁
inst✝ : IsIso ((conjugateEquiv adj₁ adj₂) α)
⊢ IsIso α

Tactic:
suffices IsIso ((conjugateEquiv adj₁ adj₂).symm (conjugateEquiv adj₁ adj₂ α))
  by simpa using this

Result:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : L₂ ⟶ L₁
inst✝ : IsIso ((conjugateEquiv adj₁ adj₂) α)
⊢ IsIso ((conjugateEquiv adj₁ adj₂).symm ((conjugateEquiv adj₁ adj₂) α))

Proof state:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : L₂ ⟶ L₁
inst✝ : IsIso ((conjugateEquiv adj₁ adj₂) α)
⊢ IsIso ((conjugateEquiv adj₁ adj₂).symm ((conjugateEquiv adj₁ adj₂) α))

Tactic:
infer_instance

Result:
no goals
-- Mathlib/Logic/Equiv/List.lean
theorem raise_lower : ∀ {l n}, List.Sorted (· ≤ ·) (n :: l) → raise (lower l n) n = l
  | [], _, _ => rfl
  | m :: l, n, h => by
    have : n ≤ m := List.rel_of_sorted_cons h _ (l.mem_cons_self _)
    simp [raise, lower, Nat.sub_add_cancel this, raise_lower h.of_cons]

Proof state:
m : ℕ
l : List ℕ
n : ℕ
h : Sorted (fun x1 x2 => x1 ≤ x2) (n :: m :: l)
⊢ raise (lower (m :: l) n) n = m :: l

Tactic:
have : n ≤ m := List.rel_of_sorted_cons h _ (l.mem_cons_self _)

Result:
m : ℕ
l : List ℕ
n : ℕ
h : Sorted (fun x1 x2 => x1 ≤ x2) (n :: m :: l)
this : n ≤ m
⊢ raise (lower (m :: l) n) n = m :: l

Proof state:
m : ℕ
l : List ℕ
n : ℕ
h : Sorted (fun x1 x2 => x1 ≤ x2) (n :: m :: l)
this : n ≤ m
⊢ raise (lower (m :: l) n) n = m :: l

Tactic:
simp [raise, lower, Nat.sub_add_cancel this, raise_lower h.of_cons]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem rpow_inv_le_iff_of_neg (hx : 0 < x) (hy : 0 < y) (hz : z < 0) :
    x ^ z⁻¹ ≤ y ↔ y ^ z ≤ x

Proof state:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
⊢ x ^ z⁻¹ ≤ y ↔ y ^ z ≤ x

Tactic:
rw [← rpow_le_rpow_iff_of_neg hy _ hz, rpow_inv_rpow _ hz.ne] <;> positivity

Result:
no goals