harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Geometry/Manifold/ChartedSpace.lean
theorem ChartedSpace.secondCountable_of_countable_cover [SecondCountableTopology H] {s : Set M}
    (hs : ⋃ (x) (_ : x ∈ s), (chartAt H x).source = univ) (hsc : s.Countable) :
    SecondCountableTopology M

Proof state:
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SecondCountableTopology H
s : Set M
hs : ⋃ x, (chartAt H ↑x).source = univ
hsc : s.Countable
this✝ : ∀ (x : M), SecondCountableTopology ↑(chartAt H x).source
this : Encodable ↑s
⊢ SecondCountableTopology M

Tactic:
exact secondCountableTopology_of_countable_cover (fun x : s ↦ (chartAt H (x : M)).open_source) hs

Result:
no goals

Proof state:
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SecondCountableTopology H
s : Set M
hs : ⋃ x ∈ s, (chartAt H x).source = univ
hsc : s.Countable
⊢ SecondCountableTopology M

Tactic:
haveI : ∀ x : M, SecondCountableTopology (chartAt H x).source :=
  fun x ↦ (chartAt (H := H) x).secondCountableTopology_source

Result:
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SecondCountableTopology H
s : Set M
hs : ⋃ x ∈ s, (chartAt H x).source = univ
hsc : s.Countable
this : ∀ (x : M), SecondCountableTopology ↑(chartAt H x).source
⊢ SecondCountableTopology M

Proof state:
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SecondCountableTopology H
s : Set M
hs : ⋃ x ∈ s, (chartAt H x).source = univ
hsc : s.Countable
this : ∀ (x : M), SecondCountableTopology ↑(chartAt H x).source
⊢ SecondCountableTopology M

Tactic:
haveI := hsc.toEncodable

Result:
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SecondCountableTopology H
s : Set M
hs : ⋃ x ∈ s, (chartAt H x).source = univ
hsc : s.Countable
this✝ : ∀ (x : M), SecondCountableTopology ↑(chartAt H x).source
this : Encodable ↑s
⊢ SecondCountableTopology M

Proof state:
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SecondCountableTopology H
s : Set M
hs : ⋃ x ∈ s, (chartAt H x).source = univ
hsc : s.Countable
this✝ : ∀ (x : M), SecondCountableTopology ↑(chartAt H x).source
this : Encodable ↑s
⊢ SecondCountableTopology M

Tactic:
rw [biUnion_eq_iUnion] at hs

Result:
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SecondCountableTopology H
s : Set M
hs : ⋃ x, (chartAt H ↑x).source = univ
hsc : s.Countable
this✝ : ∀ (x : M), SecondCountableTopology ↑(chartAt H x).source
this : Encodable ↑s
⊢ SecondCountableTopology M
-- Mathlib/RingTheory/Kaehler/Basic.lean
theorem KaehlerDifferential.D_tensorProductTo (x : KaehlerDifferential.ideal R S) :
    (KaehlerDifferential.D R S).tensorProductTo x =
      (KaehlerDifferential.ideal R S).toCotangent x

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : ↥(ideal R S)
⊢ LinearMap.id ((ideal R S).toCotangent x) = (ideal R S).toCotangent x

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : ↥(ideal R S)
⊢ (D R S).tensorProductTo ↑x = (ideal R S).toCotangent x

Tactic:
rw [← Derivation.liftKaehlerDifferential_apply, Derivation.liftKaehlerDifferential_D]

Result:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : ↥(ideal R S)
⊢ LinearMap.id ((ideal R S).toCotangent x) = (ideal R S).toCotangent x
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem mk_finset_of_infinite (α : Type u) [Infinite α] : #(Finset α) = #α

Proof state:
α : Type u
inst✝ : Infinite α
⊢ #(Finset α) = #α

Tactic:
exact Eq.symm <|
  le_antisymm (mk_le_of_injective fun _ _ => Finset.singleton_inj.1) <|
    calc
      #(Finset α) ≤ #(List α) := mk_le_of_surjective List.toFinset_surjective
      _ = #α := mk_list_eq_mk α

Result:
no goals

Proof state:
α : Type u
inst✝ : Infinite α
⊢ #(Finset α) = #α

Tactic:
classical
exact Eq.symm <|
  le_antisymm (mk_le_of_injective fun _ _ => Finset.singleton_inj.1) <|
    calc
      #(Finset α) ≤ #(List α) := mk_le_of_surjective List.toFinset_surjective
      _ = #α := mk_list_eq_mk α

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem oangle_neg_left_eq_neg_right (x y : V) : o.oangle (-x) y = o.oangle x (-y)

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ o.oangle (-x) y = o.oangle x (-y)

Tactic:
rw [← neg_neg y, oangle_neg_neg, neg_neg]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Quotient.lean
theorem norm_trivial_quotient_mk (S : AddSubgroup M)
    (h : (S.topologicalClosure : Set M) = Set.univ) : ‖S.normedMk‖ = 0

Proof state:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
h : ↑S.topologicalClosure = univ
⊢ ‖S.normedMk‖ = 0

Tactic:
refine le_antisymm (opNorm_le_bound _ le_rfl fun x => ?_) (norm_nonneg _)

Result:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
h : ↑S.topologicalClosure = univ
x : M
⊢ ‖S.normedMk x‖ ≤ 0 * ‖x‖

Proof state:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
h : ↑S.topologicalClosure = univ
x : M
hker : x ∈ S.normedMk.ker.topologicalClosure
⊢ ‖S.normedMk x‖ ≤ 0 * ‖x‖

Tactic:
rw [ker_normedMk] at hker

Result:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
h : ↑S.topologicalClosure = univ
x : M
hker : x ∈ S.topologicalClosure
⊢ ‖S.normedMk x‖ ≤ 0 * ‖x‖

Proof state:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
h : ↑S.topologicalClosure = univ
x : M
⊢ ‖S.normedMk x‖ ≤ 0 * ‖x‖

Tactic:
have hker : x ∈ S.normedMk.ker.topologicalClosure := by
  rw [S.ker_normedMk, ← SetLike.mem_coe, h]
  trivial

Result:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
h : ↑S.topologicalClosure = univ
x : M
hker : x ∈ S.normedMk.ker.topologicalClosure
⊢ ‖S.normedMk x‖ ≤ 0 * ‖x‖

Proof state:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
h : ↑S.topologicalClosure = univ
x : M
⊢ x ∈ univ

Tactic:
trivial

Result:
no goals

Proof state:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
h : ↑S.topologicalClosure = univ
x : M
hker : x ∈ S.topologicalClosure
⊢ ‖S.normedMk x‖ ≤ 0 * ‖x‖

Tactic:
simp only [(quotient_norm_eq_zero_iff S x).mpr hker, normedMk.apply, zero_mul, le_rfl]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
h : ↑S.topologicalClosure = univ
x : M
⊢ x ∈ S.normedMk.ker.topologicalClosure

Tactic:
rw [S.ker_normedMk, ← SetLike.mem_coe, h]

Result:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
h : ↑S.topologicalClosure = univ
x : M
⊢ x ∈ univ
-- Mathlib/RingTheory/Localization/Away/Basic.lean
theorem selfZPow_neg_natCast (d : ℕ) : selfZPow x B (-d) = mk' _ (1 : R) (Submonoid.pow x d)

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
d : ℕ
⊢ selfZPow x B (-↑d) = mk' B 1 (Submonoid.pow x d)

Tactic:
simp [selfZPow_of_nonpos _ _ (neg_nonpos.mpr (Int.natCast_nonneg d))]

Result:
no goals
-- Mathlib/Analysis/PSeries.lean
theorem summable_pow_div_add {α : Type*} (x : α) [RCLike α] (q k : ℕ) (hq : 1 < q) :
    Summable fun n : ℕ => ‖(x / (↑n + k) ^ q)‖

Proof state:
case h
α : Type u_1
x : α
inst✝ : RCLike α
q k : ℕ
hq : 1 < q
⊢ Summable fun x => 1 / ‖(↑x + ↑k) ^ q‖

Tactic:
simpa [hq, Nat.cast_add, one_div, norm_inv, norm_pow, RCLike.norm_natCast,
  Real.summable_nat_pow_inv, iff_true]
    using summable_nat_add_iff (f := fun x => ‖1 / (x ^ q : α)‖) k

Result:
no goals

Proof state:
α : Type u_1
x : α
inst✝ : RCLike α
q k : ℕ
hq : 1 < q
⊢ Summable fun n => ‖x‖ / ‖(↑n + ↑k) ^ q‖

Tactic:
apply Summable.const_div

Result:
case h
α : Type u_1
x : α
inst✝ : RCLike α
q k : ℕ
hq : 1 < q
⊢ Summable fun x => 1 / ‖(↑x + ↑k) ^ q‖

Proof state:
α : Type u_1
x : α
inst✝ : RCLike α
q k : ℕ
hq : 1 < q
⊢ Summable fun n => ‖x / (↑n + ↑k) ^ q‖

Tactic:
simp_rw [norm_div]

Result:
α : Type u_1
x : α
inst✝ : RCLike α
q k : ℕ
hq : 1 < q
⊢ Summable fun n => ‖x‖ / ‖(↑n + ↑k) ^ q‖
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem append_eq_of_isSuffixOf?_eq_some [BEq α] [LawfulBEq α] {xs ys zs : List α}
    (h : xs.isSuffixOf? ys = some zs) : zs ++ xs = ys

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
xs ys zs : List α
h : xs.isSuffixOf? ys = some zs
⊢ zs ++ xs = ys

Tactic:
simp_all

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
theorem smul_dotProduct [IsScalarTower R α α] (x : R) (v w : m → α) :
    x • v ⬝ᵥ w = x • (v ⬝ᵥ w)

Proof state:
m : Type u_2
R : Type u_7
α : Type v
inst✝⁵ : Fintype m
inst✝⁴ : Monoid R
inst✝³ : Mul α
inst✝² : AddCommMonoid α
inst✝¹ : DistribMulAction R α
inst✝ : IsScalarTower R α α
x : R
v w : m → α
⊢ x • v ⬝ᵥ w = x • (v ⬝ᵥ w)

Tactic:
simp [dotProduct, Finset.smul_sum, smul_mul_assoc]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/InverseDeriv.lean
theorem hasDerivWithinAt_arcsin_Iic {x : ℝ} (h : x ≠ 1) :
    HasDerivWithinAt arcsin (1 / √(1 - x ^ 2)) (Iic x) x

Proof state:
case inl
h : -1 ≠ 1
⊢ HasDerivWithinAt arcsin (1 / √(1 - (-1) ^ 2)) (Iic (-1)) (-1)

Tactic:
convert (hasDerivWithinAt_const (-1 : ℝ) _ (-(π / 2))).congr _ _ <;>
  simp +contextual [arcsin_of_le_neg_one]

Result:
no goals

Proof state:
x : ℝ
h : x ≠ 1
⊢ HasDerivWithinAt arcsin (1 / √(1 - x ^ 2)) (Iic x) x

Tactic:
rcases em (x = -1) with (rfl | h')

Result:
case inl
h : -1 ≠ 1
⊢ HasDerivWithinAt arcsin (1 / √(1 - (-1) ^ 2)) (Iic (-1)) (-1)

case inr
x : ℝ
h : x ≠ 1
h' : ¬x = -1
⊢ HasDerivWithinAt arcsin (1 / √(1 - x ^ 2)) (Iic x) x

Proof state:
case inr
x : ℝ
h : x ≠ 1
h' : ¬x = -1
⊢ HasDerivWithinAt arcsin (1 / √(1 - x ^ 2)) (Iic x) x

Tactic:
exact (hasDerivAt_arcsin h' h).hasDerivWithinAt

Result:
no goals
-- Mathlib/Geometry/Euclidean/Inversion/Basic.lean
theorem inversion_dist_center (c x : P) : inversion c (dist x c) x = x

Proof state:
case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x : P
hne : x ≠ c
⊢ inversion c (dist x c) x = x

Tactic:
rw [inversion, div_self, one_pow, one_smul, vsub_vadd]

Result:
case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x : P
hne : x ≠ c
⊢ dist x c ≠ 0

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x : P
⊢ inversion c (dist x c) x = x

Tactic:
rcases eq_or_ne x c with (rfl | hne)

Result:
case inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
x : P
⊢ inversion x (dist x x) x = x

case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x : P
hne : x ≠ c
⊢ inversion c (dist x c) x = x

Proof state:
case inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
x : P
⊢ inversion x (dist x x) x = x

Tactic:
apply inversion_self

Result:
no goals

Proof state:
case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x : P
hne : x ≠ c
⊢ dist x c ≠ 0

Tactic:
rwa [dist_ne_zero]

Result:
no goals
-- Mathlib/Data/Finset/Basic.lean
theorem filter_cons {a : α} (s : Finset α) (ha : a ∉ s) :
    filter p (cons a s ha) =
      if p a then cons a (filter p s) ((mem_of_mem_filter _).mt ha) else filter p s

Proof state:
case pos
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Finset α
ha : a ∉ s
h : p a
⊢ filter p (cons a s ha) = cons a (filter p s) ⋯

Tactic:
rw [filter_cons_of_pos _ _ _ ha h]

Result:
no goals

Proof state:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Finset α
ha : a ∉ s
⊢ filter p (cons a s ha) = if p a then cons a (filter p s) ⋯ else filter p s

Tactic:
split_ifs with h

Result:
case pos
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Finset α
ha : a ∉ s
h : p a
⊢ filter p (cons a s ha) = cons a (filter p s) ⋯

case neg
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Finset α
ha : a ∉ s
h : ¬p a
⊢ filter p (cons a s ha) = filter p s

Proof state:
case neg
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Finset α
ha : a ∉ s
h : ¬p a
⊢ filter p (cons a s ha) = filter p s

Tactic:
rw [filter_cons_of_neg _ _ _ ha h]

Result:
no goals
-- Mathlib/Algebra/Polynomial/BigOperators.lean
theorem leadingCoeff_multiset_prod :
    t.prod.leadingCoeff = (t.map fun f => leadingCoeff f).prod

Proof state:
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
t : Multiset R[X]
⊢ (Multiset.map (⇑leadingCoeffHom) t).prod = (Multiset.map (fun f => f.leadingCoeff) t).prod

Tactic:
simp only [leadingCoeffHom_apply]

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
t : Multiset R[X]
⊢ t.prod.leadingCoeff = (Multiset.map (fun f => f.leadingCoeff) t).prod

Tactic:
rw [← leadingCoeffHom_apply, MonoidHom.map_multiset_prod]

Result:
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
t : Multiset R[X]
⊢ (Multiset.map (⇑leadingCoeffHom) t).prod = (Multiset.map (fun f => f.leadingCoeff) t).prod
-- Mathlib/Algebra/Group/End.lean
theorem zpow_apply_comm {α : Type*} (σ : Perm α) (m n : ℤ) {x : α} :
    (σ ^ m) ((σ ^ n) x) = (σ ^ n) ((σ ^ m) x)

Proof state:
α : Type u_6
σ : Perm α
m n : ℤ
x : α
⊢ (σ ^ m) ((σ ^ n) x) = (σ ^ n) ((σ ^ m) x)

Tactic:
rw [← Equiv.Perm.mul_apply, ← Equiv.Perm.mul_apply, zpow_mul_comm]

Result:
no goals
-- Mathlib/Order/Filter/Partial.lean
theorem rtendsto_iff_le_rcomap (r : Rel α β) (l₁ : Filter α) (l₂ : Filter β) :
    RTendsto r l₁ l₂ ↔ l₁ ≤ l₂.rcomap r

Proof state:
α : Type u
β : Type v
r : Rel α β
l₁ : Filter α
l₂ : Filter β
⊢ RTendsto r l₁ l₂ ↔ l₁ ≤ rcomap r l₂

Tactic:
rw [rtendsto_def]

Result:
α : Type u
β : Type v
r : Rel α β
l₁ : Filter α
l₂ : Filter β
⊢ (∀ s ∈ l₂, r.core s ∈ l₁) ↔ l₁ ≤ rcomap r l₂

Proof state:
α : Type u
β : Type v
r : Rel α β
l₁ : Filter α
l₂ : Filter β
⊢ (∀ s ∈ l₂, r.core s ∈ l₁) ↔ l₁ ≤ rcomap r l₂

Tactic:
simp_rw [← l₂.mem_sets]

Result:
α : Type u
β : Type v
r : Rel α β
l₁ : Filter α
l₂ : Filter β
⊢ (∀ s ∈ l₂.sets, r.core s ∈ l₁) ↔ l₁ ≤ rcomap r l₂

Proof state:
case mpr
α : Type u
β : Type v
r : Rel α β
l₁ : Filter α
l₂ : Filter β
⊢ l₁ ≤ rcomap r l₂ → ∀ s ∈ l₂.sets, r.core s ∈ l₁

Tactic:
simpa [Filter.le_def, rcomap, Rel.mem_image] using fun h t tl₂ => h _ t tl₂ Set.Subset.rfl

Result:
no goals

Proof state:
α : Type u
β : Type v
r : Rel α β
l₁ : Filter α
l₂ : Filter β
⊢ (∀ s ∈ l₂.sets, r.core s ∈ l₁) ↔ l₁ ≤ rcomap r l₂

Tactic:
constructor

Result:
case mp
α : Type u
β : Type v
r : Rel α β
l₁ : Filter α
l₂ : Filter β
⊢ (∀ s ∈ l₂.sets, r.core s ∈ l₁) → l₁ ≤ rcomap r l₂

case mpr
α : Type u
β : Type v
r : Rel α β
l₁ : Filter α
l₂ : Filter β
⊢ l₁ ≤ rcomap r l₂ → ∀ s ∈ l₂.sets, r.core s ∈ l₁

Proof state:
case mp
α : Type u
β : Type v
r : Rel α β
l₁ : Filter α
l₂ : Filter β
⊢ (∀ s ∈ l₂.sets, r.core s ∈ l₁) → l₁ ≤ rcomap r l₂

Tactic:
simpa [Filter.le_def, rcomap, Rel.mem_image] using fun h s t tl₂ => mem_of_superset (h t tl₂)

Result:
no goals
-- Mathlib/Algebra/Group/Indicator.lean
theorem mulIndicator_one (s : Set α) : (mulIndicator s fun _ => (1 : M)) = fun _ => (1 : M) :=
  mulIndicator_eq_one.2 <| by simp only [mulSupport_one, empty_disjoint]

Proof state:
α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
⊢ Disjoint (mulSupport fun x => 1) s

Tactic:
simp only [mulSupport_one, empty_disjoint]

Result:
no goals
-- Mathlib/Algebra/Homology/DerivedCategory/Ext/Basic.lean
@[simp]
lemma zero_hom : (0 : Ext X Y n).hom = 0

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y : C
n : ℕ
inst✝ : HasDerivedCategory C
β : Ext 0 Y n := 0
hβ : β.hom = 0
this : 0 = comp 0 β ⋯
⊢ hom 0 = 0

Tactic:
rw [this, comp_hom, hβ, ShiftedHom.comp_zero]

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y : C
n : ℕ
inst✝ : HasDerivedCategory C
β : Ext 0 Y n := 0
⊢ hom 0 = 0

Tactic:
have hβ : β.hom = 0 := by apply (Functor.map_isZero _ (isZero_zero C)).eq_of_src

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y : C
n : ℕ
inst✝ : HasDerivedCategory C
β : Ext 0 Y n := 0
hβ : β.hom = 0
⊢ hom 0 = 0

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y : C
n : ℕ
inst✝ : HasDerivedCategory C
β : Ext 0 Y n := 0
hβ : β.hom = 0
⊢ hom 0 = 0

Tactic:
have : (0 : Ext X Y n) = (0 : Ext X 0 0).comp β (zero_add n) := by simp [β]

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y : C
n : ℕ
inst✝ : HasDerivedCategory C
β : Ext 0 Y n := 0
hβ : β.hom = 0
this : 0 = comp 0 β ⋯
⊢ hom 0 = 0

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y : C
n : ℕ
inst✝ : HasDerivedCategory C
⊢ hom 0 = 0

Tactic:
let β : Ext 0 Y n := 0

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y : C
n : ℕ
inst✝ : HasDerivedCategory C
β : Ext 0 Y n := 0
⊢ hom 0 = 0

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y : C
n : ℕ
inst✝ : HasDerivedCategory C
β : Ext 0 Y n := 0
hβ : β.hom = 0
⊢ 0 = comp 0 β ⋯

Tactic:
simp [β]

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y : C
n : ℕ
inst✝ : HasDerivedCategory C
β : Ext 0 Y n := 0
⊢ β.hom = 0

Tactic:
apply (Functor.map_isZero _ (isZero_zero C)).eq_of_src

Result:
no goals
-- Mathlib/CategoryTheory/GradedObject/Monoidal.lean
@[reassoc (attr := simp)]
lemma ι_tensorHom {X₁ X₂ Y₁ Y₂ : GradedObject I C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂)
    [HasTensor X₁ Y₁] [HasTensor X₂ Y₂] (i₁ i₂ i₁₂ : I) (h : i₁ + i₂ = i₁₂) :
    ιTensorObj X₁ Y₁ i₁ i₂ i₁₂ h ≫ tensorHom f g i₁₂ =
      (f i₁ ⊗ g i₂) ≫ ιTensorObj X₂ Y₂ i₁ i₂ i₁₂ h

Proof state:
I : Type u
inst✝⁴ : AddMonoid I
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : MonoidalCategory C
X₁ X₂ Y₁ Y₂ : GradedObject I C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
inst✝¹ : X₁.HasTensor Y₁
inst✝ : X₂.HasTensor Y₂
i₁ i₂ i₁₂ : I
h : i₁ + i₂ = i₁₂
⊢ ιTensorObj X₁ Y₁ i₁ i₂ i₁₂ h ≫ tensorHom f g i₁₂ = (f i₁ ⊗ g i₂) ≫ ιTensorObj X₂ Y₂ i₁ i₂ i₁₂ h

Tactic:
rw [MonoidalCategory.tensorHom_def, assoc]

Result:
I : Type u
inst✝⁴ : AddMonoid I
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : MonoidalCategory C
X₁ X₂ Y₁ Y₂ : GradedObject I C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
inst✝¹ : X₁.HasTensor Y₁
inst✝ : X₂.HasTensor Y₂
i₁ i₂ i₁₂ : I
h : i₁ + i₂ = i₁₂
⊢ ιTensorObj X₁ Y₁ i₁ i₂ i₁₂ h ≫ tensorHom f g i₁₂ = f i₁ ▷ Y₁ i₂ ≫ X₂ i₁ ◁ g i₂ ≫ ιTensorObj X₂ Y₂ i₁ i₂ i₁₂ h

Proof state:
I : Type u
inst✝⁴ : AddMonoid I
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : MonoidalCategory C
X₁ X₂ Y₁ Y₂ : GradedObject I C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
inst✝¹ : X₁.HasTensor Y₁
inst✝ : X₂.HasTensor Y₂
i₁ i₂ i₁₂ : I
h : i₁ + i₂ = i₁₂
⊢ ιTensorObj X₁ Y₁ i₁ i₂ i₁₂ h ≫ tensorHom f g i₁₂ = f i₁ ▷ Y₁ i₂ ≫ X₂ i₁ ◁ g i₂ ≫ ιTensorObj X₂ Y₂ i₁ i₂ i₁₂ h

Tactic:
apply ι_mapBifunctorMapMap

Result:
no goals
-- Mathlib/Data/Matroid/Sum.lean
@[simp] lemma disjointSigma_ground_eq {h} : (Matroid.disjointSigma M h).E = ⋃ i : ι, (M i).E

Proof state:
case h
α : Type u_1
ι : Type u_2
M : ι → Matroid α
h : Pairwise (Disjoint on fun i => (M i).E)
x✝ : α
⊢ x✝ ∈ (Matroid.disjointSigma M h).E ↔ x✝ ∈ ⋃ i, (M i).E

Tactic:
simp [Matroid.disjointSigma, mapEmbedding, restrictSubtype]

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_2
M : ι → Matroid α
h : Pairwise (Disjoint on fun i => (M i).E)
⊢ (Matroid.disjointSigma M h).E = ⋃ i, (M i).E

Tactic:
ext

Result:
case h
α : Type u_1
ι : Type u_2
M : ι → Matroid α
h : Pairwise (Disjoint on fun i => (M i).E)
x✝ : α
⊢ x✝ ∈ (Matroid.disjointSigma M h).E ↔ x✝ ∈ ⋃ i, (M i).E
-- Mathlib/Algebra/Group/Pointwise/Set/Card.lean
@[to_additive (attr := simp)]
lemma encard_inv (s : Set G) : s⁻¹.encard = s.encard

Proof state:
G : Type u_1
inst✝ : InvolutiveInv G
s : Set G
⊢ s⁻¹.encard = s.encard

Tactic:
simp [ENat.card, ← toENat_cardinalMk]

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/Defs.lean
theorem Basis.coe_ofEquivFun [Finite ι] [DecidableEq ι] (e : M ≃ₗ[R] ι → R) :
    (Basis.ofEquivFun e : ι → M) = fun i => e.symm (Pi.single i 1) :=
  funext fun i =>
    e.injective <|
      funext fun j => by
        simp [Basis.ofEquivFun, ← Finsupp.single_eq_pi_single]

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
e : M ≃ₗ[R] ι → R
i j : ι
⊢ e ((ofEquivFun e) i) j = e (e.symm (Pi.single i 1)) j

Tactic:
simp [Basis.ofEquivFun, ← Finsupp.single_eq_pi_single]

Result:
no goals
-- Mathlib/FieldTheory/ChevalleyWarning.lean
theorem char_dvd_card_solutions_of_add_lt {f₁ f₂ : MvPolynomial σ K}
    (h : f₁.totalDegree + f₂.totalDegree < Fintype.card σ) :
    p ∣ Fintype.card { x : σ → K // eval x f₁ = 0 ∧ eval x f₂ = 0 }

Proof state:
K : Type u_1
σ : Type u_2
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
f₁ f₂ : MvPolynomial σ K
h : f₁.totalDegree + f₂.totalDegree < Fintype.card σ
⊢ p ∣ Fintype.card { x // (eval x) f₁ = 0 ∧ (eval x) f₂ = 0 }

Tactic:
let F : Bool → MvPolynomial σ K := fun b => cond b f₂ f₁

Result:
K : Type u_1
σ : Type u_2
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
f₁ f₂ : MvPolynomial σ K
h : f₁.totalDegree + f₂.totalDegree < Fintype.card σ
F : Bool → MvPolynomial σ K := fun b => bif b then f₂ else f₁
⊢ p ∣ Fintype.card { x // (eval x) f₁ = 0 ∧ (eval x) f₂ = 0 }

Proof state:
K : Type u_1
σ : Type u_2
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
f₁ f₂ : MvPolynomial σ K
h : f₁.totalDegree + f₂.totalDegree < Fintype.card σ
F : Bool → MvPolynomial σ K := fun b => bif b then f₂ else f₁
this : ∑ b : Bool, (F b).totalDegree < Fintype.card σ
⊢ p ∣ Fintype.card { x // (eval x) f₁ = 0 ∧ (eval x) f₂ = 0 }

Tactic:
simpa only [Bool.forall_bool] using char_dvd_card_solutions_of_fintype_sum_lt p this

Result:
no goals

Proof state:
K : Type u_1
σ : Type u_2
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
f₁ f₂ : MvPolynomial σ K
h : f₁.totalDegree + f₂.totalDegree < Fintype.card σ
F : Bool → MvPolynomial σ K := fun b => bif b then f₂ else f₁
⊢ p ∣ Fintype.card { x // (eval x) f₁ = 0 ∧ (eval x) f₂ = 0 }

Tactic:
have : (∑ b : Bool, (F b).totalDegree) < Fintype.card σ := (add_comm _ _).trans_lt h

Result:
K : Type u_1
σ : Type u_2
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
f₁ f₂ : MvPolynomial σ K
h : f₁.totalDegree + f₂.totalDegree < Fintype.card σ
F : Bool → MvPolynomial σ K := fun b => bif b then f₂ else f₁
this : ∑ b : Bool, (F b).totalDegree < Fintype.card σ
⊢ p ∣ Fintype.card { x // (eval x) f₁ = 0 ∧ (eval x) f₂ = 0 }
-- Mathlib/LinearAlgebra/Lagrange.lean
theorem nodal_insert_eq_nodal [DecidableEq ι] {i : ι} (hi : i ∉ s) :
    nodal (insert i s) v = (X - C (v i)) * nodal s v

Proof state:
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst✝ : DecidableEq ι
i : ι
hi : i ∉ s
⊢ nodal (insert i s) v = (X - C (v i)) * nodal s v

Tactic:
simp_rw [nodal, prod_insert hi]

Result:
no goals