harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean
@[reassoc (attr := simp)]
lemma toCycles_comp_leftHomologyπ : S.toCycles ≫ S.leftHomologyπ = 0 :=
  S.liftCycles_leftHomologyπ_eq_zero_of_boundary S.f (𝟙 _) (by rw [id_comp])

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasLeftHomology
⊢ S.f = 𝟙 S.X₁ ≫ S.f

Tactic:
rw [id_comp]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Rigid/Basic.lean
theorem leftAdjointMate_comp {X Y Z : C} [HasLeftDual X] [HasLeftDual Y] {f : X ⟶ Y}
    {g : (ᘁX) ⟶ Z} :
    (ᘁf) ≫ g =
      (λ_ _).inv ≫
        η_ (ᘁX : C) X ▷ _ ≫ (g ⊗ f) ▷ _ ≫ (α_ _ _ _).hom ≫ _ ◁ ε_ _ _ ≫ (ρ_ _).hom :=
  calc
    _ = 𝟙 _ ⊗≫ η_ (ᘁX : C) X ▷ (ᘁY) ⊗≫ (ᘁX) ◁ f ▷ (ᘁY) ⊗≫ ((ᘁX) ◁ ε_ (ᘁY) Y ≫ g ▷ 𝟙_ C) ⊗≫ 𝟙 _

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : HasLeftDual X
inst✝ : HasLeftDual Y
f : X ⟶ Y
g : ᘁX ⟶ Z
⊢ ((λ_ ᘁY).inv ≫ η_ (ᘁX) X ▷ ᘁY ≫ (ᘁX ◁ f) ▷ ᘁY ≫ (α_ (ᘁX) Y ᘁY).hom ≫ ᘁX ◁ ε_ (ᘁY) Y ≫ (ρ_ ᘁX).hom) ≫ g =
    𝟙 ᘁY ⊗≫ η_ (ᘁX) X ▷ ᘁY ⊗≫ ᘁX ◁ f ▷ ᘁY ⊗≫ (ᘁX ◁ ε_ (ᘁY) Y ≫ g ▷ 𝟙_ C) ⊗≫ 𝟙 Z

Tactic:
monoidal

Result:
no goals

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : HasLeftDual X
inst✝ : HasLeftDual Y
f : X ⟶ Y
g : ᘁX ⟶ Z
⊢ (ᘁf) ≫ g = 𝟙 ᘁY ⊗≫ η_ (ᘁX) X ▷ ᘁY ⊗≫ ᘁX ◁ f ▷ ᘁY ⊗≫ (ᘁX ◁ ε_ (ᘁY) Y ≫ g ▷ 𝟙_ C) ⊗≫ 𝟙 Z

Tactic:
dsimp only [leftAdjointMate]

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : HasLeftDual X
inst✝ : HasLeftDual Y
f : X ⟶ Y
g : ᘁX ⟶ Z
⊢ ((λ_ ᘁY).inv ≫ η_ (ᘁX) X ▷ ᘁY ≫ (ᘁX ◁ f) ▷ ᘁY ≫ (α_ (ᘁX) Y ᘁY).hom ≫ ᘁX ◁ ε_ (ᘁY) Y ≫ (ρ_ ᘁX).hom) ≫ g =
    𝟙 ᘁY ⊗≫ η_ (ᘁX) X ▷ ᘁY ⊗≫ ᘁX ◁ f ▷ ᘁY ⊗≫ (ᘁX ◁ ε_ (ᘁY) Y ≫ g ▷ 𝟙_ C) ⊗≫ 𝟙 Z

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : HasLeftDual X
inst✝ : HasLeftDual Y
f : X ⟶ Y
g : ᘁX ⟶ Z
⊢ 𝟙 ᘁY ⊗≫ η_ (ᘁX) X ▷ ᘁY ⊗≫ ᘁX ◁ f ▷ ᘁY ⊗≫ (g ▷ (Y ⊗ ᘁY) ≫ Z ◁ ε_ (ᘁY) Y) ⊗≫ 𝟙 Z =
    (λ_ ᘁY).inv ≫ η_ (ᘁX) X ▷ ᘁY ≫ (ᘁX ◁ f ≫ g ▷ Y) ▷ ᘁY ≫ (α_ Z Y ᘁY).hom ≫ Z ◁ ε_ (ᘁY) Y ≫ (ρ_ Z).hom

Tactic:
monoidal

Result:
no goals

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : HasLeftDual X
inst✝ : HasLeftDual Y
f : X ⟶ Y
g : ᘁX ⟶ Z
⊢ 𝟙 ᘁY ⊗≫ η_ (ᘁX) X ▷ ᘁY ⊗≫ ᘁX ◁ f ▷ ᘁY ⊗≫ (ᘁX ◁ ε_ (ᘁY) Y ≫ g ▷ 𝟙_ C) ⊗≫ 𝟙 Z =
    (λ_ ᘁY).inv ≫ η_ (ᘁX) X ▷ ᘁY ≫ (g ⊗ f) ▷ ᘁY ≫ (α_ Z Y ᘁY).hom ≫ Z ◁ ε_ (ᘁY) Y ≫ (ρ_ Z).hom

Tactic:
rw [whisker_exchange, tensorHom_def']

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : HasLeftDual X
inst✝ : HasLeftDual Y
f : X ⟶ Y
g : ᘁX ⟶ Z
⊢ 𝟙 ᘁY ⊗≫ η_ (ᘁX) X ▷ ᘁY ⊗≫ ᘁX ◁ f ▷ ᘁY ⊗≫ (g ▷ (Y ⊗ ᘁY) ≫ Z ◁ ε_ (ᘁY) Y) ⊗≫ 𝟙 Z =
    (λ_ ᘁY).inv ≫ η_ (ᘁX) X ▷ ᘁY ≫ (ᘁX ◁ f ≫ g ▷ Y) ▷ ᘁY ≫ (α_ Z Y ᘁY).hom ≫ Z ◁ ε_ (ᘁY) Y ≫ (ρ_ Z).hom
-- Mathlib/Algebra/Group/Subgroup/Defs.lean
theorem coe_inclusion {H K : Subgroup G} {h : H ≤ K} (a : H) : (inclusion h a : G) = a

Proof state:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H ≤ K
a : ↥H
⊢ ↑((inclusion h) a) = ↑a

Tactic:
cases a

Result:
case mk
G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H ≤ K
val✝ : G
property✝ : val✝ ∈ H
⊢ ↑((inclusion h) ⟨val✝, property✝⟩) = ↑⟨val✝, property✝⟩

Proof state:
case mk
G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H ≤ K
val✝ : G
property✝ : val✝ ∈ H
⊢ ↑((inclusion h) ⟨val✝, property✝⟩) = ↑⟨val✝, property✝⟩

Tactic:
simp only [inclusion, coe_mk, MonoidHom.mk'_apply]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
theorem c₄_of_isCharTwoJEqZeroNF : W.c₄ = -48 * W.a₄

Proof state:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJEqZeroNF
⊢ W.c₄ = -48 * W.a₄

Tactic:
rw [c₄, b₂_of_isCharTwoJEqZeroNF, b₄_of_isCharTwoJEqZeroNF]

Result:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJEqZeroNF
⊢ 0 ^ 2 - 24 * (2 * W.a₄) = -48 * W.a₄

Proof state:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJEqZeroNF
⊢ 0 ^ 2 - 24 * (2 * W.a₄) = -48 * W.a₄

Tactic:
ring1

Result:
no goals
-- Mathlib/Data/List/Cycle.lean
theorem prev_getLast_cons' (y : α) (hxy : x ∈ y :: l) (hx : x = y) :
    prev (y :: l) x hxy = getLast (y :: l) (cons_ne_nil _ _)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
x y : α
hxy : x ∈ y :: l
hx : x = y
⊢ (y :: l).prev x hxy = (y :: l).getLast ⋯

Tactic:
cases l <;> simp [prev, hx]

Result:
no goals
-- Mathlib/Order/Filter/Lift.lean
theorem sInter_lift_sets (hg : Monotone g) :
    ⋂₀ { s | s ∈ f.lift g } = ⋂ s ∈ f, ⋂₀ { t | t ∈ g s }

Proof state:
α : Type u_1
β : Type u_2
f : Filter α
g : Set α → Filter β
hg : Monotone g
⊢ ⋂₀ {s | s ∈ f.lift g} = ⋂ s ∈ f, ⋂₀ {t | t ∈ g s}

Tactic:
simp only [sInter_eq_biInter, mem_setOf_eq, Filter.mem_sets, mem_lift_sets hg, iInter_exists,
  iInter_and, @iInter_comm _ (Set β)]

Result:
no goals
-- Mathlib/Data/Vector/Basic.lean
@[simp] lemma get_append_cons_zero : get (append (x ::ᵥ xs) ys) ⟨0, by omega⟩ = x := rfl

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
x : α
y : β
s : σ
xs : Vector α n
ys : Vector α m
⊢ 0 < n.succ + m

Tactic:
omega

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem U_neg (n : ℤ) : U R (-n) = -U R (n - 2)

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ U R (-n) = -U R (n - 2)

Tactic:
simpa [sub_sub] using U_neg_sub_one R (n - 1)

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem integral_comp_add_right (d) : (∫ x in a..b, f (x + d)) = ∫ x in a + d..b + d, f x :=
  have A : MeasurableEmbedding fun x => x + d :=
    (Homeomorph.addRight d).isClosedEmbedding.measurableEmbedding
  calc
    (∫ x in a..b, f (x + d)) = ∫ x in a + d..b + d, f x ∂Measure.map (fun x => x + d) volume

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
d : ℝ
A : MeasurableEmbedding fun x => x + d
⊢ ∫ (x : ℝ) in a + d..b + d, f x ∂Measure.map (fun x => x + d) volume = ∫ (x : ℝ) in a + d..b + d, f x

Tactic:
rw [map_add_right_eq_self]

Result:
no goals

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
d : ℝ
A : MeasurableEmbedding fun x => x + d
⊢ ∫ (x : ℝ) in a..b, f (x + d) = ∫ (x : ℝ) in a + d..b + d, f x ∂Measure.map (fun x => x + d) volume

Tactic:
simp [intervalIntegral, A.setIntegral_map]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Basis.lean
theorem linearMap_toMatrix_mul_basis_toMatrix [Finite κ'] [DecidableEq ι] [DecidableEq ι'] :
    LinearMap.toMatrix b' c' f * b'.toMatrix b = LinearMap.toMatrix b c' f :=
  (Matrix.toLin b c').injective <| by
    rw [toLin_toMatrix, toLin_mul b b' c', toLin_toMatrix, b'.toLin_toMatrix, LinearMap.comp_id]

Proof state:
ι : Type u_1
ι' : Type u_2
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
N : Type u_9
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R N
b : Basis ι R M
b' : Basis ι' R M
c' : Basis κ' R N
f : M →ₗ[R] N
inst✝⁴ : Fintype ι'
inst✝³ : Fintype ι
inst✝² : Finite κ'
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq ι'
⊢ (toLin b c') ((toMatrix b' c') f * b'.toMatrix ⇑b) = (toLin b c') ((toMatrix b c') f)

Tactic:
rw [toLin_toMatrix, toLin_mul b b' c', toLin_toMatrix, b'.toLin_toMatrix, LinearMap.comp_id]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getElem_and {x y : BitVec w} {i : Nat} (h : i < w) : (x &&& y)[i] = (x[i] && y[i])

Proof state:
w : Nat
x y : BitVec w
i : Nat
h : i < w
⊢ (x &&& y)[i] = (x[i] && y[i])

Tactic:
simp [getElem_eq_testBit_toNat]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean
theorem isAdjMatrix_adjMatrix [Zero α] [One α] : (G.adjMatrix α).IsAdjMatrix :=
  { zero_or_one := fun i j => by by_cases h : G.Adj i j <;> simp [h] }

Proof state:
V : Type u_1
α : Type u_2
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Zero α
inst✝ : One α
i j : V
⊢ adjMatrix α G i j = 0 ∨ adjMatrix α G i j = 1

Tactic:
by_cases h : G.Adj i j <;> simp [h]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Hausdorff.lean
theorem isometry_map_mkMetric (m : ℝ≥0∞ → ℝ≥0∞) {f : X → Y} (hf : Isometry f)
    (H : Monotone m ∨ Surjective f) : map f (mkMetric m) = restrict (range f) (mkMetric m)

Proof state:
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
m : ℝ≥0∞ → ℝ≥0∞
f : X → Y
hf : Isometry f
H : Monotone m ∨ Surjective f
⊢ (map f) (mkMetric m) = (restrict (range f)) (mkMetric m)

Tactic:
rw [← isometry_comap_mkMetric _ hf H, map_comap]

Result:
no goals
-- Mathlib/Probability/Kernel/MeasurableLIntegral.lean
theorem _root_.Measurable.lintegral_kernel_prod_left {f : β → α → ℝ≥0∞}
    (hf : Measurable (uncurry f)) : Measurable fun y => ∫⁻ x, f x y ∂κ y

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : β → α → ℝ≥0∞
hf : Measurable (uncurry f)
⊢ Measurable fun y => ∫⁻ (x : β), f x y ∂κ y

Tactic:
fun_prop

Result:
no goals
-- Mathlib/RingTheory/Localization/NumDen.lean
theorem num_mul_den_eq_num_iff_eq {x y : K} :
    x * algebraMap A K (den A y) = algebraMap A K (num A y) ↔ x = y :=
  ⟨fun h => by simpa only [mk'_num_den] using eq_mk'_iff_mul_eq.mpr h, fun h ↦
    eq_mk'_iff_mul_eq.mp (by rw [h, mk'_num_den])⟩

Proof state:
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x y : K
h : x = y
⊢ x = mk' K (num A y) (den A y)

Tactic:
rw [h, mk'_num_den]

Result:
no goals

Proof state:
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x y : K
h : x * (algebraMap A K) ↑(den A y) = (algebraMap A K) (num A y)
⊢ x = y

Tactic:
simpa only [mk'_num_den] using eq_mk'_iff_mul_eq.mpr h

Result:
no goals
-- Mathlib/Data/Finsupp/Pointwise.lean
lemma support_mul_subset_right {g₁ g₂ : α →₀ β} :
    (g₁ * g₂).support ⊆ g₂.support := fun x hx => by
  aesop

Proof state:
α : Type u₁
β : Type u₂
inst✝ : MulZeroClass β
g₁ g₂ : α →₀ β
x : α
hx : x ∈ (g₁ * g₂).support
⊢ x ∈ g₂.support

Tactic:
aesop

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/Tagged.lean
theorem distortion_disjUnion (h : Disjoint π₁.iUnion π₂.iUnion) :
    (π₁.disjUnion π₂ h).distortion = max π₁.distortion π₂.distortion

Proof state:
ι : Type u_1
I : Box ι
π₁ π₂ : TaggedPrepartition I
inst✝ : Fintype ι
h : Disjoint π₁.iUnion π₂.iUnion
⊢ (π₁.disjUnion π₂ h).distortion = π₁.distortion ⊔ π₂.distortion

Tactic:
classical exact sup_union

Result:
no goals

Proof state:
ι : Type u_1
I : Box ι
π₁ π₂ : TaggedPrepartition I
inst✝ : Fintype ι
h : Disjoint π₁.iUnion π₂.iUnion
⊢ (π₁.disjUnion π₂ h).distortion = π₁.distortion ⊔ π₂.distortion

Tactic:
exact sup_union

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem edist_le_ofReal {x y : α} {r : ℝ} (hr : 0 ≤ r) :
    edist x y ≤ ENNReal.ofReal r ↔ dist x y ≤ r

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
r : ℝ
hr : 0 ≤ r
⊢ edist x y ≤ ENNReal.ofReal r ↔ dist x y ≤ r

Tactic:
rw [edist_dist, ENNReal.ofReal_le_ofReal_iff hr]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem getKey?_insertManyIfNewUnit_list_of_not_mem_of_mem [EquivBEq α] [LawfulHashable α]
    {l : List α} {k k' : α} (k_beq : k == k')
    (not_mem : ¬ k ∈ m)
    (distinct : l.Pairwise (fun a b => (a == b) = false)) (mem : k ∈ l) :
    getKey? (insertManyIfNewUnit m l) k' = some k

Proof state:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List α
k k' : α
k_beq : (k == k') = true
distinct : List.Pairwise (fun a b => (a == b) = false) l
mem : k ∈ l
not_mem : m.contains k = false
⊢ (insertManyIfNewUnit m l).getKey? k' = some k

Tactic:
exact Raw₀.Const.getKey?_insertManyIfNewUnit_list_of_contains_eq_false_of_mem ⟨m.1, _⟩
  m.2 k_beq not_mem distinct mem

Result:
no goals

Proof state:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List α
k k' : α
k_beq : (k == k') = true
not_mem : ¬k ∈ m
distinct : List.Pairwise (fun a b => (a == b) = false) l
mem : k ∈ l
⊢ (insertManyIfNewUnit m l).getKey? k' = some k

Tactic:
simp only [mem_iff_contains, Bool.not_eq_true] at not_mem

Result:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List α
k k' : α
k_beq : (k == k') = true
distinct : List.Pairwise (fun a b => (a == b) = false) l
mem : k ∈ l
not_mem : m.contains k = false
⊢ (insertManyIfNewUnit m l).getKey? k' = some k
-- Mathlib/Data/List/Infix.lean
theorem get_tails (l : List α) (n : Fin (length (tails l))) : (tails l).get n = l.drop n

Proof state:
α : Type u_1
l : List α
n : Fin l.tails.length
⊢ l.tails.get n = drop (↑n) l

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/ZFC/Basic.lean
lemma Definable.out_equiv {n} (f : (Fin n → ZFSet.{u}) → ZFSet.{u}) [Definable n f]
    {xs ys : Fin n → PSet} (h : ∀ i, xs i ≈ ys i) :
    out f xs ≈ out f ys

Proof state:
n : ℕ
f : (Fin n → ZFSet.{u}) → ZFSet.{u}
inst✝ : Definable n f
xs ys : Fin n → PSet.{u}
h : ∀ (i : Fin n), xs i ≈ ys i
⊢ (f fun x => ZFSet.mk (xs x)) = f fun x => ZFSet.mk (ys x)

Tactic:
exact congrArg _ (funext fun i ↦ Quotient.sound (h i))

Result:
no goals

Proof state:
n : ℕ
f : (Fin n → ZFSet.{u}) → ZFSet.{u}
inst✝ : Definable n f
xs ys : Fin n → PSet.{u}
h : ∀ (i : Fin n), xs i ≈ ys i
⊢ out f xs ≈ out f ys

Tactic:
rw [← Quotient.eq_iff_equiv, mk_eq, mk_eq, mk_out, mk_out]

Result:
n : ℕ
f : (Fin n → ZFSet.{u}) → ZFSet.{u}
inst✝ : Definable n f
xs ys : Fin n → PSet.{u}
h : ∀ (i : Fin n), xs i ≈ ys i
⊢ (f fun x => ZFSet.mk (xs x)) = f fun x => ZFSet.mk (ys x)
-- Mathlib/Algebra/Order/Group/Basic.lean
@[to_additive zsmul_pos] lemma one_lt_zpow (ha : 1 < a) (hn : 0 < n) : 1 < a ^ n

Proof state:
α : Type u_1
inst✝ : OrderedCommGroup α
n : ℤ
a : α
ha : 1 < a
hn : 0 < n
⊢ 1 < a ^ n

Tactic:
simpa using zpow_right_strictMono ha hn

Result:
no goals
-- Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean
theorem not_mem_prime_iff_unit_in_stalk (r : Γ.obj (op X)) (x : X) :
    r ∉ (X.toΓSpecFun x).asIdeal ↔ IsUnit (X.presheaf.Γgerm x r)

Proof state:
X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
x : ↑X.toTopCat
⊢ r ∉ (X.toΓSpecFun x).asIdeal ↔ IsUnit ((ConcreteCategory.hom (X.presheaf.Γgerm x)) r)

Tactic:
simp [toΓSpecFun, IsLocalRing.closedPoint]

Result:
no goals
-- Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean
theorem support_toFinsupp (p : SkewMonoidAlgebra k G) : p.toFinsupp.support = p.support

Proof state:
k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
p : SkewMonoidAlgebra k G
⊢ p.toFinsupp.support = p.support

Tactic:
rw [support]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/MapComap.lean
@[simp]
lemma fst_zero : fst (0 : Kernel α (β × γ)) = 0

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
⊢ fst 0 = 0

Tactic:
simp [fst]

Result:
no goals
-- Mathlib/Data/Vector/Mem.lean
theorem mem_map_iff (b : β) (v : Vector α n) (f : α → β) :
    b ∈ (v.map f).toList ↔ ∃ a : α, a ∈ v.toList ∧ f a = b

Proof state:
α : Type u_1
β : Type u_2
n : ℕ
b : β
v : Vector α n
f : α → β
⊢ b ∈ (map f v).toList ↔ ∃ a ∈ v.toList, f a = b

Tactic:
rw [Vector.toList_map, List.mem_map]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean
theorem angle_neg (v₁ v₂ v₃ : V) : ∠ (-v₁) (-v₂) (-v₃) = ∠ v₁ v₂ v₃

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
v₁ v₂ v₃ : V
⊢ ∠ (-v₁) (-v₂) (-v₃) = ∠ v₁ v₂ v₃

Tactic:
simpa only [zero_sub] using angle_const_sub 0 v₁ v₂ v₃

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean
theorem continuousAt_rpow_const {x : ℝ≥0} {y : ℝ} (h : x ≠ 0 ∨ 0 ≤ y) :
    ContinuousAt (fun z => z ^ y) x :=
  h.elim (fun h => tendsto_id.nnrpow tendsto_const_nhds (Or.inl h)) fun h =>
    h.eq_or_lt.elim (fun h => h ▸ by simp only [rpow_zero, continuousAt_const]) fun h =>
      tendsto_id.nnrpow tendsto_const_nhds (Or.inr h)

Proof state:
x : ℝ≥0
y : ℝ
h✝¹ : x ≠ 0 ∨ 0 ≤ y
h✝ : 0 ≤ y
h : 0 = y
⊢ ContinuousAt (fun z => z ^ 0) x

Tactic:
simp only [rpow_zero, continuousAt_const]

Result:
no goals
-- Mathlib/LinearAlgebra/UnitaryGroup.lean
theorem mem_unitaryGroup_iff' : A ∈ Matrix.unitaryGroup n α ↔ star A * A = 1

Proof state:
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A : Matrix n n α
⊢ A ∈ unitaryGroup n α ↔ star A * A = 1

Tactic:
refine ⟨And.left, fun hA => ⟨hA, ?_⟩⟩

Result:
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A : Matrix n n α
hA : star A * A = 1
⊢ A * star A = 1

Proof state:
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A : Matrix n n α
hA : star A * A = 1
⊢ A * star A = 1

Tactic:
rwa [mul_eq_one_comm] at hA

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValue?_eq_some_getValue [BEq α] {l : List ((_ : α) × β)} {a : α} (h : containsKey a l) :
    getValue? a l = some (getValue a l h)

Proof state:
α : Type u
β : Type v
inst✝ : BEq α
l : List ((_ : α) × β)
a : α
h : containsKey a l = true
⊢ getValue? a l = some (getValue a l h)

Tactic:
simp [getValue]

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/FourFunctions.lean
private lemma filter_collapse_eq (ha : a ∉ s) (𝒜 : Finset (Finset α)) :
    {t ∈ 𝒜 | t.erase a = s} =
      if s ∈ 𝒜 then
        (if insert a s ∈ 𝒜 then {s, insert a s} else {s})
      else
        (if insert a s ∈ 𝒜 then {insert a s} else ∅)

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
t : Finset α
⊢ t ∈ filter (fun t => t.erase a = s) 𝒜 ↔
    t ∈ if s ∈ 𝒜 then if insert a s ∈ 𝒜 then {s, insert a s} else {s} else if insert a s ∈ 𝒜 then {insert a s} else ∅

Tactic:
split_ifs <;> simp [erase_eq_iff ha] <;> aesop

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
⊢ filter (fun t => t.erase a = s) 𝒜 =
    if s ∈ 𝒜 then if insert a s ∈ 𝒜 then {s, insert a s} else {s} else if insert a s ∈ 𝒜 then {insert a s} else ∅

Tactic:
ext t

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
t : Finset α
⊢ t ∈ filter (fun t => t.erase a = s) 𝒜 ↔
    t ∈ if s ∈ 𝒜 then if insert a s ∈ 𝒜 then {s, insert a s} else {s} else if insert a s ∈ 𝒜 then {insert a s} else ∅
-- Mathlib/Geometry/Manifold/LocalInvariantProperties.lean
theorem liftPropWithinAt_of_liftPropAt_of_mem_nhds (h : LiftPropAt P g x) (hs : s ∈ 𝓝 x) :
    LiftPropWithinAt P g s x

Proof state:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
x : M
hG : G.LocalInvariantProp G' P
h : LiftPropAt P g x
hs : s ∈ 𝓝 x
⊢ LiftPropWithinAt P g s x

Tactic:
rwa [← univ_inter s, hG.liftPropWithinAt_inter hs]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Equiv.lean
@[simp] lemma commAlgEquiv_X (i) : commAlgEquiv R S₁ S₂ (.X i) = .C (.X i)

Proof state:
R : Type u_2
S₁ : Type u_3
S₂ : Type u_4
inst✝ : CommSemiring R
i : S₁
⊢ (commAlgEquiv R S₁ S₂) (X i) = C (X i)

Tactic:
simp [commAlgEquiv]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Basic.lean
@[simp] lemma fromEdgeSet_disjoint : Disjoint (fromEdgeSet s) G ↔ Disjoint s G.edgeSet

Proof state:
V : Type u
G : SimpleGraph V
s : Set (Sym2 V)
⊢ Disjoint (fromEdgeSet s) G ↔ Disjoint s G.edgeSet

Tactic:
rw [disjoint_comm, disjoint_fromEdgeSet, disjoint_comm]

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/Lebesgue.lean
theorem rnDeriv_withDensity₀ (ν : Measure α) [SigmaFinite ν] {f : α → ℝ≥0∞}
    (hf : AEMeasurable f ν) :
    (ν.withDensity f).rnDeriv ν =ᵐ[ν] f :=
  have : ν.withDensity f = 0 + ν.withDensity f

Proof state:
α : Type u_1
m : MeasurableSpace α
ν : Measure α
inst✝ : SigmaFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f ν
⊢ ν.withDensity f = 0 + ν.withDensity f

Tactic:
rw [zero_add]

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem TendstoUniformlyOn.prod_map {ι' α' β' : Type*} [UniformSpace β'] {F' : ι' → α' → β'}
    {f' : α' → β'} {p' : Filter ι'} {s' : Set α'} (h : TendstoUniformlyOn F f p s)
    (h' : TendstoUniformlyOn F' f' p' s') :
    TendstoUniformlyOn (fun i : ι × ι' => Prod.map (F i.1) (F' i.2)) (Prod.map f f') (p ×ˢ p')
      (s ×ˢ s')

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
ι' : Type u_1
α' : Type u_2
β' : Type u_3
inst✝ : UniformSpace β'
F' : ι' → α' → β'
f' : α' → β'
p' : Filter ι'
s' : Set α'
h : TendstoUniformlyOnFilter F f p (𝓟 s)
h' : TendstoUniformlyOnFilter F' f' p' (𝓟 s')
⊢ TendstoUniformlyOnFilter (fun i => Prod.map (F i.1) (F' i.2)) (Prod.map f f') (p ×ˢ p') (𝓟 (s ×ˢ s'))

Tactic:
simpa only [prod_principal_principal] using h.prod_map h'

Result:
no goals

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
ι' : Type u_1
α' : Type u_2
β' : Type u_3
inst✝ : UniformSpace β'
F' : ι' → α' → β'
f' : α' → β'
p' : Filter ι'
s' : Set α'
h : TendstoUniformlyOn F f p s
h' : TendstoUniformlyOn F' f' p' s'
⊢ TendstoUniformlyOn (fun i => Prod.map (F i.1) (F' i.2)) (Prod.map f f') (p ×ˢ p') (s ×ˢ s')

Tactic:
rw [tendstoUniformlyOn_iff_tendstoUniformlyOnFilter] at h h' ⊢

Result:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
ι' : Type u_1
α' : Type u_2
β' : Type u_3
inst✝ : UniformSpace β'
F' : ι' → α' → β'
f' : α' → β'
p' : Filter ι'
s' : Set α'
h : TendstoUniformlyOnFilter F f p (𝓟 s)
h' : TendstoUniformlyOnFilter F' f' p' (𝓟 s')
⊢ TendstoUniformlyOnFilter (fun i => Prod.map (F i.1) (F' i.2)) (Prod.map f f') (p ×ˢ p') (𝓟 (s ×ˢ s'))
-- Mathlib/Data/List/Intervals.lean
theorem pairwise_lt (n m : ℕ) : Pairwise (· < ·) (Ico n m)

Proof state:
n m : ℕ
⊢ Pairwise (fun x1 x2 => x1 < x2) (Ico n m)

Tactic:
dsimp [Ico]

Result:
n m : ℕ
⊢ Pairwise (fun x1 x2 => x1 < x2) (range' n (m - n))

Proof state:
n m : ℕ
⊢ Pairwise (fun x1 x2 => x1 < x2) (range' n (m - n))

Tactic:
simp [pairwise_lt_range']

Result:
no goals
-- Mathlib/Algebra/EuclideanDomain/Basic.lean
theorem gcd_zero_right (a : R) : gcd a 0 = a

Proof state:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a : R
⊢ gcd a 0 = a

Tactic:
rw [gcd]

Result:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a : R
⊢ (if a0 : a = 0 then 0
    else
      let_fun x := ⋯;
      gcd (0 % a) a) =
    a

Proof state:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a : R
⊢ (if a0 : a = 0 then 0
    else
      let_fun x := ⋯;
      gcd (0 % a) a) =
    a

Tactic:
split_ifs with h <;> simp only [h, zero_mod, gcd_zero_left]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean
/-- A vector with coprime entries, left-multiplied by a matrix in `SL(2, R)`, has
coprime entries. -/
lemma mulVecSL {v : Fin 2 → R} (hab : IsCoprime (v 0) (v 1)) (A : SL(2, R)) :
    IsCoprime ((A.1 *ᵥ v) 0) ((A.1 *ᵥ v) 1)

Proof state:
R : Type u_1
inst✝ : CommRing R
v : Fin 2 → R
hab : IsCoprime (v 0) (v 1)
A : SL(2, R)
⊢ IsCoprime ((↑A *ᵥ v) 0) ((↑A *ᵥ v) 1)

Tactic:
simpa only [← vecMul_transpose] using hab.vecMulSL A.transpose

Result:
no goals