harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/BigOperators/GroupWithZero/Action.lean
theorem smul_prod [Monoid α] [Monoid β] [MulAction α β] [IsScalarTower α β β] [SMulCommClass α β β]
    (l : List β) (m : α) :
    m ^ l.length • l.prod = (l.map (m • ·)).prod

Proof state:
case cons
α : Type u_1
β : Type u_2
inst✝⁴ : Monoid α
inst✝³ : Monoid β
inst✝² : MulAction α β
inst✝¹ : IsScalarTower α β β
inst✝ : SMulCommClass α β β
m : α
head : β
tail : List β
ih : m ^ tail.length • tail.prod = (map (fun x => m • x) tail).prod
⊢ m ^ (head :: tail).length • (head :: tail).prod = (map (fun x => m • x) (head :: tail)).prod

Tactic:
simp [← ih, smul_mul_smul_comm, pow_succ']

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : Monoid α
inst✝³ : Monoid β
inst✝² : MulAction α β
inst✝¹ : IsScalarTower α β β
inst✝ : SMulCommClass α β β
l : List β
m : α
⊢ m ^ l.length • l.prod = (map (fun x => m • x) l).prod

Tactic:
induction l with
| nil => simp
| cons head tail ih => simp [← ih, smul_mul_smul_comm, pow_succ']

Result:
no goals

Proof state:
case nil
α : Type u_1
β : Type u_2
inst✝⁴ : Monoid α
inst✝³ : Monoid β
inst✝² : MulAction α β
inst✝¹ : IsScalarTower α β β
inst✝ : SMulCommClass α β β
m : α
⊢ m ^ [].length • [].prod = (map (fun x => m • x) []).prod

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Regularity/Uniform.lean
theorem nonuniformWitness_subset (h : ¬G.IsUniform ε s t) : G.nonuniformWitness ε s t ⊆ s

Proof state:
case neg
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h : ¬G.IsUniform ε s t
h✝ : ¬WellOrderingRel s t
⊢ (G.nonuniformWitnesses ε t s).2 ⊆ s

Tactic:
exact G.right_nonuniformWitnesses_subset fun i => h i.symm

Result:
no goals

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h : ¬G.IsUniform ε s t
⊢ (if WellOrderingRel s t then (G.nonuniformWitnesses ε s t).1 else (G.nonuniformWitnesses ε t s).2) ⊆ s

Tactic:
split_ifs

Result:
case pos
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h : ¬G.IsUniform ε s t
h✝ : WellOrderingRel s t
⊢ (G.nonuniformWitnesses ε s t).1 ⊆ s

case neg
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h : ¬G.IsUniform ε s t
h✝ : ¬WellOrderingRel s t
⊢ (G.nonuniformWitnesses ε t s).2 ⊆ s

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h : ¬G.IsUniform ε s t
⊢ G.nonuniformWitness ε s t ⊆ s

Tactic:
unfold nonuniformWitness

Result:
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h : ¬G.IsUniform ε s t
⊢ (if WellOrderingRel s t then (G.nonuniformWitnesses ε s t).1 else (G.nonuniformWitnesses ε t s).2) ⊆ s

Proof state:
case pos
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h : ¬G.IsUniform ε s t
h✝ : WellOrderingRel s t
⊢ (G.nonuniformWitnesses ε s t).1 ⊆ s

Tactic:
exact G.left_nonuniformWitnesses_subset h

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
theorem norm_one : norm (1 : PadicSeq p) = 1

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
h1 : ¬1 ≈ 0
⊢ norm 1 = 1

Tactic:
simp [h1, norm, hp.1.one_lt]

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ norm 1 = 1

Tactic:
have h1 : ¬(1 : PadicSeq p) ≈ 0 := one_not_equiv_zero _

Result:
p : ℕ
hp : Fact (Nat.Prime p)
h1 : ¬1 ≈ 0
⊢ norm 1 = 1
-- Mathlib/CategoryTheory/Localization/CalculusOfFractions/Preadditive.lean
@[simp]
lemma map_add (F : C ⥤ D) (hF : W.IsInvertedBy F) [Preadditive D] [F.Additive] :
    φ.add.map F hF = φ.fst.map F hF + φ.snd.map F hF

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✝² : Preadditive C
W : MorphismProperty C
X Y : C
φ : W.LeftFraction₂ X Y
F : C ⥤ D
hF : W.IsInvertedBy F
inst✝¹ : Preadditive D
inst✝ : F.Additive
this : IsIso (F.map φ.s)
⊢ φ.add.map F hF = φ.fst.map F hF + φ.snd.map F hF

Tactic:
rw [← cancel_mono (F.map φ.s), add_comp, LeftFraction.map_comp_map_s,
  LeftFraction.map_comp_map_s, LeftFraction.map_comp_map_s, F.map_add]

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✝² : Preadditive C
W : MorphismProperty C
X Y : C
φ : W.LeftFraction₂ X Y
F : C ⥤ D
hF : W.IsInvertedBy F
inst✝¹ : Preadditive D
inst✝ : F.Additive
⊢ φ.add.map F hF = φ.fst.map F hF + φ.snd.map F hF

Tactic:
have := hF φ.s φ.hs

Result:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
inst✝² : Preadditive C
W : MorphismProperty C
X Y : C
φ : W.LeftFraction₂ X Y
F : C ⥤ D
hF : W.IsInvertedBy F
inst✝¹ : Preadditive D
inst✝ : F.Additive
this : IsIso (F.map φ.s)
⊢ φ.add.map F hF = φ.fst.map F hF + φ.snd.map F hF
-- Mathlib/LinearAlgebra/Matrix/Nondegenerate.lean
theorem eq_zero_of_mulVec_eq_zero [DecidableEq m] {M : Matrix m m A} (hM : M.det ≠ 0) {v : m → A}
    (hv : M *ᵥ v = 0) : v = 0 :=
  eq_zero_of_vecMul_eq_zero (by rwa [det_transpose]) ((vecMul_transpose M v).trans hv)

Proof state:
m : Type u_1
A : Type u_3
inst✝³ : Fintype m
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : M.det ≠ 0
v : m → A
hv : M *ᵥ v = 0
⊢ Mᵀ.det ≠ 0

Tactic:
rwa [det_transpose]

Result:
no goals
-- Mathlib/Topology/Algebra/Monoid.lean
theorem LocallyFinite.exists_finset_mulSupport {M : Type*} [CommMonoid M] {f : ι → X → M}
    (hf : LocallyFinite fun i => mulSupport <| f i) (x₀ : X) :
    ∃ I : Finset ι, ∀ᶠ x in 𝓝 x₀, (mulSupport fun i => f i x) ⊆ I

Proof state:
ι : Type u_1
X : Type u_5
inst✝¹ : TopologicalSpace X
M : Type u_6
inst✝ : CommMonoid M
f : ι → X → M
hf : LocallyFinite fun i => mulSupport (f i)
x₀ : X
⊢ ∃ I, ∀ᶠ (x : X) in 𝓝 x₀, (mulSupport fun i => f i x) ⊆ ↑I

Tactic:
rcases hf x₀ with ⟨U, hxU, hUf⟩

Result:
case intro.intro
ι : Type u_1
X : Type u_5
inst✝¹ : TopologicalSpace X
M : Type u_6
inst✝ : CommMonoid M
f : ι → X → M
hf : LocallyFinite fun i => mulSupport (f i)
x₀ : X
U : Set X
hxU : U ∈ 𝓝 x₀
hUf : {i | ((fun i => mulSupport (f i)) i ∩ U).Nonempty}.Finite
⊢ ∃ I, ∀ᶠ (x : X) in 𝓝 x₀, (mulSupport fun i => f i x) ⊆ ↑I

Proof state:
case intro.intro
ι : Type u_1
X : Type u_5
inst✝¹ : TopologicalSpace X
M : Type u_6
inst✝ : CommMonoid M
f : ι → X → M
hf : LocallyFinite fun i => mulSupport (f i)
x₀ : X
U : Set X
hxU : U ∈ 𝓝 x₀
hUf : {i | ((fun i => mulSupport (f i)) i ∩ U).Nonempty}.Finite
y : X
hy : y ∈ U
i : ι
hi : i ∈ mulSupport fun i => f i y
⊢ i ∈ ↑hUf.toFinset

Tactic:
rw [hUf.coe_toFinset]

Result:
case intro.intro
ι : Type u_1
X : Type u_5
inst✝¹ : TopologicalSpace X
M : Type u_6
inst✝ : CommMonoid M
f : ι → X → M
hf : LocallyFinite fun i => mulSupport (f i)
x₀ : X
U : Set X
hxU : U ∈ 𝓝 x₀
hUf : {i | ((fun i => mulSupport (f i)) i ∩ U).Nonempty}.Finite
y : X
hy : y ∈ U
i : ι
hi : i ∈ mulSupport fun i => f i y
⊢ i ∈ {i | ((fun i => mulSupport (f i)) i ∩ U).Nonempty}

Proof state:
case intro.intro
ι : Type u_1
X : Type u_5
inst✝¹ : TopologicalSpace X
M : Type u_6
inst✝ : CommMonoid M
f : ι → X → M
hf : LocallyFinite fun i => mulSupport (f i)
x₀ : X
U : Set X
hxU : U ∈ 𝓝 x₀
hUf : {i | ((fun i => mulSupport (f i)) i ∩ U).Nonempty}.Finite
y : X
hy : y ∈ U
i : ι
hi : i ∈ mulSupport fun i => f i y
⊢ i ∈ {i | ((fun i => mulSupport (f i)) i ∩ U).Nonempty}

Tactic:
exact ⟨y, hi, hy⟩

Result:
no goals

Proof state:
case intro.intro
ι : Type u_1
X : Type u_5
inst✝¹ : TopologicalSpace X
M : Type u_6
inst✝ : CommMonoid M
f : ι → X → M
hf : LocallyFinite fun i => mulSupport (f i)
x₀ : X
U : Set X
hxU : U ∈ 𝓝 x₀
hUf : {i | ((fun i => mulSupport (f i)) i ∩ U).Nonempty}.Finite
⊢ ∃ I, ∀ᶠ (x : X) in 𝓝 x₀, (mulSupport fun i => f i x) ⊆ ↑I

Tactic:
refine ⟨hUf.toFinset, mem_of_superset hxU fun y hy i hi => ?_⟩

Result:
case intro.intro
ι : Type u_1
X : Type u_5
inst✝¹ : TopologicalSpace X
M : Type u_6
inst✝ : CommMonoid M
f : ι → X → M
hf : LocallyFinite fun i => mulSupport (f i)
x₀ : X
U : Set X
hxU : U ∈ 𝓝 x₀
hUf : {i | ((fun i => mulSupport (f i)) i ∩ U).Nonempty}.Finite
y : X
hy : y ∈ U
i : ι
hi : i ∈ mulSupport fun i => f i y
⊢ i ∈ ↑hUf.toFinset
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem MeasurePreserving.lintegral_comp_emb {mb : MeasurableSpace β} {ν : Measure β} {g : α → β}
    (hg : MeasurePreserving g μ ν) (hge : MeasurableEmbedding g) (f : β → ℝ≥0∞) :
    ∫⁻ a, f (g a) ∂μ = ∫⁻ b, f b ∂ν

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
mb : MeasurableSpace β
ν : Measure β
g : α → β
hg : MeasurePreserving g μ ν
hge : MeasurableEmbedding g
f : β → ℝ≥0∞
⊢ ∫⁻ (a : α), f (g a) ∂μ = ∫⁻ (b : β), f b ∂ν

Tactic:
rw [← hg.map_eq, hge.lintegral_map]

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem pred_ncard_le_ncard_diff_singleton (s : Set α) (a : α) : s.ncard - 1 ≤ (s \ {a}).ncard

Proof state:
case inl
α : Type u_1
s : Set α
a : α
hs : s.Finite
⊢ s.ncard - 1 ≤ (s \ {a}).ncard

Tactic:
by_cases h : a ∈ s

Result:
case pos
α : Type u_1
s : Set α
a : α
hs : s.Finite
h : a ∈ s
⊢ s.ncard - 1 ≤ (s \ {a}).ncard

case neg
α : Type u_1
s : Set α
a : α
hs : s.Finite
h : a ∉ s
⊢ s.ncard - 1 ≤ (s \ {a}).ncard

Proof state:
α : Type u_1
s : Set α
a : α
⊢ s.ncard - 1 ≤ (s \ {a}).ncard

Tactic:
rcases s.finite_or_infinite with hs | hs

Result:
case inl
α : Type u_1
s : Set α
a : α
hs : s.Finite
⊢ s.ncard - 1 ≤ (s \ {a}).ncard

case inr
α : Type u_1
s : Set α
a : α
hs : s.Infinite
⊢ s.ncard - 1 ≤ (s \ {a}).ncard

Proof state:
case inr
α : Type u_1
s : Set α
a : α
hs : s.Infinite
⊢ s.ncard - 1 ≤ (s \ {a}).ncard

Tactic:
convert Nat.zero_le _

Result:
case h.e'_3
α : Type u_1
s : Set α
a : α
hs : s.Infinite
⊢ s.ncard - 1 = 0

Proof state:
case neg
α : Type u_1
s : Set α
a : α
hs : s.Finite
h : a ∉ s
⊢ s.ncard - 1 ≤ (s \ {a}).ncard

Tactic:
rw [diff_singleton_eq_self h]

Result:
case neg
α : Type u_1
s : Set α
a : α
hs : s.Finite
h : a ∉ s
⊢ s.ncard - 1 ≤ s.ncard

Proof state:
case h.e'_3
α : Type u_1
s : Set α
a : α
hs : s.Infinite
⊢ s.ncard - 1 = 0

Tactic:
rw [hs.ncard]

Result:
no goals

Proof state:
case pos
α : Type u_1
s : Set α
a : α
hs : s.Finite
h : a ∈ s
⊢ s.ncard - 1 ≤ (s \ {a}).ncard

Tactic:
rw [ncard_diff_singleton_of_mem h hs]

Result:
no goals

Proof state:
case neg
α : Type u_1
s : Set α
a : α
hs : s.Finite
h : a ∉ s
⊢ s.ncard - 1 ≤ s.ncard

Tactic:
apply Nat.pred_le

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/PreservesHomology.lean
@[reassoc]
lemma mapLeftHomologyIso_hom_naturality [S₁.HasLeftHomology] [S₂.HasLeftHomology]
    [F.PreservesLeftHomologyOf S₁] [F.PreservesLeftHomologyOf S₂] :
    leftHomologyMap (F.mapShortComplex.map φ) ≫ (S₂.mapLeftHomologyIso F).hom =
      (S₁.mapLeftHomologyIso F).hom ≫ F.map (leftHomologyMap φ)

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₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : S₁.HasLeftHomology
inst✝² : S₂.HasLeftHomology
inst✝¹ : F.PreservesLeftHomologyOf S₁
inst✝ : F.PreservesLeftHomologyOf S₂
⊢ leftHomologyMap' (F.mapShortComplex.map φ) (F.mapShortComplex.obj S₁).leftHomologyData
        (F.mapShortComplex.obj S₂).leftHomologyData ≫
      leftHomologyMap' (𝟙 (S₂.map F)) (S₂.map F).leftHomologyData (S₂.leftHomologyData.map F) =
    leftHomologyMap' (𝟙 (S₁.map F)) (S₁.map F).leftHomologyData (S₁.leftHomologyData.map F) ≫
      F.map (leftHomologyMap' φ S₁.leftHomologyData S₂.leftHomologyData)

Tactic:
simp only [LeftHomologyData.map_leftHomologyMap', Functor.mapShortComplex_obj,
  ← leftHomologyMap'_comp, comp_id, id_comp]

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₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : S₁.HasLeftHomology
inst✝² : S₂.HasLeftHomology
inst✝¹ : F.PreservesLeftHomologyOf S₁
inst✝ : F.PreservesLeftHomologyOf S₂
⊢ leftHomologyMap (F.mapShortComplex.map φ) ≫ (S₂.mapLeftHomologyIso F).hom =
    (S₁.mapLeftHomologyIso F).hom ≫ F.map (leftHomologyMap φ)

Tactic:
dsimp only [leftHomologyMap, mapLeftHomologyIso, LeftHomologyData.leftHomologyIso,
  leftHomologyMapIso', Iso.refl]

Result:
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₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : S₁.HasLeftHomology
inst✝² : S₂.HasLeftHomology
inst✝¹ : F.PreservesLeftHomologyOf S₁
inst✝ : F.PreservesLeftHomologyOf S₂
⊢ leftHomologyMap' (F.mapShortComplex.map φ) (F.mapShortComplex.obj S₁).leftHomologyData
        (F.mapShortComplex.obj S₂).leftHomologyData ≫
      leftHomologyMap' (𝟙 (S₂.map F)) (S₂.map F).leftHomologyData (S₂.leftHomologyData.map F) =
    leftHomologyMap' (𝟙 (S₁.map F)) (S₁.map F).leftHomologyData (S₁.leftHomologyData.map F) ≫
      F.map (leftHomologyMap' φ S₁.leftHomologyData S₂.leftHomologyData)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Compare.lean
theorem compare_eq_lt {a b : Nat} : compare a b = .lt ↔ a < b

Proof state:
a b : Nat
⊢ compare a b = Ordering.lt ↔ a < b

Tactic:
rw [compare_def_lt]

Result:
a b : Nat
⊢ (if a < b then Ordering.lt else if b < a then Ordering.gt else Ordering.eq) = Ordering.lt ↔ a < b

Proof state:
a b : Nat
⊢ (if a < b then Ordering.lt else if b < a then Ordering.gt else Ordering.eq) = Ordering.lt ↔ a < b

Tactic:
(repeat' split) <;> simp [*]

Result:
no goals

Proof state:
a b : Nat
⊢ (if a < b then Ordering.lt else if b < a then Ordering.gt else Ordering.eq) = Ordering.lt ↔ a < b

Tactic:
repeat' split

Result:
case isTrue
a b : Nat
h✝ : a < b
⊢ Ordering.lt = Ordering.lt ↔ a < b

case isFalse.isTrue
a b : Nat
h✝¹ : ¬a < b
h✝ : b < a
⊢ Ordering.gt = Ordering.lt ↔ a < b

case isFalse.isFalse
a b : Nat
h✝¹ : ¬a < b
h✝ : ¬b < a
⊢ Ordering.eq = Ordering.lt ↔ a < b

Proof state:
case isFalse
a b : Nat
h✝ : ¬a < b
⊢ (if b < a then Ordering.gt else Ordering.eq) = Ordering.lt ↔ a < b

Tactic:
split

Result:
case isFalse.isTrue
a b : Nat
h✝¹ : ¬a < b
h✝ : b < a
⊢ Ordering.gt = Ordering.lt ↔ a < b

case isFalse.isFalse
a b : Nat
h✝¹ : ¬a < b
h✝ : ¬b < a
⊢ Ordering.eq = Ordering.lt ↔ a < b
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean
theorem of_bot' {X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C} {h₁₁ : X₁₁ ⟶ X₁₂} {h₂₁ : X₂₁ ⟶ X₂₂}
    {h₃₁ : X₃₁ ⟶ X₃₂} {v₃₁ : X₁₁ ⟶ X₃₁} {v₁₂ : X₁₂ ⟶ X₂₂} {v₂₁ : X₂₁ ⟶ X₃₁} {v₂₂ : X₂₂ ⟶ X₃₂}
    (s : IsPullback h₁₁ v₃₁ (v₁₂ ≫ v₂₂) h₃₁) (t : IsPullback h₂₁ v₂₁ v₂₂ h₃₁) :
    IsPullback h₁₁ (t.lift (h₁₁ ≫ v₁₂) v₃₁ (by rw [Category.assoc, s.w])) v₁₂ h₂₁ :=
  of_bot ((t.lift_snd _ _ _) ▸ s) (by simp only [lift_fst]) t

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C
h₁₁ : X₁₁ ⟶ X₁₂
h₂₁ : X₂₁ ⟶ X₂₂
h₃₁ : X₃₁ ⟶ X₃₂
v₃₁ : X₁₁ ⟶ X₃₁
v₁₂ : X₁₂ ⟶ X₂₂
v₂₁ : X₂₁ ⟶ X₃₁
v₂₂ : X₂₂ ⟶ X₃₂
s : IsPullback h₁₁ v₃₁ (v₁₂ ≫ v₂₂) h₃₁
t : IsPullback h₂₁ v₂₁ v₂₂ h₃₁
⊢ (h₁₁ ≫ v₁₂) ≫ v₂₂ = v₃₁ ≫ h₃₁

Tactic:
rw [Category.assoc, s.w]

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C
h₁₁ : X₁₁ ⟶ X₁₂
h₂₁ : X₂₁ ⟶ X₂₂
h₃₁ : X₃₁ ⟶ X₃₂
v₃₁ : X₁₁ ⟶ X₃₁
v₁₂ : X₁₂ ⟶ X₂₂
v₂₁ : X₂₁ ⟶ X₃₁
v₂₂ : X₂₂ ⟶ X₃₂
s : IsPullback h₁₁ v₃₁ (v₁₂ ≫ v₂₂) h₃₁
t : IsPullback h₂₁ v₂₁ v₂₂ h₃₁
⊢ h₁₁ ≫ v₁₂ = t.lift (h₁₁ ≫ v₁₂) v₃₁ ⋯ ≫ h₂₁

Tactic:
simp only [lift_fst]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/ChosenFiniteProducts.lean
lemma tensorProd_isSheaf : Presheaf.IsSheaf J (X.val ⊗ Y.val)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : Type u₂
inst✝¹ : Category.{v₂, u₂} A
J : GrothendieckTopology C
inst✝ : ChosenFiniteProducts A
X Y : Sheaf J A
⊢ Presheaf.IsSheaf J (X.val ⊗ Y.val)

Tactic:
apply isSheaf_of_isLimit (E := (Cones.postcompose (pairComp X Y (sheafToPresheaf J A)).inv).obj
  (ChosenFiniteProducts.product X.val Y.val).cone)

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : Type u₂
inst✝¹ : Category.{v₂, u₂} A
J : GrothendieckTopology C
inst✝ : ChosenFiniteProducts A
X Y : Sheaf J A
⊢ IsLimit
    ((Cones.postcompose (pairComp X Y (sheafToPresheaf J A)).inv).obj (ChosenFiniteProducts.product X.val Y.val).cone)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : Type u₂
inst✝¹ : Category.{v₂, u₂} A
J : GrothendieckTopology C
inst✝ : ChosenFiniteProducts A
X Y : Sheaf J A
⊢ IsLimit
    ((Cones.postcompose (pairComp X Y (sheafToPresheaf J A)).inv).obj (ChosenFiniteProducts.product X.val Y.val).cone)

Tactic:
exact (IsLimit.postcomposeInvEquiv _ _).invFun (ChosenFiniteProducts.product X.val Y.val).isLimit

Result:
no goals
-- Mathlib/LinearAlgebra/Finsupp/Span.lean
theorem lsingle_range_le_ker_lapply (s t : Set α) (h : Disjoint s t) :
    ⨆ a ∈ s, LinearMap.range (lsingle a : M →ₗ[R] α →₀ M) ≤
      ⨅ a ∈ t, ker (lapply a : (α →₀ M) →ₗ[R] M)

Proof state:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
h : Disjoint s t
a₁ : α
h₁ : a₁ ∈ s
b : M
a✝ : b ∈ ⊤
a₂ : α
h₂ : a₂ ∈ t
this : a₁ ≠ a₂
⊢ (lapply a₂ ∘ₗ lsingle a₁) b = 0

Tactic:
exact single_eq_of_ne this

Result:
no goals

Proof state:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
h : Disjoint s t
a₁ : α
h₁ : a₁ ∈ s
b : M
a✝ : b ∈ ⊤
a₂ : α
h₂ : a₂ ∈ t
⊢ (lapply a₂ ∘ₗ lsingle a₁) b = 0

Tactic:
have : a₁ ≠ a₂ := fun eq => h.le_bot ⟨h₁, eq.symm ▸ h₂⟩

Result:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
h : Disjoint s t
a₁ : α
h₁ : a₁ ∈ s
b : M
a✝ : b ∈ ⊤
a₂ : α
h₂ : a₂ ∈ t
this : a₁ ≠ a₂
⊢ (lapply a₂ ∘ₗ lsingle a₁) b = 0

Proof state:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
h : Disjoint s t
a₁ : α
h₁ : a₁ ∈ s
⊢ ∀ ⦃x : M⦄, x ∈ ⊤ → ∀ i ∈ t, (lapply i ∘ₗ lsingle a₁) x = 0

Tactic:
intro b _ a₂ h₂

Result:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
h : Disjoint s t
a₁ : α
h₁ : a₁ ∈ s
b : M
a✝ : b ∈ ⊤
a₂ : α
h₂ : a₂ ∈ t
⊢ (lapply a₂ ∘ₗ lsingle a₁) b = 0

Proof state:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
h : Disjoint s t
a₁ : α
h₁ : a₁ ∈ s
⊢ comap (lsingle a₁) (⨅ a ∈ t, ker (lapply a)) = ⊤

Tactic:
simp only [(ker_comp _ _).symm, eq_top_iff, SetLike.le_def, mem_ker, comap_iInf, mem_iInf]

Result:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
h : Disjoint s t
a₁ : α
h₁ : a₁ ∈ s
⊢ ∀ ⦃x : M⦄, x ∈ ⊤ → ∀ i ∈ t, (lapply i ∘ₗ lsingle a₁) x = 0

Proof state:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
h : Disjoint s t
⊢ ⨆ a ∈ s, LinearMap.range (lsingle a) ≤ ⨅ a ∈ t, ker (lapply a)

Tactic:
refine iSup_le fun a₁ => iSup_le fun h₁ => range_le_iff_comap.2 ?_

Result:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
h : Disjoint s t
a₁ : α
h₁ : a₁ ∈ s
⊢ comap (lsingle a₁) (⨅ a ∈ t, ker (lapply a)) = ⊤
-- Mathlib/Combinatorics/SimpleGraph/Matching.lean
lemma IsMatching.sup (hM : M.IsMatching) (hM' : M'.IsMatching)
    (hd : Disjoint M.support M'.support) : (M ⊔ M').IsMatching

Proof state:
case h
V : Type u_1
G : SimpleGraph V
M M' : G.Subgraph
hM : M.IsMatching
hM' : M'.IsMatching
hd✝ : Disjoint M.support M'.support
v : V
hv : v ∈ (M ⊔ M').verts
N N' : G.Subgraph
hN : N.IsMatching
hd : Disjoint N.support N'.support
hmN : v ∈ N.verts
w : V
hw : (fun w => N.Adj v w) w ∧ ∀ (y : V), (fun w => N.Adj v w) y → y = w
⊢ (fun w => (N ⊔ N').Adj v w) w ∧ ∀ (y : V), (fun w => (N ⊔ N').Adj v w) y → y = w

Tactic:
refine ⟨sup_adj.mpr (.inl hw.1), ?_⟩

Result:
case h
V : Type u_1
G : SimpleGraph V
M M' : G.Subgraph
hM : M.IsMatching
hM' : M'.IsMatching
hd✝ : Disjoint M.support M'.support
v : V
hv : v ∈ (M ⊔ M').verts
N N' : G.Subgraph
hN : N.IsMatching
hd : Disjoint N.support N'.support
hmN : v ∈ N.verts
w : V
hw : (fun w => N.Adj v w) w ∧ ∀ (y : V), (fun w => N.Adj v w) y → y = w
⊢ ∀ (y : V), (fun w => (N ⊔ N').Adj v w) y → y = w
-- Mathlib/Data/Nat/Digits.lean
theorem modEq_three_digits_sum (n : ℕ) : n ≡ (digits 10 n).sum [MOD 3] :=
  modEq_digits_sum 3 10 (by norm_num) n

Proof state:
n : ℕ
⊢ 10 % 3 = 1

Tactic:
norm_num

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem meas_ge_le_lintegral_div {f : α → ℝ≥0∞} (hf : AEMeasurable f μ) {ε : ℝ≥0∞} (hε : ε ≠ 0)
    (hε' : ε ≠ ∞) : μ { x | ε ≤ f x } ≤ (∫⁻ a, f a ∂μ) / ε :=
  (ENNReal.le_div_iff_mul_le (Or.inl hε) (Or.inl hε')).2 <| by
    rw [mul_comm]
    exact mul_meas_ge_le_lintegral₀ hf ε

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
ε : ℝ≥0∞
hε : ε ≠ 0
hε' : ε ≠ ⊤
⊢ μ {x | ε ≤ f x} * ε ≤ ∫⁻ (a : α), f a ∂μ

Tactic:
rw [mul_comm]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
ε : ℝ≥0∞
hε : ε ≠ 0
hε' : ε ≠ ⊤
⊢ ε * μ {x | ε ≤ f x} ≤ ∫⁻ (a : α), f a ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
ε : ℝ≥0∞
hε : ε ≠ 0
hε' : ε ≠ ⊤
⊢ ε * μ {x | ε ≤ f x} ≤ ∫⁻ (a : α), f a ∂μ

Tactic:
exact mul_meas_ge_le_lintegral₀ hf ε

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Add.lean
@[simp]
lemma DifferentiableAt.add_iff_left (hg : DifferentiableAt 𝕜 g x) :
    DifferentiableAt 𝕜 (fun y => f y + g y) x ↔ DifferentiableAt 𝕜 f x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
x : E
hg : DifferentiableAt 𝕜 g x
⊢ DifferentiableAt 𝕜 (fun y => f y + g y) x ↔ DifferentiableAt 𝕜 f x

Tactic:
refine ⟨fun h ↦ ?_, fun hf ↦ hf.add hg⟩

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
x : E
hg : DifferentiableAt 𝕜 g x
h : DifferentiableAt 𝕜 (fun y => f y + g y) x
⊢ DifferentiableAt 𝕜 f x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
x : E
hg : DifferentiableAt 𝕜 g x
h : DifferentiableAt 𝕜 (fun y => f y + g y) x
⊢ DifferentiableAt 𝕜 f x

Tactic:
simpa only [add_sub_cancel_right] using h.sub hg

Result:
no goals