harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_sum {α : Type*} {ι : Type*} [CommMonoid α] (f : ι → Multiset α) (s : Finset ι) :
    (∑ x ∈ s, f x).prod = ∏ x ∈ s, (f x).prod

Proof state:
case cons
α : Type u_6
ι : Type u_7
inst✝ : CommMonoid α
f : ι → Multiset α
a : ι
s : Finset ι
has : a ∉ s
ih : (∑ x ∈ s, f x).prod = ∏ x ∈ s, (f x).prod
⊢ (∑ x ∈ Finset.cons a s has, f x).prod = ∏ x ∈ Finset.cons a s has, (f x).prod

Tactic:
rw [Finset.sum_cons, Finset.prod_cons, Multiset.prod_add, ih]

Result:
no goals

Proof state:
α : Type u_6
ι : Type u_7
inst✝ : CommMonoid α
f : ι → Multiset α
s : Finset ι
⊢ (∑ x ∈ s, f x).prod = ∏ x ∈ s, (f x).prod

Tactic:
induction s using Finset.cons_induction with
| empty => rw [Finset.sum_empty, Finset.prod_empty, Multiset.prod_zero]
| cons a s has ih => rw [Finset.sum_cons, Finset.prod_cons, Multiset.prod_add, ih]

Result:
no goals

Proof state:
case empty
α : Type u_6
ι : Type u_7
inst✝ : CommMonoid α
f : ι → Multiset α
⊢ (∑ x ∈ ∅, f x).prod = ∏ x ∈ ∅, (f x).prod

Tactic:
rw [Finset.sum_empty, Finset.prod_empty, Multiset.prod_zero]

Result:
no goals
-- Mathlib/Order/SuccPred/Basic.lean
theorem Ioc_succ_right (h : a < succ b) : Ioc a (succ b) = insert (succ b) (Ioc a b)

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
h : a < succ b
⊢ Ioc a (succ b) = insert (succ b) (Ioc a b)

Tactic:
simp_rw [← Ioi_inter_Iic, Iic_succ, inter_insert_of_mem (mem_Ioi.2 h)]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem decide_beq_decide (p q : Prop) [dpq : Decidable (p ↔ q)] [dp : Decidable p] [dq : Decidable q] :
    (decide p == decide q) = decide (p ↔ q)

Proof state:
case isTrue
p✝ q : Prop
dpq : Decidable (p✝ ↔ q)
dq : Decidable q
p : p✝
⊢ (decide p✝ == decide q) = decide (p✝ ↔ q)

Tactic:
simp [p]

Result:
no goals

Proof state:
p q : Prop
dpq : Decidable (p ↔ q)
dp : Decidable p
dq : Decidable q
⊢ (decide p == decide q) = decide (p ↔ q)

Tactic:
cases dp with | _ p => simp [p]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/WF.lean
theorem setBlack_idem {t : RBNode α} : t.setBlack.setBlack = t.setBlack

Proof state:
α : Type u_1
t : RBNode α
⊢ t.setBlack.setBlack = t.setBlack

Tactic:
cases t <;> rfl

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
theorem prod.map_map {A₁ A₂ A₃ B₁ B₂ B₃ : C} [HasBinaryProduct A₁ B₁] [HasBinaryProduct A₂ B₂]
    [HasBinaryProduct A₃ B₃] (f : A₁ ⟶ A₂) (g : B₁ ⟶ B₂) (h : A₂ ⟶ A₃) (k : B₂ ⟶ B₃) :
    prod.map f g ≫ prod.map h k = prod.map (f ≫ h) (g ≫ k)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
A₁ A₂ A₃ B₁ B₂ B₃ : C
inst✝² : HasBinaryProduct A₁ B₁
inst✝¹ : HasBinaryProduct A₂ B₂
inst✝ : HasBinaryProduct A₃ B₃
f : A₁ ⟶ A₂
g : B₁ ⟶ B₂
h : A₂ ⟶ A₃
k : B₂ ⟶ B₃
⊢ map f g ≫ map h k = map (f ≫ h) (g ≫ k)

Tactic:
ext <;> simp

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

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

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

Result:
no goals

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

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

Result:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
h : m.contains k = false
h' : (f (m.get? k)).isSome = true
⊢ (m.alter k f).size = m.size + 1
-- Mathlib/Algebra/Order/Interval/Finset/SuccPred.lean
lemma Icc_add_one_sub_one_eq_Ioo (a b : α) : Icc (a + 1) (b - 1) = Ioo a b

Proof state:
α : Type u_2
inst✝⁷ : LinearOrder α
inst✝⁶ : One α
inst✝⁵ : LocallyFiniteOrder α
inst✝⁴ : Add α
inst✝³ : Sub α
inst✝² : SuccAddOrder α
inst✝¹ : PredSubOrder α
inst✝ : Nontrivial α
a b : α
⊢ Icc (a + 1) (b - 1) = Ioo a b

Tactic:
simpa [succ_eq_add_one, pred_eq_sub_one] using Icc_succ_pred_eq_Ioo a b

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Operations.lean
theorem prod_eq_bot_iff {s : Submonoid M} {t : Submonoid N} : s.prod t = ⊥ ↔ s = ⊥ ∧ t = ⊥

Proof state:
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
s : Submonoid M
t : Submonoid N
⊢ s.prod t = ⊥ ↔ s = ⊥ ∧ t = ⊥

Tactic:
simp only [eq_bot_iff, prod_le_iff, (gc_map_comap _).le_iff_le, comap_bot', mker_inl, mker_inr]

Result:
no goals
-- Mathlib/RingTheory/Etale/Basic.lean
theorem iff_unramified_and_smooth :
    FormallyEtale R A ↔ FormallyUnramified R A ∧ FormallySmooth R A

Proof state:
R : Type u
inst✝² : CommRing R
A : Type u
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ FormallyEtale R A ↔ FormallyUnramified R A ∧ FormallySmooth R A

Tactic:
rw [FormallyUnramified.iff_comp_injective, formallySmooth_iff, formallyEtale_iff]

Result:
R : Type u
inst✝² : CommRing R
A : Type u
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ (∀ ⦃B : Type u⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
      I ^ 2 = ⊥ → Function.Bijective (Ideal.Quotient.mkₐ R I).comp) ↔
    (∀ ⦃B : Type u⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
        I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp) ∧
      ∀ ⦃B : Type u⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
        I ^ 2 = ⊥ → Function.Surjective (Ideal.Quotient.mkₐ R I).comp

Proof state:
R : Type u
inst✝² : CommRing R
A : Type u
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ (∀ ⦃B : Type u⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
      I ^ 2 = ⊥ → Function.Bijective (Ideal.Quotient.mkₐ R I).comp) ↔
    (∀ ⦃B : Type u⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
        I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp) ∧
      ∀ ⦃B : Type u⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
        I ^ 2 = ⊥ → Function.Surjective (Ideal.Quotient.mkₐ R I).comp

Tactic:
simp_rw [← forall_and, Function.Bijective]

Result:
no goals
-- Mathlib/CategoryTheory/Enriched/Ordinary/Basic.lean
@[simp]
lemma eHomWhiskerLeft_id (X Y : C) : eHomWhiskerLeft V X (𝟙 Y) = 𝟙 _

Proof state:
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y : C
⊢ eHomWhiskerLeft V X (𝟙 Y) = 𝟙 (EnrichedCategory.Hom X Y)

Tactic:
simp [eHomWhiskerLeft]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Monadic.lean
theorem forIn'_yield_eq_foldl
    (l : Array α) (f : (a : α) → a ∈ l → β → β) (init : β) :
    forIn' (m := Id) l init (fun a m b => .yield (f a m b)) =
      l.attach.foldl (fun b ⟨a, h⟩ => f a h b) init

Proof state:
α : Type u_1
β : Type u_2
l : Array α
f : (a : α) → a ∈ l → β → β
init : β
⊢ (forIn' l init fun a m b => ForInStep.yield (f a m b)) =
    foldl
      (fun b x =>
        match x with
        | ⟨a, h⟩ => f a h b)
      init l.attach

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
init : β
toList✝ : List α
f : (a : α) → a ∈ { toList := toList✝ } → β → β
⊢ (forIn' { toList := toList✝ } init fun a m b => ForInStep.yield (f a m b)) =
    foldl
      (fun b x =>
        match x with
        | ⟨a, h⟩ => f a h b)
      init { toList := toList✝ }.attach

Proof state:
case mk
α : Type u_1
β : Type u_2
init : β
toList✝ : List α
f : (a : α) → a ∈ { toList := toList✝ } → β → β
⊢ (forIn' { toList := toList✝ } init fun a m b => ForInStep.yield (f a m b)) =
    foldl
      (fun b x =>
        match x with
        | ⟨a, h⟩ => f a h b)
      init { toList := toList✝ }.attach

Tactic:
simp [List.foldl_map]

Result:
no goals
-- Mathlib/LinearAlgebra/Prod.lean
theorem snd_comp_prodAssoc :
    (LinearMap.snd R M₁ (M₂ × M₃)).comp (prodAssoc R M₁ M₂ M₃).toLinearMap =
    (LinearMap.snd R M₁ M₂).prodMap (LinearMap.id : M₃ →ₗ[R] M₃)

Proof state:
R : Type u
M₂ : Type w
M₃ : Type y
M₁ : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
⊢ LinearMap.snd R M₁ (M₂ × M₃) ∘ₗ ↑(prodAssoc R M₁ M₂ M₃) = (LinearMap.snd R M₁ M₂).prodMap LinearMap.id

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/RingTheory/Localization/Integral.lean
theorem coeffIntegerNormalization_of_not_mem_support (p : S[X]) (i : ℕ) (h : coeff p i = 0) :
    coeffIntegerNormalization M p i = 0

Proof state:
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
p : S[X]
i : ℕ
h : p.coeff i = 0
⊢ coeffIntegerNormalization M p i = 0

Tactic:
simp only [coeffIntegerNormalization, h, mem_support_iff, eq_self_iff_true, not_true, Ne,
  dif_neg, not_false_iff]

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ico_inter_Ici (a b c : α) : Ico a b ∩ Ici c = Ico (a ⊔ c) b

Proof state:
α : Type u_1
inst✝ : SemilatticeSup α
a b c : α
⊢ Ico a b ∩ Ici c = Ico (a ⊔ c) b

Tactic:
rw [← Ici_inter_Iio, ← Ici_inter_Iio, ← Ici_inter_Ici, inter_right_comm]

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Module.lean
theorem ContinuousLinearMap.hasSum {f : ι → M} (φ : M →SL[σ] M₂) {x : M}
    (hf : HasSum f x) : HasSum (fun b : ι ↦ φ (f b)) (φ x)

Proof state:
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R₂ M₂
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalSpace M₂
σ : R →+* R₂
f : ι → M
φ : M →SL[σ] M₂
x : M
hf : HasSum f x
⊢ HasSum (fun b => φ (f b)) (φ x)

Tactic:
simpa only using hf.map φ.toLinearMap.toAddMonoidHom φ.continuous

Result:
no goals
-- Mathlib/Topology/EMetricSpace/Defs.lean
theorem mem_ball_self (h : 0 < ε) : x ∈ ball x ε

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
ε : ℝ≥0∞
h : 0 < ε
⊢ x ∈ ball x ε

Tactic:
rwa [mem_ball, edist_self]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem mul_rpow_of_ne_zero {x y : ℝ≥0∞} (hx : x ≠ 0) (hy : y ≠ 0) (z : ℝ) :
    (x * y) ^ z = x ^ z * y ^ z

Proof state:
x y : ℝ≥0∞
hx : x ≠ 0
hy : y ≠ 0
z : ℝ
⊢ (x * y) ^ z = x ^ z * y ^ z

Tactic:
simp [*, mul_rpow_eq_ite]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem not_cons (x : BitVec w) (b : Bool) : ~~~(cons b x) = cons (!b) (~~~x)

Proof state:
w : Nat
x : BitVec w
b : Bool
⊢ ~~~cons b x = cons (!b) (~~~x)

Tactic:
simp [cons]

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/DyckWord.lean
lemma nest_denest (hn) : (p.denest hn).nest = p

Proof state:
p : DyckWord
hn : p.IsNested
⊢ (p.denest hn).nest = p

Tactic:
simpa [DyckWord.ext_iff] using p.cons_tail_dropLast_concat hn.1

Result:
no goals
-- Mathlib/Algebra/Homology/HomologicalComplexBiprod.lean
@[reassoc (attr := simp)]
lemma biprod_inr_snd_f (i : ι) :
    (biprod.inr : L ⟶ K ⊞ L).f i ≫ (biprod.snd : K ⊞ L ⟶ L).f i = 𝟙 _

Proof state:
C : Type u_1
ι : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
inst✝ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (L.X i)
i : ι
⊢ biprod.inr.f i ≫ biprod.snd.f i = 𝟙 (L.X i)

Tactic:
rw [← comp_f, biprod.inr_snd, id_f]

Result:
no goals
-- Mathlib/Algebra/Group/Invertible/Defs.lean
theorem invOf_mul [Monoid α] (a b : α) [Invertible a] [Invertible b] [Invertible (a * b)] :
    ⅟ (a * b) = ⅟ b * ⅟ a :=
  invOf_eq_right_inv (by simp [← mul_assoc])

Proof state:
α : Type u
inst✝³ : Monoid α
a b : α
inst✝² : Invertible a
inst✝¹ : Invertible b
inst✝ : Invertible (a * b)
⊢ a * b * (⅟b * ⅟a) = 1

Tactic:
simp [← mul_assoc]

Result:
no goals
-- Mathlib/RingTheory/Valuation/Integers.lean
lemma mem_integer_iff (r : R) : r ∈ v.integer ↔ v r ≤ 1

Proof state:
R : Type u
Γ₀ : Type v
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
r : R
⊢ r ∈ v.integer ↔ v r ≤ 1

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/Filter/Pi.lean
theorem coprodᵢ_eq_bot_iff [∀ i, Nonempty (α i)] : Filter.coprodᵢ f = ⊥ ↔ f = ⊥

Proof state:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
inst✝ : ∀ (i : ι), Nonempty (α i)
⊢ Filter.coprodᵢ f = ⊥ ↔ f = ⊥

Tactic:
simpa [funext_iff] using coprodᵢ_neBot_iff.not

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem list_map {f : α → List β} {g : α → β → σ} (hf : Primrec f) (hg : Primrec₂ g) :
    Primrec fun a => (f a).map (g a) :=
  (list_foldr hf (const []) <|
        to₂ <| list_cons.comp (hg.comp fst (fst.comp snd)) (snd.comp snd)).of_eq
    fun a => by induction f a <;> simp [*]

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → List β
g : α → β → σ
hf : Primrec f
hg : Primrec₂ g
a : α
⊢ List.foldr (fun b s => g (a, b, s).1 (a, b, s).2.1 :: (a, b, s).2.2) [] (f a) = List.map (g a) (f a)

Tactic:
induction f a <;> simp [*]

Result:
no goals
-- Mathlib/GroupTheory/OrderOfElement.lean
lemma CharP.addOrderOf_one : CharP R (addOrderOf (1 : R)) where
  cast_eq_zero_iff' n

Proof state:
R : Type u_6
inst✝ : NonAssocRing R
n : ℕ
⊢ ↑n = 0 ↔ addOrderOf 1 ∣ n

Tactic:
rw [← Nat.smul_one_eq_cast, addOrderOf_dvd_iff_nsmul_eq_zero]

Result:
no goals
-- Mathlib/RingTheory/WittVector/Basic.lean
theorem matrix_vecEmpty_coeff {R} (i j) :
    @coeff p R (Matrix.vecEmpty i) j = (Matrix.vecEmpty i : ℕ → R) j

Proof state:
p : ℕ
R : Type u_5
i : Fin 0
j : ℕ
⊢ (![] i).coeff j = ![] i j

Tactic:
rcases i with ⟨_ | _ | _ | _ | i_val, ⟨⟩⟩

Result:
no goals
-- Mathlib/Data/Finset/Prod.lean
theorem product_eq_biUnion [DecidableEq (α × β)] (s : Finset α) (t : Finset β) :
    s ×ˢ t = s.biUnion fun a => t.image fun b => (a, b) :=
  ext fun ⟨x, y⟩ => by
    simp only [mem_product, mem_biUnion, mem_image, exists_prop, Prod.mk.inj_iff, and_left_comm,
      exists_and_left, exists_eq_right, exists_eq_left]

Proof state:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq (α × β)
s : Finset α
t : Finset β
x✝ : α × β
x : α
y : β
⊢ (x, y) ∈ s ×ˢ t ↔ (x, y) ∈ s.biUnion fun a => image (fun b => (a, b)) t

Tactic:
simp only [mem_product, mem_biUnion, mem_image, exists_prop, Prod.mk.inj_iff, and_left_comm,
  exists_and_left, exists_eq_right, exists_eq_left]

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem Surjective.preimage_subset_preimage_iff {s t : Set β} (hf : Surjective f) :
    f ⁻¹' s ⊆ f ⁻¹' t ↔ s ⊆ t

Proof state:
case hs
α : Type u_1
β : Type u_2
f : α → β
s t : Set β
hf : Surjective f
⊢ s ⊆ range f

Tactic:
rw [hf.range_eq]

Result:
case hs
α : Type u_1
β : Type u_2
f : α → β
s t : Set β
hf : Surjective f
⊢ s ⊆ univ

Proof state:
case hs
α : Type u_1
β : Type u_2
f : α → β
s t : Set β
hf : Surjective f
⊢ s ⊆ univ

Tactic:
apply subset_univ

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s t : Set β
hf : Surjective f
⊢ f ⁻¹' s ⊆ f ⁻¹' t ↔ s ⊆ t

Tactic:
apply Set.preimage_subset_preimage_iff

Result:
case hs
α : Type u_1
β : Type u_2
f : α → β
s t : Set β
hf : Surjective f
⊢ s ⊆ range f
-- Mathlib/AlgebraicTopology/DoldKan/FunctorGamma.lean
theorem Obj.map_on_summand' {Δ Δ' : SimplexCategoryᵒᵖ} (A : Splitting.IndexSet Δ) (θ : Δ ⟶ Δ') :
    ((splitting K).cofan Δ).inj A ≫ (obj K).map θ =
      Obj.Termwise.mapMono K (image.ι (θ.unop ≫ A.e)) ≫
        ((splitting K).cofan Δ').inj (A.pull θ)

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K : ChainComplex C ℕ
inst✝ : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
⊢ ((splitting K).cofan Δ).inj A ≫ (obj K).map θ =
    Termwise.mapMono K (image.ι (θ.unop ≫ A.e)) ≫ ((splitting K).cofan Δ').inj (A.pull θ)

Tactic:
apply Obj.map_on_summand

Result:
case fac
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K : ChainComplex C ℕ
inst✝ : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
⊢ factorThruImage (θ.unop ≫ A.e) ≫ image.ι (θ.unop ≫ A.e) = θ.unop ≫ A.e

Proof state:
case fac
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K : ChainComplex C ℕ
inst✝ : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
⊢ factorThruImage (θ.unop ≫ A.e) ≫ image.ι (θ.unop ≫ A.e) = θ.unop ≫ A.e

Tactic:
apply image.fac

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem or_eq_true_iff : ∀ {x y : Bool}, (x || y) = true ↔ x = true ∨ y = true

Proof state:
⊢ ∀ {x y : Bool}, (x || y) = true ↔ x = true ∨ y = true

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem _root_.MeasureTheory.Integrable.hasSum_intervalIntegral_comp_add_int (hfi : Integrable f) :
    HasSum (fun n : ℤ => ∫ x in (0 : ℝ)..(1 : ℝ), f (x + n)) (∫ x, f x)

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
hfi : Integrable f volume
⊢ HasSum (fun n => ∫ (x : ℝ) in 0 ..1, f (x + ↑n)) (∫ (x : ℝ), f x)

Tactic:
simpa only [integral_comp_add_right, zero_add, add_comm (1 : ℝ)] using
  hfi.hasSum_intervalIntegral 0

Result:
no goals
-- Mathlib/Data/Matroid/Map.lean
lemma restrictSubtype_dual' (hM : M.E = E) : (M.restrictSubtype E)✶ = M✶.restrictSubtype E

Proof state:
α : Type u_1
E : Set α
M : Matroid α
hM : M.E = E
⊢ (M.restrictSubtype E)✶ = M✶.restrictSubtype E

Tactic:
rw [← hM, restrictSubtype_dual]

Result:
no goals
-- Mathlib/GroupTheory/Torsion.lean
theorem ExponentExists.isTorsion (h : ExponentExists G) : IsTorsion G := fun g => by
  obtain ⟨n, npos, hn⟩ := h
  exact isOfFinOrder_iff_pow_eq_one.mpr ⟨n, npos, hn g⟩

Proof state:
G : Type u_1
inst✝ : Group G
h : ExponentExists G
g : G
⊢ IsOfFinOrder g

Tactic:
obtain ⟨n, npos, hn⟩ := h

Result:
case intro.intro
G : Type u_1
inst✝ : Group G
g : G
n : ℕ
npos : 0 < n
hn : ∀ (g : G), g ^ n = 1
⊢ IsOfFinOrder g

Proof state:
case intro.intro
G : Type u_1
inst✝ : Group G
g : G
n : ℕ
npos : 0 < n
hn : ∀ (g : G), g ^ n = 1
⊢ IsOfFinOrder g

Tactic:
exact isOfFinOrder_iff_pow_eq_one.mpr ⟨n, npos, hn g⟩

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Group.lean
theorem multipliable_iff_cauchySeq_finset [CompleteSpace α] {f : β → α} :
    Multipliable f ↔ CauchySeq fun s : Finset β ↦ ∏ b ∈ s, f b

Proof state:
α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : UniformSpace α
inst✝ : CompleteSpace α
f : β → α
⊢ Multipliable f ↔ CauchySeq fun s => ∏ b ∈ s, f b

Tactic:
exact cauchy_map_iff_exists_tendsto.symm

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : UniformSpace α
inst✝ : CompleteSpace α
f : β → α
⊢ Multipliable f ↔ CauchySeq fun s => ∏ b ∈ s, f b

Tactic:
classical exact cauchy_map_iff_exists_tendsto.symm

Result:
no goals
-- Mathlib/CategoryTheory/Adhesive.lean
theorem adhesive_of_preserves_and_reflects_isomorphism (F : C ⥤ D)
    [Adhesive D] [HasPullbacks C] [HasPushouts C]
    [PreservesLimitsOfShape WalkingCospan F]
    [PreservesColimitsOfShape WalkingSpan F]
    [F.ReflectsIsomorphisms] :
    Adhesive C

Proof state:
C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u''
inst✝⁶ : Category.{v'', u''} D
F : C ⥤ D
inst✝⁵ : Adhesive D
inst✝⁴ : HasPullbacks C
inst✝³ : HasPushouts C
inst✝² : PreservesLimitsOfShape WalkingCospan F
inst✝¹ : PreservesColimitsOfShape WalkingSpan F
inst✝ : F.ReflectsIsomorphisms
this✝ : ReflectsLimitsOfShape WalkingCospan F
this : ReflectsColimitsOfShape WalkingSpan F
⊢ Adhesive C

Tactic:
exact adhesive_of_preserves_and_reflects F

Result:
no goals

Proof state:
C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u''
inst✝⁶ : Category.{v'', u''} D
F : C ⥤ D
inst✝⁵ : Adhesive D
inst✝⁴ : HasPullbacks C
inst✝³ : HasPushouts C
inst✝² : PreservesLimitsOfShape WalkingCospan F
inst✝¹ : PreservesColimitsOfShape WalkingSpan F
inst✝ : F.ReflectsIsomorphisms
this : ReflectsLimitsOfShape WalkingCospan F
⊢ Adhesive C

Tactic:
haveI : ReflectsColimitsOfShape WalkingSpan F :=
  reflectsColimitsOfShape_of_reflectsIsomorphisms

Result:
C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u''
inst✝⁶ : Category.{v'', u''} D
F : C ⥤ D
inst✝⁵ : Adhesive D
inst✝⁴ : HasPullbacks C
inst✝³ : HasPushouts C
inst✝² : PreservesLimitsOfShape WalkingCospan F
inst✝¹ : PreservesColimitsOfShape WalkingSpan F
inst✝ : F.ReflectsIsomorphisms
this✝ : ReflectsLimitsOfShape WalkingCospan F
this : ReflectsColimitsOfShape WalkingSpan F
⊢ Adhesive C

Proof state:
C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u''
inst✝⁶ : Category.{v'', u''} D
F : C ⥤ D
inst✝⁵ : Adhesive D
inst✝⁴ : HasPullbacks C
inst✝³ : HasPushouts C
inst✝² : PreservesLimitsOfShape WalkingCospan F
inst✝¹ : PreservesColimitsOfShape WalkingSpan F
inst✝ : F.ReflectsIsomorphisms
⊢ Adhesive C

Tactic:
haveI : ReflectsLimitsOfShape WalkingCospan F :=
  reflectsLimitsOfShape_of_reflectsIsomorphisms

Result:
C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u''
inst✝⁶ : Category.{v'', u''} D
F : C ⥤ D
inst✝⁵ : Adhesive D
inst✝⁴ : HasPullbacks C
inst✝³ : HasPushouts C
inst✝² : PreservesLimitsOfShape WalkingCospan F
inst✝¹ : PreservesColimitsOfShape WalkingSpan F
inst✝ : F.ReflectsIsomorphisms
this : ReflectsLimitsOfShape WalkingCospan F
⊢ Adhesive C
-- Mathlib/Algebra/Module/Submodule/Equiv.lean
theorem apply_ofBijective_symm_apply [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {h}
    (x : M₂) : f ((ofBijective f h).symm x) = x

Proof state:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
f : M →ₛₗ[σ₁₂] M₂
inst✝¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ₁₂
h : Bijective ⇑f
x : M₂
⊢ f ((ofBijective f h).symm x) = x

Tactic:
rw [← ofBijective_apply f ((ofBijective f h).symm x), apply_symm_apply]

Result:
no goals
-- Mathlib/Topology/Category/TopCat/Limits/Basic.lean
lemma isOpen_iff_of_isColimit (X : Set c.pt) :
    IsOpen X ↔ ∀ (j : J), IsOpen (c.ι.app j ⁻¹' X)

Proof state:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cocone F
hc : IsColimit c
X : Set ↑c.pt
⊢ TopologicalSpace.IsOpen X ↔ ∀ (j : J), IsOpen (⇑(ConcreteCategory.hom (c.ι.app j)) ⁻¹' X)

Tactic:
simp only [← isOpen_coinduced]

Result:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cocone F
hc : IsColimit c
X : Set ↑c.pt
⊢ TopologicalSpace.IsOpen X ↔ ∀ (j : J), IsOpen X

Proof state:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cocone F
hc : IsColimit c
X : Set ↑c.pt
⊢ IsOpen X ↔ ∀ (j : J), IsOpen (⇑(ConcreteCategory.hom (c.ι.app j)) ⁻¹' X)

Tactic:
trans (⨆ (j : J), (F.obj j).str.coinduced (c.ι.app j)).IsOpen X

Result:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cocone F
hc : IsColimit c
X : Set ↑c.pt
⊢ IsOpen X ↔ TopologicalSpace.IsOpen X

J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cocone F
hc : IsColimit c
X : Set ↑c.pt
⊢ TopologicalSpace.IsOpen X ↔ ∀ (j : J), IsOpen (⇑(ConcreteCategory.hom (c.ι.app j)) ⁻¹' X)

Proof state:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cocone F
hc : IsColimit c
X : Set ↑c.pt
⊢ IsOpen X ↔ TopologicalSpace.IsOpen X

Tactic:
rw [← coinduced_of_isColimit c hc, isOpen_fold]

Result:
no goals

Proof state:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cocone F
hc : IsColimit c
X : Set ↑c.pt
⊢ TopologicalSpace.IsOpen X ↔ ∀ (j : J), IsOpen X

Tactic:
apply isOpen_iSup_iff

Result:
no goals