harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean
theorem ne₂₃_of_not_collinear {p₁ p₂ p₃ : P} (h : ¬Collinear k ({p₁, p₂, p₃} : Set P)) :
    p₂ ≠ p₃

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ : P
h : ¬Collinear k {p₁, p₂, p₂}
⊢ False

Tactic:
simp [collinear_pair] at h

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ : P
h : ¬Collinear k {p₁, p₂, p₃}
⊢ p₂ ≠ p₃

Tactic:
rintro rfl

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ : P
h : ¬Collinear k {p₁, p₂, p₂}
⊢ False
-- Mathlib/Data/List/Sort.lean
theorem sorted_listMap (e : ra ↪r rb) {l : List α} : (l.map e).Sorted rb ↔ l.Sorted ra

Proof state:
α : Type u_1
β : Type u_2
ra : α → α → Prop
rb : β → β → Prop
e : ra ↪r rb
l : List α
⊢ Sorted rb (List.map (⇑e) l) ↔ Sorted ra l

Tactic:
simp [Sorted, pairwise_map, e.map_rel_iff]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Finite.lean
theorem neighborFinset_compl [DecidableEq V] [DecidableRel G.Adj] (v : V) :
    Gᶜ.neighborFinset v = (G.neighborFinset v)ᶜ \ {v}

Proof state:
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
⊢ Gᶜ.neighborFinset v = (G.neighborFinset v)ᶜ \ {v}

Tactic:
simp only [neighborFinset, neighborSet_compl, Set.toFinset_diff, Set.toFinset_compl,
  Set.toFinset_singleton]

Result:
no goals
-- Mathlib/Analysis/Calculus/LogDeriv.lean
theorem logDeriv_id (x : 𝕜) : logDeriv id x = 1 / x

Proof state:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
⊢ logDeriv id x = 1 / x

Tactic:
simp [logDeriv_apply]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Expect.lean
lemma smul_expect {G : Type*} [DistribSMul G M] [SMulCommClass G ℚ≥0 M] (a : G)
    (s : Finset ι) (f : ι → M) : a • 𝔼 i ∈ s, f i = 𝔼 i ∈ s, a • f i

Proof state:
ι : Type u_1
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module ℚ≥0 M
G : Type u_5
inst✝¹ : DistribSMul G M
inst✝ : SMulCommClass G ℚ≥0 M
a : G
s : Finset ι
f : ι → M
⊢ a • 𝔼 i ∈ s, f i = 𝔼 i ∈ s, a • f i

Tactic:
simp only [expect, smul_sum, smul_comm]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem tensor_whiskerLeft_symm (X Y : C) {Z Z' : C} (f : Z ⟶ Z') :
    X ◁ Y ◁ f = (α_ X Y Z).inv ≫ (X ⊗ Y) ◁ f ≫ (α_ X Y Z').hom

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z Z' : C
f : Z ⟶ Z'
⊢ X ◁ Y ◁ f = (α_ X Y Z).inv ≫ (X ⊗ Y) ◁ f ≫ (α_ X Y Z').hom

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Abelian.lean
@[reassoc]
lemma abelianImageToKernel_comp_kernel_ι_comp_cokernel_π :
    S.abelianImageToKernel ≫ kernel.ι S.g ≫ cokernel.π S.f = 0

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
⊢ S.abelianImageToKernel ≫ kernel.ι S.g ≫ cokernel.π S.f = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
lemma restrict_closure_eq (M : Matroid α) (hXR : X ⊆ R) (hR : R ⊆ M.E

Proof state:
α : Type u_2
X R : Set α
M : Matroid α
hXR : X ⊆ R
hR : autoParam (R ⊆ M.E) _auto✝
⊢ (M ↾ R).closure X = M.closure X ∩ R

Tactic:
rw [restrict_closure_eq', diff_eq_empty.mpr hR, union_empty, inter_eq_self_of_subset_left hXR]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem mk_set {α : Type u} : #(Set α) = 2 ^ #α

Proof state:
α : Type u
⊢ #(Set α) = 2 ^ #α

Tactic:
simp [← one_add_one_eq_two, Set, mk_arrow]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/RiemannZeta.lean
lemma HurwitzZeta.expZeta_zero : expZeta 0 = riemannZeta

Proof state:
⊢ expZeta 0 = riemannZeta

Tactic:
ext1 s

Result:
case h
s : ℂ
⊢ expZeta 0 s = riemannZeta s

Proof state:
case h
s : ℂ
⊢ expZeta 0 s = riemannZeta s

Tactic:
rw [expZeta, cosZeta_zero, add_right_eq_self, mul_eq_zero, eq_false_intro I_ne_zero, false_or,
  ← eq_neg_self_iff, ← sinZeta_neg, neg_zero]

Result:
no goals
-- Mathlib/Order/SuccPred/CompleteLinearOrder.lean
theorem iSup_Iio_eq_self_iff_isSuccPrelimit : ⨆ a : Iio x, a.1 = x ↔ IsSuccPrelimit x

Proof state:
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
x : α
⊢ ⨆ a, ↑a = x ↔ IsSuccPrelimit x

Tactic:
rw [← sSup_eq_iSup', sSup_Iio_eq_self_iff_isSuccPrelimit]

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma add_succ_lt_add (hab : a < b) (hcd : c < d) : a + c + 1 < b + d

Proof state:
a b c d : ℕ
hab : a < b
hcd : c < d
⊢ a + c + 1 < b + d

Tactic:
omega

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean
theorem arccos_of_le_neg_one {x : ℝ} (hx : x ≤ -1) : arccos x = π

Proof state:
x : ℝ
hx : x ≤ -1
⊢ arccos x = π

Tactic:
rw [arccos, arcsin_of_le_neg_one hx, sub_neg_eq_add, add_halves]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/NonabelianCohomology/H1.lean
lemma ev_symm (γ : OneCocycle G U) (i j : I) ⦃T : C⦄ (a : T ⟶ U i) (b : T ⟶ U j) :
    γ.ev i j a b = (γ.ev j i b a)⁻¹

Proof state:
C : Type u
inst✝ : Category.{v, u} C
G : Cᵒᵖ ⥤ Grp
I : Type w'
U : I → C
γ : OneCocycle G U
i j : I
T : C
a : T ⟶ U i
b : T ⟶ U j
⊢ γ.ev i j a b = (γ.ev j i b a)⁻¹

Tactic:
rw [← mul_left_inj (γ.ev j i b a), γ.ev_trans i j i a b a,
  ev_refl, inv_mul_cancel]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
theorem coprod.map_comp_inl_inr_codiag [HasColimitsOfShape (Discrete WalkingPair) C] {X X' Y Y' : C}
    (g : X ⟶ Y) (g' : X' ⟶ Y') :
    coprod.map (g ≫ coprod.inl) (g' ≫ coprod.inr) ≫ codiag (Y ⨿ Y') = coprod.map g g'

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimitsOfShape (Discrete WalkingPair) C
X X' Y Y' : C
g : X ⟶ Y
g' : X' ⟶ Y'
⊢ map (g ≫ inl) (g' ≫ inr) ≫ codiag (Y ⨿ Y') = map g g'

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/WithLp.lean
theorem contDiffAt_piLp :
    ContDiffAt 𝕜 n f y ↔ ∀ i, ContDiffAt 𝕜 n (fun x => f x i) y

Proof state:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Fintype ι
p : ENNReal
inst✝ : Fact (1 ≤ p)
n : WithTop ℕ∞
f : H → PiLp p E
y : H
⊢ ContDiffAt 𝕜 n f y ↔ ∀ (i : ι), ContDiffAt 𝕜 n (fun x => f x i) y

Tactic:
rw [← (PiLp.continuousLinearEquiv p 𝕜 E).comp_contDiffAt_iff, contDiffAt_pi]

Result:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Fintype ι
p : ENNReal
inst✝ : Fact (1 ≤ p)
n : WithTop ℕ∞
f : H → PiLp p E
y : H
⊢ (∀ (i : ι), ContDiffAt 𝕜 n (fun x => (⇑(PiLp.continuousLinearEquiv p 𝕜 E) ∘ f) x i) y) ↔
    ∀ (i : ι), ContDiffAt 𝕜 n (fun x => f x i) y

Proof state:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Fintype ι
p : ENNReal
inst✝ : Fact (1 ≤ p)
n : WithTop ℕ∞
f : H → PiLp p E
y : H
⊢ (∀ (i : ι), ContDiffAt 𝕜 n (fun x => (⇑(PiLp.continuousLinearEquiv p 𝕜 E) ∘ f) x i) y) ↔
    ∀ (i : ι), ContDiffAt 𝕜 n (fun x => f x i) y

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/Order/OrderClosed.lean
theorem Ioo_subset_closure_interior : Ioo a b ⊆ closure (interior (Ioo a b))

Proof state:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
a b : α
⊢ Ioo a b ⊆ closure (interior (Ioo a b))

Tactic:
simp only [interior_Ioo, subset_closure]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean
theorem HasFTaylorSeriesUpTo.of_le (h : HasFTaylorSeriesUpTo n f p) (hmn : m ≤ n) :
    HasFTaylorSeriesUpTo m f p

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
m n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpTo n f p
hmn : m ≤ n
⊢ HasFTaylorSeriesUpTo m f p

Tactic:
rw [← hasFTaylorSeriesUpToOn_univ_iff] at h ⊢

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
m n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p univ
hmn : m ≤ n
⊢ HasFTaylorSeriesUpToOn m f p univ

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
m n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p univ
hmn : m ≤ n
⊢ HasFTaylorSeriesUpToOn m f p univ

Tactic:
exact h.of_le hmn

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Definitions.lean
theorem natDegree_eq_of_degree_eq [Semiring S] {q : S[X]} (h : degree p = degree q) :
    natDegree p = natDegree q

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
q : S[X]
h : p.degree = q.degree
⊢ p.natDegree = q.natDegree

Tactic:
unfold natDegree

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
q : S[X]
h : p.degree = q.degree
⊢ WithBot.unbotD 0 p.degree = WithBot.unbotD 0 q.degree

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
q : S[X]
h : p.degree = q.degree
⊢ WithBot.unbotD 0 p.degree = WithBot.unbotD 0 q.degree

Tactic:
rw [h]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/ENat.lean
theorem toENat_congr {α : Type u} {β : Type v} (e : α ≃ β) : toENat #α = toENat #β

Proof state:
α : Type u
β : Type v
e : α ≃ β
⊢ toENat #α = toENat #β

Tactic:
rw [← toENat_lift, lift_mk_eq.{_, _,v}.mpr ⟨e⟩, toENat_lift]

Result:
no goals
-- Mathlib/Algebra/Quaternion.lean
theorem mk_univ_quaternionAlgebra_of_infinite [Infinite R] :
    #(Set.univ : Set ℍ[R,c₁,c₂,c₃]) = #R

Proof state:
R : Type u_1
c₁ c₂ c₃ : R
inst✝ : Infinite R
⊢ #↑Set.univ = #R

Tactic:
rw [mk_univ_quaternionAlgebra, pow_four]

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
theorem card_le_card_biUnion_add_card_fiber {s : Finset ι} {f : ι → Finset α}
    (hs : (s : Set ι).PairwiseDisjoint f) : #s ≤ #(s.biUnion f) + #{i ∈ s | f i = ∅}

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : DecidableEq α
s : Finset ι
f : ι → Finset α
hs : (↑s).PairwiseDisjoint f
⊢ #s ≤ #(s.biUnion f) + #(filter (fun i => f i = ∅) s)

Tactic:
rw [← Finset.filter_card_add_filter_neg_card_eq_card fun i ↦ f i = ∅, add_comm]

Result:
ι : Type u_1
α : Type u_2
inst✝ : DecidableEq α
s : Finset ι
f : ι → Finset α
hs : (↑s).PairwiseDisjoint f
⊢ #(filter (fun a => ¬f a = ∅) s) + #(filter (fun i => f i = ∅) s) ≤ #(s.biUnion f) + #(filter (fun i => f i = ∅) s)

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : DecidableEq α
s : Finset ι
f : ι → Finset α
hs : (↑s).PairwiseDisjoint f
⊢ #(filter (fun a => ¬f a = ∅) s) + #(filter (fun i => f i = ∅) s) ≤ #(s.biUnion f) + #(filter (fun i => f i = ∅) s)

Tactic:
exact
  add_le_add_right
    ((card_le_card_biUnion (hs.subset <| filter_subset _ _) fun i hi ↦
          nonempty_of_ne_empty <| (mem_filter.1 hi).2).trans <|
      card_le_card <| biUnion_subset_biUnion_of_subset_left _ <| filter_subset _ _)
    _

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
theorem diagonal_const_mulVec (x : α) (v : m → α) :
    (diagonal fun _ => x) *ᵥ v = x • v

Proof state:
case h
m : Type u_2
α : Type v
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
x : α
v : m → α
x✝ : m
⊢ ((diagonal fun x_1 => x) *ᵥ v) x✝ = (x • v) x✝

Tactic:
simp [mulVec_diagonal]

Result:
no goals

Proof state:
m : Type u_2
α : Type v
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
x : α
v : m → α
⊢ (diagonal fun x_1 => x) *ᵥ v = x • v

Tactic:
ext

Result:
case h
m : Type u_2
α : Type v
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
x : α
v : m → α
x✝ : m
⊢ ((diagonal fun x_1 => x) *ᵥ v) x✝ = (x • v) x✝
-- Mathlib/Data/QPF/Univariate/Basic.lean
theorem supp_eq {α : Type u} (x : F α) :
    supp x = { u | ∀ a f, abs ⟨a, f⟩ = x → u ∈ f '' univ }

Proof state:
case h
F : Type u → Type u
q : QPF F
α : Type u
x : F α
x✝ : α
⊢ x✝ ∈ supp x ↔ x✝ ∈ {u | ∀ (a : (P F).A) (f : (P F).B a → α), abs ⟨a, f⟩ = x → u ∈ f '' univ}

Tactic:
apply mem_supp

Result:
no goals

Proof state:
F : Type u → Type u
q : QPF F
α : Type u
x : F α
⊢ supp x = {u | ∀ (a : (P F).A) (f : (P F).B a → α), abs ⟨a, f⟩ = x → u ∈ f '' univ}

Tactic:
ext

Result:
case h
F : Type u → Type u
q : QPF F
α : Type u
x : F α
x✝ : α
⊢ x✝ ∈ supp x ↔ x✝ ∈ {u | ∀ (a : (P F).A) (f : (P F).B a → α), abs ⟨a, f⟩ = x → u ∈ f '' univ}
-- Mathlib/Order/CompleteLattice.lean
theorem Function.Surjective.iSup_congr {g : ι' → α} (h : ι → ι') (h1 : Surjective h)
    (h2 : ∀ x, g (h x) = f x) : ⨆ x, f x = ⨆ y, g y

Proof state:
case h.e'_2.h.e'_4.h
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
inst✝ : SupSet α
f : ι → α
g : ι' → α
h : ι → ι'
h1 : Surjective h
h2 : ∀ (x : ι), g (h x) = f x
x✝ : ι
⊢ f x✝ = g (h x✝)

Tactic:
exact (h2 _).symm

Result:
no goals

Proof state:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
inst✝ : SupSet α
f : ι → α
g : ι' → α
h : ι → ι'
h1 : Surjective h
h2 : ∀ (x : ι), g (h x) = f x
⊢ ⨆ x, f x = ⨆ y, g y

Tactic:
convert h1.iSup_comp g

Result:
case h.e'_2.h.e'_4.h
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
inst✝ : SupSet α
f : ι → α
g : ι' → α
h : ι → ι'
h1 : Surjective h
h2 : ∀ (x : ι), g (h x) = f x
x✝ : ι
⊢ f x✝ = g (h x✝)
-- Mathlib/GroupTheory/OrderOfElement.lean
theorem Submonoid.isOfFinOrder_coe {H : Submonoid G} {x : H} :
    IsOfFinOrder (x : G) ↔ IsOfFinOrder x

Proof state:
G : Type u_1
inst✝ : Monoid G
H : Submonoid G
x : ↥H
⊢ (∃ n, 0 < n ∧ ↑x ^ n = 1) ↔ ∃ n, 0 < n ∧ x ^ n = 1

Tactic:
norm_cast

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Monoid G
H : Submonoid G
x : ↥H
⊢ IsOfFinOrder ↑x ↔ IsOfFinOrder x

Tactic:
rw [isOfFinOrder_iff_pow_eq_one, isOfFinOrder_iff_pow_eq_one]

Result:
G : Type u_1
inst✝ : Monoid G
H : Submonoid G
x : ↥H
⊢ (∃ n, 0 < n ∧ ↑x ^ n = 1) ↔ ∃ n, 0 < n ∧ x ^ n = 1
-- Mathlib/Data/Fintype/Units.lean
theorem Fintype.card_eq_card_units_add_one [GroupWithZero α] [Fintype α] [DecidableEq α] :
    Fintype.card α = Fintype.card αˣ + 1

Proof state:
α : Type u_1
inst✝² : GroupWithZero α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ card α = card αˣ + 1

Tactic:
rw [Fintype.card_units, tsub_add_cancel_of_le Fintype.card_pos]

Result:
no goals
-- Mathlib/Algebra/Ring/SumsOfSquares.lean
theorem mem_sumSq {s : T} : s ∈ sumSq T ↔ IsSumSq s

Proof state:
T : Type u_2
inst✝ : NonUnitalCommSemiring T
s : T
⊢ s ∈ sumSq T ↔ IsSumSq s

Tactic:
simp [← NonUnitalSubsemiring.mem_toAddSubmonoid]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Linear.lean
@[simp]
lemma rightHomologyMap'_smul :
    rightHomologyMap' (a • φ) h₁ h₂ = a • rightHomologyMap' φ h₁ h₂

Proof state:
R : Type u_1
C : Type u_2
inst✝³ : Semiring R
inst✝² : Category.{u_3, u_2} C
inst✝¹ : Preadditive C
inst✝ : Linear R C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
a : R
γ : RightHomologyMapData φ h₁ h₂
⊢ rightHomologyMap' (a • φ) h₁ h₂ = a • rightHomologyMap' φ h₁ h₂

Tactic:
simp only [(γ.smul a).rightHomologyMap'_eq, RightHomologyMapData.smul_φH, γ.rightHomologyMap'_eq]

Result:
no goals

Proof state:
R : Type u_1
C : Type u_2
inst✝³ : Semiring R
inst✝² : Category.{u_3, u_2} C
inst✝¹ : Preadditive C
inst✝ : Linear R C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
a : R
⊢ rightHomologyMap' (a • φ) h₁ h₂ = a • rightHomologyMap' φ h₁ h₂

Tactic:
have γ : RightHomologyMapData φ h₁ h₂ := default

Result:
R : Type u_1
C : Type u_2
inst✝³ : Semiring R
inst✝² : Category.{u_3, u_2} C
inst✝¹ : Preadditive C
inst✝ : Linear R C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
a : R
γ : RightHomologyMapData φ h₁ h₂
⊢ rightHomologyMap' (a • φ) h₁ h₂ = a • rightHomologyMap' φ h₁ h₂
-- Mathlib/Data/Sigma/Lex.lean
theorem Lex.mono (hr : ∀ a b, r₁ a b → r₂ a b) (hs : ∀ i a b, s₁ i a b → s₂ i a b) {a b : Σ i, α i}
    (h : Lex r₁ s₁ a b) : Lex r₂ s₂ a b

Proof state:
case right
ι : Type u_1
α : ι → Type u_2
r₁ r₂ : ι → ι → Prop
s₁ s₂ : (i : ι) → α i → α i → Prop
hr : ∀ (a b : ι), r₁ a b → r₂ a b
hs : ∀ (i : ι) (a b : α i), s₁ i a b → s₂ i a b
i✝ : ι
a b : α i✝
hab : s₁ i✝ a b
⊢ Lex r₂ s₂ ⟨i✝, a⟩ ⟨i✝, b⟩

Tactic:
exact Lex.right _ _ (hs _ _ _ hab)

Result:
no goals

Proof state:
case left
ι : Type u_1
α : ι → Type u_2
r₁ r₂ : ι → ι → Prop
s₁ s₂ : (i : ι) → α i → α i → Prop
hr : ∀ (a b : ι), r₁ a b → r₂ a b
hs : ∀ (i : ι) (a b : α i), s₁ i a b → s₂ i a b
i✝ j✝ : ι
a : α i✝
b : α j✝
hij : r₁ i✝ j✝
⊢ Lex r₂ s₂ ⟨i✝, a⟩ ⟨j✝, b⟩

Tactic:
exact Lex.left _ _ (hr _ _ hij)

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_2
r₁ r₂ : ι → ι → Prop
s₁ s₂ : (i : ι) → α i → α i → Prop
hr : ∀ (a b : ι), r₁ a b → r₂ a b
hs : ∀ (i : ι) (a b : α i), s₁ i a b → s₂ i a b
a b : (i : ι) × α i
h : Lex r₁ s₁ a b
⊢ Lex r₂ s₂ a b

Tactic:
obtain ⟨a, b, hij⟩ | ⟨a, b, hab⟩ := h

Result:
case left
ι : Type u_1
α : ι → Type u_2
r₁ r₂ : ι → ι → Prop
s₁ s₂ : (i : ι) → α i → α i → Prop
hr : ∀ (a b : ι), r₁ a b → r₂ a b
hs : ∀ (i : ι) (a b : α i), s₁ i a b → s₂ i a b
i✝ j✝ : ι
a : α i✝
b : α j✝
hij : r₁ i✝ j✝
⊢ Lex r₂ s₂ ⟨i✝, a⟩ ⟨j✝, b⟩

case right
ι : Type u_1
α : ι → Type u_2
r₁ r₂ : ι → ι → Prop
s₁ s₂ : (i : ι) → α i → α i → Prop
hr : ∀ (a b : ι), r₁ a b → r₂ a b
hs : ∀ (i : ι) (a b : α i), s₁ i a b → s₂ i a b
i✝ : ι
a b : α i✝
hab : s₁ i✝ a b
⊢ Lex r₂ s₂ ⟨i✝, a⟩ ⟨i✝, b⟩
-- Mathlib/InformationTheory/KullbackLeibler/Basic.lean
@[simp]
lemma klDiv_of_not_ac (h : ¬ μ ≪ ν) : klDiv μ ν = ∞

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : ¬μ ≪ ν
⊢ (if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), llr μ ν x ∂μ + (ν univ).toReal - (μ univ).toReal)
    else ⊤) =
    ⊤

Tactic:
exact if_neg (not_and_of_not_left _ h)

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : ¬μ ≪ ν
⊢ klDiv μ ν = ⊤

Tactic:
rw [klDiv_def]

Result:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : ¬μ ≪ ν
⊢ (if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), llr μ ν x ∂μ + (ν univ).toReal - (μ univ).toReal)
    else ⊤) =
    ⊤
-- Mathlib/Analysis/Calculus/Deriv/Basic.lean
theorem hasFDerivAtFilter_iff_hasDerivAtFilter {f' : 𝕜 →L[𝕜] F} :
    HasFDerivAtFilter f f' x L ↔ HasDerivAtFilter f (f' 1) x L

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : TopologicalSpace F
f : 𝕜 → F
x : 𝕜
L : Filter 𝕜
inst✝ : ContinuousSMul 𝕜 F
f' : 𝕜 →L[𝕜] F
⊢ HasFDerivAtFilter f f' x L ↔ HasDerivAtFilter f (f' 1) x L

Tactic:
simp [HasDerivAtFilter]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/AddContent.lean
lemma addContent_diff_of_ne_top (m : AddContent C) (hC : IsSetRing C)
    (hm_ne_top : ∀ s ∈ C, m s ≠ ∞)
    {s t : Set α} (hs : s ∈ C) (ht : t ∈ C) (hts : t ⊆ s) :
    m (s \ t) = m s - m t

Proof state:
α : Type u_1
C : Set (Set α)
m : AddContent C
hC : IsSetRing C
hm_ne_top : ∀ s ∈ C, m s ≠ ⊤
s t : Set α
hs : s ∈ C
ht : t ∈ C
hts : t ⊆ s
h_union : m s = m t + m (s \ t)
⊢ m (s \ t) = m s - m t

Tactic:
rw [h_union, ENNReal.add_sub_cancel_left (hm_ne_top _ ht)]

Result:
no goals

Proof state:
α : Type u_1
C : Set (Set α)
m : AddContent C
hC : IsSetRing C
hm_ne_top : ∀ s ∈ C, m s ≠ ⊤
s t : Set α
hs : s ∈ C
ht : t ∈ C
hts : t ⊆ s
h_union : m (t ∪ s \ t) = m t + m (s \ t)
⊢ m (s \ t) = m s - m t

Tactic:
simp_rw [Set.union_diff_self, Set.union_eq_right.mpr hts] at h_union

Result:
α : Type u_1
C : Set (Set α)
m : AddContent C
hC : IsSetRing C
hm_ne_top : ∀ s ∈ C, m s ≠ ⊤
s t : Set α
hs : s ∈ C
ht : t ∈ C
hts : t ⊆ s
h_union : m s = m t + m (s \ t)
⊢ m (s \ t) = m s - m t

Proof state:
α : Type u_1
C : Set (Set α)
m : AddContent C
hC : IsSetRing C
hm_ne_top : ∀ s ∈ C, m s ≠ ⊤
s t : Set α
hs : s ∈ C
ht : t ∈ C
hts : t ⊆ s
⊢ m (s \ t) = m s - m t

Tactic:
have h_union : m (t ∪ s \ t) = m t + m (s \ t) :=
  addContent_union hC ht (hC.diff_mem hs ht) disjoint_sdiff_self_right

Result:
α : Type u_1
C : Set (Set α)
m : AddContent C
hC : IsSetRing C
hm_ne_top : ∀ s ∈ C, m s ≠ ⊤
s t : Set α
hs : s ∈ C
ht : t ∈ C
hts : t ⊆ s
h_union : m (t ∪ s \ t) = m t + m (s \ t)
⊢ m (s \ t) = m s - m t
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Icc_eq_Ioo_same_iff : Icc a b = Ioo a b ↔ ¬a ≤ b where
  mp h

Proof state:
α : Type u_1
inst✝ : Preorder α
a b : α
h : ¬a ≤ b
⊢ Icc a b = Ioo a b

Tactic:
rw [Icc_eq_empty h, Ioo_eq_empty (mt le_of_lt h)]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
a b : α
h : Icc a b = Ioo a b
⊢ ¬a ≤ b

Tactic:
simpa using Set.ext_iff.mp h b

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
theorem WithSeminorms.continuousSMul (hp : WithSeminorms p) : ContinuousSMul 𝕜 E

Proof state:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
⊢ ContinuousSMul 𝕜 E

Tactic:
exact ModuleFilterBasis.continuousSMul _

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory.lean
theorem NatTrans.mapHomotopyCategory_id (c : ComplexShape ι) (F : V ⥤ W) [F.Additive] :
    NatTrans.mapHomotopyCategory (𝟙 F) c = 𝟙 (F.mapHomotopyCategory c)

Proof state:
ι : Type u_2
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
W : Type u_3
inst✝² : Category.{u_4, u_3} W
inst✝¹ : Preadditive W
c : ComplexShape ι
F : V ⥤ W
inst✝ : F.Additive
⊢ mapHomotopyCategory (𝟙 F) c = 𝟙 (F.mapHomotopyCategory c)

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
theorem HasFPowerSeriesAt.hasStrictFDerivAt (h : HasFPowerSeriesAt f p x) :
    HasStrictFDerivAt f (continuousMultilinearCurryFin1 𝕜 E F (p 1)) x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
x : E
h : HasFPowerSeriesAt f p x
⊢ HasStrictFDerivAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p 1)) x

Tactic:
simpa only [hasStrictFDerivAt_iff_isLittleO, Set.insert_eq_of_mem, Set.mem_univ,
    Set.univ_prod_univ, nhdsWithin_univ]
  using (h.hasFPowerSeriesWithinAt (s := Set.univ)).hasStrictFDerivWithinAt

Result:
no goals
-- Mathlib/Data/Real/Archimedean.lean
theorem sSup_empty : sSup (∅ : Set ℝ) = 0 :=
  dif_neg <| by simp

Proof state:
⊢ ¬(∅.Nonempty ∧ BddAbove ∅)

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem norm_div_eq_zero_iff : ‖a / b‖ = 0 ↔ a = b

Proof state:
E : Type u_5
inst✝ : NormedGroup E
a b : E
⊢ ‖a / b‖ = 0 ↔ a = b

Tactic:
rw [norm_eq_zero', div_eq_one]

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Pointwise.lean
theorem pow_eq_closure_pow_set (s : AddSubmonoid R) (n : ℕ) :
    s ^ n = closure ((s : Set R) ^ n)

Proof state:
R : Type u_4
inst✝ : Semiring R
s : AddSubmonoid R
n : ℕ
⊢ s ^ n = closure (↑s ^ n)

Tactic:
rw [← closure_pow, closure_eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getD_eq_fallback_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α}
    {fallback : β} : m.contains a = false → getD m a fallback = fallback

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
a : α
fallback : β
⊢ m.contains a = false → getD m a fallback = fallback

Tactic:
simp_to_raw using Raw₀.Const.getD_eq_fallback

Result:
no goals