harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/SetFamily/Compression/UV.lean
theorem aux (huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜) :
    v = ∅ → u = ∅

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
⊢ v = ∅ → u = ∅

Tactic:
rintro rfl

Result:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u : Finset α
huv : ∀ x ∈ u, ∃ y ∈ ∅, IsCompressed (u.erase x) (∅.erase y) 𝒜
⊢ u = ∅

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u : Finset α
huv : ∀ x ∈ u, ∃ y ∈ ∅, IsCompressed (u.erase x) (∅.erase y) 𝒜
a : α
ha : a ∈ u
⊢ False

Tactic:
obtain ⟨_, ⟨⟩, -⟩ := huv a ha

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u : Finset α
huv : ∀ x ∈ u, ∃ y ∈ ∅, IsCompressed (u.erase x) (∅.erase y) 𝒜
⊢ u = ∅

Tactic:
refine eq_empty_of_forall_not_mem fun a ha ↦ ?_

Result:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u : Finset α
huv : ∀ x ∈ u, ∃ y ∈ ∅, IsCompressed (u.erase x) (∅.erase y) 𝒜
a : α
ha : a ∈ u
⊢ False
-- Mathlib/AlgebraicTopology/DoldKan/EquivalencePseudoabelian.lean
theorem hη :
    Compatibility.τ₀ =
      Compatibility.τ₁ isoN₁ isoΓ₀
        (N₁Γ₀ : Γ ⋙ N₁ ≅ (toKaroubiEquivalence (ChainComplex C ℕ)).functor)

Proof state:
case w.w.h
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ Preadditive.DoldKan.equivalence.counitIso.hom.app ((toKaroubiEquivalence (ChainComplex C ℕ)).functor.obj K) =
    Preadditive.DoldKan.equivalence.functor.map (isoΓ₀.hom.app K) ≫ isoN₁.hom.app (Γ.obj K) ≫ N₁Γ₀.hom.app K

Tactic:
exact (N₂Γ₂_compatible_with_N₁Γ₀ K).trans (by simp )

Result:
no goals

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
⊢ Compatibility.τ₀ = Compatibility.τ₁ isoN₁ isoΓ₀ N₁Γ₀

Tactic:
ext K : 3

Result:
case w.w.h
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ Compatibility.τ₀.hom.app K = (Compatibility.τ₁ isoN₁ isoΓ₀ N₁Γ₀).hom.app K

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ N₂Γ₂ToKaroubiIso.hom.app K ≫ N₁Γ₀.hom.app K =
    Preadditive.DoldKan.equivalence.functor.map (isoΓ₀.hom.app K) ≫ isoN₁.hom.app (Γ.obj K) ≫ N₁Γ₀.hom.app K

Tactic:
simp

Result:
no goals

Proof state:
case w.w.h
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ Compatibility.τ₀.hom.app K = (Compatibility.τ₁ isoN₁ isoΓ₀ N₁Γ₀).hom.app K

Tactic:
simp only [Compatibility.τ₀_hom_app, Compatibility.τ₁_hom_app]

Result:
case w.w.h
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ Preadditive.DoldKan.equivalence.counitIso.hom.app ((toKaroubiEquivalence (ChainComplex C ℕ)).functor.obj K) =
    Preadditive.DoldKan.equivalence.functor.map (isoΓ₀.hom.app K) ≫ isoN₁.hom.app (Γ.obj K) ≫ N₁Γ₀.hom.app K
-- Mathlib/GroupTheory/DoubleCoset.lean
theorem right_bot_eq_right_quot (H : Subgroup G) :
    Quotient (H : Set G) (⊥ : Subgroup G) = _root_.Quotient (QuotientGroup.rightRel H)

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ Quotient ↑H ↑⊥ = _root_.Quotient (QuotientGroup.rightRel H)

Tactic:
unfold Quotient

Result:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ _root_.Quotient (setoid ↑H ↑⊥) = _root_.Quotient (QuotientGroup.rightRel H)

Proof state:
case e_s
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ setoid ↑H ↑⊥ = QuotientGroup.rightRel H

Tactic:
ext

Result:
case e_s.a
G : Type u_1
inst✝ : Group G
H : Subgroup G
a✝ b✝ : G
⊢ (setoid ↑H ↑⊥) a✝ b✝ ↔ (QuotientGroup.rightRel H) a✝ b✝

Proof state:
case e_s.a
G : Type u_1
inst✝ : Group G
H : Subgroup G
a✝ b✝ : G
⊢ (setoid ↑H ↑⊥) a✝ b✝ ↔ (QuotientGroup.rightRel H) a✝ b✝

Tactic:
simp_rw [← rel_bot_eq_right_group_rel H]

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ _root_.Quotient (setoid ↑H ↑⊥) = _root_.Quotient (QuotientGroup.rightRel H)

Tactic:
congr

Result:
case e_s
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ setoid ↑H ↑⊥ = QuotientGroup.rightRel H
-- Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean
theorem _root_.stronglyMeasurable_of_stronglyMeasurable_union_cover {m : MeasurableSpace α}
    [TopologicalSpace β] {f : α → β} (s t : Set α) (hs : MeasurableSet s) (ht : MeasurableSet t)
    (h : univ ⊆ s ∪ t) (hc : StronglyMeasurable fun a : s => f a)
    (hd : StronglyMeasurable fun a : t => f a) : StronglyMeasurable f

Proof state:
case pos.intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a => f ↑a
hd : StronglyMeasurable fun a => f ↑a
a✝ : Nontrivial β
inhabited_h : Inhabited β
x : { x // x ∈ s }
⊢ Function.extend Subtype.val (fun x => f ↑x) (Function.extend Subtype.val (fun x => f ↑x) fun x => default) ↑x = f ↑x

Tactic:
simp [Subtype.coe_injective.extend_apply]

Result:
no goals
-- Mathlib/Analysis/Complex/UpperHalfPlane/Topology.lean
lemma ofComplex_apply_eq_ite (w : ℂ) :
    ofComplex w = if hw : 0 < w.im then ⟨w, hw⟩ else Classical.choice inferInstance

Proof state:
case neg
w : ℂ
hw : ¬0 < w.im
⊢ ↑ofComplex w = Classical.choice ⋯

Tactic:
change (Function.invFunOn UpperHalfPlane.coe Set.univ w) = _

Result:
case neg
w : ℂ
hw : ¬0 < w.im
⊢ invFunOn UpperHalfPlane.coe univ w = Classical.choice ⋯

Proof state:
a : ℍ
hw : ¬0 < (↑a).im
⊢ (↑a).im ≤ 0

Tactic:
simpa using hw

Result:
no goals

Proof state:
case neg
w : ℂ
hw : ¬0 < w.im
⊢ invFunOn UpperHalfPlane.coe univ w = Classical.choice ⋯

Tactic:
simp only [invFunOn, dite_eq_right_iff, mem_univ, true_and]

Result:
case neg
w : ℂ
hw : ¬0 < w.im
⊢ ∀ (h : ∃ a, ↑a = w), Classical.choose ⋯ = Classical.choice ⋯

Proof state:
case pos
w : ℂ
hw : 0 < w.im
⊢ ↑ofComplex w = ⟨w, hw⟩

Tactic:
exact ofComplex_apply ⟨w, hw⟩

Result:
no goals

Proof state:
case neg.intro
a : ℍ
hw : ¬0 < (↑a).im
⊢ Classical.choose ⋯ = Classical.choice ⋯

Tactic:
exact (a.prop.not_le (by simpa using hw)).elim

Result:
no goals

Proof state:
w : ℂ
⊢ ↑ofComplex w = if hw : 0 < w.im then ⟨w, hw⟩ else Classical.choice ⋯

Tactic:
split_ifs with hw

Result:
case pos
w : ℂ
hw : 0 < w.im
⊢ ↑ofComplex w = ⟨w, hw⟩

case neg
w : ℂ
hw : ¬0 < w.im
⊢ ↑ofComplex w = Classical.choice ⋯

Proof state:
case neg
w : ℂ
hw : ¬0 < w.im
⊢ ∀ (h : ∃ a, ↑a = w), Classical.choose ⋯ = Classical.choice ⋯

Tactic:
rintro ⟨a, rfl⟩

Result:
case neg.intro
a : ℍ
hw : ¬0 < (↑a).im
⊢ Classical.choose ⋯ = Classical.choice ⋯
-- Mathlib/NumberTheory/ModularForms/JacobiTheta/TwoVariable.lean
/-- A uniform upper bound for `jacobiTheta₂'_term` on compact subsets. -/
lemma norm_jacobiTheta₂'_term_le {S T : ℝ} (hT : 0 < T) {z τ : ℂ}
    (hz : |im z| ≤ S) (hτ : T ≤ im τ) (n : ℤ) :
    ‖jacobiTheta₂'_term n z τ‖ ≤ 2 * π * |n| * rexp (-π * (T * n ^ 2 - 2 * S * |n|))

Proof state:
S T : ℝ
hT : 0 < T
z τ : ℂ
hz : |z.im| ≤ S
hτ : T ≤ τ.im
n : ℤ
⊢ ‖2 * ↑π * I * ↑n‖ * ‖jacobiTheta₂_term n z τ‖ ≤ 2 * π * ↑|n| * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))

Tactic:
refine mul_le_mul (le_of_eq ?_) (norm_jacobiTheta₂_term_le hT hz hτ n)
  (norm_nonneg _) (by positivity)

Result:
S T : ℝ
hT : 0 < T
z τ : ℂ
hz : |z.im| ≤ S
hτ : T ≤ τ.im
n : ℤ
⊢ ‖2 * ↑π * I * ↑n‖ = 2 * π * ↑|n|

Proof state:
S T : ℝ
hT : 0 < T
z τ : ℂ
hz : |z.im| ≤ S
hτ : T ≤ τ.im
n : ℤ
⊢ ‖2 * ↑π * I * ↑n‖ = 2 * π * ↑|n|

Tactic:
simp only [norm_mul, Complex.norm_two, norm_I, Complex.norm_of_nonneg pi_pos.le,
  norm_intCast, mul_one, Int.cast_abs]

Result:
no goals

Proof state:
S T : ℝ
hT : 0 < T
z τ : ℂ
hz : |z.im| ≤ S
hτ : T ≤ τ.im
n : ℤ
⊢ 0 ≤ 2 * π * ↑|n|

Tactic:
positivity

Result:
no goals

Proof state:
S T : ℝ
hT : 0 < T
z τ : ℂ
hz : |z.im| ≤ S
hτ : T ≤ τ.im
n : ℤ
⊢ ‖jacobiTheta₂'_term n z τ‖ ≤ 2 * π * ↑|n| * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))

Tactic:
rw [jacobiTheta₂'_term, norm_mul]

Result:
S T : ℝ
hT : 0 < T
z τ : ℂ
hz : |z.im| ≤ S
hτ : T ≤ τ.im
n : ℤ
⊢ ‖2 * ↑π * I * ↑n‖ * ‖jacobiTheta₂_term n z τ‖ ≤ 2 * π * ↑|n| * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem preimage_const_add_Ico : (fun x => a + x) ⁻¹' Ico b c = Ico (b - a) (c - a)

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => a + x) ⁻¹' Ico b c = Ico (b - a) (c - a)

Tactic:
simp [← Ici_inter_Iio]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
theorem eval_mul_X : (p * X).eval x = p.eval x * x

Proof state:
case h_monomial
R : Type u
inst✝ : Semiring R
p : R[X]
x : R
n : ℕ
a : R
⊢ eval x ((monomial n) a * X) = eval x ((monomial n) a) * x

Tactic:
simp only [← monomial_one_one_eq_X, monomial_mul_monomial, eval_monomial, mul_one, pow_succ,
  mul_assoc]

Result:
no goals

Proof state:
case h_add
R : Type u
inst✝ : Semiring R
p✝ : R[X]
x : R
p q : R[X]
ph : eval x (p * X) = eval x p * x
qh : eval x (q * X) = eval x q * x
⊢ eval x ((p + q) * X) = eval x (p + q) * x

Tactic:
simp only [add_mul, eval_add, ph, qh]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
x : R
⊢ eval x (p * X) = eval x p * x

Tactic:
induction p using Polynomial.induction_on' with
| h_add p q ph qh =>
  simp only [add_mul, eval_add, ph, qh]
| h_monomial n a =>
  simp only [← monomial_one_one_eq_X, monomial_mul_monomial, eval_monomial, mul_one, pow_succ,
    mul_assoc]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Gaussian/PoissonSummation.lean
lemma rexp_neg_quadratic_isLittleO_rpow_atTop {a : ℝ} (ha : a < 0) (b s : ℝ) :
    (fun x ↦ rexp (a * x ^ 2 + b * x)) =o[atTop] (· ^ s)

Proof state:
a : ℝ
ha : a < 0
b s : ℝ
⊢ Tendsto (fun x => -x - (a * x ^ 2 + b * x)) atTop atTop

Tactic:
have : (fun x ↦ -x - (a * x ^ 2 + b * x)) = fun x ↦ x * (-a * x - (b + 1)) := by
  ext1 x; ring_nf

Result:
a : ℝ
ha : a < 0
b s : ℝ
this : (fun x => -x - (a * x ^ 2 + b * x)) = fun x => x * (-a * x - (b + 1))
⊢ Tendsto (fun x => -x - (a * x ^ 2 + b * x)) atTop atTop

Proof state:
a : ℝ
ha : a < 0
b s : ℝ
this : (fun x => -x - (a * x ^ 2 + b * x)) = fun x => x * (-a * x - (b + 1))
⊢ Tendsto (fun x => x * (-a * x - (b + 1))) atTop atTop

Tactic:
exact tendsto_id.atTop_mul_atTop₀ <| tendsto_atTop_add_const_right _ _ <|
  tendsto_id.const_mul_atTop (neg_pos.mpr ha)

Result:
no goals

Proof state:
a : ℝ
ha : a < 0
b s : ℝ
this : (fun x => -x - (a * x ^ 2 + b * x)) = fun x => x * (-a * x - (b + 1))
⊢ Tendsto (fun x => -x - (a * x ^ 2 + b * x)) atTop atTop

Tactic:
rw [this]

Result:
a : ℝ
ha : a < 0
b s : ℝ
this : (fun x => -x - (a * x ^ 2 + b * x)) = fun x => x * (-a * x - (b + 1))
⊢ Tendsto (fun x => x * (-a * x - (b + 1))) atTop atTop

Proof state:
a : ℝ
ha : a < 0
b s : ℝ
⊢ (fun x => rexp (a * x ^ 2 + b * x)) =o[atTop] fun x => rexp (-x)

Tactic:
rw [isLittleO_exp_comp_exp_comp]

Result:
a : ℝ
ha : a < 0
b s : ℝ
⊢ Tendsto (fun x => -x - (a * x ^ 2 + b * x)) atTop atTop

Proof state:
a : ℝ
ha : a < 0
b s : ℝ
⊢ (fun x => -x - (a * x ^ 2 + b * x)) = fun x => x * (-a * x - (b + 1))

Tactic:
ext1 x

Result:
case h
a : ℝ
ha : a < 0
b s x : ℝ
⊢ -x - (a * x ^ 2 + b * x) = x * (-a * x - (b + 1))

Proof state:
a : ℝ
ha : a < 0
b s : ℝ
this : (fun x => rexp (a * x ^ 2 + b * x)) =o[atTop] fun x => rexp (-x)
⊢ (fun x => rexp (a * x ^ 2 + b * x)) =o[atTop] fun x => x ^ s

Tactic:
refine this.trans ?_

Result:
a : ℝ
ha : a < 0
b s : ℝ
this : (fun x => rexp (a * x ^ 2 + b * x)) =o[atTop] fun x => rexp (-x)
⊢ (fun x => rexp (-x)) =o[atTop] fun x => x ^ s

Proof state:
case h
a : ℝ
ha : a < 0
b s x : ℝ
⊢ -x - (a * x ^ 2 + b * x) = x * (-a * x - (b + 1))

Tactic:
ring_nf

Result:
no goals

Proof state:
a : ℝ
ha : a < 0
b s : ℝ
this : (fun x => rexp (a * x ^ 2 + b * x)) =o[atTop] fun x => rexp (-x)
⊢ (fun x => rexp (-x)) =o[atTop] fun x => x ^ s

Tactic:
simpa only [neg_one_mul] using isLittleO_exp_neg_mul_rpow_atTop zero_lt_one s

Result:
no goals

Proof state:
a : ℝ
ha : a < 0
b s : ℝ
⊢ (fun x => rexp (a * x ^ 2 + b * x)) =o[atTop] fun x => x ^ s

Tactic:
suffices (fun x ↦ rexp (a * x ^ 2 + b * x)) =o[atTop] (fun x ↦ rexp (-x)) by
  refine this.trans ?_
  simpa only [neg_one_mul] using isLittleO_exp_neg_mul_rpow_atTop zero_lt_one s

Result:
a : ℝ
ha : a < 0
b s : ℝ
⊢ (fun x => rexp (a * x ^ 2 + b * x)) =o[atTop] fun x => rexp (-x)
-- Mathlib/LinearAlgebra/Span/Basic.lean
theorem prod_top : (prod ⊤ ⊤ : Submodule R (M × M')) = ⊤

Proof state:
R : Type u_1
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type u_9
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
⊢ ⊤.prod ⊤ = ⊤

Tactic:
ext

Result:
case h
R : Type u_1
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type u_9
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
x✝ : M × M'
⊢ x✝ ∈ ⊤.prod ⊤ ↔ x✝ ∈ ⊤

Proof state:
case h
R : Type u_1
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type u_9
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
x✝ : M × M'
⊢ x✝ ∈ ⊤.prod ⊤ ↔ x✝ ∈ ⊤

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Set/NAry.lean
lemma image2_inter_right (hf : Injective2 f) :
    image2 f s (t ∩ t') = image2 f s t ∩ image2 f s t'

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t t' : Set β
hf : Injective2 f
⊢ image2 f s (t ∩ t') = image2 f s t ∩ image2 f s t'

Tactic:
simp_rw [← image_uncurry_prod, prod_inter, image_inter hf.uncurry]

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/Pi.lean
theorem pi_eq_generateFrom {C : ∀ i, Set (Set (α i))}
    (hC : ∀ i, generateFrom (C i) = by apply_assumption) (h2C : ∀ i, IsPiSystem (C i))
    (h3C : ∀ i, (μ i).FiniteSpanningSetsIn (C i)) {μν : Measure (∀ i, α i)}
    (h₁ : ∀ s : ∀ i, Set (α i), (∀ i, s i ∈ C i) → μν (pi univ s) = ∏ i, μ i (s i)) :
    Measure.pi μ = μν

Proof state:
ι : Type u_1
α : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), generateFrom (C i) = inst✝ i
h2C : ∀ (i : ι), IsPiSystem (C i)
h3C : (i : ι) → (μ i).FiniteSpanningSetsIn (C i)
μν : Measure ((i : ι) → α i)
h₁ : ∀ (s : (i : ι) → Set (α i)), (∀ (i : ι), s i ∈ C i) → μν (univ.pi s) = ∏ i : ι, (μ i) (s i)
i : ι
s : Set (α i)
hs : s ∈ C i
⊢ MeasurableSet s

Tactic:
exact measurableSet_generateFrom hs

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
theorem neg_vecMul [Fintype m] (v : m → α) (A : Matrix m n α) : (-v) ᵥ* A = - (v ᵥ* A)

Proof state:
case h
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype m
v : m → α
A : Matrix m n α
x✝ : n
⊢ (-v ᵥ* A) x✝ = (-(v ᵥ* A)) x✝

Tactic:
apply neg_dotProduct

Result:
no goals

Proof state:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype m
v : m → α
A : Matrix m n α
⊢ -v ᵥ* A = -(v ᵥ* A)

Tactic:
ext

Result:
case h
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype m
v : m → α
A : Matrix m n α
x✝ : n
⊢ (-v ᵥ* A) x✝ = (-(v ᵥ* A)) x✝
-- Mathlib/CategoryTheory/Monoidal/Preadditive.lean
theorem leftDistributor_ext₂_right {J : Type} [Fintype J]
    {X Y Z : C} {f : J → C} {g h : X ⟶ Y ⊗ (Z ⊗ ⨁ f)}
    (w : ∀ j, g ≫ (Y ◁ (Z ◁ biproduct.π f j)) = h ≫ (Y ◁ (Z ◁ biproduct.π f j))) :
    g = h

Proof state:
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X Y Z : C
f : J → C
g h : X ⟶ Y ⊗ Z ⊗ ⨁ f
w : ∀ (j : J), g ≫ Y ◁ Z ◁ biproduct.π f j = h ≫ Y ◁ Z ◁ biproduct.π f j
j✝ : J
⊢ (g ≫ (α_ Y Z (⨁ f)).inv) ≫ (Y ⊗ Z) ◁ biproduct.π f j✝ = (h ≫ (α_ Y Z (⨁ f)).inv) ≫ (Y ⊗ Z) ◁ biproduct.π f j✝

Tactic:
simp [w]

Result:
no goals

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X Y Z : C
f : J → C
g h : X ⟶ Y ⊗ Z ⊗ ⨁ f
w : ∀ (j : J), g ≫ Y ◁ Z ◁ biproduct.π f j = h ≫ Y ◁ Z ◁ biproduct.π f j
⊢ g = h

Tactic:
apply (cancel_mono (α_ _ _ _).inv).mp

Result:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X Y Z : C
f : J → C
g h : X ⟶ Y ⊗ Z ⊗ ⨁ f
w : ∀ (j : J), g ≫ Y ◁ Z ◁ biproduct.π f j = h ≫ Y ◁ Z ◁ biproduct.π f j
⊢ g ≫ (α_ Y Z (⨁ f)).inv = h ≫ (α_ Y Z (⨁ f)).inv

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X Y Z : C
f : J → C
g h : X ⟶ Y ⊗ Z ⊗ ⨁ f
w : ∀ (j : J), g ≫ Y ◁ Z ◁ biproduct.π f j = h ≫ Y ◁ Z ◁ biproduct.π f j
⊢ g ≫ (α_ Y Z (⨁ f)).inv = h ≫ (α_ Y Z (⨁ f)).inv

Tactic:
ext

Result:
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X Y Z : C
f : J → C
g h : X ⟶ Y ⊗ Z ⊗ ⨁ f
w : ∀ (j : J), g ≫ Y ◁ Z ◁ biproduct.π f j = h ≫ Y ◁ Z ◁ biproduct.π f j
j✝ : J
⊢ (g ≫ (α_ Y Z (⨁ f)).inv) ≫ (Y ⊗ Z) ◁ biproduct.π f j✝ = (h ≫ (α_ Y Z (⨁ f)).inv) ≫ (Y ⊗ Z) ◁ biproduct.π f j✝
-- Mathlib/Probability/Kernel/Composition/MapComap.lean
lemma sum_prodMkLeft {ι : Type*} [Countable ι] {κ : ι → Kernel α β} :
    Kernel.sum (fun i ↦ Kernel.prodMkLeft γ (κ i)) = Kernel.prodMkLeft γ (Kernel.sum κ)

Proof state:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_5
inst✝ : Countable ι
κ : ι → Kernel α β
a✝¹ : γ × α
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ ((Kernel.sum fun i => prodMkLeft γ (κ i)) a✝¹) s✝ = ((prodMkLeft γ (Kernel.sum κ)) a✝¹) s✝

Tactic:
simp_rw [sum_apply, prodMkLeft_apply, sum_apply]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_5
inst✝ : Countable ι
κ : ι → Kernel α β
⊢ (Kernel.sum fun i => prodMkLeft γ (κ i)) = prodMkLeft γ (Kernel.sum κ)

Tactic:
ext

Result:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_5
inst✝ : Countable ι
κ : ι → Kernel α β
a✝¹ : γ × α
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ ((Kernel.sum fun i => prodMkLeft γ (κ i)) a✝¹) s✝ = ((prodMkLeft γ (Kernel.sum κ)) a✝¹) s✝
-- Mathlib/Algebra/Homology/ShortComplex/Exact.lean
@[reassoc (attr := simp, nolint unusedHavesSuffices)]
lemma Exact.liftFromProjective_comp
    (hS : S.Exact) {P : C} (f : P ⟶ S.X₂) [Projective P] (hf : f ≫ S.g = 0) :
    hS.liftFromProjective f hf ≫ S.f = f

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Abelian C
S : ShortComplex C
hS : S.Exact
P : C
f : P ⟶ S.X₂
inst✝ : Projective P
hf : f ≫ S.g = 0
this : Epi S.toCycles
⊢ Projective.factorThru (S.liftCycles f hf) S.toCycles ≫ S.f = f

Tactic:
rw [← toCycles_i, Projective.factorThru_comp_assoc, liftCycles_i]

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Abelian C
S : ShortComplex C
hS : S.Exact
P : C
f : P ⟶ S.X₂
inst✝ : Projective P
hf : f ≫ S.g = 0
this : Epi S.toCycles
⊢ hS.liftFromProjective f hf ≫ S.f = f

Tactic:
dsimp [liftFromProjective]

Result:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Abelian C
S : ShortComplex C
hS : S.Exact
P : C
f : P ⟶ S.X₂
inst✝ : Projective P
hf : f ≫ S.g = 0
this : Epi S.toCycles
⊢ Projective.factorThru (S.liftCycles f hf) S.toCycles ≫ S.f = f

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Abelian C
S : ShortComplex C
hS : S.Exact
P : C
f : P ⟶ S.X₂
inst✝ : Projective P
hf : f ≫ S.g = 0
⊢ hS.liftFromProjective f hf ≫ S.f = f

Tactic:
have := hS.epi_toCycles

Result:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Abelian C
S : ShortComplex C
hS : S.Exact
P : C
f : P ⟶ S.X₂
inst✝ : Projective P
hf : f ≫ S.g = 0
this : Epi S.toCycles
⊢ hS.liftFromProjective f hf ≫ S.f = f
-- Mathlib/Data/List/Defs.lean
theorem iterate_eq_iterateTR : @iterate = @iterateTR

Proof state:
⊢ @iterate = @iterateTR

Tactic:
funext α f a n

Result:
case h.h.h.h
α : Type u_7
f : α → α
a : α
n : ℕ
⊢ iterate f a n = iterateTR f a n

Proof state:
case h.h.h.h
α : Type u_7
f : α → α
a : α
n : ℕ
⊢ iterate f a n = iterateTR f a n

Tactic:
exact Eq.symm <| iterateTR_loop_eq f a n []

Result:
no goals
-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
lemma HasUnifEigenvector.pow_apply {f : End R M} {μ : R} {v : M} (hv : f.HasUnifEigenvector μ 1 v)
    (n : ℕ) : (f ^ n) v = μ ^ n • v

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
v : M
hv : f.HasUnifEigenvector μ 1 v
n : ℕ
⊢ (f ^ n) v = μ ^ n • v

Tactic:
induction n <;> simp [*, pow_succ f, hv.apply_eq_smul, smul_smul, pow_succ' μ]

Result:
no goals
-- Mathlib/Data/Finset/Sups.lean
theorem disjSups_union_right : s ○ (t₁ ∪ t₂) = s ○ t₁ ∪ s ○ t₂

Proof state:
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t₁ t₂ : Finset α
⊢ s ○ (t₁ ∪ t₂) = s ○ t₁ ∪ s ○ t₂

Tactic:
simp [disjSups, filter_union, image_union]

Result:
no goals
-- Mathlib/Data/Bundle.lean
theorem TotalSpace.range_mk (b : B) : range ((↑) : E b → TotalSpace F E) = π F E ⁻¹' {b}

Proof state:
case h₂.mk
B : Type u_1
F : Type u_2
E : B → Type u_3
proj✝ : B
x : E proj✝
⊢ { proj := proj✝, snd := x } ∈ range (mk { proj := proj✝, snd := x }.proj)

Tactic:
exact ⟨x, rfl⟩

Result:
no goals

Proof state:
case h₁
B : Type u_1
F : Type u_2
E : B → Type u_3
b : B
⊢ range (mk b) ⊆ proj ⁻¹' {b}

Tactic:
rintro _ ⟨x, rfl⟩

Result:
case h₁.intro
B : Type u_1
F : Type u_2
E : B → Type u_3
b : B
x : E b
⊢ { proj := b, snd := x } ∈ proj ⁻¹' {b}

Proof state:
case h₁.intro
B : Type u_1
F : Type u_2
E : B → Type u_3
b : B
x : E b
⊢ { proj := b, snd := x } ∈ proj ⁻¹' {b}

Tactic:
rfl

Result:
no goals

Proof state:
case h₂
B : Type u_1
F : Type u_2
E : B → Type u_3
b : B
⊢ proj ⁻¹' {b} ⊆ range (mk b)

Tactic:
rintro ⟨_, x⟩ rfl

Result:
case h₂.mk
B : Type u_1
F : Type u_2
E : B → Type u_3
proj✝ : B
x : E proj✝
⊢ { proj := proj✝, snd := x } ∈ range (mk { proj := proj✝, snd := x }.proj)

Proof state:
B : Type u_1
F : Type u_2
E : B → Type u_3
b : B
⊢ range (mk b) = proj ⁻¹' {b}

Tactic:
apply Subset.antisymm

Result:
case h₁
B : Type u_1
F : Type u_2
E : B → Type u_3
b : B
⊢ range (mk b) ⊆ proj ⁻¹' {b}

case h₂
B : Type u_1
F : Type u_2
E : B → Type u_3
b : B
⊢ proj ⁻¹' {b} ⊆ range (mk b)