harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Basis/Bilinear.lean
theorem sum_repr_mul_repr_mul {B : Mₗ →ₗ[Rₗ] Nₗ →ₗ[Rₗ] Pₗ} (x y) :
    ((b₁'.repr x).sum fun i xi => (b₂'.repr y).sum fun j yj => xi • yj • B (b₁' i) (b₂' j)) =
      B x y

Proof state:
ι₁ : Type u_1
ι₂ : Type u_2
Rₗ : Type u_10
Mₗ : Type u_11
Nₗ : Type u_12
Pₗ : Type u_13
inst✝⁶ : CommSemiring Rₗ
inst✝⁵ : AddCommMonoid Mₗ
inst✝⁴ : AddCommMonoid Nₗ
inst✝³ : AddCommMonoid Pₗ
inst✝² : Module Rₗ Mₗ
inst✝¹ : Module Rₗ Nₗ
inst✝ : Module Rₗ Pₗ
b₁' : Basis ι₁ Rₗ Mₗ
b₂' : Basis ι₂ Rₗ Nₗ
B : Mₗ →ₗ[Rₗ] Nₗ →ₗ[Rₗ] Pₗ
x : Mₗ
y : Nₗ
⊢ ((b₁'.repr x).sum fun i xi => (b₂'.repr y).sum fun j yj => xi • yj • (B (b₁' i)) (b₂' j)) = (B x) y

Tactic:
conv_rhs => rw [← b₁'.linearCombination_repr x, ← b₂'.linearCombination_repr y]

Result:
ι₁ : Type u_1
ι₂ : Type u_2
Rₗ : Type u_10
Mₗ : Type u_11
Nₗ : Type u_12
Pₗ : Type u_13
inst✝⁶ : CommSemiring Rₗ
inst✝⁵ : AddCommMonoid Mₗ
inst✝⁴ : AddCommMonoid Nₗ
inst✝³ : AddCommMonoid Pₗ
inst✝² : Module Rₗ Mₗ
inst✝¹ : Module Rₗ Nₗ
inst✝ : Module Rₗ Pₗ
b₁' : Basis ι₁ Rₗ Mₗ
b₂' : Basis ι₂ Rₗ Nₗ
B : Mₗ →ₗ[Rₗ] Nₗ →ₗ[Rₗ] Pₗ
x : Mₗ
y : Nₗ
⊢ ((b₁'.repr x).sum fun i xi => (b₂'.repr y).sum fun j yj => xi • yj • (B (b₁' i)) (b₂' j)) =
    (B ((Finsupp.linearCombination Rₗ ⇑b₁') (b₁'.repr x))) ((Finsupp.linearCombination Rₗ ⇑b₂') (b₂'.repr y))

Proof state:
ι₁ : Type u_1
ι₂ : Type u_2
Rₗ : Type u_10
Mₗ : Type u_11
Nₗ : Type u_12
Pₗ : Type u_13
inst✝⁶ : CommSemiring Rₗ
inst✝⁵ : AddCommMonoid Mₗ
inst✝⁴ : AddCommMonoid Nₗ
inst✝³ : AddCommMonoid Pₗ
inst✝² : Module Rₗ Mₗ
inst✝¹ : Module Rₗ Nₗ
inst✝ : Module Rₗ Pₗ
b₁' : Basis ι₁ Rₗ Mₗ
b₂' : Basis ι₂ Rₗ Nₗ
B : Mₗ →ₗ[Rₗ] Nₗ →ₗ[Rₗ] Pₗ
x : Mₗ
y : Nₗ
⊢ ((b₁'.repr x).sum fun i xi => (b₂'.repr y).sum fun j yj => xi • yj • (B (b₁' i)) (b₂' j)) =
    (B ((Finsupp.linearCombination Rₗ ⇑b₁') (b₁'.repr x))) ((Finsupp.linearCombination Rₗ ⇑b₂') (b₂'.repr y))

Tactic:
simp_rw [Finsupp.linearCombination_apply, Finsupp.sum, map_sum₂, map_sum, LinearMap.map_smul₂,
  LinearMap.map_smul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem or_and_right : (a ∨ b) ∧ c ↔ (a ∧ c) ∨ (b ∧ c)

Proof state:
a b c : Prop
⊢ (a ∨ b) ∧ c ↔ a ∧ c ∨ b ∧ c

Tactic:
rw [@and_comm (a ∨ b), and_or_left, @and_comm c, @and_comm c]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/ByteSubarray.lean
theorem stop_eq_start_add_size (self : ByteSubarray) : self.stop = self.start + self.size

Proof state:
self : ByteSubarray
⊢ self.stop = self.start + self.size

Tactic:
rw [ByteSubarray.size, Nat.add_sub_cancel' self.start_le_stop]

Result:
no goals
-- Mathlib/ModelTheory/Substructures.lean
theorem toHom_range (f : M ≃[L] N) : f.toHom.range = ⊤

Proof state:
L : Language
M : Type w
N : Type u_1
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃[L] N
⊢ f.toHom.range = ⊤

Tactic:
ext n

Result:
case h
L : Language
M : Type w
N : Type u_1
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃[L] N
n : N
⊢ n ∈ f.toHom.range ↔ n ∈ ⊤

Proof state:
case h
L : Language
M : Type w
N : Type u_1
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃[L] N
n : N
⊢ ∃ y, f y = n

Tactic:
exact ⟨f.symm n, apply_symm_apply _ _⟩

Result:
no goals

Proof state:
case h
L : Language
M : Type w
N : Type u_1
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃[L] N
n : N
⊢ n ∈ f.toHom.range ↔ n ∈ ⊤

Tactic:
simp only [Hom.mem_range, coe_toHom, Substructure.mem_top, iff_true]

Result:
case h
L : Language
M : Type w
N : Type u_1
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃[L] N
n : N
⊢ ∃ y, f y = n
-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
theorem genEigenspace_eq_genEigenspace_maxUnifEigenspaceIndex_of_le [IsNoetherian R M]
    (f : End R M) (μ : R) {k : ℕ} (hk : maxUnifEigenspaceIndex f μ ≤ k) :
    f.genEigenspace μ k = f.genEigenspace μ (maxUnifEigenspaceIndex f μ) :=
  le_antisymm
    (genEigenspace_le_genEigenspace_maxUnifEigenspaceIndex _ _ _)
    ((f.genEigenspace μ).monotone <| by simpa using hk)

Proof state:
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : End R M
μ : R
k : ℕ
hk : f.maxUnifEigenspaceIndex μ ≤ k
⊢ ↑(f.maxUnifEigenspaceIndex μ) ≤ ↑k

Tactic:
simpa using hk

Result:
no goals
-- Mathlib/CategoryTheory/Galois/Basic.lean
@[simp]
lemma fiberBinaryProductEquiv_symm_snd_apply {X Y : C} (x : F.obj X) (y : F.obj Y) :
    F.map prod.snd ((fiberBinaryProductEquiv F X Y).symm (x, y)) = y

Proof state:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X Y : C
x : (F.obj X).carrier
y : (F.obj Y).carrier
⊢ ((Types.binaryProductIso (F.obj X).carrier (F.obj Y).carrier).inv ≫
        (PreservesLimitPair.iso (F ⋙ FintypeCat.incl) X Y).inv ≫ (F ⋙ FintypeCat.incl).map prod.snd)
      (x, y) =
    y

Tactic:
erw [PreservesLimitPair.iso_inv_snd, Types.binaryProductIso_inv_comp_snd]

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X Y : C
x : (F.obj X).carrier
y : (F.obj Y).carrier
⊢ F.map prod.snd
      ((PreservesLimitPair.iso (F ⋙ FintypeCat.incl) X Y).inv
        ((Types.binaryProductIso (F.obj X).carrier (F.obj Y).carrier).inv (x, y))) =
    y

Tactic:
change ((Types.binaryProductIso _ _).inv ≫ _ ≫ (F ⋙ FintypeCat.incl).map prod.snd) _ = _

Result:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X Y : C
x : (F.obj X).carrier
y : (F.obj Y).carrier
⊢ ((Types.binaryProductIso (F.obj X).carrier (F.obj Y).carrier).inv ≫
        (PreservesLimitPair.iso (F ⋙ FintypeCat.incl) X Y).inv ≫ (F ⋙ FintypeCat.incl).map prod.snd)
      (x, y) =
    y

Proof state:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X Y : C
x : (F.obj X).carrier
y : (F.obj Y).carrier
⊢ F.map prod.snd ((fiberBinaryProductEquiv F X Y).symm (x, y)) = y

Tactic:
simp only [fiberBinaryProductEquiv, comp_obj, FintypeCat.incl_obj, Iso.toEquiv_comp,
  Equiv.symm_trans_apply, Iso.toEquiv_symm_fun]

Result:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X Y : C
x : (F.obj X).carrier
y : (F.obj Y).carrier
⊢ F.map prod.snd
      ((PreservesLimitPair.iso (F ⋙ FintypeCat.incl) X Y).inv
        ((Types.binaryProductIso (F.obj X).carrier (F.obj Y).carrier).inv (x, y))) =
    y
-- Mathlib/GroupTheory/FreeGroup/Reduce.lean
theorem toWord_of_pow (a : α) (n : ℕ) : (of a ^ n).toWord = List.replicate n (a, true)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
n : ℕ
⊢ Quot.lift reduce ⋯ (mk (List.replicate n (a, true))) = List.replicate n (a, true)

Tactic:
exact reduce_replicate _ _

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
n : ℕ
⊢ (of a ^ n).toWord = List.replicate n (a, true)

Tactic:
rw [of, pow_mk, List.flatten_replicate_singleton, toWord]

Result:
α : Type u_1
inst✝ : DecidableEq α
a : α
n : ℕ
⊢ Quot.lift reduce ⋯ (mk (List.replicate n (a, true))) = List.replicate n (a, true)
-- Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean
theorem IsBigO.mul_atTop_rpow_of_isBigO_rpow {f g : ℝ → E}
    (hf : f =O[atTop] fun t ↦ (t : ℝ) ^ a) (hg : g =O[atTop] fun t ↦ (t : ℝ) ^ b)
    (h : a + b ≤ c) :
    (f * g) =O[atTop] fun t ↦ (t : ℝ) ^ c

Proof state:
E : Type u_2
inst✝ : SeminormedRing E
a b c : ℝ
f g : ℝ → E
hf : f =O[atTop] fun t => t ^ a
hg : g =O[atTop] fun t => t ^ b
h : a + b ≤ c
⊢ ∀ᶠ (x : ℝ) in atTop, ‖x ^ a * x ^ b‖ ≤ x ^ c

Tactic:
filter_upwards [eventually_ge_atTop 1] with t ht

Result:
case h
E : Type u_2
inst✝ : SeminormedRing E
a b c : ℝ
f g : ℝ → E
hf : f =O[atTop] fun t => t ^ a
hg : g =O[atTop] fun t => t ^ b
h : a + b ≤ c
t : ℝ
ht : 1 ≤ t
⊢ ‖t ^ a * t ^ b‖ ≤ t ^ c

Proof state:
case h
E : Type u_2
inst✝ : SeminormedRing E
a b c : ℝ
f g : ℝ → E
hf : f =O[atTop] fun t => t ^ a
hg : g =O[atTop] fun t => t ^ b
h : a + b ≤ c
t : ℝ
ht : 1 ≤ t
⊢ ‖t ^ a * t ^ b‖ ≤ t ^ c

Tactic:
rw [← Real.rpow_add (zero_lt_one.trans_le ht), Real.norm_of_nonneg (Real.rpow_nonneg
  (zero_le_one.trans ht) (a + b))]

Result:
case h
E : Type u_2
inst✝ : SeminormedRing E
a b c : ℝ
f g : ℝ → E
hf : f =O[atTop] fun t => t ^ a
hg : g =O[atTop] fun t => t ^ b
h : a + b ≤ c
t : ℝ
ht : 1 ≤ t
⊢ t ^ (a + b) ≤ t ^ c

Proof state:
E : Type u_2
inst✝ : SeminormedRing E
a b c : ℝ
f g : ℝ → E
hf : f =O[atTop] fun t => t ^ a
hg : g =O[atTop] fun t => t ^ b
h : a + b ≤ c
⊢ (f * g) =O[atTop] fun t => t ^ c

Tactic:
refine (hf.mul hg).trans (Eventually.isBigO ?_)

Result:
E : Type u_2
inst✝ : SeminormedRing E
a b c : ℝ
f g : ℝ → E
hf : f =O[atTop] fun t => t ^ a
hg : g =O[atTop] fun t => t ^ b
h : a + b ≤ c
⊢ ∀ᶠ (x : ℝ) in atTop, ‖x ^ a * x ^ b‖ ≤ x ^ c

Proof state:
case h
E : Type u_2
inst✝ : SeminormedRing E
a b c : ℝ
f g : ℝ → E
hf : f =O[atTop] fun t => t ^ a
hg : g =O[atTop] fun t => t ^ b
h : a + b ≤ c
t : ℝ
ht : 1 ≤ t
⊢ t ^ (a + b) ≤ t ^ c

Tactic:
exact Real.rpow_le_rpow_of_exponent_le ht h

Result:
no goals
-- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
theorem QuadraticMap.isSymm_toMatrix' (Q : QuadraticForm R (n → R)) : Q.toMatrix'.IsSymm

Proof state:
case a
R : Type u_3
n : Type w
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Invertible 2
Q : QuadraticForm R (n → R)
i j : n
⊢ (toMatrix' Q).transpose i j = toMatrix' Q i j

Tactic:
rw [toMatrix', Matrix.transpose_apply, LinearMap.toMatrix₂'_apply, LinearMap.toMatrix₂'_apply,
  ← associated_isSymm]

Result:
no goals

Proof state:
R : Type u_3
n : Type w
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Invertible 2
Q : QuadraticForm R (n → R)
⊢ (toMatrix' Q).IsSymm

Tactic:
ext i j

Result:
case a
R : Type u_3
n : Type w
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Invertible 2
Q : QuadraticForm R (n → R)
i j : n
⊢ (toMatrix' Q).transpose i j = toMatrix' Q i j
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Bootstrap.lean
theorem foldlM_eq_foldlM_toList [Monad m]
    (f : β → α → m β) (init : β) (arr : Array α) :
    arr.foldlM f init = arr.toList.foldlM f init

Proof state:
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
inst✝ : Monad m
f : β → α → m β
init : β
arr : Array α
⊢ foldlM f init arr = List.foldlM f init arr.toList

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem smul [NormedField 𝕜] [NormedSpace 𝕜 β] (hT : DominatedFinMeasAdditive μ T C) (c : 𝕜) :
    DominatedFinMeasAdditive μ (fun s => c • T s) (‖c‖ * C)

Proof state:
α : Type u_1
𝕜 : Type u_6
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝² : SeminormedAddCommGroup β
T : Set α → β
C : ℝ
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 β
hT : DominatedFinMeasAdditive μ T C
c : 𝕜
s : Set α
hs : MeasurableSet s
hμs : μ s < ⊤
⊢ ‖c • T s‖ ≤ ‖c‖ * C * (μ s).toReal

Tactic:
rw [norm_smul, mul_assoc]

Result:
α : Type u_1
𝕜 : Type u_6
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝² : SeminormedAddCommGroup β
T : Set α → β
C : ℝ
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 β
hT : DominatedFinMeasAdditive μ T C
c : 𝕜
s : Set α
hs : MeasurableSet s
hμs : μ s < ⊤
⊢ ‖c‖ * ‖T s‖ ≤ ‖c‖ * (C * (μ s).toReal)

Proof state:
α : Type u_1
𝕜 : Type u_6
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝² : SeminormedAddCommGroup β
T : Set α → β
C : ℝ
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 β
hT : DominatedFinMeasAdditive μ T C
c : 𝕜
⊢ DominatedFinMeasAdditive μ (fun s => c • T s) (‖c‖ * C)

Tactic:
refine ⟨hT.1.smul c, fun s hs hμs => ?_⟩

Result:
α : Type u_1
𝕜 : Type u_6
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝² : SeminormedAddCommGroup β
T : Set α → β
C : ℝ
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 β
hT : DominatedFinMeasAdditive μ T C
c : 𝕜
s : Set α
hs : MeasurableSet s
hμs : μ s < ⊤
⊢ ‖(fun s => c • T s) s‖ ≤ ‖c‖ * C * (μ s).toReal

Proof state:
α : Type u_1
𝕜 : Type u_6
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝² : SeminormedAddCommGroup β
T : Set α → β
C : ℝ
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 β
hT : DominatedFinMeasAdditive μ T C
c : 𝕜
s : Set α
hs : MeasurableSet s
hμs : μ s < ⊤
⊢ ‖(fun s => c • T s) s‖ ≤ ‖c‖ * C * (μ s).toReal

Tactic:
dsimp only

Result:
α : Type u_1
𝕜 : Type u_6
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝² : SeminormedAddCommGroup β
T : Set α → β
C : ℝ
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 β
hT : DominatedFinMeasAdditive μ T C
c : 𝕜
s : Set α
hs : MeasurableSet s
hμs : μ s < ⊤
⊢ ‖c • T s‖ ≤ ‖c‖ * C * (μ s).toReal

Proof state:
α : Type u_1
𝕜 : Type u_6
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝² : SeminormedAddCommGroup β
T : Set α → β
C : ℝ
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 β
hT : DominatedFinMeasAdditive μ T C
c : 𝕜
s : Set α
hs : MeasurableSet s
hμs : μ s < ⊤
⊢ ‖c‖ * ‖T s‖ ≤ ‖c‖ * (C * (μ s).toReal)

Tactic:
exact mul_le_mul le_rfl (hT.2 s hs hμs) (norm_nonneg _) (norm_nonneg _)

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree.lean
@[simp]
lemma leadingCoeff_Ψ₃ (h : (3 : R) ≠ 0) : W.Ψ₃.leadingCoeff = 3

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
h : 3 ≠ 0
⊢ W.Ψ₃.leadingCoeff = 3

Tactic:
rw [leadingCoeff, W.natDegree_Ψ₃ h, coeff_Ψ₃]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean
@[reassoc]
lemma homologyMap_comp : homologyMap (φ ≫ ψ) i = homologyMap φ i ≫ homologyMap ψ i

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
ψ : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
⊢ ShortComplex.homologyMap ((shortComplexFunctor C c i).map (φ ≫ ψ)) =
    ShortComplex.homologyMap ((shortComplexFunctor C c i).map φ) ≫
      ShortComplex.homologyMap ((shortComplexFunctor C c i).map ψ)

Tactic:
rw [Functor.map_comp, ShortComplex.homologyMap_comp]

Result:
no goals

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
ψ : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
⊢ homologyMap (φ ≫ ψ) i = homologyMap φ i ≫ homologyMap ψ i

Tactic:
dsimp [homologyMap]

Result:
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
ψ : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
⊢ ShortComplex.homologyMap ((shortComplexFunctor C c i).map (φ ≫ ψ)) =
    ShortComplex.homologyMap ((shortComplexFunctor C c i).map φ) ≫
      ShortComplex.homologyMap ((shortComplexFunctor C c i).map ψ)
-- Mathlib/Data/Seq/WSeq.lean
theorem bind_assoc (s : WSeq α) (f : α → WSeq β) (g : β → WSeq γ) :
    bind (bind s f) g ~ʷ bind s fun x : α => bind (f x) g

Proof state:
α : Type u
β : Type v
γ : Type w
s : WSeq α
f : α → WSeq β
g : β → WSeq γ
⊢ (map (map g) (map f s)).join.join ~ʷ (map (fun x => (map g (f x)).join) s).join

Tactic:
erw [← map_comp f (map g), map_comp (map g ∘ f) join]

Result:
α : Type u
β : Type v
γ : Type w
s : WSeq α
f : α → WSeq β
g : β → WSeq γ
⊢ (map (map g ∘ f) s).join.join ~ʷ (map join (map (map g ∘ f) s)).join

Proof state:
α : Type u
β : Type v
γ : Type w
s : WSeq α
f : α → WSeq β
g : β → WSeq γ
⊢ (map (map g ∘ f) s).join.join ~ʷ (map join (map (map g ∘ f) s)).join

Tactic:
apply join_join

Result:
no goals

Proof state:
α : Type u
β : Type v
γ : Type w
s : WSeq α
f : α → WSeq β
g : β → WSeq γ
⊢ (s.bind f).bind g ~ʷ s.bind fun x => (f x).bind g

Tactic:
simp only [bind, map_join]

Result:
α : Type u
β : Type v
γ : Type w
s : WSeq α
f : α → WSeq β
g : β → WSeq γ
⊢ (map (map g) (map f s)).join.join ~ʷ (map (fun x => (map g (f x)).join) s).join
-- Mathlib/RingTheory/Polynomial/Pochhammer.lean
theorem descPochhammer_ne_zero_eval_zero {n : ℕ} (h : n ≠ 0) : (descPochhammer R n).eval 0 = 0

Proof state:
R : Type u
inst✝ : Ring R
n : ℕ
h : n ≠ 0
⊢ eval 0 (descPochhammer R n) = 0

Tactic:
simp [descPochhammer_eval_zero, h]

Result:
no goals
-- Mathlib/Algebra/Ring/BooleanRing.lean
theorem inf_assoc (a b c : α) : a ⊓ b ⊓ c = a ⊓ (b ⊓ c)

Proof state:
α : Type u_1
inst✝ : BooleanRing α
a b c : α
⊢ a * b * c = a * (b * c)

Tactic:
ring

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem toArray_eq_append_iff {xs : List α} {as bs : Array α} :
    xs.toArray = as ++ bs ↔ xs = as.toList ++ bs.toList

Proof state:
α : Type u_1
xs : List α
as bs : Array α
⊢ xs.toArray = as ++ bs ↔ xs = as.toList ++ bs.toList

Tactic:
cases as

Result:
case mk
α : Type u_1
xs : List α
bs : Array α
toList✝ : List α
⊢ xs.toArray = { toList := toList✝ } ++ bs ↔ xs = { toList := toList✝ }.toList ++ bs.toList

Proof state:
case mk.mk
α : Type u_1
xs toList✝¹ toList✝ : List α
⊢ xs.toArray = { toList := toList✝¹ } ++ { toList := toList✝ } ↔
    xs = { toList := toList✝¹ }.toList ++ { toList := toList✝ }.toList

Tactic:
simp

Result:
no goals

Proof state:
case mk
α : Type u_1
xs : List α
bs : Array α
toList✝ : List α
⊢ xs.toArray = { toList := toList✝ } ++ bs ↔ xs = { toList := toList✝ }.toList ++ bs.toList

Tactic:
cases bs

Result:
case mk.mk
α : Type u_1
xs toList✝¹ toList✝ : List α
⊢ xs.toArray = { toList := toList✝¹ } ++ { toList := toList✝ } ↔
    xs = { toList := toList✝¹ }.toList ++ { toList := toList✝ }.toList
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem isInt_rpow_neg {a b : ℝ} {nb ne : ℕ}
    (pb : IsInt b (Int.negOfNat nb)) (pe' : IsInt (a ^ (Int.negOfNat nb)) (Int.negOfNat ne)) :
    IsInt (a ^ b) (Int.negOfNat ne)

Proof state:
a b : ℝ
nb ne : ℕ
pb : IsInt b (Int.negOfNat nb)
pe' : IsInt (a ^ Int.negOfNat nb) (Int.negOfNat ne)
⊢ IsInt (a ^ b) (Int.negOfNat ne)

Tactic:
rwa [pb.out, Real.rpow_intCast]

Result:
no goals
-- Mathlib/Data/List/TakeWhile.lean
lemma find?_eq_head_dropWhile_not (h : ∃ x ∈ l, p x) :
    l.find? p = some ((l.dropWhile (fun x ↦ ! (p x))).head (by simpa using h))

Proof state:
α : Type u_1
p : α → Bool
l : List α
h : ∃ x, x ∈ l ∧ p x = true
⊢ dropWhile (fun x => !p x) l ≠ []

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
l : List α
h : ∃ x, x ∈ l ∧ p x = true
⊢ find? p l = some ((dropWhile (fun x => !p x) l).head ⋯)

Tactic:
rw [l.find?_eq_head?_dropWhile_not p, ← head_eq_iff_head?_eq_some]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Abs.lean
theorem HasFDerivAt.abs_of_neg (hf : HasFDerivAt f f' x)
    (h₀ : f x < 0) : HasFDerivAt (fun x ↦ |f x|) (-f') x

Proof state:
case h.e'_12
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : E →L[ℝ] ℝ
x : E
hf : HasFDerivAt f f' x
h₀ : f x < 0
⊢ -f' = (ContinuousLinearMap.smulRight 1 (-1)).comp f'

Tactic:
ext y

Result:
case h.e'_12.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : E →L[ℝ] ℝ
x : E
hf : HasFDerivAt f f' x
h₀ : f x < 0
y : E
⊢ (-f') y = ((ContinuousLinearMap.smulRight 1 (-1)).comp f') y

Proof state:
case h.e'_12.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : E →L[ℝ] ℝ
x : E
hf : HasFDerivAt f f' x
h₀ : f x < 0
y : E
⊢ (-f') y = ((ContinuousLinearMap.smulRight 1 (-1)).comp f') y

Tactic:
simp

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : E →L[ℝ] ℝ
x : E
hf : HasFDerivAt f f' x
h₀ : f x < 0
⊢ HasFDerivAt (fun x => |f x|) (-f') x

Tactic:
convert (hasDerivAt_abs_neg h₀).hasFDerivAt.comp x hf using 1

Result:
case h.e'_12
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : E →L[ℝ] ℝ
x : E
hf : HasFDerivAt f f' x
h₀ : f x < 0
⊢ -f' = (ContinuousLinearMap.smulRight 1 (-1)).comp f'
-- Mathlib/Order/SymmDiff.lean
theorem symmDiff_sup_inf : a ∆ b ⊔ a ⊓ b = a ⊔ b

Proof state:
case refine_1
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ≤ a \ b ⊔ b ⊔ b \ a

Tactic:
exact le_sup_of_le_left le_sdiff_sup

Result:
no goals

Proof state:
case refine_1
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ≤ a \ b ⊔ b \ a ⊔ b

Tactic:
rw [sup_right_comm]

Result:
case refine_1
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ≤ a \ b ⊔ b ⊔ b \ a

Proof state:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ⊔ b ≤ (a \ b ⊔ b \ a ⊔ a) ⊓ (a \ b ⊔ b \ a ⊔ b)

Tactic:
refine sup_le (le_inf le_sup_right ?_) (le_inf ?_ le_sup_right)

Result:
case refine_1
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ≤ a \ b ⊔ b \ a ⊔ b

case refine_2
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ b ≤ a \ b ⊔ b \ a ⊔ a

Proof state:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ⊔ b ≤ a ∆ b ⊔ a ⊓ b

Tactic:
rw [sup_inf_left, symmDiff]

Result:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ⊔ b ≤ (a \ b ⊔ b \ a ⊔ a) ⊓ (a \ b ⊔ b \ a ⊔ b)

Proof state:
case refine_2
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ b ≤ a \ b ⊔ b \ a ⊔ a

Tactic:
rw [sup_assoc]

Result:
case refine_2
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ b ≤ a \ b ⊔ (b \ a ⊔ a)

Proof state:
case refine_2
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ b ≤ a \ b ⊔ (b \ a ⊔ a)

Tactic:
exact le_sup_of_le_right le_sdiff_sup

Result:
no goals

Proof state:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ∆ b ⊔ a ⊓ b = a ⊔ b

Tactic:
refine le_antisymm (sup_le symmDiff_le_sup inf_le_sup) ?_

Result:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ⊔ b ≤ a ∆ b ⊔ a ⊓ b
-- Mathlib/Algebra/Homology/ShortComplex/Homology.lean
@[reassoc (attr := simp)]
lemma homologyι_naturality (φ : S₁ ⟶ S₂) [S₁.HasHomology] [S₂.HasHomology] :
    homologyMap φ ≫ S₂.homologyι = S₁.homologyι ≫ S₁.opcyclesMap φ

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
⊢ S₁.rightHomologyι ≫ opcyclesMap φ = S₁.rightHomologyIso.hom ≫ S₁.homologyι ≫ opcyclesMap φ

Tactic:
simp only [homologyι, assoc, Iso.hom_inv_id_assoc]

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
⊢ homologyMap φ ≫ S₂.homologyι = S₁.homologyι ≫ opcyclesMap φ

Tactic:
simp only [← cancel_epi S₁.rightHomologyIso.hom, rightHomologyIso_hom_naturality_assoc φ,
  rightHomologyIso_hom_comp_homologyι, rightHomologyι_naturality]

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
⊢ S₁.rightHomologyι ≫ opcyclesMap φ = S₁.rightHomologyIso.hom ≫ S₁.homologyι ≫ opcyclesMap φ