harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem MonoidHom.map_finprod_of_preimage_one (f : M →* N) (hf : ∀ x, f x = 1 → x = 1) (g : α → M) :
    f (∏ᶠ i, g i) = ∏ᶠ i, f (g i)

Proof state:
case neg
M : Type u_2
N : Type u_3
α : Sort u_4
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : M →* N
hf : ∀ (x : M), f x = 1 → x = 1
g : α → M
hg : ¬(mulSupport (g ∘ PLift.down)).Finite
⊢ f (∏ᶠ (i : α), g i) = ∏ᶠ (i : α), f (g i)

Tactic:
rw [finprod, dif_neg, f.map_one, finprod, dif_neg]

Result:
case neg.hnc
M : Type u_2
N : Type u_3
α : Sort u_4
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : M →* N
hf : ∀ (x : M), f x = 1 → x = 1
g : α → M
hg : ¬(mulSupport (g ∘ PLift.down)).Finite
⊢ ¬(mulSupport ((fun i => f (g i)) ∘ PLift.down)).Finite

case neg.hnc
M : Type u_2
N : Type u_3
α : Sort u_4
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : M →* N
hf : ∀ (x : M), f x = 1 → x = 1
g : α → M
hg : ¬(mulSupport (g ∘ PLift.down)).Finite
⊢ ¬(mulSupport ((fun i => g i) ∘ PLift.down)).Finite

Proof state:
case pos
M : Type u_2
N : Type u_3
α : Sort u_4
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : M →* N
hf : ∀ (x : M), f x = 1 → x = 1
g : α → M
hg : (mulSupport (g ∘ PLift.down)).Finite
⊢ f (∏ᶠ (i : α), g i) = ∏ᶠ (i : α), f (g i)

Tactic:
exact f.map_finprod_plift g hg

Result:
no goals

Proof state:
case neg.hnc
M : Type u_2
N : Type u_3
α : Sort u_4
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : M →* N
hf : ∀ (x : M), f x = 1 → x = 1
g : α → M
hg : ¬(mulSupport (g ∘ PLift.down)).Finite
⊢ ¬(mulSupport ((fun i => f (g i)) ∘ PLift.down)).Finite

case neg.hnc
M : Type u_2
N : Type u_3
α : Sort u_4
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : M →* N
hf : ∀ (x : M), f x = 1 → x = 1
g : α → M
hg : ¬(mulSupport (g ∘ PLift.down)).Finite
⊢ ¬(mulSupport ((fun i => g i) ∘ PLift.down)).Finite

Tactic:
exacts [Infinite.mono (fun x hx => mt (hf (g x.down)) hx) hg, hg]

Result:
no goals

Proof state:
M : Type u_2
N : Type u_3
α : Sort u_4
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : M →* N
hf : ∀ (x : M), f x = 1 → x = 1
g : α → M
⊢ f (∏ᶠ (i : α), g i) = ∏ᶠ (i : α), f (g i)

Tactic:
by_cases hg : (mulSupport <| g ∘ PLift.down).Finite

Result:
case pos
M : Type u_2
N : Type u_3
α : Sort u_4
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : M →* N
hf : ∀ (x : M), f x = 1 → x = 1
g : α → M
hg : (mulSupport (g ∘ PLift.down)).Finite
⊢ f (∏ᶠ (i : α), g i) = ∏ᶠ (i : α), f (g i)

case neg
M : Type u_2
N : Type u_3
α : Sort u_4
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : M →* N
hf : ∀ (x : M), f x = 1 → x = 1
g : α → M
hg : ¬(mulSupport (g ∘ PLift.down)).Finite
⊢ f (∏ᶠ (i : α), g i) = ∏ᶠ (i : α), f (g i)
-- Mathlib/Algebra/Algebra/Operations.lean
theorem map_op_pow (n : ℕ) :
    map (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ) (M ^ n) =
      map (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ) M ^ n

Proof state:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M : Submodule R A
n : ℕ
⊢ map (↑(opLinearEquiv R)) (M ^ n) = map (↑(opLinearEquiv R)) M ^ n

Tactic:
rw [map_equiv_eq_comap_symm, map_equiv_eq_comap_symm, comap_unop_pow]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem norm_measure_zero (f : Lp E p (0 : MeasureTheory.Measure α)) : ‖f‖ = 0

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
inst✝ : NormedAddCommGroup E
f : ↥(Lp E p 0)
⊢ ‖f‖ = 0

Tactic:
simp only [norm_def, eLpNorm_measure_zero, ENNReal.zero_toReal]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Raw.lean
theorem get!_eq [BEq α] [Hashable α] [LawfulBEq α] {m : Raw α β} (h : m.WF) {a : α}
    [Inhabited (β a)] : m.get! a = Raw₀.get! ⟨m, h.size_buckets_pos⟩ a

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
m : Raw α β
h : m.WF
a : α
inst✝ : Inhabited (β a)
⊢ m.get! a = Raw₀.get! ⟨m, ⋯⟩ a

Tactic:
simp [Raw.get!, h.size_buckets_pos]

Result:
no goals
-- Mathlib/FieldTheory/RatFunc/AsPolynomial.lean
theorem eval_X : eval f a X = a

Proof state:
K : Type u
inst✝¹ : Field K
L : Type u
inst✝ : Field L
f : K →+* L
a : L
⊢ eval f a X = a

Tactic:
simp [eval]

Result:
no goals
-- Mathlib/Data/Set/Pointwise/SMul.lean
@[to_additive] lemma mul_pair (s : Set α) (a b : α) : s * {a, b} = s <• a ∪ s <• b

Proof state:
α : Type u_2
inst✝ : Mul α
s : Set α
a b : α
⊢ (fun x => x * a) '' s ∪ (fun x => x * b) '' s = s <• a ∪ s <• b

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_2
inst✝ : Mul α
s : Set α
a b : α
⊢ s * {a, b} = s <• a ∪ s <• b

Tactic:
rw [insert_eq, mul_union, mul_singleton, mul_singleton]

Result:
α : Type u_2
inst✝ : Mul α
s : Set α
a b : α
⊢ (fun x => x * a) '' s ∪ (fun x => x * b) '' s = s <• a ∪ s <• b
-- Mathlib/Algebra/Homology/ShortComplex/PreservesHomology.lean
lemma RightHomologyData.mapRightHomologyIso_eq [S.HasRightHomology]
    [F.PreservesRightHomologyOf S] :
    S.mapRightHomologyIso F = (hr.map F).rightHomologyIso ≪≫
      F.mapIso hr.rightHomologyIso.symm

Proof state:
case w
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Category.{u_4, u_2} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S : ShortComplex C
hr : S.RightHomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : S.HasRightHomology
inst✝ : F.PreservesRightHomologyOf S
⊢ rightHomologyMap' (𝟙 (S.map F)) (S.map F).rightHomologyData (S.rightHomologyData.map F) =
    rightHomologyMap' (𝟙 (S.map F)) (S.map F).rightHomologyData (hr.map F) ≫
      F.map (rightHomologyMap' (𝟙 S) hr S.rightHomologyData)

Tactic:
simp only [map_rightHomologyMap', ← rightHomologyMap'_comp, Functor.map_id, comp_id,
  Functor.mapShortComplex_obj]

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Category.{u_4, u_2} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S : ShortComplex C
hr : S.RightHomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : S.HasRightHomology
inst✝ : F.PreservesRightHomologyOf S
⊢ S.mapRightHomologyIso F = (hr.map F).rightHomologyIso ≪≫ F.mapIso hr.rightHomologyIso.symm

Tactic:
ext

Result:
case w
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Category.{u_4, u_2} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S : ShortComplex C
hr : S.RightHomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : S.HasRightHomology
inst✝ : F.PreservesRightHomologyOf S
⊢ (S.mapRightHomologyIso F).hom = ((hr.map F).rightHomologyIso ≪≫ F.mapIso hr.rightHomologyIso.symm).hom

Proof state:
case w
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Category.{u_4, u_2} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S : ShortComplex C
hr : S.RightHomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : S.HasRightHomology
inst✝ : F.PreservesRightHomologyOf S
⊢ (S.mapRightHomologyIso F).hom = ((hr.map F).rightHomologyIso ≪≫ F.mapIso hr.rightHomologyIso.symm).hom

Tactic:
dsimp [mapRightHomologyIso, rightHomologyIso]

Result:
case w
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Category.{u_4, u_2} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S : ShortComplex C
hr : S.RightHomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : S.HasRightHomology
inst✝ : F.PreservesRightHomologyOf S
⊢ rightHomologyMap' (𝟙 (S.map F)) (S.map F).rightHomologyData (S.rightHomologyData.map F) =
    rightHomologyMap' (𝟙 (S.map F)) (S.map F).rightHomologyData (hr.map F) ≫
      F.map (rightHomologyMap' (𝟙 S) hr S.rightHomologyData)
-- Mathlib/LinearAlgebra/Matrix/Charpoly/Basic.lean
@[simp]
lemma charpoly_fromBlocks_zero₁₂ :
    (fromBlocks M₁₁ 0 M₂₁ M₂₂).charpoly = (M₁₁.charpoly * M₂₂.charpoly)

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
m : Type u_3
n : Type u_4
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Fintype n
M₁₁ : Matrix m m R
M₂₁ : Matrix n m R
M₂₂ : Matrix n n R
⊢ (fromBlocks M₁₁ 0 M₂₁ M₂₂).charpoly = M₁₁.charpoly * M₂₂.charpoly

Tactic:
simp only [charpoly, charmatrix_fromBlocks, Matrix.map_zero _ (Polynomial.C_0), neg_zero,
  det_fromBlocks_zero₁₂]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toInt_setWidth (x : BitVec w) :
    (x.setWidth v).toInt = Int.bmod x.toNat (2^v)

Proof state:
w v : Nat
x : BitVec w
⊢ (setWidth v x).toInt = (↑x.toNat).bmod (2 ^ v)

Tactic:
simp [toInt_eq_toNat_bmod, toNat_setWidth, Int.emod_bmod]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma polynomialX_eq : W'.polynomialX =
    C W'.a₁ * X 1 * X 2 - (C 3 * X 0 ^ 2 + C (2 * W'.a₂) * X 0 * X 2 + C W'.a₄ * X 2 ^ 2)

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
⊢ W'.polynomialX = C W'.a₁ * X y * X z - (C 3 * X x ^ 2 + C (2 * W'.a₂) * X x * X z + C W'.a₄ * X z ^ 2)

Tactic:
rw [polynomialX, polynomial]

Result:
R : Type r
inst✝ : CommRing R
W' : Projective R
⊢ (pderiv x)
      (X y ^ 2 * X z + C W'.a₁ * X x * X y * X z + C W'.a₃ * X y * X z ^ 2 -
        (X x ^ 3 + C W'.a₂ * X x ^ 2 * X z + C W'.a₄ * X x * X z ^ 2 + C W'.a₆ * X z ^ 3)) =
    C W'.a₁ * X y * X z - (C 3 * X x ^ 2 + C (2 * W'.a₂) * X x * X z + C W'.a₄ * X z ^ 2)

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
⊢ (pderiv x)
      (X y ^ 2 * X z + C W'.a₁ * X x * X y * X z + C W'.a₃ * X y * X z ^ 2 -
        (X x ^ 3 + C W'.a₂ * X x ^ 2 * X z + C W'.a₄ * X x * X z ^ 2 + C W'.a₆ * X z ^ 3)) =
    C W'.a₁ * X y * X z - (C 3 * X x ^ 2 + C (2 * W'.a₂) * X x * X z + C W'.a₄ * X z ^ 2)

Tactic:
pderiv_simp

Result:
R : Type r
inst✝ : CommRing R
W' : Projective R
⊢ ↑2 * X y ^ (2 - 1) * 0 * X z + X y ^ 2 * 0 +
          (((0 * X x + C W'.a₁ * 1) * X y + C W'.a₁ * X x * 0) * X z + C W'.a₁ * X x * X y * 0) +
        ((0 * X y + C W'.a₃ * 0) * X z ^ 2 + C W'.a₃ * X y * (↑2 * X z ^ (2 - 1) * 0)) -
      (↑3 * X x ^ (3 - 1) * 1 + ((0 * X x ^ 2 + C W'.a₂ * (↑2 * X x ^ (2 - 1) * 1)) * X z + C W'.a₂ * X x ^ 2 * 0) +
          ((0 * X x + C W'.a₄ * 1) * X z ^ 2 + C W'.a₄ * X x * (↑2 * X z ^ (2 - 1) * 0)) +
        (0 * X z ^ 3 + C W'.a₆ * (↑3 * X z ^ (3 - 1) * 0))) =
    C W'.a₁ * X y * X z - (3 * X x ^ 2 + 2 * C W'.a₂ * X x * X z + C W'.a₄ * X z ^ 2)

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
⊢ ↑2 * X y ^ (2 - 1) * 0 * X z + X y ^ 2 * 0 +
          (((0 * X x + C W'.a₁ * 1) * X y + C W'.a₁ * X x * 0) * X z + C W'.a₁ * X x * X y * 0) +
        ((0 * X y + C W'.a₃ * 0) * X z ^ 2 + C W'.a₃ * X y * (↑2 * X z ^ (2 - 1) * 0)) -
      (↑3 * X x ^ (3 - 1) * 1 + ((0 * X x ^ 2 + C W'.a₂ * (↑2 * X x ^ (2 - 1) * 1)) * X z + C W'.a₂ * X x ^ 2 * 0) +
          ((0 * X x + C W'.a₄ * 1) * X z ^ 2 + C W'.a₄ * X x * (↑2 * X z ^ (2 - 1) * 0)) +
        (0 * X z ^ 3 + C W'.a₆ * (↑3 * X z ^ (3 - 1) * 0))) =
    C W'.a₁ * X y * X z - (3 * X x ^ 2 + 2 * C W'.a₂ * X x * X z + C W'.a₄ * X z ^ 2)

Tactic:
ring1

Result:
no goals
-- Mathlib/Algebra/Group/Indicator.lean
theorem mulIndicator_const_preimage_eq_union (U : Set α) (s : Set M) (a : M) [Decidable (a ∈ s)]
    [Decidable ((1 : M) ∈ s)] : (U.mulIndicator fun _ => a) ⁻¹' s =
      (if a ∈ s then U else ∅) ∪ if (1 : M) ∈ s then Uᶜ else ∅

Proof state:
α : Type u_1
M : Type u_3
inst✝² : One M
U : Set α
s : Set M
a : M
inst✝¹ : Decidable (a ∈ s)
inst✝ : Decidable (1 ∈ s)
⊢ U.ite (if a ∈ s then univ else ∅) (if 1 ∈ s then univ else ∅) = (if a ∈ s then U else ∅) ∪ if 1 ∈ s then Uᶜ else ∅

Tactic:
split_ifs <;> simp [← compl_eq_univ_diff]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_3
inst✝² : One M
U : Set α
s : Set M
a : M
inst✝¹ : Decidable (a ∈ s)
inst✝ : Decidable (1 ∈ s)
⊢ (U.mulIndicator fun x => a) ⁻¹' s = (if a ∈ s then U else ∅) ∪ if 1 ∈ s then Uᶜ else ∅

Tactic:
rw [mulIndicator_preimage, preimage_one, preimage_const]

Result:
α : Type u_1
M : Type u_3
inst✝² : One M
U : Set α
s : Set M
a : M
inst✝¹ : Decidable (a ∈ s)
inst✝ : Decidable (1 ∈ s)
⊢ U.ite (if a ∈ s then univ else ∅) (if 1 ∈ s then univ else ∅) = (if a ∈ s then U else ∅) ∪ if 1 ∈ s then Uᶜ else ∅
-- Mathlib/CategoryTheory/Generator/Presheaf.lean
@[reassoc]
lemma freeYonedaHomEquiv_comp {X : C} {M : A} {F G : Cᵒᵖ ⥤ A}
    (α : freeYoneda X M ⟶ F) (f : F ⟶ G) :
    freeYonedaHomEquiv (α ≫ f) = freeYonedaHomEquiv α ≫ f.app (op X)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : HasCoproducts A
X : C
M : A
F G : Cᵒᵖ ⥤ A
α : freeYoneda X M ⟶ F
f : F ⟶ G
⊢ freeYonedaHomEquiv (α ≫ f) = freeYonedaHomEquiv α ≫ f.app (op X)

Tactic:
simp [freeYonedaHomEquiv]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Equiv.lean
lemma optionEquivRight_X_some (x : S₁) : optionEquivRight R S₁ (X (some x)) = X x

Proof state:
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
x : S₁
⊢ (optionEquivRight R S₁) (X (Option.some x)) = X x

Tactic:
simp [optionEquivRight_apply, aeval_X]

Result:
no goals
-- Mathlib/Data/Bool/Count.lean
theorem two_mul_count_bool_of_even (hl : Chain' (· ≠ ·) l) (h2 : Even (length l)) (b : Bool) :
    2 * count b l = length l

Proof state:
l : List Bool
hl : Chain' (fun x1 x2 => x1 ≠ x2) l
h2 : Even l.length
b : Bool
⊢ 2 * count b l = l.length

Tactic:
rw [← count_not_add_count l b, hl.count_not_eq_count h2, two_mul]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/LinearMap.lean
theorem rank_comp_le_right (g : V →ₗ[K] V') (f : V' →ₗ[K] V'₁) : rank (f.comp g) ≤ rank g

Proof state:
K : Type u
V : Type v
V' V'₁ : Type v'
inst✝⁶ : Ring K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V'
inst✝² : Module K V'
inst✝¹ : AddCommGroup V'₁
inst✝ : Module K V'₁
g : V →ₗ[K] V'
f : V' →ₗ[K] V'₁
⊢ (f ∘ₗ g).rank ≤ g.rank

Tactic:
simpa only [Cardinal.lift_id] using lift_rank_comp_le_right g f

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
lemma pred_succAbove (x : Fin n) (y : Fin (n + 1)) (h : y ≤ castSucc x)
    (h' := Fin.ne_zero_of_lt <| (lt_succAbove_iff_le_castSucc ..).2 h) :
    (y.succAbove x).pred h' = x

Proof state:
n : ℕ
x : Fin n
y : Fin (n + 1)
h : y ≤ x.castSucc
h' : optParam (y.succAbove x ≠ 0) ⋯
⊢ (y.succAbove x).pred h' = x

Tactic:
simp only [succAbove_of_le_castSucc _ _ h, pred_succ]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKeyD_modify (h : m.1.WF) {k k' fallback : α} {f : β → β} :
    (Const.modify m k f).getKeyD k' fallback =
      if k == k' then
        if m.contains k then k else fallback
      else
        m.getKeyD k' fallback

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
h : m.val.WF
k k' fallback : α
f : β → β
⊢ (modify m k f).getKeyD k' fallback =
    if (k == k') = true then if m.contains k = true then k else fallback else m.getKeyD k' fallback

Tactic:
simp_to_model [Const.modify] using List.Const.getKeyD_modifyKey

Result:
no goals
-- Mathlib/RingTheory/Localization/Defs.lean
theorem add_mk (a b c d) : (mk a b : Localization M) + mk c d =
    mk ((b : R) * c + (d : R) * a) (b * d)

Proof state:
R : Type u_1
inst✝ : CommSemiring R
M : Submonoid R
a : R
b : ↥M
c : R
d : ↥M
⊢ mk a b + mk c d = mk (↑d * a + ↑b * c) (d * b)

Tactic:
exact OreLocalization.oreDiv_add_oreDiv

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommSemiring R
M : Submonoid R
a : R
b : ↥M
c : R
d : ↥M
⊢ mk a b + mk c d = mk (↑b * c + ↑d * a) (b * d)

Tactic:
rw [add_comm (b * c) (d * a), mul_comm b d]

Result:
R : Type u_1
inst✝ : CommSemiring R
M : Submonoid R
a : R
b : ↥M
c : R
d : ↥M
⊢ mk a b + mk c d = mk (↑d * a + ↑b * c) (d * b)
-- Mathlib/CategoryTheory/Galois/Decomposition.lean
theorem has_decomp_connected_components' (X : C) :
    ∃ (ι : Type) (_ : Finite ι) (f : ι → C) (_ : ∐ f ≅ X), ∀ i, IsConnected (f i)

Proof state:
case intro.intro.intro.intro.intro
C : Type u₁
inst✝¹ : Category.{u₂, u₁} C
inst✝ : GaloisCategory C
X : C
ι : Type
f : ι → C
g : (i : ι) → f i ⟶ X
hl : IsColimit (Cofan.mk X g)
hc : ∀ (i : ι), IsConnected (f i)
hf : Finite ι
⊢ ∃ ι, ∃ (x : Finite ι), ∃ f x, ∀ (i : ι), IsConnected (f i)

Tactic:
exact ⟨ι, hf, f, colimit.isoColimitCocone ⟨Cofan.mk X g, hl⟩, hc⟩

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{u₂, u₁} C
inst✝ : GaloisCategory C
X : C
⊢ ∃ ι, ∃ (x : Finite ι), ∃ f x, ∀ (i : ι), IsConnected (f i)

Tactic:
obtain ⟨ι, f, g, hl, hc, hf⟩ := has_decomp_connected_components X

Result:
case intro.intro.intro.intro.intro
C : Type u₁
inst✝¹ : Category.{u₂, u₁} C
inst✝ : GaloisCategory C
X : C
ι : Type
f : ι → C
g : (i : ι) → f i ⟶ X
hl : IsColimit (Cofan.mk X g)
hc : ∀ (i : ι), IsConnected (f i)
hf : Finite ι
⊢ ∃ ι, ∃ (x : Finite ι), ∃ f x, ∀ (i : ι), IsConnected (f i)
-- Mathlib/Algebra/GroupWithZero/Units/Basic.lean
theorem exists0' {p : ∀ g : G₀, g ≠ 0 → Prop} :
    (∃ (g : G₀) (hg : g ≠ 0), p g hg) ↔ ∃ g : G₀ˣ, p g g.ne_zero :=
  Iff.trans (by simp_rw [val_mk0]) exists0.symm

Proof state:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
p : (g : G₀) → g ≠ 0 → Prop
⊢ (∃ g hg, p g hg) ↔ ∃ g hg, p ↑(mk0 g hg) ⋯

Tactic:
simp_rw [val_mk0]

Result:
no goals
-- Mathlib/Data/Holor.lean
theorem cprankMax_1 [Monoid α] [AddMonoid α] {x : Holor α ds} (h : CPRankMax1 x) :
    CPRankMax 1 x

Proof state:
α : Type
ds : List ℕ
inst✝¹ : Monoid α
inst✝ : AddMonoid α
x : Holor α ds
h : x.CPRankMax1
h' : CPRankMax (0 + 1) (x + 0)
⊢ CPRankMax 1 x

Tactic:
rwa [zero_add, add_zero] at h'

Result:
no goals

Proof state:
α : Type
ds : List ℕ
inst✝¹ : Monoid α
inst✝ : AddMonoid α
x : Holor α ds
h : x.CPRankMax1
⊢ CPRankMax 1 x

Tactic:
have h' := CPRankMax.succ 0 x 0 h CPRankMax.zero

Result:
α : Type
ds : List ℕ
inst✝¹ : Monoid α
inst✝ : AddMonoid α
x : Holor α ds
h : x.CPRankMax1
h' : CPRankMax (0 + 1) (x + 0)
⊢ CPRankMax 1 x
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Raw.lean
theorem Const.getThenInsertIfNew?_fst_eq [BEq α] [Hashable α] {m : Raw α (fun _ => β)} (h : m.WF)
    {a : α} {b : β} : (Raw.Const.getThenInsertIfNew? m a b).1 =
      (Raw₀.Const.getThenInsertIfNew? ⟨m, h.size_buckets_pos⟩ a b).1

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw α fun x => β
h : m.WF
a : α
b : β
⊢ (Raw.Const.getThenInsertIfNew? m a b).fst = (Raw₀.Const.getThenInsertIfNew? ⟨m, ⋯⟩ a b).fst

Tactic:
simp [Raw.Const.getThenInsertIfNew?, h.size_buckets_pos]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem findIdx?_eq_some_le_of_findIdx?_eq_some {xs : Array α} {p q : α → Bool} (w : ∀ x ∈ xs, p x → q x) {i : Nat}
    (h : xs.findIdx? p = some i) : ∃ j, j ≤ i ∧ xs.findIdx? q = some j

Proof state:
case mk
α : Type u_1
p q : α → Bool
i : Nat
xs : List α
w : ∀ (x : α), x ∈ { toList := xs } → p x = true → q x = true
h : findIdx? p { toList := xs } = some i
⊢ ∃ j, j ≤ i ∧ findIdx? q { toList := xs } = some j

Tactic:
simp [List.findIdx?_eq_some_le_of_findIdx?_eq_some (by simpa using w) (by simpa using h)]

Result:
no goals

Proof state:
α : Type u_1
xs : Array α
p q : α → Bool
w : ∀ (x : α), x ∈ xs → p x = true → q x = true
i : Nat
h : findIdx? p xs = some i
⊢ ∃ j, j ≤ i ∧ findIdx? q xs = some j

Tactic:
rcases xs with ⟨xs⟩

Result:
case mk
α : Type u_1
p q : α → Bool
i : Nat
xs : List α
w : ∀ (x : α), x ∈ { toList := xs } → p x = true → q x = true
h : findIdx? p { toList := xs } = some i
⊢ ∃ j, j ≤ i ∧ findIdx? q { toList := xs } = some j

Proof state:
α : Type u_1
p q : α → Bool
i : Nat
xs : List α
w : ∀ (x : α), x ∈ { toList := xs } → p x = true → q x = true
h : findIdx? p { toList := xs } = some i
⊢ ∀ (x : ?m.94172), x ∈ ?m.94173 → ?m.94174 x = true → ?m.94175 x = true

Tactic:
simpa using w

Result:
no goals

Proof state:
α : Type u_1
p q : α → Bool
i : Nat
xs : List α
w : ∀ (x : α), x ∈ { toList := xs } → p x = true → q x = true
h : findIdx? p { toList := xs } = some i
⊢ List.findIdx? p xs = some ?m.94177

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean
theorem adjMatrix_mulVec_apply [NonAssocSemiring α] (v : V) (vec : V → α) :
    (G.adjMatrix α *ᵥ vec) v = ∑ u ∈ G.neighborFinset v, vec u

Proof state:
V : Type u_1
α : Type u_2
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype V
inst✝ : NonAssocSemiring α
v : V
vec : V → α
⊢ (adjMatrix α G *ᵥ vec) v = ∑ u ∈ G.neighborFinset v, vec u

Tactic:
rw [mulVec, adjMatrix_dotProduct]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem biInter_and' (p : ι' → Prop) (q : ι → ι' → Prop) (s : ∀ x y, p y ∧ q x y → Set α) :
    ⋂ (x : ι) (y : ι') (h : p y ∧ q x y), s x y h =
      ⋂ (y : ι') (hy : p y) (x : ι) (hx : q x y), s x y ⟨hy, hx⟩

Proof state:
α : Type u_1
ι : Sort u_5
ι' : Sort u_6
p : ι' → Prop
q : ι → ι' → Prop
s : (x : ι) → (y : ι') → p y ∧ q x y → Set α
⊢ ⋂ x, ⋂ y, ⋂ (h : p y ∧ q x y), s x y h = ⋂ y, ⋂ (hy : p y), ⋂ x, ⋂ (hx : q x y), s x y ⋯

Tactic:
simp only [iInter_and, @iInter_comm _ ι]

Result:
no goals
-- Mathlib/Algebra/Homology/Additive.lean
theorem NatTrans.mapHomologicalComplex_id
    (c : ComplexShape ι) (F : W₁ ⥤ W₂) [F.PreservesZeroMorphisms] :
    NatTrans.mapHomologicalComplex (𝟙 F) c = 𝟙 (F.mapHomologicalComplex c)

Proof state:
ι : Type u_1
W₁ : Type u_3
W₂ : Type u_4
inst✝⁴ : Category.{u_5, u_3} W₁
inst✝³ : Category.{u_6, u_4} W₂
inst✝² : HasZeroMorphisms W₁
inst✝¹ : HasZeroMorphisms W₂
c : ComplexShape ι
F : W₁ ⥤ W₂
inst✝ : F.PreservesZeroMorphisms
⊢ mapHomologicalComplex (𝟙 F) c = 𝟙 (F.mapHomologicalComplex c)

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem length_reverse {u v : V} (p : G.Walk u v) : p.reverse.length = p.length

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.reverse.length = p.length

Tactic:
simp [reverse]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem mul_lt_of_lt {a b c : Cardinal} (hc : ℵ₀ ≤ c) (h1 : a < c) (h2 : b < c) : a * b < c :=
  (mul_le_mul' (le_max_left a b) (le_max_right a b)).trans_lt <|
    (lt_or_le (max a b) ℵ₀).elim (fun h => (mul_lt_aleph0 h h).trans_le hc) fun h => by
      rw [mul_eq_self h]
      exact max_lt h1 h2

Proof state:
a b c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
h1 : a < c
h2 : b < c
h : ℵ₀ ≤ a ⊔ b
⊢ a ⊔ b < c

Tactic:
exact max_lt h1 h2

Result:
no goals

Proof state:
a b c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
h1 : a < c
h2 : b < c
h : ℵ₀ ≤ a ⊔ b
⊢ (a ⊔ b) * (a ⊔ b) < c

Tactic:
rw [mul_eq_self h]

Result:
a b c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
h1 : a < c
h2 : b < c
h : ℵ₀ ≤ a ⊔ b
⊢ a ⊔ b < c
-- Mathlib/Topology/UniformSpace/Defs.lean
theorem uniformContinuousOn_univ [UniformSpace β] {f : α → β} :
    UniformContinuousOn f univ ↔ UniformContinuous f

Proof state:
α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
⊢ UniformContinuousOn f univ ↔ UniformContinuous f

Tactic:
rw [UniformContinuousOn, UniformContinuous, univ_prod_univ, principal_univ, inf_top_eq]

Result:
no goals
-- Mathlib/Analysis/SpecificLimits/Basic.lean
theorem NNReal.tendsto_inverse_atTop_nhds_zero_nat :
    Tendsto (fun n : ℕ ↦ (n : ℝ≥0)⁻¹) atTop (𝓝 0)

Proof state:
⊢ Tendsto (fun a => ↑(↑a)⁻¹) atTop (𝓝 ↑0)

Tactic:
exact _root_.tendsto_inverse_atTop_nhds_zero_nat

Result:
no goals

Proof state:
⊢ Tendsto (fun n => (↑n)⁻¹) atTop (𝓝 0)

Tactic:
rw [← NNReal.tendsto_coe]

Result:
⊢ Tendsto (fun a => ↑(↑a)⁻¹) atTop (𝓝 ↑0)
-- Mathlib/Order/SuccPred/Limit.lean
theorem mem_range_succ_of_not_isSuccPrelimit (h : ¬ IsSuccPrelimit a) :
    a ∈ range (succ : α → α)

Proof state:
case intro
α : Type u_1
a : α
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
h : ¬IsSuccPrelimit a
b : α
hb : ¬IsMax b ∧ succ b = a
⊢ a ∈ range succ

Tactic:
exact ⟨b, hb.2⟩

Result:
no goals

Proof state:
α : Type u_1
a : α
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
h : ¬IsSuccPrelimit a
⊢ a ∈ range succ

Tactic:
obtain ⟨b, hb⟩ := not_isSuccPrelimit_iff.1 h

Result:
case intro
α : Type u_1
a : α
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
h : ¬IsSuccPrelimit a
b : α
hb : ¬IsMax b ∧ succ b = a
⊢ a ∈ range succ