harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Distribution/SchwartzSpace.lean
lemma _root_.Function.HasTemperateGrowth.zero :
    Function.HasTemperateGrowth (fun _ : E ↦ (0 : F))

Proof state:
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
n : ℕ
x : E
⊢ ‖iteratedFDeriv ℝ n (fun x => 0) x‖ ≤ 0 * (1 + ‖x‖) ^ 0

Tactic:
simp only [iteratedFDeriv_zero_fun, Pi.zero_apply, norm_zero, forall_const]

Result:
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
n : ℕ
x : E
⊢ 0 ≤ 0 * (1 + ‖x‖) ^ 0

Proof state:
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
n : ℕ
x : E
⊢ 0 ≤ 0 * (1 + ‖x‖) ^ 0

Tactic:
positivity

Result:
no goals

Proof state:
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
⊢ Function.HasTemperateGrowth fun x => 0

Tactic:
refine ⟨contDiff_const, fun n ↦ ⟨0, 0, fun x ↦ ?_⟩⟩

Result:
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
n : ℕ
x : E
⊢ ‖iteratedFDeriv ℝ n (fun x => 0) x‖ ≤ 0 * (1 + ‖x‖) ^ 0
-- Mathlib/Analysis/Calculus/LocalExtr/Basic.lean
theorem IsLocalMin.hasFDerivAt_eq_zero (h : IsLocalMin f a) (hf : HasFDerivAt f f' a) : f' = 0

Proof state:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : E →L[ℝ] ℝ
a : E
h : IsLocalMin f a
hf : HasFDerivAt f f' a
⊢ f' = 0

Tactic:
ext y

Result:
case h
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : E →L[ℝ] ℝ
a : E
h : IsLocalMin f a
hf : HasFDerivAt f f' a
y : E
⊢ f' y = 0 y

Proof state:
case h
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : E →L[ℝ] ℝ
a : E
h : IsLocalMin f a
hf : HasFDerivAt f f' a
y : E
⊢ f' y = 0 y

Tactic:
apply (h.on univ).hasFDerivWithinAt_eq_zero hf.hasFDerivWithinAt <;>
    rw [posTangentConeAt_univ] <;>
  apply mem_univ

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/IsDiag.lean
theorem IsDiag.diagonal_diag [Zero α] [DecidableEq n] {A : Matrix n n α} (h : A.IsDiag) :
    diagonal (diag A) = A :=
  ext fun i j => by
    obtain rfl | hij := Decidable.eq_or_ne i j
    · rw [diagonal_apply_eq, diag]
    · rw [diagonal_apply_ne _ hij, h hij]

Proof state:
case inr
α : Type u_1
n : Type u_4
inst✝¹ : Zero α
inst✝ : DecidableEq n
A : Matrix n n α
h : A.IsDiag
i j : n
hij : i ≠ j
⊢ diagonal A.diag i j = A i j

Tactic:
rw [diagonal_apply_ne _ hij, h hij]

Result:
no goals

Proof state:
case inl
α : Type u_1
n : Type u_4
inst✝¹ : Zero α
inst✝ : DecidableEq n
A : Matrix n n α
h : A.IsDiag
i : n
⊢ diagonal A.diag i i = A i i

Tactic:
rw [diagonal_apply_eq, diag]

Result:
no goals

Proof state:
α : Type u_1
n : Type u_4
inst✝¹ : Zero α
inst✝ : DecidableEq n
A : Matrix n n α
h : A.IsDiag
i j : n
⊢ diagonal A.diag i j = A i j

Tactic:
obtain rfl | hij := Decidable.eq_or_ne i j

Result:
case inl
α : Type u_1
n : Type u_4
inst✝¹ : Zero α
inst✝ : DecidableEq n
A : Matrix n n α
h : A.IsDiag
i : n
⊢ diagonal A.diag i i = A i i

case inr
α : Type u_1
n : Type u_4
inst✝¹ : Zero α
inst✝ : DecidableEq n
A : Matrix n n α
h : A.IsDiag
i j : n
hij : i ≠ j
⊢ diagonal A.diag i j = A i j
-- Mathlib/Algebra/Order/SuccPred.lean
lemma antitoneOn_of_add_one_le (hs : s.OrdConnected) :
    (∀ a, ¬ IsMax a → a ∈ s → a + 1 ∈ s → f (a + 1) ≤ f a) → AntitoneOn f s

Proof state:
α : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α
inst✝⁴ : Preorder β
inst✝³ : Add α
inst✝² : One α
inst✝¹ : SuccAddOrder α
inst✝ : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
⊢ (∀ (a : α), ¬IsMax a → a ∈ s → a + 1 ∈ s → f (a + 1) ≤ f a) → AntitoneOn f s

Tactic:
simpa [Order.succ_eq_add_one] using antitoneOn_of_succ_le hs (f := f)

Result:
no goals
-- Mathlib/Data/Nat/Digits.lean
theorem zmodeq_ofDigits_digits (b b' : ℕ) (c : ℤ) (h : b' ≡ c [ZMOD b]) (n : ℕ) :
    n ≡ ofDigits c (digits b' n) [ZMOD b]

Proof state:
b b' : ℕ
c : ℤ
h : ↑b' ≡ c [ZMOD ↑b]
n : ℕ
⊢ ↑(ofDigits b' (b'.digits n)) ≡ ofDigits c (b'.digits n) [ZMOD ↑b]

Tactic:
rw [coe_int_ofDigits]

Result:
b b' : ℕ
c : ℤ
h : ↑b' ≡ c [ZMOD ↑b]
n : ℕ
⊢ ofDigits (↑b') (b'.digits n) ≡ ofDigits c (b'.digits n) [ZMOD ↑b]

Proof state:
b b' : ℕ
c : ℤ
h : ↑b' ≡ c [ZMOD ↑b]
n : ℕ
⊢ ofDigits (↑b') (b'.digits n) ≡ ofDigits c (b'.digits n) [ZMOD ↑b]

Tactic:
apply ofDigits_zmodeq' _ _ _ h

Result:
no goals
-- Mathlib/Combinatorics/Colex.lean
lemma insert_le_insert (ha : a ∉ s) (hb : b ∉ s) :
    toColex (insert a s) ≤ toColex (insert b s) ↔ a ≤ b

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
s : Finset α
a b : α
inst✝ : DecidableEq α
ha : a ∉ s
hb : b ∉ s
⊢ { ofColex := insert a s } ≤ { ofColex := insert b s } ↔ a ≤ b

Tactic:
rw [← cons_eq_insert _ _ ha, ← cons_eq_insert _ _ hb, cons_le_cons]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem size_alter_eq_self_of_not_mem [LawfulBEq α] {k : α} {f : Option β → Option β}
    (h : k ∉ m) (h' : (f (Const.get? m k)).isNone) : (Const.alter m k f).size = m.size

Proof state:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
β : Type v
m : DHashMap α fun x => β
inst✝ : LawfulBEq α
k : α
f : Option β → Option β
h : m.contains k = false
h' : (f (get? m k)).isNone = true
⊢ (alter m k f).size = m.size

Tactic:
exact Raw₀.Const.size_alter_eq_self_of_not_mem ⟨m.1, _⟩ m.2 h h'

Result:
no goals

Proof state:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
β : Type v
m : DHashMap α fun x => β
inst✝ : LawfulBEq α
k : α
f : Option β → Option β
h : ¬k ∈ m
h' : (f (get? m k)).isNone = true
⊢ (alter m k f).size = m.size

Tactic:
rw [mem_iff_contains, Bool.not_eq_true] at h

Result:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
β : Type v
m : DHashMap α fun x => β
inst✝ : LawfulBEq α
k : α
f : Option β → Option β
h : m.contains k = false
h' : (f (get? m k)).isNone = true
⊢ (alter m k f).size = m.size
-- Mathlib/Algebra/Lie/Nilpotent.lean
theorem ucs_mono (k : ℕ) (h : N₁ ≤ N₂) : N₁.ucs k ≤ N₂.ucs k

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N₁ N₂ : LieSubmodule R L M
inst✝ : LieModule R L M
k : ℕ
h : N₁ ≤ N₂
⊢ ucs k N₁ ≤ ucs k N₂

Tactic:
induction k with
| zero => simpa
| succ k ih =>
  simp only [ucs_succ]
  gcongr

Result:
no goals

Proof state:
case succ
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N₁ N₂ : LieSubmodule R L M
inst✝ : LieModule R L M
h : N₁ ≤ N₂
k : ℕ
ih : ucs k N₁ ≤ ucs k N₂
⊢ (ucs k N₁).normalizer ≤ (ucs k N₂).normalizer

Tactic:
gcongr

Result:
no goals

Proof state:
case zero
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N₁ N₂ : LieSubmodule R L M
inst✝ : LieModule R L M
h : N₁ ≤ N₂
⊢ ucs 0 N₁ ≤ ucs 0 N₂

Tactic:
simpa

Result:
no goals

Proof state:
case succ
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N₁ N₂ : LieSubmodule R L M
inst✝ : LieModule R L M
h : N₁ ≤ N₂
k : ℕ
ih : ucs k N₁ ≤ ucs k N₂
⊢ ucs (k + 1) N₁ ≤ ucs (k + 1) N₂

Tactic:
simp only [ucs_succ]

Result:
case succ
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N₁ N₂ : LieSubmodule R L M
inst✝ : LieModule R L M
h : N₁ ≤ N₂
k : ℕ
ih : ucs k N₁ ≤ ucs k N₂
⊢ (ucs k N₁).normalizer ≤ (ucs k N₂).normalizer
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/InverseDeriv.lean
theorem differentiableWithinAt_arcsin_Iic {x : ℝ} :
    DifferentiableWithinAt ℝ arcsin (Iic x) x ↔ x ≠ 1

Proof state:
x : ℝ
h : DifferentiableWithinAt ℝ arcsin (Iic x) x
⊢ x ≠ 1

Tactic:
rw [← neg_neg x, ← image_neg_Ici] at h

Result:
x : ℝ
h : DifferentiableWithinAt ℝ arcsin (Neg.neg '' Ici (-x)) (- -x)
⊢ x ≠ 1

Proof state:
x : ℝ
⊢ DifferentiableWithinAt ℝ arcsin (Iic x) x ↔ x ≠ 1

Tactic:
refine ⟨fun h => ?_, fun h => (hasDerivWithinAt_arcsin_Iic h).differentiableWithinAt⟩

Result:
x : ℝ
h : DifferentiableWithinAt ℝ arcsin (Iic x) x
⊢ x ≠ 1

Proof state:
x : ℝ
h : DifferentiableWithinAt ℝ arcsin (Neg.neg '' Ici (-x)) (- -x)
⊢ x ≠ 1

Tactic:
have := (h.comp (-x) differentiableWithinAt_id.neg (mapsTo_image _ _)).neg

Result:
x : ℝ
h : DifferentiableWithinAt ℝ arcsin (Neg.neg '' Ici (-x)) (- -x)
this : DifferentiableWithinAt ℝ (fun y => -(arcsin ∘ Neg.neg) y) (Ici (-x)) (-x)
⊢ x ≠ 1
-- Mathlib/Order/SupClosed.lean
@[simp] lemma infClosure_prod (s : Set α) (t : Set β) :
    infClosure (s ×ˢ t) = infClosure s ×ˢ infClosure t :=
  le_antisymm (infClosure_min (Set.prod_mono subset_infClosure subset_infClosure) <|
    infClosed_infClosure.prod infClosed_infClosure) <| by
      rintro ⟨_, _⟩ ⟨⟨u, hu, hus, rfl⟩, v, hv, hvt, rfl⟩
      refine ⟨u ×ˢ v, hu.product hv, ?_, ?_⟩
      · simpa only [coe_product] using Set.prod_mono hus hvt
      · simp [prodMk_inf'_inf']

Proof state:
case mk.intro.intro.intro.intro.intro.intro.intro.refine_1
α : Type u_3
β : Type u_4
inst✝¹ : SemilatticeInf α
inst✝ : SemilatticeInf β
s : Set α
t : Set β
u : Finset α
hu : u.Nonempty
hus : ↑u ⊆ s
v : Finset β
hv : v.Nonempty
hvt : ↑v ⊆ t
⊢ ↑(u ×ˢ v) ⊆ s ×ˢ t

Tactic:
simpa only [coe_product] using Set.prod_mono hus hvt

Result:
no goals

Proof state:
case mk.intro.intro.intro.intro.intro.intro.intro.refine_2
α : Type u_3
β : Type u_4
inst✝¹ : SemilatticeInf α
inst✝ : SemilatticeInf β
s : Set α
t : Set β
u : Finset α
hu : u.Nonempty
hus : ↑u ⊆ s
v : Finset β
hv : v.Nonempty
hvt : ↑v ⊆ t
⊢ (u ×ˢ v).inf' ⋯ id = (u.inf' hu id, v.inf' hv id)

Tactic:
simp [prodMk_inf'_inf']

Result:
no goals

Proof state:
case mk.intro.intro.intro.intro.intro.intro.intro
α : Type u_3
β : Type u_4
inst✝¹ : SemilatticeInf α
inst✝ : SemilatticeInf β
s : Set α
t : Set β
u : Finset α
hu : u.Nonempty
hus : ↑u ⊆ s
v : Finset β
hv : v.Nonempty
hvt : ↑v ⊆ t
⊢ (u.inf' hu id, v.inf' hv id) ∈ infClosure (s ×ˢ t)

Tactic:
refine ⟨u ×ˢ v, hu.product hv, ?_, ?_⟩

Result:
case mk.intro.intro.intro.intro.intro.intro.intro.refine_1
α : Type u_3
β : Type u_4
inst✝¹ : SemilatticeInf α
inst✝ : SemilatticeInf β
s : Set α
t : Set β
u : Finset α
hu : u.Nonempty
hus : ↑u ⊆ s
v : Finset β
hv : v.Nonempty
hvt : ↑v ⊆ t
⊢ ↑(u ×ˢ v) ⊆ s ×ˢ t

case mk.intro.intro.intro.intro.intro.intro.intro.refine_2
α : Type u_3
β : Type u_4
inst✝¹ : SemilatticeInf α
inst✝ : SemilatticeInf β
s : Set α
t : Set β
u : Finset α
hu : u.Nonempty
hus : ↑u ⊆ s
v : Finset β
hv : v.Nonempty
hvt : ↑v ⊆ t
⊢ (u ×ˢ v).inf' ⋯ id = (u.inf' hu id, v.inf' hv id)

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : SemilatticeInf α
inst✝ : SemilatticeInf β
s : Set α
t : Set β
⊢ infClosure s ×ˢ infClosure t ≤ infClosure (s ×ˢ t)

Tactic:
rintro ⟨_, _⟩ ⟨⟨u, hu, hus, rfl⟩, v, hv, hvt, rfl⟩

Result:
case mk.intro.intro.intro.intro.intro.intro.intro
α : Type u_3
β : Type u_4
inst✝¹ : SemilatticeInf α
inst✝ : SemilatticeInf β
s : Set α
t : Set β
u : Finset α
hu : u.Nonempty
hus : ↑u ⊆ s
v : Finset β
hv : v.Nonempty
hvt : ↑v ⊆ t
⊢ (u.inf' hu id, v.inf' hv id) ∈ infClosure (s ×ˢ t)
-- Mathlib/Data/Multiset/Fold.lean
theorem coe_fold_l (b : α) (l : List α) : fold op b l = l.foldl op b :=
  (coe_foldr_swap op b l).trans <| by simp [hc.comm]

Proof state:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
b : α
l : List α
⊢ List.foldl (fun x y => op y x) b l = List.foldl op b l

Tactic:
simp [hc.comm]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/HurwitzZetaOdd.lean
/-- If `s` is not in `-ℕ`, then `hurwitzZetaOdd a (1 - s)` is an explicit multiple of
`sinZeta s`. -/
lemma hurwitzZetaOdd_one_sub (a : UnitAddCircle) {s : ℂ} (hs : ∀ (n : ℕ), s ≠ -n) :
    hurwitzZetaOdd a (1 - s) = 2 * (2 * π) ^ (-s) * Gamma s * sin (π * s / 2) * sinZeta a s

Proof state:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
⊢ hurwitzZetaOdd a (1 - s) = 2 * (2 * ↑π) ^ (-s) * Complex.Gamma s * Complex.sin (↑π * s / 2) * sinZeta a s

Tactic:
rw [← Gammaℂ, hurwitzZetaOdd, (by ring : 1 - s + 1 = 2 - s), div_eq_mul_inv,
  inv_Gammaℝ_two_sub hs, completedHurwitzZetaOdd_one_sub, sinZeta, ← div_eq_mul_inv,
  ← mul_div_assoc, ← mul_div_assoc, mul_comm]

Result:
no goals

Proof state:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
⊢ 1 - s + 1 = 2 - s

Tactic:
ring

Result:
no goals
-- Mathlib/Algebra/Group/Indicator.lean
theorem comp_mulIndicator (h : M → β) (f : α → M) {s : Set α} {x : α} [DecidablePred (· ∈ s)] :
    h (s.mulIndicator f x) = s.piecewise (h ∘ f) (const α (h 1)) x

Proof state:
α : Type u_1
β : Type u_2
M : Type u_3
inst✝¹ : One M
h : M → β
f : α → M
s : Set α
x : α
inst✝ : DecidablePred fun x => x ∈ s
this : DecidablePred fun x => x ∈ s := Classical.decPred fun x => x ∈ s
⊢ h (s.mulIndicator f x) = s.piecewise (h ∘ f) (const α (h 1)) x

Tactic:
convert s.apply_piecewise f (const α 1) (fun _ => h) (x := x) using 2

Result:
no goals
-- Mathlib/MeasureTheory/SetSemiring.lean
lemma subset_of_diffUnion_disjointOfDiffUnion (hC : IsSetSemiring C) (hs : s ∈ C) (hI : ↑I ⊆ C)
    (t : Set α) (ht : t ∈ (hC.disjointOfDiffUnion hs hI : Set (Set α))) :
    t ⊆ s \ ⋃₀ I

Proof state:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
⊢ ∀ t ∈ ↑(hC.disjointOfDiffUnion hs hI), t ⊆ s \ ⋃₀ ↑I

Tactic:
rw [← sUnion_subset_iff, hC.diff_sUnion_eq_sUnion_disjointOfDiffUnion hs hI]

Result:
no goals

Proof state:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
t : Set α
ht : t ∈ ↑(hC.disjointOfDiffUnion hs hI)
⊢ t ⊆ s \ ⋃₀ ↑I

Tactic:
revert t ht

Result:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
⊢ ∀ t ∈ ↑(hC.disjointOfDiffUnion hs hI), t ⊆ s \ ⋃₀ ↑I
-- Mathlib/Data/Finset/Insert.lean
theorem not_nontrivial_singleton : ¬ ({a} : Finset α).Nontrivial

Proof state:
α : Type u_1
a : α
⊢ ¬{a}.Nontrivial

Tactic:
simp [Finset.Nontrivial]

Result:
no goals
-- Mathlib/Algebra/Group/Defs.lean
theorem inv_eq_of_mul_eq_one_left (h : a * b = 1) : b⁻¹ = a

Proof state:
G : Type u_1
inst✝ : DivisionMonoid G
a b : G
h : a * b = 1
⊢ b⁻¹ = a

Tactic:
rw [← inv_eq_of_mul_eq_one_right h, inv_inv]

Result:
no goals
-- Mathlib/Topology/ContinuousMap/Bounded/Basic.lean
theorem abs_diff_coe_le_dist : ‖f x - g x‖ ≤ dist f g

Proof state:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f g : α →ᵇ β
x : α
⊢ ‖f x - g x‖ ≤ ‖f - g‖

Tactic:
exact (f - g).norm_coe_le_norm x

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f g : α →ᵇ β
x : α
⊢ ‖f x - g x‖ ≤ dist f g

Tactic:
rw [dist_eq_norm]

Result:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f g : α →ᵇ β
x : α
⊢ ‖f x - g x‖ ≤ ‖f - g‖
-- Mathlib/AlgebraicTopology/DoldKan/Compatibility.lean
theorem equivalence₁UnitIso_eq : (equivalence₁ hF).unitIso = equivalence₁UnitIso hF

Proof state:
case w.w.h
A : Type u_1
A' : Type u_2
B' : Type u_4
inst✝² : Category.{u_5, u_1} A
inst✝¹ : Category.{u_7, u_2} A'
inst✝ : Category.{u_6, u_4} B'
eA : A ≌ A'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
X : A
⊢ (equivalence₁ hF).unitIso.hom.app X = (equivalence₁UnitIso hF).hom.app X

Tactic:
simp [equivalence₁]

Result:
no goals

Proof state:
A : Type u_1
A' : Type u_2
B' : Type u_4
inst✝² : Category.{u_5, u_1} A
inst✝¹ : Category.{u_7, u_2} A'
inst✝ : Category.{u_6, u_4} B'
eA : A ≌ A'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
⊢ (equivalence₁ hF).unitIso = equivalence₁UnitIso hF

Tactic:
ext X

Result:
case w.w.h
A : Type u_1
A' : Type u_2
B' : Type u_4
inst✝² : Category.{u_5, u_1} A
inst✝¹ : Category.{u_7, u_2} A'
inst✝ : Category.{u_6, u_4} B'
eA : A ≌ A'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
X : A
⊢ (equivalence₁ hF).unitIso.hom.app X = (equivalence₁UnitIso hF).hom.app X
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean
@[simp]
lemma condExp_ofNat (n : ℕ) [n.AtLeastTwo] (f : α → R) :
    μ[ofNat(n) * f|m] =ᵐ[μ] ofNat(n) * μ[f|m]

Proof state:
α : Type u_1
m m₀ : MeasurableSpace α
μ : Measure α
R : Type u_5
inst✝³ : NormedRing R
inst✝² : NormedSpace ℝ R
inst✝¹ : CompleteSpace R
n : ℕ
inst✝ : n.AtLeastTwo
f : α → R
⊢ μ[OfNat.ofNat n * f|m] =ᶠ[ae μ] OfNat.ofNat n * μ[f|m]

Tactic:
simpa [Nat.cast_smul_eq_nsmul] using condExp_smul (μ := μ) (m := m) (n : ℝ) f

Result:
no goals
-- Mathlib/Order/Disjointed.lean
lemma Fintype.sup_disjointed [Fintype ι] (f : ι → α) :
    univ.sup (disjointed f) = univ.sup f

Proof state:
α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : PartialOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : Fintype ι
f : ι → α
hun : univ.biUnion Iic = univ
⊢ univ.sup (disjointed f) = univ.sup f

Tactic:
rw [← hun, sup_biUnion, sup_biUnion, sup_congr rfl (fun i _ ↦ ?_)]

Result:
α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : PartialOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : Fintype ι
f : ι → α
hun : univ.biUnion Iic = univ
i : ι
x✝ : i ∈ univ
⊢ (Iic i).sup (disjointed f) = (Iic i).sup f

Proof state:
α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : PartialOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : Fintype ι
f : ι → α
⊢ univ.biUnion Iic = univ

Tactic:
ext r

Result:
case h
α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : PartialOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : Fintype ι
f : ι → α
r : ι
⊢ r ∈ univ.biUnion Iic ↔ r ∈ univ

Proof state:
case h
α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : PartialOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : Fintype ι
f : ι → α
r : ι
⊢ r ∈ univ.biUnion Iic ↔ r ∈ univ

Tactic:
simpa only [mem_biUnion, mem_univ, mem_Iic, true_and, iff_true] using ⟨r, le_rfl⟩

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : PartialOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : Fintype ι
f : ι → α
⊢ univ.sup (disjointed f) = univ.sup f

Tactic:
have hun : univ.biUnion Iic = (univ : Finset ι) := by
  ext r; simpa only [mem_biUnion, mem_univ, mem_Iic, true_and, iff_true] using ⟨r, le_rfl⟩

Result:
α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : PartialOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : Fintype ι
f : ι → α
hun : univ.biUnion Iic = univ
⊢ univ.sup (disjointed f) = univ.sup f

Proof state:
α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : PartialOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : Fintype ι
f : ι → α
⊢ univ.sup (disjointed f) = univ.sup f

Tactic:
classical
have hun : univ.biUnion Iic = (univ : Finset ι) := by
  ext r; simpa only [mem_biUnion, mem_univ, mem_Iic, true_and, iff_true] using ⟨r, le_rfl⟩
rw [← hun, sup_biUnion, sup_biUnion, sup_congr rfl (fun i _ ↦ ?_)]
rw [← sup'_eq_sup nonempty_Iic, ← sup'_eq_sup nonempty_Iic,
  ← partialSups_apply, ← partialSups_apply, partialSups_disjointed]

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : PartialOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : Fintype ι
f : ι → α
hun : univ.biUnion Iic = univ
i : ι
x✝ : i ∈ univ
⊢ (Iic i).sup (disjointed f) = (Iic i).sup f

Tactic:
rw [← sup'_eq_sup nonempty_Iic, ← sup'_eq_sup nonempty_Iic,
  ← partialSups_apply, ← partialSups_apply, partialSups_disjointed]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldl_map_hom (g : α → β) (f : α → α → α) (f' : β → β → β) (a : α) (l : Array α)
    (h : ∀ x y, f' (g x) (g y) = g (f x y)) :
    (l.map g).foldl f' (g a) = g (l.foldl f a)

Proof state:
case mk
α : Type u_1
β : Type u_2
g : α → β
f : α → α → α
f' : β → β → β
a : α
h : ∀ (x y : α), f' (g x) (g y) = g (f x y)
toList✝ : List α
⊢ foldl f' (g a) (map g { toList := toList✝ }) = g (foldl f a { toList := toList✝ })

Tactic:
simp

Result:
case mk
α : Type u_1
β : Type u_2
g : α → β
f : α → α → α
f' : β → β → β
a : α
h : ∀ (x y : α), f' (g x) (g y) = g (f x y)
toList✝ : List α
⊢ List.foldl f' (g a) (List.map g toList✝) = g (List.foldl f a toList✝)

Proof state:
case mk
α : Type u_1
β : Type u_2
g : α → β
f : α → α → α
f' : β → β → β
a : α
h : ∀ (x y : α), f' (g x) (g y) = g (f x y)
toList✝ : List α
⊢ List.foldl f' (g a) (List.map g toList✝) = g (List.foldl f a toList✝)

Tactic:
rw [List.foldl_map_hom _ _ _ _ _ h]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
g : α → β
f : α → α → α
f' : β → β → β
a : α
l : Array α
h : ∀ (x y : α), f' (g x) (g y) = g (f x y)
⊢ foldl f' (g a) (map g l) = g (foldl f a l)

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
g : α → β
f : α → α → α
f' : β → β → β
a : α
h : ∀ (x y : α), f' (g x) (g y) = g (f x y)
toList✝ : List α
⊢ foldl f' (g a) (map g { toList := toList✝ }) = g (foldl f a { toList := toList✝ })
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem sup_mul_eq_of_coprime_right (h : I ⊔ K = ⊤) : I ⊔ J * K = I ⊔ J

Proof state:
R : Type u
inst✝ : CommSemiring R
I J K : Ideal R
h : I ⊔ K = ⊤
⊢ I ⊔ J * K = I ⊔ J

Tactic:
rw [mul_comm]

Result:
R : Type u
inst✝ : CommSemiring R
I J K : Ideal R
h : I ⊔ K = ⊤
⊢ I ⊔ K * J = I ⊔ J

Proof state:
R : Type u
inst✝ : CommSemiring R
I J K : Ideal R
h : I ⊔ K = ⊤
⊢ I ⊔ K * J = I ⊔ J

Tactic:
exact sup_mul_eq_of_coprime_left h

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/ShiftSequence.lean
lemma shiftIso_inv_app (n a a' : ℤ) (ha' : n + a = a') (K : CochainComplex C ℤ) :
    (shiftIso C n a a' ha').inv.app K =
      ShortComplex.homologyMap ((shiftShortComplexFunctorIso C n a a' ha').inv.app K)

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
n a a' : ℤ
ha' : n + a = a'
K : CochainComplex C ℤ
⊢ ((𝟙 (homology K a') ≫ ShortComplex.homologyMap ((shiftShortComplexFunctorIso C n a a' ha').inv.app K)) ≫
        𝟙
          ((shortComplexFunctor C (up ℤ) a).obj
              ((CategoryTheory.shiftFunctor (HomologicalComplex C (up ℤ)) n).obj K)).homology) ≫
      𝟙 (((CategoryTheory.shiftFunctor (HomologicalComplex C (up ℤ)) n).obj K).homology a) =
    ShortComplex.homologyMap ((shiftShortComplexFunctorIso C n a a' ha').inv.app K)

Tactic:
erw [id_comp, comp_id, comp_id]

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
n a a' : ℤ
ha' : n + a = a'
K : CochainComplex C ℤ
⊢ (shiftIso C n a a' ha').inv.app K = ShortComplex.homologyMap ((shiftShortComplexFunctorIso C n a a' ha').inv.app K)

Tactic:
dsimp [shiftIso]

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
n a a' : ℤ
ha' : n + a = a'
K : CochainComplex C ℤ
⊢ ((𝟙 (homology K a') ≫ ShortComplex.homologyMap ((shiftShortComplexFunctorIso C n a a' ha').inv.app K)) ≫
        𝟙
          ((shortComplexFunctor C (up ℤ) a).obj
              ((CategoryTheory.shiftFunctor (HomologicalComplex C (up ℤ)) n).obj K)).homology) ≫
      𝟙 (((CategoryTheory.shiftFunctor (HomologicalComplex C (up ℤ)) n).obj K).homology a) =
    ShortComplex.homologyMap ((shiftShortComplexFunctorIso C n a a' ha').inv.app K)